Merge pull request #814 from viperproject/meilers_asserting

marcoeilers · web-flow · commit 08c001b33dec · 2024-11-13T19:51:37.000+01:00
New "asserting" expression
diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
@@ -499,6 +499,11 @@ case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition,
   lazy val typ = body.typ
 }
 
+case class Asserting(a: Exp, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
+  override lazy val check: Seq[ConsistencyError] = Consistency.checkPure(body)
+  lazy val typ = body.typ
+}
+
 // --- Old expressions
 
 sealed trait OldExp extends UnExp {
diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -771,6 +771,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(ass, exp) =>
+        parens(text("asserting") <+> nest(defaultIndent, parens(show(ass))) <+> "in" <> nest(defaultIndent, line <> show(exp)))
       case Old(exp) =>
         text("old") <> parens(show(exp))
       case LabelledOld(exp,label) =>
diff --git a/src/main/scala/viper/silver/ast/utility/Expressions.scala b/src/main/scala/viper/silver/ast/utility/Expressions.scala
@@ -25,6 +25,7 @@ object Expressions {
     case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
     case unf: Unfolding => isPure(unf.body)
     case app: Applying => isPure(app.body)
+    case Asserting(a, e) => isPure(e)
     case QuantifiedExp(_, e0) => isPure(e0)
     case Let(_, _, body) => isPure(body)
     case e: ExtensionExp => e.extensionIsPure
@@ -96,9 +97,10 @@ object Expressions {
   def asBooleanExp(e: Exp): Exp = {
     e.transform({
       case _: AccessPredicate | _: MagicWand => TrueLit()()
-      case fa@Forall(vs,ts,body) => Forall(vs,ts,asBooleanExp(body))(fa.pos,fa.info)
+      case fa@Forall(vs,ts,body) => Forall(vs, ts, asBooleanExp(body))(fa.pos, fa.info, fa.errT)
       case Unfolding(_, exp) => asBooleanExp(exp)
       case Applying(_, exp) => asBooleanExp(exp)
+      case ass@Asserting(a, exp) => Asserting(asBooleanExp(a), asBooleanExp(exp))(ass.pos, ass.info, ass.errT)
     })
   }
 
@@ -199,6 +201,7 @@ object Expressions {
           case MapLookup(m, k) => List(MapContains(k, m)(p))
           case Unfolding(pred, _) => List(pred)
           case Applying(wand, _) => List(wand)
+          case Asserting(a, _) => List(a)
           case _ => Nil
         }
         // Only use non-trivial conditions for the subnodes.
diff --git a/src/main/scala/viper/silver/ast/utility/Nodes.scala b/src/main/scala/viper/silver/ast/utility/Nodes.scala
@@ -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(ass, body) => Seq(ass, body)
           case Old(exp) => Seq(exp)
           case CondExp(cond, thn, els) => Seq(cond, thn, els)
           case Let(v, exp, body) => Seq(v, exp, body)
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -152,7 +152,7 @@ object FastParserCompanion {
     // maps
     PKw.Map, PKwOp.Range, PKwOp.Domain,
     // prover hint expressions
-    PKwOp.Unfolding, PKwOp.In, PKwOp.Applying,
+    PKwOp.Unfolding, PKwOp.In, PKwOp.Applying, PKwOp.Asserting,
     // old expression
     PKwOp.Old, PKw.Lhs,
     // other expressions
@@ -365,7 +365,7 @@ class FastParser {
   def atomReservedKw[$: P]: P[PExp] = {
     reservedKwMany(
       StringIn("true", "false", "null", "old", "result", "acc", "none", "wildcard", "write", "epsilon", "perm", "let", "forall", "exists", "forperm",
-        "unfolding", "applying", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
+        "unfolding", "applying", "asserting", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
       str => pos => str match {
         case "true" => Pass.map(_ => PBoolLit(PReserved(PKw.True)(pos))(_))
         case "false" => Pass.map(_ => PBoolLit(PReserved(PKw.False)(pos))(_))
@@ -384,6 +384,7 @@ class FastParser {
         case "forperm" => forperm.map(_(PReserved(PKw.Forperm)(pos)))
         case "unfolding" => unfolding.map(_(PReserved(PKwOp.Unfolding)(pos)))
         case "applying" => applying.map(_(PReserved(PKwOp.Applying)(pos)))
+        case "asserting" => asserting.map(_(PReserved(PKwOp.Asserting)(pos)))
         case "Set" => setConstructor.map(_(PReserved(PKwOp.Set)(pos)))
         case "Seq" => seqConstructor.map(_(PReserved(PKwOp.Seq)(pos)))
         case "Multiset" => multisetConstructor.map(_(PReserved(PKwOp.Multiset)(pos)))
@@ -652,6 +653,10 @@ class FastParser {
       PApplying(_, wand.inner, op, b)
   }
 
+  def asserting[$: P]: P[PKwOp.Asserting => Pos => PExp] = P(exp.parens ~ PKwOp.In ~ exp).map {
+    case (a, in, b) => PAsserting(_, a.inner, in, b)
+  }
+
   def predicateAccessAssertion[$: P]: P[PAccAssertion] = P(accessPred | predAcc)
 
   def setConstructor[$: P]: P[PKwOp.Set => Pos => PExp] =
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1080,6 +1080,12 @@ case class PApplying(applying: PKwOp.Applying, wand: PExp, in: PKwOp.In, exp: PE
     List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
 }
 
+case class PAsserting(asserting: PKwOp.Asserting, a: PExp, in: PKwOp.In, exp: PExp)(val pos: (Position, Position)) extends PHeapOpApp {
+  override val args = Seq(a, exp)
+  override val signatures: List[PTypeSubstitution] =
+    List(Map(POpApp.pArgS(0) -> Impure, POpApp.pResS -> POpApp.pArg(1)))
+}
+
 sealed trait PBinder extends PExp with PScope {
   def boundVars: Seq[PLogicalVarDecl]
 
diff --git a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
@@ -494,6 +494,8 @@ object PKwOp {
   type Unfolding = PReserved[Unfolding.type]
   case object Applying    extends PKwOp("applying")                 with PKeywordAtom with RightSpace
   type Applying = PReserved[Applying.type]
+  case object Asserting   extends PKwOp("asserting")                with PKeywordAtom with RightSpace
+  type Asserting = PReserved[Asserting.type]
   case object Let         extends PKwOp("let")                      with PKeywordAtom with RightSpace
   type Let = PReserved[Let.type]
 
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
@@ -513,6 +513,8 @@ case class Translator(program: PProgram) {
         Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos, info)
       case PApplying(_, wand, _, e) =>
         Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos, info)
+      case PAsserting(_, a, _, e) =>
+        Asserting(exp(a), exp(e))(pos, info)
       case pl@PLet(_, _, _, exp1, _, PLetNestedScope(body)) =>
         Let(liftLogicalDecl(pl.decl), exp(exp1.inner), exp(body))(pos, info)
       case _: PLetNestedScope =>
diff --git a/src/test/resources/all/asserting/function.vpr b/src/test/resources/all/asserting/function.vpr
@@ -0,0 +1,38 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function fplusone(x: Ref, y: Ref): Int
+    requires acc(x.f)
+{
+  asserting (x != null) in (x.f + 1)
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fplusone2(x: Ref, y: Ref): Int
+    requires acc(x.f)
+{
+  asserting (x != y) in (x.f + 1)
+}
+
+method main()
+{
+  var x: Ref
+  x := new(f)
+
+  var hmm: Int
+  hmm := fplusone(x, x)
+  hmm := asserting (hmm == x.f + 1) in hmm
+}
+
+method main2()
+{
+  var x: Ref
+  x := new(f)
+
+  var hmm: Int
+  hmm := fplusone(x, x)
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  hmm := asserting (hmm == x.f) in hmm
+}
diff --git a/src/test/resources/all/asserting/other-fail.vpr b/src/test/resources/all/asserting/other-fail.vpr
@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+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
+}
diff --git a/src/test/resources/all/asserting/qp.vpr b/src/test/resources/all/asserting/qp.vpr
@@ -0,0 +1,44 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method m1(s: Set[Ref])
+  requires |s| > 0
+{
+  inhale forall x: Ref :: x in (asserting(|s| > 0) in s) ==> acc(x.f)
+}
+
+method m1Fail(s: Set[Ref])
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in (asserting(|s| > 0) in s) ==> acc(x.f)
+}
+
+method m2(s: Set[Ref])
+  requires |s| > 0
+  requires !(null in s)
+{
+  inhale forall x: Ref :: x in s ==> acc((asserting (x != null) in x).f)
+}
+
+method m2Fail(s: Set[Ref])
+  requires |s| > 0
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in s ==> acc((asserting (x != null) in x).f)
+}
+
+method m3(s: Set[Ref])
+  requires |s| > 0
+  requires !(null in s)
+{
+  inhale forall x: Ref :: x in s ==> acc(x.f, asserting (x != null) in write)
+}
+
+method m3Fail(s: Set[Ref])
+  requires |s| > 0
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in s ==> acc(x.f, asserting (x != null) in write)
+}
diff --git a/src/test/resources/all/asserting/simple-fail.vpr b/src/test/resources/all/asserting/simple-fail.vpr
@@ -0,0 +1,73 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method assign() {
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (false) in 0
+}
+
+method assign2(i: Int) {
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (i > 0) in 0
+}
+
+method assign3(i: Int)
+  requires i > 5
+{
+  var x: Int := asserting (i > 0) in 0
+}
+
+method pres()
+  //:: ExpectedOutput(not.wellformed:assertion.false)
+  requires asserting (false) in false
+{
+  assert false
+}
+
+method pres2(x: Ref)
+  //:: ExpectedOutput(not.wellformed:insufficient.permission)
+  requires asserting (acc(x.f)) in false
+{
+  assert false
+}
+
+method pres3(x: Ref)
+  requires acc(x.f)
+  requires asserting (acc(x.f)) in false
+{
+  assert false
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun(): Int
+{
+  asserting (false) in 0
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function fun2(x: Ref): Int
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun3(x: Ref): Int
+  requires acc(x.f)
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+function fun4(x: Ref): Int
+  requires acc(x.f) && x.f > 8
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+method stateUnchanged(x: Ref)
+  requires acc(x.f)
+{
+  var y: Int := asserting (acc(x.f)) in x.f
+  assert acc(x.f)
+}
diff --git a/src/test/resources/all/asserting/trigger.vpr b/src/test/resources/all/asserting/trigger.vpr
@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function trigger(i: Int): Bool
+{
+  true
+}
+
+method triggerUse(s: Seq[Int])
+  requires |s| > 0
+  requires forall i: Int :: {trigger(i)} 0 <= i < |s| ==> s[i] > 0
+{
+  assert asserting (trigger(0)) in s[0] > 0
+}
+
+method triggerUse2(s: Seq[Int])
+  requires |s| > 0
+  requires forall i: Int :: {trigger(i)} 0 <= i < |s| ==> s[i] > 0
+{
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert s[0] > 0
+}
diff --git a/src/test/resources/all/asserting/wand.vpr b/src/test/resources/all/asserting/wand.vpr
@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+field g: Int
+
+method test0(x: Ref)
+{
+    package acc(x.f) && (asserting (acc(x.f)) in (x.f == 0)) --* acc(x.f) {}
+}
+
+method test1(x: Ref)
+{
+    //:: ExpectedOutput(package.failed:insufficient.permission)
+    package acc(x.f) && (asserting (acc(x.g)) in (x.f == 0)) --* acc(x.f) {}
+}
+
