summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/VC.cs')
-rw-r--r--Source/VCGeneration/VC.cs228
1 files changed, 214 insertions, 14 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 33e2f928..ad067c04 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1386,7 +1386,8 @@ namespace VC {
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
+ var namedAssumeVars = new List<VCExprVar>();
+ VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars);
Contract.Assert(vc != null);
if (!CommandLineOptions.Clo.UseLabels)
@@ -1414,7 +1415,7 @@ namespace VC {
string desc = cce.NonNull(impl.Name);
if (no >= 0)
desc += "_split" + no;
- checker.BeginCheck(desc, vc, reporter);
+ checker.BeginCheck(desc, vc, reporter, namedAssumeVars);
}
private void SoundnessCheck(HashSet<List<Block>/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {
@@ -1519,7 +1520,7 @@ namespace VC {
}
}
- public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
+ public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null)
{
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
@@ -1527,10 +1528,10 @@ namespace VC {
Contract.Ensures(Contract.Result<VCExpr>() != null);
label2absy = new Dictionary<int, Absy>();
- return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
+ return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars);
}
- public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
+ public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null) {
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1567,7 +1568,8 @@ namespace VC {
}
break;
case CommandLineOptions.VCVariety.DagIterative:
- vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
+ // TODO(wuestholz): Support named assume statements not just for this encoding.
+ vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars);
break;
case CommandLineOptions.VCVariety.Doomed:
vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);
@@ -2021,6 +2023,16 @@ namespace VC {
protected ProverContext/*!*/ context;
Program/*!*/ program;
+ public IEnumerable<string> NecessaryAssumes
+ {
+ get { return program.NecessaryAssumes; }
+ }
+
+ public void AddNecessaryAssume(string id)
+ {
+ program.NecessaryAssumes.Add(id);
+ }
+
public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
@@ -2229,10 +2241,11 @@ namespace VC {
impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })));
ResetPredecessors(impl.Blocks);
- if(CommandLineOptions.Clo.KInductionDepth < 0) {
+ var k = Math.Max(CommandLineOptions.Clo.KInductionDepth, QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1));
+ if(k < 0) {
ConvertCFG2DAGStandard(impl, edgesCut, taskID);
} else {
- ConvertCFG2DAGKInduction(impl, edgesCut, taskID);
+ ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k);
}
#region Debug Tracing
@@ -2497,14 +2510,12 @@ namespace VC {
return referencedVars;
}
- private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID) {
+ private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID, int inductionK) {
// K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses
Contract.Requires(edgesCut == null);
Contract.Requires(taskID == -1);
-
- int inductionK = CommandLineOptions.Clo.KInductionDepth;
- Contract.Assume(inductionK >= 0);
+ Contract.Requires(0 <= inductionK);
bool contRuleApplication = true;
while (contRuleApplication) {
@@ -2819,6 +2830,11 @@ namespace VC {
mvInfo = new ModelViewInfo(program, impl);
Convert2PassiveCmd(impl, mvInfo);
+ if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation"))
+ {
+ InstrumentWithMayUnverifiedConditions(impl, exitBlock);
+ }
+
#region Peep-hole optimizations
if (CommandLineOptions.Clo.RemoveEmptyBlocks){
#region Get rid of empty blocks
@@ -2854,6 +2870,190 @@ namespace VC {
return gotoCmdOrigins;
}
+ #region Simplified May-Unverified Analysis and Instrumentation
+
+ static void InstrumentWithMayUnverifiedConditions(Implementation impl, Block unifiedExitBlock)
+ {
+ var q = new Queue<Block>();
+ q.Enqueue(unifiedExitBlock);
+ var conditionOnBlockEntry = new Dictionary<Block, HashSet<Variable>>();
+ while (q.Any())
+ {
+ var block = q.Dequeue();
+
+ if (conditionOnBlockEntry.ContainsKey(block))
+ {
+ continue;
+ }
+
+ var gotoCmd = block.TransferCmd as GotoCmd;
+ if (gotoCmd != null && gotoCmd.labelTargets.Any(b => !conditionOnBlockEntry.ContainsKey(b)))
+ {
+ q.Enqueue(block);
+ continue;
+ }
+
+ HashSet<Variable> cond = new HashSet<Variable>();
+ if (gotoCmd != null)
+ {
+ var mayInstrs = new List<Block>();
+ bool noInstr = true;
+ foreach (var succ in gotoCmd.labelTargets)
+ {
+ var c = conditionOnBlockEntry[succ];
+ if (c != null)
+ {
+ mayInstrs.Add(succ);
+ }
+ else
+ {
+ noInstr = false;
+ }
+ cond = JoinVariableSets(cond, c);
+ }
+ if (!noInstr)
+ {
+ foreach (var instr in mayInstrs)
+ {
+ InstrumentWithCondition(instr, 0, conditionOnBlockEntry[instr]);
+ }
+ }
+ }
+
+ for (int i = block.Cmds.Count - 1; 0 <= i; i--)
+ {
+ var cmd = block.Cmds[i];
+ if (cond == null) { break; }
+
+ var assertCmd = cmd as AssertCmd;
+ if (assertCmd != null)
+ {
+ var litExpr = assertCmd.Expr as LiteralExpr;
+ if (litExpr != null && litExpr.IsTrue)
+ {
+ continue;
+ }
+
+ HashSet<Variable> vu = null;
+ if (assertCmd.VerifiedUnder == null)
+ {
+ vu = null;
+ }
+ else
+ {
+ HashSet<Variable> vars;
+ if (IsConjunctionOfAssumptionVariables(assertCmd.VerifiedUnder, out vars))
+ {
+ vu = vars;
+ // TODO(wuestholz): Maybe drop the :verified_under attribute.
+ }
+ else
+ {
+ vu = null;
+ }
+ }
+
+ if (vu == null)
+ {
+ InstrumentWithCondition(block, i + 1, cond);
+ }
+
+ cond = JoinVariableSets(cond, vu);
+ }
+ }
+
+ if (cond != null && block.Predecessors.Count == 0)
+ {
+ // TODO(wuestholz): Should we rather instrument each block?
+ InstrumentWithCondition(block, 0, cond);
+ }
+
+ foreach (var pred in block.Predecessors)
+ {
+ q.Enqueue(pred);
+ }
+
+ conditionOnBlockEntry[block] = cond;
+ }
+ }
+
+ private static void InstrumentWithCondition(Block block, int idx, HashSet<Variable> condition)
+ {
+ var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr)new IdentifierExpr(Token.NoToken, v)).ToList());
+ block.Cmds.Insert(idx, new AssumeCmd(Token.NoToken, Expr.Not(conj)));
+ }
+
+ static HashSet<Variable> JoinVariableSets(HashSet<Variable> c0, HashSet<Variable> c1)
+ {
+ // We use the following lattice:
+ // - Top: null (i.e., true)
+ // - Bottom: new HashSet<Variable>() (i.e., false)
+ // - Other Elements: new HashSet<Variable>(...) (i.e., conjunctions of assumption variables)
+
+ if (c0 == null || c1 == null)
+ {
+ return null;
+ }
+ var result = new HashSet<Variable>(c0);
+ result.UnionWith(c1);
+ return result;
+ }
+
+ static bool IsAssumptionVariableOrIncarnation(Variable v)
+ {
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "assumption")) { return true; }
+ var incar = v as Incarnation;
+ return incar == null || QKeyValue.FindBoolAttribute(incar.OriginalVariable.Attributes, "assumption");
+ }
+
+ static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet<Variable> variables)
+ {
+ Contract.Requires(expr != null);
+
+ variables = null;
+ var litExpr = expr as LiteralExpr;
+ if (litExpr != null && (litExpr.IsFalse || litExpr.IsTrue))
+ {
+ if (litExpr.IsTrue)
+ {
+ variables = new HashSet<Variable>();
+ }
+ return true;
+ }
+
+ var idExpr = expr as IdentifierExpr;
+ if (idExpr != null && IsAssumptionVariableOrIncarnation(idExpr.Decl))
+ {
+ variables = new HashSet<Variable>();
+ variables.Add(idExpr.Decl);
+ return true;
+ }
+
+ var andExpr = expr as NAryExpr;
+ if (andExpr != null)
+ {
+ var fun = andExpr.Fun as BinaryOperator;
+ if (fun != null && fun.Op == BinaryOperator.Opcode.And && andExpr.Args != null)
+ {
+ bool res = true;
+ variables = new HashSet<Variable>();
+ foreach (var op in andExpr.Args)
+ {
+ HashSet<Variable> vars;
+ var r = IsConjunctionOfAssumptionVariables(op, out vars);
+ res &= r;
+ variables = JoinVariableSets(variables, vars);
+ if (!res) { break; }
+ }
+ return res;
+ }
+ }
+
+ return false;
+ }
+
+ #endregion
+
private static void HandleSelectiveChecking(Implementation impl)
{
if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") ||
@@ -3193,7 +3393,7 @@ namespace VC {
Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount,
- bool isPositiveContext = true)
+ bool isPositiveContext = true, IList<VCExprVar> namedAssumeVars = null)
{
Contract.Requires(blocks != null);
Contract.Requires(proverCtxt != null);
@@ -3253,7 +3453,7 @@ namespace VC {
}
VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);
- VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+ VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars);
assertionCount += context.AssertionCount;
VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 19:18:24 +0000