From a06efe037aa2da7fa815e7b914a236762e58b577 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 26 Sep 2024 21:01:20 +0200 Subject: [PATCH 1/2] asserting (a) in e --- src/main/scala/viper/silver/ast/Expression.scala | 5 +++++ .../scala/viper/silver/ast/pretty/PrettyPrinter.scala | 2 ++ .../scala/viper/silver/ast/utility/Expressions.scala | 5 ++++- src/main/scala/viper/silver/ast/utility/Nodes.scala | 1 + src/main/scala/viper/silver/parser/FastParser.scala | 9 +++++++-- src/main/scala/viper/silver/parser/ParseAst.scala | 6 ++++++ src/main/scala/viper/silver/parser/ParseAstKeyword.scala | 2 ++ src/main/scala/viper/silver/parser/Translator.scala | 2 ++ 8 files changed, 29 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala index 0d206d9ae..1b64f482b 100644 --- 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 index 2003fd387..64e1db3f4 100644 --- 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 index b4fa7c980..df83efbae 100644 --- 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 index 0dc99d7dd..53759e73c 100644 --- 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 index dfc503ef5..eae845045 100644 --- 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 index 4e59f54c4..cc4fd40d5 100644 --- 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 index 646c14819..daed9a67f 100644 --- 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 index 4a6f469d2..91653fb3d 100644 --- 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 => From f649c0baf2fc133a5d99261dbb567b8a33732588 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 27 Sep 2024 10:53:00 +0200 Subject: [PATCH 2/2] Adding tests --- src/test/resources/all/asserting/function.vpr | 38 ++++++++++ .../resources/all/asserting/other-fail.vpr | 19 +++++ src/test/resources/all/asserting/qp.vpr | 44 +++++++++++ .../resources/all/asserting/simple-fail.vpr | 73 +++++++++++++++++++ src/test/resources/all/asserting/trigger.vpr | 22 ++++++ src/test/resources/all/asserting/wand.vpr | 17 +++++ 6 files changed, 213 insertions(+) create mode 100644 src/test/resources/all/asserting/function.vpr create mode 100644 src/test/resources/all/asserting/other-fail.vpr create mode 100644 src/test/resources/all/asserting/qp.vpr create mode 100644 src/test/resources/all/asserting/simple-fail.vpr create mode 100644 src/test/resources/all/asserting/trigger.vpr create mode 100644 src/test/resources/all/asserting/wand.vpr diff --git a/src/test/resources/all/asserting/function.vpr b/src/test/resources/all/asserting/function.vpr new file mode 100644 index 000000000..144a7e4ab --- /dev/null +++ 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 +} \ No newline at end of file diff --git a/src/test/resources/all/asserting/other-fail.vpr b/src/test/resources/all/asserting/other-fail.vpr new file mode 100644 index 000000000..465a83c9e --- /dev/null +++ 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 +} \ No newline at end of file diff --git a/src/test/resources/all/asserting/qp.vpr b/src/test/resources/all/asserting/qp.vpr new file mode 100644 index 000000000..474714a95 --- /dev/null +++ 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) +} \ No newline at end of file diff --git a/src/test/resources/all/asserting/simple-fail.vpr b/src/test/resources/all/asserting/simple-fail.vpr new file mode 100644 index 000000000..5c5791f5d --- /dev/null +++ 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) +} \ No newline at end of file diff --git a/src/test/resources/all/asserting/trigger.vpr b/src/test/resources/all/asserting/trigger.vpr new file mode 100644 index 000000000..f27f14fab --- /dev/null +++ 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 +} \ No newline at end of file diff --git a/src/test/resources/all/asserting/wand.vpr b/src/test/resources/all/asserting/wand.vpr new file mode 100644 index 000000000..67a026f8e --- /dev/null +++ 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) {} +} +