diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 7 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 812 | ||||
| -rw-r--r-- | Test/stratifiedinline/runtest.bat | 20 |
4 files changed, 12 insertions, 829 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index d9213c47..f2148158 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -559,7 +559,6 @@ namespace Microsoft.Boogie { public Inlining ProcedureInlining = Inlining.Assume;
public bool PrintInlined = false;
public bool ExtractLoops = false;
- public int ProcedureCopyBound = 0;
public int StratifiedInlining = 0;
public int StratifiedInliningOption = 0;
public bool StratifiedInliningWithoutModels = false; // disable model generation for SI
@@ -976,12 +975,6 @@ namespace Microsoft.Boogie { }
return true;
- case "procCopyBound":
- if (ps.ConfirmArgumentCount(1)) {
- ProcedureCopyBound = Int32.Parse(args[ps.i]);
- }
- return true;
-
case "stratifiedInline":
if (ps.ConfirmArgumentCount(1)) {
switch (args[ps.i]) {
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 014af458..48791385 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -85,7 +85,7 @@ namespace Microsoft.Boogie.SMTLib {
currentLogFile = OpenOutputFile("");
}
- if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.ContractInfer)
+ if (CommandLineOptions.Clo.ContractInfer)
{
SendThisVC("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 3bbe92a1..18ff4c87 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -115,7 +115,6 @@ namespace VC public Function function;
public Variable controlFlowVariable;
public List<Variable> interfaceVars;
- public List<List<Variable>> interfaceVarCopies;
public Expr assertExpr;
public VCExpr vcexpr;
public List<VCExprVar> privateVars;
@@ -199,16 +198,6 @@ namespace VC this.function = new Function(Token.NoToken, proc.Name, functionInterfaceVars, returnVar);
ctxt.DeclareFunction(this.function, "");
- interfaceVarCopies = new List<List<Variable>>();
- int temp = 0;
- for (int i = 0; i < CommandLineOptions.Clo.ProcedureCopyBound; i++) {
- interfaceVarCopies.Add(new List<Variable>());
- foreach (Variable v in interfaceVars) {
- Constant constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type));
- interfaceVarCopies[i].Add(constant);
- }
- }
-
inline_cnt = 0;
privateVars = new List<VCExprVar>();
interfaceExprVars = new List<VCExprVar>();
@@ -362,10 +351,6 @@ namespace VC info.initialized = true;
}
- public Dictionary<string, List<VCExprVar>> interfaceVarCopies;
- public Dictionary<string, List<VCExprVar>> privateVarCopies;
- Dictionary<string, VCExpr> procVcCopies;
-
public struct CallSite {
public string callerName;
public string calleeName;
@@ -380,52 +365,6 @@ namespace VC }
};
- static public int callSiteConstantCount = 0;
- Dictionary<string, List<CallSite>> calleeToCallSites;
- Dictionary<string, List<CallSite>> callerToCallSites;
-
- private void CreateProcedureCopies(Implementation impl, Program program, ApiChecker checker, VCExpr vcMain) {
- interfaceVarCopies = new Dictionary<string, List<VCExprVar>>();
- privateVarCopies = new Dictionary<string, List<VCExprVar>>();
- procVcCopies = new Dictionary<string, VCExpr>();
- calleeToCallSites = new Dictionary<string, List<CallSite>>();
- callerToCallSites = new Dictionary<string, List<CallSite>>();
-
- interfaceVarCopies[impl.Name] = new List<VCExprVar>();
- privateVarCopies[impl.Name] = new List<VCExprVar>();
- calleeToCallSites[impl.Name] = new List<CallSite>();
- callerToCallSites[impl.Name] = new List<CallSite>();
- foreach (var info in implName2StratifiedInliningInfo.Values) {
- Contract.Assert(info != null);
- interfaceVarCopies[info.impl.Name] = new List<VCExprVar>();
- privateVarCopies[info.impl.Name] = new List<VCExprVar>();
- calleeToCallSites[info.impl.Name] = new List<CallSite>();
- callerToCallSites[info.impl.Name] = new List<CallSite>();
- CreateProcedureCopy(info, checker);
- }
-
- BoundingVCMutator bm = new BoundingVCMutator(checker, impl.Name, interfaceVarCopies, calleeToCallSites, callerToCallSites);
- procVcCopies[impl.Name] = bm.Mutate(vcMain, true);
- foreach (var key in implName2StratifiedInliningInfo.Keys) {
- bm = new BoundingVCMutator(checker, key, interfaceVarCopies, calleeToCallSites, callerToCallSites);
- procVcCopies[key] = bm.Mutate(procVcCopies[key], true);
- }
- }
-
- // Return i if (prefix::i) is in labels
- public static int pcbFindLabel(IList<string> labels, string prefix)
- {
- foreach (var s in labels)
- {
- if (s.StartsWith(prefix))
- {
- return Int32.Parse(s.Substring(prefix.Length));
- }
- }
- Contract.Assert(false);
- return -1;
- }
-
public class SummaryComputation
{
// The verification state
@@ -667,124 +606,12 @@ namespace VC ret.Add(root);
return ret;
}
-
- }
-
- public class BoundingVCMutator : MutatingVCExprVisitor<bool> {
- ApiChecker checker;
- string implName;
- Dictionary<string, List<VCExprVar>> interfaceVarCopies;
- Dictionary<string, List<CallSite>> calleeToCallSites;
- Dictionary<string, List<CallSite>> callerToCallSites;
-
- public BoundingVCMutator(
- ApiChecker checker,
- string implName,
- Dictionary<string, List<VCExprVar>> interfaceVarCopies,
- Dictionary<string, List<CallSite>> calleeToCallSites,
- Dictionary<string, List<CallSite>> callerToCallSites)
- : base(checker.underlyingChecker.VCExprGen) {
- this.checker = checker;
- this.implName = implName;
- this.interfaceVarCopies = interfaceVarCopies;
- this.calleeToCallSites = calleeToCallSites;
- this.callerToCallSites = callerToCallSites;
- }
-
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- bool changed,
- bool arg) {
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr node;
- if (changed)
- node = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments);
- else
- node = originalNode;
-
- VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
- if (lop == null) return node;
-
- string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)
- if (!lop.label.Substring(1).StartsWith(prefix)) return node;
-
- VCExprNAry retnary = node as VCExprNAry;
- Debug.Assert(retnary != null);
-
- VCExprNAry callExpr = retnary[0] as VCExprNAry;
- Debug.Assert(callExpr != null);
-
- VCExprBoogieFunctionOp op = callExpr.Op as VCExprBoogieFunctionOp;
- if (op == null) return callExpr;
-
- if (!interfaceVarCopies.ContainsKey(op.Func.Name)) return callExpr;
-
- var constName = "pcb_callsite_constant_" + StratifiedVCGen.callSiteConstantCount++;
- var constant = Gen.Variable(constName, Bpl.Type.Bool);
- checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, constName, Bpl.Type.Bool)), false, null);
- CallSite cs = new CallSite(implName, op.Func.Name, constant, callExpr);
- calleeToCallSites[op.Func.Name].Add(cs);
- callerToCallSites[implName].Add(cs);
-
- var iv = interfaceVarCopies[op.Func.Name];
- Contract.Assert(op.Arity == iv.Count);
-
- VCExpr conj = VCExpressionGenerator.True;
- for (int i = 0; i < iv.Count; i++) {
- var c = Gen.Eq(callExpr[i], iv[i]);
- conj = Gen.And(conj, c);
- }
-
- return Gen.Implies(constant, conj);
- }
-
- } // end BoundingVCMutator
-
- private void CreateProcedureCopy(StratifiedInliningInfo info, ApiChecker checker)
- {
- var translator = checker.underlyingChecker.TheoremProver.Context.BoogieExprTranslator;
- var Gen = checker.underlyingChecker.VCExprGen;
- var expr = info.vcexpr;
-
- // Instantiate the interface variables
- Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();
- for (int i = 0; i < info.interfaceExprVars.Count; i++) {
- var v = info.interfaceExprVars[i];
- string newName = v.Name + "_iv_" + newVarCnt.ToString();
- newVarCnt++;
- var vp = Gen.Variable(newName, v.Type);
- substForallDict.Add(v, vp);
- interfaceVarCopies[info.impl.Name].Add(vp);
- }
- VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
- SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(Gen);
- Contract.Assert(subst != null);
- expr = subst.Mutate(expr, substForall);
-
- // Instantiate and declare the private variables
- Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();
- foreach (VCExprVar v in info.privateVars) {
- Contract.Assert(v != null);
- string newName = v.Name + "_pv_" + newVarCnt.ToString();
- newVarCnt++;
- checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
- var vp = Gen.Variable(newName, v.Type);
- substExistsDict.Add(v, vp);
- privateVarCopies[info.impl.Name].Add(vp);
- }
- VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
- subst = new SubstitutingVCExprVisitor(Gen);
- expr = subst.Mutate(expr, substExists);
-
- procVcCopies[info.impl.Name] = expr;
}
public class CoverageGraphManager
{
public static int timeStamp = 0;
-
public class Task
{
public enum TaskType { NONE, STEP, INLINE, BLOCK, REACHABLE };
@@ -1629,7 +1456,7 @@ namespace VC Contract.Assert(implName2StratifiedInliningInfo != null);
this.program = program;
- if (!createVConDemand || CommandLineOptions.Clo.ProcedureCopyBound > 0)
+ if (!createVConDemand)
{
foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)
{
@@ -1937,347 +1764,6 @@ namespace VC return ret;
}
- public class PCBInliner : MutatingVCExprVisitor<bool> {
- private VCExprVar callSiteConstant;
- private VCExpr expr;
-
- public PCBInliner(VCExpressionGenerator gen, VCExprVar callSiteConstant, VCExpr expr)
- : base(gen) {
- Contract.Requires(gen != null);
- this.callSiteConstant = callSiteConstant;
- this.expr = expr;
- }
-
- 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;
-
- VCExprNAry naryExpr = ret as VCExprNAry;
- if (naryExpr == null) return ret;
- if (naryExpr.Op != VCExpressionGenerator.ImpliesOp) return ret;
- if (naryExpr[0] != callSiteConstant) return ret;
- return expr;
- }
-
- } // end PCBInliner
-
- private void InlineCallSite(CallSite cs, ApiChecker checker)
- {
- var Gen = checker.underlyingChecker.VCExprGen;
- var callee = cs.calleeName;
- var caller = cs.callerName;
- Helpers.ExtraTraceInformation("inlining call from " + caller + "to " + callee);
- var expr = cs.callExpr;
- VCExpr expansion = procVcCopies[callee];
- List<VCExprVar> interfaceExprVars = interfaceVarCopies[callee];
- List<VCExprVar> privateVars = privateVarCopies[callee];
-
- // Instantiate the "forall" variables
- Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();
- Contract.Assert(interfaceExprVars.Count == expr.Length);
- for (int i = 0; i < interfaceExprVars.Count; i++) {
- substForallDict.Add(interfaceExprVars[i], expr[i]);
- }
- VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
- SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(Gen);
- expansion = subst.Mutate(expansion, substForall);
-
- // Instantiate and declare the "exists" variables
- Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();
- for (int i = 0; i < privateVars.Count; i++) {
- VCExprVar v = privateVars[i];
- string newName = v.Name + "_si_" + newVarCnt.ToString();
- newVarCnt++;
- checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
- var vp = Gen.Variable(newName, v.Type);
- substExistsDict.Add(v, vp);
- privateVarCopies[cs.callerName].Add(vp);
- }
- VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
- subst = new SubstitutingVCExprVisitor(Gen);
- expansion = subst.Mutate(expansion, substExists);
-
- Dictionary<VCExprVar, VCExpr> substCallSiteConstantDict = new Dictionary<VCExprVar, VCExpr>();
- foreach (CallSite oldSite in callerToCallSites[callee]) {
- var newConstName = "pcb_callsite_constant_" + StratifiedVCGen.callSiteConstantCount++;
- var newConstant = Gen.Variable(newConstName, Bpl.Type.Bool);
- checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newConstName, Bpl.Type.Bool)), false, null);
- substCallSiteConstantDict.Add(oldSite.callSiteConstant, newConstant);
- subst = new SubstitutingVCExprVisitor(Gen);
- var newCallExpr = subst.Mutate(oldSite.callExpr, substForall);
- subst = new SubstitutingVCExprVisitor(Gen);
- newCallExpr = subst.Mutate(newCallExpr, substExists);
- var newSite = new CallSite(caller, oldSite.calleeName, newConstant, (VCExprNAry)newCallExpr);
- callerToCallSites[caller].Add(newSite);
- calleeToCallSites[oldSite.calleeName].Add(newSite);
- }
- VCExprSubstitution substCallSiteConstant = new VCExprSubstitution(substCallSiteConstantDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
- subst = new SubstitutingVCExprVisitor(Gen);
- expansion = subst.Mutate(expansion, substCallSiteConstant);
-
- PCBInliner inliner = new PCBInliner(Gen, cs.callSiteConstant, expansion);
- procVcCopies[cs.callerName] = inliner.Mutate(procVcCopies[cs.callerName], true);
-
- callerToCallSites[caller].Remove(cs);
- calleeToCallSites[callee].Remove(cs);
- }
-
-#if SuperAwesomeMethod
- private Outcome FindUnsatCoreInMainCallees(Implementation impl, ApiChecker checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List<VCExpr> assumptions, out HashSet<VCExprVar> unsatCore)
- {
- Debug.Assert(checker is ApiChecker);
- unsatCore = null;
- List<int> unsatCoreIndices;
- Outcome ret;
- ret = checker.CheckAssumptions(assumptions, out unsatCoreIndices);
- if (ret == Outcome.Errors) return ret;
- unsatCore = new HashSet<VCExprVar>();
- HashSet<VCExprVar> implCallees = new HashSet<VCExprVar>();
- foreach (CallSite cs in callerToCallSites[impl.Name]) {
- implCallees.Add(cs.callSiteConstant);
- }
- for (int i = 0; i < unsatCoreIndices.Count; i++) {
- VCExprVar assumption = (VCExprVar)assumptions[unsatCoreIndices[i]];
- if (implCallees.Contains(assumption)) {
- unsatCore.Add(assumption);
- }
- }
- return Outcome.Correct;
- }
-
- private Outcome FindUnsatCore(Implementation impl, ApiChecker checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List<VCExpr> assumptions, out HashSet<VCExprVar> unsatCore)
- {
- Helpers.ExtraTraceInformation("Number of assumptions = " + assumptions.Count);
- unsatCore = null;
- List<int> unsatCoreIndices;
- Outcome ret;
- ret = checker.CheckAssumptions(assumptions, out unsatCoreIndices);
- if (ret == Outcome.Errors) return ret;
- unsatCore = new HashSet<VCExprVar>();
- for (int i = 0; i < unsatCoreIndices.Count; i++) {
- unsatCore.Add((VCExprVar)assumptions[unsatCoreIndices[i]]);
- }
-
- Helpers.ExtraTraceInformation("Number of elements in unsat core = " + unsatCore.Count);
-
- HashSet<CallSite> reachableCallSites = new HashSet<CallSite>();
- Stack<string> stack = new Stack<string>();
- HashSet<string> set = new HashSet<string>();
- stack.Push(impl.Name);
- while (stack.Count > 0) {
- string caller = stack.Peek();
- stack.Pop();
- if (set.Contains(caller)) continue;
- set.Add(caller);
- foreach (CallSite cs in callerToCallSites[caller]) {
- if (unsatCore.Contains(cs.callSiteConstant)) {
- reachableCallSites.Add(cs);
- stack.Push(cs.calleeName);
- }
- }
- }
-
- Graph<CallSite> callGraph = new Graph<CallSite>();
- foreach (CallSite cs1 in reachableCallSites) {
- callGraph.AddSource(cs1);
- foreach (CallSite cs2 in calleeToCallSites[cs1.callerName]) {
- if (reachableCallSites.Contains(cs2)) {
- callGraph.AddEdge(cs1, cs2);
- }
- }
- }
-
- List<CallSite> sortedCallSites = new List<CallSite>();
- foreach (CallSite cs in callGraph.TopologicalSort()) {
- checker.Push();
- checker.AddAxiom(cs.callSiteConstant);
- sortedCallSites.Add(cs);
- }
-
- ret = checker.CheckVC();
- Debug.Assert(ret == Outcome.Correct);
-
- reporter.unsatCoreMode = true;
- VCExpr curr = VCExpressionGenerator.True;
- HashSet<CallSite> relevantCallSites = new HashSet<CallSite>();
- HashSet<VCExprVar> relevantUnsatCore = new HashSet<VCExprVar>();
- int index = sortedCallSites.Count;
- int queries = 0;
- while (index > 0) {
- checker.Pop();
- index--;
- CallSite cs = sortedCallSites[index];
- bool check = (cs.callerName == impl.Name);
- foreach (CallSite x in calleeToCallSites[cs.callerName]) {
- check = check || relevantCallSites.Contains(x);
- }
- if (!check) continue;
- bool relevant = (cs.callerName != impl.Name);
- foreach (CallSite x in calleeToCallSites[cs.calleeName]) {
- if (x.callSiteConstant == cs.callSiteConstant) continue;
- relevant = relevant && !reachableCallSites.Contains(x);
- }
- if (relevant) {
- curr = Gen.And(cs.callSiteConstant, curr);
- relevantCallSites.Add(cs);
- relevantUnsatCore.Add(cs.callSiteConstant);
- continue;
- }
-
- queries++;
- checker.Push();
- checker.AddAxiom(curr);
- ret = checker.CheckVC();
- checker.Pop();
-
- if (ret == Outcome.Errors || ret == Outcome.TimedOut) {
- curr = Gen.And(cs.callSiteConstant, curr);
- relevantCallSites.Add(cs);
- relevantUnsatCore.Add(cs.callSiteConstant);
- }
- }
- reporter.unsatCoreMode = false;
-
- unsatCore = relevantUnsatCore;
- Helpers.ExtraTraceInformation("Number of queries = " + queries);
- Helpers.ExtraTraceInformation("Unsat core after pruning = " + unsatCore.Count);
- return Outcome.Correct;
- }
-
- HashSet<string> ComputeReachableImplementations(Implementation impl) {
- Stack<string> stack = new Stack<string>();
- HashSet<string> set = new HashSet<string>();
- stack.Push(impl.Name);
- while (stack.Count > 0) {
- string caller = stack.Peek();
- stack.Pop();
- if (set.Contains(caller)) continue;
- set.Add(caller);
- foreach (CallSite cs in callerToCallSites[caller]) {
- stack.Push(cs.calleeName);
- }
- }
- return set;
- }
-
- private bool Verified(HashSet<VCExprVar> unsatCore) {
- bool verified = true;
- foreach (string name in calleeToCallSites.Keys) {
- int numInlined = 0;
- foreach (CallSite cs in calleeToCallSites[name]) {
- if (unsatCore.Contains(cs.callSiteConstant))
- numInlined++;
- }
- if (numInlined > 1) {
- Helpers.ExtraTraceInformation("callee name = " + name);
- Helpers.ExtraTraceInformation("number of inlines = " + numInlined);
- verified = false;
- }
- }
- return verified;
- }
-
- private void InlineBottomUp(ApiChecker checker, HashSet<VCExprVar> unsatCore)
- {
- Graph<string> callGraph = new Graph<string>();
- foreach (string name in calleeToCallSites.Keys) {
- callGraph.AddSource(name);
- foreach (CallSite cs in calleeToCallSites[name]) {
- callGraph.AddEdge(name, cs.callerName);
- }
- }
- foreach (string name in callGraph.TopologicalSort()) {
- HashSet<CallSite> toBeInlined = new HashSet<CallSite>();
- foreach (CallSite cs in calleeToCallSites[name]) {
- if (unsatCore.Contains(cs.callSiteConstant)) {
- Debug.Assert(name == cs.calleeName);
- toBeInlined.Add(cs);
- }
- }
- foreach (CallSite cs in toBeInlined) {
- InlineCallSite(cs, checker);
- }
- }
- }
-
- private void InlineIntoMain(ApiChecker checker, Implementation impl, HashSet<VCExprVar> unsatCore)
- {
- HashSet<CallSite> toBeInlined = new HashSet<CallSite>();
- foreach (CallSite cs in callerToCallSites[impl.Name]) {
- if (unsatCore.Contains(cs.callSiteConstant)) {
- toBeInlined.Add(cs);
- }
- }
- foreach (CallSite cs in toBeInlined) {
- InlineCallSite(cs, checker);
- }
- }
-
- private Outcome SuperAwesomeMethod(Checker underlyingChecker, Implementation impl, VCExpr vcMain) {
- // Create the call graph
- // while (true)
- // 1. Create boolean variables for each call site
- // 2. Create the implications both at the top level and at the call sites
- // 3. Verify using CheckAssumptions
- // 4. Traverse call graph bottom up. For each procedure, inline all incoming edges in the unsatCore and update call graph
- // 5. If no node had more than one incoming edges set to true, break
-
- var Gen = underlyingChecker.VCExprGen;
- PCBErrorReporter reporter = new PCBErrorReporter(impl);
- ApiChecker checker;
- checker = new ApiChecker(VCExpressionGenerator.False, reporter, underlyingChecker, null);
- CreateProcedureCopies(impl, program, checker, vcMain);
-
- int iter = 0;
- while (true) {
- Helpers.ExtraTraceInformation("Iteration number " + iter++);
- Outcome ret;
-
- checker.Push();
-
- var reachableImpls = ComputeReachableImplementations(impl);
- var assumptions = new List<VCExpr>();
- foreach (string name in reachableImpls) {
- VCExpr expr = procVcCopies[name];
- if (name == impl.Name) {
- checker.AddAxiom(Gen.Not(expr));
- continue;
- }
- var cscExpr = VCExpressionGenerator.False;
- foreach (CallSite callSite in calleeToCallSites[name]) {
- if (reachableImpls.Contains(callSite.callerName)) {
- assumptions.Add(callSite.callSiteConstant);
- cscExpr = Gen.Or(callSite.callSiteConstant, cscExpr);
- }
- }
- expr = Gen.Implies(cscExpr, expr);
- checker.AddAxiom(expr);
- }
- HashSet<VCExprVar> unsatCore;
- ret = FindUnsatCore(impl, checker, Gen, reporter, assumptions, out unsatCore);
-
- checker.Pop();
-
- if (ret == Outcome.Errors)
- return ret;
-
- if (Verified(unsatCore))
- return Outcome.Correct;
-
- //InlineBottomUp(checker, unsatCore);
- InlineIntoMain(checker, impl, unsatCore);
- }
- }
-#endif
-
// A step of the stratified inlining algorithm: both under-approx and over-approx queries
private Outcome stratifiedStep(int bound, VerificationState vState, HashSet<int> block)
{
@@ -3234,21 +2720,6 @@ namespace VC }
}
- public class PCBErrorReporter : ProverInterface.ErrorHandler {
- public bool unsatCoreMode;
- public Implementation mainImpl;
-
- public PCBErrorReporter(Implementation impl) {
- this.unsatCoreMode = false;
- this.mainImpl = impl;
- }
-
- public override void OnModel(IList<string> labels, ErrorModel errModel) {
- if (unsatCoreMode) return;
- Console.WriteLine("Error in " + mainImpl.Name);
- }
- }
-
public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler
{
Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;
@@ -3428,13 +2899,6 @@ namespace VC }
public override void OnModel(IList<string> labels, ErrorModel errModel) {
- if (CommandLineOptions.Clo.UseLabels)
- OnModelOld(labels, errModel);
- else
- OnModelNew(labels, errModel);
- }
-
- private void OnModelNew(IList<string> labels, ErrorModel errModel) {
List<Absy> absyList = new List<Absy>();
foreach (var label in labels) {
absyList.Add(Label2Absy(label));
@@ -3550,280 +3014,6 @@ namespace VC return newCounterexample;
}
- public void OnModelOld(IList<string/*!*/>/*!*/ labels, ErrorModel errModel)
- {
- Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || errModel != null);
-
- candidatesToExpand = new List<int>();
-
- Model model = null;
- if (errModel != null) model = errModel.ToModel();
-
- if (underapproximationMode)
- {
- var cex = GenerateTraceMain(labels, model, mvInfo);
- Debug.Assert(candidatesToExpand.All(calls.isSkipped));
- if (cex != null) {
- GetModelWithStates(model);
- callback.OnCounterexample(cex, null);
- this.PrintModel(model);
- }
- return;
- }
-
- Contract.Assert(calls != null);
-
- GenerateTraceMain(labels, model, mvInfo);
- }
-
- // Construct the interprocedural trace
- private Counterexample GenerateTraceMain(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo)
- {
- Contract.Requires(cce.NonNullElements(labels));
- if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null)
- {
- errModel.Write(ErrorReporter.ModelWriter);
- ErrorReporter.ModelWriter.Flush();
- }
-
- orderedStateIds = new List<Tuple<int,int>>();
- Counterexample newCounterexample =
- GenerateTrace(labels, errModel, 0, mainImpl);
-
- if (newCounterexample == null)
- return null;
-
- #region Map passive program errors back to original program errors
- ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;
- if (returnExample != null && gotoCmdOrigins != null)
- {
- foreach (Block b in returnExample.Trace)
- {
- Contract.Assert(b != null);
- Contract.Assume(b.TransferCmd != null);
- ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd];
- if (cmd != null)
- {
- returnExample.FailingReturn = cmd;
- break;
- }
- }
- }
- #endregion
-
- return newCounterexample;
- }
-
- private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,
- int candidateId, Implementation procImpl)
- {
- Contract.Requires(cce.NonNullElements(labels));
- Contract.Requires(procImpl != null);
-
- Hashtable traceNodes = new Hashtable();
- //string procPrefix = "si_inline_" + candidateId.ToString() + "_";
-
- //Console.WriteLine("GenerateTrace: {0}", procImpl.Name);
- 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);
- }
-
- BlockSeq trace = new BlockSeq();
- 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, BlockSeq/*!*/ 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)
- {
- CmdSeq cmds = b.Cmds;
- TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
- for (int i = 0; i < cmds.Length; 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))
- {
- Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, 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)
- {
- var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
-
- // Record concrete value of the argument to this procedure
- var args = new List<Model.Element>();
- 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 = 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.Length - 1, i)] =
- new CalleeCounterexampleInfo(null, args);
- continue;
- }
-
- if (!implName2StratifiedInliningInfo.ContainsKey(calleeName))
- continue;
-
- Contract.Assert(calls != null);
-
- if (calls.isPCBCandidate(candidateId))
- {
- Contract.Assert(procBoundingMode);
- // We're already inside PCB VCs. The lookup for procedure calls
- // is different here
- var uid = calls.pcbBoogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)];
- var pcopy = pcbFindLabel(labels, string.Format("PCB_{0}_", uid));
- var actualId = calls.procCopy2Id[Tuple.Create(calleeName, pcopy)];
-
- orderedStateIds.Add(new Tuple<int, int>(actualId, StratifiedInliningErrorReporter.CALL));
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
- new CalleeCounterexampleInfo(
- cce.NonNull(GenerateTrace(labels, errModel, actualId, implName2StratifiedInliningInfo[calleeName].impl)),
- new List<Model.Element>());
- orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));
- }
- else
- {
- int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)];
-
- if (calls.currCandidates.Contains(calleeId)) {
- if (procBoundingMode) {
- // Entering PCB VCs
- var pcopy = pcbFindLabel(labels, string.Format("PCB_CONNECT_{0}_", calleeId));
- Contract.Assert(pcopy >= 0 && pcopy < CommandLineOptions.Clo.ProcedureCopyBound);
- var actualId = calls.procCopy2Id[Tuple.Create(calleeName, pcopy)];
-
- orderedStateIds.Add(new Tuple<int, int>(actualId, StratifiedInliningErrorReporter.CALL));
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
- new CalleeCounterexampleInfo(
- cce.NonNull(GenerateTrace(labels, errModel, actualId, implName2StratifiedInliningInfo[calleeName].impl)),
- new List<Model.Element>());
- orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));
- }
- else {
- candidatesToExpand.Add(calleeId);
- }
- }
- else {
- orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
- new CalleeCounterexampleInfo(
- cce.NonNull(GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),
- new List<Model.Element>());
- 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;
- //return GenerateTraceRec(labels, errModel, candidateId, bb, traceNodes, trace, calleeCounterexamples);
- }
- }
- if (b != null) continue;
- }
- return null;
- }
-
- //return null;
-
- }
-
public override Absy Label2Absy(string label)
{
//Contract.Requires(label != null);
diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat index 3ba74096..2bb3cbd5 100644 --- a/Test/stratifiedinline/runtest.bat +++ b/Test/stratifiedinline/runtest.bat @@ -5,33 +5,33 @@ set BGEXE=..\..\Binaries\Boogie.exe rem set BGEXE=mono ..\..\Binaries\Boogie.exe
echo ----- Running regression test bar1.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 bar1.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar1.bpl
echo -----
echo ----- Running regression test bar2.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 bar2.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar2.bpl
echo -----
echo ----- Running regression test bar3.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 bar3.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar3.bpl
echo -----
echo ----- Running regression test bar4.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 bar4.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar4.bpl
echo -----
echo ----- Running regression test bar6.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 bar6.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar6.bpl
echo -----
echo ----- Running regression test bar7.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar7.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar7.bpl
echo -----
echo ----- Running regression test bar8.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar8.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar8.bpl
echo -----
echo ----- Running regression test bar9.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar9.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar9.bpl
echo -----
echo ----- Running regression test bar10.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar10.bpl
echo -----
echo ----- Running regression test bar11.bpl
-%BGEXE% %* /noinfer /stratifiedInline:1 bar11.bpl
+%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar11.bpl
echo -----
|