From da8c49dcef6275c54e7fe37c0f37e3a9b30e1074 Mon Sep 17 00:00:00 2001 From: Robby Date: Thu, 14 Sep 2023 19:11:08 -0500 Subject: [PATCH] Various improvements. --- .../scala/org/sireum/logika/Context.scala | 10 ++++----- .../main/scala/org/sireum/logika/Logika.scala | 22 ++++++++++++++----- .../main/scala/org/sireum/logika/Util.scala | 8 +++---- .../logika/plugin/InceptionPlugin.scala | 2 +- 4 files changed, 27 insertions(+), 15 deletions(-) diff --git a/shared/src/main/scala/org/sireum/logika/Context.scala b/shared/src/main/scala/org/sireum/logika/Context.scala index 506410b1..033893f7 100644 --- a/shared/src/main/scala/org/sireum/logika/Context.scala +++ b/shared/src/main/scala/org/sireum/logika/Context.scala @@ -107,18 +107,18 @@ object Context { return r } - def localMap(sm: HashMap[String, AST.Typed]): HashSMap[String, (ISZ[String], AST.Id, AST.Typed)] = { - var r = HashSMap.empty[String, (ISZ[String], AST.Id, AST.Typed)] + def localMap(sm: HashMap[String, AST.Typed]): HashSMap[String, (B, ISZ[String], AST.Id, AST.Typed)] = { + var r = HashSMap.empty[String, (B, ISZ[String], AST.Id, AST.Typed)] for (p <- params) { val (id, t) = p - r = r + id.value ~> ((name, id, t.subst(sm))) + r = r + id.value ~> ((T, name, id, t.subst(sm))) } for (x <- reads ++ modifies) { x.resOpt.get match { case res: AST.ResolvedInfo.LocalVar if !r.contains(res.id) => - r = r + res.id ~> ((res.context, AST.Id(res.id, AST.Attr(x.posOpt)), x.typedOpt.get.subst(sm))) + r = r + res.id ~> ((res.isVal, res.context, AST.Id(res.id, AST.Attr(x.posOpt)), x.typedOpt.get.subst(sm))) case res: AST.ResolvedInfo.Var if !(res.isInObject || res.owner.isEmpty) && !r.contains("this") => - r = r + "this" ~> ((name, AST.Id("this", AST.Attr(x.posOpt)), receiverTypeOpt.get)) + r = r + "this" ~> ((T, name, AST.Id("this", AST.Attr(x.posOpt)), receiverTypeOpt.get)) case _ => } } diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala index 8839524c..9583bd54 100644 --- a/shared/src/main/scala/org/sireum/logika/Logika.scala +++ b/shared/src/main/scala/org/sireum/logika/Logika.scala @@ -918,6 +918,8 @@ import Util._ (jps, eps, sps, cps, mps) } + @strictpure def isSymExe: B = config.mode == Config.VerificationMode.SymExe + def zero(tipe: AST.Typed.Name, pos: Position): State.Value = { tipe match { case AST.Typed.z => return State.Value.Z(0, pos) @@ -936,7 +938,7 @@ import Util._ return s0 } val pos = posOpt.get - if (config.mode != Config.VerificationMode.SymExe) { + if (!isSymExe) { val (s1, size) = s0.freshSym(AST.Typed.z, pos) val (s2, loCond) = s1.freshSym(AST.Typed.b, pos) val (s3, hiCond) = s2.freshSym(AST.Typed.b, pos) @@ -1085,7 +1087,7 @@ import Util._ if (!info.ast.isVal) { return None() } - AST.Util.constantInitOpt(info.ast) match { + AST.Util.constantInitOpt(info.ast.initOpt, info.ast.attr.typedOpt) match { case Some(exp) => val r = evalExp(Split.Disabled, smt2, cache, rtCheck, s0, exp, reporter) assert(r.size == 1) @@ -1298,6 +1300,16 @@ import Util._ val (s1, v) = nameIntro(pos, s0, name :+ id, t, Some(pos)) return (s1, v) case res: AST.ResolvedInfo.LocalVar => + if (res.context.isEmpty) { + th.nameMap.get(ISZ(res.id)) match { + case Some(info: Info.LocalVar) => + AST.Util.constantInitOpt(info.initOpt, info.typedOpt) match { + case Some(init) => return evalExp(split, smt2, cache, rtCheck, s0, init, reporter)(0) + case _ => + } + case _ => + } + } val (s1, r) = idIntro(pos, s0, res.context, res.id, t, None()) return (s1, r) case res: AST.ResolvedInfo.Var => @@ -1405,7 +1417,7 @@ import Util._ if (!rtCheck || !s0.ok) { return s0 } - if (config.mode != Config.VerificationMode.SymExe) { + if (!isSymExe) { val tipe = value.tipe.asInstanceOf[AST.Typed.Name] val (s1, cond) = s0.freshSym(AST.Typed.b, pos) val s2 = s1.addClaims(ISZ( @@ -2507,7 +2519,7 @@ import Util._ } var localInMap = mctx.localInMap for (p <- mctx.localMap(typeSubstMap).entries) { - val (id, (ctx, _, t)) = p + val (id, (_, ctx, _, t)) = p val (s7, sym): (State, State.Value.Sym) = idIntro(pos, s1, ctx, id, t, None()) localInMap = localInMap + id ~> sym s1 = s7 @@ -3684,7 +3696,7 @@ import Util._ posOpt: Option[Position], rwLocals: ISZ[AST.ResolvedInfo], reporter: Reporter): State = { val conclusion = State.Claim.Prop(T, sym) val pos = posOpt.get - if (config.mode != Config.VerificationMode.SymExe) { + if (!isSymExe) { Util.claimsToExpsLastOpt(jescmPlugins._4, pos, context.methodName, s0.claims :+ conclusion, th, F, config.atRewrite) match { case (pcs, Some(conc), _) => val pcs2: HashSSet[AST.Exp] = if (rwLocals.nonEmpty) { diff --git a/shared/src/main/scala/org/sireum/logika/Util.scala b/shared/src/main/scala/org/sireum/logika/Util.scala index f647cfc4..64f00e28 100644 --- a/shared/src/main/scala/org/sireum/logika/Util.scala +++ b/shared/src/main/scala/org/sireum/logika/Util.scala @@ -1994,7 +1994,7 @@ object Util { case Some(receiverType) => val (s1, thiz) = idIntro(mctx.posOpt.get, s0, mctx.name, "this", receiverType, mctx.posOpt) localInMap = localInMap + "this" ~> thiz - s0 = s1.addClaim(State.Claim.Input(T, F, mctx.name, "this", thiz, thiz.pos)) + s0 = if (!l.th.isMutable(receiverType)) s1 else s1.addClaim(State.Claim.Input(T, F, mctx.name, "this", thiz, thiz.pos)) thisAdded = T for (p <- mctx.fieldVarMap(TypeChecker.emptySubstMap).entries) { val (id, (t, posOpt)) = p @@ -2005,18 +2005,18 @@ object Util { case _ => } for (v <- mctx.localMap(TypeChecker.emptySubstMap).values) { - val (mname, id, t) = v + val (isVal, mname, id, t) = v val posOpt = id.attr.posOpt if (id.value != "this") { val (s1, sym) = idIntro(posOpt.get, s0, mname, id.value, t, posOpt) - s0 = s1.addClaim(State.Claim.Input(T, F, mname, id.value, sym, sym.pos)) + s0 = if (isVal && !l.th.isMutable(t)) s1 else s1.addClaim(State.Claim.Input(T, F, mname, id.value, sym, sym.pos)) if (!isHelper) { s0 = assumeValueInv(l, smt2, cache, T, s0, sym, posOpt.get, reporter) } localInMap = localInMap + id.value ~> sym } else if (!thisAdded) { val (s1, sym) = idIntro(posOpt.get, s0, mname, id.value, t, mctx.posOpt) - s0 = s1.addClaim(State.Claim.Input(T, F, mname, id.value, sym, sym.pos)) + s0 = if (!l.th.isMutable(t)) s1 else s1.addClaim(State.Claim.Input(T, F, mname, id.value, sym, sym.pos)) localInMap = localInMap + id.value ~> sym thisAdded = T } diff --git a/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala index b4acce61..fb70012b 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala @@ -294,7 +294,7 @@ import InceptionPlugin._ return emptyResult } val (status, nextFresh, claims, claim): (B, Z, ISZ[State.Claim], State.Claim) = - if (logika.config.mode == Config.VerificationMode.SymExe) + if (logika.isSymExe) logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter) else logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter) if (status && logika.config.detailedInfo) {