diff options
| author |  akashlal <unknown> | 2010-07-07 17:52:18 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2010-07-07 17:52:18 +0000 |
| commit | 2235d3dc9e090a1d4b13d653138838624c70ba26 (patch) | |
| tree | cd24b337a633b8d0a189c0de269bb7dadad0a083 /Source/VCGeneration/VC.ssc | |
| parent | c9149ae1142d787e736f3fc7eea616d6422d31fb (diff) | |
Boogie: Added stratified inlining. It is enabled using the flag /stratifiedInline:1.
Diffstat (limited to 'Source/VCGeneration/VC.ssc')
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 803 |
1 files changed, 800 insertions, 3 deletions
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index f169e424..f5a57cf6 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -34,11 +34,16 @@ namespace VC this.appendLogFile = appendLogFile;
this.logFilePath = logFilePath;
implName2LazyInliningInfo = new Dictionary<string!, LazyInliningInfo!>();
+ implName2StratifiedInliningInfo = new Dictionary<string!, StratifiedInliningInfo!>();
base(program);
if (CommandLineOptions.Clo.LazyInlining > 0)
{
this.GenerateVCsForLazyInlining(program);
}
+ if (CommandLineOptions.Clo.StratifiedInlining > 0)
+ {
+ this.GenerateVCsForStratifiedInlining(program);
+ }
// base();
}
@@ -63,7 +68,7 @@ namespace VC return new AssumeCmd(assrt.tok, expr);
}
-
+
#region LazyInlining
public class LazyInliningInfo {
public Implementation! impl;
@@ -234,6 +239,140 @@ namespace VC checker.TheoremProver.PushVCExpression(vcexpr);
}
#endregion
+
+ #region StratifiedInlining
+ public class StratifiedInliningInfo : LazyInliningInfo
+ {
+ public int inline_cnt;
+ public List<VCExprVar!>! privateVars;
+ public List<VCExprVar!>! interfaceExprVars;
+ public VCExpr funcExpr;
+ public VCExpr falseExpr;
+
+ public StratifiedInliningInfo(Implementation! impl, Program! program, int uniqueid)
+ : base(impl, program, uniqueid)
+ {
+ inline_cnt = 0;
+ privateVars = new List<VCExprVar!>();
+ interfaceExprVars = new List<VCExprVar!>();
+ }
+
+ }
+
+ private Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo;
+
+ public void GenerateVCsForStratifiedInlining(Program! program)
+ {
+ Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);
+ foreach (Declaration! decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ Procedure! proc = (!)impl.Proc;
+ if (proc.FindExprAttribute("inline") != null) {
+ StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, QuantifierExpr.GetNextSkolemId());
+ implName2StratifiedInliningInfo[impl.Name] = info;
+ // We don't need controlFlowVariable for stratified Inlining
+ //impl.LocVars.Add(info.controlFlowVariable);
+ ExprSeq! exprs = new ExprSeq();
+ foreach (Variable! v in program.GlobalVariables())
+ {
+ exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ }
+ foreach (Variable! v in proc.InParams)
+ {
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (Variable! v in proc.OutParams)
+ {
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (IdentifierExpr! ie in proc.Modifies)
+ {
+ if (ie.Decl == null) continue;
+ exprs.Add(ie);
+ }
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);
+ proc.Ensures.Add(new Ensures(true, freePostExpr));
+ }
+ }
+
+ foreach (StratifiedInliningInfo! info in implName2StratifiedInliningInfo.Values)
+ {
+ GenerateVCForStratifiedInlining(program, info, checker);
+ }
+ }
+
+ private void GenerateVCForStratifiedInlining(Program! program, StratifiedInliningInfo! info, Checker! checker)
+ requires info.impl != null;
+ requires info.impl.Proc != null;
+ {
+ Implementation! impl = info.impl;
+ ConvertCFG2DAG(impl, program);
+ info.gotoCmdOrigins = PassifyImpl(impl, program);
+ assert info.exitIncarnationMap != null;
+ Hashtable/*<int, Absy!>*/! label2absy;
+ VCExpressionGenerator! gen = checker.VCExprGen;
+ VCExpr! vcexpr = gen.Not(GenerateVC(impl, null, out label2absy, checker));
+ info.label2absy = label2absy;
+
+ Boogie2VCExprTranslator! translator = checker.TheoremProver.Context.BoogieExprTranslator;
+ info.privateVars = new List<VCExprVar!>();
+ foreach (Variable! v in impl.LocVars)
+ {
+ info.privateVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable! v in impl.OutParams)
+ {
+ info.privateVars.Add(translator.LookupVariable(v));
+ }
+
+ info.interfaceExprVars = new List<VCExprVar!>();
+ List<VCExpr!> interfaceExprs = new List<VCExpr!>();
+ foreach (Variable! v in info.interfaceVars)
+ {
+ VCExprVar! ev = translator.LookupVariable(v);
+ info.interfaceExprVars.Add(ev);
+ interfaceExprs.Add(ev);
+ }
+
+ Function! function = (!)info.function;
+ info.funcExpr = gen.Function(function, interfaceExprs);
+ info.vcexpr = vcexpr;
+
+ // Build the "false" expression: forall a b c: foo(a,b,c) <==> false
+
+ info.falseExpr = gen.Eq(info.funcExpr, VCExpressionGenerator.False);
+
+ List<VCTrigger!> triggers = new List<VCTrigger!>();
+ List<VCExpr!> exprs = new List<VCExpr!>();
+ exprs.Add(info.funcExpr);
+ VCTrigger! trigger = new VCTrigger(true, exprs);
+ triggers.Add(trigger);
+
+ Expr e = new LiteralExpr(Token.NoToken, BigNum.FromInt(1));
+ QKeyValue q = new QKeyValue(Token.NoToken, "weight", new List<object!>(new object![] { e }), null);
+ //info.interfaceExprVars.Reverse();
+ info.falseExpr = gen.Forall(new List<TypeVariable!>(), info.interfaceExprVars, triggers,
+ new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), info.falseExpr);
+
+ //checker.TheoremProver.PushVCExpression(vcexpr);
+ /*
+ Console.WriteLine("Procedure: {0}", info.impl.Name);
+ Console.Write("For all: ");
+ foreach(VCExprVar! v in info.interfaceExprVars) {
+ Console.Write(v.ToString() + " ");
+ }
+ Console.WriteLine();
+ Console.Write("There exists: ");
+ foreach(VCExprVar! v in info.privateVars) {
+ Console.Write(v.ToString() + " ");
+ }
+ Console.WriteLine();
+ Console.WriteLine(vcexpr.ToString());
+ */
+ }
+ #endregion
#region Soundness smoke tester
class SmokeTester
@@ -1361,6 +1500,10 @@ namespace VC if (impl.SkipVerification) {
return Outcome.Inconclusive; // not sure about this one
}
+
+ if (CommandLineOptions.Clo.StratifiedInlining > 0) {
+ return StratifiedVerifyImplementation(impl, program, callback);
+ }
callback.OnProgress("VCgen", 0, 0, 0.0);
@@ -1514,6 +1657,445 @@ namespace VC return outcome;
}
+ public override Outcome StratifiedVerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)
+ throws UnexpectedProverOutputException;
+ {
+ // Get the checker
+ Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);
+
+ // Get the VC of the current procedure
+ VCExpr! vc;
+ StratifiedInliningErrorReporter! reporter;
+ Hashtable/*<int, Absy!>*/! mainLabel2absy;
+ GetVC(impl, program, callback, out vc, out mainLabel2absy, out reporter);
+
+ // Find all procedure calls in vc and put labels on them
+ FCallHandler calls = new FCallHandler(checker.VCExprGen, implName2StratifiedInliningInfo, mainLabel2absy);
+ calls.setCurrProcAsMain();
+ vc = calls.Mutate(vc, true);
+ reporter.SetCandidateHandler(calls);
+
+ Outcome ret = Outcome.Correct;
+
+ int expansionCount = 0;
+ int total_axioms_pushed = 0;
+
+ /*
+ // Do eager inlining
+ while(calls.currCandidates.Count != 0)
+ {
+ List<int>! toExpand = new List<int>();
+ foreach(int id in calls.currCandidates) {
+ toExpand.Add(id);
+ }
+ expansionCount += toExpand.Count;
+ total_axioms_pushed +=
+ DoExpansion(toExpand, calls, checker);
+ }
+ */
+
+ int cnt = 0;
+ while(cnt < 500) {
+ cnt ++;
+
+ // Push "false"
+ checker.TheoremProver.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");
+
+ int prev_axioms_pushed = checker.TheoremProver.NumAxiomsPushed();
+
+ foreach(int id in calls.currCandidates) {
+ VCExprNAry! vce = calls.id2Candidate[id];
+ VCExpr! falseExpr = checker.VCExprGen.Eq(vce, VCExpressionGenerator.False);
+ checker.TheoremProver.PushVCExpression(falseExpr);
+ }
+ int axioms_pushed = checker.TheoremProver.NumAxiomsPushed();
+
+ // Note: axioms_pushed may not be the same as calls.currCandidates.Count
+ // because PushVCExpression pushes other stuff too (which always seems
+ // to be TRUE)
+
+ reporter.underapproximationMode = true;
+
+ // Check!
+ //Console.Write("Checking with preds == false: "); Console.Out.Flush();
+ ret = CheckVC(vc, reporter, checker, impl.Name);
+ //Console.WriteLine(ret.ToString());
+
+ // Pop
+ for(int i = 0; i < axioms_pushed - prev_axioms_pushed; i++) {
+ checker.TheoremProver.Pop();
+ }
+
+ checker.TheoremProver.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
+
+ if(ret == Outcome.Errors) {
+ break;
+ }
+
+ // If we didn't underapproximate, then we're done
+ if(calls.currCandidates.Count == 0) {
+ break;
+ }
+
+ checker.TheoremProver.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;");
+ // Push "true" (No-op)
+ // Check
+ reporter.underapproximationMode = false;
+
+ //Console.Write("Checking with preds == true: "); Console.Out.Flush();
+ ret = CheckVC(vc, reporter, checker, impl.Name);
+ //Console.WriteLine(ret.ToString());
+
+ if(ret == Outcome.Correct) {
+ break;
+ }
+
+ checker.TheoremProver.LogComment(";;;;;;;;;;;; Overapprox mode end ;;;;;;;;;;");
+
+ checker.TheoremProver.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
+
+ // Look at the errors to see what to inline
+ assert reporter.candidatesToExpand.Count != 0;
+
+ expansionCount += reporter.candidatesToExpand.Count;
+ total_axioms_pushed +=
+ DoExpansion(reporter.candidatesToExpand, calls, checker);
+
+ checker.TheoremProver.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
+ }
+
+ // Pop off everything that we pushed so that there are no side effects from
+ // this call to VerifyImplementation
+ for(int i = 0; i < total_axioms_pushed; i++) {
+ checker.TheoremProver.Pop();
+ }
+
+ if(cnt == 500)
+ {
+ checker.TheoremProver.LogComment("Stratified Inlining: timeout");
+ }
+
+ checker.TheoremProver.LogComment(string.Format("Stratified Inlining: Calls to Z3: {0}", 2*cnt));
+ checker.TheoremProver.LogComment(string.Format("Stratified Inlining: Expansions performed: {0}", expansionCount));
+ checker.TheoremProver.LogComment(string.Format("Stratified Inlining: Candidates left: {0}", calls.currCandidates.Count));
+
+ return ret;
+ }
+
+ // A counter for adding new variables
+ static int newVarCnt = 0;
+
+ // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
+ // Returns the number of axioms pushed.
+ private int DoExpansion(List<int>! candidates,
+ FCallHandler! calls, Checker! checker)
+ throws UnexpectedProverOutputException;
+ {
+ int old_axioms_pushed = checker.TheoremProver.NumAxiomsPushed();
+ foreach(int id in candidates) {
+ VCExprNAry! expr = calls.id2Candidate[id];
+ string procName = ((!)(expr.Op as VCExprBoogieFunctionOp)).Func.Name;
+ if(!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;
+
+ //Console.WriteLine("Expanding: {0}", expr.ToString());
+
+ StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];
+ VCExpr! expansion = (!)info.vcexpr;
+
+ // Instantiate the "forall" variables
+ Dictionary<VCExprVar!, VCExpr!>! substForallDict = new Dictionary<VCExprVar!, VCExpr!>();
+ 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(checker.VCExprGen);
+ expansion = subst.Mutate(expansion, substForall);
+
+ // Instantiate and declare the "exists" variables
+ Dictionary<VCExprVar!, VCExpr!>! substExistsDict = new Dictionary<VCExprVar!, VCExpr!>();
+ for(int i = 0; i < info.privateVars.Count; i++) {
+ VCExprVar! v = info.privateVars[i];
+ string newName = v.Name + "_si_" + newVarCnt.ToString();
+ newVarCnt ++;
+ checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
+ substExistsDict.Add(v, checker.VCExprGen.Variable(newName, v.Type));
+ }
+ VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable!, Microsoft.Boogie.Type!>());
+
+ subst = new SubstitutingVCExprVisitor(checker.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(expr, expansion);
+ checker.TheoremProver.PushVCExpression(expansion);
+
+ }
+ int axioms_pushed = checker.TheoremProver.NumAxiomsPushed() - old_axioms_pushed;
+ checker.TheoremProver.FlushAxiomsToTheoremProver();
+ return axioms_pushed;
+ }
+
+ // Return the VC for the impl (don't pass it to the theorem prover).
+ // GetVC is a cheap imitation of VerifyImplementatio, except that the VC is not passed to the theorem prover.
+ private void GetVC(Implementation! impl, Program! program, VerifierCallback! callback, out VCExpr! vc, out Hashtable/*<int, Absy!>*/! label2absy, out StratifiedInliningErrorReporter! reporter)
+ {
+ ConvertCFG2DAG(impl, program);
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program);
+ Checker! checker = FindCheckerFor(impl, CommandLineOptions.Clo.ProverKillTime);
+
+ vc = GenerateVC(impl, null, out label2absy, checker);
+
+ /*
+ ErrorReporter errReporter;
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
+ errReporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, (DeclFreeProverContext!) checker.TheoremProver.Context, program);
+ } else {
+ errReporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, (DeclFreeProverContext!) checker.TheoremProver.Context, program);
+ }
+ */
+
+ reporter = new StratifiedInliningErrorReporter(
+ (!)implName2StratifiedInliningInfo, checker.TheoremProver, callback,
+ (DeclFreeProverContext)checker.TheoremProver.Context, gotoCmdOrigins, program, impl);
+
+ }
+
+ private Outcome CheckVC(VCExpr! vc, StratifiedInliningErrorReporter! reporter, Checker! checker, string! implName)
+ throws UnexpectedProverOutputException;
+ {
+ checker.TheoremProver.FlushAxiomsToTheoremProver();
+ checker.BeginCheck(implName, vc, reporter);
+ checker.ProverDone.WaitOne();
+
+ ProverInterface.Outcome outcome = (checker).ReadOutcome();
+
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid:
+ return Outcome.Correct;
+ case ProverInterface.Outcome.Invalid:
+ return Outcome.Errors;
+ case ProverInterface.Outcome.OutOfMemory:
+ return Outcome.OutOfMemory;
+ case ProverInterface.Outcome.TimeOut:
+ return Outcome.TimedOut;
+ case ProverInterface.Outcome.Undetermined:
+ return Outcome.Inconclusive;
+ default:
+ assert false;
+ }
+
+ }
+
+ /*
+ // Collects all function calls in the VCExpr
+ public class FCallCollector : TraversingVCExprVisitor<bool, bool> {
+ Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo;
+ public List<VCExprNAry!>! fcalls;
+
+ public FCallCollector(Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo) {
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ fcalls = new List<VCExprNAry!>();
+ }
+
+ protected override bool StandardResult(VCExpr! node, bool arg) {
+ VCExprNAry vnary = node as VCExprNAry;
+ if(vnary == null) return true;
+ VCExprBoogieFunctionOp bop = vnary.Op as VCExprBoogieFunctionOp;
+ if(bop == null) return true;
+ if(implName2StratifiedInliningInfo.ContainsKey(bop.Func.Name)) {
+ fcalls.Add(vnary);
+ }
+ return true;
+ }
+
+ }
+ */
+
+ // 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 Hashtable/*<int, Absy!>*/! mainLabel2absy;
+ public Dictionary<NAryExpr!, int>! boogieExpr2Id;
+ public Dictionary<int, VCExprNAry!>! id2Candidate;
+ public Dictionary<VCExprNAry!, int>! candidate2Id;
+ public Dictionary<string!, int>! label2Id;
+ public Microsoft.SpecSharp.Collections.Set<int> currCandidates;
+
+ // Name of the procedure who's VC we're mutating
+ string currProc;
+
+ // The 0^th candidate is main
+ static int candidateCount = 1;
+ public int currInlineCount;
+
+ public FCallHandler(VCExpressionGenerator! gen,
+ Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo,
+ Hashtable/*<int, Absy!>*/! mainLabel2absy)
+ : base(gen)
+ {
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ this.mainLabel2absy = mainLabel2absy;
+ id2Candidate = new Dictionary<int, VCExprNAry!>();
+ candidate2Id = new Dictionary<VCExprNAry!, int>();
+ boogieExpr2Id = new Dictionary<NAryExpr!, int>();
+ label2Id = new Dictionary<string!, int>();
+ currCandidates = new Microsoft.SpecSharp.Collections.Set<int>();
+ currInlineCount = 0;
+ currProc = null;
+ }
+
+ public void Clear()
+ {
+ currCandidates = new Microsoft.SpecSharp.Collections.Set<int>();
+ }
+
+ private int GetId(VCExprNAry! vc)
+ {
+ if(candidate2Id.ContainsKey(vc))
+ return candidate2Id[vc];
+
+
+ int id = candidateCount;
+ candidate2Id[vc] = id;
+ id2Candidate[id] = vc;
+
+ candidateCount ++;
+ currCandidates.Add(id);
+
+ return id;
+ }
+
+ private string! GetLabel(int id)
+ {
+ string! ret = "si_fcall_" + id.ToString();
+ if(!label2Id.ContainsKey(ret))
+ label2Id[ret] = id;
+
+ return ret;
+ }
+
+ public int GetId(string! label)
+ {
+ if(!label2Id.ContainsKey(label)) return -1;
+ return label2Id[label];
+ }
+
+ public string! RenameAbsyLabel(string !label)
+ requires label.Length >= 1;
+ {
+ // Remove the sign from the label
+ string! nosign = label.Substring(1);
+ return "si_inline_" + currInlineCount.ToString() + "_" + nosign;
+ }
+
+ public string ParseRenamedAbsyLabel(string! label)
+ {
+ string! prefix = RenameAbsyLabel("+");
+ if(!label.StartsWith(prefix))
+ return null;
+ return label.Substring(prefix.Length);
+ }
+
+ public void setCurrProc(string! name)
+ {
+ currProc = name;
+ assert implName2StratifiedInliningInfo.ContainsKey(name);
+ }
+
+ public void setCurrProcAsMain()
+ {
+ currProc = "";
+ }
+
+ private Hashtable/*<int,absy>*/! getLabel2absy()
+ {
+ assert currProc != null;
+ if(currProc == "") {
+ return mainLabel2absy;
+ }
+ return (!)implName2StratifiedInliningInfo[currProc].label2absy;
+ }
+
+ // Finds labels and changes them:
+ // si_fcall_id: if "id" corresponds to a tracked procedure call, then
+ // si_fcall_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)
+ {
+ 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;
+ 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));
+ Hashtable! label2absy = getLabel2absy();
+ Absy cmd = label2absy[id] as Absy;
+ label2absy.Remove(id);
+
+ assert cmd != null;
+ AssumeCmd acmd = cmd as AssumeCmd;
+ assert acmd != null;
+ NAryExpr naryExpr = acmd.Expr as NAryExpr;
+ assert naryExpr != null;
+
+ string! calleeName = naryExpr.Fun.FunctionName;
+
+ VCExprNAry callExpr = retnary[0] as VCExprNAry;
+ assert callExpr != null;
+
+ if(implName2StratifiedInliningInfo.ContainsKey(calleeName)) {
+ int candidateId = GetId(callExpr);
+ boogieExpr2Id[naryExpr] = candidateId;
+ string! label = GetLabel(candidateId);
+ return Gen.LabelPos(label, callExpr);
+ } else {
+ return callExpr;
+ }
+ }
+
+ // Else, rename label
+ string! newLabel = RenameAbsyLabel(lop.label);
+ if(lop.pos) {
+ return Gen.LabelPos(newLabel, retnary[0]);
+ } else {
+ return Gen.LabelNeg(newLabel, retnary[0]);
+ }
+
+ }
+
+ } // end FCallHandler
+
public class ErrorReporter : ProverInterface.ErrorHandler {
Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins;
Hashtable/*<int, Absy!>*/! label2absy;
@@ -1668,6 +2250,206 @@ namespace VC }
}
+ public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler {
+ Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo;
+ ProverInterface! theoremProver;
+ VerifierCallback! callback;
+ FCallHandler calls;
+ Program! program;
+ Implementation! mainImpl;
+ DeclFreeProverContext! context;
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;
+
+ public bool underapproximationMode;
+ public List<int>! candidatesToExpand;
+
+ public StratifiedInliningErrorReporter(Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo,
+ ProverInterface! theoremProver, VerifierCallback! callback, DeclFreeProverContext! context,
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,
+ Program! program, Implementation! mainImpl) {
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ this.theoremProver = theoremProver;
+ this.callback = callback;
+ this.context = context;
+ this.program = program;
+ this.mainImpl = mainImpl;
+ this.underapproximationMode = false;
+ this.calls = null;
+ this.candidatesToExpand = new List<int>();
+ this.gotoCmdOrigins = gotoCmdOrigins;
+ }
+
+ public void SetCandidateHandler(FCallHandler! calls)
+ {
+ this.calls = calls;
+ }
+
+ public override void OnModel(IList<string!>! labels, ErrorModel errModel) {
+ if(underapproximationMode) {
+ if(errModel == null) return;
+ GenerateTraceMain(labels, errModel);
+ return;
+ }
+
+ assert calls != null;
+ assert errModel != null;
+
+ candidatesToExpand = new List<int>();
+ foreach(string! lab in labels)
+ {
+ int id = calls.GetId(lab);
+ if(id < 0) continue;
+ if(!calls.currCandidates.Contains(id)) continue;
+ candidatesToExpand.Add(id);
+ }
+
+ }
+
+ // Construct the interprocedural trace
+ private void GenerateTraceMain(IList<string!>! labels, ErrorModel! errModel) {
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {
+ errModel.Print(ErrorReporter.ModelWriter);
+ ErrorReporter.ModelWriter.Flush();
+ }
+
+ Counterexample newCounterexample =
+ GenerateTrace(labels, errModel, 0, mainImpl);
+
+ if(newCounterexample == null) return;
+
+ #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) {
+ assume b.TransferCmd != null;
+ ReturnCmd cmd = (ReturnCmd) gotoCmdOrigins[b.TransferCmd];
+ if (cmd != null)
+ {
+ returnExample.FailingReturn = cmd;
+ break;
+ }
+ }
+ }
+ #endregion
+
+ callback.OnCounterexample(newCounterexample, null);
+ }
+
+ private Counterexample GenerateTrace(IList<string!>! labels, ErrorModel! errModel,
+ int candidateId, Implementation! procImpl) {
+
+ Hashtable traceNodes = new Hashtable();
+ foreach (string! s in labels) {
+ string! procPrefix = "si_inline_" + candidateId.ToString() + "_";
+ if(!s.StartsWith(procPrefix))
+ continue;
+
+ Absy! absy;
+
+ if(candidateId == 0) {
+ absy = Label2Absy(s.Substring(procPrefix.Length));
+ } else {
+ absy = Label2Absy(procImpl.Name, s.Substring(procPrefix.Length));
+ }
+
+ 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 = (!) procImpl.Blocks[0];
+ assert traceNodes.Contains(entryBlock);
+ trace.Add(entryBlock);
+
+ Dictionary<Absy!, CalleeCounterexampleInfo!>! calleeCounterexamples = new Dictionary<Absy!, CalleeCounterexampleInfo!>();
+ Counterexample newCounterexample = GenerateTraceRec(labels, errModel, entryBlock, traceNodes, trace, calleeCounterexamples);
+
+ return newCounterexample;
+
+ }
+
+ private Counterexample GenerateTraceRec(
+ IList<string!>! labels, ErrorModel! errModel,
+ Block! b, Hashtable! traceNodes, BlockSeq! trace,
+ Dictionary<Absy!, CalleeCounterexampleInfo!>! calleeCounterexamples)
+ {
+ // After translation, all potential errors come from asserts.
+ CmdSeq! cmds = b.Cmds;
+ TransferCmd! transferCmd = (!)b.TransferCmd;
+ for (int i = 0; i < cmds.Length; i++)
+ {
+ Cmd! cmd = (!) 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, new Dictionary<Incarnation, Absy!>());
+ 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;
+ if (!implName2StratifiedInliningInfo.ContainsKey(calleeName)) continue;
+
+ assert calls != null;
+ int calleeId = calls.boogieExpr2Id[naryExpr];
+
+ calleeCounterexamples[assumeCmd] =
+ new CalleeCounterexampleInfo(
+ (!)GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl),
+ new List<object!>());
+
+ }
+
+ GotoCmd gotoCmd = transferCmd as GotoCmd;
+ if (gotoCmd != null)
+ {
+ foreach (Block! bb in (!)gotoCmd.labelTargets)
+ {
+ if (traceNodes.Contains(bb)){
+ trace.Add(bb);
+ return GenerateTraceRec(labels, errModel, bb, traceNodes, trace, calleeCounterexamples);
+ }
+ }
+ }
+
+ return null;
+
+ }
+
+ public override Absy! Label2Absy(string! label)
+ {
+ int id = int.Parse(label);
+ assert calls != null;
+ return (Absy!) calls.mainLabel2absy[id];
+ }
+
+ public Absy! Label2Absy(string! procName, string! label)
+ {
+ int id = int.Parse(label);
+ Hashtable! l2a = (!)implName2StratifiedInliningInfo[procName].label2absy;
+ return (Absy!) l2a[id];
+ }
+
+ public override void OnResourceExceeded(string! msg)
+ {
+ //resourceExceededMessage = msg;
+ }
+
+ public override void OnProverWarning(string! msg)
+ {
+ callback.OnWarning(msg);
+ }
+ }
+
protected void ConvertCFG2DAG(Implementation! impl, Program! program)
{
impl.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
@@ -1922,7 +2704,15 @@ namespace VC exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
}
#endregion
-
+
+ #region Support for stratified lazy inlining
+ if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(impl.Name))
+ {
+ Expr! assertExpr = implName2StratifiedInliningInfo[impl.Name].assertExpr;
+ exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
+ }
+ #endregion
+
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
@@ -1952,7 +2742,13 @@ namespace VC info.exitIncarnationMap = exitIncarnationMap;
info.incarnationOriginMap = this.incarnationOriginMap;
}
-
+ if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(impl.Name))
+ {
+ StratifiedInliningInfo! info = implName2StratifiedInliningInfo[impl.Name];
+ info.exitIncarnationMap = exitIncarnationMap;
+ info.incarnationOriginMap = this.incarnationOriginMap;
+ }
+
if (CommandLineOptions.Clo.LiveVariableAnalysis) {
Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
}
@@ -2971,6 +3767,7 @@ namespace VC SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);
}
+
VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);
VCExpr vc = Wlp.Block(block, SuccCorrect, context);
|