From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/VCGeneration/ConditionGeneration.cs | 4026 ++++++++++++++-------------- 1 file changed, 2041 insertions(+), 1985 deletions(-) (limited to 'Source/VCGeneration/ConditionGeneration.cs') diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 515ec16d..19438924 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1,1985 +1,2041 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Linq; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using System.Threading; -using System.IO; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; -using Set = Microsoft.Boogie.GSet; - -namespace Microsoft.Boogie { - - public class CalleeCounterexampleInfo { - public Counterexample counterexample; - public List/*!>!*/ args; - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(args)); - } - - public CalleeCounterexampleInfo(Counterexample cex, List!*/> x) - { - Contract.Requires(cce.NonNullElements(x)); - counterexample = cex; - args = x; - } - } - - public class TraceLocation : IEquatable - { - public int numBlock; - public int numInstr; - - public TraceLocation(int numBlock, int numInstr) - { - this.numBlock = numBlock; - this.numInstr = numInstr; - } - - public override bool Equals(object obj) - { - TraceLocation that = obj as TraceLocation; - if (that == null) return false; - return (numBlock == that.numBlock && numInstr == that.numInstr); - } - - public bool Equals(TraceLocation that) - { - return (numBlock == that.numBlock && numInstr == that.numInstr); - } - - public override int GetHashCode() - { - return numBlock.GetHashCode() ^ 131 * numInstr.GetHashCode(); - } - } - - public abstract class Counterexample { - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Trace != null); - Contract.Invariant(Context != null); - Contract.Invariant(cce.NonNullElements(relatedInformation)); - Contract.Invariant(cce.NonNullDictionaryAndValues(calleeCounterexamples)); - } - - [Peer] - public List Trace; - public Model Model; - public VC.ModelViewInfo MvInfo; - public ProverContext Context; - [Peer] - public List/*!>!*/ relatedInformation; - public string OriginalRequestId; - public string RequestId; - public abstract byte[] Checksum { get; } - public byte[] SugaredCmdChecksum; - - public Dictionary calleeCounterexamples; - - internal Counterexample(List trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) { - Contract.Requires(trace != null); - Contract.Requires(context != null); - this.Trace = trace; - this.Model = model; - this.MvInfo = mvInfo; - this.Context = context; - this.relatedInformation = new List(); - this.calleeCounterexamples = new Dictionary(); - } - - // Create a shallow copy of the counterexample - public abstract Counterexample Clone(); - - public void AddCalleeCounterexample(TraceLocation loc, CalleeCounterexampleInfo cex) - { - Contract.Requires(cex != null); - calleeCounterexamples[loc] = cex; - } - - public void AddCalleeCounterexample(int numBlock, int numInstr, CalleeCounterexampleInfo cex) - { - Contract.Requires(cex != null); - calleeCounterexamples[new TraceLocation(numBlock, numInstr)] = cex; - } - - public void AddCalleeCounterexample(Dictionary cs) - { - Contract.Requires(cce.NonNullDictionaryAndValues(cs)); - foreach (TraceLocation loc in cs.Keys) - { - AddCalleeCounterexample(loc, cs[loc]); - } - } - - // Looks up the Cmd at a given index into the trace - public Cmd getTraceCmd(TraceLocation loc) - { - Debug.Assert(loc.numBlock < Trace.Count); - Block b = Trace[loc.numBlock]; - Debug.Assert(loc.numInstr < b.Cmds.Count); - return b.Cmds[loc.numInstr]; - } - - // Looks up the name of the called procedure. - // Asserts that the name exists - public string getCalledProcName(Cmd cmd) - { - // There are two options: - // 1. cmd is a CallCmd - // 2. cmd is an AssumeCmd (passified version of a CallCmd) - if(cmd is CallCmd) { - return (cmd as CallCmd).Proc.Name; - } - AssumeCmd assumeCmd = cmd as AssumeCmd; - Debug.Assert(assumeCmd != null); - - NAryExpr naryExpr = assumeCmd.Expr as NAryExpr; - Debug.Assert(naryExpr != null); - - return naryExpr.Fun.FunctionName; - } - - public void Print(int indent, TextWriter tw, Action blockAction = null) { - int numBlock = -1; - string ind = new string(' ', indent); - foreach (Block b in Trace) { - Contract.Assert(b != null); - numBlock++; - if (b.tok == null) { - tw.WriteLine("{0}", ind); - } 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)) { - if (blockAction != null) - { - blockAction(b); - } - - tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind); - - for (int numInstr = 0; numInstr < b.Cmds.Count; numInstr++) - { - var loc = new TraceLocation(numBlock, numInstr); - if (calleeCounterexamples.ContainsKey(loc)) - { - var cmd = getTraceCmd(loc); - var calleeName = getCalledProcName(cmd); - if (calleeName.StartsWith(VC.StratifiedVCGen.recordProcName) && CommandLineOptions.Clo.StratifiedInlining > 0) - { - Contract.Assert(calleeCounterexamples[loc].args.Count == 1); - var arg = calleeCounterexamples[loc].args[0]; - tw.WriteLine("{0}value = {1}", ind, arg.ToString()); - } - else - { - tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind); - calleeCounterexamples[loc].counterexample.Print(indent + 4, tw); - tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind); - } - } - } - } - } - } - } - - public static bool firstModelFile = true; - - public bool ModelHasStatesAlready = false; - - public void PrintModel(TextWriter tw) - { - var filename = CommandLineOptions.Clo.ModelViewFile; - if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return; - - if (!ModelHasStatesAlready) { - PopulateModelWithStates(); - ModelHasStatesAlready = true; - } - - if (filename == "-") { - Model.Write(tw); - tw.Flush(); - } else { - using (var wr = new StreamWriter(filename, !firstModelFile)) { - firstModelFile = false; - Model.Write(wr); - } - } - } - - void ApplyRedirections(Model m) { - var mapping = new Dictionary(); - foreach (var name in new string[] { "U_2_bool", "U_2_int" }) { - Model.Func f = m.TryGetFunc(name); - if (f != null && f.Arity == 1) { - foreach (var ft in f.Apps) mapping[ft.Args[0]] = ft.Result; - } - } - m.Substitute(mapping); - } - - public void PopulateModelWithStates() - { - Contract.Requires(Model != null); - - Model m = Model; - ApplyRedirections(m); - - var mvstates = m.TryGetFunc("$mv_state"); - if (MvInfo == null || mvstates == null || (mvstates.Arity == 1 && mvstates.Apps.Count() == 0)) - return; - - Contract.Assert(mvstates.Arity == 2); - - foreach (Variable v in MvInfo.AllVariables) { - m.InitialState.AddBinding(v.Name, GetModelValue(m, v)); - } - - var states = new List(); - foreach (var t in mvstates.Apps) - states.Add(t.Args[1].AsInt()); - - states.Sort(); - - for (int i = 0; i < states.Count; ++i) { - var s = states[i]; - if (0 <= s && s < MvInfo.CapturePoints.Count) { - VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s]; - var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Dictionary(); - var cs = m.MkState(map.Description); - - foreach (Variable v in MvInfo.AllVariables) { - Expr e = map.IncarnationMap.ContainsKey(v) ? map.IncarnationMap[v] : null; - if (e == null) continue; - - Expr prevIncV = prevInc.ContainsKey(v) ? prevInc[v] : null; - if (prevIncV == e) continue; // skip unchanged variables - - Model.Element elt; - - if (e is IdentifierExpr) { - IdentifierExpr ide = (IdentifierExpr)e; - elt = GetModelValue(m, ide.Decl); - } else if (e is LiteralExpr) { - LiteralExpr lit = (LiteralExpr)e; - elt = m.MkElement(lit.Val.ToString()); - } else { - elt = m.MkFunc(e.ToString(), 0).GetConstant(); - } - - cs.AddBinding(v.Name, elt); - } - - } else { - Contract.Assume(false); - } - } - } - - private Model.Element GetModelValue(Model m, Variable v) { - Model.Element elt; - // first, get the unique name - string uniqueName; - VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v); - if (vvar == null) { - uniqueName = v.Name; - } else { - uniqueName = Context.Lookup(vvar); - } - - var f = m.TryGetFunc(uniqueName); - if (f == null) { - f = m.MkFunc(uniqueName, 0); - } - elt = f.GetConstant(); - return elt; - } - - public abstract int GetLocation(); - } - - public class CounterexampleComparer : IComparer { - - private int Compare(List bs1, List bs2) - { - if (bs1.Count < bs2.Count) - { - return -1; - } - else if (bs2.Count < bs1.Count) - { - return 1; - } - - for (int i = 0; i < bs1.Count; i++) - { - var b1 = bs1[i]; - var b2 = bs2[i]; - if (b1.tok.pos < b2.tok.pos) - { - return -1; - } - else if (b2.tok.pos < b1.tok.pos) - { - return 1; - } - } - - return 0; - } - - public int Compare(Counterexample c1, Counterexample c2) - { - //Contract.Requires(c1 != null); - //Contract.Requires(c2 != null); - if (c1.GetLocation() == c2.GetLocation()) - { - var c = Compare(c1.Trace, c2.Trace); - if (c != 0) - { - return c; - } - // TODO(wuestholz): Generalize this to compare all IPotentialErrorNodes of the counterexample. - var a1 = c1 as AssertCounterexample; - var a2 = c2 as AssertCounterexample; - if (a1 != null && a2 != null) - { - var s1 = a1.FailingAssert.ErrorData as string; - var s2 = a2.FailingAssert.ErrorData as string; - if (s1 != null && s2 != null) - { - return s1.CompareTo(s2); - } - } - - return 0; - } - if (c1.GetLocation() > c2.GetLocation()) - { - return 1; - } - return -1; - } - } - - public class AssertCounterexample : Counterexample { - [Peer] - public AssertCmd FailingAssert; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(FailingAssert != null); - } - - - public AssertCounterexample(List trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context) - : base(trace, model, mvInfo, context) { - Contract.Requires(trace != null); - Contract.Requires(failingAssert != null); - Contract.Requires(context != null); - this.FailingAssert = failingAssert; - } - - public override int GetLocation() { - return FailingAssert.tok.line * 1000 + FailingAssert.tok.col; - } - - public override byte[] Checksum - { - get { return FailingAssert.Checksum; } - } - - public override Counterexample Clone() - { - var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo, Context); - ret.calleeCounterexamples = calleeCounterexamples; - return ret; - } - } - - public class CallCounterexample : Counterexample { - public CallCmd FailingCall; - public Requires FailingRequires; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(FailingCall != null); - Contract.Invariant(FailingRequires != null); - } - - - public CallCounterexample(List trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum = null) - : base(trace, model, mvInfo, context) { - Contract.Requires(!failingRequires.Free); - Contract.Requires(trace != null); - Contract.Requires(context != null); - Contract.Requires(failingCall != null); - Contract.Requires(failingRequires != null); - this.FailingCall = failingCall; - this.FailingRequires = failingRequires; - this.checksum = checksum; - this.SugaredCmdChecksum = failingCall.Checksum; - } - - public override int GetLocation() { - return FailingCall.tok.line * 1000 + FailingCall.tok.col; - } - - byte[] checksum; - public override byte[] Checksum - { - get { return checksum; } - } - - public override Counterexample Clone() - { - var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context, Checksum); - ret.calleeCounterexamples = calleeCounterexamples; - return ret; - } - } - - public class ReturnCounterexample : Counterexample { - public TransferCmd FailingReturn; - public Ensures FailingEnsures; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(FailingEnsures != null); - Contract.Invariant(FailingReturn != null); - } - - - public ReturnCounterexample(List trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum) - : base(trace, model, mvInfo, context) { - Contract.Requires(trace != null); - Contract.Requires(context != null); - Contract.Requires(failingReturn != null); - Contract.Requires(failingEnsures != null); - Contract.Requires(!failingEnsures.Free); - this.FailingReturn = failingReturn; - this.FailingEnsures = failingEnsures; - this.checksum = checksum; - } - - public override int GetLocation() { - return FailingReturn.tok.line * 1000 + FailingReturn.tok.col; - } - - byte[] checksum; - - /// - /// Returns the checksum of the corresponding assertion. - /// - public override byte[] Checksum - { - get - { - return checksum; - } - } - - public override Counterexample Clone() - { - var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context, checksum); - ret.calleeCounterexamples = calleeCounterexamples; - return ret; - } - } - - public class VerifierCallback { - // reason == null means this is genuine counterexample returned by the prover - // other reason means it's time out/memory out/crash - public virtual void OnCounterexample(Counterexample ce, string/*?*/ reason) { - Contract.Requires(ce != null); - } - - // called in case resource is exceeded and we don't have counterexample - public virtual void OnTimeout(string reason) { - Contract.Requires(reason != null); - } - - public virtual void OnOutOfMemory(string reason) { - Contract.Requires(reason != null); - } - - public virtual void OnProgress(string phase, int step, int totalSteps, double progressEstimate) { - } - - public virtual void OnUnreachableCode(Implementation impl) { - Contract.Requires(impl != null); - } - - public virtual void OnWarning(string msg) { - Contract.Requires(msg != null); - switch (CommandLineOptions.Clo.PrintProverWarnings) { - case CommandLineOptions.ProverWarnings.None: - break; - case CommandLineOptions.ProverWarnings.Stdout: - Console.WriteLine("Prover warning: " + msg); - break; - case CommandLineOptions.ProverWarnings.Stderr: - Console.Error.WriteLine("Prover warning: " + msg); - break; - default: - Contract.Assume(false); - throw new cce.UnreachableException(); // unexpected case - } - } - } -} - -//////////////////////////////////////////// - -namespace VC { - using Bpl = Microsoft.Boogie; - - public class VCGenException : Exception { - public VCGenException(string s) - : base(s) { - } - } - [ContractClassFor(typeof(ConditionGeneration))] - public abstract class ConditionGenerationContracts : ConditionGeneration { - public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) { - Contract.Requires(impl != null); - Contract.Requires(callback != null); - Contract.EnsuresOnThrow(true); - throw new NotImplementedException(); - } - public ConditionGenerationContracts(Program p, List checkers) - : base(p, checkers) { - } - } - - [ContractClass(typeof(ConditionGenerationContracts))] - public abstract class ConditionGeneration : IDisposable { - protected internal object CheckerCommonState; - - public enum Outcome { - Correct, - Errors, - TimedOut, - OutOfMemory, - Inconclusive, - ReachedBound - } - - public static Outcome ProverInterfaceOutcomeToConditionGenerationOutcome(ProverInterface.Outcome outcome) { - switch (outcome) { - 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; - case ProverInterface.Outcome.Valid: - return Outcome.Correct; - } - return Outcome.Inconclusive; // unreachable but the stupid compiler does not understand - } - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(checkers)); - Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap)); - Contract.Invariant(program != null); - } - - public int CumulativeAssertionCount; // for statistics - - protected readonly List/*!>!*/ checkers; - - private bool _disposed; - - protected Implementation currentImplementation; - - protected List CurrentLocalVariables = null; - - // shared across each implementation; created anew for each implementation - protected Dictionary variable2SequenceNumber; - public Dictionary/*!>!*/ incarnationOriginMap = new Dictionary(); - - public Program program; - protected string/*?*/ logFilePath; - protected bool appendLogFile; - - public static List errorModelList; - - public ConditionGeneration(Program p, List checkers) { - Contract.Requires(p != null && checkers != null && cce.NonNullElements(checkers)); - program = p; - this.checkers = checkers; - Cores = 1; - } - - /// - /// Takes an implementation and constructs a verification condition and sends - /// it to the theorem prover. - /// Returns null if "impl" is correct. Otherwise, returns a list of counterexamples, - /// each counterexample consisting of an array of labels. - /// - /// - public Outcome VerifyImplementation(Implementation impl, out List/*?*/ errors, string requestId = null) { - Contract.Requires(impl != null); - - Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null)); - Contract.Ensures(Contract.Result() != Outcome.Errors || errors != null); - Contract.EnsuresOnThrow(true); - Helpers.ExtraTraceInformation("Starting implementation verification"); - - CounterexampleCollector collector = new CounterexampleCollector(); - collector.RequestId = requestId; - Outcome outcome = VerifyImplementation(impl, collector); - if (outcome == Outcome.Errors || outcome == Outcome.TimedOut || outcome == Outcome.OutOfMemory) { - errors = collector.examples; - } else { - errors = null; - } - - Helpers.ExtraTraceInformation("Finished implementation verification"); - return outcome; - } - - /// - /// Takes an implementation and constructs a verification condition and sends - /// it to the theorem prover. - /// Returns null if "impl" is correct. Otherwise, returns a list of counterexamples, - /// each counterexample consisting of an array of labels. - /// - /// - public Outcome VerifyImplementation(Implementation impl, out List errors, out List errorsModel) - { - Contract.Ensures(Contract.Result() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null); - Contract.EnsuresOnThrow(true); - List errorsOut; - - Outcome outcome; - errorModelList = new List(); - outcome = VerifyImplementation(impl, out errorsOut); - errors = errorsOut; - errorsModel = errorModelList; - - return outcome; - } - - public abstract Outcome VerifyImplementation(Implementation impl, VerifierCallback callback); - - /////////////////////////////////// Common Methods and Classes ////////////////////////////////////////// - - #region Methods for injecting pre- and postconditions - private static void - ThreadInCodeExpr(Implementation impl, - Block targetBlock, - CodeExpr codeExpr, - bool replaceWithAssert, - TokenTextWriter debugWriter) { - Contract.Requires(impl != null); - Contract.Requires(codeExpr != null); - Contract.Requires(targetBlock != null); - // Go through codeExpr and for all blocks that have a "return e" - // as their transfer command: - // Replace all "return e" with "assert/assume e" - // Change the transfer command to "goto targetBlock" - // Then add all of the blocks in codeExpr to the implementation (at the end) - foreach (Block b in codeExpr.Blocks) { - Contract.Assert(b != null); - ReturnExprCmd rec = b.TransferCmd as ReturnExprCmd; - if (rec != null) { // otherwise it is a goto command - if (replaceWithAssert) { - Ensures ens = new Ensures(rec.tok, false, rec.Expr, null); - Contract.Assert(ens != null); - Cmd c = new AssertEnsuresCmd(ens); - Contract.Assert(c != null); - b.Cmds.Add(c); - } else { - b.Cmds.Add(new AssumeCmd(rec.tok, rec.Expr)); - } - b.TransferCmd = new GotoCmd(Token.NoToken, - new List { targetBlock.Label }, - new List { targetBlock }); - targetBlock.Predecessors.Add(b); - } - impl.Blocks.Add(b); - } - if (debugWriter != null) { - codeExpr.Emit(debugWriter, 1, false); - } - return; - } - - private static void AddAsPrefix(Block b, List cs) { - Contract.Requires(b != null); - Contract.Requires(cs != null); - List newCommands = new List(); - newCommands.AddRange(cs); - newCommands.AddRange(b.Cmds); - b.Cmds = newCommands; - } - - - /// - /// Modifies an implementation by prepending it with startCmds and then, as assume - /// statements, all preconditions. Insert new blocks as needed, and adjust impl.Blocks[0] - /// accordingly to make it the new implementation entry block. - /// - /// - /// - protected static void InjectPreconditions(Implementation impl, [Captured] List startCmds) { - Contract.Requires(impl != null); - Contract.Requires(startCmds != null); - Contract.Requires(impl.Proc != null); - - TokenTextWriter debugWriter = null; - if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { - debugWriter = new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false); - debugWriter.WriteLine("Effective precondition:"); - } - - Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); - string blockLabel = "PreconditionGeneratedEntry"; - - Block origStartBlock = impl.Blocks[0]; - Block insertionPoint = new Block( - new Token(-17, -4), blockLabel, startCmds, - new GotoCmd(Token.NoToken, new List { origStartBlock.Label }, new List { origStartBlock })); - - impl.Blocks[0] = insertionPoint; // make insertionPoint the start block - impl.Blocks.Add(origStartBlock); // and put the previous start block at the end of the list - - // (free and checked) requires clauses - foreach (Requires req in impl.Proc.Requires) - // invariant: insertionPoint.TransferCmd is "goto origStartBlock;", but origStartBlock.Predecessors has not yet been updated - { - Contract.Assert(req != null); - Expr e = Substituter.Apply(formalProcImplSubst, req.Condition); - Cmd c = new AssumeCmd(req.tok, e); - insertionPoint.Cmds.Add(c); - if (debugWriter != null) { - c.Emit(debugWriter, 1); - } - } - origStartBlock.Predecessors.Add(insertionPoint); - - if (debugWriter != null) { - debugWriter.WriteLine(); - } - } - /// - /// Modifies an implementation by inserting all postconditions - /// as assert statements at the end of the implementation - /// Returns the possibly-new unified exit block of the implementation - /// - /// - /// The unified exit block that has - /// already been constructed for the implementation (and so - /// is already an element of impl.Blocks) - /// - protected static void InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary gotoCmdOrigins) { - Contract.Requires(impl != null); - Contract.Requires(unifiedExitBlock != null); - Contract.Requires(gotoCmdOrigins != null); - Contract.Requires(impl.Proc != null); - Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd); - - TokenTextWriter debugWriter = null; - if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { - debugWriter = new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false); - debugWriter.WriteLine("Effective postcondition:"); - } - - Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); - - // (free and checked) ensures clauses - foreach (Ensures ens in impl.Proc.Ensures) { - Contract.Assert(ens != null); - if (!ens.Free) { // skip free ensures clauses - Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); - Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone()); - ensCopy.Condition = e; - AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); - c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; - unifiedExitBlock.Cmds.Add(c); - if (debugWriter != null) { - c.Emit(debugWriter, 1); - } - } - } - - if (debugWriter != null) { - debugWriter.WriteLine(); - } - } - - - /// - /// Get the pre-condition of an implementation, including the where clauses from the in-parameters. - /// - /// - protected static List GetPre(Implementation impl) { - Contract.Requires(impl != null); - Contract.Requires(impl.Proc != null); - Contract.Ensures(Contract.Result>() != null); - - - TokenTextWriter debugWriter = null; - if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { - debugWriter = new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false); - debugWriter.WriteLine("Effective precondition:"); - } - - Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); - List pre = new List(); - - // (free and checked) requires clauses - foreach (Requires req in impl.Proc.Requires) { - Contract.Assert(req != null); - Expr e = Substituter.Apply(formalProcImplSubst, req.Condition); - Contract.Assert(e != null); - Cmd c = new AssumeCmd(req.tok, e); - Contract.Assert(c != null); - pre.Add(c); - - if (debugWriter != null) { - c.Emit(debugWriter, 1); - } - } - - if (debugWriter != null) { - debugWriter.WriteLine(); - } - - return pre; - } - - /// - /// Get the post-condition of an implementation. - /// - /// - protected static List GetPost(Implementation impl) { - - - Contract.Requires(impl != null); - Contract.Requires(impl.Proc != null); - Contract.Ensures(Contract.Result>() != null); - if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { - Console.WriteLine("Effective postcondition:"); - } - - // Construct an Expr for the post-condition - Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); - List post = new List(); - foreach (Ensures ens in impl.Proc.Ensures) { - Contract.Assert(ens != null); - if (!ens.Free) { - Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); - Contract.Assert(e != null); - Ensures ensCopy = cce.NonNull((Ensures)ens.Clone()); - ensCopy.Condition = e; - Cmd c = new AssertEnsuresCmd(ensCopy); - ((AssertEnsuresCmd)c).ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; - post.Add(c); - - if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { - c.Emit(new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false), 1); - } - } - } - - if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { - Console.WriteLine(); - } - - return post; - } - - /// - /// Get the where clauses from the in- and out-parameters as - /// a sequence of assume commands. - /// As a side effect, this method adds these where clauses to the out parameters. - /// - /// - protected static List GetParamWhereClauses(Implementation impl) { - Contract.Requires(impl != null); - Contract.Requires(impl.Proc != null); - Contract.Ensures(Contract.Result>() != null); - TokenTextWriter debugWriter = null; - if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { - debugWriter = new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false); - debugWriter.WriteLine("Effective precondition from where-clauses:"); - } - - Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); - List whereClauses = new List(); - - // where clauses of in-parameters - foreach (Formal f in impl.Proc.InParams) { - Contract.Assert(f != null); - if (f.TypedIdent.WhereExpr != null) { - Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr); - Cmd c = new AssumeCmd(f.tok, e); - whereClauses.Add(c); - - if (debugWriter != null) { - c.Emit(debugWriter, 1); - } - } - } - - // where clauses of out-parameters - Contract.Assert(impl.OutParams.Count == impl.Proc.OutParams.Count); - for (int i = 0; i < impl.OutParams.Count; i++) { - Variable f = cce.NonNull(impl.Proc.OutParams[i]); - if (f.TypedIdent.WhereExpr != null) { - Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr); - Cmd c = new AssumeCmd(f.tok, e); - whereClauses.Add(c); - - Variable fi = cce.NonNull(impl.OutParams[i]); - Contract.Assume(fi.TypedIdent.WhereExpr == null); - fi.TypedIdent.WhereExpr = e; - - if (debugWriter != null) { - c.Emit(debugWriter, 1); - } - } - } - - if (debugWriter != null) { - debugWriter.WriteLine(); - } - - return whereClauses; - } - - protected static void RestoreParamWhereClauses(Implementation impl) { - Contract.Requires(impl != null); - // 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) { - Contract.Assert(f != null); - f.TypedIdent.WhereExpr = null; - } - } - #endregion - - - protected Checker FindCheckerFor(int timeout, bool isBlocking = true) - { - Contract.Ensures(!isBlocking || Contract.Result() != null); - - var maxRetries = 3; - lock (checkers) - { - retry: - // Look for existing checker. - for (int i = 0; i < checkers.Count; i++) - { - var c = checkers[i]; - if (Monitor.TryEnter(c)) - { - try - { - if (c.WillingToHandle(timeout, program)) - { - c.GetReady(); - return c; - } - else if (c.IsIdle || c.IsClosed) - { - if (c.IsIdle) - { - c.Retarget(program, c.TheoremProver.Context, timeout); - c.GetReady(); - return c; - } - else - { - checkers.RemoveAt(i); - } - } - } - finally - { - Monitor.Exit(c); - } - } - } - - if (Cores <= checkers.Count) - { - if (isBlocking || 0 < maxRetries) - { - Monitor.Wait(checkers, 50); - maxRetries--; - goto retry; - } - else - { - return null; - } - } - - // Create a new checker. - string log = logFilePath; - if (log != null && !log.Contains("@PROC@") && checkers.Count > 0) - { - log = log + "." + checkers.Count; - } - Checker ch = new Checker(this, program, log, appendLogFile, timeout); - ch.GetReady(); - checkers.Add(ch); - return ch; - } - } - - - virtual public void Close() { - } - - - public class CounterexampleCollector : VerifierCallback { - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(examples)); - } - - public string RequestId; - - public readonly List/*!>!*/ examples = new List(); - public override void OnCounterexample(Counterexample ce, string/*?*/ reason) { - //Contract.Requires(ce != null); - if (RequestId != null) - { - ce.RequestId = RequestId; - } - if (ce.OriginalRequestId == null && 1 < CommandLineOptions.Clo.VerifySnapshots) - { - ce.OriginalRequestId = RequestId; - } - examples.Add(ce); - } - - public override void OnUnreachableCode(Implementation impl) { - //Contract.Requires(impl != null); - System.Console.WriteLine("found unreachable code:"); - EmitImpl(impl, false); - // TODO report error about next to last in seq - } - } - - protected static void EmitImpl(Implementation impl, bool printDesugarings) { - Contract.Requires(impl != null); - int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; - CommandLineOptions.Clo.PrintUnstructured = 2; // print only the unstructured program - bool oldPrintDesugaringSetting = CommandLineOptions.Clo.PrintDesugarings; - CommandLineOptions.Clo.PrintDesugarings = printDesugarings; - impl.Emit(new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false), 0); - CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting; - CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; - } - - - protected Block GenerateUnifiedExit(Implementation impl, Dictionary gotoCmdOrigins) { - Contract.Requires(impl != null); - Contract.Requires(gotoCmdOrigins != null); - Contract.Ensures(Contract.Result() != null); - - Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); - Block/*?*/ exitBlock = null; - #region Create a unified exit block, if there's more than one - { - int returnBlocks = 0; - foreach (Block b in impl.Blocks) { - if (b.TransferCmd is ReturnCmd) { - exitBlock = b; - returnBlocks++; - } - } - if (returnBlocks > 1) { - string unifiedExitLabel = "GeneratedUnifiedExit"; - Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(Token.NoToken)); - Contract.Assert(unifiedExit != null); - foreach (Block b in impl.Blocks) { - if (b.TransferCmd is ReturnCmd) { - List labels = new List(); - labels.Add(unifiedExitLabel); - List bs = new List(); - bs.Add(unifiedExit); - GotoCmd go = new GotoCmd(Token.NoToken, labels, bs); - gotoCmdOrigins[go] = (ReturnCmd)b.TransferCmd; - b.TransferCmd = go; - unifiedExit.Predecessors.Add(b); - } - } - - exitBlock = unifiedExit; - impl.Blocks.Add(unifiedExit); - } - Contract.Assert(exitBlock != null); - } - return exitBlock; - #endregion - } - - protected static void ResetPredecessors(List blocks) { - Contract.Requires(blocks != null); - foreach (Block b in blocks) { - Contract.Assert(b != null); - b.Predecessors = new List(); - } - foreach (Block b in blocks) { - Contract.Assert(b != null); - foreach (Block ch in Exits(b)) { - Contract.Assert(ch != null); - ch.Predecessors.Add(b); - } - } - } - - protected static IEnumerable Exits(Block b) { - Contract.Requires(b != null); - GotoCmd g = b.TransferCmd as GotoCmd; - if (g != null) { - return cce.NonNull(g.labelTargets); - } - return new List(); - } - - protected Variable CreateIncarnation(Variable x, Absy a) { - Contract.Requires(this.variable2SequenceNumber != null); - Contract.Requires(this.CurrentLocalVariables != null); - Contract.Requires(a is Block || a is AssignCmd || a is HavocCmd); - - Contract.Requires(x != null); - Contract.Ensures(Contract.Result() != null); - - int currentIncarnationNumber = - variable2SequenceNumber.ContainsKey(x) - ? - variable2SequenceNumber[x] - : - -1; - Variable v = new Incarnation(x, currentIncarnationNumber + 1); - variable2SequenceNumber[x] = currentIncarnationNumber + 1; - CurrentLocalVariables.Add(v); - incarnationOriginMap.Add((Incarnation)v, a); - return v; - } - - /// - /// Compute the incarnation map at the beginning of block "b" from the incarnation blocks of the - /// predecessors of "b". - /// - /// The predecessor map b.map for block "b" is defined as follows: - /// b.map.Domain == Union{Block p in b.predecessors; p.map.Domain} - /// Forall{Variable v in b.map.Domain; - /// b.map[v] == (v in Intersection{Block p in b.predecessors; p.map}.Domain - /// ? b.predecessors[0].map[v] - /// : new Variable())} - /// Every variable that b.map maps to a fresh variable requires a fixup in all predecessor blocks. - /// - /// - /// Gives incarnation maps for b's predecessors. - /// - protected Dictionary ComputeIncarnationMap(Block b, Dictionary> block2Incarnation) { - Contract.Requires(b != null); - Contract.Requires(block2Incarnation != null); - Contract.Ensures(Contract.Result>() != null); - - if (b.Predecessors.Count == 0) { - return new Dictionary(); - } - - Dictionary incarnationMap = null; - Set /*Variable*/ fixUps = new Set /*Variable*/ (); - foreach (Block pred in b.Predecessors) { - Contract.Assert(pred != null); - Contract.Assert(block2Incarnation.ContainsKey(pred)); // otherwise, Passive Transformation found a block whose predecessors have not been processed yet - Dictionary predMap = (Dictionary)block2Incarnation[pred]; - Contract.Assert(predMap != null); - if (incarnationMap == null) { - incarnationMap = new Dictionary(predMap); - continue; - } - - ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ (); - foreach (Variable v in incarnationMap.Keys) { - Contract.Assert(v != null); - if (!predMap.ContainsKey(v)) { - // conflict!! - conflicts.Add(v); - fixUps.Add(v); - } - } - // Now that we're done with enumeration, we'll do all the removes - foreach (Variable v in conflicts) { - Contract.Assert(v != null); - incarnationMap.Remove(v); - } - foreach (Variable v in predMap.Keys) { - Contract.Assert(v != null); - if (!incarnationMap.ContainsKey(v)) { - // v was not in the domain of the predecessors seen so far, so it needs to be fixed up - fixUps.Add(v); - } else { - // v in incarnationMap ==> all pred blocks (up to now) all agree on its incarnation - if (predMap[v] != incarnationMap[v]) { - // conflict!! - incarnationMap.Remove(v); - fixUps.Add(v); - } - } - } - } - - #region Second, for all variables in the fixups list, introduce a new incarnation and push it back into the preds. - foreach (Variable v in fixUps) { - Contract.Assert(v != null); - if (!b.IsLive(v)) - continue; - Variable v_prime = CreateIncarnation(v, b); - IdentifierExpr ie = new IdentifierExpr(v_prime.tok, v_prime); - Contract.Assert(incarnationMap != null); - incarnationMap[v] = ie; - foreach (Block pred in b.Predecessors) { - Contract.Assert(pred != null); - #region Create an assume command equating v_prime with its last incarnation in pred - #region Create an identifier expression for the last incarnation in pred - Dictionary predMap = (Dictionary)cce.NonNull(block2Incarnation[pred]); - - Expr pred_incarnation_exp; - Expr o = predMap.ContainsKey(v) ? predMap[v] : null; - if (o == null) { - Variable predIncarnation = v; - IdentifierExpr ie2 = new IdentifierExpr(predIncarnation.tok, predIncarnation); - pred_incarnation_exp = ie2; - } else { - pred_incarnation_exp = o; - } - #endregion - #region Create an identifier expression for the new incarnation - IdentifierExpr v_prime_exp = new IdentifierExpr(v_prime.tok, v_prime); - #endregion - #region Create the assume command itself - AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp, v_prime.Name.Contains("a##post##"))); - pred.Cmds.Add(ac); - #endregion - #endregion - } - } - #endregion - - Contract.Assert(incarnationMap != null); - return incarnationMap; - } - - Dictionary preHavocIncarnationMap = null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement - - protected void TurnIntoPassiveBlock(Block b, Dictionary incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst, MutableVariableCollector variableCollector, byte[] currentChecksum = null) { - Contract.Requires(b != null); - Contract.Requires(incarnationMap != null); - Contract.Requires(mvInfo != null); - Contract.Requires(oldFrameSubst != null); - #region Walk forward over the commands in this block and convert them to passive commands - - List passiveCmds = new List(); - foreach (Cmd c in b.Cmds) { - Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction - ChecksumHelper.ComputeChecksums(c, currentImplementation, variableCollector.UsedVariables, currentChecksum); - variableCollector.Visit(c); - currentChecksum = c.Checksum; - TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, b); - } - b.Checksum = currentChecksum; - b.Cmds = passiveCmds; - - if (b.TransferCmd is ReturnExprCmd) { - ReturnExprCmd rec = (ReturnExprCmd)b.TransferCmd.Clone(); - Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap); - rec.Expr = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, rec.Expr); - b.TransferCmd = rec; - } - #endregion - } - - protected Dictionary Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) { - Contract.Requires(impl != null); - Contract.Requires(mvInfo != null); - - currentImplementation = impl; - - var start = DateTime.UtcNow; - - Dictionary r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo); - - var end = DateTime.UtcNow; - - if (CommandLineOptions.Clo.TraceCachingForDebugging) - { - Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds); - } - - if (CommandLineOptions.Clo.TraceCachingForDebugging) - { - using (var tokTxtWr = new TokenTextWriter("", Console.Out, false, false)) - { - var pd = CommandLineOptions.Clo.PrintDesugarings; - var pu = CommandLineOptions.Clo.PrintUnstructured; - CommandLineOptions.Clo.PrintDesugarings = true; - CommandLineOptions.Clo.PrintUnstructured = 1; - impl.Emit(tokTxtWr, 0); - CommandLineOptions.Clo.PrintDesugarings = pd; - CommandLineOptions.Clo.PrintUnstructured = pu; - } - } - - currentImplementation = null; - - RestoreParamWhereClauses(impl); - - #region Debug Tracing - if (CommandLineOptions.Clo.TraceVerify) { - Console.WriteLine("after conversion to passive commands"); - EmitImpl(impl, true); - } - #endregion - - return r; - } - - protected Dictionary ConvertBlocks2PassiveCmd(List blocks, List modifies, ModelViewInfo mvInfo) { - Contract.Requires(blocks != null); - Contract.Requires(modifies != null); - Contract.Requires(mvInfo != null); - #region Convert to Passive Commands - - #region Topological sort -- need to process in a linearization of the partial order - Graph dag = new Graph(); - dag.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph - foreach (Block b in blocks) { - GotoCmd gtc = b.TransferCmd as GotoCmd; - if (gtc != null) { - Contract.Assume(gtc.labelTargets != null); - foreach (Block dest in gtc.labelTargets) { - Contract.Assert(dest != null); - dag.AddEdge(b, dest); - } - } - } - - IEnumerable sortedNodes; - if (CommandLineOptions.Clo.ModifyTopologicalSorting) { - sortedNodes = dag.TopologicalSort(true); - } else { - sortedNodes = dag.TopologicalSort(); - } - - Contract.Assert(sortedNodes != null); - #endregion - - Substitution oldFrameSubst = ComputeOldExpressionSubstitution(modifies); - - // 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. - Dictionary> block2Incarnation = new Dictionary>(); - Block exitBlock = null; - Dictionary exitIncarnationMap = null; - var variableCollectors = new Dictionary(); - foreach (Block b in sortedNodes) { - Contract.Assert(b != null); - Contract.Assert(!block2Incarnation.ContainsKey(b)); - Dictionary incarnationMap = ComputeIncarnationMap(b, block2Incarnation); - - // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out. - b.liveVarsBefore = null; - - // Decrement the succCount field in each predecessor. Once the field reaches zero in any block, - // all its successors have been passified. Consequently, its entry in block2Incarnation can be removed. - byte[] currentChecksum = null; - var mvc = new MutableVariableCollector(); - variableCollectors[b] = mvc; - foreach (Block p in b.Predecessors) { - p.succCount--; - if (p.Checksum != null) - { - // Compute the checksum based on the checksums of the predecessor. The order should not matter. - currentChecksum = ChecksumHelper.CombineChecksums(p.Checksum, currentChecksum, true); - } - mvc.AddUsedVariables(variableCollectors[p].UsedVariables); - if (p.succCount == 0) - block2Incarnation.Remove(p); - } - - #region Each block's map needs to be available to successor blocks - GotoCmd gotoCmd = b.TransferCmd as GotoCmd; - if (gotoCmd == null) { - b.succCount = 0; - } - else { - // incarnationMap needs to be added only if there is some successor of b - b.succCount = gotoCmd.labelNames.Count; - block2Incarnation.Add(b, incarnationMap); - } - #endregion Each block's map needs to be available to successor blocks - - TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst, mvc, currentChecksum); - exitBlock = b; - exitIncarnationMap = incarnationMap; - } - - variableCollectors.Clear(); - - // Verify that exitBlock is indeed the unique exit block - Contract.Assert(exitBlock != null); - Contract.Assert(exitBlock.TransferCmd is ReturnCmd); - #endregion Convert to Passive Commands - - return exitIncarnationMap; - } - - /// - /// Compute the substitution for old expressions. - /// - protected static Substitution ComputeOldExpressionSubstitution(List modifies) - { - Dictionary oldFrameMap = new Dictionary(); - foreach (IdentifierExpr ie in modifies) - { - Contract.Assert(ie != null); - if (!oldFrameMap.ContainsKey(cce.NonNull(ie.Decl))) - oldFrameMap.Add(ie.Decl, ie); - } - return Substituter.SubstitutionFromHashtable(oldFrameMap); - } - - public enum CachingAction : byte - { - DoNothingToAssert, - MarkAsPartiallyVerified, - MarkAsFullyVerified, - RecycleError, - AssumeNegationOfAssumptionVariable, - DropAssume - } - - public long[] CachingActionCounts; - - void TraceCachingAction(Cmd cmd, CachingAction action) - { - if (CommandLineOptions.Clo.TraceCachingForTesting) - { - using (var tokTxtWr = new TokenTextWriter("", Console.Out, false, false)) - { - var loc = cmd.tok != null && cmd.tok != Token.NoToken ? string.Format("{0}({1},{2})", cmd.tok.filename, cmd.tok.line, cmd.tok.col) : ""; - Console.Write("Processing command (at {0}) ", loc); - cmd.Emit(tokTxtWr, 0); - Console.Out.WriteLine(" >>> {0}", action); - } - } - - if (CommandLineOptions.Clo.TraceCachingForBenchmarking && CachingActionCounts != null) - { - Interlocked.Increment(ref CachingActionCounts[(int)action]); - } - } - - /// - /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc - /// Meanwhile, record any information needed to later reconstruct a model view. - /// - protected void TurnIntoPassiveCmd(Cmd c, Dictionary incarnationMap, Substitution oldFrameSubst, List passiveCmds, ModelViewInfo mvInfo, Block containingBlock) { - Contract.Requires(c != null); - Contract.Requires(incarnationMap != null); - Contract.Requires(oldFrameSubst != null); - Contract.Requires(passiveCmds != null); - Contract.Requires(mvInfo != null); - Contract.Requires(containingBlock != null); - - Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap); - #region assert/assume P |--> assert/assume P[x := in(x)], out := in - if (c is PredicateCmd) { - Contract.Assert(c is AssertCmd || c is AssumeCmd); // otherwise, unexpected PredicateCmd type - - PredicateCmd pc = (PredicateCmd)c.Clone(); - Contract.Assert(pc != null); - - Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr); - if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) { - string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState"); - if (description != null) { - Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new List { Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count) }); - copy = Bpl.Expr.And(mv, copy); - mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, new Dictionary(incarnationMap))); - } - } - Contract.Assert(copy != null); - var dropCmd = false; - var relevantAssumpVars = currentImplementation != null ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap) : new List(); - var relevantDoomedAssumpVars = currentImplementation != null ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap) : new List(); - var checksum = pc.Checksum; - if (pc is AssertCmd) { - var ac = (AssertCmd)pc; - ac.OrigExpr = ac.Expr; - Contract.Assert(ac.IncarnationMap == null); - ac.IncarnationMap = (Dictionary)cce.NonNull(new Dictionary(incarnationMap)); - - var subsumption = Wlp.Subsumption(ac); - if (relevantDoomedAssumpVars.Any()) - { - TraceCachingAction(pc, CachingAction.DoNothingToAssert); - } - else if (currentImplementation != null - && currentImplementation.HasCachedSnapshot - && checksum != null - && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum) - && !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum)) - { - if (!currentImplementation.AnyErrorsInCachedSnapshot - && currentImplementation.InjectedAssumptionVariables.Count == 1 - && relevantAssumpVars.Count == 1) - { - TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified); - } - else - { - bool isTrue; - var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue); - TraceCachingAction(pc, !isTrue ? CachingAction.MarkAsPartiallyVerified : CachingAction.MarkAsFullyVerified); - var litExpr = ac.Expr as LiteralExpr; - if (litExpr == null || !litExpr.IsTrue) - { - ac.MarkAsVerifiedUnder(assmVars); - } - else - { - dropCmd = true; - } - } - } - else if (currentImplementation != null - && currentImplementation.HasCachedSnapshot - && relevantAssumpVars.Count == 0 - && checksum != null - && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum) - && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum)) - { - TraceCachingAction(pc, CachingAction.RecycleError); - ac.MarkAsVerifiedUnder(Expr.True); - currentImplementation.AddRecycledFailingAssertion(ac); - pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List(), pc.Attributes); - } - else - { - TraceCachingAction(pc, CachingAction.DoNothingToAssert); - } - } - else if (pc is AssumeCmd - && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot") - && pc.SugaredCmdChecksum != null) - { - if (!relevantDoomedAssumpVars.Any() - && currentImplementation.HasCachedSnapshot - && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.SugaredCmdChecksum) - && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.SugaredCmdChecksum)) - { - bool isTrue; - var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue); - if (!isTrue) - { - copy = LiteralExpr.Imp(assmVars, copy); - TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified); - } - else - { - TraceCachingAction(pc, CachingAction.MarkAsFullyVerified); - } - } - else - { - TraceCachingAction(pc, CachingAction.DropAssume); - dropCmd = true; - } - } - else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization")) - { - var identExpr = pc.Expr as IdentifierExpr; - if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl)) - { - incarnationMap[identExpr.Decl] = LiteralExpr.True; - dropCmd = true; - } - } - pc.Expr = copy; - if (!dropCmd) - { - passiveCmds.Add(pc); - } - } - #endregion - #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below] - else if (c is AssignCmd) { - AssignCmd assign = ((AssignCmd)c).AsSimpleAssignCmd; // first remove map assignments - Contract.Assert(assign != null); - #region Substitute all variables in E with the current map - List copies = new List(); - foreach (Expr e in assign.Rhss) { - Contract.Assert(e != null); - copies.Add(Substituter.ApplyReplacingOldExprs(incarnationSubst, - oldFrameSubst, - e)); - } - #endregion - - List!*/> assumptions = new List(); - // it might be too slow to create a new dictionary each time ... - IDictionary newIncarnationMappings = - new Dictionary(); - - for (int i = 0; i < assign.Lhss.Count; ++i) { - IdentifierExpr lhsIdExpr = - cce.NonNull((SimpleAssignLhs)assign.Lhss[i]).AssignedVariable; - Variable lhs = cce.NonNull(lhsIdExpr.Decl); - Contract.Assert(lhs != null); - Expr rhs = assign.Rhss[i]; - Contract.Assert(rhs != null); - - // don't create incarnations for assignments of literals or single variables. - if (rhs is LiteralExpr) { - incarnationMap[lhs] = rhs; - } else if (rhs is IdentifierExpr) { - IdentifierExpr ie = (IdentifierExpr)rhs; - if (incarnationMap.ContainsKey(cce.NonNull(ie.Decl))) - newIncarnationMappings[lhs] = cce.NonNull((Expr)incarnationMap[ie.Decl]); - else - newIncarnationMappings[lhs] = ie; - } else { - IdentifierExpr x_prime_exp = null; - #region Make a new incarnation, x', for variable x, but only if x is *not* already an incarnation - if (lhs is Incarnation) { - // incarnations are already written only once, no need to make an incarnation of an incarnation - x_prime_exp = lhsIdExpr; - } else { - Variable v = CreateIncarnation(lhs, c); - x_prime_exp = new IdentifierExpr(lhsIdExpr.tok, v); - newIncarnationMappings[lhs] = x_prime_exp; - } - #endregion - - var nAryExpr = copies[i] as NAryExpr; - if (nAryExpr != null) - { - var binOp = nAryExpr.Fun as BinaryOperator; - if (binOp != null - && binOp.Op == BinaryOperator.Opcode.And) - { - var arg0 = nAryExpr.Args[0] as LiteralExpr; - var arg1 = nAryExpr.Args[1] as LiteralExpr; - if ((arg0 != null && arg0.IsTrue) || (arg1 != null && arg1.IsFalse)) - { - // Replace the expressions "true && arg1" or "arg0 && false" by "arg1". - copies[i] = nAryExpr.Args[1]; - } - } - } - - #region Create an assume command with the new variable - assumptions.Add(TypedExprEq(x_prime_exp, copies[i], x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##post##"))); - #endregion - } - } - - foreach (KeyValuePair pair in newIncarnationMappings) { - Contract.Assert(pair.Key != null && pair.Value != null); - incarnationMap[pair.Key] = pair.Value; - } - - if (assumptions.Count > 0) { - Expr assumption = assumptions[0]; - - for (int i = 1; i < assumptions.Count; ++i) { - Contract.Assert(assumption != null); - assumption = Expr.And(assumption, assumptions[i]); - } - passiveCmds.Add(new AssumeCmd(c.tok, assumption)); - } - - if (currentImplementation != null - && currentImplementation.HasCachedSnapshot - && !currentImplementation.AnyErrorsInCachedSnapshot - && currentImplementation.InjectedAssumptionVariables.Count == 1 - && assign.Lhss.Count == 1) - { - var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr; - Expr incarnation; - if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && incarnationMap.TryGetValue(identExpr.Decl, out incarnation)) - { - TraceCachingAction(assign, CachingAction.AssumeNegationOfAssumptionVariable); - passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation))); - } - } - } - #endregion - #region havoc w |--> assume whereClauses, out := in( w |-> w' ) - else if (c is HavocCmd) { - if (this.preHavocIncarnationMap == null) // Save a copy of the incarnation map (at the top of a sequence of havoc statements) - this.preHavocIncarnationMap = new Dictionary(incarnationMap); - - HavocCmd hc = (HavocCmd)c; - Contract.Assert(c != null); - // If an assumption variable for postconditions is included here, it must have been assigned within a loop. - // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop - // invariant) in the previous snapshot and are therefore not going refer to the assumption variable after - // the loop. We can achieve this by simply not updating/adding it in the incarnation map. - List havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##post##"))).ToList(); - // First, compute the new incarnations - foreach (IdentifierExpr ie in havocVars) { - Contract.Assert(ie != null); - if (!(ie.Decl is Incarnation)) { - Variable x = cce.NonNull(ie.Decl); - Variable x_prime = CreateIncarnation(x, c); - incarnationMap[x] = new IdentifierExpr(x_prime.tok, x_prime); - } - } - // Then, perform the assume of the where clauses, using the updated incarnations - Substitution updatedIncarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap); - foreach (IdentifierExpr ie in havocVars) { - Contract.Assert(ie != null); - if (!(ie.Decl is Incarnation)) { - Variable x = cce.NonNull(ie.Decl); - Bpl.Expr w = x.TypedIdent.WhereExpr; - if (w != null) { - Expr copy = Substituter.ApplyReplacingOldExprs(updatedIncarnationSubst, oldFrameSubst, w); - passiveCmds.Add(new AssumeCmd(c.tok, copy)); - } - } - } - } - #endregion - else if (c is CommentCmd) { - // comments are just for debugging and don't affect verification - } else if (c is SugaredCmd) { - SugaredCmd sug = (SugaredCmd)c; - Contract.Assert(sug != null); - Cmd cmd = sug.Desugaring; - Contract.Assert(cmd != null); - TurnIntoPassiveCmd(cmd, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, containingBlock); - } else if (c is StateCmd) { - this.preHavocIncarnationMap = null; // we do not need to remeber the previous incarnations - StateCmd st = (StateCmd)c; - Contract.Assert(st != null); - // account for any where clauses among the local variables - foreach (Variable v in st.Locals) { - Contract.Assert(v != null); - Expr w = v.TypedIdent.WhereExpr; - if (w != null) { - passiveCmds.Add(new AssumeCmd(v.tok, w)); - } - } - // do the sub-commands - foreach (Cmd s in st.Cmds) { - Contract.Assert(s != null); - TurnIntoPassiveCmd(s, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, containingBlock); - } - // remove the local variables from the incarnation map - foreach (Variable v in st.Locals) { - Contract.Assert(v != null); - incarnationMap.Remove(v); - } - } - #region There shouldn't be any other types of commands at this point - else { - Debug.Fail("Internal Error: Passive transformation handed a command that is not one of assert,assume,havoc,assign."); - } - #endregion - - - #region We remember if we have put an havoc statement into a passive form - - if (!(c is HavocCmd)) - this.preHavocIncarnationMap = null; - // else: it has already been set by the case for the HavocCmd - #endregion - } - - NAryExpr TypedExprEq(Expr e0, Expr e1, bool doNotResolveOverloading = false) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); - NAryExpr e = Expr.Eq(e0, e1); - var fun = e.Fun as IOverloadedAppliable; - if (fun != null) - { - fun.DoNotResolveOverloading = doNotResolveOverloading; - } - e.Type = Bpl.Type.Bool; - e.TypeParameters = SimpleTypeParamInstantiation.EMPTY; - return e; - } - - /// - /// Creates a new block to add to impl.Blocks, where impl is the implementation that contains - /// succ. Caller must do the add to impl.Blocks. - /// - protected Block CreateBlockBetween(int predIndex, Block succ) { - Contract.Requires(0 <= predIndex && predIndex < succ.Predecessors.Count); - - - Contract.Requires(succ != null); - Contract.Ensures(Contract.Result() != null); - - Block pred = cce.NonNull(succ.Predecessors[predIndex]); - - string newBlockLabel = pred.Label + "_@2_" + succ.Label; - - // successor of newBlock list - List ls = new List(); - ls.Add(succ.Label); - List bs = new List(); - bs.Add(succ); - - Block newBlock = new Block( - new Token(-17, -4), - newBlockLabel, - new List(), - new GotoCmd(Token.NoToken, ls, bs) - ); - - // predecessors of newBlock - List ps = new List(); - ps.Add(pred); - newBlock.Predecessors = ps; - - // fix successors of pred - #region Change the edge "pred->succ" to "pred->newBlock" - GotoCmd gtc = (GotoCmd)cce.NonNull(pred.TransferCmd); - Contract.Assume(gtc.labelTargets != null); - Contract.Assume(gtc.labelNames != null); - for (int i = 0, n = gtc.labelTargets.Count; i < n; i++) { - if (gtc.labelTargets[i] == succ) { - gtc.labelTargets[i] = newBlock; - gtc.labelNames[i] = newBlockLabel; - break; - } - } - #endregion Change the edge "pred->succ" to "pred->newBlock" - - // fix predecessors of succ - succ.Predecessors[predIndex] = newBlock; - - return newBlock; - } - - protected void AddBlocksBetween(List blocks) { - Contract.Requires(blocks != null); - #region Introduce empty blocks between join points and their multi-successor predecessors - List tweens = new List(); - foreach (Block b in blocks) { - int nPreds = b.Predecessors.Count; - if (nPreds > 1) { - // b is a join point (i.e., it has more than one predecessor) - for (int i = 0; i < nPreds; i++) { - GotoCmd gotocmd = (GotoCmd)(cce.NonNull(b.Predecessors[i]).TransferCmd); - if (gotocmd.labelNames != null && gotocmd.labelNames.Count > 1) { - tweens.Add(CreateBlockBetween(i, b)); - } - } - } - } - blocks.AddRange(tweens); // must wait until iteration is done before changing the list - #endregion - } - - - public void Dispose() - { - Dispose(true); - GC.SuppressFinalize(this); - } - - protected virtual void Dispose(bool disposing) - { - if (!_disposed) - { - if (disposing) - { - Close(); - } - _disposed = true; - } - } - - public int Cores { get; set; } - } - - public class ModelViewInfo - { - public readonly List AllVariables = new List(); - public readonly List CapturePoints = new List(); - public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "$mv_state", - new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true), - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true) }, - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false)); - public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "$mv_state_const", Bpl.Type.Int)); - - public ModelViewInfo(Program program, Implementation impl) { - Contract.Requires(program != null); - Contract.Requires(impl != null); - - // global variables - lock (program.TopLevelDeclarations) - { - foreach (var v in program.Variables) - { - if (!(v is Constant)) - { - AllVariables.Add(v); - } - } - } - // implementation parameters - foreach (Variable p in impl.InParams) { - AllVariables.Add(p); - } - foreach (Variable p in impl.OutParams) { - AllVariables.Add(p); - } - // implementation locals - foreach (Variable v in impl.LocVars) { - AllVariables.Add(v); - } - } - - public ModelViewInfo(CodeExpr codeExpr) { - Contract.Requires(codeExpr != null); - // TODO: also need all variables of enclosing scopes (the global variables of the program, the parameters - // and perhaps locals of the implementation (if any), any enclosing code expressions). - - foreach (Variable v in codeExpr.LocVars) { - AllVariables.Add(v); - } - } - - public class Mapping - { - public readonly string Description; - public readonly Dictionary IncarnationMap; - public Mapping(string description, Dictionary incarnationMap) { - Description = description; - IncarnationMap = incarnationMap; - } - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Linq; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics; +using System.Threading; +using System.IO; +using Microsoft.Boogie; +using Microsoft.Boogie.GraphUtil; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; +using Microsoft.Boogie.VCExprAST; +using Set = Microsoft.Boogie.GSet; + +namespace Microsoft.Boogie { + + public class CalleeCounterexampleInfo { + public Counterexample counterexample; + public List/*!>!*/ args; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(args)); + } + + public CalleeCounterexampleInfo(Counterexample cex, List!*/> x) + { + Contract.Requires(cce.NonNullElements(x)); + counterexample = cex; + args = x; + } + } + + public class TraceLocation : IEquatable + { + public int numBlock; + public int numInstr; + + public TraceLocation(int numBlock, int numInstr) + { + this.numBlock = numBlock; + this.numInstr = numInstr; + } + + public override bool Equals(object obj) + { + TraceLocation that = obj as TraceLocation; + if (that == null) return false; + return (numBlock == that.numBlock && numInstr == that.numInstr); + } + + public bool Equals(TraceLocation that) + { + return (numBlock == that.numBlock && numInstr == that.numInstr); + } + + public override int GetHashCode() + { + return numBlock.GetHashCode() ^ 131 * numInstr.GetHashCode(); + } + } + + public abstract class Counterexample { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Trace != null); + Contract.Invariant(Context != null); + Contract.Invariant(cce.NonNullElements(relatedInformation)); + Contract.Invariant(cce.NonNullDictionaryAndValues(calleeCounterexamples)); + } + + [Peer] + public List Trace; + public Model Model; + public VC.ModelViewInfo MvInfo; + public ProverContext Context; + [Peer] + public List/*!>!*/ relatedInformation; + public string OriginalRequestId; + public string RequestId; + public abstract byte[] Checksum { get; } + public byte[] SugaredCmdChecksum; + public bool IsAuxiliaryCexForDiagnosingTimeouts; + + public Dictionary calleeCounterexamples; + + internal Counterexample(List trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) { + Contract.Requires(trace != null); + Contract.Requires(context != null); + this.Trace = trace; + this.Model = model; + this.MvInfo = mvInfo; + this.Context = context; + this.relatedInformation = new List(); + this.calleeCounterexamples = new Dictionary(); + } + + // Create a shallow copy of the counterexample + public abstract Counterexample Clone(); + + public void AddCalleeCounterexample(TraceLocation loc, CalleeCounterexampleInfo cex) + { + Contract.Requires(cex != null); + calleeCounterexamples[loc] = cex; + } + + public void AddCalleeCounterexample(int numBlock, int numInstr, CalleeCounterexampleInfo cex) + { + Contract.Requires(cex != null); + calleeCounterexamples[new TraceLocation(numBlock, numInstr)] = cex; + } + + public void AddCalleeCounterexample(Dictionary cs) + { + Contract.Requires(cce.NonNullDictionaryAndValues(cs)); + foreach (TraceLocation loc in cs.Keys) + { + AddCalleeCounterexample(loc, cs[loc]); + } + } + + // Looks up the Cmd at a given index into the trace + public Cmd getTraceCmd(TraceLocation loc) + { + Debug.Assert(loc.numBlock < Trace.Count); + Block b = Trace[loc.numBlock]; + Debug.Assert(loc.numInstr < b.Cmds.Count); + return b.Cmds[loc.numInstr]; + } + + // Looks up the name of the called procedure. + // Asserts that the name exists + public string getCalledProcName(Cmd cmd) + { + // There are two options: + // 1. cmd is a CallCmd + // 2. cmd is an AssumeCmd (passified version of a CallCmd) + if(cmd is CallCmd) { + return (cmd as CallCmd).Proc.Name; + } + AssumeCmd assumeCmd = cmd as AssumeCmd; + Debug.Assert(assumeCmd != null); + + NAryExpr naryExpr = assumeCmd.Expr as NAryExpr; + Debug.Assert(naryExpr != null); + + return naryExpr.Fun.FunctionName; + } + + public void Print(int indent, TextWriter tw, Action blockAction = null) { + int numBlock = -1; + string ind = new string(' ', indent); + foreach (Block b in Trace) { + Contract.Assert(b != null); + numBlock++; + if (b.tok == null) { + tw.WriteLine("{0}", ind); + } 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)) { + if (blockAction != null) + { + blockAction(b); + } + + tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind); + + for (int numInstr = 0; numInstr < b.Cmds.Count; numInstr++) + { + var loc = new TraceLocation(numBlock, numInstr); + if (calleeCounterexamples.ContainsKey(loc)) + { + var cmd = getTraceCmd(loc); + var calleeName = getCalledProcName(cmd); + if (calleeName.StartsWith(VC.StratifiedVCGen.recordProcName) && CommandLineOptions.Clo.StratifiedInlining > 0) + { + Contract.Assert(calleeCounterexamples[loc].args.Count == 1); + var arg = calleeCounterexamples[loc].args[0]; + tw.WriteLine("{0}value = {1}", ind, arg.ToString()); + } + else + { + tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind); + calleeCounterexamples[loc].counterexample.Print(indent + 4, tw); + tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind); + } + } + } + } + } + } + } + + public static bool firstModelFile = true; + + public bool ModelHasStatesAlready = false; + + public void PrintModel(TextWriter tw) + { + var filename = CommandLineOptions.Clo.ModelViewFile; + if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return; + + if (!ModelHasStatesAlready) { + PopulateModelWithStates(); + ModelHasStatesAlready = true; + } + + if (filename == "-") { + Model.Write(tw); + tw.Flush(); + } else { + using (var wr = new StreamWriter(filename, !firstModelFile)) { + firstModelFile = false; + Model.Write(wr); + } + } + } + + void ApplyRedirections(Model m) { + var mapping = new Dictionary(); + foreach (var name in new string[] { "U_2_bool", "U_2_int" }) { + Model.Func f = m.TryGetFunc(name); + if (f != null && f.Arity == 1) { + foreach (var ft in f.Apps) mapping[ft.Args[0]] = ft.Result; + } + } + m.Substitute(mapping); + } + + public void PopulateModelWithStates() + { + Contract.Requires(Model != null); + + Model m = Model; + ApplyRedirections(m); + + var mvstates = m.TryGetFunc("$mv_state"); + if (MvInfo == null || mvstates == null || (mvstates.Arity == 1 && mvstates.Apps.Count() == 0)) + return; + + Contract.Assert(mvstates.Arity == 2); + + foreach (Variable v in MvInfo.AllVariables) { + m.InitialState.AddBinding(v.Name, GetModelValue(m, v)); + } + + var states = new List(); + foreach (var t in mvstates.Apps) + states.Add(t.Args[1].AsInt()); + + states.Sort(); + + for (int i = 0; i < states.Count; ++i) { + var s = states[i]; + if (0 <= s && s < MvInfo.CapturePoints.Count) { + VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s]; + var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Dictionary(); + var cs = m.MkState(map.Description); + + foreach (Variable v in MvInfo.AllVariables) { + Expr e = map.IncarnationMap.ContainsKey(v) ? map.IncarnationMap[v] : null; + if (e == null) continue; + + Expr prevIncV = prevInc.ContainsKey(v) ? prevInc[v] : null; + if (prevIncV == e) continue; // skip unchanged variables + + Model.Element elt; + + if (e is IdentifierExpr) { + IdentifierExpr ide = (IdentifierExpr)e; + elt = GetModelValue(m, ide.Decl); + } else if (e is LiteralExpr) { + LiteralExpr lit = (LiteralExpr)e; + elt = m.MkElement(lit.Val.ToString()); + } else { + elt = m.MkFunc(e.ToString(), 0).GetConstant(); + } + + cs.AddBinding(v.Name, elt); + } + + } else { + Contract.Assume(false); + } + } + } + + private Model.Element GetModelValue(Model m, Variable v) { + Model.Element elt; + // first, get the unique name + string uniqueName; + VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v); + if (vvar == null) { + uniqueName = v.Name; + } else { + uniqueName = Context.Lookup(vvar); + } + + var f = m.TryGetFunc(uniqueName); + if (f == null) { + f = m.MkFunc(uniqueName, 0); + } + elt = f.GetConstant(); + return elt; + } + + public abstract int GetLocation(); + } + + public class CounterexampleComparer : IComparer, IEqualityComparer { + + private int Compare(List bs1, List bs2) + { + if (bs1.Count < bs2.Count) + { + return -1; + } + else if (bs2.Count < bs1.Count) + { + return 1; + } + + for (int i = 0; i < bs1.Count; i++) + { + var b1 = bs1[i]; + var b2 = bs2[i]; + if (b1.tok.pos < b2.tok.pos) + { + return -1; + } + else if (b2.tok.pos < b1.tok.pos) + { + return 1; + } + } + + return 0; + } + + public int Compare(Counterexample c1, Counterexample c2) + { + //Contract.Requires(c1 != null); + //Contract.Requires(c2 != null); + if (c1.GetLocation() == c2.GetLocation()) + { + var c = Compare(c1.Trace, c2.Trace); + if (c != 0) + { + return c; + } + // TODO(wuestholz): Generalize this to compare all IPotentialErrorNodes of the counterexample. + var a1 = c1 as AssertCounterexample; + var a2 = c2 as AssertCounterexample; + if (a1 != null && a2 != null) + { + var s1 = a1.FailingAssert.ErrorData as string; + var s2 = a2.FailingAssert.ErrorData as string; + if (s1 != null && s2 != null) + { + return s1.CompareTo(s2); + } + } + + return 0; + } + if (c1.GetLocation() > c2.GetLocation()) + { + return 1; + } + return -1; + } + + public bool Equals(Counterexample x, Counterexample y) + { + return Compare(x, y) == 0; + } + + public int GetHashCode(Counterexample obj) + { + return 0; + } + } + + public class AssertCounterexample : Counterexample { + [Peer] + public AssertCmd FailingAssert; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(FailingAssert != null); + } + + + public AssertCounterexample(List trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context) + : base(trace, model, mvInfo, context) { + Contract.Requires(trace != null); + Contract.Requires(failingAssert != null); + Contract.Requires(context != null); + this.FailingAssert = failingAssert; + } + + public override int GetLocation() { + return FailingAssert.tok.line * 1000 + FailingAssert.tok.col; + } + + public override byte[] Checksum + { + get { return FailingAssert.Checksum; } + } + + public override Counterexample Clone() + { + var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo, Context); + ret.calleeCounterexamples = calleeCounterexamples; + return ret; + } + } + + public class CallCounterexample : Counterexample { + public CallCmd FailingCall; + public Requires FailingRequires; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(FailingCall != null); + Contract.Invariant(FailingRequires != null); + } + + + public CallCounterexample(List trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum = null) + : base(trace, model, mvInfo, context) { + Contract.Requires(!failingRequires.Free); + Contract.Requires(trace != null); + Contract.Requires(context != null); + Contract.Requires(failingCall != null); + Contract.Requires(failingRequires != null); + this.FailingCall = failingCall; + this.FailingRequires = failingRequires; + this.checksum = checksum; + this.SugaredCmdChecksum = failingCall.Checksum; + } + + public override int GetLocation() { + return FailingCall.tok.line * 1000 + FailingCall.tok.col; + } + + byte[] checksum; + public override byte[] Checksum + { + get { return checksum; } + } + + public override Counterexample Clone() + { + var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context, Checksum); + ret.calleeCounterexamples = calleeCounterexamples; + return ret; + } + } + + public class ReturnCounterexample : Counterexample { + public TransferCmd FailingReturn; + public Ensures FailingEnsures; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(FailingEnsures != null); + Contract.Invariant(FailingReturn != null); + } + + + public ReturnCounterexample(List trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum) + : base(trace, model, mvInfo, context) { + Contract.Requires(trace != null); + Contract.Requires(context != null); + Contract.Requires(failingReturn != null); + Contract.Requires(failingEnsures != null); + Contract.Requires(!failingEnsures.Free); + this.FailingReturn = failingReturn; + this.FailingEnsures = failingEnsures; + this.checksum = checksum; + } + + public override int GetLocation() { + return FailingReturn.tok.line * 1000 + FailingReturn.tok.col; + } + + byte[] checksum; + + /// + /// Returns the checksum of the corresponding assertion. + /// + public override byte[] Checksum + { + get + { + return checksum; + } + } + + public override Counterexample Clone() + { + var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context, checksum); + ret.calleeCounterexamples = calleeCounterexamples; + return ret; + } + } + + public class VerifierCallback { + // reason == null means this is genuine counterexample returned by the prover + // other reason means it's time out/memory out/crash + public virtual void OnCounterexample(Counterexample ce, string/*?*/ reason) { + Contract.Requires(ce != null); + } + + // called in case resource is exceeded and we don't have counterexample + public virtual void OnTimeout(string reason) { + Contract.Requires(reason != null); + } + + public virtual void OnOutOfMemory(string reason) { + Contract.Requires(reason != null); + } + + public virtual void OnProgress(string phase, int step, int totalSteps, double progressEstimate) { + } + + public virtual void OnUnreachableCode(Implementation impl) { + Contract.Requires(impl != null); + } + + public virtual void OnWarning(string msg) { + Contract.Requires(msg != null); + switch (CommandLineOptions.Clo.PrintProverWarnings) { + case CommandLineOptions.ProverWarnings.None: + break; + case CommandLineOptions.ProverWarnings.Stdout: + Console.WriteLine("Prover warning: " + msg); + break; + case CommandLineOptions.ProverWarnings.Stderr: + Console.Error.WriteLine("Prover warning: " + msg); + break; + default: + Contract.Assume(false); + throw new cce.UnreachableException(); // unexpected case + } + } + } +} + +//////////////////////////////////////////// + +namespace VC { + using Bpl = Microsoft.Boogie; + + public class VCGenException : Exception { + public VCGenException(string s) + : base(s) { + } + } + [ContractClassFor(typeof(ConditionGeneration))] + public abstract class ConditionGenerationContracts : ConditionGeneration { + public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) { + Contract.Requires(impl != null); + Contract.Requires(callback != null); + Contract.EnsuresOnThrow(true); + throw new NotImplementedException(); + } + public ConditionGenerationContracts(Program p, List checkers) + : base(p, checkers) { + } + } + + [ContractClass(typeof(ConditionGenerationContracts))] + public abstract class ConditionGeneration : IDisposable { + protected internal object CheckerCommonState; + + public enum Outcome { + Correct, + Errors, + TimedOut, + OutOfMemory, + Inconclusive, + ReachedBound + } + + public static Outcome ProverInterfaceOutcomeToConditionGenerationOutcome(ProverInterface.Outcome outcome) { + switch (outcome) { + 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; + case ProverInterface.Outcome.Valid: + return Outcome.Correct; + } + return Outcome.Inconclusive; // unreachable but the stupid compiler does not understand + } + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(checkers)); + Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap)); + Contract.Invariant(program != null); + } + + public int CumulativeAssertionCount; // for statistics + + protected readonly List/*!>!*/ checkers; + + private bool _disposed; + + protected Implementation currentImplementation; + + protected List CurrentLocalVariables = null; + + // shared across each implementation; created anew for each implementation + protected Dictionary variable2SequenceNumber; + public Dictionary/*!>!*/ incarnationOriginMap = new Dictionary(); + + public Program program; + protected string/*?*/ logFilePath; + protected bool appendLogFile; + + public static List errorModelList; + + public ConditionGeneration(Program p, List checkers) { + Contract.Requires(p != null && checkers != null && cce.NonNullElements(checkers)); + program = p; + this.checkers = checkers; + Cores = 1; + } + + /// + /// Takes an implementation and constructs a verification condition and sends + /// it to the theorem prover. + /// Returns null if "impl" is correct. Otherwise, returns a list of counterexamples, + /// each counterexample consisting of an array of labels. + /// + /// + public Outcome VerifyImplementation(Implementation impl, out List/*?*/ errors, string requestId = null) { + Contract.Requires(impl != null); + + Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null)); + Contract.Ensures(Contract.Result() != Outcome.Errors || errors != null); + Contract.EnsuresOnThrow(true); + Helpers.ExtraTraceInformation("Starting implementation verification"); + + CounterexampleCollector collector = new CounterexampleCollector(); + collector.RequestId = requestId; + Outcome outcome = VerifyImplementation(impl, collector); + if (outcome == Outcome.Errors || outcome == Outcome.TimedOut || outcome == Outcome.OutOfMemory) { + errors = collector.examples; + } else { + errors = null; + } + + Helpers.ExtraTraceInformation("Finished implementation verification"); + return outcome; + } + + /// + /// Takes an implementation and constructs a verification condition and sends + /// it to the theorem prover. + /// Returns null if "impl" is correct. Otherwise, returns a list of counterexamples, + /// each counterexample consisting of an array of labels. + /// + /// + public Outcome VerifyImplementation(Implementation impl, out List errors, out List errorsModel) + { + Contract.Ensures(Contract.Result() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null); + Contract.EnsuresOnThrow(true); + List errorsOut; + + Outcome outcome; + errorModelList = new List(); + outcome = VerifyImplementation(impl, out errorsOut); + errors = errorsOut; + errorsModel = errorModelList; + + return outcome; + } + + public abstract Outcome VerifyImplementation(Implementation impl, VerifierCallback callback); + + /////////////////////////////////// Common Methods and Classes ////////////////////////////////////////// + + #region Methods for injecting pre- and postconditions + private static void + ThreadInCodeExpr(Implementation impl, + Block targetBlock, + CodeExpr codeExpr, + bool replaceWithAssert, + TokenTextWriter debugWriter) { + Contract.Requires(impl != null); + Contract.Requires(codeExpr != null); + Contract.Requires(targetBlock != null); + // Go through codeExpr and for all blocks that have a "return e" + // as their transfer command: + // Replace all "return e" with "assert/assume e" + // Change the transfer command to "goto targetBlock" + // Then add all of the blocks in codeExpr to the implementation (at the end) + foreach (Block b in codeExpr.Blocks) { + Contract.Assert(b != null); + ReturnExprCmd rec = b.TransferCmd as ReturnExprCmd; + if (rec != null) { // otherwise it is a goto command + if (replaceWithAssert) { + Ensures ens = new Ensures(rec.tok, false, rec.Expr, null); + Contract.Assert(ens != null); + Cmd c = new AssertEnsuresCmd(ens); + Contract.Assert(c != null); + b.Cmds.Add(c); + } else { + b.Cmds.Add(new AssumeCmd(rec.tok, rec.Expr)); + } + b.TransferCmd = new GotoCmd(Token.NoToken, + new List { targetBlock.Label }, + new List { targetBlock }); + targetBlock.Predecessors.Add(b); + } + impl.Blocks.Add(b); + } + if (debugWriter != null) { + codeExpr.Emit(debugWriter, 1, false); + } + return; + } + + private static void AddAsPrefix(Block b, List cs) { + Contract.Requires(b != null); + Contract.Requires(cs != null); + List newCommands = new List(); + newCommands.AddRange(cs); + newCommands.AddRange(b.Cmds); + b.Cmds = newCommands; + } + + + /// + /// Modifies an implementation by prepending it with startCmds and then, as assume + /// statements, all preconditions. Insert new blocks as needed, and adjust impl.Blocks[0] + /// accordingly to make it the new implementation entry block. + /// + /// + /// + protected static void InjectPreconditions(Implementation impl, [Captured] List startCmds) { + Contract.Requires(impl != null); + Contract.Requires(startCmds != null); + Contract.Requires(impl.Proc != null); + + TokenTextWriter debugWriter = null; + if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { + debugWriter = new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false); + debugWriter.WriteLine("Effective precondition:"); + } + + Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); + string blockLabel = "PreconditionGeneratedEntry"; + + Block origStartBlock = impl.Blocks[0]; + Block insertionPoint = new Block( + new Token(-17, -4), blockLabel, startCmds, + new GotoCmd(Token.NoToken, new List { origStartBlock.Label }, new List { origStartBlock })); + + impl.Blocks[0] = insertionPoint; // make insertionPoint the start block + impl.Blocks.Add(origStartBlock); // and put the previous start block at the end of the list + + // (free and checked) requires clauses + foreach (Requires req in impl.Proc.Requires) + // invariant: insertionPoint.TransferCmd is "goto origStartBlock;", but origStartBlock.Predecessors has not yet been updated + { + Contract.Assert(req != null); + Expr e = Substituter.Apply(formalProcImplSubst, req.Condition); + Cmd c = new AssumeCmd(req.tok, e); + c.IrrelevantForChecksumComputation = true; + insertionPoint.Cmds.Add(c); + if (debugWriter != null) { + c.Emit(debugWriter, 1); + } + } + origStartBlock.Predecessors.Add(insertionPoint); + + if (impl.ExplicitAssumptionAboutCachedPrecondition != null) + { + insertionPoint.Cmds.Add(impl.ExplicitAssumptionAboutCachedPrecondition); + } + + if (debugWriter != null) { + debugWriter.WriteLine(); + } + } + /// + /// Modifies an implementation by inserting all postconditions + /// as assert statements at the end of the implementation + /// Returns the possibly-new unified exit block of the implementation + /// + /// + /// The unified exit block that has + /// already been constructed for the implementation (and so + /// is already an element of impl.Blocks) + /// + protected static void InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary gotoCmdOrigins) { + Contract.Requires(impl != null); + Contract.Requires(unifiedExitBlock != null); + Contract.Requires(gotoCmdOrigins != null); + Contract.Requires(impl.Proc != null); + Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd); + + TokenTextWriter debugWriter = null; + if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { + debugWriter = new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false); + debugWriter.WriteLine("Effective postcondition:"); + } + + Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); + + // (free and checked) ensures clauses + foreach (Ensures ens in impl.Proc.Ensures) { + Contract.Assert(ens != null); + if (!ens.Free) { // skip free ensures clauses + Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); + Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone()); + ensCopy.Condition = e; + AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); + c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; + unifiedExitBlock.Cmds.Add(c); + if (debugWriter != null) { + c.Emit(debugWriter, 1); + } + } + } + + if (debugWriter != null) { + debugWriter.WriteLine(); + } + } + + + /// + /// Get the pre-condition of an implementation, including the where clauses from the in-parameters. + /// + /// + protected static List GetPre(Implementation impl) { + Contract.Requires(impl != null); + Contract.Requires(impl.Proc != null); + Contract.Ensures(Contract.Result>() != null); + + + TokenTextWriter debugWriter = null; + if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { + debugWriter = new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false); + debugWriter.WriteLine("Effective precondition:"); + } + + Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); + List pre = new List(); + + // (free and checked) requires clauses + foreach (Requires req in impl.Proc.Requires) { + Contract.Assert(req != null); + Expr e = Substituter.Apply(formalProcImplSubst, req.Condition); + Contract.Assert(e != null); + Cmd c = new AssumeCmd(req.tok, e); + Contract.Assert(c != null); + pre.Add(c); + + if (debugWriter != null) { + c.Emit(debugWriter, 1); + } + } + + if (debugWriter != null) { + debugWriter.WriteLine(); + } + + return pre; + } + + /// + /// Get the post-condition of an implementation. + /// + /// + protected static List GetPost(Implementation impl) { + + + Contract.Requires(impl != null); + Contract.Requires(impl.Proc != null); + Contract.Ensures(Contract.Result>() != null); + if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { + Console.WriteLine("Effective postcondition:"); + } + + // Construct an Expr for the post-condition + Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); + List post = new List(); + foreach (Ensures ens in impl.Proc.Ensures) { + Contract.Assert(ens != null); + if (!ens.Free) { + Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); + Contract.Assert(e != null); + Ensures ensCopy = cce.NonNull((Ensures)ens.Clone()); + ensCopy.Condition = e; + Cmd c = new AssertEnsuresCmd(ensCopy); + ((AssertEnsuresCmd)c).ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; + post.Add(c); + + if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { + c.Emit(new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false), 1); + } + } + } + + if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { + Console.WriteLine(); + } + + return post; + } + + /// + /// Get the where clauses from the in- and out-parameters as + /// a sequence of assume commands. + /// As a side effect, this method adds these where clauses to the out parameters. + /// + /// + protected static List GetParamWhereClauses(Implementation impl) { + Contract.Requires(impl != null); + Contract.Requires(impl.Proc != null); + Contract.Ensures(Contract.Result>() != null); + TokenTextWriter debugWriter = null; + if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { + debugWriter = new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false); + debugWriter.WriteLine("Effective precondition from where-clauses:"); + } + + Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap()); + List whereClauses = new List(); + + // where clauses of in-parameters + foreach (Formal f in impl.Proc.InParams) { + Contract.Assert(f != null); + if (f.TypedIdent.WhereExpr != null) { + Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr); + Cmd c = new AssumeCmd(f.tok, e); + whereClauses.Add(c); + + if (debugWriter != null) { + c.Emit(debugWriter, 1); + } + } + } + + // where clauses of out-parameters + Contract.Assert(impl.OutParams.Count == impl.Proc.OutParams.Count); + for (int i = 0; i < impl.OutParams.Count; i++) { + Variable f = cce.NonNull(impl.Proc.OutParams[i]); + if (f.TypedIdent.WhereExpr != null) { + Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr); + Cmd c = new AssumeCmd(f.tok, e); + whereClauses.Add(c); + + Variable fi = cce.NonNull(impl.OutParams[i]); + Contract.Assume(fi.TypedIdent.WhereExpr == null); + fi.TypedIdent.WhereExpr = e; + + if (debugWriter != null) { + c.Emit(debugWriter, 1); + } + } + } + + if (debugWriter != null) { + debugWriter.WriteLine(); + } + + return whereClauses; + } + + protected static void RestoreParamWhereClauses(Implementation impl) { + Contract.Requires(impl != null); + // 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) { + Contract.Assert(f != null); + f.TypedIdent.WhereExpr = null; + } + } + #endregion + + + protected Checker FindCheckerFor(int timeout, bool isBlocking = true, int waitTimeinMs = 50, int maxRetries = 3) + { + Contract.Requires(0 <= waitTimeinMs && 0 <= maxRetries); + Contract.Ensures(!isBlocking || Contract.Result() != null); + + lock (checkers) + { + retry: + // Look for existing checker. + for (int i = 0; i < checkers.Count; i++) + { + var c = checkers[i]; + if (Monitor.TryEnter(c)) + { + try + { + if (c.WillingToHandle(timeout, program)) + { + c.GetReady(); + return c; + } + else if (c.IsIdle || c.IsClosed) + { + if (c.IsIdle) + { + c.Retarget(program, c.TheoremProver.Context, timeout); + c.GetReady(); + return c; + } + else + { + checkers.RemoveAt(i); + i--; + continue; + } + } + } + finally + { + Monitor.Exit(c); + } + } + } + + if (Cores <= checkers.Count) + { + if (isBlocking || 0 < maxRetries) + { + if (0 < waitTimeinMs) + { + Monitor.Wait(checkers, waitTimeinMs); + } + maxRetries--; + goto retry; + } + else + { + return null; + } + } + + // Create a new checker. + string log = logFilePath; + if (log != null && !log.Contains("@PROC@") && checkers.Count > 0) + { + log = log + "." + checkers.Count; + } + Checker ch = new Checker(this, program, log, appendLogFile, timeout); + ch.GetReady(); + checkers.Add(ch); + return ch; + } + } + + + virtual public void Close() { + } + + + public class CounterexampleCollector : VerifierCallback { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(examples)); + } + + public string RequestId; + + public readonly List/*!>!*/ examples = new List(); + public override void OnCounterexample(Counterexample ce, string/*?*/ reason) { + //Contract.Requires(ce != null); + if (RequestId != null) + { + ce.RequestId = RequestId; + } + if (ce.OriginalRequestId == null && 1 < CommandLineOptions.Clo.VerifySnapshots) + { + ce.OriginalRequestId = RequestId; + } + examples.Add(ce); + } + + public override void OnUnreachableCode(Implementation impl) { + //Contract.Requires(impl != null); + System.Console.WriteLine("found unreachable code:"); + EmitImpl(impl, false); + // TODO report error about next to last in seq + } + } + + protected static void EmitImpl(Implementation impl, bool printDesugarings) { + Contract.Requires(impl != null); + int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; + CommandLineOptions.Clo.PrintUnstructured = 2; // print only the unstructured program + bool oldPrintDesugaringSetting = CommandLineOptions.Clo.PrintDesugarings; + CommandLineOptions.Clo.PrintDesugarings = printDesugarings; + impl.Emit(new TokenTextWriter("", Console.Out, /*setTokens=*/ false, /*pretty=*/ false), 0); + CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting; + CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; + } + + + protected Block GenerateUnifiedExit(Implementation impl, Dictionary gotoCmdOrigins) { + Contract.Requires(impl != null); + Contract.Requires(gotoCmdOrigins != null); + Contract.Ensures(Contract.Result() != null); + + Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); + Block/*?*/ exitBlock = null; + #region Create a unified exit block, if there's more than one + { + int returnBlocks = 0; + foreach (Block b in impl.Blocks) { + if (b.TransferCmd is ReturnCmd) { + exitBlock = b; + returnBlocks++; + } + } + if (returnBlocks > 1) { + string unifiedExitLabel = "GeneratedUnifiedExit"; + Block unifiedExit; + unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); + Contract.Assert(unifiedExit != null); + foreach (Block b in impl.Blocks) { + if (b.TransferCmd is ReturnCmd) { + List labels = new List(); + labels.Add(unifiedExitLabel); + List bs = new List(); + bs.Add(unifiedExit); + GotoCmd go = new GotoCmd(Token.NoToken, labels, bs); + gotoCmdOrigins[go] = (ReturnCmd)b.TransferCmd; + b.TransferCmd = go; + unifiedExit.Predecessors.Add(b); + } + } + + exitBlock = unifiedExit; + impl.Blocks.Add(unifiedExit); + } + Contract.Assert(exitBlock != null); + } + return exitBlock; + #endregion + } + + protected static void ResetPredecessors(List blocks) { + Contract.Requires(blocks != null); + foreach (Block b in blocks) { + Contract.Assert(b != null); + b.Predecessors = new List(); + } + foreach (Block b in blocks) { + Contract.Assert(b != null); + foreach (Block ch in Exits(b)) { + Contract.Assert(ch != null); + ch.Predecessors.Add(b); + } + } + } + + protected static IEnumerable Exits(Block b) { + Contract.Requires(b != null); + GotoCmd g = b.TransferCmd as GotoCmd; + if (g != null) { + return cce.NonNull(g.labelTargets); + } + return new List(); + } + + protected Variable CreateIncarnation(Variable x, Absy a) { + Contract.Requires(this.variable2SequenceNumber != null); + Contract.Requires(this.CurrentLocalVariables != null); + Contract.Requires(a is Block || a is AssignCmd || a is HavocCmd); + + Contract.Requires(x != null); + Contract.Ensures(Contract.Result() != null); + + int currentIncarnationNumber = + variable2SequenceNumber.ContainsKey(x) + ? + variable2SequenceNumber[x] + : + -1; + Variable v = new Incarnation(x, currentIncarnationNumber + 1); + variable2SequenceNumber[x] = currentIncarnationNumber + 1; + CurrentLocalVariables.Add(v); + incarnationOriginMap.Add((Incarnation)v, a); + return v; + } + + /// + /// Compute the incarnation map at the beginning of block "b" from the incarnation blocks of the + /// predecessors of "b". + /// + /// The predecessor map b.map for block "b" is defined as follows: + /// b.map.Domain == Union{Block p in b.predecessors; p.map.Domain} + /// Forall{Variable v in b.map.Domain; + /// b.map[v] == (v in Intersection{Block p in b.predecessors; p.map}.Domain + /// ? b.predecessors[0].map[v] + /// : new Variable())} + /// Every variable that b.map maps to a fresh variable requires a fixup in all predecessor blocks. + /// + /// + /// Gives incarnation maps for b's predecessors. + /// + protected Dictionary ComputeIncarnationMap(Block b, Dictionary> block2Incarnation) { + Contract.Requires(b != null); + Contract.Requires(block2Incarnation != null); + Contract.Ensures(Contract.Result>() != null); + + if (b.Predecessors.Count == 0) { + return new Dictionary(); + } + + Dictionary incarnationMap = null; + Set /*Variable*/ fixUps = new Set /*Variable*/ (); + foreach (Block pred in b.Predecessors) { + Contract.Assert(pred != null); + Contract.Assert(block2Incarnation.ContainsKey(pred)); // otherwise, Passive Transformation found a block whose predecessors have not been processed yet + Dictionary predMap = (Dictionary)block2Incarnation[pred]; + Contract.Assert(predMap != null); + if (incarnationMap == null) { + incarnationMap = new Dictionary(predMap); + continue; + } + + ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ (); + foreach (Variable v in incarnationMap.Keys) { + Contract.Assert(v != null); + if (!predMap.ContainsKey(v)) { + // conflict!! + conflicts.Add(v); + fixUps.Add(v); + } + } + // Now that we're done with enumeration, we'll do all the removes + foreach (Variable v in conflicts) { + Contract.Assert(v != null); + incarnationMap.Remove(v); + } + foreach (Variable v in predMap.Keys) { + Contract.Assert(v != null); + if (!incarnationMap.ContainsKey(v)) { + // v was not in the domain of the predecessors seen so far, so it needs to be fixed up + fixUps.Add(v); + } else { + // v in incarnationMap ==> all pred blocks (up to now) all agree on its incarnation + if (predMap[v] != incarnationMap[v]) { + // conflict!! + incarnationMap.Remove(v); + fixUps.Add(v); + } + } + } + } + + #region Second, for all variables in the fixups list, introduce a new incarnation and push it back into the preds. + foreach (Variable v in fixUps) { + Contract.Assert(v != null); + if (!b.IsLive(v)) + continue; + Variable v_prime = CreateIncarnation(v, b); + IdentifierExpr ie = new IdentifierExpr(v_prime.tok, v_prime); + Contract.Assert(incarnationMap != null); + incarnationMap[v] = ie; + foreach (Block pred in b.Predecessors) { + Contract.Assert(pred != null); + #region Create an assume command equating v_prime with its last incarnation in pred + #region Create an identifier expression for the last incarnation in pred + Dictionary predMap = (Dictionary)cce.NonNull(block2Incarnation[pred]); + + Expr pred_incarnation_exp; + Expr o = predMap.ContainsKey(v) ? predMap[v] : null; + if (o == null) { + Variable predIncarnation = v; + IdentifierExpr ie2 = new IdentifierExpr(predIncarnation.tok, predIncarnation); + pred_incarnation_exp = ie2; + } else { + pred_incarnation_exp = o; + } + #endregion + #region Create an identifier expression for the new incarnation + IdentifierExpr v_prime_exp = new IdentifierExpr(v_prime.tok, v_prime); + #endregion + #region Create the assume command itself + AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp, v_prime.Name.Contains("a##cached##"))); + pred.Cmds.Add(ac); + #endregion + #endregion + } + } + #endregion + + Contract.Assert(incarnationMap != null); + return incarnationMap; + } + + Dictionary preHavocIncarnationMap = null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement + + protected void TurnIntoPassiveBlock(Block b, Dictionary incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst, MutableVariableCollector variableCollector, byte[] currentChecksum = null) { + Contract.Requires(b != null); + Contract.Requires(incarnationMap != null); + Contract.Requires(mvInfo != null); + Contract.Requires(oldFrameSubst != null); + #region Walk forward over the commands in this block and convert them to passive commands + + List passiveCmds = new List(); + foreach (Cmd c in b.Cmds) { + Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction + ChecksumHelper.ComputeChecksums(c, currentImplementation, variableCollector.UsedVariables, currentChecksum); + variableCollector.Visit(c); + currentChecksum = c.Checksum; + TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, b); + } + b.Checksum = currentChecksum; + b.Cmds = passiveCmds; + + if (b.TransferCmd is ReturnExprCmd) { + ReturnExprCmd rec = (ReturnExprCmd)b.TransferCmd.Clone(); + Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap); + rec.Expr = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, rec.Expr); + b.TransferCmd = rec; + } + #endregion + } + + protected Dictionary Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) { + Contract.Requires(impl != null); + Contract.Requires(mvInfo != null); + + currentImplementation = impl; + + var start = DateTime.UtcNow; + + Dictionary r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo); + + var end = DateTime.UtcNow; + + if (CommandLineOptions.Clo.TraceCachingForDebugging) + { + Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds); + } + + if (CommandLineOptions.Clo.TraceCachingForDebugging) + { + using (var tokTxtWr = new TokenTextWriter("", Console.Out, false, false)) + { + var pd = CommandLineOptions.Clo.PrintDesugarings; + var pu = CommandLineOptions.Clo.PrintUnstructured; + CommandLineOptions.Clo.PrintDesugarings = true; + CommandLineOptions.Clo.PrintUnstructured = 1; + impl.Emit(tokTxtWr, 0); + CommandLineOptions.Clo.PrintDesugarings = pd; + CommandLineOptions.Clo.PrintUnstructured = pu; + } + } + + currentImplementation = null; + + RestoreParamWhereClauses(impl); + + #region Debug Tracing + if (CommandLineOptions.Clo.TraceVerify) { + Console.WriteLine("after conversion to passive commands"); + EmitImpl(impl, true); + } + #endregion + + return r; + } + + protected Dictionary ConvertBlocks2PassiveCmd(List blocks, List modifies, ModelViewInfo mvInfo) { + Contract.Requires(blocks != null); + Contract.Requires(modifies != null); + Contract.Requires(mvInfo != null); + #region Convert to Passive Commands + + #region Topological sort -- need to process in a linearization of the partial order + Graph dag = new Graph(); + dag.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph + foreach (Block b in blocks) { + GotoCmd gtc = b.TransferCmd as GotoCmd; + if (gtc != null) { + Contract.Assume(gtc.labelTargets != null); + foreach (Block dest in gtc.labelTargets) { + Contract.Assert(dest != null); + dag.AddEdge(b, dest); + } + } + } + + IEnumerable sortedNodes; + if (CommandLineOptions.Clo.ModifyTopologicalSorting) { + sortedNodes = dag.TopologicalSort(true); + } else { + sortedNodes = dag.TopologicalSort(); + } + + Contract.Assert(sortedNodes != null); + #endregion + + Substitution oldFrameSubst = ComputeOldExpressionSubstitution(modifies); + + // 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. + Dictionary> block2Incarnation = new Dictionary>(); + Block exitBlock = null; + Dictionary exitIncarnationMap = null; + var variableCollectors = new Dictionary(); + foreach (Block b in sortedNodes) { + Contract.Assert(b != null); + Contract.Assert(!block2Incarnation.ContainsKey(b)); + Dictionary incarnationMap = ComputeIncarnationMap(b, block2Incarnation); + + // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out. + b.liveVarsBefore = null; + + // Decrement the succCount field in each predecessor. Once the field reaches zero in any block, + // all its successors have been passified. Consequently, its entry in block2Incarnation can be removed. + byte[] currentChecksum = null; + var mvc = new MutableVariableCollector(); + variableCollectors[b] = mvc; + foreach (Block p in b.Predecessors) { + p.succCount--; + if (p.Checksum != null) + { + // Compute the checksum based on the checksums of the predecessor. The order should not matter. + currentChecksum = ChecksumHelper.CombineChecksums(p.Checksum, currentChecksum, true); + } + mvc.AddUsedVariables(variableCollectors[p].UsedVariables); + if (p.succCount == 0) + block2Incarnation.Remove(p); + } + + #region Each block's map needs to be available to successor blocks + GotoCmd gotoCmd = b.TransferCmd as GotoCmd; + if (gotoCmd == null) { + b.succCount = 0; + } + else { + // incarnationMap needs to be added only if there is some successor of b + b.succCount = gotoCmd.labelNames.Count; + block2Incarnation.Add(b, incarnationMap); + } + #endregion Each block's map needs to be available to successor blocks + + TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst, mvc, currentChecksum); + exitBlock = b; + exitIncarnationMap = incarnationMap; + } + + variableCollectors.Clear(); + + // Verify that exitBlock is indeed the unique exit block + Contract.Assert(exitBlock != null); + Contract.Assert(exitBlock.TransferCmd is ReturnCmd); + #endregion Convert to Passive Commands + + return exitIncarnationMap; + } + + /// + /// Compute the substitution for old expressions. + /// + protected static Substitution ComputeOldExpressionSubstitution(List modifies) + { + Dictionary oldFrameMap = new Dictionary(); + foreach (IdentifierExpr ie in modifies) + { + Contract.Assert(ie != null); + if (!oldFrameMap.ContainsKey(cce.NonNull(ie.Decl))) + oldFrameMap.Add(ie.Decl, ie); + } + return Substituter.SubstitutionFromHashtable(oldFrameMap); + } + + public enum CachingAction : byte + { + DoNothingToAssert, + MarkAsPartiallyVerified, + MarkAsFullyVerified, + RecycleError, + AssumeNegationOfAssumptionVariable, + DropAssume + } + + public long[] CachingActionCounts; + + void TraceCachingAction(Cmd cmd, CachingAction action) + { + if (CommandLineOptions.Clo.TraceCachingForTesting) + { + using (var tokTxtWr = new TokenTextWriter("", Console.Out, false, false)) + { + var loc = cmd.tok != null && cmd.tok != Token.NoToken ? string.Format("{0}({1},{2})", cmd.tok.filename, cmd.tok.line, cmd.tok.col) : ""; + Console.Write("Processing command (at {0}) ", loc); + cmd.Emit(tokTxtWr, 0); + Console.Out.WriteLine(" >>> {0}", action); + } + } + + if (CommandLineOptions.Clo.TraceCachingForBenchmarking && CachingActionCounts != null) + { + Interlocked.Increment(ref CachingActionCounts[(int)action]); + } + } + + /// + /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc + /// Meanwhile, record any information needed to later reconstruct a model view. + /// + protected void TurnIntoPassiveCmd(Cmd c, Dictionary incarnationMap, Substitution oldFrameSubst, List passiveCmds, ModelViewInfo mvInfo, Block containingBlock) { + Contract.Requires(c != null); + Contract.Requires(incarnationMap != null); + Contract.Requires(oldFrameSubst != null); + Contract.Requires(passiveCmds != null); + Contract.Requires(mvInfo != null); + Contract.Requires(containingBlock != null); + + Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap); + #region assert/assume P |--> assert/assume P[x := in(x)], out := in + if (c is PredicateCmd) { + Contract.Assert(c is AssertCmd || c is AssumeCmd); // otherwise, unexpected PredicateCmd type + + PredicateCmd pc = (PredicateCmd)c.Clone(); + Contract.Assert(pc != null); + + QKeyValue current = pc.Attributes; + while (current != null) + { + if (current.Key == "minimize" || current.Key == "maximize") { + Contract.Assume(current.Params.Count == 1); + var param = current.Params[0] as Expr; + Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv)); + current.ClearParams(); + current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param)); + } + if (current.Key == "verified_under") { + Contract.Assume(current.Params.Count == 1); + var param = current.Params[0] as Expr; + Contract.Assume(param != null && param.Type.IsBool); + current.ClearParams(); + current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param)); + } + current = current.Next; + } + + Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr); + if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) { + string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState"); + if (description != null) { + Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new List { Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count) }); + copy = Bpl.Expr.And(mv, copy); + mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, new Dictionary(incarnationMap))); + } + } + Contract.Assert(copy != null); + var dropCmd = false; + var relevantAssumpVars = currentImplementation != null ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap) : new List(); + var relevantDoomedAssumpVars = currentImplementation != null ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap) : new List(); + var checksum = pc.Checksum; + if (pc is AssertCmd) { + var ac = (AssertCmd)pc; + ac.OrigExpr = ac.Expr; + Contract.Assert(ac.IncarnationMap == null); + ac.IncarnationMap = (Dictionary)cce.NonNull(new Dictionary(incarnationMap)); + + var subsumption = Wlp.Subsumption(ac); + if (relevantDoomedAssumpVars.Any()) + { + TraceCachingAction(pc, CachingAction.DoNothingToAssert); + } + else if (currentImplementation != null + && currentImplementation.HasCachedSnapshot + && checksum != null + && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum) + && !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum)) + { + if (!currentImplementation.AnyErrorsInCachedSnapshot + && currentImplementation.InjectedAssumptionVariables.Count == 1 + && relevantAssumpVars.Count == 1) + { + TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified); + } + else + { + bool isTrue; + var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue); + TraceCachingAction(pc, !isTrue ? CachingAction.MarkAsPartiallyVerified : CachingAction.MarkAsFullyVerified); + var litExpr = ac.Expr as LiteralExpr; + if (litExpr == null || !litExpr.IsTrue) + { + ac.MarkAsVerifiedUnder(assmVars); + } + else + { + dropCmd = true; + } + } + } + else if (currentImplementation != null + && currentImplementation.HasCachedSnapshot + && relevantAssumpVars.Count == 0 + && checksum != null + && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum) + && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum)) + { + TraceCachingAction(pc, CachingAction.RecycleError); + ac.MarkAsVerifiedUnder(Expr.True); + currentImplementation.AddRecycledFailingAssertion(ac); + pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List(), pc.Attributes); + } + else + { + TraceCachingAction(pc, CachingAction.DoNothingToAssert); + } + } + else if (pc is AssumeCmd + && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot") + && pc.SugaredCmdChecksum != null) + { + if (!relevantDoomedAssumpVars.Any() + && currentImplementation.HasCachedSnapshot + && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.SugaredCmdChecksum) + && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.SugaredCmdChecksum)) + { + bool isTrue; + var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue); + if (!isTrue) + { + copy = LiteralExpr.Imp(assmVars, copy); + TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified); + } + else + { + TraceCachingAction(pc, CachingAction.MarkAsFullyVerified); + } + } + else + { + TraceCachingAction(pc, CachingAction.DropAssume); + dropCmd = true; + } + } + else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization")) + { + var identExpr = pc.Expr as IdentifierExpr; + if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl)) + { + incarnationMap[identExpr.Decl] = LiteralExpr.True; + dropCmd = true; + } + } + pc.Expr = copy; + if (!dropCmd) + { + passiveCmds.Add(pc); + } + } + #endregion + #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below] + else if (c is AssignCmd) { + AssignCmd assign = ((AssignCmd)c).AsSimpleAssignCmd; // first remove map assignments + Contract.Assert(assign != null); + #region Substitute all variables in E with the current map + List copies = new List(); + foreach (Expr e in assign.Rhss) { + Contract.Assert(e != null); + copies.Add(Substituter.ApplyReplacingOldExprs(incarnationSubst, + oldFrameSubst, + e)); + } + #endregion + + List!*/> assumptions = new List(); + // it might be too slow to create a new dictionary each time ... + IDictionary newIncarnationMappings = + new Dictionary(); + + for (int i = 0; i < assign.Lhss.Count; ++i) { + IdentifierExpr lhsIdExpr = + cce.NonNull((SimpleAssignLhs)assign.Lhss[i]).AssignedVariable; + Variable lhs = cce.NonNull(lhsIdExpr.Decl); + Contract.Assert(lhs != null); + Expr rhs = assign.Rhss[i]; + Contract.Assert(rhs != null); + + // don't create incarnations for assignments of literals or single variables. + if (rhs is LiteralExpr) { + incarnationMap[lhs] = rhs; + } else if (rhs is IdentifierExpr) { + IdentifierExpr ie = (IdentifierExpr)rhs; + if (incarnationMap.ContainsKey(cce.NonNull(ie.Decl))) + newIncarnationMappings[lhs] = cce.NonNull((Expr)incarnationMap[ie.Decl]); + else + newIncarnationMappings[lhs] = ie; + } else { + IdentifierExpr x_prime_exp = null; + #region Make a new incarnation, x', for variable x, but only if x is *not* already an incarnation + if (lhs is Incarnation) { + // incarnations are already written only once, no need to make an incarnation of an incarnation + x_prime_exp = lhsIdExpr; + } else { + Variable v = CreateIncarnation(lhs, c); + x_prime_exp = new IdentifierExpr(lhsIdExpr.tok, v); + newIncarnationMappings[lhs] = x_prime_exp; + } + #endregion + + var nAryExpr = copies[i] as NAryExpr; + if (nAryExpr != null) + { + var binOp = nAryExpr.Fun as BinaryOperator; + if (binOp != null + && binOp.Op == BinaryOperator.Opcode.And) + { + var arg0 = nAryExpr.Args[0] as LiteralExpr; + var arg1 = nAryExpr.Args[1] as LiteralExpr; + if ((arg0 != null && arg0.IsTrue) || (arg1 != null && arg1.IsFalse)) + { + // Replace the expressions "true && arg1" or "arg0 && false" by "arg1". + copies[i] = nAryExpr.Args[1]; + } + } + } + + #region Create an assume command with the new variable + assumptions.Add(TypedExprEq(x_prime_exp, copies[i], x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##cached##"))); + #endregion + } + } + + foreach (KeyValuePair pair in newIncarnationMappings) { + Contract.Assert(pair.Key != null && pair.Value != null); + incarnationMap[pair.Key] = pair.Value; + } + + if (assumptions.Count > 0) { + Expr assumption = assumptions[0]; + + for (int i = 1; i < assumptions.Count; ++i) { + Contract.Assert(assumption != null); + assumption = Expr.And(assumption, assumptions[i]); + } + passiveCmds.Add(new AssumeCmd(c.tok, assumption)); + } + + if (currentImplementation != null + && currentImplementation.HasCachedSnapshot + && !currentImplementation.AnyErrorsInCachedSnapshot + && currentImplementation.DoomedInjectedAssumptionVariables.Count == 0 + && currentImplementation.InjectedAssumptionVariables.Count == 1 + && assign.Lhss.Count == 1) + { + var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr; + Expr incarnation; + if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && incarnationMap.TryGetValue(identExpr.Decl, out incarnation)) + { + TraceCachingAction(assign, CachingAction.AssumeNegationOfAssumptionVariable); + passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation))); + } + } + } + #endregion + #region havoc w |--> assume whereClauses, out := in( w |-> w' ) + else if (c is HavocCmd) { + if (this.preHavocIncarnationMap == null) // Save a copy of the incarnation map (at the top of a sequence of havoc statements) + this.preHavocIncarnationMap = new Dictionary(incarnationMap); + + HavocCmd hc = (HavocCmd)c; + Contract.Assert(c != null); + // If an assumption variable for postconditions is included here, it must have been assigned within a loop. + // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop + // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the + // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map. + List havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##cached##"))).ToList(); + // First, compute the new incarnations + foreach (IdentifierExpr ie in havocVars) { + Contract.Assert(ie != null); + if (!(ie.Decl is Incarnation)) { + Variable x = cce.NonNull(ie.Decl); + Variable x_prime = CreateIncarnation(x, c); + incarnationMap[x] = new IdentifierExpr(x_prime.tok, x_prime); + } + } + // Then, perform the assume of the where clauses, using the updated incarnations + Substitution updatedIncarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap); + foreach (IdentifierExpr ie in havocVars) { + Contract.Assert(ie != null); + if (!(ie.Decl is Incarnation)) { + Variable x = cce.NonNull(ie.Decl); + Bpl.Expr w = x.TypedIdent.WhereExpr; + if (w != null) { + Expr copy = Substituter.ApplyReplacingOldExprs(updatedIncarnationSubst, oldFrameSubst, w); + passiveCmds.Add(new AssumeCmd(c.tok, copy)); + } + } + } + + // Add the following assume-statement for each assumption variable 'v', where 'v_post' is the new incarnation and 'v_pre' is the old one: + // assume v_post ==> v_pre; + foreach (IdentifierExpr ie in havocVars) + { + if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption")) + { + var preInc = (Expr)(preHavocIncarnationMap[ie.Decl].Clone()); + var postInc = (Expr)(incarnationMap[ie.Decl].Clone()); + passiveCmds.Add(new AssumeCmd(c.tok, Expr.Imp(postInc, preInc))); + } + } + } + #endregion + else if (c is CommentCmd) { + // comments are just for debugging and don't affect verification + } else if (c is SugaredCmd) { + SugaredCmd sug = (SugaredCmd)c; + Contract.Assert(sug != null); + Cmd cmd = sug.Desugaring; + Contract.Assert(cmd != null); + TurnIntoPassiveCmd(cmd, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, containingBlock); + } else if (c is StateCmd) { + this.preHavocIncarnationMap = null; // we do not need to remeber the previous incarnations + StateCmd st = (StateCmd)c; + Contract.Assert(st != null); + // account for any where clauses among the local variables + foreach (Variable v in st.Locals) { + Contract.Assert(v != null); + Expr w = v.TypedIdent.WhereExpr; + if (w != null) { + passiveCmds.Add(new AssumeCmd(v.tok, w)); + } + } + // do the sub-commands + foreach (Cmd s in st.Cmds) { + Contract.Assert(s != null); + TurnIntoPassiveCmd(s, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, containingBlock); + } + // remove the local variables from the incarnation map + foreach (Variable v in st.Locals) { + Contract.Assert(v != null); + incarnationMap.Remove(v); + } + } + #region There shouldn't be any other types of commands at this point + else { + Debug.Fail("Internal Error: Passive transformation handed a command that is not one of assert,assume,havoc,assign."); + } + #endregion + + + #region We remember if we have put an havoc statement into a passive form + + if (!(c is HavocCmd)) + this.preHavocIncarnationMap = null; + // else: it has already been set by the case for the HavocCmd + #endregion + } + + NAryExpr TypedExprEq(Expr e0, Expr e1, bool doNotResolveOverloading = false) { + Contract.Requires(e0 != null); + Contract.Requires(e1 != null); + NAryExpr e = Expr.Eq(e0, e1); + var fun = e.Fun as IOverloadedAppliable; + if (fun != null) + { + fun.DoNotResolveOverloading = doNotResolveOverloading; + } + e.Type = Bpl.Type.Bool; + e.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + return e; + } + + /// + /// Creates a new block to add to impl.Blocks, where impl is the implementation that contains + /// succ. Caller must do the add to impl.Blocks. + /// + protected Block CreateBlockBetween(int predIndex, Block succ) { + Contract.Requires(0 <= predIndex && predIndex < succ.Predecessors.Count); + + + Contract.Requires(succ != null); + Contract.Ensures(Contract.Result() != null); + + Block pred = cce.NonNull(succ.Predecessors[predIndex]); + + string newBlockLabel = pred.Label + "_@2_" + succ.Label; + + // successor of newBlock list + List ls = new List(); + ls.Add(succ.Label); + List bs = new List(); + bs.Add(succ); + + Block newBlock = new Block( + new Token(-17, -4), + newBlockLabel, + new List(), + new GotoCmd(Token.NoToken, ls, bs) + ); + + // predecessors of newBlock + List ps = new List(); + ps.Add(pred); + newBlock.Predecessors = ps; + + // fix successors of pred + #region Change the edge "pred->succ" to "pred->newBlock" + GotoCmd gtc = (GotoCmd)cce.NonNull(pred.TransferCmd); + Contract.Assume(gtc.labelTargets != null); + Contract.Assume(gtc.labelNames != null); + for (int i = 0, n = gtc.labelTargets.Count; i < n; i++) { + if (gtc.labelTargets[i] == succ) { + gtc.labelTargets[i] = newBlock; + gtc.labelNames[i] = newBlockLabel; + break; + } + } + #endregion Change the edge "pred->succ" to "pred->newBlock" + + // fix predecessors of succ + succ.Predecessors[predIndex] = newBlock; + + return newBlock; + } + + protected void AddBlocksBetween(List blocks) { + Contract.Requires(blocks != null); + #region Introduce empty blocks between join points and their multi-successor predecessors + List tweens = new List(); + foreach (Block b in blocks) { + int nPreds = b.Predecessors.Count; + if (nPreds > 1) { + // b is a join point (i.e., it has more than one predecessor) + for (int i = 0; i < nPreds; i++) { + GotoCmd gotocmd = (GotoCmd)(cce.NonNull(b.Predecessors[i]).TransferCmd); + if (gotocmd.labelNames != null && gotocmd.labelNames.Count > 1) { + tweens.Add(CreateBlockBetween(i, b)); + } + } + } + } + blocks.AddRange(tweens); // must wait until iteration is done before changing the list + #endregion + } + + + public void Dispose() + { + Dispose(true); + GC.SuppressFinalize(this); + } + + protected virtual void Dispose(bool disposing) + { + if (!_disposed) + { + if (disposing) + { + Close(); + } + _disposed = true; + } + } + + public int Cores { get; set; } + } + + public class ModelViewInfo + { + public readonly List AllVariables = new List(); + public readonly List CapturePoints = new List(); + public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "$mv_state", + new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true), + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true) }, + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false)); + public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "$mv_state_const", Bpl.Type.Int)); + + public ModelViewInfo(Program program, Implementation impl) { + Contract.Requires(program != null); + Contract.Requires(impl != null); + + // global variables + lock (program.TopLevelDeclarations) + { + foreach (var v in program.Variables) + { + if (!(v is Constant)) + { + AllVariables.Add(v); + } + } + } + // implementation parameters + foreach (Variable p in impl.InParams) { + AllVariables.Add(p); + } + foreach (Variable p in impl.OutParams) { + AllVariables.Add(p); + } + // implementation locals + foreach (Variable v in impl.LocVars) { + AllVariables.Add(v); + } + } + + public ModelViewInfo(CodeExpr codeExpr) { + Contract.Requires(codeExpr != null); + // TODO: also need all variables of enclosing scopes (the global variables of the program, the parameters + // and perhaps locals of the implementation (if any), any enclosing code expressions). + + foreach (Variable v in codeExpr.LocVars) { + AllVariables.Add(v); + } + } + + public class Mapping + { + public readonly string Description; + public readonly Dictionary IncarnationMap; + public Mapping(string description, Dictionary incarnationMap) { + Description = description; + IncarnationMap = incarnationMap; + } + } + } +} -- cgit v1.2.3