summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/StratifiedVC.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/StratifiedVC.cs')
-rw-r--r--Source/VCGeneration/StratifiedVC.cs5809
1 files changed, 2906 insertions, 2903 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 037fa2be..789f86f5 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1,2903 +1,2906 @@
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.Diagnostics;
-using System.Linq;
-using System.Text;
-using System.IO;
-using Microsoft.Boogie;
-using Microsoft.Boogie.GraphUtil;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-
-namespace VC {
- using Bpl = Microsoft.Boogie;
-
- public class StratifiedVC {
- public StratifiedInliningInfo info;
- public int id;
- public List<VCExprVar> interfaceExprVars;
-
- // boolControlVC (block -> its bool variable)
- public Dictionary<Block, VCExpr> blockToControlVar;
- // While using labels (block -> its label)
- public Dictionary<Absy, string> block2label;
-
- public Dictionary<Block, List<StratifiedCallSite>> callSites;
- public Dictionary<Block, List<StratifiedCallSite>> recordProcCallSites;
- public VCExpr vcexpr;
-
- // Must-Reach Information
- Dictionary<Block, VCExprVar> mustReachVar;
- List<VCExprLetBinding> mustReachBindings;
-
- public StratifiedVC(StratifiedInliningInfo siInfo, HashSet<string> procCalls) {
- info = siInfo;
- info.GenerateVC();
- var vcgen = info.vcgen;
- var prover = vcgen.prover;
- VCExpressionGenerator gen = prover.VCExprGen;
- var bet = prover.Context.BoogieExprTranslator;
-
- vcexpr = info.vcexpr;
- id = vcgen.CreateNewId();
- interfaceExprVars = new List<VCExprVar>();
- Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
- foreach (VCExprVar v in info.interfaceExprVars) {
- VCExprVar newVar = vcgen.CreateNewVar(v.Type);
- interfaceExprVars.Add(newVar);
- substDict.Add(v, newVar);
- }
- foreach (VCExprVar v in info.privateExprVars) {
- substDict.Add(v, vcgen.CreateNewVar(v.Type));
- }
- if(info.controlFlowVariable != null)
- substDict.Add(bet.LookupVariable(info.controlFlowVariable), gen.Integer(BigNum.FromInt(id)));
- VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
- SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
- vcexpr = substVisitor.Mutate(vcexpr, subst);
-
- // For BoolControlVC generation
- if (info.blockToControlVar != null)
- {
- blockToControlVar = new Dictionary<Block, VCExpr>();
- foreach (var tup in info.blockToControlVar)
- blockToControlVar.Add(tup.Key, substDict[tup.Value]);
- }
-
- // labels
- if (info.label2absy != null)
- {
- block2label = new Dictionary<Absy, string>();
- vcexpr = RenameVCExprLabels.Apply(vcexpr, info.vcgen.prover.VCExprGen, info.label2absy, block2label);
- }
-
- if(procCalls != null)
- vcexpr = RemoveProcedureCalls.Apply(vcexpr, info.vcgen.prover.VCExprGen, procCalls);
-
- callSites = new Dictionary<Block, List<StratifiedCallSite>>();
- foreach (Block b in info.callSites.Keys) {
- callSites[b] = new List<StratifiedCallSite>();
- foreach (CallSite cs in info.callSites[b]) {
- callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst));
- }
- }
-
- recordProcCallSites = new Dictionary<Block, List<StratifiedCallSite>>();
- foreach (Block b in info.recordProcCallSites.Keys) {
- recordProcCallSites[b] = new List<StratifiedCallSite>();
- foreach (CallSite cs in info.recordProcCallSites[b]) {
- recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst));
- }
- }
- }
-
- public VCExpr MustReach(Block block)
- {
- Contract.Assert(!CommandLineOptions.Clo.UseLabels);
-
- // This information is computed lazily
- if (mustReachBindings == null)
- {
- var vcgen = info.vcgen;
- var gen = vcgen.prover.VCExprGen;
- var impl = info.impl;
- mustReachVar = new Dictionary<Block, VCExprVar>();
- mustReachBindings = new List<VCExprLetBinding>();
- foreach (Block b in impl.Blocks)
- mustReachVar[b] = vcgen.CreateNewVar(Bpl.Type.Bool);
-
- var dag = new Graph<Block>();
- dag.AddSource(impl.Blocks[0]);
- foreach (Block b in impl.Blocks)
- {
- var gtc = b.TransferCmd as GotoCmd;
- if (gtc != null)
- foreach (Block dest in gtc.labelTargets)
- dag.AddEdge(dest, b);
- }
- IEnumerable sortedNodes = dag.TopologicalSort();
-
- foreach (Block currBlock in dag.TopologicalSort())
- {
- if (currBlock == impl.Blocks[0])
- {
- mustReachBindings.Add(gen.LetBinding(mustReachVar[currBlock], VCExpressionGenerator.True));
- continue;
- }
-
- VCExpr expr = VCExpressionGenerator.False;
- foreach (var pred in dag.Successors(currBlock))
- {
- VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(pred.UniqueId)));
- VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(currBlock.UniqueId)));
- expr = gen.Or(expr, gen.And(mustReachVar[pred], controlTransferExpr));
- }
- mustReachBindings.Add(gen.LetBinding(mustReachVar[currBlock], expr));
- }
- }
-
- Contract.Assert(mustReachVar.ContainsKey(block));
- return info.vcgen.prover.VCExprGen.Let(mustReachBindings, mustReachVar[block]);
- }
-
- public List<StratifiedCallSite> CallSites {
- get {
- var ret = new List<StratifiedCallSite>();
- foreach (var b in callSites.Keys) {
- foreach (var cs in callSites[b]) {
- ret.Add(cs);
- }
- }
- return ret;
- }
- }
-
- public List<StratifiedCallSite> RecordProcCallSites {
- get {
- var ret = new List<StratifiedCallSite>();
- foreach (var b in recordProcCallSites.Keys) {
- foreach (var cs in recordProcCallSites[b]) {
- ret.Add(cs);
- }
- }
- return ret;
- }
- }
-
- public override string ToString()
- {
- return info.impl.Name;
- }
- }
-
- // Rename all labels in a VC to (globally) fresh labels
- class RenameVCExprLabels : MutatingVCExprVisitor<bool>
- {
- Dictionary<int, Absy> label2absy;
- Dictionary<Absy, string> absy2newlabel;
- static int counter = 11;
-
- RenameVCExprLabels(VCExpressionGenerator gen, Dictionary<int, Absy> label2absy, Dictionary<Absy, string> absy2newlabel)
- : base(gen)
- {
- this.label2absy = label2absy;
- this.absy2newlabel = absy2newlabel;
- }
-
- public static VCExpr Apply(VCExpr expr, VCExpressionGenerator gen, Dictionary<int, Absy> label2absy, Dictionary<Absy, string> absy2newlabel)
- {
- return (new RenameVCExprLabels(gen, label2absy, absy2newlabel)).Mutate(expr, true);
- }
-
- // Finds labels and changes them to a globally unique label:
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- bool changed,
- bool arg)
- {
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr ret;
- if (changed)
- ret = Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- ret = originalNode;
-
- VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
- if (lop == null) return ret;
- if (!(ret is VCExprNAry)) return ret;
- VCExprNAry retnary = (VCExprNAry)ret;
-
- // remove the sign
- var nosign = 0;
- if (!Int32.TryParse(lop.label.Substring(1), out nosign))
- return ret;
-
- if (!label2absy.ContainsKey(nosign))
- return ret;
-
- string newLabel = "SI" + counter.ToString();
- counter++;
- absy2newlabel[label2absy[nosign]] = newLabel;
-
- if (lop.pos)
- {
- return Gen.LabelPos(newLabel, retnary[0]);
- }
- else
- {
- return Gen.LabelNeg(newLabel, retnary[0]);
- }
-
- }
- }
-
- // Remove the uninterpreted function calls that substitute procedure calls
- class RemoveProcedureCalls : MutatingVCExprVisitor<bool>
- {
- HashSet<string> procNames;
-
- RemoveProcedureCalls(VCExpressionGenerator gen, HashSet<string> procNames)
- : base(gen)
- {
- this.procNames = procNames;
- }
-
- public static VCExpr Apply(VCExpr expr, VCExpressionGenerator gen, HashSet<string> procNames)
- {
- return (new RemoveProcedureCalls(gen, procNames)).Mutate(expr, true);
- }
-
- // Finds labels and changes them to a globally unique label:
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- bool changed,
- bool arg)
- {
- //Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr ret;
- if (changed)
- ret = Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- ret = originalNode;
-
- if (!(ret is VCExprNAry)) return ret;
- VCExprNAry retnary = (VCExprNAry)ret;
- if (!(retnary.Op is VCExprBoogieFunctionOp))
- return ret;
-
- var fcall = (retnary.Op as VCExprBoogieFunctionOp).Func.Name;
- if (procNames.Contains(fcall))
- return VCExpressionGenerator.True;
- return ret;
- }
- }
-
-
- public class CallSite {
- public string calleeName;
- public List<VCExpr> interfaceExprs;
- public Block block;
- public int numInstr; // for TraceLocation
- public VCExprVar callSiteVar;
- public QKeyValue Attributes; // attributes on the call cmd
- public CallSite(string callee, List<VCExpr> interfaceExprs, VCExprVar callSiteVar, Block block, int numInstr, QKeyValue Attributes)
- {
- this.calleeName = callee;
- this.interfaceExprs = interfaceExprs;
- this.callSiteVar = callSiteVar;
- this.block = block;
- this.numInstr = numInstr;
- this.Attributes = Attributes;
- }
- }
-
- public class StratifiedCallSite {
- public CallSite callSite;
- public List<VCExpr> interfaceExprs;
- public VCExpr callSiteExpr;
-
- public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst) {
- callSite = cs;
- interfaceExprs = new List<VCExpr>();
- foreach (VCExpr v in cs.interfaceExprs) {
- interfaceExprs.Add(substVisitor.Mutate(v, subst));
- }
- if (callSite.callSiteVar != null)
- callSiteExpr = substVisitor.Mutate(callSite.callSiteVar, subst);
- }
-
- public VCExpr Attach(StratifiedVC svc) {
- Contract.Assert(interfaceExprs.Count == svc.interfaceExprVars.Count);
- StratifiedInliningInfo info = svc.info;
- ProverInterface prover = info.vcgen.prover;
- VCExpressionGenerator gen = prover.VCExprGen;
-
- Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
- for (int i = 0; i < svc.interfaceExprVars.Count; i++) {
- VCExprVar v = svc.interfaceExprVars[i];
- substDict.Add(v, interfaceExprs[i]);
- }
- VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
- SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
- svc.vcexpr = substVisitor.Mutate(svc.vcexpr, subst);
- foreach (StratifiedCallSite scs in svc.CallSites) {
- List<VCExpr> newInterfaceExprs = new List<VCExpr>();
- foreach (VCExpr expr in scs.interfaceExprs) {
- newInterfaceExprs.Add(substVisitor.Mutate(expr, subst));
- }
- scs.interfaceExprs = newInterfaceExprs;
- }
- foreach (StratifiedCallSite scs in svc.RecordProcCallSites) {
- List<VCExpr> newInterfaceExprs = new List<VCExpr>();
- foreach (VCExpr expr in scs.interfaceExprs) {
- newInterfaceExprs.Add(substVisitor.Mutate(expr, subst));
- }
- scs.interfaceExprs = newInterfaceExprs;
- }
- //return gen.Implies(callSiteExpr, svc.vcexpr);
- return svc.vcexpr;
- }
-
- public override string ToString()
- {
- return callSite.calleeName;
- }
- }
-
- public class StratifiedInliningInfo {
- public StratifiedVCGenBase vcgen;
- public Implementation impl;
- public Function function;
- public Variable controlFlowVariable;
- public Cmd exitAssertCmd;
- public VCExpr vcexpr;
- public List<VCExprVar> interfaceExprVars;
- public List<VCExprVar> privateExprVars;
- public Dictionary<int, Absy> label2absy;
- public ModelViewInfo mvInfo;
- public Dictionary<Block, List<CallSite>> callSites;
- public Dictionary<Block, List<CallSite>> recordProcCallSites;
- public bool initialized { get; private set; }
- // Instrumentation to apply after PassiveImpl, but before VCGen
- Action<Implementation> PassiveImplInstrumentation;
-
- // boolControlVC (block -> its Bool variable)
- public Dictionary<Block, VCExprVar> blockToControlVar;
-
- public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen, Action<Implementation> PassiveImplInstrumentation) {
- vcgen = stratifiedVcGen;
- impl = implementation;
- this.PassiveImplInstrumentation = PassiveImplInstrumentation;
-
- List<Variable> functionInterfaceVars = new List<Variable>();
- foreach (Variable v in vcgen.program.GlobalVariables) {
- functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
- }
- foreach (Variable v in impl.InParams) {
- functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
- }
- foreach (Variable v in impl.OutParams) {
- functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
- }
- foreach (IdentifierExpr e in impl.Proc.Modifies) {
- if (e.Decl == null) continue;
- functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", e.Decl.TypedIdent.Type), true));
- }
- Formal returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false);
- function = new Function(Token.NoToken, impl.Name, functionInterfaceVars, returnVar);
- vcgen.prover.Context.DeclareFunction(function, "");
-
- List<Expr> exprs = new List<Expr>();
- foreach (Variable v in vcgen.program.GlobalVariables) {
- Contract.Assert(v != null);
- exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
- }
- foreach (Variable v in impl.Proc.InParams) {
- Contract.Assert(v != null);
- exprs.Add(new IdentifierExpr(Token.NoToken, v));
- }
- foreach (Variable v in impl.Proc.OutParams) {
- Contract.Assert(v != null);
- exprs.Add(new IdentifierExpr(Token.NoToken, v));
- }
- foreach (IdentifierExpr ie in impl.Proc.Modifies) {
- Contract.Assert(ie != null);
- if (ie.Decl == null)
- continue;
- exprs.Add(ie);
- }
- Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
- impl.Proc.Ensures.Add(new Ensures(Token.NoToken, true, freePostExpr, "", new QKeyValue(Token.NoToken, "si_fcall", new List<object>(), null)));
-
- initialized = false;
- }
-
- public void GenerateVCBoolControl()
- {
- Debug.Assert(!initialized);
- Debug.Assert(CommandLineOptions.Clo.SIBoolControlVC);
-
- // fix names for exit variables
- var outputVariables = new List<Variable>();
- var assertConjuncts = new List<Expr>();
- foreach (Variable v in impl.OutParams)
- {
- Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
- outputVariables.Add(c);
- Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
- assertConjuncts.Add(eqExpr);
- }
- foreach (IdentifierExpr e in impl.Proc.Modifies)
- {
- if (e.Decl == null) continue;
- Variable v = e.Decl;
- Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
- outputVariables.Add(c);
- Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
- assertConjuncts.Add(eqExpr);
- }
- exitAssertCmd = new AssumeCmd(Token.NoToken, Expr.BinaryTreeAnd(assertConjuncts));
- (exitAssertCmd as AssumeCmd).Attributes = new QKeyValue(Token.NoToken, "exitAssert", new List<object>(), null);
-
- // no need for label2absy
- label2absy = new Dictionary<int, Absy>();
-
- // Passify
- Program program = vcgen.program;
- ProverInterface proverInterface = vcgen.prover;
- vcgen.ConvertCFG2DAG(impl);
- vcgen.PassifyImpl(impl, out mvInfo);
-
- VCExpressionGenerator gen = proverInterface.VCExprGen;
- var exprGen = proverInterface.Context.ExprGen;
- var translator = proverInterface.Context.BoogieExprTranslator;
-
- // add a boolean variable at each call site
- vcgen.InstrumentCallSites(impl);
-
- // typecheck
- var tc = new TypecheckingContext(null);
- impl.Typecheck(tc);
-
- ///////////////////
- // Generate the VC
- ///////////////////
-
- // block -> bool variable
- blockToControlVar = new Dictionary<Block, VCExprVar>();
- foreach (var b in impl.Blocks)
- blockToControlVar.Add(b, gen.Variable(b.Label + "_holds", Bpl.Type.Bool));
-
- vcexpr = VCExpressionGenerator.True;
- foreach (var b in impl.Blocks)
- {
- // conjoin all assume cmds
- VCExpr c = VCExpressionGenerator.True;
- foreach (var cmd in b.Cmds)
- {
- var acmd = cmd as AssumeCmd;
- if (acmd == null)
- {
- Debug.Assert(cmd is AssertCmd && (cmd as AssertCmd).Expr is LiteralExpr &&
- ((cmd as AssertCmd).Expr as LiteralExpr).IsTrue);
- continue;
- }
- var expr = translator.Translate(acmd.Expr);
- // Label the assume if it is a procedure call
- NAryExpr naryExpr = acmd.Expr as NAryExpr;
- if (naryExpr != null && naryExpr.Fun is FunctionCall)
- {
- var id = acmd.UniqueId;
- label2absy[id] = acmd;
- expr = gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), expr);
- }
-
- c = gen.AndSimp(c, expr);
- }
-
- // block implies a disjunction of successors
- Debug.Assert(!(b.TransferCmd is ReturnExprCmd), "Not supported");
- var gc = b.TransferCmd as GotoCmd;
- if (gc != null)
- {
- VCExpr succ = VCExpressionGenerator.False;
- foreach (var sb in gc.labelTargets)
- succ = gen.OrSimp(succ, blockToControlVar[sb]);
- c = gen.AndSimp(c, succ);
- }
- else
- {
- // nothing to do
- }
- vcexpr = gen.AndSimp(vcexpr, gen.Eq(blockToControlVar[b], c));
- }
- // assert start block
- vcexpr = gen.AndSimp(vcexpr, blockToControlVar[impl.Blocks[0]]);
-
- //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);
- // Collect other information
- callSites = vcgen.CollectCallSites(impl);
- recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);
-
- // record interface variables
- privateExprVars = new List<VCExprVar>();
- foreach (Variable v in impl.LocVars)
- {
- privateExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in impl.OutParams)
- {
- privateExprVars.Add(translator.LookupVariable(v));
- }
- privateExprVars.AddRange(blockToControlVar.Values);
-
- interfaceExprVars = new List<VCExprVar>();
- foreach (Variable v in program.GlobalVariables)
- {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in impl.InParams)
- {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in outputVariables)
- {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
- }
-
- public void GenerateVC() {
- if (initialized) return;
- if (CommandLineOptions.Clo.SIBoolControlVC)
- {
- GenerateVCBoolControl();
- initialized = true;
- return;
- }
- List<Variable> outputVariables = new List<Variable>();
- List<Expr> assertConjuncts = new List<Expr>();
- foreach (Variable v in impl.OutParams) {
- Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
- outputVariables.Add(c);
- Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
- assertConjuncts.Add(eqExpr);
- }
- foreach (IdentifierExpr e in impl.Proc.Modifies) {
- if (e.Decl == null) continue;
- Variable v = e.Decl;
- Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
- outputVariables.Add(c);
- Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
- assertConjuncts.Add(eqExpr);
- }
- exitAssertCmd = new AssertCmd(Token.NoToken, Expr.Not(Expr.BinaryTreeAnd(assertConjuncts)));
-
- Program program = vcgen.program;
- ProverInterface proverInterface = vcgen.prover;
- vcgen.ConvertCFG2DAG(impl);
- vcgen.PassifyImpl(impl, out mvInfo);
-
- if (PassiveImplInstrumentation != null)
- PassiveImplInstrumentation(impl);
-
- VCExpressionGenerator gen = proverInterface.VCExprGen;
- var exprGen = proverInterface.Context.ExprGen;
- var translator = proverInterface.Context.BoogieExprTranslator;
-
- VCExpr controlFlowVariableExpr = null;
- if (!CommandLineOptions.Clo.UseLabels) {
- controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
- controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);
- }
-
- vcgen.InstrumentCallSites(impl);
-
- label2absy = new Dictionary<int, Absy>();
- VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);
- translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
- vcexpr = gen.Not(vcgen.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverInterface.Context));
-
- if (controlFlowVariableExpr != null)
- {
- VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));
- VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
- vcexpr = exprGen.And(eqExpr, vcexpr);
- }
-
- callSites = vcgen.CollectCallSites(impl);
- recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);
-
- privateExprVars = new List<VCExprVar>();
- foreach (Variable v in impl.LocVars) {
- privateExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in impl.OutParams) {
- privateExprVars.Add(translator.LookupVariable(v));
- }
-
- interfaceExprVars = new List<VCExprVar>();
- foreach (Variable v in program.GlobalVariables) {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in impl.InParams) {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in outputVariables) {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
-
- initialized = true;
- }
- }
-
- public abstract class StratifiedVCGenBase : VCGen {
- public readonly static string recordProcName = "boogie_si_record";
- public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
- public ProverInterface prover;
-
- public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers, Action<Implementation> PassiveImplInstrumentation)
- : base(program, logFilePath, appendLogFile, checkers) {
- implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();
- prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
- foreach (var impl in program.Implementations) {
- implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this, PassiveImplInstrumentation);
- }
- GenerateRecordFunctions();
- }
-
- private void GenerateRecordFunctions() {
- foreach (var proc in program.Procedures) {
- if (!proc.Name.StartsWith(recordProcName)) continue;
- Contract.Assert(proc.InParams.Count == 1);
-
- // Make a new function
- TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
- Contract.Assert(ti != null);
- Formal returnVar = new Formal(Token.NoToken, ti, false);
- Contract.Assert(returnVar != null);
-
- // Get record type
- var argtype = proc.InParams[0].TypedIdent.Type;
-
- var ins = new List<Variable>();
- ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));
-
- var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);
- prover.Context.DeclareFunction(recordFunc, "");
-
- var exprs = new List<Expr>();
- exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));
-
- Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);
- proc.Ensures.Add(new Ensures(true, freePostExpr));
- }
- }
-
- public override void Close() {
- prover.Close();
- base.Close();
- }
-
- public void InstrumentCallSites(Implementation implementation) {
- var callSiteId = 0;
- foreach (Block block in implementation.Blocks) {
- List<Cmd> newCmds = new List<Cmd>();
- for (int i = 0; i < block.Cmds.Count; i++) {
- Cmd cmd = block.Cmds[i];
- newCmds.Add(cmd);
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- if (assumeCmd == null) continue;
- NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
- if (naryExpr == null) continue;
- if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;
- Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "SICS" + callSiteId, Microsoft.Boogie.Type.Bool));
- implementation.LocVars.Add(callSiteVar);
- newCmds.Add(new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar)));
- callSiteId++;
- }
- block.Cmds = newCmds;
- }
- }
-
- public Dictionary<Block, List<CallSite>> CollectCallSites(Implementation implementation) {
- var callSites = new Dictionary<Block, List<CallSite>>();
- foreach (Block block in implementation.Blocks) {
- for (int i = 0; i < block.Cmds.Count; i++) {
- Cmd cmd = block.Cmds[i];
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- if (assumeCmd == null) continue;
- NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
- if (naryExpr == null) continue;
- if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;
- List<VCExpr> interfaceExprs = new List<VCExpr>();
- foreach (Expr e in naryExpr.Args) {
- interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e));
- }
- int instr = i;
- i++;
- AssumeCmd callSiteAssumeCmd = (AssumeCmd)block.Cmds[i];
- IdentifierExpr iexpr = (IdentifierExpr) callSiteAssumeCmd.Expr;
- CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr, assumeCmd.Attributes);
- if (!callSites.ContainsKey(block))
- callSites[block] = new List<CallSite>();
- callSites[block].Add(cs);
- }
- }
- return callSites;
- }
-
- public Dictionary<Block, List<CallSite>> CollectRecordProcedureCallSites(Implementation implementation) {
- var callSites = new Dictionary<Block, List<CallSite>>();
- foreach (Block block in implementation.Blocks) {
- for (int i = 0; i < block.Cmds.Count; i++) {
- AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd;
- if (assumeCmd == null) continue;
- NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
- if (naryExpr == null) continue;
- if (!naryExpr.Fun.FunctionName.StartsWith(recordProcName)) continue;
- List<VCExpr> interfaceExprs = new List<VCExpr>();
- foreach (Expr e in naryExpr.Args) {
- interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e));
- }
- CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, null, block, i, assumeCmd.Attributes);
- if (!callSites.ContainsKey(block))
- callSites[block] = new List<CallSite>();
- callSites[block].Add(cs);
- }
- }
- return callSites;
- }
-
- private int macroCountForStratifiedInlining = 0;
- public Macro CreateNewMacro() {
- string newName = "SIMacro@" + macroCountForStratifiedInlining.ToString();
- macroCountForStratifiedInlining++;
- return new Macro(Token.NoToken, newName, new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));
- }
- private int varCountForStratifiedInlining = 0;
- public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {
- string newName = "SIV@" + varCountForStratifiedInlining.ToString();
- varCountForStratifiedInlining++;
- Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));
- prover.Context.DeclareConstant(newVar, false, null);
- return prover.VCExprGen.Variable(newVar.Name, type);
- }
- private int idCountForStratifiedInlining = 0;
- public int CreateNewId() {
- return idCountForStratifiedInlining++;
- }
-
- // Used inside PassifyImpl
- protected override void addExitAssert(string implName, Block exitBlock) {
- if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {
- var exitAssertCmd = implName2StratifiedInliningInfo[implName].exitAssertCmd;
- if(exitAssertCmd != null) exitBlock.Cmds.Add(exitAssertCmd);
- }
- }
-
- public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {
- // Construct the set of inlined procs in the original program
- var inlinedProcs = new HashSet<string>();
- foreach (var decl in program.TopLevelDeclarations) {
- // Implementations
- if (decl is Implementation) {
- var impl = decl as Implementation;
- if (!(impl.Proc is LoopProcedure)) {
- inlinedProcs.Add(impl.Name);
- }
- }
-
- // And recording procedures
- if (decl is Procedure) {
- var proc = decl as Procedure;
- if (proc.Name.StartsWith(recordProcName)) {
- Debug.Assert(!(decl is LoopProcedure));
- inlinedProcs.Add(proc.Name);
- }
- }
- }
-
- return extractLoopTraceRec(
- new CalleeCounterexampleInfo(cex, new List<object>()),
- mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
- }
-
- protected override bool elIsLoop(string procname) {
- StratifiedInliningInfo info = null;
- if (implName2StratifiedInliningInfo.ContainsKey(procname)) {
- info = implName2StratifiedInliningInfo[procname];
- }
-
- if (info == null) return false;
-
- var lp = info.impl.Proc as LoopProcedure;
-
- if (lp == null) return false;
- return true;
- }
-
- public abstract Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars);
- }
-
- public class StratifiedVCGen : StratifiedVCGenBase {
- public bool PersistCallTree;
- public static HashSet<string> callTree = null;
- public int numInlined = 0;
- public int vcsize = 0;
- private HashSet<string> procsThatReachedRecBound;
- private Dictionary<string, int> extraRecBound;
-
- public StratifiedVCGen(bool usePrevCallTree, HashSet<string> prevCallTree,
- Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
- : this(program, logFilePath, appendLogFile, checkers)
- {
- if (usePrevCallTree) {
- callTree = prevCallTree;
- PersistCallTree = true;
- }
- else {
- PersistCallTree = false;
- }
- }
-
- public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
- : base(program, logFilePath, appendLogFile, checkers, null) {
- PersistCallTree = false;
- procsThatReachedRecBound = new HashSet<string>();
-
- extraRecBound = new Dictionary<string, int>();
- program.TopLevelDeclarations.OfType<Implementation>()
- .Iter(impl =>
- {
- var b = QKeyValue.FindIntAttribute(impl.Attributes, "SIextraRecBound", -1);
- if (b != -1) extraRecBound.Add(impl.Name, b);
- });
- }
-
- // Extra rec bound for procedures
- public int GetExtraRecBound(string procName) {
- if (!extraRecBound.ContainsKey(procName))
- return 0;
- else return extraRecBound[procName];
- }
-
- public class ApiChecker {
- public ProverInterface prover;
- public ProverInterface.ErrorHandler reporter;
-
- public ApiChecker(ProverInterface prover, ProverInterface.ErrorHandler reporter) {
- this.reporter = reporter;
- this.prover = prover;
- }
-
- private Outcome CheckVC() {
- prover.Check();
- ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter);
-
- return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
- }
-
- public Outcome CheckAssumptions(List<VCExpr> assumptions) {
- if (assumptions.Count == 0) {
- return CheckVC();
- }
-
- prover.Push();
- foreach (var a in assumptions) {
- prover.Assert(a, true);
- }
- Outcome ret = CheckVC();
- prover.Pop();
- return ret;
- }
-
- public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions) {
- List<int> unsatisfiedSoftAssumptions;
- ProverInterface.Outcome outcome = prover.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter);
- return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
- }
-
- public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore) {
- ProverInterface.Outcome outcome = prover.CheckAssumptions(assumptions, out unsatCore, reporter);
- return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
- }
- }
-
- // Store important information related to a single VerifyImplementation query
- public class VerificationState {
- // The call tree
- public FCallHandler calls;
- public ApiChecker checker;
- // For statistics
- public int vcSize;
- public int expansionCount;
-
- public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter) {
- prover.Assert(vcMain, true);
- this.calls = calls;
- this.checker = new ApiChecker(prover, reporter);
- vcSize = 0;
- expansionCount = 0;
- }
- }
-
- class FindLeastOORException : Exception
- {
- public Outcome outcome;
-
- public FindLeastOORException(string msg, Outcome outcome)
- : base(msg)
- {
- this.outcome = outcome;
- }
- }
-
- public override Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- // Record current time
- var startTime = DateTime.UtcNow;
-
- // No Max: avoids theorem prover restarts
- CommandLineOptions.Clo.MaxProverMemory = 0;
-
- // Initialize cache
- satQueryCache = new Dictionary<int, List<HashSet<string>>>();
- unsatQueryCache = new Dictionary<int, List<HashSet<string>>>();
-
- Contract.Assert(implName2StratifiedInliningInfo != null);
-
- // Build VCs for all procedures
- implName2StratifiedInliningInfo.Values
- .Iter(info => info.GenerateVC());
-
- // Get the VC of the current procedure
- VCExpr vcMain = implName2StratifiedInliningInfo[impl.Name].vcexpr;
- Dictionary<int, Absy> mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;
-
- // Find all procedure calls in vc and put labels on them
- FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
- calls.setCurrProcAsMain();
- vcMain = calls.Mutate(vcMain, true);
-
- try
- {
-
- // Put all of the necessary state into one object
- var vState = new VerificationState(vcMain, calls, prover, new EmptyErrorHandler());
-
- // We'll restore the original state of the theorem prover at the end
- // of this procedure
- vState.checker.prover.Push();
-
- // Do eager inlining
- while (calls.currCandidates.Count > 0)
- {
- List<int> toExpand = new List<int>();
-
- foreach (int id in calls.currCandidates)
- {
- Debug.Assert(calls.getRecursionBound(id) <= 1, "Recursion not supported");
- toExpand.Add(id);
- }
- DoExpansion(toExpand, vState);
- }
-
- // Find all the boolean constants
- var allConsts = new HashSet<VCExprVar>();
- foreach (var constant in program.Constants)
- {
- if (!allBoolVars.Contains(constant.Name)) continue;
- var v = prover.Context.BoogieExprTranslator.LookupVariable(constant);
- allConsts.Add(v);
- }
-
- // Now, lets start the algo
- var min = refinementLoop(vState.checker, new HashSet<VCExprVar>(), allConsts, allConsts);
-
- var ret = new HashSet<string>();
- foreach (var v in min)
- {
- //Console.WriteLine(v.Name);
- ret.Add(v.Name);
- }
- allBoolVars = ret;
-
- vState.checker.prover.Pop();
-
- return Outcome.Correct;
- }
- catch (FindLeastOORException e)
- {
- Console.WriteLine("Exception in FindLeastToVerify: {0}, {1}", e.Message, e.outcome);
- return e.outcome;
- }
- }
-
- private HashSet<VCExprVar> refinementLoop(ApiChecker apiChecker, HashSet<VCExprVar> trackedVars, HashSet<VCExprVar> trackedVarsUpperBound, HashSet<VCExprVar> allVars) {
- Debug.Assert(trackedVars.IsSubsetOf(trackedVarsUpperBound));
-
- // If we already know the fate of all vars, then we're done.
- if (trackedVars.Count == trackedVarsUpperBound.Count)
- return new HashSet<VCExprVar>(trackedVars);
-
- // See if we already have enough variables tracked
- var success = refinementLoopCheckPath(apiChecker, trackedVars, allVars);
- if (success) {
- // We have enough
- return new HashSet<VCExprVar>(trackedVars);
- }
-
- // If all that remains is 1 variable, then we know that we must track it
- if (trackedVars.Count + 1 == trackedVarsUpperBound.Count)
- return new HashSet<VCExprVar>(trackedVarsUpperBound);
-
- // Partition the remaining set of variables
- HashSet<VCExprVar> part1, part2;
- var temp = new HashSet<VCExprVar>(trackedVarsUpperBound);
- temp.ExceptWith(trackedVars);
- Partition<VCExprVar>(temp, out part1, out part2);
-
- // First half
- var fh = new HashSet<VCExprVar>(trackedVars); fh.UnionWith(part2);
- var s1 = refinementLoop(apiChecker, fh, trackedVarsUpperBound, allVars);
-
- var a = new HashSet<VCExprVar>(part1); a.IntersectWith(s1);
- var b = new HashSet<VCExprVar>(part1); b.ExceptWith(s1);
- var c = new HashSet<VCExprVar>(trackedVarsUpperBound); c.ExceptWith(b);
- a.UnionWith(trackedVars);
-
- // Second half
- return refinementLoop(apiChecker, a, c, allVars);
- }
-
- Dictionary<int, List<HashSet<string>>> satQueryCache;
- Dictionary<int, List<HashSet<string>>> unsatQueryCache;
-
- private bool refinementLoopCheckPath(ApiChecker apiChecker, HashSet<VCExprVar> varsToSet, HashSet<VCExprVar> allVars) {
- var assumptions = new List<VCExpr>();
- var prover = apiChecker.prover;
- var query = new HashSet<string>();
- varsToSet.Iter(v => query.Add(v.Name));
-
- if (checkCache(query, unsatQueryCache)) {
- prover.LogComment("FindLeast: Query Cache Hit");
- return true;
- }
- if (checkCache(query, satQueryCache)) {
- prover.LogComment("FindLeast: Query Cache Hit");
- return false;
- }
-
- prover.LogComment("FindLeast: Query Begin");
-
- foreach (var c in allVars) {
- if (varsToSet.Contains(c)) {
- assumptions.Add(c);
- }
- else {
- assumptions.Add(prover.VCExprGen.Not(c));
- }
- }
-
- var o = apiChecker.CheckAssumptions(assumptions);
- if (o != Outcome.Correct && o != Outcome.Errors)
- {
- throw new FindLeastOORException("OOR", o);
- }
- //Console.WriteLine("Result = " + o.ToString());
- prover.LogComment("FindLeast: Query End");
-
- if (o == Outcome.Correct) {
- insertCache(query, unsatQueryCache);
- return true;
- }
-
- insertCache(query, satQueryCache);
- return false;
- }
-
- private bool checkCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache) {
- if (!cache.ContainsKey(q.Count)) return false;
- foreach (var s in cache[q.Count]) {
- if (q.SetEquals(s)) return true;
- }
- return false;
- }
-
- private void insertCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache) {
- if (!cache.ContainsKey(q.Count)) {
- cache.Add(q.Count, new List<HashSet<string>>());
- }
- cache[q.Count].Add(q);
- }
-
- public static void Partition<T>(HashSet<T> values, out HashSet<T> part1, out HashSet<T> part2) {
- part1 = new HashSet<T>();
- part2 = new HashSet<T>();
- var size = values.Count;
- var crossed = false;
- var curr = 0;
- foreach (var s in values) {
- if (crossed) part2.Add(s);
- else part1.Add(s);
- curr++;
- if (!crossed && curr >= size / 2) crossed = true;
- }
- }
-
- public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {
- Debug.Assert(QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"));
- Debug.Assert(this.program == program);
-
- // Record current time
- var startTime = DateTime.UtcNow;
-
- // Flush any axioms that came with the program before we start SI on this implementation
- prover.AssertAxioms();
-
- // Run live variable analysis
- if (CommandLineOptions.Clo.LiveVariableAnalysis == 2) {
- Microsoft.Boogie.InterProcGenKill.ComputeLiveVars(impl, program);
- }
-
- // Get the VC of the current procedure
- StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];
- info.GenerateVC();
- VCExpr vc = info.vcexpr;
- Dictionary<int, Absy> mainLabel2absy = info.label2absy;
- var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info);
-
- // Find all procedure calls in vc and put labels on them
- FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
- calls.setCurrProcAsMain();
- vc = calls.Mutate(vc, true);
- reporter.SetCandidateHandler(calls);
- calls.id2VC.Add(0, vc);
- calls.extraRecursion = extraRecBound;
- if (CommandLineOptions.Clo.SIBoolControlVC)
- {
- calls.candiate2block2controlVar.Add(0, new Dictionary<Block, VCExpr>());
- implName2StratifiedInliningInfo[impl.Name].blockToControlVar.Iter(tup =>
- calls.candiate2block2controlVar[0].Add(tup.Key, tup.Value));
- }
-
- // We'll restore the original state of the theorem prover at the end
- // of this procedure
- prover.Push();
-
- // Put all of the necessary state into one object
- var vState = new VerificationState(vc, calls, prover, reporter);
- vState.vcSize += SizeComputingVisitor.ComputeSize(vc);
-
- Outcome ret = Outcome.ReachedBound;
-
- #region eager inlining
- for (int i = 1; i < CommandLineOptions.Clo.StratifiedInlining && calls.currCandidates.Count > 0; i++) {
- List<int> toExpand = new List<int>();
-
- foreach (int id in calls.currCandidates) {
- if (calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound) {
- toExpand.Add(id);
- }
- }
- DoExpansion(toExpand, vState);
- }
- #endregion
-
- #region Repopulate call tree, if there is one
- if (PersistCallTree && callTree != null) {
- bool expand = true;
- while (expand) {
- List<int> toExpand = new List<int>();
- foreach (int id in calls.currCandidates) {
- if (callTree.Contains(calls.getPersistentId(id))) {
- toExpand.Add(id);
- }
- }
- if (toExpand.Count == 0) expand = false;
- else {
- DoExpansion(toExpand, vState);
- }
- }
- }
- #endregion
-
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1) {
- Console.WriteLine(">> SI: Size of VC after eager inlining: {0}", vState.vcSize);
- }
-
- // Under-approx query is only needed if something was inlined since
- // the last time an under-approx query was made
- // TODO: introduce this
- // bool underApproxNeeded = true;
-
- // The recursion bound for stratified search
- int bound = CommandLineOptions.Clo.NonUniformUnfolding ? CommandLineOptions.Clo.RecursionBound : 1;
-
- int done = 0;
-
- int iters = 0;
-
- // for blocking candidates (and focusing on a counterexample)
- var block = new HashSet<int>();
-
- // Process tasks while not done. We're done when:
- // case 1: (correct) We didn't find a bug (either an over-approx query was valid
- // or we reached the recursion bound) and the task is "step"
- // case 2: (bug) We find a bug
- // case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
- while (true)
- {
- // Check timeout
- if (CommandLineOptions.Clo.ProverKillTime != -1)
- {
- if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)
- {
- ret = Outcome.TimedOut;
- break;
- }
- }
-
- if (done > 0)
- {
- break;
- }
-
- // Stratified Step
- ret = stratifiedStep(bound, vState, block);
- iters++;
-
- // Sorry, out of luck (time/memory)
- if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut)
- {
- done = 3;
- continue;
- }
-
- if (ret == Outcome.Errors && reporter.underapproximationMode)
- {
- // Found a bug
- done = 2;
- }
- else if (ret == Outcome.Correct)
- {
- if (block.Count == 0)
- {
- // Correct
- done = 1;
- }
- else
- {
- // reset blocked and continue loop
- block.Clear();
- }
- }
- else if (ret == Outcome.ReachedBound)
- {
- if (block.Count == 0)
- {
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
- Console.WriteLine(">> SI: Exhausted Bound {0}", bound);
-
- // Increment bound
- bound++;
-
- if (bound > CommandLineOptions.Clo.RecursionBound)
- {
- // Correct under bound
- done = 1;
- }
- }
- else
- {
- // reset blocked and continue loop
- block.Clear();
- }
- }
- else
- {
- // Do inlining
- Debug.Assert(ret == Outcome.Errors && !reporter.underapproximationMode);
- Contract.Assert(reporter.candidatesToExpand.Count != 0);
-
- #region expand call tree
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1)
- {
- Console.Write(">> SI Inlining: ");
- reporter.candidatesToExpand
- .Select(c => calls.getProc(c))
- .Iter(c => Console.Write("{0} ", c));
-
- Console.WriteLine();
- }
-
- // Expand and try again
- vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
- DoExpansion(reporter.candidatesToExpand, vState);
- vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
-
- #endregion
- }
- }
-
- // Pop off everything that we pushed so that there are no side effects from
- // this call to VerifyImplementation
- vState.checker.prover.Pop();
-
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1) {
- Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);
- Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);
- Console.WriteLine(">> SI: VC Size: {0}", vState.vcSize);
- }
-
- vcsize = vState.vcSize;
- numInlined = (calls.candidateParent.Keys.Count + 1) - (calls.currCandidates.Count);
-
- var rbound = "Procs that reached bound: ";
- foreach (var s in procsThatReachedRecBound) rbound += " " + s;
- if (ret == Outcome.ReachedBound) Helpers.ExtraTraceInformation(rbound);
- if (CommandLineOptions.Clo.StackDepthBound > 0 && ret == Outcome.Correct) ret = Outcome.ReachedBound;
-
- // Store current call tree
- if (PersistCallTree && (ret == Outcome.Correct || ret == Outcome.Errors || ret == Outcome.ReachedBound)) {
- callTree = new HashSet<string>();
- //var persistentNodes = new HashSet<int>(calls.candidateParent.Values);
- var persistentNodes = new HashSet<int>(calls.candidateParent.Keys);
- persistentNodes.Add(0);
- persistentNodes.ExceptWith(calls.currCandidates);
-
- foreach (var id in persistentNodes) {
- var pid = calls.getPersistentId(id);
- Debug.Assert(!callTree.Contains(pid));
- callTree.Add(pid);
- }
- }
- return ret;
- }
-
- // A step of the stratified inlining algorithm: both under-approx and over-approx queries
- private Outcome stratifiedStep(int bound, VerificationState vState, HashSet<int> block) {
- var calls = vState.calls;
- var checker = vState.checker;
- var prover = checker.prover;
- var reporter = checker.reporter as StratifiedInliningErrorReporter;
-
- reporter.underapproximationMode = true;
- prover.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");
- List<VCExpr> assumptions = new List<VCExpr>();
-
- foreach (int id in calls.currCandidates) {
- assumptions.Add(calls.getFalseExpr(id));
- }
- Outcome ret = checker.CheckAssumptions(assumptions);
- prover.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
-
- if (ret != Outcome.Correct) {
- // Either the query returned an error or it ran out of memory or time.
- // In all cases, we are done.
- return ret;
- }
-
- if (calls.currCandidates.Count == 0) {
- // If we didn't underapproximate, then we're done
- return ret;
- }
-
- prover.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;");
-
- // Over-approx query
- reporter.underapproximationMode = false;
-
- // Push "true" for all, except:
- // push "false" for all candidates that have reached
- // the recursion bounds
-
- bool allTrue = true;
- bool allFalse = true;
- List<VCExpr> softAssumptions = new List<VCExpr>();
-
- assumptions = new List<VCExpr>();
- procsThatReachedRecBound.Clear();
-
- foreach (int id in calls.currCandidates) {
-
- int idBound = calls.getRecursionBound(id);
- int sd = calls.getStackDepth(id);
- if (idBound <= bound && (CommandLineOptions.Clo.StackDepthBound == 0 || sd <= CommandLineOptions.Clo.StackDepthBound)) {
- if (idBound > 1)
- softAssumptions.Add(calls.getFalseExpr(id));
-
- if (block.Contains(id)) {
- assumptions.Add(calls.getFalseExpr(id));
- allTrue = false;
- }
- else {
- allFalse = false;
- }
- }
- else {
- procsThatReachedRecBound.Add(calls.getProc(id));
- assumptions.Add(calls.getFalseExpr(id));
- allTrue = false;
- }
- }
-
- if (allFalse) {
- // If we made all candidates false, then this is the same
- // as the underapprox query. We already know the answer.
- ret = Outcome.Correct;
- }
- else {
- ret = CommandLineOptions.Clo.NonUniformUnfolding
- ? checker.CheckAssumptions(assumptions, softAssumptions)
- : checker.CheckAssumptions(assumptions);
- }
-
- if (ret != Outcome.Correct && ret != Outcome.Errors) {
- // The query ran out of memory or time, that's it,
- // we cannot do better. Give up!
- return ret;
- }
-
- if (ret == Outcome.Correct) {
- // If nothing was made false, then the program is correct
- if (allTrue) {
- return ret;
- }
-
- // Nothing more can be done with current recursion bound.
- return Outcome.ReachedBound;
- }
-
- Contract.Assert(ret == Outcome.Errors);
-
- prover.LogComment(";;;;;;;;;;;; Overapprox mode end ;;;;;;;;;;");
-
- return ret;
- }
-
- // A counter for adding new variables
- static int newVarCnt = 0;
-
- // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
- private void DoExpansion(List<int>/*!*/ candidates, VerificationState vState) {
- Contract.Requires(candidates != null);
- Contract.Requires(vState.calls != null);
- Contract.Requires(vState.checker.prover != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- vState.expansionCount += candidates.Count;
-
- var prover = vState.checker.prover;
- var calls = vState.calls;
-
- VCExpr exprToPush = VCExpressionGenerator.True;
- Contract.Assert(exprToPush != null);
- foreach (int id in candidates) {
- VCExprNAry expr = calls.id2Candidate[id];
- Contract.Assert(expr != null);
- string procName = cce.NonNull(expr.Op as VCExprBoogieFunctionOp).Func.Name;
- if (!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;
-
- StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];
- info.GenerateVC();
- //Console.WriteLine("Inlining {0}", procName);
- VCExpr expansion = cce.NonNull(info.vcexpr);
-
- // Instantiate the "forall" variables
- Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();
- Contract.Assert(info.interfaceExprVars.Count == expr.Length);
- for (int i = 0; i < info.interfaceExprVars.Count; i++) {
- substForallDict.Add(info.interfaceExprVars[i], expr[i]);
- }
- VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
-
- SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(prover.VCExprGen);
- Contract.Assert(subst != null);
- expansion = subst.Mutate(expansion, substForall);
-
- // Instantiate and declare the "exists" variables
- Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();
- foreach (VCExprVar v in info.privateExprVars) {
- Contract.Assert(v != null);
- string newName = v.Name + "_si_" + newVarCnt.ToString();
- newVarCnt++;
- prover.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
- substExistsDict.Add(v, prover.VCExprGen.Variable(newName, v.Type));
- }
- if (CommandLineOptions.Clo.SIBoolControlVC)
- {
- // record the mapping for control booleans (for tracing the path later)
- calls.candiate2block2controlVar[id] = new Dictionary<Block, VCExpr>();
- foreach (var tup in info.blockToControlVar)
- {
- calls.candiate2block2controlVar[id].Add(tup.Key,
- substExistsDict[tup.Value]);
- }
- }
- if (CommandLineOptions.Clo.ModelViewFile != null) {
- SaveSubstitution(vState, id, substForallDict, substExistsDict);
- }
- VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
-
- subst = new SubstitutingVCExprVisitor(prover.VCExprGen);
- expansion = subst.Mutate(expansion, substExists);
-
- if (!calls.currCandidates.Contains(id)) {
- Console.WriteLine("Don't know what we just expanded");
- }
-
- calls.currCandidates.Remove(id);
-
- // Record the new set of candidates and rename absy labels
- calls.currInlineCount = id;
- calls.setCurrProc(procName);
- expansion = calls.Mutate(expansion, true);
-
- //expansion = checker.VCExprGen.Eq(calls.id2ControlVar[id], expansion);
- expansion = prover.VCExprGen.Implies(calls.id2ControlVar[id], expansion);
- calls.id2VC.Add(id, expansion);
-
- exprToPush = prover.VCExprGen.And(exprToPush, expansion);
- }
- vState.checker.prover.Assert(exprToPush, true);
- vState.vcSize += SizeComputingVisitor.ComputeSize(exprToPush);
- }
-
- private void SaveSubstitution(VerificationState vState, int id,
- Dictionary<VCExprVar, VCExpr> substForallDict, Dictionary<VCExprVar, VCExpr> substExistsDict) {
- var prover = vState.checker.prover;
- var calls = vState.calls;
- Boogie2VCExprTranslator translator = prover.Context.BoogieExprTranslator;
- VCExprVar mvStateConstant = translator.LookupVariable(ModelViewInfo.MVState_ConstantDef);
- substExistsDict.Add(mvStateConstant, prover.VCExprGen.Integer(BigNum.FromInt(id)));
- Dictionary<VCExprVar, VCExpr> mapping = new Dictionary<VCExprVar, VCExpr>();
- foreach (var key in substForallDict.Keys)
- mapping[key] = substForallDict[key];
- foreach (var key in substExistsDict.Keys)
- mapping[key] = substExistsDict[key];
- calls.id2Vars[id] = mapping;
- }
-
- // Uniquely identifies a procedure call (the call expr, instance)
- public class BoogieCallExpr : IEquatable<BoogieCallExpr> {
- public NAryExpr expr;
- public int inlineCnt;
-
- public BoogieCallExpr(NAryExpr expr, int inlineCnt) {
- this.expr = expr;
- this.inlineCnt = inlineCnt;
- }
-
- public override int GetHashCode() {
- return expr.GetHashCode() + 131 * inlineCnt.GetHashCode();
- }
-
- public override bool Equals(object obj) {
- BoogieCallExpr that = obj as BoogieCallExpr;
- return (expr == that.expr && inlineCnt == that.inlineCnt);
- }
-
- public bool Equals(BoogieCallExpr that) {
- return (expr == that.expr && inlineCnt == that.inlineCnt);
- }
- }
-
- // This class is used to traverse VCs and do the following:
- // -- collect the set of FunctionCall nodes and label them with a unique string
- // -- Rename all other labels (so that calling this on the same VC results in
- // VCs with different labels each time)
- public class FCallHandler : MutatingVCExprVisitor<bool> {
- Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;
- public readonly Dictionary<int, Absy>/*!*/ mainLabel2absy;
- public Dictionary<BoogieCallExpr/*!*/, int>/*!*/ boogieExpr2Id;
- public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;
- public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;
- public Dictionary<int, VCExprVar/*!*/>/*!*/ id2ControlVar;
- public Dictionary<int, VCExpr> id2VC;
- public Dictionary<string/*!*/, int>/*!*/ label2Id;
- // candidate to block to Bool Control variable
- public Dictionary<int, Dictionary<Block, VCExpr>> candiate2block2controlVar;
- // Stores the candidate from which this one originated
- public Dictionary<int, int> candidateParent;
- // Mapping from candidate Id to the "si_unique_call" id that led to
- // this candidate. This is useful for getting persistent names for
- // candidates
- public Dictionary<int, int> candidate2callId;
- // A cache for candidate id to its persistent name
- public Dictionary<int, string> persistentNameCache;
- // Inverse of the above map
- public Dictionary<string, int> persistentNameInv;
- // Used to record candidates recently added
- public HashSet<int> recentlyAddedCandidates;
- // Name of main procedure
- private string mainProcName;
- // A map from candidate id to the VCExpr that represents its
- // first argument (used for obtaining concrete values in error trace)
- public Dictionary<int, VCExpr> argExprMap;
-
- // map from candidate to summary candidates
- public Dictionary<int, List<Tuple<VCExprVar, VCExpr>>> summaryCandidates;
- private Dictionary<string, List<Tuple<VCExprVar, VCExpr>>> summaryTemp;
- // set of all boolean guards of summaries
- public HashSet<VCExprVar> allSummaryConst;
-
- public HashSet<int> forcedCandidates;
-
- // User info -- to decrease/increase calculation of recursion bound
- public Dictionary<int, int> recursionIncrement;
- public Dictionary<string, int> extraRecursion;
-
- public HashSet<int> currCandidates;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- Contract.Invariant(mainLabel2absy != null);
- Contract.Invariant(boogieExpr2Id != null);
- Contract.Invariant(cce.NonNullDictionaryAndValues(id2Candidate));
- Contract.Invariant(cce.NonNullDictionaryAndValues(id2ControlVar));
- Contract.Invariant(label2Id != null);
- }
-
- // Name of the procedure whose VC we're mutating
- string currProc;
-
- // The 0^th candidate is main
- static int candidateCount = 1;
- public int currInlineCount;
-
- public Dictionary<int, Dictionary<VCExprVar, VCExpr>> id2Vars;
-
- public FCallHandler(VCExpressionGenerator/*!*/ gen,
- Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,
- string mainProcName, Dictionary<int, Absy>/*!*/ mainLabel2absy)
- : base(gen) {
- Contract.Requires(gen != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- Contract.Requires(mainLabel2absy != null);
- this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
- this.mainProcName = mainProcName;
- this.mainLabel2absy = mainLabel2absy;
- id2Candidate = new Dictionary<int, VCExprNAry>();
- id2ControlVar = new Dictionary<int, VCExprVar>();
- boogieExpr2Id = new Dictionary<BoogieCallExpr, int>();
- label2Id = new Dictionary<string, int>();
- currCandidates = new HashSet<int>();
- currInlineCount = 0;
- currProc = null;
- labelRenamer = new Dictionary<string, int>();
- labelRenamerInv = new Dictionary<string, string>();
- candidateParent = new Dictionary<int, int>();
- //callGraphMapping = new Dictionary<int, int>();
- recursionIncrement = new Dictionary<int, int>();
- candidate2callId = new Dictionary<int, int>();
- persistentNameCache = new Dictionary<int, string>();
- persistentNameInv = new Dictionary<string, int>();
- persistentNameCache[0] = "0";
- persistentNameInv["0"] = 0;
- recentlyAddedCandidates = new HashSet<int>();
- argExprMap = new Dictionary<int, VCExpr>();
- recordExpr2Var = new Dictionary<BoogieCallExpr, VCExpr>();
- candiate2block2controlVar = new Dictionary<int, Dictionary<Block, VCExpr>>();
-
- forcedCandidates = new HashSet<int>();
- extraRecursion = new Dictionary<string, int>();
-
- id2Vars = new Dictionary<int, Dictionary<VCExprVar, VCExpr>>();
- summaryCandidates = new Dictionary<int, List<Tuple<VCExprVar, VCExpr>>>();
- summaryTemp = new Dictionary<string, List<Tuple<VCExprVar, VCExpr>>>();
- allSummaryConst = new HashSet<VCExprVar>();
- id2VC = new Dictionary<int, VCExpr>();
- }
-
- public void Clear() {
- currCandidates = new HashSet<int>();
- }
-
- // Return the set of all candidates
- public HashSet<int> getAllCandidates() {
- var ret = new HashSet<int>(candidateParent.Keys);
- ret.Add(0);
- return ret;
- }
-
- // Given a candidate "id", let proc(id) be the
- // procedure corresponding to id. This procedure returns
- // the number of times proc(id) appears as an ancestor
- // of id. This is the same as the number of times we've
- // recursed on proc(id)
- public int getRecursionBound(int id) {
- int ret = 1;
- var str = getProc(id);
-
- while (candidateParent.ContainsKey(id)) {
- if (recursionIncrement.ContainsKey(id)) ret += recursionIncrement[id];
- id = candidateParent[id];
- if (getProc(id) == str && !forcedCandidates.Contains(id)) ret++;
- }
-
- // Usual
- if (!extraRecursion.ContainsKey(str))
- return ret;
-
- // Usual
- if (ret <= CommandLineOptions.Clo.RecursionBound - 1)
- return ret;
-
- // Special
- if (ret >= CommandLineOptions.Clo.RecursionBound &&
- ret <= CommandLineOptions.Clo.RecursionBound + extraRecursion[str] - 1)
- return CommandLineOptions.Clo.RecursionBound - 1;
-
- // Special
- return ret - extraRecursion[str];
- }
-
- // This procedure returns the stack depth of the candidate
- // (distance from main)
- public int getStackDepth(int id)
- {
- int ret = 1;
-
- while (candidateParent.ContainsKey(id))
- {
- ret++;
- id = candidateParent[id];
- }
-
- return ret;
- }
-
- // Set user-define increment/decrement to recursionBound
- public void setRecursionIncrement(int id, int incr) {
- if (recursionIncrement.ContainsKey(id))
- recursionIncrement[id] = incr;
- else
- recursionIncrement.Add(id, incr);
- }
-
- // Returns the name of the procedure corresponding to candidate id
- public string getProc(int id) {
- if (id == 0) return mainProcName;
-
- return (id2Candidate[id].Op as VCExprBoogieFunctionOp).Func.Name;
- }
-
- // Get a unique id for this candidate (dependent only on the Call
- // graph of the program). The persistent id is:
- // 0: for main
- // a_b_c: where a is the persistent id of parent, and b is the procedure name
- // and c is the unique call id (if any)
- public string getPersistentId(int top_id) {
- if (top_id == 0) return "0";
- Debug.Assert(candidateParent.ContainsKey(top_id));
- if (persistentNameCache.ContainsKey(top_id))
- return persistentNameCache[top_id];
-
- var parent_id = getPersistentId(candidateParent[top_id]);
- var call_id = candidate2callId.ContainsKey(top_id) ? candidate2callId[top_id] : -1;
- var ret = string.Format("{0}_131_{1}_131_{2}", parent_id, getProc(top_id), call_id);
- persistentNameCache[top_id] = ret;
- persistentNameInv[ret] = top_id;
- return ret;
- }
-
- public int getCandidateFromGraphNode(string n) {
- if (!persistentNameInv.ContainsKey(n)) {
- return -1;
- }
- return persistentNameInv[n];
- }
-
- private int GetNewId(VCExprNAry vc) {
- Contract.Requires(vc != null);
- int id = candidateCount;
-
- id2Candidate[id] = vc;
- id2ControlVar[id] = Gen.Variable("si_control_var_bool_" + id.ToString(), Microsoft.Boogie.Type.Bool);
-
- candidateCount++;
- currCandidates.Add(id);
- recentlyAddedCandidates.Add(id);
-
- return id;
- }
-
- private string GetLabel(int id) {
- Contract.Ensures(Contract.Result<string>() != null);
-
- string ret = "si_fcall_" + id.ToString();
- if (!label2Id.ContainsKey(ret))
- label2Id[ret] = id;
-
- return ret;
- }
-
- public int GetId(string label) {
- Contract.Requires(label != null);
- if (!label2Id.ContainsKey(label))
- return -1;
- return label2Id[label];
- }
-
- Dictionary<string, int> labelRenamer;
- Dictionary<string, string> labelRenamerInv;
-
- public string RenameAbsyLabel(string label) {
- Contract.Requires(label != null);
- Contract.Requires(label.Length >= 1);
- Contract.Ensures(Contract.Result<string>() != null);
-
- // Remove the sign from the label
- string nosign = label.Substring(1);
- var ret = "si_inline_" + currInlineCount.ToString() + "_" + nosign;
-
- if (!labelRenamer.ContainsKey(ret)) {
- var c = labelRenamer.Count + 11; // two digit labels only
- labelRenamer.Add(ret, c);
- labelRenamerInv.Add(c.ToString(), ret);
- }
- return labelRenamer[ret].ToString();
- }
-
- public string ParseRenamedAbsyLabel(string label, int cnt) {
- Contract.Requires(label != null);
- if (!labelRenamerInv.ContainsKey(label)) {
- return null;
- }
- var str = labelRenamerInv[label];
- var prefix = "si_inline_" + cnt.ToString() + "_";
- if (!str.StartsWith(prefix)) return null;
- return str.Substring(prefix.Length);
- }
-
- public void setCurrProc(string name) {
- Contract.Requires(name != null);
- currProc = name;
- Contract.Assert(implName2StratifiedInliningInfo.ContainsKey(name));
- }
-
- public void setCurrProcAsMain() {
- currProc = "";
- }
-
- // Return the formula (candidate IFF false)
- public VCExpr getFalseExpr(int candidateId) {
- //return Gen.Eq(VCExpressionGenerator.False, id2ControlVar[candidateId]);
- return Gen.Not(id2ControlVar[candidateId]);
- }
-
- // Return the formula (candidate IFF true)
- public VCExpr getTrueExpr(int candidateId) {
- return Gen.Eq(VCExpressionGenerator.True, id2ControlVar[candidateId]);
- }
-
- public Dictionary<int, Absy> getLabel2absy() {
- Contract.Ensures(Contract.Result<Dictionary<int, Absy>>() != null);
-
- Contract.Assert(currProc != null);
- if (currProc == "") {
- return mainLabel2absy;
- }
- return cce.NonNull(implName2StratifiedInliningInfo[currProc].label2absy);
- }
-
- // Finds labels and changes them:
- // si_fcall_id: if "id" corresponds to a tracked procedure call, then
- // si_control_var_candidateId
- // si_fcall_id: if "id" does not corresponds to a tracked procedure call, then
- // delete
- // num: si_inline_num
- //
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- // has any of the subexpressions changed?
- bool changed,
- bool arg) {
- //Contract.Requires(originalNode != null);
- //Contract.Requires(cce.NonNullElements(newSubExprs));
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr ret;
- if (changed)
- ret = Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- ret = originalNode;
-
- VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
- if (lop == null) return ret;
- if (!(ret is VCExprNAry)) return ret;
-
- VCExprNAry retnary = (VCExprNAry)ret;
- Contract.Assert(retnary != null);
- string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)
- if (lop.label.Substring(1).StartsWith(prefix)) {
- int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
- Dictionary<int, Absy> label2absy = getLabel2absy();
- Absy cmd = label2absy[id] as Absy;
- //label2absy.Remove(id);
-
- Contract.Assert(cmd != null);
- AssumeCmd acmd = cmd as AssumeCmd;
- Contract.Assert(acmd != null);
- NAryExpr naryExpr = acmd.Expr as NAryExpr;
- Contract.Assert(naryExpr != null);
-
- string calleeName = naryExpr.Fun.FunctionName;
-
- VCExprNAry callExpr = retnary[0] as VCExprNAry;
-
- if (implName2StratifiedInliningInfo.ContainsKey(calleeName)) {
- Contract.Assert(callExpr != null);
- int candidateId = GetNewId(callExpr);
- boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId;
- candidateParent[candidateId] = currInlineCount;
- candiate2block2controlVar[candidateId] = new Dictionary<Block, VCExpr>();
-
- string label = GetLabel(candidateId);
- var unique_call_id = QKeyValue.FindIntAttribute(acmd.Attributes, "si_unique_call", -1);
- if (unique_call_id != -1)
- candidate2callId[candidateId] = unique_call_id;
-
- //return Gen.LabelPos(label, callExpr);
- return Gen.LabelPos(label, id2ControlVar[candidateId]);
- }
- else if (calleeName.StartsWith(recordProcName)) {
- Contract.Assert(callExpr != null);
- Debug.Assert(callExpr.Length == 1);
- Debug.Assert(callExpr[0] != null);
- recordExpr2Var[new BoogieCallExpr(naryExpr, currInlineCount)] = callExpr[0];
- return callExpr;
- }
- else {
- // callExpr can be null; this happens when the FunctionCall was on a
- // pure function (not procedure) and the function got inlined
- return retnary[0];
- }
- }
-
- // Else, rename label
- string newLabel = RenameAbsyLabel(lop.label);
- if (lop.pos) {
- return Gen.LabelPos(newLabel, retnary[0]);
- }
- else {
- return Gen.LabelNeg(newLabel, retnary[0]);
- }
-
- }
-
- // Upgrades summaryTemp to summaryCandidates by matching ensure clauses with
- // the appropriate candidate they came from
- public void matchSummaries() {
- var id2Set = new Dictionary<string, List<Tuple<int, HashSet<VCExprVar>>>>();
- foreach (var id in recentlyAddedCandidates) {
- var collect = new CollectVCVars();
- var proc = getProc(id);
- if (!id2Set.ContainsKey(proc)) id2Set.Add(proc, new List<Tuple<int, HashSet<VCExprVar>>>());
- id2Set[proc].Add(Tuple.Create(id, collect.Collect(id2Candidate[id], true)));
- }
-
- foreach (var kvp in summaryTemp) {
- Contract.Assert(id2Set.ContainsKey(kvp.Key));
- var ls = id2Set[kvp.Key];
- foreach (var tup in kvp.Value) {
- var collect = new CollectVCVars();
- var s1 = collect.Collect(tup.Item2, true);
- var found = false;
- foreach (var t in ls) {
- var s2 = t.Item2;
- if (s1.IsSubsetOf(s2)) {
- if (!summaryCandidates.ContainsKey(t.Item1))
- summaryCandidates.Add(t.Item1, new List<Tuple<VCExprVar, VCExpr>>());
- summaryCandidates[t.Item1].Add(tup);
- allSummaryConst.Add(tup.Item1);
- found = true;
- break;
- }
- }
- Contract.Assert(found);
- }
- }
- summaryTemp.Clear();
- }
-
- public IEnumerable<int> getInlinedCandidates() {
- return candidateParent.Keys.Except(currCandidates).Union(new int[] { 0 });
- }
-
- } // end FCallHandler
-
- // Collects the set of all VCExprVar in a given VCExpr
- class CollectVCVars : CollectingVCExprVisitor<HashSet<VCExprVar>, bool> {
- public override HashSet<VCExprVar> Visit(VCExprVar node, bool arg) {
- var ret = new HashSet<VCExprVar>();
- ret.Add(node);
- return ret;
- }
-
- protected override HashSet<VCExprVar> CombineResults(List<HashSet<VCExprVar>> results, bool arg) {
- var ret = new HashSet<VCExprVar>();
- results.Iter(s => ret.UnionWith(s));
- return ret;
- }
- }
-
- public class FCallInliner : MutatingVCExprVisitor<bool> {
- public Dictionary<int, VCExpr/*!*/>/*!*/ subst;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullDictionaryAndValues(subst));
- }
-
-
- public FCallInliner(VCExpressionGenerator gen)
- : base(gen) {
- Contract.Requires(gen != null);
- subst = new Dictionary<int, VCExpr>();
- }
-
- public void Clear() {
- subst = new Dictionary<int, VCExpr>();
- }
-
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- // has any of the subexpressions changed?
- bool changed,
- bool arg) {
- //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr ret;
- if (changed)
- ret = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments);
- else
- ret = originalNode;
-
- VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
- if (lop == null) return ret;
- if (!(ret is VCExprNAry)) return ret;
-
- string prefix = "si_fcall_"; // from FCallHandler::GetLabel
- if (lop.label.Substring(1).StartsWith(prefix)) {
- int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
- if (subst.ContainsKey(id)) {
- return subst[id];
- }
- }
- return ret;
- }
-
- } // end FCallInliner
-
-
-
- public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler {
- Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
- ProverInterface theoremProver;
- VerifierCallback callback;
- FCallHandler calls;
- StratifiedInliningInfo mainInfo;
- StratifiedVC mainVC;
-
- public bool underapproximationMode;
- public List<int> candidatesToExpand;
- public List<StratifiedCallSite> callSitesToExpand;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(candidatesToExpand != null);
- Contract.Invariant(mainInfo != null);
- Contract.Invariant(callback != null);
- Contract.Invariant(theoremProver != null);
- Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- }
-
-
- public StratifiedInliningErrorReporter(Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo,
- ProverInterface theoremProver, VerifierCallback callback,
- StratifiedInliningInfo mainInfo) {
- Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- Contract.Requires(theoremProver != null);
- Contract.Requires(callback != null);
- Contract.Requires(mainInfo != null);
- this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
- this.theoremProver = theoremProver;
- this.callback = callback;
- this.mainInfo = mainInfo;
- this.underapproximationMode = false;
- this.calls = null;
- this.candidatesToExpand = new List<int>();
- }
-
- public StratifiedInliningErrorReporter(Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo,
- ProverInterface theoremProver, VerifierCallback callback,
- StratifiedVC mainVC) {
- Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- Contract.Requires(theoremProver != null);
- Contract.Requires(callback != null);
- Contract.Requires(mainVC != null);
- this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
- this.theoremProver = theoremProver;
- this.callback = callback;
- this.mainVC = mainVC;
- this.underapproximationMode = false;
- this.candidatesToExpand = new List<int>();
- }
-
- public void SetCandidateHandler(FCallHandler calls) {
- Contract.Requires(calls != null);
- this.calls = calls;
- }
-
- List<Tuple<int, int>> orderedStateIds;
-
- private Model.Element GetModelValue(Model m, Variable v, int candidateId) {
- // first, get the unique name
- string uniqueName;
-
- VCExprVar vvar = theoremProver.Context.BoogieExprTranslator.TryLookupVariable(v);
- if (vvar == null) {
- uniqueName = v.Name;
- }
- else {
- if (candidateId != 0) {
- Dictionary<VCExprVar, VCExpr> mapping = calls.id2Vars[candidateId];
- if (mapping.ContainsKey(vvar)) {
- VCExpr e = mapping[vvar];
- if (e is VCExprLiteral) {
- VCExprLiteral lit = (VCExprLiteral)e;
- return m.MkElement(lit.ToString());
- }
- vvar = (VCExprVar)mapping[vvar];
- }
- }
- uniqueName = theoremProver.Context.Lookup(vvar);
- }
-
- var f = m.TryGetFunc(uniqueName);
- if (f == null)
- return m.MkFunc("@undefined", 0).GetConstant();
- return f.GetConstant();
- }
-
- public readonly static int CALL = -1;
- public readonly static int RETURN = -2;
-
- public void PrintModel(Model model) {
- var filename = CommandLineOptions.Clo.ModelViewFile;
- if (model == null || filename == null) return;
-
- if (filename == "-") {
- model.Write(Console.Out);
- Console.Out.Flush();
- }
- else {
- using (var wr = new StreamWriter(filename, !Counterexample.firstModelFile)) {
- Counterexample.firstModelFile = false;
- model.Write(wr);
- }
- }
- }
-
- private void GetModelWithStates(Model m) {
- if (m == null) return;
- var mvInfo = mainInfo.mvInfo;
- var mvstates = m.TryGetFunc("$mv_state");
- if (mvstates == null)
- return;
-
- Contract.Assert(mvstates.Arity == 2);
-
- foreach (Variable v in mvInfo.AllVariables) {
- m.InitialState.AddBinding(v.Name, GetModelValue(m, v, 0));
- }
-
- int lastCandidate = 0;
- int lastCapturePoint = CALL;
- for (int i = 0; i < this.orderedStateIds.Count; ++i) {
- var s = orderedStateIds[i];
- int candidate = s.Item1;
- int capturePoint = s.Item2;
- string implName = calls.getProc(candidate);
- ModelViewInfo info = candidate == 0 ? mvInfo : implName2StratifiedInliningInfo[implName].mvInfo;
-
- if (capturePoint == CALL || capturePoint == RETURN) {
- lastCandidate = candidate;
- lastCapturePoint = capturePoint;
- continue;
- }
-
- Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);
- VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];
- var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)
- ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary<Variable, Expr>();
- var cs = m.MkState(map.Description);
-
- foreach (Variable v in info.AllVariables) {
- var e = (Expr)map.IncarnationMap[v];
-
- if (e == null) {
- if (lastCapturePoint == CALL || lastCapturePoint == RETURN) {
- cs.AddBinding(v.Name, GetModelValue(m, v, candidate));
- }
- continue;
- }
-
- if (lastCapturePoint != CALL && lastCapturePoint != RETURN && prevInc[v] == e) continue; // skip unchanged variables
-
- Model.Element elt;
- if (e is IdentifierExpr) {
- IdentifierExpr ide = (IdentifierExpr)e;
- elt = GetModelValue(m, ide.Decl, candidate);
- }
- else if (e is LiteralExpr) {
- LiteralExpr lit = (LiteralExpr)e;
- elt = m.MkElement(lit.Val.ToString());
- }
- else {
- Contract.Assume(false);
- elt = m.MkFunc(e.ToString(), 0).GetConstant();
- }
- cs.AddBinding(v.Name, elt);
- }
-
- lastCandidate = candidate;
- lastCapturePoint = capturePoint;
- }
-
- return;
- }
-
- public override void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null)
- {
- //Contract.Requires(message != null);
- }
-
- public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) {
- if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
- model.Write(ErrorReporter.ModelWriter);
- ErrorReporter.ModelWriter.Flush();
- }
-
- // Timeout?
- if (proverOutcome != ProverInterface.Outcome.Invalid)
- return;
-
- candidatesToExpand = new List<int>();
- orderedStateIds = new List<Tuple<int, int>>();
- var cex = GenerateTrace(labels, model, 0, mainInfo.impl, mainInfo.mvInfo);
-
- if (underapproximationMode && cex != null) {
- //Debug.Assert(candidatesToExpand.All(calls.isSkipped));
- GetModelWithStates(model);
- callback.OnCounterexample(cex, null);
- this.PrintModel(model);
- }
- }
-
- private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,
- int candidateId, Implementation procImpl, ModelViewInfo mvInfo) {
- Contract.Requires(cce.NonNullElements(labels));
- Contract.Requires(procImpl != null);
-
- Hashtable traceNodes = new Hashtable();
-
- if (!CommandLineOptions.Clo.SIBoolControlVC)
- {
- foreach (string s in labels)
- {
- Contract.Assert(s != null);
- var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId);
-
- if (absylabel == null) continue;
-
- Absy absy;
-
- if (candidateId == 0)
- {
- absy = Label2Absy(absylabel);
- }
- else
- {
- absy = Label2Absy(procImpl.Name, absylabel);
- }
-
- if (traceNodes.ContainsKey(absy))
- System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");
- else
- traceNodes.Add(absy, null);
- }
- }
- else
- {
- Debug.Assert(CommandLineOptions.Clo.UseProverEvaluate, "Must use prover evaluate option with boolControlVC");
- var block = procImpl.Blocks[0];
- traceNodes.Add(block, null);
- while (true)
- {
- var gc = block.TransferCmd as GotoCmd;
- if (gc == null) break;
- Block next = null;
- foreach (var succ in gc.labelTargets)
- {
- var succtaken = (bool) theoremProver.Evaluate(calls.candiate2block2controlVar[candidateId][succ]);
- if (succtaken)
- {
- next = succ;
- traceNodes.Add(succ, null);
- break;
- }
- }
- Debug.Assert(next != null, "Must find a successor");
- Debug.Assert(traceNodes.ContainsKey(next), "CFG cannot be cyclic");
- block = next;
- }
- }
-
- List<Block> trace = new List<Block>();
- Block entryBlock = cce.NonNull(procImpl.Blocks[0]);
- Contract.Assert(entryBlock != null);
- Contract.Assert(traceNodes.Contains(entryBlock));
- trace.Add(entryBlock);
-
- var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
- Counterexample newCounterexample = GenerateTraceRec(labels, errModel, mvInfo, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples);
-
- return newCounterexample;
- }
-
- private Counterexample GenerateTraceRec(
- IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,
- int candidateId,
- Block/*!*/ b, Hashtable/*!*/ traceNodes, List<Block>/*!*/ trace,
- Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {
- Contract.Requires(cce.NonNullElements(labels));
- Contract.Requires(b != null);
- Contract.Requires(traceNodes != null);
- Contract.Requires(trace != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
- // After translation, all potential errors come from asserts.
- while (true) {
- List<Cmd> cmds = b.Cmds;
- TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
- for (int i = 0; i < cmds.Count; i++) {
- Cmd cmd = cce.NonNull(cmds[i]);
-
- // Skip if 'cmd' not contained in the trace or not an assert
- if ((cmd is AssertCmd && traceNodes.Contains(cmd)) ||
- (cmd is AssumeCmd && QKeyValue.FindBoolAttribute((cmd as AssumeCmd).Attributes, "exitAssert")))
- {
- var acmd = cmd as AssertCmd;
- if (acmd == null) { acmd = new AssertCmd(Token.NoToken, Expr.True); }
- Counterexample newCounterexample = AssertCmdToCounterexample(acmd, transferCmd, trace, errModel, mvInfo, theoremProver.Context);
- newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
- return newCounterexample;
- }
-
- // Counterexample generation for inlined procedures
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- if (assumeCmd == null)
- continue;
- NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
- if (naryExpr == null)
- continue;
- string calleeName = naryExpr.Fun.FunctionName;
- Contract.Assert(calleeName != null);
-
- BinaryOperator binOp = naryExpr.Fun as BinaryOperator;
- if (binOp != null && binOp.Op == BinaryOperator.Opcode.And) {
- Expr expr = naryExpr.Args[0];
- NAryExpr mvStateExpr = expr as NAryExpr;
- if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == ModelViewInfo.MVState_FunctionDef.Name) {
- LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr;
- orderedStateIds.Add(new Tuple<int, int>(candidateId, x.asBigNum.ToInt));
- }
- }
-
- if (calleeName.StartsWith(recordProcName) && (errModel != null || CommandLineOptions.Clo.UseProverEvaluate)) {
- var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
-
- // Record concrete value of the argument to this procedure
- var args = new List<object>();
- if (errModel == null && CommandLineOptions.Clo.UseProverEvaluate)
- {
- object exprv;
- try
- {
- exprv = theoremProver.Evaluate(expr);
- }
- catch (Exception)
- {
- exprv = null;
- }
- args.Add(exprv);
- }
- else
- {
- if (expr is VCExprIntLit)
- {
- args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));
- }
- else if (expr == VCExpressionGenerator.True)
- {
- args.Add(errModel.MkElement("true"));
- }
- else if (expr == VCExpressionGenerator.False)
- {
- args.Add(errModel.MkElement("false"));
- }
- else if (expr is VCExprVar)
- {
- var idExpr = expr as VCExprVar;
- string name = theoremProver.Context.Lookup(idExpr);
- Contract.Assert(name != null);
- Model.Func f = errModel.TryGetFunc(name);
- if (f != null)
- {
- args.Add(f.GetConstant());
- }
- }
- else
- {
- Contract.Assert(false);
- }
- }
- calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =
- new CalleeCounterexampleInfo(null, args);
- continue;
- }
-
- if (!implName2StratifiedInliningInfo.ContainsKey(calleeName))
- continue;
-
- Contract.Assert(calls != null);
-
- int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)];
-
- if (calls.currCandidates.Contains(calleeId)) {
- candidatesToExpand.Add(calleeId);
- }
- else {
- orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));
- var calleeInfo = implName2StratifiedInliningInfo[calleeName];
- calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =
- new CalleeCounterexampleInfo(GenerateTrace(labels, errModel, calleeId, calleeInfo.impl, calleeInfo.mvInfo), new List<object>());
- orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));
- }
- }
-
- GotoCmd gotoCmd = transferCmd as GotoCmd;
- if (gotoCmd != null) {
- b = null;
- foreach (Block bb in cce.NonNull(gotoCmd.labelTargets)) {
- Contract.Assert(bb != null);
- if (traceNodes.Contains(bb)) {
- trace.Add(bb);
- b = bb;
- break;
- }
- }
- if (b != null) continue;
- }
- return null;
- }
- }
-
- public override Absy Label2Absy(string label) {
- //Contract.Requires(label != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
-
- int id = int.Parse(label);
- Contract.Assert(calls != null);
- return cce.NonNull((Absy)calls.mainLabel2absy[id]);
- }
-
- public Absy Label2Absy(string procName, string label) {
- Contract.Requires(label != null);
- Contract.Requires(procName != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
-
- int id = int.Parse(label);
- Dictionary<int, Absy> l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;
- return cce.NonNull((Absy)l2a[id]);
- }
-
- public override void OnProverWarning(string msg) {
- //Contract.Requires(msg != null);
- callback.OnWarning(msg);
- }
- }
-
- } // class StratifiedVCGen
-
- public class EmptyErrorHandler : ProverInterface.ErrorHandler
- {
- public override void OnModel(IList<string> labels, Model model, ProverInterface.Outcome proverOutcome)
- { }
- }
-
- public class InvalidProgramForSecureVc : Exception
- {
- public InvalidProgramForSecureVc(string msg) :
- base(msg) { }
- }
-
- public class SecureVCGen : VCGen
- {
- // Z3
- ProverInterface prover;
- // Handler
- ErrorReporter handler;
- // dump file
- public static TokenTextWriter outfile = null;
-
-
- public SecureVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
- : base(program, logFilePath, appendLogFile, checkers)
- {
- prover = null;
- handler = null;
- if (CommandLineOptions.Clo.SecureVcGen != "" && outfile == null)
- {
- outfile = new TokenTextWriter(new StreamWriter(CommandLineOptions.Clo.SecureVcGen));
- CommandLineOptions.Clo.PrintInstrumented = true;
- var implsToVerify = new HashSet<string>(
- program.TopLevelDeclarations.OfType<Implementation>()
- .Where(impl => !impl.SkipVerification)
- .Select(impl => impl.Name));
-
- foreach (var decl in program.TopLevelDeclarations)
- {
- if (decl is NamedDeclaration && implsToVerify.Contains((decl as NamedDeclaration).Name))
- continue;
- decl.Emit(outfile, 0);
- }
- }
- }
-
- private Block GetExitBlock(Implementation impl)
- {
- var exitblocks = impl.Blocks.Where(blk => blk.TransferCmd is ReturnCmd);
- if (exitblocks.Count() == 1)
- return exitblocks.First();
- // create a new exit block
- var eb = new Block(Token.NoToken, "SVCeb", new List<Cmd>(), new ReturnCmd(Token.NoToken));
- foreach (var b in exitblocks)
- {
- b.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { eb });
- }
- impl.Blocks.Add(eb);
- return eb;
- }
-
- //static int LocalVarCounter = 0;
- private LocalVariable GetNewLocal(Variable v, string suffix)
- {
- return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken,
- string.Format("svc_{0}_{1}", v.Name, suffix), v.TypedIdent.Type));
- }
-
- private void GenVc(Implementation impl, VerifierCallback collector)
- {
- if (impl.Proc.Requires.Any())
- throw new InvalidProgramForSecureVc("SecureVc: Requires not supported");
- if(impl.LocVars.Any(v => isVisible(v)))
- throw new InvalidProgramForSecureVc("SecureVc: Visible Local variables not allowed");
-
- // Desugar procedure calls
- DesugarCalls(impl);
-
- // Gather spec, remove existing ensures
- var secureAsserts = new List<AssertCmd>();
- var logicalAsserts = new List<AssertCmd>();
-
- foreach (var ens in impl.Proc.Ensures)
- {
- if(ens.Free)
- throw new InvalidProgramForSecureVc("SecureVc: Free Ensures not supported");
- var dd = new Duplicator();
- secureAsserts.Add(new AssertCmd(ens.tok, Expr.Not(ens.Condition)));
- logicalAsserts.Add(dd.VisitAssertCmd(new AssertCmd(ens.tok, ens.Condition)) as AssertCmd);
- }
- impl.Proc.Ensures.Clear();
-
- // Make a copy of the impl
- var dup = new Duplicator();
- var implDup = dup.VisitImplementation(impl);
-
- // Get exit block
- var eb = GetExitBlock(impl);
-
- // Create two blocks: one for secureAsserts, one for logical asserts
- var ebSecure = new Block(Token.NoToken, "svc_secure_asserts", new List<Cmd>(), new ReturnCmd(Token.NoToken));
- var ebLogical = new Block(Token.NoToken, "svc_logical_asserts", new List<Cmd>(), new ReturnCmd(Token.NoToken));
-
- eb.TransferCmd = new GotoCmd(eb.TransferCmd.tok, new List<Block> { ebSecure, ebLogical });
- impl.Blocks.Add(ebSecure);
- impl.Blocks.Add(ebLogical);
-
- // Rename spec, while create copies of the hidden variables
- var substOld = new Dictionary<Variable, Expr>();
- var substVarSpec = new Dictionary<Variable, Expr>();
- var substVarPath = new Dictionary<Variable, Expr>();
- foreach (var g in program.GlobalVariables)
- {
- if (!isHidden(g)) continue;
- var lv = GetNewLocal(g, "In");
- impl.LocVars.Add(lv);
- substOld.Add(g, Expr.Ident(lv));
- }
-
- for(int i = 0; i < impl.InParams.Count; i++)
- {
- var v = impl.Proc.InParams[i];
- if (!isHidden(v))
- {
- substVarSpec.Add(impl.Proc.InParams[i], Expr.Ident(impl.InParams[i]));
- continue;
- }
-
- var lv = GetNewLocal(v, "In");
- impl.LocVars.Add(lv);
- substVarSpec.Add(v, Expr.Ident(lv));
- substVarPath.Add(impl.InParams[i], Expr.Ident(lv));
- }
-
- for (int i = 0; i < impl.OutParams.Count; i++)
- {
- var v = impl.Proc.OutParams[i];
- if (!isHidden(v))
- {
- substVarSpec.Add(impl.Proc.OutParams[i], Expr.Ident(impl.OutParams[i]));
- continue;
- }
-
- var lv = GetNewLocal(v, "Out");
- impl.LocVars.Add(lv);
- substVarSpec.Add(v, Expr.Ident(lv));
- substVarPath.Add(impl.OutParams[i], Expr.Ident(lv));
- }
-
- foreach (var g in program.GlobalVariables)
- {
- if (!isHidden(g)) continue;
- if (!impl.Proc.Modifies.Any(ie => ie.Name == g.Name)) continue;
-
- var lv = GetNewLocal(g, "Out");
- impl.LocVars.Add(lv);
- substVarSpec.Add(g, Expr.Ident(lv));
- substVarPath.Add(g, Expr.Ident(lv));
- }
-
- secureAsserts = secureAsserts.ConvertAll(ac =>
- Substituter.ApplyReplacingOldExprs(
- Substituter.SubstitutionFromHashtable(substVarSpec),
- Substituter.SubstitutionFromHashtable(substOld),
- ac) as AssertCmd);
-
- var substVarProcToImpl = new Dictionary<Variable, Expr>();
- for (int i = 0; i < impl.InParams.Count; i++)
- substVarProcToImpl.Add(impl.Proc.InParams[i], Expr.Ident(impl.InParams[i]));
-
- for (int i = 0; i < impl.OutParams.Count; i++)
- substVarProcToImpl.Add(impl.Proc.OutParams[i], Expr.Ident(impl.OutParams[i]));
-
- logicalAsserts = logicalAsserts.ConvertAll(ac =>
- Substituter.Apply(Substituter.SubstitutionFromHashtable(substVarProcToImpl), ac)
- as AssertCmd);
-
- // Paths
- foreach (var path in GetAllPaths(implDup))
- {
- var wp = ComputeWP(implDup, path);
-
- // replace hidden variables to match those used in the spec
- wp = Substituter.ApplyReplacingOldExprs(
- Substituter.SubstitutionFromHashtable(substVarPath),
- Substituter.SubstitutionFromHashtable(substOld),
- wp);
-
- ebSecure.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(wp)));
- }
-
- ebSecure.Cmds.AddRange(secureAsserts);
- ebLogical.Cmds.AddRange(logicalAsserts);
-
- if (outfile != null)
- {
- impl.Proc.Emit(outfile, 0);
- impl.Emit(outfile, 0);
- }
-
- ModelViewInfo mvInfo;
- ConvertCFG2DAG(impl);
- var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
-
- var gen = prover.VCExprGen;
- var exprGen = prover.Context.ExprGen;
- var translator = prover.Context.BoogieExprTranslator;
-
- var label2absy = new Dictionary<int, Absy>();
- VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, prover.Context);
- translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
- var implVc = gen.Not(GenerateVCAux(impl, null, label2absy, prover.Context));
-
- handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, prover.Context, program);
-
- prover.Assert(implVc, true);
- }
-
- Expr ComputeWP(Implementation impl, List<Cmd> path)
- {
- Expr expr = Expr.True;
-
- // create constants for out varibles
- var subst = new Dictionary<Variable, Expr>();
- foreach (var g in impl.Proc.Modifies)
- {
- var c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,
- "svc_out_const_" + g.Name, g.Decl.TypedIdent.Type));
- subst.Add(c, g);
- expr = Expr.And(expr, Expr.Eq(Expr.Ident(c), g));
- }
-
- foreach (var v in impl.OutParams)
- {
- var c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,
- "svc_out_const_" + v.Name, v.TypedIdent.Type));
- subst.Add(c, Expr.Ident(v));
- expr = Expr.And(expr, Expr.Eq(Expr.Ident(c), Expr.Ident(v)));
- }
-
- // we need this technicality
- var subst1 = new Dictionary<Variable, Expr>();
- foreach (var g in program.GlobalVariables)
- {
- subst1.Add(g, new OldExpr(Token.NoToken, Expr.Ident(g)));
- }
-
- // Implicitly close with havoc of all the locals and OutParams
- path.Insert(0, new HavocCmd(Token.NoToken, new List<IdentifierExpr>(
- impl.LocVars.Select(v => Expr.Ident(v)).Concat(
- impl.OutParams.Select(v => Expr.Ident(v))))));
-
- for (int i = path.Count - 1; i >= 0; i--)
- {
- var cmd = path[i];
- if (cmd is AssumeCmd)
- {
- expr = Expr.And(expr, (cmd as AssumeCmd).Expr);
- }
- else if (cmd is AssignCmd)
- {
- var h = new Dictionary<Variable, Expr>();
- var acmd = cmd as AssignCmd;
- for (int j = 0; j < acmd.Lhss.Count; j++)
- {
- h.Add(acmd.Lhss[j].DeepAssignedVariable, acmd.Rhss[j]);
- }
- var s = Substituter.SubstitutionFromHashtable(h);
- expr = Substituter.Apply(s, expr);
- }
- else if (cmd is HavocCmd)
- {
- var h = new Dictionary<Variable, Expr>();
- var formals = new List<Variable>();
-
- var vc = new VariableCollector();
- vc.VisitExpr(expr);
-
- foreach (var ie in (cmd as HavocCmd).Vars)
- {
- if (!vc.usedVars.Contains(ie.Decl)) continue;
- var f = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,
- ie.Decl.Name + "_formal", ie.Decl.TypedIdent.Type));
- h.Add(ie.Decl, Expr.Ident(f));
- formals.Add(f);
- }
- if (!formals.Any())
- continue;
- var s = Substituter.SubstitutionFromHashtable(h);
- expr = Substituter.Apply(s, expr);
- expr = new ExistsExpr(Token.NoToken, formals, expr);
- }
- else
- {
- throw new InvalidProgramForSecureVc(string.Format("Unhandled cmd: {0}", cmd));
- }
- }
-
- // Implicitly close with havoc of all the locals and OutParams
-
-
-
- expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst1), expr);
- expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst),
- Substituter.SubstitutionFromHashtable(new Dictionary<Variable,Expr>()), expr);
- expr.Typecheck(new TypecheckingContext(null));
- return expr;
- }
-
- // Generate all paths in the impl
- IEnumerable<List<Cmd>> GetAllPaths(Implementation impl)
- {
- var stk = new Stack<Tuple<Block, int>>();
- stk.Push(Tuple.Create(impl.Blocks[0], 0));
-
- while (stk.Any())
- {
- var tup = stk.Peek();
- if (tup.Item1.TransferCmd is ReturnCmd)
- {
- var ret = new List<Cmd>();
- var ls = stk.ToList();
- ls.Iter(t => ret.AddRange(t.Item1.Cmds));
- yield return ret;
-
- stk.Pop();
- continue;
- }
-
- stk.Pop();
-
- var gc = tup.Item1.TransferCmd as GotoCmd;
- if (gc.labelTargets.Count <= tup.Item2)
- continue;
-
- stk.Push(Tuple.Create(tup.Item1, tup.Item2 + 1));
- stk.Push(Tuple.Create(gc.labelTargets[tup.Item2], 0));
- }
- yield break;
- }
-
- bool isHidden(Variable v)
- {
- return QKeyValue.FindBoolAttribute(v.Attributes, "hidden");
- }
-
- bool isVisible(Variable v)
- {
- return !isHidden(v);
- }
-
- public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback)
- {
- Debug.Assert(this.program == program);
-
- // Record current time
- var startTime = DateTime.UtcNow;
-
- CommandLineOptions.Clo.ProverCCLimit = 1;
- prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
-
- // Flush any axioms that came with the program before we start SI on this implementation
- prover.AssertAxioms();
-
- GenVc(impl, callback);
-
- prover.Check();
- var outcome = prover.CheckOutcomeCore(handler);
- //var outcome = ProverInterface.Outcome.Valid;
-
- prover.Close();
-
-
-
- //Console.WriteLine("Answer = {0}", outcome);
-
- return ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
- }
- }
-
-} // namespace VC
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.Diagnostics;
+using System.Linq;
+using System.Text;
+using System.IO;
+using Microsoft.Boogie;
+using Microsoft.Boogie.GraphUtil;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace VC {
+ using Bpl = Microsoft.Boogie;
+
+ public class StratifiedVC {
+ public StratifiedInliningInfo info;
+ public int id;
+ public List<VCExprVar> interfaceExprVars;
+
+ // boolControlVC (block -> its bool variable)
+ public Dictionary<Block, VCExpr> blockToControlVar;
+ // While using labels (block -> its label)
+ public Dictionary<Absy, string> block2label;
+
+ public Dictionary<Block, List<StratifiedCallSite>> callSites;
+ public Dictionary<Block, List<StratifiedCallSite>> recordProcCallSites;
+ public VCExpr vcexpr;
+
+ // Must-Reach Information
+ Dictionary<Block, VCExprVar> mustReachVar;
+ List<VCExprLetBinding> mustReachBindings;
+
+ public StratifiedVC(StratifiedInliningInfo siInfo, HashSet<string> procCalls) {
+ info = siInfo;
+ info.GenerateVC();
+ var vcgen = info.vcgen;
+ var prover = vcgen.prover;
+ VCExpressionGenerator gen = prover.VCExprGen;
+ var bet = prover.Context.BoogieExprTranslator;
+
+ vcexpr = info.vcexpr;
+ id = vcgen.CreateNewId();
+ interfaceExprVars = new List<VCExprVar>();
+ Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
+ foreach (VCExprVar v in info.interfaceExprVars) {
+ VCExprVar newVar = vcgen.CreateNewVar(v.Type);
+ interfaceExprVars.Add(newVar);
+ substDict.Add(v, newVar);
+ }
+ foreach (VCExprVar v in info.privateExprVars) {
+ substDict.Add(v, vcgen.CreateNewVar(v.Type));
+ }
+ if(info.controlFlowVariable != null)
+ substDict.Add(bet.LookupVariable(info.controlFlowVariable), gen.Integer(BigNum.FromInt(id)));
+ VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+ SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
+ vcexpr = substVisitor.Mutate(vcexpr, subst);
+
+ // For BoolControlVC generation
+ if (info.blockToControlVar != null)
+ {
+ blockToControlVar = new Dictionary<Block, VCExpr>();
+ foreach (var tup in info.blockToControlVar)
+ blockToControlVar.Add(tup.Key, substDict[tup.Value]);
+ }
+
+ // labels
+ if (info.label2absy != null)
+ {
+ block2label = new Dictionary<Absy, string>();
+ vcexpr = RenameVCExprLabels.Apply(vcexpr, info.vcgen.prover.VCExprGen, info.label2absy, block2label);
+ }
+
+ if(procCalls != null)
+ vcexpr = RemoveProcedureCalls.Apply(vcexpr, info.vcgen.prover.VCExprGen, procCalls);
+
+ callSites = new Dictionary<Block, List<StratifiedCallSite>>();
+ foreach (Block b in info.callSites.Keys) {
+ callSites[b] = new List<StratifiedCallSite>();
+ foreach (CallSite cs in info.callSites[b]) {
+ callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst));
+ }
+ }
+
+ recordProcCallSites = new Dictionary<Block, List<StratifiedCallSite>>();
+ foreach (Block b in info.recordProcCallSites.Keys) {
+ recordProcCallSites[b] = new List<StratifiedCallSite>();
+ foreach (CallSite cs in info.recordProcCallSites[b]) {
+ recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst));
+ }
+ }
+ }
+
+ public VCExpr MustReach(Block block)
+ {
+ Contract.Assert(!CommandLineOptions.Clo.UseLabels);
+
+ // This information is computed lazily
+ if (mustReachBindings == null)
+ {
+ var vcgen = info.vcgen;
+ var gen = vcgen.prover.VCExprGen;
+ var impl = info.impl;
+ mustReachVar = new Dictionary<Block, VCExprVar>();
+ mustReachBindings = new List<VCExprLetBinding>();
+ foreach (Block b in impl.Blocks)
+ mustReachVar[b] = vcgen.CreateNewVar(Bpl.Type.Bool);
+
+ var dag = new Graph<Block>();
+ dag.AddSource(impl.Blocks[0]);
+ foreach (Block b in impl.Blocks)
+ {
+ var gtc = b.TransferCmd as GotoCmd;
+ if (gtc != null)
+ foreach (Block dest in gtc.labelTargets)
+ dag.AddEdge(dest, b);
+ }
+ IEnumerable sortedNodes = dag.TopologicalSort();
+
+ foreach (Block currBlock in dag.TopologicalSort())
+ {
+ if (currBlock == impl.Blocks[0])
+ {
+ mustReachBindings.Add(gen.LetBinding(mustReachVar[currBlock], VCExpressionGenerator.True));
+ continue;
+ }
+
+ VCExpr expr = VCExpressionGenerator.False;
+ foreach (var pred in dag.Successors(currBlock))
+ {
+ VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(pred.UniqueId)));
+ VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(currBlock.UniqueId)));
+ expr = gen.Or(expr, gen.And(mustReachVar[pred], controlTransferExpr));
+ }
+ mustReachBindings.Add(gen.LetBinding(mustReachVar[currBlock], expr));
+ }
+ }
+
+ Contract.Assert(mustReachVar.ContainsKey(block));
+ return info.vcgen.prover.VCExprGen.Let(mustReachBindings, mustReachVar[block]);
+ }
+
+ public List<StratifiedCallSite> CallSites {
+ get {
+ var ret = new List<StratifiedCallSite>();
+ foreach (var b in callSites.Keys) {
+ foreach (var cs in callSites[b]) {
+ ret.Add(cs);
+ }
+ }
+ return ret;
+ }
+ }
+
+ public List<StratifiedCallSite> RecordProcCallSites {
+ get {
+ var ret = new List<StratifiedCallSite>();
+ foreach (var b in recordProcCallSites.Keys) {
+ foreach (var cs in recordProcCallSites[b]) {
+ ret.Add(cs);
+ }
+ }
+ return ret;
+ }
+ }
+
+ public override string ToString()
+ {
+ return info.impl.Name;
+ }
+ }
+
+ // Rename all labels in a VC to (globally) fresh labels
+ class RenameVCExprLabels : MutatingVCExprVisitor<bool>
+ {
+ Dictionary<int, Absy> label2absy;
+ Dictionary<Absy, string> absy2newlabel;
+ static int counter = 11;
+
+ RenameVCExprLabels(VCExpressionGenerator gen, Dictionary<int, Absy> label2absy, Dictionary<Absy, string> absy2newlabel)
+ : base(gen)
+ {
+ this.label2absy = label2absy;
+ this.absy2newlabel = absy2newlabel;
+ }
+
+ public static VCExpr Apply(VCExpr expr, VCExpressionGenerator gen, Dictionary<int, Absy> label2absy, Dictionary<Absy, string> absy2newlabel)
+ {
+ return (new RenameVCExprLabels(gen, label2absy, absy2newlabel)).Mutate(expr, true);
+ }
+
+ // Finds labels and changes them to a globally unique label:
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
+ List<VCExpr/*!*/>/*!*/ newSubExprs,
+ bool changed,
+ bool arg)
+ {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
+ if (lop == null) return ret;
+ if (!(ret is VCExprNAry)) return ret;
+ VCExprNAry retnary = (VCExprNAry)ret;
+
+ // remove the sign
+ var nosign = 0;
+ if (!Int32.TryParse(lop.label.Substring(1), out nosign))
+ return ret;
+
+ if (!label2absy.ContainsKey(nosign))
+ return ret;
+
+ string newLabel = "SI" + counter.ToString();
+ counter++;
+ absy2newlabel[label2absy[nosign]] = newLabel;
+
+ if (lop.pos)
+ {
+ return Gen.LabelPos(newLabel, retnary[0]);
+ }
+ else
+ {
+ return Gen.LabelNeg(newLabel, retnary[0]);
+ }
+
+ }
+ }
+
+ // Remove the uninterpreted function calls that substitute procedure calls
+ class RemoveProcedureCalls : MutatingVCExprVisitor<bool>
+ {
+ HashSet<string> procNames;
+
+ RemoveProcedureCalls(VCExpressionGenerator gen, HashSet<string> procNames)
+ : base(gen)
+ {
+ this.procNames = procNames;
+ }
+
+ public static VCExpr Apply(VCExpr expr, VCExpressionGenerator gen, HashSet<string> procNames)
+ {
+ return (new RemoveProcedureCalls(gen, procNames)).Mutate(expr, true);
+ }
+
+ // Finds labels and changes them to a globally unique label:
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
+ List<VCExpr/*!*/>/*!*/ newSubExprs,
+ bool changed,
+ bool arg)
+ {
+ //Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ if (!(ret is VCExprNAry)) return ret;
+ VCExprNAry retnary = (VCExprNAry)ret;
+ if (!(retnary.Op is VCExprBoogieFunctionOp))
+ return ret;
+
+ var fcall = (retnary.Op as VCExprBoogieFunctionOp).Func.Name;
+ if (procNames.Contains(fcall))
+ return VCExpressionGenerator.True;
+ return ret;
+ }
+ }
+
+
+ public class CallSite {
+ public string calleeName;
+ public List<VCExpr> interfaceExprs;
+ public Block block;
+ public int numInstr; // for TraceLocation
+ public VCExprVar callSiteVar;
+ public QKeyValue Attributes; // attributes on the call cmd
+ public CallSite(string callee, List<VCExpr> interfaceExprs, VCExprVar callSiteVar, Block block, int numInstr, QKeyValue Attributes)
+ {
+ this.calleeName = callee;
+ this.interfaceExprs = interfaceExprs;
+ this.callSiteVar = callSiteVar;
+ this.block = block;
+ this.numInstr = numInstr;
+ this.Attributes = Attributes;
+ }
+ }
+
+ public class StratifiedCallSite {
+ public CallSite callSite;
+ public List<VCExpr> interfaceExprs;
+ public VCExpr callSiteExpr;
+
+ public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst) {
+ callSite = cs;
+ interfaceExprs = new List<VCExpr>();
+ foreach (VCExpr v in cs.interfaceExprs) {
+ interfaceExprs.Add(substVisitor.Mutate(v, subst));
+ }
+ if (callSite.callSiteVar != null)
+ callSiteExpr = substVisitor.Mutate(callSite.callSiteVar, subst);
+ }
+
+ public VCExpr Attach(StratifiedVC svc) {
+ Contract.Assert(interfaceExprs.Count == svc.interfaceExprVars.Count);
+ StratifiedInliningInfo info = svc.info;
+ ProverInterface prover = info.vcgen.prover;
+ VCExpressionGenerator gen = prover.VCExprGen;
+
+ Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
+ for (int i = 0; i < svc.interfaceExprVars.Count; i++) {
+ VCExprVar v = svc.interfaceExprVars[i];
+ substDict.Add(v, interfaceExprs[i]);
+ }
+ VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+ SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
+ svc.vcexpr = substVisitor.Mutate(svc.vcexpr, subst);
+ foreach (StratifiedCallSite scs in svc.CallSites) {
+ List<VCExpr> newInterfaceExprs = new List<VCExpr>();
+ foreach (VCExpr expr in scs.interfaceExprs) {
+ newInterfaceExprs.Add(substVisitor.Mutate(expr, subst));
+ }
+ scs.interfaceExprs = newInterfaceExprs;
+ }
+ foreach (StratifiedCallSite scs in svc.RecordProcCallSites) {
+ List<VCExpr> newInterfaceExprs = new List<VCExpr>();
+ foreach (VCExpr expr in scs.interfaceExprs) {
+ newInterfaceExprs.Add(substVisitor.Mutate(expr, subst));
+ }
+ scs.interfaceExprs = newInterfaceExprs;
+ }
+ //return gen.Implies(callSiteExpr, svc.vcexpr);
+ return svc.vcexpr;
+ }
+
+ public override string ToString()
+ {
+ return callSite.calleeName;
+ }
+ }
+
+ public class StratifiedInliningInfo {
+ public StratifiedVCGenBase vcgen;
+ public Implementation impl;
+ public Function function;
+ public Variable controlFlowVariable;
+ public Cmd exitAssertCmd;
+ public VCExpr vcexpr;
+ public List<VCExprVar> interfaceExprVars;
+ public List<VCExprVar> privateExprVars;
+ public Dictionary<int, Absy> label2absy;
+ public ModelViewInfo mvInfo;
+ public Dictionary<Block, List<CallSite>> callSites;
+ public Dictionary<Block, List<CallSite>> recordProcCallSites;
+ public bool initialized { get; private set; }
+ // Instrumentation to apply after PassiveImpl, but before VCGen
+ Action<Implementation> PassiveImplInstrumentation;
+
+ // boolControlVC (block -> its Bool variable)
+ public Dictionary<Block, VCExprVar> blockToControlVar;
+
+ public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen, Action<Implementation> PassiveImplInstrumentation) {
+ vcgen = stratifiedVcGen;
+ impl = implementation;
+ this.PassiveImplInstrumentation = PassiveImplInstrumentation;
+
+ List<Variable> functionInterfaceVars = new List<Variable>();
+ foreach (Variable v in vcgen.program.GlobalVariables) {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (Variable v in impl.InParams) {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (Variable v in impl.OutParams) {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (IdentifierExpr e in impl.Proc.Modifies) {
+ if (e.Decl == null) continue;
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", e.Decl.TypedIdent.Type), true));
+ }
+ Formal returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false);
+ function = new Function(Token.NoToken, impl.Name, functionInterfaceVars, returnVar);
+ vcgen.prover.Context.DeclareFunction(function, "");
+
+ List<Expr> exprs = new List<Expr>();
+ foreach (Variable v in vcgen.program.GlobalVariables) {
+ Contract.Assert(v != null);
+ exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ }
+ foreach (Variable v in impl.Proc.InParams) {
+ Contract.Assert(v != null);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (Variable v in impl.Proc.OutParams) {
+ Contract.Assert(v != null);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (IdentifierExpr ie in impl.Proc.Modifies) {
+ Contract.Assert(ie != null);
+ if (ie.Decl == null)
+ continue;
+ exprs.Add(ie);
+ }
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
+ impl.Proc.Ensures.Add(new Ensures(Token.NoToken, true, freePostExpr, "", new QKeyValue(Token.NoToken, "si_fcall", new List<object>(), null)));
+
+ initialized = false;
+ }
+
+ public void GenerateVCBoolControl()
+ {
+ Debug.Assert(!initialized);
+ Debug.Assert(CommandLineOptions.Clo.SIBoolControlVC);
+
+ // fix names for exit variables
+ var outputVariables = new List<Variable>();
+ var assertConjuncts = new List<Expr>();
+ foreach (Variable v in impl.OutParams)
+ {
+ Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
+ outputVariables.Add(c);
+ Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
+ assertConjuncts.Add(eqExpr);
+ }
+ foreach (IdentifierExpr e in impl.Proc.Modifies)
+ {
+ if (e.Decl == null) continue;
+ Variable v = e.Decl;
+ Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
+ outputVariables.Add(c);
+ Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
+ assertConjuncts.Add(eqExpr);
+ }
+ exitAssertCmd = new AssumeCmd(Token.NoToken, Expr.BinaryTreeAnd(assertConjuncts));
+ (exitAssertCmd as AssumeCmd).Attributes = new QKeyValue(Token.NoToken, "exitAssert", new List<object>(), null);
+
+ // no need for label2absy
+ label2absy = new Dictionary<int, Absy>();
+
+ // Passify
+ Program program = vcgen.program;
+ ProverInterface proverInterface = vcgen.prover;
+ vcgen.ConvertCFG2DAG(impl);
+ vcgen.PassifyImpl(impl, out mvInfo);
+
+ VCExpressionGenerator gen = proverInterface.VCExprGen;
+ var exprGen = proverInterface.Context.ExprGen;
+ var translator = proverInterface.Context.BoogieExprTranslator;
+
+ // add a boolean variable at each call site
+ vcgen.InstrumentCallSites(impl);
+
+ // typecheck
+ var tc = new TypecheckingContext(null);
+ impl.Typecheck(tc);
+
+ ///////////////////
+ // Generate the VC
+ ///////////////////
+
+ // block -> bool variable
+ blockToControlVar = new Dictionary<Block, VCExprVar>();
+ foreach (var b in impl.Blocks)
+ blockToControlVar.Add(b, gen.Variable(b.Label + "_holds", Bpl.Type.Bool));
+
+ vcexpr = VCExpressionGenerator.True;
+ foreach (var b in impl.Blocks)
+ {
+ // conjoin all assume cmds
+ VCExpr c = VCExpressionGenerator.True;
+ foreach (var cmd in b.Cmds)
+ {
+ var acmd = cmd as AssumeCmd;
+ if (acmd == null)
+ {
+ Debug.Assert(cmd is AssertCmd && (cmd as AssertCmd).Expr is LiteralExpr &&
+ ((cmd as AssertCmd).Expr as LiteralExpr).IsTrue);
+ continue;
+ }
+ var expr = translator.Translate(acmd.Expr);
+ // Label the assume if it is a procedure call
+ NAryExpr naryExpr = acmd.Expr as NAryExpr;
+ if (naryExpr != null && naryExpr.Fun is FunctionCall)
+ {
+ var id = acmd.UniqueId;
+ label2absy[id] = acmd;
+ expr = gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), expr);
+ }
+
+ c = gen.AndSimp(c, expr);
+ }
+
+ // block implies a disjunction of successors
+ Debug.Assert(!(b.TransferCmd is ReturnExprCmd), "Not supported");
+ var gc = b.TransferCmd as GotoCmd;
+ if (gc != null)
+ {
+ VCExpr succ = VCExpressionGenerator.False;
+ foreach (var sb in gc.labelTargets)
+ succ = gen.OrSimp(succ, blockToControlVar[sb]);
+ c = gen.AndSimp(c, succ);
+ }
+ else
+ {
+ // nothing to do
+ }
+ vcexpr = gen.AndSimp(vcexpr, gen.Eq(blockToControlVar[b], c));
+ }
+ // assert start block
+ vcexpr = gen.AndSimp(vcexpr, blockToControlVar[impl.Blocks[0]]);
+
+ //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);
+ // Collect other information
+ callSites = vcgen.CollectCallSites(impl);
+ recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);
+
+ // record interface variables
+ privateExprVars = new List<VCExprVar>();
+ foreach (Variable v in impl.LocVars)
+ {
+ privateExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in impl.OutParams)
+ {
+ privateExprVars.Add(translator.LookupVariable(v));
+ }
+ privateExprVars.AddRange(blockToControlVar.Values);
+
+ interfaceExprVars = new List<VCExprVar>();
+ foreach (Variable v in program.GlobalVariables)
+ {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in impl.InParams)
+ {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in outputVariables)
+ {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+ }
+
+ public void GenerateVC() {
+ if (initialized) return;
+ if (CommandLineOptions.Clo.SIBoolControlVC)
+ {
+ GenerateVCBoolControl();
+ initialized = true;
+ return;
+ }
+ List<Variable> outputVariables = new List<Variable>();
+ List<Expr> assertConjuncts = new List<Expr>();
+ foreach (Variable v in impl.OutParams) {
+ Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
+ outputVariables.Add(c);
+ Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
+ assertConjuncts.Add(eqExpr);
+ }
+ foreach (IdentifierExpr e in impl.Proc.Modifies) {
+ if (e.Decl == null) continue;
+ Variable v = e.Decl;
+ Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
+ outputVariables.Add(c);
+ Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
+ assertConjuncts.Add(eqExpr);
+ }
+ exitAssertCmd = new AssertCmd(Token.NoToken, Expr.Not(Expr.BinaryTreeAnd(assertConjuncts)));
+
+ Program program = vcgen.program;
+ ProverInterface proverInterface = vcgen.prover;
+ vcgen.ConvertCFG2DAG(impl);
+ vcgen.PassifyImpl(impl, out mvInfo);
+
+ VCExpressionGenerator gen = proverInterface.VCExprGen;
+ var exprGen = proverInterface.Context.ExprGen;
+ var translator = proverInterface.Context.BoogieExprTranslator;
+
+ VCExpr controlFlowVariableExpr = null;
+ if (!CommandLineOptions.Clo.UseLabels) {
+ controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
+ controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);
+ }
+
+ vcgen.InstrumentCallSites(impl);
+
+ if (PassiveImplInstrumentation != null)
+ PassiveImplInstrumentation(impl);
+
+ label2absy = new Dictionary<int, Absy>();
+ VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);
+ translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
+ vcexpr = gen.Not(vcgen.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverInterface.Context));
+
+ if (controlFlowVariableExpr != null)
+ {
+ VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));
+ VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
+ vcexpr = exprGen.And(eqExpr, vcexpr);
+ }
+
+ callSites = vcgen.CollectCallSites(impl);
+ recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);
+
+ privateExprVars = new List<VCExprVar>();
+ foreach (Variable v in impl.LocVars) {
+ privateExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in impl.OutParams) {
+ privateExprVars.Add(translator.LookupVariable(v));
+ }
+
+ interfaceExprVars = new List<VCExprVar>();
+ foreach (Variable v in program.GlobalVariables) {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in impl.InParams) {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in outputVariables) {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+
+ initialized = true;
+ }
+ }
+
+ public abstract class StratifiedVCGenBase : VCGen {
+ public readonly static string recordProcName = "boogie_si_record";
+ public readonly static string callSiteVarAttr = "callSiteVar";
+ public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
+ public ProverInterface prover;
+
+ public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers, Action<Implementation> PassiveImplInstrumentation)
+ : base(program, logFilePath, appendLogFile, checkers) {
+ implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();
+ prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
+ foreach (var impl in program.Implementations) {
+ implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this, PassiveImplInstrumentation);
+ }
+ GenerateRecordFunctions();
+ }
+
+ private void GenerateRecordFunctions() {
+ foreach (var proc in program.Procedures) {
+ if (!proc.Name.StartsWith(recordProcName)) continue;
+ Contract.Assert(proc.InParams.Count == 1);
+
+ // Make a new function
+ TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
+ Contract.Assert(ti != null);
+ Formal returnVar = new Formal(Token.NoToken, ti, false);
+ Contract.Assert(returnVar != null);
+
+ // Get record type
+ var argtype = proc.InParams[0].TypedIdent.Type;
+
+ var ins = new List<Variable>();
+ ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));
+
+ var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);
+ prover.Context.DeclareFunction(recordFunc, "");
+
+ var exprs = new List<Expr>();
+ exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));
+
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);
+ proc.Ensures.Add(new Ensures(true, freePostExpr));
+ }
+ }
+
+ public override void Close() {
+ prover.Close();
+ base.Close();
+ }
+
+ public void InstrumentCallSites(Implementation implementation) {
+ var callSiteId = 0;
+ foreach (Block block in implementation.Blocks) {
+ List<Cmd> newCmds = new List<Cmd>();
+ for (int i = 0; i < block.Cmds.Count; i++) {
+ Cmd cmd = block.Cmds[i];
+ newCmds.Add(cmd);
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ if (assumeCmd == null) continue;
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null) continue;
+ if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;
+ Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "SICS" + callSiteId, Microsoft.Boogie.Type.Bool));
+ implementation.LocVars.Add(callSiteVar);
+ var toInsert = new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar),
+ new QKeyValue(Token.NoToken, callSiteVarAttr, new List<object>(), null));
+ newCmds.Add(toInsert);
+ callSiteId++;
+ }
+ block.Cmds = newCmds;
+ }
+ }
+
+ public Dictionary<Block, List<CallSite>> CollectCallSites(Implementation implementation) {
+ var callSites = new Dictionary<Block, List<CallSite>>();
+ foreach (Block block in implementation.Blocks) {
+ for (int i = 0; i < block.Cmds.Count; i++) {
+ Cmd cmd = block.Cmds[i];
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ if (assumeCmd == null) continue;
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null) continue;
+ if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;
+ List<VCExpr> interfaceExprs = new List<VCExpr>();
+ foreach (Expr e in naryExpr.Args) {
+ interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e));
+ }
+ int instr = i;
+ i++;
+ AssumeCmd callSiteAssumeCmd = (AssumeCmd)block.Cmds[i];
+ IdentifierExpr iexpr = (IdentifierExpr) callSiteAssumeCmd.Expr;
+ CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr, assumeCmd.Attributes);
+ if (!callSites.ContainsKey(block))
+ callSites[block] = new List<CallSite>();
+ callSites[block].Add(cs);
+ }
+ }
+ return callSites;
+ }
+
+ public Dictionary<Block, List<CallSite>> CollectRecordProcedureCallSites(Implementation implementation) {
+ var callSites = new Dictionary<Block, List<CallSite>>();
+ foreach (Block block in implementation.Blocks) {
+ for (int i = 0; i < block.Cmds.Count; i++) {
+ AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd;
+ if (assumeCmd == null) continue;
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null) continue;
+ if (!naryExpr.Fun.FunctionName.StartsWith(recordProcName)) continue;
+ List<VCExpr> interfaceExprs = new List<VCExpr>();
+ foreach (Expr e in naryExpr.Args) {
+ interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e));
+ }
+ CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, null, block, i, assumeCmd.Attributes);
+ if (!callSites.ContainsKey(block))
+ callSites[block] = new List<CallSite>();
+ callSites[block].Add(cs);
+ }
+ }
+ return callSites;
+ }
+
+ private int macroCountForStratifiedInlining = 0;
+ public Macro CreateNewMacro() {
+ string newName = "SIMacro@" + macroCountForStratifiedInlining.ToString();
+ macroCountForStratifiedInlining++;
+ return new Macro(Token.NoToken, newName, new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));
+ }
+ private int varCountForStratifiedInlining = 0;
+ public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {
+ string newName = "SIV@" + varCountForStratifiedInlining.ToString();
+ varCountForStratifiedInlining++;
+ Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));
+ prover.Context.DeclareConstant(newVar, false, null);
+ return prover.VCExprGen.Variable(newVar.Name, type);
+ }
+ private int idCountForStratifiedInlining = 0;
+ public int CreateNewId() {
+ return idCountForStratifiedInlining++;
+ }
+
+ // Used inside PassifyImpl
+ protected override void addExitAssert(string implName, Block exitBlock) {
+ if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {
+ var exitAssertCmd = implName2StratifiedInliningInfo[implName].exitAssertCmd;
+ if(exitAssertCmd != null) exitBlock.Cmds.Add(exitAssertCmd);
+ }
+ }
+
+ public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {
+ // Construct the set of inlined procs in the original program
+ var inlinedProcs = new HashSet<string>();
+ foreach (var decl in program.TopLevelDeclarations) {
+ // Implementations
+ if (decl is Implementation) {
+ var impl = decl as Implementation;
+ if (!(impl.Proc is LoopProcedure)) {
+ inlinedProcs.Add(impl.Name);
+ }
+ }
+
+ // And recording procedures
+ if (decl is Procedure) {
+ var proc = decl as Procedure;
+ if (proc.Name.StartsWith(recordProcName)) {
+ Debug.Assert(!(decl is LoopProcedure));
+ inlinedProcs.Add(proc.Name);
+ }
+ }
+ }
+
+ return extractLoopTraceRec(
+ new CalleeCounterexampleInfo(cex, new List<object>()),
+ mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
+ }
+
+ protected override bool elIsLoop(string procname) {
+ StratifiedInliningInfo info = null;
+ if (implName2StratifiedInliningInfo.ContainsKey(procname)) {
+ info = implName2StratifiedInliningInfo[procname];
+ }
+
+ if (info == null) return false;
+
+ var lp = info.impl.Proc as LoopProcedure;
+
+ if (lp == null) return false;
+ return true;
+ }
+
+ public abstract Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars);
+ }
+
+ public class StratifiedVCGen : StratifiedVCGenBase {
+ public bool PersistCallTree;
+ public static HashSet<string> callTree = null;
+ public int numInlined = 0;
+ public int vcsize = 0;
+ private HashSet<string> procsThatReachedRecBound;
+ private Dictionary<string, int> extraRecBound;
+
+ public StratifiedVCGen(bool usePrevCallTree, HashSet<string> prevCallTree,
+ Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : this(program, logFilePath, appendLogFile, checkers)
+ {
+ if (usePrevCallTree) {
+ callTree = prevCallTree;
+ PersistCallTree = true;
+ }
+ else {
+ PersistCallTree = false;
+ }
+ }
+
+ public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, logFilePath, appendLogFile, checkers, null) {
+ PersistCallTree = false;
+ procsThatReachedRecBound = new HashSet<string>();
+
+ extraRecBound = new Dictionary<string, int>();
+ program.TopLevelDeclarations.OfType<Implementation>()
+ .Iter(impl =>
+ {
+ var b = QKeyValue.FindIntAttribute(impl.Attributes, "SIextraRecBound", -1);
+ if (b != -1) extraRecBound.Add(impl.Name, b);
+ });
+ }
+
+ // Extra rec bound for procedures
+ public int GetExtraRecBound(string procName) {
+ if (!extraRecBound.ContainsKey(procName))
+ return 0;
+ else return extraRecBound[procName];
+ }
+
+ public class ApiChecker {
+ public ProverInterface prover;
+ public ProverInterface.ErrorHandler reporter;
+
+ public ApiChecker(ProverInterface prover, ProverInterface.ErrorHandler reporter) {
+ this.reporter = reporter;
+ this.prover = prover;
+ }
+
+ private Outcome CheckVC() {
+ prover.Check();
+ ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter);
+
+ return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+ }
+
+ public Outcome CheckAssumptions(List<VCExpr> assumptions) {
+ if (assumptions.Count == 0) {
+ return CheckVC();
+ }
+
+ prover.Push();
+ foreach (var a in assumptions) {
+ prover.Assert(a, true);
+ }
+ Outcome ret = CheckVC();
+ prover.Pop();
+ return ret;
+ }
+
+ public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions) {
+ List<int> unsatisfiedSoftAssumptions;
+ ProverInterface.Outcome outcome = prover.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter);
+ return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+ }
+
+ public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore) {
+ ProverInterface.Outcome outcome = prover.CheckAssumptions(assumptions, out unsatCore, reporter);
+ return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+ }
+ }
+
+ // Store important information related to a single VerifyImplementation query
+ public class VerificationState {
+ // The call tree
+ public FCallHandler calls;
+ public ApiChecker checker;
+ // For statistics
+ public int vcSize;
+ public int expansionCount;
+
+ public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter) {
+ prover.Assert(vcMain, true);
+ this.calls = calls;
+ this.checker = new ApiChecker(prover, reporter);
+ vcSize = 0;
+ expansionCount = 0;
+ }
+ }
+
+ class FindLeastOORException : Exception
+ {
+ public Outcome outcome;
+
+ public FindLeastOORException(string msg, Outcome outcome)
+ : base(msg)
+ {
+ this.outcome = outcome;
+ }
+ }
+
+ public override Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
+ // Record current time
+ var startTime = DateTime.UtcNow;
+
+ // No Max: avoids theorem prover restarts
+ CommandLineOptions.Clo.MaxProverMemory = 0;
+
+ // Initialize cache
+ satQueryCache = new Dictionary<int, List<HashSet<string>>>();
+ unsatQueryCache = new Dictionary<int, List<HashSet<string>>>();
+
+ Contract.Assert(implName2StratifiedInliningInfo != null);
+
+ // Build VCs for all procedures
+ implName2StratifiedInliningInfo.Values
+ .Iter(info => info.GenerateVC());
+
+ // Get the VC of the current procedure
+ VCExpr vcMain = implName2StratifiedInliningInfo[impl.Name].vcexpr;
+ Dictionary<int, Absy> mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;
+
+ // Find all procedure calls in vc and put labels on them
+ FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
+ calls.setCurrProcAsMain();
+ vcMain = calls.Mutate(vcMain, true);
+
+ try
+ {
+
+ // Put all of the necessary state into one object
+ var vState = new VerificationState(vcMain, calls, prover, new EmptyErrorHandler());
+
+ // We'll restore the original state of the theorem prover at the end
+ // of this procedure
+ vState.checker.prover.Push();
+
+ // Do eager inlining
+ while (calls.currCandidates.Count > 0)
+ {
+ List<int> toExpand = new List<int>();
+
+ foreach (int id in calls.currCandidates)
+ {
+ Debug.Assert(calls.getRecursionBound(id) <= 1, "Recursion not supported");
+ toExpand.Add(id);
+ }
+ DoExpansion(toExpand, vState);
+ }
+
+ // Find all the boolean constants
+ var allConsts = new HashSet<VCExprVar>();
+ foreach (var constant in program.Constants)
+ {
+ if (!allBoolVars.Contains(constant.Name)) continue;
+ var v = prover.Context.BoogieExprTranslator.LookupVariable(constant);
+ allConsts.Add(v);
+ }
+
+ // Now, lets start the algo
+ var min = refinementLoop(vState.checker, new HashSet<VCExprVar>(), allConsts, allConsts);
+
+ var ret = new HashSet<string>();
+ foreach (var v in min)
+ {
+ //Console.WriteLine(v.Name);
+ ret.Add(v.Name);
+ }
+ allBoolVars = ret;
+
+ vState.checker.prover.Pop();
+
+ return Outcome.Correct;
+ }
+ catch (FindLeastOORException e)
+ {
+ Console.WriteLine("Exception in FindLeastToVerify: {0}, {1}", e.Message, e.outcome);
+ return e.outcome;
+ }
+ }
+
+ private HashSet<VCExprVar> refinementLoop(ApiChecker apiChecker, HashSet<VCExprVar> trackedVars, HashSet<VCExprVar> trackedVarsUpperBound, HashSet<VCExprVar> allVars) {
+ Debug.Assert(trackedVars.IsSubsetOf(trackedVarsUpperBound));
+
+ // If we already know the fate of all vars, then we're done.
+ if (trackedVars.Count == trackedVarsUpperBound.Count)
+ return new HashSet<VCExprVar>(trackedVars);
+
+ // See if we already have enough variables tracked
+ var success = refinementLoopCheckPath(apiChecker, trackedVars, allVars);
+ if (success) {
+ // We have enough
+ return new HashSet<VCExprVar>(trackedVars);
+ }
+
+ // If all that remains is 1 variable, then we know that we must track it
+ if (trackedVars.Count + 1 == trackedVarsUpperBound.Count)
+ return new HashSet<VCExprVar>(trackedVarsUpperBound);
+
+ // Partition the remaining set of variables
+ HashSet<VCExprVar> part1, part2;
+ var temp = new HashSet<VCExprVar>(trackedVarsUpperBound);
+ temp.ExceptWith(trackedVars);
+ Partition<VCExprVar>(temp, out part1, out part2);
+
+ // First half
+ var fh = new HashSet<VCExprVar>(trackedVars); fh.UnionWith(part2);
+ var s1 = refinementLoop(apiChecker, fh, trackedVarsUpperBound, allVars);
+
+ var a = new HashSet<VCExprVar>(part1); a.IntersectWith(s1);
+ var b = new HashSet<VCExprVar>(part1); b.ExceptWith(s1);
+ var c = new HashSet<VCExprVar>(trackedVarsUpperBound); c.ExceptWith(b);
+ a.UnionWith(trackedVars);
+
+ // Second half
+ return refinementLoop(apiChecker, a, c, allVars);
+ }
+
+ Dictionary<int, List<HashSet<string>>> satQueryCache;
+ Dictionary<int, List<HashSet<string>>> unsatQueryCache;
+
+ private bool refinementLoopCheckPath(ApiChecker apiChecker, HashSet<VCExprVar> varsToSet, HashSet<VCExprVar> allVars) {
+ var assumptions = new List<VCExpr>();
+ var prover = apiChecker.prover;
+ var query = new HashSet<string>();
+ varsToSet.Iter(v => query.Add(v.Name));
+
+ if (checkCache(query, unsatQueryCache)) {
+ prover.LogComment("FindLeast: Query Cache Hit");
+ return true;
+ }
+ if (checkCache(query, satQueryCache)) {
+ prover.LogComment("FindLeast: Query Cache Hit");
+ return false;
+ }
+
+ prover.LogComment("FindLeast: Query Begin");
+
+ foreach (var c in allVars) {
+ if (varsToSet.Contains(c)) {
+ assumptions.Add(c);
+ }
+ else {
+ assumptions.Add(prover.VCExprGen.Not(c));
+ }
+ }
+
+ var o = apiChecker.CheckAssumptions(assumptions);
+ if (o != Outcome.Correct && o != Outcome.Errors)
+ {
+ throw new FindLeastOORException("OOR", o);
+ }
+ //Console.WriteLine("Result = " + o.ToString());
+ prover.LogComment("FindLeast: Query End");
+
+ if (o == Outcome.Correct) {
+ insertCache(query, unsatQueryCache);
+ return true;
+ }
+
+ insertCache(query, satQueryCache);
+ return false;
+ }
+
+ private bool checkCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache) {
+ if (!cache.ContainsKey(q.Count)) return false;
+ foreach (var s in cache[q.Count]) {
+ if (q.SetEquals(s)) return true;
+ }
+ return false;
+ }
+
+ private void insertCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache) {
+ if (!cache.ContainsKey(q.Count)) {
+ cache.Add(q.Count, new List<HashSet<string>>());
+ }
+ cache[q.Count].Add(q);
+ }
+
+ public static void Partition<T>(HashSet<T> values, out HashSet<T> part1, out HashSet<T> part2) {
+ part1 = new HashSet<T>();
+ part2 = new HashSet<T>();
+ var size = values.Count;
+ var crossed = false;
+ var curr = 0;
+ foreach (var s in values) {
+ if (crossed) part2.Add(s);
+ else part1.Add(s);
+ curr++;
+ if (!crossed && curr >= size / 2) crossed = true;
+ }
+ }
+
+ public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {
+ Debug.Assert(QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"));
+ Debug.Assert(this.program == program);
+
+ // Record current time
+ var startTime = DateTime.UtcNow;
+
+ // Flush any axioms that came with the program before we start SI on this implementation
+ prover.AssertAxioms();
+
+ // Run live variable analysis
+ if (CommandLineOptions.Clo.LiveVariableAnalysis == 2) {
+ Microsoft.Boogie.InterProcGenKill.ComputeLiveVars(impl, program);
+ }
+
+ // Get the VC of the current procedure
+ StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];
+ info.GenerateVC();
+ VCExpr vc = info.vcexpr;
+ Dictionary<int, Absy> mainLabel2absy = info.label2absy;
+ var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info);
+
+ // Find all procedure calls in vc and put labels on them
+ FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
+ calls.setCurrProcAsMain();
+ vc = calls.Mutate(vc, true);
+ reporter.SetCandidateHandler(calls);
+ calls.id2VC.Add(0, vc);
+ calls.extraRecursion = extraRecBound;
+ if (CommandLineOptions.Clo.SIBoolControlVC)
+ {
+ calls.candiate2block2controlVar.Add(0, new Dictionary<Block, VCExpr>());
+ implName2StratifiedInliningInfo[impl.Name].blockToControlVar.Iter(tup =>
+ calls.candiate2block2controlVar[0].Add(tup.Key, tup.Value));
+ }
+
+ // We'll restore the original state of the theorem prover at the end
+ // of this procedure
+ prover.Push();
+
+ // Put all of the necessary state into one object
+ var vState = new VerificationState(vc, calls, prover, reporter);
+ vState.vcSize += SizeComputingVisitor.ComputeSize(vc);
+
+ Outcome ret = Outcome.ReachedBound;
+
+ #region eager inlining
+ for (int i = 1; i < CommandLineOptions.Clo.StratifiedInlining && calls.currCandidates.Count > 0; i++) {
+ List<int> toExpand = new List<int>();
+
+ foreach (int id in calls.currCandidates) {
+ if (calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound) {
+ toExpand.Add(id);
+ }
+ }
+ DoExpansion(toExpand, vState);
+ }
+ #endregion
+
+ #region Repopulate call tree, if there is one
+ if (PersistCallTree && callTree != null) {
+ bool expand = true;
+ while (expand) {
+ List<int> toExpand = new List<int>();
+ foreach (int id in calls.currCandidates) {
+ if (callTree.Contains(calls.getPersistentId(id))) {
+ toExpand.Add(id);
+ }
+ }
+ if (toExpand.Count == 0) expand = false;
+ else {
+ DoExpansion(toExpand, vState);
+ }
+ }
+ }
+ #endregion
+
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1) {
+ Console.WriteLine(">> SI: Size of VC after eager inlining: {0}", vState.vcSize);
+ }
+
+ // Under-approx query is only needed if something was inlined since
+ // the last time an under-approx query was made
+ // TODO: introduce this
+ // bool underApproxNeeded = true;
+
+ // The recursion bound for stratified search
+ int bound = CommandLineOptions.Clo.NonUniformUnfolding ? CommandLineOptions.Clo.RecursionBound : 1;
+
+ int done = 0;
+
+ int iters = 0;
+
+ // for blocking candidates (and focusing on a counterexample)
+ var block = new HashSet<int>();
+
+ // Process tasks while not done. We're done when:
+ // case 1: (correct) We didn't find a bug (either an over-approx query was valid
+ // or we reached the recursion bound) and the task is "step"
+ // case 2: (bug) We find a bug
+ // case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
+ while (true)
+ {
+ // Check timeout
+ if (CommandLineOptions.Clo.ProverKillTime != -1)
+ {
+ if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)
+ {
+ ret = Outcome.TimedOut;
+ break;
+ }
+ }
+
+ if (done > 0)
+ {
+ break;
+ }
+
+ // Stratified Step
+ ret = stratifiedStep(bound, vState, block);
+ iters++;
+
+ // Sorry, out of luck (time/memory)
+ if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut)
+ {
+ done = 3;
+ continue;
+ }
+
+ if (ret == Outcome.Errors && reporter.underapproximationMode)
+ {
+ // Found a bug
+ done = 2;
+ }
+ else if (ret == Outcome.Correct)
+ {
+ if (block.Count == 0)
+ {
+ // Correct
+ done = 1;
+ }
+ else
+ {
+ // reset blocked and continue loop
+ block.Clear();
+ }
+ }
+ else if (ret == Outcome.ReachedBound)
+ {
+ if (block.Count == 0)
+ {
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
+ Console.WriteLine(">> SI: Exhausted Bound {0}", bound);
+
+ // Increment bound
+ bound++;
+
+ if (bound > CommandLineOptions.Clo.RecursionBound)
+ {
+ // Correct under bound
+ done = 1;
+ }
+ }
+ else
+ {
+ // reset blocked and continue loop
+ block.Clear();
+ }
+ }
+ else
+ {
+ // Do inlining
+ Debug.Assert(ret == Outcome.Errors && !reporter.underapproximationMode);
+ Contract.Assert(reporter.candidatesToExpand.Count != 0);
+
+ #region expand call tree
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1)
+ {
+ Console.Write(">> SI Inlining: ");
+ reporter.candidatesToExpand
+ .Select(c => calls.getProc(c))
+ .Iter(c => Console.Write("{0} ", c));
+
+ Console.WriteLine();
+ }
+
+ // Expand and try again
+ vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
+ DoExpansion(reporter.candidatesToExpand, vState);
+ vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
+
+ #endregion
+ }
+ }
+
+ // Pop off everything that we pushed so that there are no side effects from
+ // this call to VerifyImplementation
+ vState.checker.prover.Pop();
+
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1) {
+ Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);
+ Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);
+ Console.WriteLine(">> SI: VC Size: {0}", vState.vcSize);
+ }
+
+ vcsize = vState.vcSize;
+ numInlined = (calls.candidateParent.Keys.Count + 1) - (calls.currCandidates.Count);
+
+ var rbound = "Procs that reached bound: ";
+ foreach (var s in procsThatReachedRecBound) rbound += " " + s;
+ if (ret == Outcome.ReachedBound) Helpers.ExtraTraceInformation(rbound);
+ if (CommandLineOptions.Clo.StackDepthBound > 0 && ret == Outcome.Correct) ret = Outcome.ReachedBound;
+
+ // Store current call tree
+ if (PersistCallTree && (ret == Outcome.Correct || ret == Outcome.Errors || ret == Outcome.ReachedBound)) {
+ callTree = new HashSet<string>();
+ //var persistentNodes = new HashSet<int>(calls.candidateParent.Values);
+ var persistentNodes = new HashSet<int>(calls.candidateParent.Keys);
+ persistentNodes.Add(0);
+ persistentNodes.ExceptWith(calls.currCandidates);
+
+ foreach (var id in persistentNodes) {
+ var pid = calls.getPersistentId(id);
+ Debug.Assert(!callTree.Contains(pid));
+ callTree.Add(pid);
+ }
+ }
+ return ret;
+ }
+
+ // A step of the stratified inlining algorithm: both under-approx and over-approx queries
+ private Outcome stratifiedStep(int bound, VerificationState vState, HashSet<int> block) {
+ var calls = vState.calls;
+ var checker = vState.checker;
+ var prover = checker.prover;
+ var reporter = checker.reporter as StratifiedInliningErrorReporter;
+
+ reporter.underapproximationMode = true;
+ prover.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");
+ List<VCExpr> assumptions = new List<VCExpr>();
+
+ foreach (int id in calls.currCandidates) {
+ assumptions.Add(calls.getFalseExpr(id));
+ }
+ Outcome ret = checker.CheckAssumptions(assumptions);
+ prover.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
+
+ if (ret != Outcome.Correct) {
+ // Either the query returned an error or it ran out of memory or time.
+ // In all cases, we are done.
+ return ret;
+ }
+
+ if (calls.currCandidates.Count == 0) {
+ // If we didn't underapproximate, then we're done
+ return ret;
+ }
+
+ prover.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;");
+
+ // Over-approx query
+ reporter.underapproximationMode = false;
+
+ // Push "true" for all, except:
+ // push "false" for all candidates that have reached
+ // the recursion bounds
+
+ bool allTrue = true;
+ bool allFalse = true;
+ List<VCExpr> softAssumptions = new List<VCExpr>();
+
+ assumptions = new List<VCExpr>();
+ procsThatReachedRecBound.Clear();
+
+ foreach (int id in calls.currCandidates) {
+
+ int idBound = calls.getRecursionBound(id);
+ int sd = calls.getStackDepth(id);
+ if (idBound <= bound && (CommandLineOptions.Clo.StackDepthBound == 0 || sd <= CommandLineOptions.Clo.StackDepthBound)) {
+ if (idBound > 1)
+ softAssumptions.Add(calls.getFalseExpr(id));
+
+ if (block.Contains(id)) {
+ assumptions.Add(calls.getFalseExpr(id));
+ allTrue = false;
+ }
+ else {
+ allFalse = false;
+ }
+ }
+ else {
+ procsThatReachedRecBound.Add(calls.getProc(id));
+ assumptions.Add(calls.getFalseExpr(id));
+ allTrue = false;
+ }
+ }
+
+ if (allFalse) {
+ // If we made all candidates false, then this is the same
+ // as the underapprox query. We already know the answer.
+ ret = Outcome.Correct;
+ }
+ else {
+ ret = CommandLineOptions.Clo.NonUniformUnfolding
+ ? checker.CheckAssumptions(assumptions, softAssumptions)
+ : checker.CheckAssumptions(assumptions);
+ }
+
+ if (ret != Outcome.Correct && ret != Outcome.Errors) {
+ // The query ran out of memory or time, that's it,
+ // we cannot do better. Give up!
+ return ret;
+ }
+
+ if (ret == Outcome.Correct) {
+ // If nothing was made false, then the program is correct
+ if (allTrue) {
+ return ret;
+ }
+
+ // Nothing more can be done with current recursion bound.
+ return Outcome.ReachedBound;
+ }
+
+ Contract.Assert(ret == Outcome.Errors);
+
+ prover.LogComment(";;;;;;;;;;;; Overapprox mode end ;;;;;;;;;;");
+
+ return ret;
+ }
+
+ // A counter for adding new variables
+ static int newVarCnt = 0;
+
+ // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
+ private void DoExpansion(List<int>/*!*/ candidates, VerificationState vState) {
+ Contract.Requires(candidates != null);
+ Contract.Requires(vState.calls != null);
+ Contract.Requires(vState.checker.prover != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
+ vState.expansionCount += candidates.Count;
+
+ var prover = vState.checker.prover;
+ var calls = vState.calls;
+
+ VCExpr exprToPush = VCExpressionGenerator.True;
+ Contract.Assert(exprToPush != null);
+ foreach (int id in candidates) {
+ VCExprNAry expr = calls.id2Candidate[id];
+ Contract.Assert(expr != null);
+ string procName = cce.NonNull(expr.Op as VCExprBoogieFunctionOp).Func.Name;
+ if (!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;
+
+ StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];
+ info.GenerateVC();
+ //Console.WriteLine("Inlining {0}", procName);
+ VCExpr expansion = cce.NonNull(info.vcexpr);
+
+ // Instantiate the "forall" variables
+ Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();
+ Contract.Assert(info.interfaceExprVars.Count == expr.Length);
+ for (int i = 0; i < info.interfaceExprVars.Count; i++) {
+ substForallDict.Add(info.interfaceExprVars[i], expr[i]);
+ }
+ VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+
+ SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(prover.VCExprGen);
+ Contract.Assert(subst != null);
+ expansion = subst.Mutate(expansion, substForall);
+
+ // Instantiate and declare the "exists" variables
+ Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();
+ foreach (VCExprVar v in info.privateExprVars) {
+ Contract.Assert(v != null);
+ string newName = v.Name + "_si_" + newVarCnt.ToString();
+ newVarCnt++;
+ prover.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
+ substExistsDict.Add(v, prover.VCExprGen.Variable(newName, v.Type));
+ }
+ if (CommandLineOptions.Clo.SIBoolControlVC)
+ {
+ // record the mapping for control booleans (for tracing the path later)
+ calls.candiate2block2controlVar[id] = new Dictionary<Block, VCExpr>();
+ foreach (var tup in info.blockToControlVar)
+ {
+ calls.candiate2block2controlVar[id].Add(tup.Key,
+ substExistsDict[tup.Value]);
+ }
+ }
+ if (CommandLineOptions.Clo.ModelViewFile != null) {
+ SaveSubstitution(vState, id, substForallDict, substExistsDict);
+ }
+ VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+
+ subst = new SubstitutingVCExprVisitor(prover.VCExprGen);
+ expansion = subst.Mutate(expansion, substExists);
+
+ if (!calls.currCandidates.Contains(id)) {
+ Console.WriteLine("Don't know what we just expanded");
+ }
+
+ calls.currCandidates.Remove(id);
+
+ // Record the new set of candidates and rename absy labels
+ calls.currInlineCount = id;
+ calls.setCurrProc(procName);
+ expansion = calls.Mutate(expansion, true);
+
+ //expansion = checker.VCExprGen.Eq(calls.id2ControlVar[id], expansion);
+ expansion = prover.VCExprGen.Implies(calls.id2ControlVar[id], expansion);
+ calls.id2VC.Add(id, expansion);
+
+ exprToPush = prover.VCExprGen.And(exprToPush, expansion);
+ }
+ vState.checker.prover.Assert(exprToPush, true);
+ vState.vcSize += SizeComputingVisitor.ComputeSize(exprToPush);
+ }
+
+ private void SaveSubstitution(VerificationState vState, int id,
+ Dictionary<VCExprVar, VCExpr> substForallDict, Dictionary<VCExprVar, VCExpr> substExistsDict) {
+ var prover = vState.checker.prover;
+ var calls = vState.calls;
+ Boogie2VCExprTranslator translator = prover.Context.BoogieExprTranslator;
+ VCExprVar mvStateConstant = translator.LookupVariable(ModelViewInfo.MVState_ConstantDef);
+ substExistsDict.Add(mvStateConstant, prover.VCExprGen.Integer(BigNum.FromInt(id)));
+ Dictionary<VCExprVar, VCExpr> mapping = new Dictionary<VCExprVar, VCExpr>();
+ foreach (var key in substForallDict.Keys)
+ mapping[key] = substForallDict[key];
+ foreach (var key in substExistsDict.Keys)
+ mapping[key] = substExistsDict[key];
+ calls.id2Vars[id] = mapping;
+ }
+
+ // Uniquely identifies a procedure call (the call expr, instance)
+ public class BoogieCallExpr : IEquatable<BoogieCallExpr> {
+ public NAryExpr expr;
+ public int inlineCnt;
+
+ public BoogieCallExpr(NAryExpr expr, int inlineCnt) {
+ this.expr = expr;
+ this.inlineCnt = inlineCnt;
+ }
+
+ public override int GetHashCode() {
+ return expr.GetHashCode() + 131 * inlineCnt.GetHashCode();
+ }
+
+ public override bool Equals(object obj) {
+ BoogieCallExpr that = obj as BoogieCallExpr;
+ return (expr == that.expr && inlineCnt == that.inlineCnt);
+ }
+
+ public bool Equals(BoogieCallExpr that) {
+ return (expr == that.expr && inlineCnt == that.inlineCnt);
+ }
+ }
+
+ // This class is used to traverse VCs and do the following:
+ // -- collect the set of FunctionCall nodes and label them with a unique string
+ // -- Rename all other labels (so that calling this on the same VC results in
+ // VCs with different labels each time)
+ public class FCallHandler : MutatingVCExprVisitor<bool> {
+ Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;
+ public readonly Dictionary<int, Absy>/*!*/ mainLabel2absy;
+ public Dictionary<BoogieCallExpr/*!*/, int>/*!*/ boogieExpr2Id;
+ public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;
+ public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;
+ public Dictionary<int, VCExprVar/*!*/>/*!*/ id2ControlVar;
+ public Dictionary<int, VCExpr> id2VC;
+ public Dictionary<string/*!*/, int>/*!*/ label2Id;
+ // candidate to block to Bool Control variable
+ public Dictionary<int, Dictionary<Block, VCExpr>> candiate2block2controlVar;
+ // Stores the candidate from which this one originated
+ public Dictionary<int, int> candidateParent;
+ // Mapping from candidate Id to the "si_unique_call" id that led to
+ // this candidate. This is useful for getting persistent names for
+ // candidates
+ public Dictionary<int, int> candidate2callId;
+ // A cache for candidate id to its persistent name
+ public Dictionary<int, string> persistentNameCache;
+ // Inverse of the above map
+ public Dictionary<string, int> persistentNameInv;
+ // Used to record candidates recently added
+ public HashSet<int> recentlyAddedCandidates;
+ // Name of main procedure
+ private string mainProcName;
+ // A map from candidate id to the VCExpr that represents its
+ // first argument (used for obtaining concrete values in error trace)
+ public Dictionary<int, VCExpr> argExprMap;
+
+ // map from candidate to summary candidates
+ public Dictionary<int, List<Tuple<VCExprVar, VCExpr>>> summaryCandidates;
+ private Dictionary<string, List<Tuple<VCExprVar, VCExpr>>> summaryTemp;
+ // set of all boolean guards of summaries
+ public HashSet<VCExprVar> allSummaryConst;
+
+ public HashSet<int> forcedCandidates;
+
+ // User info -- to decrease/increase calculation of recursion bound
+ public Dictionary<int, int> recursionIncrement;
+ public Dictionary<string, int> extraRecursion;
+
+ public HashSet<int> currCandidates;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ Contract.Invariant(mainLabel2absy != null);
+ Contract.Invariant(boogieExpr2Id != null);
+ Contract.Invariant(cce.NonNullDictionaryAndValues(id2Candidate));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(id2ControlVar));
+ Contract.Invariant(label2Id != null);
+ }
+
+ // Name of the procedure whose VC we're mutating
+ string currProc;
+
+ // The 0^th candidate is main
+ static int candidateCount = 1;
+ public int currInlineCount;
+
+ public Dictionary<int, Dictionary<VCExprVar, VCExpr>> id2Vars;
+
+ public FCallHandler(VCExpressionGenerator/*!*/ gen,
+ Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,
+ string mainProcName, Dictionary<int, Absy>/*!*/ mainLabel2absy)
+ : base(gen) {
+ Contract.Requires(gen != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ Contract.Requires(mainLabel2absy != null);
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ this.mainProcName = mainProcName;
+ this.mainLabel2absy = mainLabel2absy;
+ id2Candidate = new Dictionary<int, VCExprNAry>();
+ id2ControlVar = new Dictionary<int, VCExprVar>();
+ boogieExpr2Id = new Dictionary<BoogieCallExpr, int>();
+ label2Id = new Dictionary<string, int>();
+ currCandidates = new HashSet<int>();
+ currInlineCount = 0;
+ currProc = null;
+ labelRenamer = new Dictionary<string, int>();
+ labelRenamerInv = new Dictionary<string, string>();
+ candidateParent = new Dictionary<int, int>();
+ //callGraphMapping = new Dictionary<int, int>();
+ recursionIncrement = new Dictionary<int, int>();
+ candidate2callId = new Dictionary<int, int>();
+ persistentNameCache = new Dictionary<int, string>();
+ persistentNameInv = new Dictionary<string, int>();
+ persistentNameCache[0] = "0";
+ persistentNameInv["0"] = 0;
+ recentlyAddedCandidates = new HashSet<int>();
+ argExprMap = new Dictionary<int, VCExpr>();
+ recordExpr2Var = new Dictionary<BoogieCallExpr, VCExpr>();
+ candiate2block2controlVar = new Dictionary<int, Dictionary<Block, VCExpr>>();
+
+ forcedCandidates = new HashSet<int>();
+ extraRecursion = new Dictionary<string, int>();
+
+ id2Vars = new Dictionary<int, Dictionary<VCExprVar, VCExpr>>();
+ summaryCandidates = new Dictionary<int, List<Tuple<VCExprVar, VCExpr>>>();
+ summaryTemp = new Dictionary<string, List<Tuple<VCExprVar, VCExpr>>>();
+ allSummaryConst = new HashSet<VCExprVar>();
+ id2VC = new Dictionary<int, VCExpr>();
+ }
+
+ public void Clear() {
+ currCandidates = new HashSet<int>();
+ }
+
+ // Return the set of all candidates
+ public HashSet<int> getAllCandidates() {
+ var ret = new HashSet<int>(candidateParent.Keys);
+ ret.Add(0);
+ return ret;
+ }
+
+ // Given a candidate "id", let proc(id) be the
+ // procedure corresponding to id. This procedure returns
+ // the number of times proc(id) appears as an ancestor
+ // of id. This is the same as the number of times we've
+ // recursed on proc(id)
+ public int getRecursionBound(int id) {
+ int ret = 1;
+ var str = getProc(id);
+
+ while (candidateParent.ContainsKey(id)) {
+ if (recursionIncrement.ContainsKey(id)) ret += recursionIncrement[id];
+ id = candidateParent[id];
+ if (getProc(id) == str && !forcedCandidates.Contains(id)) ret++;
+ }
+
+ // Usual
+ if (!extraRecursion.ContainsKey(str))
+ return ret;
+
+ // Usual
+ if (ret <= CommandLineOptions.Clo.RecursionBound - 1)
+ return ret;
+
+ // Special
+ if (ret >= CommandLineOptions.Clo.RecursionBound &&
+ ret <= CommandLineOptions.Clo.RecursionBound + extraRecursion[str] - 1)
+ return CommandLineOptions.Clo.RecursionBound - 1;
+
+ // Special
+ return ret - extraRecursion[str];
+ }
+
+ // This procedure returns the stack depth of the candidate
+ // (distance from main)
+ public int getStackDepth(int id)
+ {
+ int ret = 1;
+
+ while (candidateParent.ContainsKey(id))
+ {
+ ret++;
+ id = candidateParent[id];
+ }
+
+ return ret;
+ }
+
+ // Set user-define increment/decrement to recursionBound
+ public void setRecursionIncrement(int id, int incr) {
+ if (recursionIncrement.ContainsKey(id))
+ recursionIncrement[id] = incr;
+ else
+ recursionIncrement.Add(id, incr);
+ }
+
+ // Returns the name of the procedure corresponding to candidate id
+ public string getProc(int id) {
+ if (id == 0) return mainProcName;
+
+ return (id2Candidate[id].Op as VCExprBoogieFunctionOp).Func.Name;
+ }
+
+ // Get a unique id for this candidate (dependent only on the Call
+ // graph of the program). The persistent id is:
+ // 0: for main
+ // a_b_c: where a is the persistent id of parent, and b is the procedure name
+ // and c is the unique call id (if any)
+ public string getPersistentId(int top_id) {
+ if (top_id == 0) return "0";
+ Debug.Assert(candidateParent.ContainsKey(top_id));
+ if (persistentNameCache.ContainsKey(top_id))
+ return persistentNameCache[top_id];
+
+ var parent_id = getPersistentId(candidateParent[top_id]);
+ var call_id = candidate2callId.ContainsKey(top_id) ? candidate2callId[top_id] : -1;
+ var ret = string.Format("{0}_131_{1}_131_{2}", parent_id, getProc(top_id), call_id);
+ persistentNameCache[top_id] = ret;
+ persistentNameInv[ret] = top_id;
+ return ret;
+ }
+
+ public int getCandidateFromGraphNode(string n) {
+ if (!persistentNameInv.ContainsKey(n)) {
+ return -1;
+ }
+ return persistentNameInv[n];
+ }
+
+ private int GetNewId(VCExprNAry vc) {
+ Contract.Requires(vc != null);
+ int id = candidateCount;
+
+ id2Candidate[id] = vc;
+ id2ControlVar[id] = Gen.Variable("si_control_var_bool_" + id.ToString(), Microsoft.Boogie.Type.Bool);
+
+ candidateCount++;
+ currCandidates.Add(id);
+ recentlyAddedCandidates.Add(id);
+
+ return id;
+ }
+
+ private string GetLabel(int id) {
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ string ret = "si_fcall_" + id.ToString();
+ if (!label2Id.ContainsKey(ret))
+ label2Id[ret] = id;
+
+ return ret;
+ }
+
+ public int GetId(string label) {
+ Contract.Requires(label != null);
+ if (!label2Id.ContainsKey(label))
+ return -1;
+ return label2Id[label];
+ }
+
+ Dictionary<string, int> labelRenamer;
+ Dictionary<string, string> labelRenamerInv;
+
+ public string RenameAbsyLabel(string label) {
+ Contract.Requires(label != null);
+ Contract.Requires(label.Length >= 1);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ // Remove the sign from the label
+ string nosign = label.Substring(1);
+ var ret = "si_inline_" + currInlineCount.ToString() + "_" + nosign;
+
+ if (!labelRenamer.ContainsKey(ret)) {
+ var c = labelRenamer.Count + 11; // two digit labels only
+ labelRenamer.Add(ret, c);
+ labelRenamerInv.Add(c.ToString(), ret);
+ }
+ return labelRenamer[ret].ToString();
+ }
+
+ public string ParseRenamedAbsyLabel(string label, int cnt) {
+ Contract.Requires(label != null);
+ if (!labelRenamerInv.ContainsKey(label)) {
+ return null;
+ }
+ var str = labelRenamerInv[label];
+ var prefix = "si_inline_" + cnt.ToString() + "_";
+ if (!str.StartsWith(prefix)) return null;
+ return str.Substring(prefix.Length);
+ }
+
+ public void setCurrProc(string name) {
+ Contract.Requires(name != null);
+ currProc = name;
+ Contract.Assert(implName2StratifiedInliningInfo.ContainsKey(name));
+ }
+
+ public void setCurrProcAsMain() {
+ currProc = "";
+ }
+
+ // Return the formula (candidate IFF false)
+ public VCExpr getFalseExpr(int candidateId) {
+ //return Gen.Eq(VCExpressionGenerator.False, id2ControlVar[candidateId]);
+ return Gen.Not(id2ControlVar[candidateId]);
+ }
+
+ // Return the formula (candidate IFF true)
+ public VCExpr getTrueExpr(int candidateId) {
+ return Gen.Eq(VCExpressionGenerator.True, id2ControlVar[candidateId]);
+ }
+
+ public Dictionary<int, Absy> getLabel2absy() {
+ Contract.Ensures(Contract.Result<Dictionary<int, Absy>>() != null);
+
+ Contract.Assert(currProc != null);
+ if (currProc == "") {
+ return mainLabel2absy;
+ }
+ return cce.NonNull(implName2StratifiedInliningInfo[currProc].label2absy);
+ }
+
+ // Finds labels and changes them:
+ // si_fcall_id: if "id" corresponds to a tracked procedure call, then
+ // si_control_var_candidateId
+ // si_fcall_id: if "id" does not corresponds to a tracked procedure call, then
+ // delete
+ // num: si_inline_num
+ //
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
+ List<VCExpr/*!*/>/*!*/ newSubExprs,
+ // has any of the subexpressions changed?
+ bool changed,
+ bool arg) {
+ //Contract.Requires(originalNode != null);
+ //Contract.Requires(cce.NonNullElements(newSubExprs));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
+ if (lop == null) return ret;
+ if (!(ret is VCExprNAry)) return ret;
+
+ VCExprNAry retnary = (VCExprNAry)ret;
+ Contract.Assert(retnary != null);
+ string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)
+ if (lop.label.Substring(1).StartsWith(prefix)) {
+ int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
+ Dictionary<int, Absy> label2absy = getLabel2absy();
+ Absy cmd = label2absy[id] as Absy;
+ //label2absy.Remove(id);
+
+ Contract.Assert(cmd != null);
+ AssumeCmd acmd = cmd as AssumeCmd;
+ Contract.Assert(acmd != null);
+ NAryExpr naryExpr = acmd.Expr as NAryExpr;
+ Contract.Assert(naryExpr != null);
+
+ string calleeName = naryExpr.Fun.FunctionName;
+
+ VCExprNAry callExpr = retnary[0] as VCExprNAry;
+
+ if (implName2StratifiedInliningInfo.ContainsKey(calleeName)) {
+ Contract.Assert(callExpr != null);
+ int candidateId = GetNewId(callExpr);
+ boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId;
+ candidateParent[candidateId] = currInlineCount;
+ candiate2block2controlVar[candidateId] = new Dictionary<Block, VCExpr>();
+
+ string label = GetLabel(candidateId);
+ var unique_call_id = QKeyValue.FindIntAttribute(acmd.Attributes, "si_unique_call", -1);
+ if (unique_call_id != -1)
+ candidate2callId[candidateId] = unique_call_id;
+
+ //return Gen.LabelPos(label, callExpr);
+ return Gen.LabelPos(label, id2ControlVar[candidateId]);
+ }
+ else if (calleeName.StartsWith(recordProcName)) {
+ Contract.Assert(callExpr != null);
+ Debug.Assert(callExpr.Length == 1);
+ Debug.Assert(callExpr[0] != null);
+ recordExpr2Var[new BoogieCallExpr(naryExpr, currInlineCount)] = callExpr[0];
+ return callExpr;
+ }
+ else {
+ // callExpr can be null; this happens when the FunctionCall was on a
+ // pure function (not procedure) and the function got inlined
+ return retnary[0];
+ }
+ }
+
+ // Else, rename label
+ string newLabel = RenameAbsyLabel(lop.label);
+ if (lop.pos) {
+ return Gen.LabelPos(newLabel, retnary[0]);
+ }
+ else {
+ return Gen.LabelNeg(newLabel, retnary[0]);
+ }
+
+ }
+
+ // Upgrades summaryTemp to summaryCandidates by matching ensure clauses with
+ // the appropriate candidate they came from
+ public void matchSummaries() {
+ var id2Set = new Dictionary<string, List<Tuple<int, HashSet<VCExprVar>>>>();
+ foreach (var id in recentlyAddedCandidates) {
+ var collect = new CollectVCVars();
+ var proc = getProc(id);
+ if (!id2Set.ContainsKey(proc)) id2Set.Add(proc, new List<Tuple<int, HashSet<VCExprVar>>>());
+ id2Set[proc].Add(Tuple.Create(id, collect.Collect(id2Candidate[id], true)));
+ }
+
+ foreach (var kvp in summaryTemp) {
+ Contract.Assert(id2Set.ContainsKey(kvp.Key));
+ var ls = id2Set[kvp.Key];
+ foreach (var tup in kvp.Value) {
+ var collect = new CollectVCVars();
+ var s1 = collect.Collect(tup.Item2, true);
+ var found = false;
+ foreach (var t in ls) {
+ var s2 = t.Item2;
+ if (s1.IsSubsetOf(s2)) {
+ if (!summaryCandidates.ContainsKey(t.Item1))
+ summaryCandidates.Add(t.Item1, new List<Tuple<VCExprVar, VCExpr>>());
+ summaryCandidates[t.Item1].Add(tup);
+ allSummaryConst.Add(tup.Item1);
+ found = true;
+ break;
+ }
+ }
+ Contract.Assert(found);
+ }
+ }
+ summaryTemp.Clear();
+ }
+
+ public IEnumerable<int> getInlinedCandidates() {
+ return candidateParent.Keys.Except(currCandidates).Union(new int[] { 0 });
+ }
+
+ } // end FCallHandler
+
+ // Collects the set of all VCExprVar in a given VCExpr
+ class CollectVCVars : CollectingVCExprVisitor<HashSet<VCExprVar>, bool> {
+ public override HashSet<VCExprVar> Visit(VCExprVar node, bool arg) {
+ var ret = new HashSet<VCExprVar>();
+ ret.Add(node);
+ return ret;
+ }
+
+ protected override HashSet<VCExprVar> CombineResults(List<HashSet<VCExprVar>> results, bool arg) {
+ var ret = new HashSet<VCExprVar>();
+ results.Iter(s => ret.UnionWith(s));
+ return ret;
+ }
+ }
+
+ public class FCallInliner : MutatingVCExprVisitor<bool> {
+ public Dictionary<int, VCExpr/*!*/>/*!*/ subst;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullDictionaryAndValues(subst));
+ }
+
+
+ public FCallInliner(VCExpressionGenerator gen)
+ : base(gen) {
+ Contract.Requires(gen != null);
+ subst = new Dictionary<int, VCExpr>();
+ }
+
+ public void Clear() {
+ subst = new Dictionary<int, VCExpr>();
+ }
+
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
+ List<VCExpr/*!*/>/*!*/ newSubExprs,
+ // has any of the subexpressions changed?
+ bool changed,
+ bool arg) {
+ //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
+ if (lop == null) return ret;
+ if (!(ret is VCExprNAry)) return ret;
+
+ string prefix = "si_fcall_"; // from FCallHandler::GetLabel
+ if (lop.label.Substring(1).StartsWith(prefix)) {
+ int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
+ if (subst.ContainsKey(id)) {
+ return subst[id];
+ }
+ }
+ return ret;
+ }
+
+ } // end FCallInliner
+
+
+
+ public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler {
+ Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
+ ProverInterface theoremProver;
+ VerifierCallback callback;
+ FCallHandler calls;
+ StratifiedInliningInfo mainInfo;
+ StratifiedVC mainVC;
+
+ public bool underapproximationMode;
+ public List<int> candidatesToExpand;
+ public List<StratifiedCallSite> callSitesToExpand;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(candidatesToExpand != null);
+ Contract.Invariant(mainInfo != null);
+ Contract.Invariant(callback != null);
+ Contract.Invariant(theoremProver != null);
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ }
+
+
+ public StratifiedInliningErrorReporter(Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo,
+ ProverInterface theoremProver, VerifierCallback callback,
+ StratifiedInliningInfo mainInfo) {
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ Contract.Requires(theoremProver != null);
+ Contract.Requires(callback != null);
+ Contract.Requires(mainInfo != null);
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ this.theoremProver = theoremProver;
+ this.callback = callback;
+ this.mainInfo = mainInfo;
+ this.underapproximationMode = false;
+ this.calls = null;
+ this.candidatesToExpand = new List<int>();
+ }
+
+ public StratifiedInliningErrorReporter(Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo,
+ ProverInterface theoremProver, VerifierCallback callback,
+ StratifiedVC mainVC) {
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ Contract.Requires(theoremProver != null);
+ Contract.Requires(callback != null);
+ Contract.Requires(mainVC != null);
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ this.theoremProver = theoremProver;
+ this.callback = callback;
+ this.mainVC = mainVC;
+ this.underapproximationMode = false;
+ this.candidatesToExpand = new List<int>();
+ }
+
+ public void SetCandidateHandler(FCallHandler calls) {
+ Contract.Requires(calls != null);
+ this.calls = calls;
+ }
+
+ List<Tuple<int, int>> orderedStateIds;
+
+ private Model.Element GetModelValue(Model m, Variable v, int candidateId) {
+ // first, get the unique name
+ string uniqueName;
+
+ VCExprVar vvar = theoremProver.Context.BoogieExprTranslator.TryLookupVariable(v);
+ if (vvar == null) {
+ uniqueName = v.Name;
+ }
+ else {
+ if (candidateId != 0) {
+ Dictionary<VCExprVar, VCExpr> mapping = calls.id2Vars[candidateId];
+ if (mapping.ContainsKey(vvar)) {
+ VCExpr e = mapping[vvar];
+ if (e is VCExprLiteral) {
+ VCExprLiteral lit = (VCExprLiteral)e;
+ return m.MkElement(lit.ToString());
+ }
+ vvar = (VCExprVar)mapping[vvar];
+ }
+ }
+ uniqueName = theoremProver.Context.Lookup(vvar);
+ }
+
+ var f = m.TryGetFunc(uniqueName);
+ if (f == null)
+ return m.MkFunc("@undefined", 0).GetConstant();
+ return f.GetConstant();
+ }
+
+ public readonly static int CALL = -1;
+ public readonly static int RETURN = -2;
+
+ public void PrintModel(Model model) {
+ var filename = CommandLineOptions.Clo.ModelViewFile;
+ if (model == null || filename == null) return;
+
+ if (filename == "-") {
+ model.Write(Console.Out);
+ Console.Out.Flush();
+ }
+ else {
+ using (var wr = new StreamWriter(filename, !Counterexample.firstModelFile)) {
+ Counterexample.firstModelFile = false;
+ model.Write(wr);
+ }
+ }
+ }
+
+ private void GetModelWithStates(Model m) {
+ if (m == null) return;
+ var mvInfo = mainInfo.mvInfo;
+ var mvstates = m.TryGetFunc("$mv_state");
+ if (mvstates == null)
+ return;
+
+ Contract.Assert(mvstates.Arity == 2);
+
+ foreach (Variable v in mvInfo.AllVariables) {
+ m.InitialState.AddBinding(v.Name, GetModelValue(m, v, 0));
+ }
+
+ int lastCandidate = 0;
+ int lastCapturePoint = CALL;
+ for (int i = 0; i < this.orderedStateIds.Count; ++i) {
+ var s = orderedStateIds[i];
+ int candidate = s.Item1;
+ int capturePoint = s.Item2;
+ string implName = calls.getProc(candidate);
+ ModelViewInfo info = candidate == 0 ? mvInfo : implName2StratifiedInliningInfo[implName].mvInfo;
+
+ if (capturePoint == CALL || capturePoint == RETURN) {
+ lastCandidate = candidate;
+ lastCapturePoint = capturePoint;
+ continue;
+ }
+
+ Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);
+ VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];
+ var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)
+ ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary<Variable, Expr>();
+ var cs = m.MkState(map.Description);
+
+ foreach (Variable v in info.AllVariables) {
+ var e = (Expr)map.IncarnationMap[v];
+
+ if (e == null) {
+ if (lastCapturePoint == CALL || lastCapturePoint == RETURN) {
+ cs.AddBinding(v.Name, GetModelValue(m, v, candidate));
+ }
+ continue;
+ }
+
+ if (lastCapturePoint != CALL && lastCapturePoint != RETURN && prevInc[v] == e) continue; // skip unchanged variables
+
+ Model.Element elt;
+ if (e is IdentifierExpr) {
+ IdentifierExpr ide = (IdentifierExpr)e;
+ elt = GetModelValue(m, ide.Decl, candidate);
+ }
+ else if (e is LiteralExpr) {
+ LiteralExpr lit = (LiteralExpr)e;
+ elt = m.MkElement(lit.Val.ToString());
+ }
+ else {
+ Contract.Assume(false);
+ elt = m.MkFunc(e.ToString(), 0).GetConstant();
+ }
+ cs.AddBinding(v.Name, elt);
+ }
+
+ lastCandidate = candidate;
+ lastCapturePoint = capturePoint;
+ }
+
+ return;
+ }
+
+ public override void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null)
+ {
+ //Contract.Requires(message != null);
+ }
+
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) {
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
+ model.Write(ErrorReporter.ModelWriter);
+ ErrorReporter.ModelWriter.Flush();
+ }
+
+ // Timeout?
+ if (proverOutcome != ProverInterface.Outcome.Invalid)
+ return;
+
+ candidatesToExpand = new List<int>();
+ orderedStateIds = new List<Tuple<int, int>>();
+ var cex = GenerateTrace(labels, model, 0, mainInfo.impl, mainInfo.mvInfo);
+
+ if (underapproximationMode && cex != null) {
+ //Debug.Assert(candidatesToExpand.All(calls.isSkipped));
+ GetModelWithStates(model);
+ callback.OnCounterexample(cex, null);
+ this.PrintModel(model);
+ }
+ }
+
+ private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,
+ int candidateId, Implementation procImpl, ModelViewInfo mvInfo) {
+ Contract.Requires(cce.NonNullElements(labels));
+ Contract.Requires(procImpl != null);
+
+ Hashtable traceNodes = new Hashtable();
+
+ if (!CommandLineOptions.Clo.SIBoolControlVC)
+ {
+ foreach (string s in labels)
+ {
+ Contract.Assert(s != null);
+ var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId);
+
+ if (absylabel == null) continue;
+
+ Absy absy;
+
+ if (candidateId == 0)
+ {
+ absy = Label2Absy(absylabel);
+ }
+ else
+ {
+ absy = Label2Absy(procImpl.Name, absylabel);
+ }
+
+ if (traceNodes.ContainsKey(absy))
+ System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");
+ else
+ traceNodes.Add(absy, null);
+ }
+ }
+ else
+ {
+ Debug.Assert(CommandLineOptions.Clo.UseProverEvaluate, "Must use prover evaluate option with boolControlVC");
+ var block = procImpl.Blocks[0];
+ traceNodes.Add(block, null);
+ while (true)
+ {
+ var gc = block.TransferCmd as GotoCmd;
+ if (gc == null) break;
+ Block next = null;
+ foreach (var succ in gc.labelTargets)
+ {
+ var succtaken = (bool) theoremProver.Evaluate(calls.candiate2block2controlVar[candidateId][succ]);
+ if (succtaken)
+ {
+ next = succ;
+ traceNodes.Add(succ, null);
+ break;
+ }
+ }
+ Debug.Assert(next != null, "Must find a successor");
+ Debug.Assert(traceNodes.ContainsKey(next), "CFG cannot be cyclic");
+ block = next;
+ }
+ }
+
+ List<Block> trace = new List<Block>();
+ Block entryBlock = cce.NonNull(procImpl.Blocks[0]);
+ Contract.Assert(entryBlock != null);
+ Contract.Assert(traceNodes.Contains(entryBlock));
+ trace.Add(entryBlock);
+
+ var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
+ Counterexample newCounterexample = GenerateTraceRec(labels, errModel, mvInfo, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples);
+
+ return newCounterexample;
+ }
+
+ private Counterexample GenerateTraceRec(
+ IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,
+ int candidateId,
+ Block/*!*/ b, Hashtable/*!*/ traceNodes, List<Block>/*!*/ trace,
+ Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {
+ Contract.Requires(cce.NonNullElements(labels));
+ Contract.Requires(b != null);
+ Contract.Requires(traceNodes != null);
+ Contract.Requires(trace != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
+ // After translation, all potential errors come from asserts.
+ while (true) {
+ List<Cmd> cmds = b.Cmds;
+ TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
+ for (int i = 0; i < cmds.Count; i++) {
+ Cmd cmd = cce.NonNull(cmds[i]);
+
+ // Skip if 'cmd' not contained in the trace or not an assert
+ if ((cmd is AssertCmd && traceNodes.Contains(cmd)) ||
+ (cmd is AssumeCmd && QKeyValue.FindBoolAttribute((cmd as AssumeCmd).Attributes, "exitAssert")))
+ {
+ var acmd = cmd as AssertCmd;
+ if (acmd == null) { acmd = new AssertCmd(Token.NoToken, Expr.True); }
+ Counterexample newCounterexample = AssertCmdToCounterexample(acmd, transferCmd, trace, errModel, mvInfo, theoremProver.Context);
+ newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
+ return newCounterexample;
+ }
+
+ // Counterexample generation for inlined procedures
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ if (assumeCmd == null)
+ continue;
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null)
+ continue;
+ string calleeName = naryExpr.Fun.FunctionName;
+ Contract.Assert(calleeName != null);
+
+ BinaryOperator binOp = naryExpr.Fun as BinaryOperator;
+ if (binOp != null && binOp.Op == BinaryOperator.Opcode.And) {
+ Expr expr = naryExpr.Args[0];
+ NAryExpr mvStateExpr = expr as NAryExpr;
+ if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == ModelViewInfo.MVState_FunctionDef.Name) {
+ LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr;
+ orderedStateIds.Add(new Tuple<int, int>(candidateId, x.asBigNum.ToInt));
+ }
+ }
+
+ if (calleeName.StartsWith(recordProcName) && (errModel != null || CommandLineOptions.Clo.UseProverEvaluate)) {
+ var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
+
+ // Record concrete value of the argument to this procedure
+ var args = new List<object>();
+ if (errModel == null && CommandLineOptions.Clo.UseProverEvaluate)
+ {
+ object exprv;
+ try
+ {
+ exprv = theoremProver.Evaluate(expr);
+ }
+ catch (Exception)
+ {
+ exprv = null;
+ }
+ args.Add(exprv);
+ }
+ else
+ {
+ if (expr is VCExprIntLit)
+ {
+ args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));
+ }
+ else if (expr == VCExpressionGenerator.True)
+ {
+ args.Add(errModel.MkElement("true"));
+ }
+ else if (expr == VCExpressionGenerator.False)
+ {
+ args.Add(errModel.MkElement("false"));
+ }
+ else if (expr is VCExprVar)
+ {
+ var idExpr = expr as VCExprVar;
+ string name = theoremProver.Context.Lookup(idExpr);
+ Contract.Assert(name != null);
+ Model.Func f = errModel.TryGetFunc(name);
+ if (f != null)
+ {
+ args.Add(f.GetConstant());
+ }
+ }
+ else
+ {
+ Contract.Assert(false);
+ }
+ }
+ calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =
+ new CalleeCounterexampleInfo(null, args);
+ continue;
+ }
+
+ if (!implName2StratifiedInliningInfo.ContainsKey(calleeName))
+ continue;
+
+ Contract.Assert(calls != null);
+
+ int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)];
+
+ if (calls.currCandidates.Contains(calleeId)) {
+ candidatesToExpand.Add(calleeId);
+ }
+ else {
+ orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));
+ var calleeInfo = implName2StratifiedInliningInfo[calleeName];
+ calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =
+ new CalleeCounterexampleInfo(GenerateTrace(labels, errModel, calleeId, calleeInfo.impl, calleeInfo.mvInfo), new List<object>());
+ orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));
+ }
+ }
+
+ GotoCmd gotoCmd = transferCmd as GotoCmd;
+ if (gotoCmd != null) {
+ b = null;
+ foreach (Block bb in cce.NonNull(gotoCmd.labelTargets)) {
+ Contract.Assert(bb != null);
+ if (traceNodes.Contains(bb)) {
+ trace.Add(bb);
+ b = bb;
+ break;
+ }
+ }
+ if (b != null) continue;
+ }
+ return null;
+ }
+ }
+
+ public override Absy Label2Absy(string label) {
+ //Contract.Requires(label != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+
+ int id = int.Parse(label);
+ Contract.Assert(calls != null);
+ return cce.NonNull((Absy)calls.mainLabel2absy[id]);
+ }
+
+ public Absy Label2Absy(string procName, string label) {
+ Contract.Requires(label != null);
+ Contract.Requires(procName != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+
+ int id = int.Parse(label);
+ Dictionary<int, Absy> l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;
+ return cce.NonNull((Absy)l2a[id]);
+ }
+
+ public override void OnProverWarning(string msg) {
+ //Contract.Requires(msg != null);
+ callback.OnWarning(msg);
+ }
+ }
+
+ } // class StratifiedVCGen
+
+ public class EmptyErrorHandler : ProverInterface.ErrorHandler
+ {
+ public override void OnModel(IList<string> labels, Model model, ProverInterface.Outcome proverOutcome)
+ { }
+ }
+
+ public class InvalidProgramForSecureVc : Exception
+ {
+ public InvalidProgramForSecureVc(string msg) :
+ base(msg) { }
+ }
+
+ public class SecureVCGen : VCGen
+ {
+ // Z3
+ ProverInterface prover;
+ // Handler
+ ErrorReporter handler;
+ // dump file
+ public static TokenTextWriter outfile = null;
+
+
+ public SecureVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, logFilePath, appendLogFile, checkers)
+ {
+ prover = null;
+ handler = null;
+ if (CommandLineOptions.Clo.SecureVcGen != "" && outfile == null)
+ {
+ outfile = new TokenTextWriter(new StreamWriter(CommandLineOptions.Clo.SecureVcGen));
+ CommandLineOptions.Clo.PrintInstrumented = true;
+ var implsToVerify = new HashSet<string>(
+ program.TopLevelDeclarations.OfType<Implementation>()
+ .Where(impl => !impl.SkipVerification)
+ .Select(impl => impl.Name));
+
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ if (decl is NamedDeclaration && implsToVerify.Contains((decl as NamedDeclaration).Name))
+ continue;
+ decl.Emit(outfile, 0);
+ }
+ }
+ }
+
+ private Block GetExitBlock(Implementation impl)
+ {
+ var exitblocks = impl.Blocks.Where(blk => blk.TransferCmd is ReturnCmd);
+ if (exitblocks.Count() == 1)
+ return exitblocks.First();
+ // create a new exit block
+ var eb = new Block(Token.NoToken, "SVCeb", new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ foreach (var b in exitblocks)
+ {
+ b.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { eb });
+ }
+ impl.Blocks.Add(eb);
+ return eb;
+ }
+
+ //static int LocalVarCounter = 0;
+ private LocalVariable GetNewLocal(Variable v, string suffix)
+ {
+ return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken,
+ string.Format("svc_{0}_{1}", v.Name, suffix), v.TypedIdent.Type));
+ }
+
+ private void GenVc(Implementation impl, VerifierCallback collector)
+ {
+ if (impl.Proc.Requires.Any())
+ throw new InvalidProgramForSecureVc("SecureVc: Requires not supported");
+ if(impl.LocVars.Any(v => isVisible(v)))
+ throw new InvalidProgramForSecureVc("SecureVc: Visible Local variables not allowed");
+
+ // Desugar procedure calls
+ DesugarCalls(impl);
+
+ // Gather spec, remove existing ensures
+ var secureAsserts = new List<AssertCmd>();
+ var logicalAsserts = new List<AssertCmd>();
+
+ foreach (var ens in impl.Proc.Ensures)
+ {
+ if(ens.Free)
+ throw new InvalidProgramForSecureVc("SecureVc: Free Ensures not supported");
+ var dd = new Duplicator();
+ secureAsserts.Add(new AssertCmd(ens.tok, Expr.Not(ens.Condition)));
+ logicalAsserts.Add(dd.VisitAssertCmd(new AssertCmd(ens.tok, ens.Condition)) as AssertCmd);
+ }
+ impl.Proc.Ensures.Clear();
+
+ // Make a copy of the impl
+ var dup = new Duplicator();
+ var implDup = dup.VisitImplementation(impl);
+
+ // Get exit block
+ var eb = GetExitBlock(impl);
+
+ // Create two blocks: one for secureAsserts, one for logical asserts
+ var ebSecure = new Block(Token.NoToken, "svc_secure_asserts", new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ var ebLogical = new Block(Token.NoToken, "svc_logical_asserts", new List<Cmd>(), new ReturnCmd(Token.NoToken));
+
+ eb.TransferCmd = new GotoCmd(eb.TransferCmd.tok, new List<Block> { ebSecure, ebLogical });
+ impl.Blocks.Add(ebSecure);
+ impl.Blocks.Add(ebLogical);
+
+ // Rename spec, while create copies of the hidden variables
+ var substOld = new Dictionary<Variable, Expr>();
+ var substVarSpec = new Dictionary<Variable, Expr>();
+ var substVarPath = new Dictionary<Variable, Expr>();
+ foreach (var g in program.GlobalVariables)
+ {
+ if (!isHidden(g)) continue;
+ var lv = GetNewLocal(g, "In");
+ impl.LocVars.Add(lv);
+ substOld.Add(g, Expr.Ident(lv));
+ }
+
+ for(int i = 0; i < impl.InParams.Count; i++)
+ {
+ var v = impl.Proc.InParams[i];
+ if (!isHidden(v))
+ {
+ substVarSpec.Add(impl.Proc.InParams[i], Expr.Ident(impl.InParams[i]));
+ continue;
+ }
+
+ var lv = GetNewLocal(v, "In");
+ impl.LocVars.Add(lv);
+ substVarSpec.Add(v, Expr.Ident(lv));
+ substVarPath.Add(impl.InParams[i], Expr.Ident(lv));
+ }
+
+ for (int i = 0; i < impl.OutParams.Count; i++)
+ {
+ var v = impl.Proc.OutParams[i];
+ if (!isHidden(v))
+ {
+ substVarSpec.Add(impl.Proc.OutParams[i], Expr.Ident(impl.OutParams[i]));
+ continue;
+ }
+
+ var lv = GetNewLocal(v, "Out");
+ impl.LocVars.Add(lv);
+ substVarSpec.Add(v, Expr.Ident(lv));
+ substVarPath.Add(impl.OutParams[i], Expr.Ident(lv));
+ }
+
+ foreach (var g in program.GlobalVariables)
+ {
+ if (!isHidden(g)) continue;
+ if (!impl.Proc.Modifies.Any(ie => ie.Name == g.Name)) continue;
+
+ var lv = GetNewLocal(g, "Out");
+ impl.LocVars.Add(lv);
+ substVarSpec.Add(g, Expr.Ident(lv));
+ substVarPath.Add(g, Expr.Ident(lv));
+ }
+
+ secureAsserts = secureAsserts.ConvertAll(ac =>
+ Substituter.ApplyReplacingOldExprs(
+ Substituter.SubstitutionFromHashtable(substVarSpec),
+ Substituter.SubstitutionFromHashtable(substOld),
+ ac) as AssertCmd);
+
+ var substVarProcToImpl = new Dictionary<Variable, Expr>();
+ for (int i = 0; i < impl.InParams.Count; i++)
+ substVarProcToImpl.Add(impl.Proc.InParams[i], Expr.Ident(impl.InParams[i]));
+
+ for (int i = 0; i < impl.OutParams.Count; i++)
+ substVarProcToImpl.Add(impl.Proc.OutParams[i], Expr.Ident(impl.OutParams[i]));
+
+ logicalAsserts = logicalAsserts.ConvertAll(ac =>
+ Substituter.Apply(Substituter.SubstitutionFromHashtable(substVarProcToImpl), ac)
+ as AssertCmd);
+
+ // Paths
+ foreach (var path in GetAllPaths(implDup))
+ {
+ var wp = ComputeWP(implDup, path);
+
+ // replace hidden variables to match those used in the spec
+ wp = Substituter.ApplyReplacingOldExprs(
+ Substituter.SubstitutionFromHashtable(substVarPath),
+ Substituter.SubstitutionFromHashtable(substOld),
+ wp);
+
+ ebSecure.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(wp)));
+ }
+
+ ebSecure.Cmds.AddRange(secureAsserts);
+ ebLogical.Cmds.AddRange(logicalAsserts);
+
+ if (outfile != null)
+ {
+ impl.Proc.Emit(outfile, 0);
+ impl.Emit(outfile, 0);
+ }
+
+ ModelViewInfo mvInfo;
+ ConvertCFG2DAG(impl);
+ var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
+
+ var gen = prover.VCExprGen;
+ var exprGen = prover.Context.ExprGen;
+ var translator = prover.Context.BoogieExprTranslator;
+
+ var label2absy = new Dictionary<int, Absy>();
+ VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, prover.Context);
+ translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
+ var implVc = gen.Not(GenerateVCAux(impl, null, label2absy, prover.Context));
+
+ handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, prover.Context, program);
+
+ prover.Assert(implVc, true);
+ }
+
+ Expr ComputeWP(Implementation impl, List<Cmd> path)
+ {
+ Expr expr = Expr.True;
+
+ // create constants for out varibles
+ var subst = new Dictionary<Variable, Expr>();
+ foreach (var g in impl.Proc.Modifies)
+ {
+ var c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,
+ "svc_out_const_" + g.Name, g.Decl.TypedIdent.Type));
+ subst.Add(c, g);
+ expr = Expr.And(expr, Expr.Eq(Expr.Ident(c), g));
+ }
+
+ foreach (var v in impl.OutParams)
+ {
+ var c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,
+ "svc_out_const_" + v.Name, v.TypedIdent.Type));
+ subst.Add(c, Expr.Ident(v));
+ expr = Expr.And(expr, Expr.Eq(Expr.Ident(c), Expr.Ident(v)));
+ }
+
+ // we need this technicality
+ var subst1 = new Dictionary<Variable, Expr>();
+ foreach (var g in program.GlobalVariables)
+ {
+ subst1.Add(g, new OldExpr(Token.NoToken, Expr.Ident(g)));
+ }
+
+ // Implicitly close with havoc of all the locals and OutParams
+ path.Insert(0, new HavocCmd(Token.NoToken, new List<IdentifierExpr>(
+ impl.LocVars.Select(v => Expr.Ident(v)).Concat(
+ impl.OutParams.Select(v => Expr.Ident(v))))));
+
+ for (int i = path.Count - 1; i >= 0; i--)
+ {
+ var cmd = path[i];
+ if (cmd is AssumeCmd)
+ {
+ expr = Expr.And(expr, (cmd as AssumeCmd).Expr);
+ }
+ else if (cmd is AssignCmd)
+ {
+ var h = new Dictionary<Variable, Expr>();
+ var acmd = cmd as AssignCmd;
+ for (int j = 0; j < acmd.Lhss.Count; j++)
+ {
+ h.Add(acmd.Lhss[j].DeepAssignedVariable, acmd.Rhss[j]);
+ }
+ var s = Substituter.SubstitutionFromHashtable(h);
+ expr = Substituter.Apply(s, expr);
+ }
+ else if (cmd is HavocCmd)
+ {
+ var h = new Dictionary<Variable, Expr>();
+ var formals = new List<Variable>();
+
+ var vc = new VariableCollector();
+ vc.VisitExpr(expr);
+
+ foreach (var ie in (cmd as HavocCmd).Vars)
+ {
+ if (!vc.usedVars.Contains(ie.Decl)) continue;
+ var f = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,
+ ie.Decl.Name + "_formal", ie.Decl.TypedIdent.Type));
+ h.Add(ie.Decl, Expr.Ident(f));
+ formals.Add(f);
+ }
+ if (!formals.Any())
+ continue;
+ var s = Substituter.SubstitutionFromHashtable(h);
+ expr = Substituter.Apply(s, expr);
+ expr = new ExistsExpr(Token.NoToken, formals, expr);
+ }
+ else
+ {
+ throw new InvalidProgramForSecureVc(string.Format("Unhandled cmd: {0}", cmd));
+ }
+ }
+
+ // Implicitly close with havoc of all the locals and OutParams
+
+
+
+ expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst1), expr);
+ expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst),
+ Substituter.SubstitutionFromHashtable(new Dictionary<Variable,Expr>()), expr);
+ expr.Typecheck(new TypecheckingContext(null));
+ return expr;
+ }
+
+ // Generate all paths in the impl
+ IEnumerable<List<Cmd>> GetAllPaths(Implementation impl)
+ {
+ var stk = new Stack<Tuple<Block, int>>();
+ stk.Push(Tuple.Create(impl.Blocks[0], 0));
+
+ while (stk.Any())
+ {
+ var tup = stk.Peek();
+ if (tup.Item1.TransferCmd is ReturnCmd)
+ {
+ var ret = new List<Cmd>();
+ var ls = stk.ToList();
+ ls.Iter(t => ret.AddRange(t.Item1.Cmds));
+ yield return ret;
+
+ stk.Pop();
+ continue;
+ }
+
+ stk.Pop();
+
+ var gc = tup.Item1.TransferCmd as GotoCmd;
+ if (gc.labelTargets.Count <= tup.Item2)
+ continue;
+
+ stk.Push(Tuple.Create(tup.Item1, tup.Item2 + 1));
+ stk.Push(Tuple.Create(gc.labelTargets[tup.Item2], 0));
+ }
+ yield break;
+ }
+
+ bool isHidden(Variable v)
+ {
+ return QKeyValue.FindBoolAttribute(v.Attributes, "hidden");
+ }
+
+ bool isVisible(Variable v)
+ {
+ return !isHidden(v);
+ }
+
+ public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback)
+ {
+ Debug.Assert(this.program == program);
+
+ // Record current time
+ var startTime = DateTime.UtcNow;
+
+ CommandLineOptions.Clo.ProverCCLimit = 1;
+ prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
+
+ // Flush any axioms that came with the program before we start SI on this implementation
+ prover.AssertAxioms();
+
+ GenVc(impl, callback);
+
+ prover.Check();
+ var outcome = prover.CheckOutcomeCore(handler);
+ //var outcome = ProverInterface.Outcome.Valid;
+
+ prover.Close();
+
+
+
+ //Console.WriteLine("Answer = {0}", outcome);
+
+ return ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+ }
+ }
+
+} // namespace VC