Skip to content

Commit

Permalink
Various improvements.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Sep 15, 2023
1 parent 1db9387 commit da8c49d
Show file tree
Hide file tree
Showing 4 changed files with 27 additions and 15 deletions.
10 changes: 5 additions & 5 deletions shared/src/main/scala/org/sireum/logika/Context.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ =>
}
}
Expand Down
22 changes: 17 additions & 5 deletions shared/src/main/scala/org/sireum/logika/Logika.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 =>
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) {
Expand Down
8 changes: 4 additions & 4 deletions shared/src/main/scala/org/sireum/logika/Util.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
}
Expand Down
2 changes: 1 addition & 1 deletion shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down

0 comments on commit da8c49d

Please sign in to comment.