From 92425f2e247a15e50dcec6bdabf4b6988a8486c7 Mon Sep 17 00:00:00 2001 From: Robby Date: Mon, 11 Sep 2023 12:12:31 -0500 Subject: [PATCH] Premise now adds to path conditions without runtime-checking (assumed). Need to fix evalConstructor. --- .../org/sireum/logika/example/field-access.sc | 6 +++++- .../scala/org/sireum/logika/example/oop.sc | 4 ++-- .../org/sireum/logika/example/premise.sc | 4 ++-- .../main/scala/org/sireum/logika/Logika.scala | 20 +++++++++++++------ .../org/sireum/logika/plugin/AutoPlugin.scala | 4 ++-- 5 files changed, 25 insertions(+), 13 deletions(-) diff --git a/jvm/src/test/scala/org/sireum/logika/example/field-access.sc b/jvm/src/test/scala/org/sireum/logika/example/field-access.sc index ddb4e124..2a655fdc 100644 --- a/jvm/src/test/scala/org/sireum/logika/example/field-access.sc +++ b/jvm/src/test/scala/org/sireum/logika/example/field-access.sc @@ -30,7 +30,11 @@ Deduce( Old(baz) ≡ Baz(Foo(0), Bar(10), 100)(foo = Baz(Foo(0), Bar(10), 100).foo(x = 1) ) by Premise, - baz ≡ Old(baz)(bar = Bar(2)) by Premise + baz ≡ Baz( + Foo(1), + Baz(Foo(0), Bar(10), 100).bar, + Baz(Foo(0), Bar(10), 100).z + )(bar = Bar(2)) by Premise ) assert(baz.foo.x == 1 & baz.bar.y == 2 & baz.z == 100) diff --git a/jvm/src/test/scala/org/sireum/logika/example/oop.sc b/jvm/src/test/scala/org/sireum/logika/example/oop.sc index 576756f9..e28f51a4 100644 --- a/jvm/src/test/scala/org/sireum/logika/example/oop.sc +++ b/jvm/src/test/scala/org/sireum/logika/example/oop.sc @@ -39,8 +39,8 @@ object B { a.x = a.x + inc a.y = a.y + a.x Deduce( - Old(a) ≡ At(a, 0)(x = At(a, 0).x + B.inc) by Premise, - a ≡ Old(a)(y = Old(a).y + Old(a).x) by Premise + Old(a) ≡ At(a, 0)(x = At(a, 0).x + B.inc) by Premise + //FIXME evalConstructor: a ≡ At(a, 0)(x = At(a, 0).x + B.inc)(y = Old(a).y + Old(a).x) by Premise ) } } diff --git a/jvm/src/test/scala/org/sireum/logika/example/premise.sc b/jvm/src/test/scala/org/sireum/logika/example/premise.sc index a4c7aa13..be42f844 100644 --- a/jvm/src/test/scala/org/sireum/logika/example/premise.sc +++ b/jvm/src/test/scala/org/sireum/logika/example/premise.sc @@ -101,7 +101,7 @@ def testIdString(): Unit = { //@formatter:off At[Z]("addY.n", 0) == 0 by Premise, At[Z]("addY.n", 1) == 1 by Premise, - At(y, 0) + At[Z]("addY.n", 0) == At(y, 0) + 0 by Premise, + At(y, 1) == At(y, 0) + At[Z]("addY.n", 0) by Premise, y == At(y, 0) + 0 + 1 by Premise //@formatter:on ) @@ -128,7 +128,7 @@ def testNameString(): Unit = { //@formatter:off At[Z]("addFooY.n", 0) == 0 by Premise, At[Z]("addFooY.n", 1) == 1 by Premise, - At(Foo.y, 0) + At[Z]("addFooY.n", 0) == At(Foo.y, 0) + 0 by Premise, + At(Foo.y, 1) == At(Foo.y, 0) + 0 by Premise, Foo.y == At(Foo.y, 0) + 0 + 1 by Premise //@formatter:on ) diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala index 7798db13..9b143208 100644 --- a/shared/src/main/scala/org/sireum/logika/Logika.scala +++ b/shared/src/main/scala/org/sireum/logika/Logika.scala @@ -1589,6 +1589,9 @@ import Util._ case res: AST.ResolvedInfo.Tuple => assert(receiverOpt.nonEmpty) return evalTupleProjection(res) + case AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.Apply) => + assert(receiverOpt.nonEmpty) + return evalExp(split, smt2, cache, rtCheck, state, receiverOpt.get, reporter) case _ => reporter.warn(e.posOpt, kind, s"Not currently supported: $e") return ISZ((state(status = State.Status.Error), State.errorValue)) @@ -1697,12 +1700,16 @@ import Util._ case _ => } val s4 = s3.addClaim(State.Claim.Let.AdtLit(sym, args.toIS[Option[State.Value]].map((vOpt: Option[State.Value]) => vOpt.get))) - val (s5, vs) = addValueInv(this, smt2, cache, T, s4, sym, attr.posOpt.get, reporter) - var s6 = s5 - for (v <- vs if s6.ok) { - s6 = evalAssertH(T, smt2, cache, st"Invariant on ${(ti.name, ".")} construction".render, s6, v, attr.posOpt, reporter) + if (rtCheck) { + val (s5, vs) = addValueInv(this, smt2, cache, T, s4, sym, attr.posOpt.get, reporter) + var s6 = s5 + for (v <- vs if s6.ok) { + s6 = evalAssertH(T, smt2, cache, st"Invariant on ${(ti.name, ".")} construction".render, s6, v, attr.posOpt, reporter) + } + r = r :+ ((s4(nextFresh = s6.nextFresh, status = s6.status), sym)) + } else { + r = r :+ ((s4, sym)) } - r = r :+ ((s4(nextFresh = s6.nextFresh, status = s6.status), sym)) } else { r = r :+ ((s2, State.errorValue)) } @@ -1823,7 +1830,8 @@ import Util._ def evalOld(exp: AST.Exp.Old): (State, State.Value) = { for (i <- state.claims.size - 1 to 0 by -1) { state.claims(i) match { - case c: State.Claim.Old => return (state, c.value) + case c: State.Claim.Old => + return (state, c.value) case _ => } } diff --git a/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala index 01d642b9..644bf2db 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala @@ -306,7 +306,7 @@ object AutoPlugin { |}""".render) } val (stat, nextFresh, premises, conclusion) = - logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter) + logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter) return Plugin.Result(stat, nextFresh, premises :+ conclusion) } else if (id == "Premise") { AutoPlugin.detectOrIntro(logika.th, step.claim, pathConditions) match { @@ -315,7 +315,7 @@ object AutoPlugin { reporter.inform(pos, Logika.Reporter.Info.Kind.Verified, acceptMsg.render) } val (stat, nextFresh, premises, conclusion) = - logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter) + logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter) return Plugin.Result(stat, nextFresh, premises :+ conclusion) case _ => reporter.error(posOpt, Logika.kind,