Skip to content

Commit

Permalink
substitution
Browse files Browse the repository at this point in the history
  • Loading branch information
@AndreaKe
AndreaKe committed Oct 7, 2023
1 parent 3782b32 commit 4459d67
Show file tree
Hide file tree
Showing 10 changed files with 89 additions and 52 deletions.
17 changes: 11 additions & 6 deletions src/main/scala/decider/Decider.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
package viper.silicon.decider

import com.typesafe.scalalogging.Logger
import org.jgrapht.alg.util.Pair
import viper.silicon._
import viper.silicon.common.collections.immutable.InsertionOrderedSet
import viper.silicon.interfaces._
Expand All @@ -16,7 +17,6 @@ import viper.silicon.state._
import viper.silicon.state.terms._
import viper.silicon.verifier.{Verifier, VerifierComponent}
import viper.silver.ast
import viper.silver.ast.TrueLit
import viper.silver.components.StatefulComponent
import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage}
import viper.silver.verifier.{DependencyNotFoundError, Model}
Expand All @@ -37,7 +37,7 @@ trait Decider {

def checkSmoke(isAssert: Boolean = false): Boolean

def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit
def setCurrentBranchCondition(t: Term, te: Option[Pair[ast.Exp, ast.Exp]] = None): Unit
def setPathConditionMark(): Mark

def finishDebugSubExp(str : String): Unit
Expand Down Expand Up @@ -204,11 +204,16 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
//symbExLog.closeScope(sepIdentifier)
}

def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit = {
pathConditions.setCurrentBranchCondition(t, te)
def setCurrentBranchCondition(t: Term, te: Option[Pair[ast.Exp, ast.Exp]] = None): Unit = {
te match {
case Some(e) => assume(t, e)
case None => assume(t, new DebugExp("current branch condition", InsertionOrderedSet.empty)) // TODO ake
case Some(e) => {
pathConditions.setCurrentBranchCondition(t, Some(e.getFirst))
assume(t, e.getSecond)
}
case None => {
pathConditions.setCurrentBranchCondition(t, None)
assume(t, new DebugExp("current branch condition"))
} // TODO ake
}
}

Expand Down
16 changes: 13 additions & 3 deletions src/main/scala/rules/Brancher.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@

package viper.silicon.rules

import org.jgrapht.alg.util.Pair

import java.util.concurrent._
import viper.silicon.common.concurrency._
import viper.silicon.decider.PathConditionStack
Expand All @@ -15,7 +17,7 @@ import viper.silicon.state.State
import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term}
import viper.silicon.verifier.Verifier
import viper.silver.ast
import viper.silver.reporter.{BranchFailureMessage}
import viper.silver.reporter.BranchFailureMessage
import viper.silver.verifier.Failure

trait BranchingRules extends SymbolicExecutionRules {
Expand Down Expand Up @@ -126,7 +128,11 @@ object brancher extends BranchingRules {

executionFlowController.locally(s, v0)((s1, v1) => {
v1.decider.prover.comment(s"[else-branch: $cnt | $negatedCondition]")
v1.decider.setCurrentBranchCondition(negatedCondition, negatedConditionExp)
var branchCondExp : Option[Pair[ast.Exp, ast.Exp]] = None
if(negatedConditionExp.isDefined){
branchCondExp = Some(new Pair(negatedConditionExp.get, s1.substituteVarsInExp(negatedConditionExp.get)))
}
v1.decider.setCurrentBranchCondition(negatedCondition, branchCondExp)

if (v.uniqueId != v0.uniqueId)
v1.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
Expand Down Expand Up @@ -159,7 +165,11 @@ object brancher extends BranchingRules {
v.symbExLog.markReachable(uidBranchPoint)
executionFlowController.locally(s, v)((s1, v1) => {
v1.decider.prover.comment(s"[then-branch: $cnt | $condition]")
v1.decider.setCurrentBranchCondition(condition, conditionExp)
var branchCondExp: Option[Pair[ast.Exp, ast.Exp]] = None
if (conditionExp.isDefined) {
branchCondExp = Some(new Pair(conditionExp.get, s1.substituteVarsInExp(conditionExp.get)))
}
v1.decider.setCurrentBranchCondition(condition, branchCondExp)

fThen(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
})
Expand Down
16 changes: 7 additions & 9 deletions src/main/scala/rules/Consumer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -365,8 +365,8 @@ object consumer extends ConsumptionRules {
val (smDef1, smCache1) =
quantifiedChunkSupporter.summarisingSnapshotMap(
s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
val argsString = eArgs.mkString(", ")
val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}($argsString)", InsertionOrderedSet.empty)
val argsString = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}($argsString)")
v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
s2.copy(smCache = smCache1)
} else {
Expand Down Expand Up @@ -422,9 +422,9 @@ object consumer extends ConsumptionRules {
val (smDef1, smCache1) =
quantifiedChunkSupporter.summarisingSnapshotMap(
s1, wand, formalVars, relevantChunks, v1)
val argsString = bodyVars.mkString(", ")
val argsString = bodyVars.map(e => s1.substituteVarsInExp(e)).mkString(", ")
val predName = MagicWandIdentifier(wand, s.program).toString
val debugExp = new DebugExp(s"Predicate Trigger: $predName($argsString)\"", InsertionOrderedSet.empty)
val debugExp = new DebugExp(s"Predicate Trigger: $predName($argsString)")
v1.decider.assume(PredicateTrigger(predName, smDef1.sm, tArgs), debugExp)
s1.copy(smCache = smCache1)
} else {
Expand Down Expand Up @@ -486,20 +486,18 @@ object consumer extends ConsumptionRules {
case Quantification(q, vars, body, trgs, name, isGlob, weight) =>
val transformed = FunctionPreconditionTransformer.transform(body, s3.program)


val debugExp = new DebugExp(e)
v2.decider.assume(Quantification(q, vars, transformed, trgs, name+"_precondition", isGlob, weight), debugExp)
v2.decider.assume(Quantification(q, vars, transformed, trgs, name+"_precondition", isGlob, weight), s3.substituteVarsInExp(e))
Quantification(q, vars, Implies(transformed, body), trgs, name, isGlob, weight)
case _ => t
}
v2.decider.assert(termToAssert) {
case true =>
v2.decider.assume(t, e)
v2.decider.assume(t, s3.substituteVarsInExp(e))
QS(s3, v2)
case false =>
val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3)
if (s3.retryLevel == 0 && v2.reportFurtherErrors()){
v2.decider.assume(t, e)
v2.decider.assume(t, s1.substituteVarsInExp(e))
failure combine QS(s3, v2)
} else failure}})
})((s4, v4) => {
Expand Down
31 changes: 18 additions & 13 deletions src/main/scala/rules/Evaluator.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@

package viper.silicon.rules

import org.jgrapht.alg.util.Pair
import viper.silver.ast
import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, VerifierWarning}
import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, PreconditionInAppFalse}
Expand Down Expand Up @@ -296,7 +297,7 @@ object evaluator extends EvaluationRules {
eval(s, e0, pve, v)((s1, t0, v1) => {
val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables)
val debugExpr = ast.EqCmp(x.localVar, e0)()
v1.decider.assume(t === t0, debugExpr)
v1.decider.assume(t === t0, s1.substituteVarsInExp(debugExpr))
val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function])
eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q)
})
Expand Down Expand Up @@ -463,7 +464,8 @@ object evaluator extends EvaluationRules {
val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ)))
val (s2, pmDef) = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s1.program))) {
val (s2, smDef, pmDef) = quantifiedChunkSupporter.heapSummarisingMaps(s1, wand, formalVars, relevantChunks, v1)
val debugExp = new DebugExp(s"Predicate Trigger: ${identifier.toString}(${args.mkString})", InsertionOrderedSet.empty)
val argsString = bodyVars.map(e => s2.substituteVarsInExp(e)).mkString(", ")
val debugExp = new DebugExp(s"Predicate Trigger: ${identifier.toString}($argsString)")
v1.decider.assume(PredicateTrigger(identifier.toString, smDef.sm, args), debugExp)
(s2, pmDef)
} else {
Expand Down Expand Up @@ -493,7 +495,7 @@ object evaluator extends EvaluationRules {
val currentPermAmount = PermLookup(field.name, pmDef.pm, args.head)
v1.decider.prover.comment(s"perm($resacc) ~~> assume upper permission bound")
val debugExpr = ast.LeCmp(ast.CurrentPerm(resacc)(), ast.IntLit(1)())()
v1.decider.assume(PermAtMost(currentPermAmount, FullPerm), debugExpr)
v1.decider.assume(PermAtMost(currentPermAmount, FullPerm), s2.substituteVarsInExp(debugExpr))
(s2, currentPermAmount)

case predicate: ast.Predicate =>
Expand All @@ -504,7 +506,8 @@ object evaluator extends EvaluationRules {
s1, predicate, s1.predicateFormalVarMap(predicate), relevantChunks, v1)
if (s2.heapDependentTriggers.contains(predicate)){
val trigger = PredicateTrigger(predicate.name, smDef.sm, args)
val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}(${args.mkString})", InsertionOrderedSet.empty)
val argsString = args.mkString(", ") // TODO ake: exp + substitution
val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}($argsString)")
v1.decider.assume(trigger, debugExp)
}
(s2, PredicatePermLookup(identifier.toString, pmDef.pm, args))
Expand Down Expand Up @@ -777,7 +780,7 @@ object evaluator extends EvaluationRules {
consumes(s3, pres, _ => pvePre, v2)((s4, snap, v3) => {
val snap1 = snap.convert(sorts.Snap)
val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
v3.decider.assume(preFApp, fapp)
v3.decider.assume(preFApp, s4.substituteVarsInExp(fapp))
val tFApp = App(v3.symbolConverter.toFunction(func), snap1 :: tArgs)
val fr5 =
s4.functionRecorder.changeDepthBy(-1)
Expand Down Expand Up @@ -880,22 +883,22 @@ object evaluator extends EvaluationRules {
val failure = createFailure(pve dueTo SeqIndexExceedsLength(e0, e1), v1, s1)
if (s1.retryLevel == 0 && v1.reportFurtherErrors()) {
val debugExpr = ast.LeCmp(e1, ast.SeqLength(e0)())()
v1.decider.assume(Less(t1, SeqLength(t0)), debugExpr)
v1.decider.assume(Less(t1, SeqLength(t0)), s1.substituteVarsInExp(debugExpr))
failure combine Q(s1, SeqAt(t0, t1), v1)
} else failure}
case false =>
val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1)
if (s1.retryLevel == 0) {
val debugExpr = ast.GeCmp(e1, ast.IntLit(0)())()
v1.decider.assume(AtLeast(t1, IntLiteral(0)), debugExpr)
v1.decider.assume(AtLeast(t1, IntLiteral(0)), s1.substituteVarsInExp(debugExpr))
v1.decider.assert(Less(t1, SeqLength(t0))) {
case true =>
failure1 combine Q(s1, SeqAt(t0, t1), v1)
case false =>
val failure2 = failure1 combine createFailure(pve dueTo SeqIndexExceedsLength(e0, e1), v1, s1)
if (v1.reportFurtherErrors()) {
val debugExpr = ast.LeCmp(e1, ast.SeqLength(e0)())()
v1.decider.assume(Less(t1, SeqLength(t0)), debugExpr)
v1.decider.assume(Less(t1, SeqLength(t0)), s1.substituteVarsInExp(debugExpr))
failure2 combine Q(s1, SeqAt(t0, t1), v1)
} else failure2}
} else failure1}}})
Expand All @@ -921,22 +924,22 @@ object evaluator extends EvaluationRules {
val failure = createFailure(pve dueTo SeqIndexExceedsLength(e0, e1), v1, s1)
if (s1.retryLevel == 0 && v1.reportFurtherErrors()) {
val debugExpr = ast.LeCmp(e1, ast.SeqLength(e0)())()
v1.decider.assume(Less(t1, SeqLength(t0)), debugExpr)
v1.decider.assume(Less(t1, SeqLength(t0)), s1.substituteVarsInExp(debugExpr))
failure combine Q(s1, SeqUpdate(t0, t1, t2), v1)}
else failure}
case false =>
val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1)
if (s1.retryLevel == 0) {
val debugExpr = ast.GeCmp(e1, ast.IntLit(0)())()
v1.decider.assume(AtLeast(t1, IntLiteral(0)), debugExpr)
v1.decider.assume(AtLeast(t1, IntLiteral(0)), s1.substituteVarsInExp(debugExpr))
v1.decider.assert(Less(t1, SeqLength(t0))) {
case true =>
failure1 combine Q(s1, SeqUpdate(t0, t1, t2), v1)
case false =>
val failure2 = failure1 combine createFailure(pve dueTo SeqIndexExceedsLength(e0, e1), v1, s1)
if (v1.reportFurtherErrors()) {
val debugExpr = ast.LeCmp(e1, ast.SeqLength(e0)())()
v1.decider.assume(Less(t1, SeqLength(t0)), debugExpr)
v1.decider.assume(Less(t1, SeqLength(t0)), s1.substituteVarsInExp(debugExpr))
failure2 combine Q(s1, SeqUpdate(t0, t1, t2), v1)
} else failure2}
} else failure1}}})
Expand Down Expand Up @@ -1090,7 +1093,9 @@ object evaluator extends EvaluationRules {
val preMark = v1.decider.setPathConditionMark()
evals(s2, es1, _ => pve, v1)((s3, ts1, v2) => {
val bc = And(ts1)
v2.decider.setCurrentBranchCondition(bc, Some(viper.silicon.utils.ast.BigAnd(es1)))
val exp = viper.silicon.utils.ast.BigAnd(es1)
val expPair = Some(new Pair(exp, s1.substituteVarsInExp(exp)))
v2.decider.setCurrentBranchCondition(bc, expPair)
evals(s3, es2, _ => pve, v2)((s4, ts2, v3) => {
evalTriggers(s4, optTriggers.getOrElse(Nil), pve, v3)((s5, tTriggers, _) => { // TODO: v4 isn't forward - problem?
val (auxGlobals, auxNonGlobalQuants) =
Expand Down Expand Up @@ -1245,7 +1250,7 @@ object evaluator extends EvaluationRules {
val failure = createFailure(pve dueTo DivisionByZero(eDivisor), v, s)
if (s.retryLevel == 0 && v.reportFurtherErrors()) {
val debugExpr = ast.NeCmp(eDivisor, IntLit(0)())()
v.decider.assume(tDivisor !== tZero, debugExpr)
v.decider.assume(tDivisor !== tZero, s.substituteVarsInExp(debugExpr))
failure combine Q(s, t, v)
} else failure
}
Expand Down
18 changes: 9 additions & 9 deletions src/main/scala/rules/Executor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,7 @@ object executor extends ExecutionRules {
v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */

var invDebugExps = InsertionOrderedSet[DebugExp]().empty
invs.foreach(e => invDebugExps += new DebugExp(e))
invs.foreach(e => invDebugExps += new DebugExp(s3.substituteVarsInExp(e)))
v2.decider.assume(pcs.assumptions, new DebugExp("Loop invariant", invDebugExps))
v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
if (v2.decider.checkSmoke())
Expand Down Expand Up @@ -299,7 +299,7 @@ object executor extends ExecutionRules {

case ass @ ast.LocalVarAssign(x, rhs) =>
eval(s, rhs, AssignmentFailed(ass), v)((s1, tRhs, v1) => {
val t = ssaifyRhs(tRhs, rhs, x.name, x.typ, v)
val t = ssaifyRhs(tRhs, rhs, x.name, x.typ, v, s1)
Q(s1.copy(g = s1.g + (x, t)), v1)})

/* TODO: Encode assignments e1.f := e2 as
Expand Down Expand Up @@ -366,7 +366,7 @@ object executor extends ExecutionRules {
val ve = pve dueTo InsufficientPermission(fa)
val description = s"consume ${ass.pos}: $ass"
chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), FullPerm, ve, v2, description)((s3, h3, _, v3) => {
val tSnap = ssaifyRhs(tRhs, rhs, field.name, field.typ, v3)
val tSnap = ssaifyRhs(tRhs, rhs, field.name, field.typ, v3, s3)
val id = BasicChunkIdentifier(field.name)
val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), tSnap, FullPerm)
chunkSupporter.produce(s3, h3, newChunk, v3)((s4, h4, v4) =>
Expand All @@ -378,7 +378,7 @@ object executor extends ExecutionRules {
case ast.NewStmt(x, fields) =>
val tRcvr = v.decider.fresh(x)
val debugExpr = ast.NeCmp(x, ast.NullLit()())()
v.decider.assume(tRcvr !== Null, debugExpr)
v.decider.assume(tRcvr !== Null, s.substituteVarsInExp(debugExpr))
val newChunks = fields map (field => {
val p = FullPerm
val snap = v.decider.fresh(field.name, v.symbolConverter.toSort(field.typ))
Expand Down Expand Up @@ -541,8 +541,8 @@ object executor extends ExecutionRules {
val (smDef1, smCache1) =
quantifiedChunkSupporter.summarisingSnapshotMap(
s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
val eArgsStr = eArgs.mkString(", ")
val debugExp = new DebugExp(s"Predicate Trigger ${predicate.name}($eArgsStr)", pa, InsertionOrderedSet.empty)
val eArgsStr = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
val debugExp = new DebugExp(s"Predicate Trigger ${predicate.name}($eArgsStr)", s2.substituteVarsInExp(pa), InsertionOrderedSet.empty)
v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
smCache1
} else {
Expand Down Expand Up @@ -635,7 +635,7 @@ object executor extends ExecutionRules {
executed
}

private def ssaifyRhs(rhs: Term, rhsExp: ast.Exp, name: String, typ: ast.Type, v: Verifier): Term = {
private def ssaifyRhs(rhs: Term, rhsExp: ast.Exp, name: String, typ: ast.Type, v: Verifier, s : State): Term = {
rhs match {
case _: Var | _: Literal =>
rhs
Expand All @@ -652,8 +652,8 @@ object executor extends ExecutionRules {
* reported by Silicon issue #328.
*/
val t = v.decider.fresh(name, v.symbolConverter.toSort(typ))
val debugExpr = ast.EqCmp(ast.LocalVar(name, typ)(), rhsExp)()
v.decider.assume(t === rhs, debugExpr)
val debugExpr = ast.EqCmp(ast.LocalVar(t.toString, typ)(), rhsExp)()
v.decider.assume(t === rhs, s.substituteVarsInExp(debugExpr))
t
}
}
Expand Down
5 changes: 4 additions & 1 deletion src/main/scala/rules/MagicWandSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@

package viper.silicon.rules

import org.jgrapht.alg.util.Pair
import viper.silver.ast
import viper.silver.ast.{Exp, Stmt}
import viper.silver.cfg.Edge
Expand Down Expand Up @@ -380,7 +381,9 @@ object magicWandSupporter extends SymbolicExecutionRules {
parallelizeBranches = s.parallelizeBranches /* See comment above */
/*branchConditions = c.branchConditions*/)
executionFlowController.locally(s1, v)((s2, v1) => {
v1.decider.setCurrentBranchCondition(And(branchConditions), Some(viper.silicon.utils.ast.BigAnd(branchConditionsExp.flatten)))
val exp = viper.silicon.utils.ast.BigAnd(branchConditionsExp.flatten)
val expPair = Some(new Pair(exp, s1.substituteVarsInExp(exp)))
v1.decider.setCurrentBranchCondition(And(branchConditions), expPair)
val debugExp = new DebugExp("Test", InsertionOrderedSet.empty)
conservedPcs.foreach(pcs => v1.decider.assume(pcs.conditionalized, debugExp))
Q(s2, magicWandChunk, v1)})}})
Expand Down
Loading

0 comments on commit 4459d67

Please sign in to comment.