From 2235d3dc9e090a1d4b13d653138838624c70ba26 Mon Sep 17 00:00:00 2001 From: akashlal Date: Wed, 7 Jul 2010 17:52:18 +0000 Subject: Boogie: Added stratified inlining. It is enabled using the flag /stratifiedInline:1. --- Source/VCGeneration/Check.ssc | 10 + Source/VCGeneration/ConditionGeneration.ssc | 27 +- Source/VCGeneration/VC.ssc | 803 +++++++++++++++++++++++++++- Source/VCGeneration/Wlp.ssc | 14 + 4 files changed, 849 insertions(+), 5 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc index 0ccbd843..4bd6edea 100644 --- a/Source/VCGeneration/Check.ssc +++ b/Source/VCGeneration/Check.ssc @@ -469,7 +469,17 @@ namespace Microsoft.Boogie /// testing /// public virtual void PushVCExpression(VCExpr! vc) {} + public virtual string! VCExpressionToString(VCExpr! vc) { return ""; } + public virtual void Pop() + throws UnexpectedProverOutputException; + {} + public virtual int NumAxiomsPushed() + { return 0; } + public virtual int FlushAxiomsToTheoremProver() + throws UnexpectedProverOutputException; + { return 0; } + public abstract ProverContext! Context { get; } public abstract VCExpressionGenerator! VCExprGen { get; } } diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc index 6e87fd0e..a2db980d 100644 --- a/Source/VCGeneration/ConditionGeneration.ssc +++ b/Source/VCGeneration/ConditionGeneration.ssc @@ -253,10 +253,33 @@ namespace VC Helpers.ExtraTraceInformation("Finished implementation verification"); return outcome; } - + + public Outcome StratifiedVerifyImplementation(Implementation! impl, Program! program, out List? errors) + ensures result == Outcome.Errors ==> errors != null; + throws UnexpectedProverOutputException; + { + Helpers.ExtraTraceInformation("Starting implementation verification"); + + CounterexampleCollector collector = new CounterexampleCollector(); + Outcome outcome = StratifiedVerifyImplementation(impl, program, collector); + if (outcome == Outcome.Errors) { + errors = collector.examples; + } else { + errors = null; + } + + Helpers.ExtraTraceInformation("Finished implementation verification"); + return outcome; + } + public abstract Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback) throws UnexpectedProverOutputException; - + + public virtual Outcome StratifiedVerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback) + throws UnexpectedProverOutputException; + { + return VerifyImplementation(impl, program, callback); + } /////////////////////////////////// Common Methods and Classes ////////////////////////////////////////// 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(); + implName2StratifiedInliningInfo = new Dictionary(); 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! privateVars; + public List! 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(); + interfaceExprVars = new List(); + } + + } + + private Dictionary! 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/**/! 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(); + 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(); + List interfaceExprs = new List(); + 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 triggers = new List(); + List exprs = new List(); + 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(new object![] { e }), null); + //info.interfaceExprVars.Reverse(); + info.falseExpr = gen.Forall(new List(), 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/**/! 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! toExpand = new List(); + 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! 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! substForallDict = new Dictionary(); + 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()); + + SubstitutingVCExprVisitor! subst = new SubstitutingVCExprVisitor(checker.VCExprGen); + expansion = subst.Mutate(expansion, substForall); + + // Instantiate and declare the "exists" variables + Dictionary! substExistsDict = new Dictionary(); + 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()); + + 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/**/! 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 { + Dictionary! implName2StratifiedInliningInfo; + public List! fcalls; + + public FCallCollector(Dictionary! implName2StratifiedInliningInfo) { + this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo; + fcalls = new List(); + } + + 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 { + Dictionary! implName2StratifiedInliningInfo; + public readonly Hashtable/**/! mainLabel2absy; + public Dictionary! boogieExpr2Id; + public Dictionary! id2Candidate; + public Dictionary! candidate2Id; + public Dictionary! label2Id; + public Microsoft.SpecSharp.Collections.Set 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! implName2StratifiedInliningInfo, + Hashtable/**/! mainLabel2absy) + : base(gen) + { + this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo; + this.mainLabel2absy = mainLabel2absy; + id2Candidate = new Dictionary(); + candidate2Id = new Dictionary(); + boogieExpr2Id = new Dictionary(); + label2Id = new Dictionary(); + currCandidates = new Microsoft.SpecSharp.Collections.Set(); + currInlineCount = 0; + currProc = null; + } + + public void Clear() + { + currCandidates = new Microsoft.SpecSharp.Collections.Set(); + } + + 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/**/! 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! 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/**/! label2absy; @@ -1668,6 +2250,206 @@ namespace VC } } + public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler { + Dictionary! implName2StratifiedInliningInfo; + ProverInterface! theoremProver; + VerifierCallback! callback; + FCallHandler calls; + Program! program; + Implementation! mainImpl; + DeclFreeProverContext! context; + Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins; + + public bool underapproximationMode; + public List! candidatesToExpand; + + public StratifiedInliningErrorReporter(Dictionary! 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(); + this.gotoCmdOrigins = gotoCmdOrigins; + } + + public void SetCandidateHandler(FCallHandler! calls) + { + this.calls = calls; + } + + public override void OnModel(IList! labels, ErrorModel errModel) { + if(underapproximationMode) { + if(errModel == null) return; + GenerateTraceMain(labels, errModel); + return; + } + + assert calls != null; + assert errModel != null; + + candidatesToExpand = new List(); + 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! 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! 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! calleeCounterexamples = new Dictionary(); + Counterexample newCounterexample = GenerateTraceRec(labels, errModel, entryBlock, traceNodes, trace, calleeCounterexamples); + + return newCounterexample; + + } + + private Counterexample GenerateTraceRec( + IList! labels, ErrorModel! errModel, + Block! b, Hashtable! traceNodes, BlockSeq! trace, + Dictionary! 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()); + 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()); + + } + + 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); diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc index 38aa6af8..be99dd6d 100644 --- a/Source/VCGeneration/Wlp.ssc +++ b/Source/VCGeneration/Wlp.ssc @@ -31,6 +31,7 @@ namespace VC { this.Ctxt = ctxt; this.ControlFlowVariable = controlFlowVariable; } + } #region A class to compute wlp of a passive command program @@ -110,6 +111,19 @@ namespace VC { } else if (cmd is AssumeCmd) { AssumeCmd ac = (AssumeCmd)cmd; + + if(CommandLineOptions.Clo.StratifiedInlining > 0) { + // Label the assume if it is a procedure call + NAryExpr naryExpr = ac.Expr as NAryExpr; + if (naryExpr != null) { + if (naryExpr.Fun is FunctionCall) { + int id = ac.UniqueId; + ctxt.Label2absy[id] = ac; + return gen.ImpliesSimp(gen.LabelPos((!)"si_fcall_" + id.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N); + } + } + } + return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N); } else { -- cgit v1.2.3