From d03242f9efa515d848f9166244bfaaa9fefd22b0 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 17 Apr 2010 19:14:43 +0000 Subject: First cut of lazy inlining. The option can be turned on by the flag /lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented. --- Source/VCGeneration/Check.ssc | 64 ++++- Source/VCGeneration/ConditionGeneration.ssc | 85 ++++-- Source/VCGeneration/Context.ssc | 3 +- Source/VCGeneration/VC.ssc | 432 ++++++++++++++++++++++++++-- Source/VCGeneration/Wlp.ssc | 40 ++- 5 files changed, 565 insertions(+), 59 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc index ca434ec5..086c3b6d 100644 --- a/Source/VCGeneration/Check.ssc +++ b/Source/VCGeneration/Check.ssc @@ -12,6 +12,7 @@ using System.Diagnostics; using Microsoft.Contracts; using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie.VCExprAST; +using Microsoft.Basetypes; namespace Microsoft.Boogie { @@ -41,8 +42,9 @@ namespace Microsoft.Boogie public readonly AutoResetEvent! ProverDone = new AutoResetEvent(false); - private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation! impl) + private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) { + if (impl == null) return CommandLineOptions.Clo.Bitvectors; bool force_int = false; bool force_native = false; ((!)impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int); @@ -54,7 +56,7 @@ namespace Microsoft.Boogie return CommandLineOptions.Clo.Bitvectors; } - public bool WillingToHandle(Implementation! impl, int timeout) + public bool WillingToHandle(Implementation impl, int timeout) { return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl); } @@ -100,9 +102,9 @@ namespace Microsoft.Boogie ///////////////////////////////////////////////////////////////////////////////// /// - /// Constructor. Initialize a the checker with the program and log file. + /// Constructor. Initialize a checker with the program and log file. /// - public Checker(VC.ConditionGeneration! vcgen, Program! prog, string/*?*/ logFilePath, bool appendLogFile, Implementation! impl, int timeout) + public Checker(VC.ConditionGeneration! vcgen, Program! prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) { this.bitvectors = BvHandlingForImpl(impl); this.timeout = timeout; @@ -310,6 +312,60 @@ namespace Microsoft.Boogie } public virtual void Print(TextWriter! writer) { } + + public int LookupPartitionValue(int partition) + { + BigNum bignum = (BigNum) (!)partitionToValue[partition]; + return bignum.ToInt; + } + + public int LookupControlFlowFunctionAt(int cfc, int id) + { + List>! tuples = this.definedFunctions["ControlFlow"]; + foreach (List tuple in tuples) + { + if (tuple == null) continue; + if (tuple.Count != 3) continue; + if (LookupPartitionValue(tuple[0]) == cfc && LookupPartitionValue(tuple[1]) == id) + return LookupPartitionValue(tuple[2]); + } + assert false; + return 0; + } + + private string! LookupSkolemFunction(string! name) { + foreach (string! functionName in definedFunctions.Keys) + { + int index = functionName.LastIndexOf("!"); + if (index == -1) continue; + string! newFunctionName = (!)functionName.Remove(index); + if (newFunctionName.Equals(name)) + return functionName; + } + assert false; + return ""; + } + public int LookupSkolemFunctionAt(string! functionName, List! values) + { + List>! tuples = this.definedFunctions[LookupSkolemFunction(functionName)]; + assert tuples.Count > 0; + // the last tuple is a dummy tuple + for (int n = 0; n < tuples.Count - 1; n++) + { + List! tuple = (!)tuples[n]; + assert tuple.Count - 1 <= values.Count; + for (int i = 0, j = 0; i < values.Count; i++) + { + if (values[i] == tuple[j]) { + // succeeded in matching tuple[j] + j++; + if (j == tuple.Count-1) return tuple[tuple.Count - 1]; + } + } + } + assert false; + return 0; + } } public abstract class ProverInterface diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc index 7d71f166..6e63c296 100644 --- a/Source/VCGeneration/ConditionGeneration.ssc +++ b/Source/VCGeneration/ConditionGeneration.ssc @@ -23,13 +23,57 @@ namespace Microsoft.Boogie [Peer] public BlockSeq! Trace; [Peer] public List! relatedInformation; + public Dictionary! calleeCounterexamples; + internal Counterexample(BlockSeq! trace) { this.Trace = trace; this.relatedInformation = new List(); + this.calleeCounterexamples = new Dictionary(); // base(); } + public void AddCalleeCounterexample(Absy! absy, Counterexample! cex) + { + calleeCounterexamples[absy] = cex; + } + + public void AddCalleeCounterexample(Dictionary! cs) + { + foreach (Absy! absy in cs.Keys) + { + AddCalleeCounterexample(absy, cs[absy]); + } + } + + public void Print(int spaces) + { + foreach (Block! b in Trace) { + if (b.tok == null) { + Console.WriteLine(" "); + } else { + // for ErrorTrace == 1 restrict the output; + // do not print tokens with -17:-4 as their location because they have been + // introduced in the translation and do not give any useful feedback to the user + if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) { + for (int i = 0; i < spaces+4; i++) Console.Write(" "); + Console.WriteLine("{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label); + foreach (Cmd! cmd in b.Cmds) { + if (calleeCounterexamples.ContainsKey(cmd)) { + AssumeCmd! assumeCmd = (AssumeCmd!) cmd; + NAryExpr! naryExpr = (NAryExpr!) assumeCmd.Expr; + for (int i = 0; i < spaces+4; i++) Console.Write(" "); + Console.WriteLine("Inlined call to procedure {0} begins", naryExpr.Fun.FunctionName); + calleeCounterexamples[cmd].Print(spaces+4); + for (int i = 0; i < spaces+4; i++) Console.Write(" "); + Console.WriteLine("Inlined call to procedure {0} ends", naryExpr.Fun.FunctionName); + } + } + } + } + } + } + public abstract int GetLocation(); } @@ -41,7 +85,7 @@ namespace Microsoft.Boogie return -1; } } - + public class AssertCounterexample : Counterexample { [Peer] public AssertCmd! FailingAssert; @@ -158,16 +202,15 @@ namespace VC public enum Outcome { Correct, Errors, TimedOut, OutOfMemory, Inconclusive } - protected readonly List! provers = new List(); + protected readonly List! checkers = new List(); protected Implementation current_impl = null; - // shared across each implementation; created anew for each implementation protected Hashtable /*Variable -> int*/ variable2SequenceNumber; public Dictionary! incarnationOriginMap = new Dictionary(); // used only by FindCheckerFor - protected Program! program; + public Program! program; protected string/*?*/ logFilePath; protected bool appendLogFile; @@ -496,28 +539,28 @@ namespace VC #endregion - protected Checker! FindCheckerFor(Implementation! impl, int timeout) + protected Checker! FindCheckerFor(Implementation impl, int timeout) { int i = 0; - while (i < provers.Count) { - if (provers[i].Closed) { - provers.RemoveAt(i); + while (i < checkers.Count) { + if (checkers[i].Closed) { + checkers.RemoveAt(i); continue; } else { - if (!provers[i].IsBusy && provers[i].WillingToHandle(impl, timeout)) return provers[i]; + if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout)) return checkers[i]; } ++i; } string? log = logFilePath; - if (log != null && !log.Contains("@PROC@") && provers.Count > 0) - log = log + "." + provers.Count; + if (log != null && !log.Contains("@PROC@") && checkers.Count > 0) + log = log + "." + checkers.Count; Checker! ch = new Checker(this, program, log, appendLogFile, impl, timeout); - provers.Add(ch); + checkers.Add(ch); return ch; } - public void Close() { foreach (Checker! prover in provers) prover.Close(); } + public void Close() { foreach (Checker! checker in checkers) checker.Close(); } protected class CounterexampleCollector : VerifierCallback @@ -636,7 +679,6 @@ namespace VC return new List(); } - protected Variable! CreateIncarnation(Variable! x, Absy a) requires this.variable2SequenceNumber != null; requires this.current_impl != null; @@ -675,7 +717,7 @@ namespace VC { if (b.Predecessors.Length == 0) { - return new Hashtable /*Variable -> Expr*/ (); + return new Hashtable(); } Hashtable /*Variable -> Expr*/ incarnationMap = null; @@ -788,8 +830,7 @@ namespace VC #endregion } - - protected void Convert2PassiveCmd(Implementation! impl) + protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation! impl) { #region Convert to Passive Commands @@ -824,6 +865,7 @@ namespace VC // Now we can process the nodes in an order so that we're guaranteed to have // processed all of a node's predecessors before we process the node. Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/(); + Block exitBlock = null; foreach (Block! b in sortedNodes ) { assert !block2Incarnation.Contains(b); @@ -834,8 +876,13 @@ namespace VC #endregion Each block's map needs to be available to successor blocks TurnIntoPassiveBlock(b, incarnationMap, oldFrameSubst); + exitBlock = b; } + // Verify that exitBlock is indeed the unique exit block + assert exitBlock != null; + assert exitBlock.TransferCmd is ReturnCmd; + // We no longer need the where clauses on the out parameters, so we remove them to restore the situation from before VC generation foreach (Formal! f in impl.OutParams) { f.TypedIdent.WhereExpr = null; @@ -849,6 +896,8 @@ namespace VC EmitImpl(impl, true); } #endregion + + return (Hashtable) block2Incarnation[exitBlock]; } /// @@ -879,7 +928,7 @@ namespace VC { AssignCmd! assign = ((AssignCmd)c).AsSimpleAssignCmd; // first remove map assignments #region Substitute all variables in E with the current map - List! copies = new List (); + List copies = new List (); foreach (Expr! e in assign.Rhss) copies.Add(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, diff --git a/Source/VCGeneration/Context.ssc b/Source/VCGeneration/Context.ssc index be32cabe..2db00964 100644 --- a/Source/VCGeneration/Context.ssc +++ b/Source/VCGeneration/Context.ssc @@ -28,7 +28,7 @@ namespace Microsoft.Boogie public virtual void AddAxiom(Axiom! a, string attributes) { ProcessDeclaration(a); } public abstract void AddAxiom(VCExpr! vc); public virtual void DeclareGlobalVariable(GlobalVariable! v, string attributes) { ProcessDeclaration(v); } - + public abstract VCExpressionGenerator! ExprGen { get; } public abstract Boogie2VCExprTranslator! BoogieExprTranslator { get; } public abstract VCGenerationOptions! VCGenOptions { get; } @@ -194,6 +194,7 @@ namespace Microsoft.Boogie // by the various provers public abstract class VCExprTranslator : ICloneable { public abstract string! translate(VCExpr! expr, int polarity); + public abstract string! Lookup(VCExprVar! var); public abstract Object! Clone(); } } diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index ee5d3d10..faa9e55b 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -27,12 +27,18 @@ namespace VC /// /// Constructor. Initializes the theorem prover. /// + [NotDelayed] public VCGen(Program! program, string/*?*/ logFilePath, bool appendLogFile) // throws ProverException { - base(program); this.appendLogFile = appendLogFile; this.logFilePath = logFilePath; + implName2LazyInliningInfo = new Dictionary(); + base(program); + if (CommandLineOptions.Clo.LazyInlining) + { + this.GenerateVCsForLazyInlining(program); + } // base(); } @@ -58,10 +64,195 @@ namespace VC return new AssumeCmd(assrt.tok, expr); } - - - - + #region LazyInlining + public class LazyInliningInfo { + public Implementation! impl; + public int uniqueId; + public Function! function; + public Variable! controlFlowVariable; + public VCExpr vcexpr; + public Dictionary incarnationOriginMap; + public Hashtable /*Variable->Expr*/ exitIncarnationMap; + public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins; + public Hashtable/**/ label2absy; + + public LazyInliningInfo(Implementation! impl, Program! program, int uniqueId) + { + this.impl = impl; + this.uniqueId = uniqueId; + this.controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "cfc", Microsoft.Boogie.Type.Int)); + + Procedure! proc = (!)impl.Proc; + VariableSeq! interfaceVars = new VariableSeq(); + foreach (Variable! v in program.GlobalVariables()) + { + interfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true)); + } + foreach (Variable! v in proc.InParams) + { + interfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true)); + } + foreach (Variable! v in proc.OutParams) + { + interfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true)); + } + foreach (IdentifierExpr! e in proc.Modifies) + { + if (e.Decl == null) continue; + Variable! v = e.Decl; + interfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true)); + } + TypedIdent! ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool); + Formal! returnVar = new Formal(Token.NoToken, ti, false); + this.function = new Function(Token.NoToken, proc.Name, interfaceVars, returnVar); + } + } + + private Dictionary! implName2LazyInliningInfo; + + public void GenerateVCsForLazyInlining(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) { + LazyInliningInfo info = new LazyInliningInfo(impl, program, implName2LazyInliningInfo.Count); + implName2LazyInliningInfo[impl.Name] = info; + 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) + { + exprs.Add(ie); + } + Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs); + proc.Ensures.Add(new Ensures(true, freePostExpr)); + } + } + + bool oldOptionLiveVariableAnalysis = CommandLineOptions.Clo.LiveVariableAnalysis; + CommandLineOptions.Clo.LiveVariableAnalysis = false; + foreach (LazyInliningInfo! info in implName2LazyInliningInfo.Values) + { + GenerateVCForLazyInlining(program, info, checker); + } + CommandLineOptions.Clo.LiveVariableAnalysis = oldOptionLiveVariableAnalysis; + } + + private void GenerateVCForLazyInlining(Program! program, LazyInliningInfo! 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, info.controlFlowVariable, out label2absy, checker)); + info.label2absy = label2absy; + + Boogie2VCExprTranslator! translator = checker.TheoremProver.Context.BoogieExprTranslator; + List interfaceExprVars = new List(); + foreach (Variable! v in program.GlobalVariables()) + { + interfaceExprVars.Add(translator.LookupVariable(v)); + } + + foreach (Variable! v in impl.InParams) + { + interfaceExprVars.Add(translator.LookupVariable(v)); + } + + VCExpr! allAssumeExpr = VCExpressionGenerator.True; + foreach (Variable! v in impl.OutParams) + { + VCExprVar! vcvar = gen.Variable(v.Name, v.TypedIdent.Type); + interfaceExprVars.Add(vcvar); + VCExpr assumeExpr = null; + if (info.exitIncarnationMap.ContainsKey(v)) + { + Expr! ie = (Expr!) info.exitIncarnationMap[v]; + assumeExpr = gen.Eq(vcvar, translator.Translate(ie)); + } + else + { + assumeExpr = gen.Eq(vcvar, translator.LookupVariable(v)); + } + allAssumeExpr = gen.And(allAssumeExpr, assumeExpr); + } + foreach (IdentifierExpr! e in impl.Proc.Modifies) + { + if (e.Decl == null) continue; + Variable! v = e.Decl; + VCExprVar! vcvar = gen.Variable(v.Name, v.TypedIdent.Type); + interfaceExprVars.Add(vcvar); + VCExpr assumeExpr = null; + if (info.exitIncarnationMap.ContainsKey(v)) + { + Expr! ie = (Expr!) info.exitIncarnationMap[v]; + assumeExpr = gen.Eq(vcvar, translator.Translate(ie)); + } + else + { + assumeExpr = gen.Eq(vcvar, translator.LookupVariable(v)); + } + allAssumeExpr = gen.And(allAssumeExpr, assumeExpr); + } + vcexpr = gen.And(vcexpr, allAssumeExpr); + + List privateVars = new List(); + foreach (Variable! v in impl.LocVars) + { + privateVars.Add(translator.LookupVariable(v)); + } + foreach (Variable! v in impl.OutParams) + { + privateVars.Add(translator.LookupVariable(v)); + } + if (privateVars.Count > 0) + { + vcexpr = gen.Exists(new List(), privateVars, new List(), new VCQuantifierInfos(impl.Name, info.uniqueId, false, null), vcexpr); + } + + List interfaceExprs = new List(); + foreach (VCExprVar! ev in interfaceExprVars) + { + interfaceExprs.Add(ev); + } + Function! function = (!)info.function; + VCExpr! expr = gen.Function(function, interfaceExprs); + + vcexpr = gen.Implies(expr, vcexpr); + + List exprs = new List(); + exprs.Add(expr); + VCTrigger! trigger = new VCTrigger(true, exprs); + List triggers = new List(); + triggers.Add(trigger); + + interfaceExprVars.Reverse(); + vcexpr = gen.Forall(interfaceExprVars, triggers, vcexpr); + checker.TheoremProver.PushVCExpression(vcexpr); + + info.vcexpr = vcexpr; + } + #endregion + #region Soundness smoke tester class SmokeTester { @@ -272,7 +463,7 @@ namespace VC parent.PassifyImpl(impl, program); Hashtable! label2Absy; Checker! ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout); - VCExpr! vc = parent.GenerateVC(impl, out label2Absy, ch); + VCExpr! vc = parent.GenerateVC(impl, null, out label2Absy, ch); impl.Blocks = backup; if (CommandLineOptions.Clo.TraceVerify) { @@ -1066,12 +1257,12 @@ namespace VC checker = parent.FindCheckerFor(impl, timeout); Hashtable/**/! label2absy; - VCExpr! vc = parent.GenerateVC(impl, out label2absy, checker); + VCExpr! vc = parent.GenerateVC(impl, null, out label2absy, checker); if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { - reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback); + reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, (DeclFreeProverContext!) this.Checker.TheoremProver.Context, parent.program); } else { - reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback); + reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, (DeclFreeProverContext!) this.Checker.TheoremProver.Context, parent.program); } if (CommandLineOptions.Clo.TraceVerify && no >= 0) @@ -1084,7 +1275,6 @@ namespace VC if (no >= 0) desc += "_split" + no; checker.BeginCheck(desc, vc, reporter); - } private void SoundnessCheck(Dictionary! cache, Block! orig, List! copies) @@ -1134,7 +1324,7 @@ namespace VC #endregion - protected VCExpr! GenerateVC(Implementation! impl, out Hashtable/**/! label2absy, Checker! ch) + protected VCExpr! GenerateVC(Implementation! impl, Variable controlFlowVariable, out Hashtable/**/! label2absy, Checker! ch) { TypecheckingContext tc = new TypecheckingContext(null); impl.Typecheck(tc); @@ -1164,7 +1354,7 @@ namespace VC if (((!)CommandLineOptions.Clo.TheProverFactory).SupportsDags) { vc = DagVC((!)impl.Blocks[0], label2absy, new Hashtable/**/(), ch.TheoremProver.Context); } else { - vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context); + vc = LetVC((!)impl.Blocks[0], controlFlowVariable, label2absy, ch.TheoremProver.Context); } break; case CommandLineOptions.VCVariety.Doomed: @@ -1182,7 +1372,6 @@ namespace VC Console.WriteLine("ignoring ill-formed {:{0} ...} attribute on {1}, parameter should be an int", name, impl.Name); } } - public override Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback) throws UnexpectedProverOutputException; @@ -1360,20 +1549,31 @@ namespace VC } } + Dictionary! implName2LazyInliningInfo; + DeclFreeProverContext! context; + Program! program; + public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins, Hashtable/**/! label2absy, List! blocks, Dictionary! incarnationOriginMap, - VerifierCallback! callback) + VerifierCallback! callback, + Dictionary! implName2LazyInliningInfo, + DeclFreeProverContext! context, + Program! program) { this.gotoCmdOrigins = gotoCmdOrigins; this.label2absy = label2absy; this.blocks = blocks; this.incarnationOriginMap = incarnationOriginMap; this.callback = callback; + + this.implName2LazyInliningInfo = implName2LazyInliningInfo; + this.context = context; + this.program = program; // base(); } - + public override void OnModel(IList! labels, ErrorModel errModel) { if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) { errModel.Print(ErrorReporter.ModelWriter); @@ -1381,7 +1581,7 @@ namespace VC } Hashtable traceNodes = new Hashtable(); foreach (string! s in labels) { - Absy! absy =Label2Absy(s); + Absy! absy = Label2Absy(s); if (traceNodes.ContainsKey(absy)) System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes"); else @@ -1393,7 +1593,7 @@ namespace VC assert traceNodes.Contains(entryBlock); trace.Add(entryBlock); - Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap); + Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program); if (newCounterexample == null) return; @@ -1437,9 +1637,12 @@ namespace VC Hashtable/**/! label2absy, List! blocks, Dictionary! incarnationOriginMap, - VerifierCallback! callback) + VerifierCallback! callback, + Dictionary! implName2LazyInliningInfo, + DeclFreeProverContext! context, + Program! program) { - base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback); // here for aesthetic purposes + base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, context, program); // here for aesthetic purposes } public override void OnModel(IList! labels, ErrorModel errModel) { @@ -1730,6 +1933,13 @@ namespace VC } #endregion + #region Support for lazy inlining + if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(impl.Name)) + { + exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, Expr.False)); + } + #endregion + #region Debug Tracing if (CommandLineOptions.Clo.TraceVerify) { @@ -1752,7 +1962,13 @@ namespace VC Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl); } - Convert2PassiveCmd(impl); + Hashtable exitIncarnationMap = Convert2PassiveCmd(impl); + if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(impl.Name)) + { + LazyInliningInfo! info = implName2LazyInliningInfo[impl.Name]; + info.exitIncarnationMap = exitIncarnationMap; + info.incarnationOriginMap = this.incarnationOriginMap; + } if (CommandLineOptions.Clo.LiveVariableAnalysis) { Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl); @@ -1811,20 +2027,167 @@ namespace VC return gotoCmdOrigins; } - static Counterexample TraceCounterexample(Block! b, Hashtable! traceNodes, BlockSeq! trace, ErrorModel errModel, Dictionary! incarnationOriginMap) + private static Counterexample! LazyCounterexample( + ErrorModel! errModel, + Dictionary! implName2LazyInliningInfo, + DeclFreeProverContext! context, + Program! program, + string! implName, List! values) + { + VCExprTranslator! vcExprTranslator = (!)context.exprTranslator; + Boogie2VCExprTranslator! boogieExprTranslator = context.BoogieExprTranslator; + LazyInliningInfo! info = implName2LazyInliningInfo[implName]; + BlockSeq! trace = new BlockSeq(); + Block! b = ((!) info.impl).Blocks[0]; + trace.Add(b); + VCExprVar! cfcVar = boogieExprTranslator.LookupVariable(info.controlFlowVariable); + string! cfcName = vcExprTranslator.Lookup(cfcVar); + int cfcPartition = errModel.LookupSkolemFunctionAt(cfcName + "!" + info.uniqueId, values); + int cfcValue = errModel.LookupPartitionValue(cfcPartition); + + Dictionary calleeCounterexamples = new Dictionary(); + while (true) { + CmdSeq! cmds = b.Cmds; + TransferCmd! transferCmd = (!)b.TransferCmd; + for (int i = 0; i < cmds.Length; i++) + { + Cmd! cmd = (!) cmds[i]; + AssertCmd assertCmd = cmd as AssertCmd; + if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0) + { + Counterexample newCounterexample; + newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, (!)info.incarnationOriginMap); + newCounterexample.AddCalleeCounterexample(calleeCounterexamples); + return newCounterexample; + } + + 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 (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue; + + List! args = new List(); + foreach (Expr! expr in naryExpr.Args) + { + LiteralExpr litExpr = expr as LiteralExpr; + if (litExpr != null) + { + args.Add(errModel.valueToPartition[litExpr.Val]); + continue; + } + + IdentifierExpr idExpr = expr as IdentifierExpr; + assert idExpr != null; + Variable! var = (!)idExpr.Decl; + + int index = 0; + List globalVars = program.GlobalVariables(); + foreach (Variable! global in globalVars) + { + if (global == var) break; + index++; + } + if (index < globalVars.Count) + { + args.Add(values[index]); + continue; + } + + foreach (Variable! input in info.impl.InParams) + { + if (input == var) break; + index++; + } + if (index < globalVars.Count + info.impl.InParams.Length) + { + args.Add(values[index]); + continue; + } + + foreach (Variable! output in info.impl.OutParams) + { + if (output == var) break; + index++; + } + if (index < globalVars.Count + info.impl.InParams.Length + info.impl.OutParams.Length) + { + args.Add(values[index]); + continue; + } + + VCExprVar! exprVar = boogieExprTranslator.LookupVariable(var); + string! name = vcExprTranslator.Lookup(exprVar); + int partition = errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values); + args.Add(partition); + } + calleeCounterexamples[assumeCmd] = LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args); + } + + GotoCmd gotoCmd = transferCmd as GotoCmd; + if (gotoCmd == null) break; + int nextBlockId = errModel.LookupControlFlowFunctionAt(cfcValue, b.UniqueId); + b = (Block!) ((!)info.label2absy)[nextBlockId]; + trace.Add(b); + } + assert false; + } + + static Counterexample TraceCounterexample(Block! b, BlockSeq! trace, ErrorModel errModel, Dictionary! incarnationOriginMap) { // After translation, all potential errors come from asserts. + + return null; + } + + static Counterexample TraceCounterexample(Block! b, Hashtable! traceNodes, BlockSeq! trace, ErrorModel errModel, Dictionary! incarnationOriginMap, Dictionary! implName2LazyInliningInfo, DeclFreeProverContext! context, Program! program) + { + Dictionary calleeCounterexamples = new Dictionary(); + // 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)) - continue; - - return AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, incarnationOriginMap); + if (cmd is AssertCmd && traceNodes.Contains(cmd)) + { + Counterexample! newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, incarnationOriginMap); + newCounterexample.AddCalleeCounterexample(calleeCounterexamples); + return newCounterexample; + } + + #region Counterexample generation for lazily inlined procedures + if (errModel == null) continue; + 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 (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue; + VCExprTranslator! vcExprTranslator = (!)context.exprTranslator; + Boogie2VCExprTranslator! boogieExprTranslator = context.BoogieExprTranslator; + List! args = new List(); + foreach (Expr! expr in naryExpr.Args) + { + LiteralExpr litExpr = expr as LiteralExpr; + if (litExpr != null) + { + args.Add(errModel.valueToPartition[litExpr.Val]); + continue; + } + + IdentifierExpr idExpr = expr as IdentifierExpr; + assert idExpr != null; + assert idExpr.Decl != null; + VCExprVar! var = boogieExprTranslator.LookupVariable(idExpr.Decl); + string! name = vcExprTranslator.Lookup(var); + args.Add(errModel.identifierToPartition[name]); + } + calleeCounterexamples[assumeCmd] = LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args); + #endregion } GotoCmd gotoCmd = transferCmd as GotoCmd; @@ -1834,7 +2197,7 @@ namespace VC { if (traceNodes.Contains(bb)){ trace.Add(bb); - return TraceCounterexample(bb, traceNodes, trace, errModel, incarnationOriginMap); + return TraceCounterexample(bb, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program); } } } @@ -2559,16 +2922,18 @@ namespace VC // } static VCExpr! LetVC(Block! startBlock, + Variable controlFlowVariable, Hashtable/**/! label2absy, ProverContext! proverCtxt) { Hashtable/**/! blockVariables = new Hashtable/**/(); List! bindings = new List(); - VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt); + VCExpr startCorrect = LetVC(startBlock, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt); return proverCtxt.ExprGen.Let(bindings, startCorrect); } static VCExpr! LetVC(Block! block, + Variable controlFlowVariable, Hashtable/**/! label2absy, Hashtable/**/! blockVariables, List! bindings, @@ -2591,13 +2956,20 @@ namespace VC assert gotocmd.labelTargets != null; List SuccCorrectVars = new List(gotocmd.labelTargets.Length); foreach (Block! successor in gotocmd.labelTargets) { - VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt); + VCExpr s = LetVC(successor, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt); + if (controlFlowVariable != null) + { + VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable); + VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(block.UniqueId))); + VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successor.UniqueId))); + s = gen.Implies(controlTransferExpr, s); + } SuccCorrectVars.Add(s); } SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars); } - VCContext context = new VCContext(label2absy, proverCtxt); + VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable); VCExpr vc = Wlp.Block(block, SuccCorrect, context); v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool); diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc index e70b332f..38aa6af8 100644 --- a/Source/VCGeneration/Wlp.ssc +++ b/Source/VCGeneration/Wlp.ssc @@ -8,12 +8,15 @@ using System.Collections; using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; using Microsoft.Contracts; +using System.Collections.Generic; +using Microsoft.Basetypes; namespace VC { public class VCContext { [Rep] public readonly Hashtable/**/! Label2absy; [Rep] public readonly ProverContext! Ctxt; + public readonly Variable ControlFlowVariable; public VCContext(Hashtable/**/! label2absy, ProverContext! ctxt) { @@ -21,6 +24,13 @@ namespace VC { this.Ctxt = ctxt; // base(); } + + public VCContext(Hashtable/**/! label2absy, ProverContext! ctxt, Variable controlFlowVariable) + { + this.Label2absy = label2absy; + this.Ctxt = ctxt; + this.ControlFlowVariable = controlFlowVariable; + } } #region A class to compute wlp of a passive command program @@ -41,7 +51,10 @@ namespace VC { int id = b.UniqueId; expose (ctxt) { ctxt.Label2absy[id] = b; - return gen.Implies(gen.LabelPos((!)id.ToString(), VCExpressionGenerator.True), res); + if (ctxt.ControlFlowVariable != null) + return res; + else + return gen.Implies(gen.LabelPos((!)id.ToString(), VCExpressionGenerator.True), res); } } @@ -73,11 +86,26 @@ namespace VC { default: assert false; // unexpected case } -// (MSchaef) Hack: This line might be useless, but at least it is not harmfull -// need to test it - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) return gen.Implies(C, N); - - return gen.AndSimp(gen.LabelNeg((!)id.ToString(), C), N); + + // (MSchaef) Hack: This line might be useless, but at least it is not harmfull + // need to test it + if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) + return gen.Implies(C, N); + + if (ctxt.ControlFlowVariable != null) + { + VCExpr! controlFlowVariableExpr = + ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable); + VCExpr! controlFlowFunctionAppl1 = + gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id))); + VCExpr! controlFlowFunctionAppl2 = + gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id))); + VCExpr! assertFailure = gen.Eq(controlFlowFunctionAppl1, gen.Integer(BigNum.FromInt(0))); + VCExpr! assertSuccess = gen.Neq(controlFlowFunctionAppl2, gen.Integer(BigNum.FromInt(0))); + return gen.And(gen.Implies(assertFailure, C), gen.Implies(assertSuccess, N)); + } + else + return gen.AndSimp(gen.LabelNeg((!)id.ToString(), C), N); } } else if (cmd is AssumeCmd) { -- cgit v1.2.3