Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

asserting in expressions (take 2) #663

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 10 additions & 5 deletions src/main/scala/viper/silver/ast/Expression.scala
Original file line number Diff line number Diff line change
Expand Up @@ -483,17 +483,22 @@ case class CondExp(cond: Exp, thn: Exp, els: Exp)(val pos: Position = NoPosition
}

// --- Prover hint expressions

case class Unfolding(acc: PredicateAccessPredicate, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
/** Prover hint expressions. eg unfolding in */
sealed trait HintExp extends Exp {
val body: Exp
override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(body)
lazy val typ = body.typ
lazy val typ: Type = body.typ
}

case class Unfolding(acc: PredicateAccessPredicate, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends HintExp {
}

case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends HintExp {
override lazy val check : Seq[ConsistencyError] = (if(!(wand isSubtype Wand)) Seq(ConsistencyError(s"Expected wand but found ${wand.typ} ($wand)", wand.pos)) else Seq()) ++ Consistency.checkPure(body)
lazy val typ = body.typ
}

case class Asserting(assertion: Exp, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends HintExp {}

// --- Old expressions

sealed trait OldExp extends UnExp {
Expand Down
2 changes: 2 additions & 0 deletions src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -741,6 +741,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
group(parens(text("unfolding") <+> nest(defaultIndent, show(acc)) <+> "in" <> nest(defaultIndent, line <> show(exp))))
case Applying(wand, exp) =>
parens(text("applying") <+> nest(defaultIndent, show(wand)) <+> "in" <> nest(defaultIndent, line <> show(exp)))
case Asserting(assertion, exp) =>
parens(text("asserting") <+> nest(defaultIndent, parens(show(assertion))) <+> "in" <+> show(exp))
case Old(exp) =>
text("old") <> parens(show(exp))
case LabelledOld(exp,label) =>
Expand Down
3 changes: 1 addition & 2 deletions src/main/scala/viper/silver/ast/utility/Consistency.scala
Original file line number Diff line number Diff line change
Expand Up @@ -221,8 +221,7 @@ object Consistency {
}

def noGhostOperations(n: Node) = !n.existsDefined {
case u: Unfolding if !u.isPure =>
case a: Applying if !a.isPure =>
case h: HintExp if !h.isPure =>
}

/** Returns true iff the given expression is a valid trigger. */
Expand Down
3 changes: 1 addition & 2 deletions src/main/scala/viper/silver/ast/utility/Expressions.scala
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,7 @@ object Expressions {
case InhaleExhaleExp(in, ex) => isPure(in) && isPure(ex)
case BinExp(e0, e1) => isPure(e0) && isPure(e1)
case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
case unf: Unfolding => isPure(unf.body)
case app: Applying => isPure(app.body)
case h: HintExp => isPure(h.body)
case QuantifiedExp(_, e0) => isPure(e0)
case Let(_, _, body) => isPure(body)
case e: ExtensionExp => e.extensionIsPure
Expand Down
1 change: 1 addition & 0 deletions src/main/scala/viper/silver/ast/utility/Nodes.scala
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,7 @@ object Nodes {
case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc, perm)
case Unfolding(acc, body) => Seq(acc, body)
case Applying(wand, body) => Seq(wand, body)
case Asserting(assertion, body) => Seq(assertion, body)
case Old(exp) => Seq(exp)
case CondExp(cond, thn, els) => Seq(cond, thn, els)
case Let(v, exp, body) => Seq(v, exp, body)
Expand Down
7 changes: 5 additions & 2 deletions src/main/scala/viper/silver/parser/FastParser.scala
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ object FastParserCompanion {
// maps
"Map", "range",
// prover hint expressions
"unfolding", "in", "applying",
"unfolding", "in", "applying", "asserting",
// old expression
"old", "lhs",
// other expressions
Expand Down Expand Up @@ -796,7 +796,7 @@ class FastParser {
// and then look like an `fapp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut)
def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | integer | booltrue | boolfalse | nul | old
| result | unExp | typedFapp
| "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying
| "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying | asserting
| setTypedEmpty | explicitSetNonEmpty | multiSetTypedEmpty | explicitMultisetNonEmpty | seqTypedEmpty
| size | explicitSeqNonEmpty | seqRange
| mapTypedEmpty | explicitMapNonEmpty | mapDomain | mapRange
Expand Down Expand Up @@ -1210,6 +1210,9 @@ class FastParser {

def applying[_: P]: P[PExp] = FP(keyword("applying") ~/ "(" ~ magicWandExp ~ ")" ~ "in" ~ exp).map { case (pos, (a, b)) => PApplying(a, b)(pos) }


def asserting[_: P]: P[PExp] = FP(keyword("asserting") ~/ "(" ~ exp ~ ")" ~ "in" ~ exp).map { case (pos, (a, b)) => PAsserting(a, b)(pos) }

def programDecl(implicit ctx : P[_]) : P[PProgram] = P(FP((ParserExtension.newDeclAtStart(ctx) | preambleImport | defineDecl | domainDecl | fieldDecl | functionDecl | predicateDecl | methodDecl | ParserExtension.newDeclAtEnd(ctx)).rep).map {
case (pos, decls) => {
PProgram(
Expand Down
8 changes: 8 additions & 0 deletions src/main/scala/viper/silver/parser/ParseAst.scala
Original file line number Diff line number Diff line change
Expand Up @@ -717,6 +717,13 @@ case class PApplying(wand: PExp, exp: PExp)(val pos: (Position, Position)) exten
List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
}

case class PAsserting(assertion: PExp, exp: PExp)(val pos: (Position, Position)) extends POpApp {
override val opName = "applying"
dewert99 marked this conversation as resolved.
Show resolved Hide resolved
override val args = Seq(assertion, exp)
override val signatures : List[PTypeSubstitution] =
List(Map(POpApp.pArgS(0) -> Bool, POpApp.pResS -> POpApp.pArg(1)))
}

sealed trait PBinder extends PExp{
def body:PExp
var _typeSubstitutions : List[PTypeSubstitution] = null
Expand Down Expand Up @@ -1255,6 +1262,7 @@ object Nodes {
case PCall(func, args, optType) => Seq(func) ++ args ++ (optType match { case Some(t) => Seq(t) case None => Nil})
case PUnfolding(acc, exp) => Seq(acc, exp)
case PApplying(wand, exp) => Seq(wand, exp)
case PAsserting(assertion, exp) => Seq(assertion, exp)
case PExists(vars, triggers, exp) => vars ++ triggers ++ Seq(exp)
case PLabelledOld(id, e) => Seq(id, e)
case po: POldExp => Seq(po.e)
Expand Down
1 change: 1 addition & 0 deletions src/main/scala/viper/silver/parser/Transformer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ object Transformer {

case p@PUnfolding(acc, exp) => PUnfolding(go(acc), go(exp))(p.pos)
case p@PApplying(wand, exp) => PApplying(go(wand), go(exp))(p.pos)
case p@PAsserting(assertion, exp) => PAsserting(go(assertion), go(exp))(p.pos)

case p@PExists(vars, triggers, exp) => PExists(vars map go, triggers map go, go(exp))(p.pos)
case p@PForall(vars, triggers, exp) => PForall(vars map go, triggers map go, go(exp))(p.pos)
Expand Down
2 changes: 2 additions & 0 deletions src/main/scala/viper/silver/parser/Translator.scala
Original file line number Diff line number Diff line change
Expand Up @@ -442,6 +442,8 @@ case class Translator(program: PProgram) {
Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos)
case PApplying(wand, e) =>
Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos)
case PAsserting(a, e) =>
Asserting(exp(a), exp(e))(pos)
case PLet(exp1, PLetNestedScope(variable, body)) =>
Let(liftVarDecl(variable), exp(exp1), exp(body))(pos)
case _: PLetNestedScope =>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,26 +6,26 @@

package viper.silver.plugin.standard.termination

import fastparse._
import viper.silver.ast.utility.ViperStrategy
import viper.silver.ast.utility.rewriter.{SimpleContext, Strategy, StrategyBuilder}
import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
import viper.silver.ast.{Assert, CondExp, CurrentPerm, Exp, Function, HintExp, InhaleExhaleExp, MagicWand, Method, Node, Program, While}
import viper.silver.parser.FastParserCompanion.whitespace
import viper.silver.parser._
import viper.silver.plugin.standard.predicateinstance.PPredicateInstance
import viper.silver.plugin.standard.termination.transformation.Trafo
import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
import viper.silver.verifier.errors.{AssertFailed, PreconditionInAppFalse}
import viper.silver.verifier._
import fastparse._
import viper.silver.parser.FastParserCompanion.whitespace
import viper.silver.reporter.Entity
import viper.silver.verifier._
import viper.silver.verifier.errors.AssertFailed

import scala.annotation.unused

class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
@unused logger: ch.qos.logback.classic.Logger,
config: viper.silver.frontend.SilFrontendConfig,
fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
import fp.{FP, keyword, exp, ParserExtension}
import fp.{FP, ParserExtension, exp, keyword}

private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false)

Expand Down Expand Up @@ -246,8 +246,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
case _ =>
}).recurseFunc({
case CondExp(_, e1, e2) => Seq(e1, e2)
case Applying(_, exp) => Seq(exp)
case Unfolding(_, exp) => Seq(exp)
case h: HintExp => Seq(h.body)
case CurrentPerm(_) => Nil
})
}
Original file line number Diff line number Diff line change
Expand Up @@ -167,9 +167,8 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
}

private val toPureBooleanExpRecursion: PartialFunction[Node, Seq[Node]] = {
case Unfolding(_, body) => Seq(body)
case h: HintExp => Seq(h.body)
case _: AccessPredicate | _: MagicWand => Nil
case Applying(_, b) => Seq(b)
case Forall(_, _, exp) => Seq(exp)
}

Expand Down
16 changes: 16 additions & 0 deletions src/test/resources/all/asserting-in/other-fail.vpr
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
field x: Int

method test1() {
//:: ExpectedOutput(assert.failed:division.by.zero)
assert asserting (1 / 0 == 0) in true
}

method test2() {
//:: ExpectedOutput(assert.failed:division.by.zero)
assert asserting (true) in (1 / 0 == 0)
}

method test3(r: Ref) {
//:: ExpectedOutput(assert.failed:insufficient.permission)
assert asserting (true && acc(r.x)) in true
}
7 changes: 7 additions & 0 deletions src/test/resources/all/asserting-in/pass.vpr
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
field x: Int

method test1(r: Ref) returns (y: Int)
requires acc(r.x)
ensures acc(r.x) && y == r.x {
y := asserting (acc(r.x)) in r.x
}
15 changes: 15 additions & 0 deletions src/test/resources/all/asserting-in/simple-fail.vpr
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
method assign() {
//:: ExpectedOutput(assignment.failed:assertion.false)
var x: Int := asserting (false) in 0
}

method pres()
//:: ExpectedOutput(not.wellformed:assertion.false)
requires asserting (false) in false {
assert false
}

//:: ExpectedOutput(function.not.wellformed:assertion.false)
function fun(): Int {
asserting (false) in 0
}
5 changes: 5 additions & 0 deletions src/test/resources/all/asserting-in/wand.vpr
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
field f: Int

method test0(x: Ref) {
package acc(x.f) && (asserting (acc(x.f)) in (x.f == 0)) --* acc(x.f) {}
}