diff options
| -rw-r--r-- | Source/Core/Absy.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 189 |
2 files changed, 191 insertions, 0 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 8be4f24e..8a8558bf 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2241,6 +2241,7 @@ namespace Microsoft.Boogie { } public class Incarnation : LocalVariable { public int incarnationNumber; + public readonly Variable OriginalVariable; public Incarnation(Variable/*!*/ var, int i) : base( var.tok, @@ -2248,6 +2249,7 @@ namespace Microsoft.Boogie { ) { Contract.Requires(var != null); incarnationNumber = i; + OriginalVariable = var; } } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 2762fc72..ad067c04 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2830,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 @@ -2865,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") || |