Skip to content

Commit

Permalink
Refactored JustificationPlugin API.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Feb 27, 2024
1 parent 2922ce6 commit c501db6
Show file tree
Hide file tree
Showing 17 changed files with 257 additions and 252 deletions.
103 changes: 67 additions & 36 deletions shared/src/main/scala/org/sireum/logika/Logika.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1721,17 +1721,17 @@ import Util._
val (s1, cond) = s0.freshSym(AST.Typed.b, pos)
val s2 = s1.addClaim(State.Claim.Let.TypeTest(cond, F, v, tipe))
if (isCast) {
if (!rtCheck) {
val (s3, cv) = s2.freshSym(tipe, pos)
r = r :+ ((s3.addClaim(State.Claim.Let.Def(cv, v)), cv))
val s3: State = if (rtCheck) {
evalAssertH(T, smt2, cache, "asInstanceOf", s2, cond, Some(pos), ISZ(), reporter)
} else {
val s3 = evalAssertH(T, smt2, cache, "asInstanceOf", s2, cond, Some(pos), ISZ(), reporter)
if (s3.ok) {
val (s4, cv) = s3.freshSym(tipe, pos)
r = r :+ ((s4.addClaim(State.Claim.Let.Def(cv, v)), cv))
} else {
r = r :+ ((s3, State.errorValue))
}
val thiz = this
thiz(config = thiz.config(sat = F)).evalAssumeH(T, smt2, cache, "asInstanceOf", s2, cond, Some(pos), reporter)
}
if (s3.ok) {
val (s4, cv) = s3.freshSym(tipe, pos)
r = r :+ ((s4.addClaim(State.Claim.Let.Def(cv, v)), cv))
} else {
r = r :+ ((s3, State.errorValue))
}
} else {
r = r :+ ((s2, cond))
Expand All @@ -1757,8 +1757,13 @@ import Util._
val (s1, size) = s0.freshSym(AST.Typed.z, pos)
val (s2, cond) = s1.addClaim(State.Claim.Let.FieldLookup(size, o, "size")).freshSym(AST.Typed.b, pos)
val s3 = s2.addClaim(State.Claim.Let.Binary(cond, size, AST.Exp.BinaryOp.Gt, State.Value.Z(0, pos), AST.Typed.z))
s0 = if (rtCheck) evalAssertH(T, smt2, cache, s"Non-empty check for $tipe", s3, cond, Some(pos), ISZ(), reporter)
else s3.addClaim(State.Claim.Prop(T, cond))
s0 = if (rtCheck) {
evalAssertH(T, smt2, cache, s"Non-empty check for $tipe", s3, cond, Some(pos), ISZ(), reporter)
} else {
val thiz = this
thiz(config = thiz.config(sat = F)).
evalAssumeH(T, smt2, cache, s"Non-empty check for $tipe", s3, cond, Some(pos), reporter)
}
} else {
evalConstantVarInstance(smt2, cache, rtCheck, s0, tipe.ids, id, reporter) match {
case Some((s1, v)) => return value2Sym(s1, v, pos)
Expand Down Expand Up @@ -1941,17 +1946,20 @@ import Util._
case _ =>
}
val s4 = s3.addClaim(State.Claim.Let.AdtLit(sym, args.toIS[Option[State.Value]].map((vOpt: Option[State.Value]) => vOpt.get)))
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) {
val (s5, vs) = addValueInv(this, smt2, cache, T, s4, sym, attr.posOpt.get, reporter)
var s6 = s5
var thiz = this
thiz = thiz(config = thiz.config(sat = F))
for (v <- vs if s6.ok) {
if (rtCheck) {
s6 = evalAssertH(T, smt2, cache, st"Invariant on ${(ti.name, ".")} construction".render, s6, v,
attr.posOpt, ISZ(), reporter)
} else {
s6 = thiz.evalAssumeH(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))
}
Expand Down Expand Up @@ -3470,9 +3478,9 @@ import Util._
val (s1, sym) = value2Sym(s0, cond, ifExp.cond.posOpt.get)
val prop = State.Claim.Prop(T, sym)
val negProp = State.Claim.Prop(F, sym)
val thenBranch = !rtCheck || smt2.sat(context.methodName, config, cache, T,
val thenBranch = smt2.sat(context.methodName, config, cache, T,
s"$construct-true-branch at [${pos.beginLine}, ${pos.beginColumn}]", pos, s1.claims :+ prop, reporter)
val elseBranch = !rtCheck || smt2.sat(context.methodName, config, cache, T,
val elseBranch = smt2.sat(context.methodName, config, cache, T,
s"$construct-false-branch at [${pos.beginLine}, ${pos.beginColumn}]", pos, s1.claims :+ negProp, reporter)
(thenBranch, elseBranch) match {
case (T, T) =>
Expand Down Expand Up @@ -3502,8 +3510,8 @@ import Util._
r = r :+ ((s5.addClaim(State.Claim.Let.Ite(re, sym, tv, ev)), re))
}
}
case (T, F) => r = r ++ evalExp(sp, smt2, cache, rtCheck, s1, ifExp.thenExp, reporter)
case (F, T) => r = r ++ evalExp(sp, smt2, cache, rtCheck, s1, ifExp.elseExp, reporter)
case (T, F) => r = r ++ evalExp(sp, smt2, cache, rtCheck, s1.addClaim(prop), ifExp.thenExp, reporter)
case (F, T) => r = r ++ evalExp(sp, smt2, cache, rtCheck, s1.addClaim(negProp), ifExp.elseExp, reporter)
case (_, _) => r = r :+ ((s0(status = State.Status.Error), State.errorValue))
}
} else {
Expand Down Expand Up @@ -4737,8 +4745,7 @@ import Util._
cache.getTransitionAndUpdateSmt2(th, config, Cache.Transition.ProofStep(step, m.values), s0, smt2) match {
case Some((ISZ(nextState), cached)) =>
reporter.coverage(F, cached, pos)
return (nextState, m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim,
ops.ISZOps(nextState.claims).slice(s0.claims.size, nextState.claims.size)))
return (nextState, m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim))
case _ =>
}
}
Expand Down Expand Up @@ -4787,23 +4794,22 @@ import Util._
if (!plugin.checkMode(this, normStep.just, reporter)) {
return (s0(status = State.Status.Error), m)
}
val Plugin.Result(ok, nextFresh, claims) = plugin.handle(this, smt2, cache, m, s0, normStep, reporter)
val nextState = s0(status = State.statusOf(ok), nextFresh = nextFresh).addClaims(claims)
if (config.transitionCache && ok && !reporter.hasError) {
val nextState = plugin.handle(this, smt2, cache, m, s0, normStep, reporter)
if (config.transitionCache && nextState.ok && !reporter.hasError) {
val cached = cache.setTransition(th, config, Cache.Transition.ProofStep(step, m.values), s0, ISZ(nextState), smt2)
reporter.coverage(T, cached, pos)
} else {
reporter.coverage(F, zeroU64, pos)
}
return (nextState, m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim, claims))
return (nextState, m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim))
}
reporter.error(step.just.posOpt, Logika.kind, "Could not recognize justification form")
return (s0(status = State.Status.Error), m)
case step: AST.ProofAst.Step.Assume =>
val (ok, nextFresh, claims, claim) = evalRegularStepClaim(smt2, cache, s0, step.claim, step.id.posOpt, reporter)
return (s0(status = State.statusOf(ok), nextFresh = nextFresh,
claims = (s0.claims ++ claims) :+ claim),
m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim, claims :+ claim))
m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim))
case step: AST.ProofAst.Step.SubProof =>
for (sub <- step.steps if s0.ok) {
val p = evalProofStep(smt2, cache, (s0, m), sub, reporter)
Expand Down Expand Up @@ -4841,7 +4847,7 @@ import Util._
val (ok, nextFresh, claims, claim) = evalRegularStepClaimRtCheck(smt2, cache, F, s0, step.claim, step.id.posOpt, reporter)
return (s0(status = State.statusOf(ok), nextFresh = nextFresh,
claims = (s0.claims ++ claims) :+ claim),
m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim, claims :+ claim))
m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim))
case step: AST.ProofAst.Step.Let =>
for (sub <- step.steps if s0.ok) {
val p = evalProofStep(smt2, cache, (s0, m), sub, reporter)
Expand Down Expand Up @@ -4882,6 +4888,31 @@ import Util._
return (F, s0.nextFresh, s0.claims, trueClaim)
}

def evalRegularStepClaim2(smt2: Smt2, cache: Logika.Cache, s0: State, claim: AST.Exp, posOpt: Option[Position],
reporter: Reporter): State = {
return evalRegularStepClaimRtCheck2(smt2, cache, T, s0, claim, posOpt, reporter)
}

def evalRegularStepClaimValue(smt2: Smt2, cache: Logika.Cache, s0: State, claim: AST.Exp, posOpt: Option[Position],
reporter: Reporter): (State, State.Value.Sym) = {
return evalRegularStepClaimRtCheckValue(smt2, cache, T, s0, claim, posOpt, reporter)
}
def evalRegularStepClaimRtCheck2(smt2: Smt2, cache: Logika.Cache, rtCheck: B, s0: State, claim: AST.Exp,
posOpt: Option[Position], reporter: Reporter): State = {
val (s1, v) = evalRegularStepClaimRtCheckValue(smt2, cache, rtCheck, s0, claim, posOpt, reporter)
return if (s1.ok) s1.addClaim(State.Claim.Prop(T, v)) else s1
}
def evalRegularStepClaimRtCheckValue(smt2: Smt2, cache: Logika.Cache, rtCheck: B, s0: State, claim: AST.Exp,
posOpt: Option[Position], reporter: Reporter): (State, State.Value.Sym) = {
val svs = evalExp(Logika.Split.Disabled, smt2, cache, rtCheck, s0, claim, reporter)
for (sv <- svs) {
val (s1, v) = sv
val (s2, sym) = value2Sym(s1, v, posOpt.get)
return (s2, sym)
}
return (s0(status = State.Status.Error), State.errorValue)
}

@pure def claimsAnd(claims: ISZ[AST.Exp]): Option[AST.Exp] = {
if (claims.isEmpty) {
return None()
Expand Down Expand Up @@ -5226,11 +5257,13 @@ import Util._
}
}
val m = p._2
var s1 = s0(nextFresh = p._1.nextFresh, claims = ops.ISZOps(p._1.claims).slice(0, s0.claims.size))
var s1 = s0
//var s1 = s0(nextFresh = p._1.nextFresh, claims = ops.ISZOps(p._1.claims).slice(0, s0.claims.size))
if (p._1.ok) {
for (stepId <- stepIds) {
val spc = m.get(stepId).get.asInstanceOf[StepProofContext.Regular]
s1 = s1.addClaims(spc.claims)
s1 = evalAssume(smt2, cache, F, s"${spc.stepNo}", s1, spc.exp, spc.stepNo.posOpt, reporter)._1
// s1 = s1.addClaims(spc.claims)
}
}
return ISZ(s1)
Expand All @@ -5248,10 +5281,8 @@ import Util._
var st0 = st
for (premise <- sequent.premises if st0.ok) {
val (ok, nextFresh, claims, claim) = evalRegularStepClaim(smt2, cache, st0, premise, premise.posOpt, reporter)
r = r + id ~> StepProofContext.Regular(th, id(attr = AST.Attr(premise.posOpt)), premise, claims :+ claim)
r = r + id ~> StepProofContext.Regular(th, id(attr = AST.Attr(premise.posOpt)), premise)
id = id(no = id.no - 1)
st0 = st0(status = State.statusOf(ok), nextFresh = nextFresh,
claims = (st0.claims ++ claims) :+ claim)
}
return (st0, r)
}
Expand Down
5 changes: 2 additions & 3 deletions shared/src/main/scala/org/sireum/logika/StepProofContext.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,9 +41,8 @@ object StepProofContext {

@datatype class Regular(val th: TypeHierarchy,
val stepNo: AST.ProofAst.StepId,
val exp: AST.Exp,
val claims: ISZ[State.Claim]) extends StepProofContext {
@strictpure override def prettyST: ST = st"(${stepNo.prettyST}, ${exp.prettyST}, ${(for (claim <- claims) yield claim.toRawST, ", ")})"
val exp: AST.Exp) extends StepProofContext {
@strictpure override def prettyST: ST = st"(${stepNo.prettyST}, ${exp.prettyST})"
@memoize def coreExpClaim: AST.CoreExp.Base = {
return RewritingSystem.translateExp(th, F, exp)
}
Expand Down
2 changes: 1 addition & 1 deletion shared/src/main/scala/org/sireum/logika/Task.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,7 @@ object Task {
else theorem.claim)
val spcEntries = p._2.entries
for (i <- spcEntries.size - 1 to 0 by -1 if spcEntries(i)._2.isInstanceOf[StepProofContext.Regular]) {
val StepProofContext.Regular(_, _, claim, _) = spcEntries(i)._2
val StepProofContext.Regular(_, _, claim) = spcEntries(i)._2
if (normClaim == th.normalizeExp(claim)) {
if (logika.config.detailedInfo) {
reporter.inform(normClaim.posOpt.get, Logika.Reporter.Info.Kind.Verified,
Expand Down
6 changes: 2 additions & 4 deletions shared/src/main/scala/org/sireum/logika/plugin/AdmitPlugin.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,10 +54,8 @@ import org.sireum.logika.{Logika, Smt2, State, StepProofContext}

override def handle(logika: Logika, smt2: Smt2, cache: Logika.Cache,
spcMap: HashSMap[AST.ProofAst.StepId, StepProofContext], state: State,
step: AST.ProofAst.Step.Regular, reporter: Logika.Reporter): Plugin.Result = {
step: AST.ProofAst.Step.Regular, reporter: Logika.Reporter): State = {
reporter.warn(step.claim.posOpt, Logika.kind, "Admitted claim")
val q = logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
val (stat, nextFresh, claims) = (q._1, q._2, q._3 :+ q._4)
return Plugin.Result(stat, nextFresh, claims)
return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
}
}
47 changes: 21 additions & 26 deletions shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,9 @@ object AutoPlugin {
spcMap: HashSMap[AST.ProofAst.StepId, StepProofContext],
state: State,
step: AST.ProofAst.Step.Regular,
reporter: Reporter): Plugin.Result = {
reporter: Reporter): State = {

@strictpure def err: State = state(status = State.Status.Error)

val just = step.just.asInstanceOf[AST.ProofAst.Step.Justification.Ref]

Expand All @@ -272,15 +274,14 @@ object AutoPlugin {
return !ac.reporter.hasError
}

def checkValid(psmt2: Smt2, stat: B, nextFresh: Z, premises: ISZ[State.Claim], conclusion: State.Claim,
claims: ISZ[State.Claim]): Plugin.Result = {
def checkValid(psmt2: Smt2, s0: State, conclusion: State.Claim): State = {
if (id == "Algebra" && !checkAlgebraExp(step.claim)) {
return Plugin.Result.empty(nextFresh)
return err
}

var status = stat
var status = s0.ok
if (status) {
val r = psmt2.valid(logika.context.methodName, logika.config, cache, T, s"$id Justification", pos, premises,
val r = psmt2.valid(logika.context.methodName, logika.config, cache, T, s"$id Justification", pos, s0.claims,
conclusion, reporter)

def error(msg: String): B = {
Expand All @@ -296,7 +297,7 @@ object AutoPlugin {
case Smt2Query.Result.Kind.Error => error(s"Error occurred when deducing the claim of proof step ${step.id}")
}
}
return Plugin.Result(status, nextFresh, claims)
return if (status) s0.addClaim(conclusion) else err
}

val provenClaims = HashMap ++ (for (spc <- spcMap.values if spc.isInstanceOf[StepProofContext.Regular]) yield
Expand All @@ -315,7 +316,7 @@ object AutoPlugin {
|${spc.exp}
|""".render)
}
return Plugin.Result(T, state.nextFresh, spc.claims)
return state
case _ =>
logika.context.pathConditionsOpt match {
case Some(pcs@Logika.PathConditions(_, pathConditions)) if id == "Premise" || id == "Auto" =>
Expand All @@ -328,41 +329,36 @@ object AutoPlugin {
| ${(for (e <- pathConditions) yield e.prettyST, ";\n")}
|}""".render)
}
val (stat, nextFresh, premises, conclusion) =
logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
return Plugin.Result(stat, nextFresh, premises :+ conclusion)
return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
} else if (id == "Premise") {
AutoPlugin.detectOrIntro(logika.th, step.claim, pathConditions) match {
case Some(acceptMsg) =>
if (logika.config.detailedInfo) {
reporter.inform(pos, Logika.Reporter.Info.Kind.Verified, acceptMsg.render)
}
val (stat, nextFresh, premises, conclusion) =
logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
return Plugin.Result(stat, nextFresh, premises :+ conclusion)
return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
case _ =>
reporter.error(posOpt, Logika.kind,
st"""The stated claim has not been proven before nor is a premise in the path conditions:
|{
| ${(for (e <- pathConditions) yield e.prettyST, ";\n")}
|}""".render)
return Plugin.Result.empty(state.nextFresh)
return err
}
}
case _ =>
if (id == "Premise") {
reporter.error(posOpt, Logika.kind, "The stated claim has not been proven before")
return Plugin.Result.empty(state.nextFresh)
return err
}
}
}
}

if (!just.hasWitness) {
val (stat, nextFresh, premises, conclusion) =
logika(config = logika.config(isAuto = T)).
evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
return checkValid(smt2, stat, nextFresh, state.claims ++ premises, conclusion, premises :+ conclusion)
val (s0, conclusion) = logika(config = logika.config(isAuto = T)).
evalRegularStepClaimValue(smt2, cache, state, step.claim, step.id.posOpt, reporter)
return checkValid(smt2, s0, State.Claim.Prop(T, conclusion))
} else {
val psmt2 = smt2.emptyCache(logika.config)
val atMap = org.sireum.logika.Util.claimsToExps(logika.jescmPlugins._4, pos, logika.context.methodName,
Expand All @@ -386,15 +382,14 @@ object AutoPlugin {
}
}
if (!ok) {
return Plugin.Result.empty(state.nextFresh)
return err
}
val (s5, exp) = logika.rewriteAt(atMap, s1, step.claim, reporter)
val (stat, nextFresh, premises, conclusion) =
logika(config = logika.config(isAuto = T)).
evalRegularStepClaim(psmt2, cache, s5, exp, step.id.posOpt, reporter)
val r = checkValid(psmt2, stat, nextFresh, s1.claims ++ premises, conclusion, premises :+ conclusion)
val (s6, conclusion) = logika(config = logika.config(isAuto = T)).
evalRegularStepClaimValue(psmt2, cache, s5, exp, step.id.posOpt, reporter)
val r = checkValid(psmt2, s6, State.Claim.Prop(T, conclusion))
smt2.combineWith(psmt2)
return r
return if (r.ok) r(claims = state.claims ++ r.claims) else err
}
}

Expand Down
Loading

0 comments on commit c501db6

Please sign in to comment.