diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Source/VCGeneration | |
Initial set of files.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.ssc | 375 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.ssc | 790 | ||||
| -rw-r--r-- | Source/VCGeneration/Context.ssc | 199 | ||||
| -rw-r--r-- | Source/VCGeneration/OrderingAxioms.ssc | 285 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 3215 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.ssc | 817 | ||||
| -rw-r--r-- | Source/VCGeneration/VCGeneration.sscproj | 142 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.ssc | 131 |
8 files changed, 5954 insertions, 0 deletions
diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc new file mode 100644 index 00000000..f0d6c558 --- /dev/null +++ b/Source/VCGeneration/Check.ssc @@ -0,0 +1,375 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie
+{
+ /// <summary>
+ /// Interface to the theorem prover specialized to Boogie.
+ ///
+ /// This class creates the appropriate background axioms. There
+ /// should be one instance per BoogiePL program.
+ /// </summary>
+ public sealed class Checker
+ {
+ private readonly VCExpressionGenerator! gen;
+
+ private ProverInterface! thmProver;
+ private CommandLineOptions.BvHandling bitvectors;
+ private int timeout;
+
+ // state for the async interface
+ private volatile ProverInterface.Outcome outcome;
+ private volatile bool busy;
+ private volatile bool hasOutput;
+ private volatile UnexpectedProverOutputException outputExn;
+ private DateTime proverStart;
+ private TimeSpan proverRunTime;
+ private volatile ProverInterface.ErrorHandler handler;
+ private volatile bool closed;
+
+ public readonly AutoResetEvent! ProverDone = new AutoResetEvent(false);
+
+ private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation! impl)
+ {
+ bool force_int = false;
+ bool force_native = false;
+ ((!)impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);
+ impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native);
+ impl.CheckBooleanAttribute("forceBvInt", ref force_int);
+ impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native);
+ if (force_native) return CommandLineOptions.BvHandling.Z3Native;
+ if (force_int) return CommandLineOptions.BvHandling.ToInt;
+ return CommandLineOptions.Clo.Bitvectors;
+ }
+
+ public bool WillingToHandle(Implementation! impl, int timeout)
+ {
+ return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl);
+ }
+
+ public VCExpressionGenerator! VCExprGen
+ {
+ get { return this.gen; }
+ }
+ public ProverInterface! TheoremProver
+ {
+ get { return this.thmProver; }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // We share context information for the same program between different Checkers
+
+ private struct ContextCacheKey {
+ public readonly Program! program;
+ public readonly CommandLineOptions.BvHandling bitvectors;
+
+ public ContextCacheKey(Program! prog,
+ CommandLineOptions.BvHandling bitvectors) {
+ this.program = prog;
+ this.bitvectors = bitvectors;
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (that is ContextCacheKey) {
+ ContextCacheKey thatKey = (ContextCacheKey)that;
+ return this.program.Equals(thatKey.program) &&
+ this.bitvectors.Equals(thatKey.bitvectors);
+ }
+ return false;
+ }
+
+ [Pure]
+ public override int GetHashCode() {
+ return this.program.GetHashCode() + this.bitvectors.GetHashCode();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+
+ /// <summary>
+ /// Constructor. Initialize a the checker with the program and log file.
+ /// </summary>
+ public Checker(VC.ConditionGeneration! vcgen, Program! prog, string/*?*/ logFilePath, bool appendLogFile, Implementation! impl, int timeout)
+ {
+ this.bitvectors = BvHandlingForImpl(impl);
+ this.timeout = timeout;
+
+ ProverOptions! options = ((!)CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
+
+ if (logFilePath != null) {
+ options.LogFilename = logFilePath;
+ if (appendLogFile)
+ options.AppendLogFile = appendLogFile;
+ }
+
+ options.Parse(CommandLineOptions.Clo.ProverOptions);
+
+ if (timeout > 0) {
+ options.TimeLimit = timeout * 1000;
+ }
+ options.BitVectors = this.bitvectors;
+
+ ContextCacheKey key = new ContextCacheKey (prog, this.bitvectors);
+ ProverContext ctx;
+ ProverInterface prover;
+
+ if (vcgen.CheckerCommonState == null) {
+ vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext!> ();
+ }
+ IDictionary<ContextCacheKey, ProverContext!>! cachedContexts = (IDictionary<ContextCacheKey, ProverContext!>) vcgen.CheckerCommonState;
+
+ if (cachedContexts.TryGetValue(key, out ctx)) {
+ ctx = (ProverContext!)((!)ctx).Clone();
+ prover = (ProverInterface)
+ CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
+ } else {
+ ctx = (ProverContext!)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
+
+ // set up the context
+ foreach (Declaration! decl in prog.TopLevelDeclarations) {
+ TypeCtorDecl t = decl as TypeCtorDecl;
+ if (t != null) {
+ ctx.DeclareType(t, null);
+ }
+ }
+ foreach (Declaration! decl in prog.TopLevelDeclarations) {
+ Constant c = decl as Constant;
+ if (c != null) {
+ ctx.DeclareConstant(c, c.Unique, null);
+ } else {
+ Function f = decl as Function;
+ if (f != null) {
+ ctx.DeclareFunction(f, null);
+ }
+ }
+ }
+ foreach (Declaration! decl in prog.TopLevelDeclarations) {
+ bool expand = false;
+ Axiom ax = decl as Axiom;
+ decl.CheckBooleanAttribute("inline", ref expand);
+ if (!expand && ax != null) {
+ ctx.AddAxiom(ax, null);
+ }
+ }
+ foreach (Declaration! decl in prog.TopLevelDeclarations) {
+ GlobalVariable v = decl as GlobalVariable;
+ if (v != null) {
+ ctx.DeclareGlobalVariable(v, null);
+ }
+ }
+
+ // we first generate the prover and then store a clone of the
+ // context in the cache, so that the prover can setup stuff in
+ // the context to be cached
+ prover = (ProverInterface)
+ CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
+ cachedContexts.Add(key, (ProverContext!)ctx.Clone());
+ }
+
+ this.thmProver = prover;
+ this.gen = prover.VCExprGen;
+
+ // base();
+ }
+
+
+ /// <summary>
+ /// Clean-up.
+ /// </summary>
+ public void Close()
+ {
+ this.closed = true;
+ thmProver.Close();
+ }
+
+ /// <summary>
+ /// Push a Verification Condition as an Axiom
+ /// (Required for Doomed Program Point detection)
+ /// </summary>
+ public void PushVCExpr(VCExpr! vc)
+ {
+ //thmProver.Context.AddAxiom(vc);
+ thmProver.PushVCExpression(vc);
+ }
+
+ public bool IsBusy
+ {
+ get { return busy; }
+ }
+
+ public bool Closed
+ {
+ get { return closed; }
+ }
+
+ public bool HasOutput
+ {
+ get { return hasOutput; }
+ }
+
+ public TimeSpan ProverRunTime
+ {
+ get { return proverRunTime; }
+ }
+
+ private void WaitForOutput(object dummy)
+ {
+ try {
+ outcome = thmProver.CheckOutcome((!)handler);
+ } catch (UnexpectedProverOutputException e) {
+ outputExn = e;
+ }
+
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid:
+ thmProver.LogComment("Valid");
+ break;
+ case ProverInterface.Outcome.Invalid:
+ thmProver.LogComment("Invalid");
+ break;
+ case ProverInterface.Outcome.TimeOut:
+ thmProver.LogComment("Timed out");
+ break;
+ case ProverInterface.Outcome.OutOfMemory:
+ thmProver.LogComment("Out of memory");
+ break;
+ case ProverInterface.Outcome.Undetermined:
+ thmProver.LogComment("Undetermined");
+ break;
+ }
+
+ assert busy;
+ hasOutput = true;
+ proverRunTime = DateTime.Now - proverStart;
+
+ ProverDone.Set();
+ }
+
+ public void BeginCheck(string! descriptiveName, VCExpr! vc, ProverInterface.ErrorHandler! handler)
+ requires !IsBusy;
+ {
+ assert !busy;
+ busy = true;
+ hasOutput = false;
+ outputExn = null;
+ this.handler = handler;
+
+ proverStart = DateTime.Now;
+ thmProver.BeginCheck(descriptiveName, vc, handler);
+ // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
+
+ ThreadPool.QueueUserWorkItem(WaitForOutput);
+ }
+
+ public ProverInterface.Outcome ReadOutcome()
+ throws UnexpectedProverOutputException;
+ requires IsBusy;
+ requires HasOutput;
+ {
+ hasOutput = false;
+ busy = false;
+
+ if (outputExn != null) {
+ throw outputExn;
+ }
+
+ return outcome;
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public class ErrorModel {
+ public Dictionary<string!, int>! identifierToPartition;
+ public List<List<string!>>! partitionToIdentifiers;
+ public List<Object>! partitionToValue;
+ public Dictionary<object, int>! valueToPartition;
+ public Dictionary<string!, List<List<int>>!>! definedFunctions;
+
+ public ErrorModel(Dictionary<string!, int>! identifierToPartition, List<List<string!>>! partitionToIdentifiers, List<Object>! partitionToValue, Dictionary<object, int>! valueToPartition, Dictionary<string!, List<List<int>>!>! definedFunctions) {
+ this.identifierToPartition = identifierToPartition;
+ this.partitionToIdentifiers = partitionToIdentifiers;
+ this.partitionToValue = partitionToValue;
+ this.valueToPartition = valueToPartition;
+ this.definedFunctions = definedFunctions;
+ }
+
+ public virtual void Print(TextWriter! writer) { }
+ }
+
+ public abstract class ProverInterface
+ {
+ public enum Outcome { Valid, Invalid, TimeOut, OutOfMemory, Undetermined }
+
+ public class ErrorHandler
+ {
+ public virtual void OnModel(IList<string!>! labels, ErrorModel errModel)
+ {
+ }
+
+ public virtual void OnResourceExceeded(string! message)
+ {
+ }
+
+ public virtual Absy! Label2Absy(string! label)
+ {
+ throw new System.NotImplementedException();
+ }
+ }
+
+ public abstract void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler);
+ [NoDefaultContract]
+ public abstract Outcome CheckOutcome(ErrorHandler! handler);
+ throws UnexpectedProverOutputException;
+
+ public virtual void LogComment(string! comment) {
+ }
+
+ public virtual void Close() {
+ }
+
+ /// <summary>
+ /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
+ /// for now it is only implemented by ProcessTheoremProver and still requires some
+ /// testing
+ /// </summary>
+ public virtual void PushVCExpression(VCExpr! vc) {}
+
+ public abstract ProverContext! Context { get; }
+ public abstract VCExpressionGenerator! VCExprGen { get; }
+ }
+
+ public class ProverException : Exception
+ {
+ public ProverException(string s) : base(s)
+ {
+ }
+ }
+ public class UnexpectedProverOutputException : ProverException, ICheckedException
+ {
+ public UnexpectedProverOutputException(string s) : base(s)
+ {
+ }
+ }
+ public class ProverDiedException : UnexpectedProverOutputException
+ {
+ public ProverDiedException() : base("Prover died with no further output, perhaps it ran out of memory or was killed.")
+ {
+ }
+ }
+}
diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc new file mode 100644 index 00000000..2129b1fb --- /dev/null +++ b/Source/VCGeneration/ConditionGeneration.ssc @@ -0,0 +1,790 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Graphing;
+using AI = Microsoft.AbstractInterpretationFramework;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie
+{
+ public abstract class Counterexample
+ {
+ [Peer] public BlockSeq! Trace;
+ [Peer] public List<string!>! relatedInformation;
+
+ internal Counterexample(BlockSeq! trace)
+ {
+ this.Trace = trace;
+ this.relatedInformation = new List<string!>();
+ // base();
+ }
+
+ public abstract int GetLocation();
+ }
+
+ public class CounterexampleComparer : IComparer<Counterexample!>
+ {
+ public int Compare(Counterexample! c1, Counterexample! c2) {
+ if (c1.GetLocation() == c2.GetLocation()) return 0;
+ if (c1.GetLocation() > c2.GetLocation()) return 1;
+ return -1;
+ }
+ }
+
+ public class AssertCounterexample : Counterexample
+ {
+ [Peer] public AssertCmd! FailingAssert;
+
+ public AssertCounterexample(BlockSeq! trace, AssertCmd! failingAssert)
+ : base(trace)
+ {
+ this.FailingAssert = failingAssert;
+ // base(trace);
+ }
+
+ public override int GetLocation() {
+ return FailingAssert.tok.line * 1000 + FailingAssert.tok.col;
+ }
+ }
+
+ public class CallCounterexample : Counterexample
+ {
+ public CallCmd! FailingCall;
+ public Requires! FailingRequires;
+
+ public CallCounterexample(BlockSeq! trace, CallCmd! failingCall, Requires! failingRequires)
+ : base(trace)
+ requires !failingRequires.Free;
+ {
+ this.FailingCall = failingCall;
+ this.FailingRequires = failingRequires;
+ // base(trace);
+ }
+
+ public override int GetLocation() {
+ return FailingCall.tok.line * 1000 + FailingCall.tok.col;
+ }
+ }
+
+ public class ReturnCounterexample : Counterexample
+ {
+ public TransferCmd! FailingReturn;
+ public Ensures! FailingEnsures;
+
+ public ReturnCounterexample(BlockSeq! trace, TransferCmd! failingReturn, Ensures! failingEnsures)
+ : base(trace)
+ requires !failingEnsures.Free;
+ {
+ this.FailingReturn = failingReturn;
+ this.FailingEnsures = failingEnsures;
+ // base(trace);
+ }
+
+ public override int GetLocation() {
+ return FailingReturn.tok.line * 1000 + FailingReturn.tok.col;
+ }
+ }
+
+ 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)
+ {
+ }
+
+ // called in case resource is exceeded and we don't have counterexample
+ public virtual void OnTimeout(string! reason)
+ {
+ }
+
+ public virtual void OnOutOfMemory(string! reason)
+ {
+ }
+
+ public virtual void OnProgress(string phase, int step, int totalSteps, double progressEstimate)
+ {
+ }
+
+ public virtual void OnUnreachableCode(Implementation! impl)
+ {
+ }
+ }
+}
+
+////////////////////////////////////////////
+
+namespace VC
+{
+ using Bpl = Microsoft.Boogie;
+
+ public class VCGenException : Exception
+ {
+ public VCGenException(string s) : base(s)
+ {
+ }
+ }
+
+ public abstract class ConditionGeneration
+ {
+ protected internal object CheckerCommonState;
+
+ public enum Outcome { Correct, Errors, TimedOut, OutOfMemory, Inconclusive }
+
+ protected readonly List<Checker!>! provers = new List<Checker!>();
+ protected Implementation current_impl = null;
+
+
+ // shared across each implementation; created anew for each implementation
+ protected Hashtable /*Variable -> int*/ variable2SequenceNumber;
+ public Dictionary<Incarnation, Absy!>! incarnationOriginMap = new Dictionary<Incarnation, Absy!>();
+
+ // used only by FindCheckerFor
+ protected Program! program;
+ protected string/*?*/ logFilePath;
+ protected bool appendLogFile;
+
+ public ConditionGeneration(Program! p)
+ {
+ program = p;
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ /// <param name="impl"></param>
+ public Outcome VerifyImplementation(Implementation! impl, Program! program, out List<Counterexample!>? errors)
+ ensures result == Outcome.Errors ==> errors != null;
+ throws UnexpectedProverOutputException;
+ {
+ Helpers.ExtraTraceInformation("Starting implementation verification");
+
+ CounterexampleCollector collector = new CounterexampleCollector();
+ Outcome outcome = VerifyImplementation(impl, program, collector);
+ if (outcome == Outcome.Errors) {
+ errors = collector.examples;
+ } else {
+ errors = null;
+ }
+
+ Helpers.ExtraTraceInformation("Finished implementation verification");
+ return outcome;
+ }
+
+ public abstract Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)
+ throws UnexpectedProverOutputException;
+
+
+/////////////////////////////////// Common Methods and Classes //////////////////////////////////////////
+
+ protected Checker! FindCheckerFor(Implementation! impl, int timeout)
+ {
+ int i = 0;
+ while (i < provers.Count) {
+ if (provers[i].Closed) {
+ provers.RemoveAt(i);
+ continue;
+ } else {
+ if (!provers[i].IsBusy && provers[i].WillingToHandle(impl, timeout)) return provers[i];
+ }
+ ++i;
+ }
+ string? log = logFilePath;
+ if (log != null && !log.Contains("@PROC@") && provers.Count > 0)
+ log = log + "." + provers.Count;
+ Checker! ch = new Checker(this, program, log, appendLogFile, impl, timeout);
+ provers.Add(ch);
+ return ch;
+ }
+
+
+ public void Close() { foreach (Checker! prover in provers) prover.Close(); }
+
+
+ protected class CounterexampleCollector : VerifierCallback
+ {
+ public readonly List<Counterexample!>! examples = new List<Counterexample!>();
+ public override void OnCounterexample(Counterexample! ce, string? reason)
+ {
+ examples.Add(ce);
+ }
+
+ public override void OnUnreachableCode(Implementation! impl)
+ {
+ 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) {
+ 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>", Console.Out, false), 0);
+ CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;
+ CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
+
+
+ protected Block! GenerateUnifiedExit(Implementation! impl, Hashtable! gotoCmdOrigins)
+ {
+ 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 CmdSeq(),new ReturnCmd(Token.NoToken));
+
+ foreach ( Block b in impl.Blocks )
+ {
+ if ( b.TransferCmd is ReturnCmd )
+ {
+ StringSeq labels = new StringSeq();
+ labels.Add(unifiedExitLabel);
+ BlockSeq bs = new BlockSeq();
+ bs.Add(unifiedExit);
+ GotoCmd go = new GotoCmd(Token.NoToken,labels,bs);
+ gotoCmdOrigins[go] = b.TransferCmd;
+ b.TransferCmd = go;
+ unifiedExit.Predecessors.Add(b);
+ }
+ }
+
+ exitBlock = unifiedExit;
+ impl.Blocks.Add(unifiedExit);
+ }
+ assert exitBlock != null;
+ }
+ return exitBlock;
+ #endregion
+ }
+
+ /// <summary>
+ /// Helperfunction to restore the predecessor relations after loop unrolling
+ /// </summary>
+ protected void ComputePredecessors(List<Block!>! blocks)
+ {
+ #region Compute and store the Predecessor Relation on the blocks
+ // This code just here to try things out.
+ // Compute the predecessor relation for each block
+ // Store it in the Predecessors field within each block
+ foreach (Block b in blocks)
+ {
+ GotoCmd gtc = b.TransferCmd as GotoCmd;
+ if (gtc != null)
+ {
+ assume gtc.labelTargets != null;
+ foreach (Block! dest in gtc.labelTargets)
+ {
+ dest.Predecessors.Add(b);
+ }
+ }
+ }
+ #endregion Compute and store the Predecessor Relation on the blocks
+ }
+
+ protected static void ResetPredecessors(List<Block!>! blocks)
+ {
+ foreach (Block! b in blocks) {
+ b.Predecessors = new BlockSeq();
+ }
+ foreach (Block! b in blocks) {
+ foreach (Block! ch in Exits(b)) {
+ ch.Predecessors.Add(b);
+ }
+ }
+ }
+
+ protected static IEnumerable! Exits(Block! b)
+ {
+ GotoCmd g = b.TransferCmd as GotoCmd;
+ if (g != null) {
+ return (!)g.labelTargets;
+ }
+ return new List<Block!>();
+ }
+
+
+ protected Variable! CreateIncarnation(Variable! x, Absy a)
+ requires this.variable2SequenceNumber != null;
+ requires this.current_impl != null;
+ requires a is Block || a is AssignCmd || a is HavocCmd;
+ {
+ int currentIncarnationNumber =
+ variable2SequenceNumber.ContainsKey(x)
+ ?
+ (int) ((!)variable2SequenceNumber[x])
+ :
+ -1;
+ Variable v = new Incarnation(x,currentIncarnationNumber + 1);
+ variable2SequenceNumber[x] = currentIncarnationNumber + 1;
+ Debug.Assert(current_impl != null, "The field current_impl wasn't set.");
+ current_impl.LocVars.Add(v);
+ incarnationOriginMap.Add((Incarnation) v, a);
+ return v;
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ /// <param name="b"></param>
+ /// <param name="block2Incarnation">Gives incarnation maps for b's predecessors.</param>
+ /// <returns></returns>
+ protected Hashtable! /*Variable -> Expr*/ ComputeIncarnationMap(Block! b, Hashtable! /*Variable -> Expr*/ block2Incarnation)
+ {
+ if (b.Predecessors.Length == 0)
+ {
+ return new Hashtable /*Variable -> Expr*/ ();
+ }
+
+ Hashtable /*Variable -> Expr*/ incarnationMap = null;
+ Set /*Variable*/ fixUps = new Set /*Variable*/ ();
+ foreach (Block! pred in b.Predecessors)
+ {
+ Debug.Assert(block2Incarnation.Contains(pred), "Passive Transformation found a block whose predecessors have not been processed yet.");
+ Hashtable /*Variable -> Expr*/ predMap = (Hashtable! /*Variable -> Expr*/) block2Incarnation[pred];
+ if (incarnationMap == null)
+ {
+ incarnationMap = (Hashtable /*Variable -> Expr*/)predMap.Clone();
+ continue;
+ }
+
+ ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ ();
+ foreach (Variable! v in incarnationMap.Keys)
+ {
+ if (!predMap.Contains(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)
+ {
+ incarnationMap.Remove(v);
+ }
+ foreach (Variable! v in predMap.Keys)
+ {
+ if (!incarnationMap.Contains(v))
+ {
+ // v was not in the domain of the precessors 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 )
+ {
+ Variable v_prime = CreateIncarnation(v, b);
+ IdentifierExpr ie = new IdentifierExpr(v_prime.tok, v_prime);
+ assert incarnationMap != null;
+ incarnationMap[v] = ie;
+ foreach (Block! pred in b.Predecessors )
+ {
+ #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
+ Hashtable /*Variable -> Expr*/ predMap = (Hashtable! /*Variable -> Expr*/) block2Incarnation[pred];
+ Expr pred_incarnation_exp;
+ Expr o = (Expr) predMap[v];
+ 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
+ Expr e = Expr.Binary(Token.NoToken,
+ BinaryOperator.Opcode.Eq,
+ v_prime_exp,
+ pred_incarnation_exp
+ );
+ AssumeCmd ac = new AssumeCmd(v.tok,e);
+ pred.Cmds.Add(ac);
+ #endregion
+ #endregion
+ }
+ }
+ #endregion
+
+ assert incarnationMap != null;
+ return incarnationMap;
+ }
+
+ Hashtable 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, Hashtable! /*Variable -> Expr*/ incarnationMap, Substitution! oldFrameSubst)
+ {
+ #region Walk forward over the commands in this block and convert them to passive commands
+
+ CmdSeq passiveCmds = new CmdSeq();
+ foreach (Cmd! c in b.Cmds)
+ { // walk forward over the commands because the map gets modified in a forward direction
+ TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds);
+ }
+ b.Cmds = passiveCmds;
+
+ #endregion
+ }
+
+
+ protected void Convert2PassiveCmd(Implementation! impl)
+ {
+ #region Convert to Passive Commands
+
+ #region Topological sort -- need to process in a linearization of the partial order
+ Graph<Block> dag = new Graph<Block>();
+ dag.AddSource((!)impl.Blocks[0]); // there is always at least one node in the graph
+ foreach (Block b in impl.Blocks)
+ {
+ GotoCmd gtc = b.TransferCmd as GotoCmd;
+ if (gtc != null)
+ {
+ assume gtc.labelTargets != null;
+ foreach (Block! dest in gtc.labelTargets)
+ {
+ dag.AddEdge(b,dest);
+ }
+ }
+ }
+ IEnumerable! sortedNodes = dag.TopologicalSort();
+ //Debug.Assert( sortedNodes != null, "Topological Sort returned null." );
+ #endregion
+
+ // Create substitution for old expressions
+ Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();
+ assume impl.Proc != null;
+ foreach (IdentifierExpr! ie in impl.Proc.Modifies) {
+ oldFrameMap.Add((!)ie.Decl, ie);
+ }
+ Substitution oldFrameSubst = Substituter.SubstitutionFromHashtable(oldFrameMap);
+
+ // Now we can process the nodes in an order so that we're guaranteed to have
+ // processed all of a node's predecessors before we process the node.
+ Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();
+ foreach (Block! b in sortedNodes )
+ {
+ Debug.Assert( !block2Incarnation.Contains(b) );
+ Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);
+
+ #region Each block's map needs to be available to successor blocks
+ block2Incarnation.Add(b,incarnationMap);
+ #endregion Each block's map needs to be available to successor blocks
+
+ TurnIntoPassiveBlock(b, incarnationMap, oldFrameSubst);
+ }
+
+ // We no longer need the where clauses on the out parameters, so we remove them to restore the situation from before VC generation
+ foreach (Formal! f in impl.OutParams) {
+ f.TypedIdent.WhereExpr = null;
+ }
+ #endregion Convert to Passive Commands
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ Console.WriteLine("after conversion to passive commands");
+ EmitImpl(impl, true);
+ }
+ #endregion
+ }
+
+ /// <summary>
+ /// 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 remebers the incarnation map BEFORE the havoc
+ /// </summary>
+ protected void TurnIntoPassiveCmd(Cmd! c, Hashtable /*Variable -> Expr*/! incarnationMap, Substitution! oldFrameSubst, CmdSeq! passiveCmds)
+ {
+ Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap);
+ #region assert/assume P |--> assert/assume P[x := in(x)], out := in
+ if ( c is PredicateCmd )
+ {
+ Debug.Assert( c is AssertCmd || c is AssumeCmd, "Internal Error: Found a PredicateCmd h is not an assert or an assume." );
+
+ PredicateCmd! pc = (PredicateCmd) c.Clone();
+
+ if(pc is AssumeCmd && pc.Expr is LoopPredicate // Check if the PredicateCmd is in the form of "assume J", with J loop invariant predicate
+ && this.preHavocIncarnationMap != null) // Furthermore, the command just before was a (list of) havoc statements
+ {
+ LoopPredicate! lp = (LoopPredicate!) pc.Expr;
+ lp.SetPreAndPostHavocIncarnationMaps(this.preHavocIncarnationMap, (Hashtable /*Variable -> Expr*/!) incarnationMap.Clone());
+ }
+
+ Expr! copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
+ if (pc is AssertCmd) {
+ ((AssertCmd) pc).OrigExpr = pc.Expr;
+ assert ((AssertCmd) pc).IncarnationMap == null;
+ ((AssertCmd) pc).IncarnationMap = (Hashtable /*Variable -> Expr*/!) incarnationMap.Clone();
+ }
+ pc.Expr = copy;
+ 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
+ #region Substitute all variables in E with the current map
+ List<Expr!>! copies = new List<Expr!> ();
+ foreach (Expr! e in assign.Rhss)
+ copies.Add(Substituter.ApplyReplacingOldExprs(incarnationSubst,
+ oldFrameSubst,
+ e));
+ #endregion
+
+ List<Expr!>! assumptions = new List<Expr!> ();
+ // it might be too slow to create a new dictionary each time ...
+ IDictionary<Variable!, Expr!>! newIncarnationMappings =
+ new Dictionary<Variable!, Expr!> ();
+
+ for (int i = 0; i < assign.Lhss.Count; ++i) {
+ IdentifierExpr! lhsIdExpr =
+ ((SimpleAssignLhs!)assign.Lhss[i]).AssignedVariable;
+ Variable! lhs = (!)lhsIdExpr.Decl;
+ Expr! rhs = assign.Rhss[i];
+
+ // 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((!)ie.Decl) )
+ newIncarnationMappings[lhs] = (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
+ #region Create an assume command with the new variable
+ assumptions.Add(Expr.Eq(x_prime_exp, copies[i]));
+ #endregion
+ }
+ }
+
+ foreach (KeyValuePair<Variable!, Expr!> pair in newIncarnationMappings)
+ incarnationMap[pair.Key] = pair.Value;
+
+ if (assumptions.Count > 0) {
+ Expr! assumption = assumptions[0];
+ for (int i = 1; i < assumptions.Count; ++i)
+ assumption = Expr.And(assumption, assumptions[i]);
+ passiveCmds.Add(new AssumeCmd(c.tok, assumption));
+ }
+ }
+ #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 = (Hashtable) incarnationMap.Clone();
+
+ HavocCmd! hc = (HavocCmd) c;
+ IdentifierExprSeq havocVars = hc.Vars;
+ // First, compute the new incarnations
+ foreach (IdentifierExpr! ie in havocVars)
+ {
+ if ( !(ie.Decl is Incarnation) )
+ {
+ Variable x = (!)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)
+ {
+ if ( !(ie.Decl is Incarnation) )
+ {
+ Variable x = (!)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;
+ Cmd! cmd = sug.Desugaring;
+ TurnIntoPassiveCmd(cmd, incarnationMap, oldFrameSubst, passiveCmds);
+ }
+ else if (c is StateCmd)
+ {
+ this.preHavocIncarnationMap = null; // we do not need to remeber the previous incarnations
+ StateCmd! st = (StateCmd)c;
+ // account for any where clauses among the local variables
+ foreach (Variable! v in st.Locals) {
+ 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) {
+ TurnIntoPassiveCmd(s, incarnationMap, oldFrameSubst, passiveCmds);
+ }
+ // remove the local variables from the incarnation map
+ foreach (Variable! v in st.Locals) {
+ 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 rember 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
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ protected Block! CreateBlockBetween(int predIndex, Block! succ)
+ requires 0 <= predIndex && predIndex < succ.Predecessors.Length;
+ {
+ Block! pred = (!) succ.Predecessors[predIndex];
+
+ string! newBlockLabel = pred.Label + "_@2_" + succ.Label;
+
+ // successor of newBlock list
+ StringSeq ls = new StringSeq();
+ ls.Add(succ.Label);
+ BlockSeq bs = new BlockSeq();
+ bs.Add(succ);
+
+ Block newBlock = new Block(
+ new Token(-17, -4),
+ newBlockLabel,
+ new CmdSeq(),
+ new GotoCmd(Token.NoToken,ls,bs)
+ );
+
+ // predecessors of newBlock
+ BlockSeq ps = new BlockSeq();
+ ps.Add(pred);
+ newBlock.Predecessors = ps;
+
+ // fix successors of pred
+ #region Change the edge "pred->succ" to "pred->newBlock"
+ GotoCmd gtc = (GotoCmd!) pred.TransferCmd;
+ assume gtc.labelTargets != null;
+ assume gtc.labelNames != null;
+ for ( int i = 0, n = gtc.labelTargets.Length; 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(Implementation! impl)
+ {
+ #region Introduce empty blocks before all blocks with more than one predecessor
+ List<Block!> tweens = new List<Block!>();
+ foreach ( Block b in impl.Blocks )
+ {
+ int nPreds = b.Predecessors.Length;
+ if ( nPreds > 1 )
+ {
+ for (int i = 0; i < nPreds; i++ )
+ {
+ tweens.Add(CreateBlockBetween(i, b));
+ }
+ }
+ }
+ impl.Blocks.AddRange(tweens); // must wait until iteration is done before changing the list
+ #endregion
+ }
+
+ }
+}
\ No newline at end of file diff --git a/Source/VCGeneration/Context.ssc b/Source/VCGeneration/Context.ssc new file mode 100644 index 00000000..be32cabe --- /dev/null +++ b/Source/VCGeneration/Context.ssc @@ -0,0 +1,199 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Text;
+using Microsoft.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie
+{
+ /// <summary>
+ /// The methods of this class are called in the following order:
+ /// DeclareType*
+ /// (DeclareConstant DeclareFunction)*
+ /// AddAxiom*
+ /// DeclareGlobalVariable*
+ /// At this time, all "attributes" are passed in as null.
+ /// </summary>
+ public abstract class ProverContext : ICloneable {
+ protected virtual void ProcessDeclaration(Declaration! decl) {}
+ public virtual void DeclareType(TypeCtorDecl! t, string attributes) { ProcessDeclaration(t); }
+ public virtual void DeclareConstant(Constant! c, bool uniq, string attributes) { ProcessDeclaration(c); }
+ public virtual void DeclareFunction(Function! f, string attributes) { ProcessDeclaration(f); }
+ public virtual void AddAxiom(Axiom! a, string attributes) { ProcessDeclaration(a); }
+ public abstract void AddAxiom(VCExpr! vc);
+ public virtual void DeclareGlobalVariable(GlobalVariable! v, string attributes) { ProcessDeclaration(v); }
+
+ public abstract VCExpressionGenerator! ExprGen { get; }
+ public abstract Boogie2VCExprTranslator! BoogieExprTranslator { get; }
+ public abstract VCGenerationOptions! VCGenOptions { get; }
+
+ public abstract object! Clone();
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ /// <summary>
+ /// This ProverContext subclass is intended for use with untyped provers that do not require names
+ /// to be declared before use. It constructs its context from unique constants and given axioms.
+ /// </summary>
+ public class DeclFreeProverContext : ProverContext {
+ protected VCExpressionGenerator! gen;
+ protected VCGenerationOptions! genOptions;
+ protected Boogie2VCExprTranslator! translator;
+
+ protected OrderingAxiomBuilder! orderingAxiomBuilder;
+
+ StringBuilder! proverCommands;
+ StringBuilder! incrementalProverCommands;
+
+ protected List<Variable!>! distincts;
+ protected List<VCExpr!>! axiomConjuncts;
+
+ public VCExprTranslator exprTranslator;
+
+ public DeclFreeProverContext(VCExpressionGenerator! gen,
+ VCGenerationOptions! genOptions) {
+ this.gen = gen;
+ this.genOptions = genOptions;
+ Boogie2VCExprTranslator! t = new Boogie2VCExprTranslator (gen, genOptions);
+ this.translator = t;
+ OrderingAxiomBuilder! oab = new OrderingAxiomBuilder(gen, t);
+ oab.Setup();
+ this.orderingAxiomBuilder = oab;
+
+ proverCommands = new StringBuilder();
+ incrementalProverCommands = new StringBuilder();
+
+ distincts = new List<Variable!>();
+ axiomConjuncts = new List<VCExpr!>();
+
+ exprTranslator = null;
+ }
+
+ private DeclFreeProverContext(DeclFreeProverContext! ctxt) {
+ this.gen = ctxt.gen;
+ this.genOptions = ctxt.genOptions;
+ Boogie2VCExprTranslator! t = (Boogie2VCExprTranslator)ctxt.translator.Clone();
+ this.translator = t;
+ this.orderingAxiomBuilder = new OrderingAxiomBuilder(ctxt.gen, t, ctxt.orderingAxiomBuilder);
+
+ StringBuilder! cmds = new StringBuilder ();
+ cmds.Append(ctxt.proverCommands);
+ proverCommands = cmds;
+ StringBuilder! incCmds = new StringBuilder ();
+ incCmds.Append(ctxt.incrementalProverCommands);
+ incrementalProverCommands = incCmds;
+
+ distincts = new List<Variable!>(ctxt.distincts);
+ axiomConjuncts = new List<VCExpr!>(ctxt.axiomConjuncts);
+
+ if (ctxt.exprTranslator == null)
+ exprTranslator = null;
+ else
+ exprTranslator = (VCExprTranslator!)ctxt.exprTranslator.Clone();
+ }
+
+ public override object! Clone() {
+ return new DeclFreeProverContext(this);
+ }
+
+ internal protected void SayToProver(string! msg)
+ {
+ msg = msg + "\r\n";
+ proverCommands.Append(msg);
+ incrementalProverCommands.Append(msg);
+ }
+
+ protected override void ProcessDeclaration(Declaration! decl)
+ {
+ for (QKeyValue a = decl.Attributes; a != null; a = a.Next) {
+ if (a.Key == "prover" && a.Params.Count == 1) {
+ string cmd = a.Params[0] as string;
+ if (cmd != null) {
+ int pos = cmd.IndexOf(':');
+ if (pos <= 0)
+ throw new ProverException("Invalid syntax of :prover string: `" + cmd + "'");
+ string kind = cmd.Substring(0, pos);
+ if (genOptions.IsAnyProverCommandSupported(kind))
+ SayToProver(cmd.Substring(pos + 1));
+ }
+ }
+ }
+ }
+
+ public override void DeclareFunction(Function! f, string attributes) {
+ base.ProcessDeclaration(f);
+ }
+
+ public override void DeclareConstant(Constant! c, bool uniq, string attributes) {
+ base.DeclareConstant(c, uniq, attributes);
+ orderingAxiomBuilder.AddConstant(c);
+
+ // TODO: make separate distinct lists for names coming from different types
+ // e.g., one for strings, one for ints, one for program types.
+ if (uniq){
+ distincts.Add(c);
+ }
+ }
+
+ public override void AddAxiom(Axiom! ax, string attributes) {
+ base.AddAxiom(ax, attributes);
+
+ string ignore = ax.FindStringAttribute("ignore");
+ if (ignore != null && genOptions.IsAnyProverCommandSupported(ignore)) {
+ return;
+ }
+
+ axiomConjuncts.Add(translator.Translate(ax.Expr));
+ }
+
+ public override void AddAxiom(VCExpr! vc)
+ {
+ axiomConjuncts.Add(vc);
+ }
+
+ public VCExpr! Axioms {
+ get {
+ VCExpr axioms = gen.NAry(VCExpressionGenerator.AndOp, axiomConjuncts);
+ List<VCExpr!>! distinctVars = new List<VCExpr!> ();
+ foreach (Variable! v in distincts)
+ distinctVars.Add(translator.LookupVariable(v));
+ axioms = gen.AndSimp(gen.Distinct(distinctVars), axioms);
+ if (CommandLineOptions.Clo.TypeEncodingMethod != CommandLineOptions.TypeEncoding.Monomorphic)
+ axioms = gen.AndSimp(orderingAxiomBuilder.Axioms, axioms);
+ return axioms;
+ }
+ }
+
+ public string! GetProverCommands(bool full) {
+ string! res = (full ? proverCommands : incrementalProverCommands).ToString();
+ incrementalProverCommands.Length = 0;
+ return res;
+ }
+
+ public override VCExpressionGenerator! ExprGen { get {
+ return gen;
+ } }
+ public override Boogie2VCExprTranslator! BoogieExprTranslator { get {
+ return translator;
+ } }
+ public override VCGenerationOptions! VCGenOptions { get {
+ return genOptions;
+ } }
+ }
+
+ // Translator from VCExpressions to strings, which are implemented
+ // by the various provers
+ public abstract class VCExprTranslator : ICloneable {
+ public abstract string! translate(VCExpr! expr, int polarity);
+ public abstract Object! Clone();
+ }
+}
diff --git a/Source/VCGeneration/OrderingAxioms.ssc b/Source/VCGeneration/OrderingAxioms.ssc new file mode 100644 index 00000000..e4fc54f8 --- /dev/null +++ b/Source/VCGeneration/OrderingAxioms.ssc @@ -0,0 +1,285 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Text;
+using Microsoft.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+// Class for constructing and collecting the axioms of the partial
+// order <:. The class also manages "unique" attributes of constants
+// and generated the necessary assumptions for the theorem prover.
+
+// TODO: there should be an interface so that different ways to handle
+// ordering relations can be accessed uniformly
+
+namespace Microsoft.Boogie
+{
+
+ public class OrderingAxiomBuilder {
+
+ private readonly VCExpressionGenerator! Gen;
+ private readonly Boogie2VCExprTranslator! Translator;
+
+ public OrderingAxiomBuilder(VCExpressionGenerator! gen,
+ Boogie2VCExprTranslator! translator) {
+ this.Gen = gen;
+ this.Translator = translator;
+ OneStepFuns = new Dictionary<Type!, Function!> ();
+ Constants = new List<Constant!> ();
+ CompleteConstantsOpen = new List<Constant!> ();
+ AllAxioms = new List<VCExpr!> ();
+ IncAxioms = new List<VCExpr!> ();
+ }
+
+ public OrderingAxiomBuilder(VCExpressionGenerator! gen,
+ Boogie2VCExprTranslator! translator,
+ OrderingAxiomBuilder! builder) {
+ this.Gen = gen;
+ this.Translator = translator;
+ OneStepFuns = new Dictionary<Type!, Function!> (builder.OneStepFuns);
+ Constants = new List<Constant!> (builder.Constants);
+ CompleteConstantsOpen = new List<Constant!> (builder.CompleteConstantsOpen);
+ AllAxioms = new List<VCExpr!> (builder.AllAxioms);
+ IncAxioms = new List<VCExpr!> (builder.IncAxioms);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Used to axiomatise the disjoint-sub-dag specs that are
+ // described by parents with the "unique" flag
+ private readonly IDictionary<Type!, Function!>! OneStepFuns;
+
+ private Function! OneStepFunFor(Type! t) {
+ Function res;
+ if (!OneStepFuns.TryGetValue(t, out res)) {
+ VariableSeq! args = new VariableSeq ();
+ args.Add(new Formal (Token.NoToken,
+ new TypedIdent (Token.NoToken, "arg0", t),
+ true));
+ args.Add(new Formal (Token.NoToken,
+ new TypedIdent (Token.NoToken, "arg1", t),
+ true));
+ Formal! result = new Formal (Token.NoToken,
+ new TypedIdent (Token.NoToken, "res", t),
+ false);
+ res = new Function (Token.NoToken, "oneStep",
+ new TypeVariableSeq (), args, result);
+ OneStepFuns.Add(t, res);
+ }
+ return (!)res;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private readonly List<Constant!>! Constants = new List<Constant!> ();
+
+ // A list to handle constants whose direct children are fully
+ // specified (the "complete" keyword). Constants are removed from
+ // the list as soon as the corresponding axiom has been generated,
+ // which means that from this point on no further children can be
+ // added
+ private readonly List<Constant!>! CompleteConstantsOpen = new List<Constant!> ();
+
+ // list in which all axioms are collected
+ private readonly List<VCExpr!>! AllAxioms = new List<VCExpr!> ();
+
+ // list in which axioms are incrementally collected
+ private readonly List<VCExpr!>! IncAxioms = new List<VCExpr!> ();
+
+ private void AddAxiom(VCExpr! axiom) {
+ if (axiom.Equals(VCExpressionGenerator.True))
+ return;
+ AllAxioms.Add(axiom);
+ IncAxioms.Add(axiom);
+ }
+
+ // Return all axioms that were added since the last time NewAxioms
+ // was called
+ public VCExpr! GetNewAxioms() {
+ CloseChildrenCompleteConstants();
+ VCExpr! res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms);
+ IncAxioms.Clear();
+ return res;
+ }
+
+ // return all axioms
+ public VCExpr! Axioms { get {
+ CloseChildrenCompleteConstants();
+ return Gen.NAry(VCExpressionGenerator.AndOp, AllAxioms);
+ } }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Generate the normal axioms for a partial order relation
+ public void Setup() {
+ TypeVariable! alpha = new TypeVariable(Token.NoToken, "alpha");
+ List<TypeVariable!>! typeParams = new List<TypeVariable!> ();
+ typeParams.Add(alpha);
+
+ List<VCTrigger!>! triggers = new List<VCTrigger!> ();
+
+ VCExprVar! x = Gen.Variable("x", alpha);
+ VCExprVar! y = Gen.Variable("y", alpha);
+ VCExprVar! z = Gen.Variable("z", alpha);
+
+ List<VCExprVar!>! boundVars = new List<VCExprVar!> ();
+
+ // reflexivity
+ boundVars.Add(x);
+ AddAxiom(Gen.Forall(typeParams, boundVars, triggers,
+ new VCQuantifierInfos ("bg:subtype-refl", -1, false, null),
+ Gen.AtMost(x, x)));
+
+ // transitivity
+ boundVars = new List<VCExprVar!> ();
+ boundVars.Add(x); boundVars.Add(y); boundVars.Add(z);
+ triggers = new List<VCTrigger!> ();
+ triggers.Add(Gen.Trigger(true, Gen.AtMost(x, y), Gen.AtMost(y, z)));
+ VCExpr! body = Gen.Implies(Gen.And(Gen.AtMost(x, y), Gen.AtMost(y, z)),
+ Gen.AtMost(x, z));
+ AddAxiom(Gen.Forall(typeParams, boundVars, triggers,
+ new VCQuantifierInfos ("bg:subtype-trans", -1, false, null),
+ body));
+
+ // anti-symmetry
+ boundVars = new List<VCExprVar!> ();
+ boundVars.Add(x); boundVars.Add(y);
+ triggers = new List<VCTrigger!> ();
+ triggers.Add(Gen.Trigger(true, Gen.AtMost(x, y), Gen.AtMost(y, x)));
+ body = Gen.Implies(Gen.And(Gen.AtMost(x, y), Gen.AtMost(y, x)),
+ Gen.Eq(x, y));
+ AddAxiom(Gen.Forall(typeParams, boundVars, triggers,
+ new VCQuantifierInfos ("bg:subtype-antisymm", -1, false, null),
+ body));
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public void AddConstant(Constant! c) {
+ AddAxiom(GenParentConstraints(c));
+ Constants.Add(c);
+ if (c.ChildrenComplete)
+ CompleteConstantsOpen.Add(c);
+
+ // ensure that no further children are added to closed
+ // children-complete constants
+ assert !(c.Parents != null &&
+ exists{ConstantParent! p in c.Parents;
+ ((Constant!)p.Parent.Decl).ChildrenComplete &&
+ !CompleteConstantsOpen.Contains((Constant)p.Parent.Decl)});
+ }
+
+ // Generate the constraints telling that parents of a constant are
+ // strictly greater than the constant itself, and are the minimal
+ // elements with this property
+ private VCExpr! GenParentConstraints(Constant! c) {
+ VCExpr! res = VCExpressionGenerator.True;
+
+ if (c.Parents == null)
+ return res;
+
+ VCExprVar! cAsVar = Translator.LookupVariable(c);
+ VCExprVar! w = Gen.Variable("w", c.TypedIdent.Type);
+
+ // Parents of c are proper ancestors of c
+ foreach (ConstantParent! p in c.Parents) {
+ VCExprVar! par = Translator.LookupVariable((!)p.Parent.Decl);
+ res = Gen.AndSimp(res, Gen.Neq(cAsVar, par));
+ res = Gen.AndSimp(res, Gen.AtMost(cAsVar, par));
+ }
+
+ // Parents are direct ancestors of c (no other elements are in
+ // between c and a parent)
+ foreach (ConstantParent! p in c.Parents) {
+ VCExprVar! par = Translator.LookupVariable((!)p.Parent.Decl);
+ VCExpr! antecedent1 = Gen.AtMost(cAsVar, w);
+ VCExpr! antecedent2 = Gen.AtMost(w, par);
+ VCExpr! body = Gen.Implies(Gen.And(antecedent1, antecedent2),
+ Gen.Or(Gen.Eq(cAsVar, w), Gen.Eq(par, w)));
+ res = Gen.AndSimp(res,
+ Gen.Forall(w,
+ Gen.Trigger(true, antecedent1, antecedent2),
+ body));
+ }
+
+ // Ancestors of c are only c itself and the ancestors of the
+ // parents of c
+ VCExpr! minAncestors = Gen.Eq(cAsVar, w);
+ foreach (ConstantParent! p in c.Parents)
+ minAncestors =
+ Gen.Or(minAncestors,
+ Gen.AtMost(Translator.LookupVariable((!)p.Parent.Decl), w));
+
+ VCExpr! antecedent = Gen.AtMost(cAsVar, w);
+ res = Gen.AndSimp(res,
+ Gen.Forall(w,
+ Gen.Trigger(true, antecedent),
+ Gen.Implies(antecedent, minAncestors)));
+
+ // Constraints for unique child-parent edges
+ foreach (ConstantParent! p in c.Parents) {
+ if (p.Unique)
+ res =
+ Gen.AndSimp(res,
+ GenUniqueParentConstraint(c, (Constant!)p.Parent.Decl));
+ }
+
+ return res;
+ }
+
+ // Generate axioms that state that all direct children of c are
+ // specified; this is the dual of the axiom stating that all direct
+ // ancestors of a constant are known
+ private VCExpr! GenCompleteChildrenConstraints(Constant! c)
+ requires c.ChildrenComplete; {
+
+ VCExprVar! cAsVar = Translator.LookupVariable(c);
+ VCExprVar! w = Gen.Variable("w", c.TypedIdent.Type);
+
+ VCExpr! maxDescendants = Gen.Eq(cAsVar, w);
+ foreach (Constant! d in Constants) {
+ if (d.Parents != null &&
+ exists{ConstantParent! p in d.Parents; c.Equals(p.Parent.Decl)})
+ maxDescendants = Gen.Or(maxDescendants,
+ Gen.AtMost(w, Translator.LookupVariable(d)));
+ }
+
+ VCExpr! antecedent = Gen.AtMost(w, cAsVar);
+ return Gen.Forall(w,
+ Gen.Trigger(true, antecedent),
+ Gen.Implies(antecedent, maxDescendants));
+ }
+
+ private void CloseChildrenCompleteConstants() {
+ foreach (Constant! c in CompleteConstantsOpen)
+ AddAxiom(GenCompleteChildrenConstraints(c));
+ CompleteConstantsOpen.Clear();
+ }
+
+ // Generate the axiom ensuring that the sub-dags underneath unique
+ // child-parent edges are all disjoint
+ private VCExpr! GenUniqueParentConstraint(Constant! child, Constant! parent)
+ requires child.TypedIdent.Type.Equals(parent.TypedIdent.Type); {
+
+ VCExprVar! w = Gen.Variable("w", child.TypedIdent.Type);
+
+ VCExpr! antecedent =
+ Gen.AtMost(w, Translator.LookupVariable(child));
+ VCExpr! succedent =
+ Gen.Eq(Gen.Function(OneStepFunFor(child.TypedIdent.Type),
+ Translator.LookupVariable(parent), w),
+ Translator.LookupVariable(child));
+
+ return Gen.Forall(w,
+ Gen.Trigger(true, antecedent),
+ Gen.Implies(antecedent, succedent));
+ }
+
+ }
+
+}
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc new file mode 100644 index 00000000..617e52e6 --- /dev/null +++ b/Source/VCGeneration/VC.ssc @@ -0,0 +1,3215 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Graphing;
+using AI = Microsoft.AbstractInterpretationFramework;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+
+namespace VC
+{
+ using Bpl = Microsoft.Boogie;
+
+ public class VCGen : ConditionGeneration
+ {
+
+ /// <summary>
+ /// Constructor. Initializes the theorem prover.
+ /// </summary>
+ public VCGen(Program! program, string/*?*/ logFilePath, bool appendLogFile)
+ // throws ProverException
+ {
+ base(program);
+ this.appendLogFile = appendLogFile;
+ this.logFilePath = logFilePath;
+ // base();
+ }
+
+ private static AssumeCmd! AssertTurnedIntoAssume(AssertCmd! assrt)
+ {
+ Expr! expr = assrt.Expr;
+
+ switch (CommandLineOptions.Clo.UseSubsumption) {
+ case CommandLineOptions.SubsumptionOption.Never:
+ expr = Expr.True;
+ break;
+ case CommandLineOptions.SubsumptionOption.Always:
+ break;
+ case CommandLineOptions.SubsumptionOption.NotForQuantifiers:
+ if (expr is QuantifierExpr) {
+ expr = Expr.True;
+ }
+ break;
+ default:
+ assert false; // unexpected case
+ }
+
+ return new AssumeCmd(assrt.tok, expr);
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ /// <param name="impl"></param>
+ private static CmdSeq! GetParamWhereClauses(Implementation! impl)
+ requires impl.Proc != null;
+ {
+ TokenTextWriter debugWriter = null;
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
+ debugWriter = new TokenTextWriter("<console>", Console.Out, false);
+ debugWriter.WriteLine("Effective precondition from where-clauses:");
+ }
+
+ Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+ CmdSeq! whereClauses = new CmdSeq();
+
+ // where clauses of in-parameters
+ foreach (Formal! f in impl.Proc.InParams)
+ {
+ 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
+ assert impl.OutParams.Length == impl.Proc.OutParams.Length;
+ for (int i = 0; i < impl.OutParams.Length; i++) {
+ Variable f = (!)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 = (!)impl.OutParams[i];
+ assume fi.TypedIdent.WhereExpr == null;
+ fi.TypedIdent.WhereExpr = e;
+
+ if (debugWriter != null) { c.Emit(debugWriter, 1); }
+ }
+ }
+
+ if (debugWriter != null) { debugWriter.WriteLine(); }
+
+ return whereClauses;
+ }
+
+ private static void
+ ThreadInBlockExpr(Implementation! impl,
+ Block! targetBlock,
+ BlockExpr! blockExpr,
+ bool replaceWithAssert,
+ TokenTextWriter debugWriter){
+ // Go through blockExpr 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 blockExpr to the implementation (at the end)
+ foreach (Block! b in blockExpr.Blocks){
+ 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);
+ Cmd! c = new AssertEnsuresCmd(ens);
+ b.Cmds.Add(c);
+ }else{
+ b.Cmds.Add(new AssumeCmd(rec.tok, rec.Expr));
+ }
+ b.TransferCmd = new GotoCmd(Token.NoToken,
+ new StringSeq(targetBlock.Label),
+ new BlockSeq(targetBlock));
+ targetBlock.Predecessors.Add(b);
+ }
+ impl.Blocks.Add(b);
+ }
+ if (debugWriter != null){
+ blockExpr.Emit(debugWriter, 1,false);
+ }
+ return;
+ }
+
+ private static void AddAsPrefix(Block! b, CmdSeq! cs){
+ CmdSeq newCommands = new CmdSeq();
+ newCommands.AddRange(cs);
+ newCommands.AddRange(b.Cmds);
+ b.Cmds = newCommands;
+ }
+
+ /// <summary>
+ /// Modifies an implementation by inserting all preconditions
+ /// as assume statements at the beginning of the implementation
+ /// </summary>
+ /// <param name="impl"></param>
+ private static void InjectPreconditions(Implementation! impl)
+ requires impl.Proc != null;
+ {
+ TokenTextWriter debugWriter = null;
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
+ debugWriter = new TokenTextWriter("<console>", Console.Out, false);
+ debugWriter.WriteLine("Effective precondition:");
+ }
+
+ Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+
+ Block! originalEntryPoint = (!) impl.Blocks[0];
+ Block! currentEntryPoint = (!) impl.Blocks[0];
+ CmdSeq! currentClump = new CmdSeq(); // to hold onto contiguous "regular" preconditions
+
+ // (free and checked) requires clauses
+ for (int i = impl.Proc.Requires.Length-1; 0 <= i; i--){
+
+ // need to process the preconditions from bottom up, because
+ // for any that are BlockExprs, we need to thread them on
+ // to the top of the implementation
+
+ Requires req = impl.Proc.Requires[i];
+ Expr! e = Substituter.Apply(formalProcImplSubst, req.Condition);
+ BlockExpr be = req.Condition as BlockExpr;
+ if (be != null){
+ if (currentClump.Length > 0){
+ AddAsPrefix(currentEntryPoint, currentClump);
+ currentClump = new CmdSeq();
+ }
+ ThreadInBlockExpr(impl,currentEntryPoint, be,false,debugWriter);
+ currentEntryPoint = (!)be.Blocks[0];
+ }else{
+ Cmd! c = new AssumeCmd(req.tok, e);
+ currentClump.Add(c);
+ if (debugWriter != null) { c.Emit(debugWriter, 1); }
+ }
+
+ }
+
+ if (currentClump.Length > 0){
+ AddAsPrefix(currentEntryPoint, currentClump);
+ }
+
+ if (currentEntryPoint != originalEntryPoint){
+ string EntryLabel = "PreconditionGeneratedEntry";
+ Block! newEntry = new Block(new Token(-17, -4),EntryLabel,new CmdSeq(),
+ new GotoCmd(Token.NoToken,
+ new StringSeq(currentEntryPoint.Label),
+ new BlockSeq(currentEntryPoint)));
+ currentEntryPoint.Predecessors.Add(newEntry);
+ List<Block!> newBody = new List<Block!>();
+ newBody.Add(newEntry);
+ newBody.AddRange(impl.Blocks);
+ impl.Blocks = newBody;
+ }
+
+ if (debugWriter != null) { debugWriter.WriteLine(); }
+
+ return;
+ }
+ /// <summary>
+ /// Modifies an implementation by inserting all postconditions
+ /// as assert statements at the end of the implementation
+ /// </summary>
+ /// <param name="impl"></param>
+ /// <param name="unifiedExitblock">The unified exit block that has
+ /// already been constructed for the implementation (and so
+ /// is already an element of impl.Blocks)
+ /// </param>
+ private static void InjectPostConditions(Implementation! impl, Block! unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins)
+ requires impl.Proc != null;
+ {
+ TokenTextWriter debugWriter = null;
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
+ debugWriter = new TokenTextWriter("<console>", Console.Out, false);
+ debugWriter.WriteLine("Effective postcondition:");
+ }
+
+ string ExitLabel = "ReallyLastGeneratedExit";
+ Block! newExit = new Block(new Token(-17, -4),ExitLabel,new CmdSeq(),new ReturnCmd(Token.NoToken));
+ impl.Blocks.Add(newExit);
+ Block! currentEntryPoint = newExit;
+ CmdSeq! currentClump = new CmdSeq(); // to hold onto contiguous "regular" postconditions
+
+ Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+
+ // (free and checked) ensures clauses
+ for (int i = impl.Proc.Ensures.Length-1; 0 <= i; i--){
+
+ // need to process the postconditions from bottom up, because
+ // for any that are BlockExprs, we need to thread them on
+ // to the top of the implementation
+
+ Ensures ens = (impl.Proc).Ensures[i];
+ if (!ens.Free) { // free ensures aren't needed for verifying the implementation
+ Expr! e = Substituter.Apply(formalProcImplSubst, ens.Condition);
+ BlockExpr be = ens.Condition as BlockExpr;
+ if (be != null){
+ if (currentClump.Length > 0){
+ AddAsPrefix(currentEntryPoint, currentClump);
+ currentClump = new CmdSeq();
+ }
+ ThreadInBlockExpr(impl,currentEntryPoint,be,true,debugWriter);
+ currentEntryPoint = (!)be.Blocks[0];
+ }else{
+ Ensures! ensCopy = (Ensures!) ens.Clone();
+ ensCopy.Condition = e;
+ Cmd! c = new AssertEnsuresCmd(ensCopy);
+ ((AssertEnsuresCmd) c).ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;
+ currentClump.Add(c);
+ if (debugWriter != null) { c.Emit(debugWriter, 1); }
+ }
+ }
+
+ }
+
+ if (currentClump.Length > 0){
+ AddAsPrefix(currentEntryPoint, currentClump);
+ }
+
+ GotoCmd gtc = new GotoCmd(Token.NoToken,
+ new StringSeq(currentEntryPoint.Label),
+ new BlockSeq(currentEntryPoint));
+ gotoCmdOrigins[gtc] = unifiedExitBlock.TransferCmd;
+ unifiedExitBlock.TransferCmd = gtc;
+ currentEntryPoint.Predecessors.Add(unifiedExitBlock);
+
+ if (debugWriter != null) { debugWriter.WriteLine(); }
+
+ return;
+ }
+
+
+ /// <summary>
+ /// Get the pre-condition of an implementation, including the where clauses from the in-parameters.
+ /// </summary>
+ /// <param name="impl"></param>
+ private static CmdSeq! GetPre(Implementation! impl)
+ requires impl.Proc != null;
+ {
+ TokenTextWriter debugWriter = null;
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
+ debugWriter = new TokenTextWriter("<console>", Console.Out, false);
+ debugWriter.WriteLine("Effective precondition:");
+ }
+
+ Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+ CmdSeq! pre = new CmdSeq();
+
+ // (free and checked) requires clauses
+ foreach (Requires! req in impl.Proc.Requires)
+ {
+ Expr! e = Substituter.Apply(formalProcImplSubst, req.Condition);
+ Cmd! c = new AssumeCmd(req.tok, e);
+ pre.Add(c);
+
+ if (debugWriter != null) { c.Emit(debugWriter, 1); }
+ }
+
+ if (debugWriter != null) { debugWriter.WriteLine(); }
+
+ return pre;
+ }
+
+ /// <summary>
+ /// Get the post-condition of an implementation.
+ /// </summary>
+ /// <param name="impl"></param>
+ private static CmdSeq! GetPost(Implementation! impl)
+ requires impl.Proc != null;
+ {
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { Console.WriteLine("Effective postcondition:"); }
+
+ // Construct an Expr for the post-condition
+ Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+ CmdSeq! post = new CmdSeq();
+ foreach (Ensures! ens in impl.Proc.Ensures)
+ {
+ if (!ens.Free) {
+ Expr! e = Substituter.Apply(formalProcImplSubst, ens.Condition);
+ Ensures! ensCopy = (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>", Console.Out, false), 1); }
+ }
+ }
+
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { Console.WriteLine(); }
+
+ return post;
+ }
+
+
+ #region Soundness smoke tester
+ class SmokeTester
+ {
+ VCGen! parent;
+ Implementation! impl;
+ Block! initial;
+ Program! program;
+ int id;
+ Dictionary<Block!, Block!>! copies = new Dictionary<Block!, Block!>();
+ Dictionary<Block!, bool>! visited = new Dictionary<Block!, bool>();
+ VerifierCallback! callback;
+
+ internal SmokeTester(VCGen! par, Implementation! i, Program! prog, VerifierCallback! callback)
+ {
+ parent = par;
+ impl = i;
+ initial = i.Blocks[0];
+ program = prog;
+ this.callback = callback;
+ }
+
+ internal void Copy()
+ {
+ CloneBlock(impl.Blocks[0]);
+ initial = GetCopiedBlocks()[0];
+ }
+
+ internal void Test()
+ throws UnexpectedProverOutputException;
+ {
+ DFS(initial);
+ }
+
+ void TopologicalSortImpl()
+ {
+ Graph<Block> dag = new Graph<Block>();
+ dag.AddSource((!)impl.Blocks[0]); // there is always at least one node in the graph
+ foreach (Block b in impl.Blocks)
+ {
+ GotoCmd gtc = b.TransferCmd as GotoCmd;
+ if (gtc != null)
+ {
+ assume gtc.labelTargets != null;
+ foreach (Block! dest in gtc.labelTargets)
+ {
+ dag.AddEdge(b,dest);
+ }
+ }
+ }
+ impl.Blocks = new List<Block!>();
+ foreach (Block! b in dag.TopologicalSort()) {
+ impl.Blocks.Add(b);
+ }
+ }
+
+ void Emit()
+ {
+ TopologicalSortImpl();
+ EmitImpl(impl, false);
+ }
+
+ // this one copies forward
+ Block! CloneBlock(Block! b)
+ {
+ Block fake_res;
+ if (copies.TryGetValue(b, out fake_res)) {
+ return (!)fake_res;
+ }
+ Block! res;
+ res = new Block(b.tok, b.Label, new CmdSeq(b.Cmds), null);
+ copies[b] = res;
+ if (b.TransferCmd is GotoCmd) {
+ foreach (Block! ch in (!)((GotoCmd)b.TransferCmd).labelTargets) {
+ CloneBlock(ch);
+ }
+ }
+ foreach (Block! p in b.Predecessors) {
+ res.Predecessors.Add(CloneBlock(p));
+ }
+ return res;
+ }
+
+ // this one copies backwards
+ Block! CopyBlock(Block! b)
+ {
+ Block fake_res;
+ if (copies.TryGetValue(b, out fake_res)) {
+ // fake_res should be Block! but the compiler fails
+ return (!)fake_res;
+ }
+ Block! res;
+ CmdSeq seq = new CmdSeq();
+ foreach (Cmd! c in b.Cmds) {
+ AssertCmd turn = c as AssertCmd;
+ if (!turnAssertIntoAssumes || turn == null) {
+ seq.Add(c);
+ } else {
+ seq.Add(AssertTurnedIntoAssume(turn));
+ }
+ }
+ res = new Block(b.tok, b.Label, seq, null);
+ copies[b] = res;
+ foreach (Block! p in b.Predecessors) {
+ res.Predecessors.Add(CopyBlock(p));
+ }
+ return res;
+ }
+
+ List<Block!>! GetCopiedBlocks()
+ {
+ // the order of nodes in res is random (except for the first one, being the entry)
+ List<Block!> res = new List<Block!>();
+ res.Add(copies[initial]);
+
+ foreach (KeyValuePair<Block!,Block!> kv in copies) {
+ GotoCmd go = kv.Key.TransferCmd as GotoCmd;
+ ReturnCmd ret = kv.Key.TransferCmd as ReturnCmd;
+ if (kv.Key != initial) {
+ res.Add(kv.Value);
+ }
+ if (go != null) {
+ GotoCmd copy = new GotoCmd(go.tok, new StringSeq(), new BlockSeq());
+ kv.Value.TransferCmd = copy;
+ foreach (Block! b in (!)go.labelTargets) {
+ Block c;
+ if (copies.TryGetValue(b, out c)) {
+ copy.AddTarget((!)c);
+ }
+ }
+ } else if (ret != null) {
+ kv.Value.TransferCmd = ret;
+ } else {
+ assume false;
+ }
+ }
+
+ copies.Clear();
+
+ return res;
+ }
+
+ // check if e is true, false, !true, !false
+ // if so return true and the value of the expression in val
+ bool BooleanEval(Expr! e, ref bool val)
+ {
+ LiteralExpr lit = e as LiteralExpr;
+ NAryExpr call = e as NAryExpr;
+
+ if (lit != null && lit.isBool) {
+ val = lit.asBool;
+ return true;
+ } else if (call != null &&
+ call.Fun is UnaryOperator &&
+ ((UnaryOperator)call.Fun).Op == UnaryOperator.Opcode.Not &&
+ BooleanEval((!)call.Args[0], ref val)) {
+ val = !val;
+ return true;
+ }
+ // this is for the 0bv32 != 0bv32 generated by vcc
+ else if (call != null &&
+ call.Fun is BinaryOperator &&
+ ((BinaryOperator)call.Fun).Op == BinaryOperator.Opcode.Neq &&
+ call.Args[0] is LiteralExpr &&
+ ((!)call.Args[0]).Equals(call.Args[1]))
+ {
+ val = false;
+ return true;
+ }
+
+ return false;
+ }
+
+ bool IsFalse(Expr! e)
+ {
+ bool val = false;
+ return BooleanEval(e, ref val) && !val;
+ }
+
+ bool CheckUnreachable(Block! cur, CmdSeq! seq)
+ throws UnexpectedProverOutputException;
+ {
+ DateTime start = DateTime.Now;
+ if (CommandLineOptions.Clo.Trace) {
+ System.Console.Write(" soundness smoke test #{0} ... ", id);
+ }
+ callback.OnProgress("smoke", id, id, 0.0);
+
+ Token tok = new Token();
+ tok.val = "soundness smoke test assertion";
+ seq.Add(new AssertCmd(tok, Expr.False));
+ Block! copy = CopyBlock(cur);
+ copy.Cmds = seq;
+ List<Block!>! backup = impl.Blocks;
+ impl.Blocks = GetCopiedBlocks();
+ copy.TransferCmd = new ReturnCmd(Token.NoToken);
+ if (CommandLineOptions.Clo.TraceVerify) {
+ System.Console.WriteLine();
+ System.Console.WriteLine(" --- smoke #{0}, before passify", id);
+ Emit();
+ }
+ parent.current_impl = impl;
+ parent.PassifyImpl(impl, program);
+ Hashtable! label2Absy;
+ Checker! ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);
+ VCExpr! vc = parent.GenerateVC(impl, out label2Absy, ch);
+ impl.Blocks = backup;
+
+ if (CommandLineOptions.Clo.TraceVerify) {
+ System.Console.WriteLine(" --- smoke #{0}, after passify", id);
+ Emit();
+ }
+ ch.BeginCheck((!) impl.Name + "_smoke" + id++, vc, new ErrorHandler(label2Absy));
+ ch.ProverDone.WaitOne();
+ ProverInterface.Outcome outcome = ch.ReadOutcome();
+ parent.current_impl = null;
+
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ if (CommandLineOptions.Clo.Trace) {
+ System.Console.WriteLine(" [{0} s] {1}", elapsed.TotalSeconds,
+ outcome == ProverInterface.Outcome.Valid ? "OOPS" :
+ "OK" + (outcome == ProverInterface.Outcome.Invalid ? "" : " (" + outcome + ")"));
+ }
+
+ if (outcome == ProverInterface.Outcome.Valid) {
+ // copy it again, so we get the version with calls, assignments and such
+ copy = CopyBlock(cur);
+ copy.Cmds = seq;
+ impl.Blocks = GetCopiedBlocks();
+ TopologicalSortImpl();
+ callback.OnUnreachableCode(impl);
+ impl.Blocks = backup;
+ return true;
+ }
+ return false;
+ }
+
+ const bool turnAssertIntoAssumes = false;
+
+ void DFS(Block! cur)
+ throws UnexpectedProverOutputException;
+ {
+ if (visited.ContainsKey(cur)) return;
+ visited[cur] = true;
+
+ CmdSeq! seq = new CmdSeq();
+ foreach (Cmd! cmd_ in cur.Cmds) {
+ Cmd! cmd = cmd_;
+ AssertCmd assrt = cmd as AssertCmd;
+ AssumeCmd assm = cmd as AssumeCmd;
+ CallCmd call = cmd as CallCmd;
+
+ bool assumeFalse = false;
+
+ if (assrt != null) {
+ // we're not going any further
+ // it's clear the user expected unreachable code here
+ // it's not clear where did he expect it, maybe it would be right to insert
+ // a check just one command before
+ if (IsFalse(assrt.Expr)) return;
+
+ if (turnAssertIntoAssumes) {
+ cmd = AssertTurnedIntoAssume(assrt);
+ }
+ } else if (assm != null) {
+ if (IsFalse(assm.Expr)) assumeFalse = true;
+ } else if (call != null) {
+ foreach (Ensures! e in ((!)call.Proc).Ensures) {
+ if (IsFalse(e.Condition)) assumeFalse = true;
+ }
+ }
+
+ if (assumeFalse) {
+ CheckUnreachable(cur, seq);
+ return;
+ }
+
+ seq.Add(cmd);
+ }
+
+
+ GotoCmd go = cur.TransferCmd as GotoCmd;
+ ReturnCmd ret = cur.TransferCmd as ReturnCmd;
+
+ assume !(go!= null&&go.labelTargets==null&&go.labelNames!=null&&go.labelNames.Length>0) ;
+
+ if (ret != null || (go != null && ((!)go.labelTargets).Length == 0)) {
+ // we end in return, so there will be no more places to check
+ CheckUnreachable(cur, seq);
+ } else if (go != null) {
+ bool needToCheck = true;
+ // if all of our children have more than one parent, then
+ // we're in the right place to check
+ foreach (Block! target in (!)go.labelTargets) {
+ if (target.Predecessors.Length == 1) {
+ needToCheck = false;
+ }
+ }
+ if (needToCheck) {
+ CheckUnreachable(cur, seq);
+ }
+ foreach (Block! target in go.labelTargets) {
+ DFS(target);
+ }
+ }
+ }
+
+ class ErrorHandler : ProverInterface.ErrorHandler {
+ Hashtable! label2Absy;
+
+ public ErrorHandler(Hashtable! label2Absy) {
+ this.label2Absy = label2Absy;
+ }
+
+ public override Absy! Label2Absy(string! label) {
+ int id = int.Parse(label);
+ return (Absy!) label2Absy[id];
+ }
+ }
+ }
+
+
+ #endregion
+
+ #region Splitter
+ class Split
+ {
+ class BlockStats {
+ public bool big_block;
+ public int id;
+ public double assertion_cost;
+ public double assumption_cost; // before multiplier
+ public double incomming_paths;
+ public List<Block!>! virtual_successors = new List<Block!>();
+ public List<Block!>! virtual_predecesors = new List<Block!>();
+ public Dictionary<Block!,bool>? reachable_blocks;
+ public readonly Block! block;
+
+ public BlockStats(Block! b, int i)
+ {
+ block = b;
+ assertion_cost = -1;
+ id = i;
+ }
+ }
+
+ readonly List<Block!>! blocks;
+ readonly List<Block!>! big_blocks = new List<Block!>();
+ readonly Dictionary<Block!, BlockStats!>! stats = new Dictionary<Block!, BlockStats!>();
+ readonly int id;
+ static int current_id;
+ Block? split_block;
+ bool assert_to_assume;
+ List<Block!>! assumized_branches = new List<Block!>();
+ public AssertCmd? first_assert;
+
+ double score;
+ bool score_computed;
+ double total_cost;
+ int assertion_count;
+ double assertion_cost; // without multiplication by paths
+ Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins;
+ VCGen! parent;
+ Implementation! impl;
+
+ Dictionary<Block!, Block!>! copies = new Dictionary<Block!, Block!>();
+ bool doing_slice;
+ double slice_initial_limit;
+ double slice_limit;
+ bool slice_pos;
+ Dictionary<Block!, bool>! protected_from_assert_to_assume = new Dictionary<Block!,bool>();
+ Dictionary<Block!, bool>! keep_at_all = new Dictionary<Block!,bool>();
+
+ // async interface
+ private Checker checker;
+ private int splitNo;
+ internal ErrorReporter reporter;
+
+ public Split(List<Block!>! blocks, Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins, VCGen! par, Implementation! impl)
+ {
+ this.blocks = blocks;
+ this.gotoCmdOrigins = gotoCmdOrigins;
+ this.parent = par;
+ this.impl = impl;
+ this.id = current_id++;
+ }
+
+ public double Cost
+ {
+ get {
+ ComputeBestSplit();
+ return total_cost;
+ }
+ }
+
+ public bool LastChance
+ {
+ get {
+ ComputeBestSplit();
+ return assertion_count == 1 && score < 0;
+ }
+ }
+
+ public string Stats
+ {
+ get {
+ ComputeBestSplit();
+ return string.Format("(cost:{0:0}/{1:0}{2})", total_cost, assertion_cost, LastChance ? " last" : "");
+ }
+ }
+
+ public void DumpDot(int no)
+ {
+ using (System.IO.StreamWriter sw = System.IO.File.CreateText(string.Format("split.{0}.dot", no))) {
+ sw.WriteLine("digraph G {");
+
+ ComputeBestSplit();
+ List<Block!> saved = assumized_branches;
+ assumized_branches = new List<Block!>();
+ DoComputeScore(false);
+ assumized_branches = saved;
+
+ foreach (Block! b in big_blocks) {
+ BlockStats s = GetBlockStats(b);
+ foreach (Block! t in s.virtual_successors) {
+ sw.WriteLine("n{0} -> n{1};", s.id, GetBlockStats(t).id);
+ }
+ sw.WriteLine("n{0} [label=\"{1}:\\n({2:0.0}+{3:0.0})*{4:0.0}\"{5}];",
+ s.id, b.Label,
+ s.assertion_cost, s.assumption_cost, s.incomming_paths,
+ s.assertion_cost > 0 ? ",shape=box" : "");
+
+ }
+ sw.WriteLine("}");
+ sw.Close();
+ }
+
+ string filename = string.Format("split.{0}.bpl", no);
+ using (System.IO.StreamWriter sw = System.IO.File.CreateText(filename)) {
+ int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ CommandLineOptions.Clo.PrintUnstructured = 2; // print only the unstructured program
+ bool oldPrintDesugaringSetting = CommandLineOptions.Clo.PrintDesugarings;
+ CommandLineOptions.Clo.PrintDesugarings = false;
+ List<Block!> backup = impl.Blocks;
+ impl.Blocks = blocks;
+ impl.Emit(new TokenTextWriter(filename, sw, false), 0);
+ impl.Blocks = backup;
+ CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;
+ CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
+ }
+
+ int bsid;
+ BlockStats! GetBlockStats(Block! b)
+ {
+ BlockStats s;
+ if (!stats.TryGetValue(b, out s)) {
+ s = new BlockStats(b, bsid++);
+ stats[b] = s;
+ }
+ return (!)s;
+ }
+
+ double AssertionCost(PredicateCmd c)
+ {
+ return 1.0;
+ }
+
+ void CountAssertions(Block! b)
+ {
+ BlockStats s = GetBlockStats(b);
+ if (s.assertion_cost >= 0) return; // already done
+ s.big_block = true;
+ s.assertion_cost = 0;
+ s.assumption_cost = 0;
+ foreach (Cmd c in b.Cmds) {
+ if (c is AssertCmd) {
+ double cost = AssertionCost((AssertCmd)c);
+ s.assertion_cost += cost;
+ assertion_count++;
+ assertion_cost += cost;
+ } else if (c is AssumeCmd) {
+ s.assumption_cost += AssertionCost((AssumeCmd)c);
+ }
+ }
+ foreach (Block! b in Exits(b)) {
+ s.virtual_successors.Add(b);
+ }
+ if (s.virtual_successors.Count == 1) {
+ Block next = s.virtual_successors[0];
+ BlockStats se = GetBlockStats(next);
+ CountAssertions(next);
+ if (next.Predecessors.Length > 1 || se.virtual_successors.Count != 1) return;
+ s.virtual_successors[0] = se.virtual_successors[0];
+ s.assertion_cost += se.assertion_cost;
+ s.assumption_cost += se.assumption_cost;
+ se.big_block = false;
+ }
+ }
+
+ Dictionary<Block!,bool>! ComputeReachableNodes(Block! b)
+ {
+ BlockStats s = GetBlockStats(b);
+ if (s.reachable_blocks != null) {
+ return s.reachable_blocks;
+ }
+ Dictionary<Block!, bool> blocks = new Dictionary<Block!, bool>();
+ s.reachable_blocks = blocks;
+ blocks[b] = true;
+ foreach (Block! succ in Exits(b)) {
+ foreach (Block! r in ComputeReachableNodes(succ).Keys) {
+ blocks[r] = true;
+ }
+ }
+ return blocks;
+ }
+
+ double ProverCost(double vc_cost)
+ {
+ return vc_cost * vc_cost;
+ }
+
+ void ComputeBestSplit()
+ {
+ if (score_computed) return;
+ score_computed = true;
+
+ assertion_count = 0;
+
+ foreach (Block! b in blocks) {
+ CountAssertions(b);
+ }
+
+ foreach (Block! b in blocks) {
+ BlockStats bs = GetBlockStats(b);
+ if (bs.big_block) {
+ big_blocks.Add(b);
+ foreach (Block! ch in bs.virtual_successors) {
+ BlockStats chs = GetBlockStats(ch);
+ if (!chs.big_block) {
+ Console.WriteLine("non-big {0} accessed from {1}", ch, b);
+ DumpDot(-1);
+ assert false;
+ }
+ chs.virtual_predecesors.Add(b);
+ }
+ }
+ }
+
+ assumized_branches.Clear();
+ total_cost = ProverCost(DoComputeScore(false));
+
+ score = double.PositiveInfinity;
+ Block? best_split = null;
+ List<Block!>! saved_branches = new List<Block!>();
+
+ foreach (Block! b in big_blocks) {
+ GotoCmd gt = b.TransferCmd as GotoCmd;
+ if (gt == null) continue;
+ BlockSeq targ = (!)gt.labelTargets;
+ if (targ.Length < 2) continue;
+ // caution, we only consider two first exits
+
+ double left0, right0, left1, right1;
+ split_block = b;
+
+ assumized_branches.Clear();
+ assumized_branches.Add((!)targ[0]);
+ left0 = DoComputeScore(true);
+ right0 = DoComputeScore(false);
+
+ assumized_branches.Clear();
+ for (int idx = 1; idx < targ.Length; idx++) {
+ assumized_branches.Add((!)targ[idx]);
+ }
+ left1 = DoComputeScore(true);
+ right1 = DoComputeScore(false);
+
+ double current_score = ProverCost(left1) + ProverCost(right1);
+ double other_score = ProverCost(left0) + ProverCost(right0);
+
+ if (other_score < current_score) {
+ current_score = other_score;
+ assumized_branches.Clear();
+ assumized_branches.Add((!)targ[0]);
+ }
+
+ if (current_score < score) {
+ score = current_score;
+ best_split = split_block;
+ saved_branches.Clear();
+ saved_branches.AddRange(assumized_branches);
+ }
+ }
+
+ if (CommandLineOptions.Clo.VcsPathSplitMult * score > total_cost) {
+ split_block = null;
+ score = -1;
+ } else {
+ assumized_branches = saved_branches;
+ split_block = best_split;
+ }
+ }
+
+ void UpdateIncommingPaths(BlockStats! s)
+ {
+ if (s.incomming_paths < 0.0) {
+ int count = 0;
+ s.incomming_paths = 0.0;
+ if (!keep_at_all.ContainsKey(s.block)) return;
+ foreach (Block! b in s.virtual_predecesors) {
+ BlockStats! ch = GetBlockStats(b);
+ UpdateIncommingPaths(ch);
+ if (ch.incomming_paths > 0.0) {
+ s.incomming_paths += ch.incomming_paths;
+ count++;
+ }
+ }
+ if (count > 1) {
+ s.incomming_paths *= CommandLineOptions.Clo.VcsPathJoinMult;
+ }
+ }
+ }
+
+ void ComputeBlockSetsHelper(Block! b, bool allow_small)
+ {
+ if (keep_at_all.ContainsKey(b)) return;
+ keep_at_all[b] = true;
+
+ if (allow_small) {
+ foreach (Block! ch in Exits(b)) {
+ if (b == split_block && assumized_branches.Contains(ch)) continue;
+ ComputeBlockSetsHelper(ch, allow_small);
+ }
+ } else {
+ foreach (Block! ch in GetBlockStats(b).virtual_successors) {
+ if (b == split_block && assumized_branches.Contains(ch)) continue;
+ ComputeBlockSetsHelper(ch, allow_small);
+ }
+ }
+ }
+
+ void ComputeBlockSets(bool allow_small)
+ {
+ protected_from_assert_to_assume.Clear();
+ keep_at_all.Clear();
+
+ Debug.Assert(split_block == null || GetBlockStats(split_block).big_block);
+ Debug.Assert(GetBlockStats(blocks[0]).big_block);
+
+ if (assert_to_assume) {
+ foreach (Block! b in allow_small ? blocks : big_blocks) {
+ if (ComputeReachableNodes(b).ContainsKey((!)split_block)) {
+ keep_at_all[b] = true;
+ }
+ }
+
+ foreach (Block! b in assumized_branches) {
+ foreach (Block! r in ComputeReachableNodes(b).Keys) {
+ if (allow_small || GetBlockStats(r).big_block) {
+ keep_at_all[r] = true;
+ protected_from_assert_to_assume[r] = true;
+ }
+ }
+ }
+ } else {
+ ComputeBlockSetsHelper(blocks[0], allow_small);
+ }
+ }
+
+ bool ShouldAssumize(Block! b)
+ {
+ return assert_to_assume && !protected_from_assert_to_assume.ContainsKey(b);
+ }
+
+ double DoComputeScore(bool aa)
+ {
+ assert_to_assume = aa;
+ ComputeBlockSets(false);
+
+ foreach (Block! b in big_blocks) {
+ GetBlockStats(b).incomming_paths = -1.0;
+ }
+
+ GetBlockStats(blocks[0]).incomming_paths = 1.0;
+
+ double cost = 0.0;
+ foreach (Block! b in big_blocks) {
+ if (keep_at_all.ContainsKey(b)) {
+ BlockStats s = GetBlockStats(b);
+ UpdateIncommingPaths(s);
+ double local = s.assertion_cost;
+ if (ShouldAssumize(b)) {
+ local = (s.assertion_cost + s.assumption_cost) * CommandLineOptions.Clo.VcsAssumeMult;
+ } else {
+ local = s.assumption_cost * CommandLineOptions.Clo.VcsAssumeMult + s.assertion_cost;
+ }
+ local = local + local * s.incomming_paths * CommandLineOptions.Clo.VcsPathCostMult;
+ cost += local;
+ }
+ }
+
+ return cost;
+ }
+
+ CmdSeq! SliceCmds(Block! b)
+ {
+ CmdSeq! seq = b.Cmds;
+ if (!doing_slice && !ShouldAssumize(b)) return seq;
+ CmdSeq! res = new CmdSeq();
+ foreach (Cmd! c in seq) {
+ AssertCmd a = c as AssertCmd;
+ Cmd! the_new = c;
+ bool swap = false;
+ if (a != null) {
+ if (doing_slice) {
+ double cost = AssertionCost(a);
+ bool first = (slice_limit - cost) >= 0 || slice_initial_limit == slice_limit;
+ slice_limit -= cost;
+ swap = slice_pos == first;
+ } else if (assert_to_assume) {
+ swap = true;
+ } else {
+ assert false;
+ }
+
+ if (swap) {
+ the_new = AssertTurnedIntoAssume(a);
+ }
+ }
+ res.Add(the_new);
+ }
+ return res;
+ }
+
+ Block! CloneBlock(Block! b)
+ {
+ Block res;
+ if (copies.TryGetValue(b, out res)) {
+ return (!)res;
+ }
+ res = new Block(b.tok, b.Label, SliceCmds(b), b.TransferCmd);
+ GotoCmd gt = b.TransferCmd as GotoCmd;
+ copies[b] = res;
+ if (gt != null) {
+ GotoCmd newGoto = new GotoCmd(gt.tok, new StringSeq(), new BlockSeq());
+ res.TransferCmd = newGoto;
+ int pos = 0;
+ foreach (Block! ch in (!)gt.labelTargets) {
+ assert doing_slice ||
+ (!assert_to_assume ==> (keep_at_all.ContainsKey(ch) || assumized_branches.Contains(ch)));
+ if (doing_slice ||
+ ((b != split_block || assumized_branches.Contains(ch) == assert_to_assume) &&
+ keep_at_all.ContainsKey(ch))) {
+ newGoto.AddTarget(CloneBlock(ch));
+ }
+ pos++;
+ }
+ }
+ return res;
+ }
+
+ Split! DoSplit()
+ {
+ copies.Clear();
+ CloneBlock(blocks[0]);
+ List<Block!> newBlocks = new List<Block!>();
+ Hashtable newGotoCmdOrigins = new Hashtable();
+ foreach (Block! b in blocks) {
+ Block tmp;
+ if (copies.TryGetValue(b, out tmp)) {
+ newBlocks.Add((!)tmp);
+ if (gotoCmdOrigins.ContainsKey(b)) {
+ newGotoCmdOrigins[tmp] = gotoCmdOrigins[b];
+ }
+
+ foreach (Block! p in b.Predecessors) {
+ Block tmp2;
+ if (copies.TryGetValue(p, out tmp2)) {
+ tmp.Predecessors.Add(tmp2);
+ }
+ }
+ }
+ }
+
+ return new Split(newBlocks, newGotoCmdOrigins, parent, impl);
+ }
+
+ Split! SplitAt(int idx)
+ {
+ assert_to_assume = idx == 0;
+ doing_slice = false;
+ ComputeBlockSets(true);
+
+ return DoSplit();
+ }
+
+ Split! SliceAsserts(double limit, bool pos)
+ {
+ slice_pos = pos;
+ slice_limit = limit;
+ slice_initial_limit = limit;
+ doing_slice = true;
+ Split! r = DoSplit();
+
+ /*
+ Console.WriteLine("split {0} / {1} -->", limit, pos);
+ List<Block!> tmp = impl.Blocks;
+ impl.Blocks = r.blocks;
+ EmitImpl(impl, false);
+ impl.Blocks = tmp;
+ */
+
+ return r;
+ }
+
+ void Print()
+ {
+ List<Block!> tmp = impl.Blocks;
+ impl.Blocks = blocks;
+ EmitImpl(impl, false);
+ impl.Blocks = tmp;
+ }
+
+ public Counterexample! ToCounterexample()
+ {
+ BlockSeq trace = new BlockSeq();
+ foreach (Block! b in blocks) {
+ trace.Add(b);
+ }
+ foreach (Block! b in blocks) {
+ foreach (Cmd! c in b.Cmds) {
+ if (c is AssertCmd) {
+ return AssertCmdToCounterexample((AssertCmd)c, (!)b.TransferCmd, trace, null, new Dictionary<Incarnation, Absy!>());
+ }
+ }
+ }
+ assume false;
+ }
+
+ public static List<Split!>! DoSplit(Split! initial, double max_cost, int max)
+ {
+ List<Split!> res = new List<Split!>();
+ res.Add(initial);
+
+ while (res.Count < max) {
+ Split best = null;
+ int best_idx = 0, pos = 0;
+ foreach (Split! s in res) {
+ s.ComputeBestSplit(); // TODO check total_cost first
+ if (s.total_cost > max_cost &&
+ (best == null || best.total_cost < s.total_cost) &&
+ (s.assertion_count > 1 || s.split_block != null)) {
+ best = s;
+ best_idx = pos;
+ }
+ pos++;
+ }
+
+ if (best == null) break; // no split found
+
+ Split! s0, s1;
+
+ bool split_stats = CommandLineOptions.Clo.TraceVerify;
+
+ if (split_stats) {
+ Console.WriteLine("{0} {1} -->", best.split_block == null ? "SLICE" : ("SPLIT@" + best.split_block.Label), best.Stats);
+ if (best.split_block != null) {
+ GotoCmd g = best.split_block.TransferCmd as GotoCmd;
+ if (g != null) {
+ Console.Write(" exits: ");
+ foreach (Block! b in (!)g.labelTargets) {
+ Console.Write("{0} ", b.Label);
+ }
+ Console.WriteLine("");
+ Console.Write(" assumized: ");
+ foreach (Block! b in best.assumized_branches) {
+ Console.Write("{0} ", b.Label);
+ }
+ Console.WriteLine("");
+ }
+ }
+ }
+
+ if (best.split_block != null) {
+ s0 = best.SplitAt(0);
+ s1 = best.SplitAt(1);
+ } else {
+ best.split_block = null;
+ s0 = best.SliceAsserts(best.assertion_cost / 2, true);
+ s1 = best.SliceAsserts(best.assertion_cost / 2, false);
+ }
+
+ if (true) {
+ List<Block!> ss = new List<Block!>();
+ ss.Add(s0.blocks[0]);
+ ss.Add(s1.blocks[0]);
+ try {
+ best.SoundnessCheck(new Dictionary<PureCollections.Tuple!, bool>(), best.blocks[0], ss);
+ } catch (System.Exception e) {
+ Console.WriteLine(e);
+ best.DumpDot(-1);
+ s0.DumpDot(-2);
+ s1.DumpDot(-3);
+ assert false;
+ }
+ }
+
+ if (split_stats) {
+ s0.ComputeBestSplit();
+ s1.ComputeBestSplit();
+ Console.WriteLine(" --> {0}", s0.Stats);
+ Console.WriteLine(" --> {0}", s1.Stats);
+ }
+
+ if (CommandLineOptions.Clo.TraceVerify) {
+ best.Print();
+ }
+
+ res[best_idx] = s0;
+ res.Add(s1);
+ }
+
+ return res;
+ }
+
+ public Checker! Checker
+ {
+ get {
+ assert checker != null;
+ return checker;
+ }
+ }
+
+ public WaitHandle ProverDone
+ {
+ get {
+ assert checker != null;
+ return checker.ProverDone;
+ }
+ }
+
+ public void ReadOutcome(ref Outcome cur_outcome, out bool prover_failed)
+ throws UnexpectedProverOutputException;
+ {
+ ProverInterface.Outcome outcome = ((!)checker).ReadOutcome();
+
+ if (CommandLineOptions.Clo.Trace && splitNo >= 0) {
+ System.Console.WriteLine(" --> split #{0} done, [{1} s] {2}", splitNo, checker.ProverRunTime.TotalSeconds, outcome);
+ }
+
+ if (CommandLineOptions.Clo.VcsDumpSplits) {
+ DumpDot(splitNo);
+ }
+
+ prover_failed = false;
+
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid:
+ return;
+ case ProverInterface.Outcome.Invalid:
+ cur_outcome = Outcome.Errors;
+ return;
+ case ProverInterface.Outcome.OutOfMemory:
+ prover_failed = true;
+ if (cur_outcome != Outcome.Errors && cur_outcome != Outcome.Inconclusive)
+ cur_outcome = Outcome.OutOfMemory;
+ return;
+ case ProverInterface.Outcome.TimeOut:
+ prover_failed = true;
+ if (cur_outcome != Outcome.Errors && cur_outcome != Outcome.Inconclusive)
+ cur_outcome = Outcome.TimedOut;
+ return;
+ case ProverInterface.Outcome.Undetermined:
+ prover_failed = true;
+ if (cur_outcome != Outcome.Errors)
+ cur_outcome = Outcome.Inconclusive;
+ return;
+ default:
+ assert false;
+ }
+ }
+
+ public void BeginCheck(VerifierCallback! callback, int no, int timeout)
+ {
+ splitNo = no;
+
+ impl.Blocks = blocks;
+
+ checker = parent.FindCheckerFor(impl, timeout);
+
+ Hashtable/*<int, Absy!>*/! label2absy;
+ VCExpr! vc = parent.GenerateVC(impl, out label2absy, checker);
+
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
+ reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback);
+ } else {
+ reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback);
+ }
+
+ if (CommandLineOptions.Clo.TraceVerify && no >= 0)
+ {
+ Console.WriteLine("-- after split #{0}", no);
+ Print();
+ }
+
+ string! desc = (!) impl.Name;
+ if (no >= 0)
+ desc += "_split" + no;
+ checker.BeginCheck(desc, vc, reporter);
+
+ }
+
+ private void SoundnessCheck(Dictionary<PureCollections.Tuple!, bool>! cache, Block! orig, List<Block!>! copies)
+ {
+ {
+ PureCollections.Tuple t = new PureCollections.Tuple(new PureCollections.Capacity(1 + copies.Count));
+ int i = 0;
+ t[i++] = orig;
+ foreach (Block! b in copies) {
+ t[i++] = b;
+ }
+ if (cache.ContainsKey(t)) { return; }
+ cache[t] = true;
+ }
+
+ for (int i = 0; i < orig.Cmds.Length; ++i) {
+ Cmd cmd = orig.Cmds[i];
+ if (cmd is AssertCmd) {
+ int found = 0;
+ foreach (Block! c in copies) {
+ if (c.Cmds[i] == cmd) {
+ found++;
+ }
+ }
+ if (found == 0) {
+ throw new System.Exception(string.Format("missing assertion: {0}({1})", cmd.tok.filename, cmd.tok.line));
+ }
+ }
+ }
+
+ foreach (Block! exit in Exits(orig)) {
+ List<Block!>! newcopies = new List<Block!>();
+ foreach (Block! c in copies) {
+ foreach (Block! cexit in Exits(c)) {
+ if (cexit.Label == exit.Label) {
+ newcopies.Add(cexit);
+ }
+ }
+ }
+ if (newcopies.Count == 0) {
+ throw new System.Exception("missing exit " + exit.Label);
+ }
+ SoundnessCheck(cache, exit, newcopies);
+ }
+ }
+ }
+ #endregion
+
+
+ protected VCExpr! GenerateVC(Implementation! impl, out Hashtable/*<int, Absy!>*/! label2absy, Checker! ch)
+ {
+ TypecheckingContext tc = new TypecheckingContext(null);
+ impl.Typecheck(tc);
+
+ label2absy = new Hashtable/*<int, Absy!>*/();
+ VCExpr! vc;
+ switch (CommandLineOptions.Clo.vcVariety) {
+ case CommandLineOptions.VCVariety.Structured:
+ vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context);
+ break;
+ case CommandLineOptions.VCVariety.Block:
+ vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context);
+ break;
+ case CommandLineOptions.VCVariety.BlockReach:
+ vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context);
+ break;
+ case CommandLineOptions.VCVariety.Local:
+ vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context);
+ break;
+ case CommandLineOptions.VCVariety.BlockNested:
+ vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context);
+ break;
+ case CommandLineOptions.VCVariety.BlockNestedReach:
+ vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context);
+ break;
+ case CommandLineOptions.VCVariety.Dag:
+ if (((!)CommandLineOptions.Clo.TheProverFactory).SupportsDags) {
+ vc = DagVC((!)impl.Blocks[0], label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context);
+ } else {
+ vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);
+ }
+ break;
+ case CommandLineOptions.VCVariety.Doomed:
+ vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context);
+ break;
+ default:
+ assert false; // unexpected enumeration value
+ }
+ return vc;
+ }
+
+ void CheckIntAttributeOnImpl(Implementation! impl, string! name, ref int val)
+ {
+ if (!((!)impl.Proc).CheckIntAttribute(name, ref val) || !impl.CheckIntAttribute(name, ref val)) {
+ Console.WriteLine("ignoring ill-formed {:{0} ...} attribute on {1}, parameter should be an int", name, impl.Name);
+ }
+ }
+
+
+ public override Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)
+ throws UnexpectedProverOutputException;
+ {
+ if (impl.SkipVerification) {
+ return Outcome.Inconclusive; // not sure about this one
+ }
+
+ callback.OnProgress("VCgen", 0, 0, 0.0);
+
+ ConvertCFG2DAG(impl, program);
+
+ SmokeTester smoke_tester = null;
+ if (CommandLineOptions.Clo.SoundnessSmokeTest) {
+ smoke_tester = new SmokeTester(this, impl, program, callback);
+ smoke_tester.Copy();
+ }
+
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program);
+
+ double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;
+ int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits,
+ max_kg_splits = CommandLineOptions.Clo.VcsMaxKeepGoingSplits;
+ CheckIntAttributeOnImpl(impl, "vcs_max_cost", ref tmp_max_vc_cost);
+ CheckIntAttributeOnImpl(impl, "vcs_max_splits", ref max_splits);
+ CheckIntAttributeOnImpl(impl, "vcs_max_keep_going_splits", ref max_kg_splits);
+ if (tmp_max_vc_cost >= 0) {
+ max_vc_cost = tmp_max_vc_cost;
+ }
+
+ Outcome outcome = Outcome.Correct;
+
+ int cores = CommandLineOptions.Clo.VcsCores;
+ Stack<Split!> work = new Stack<Split!>();
+ List<Split!> currently_running = new List<Split!>();
+ ResetPredecessors(impl.Blocks);
+ work.Push(new Split(impl.Blocks, gotoCmdOrigins, this, impl));
+
+ bool keep_going = max_kg_splits > 1;
+ int total = 0;
+ int no = max_splits == 1 && !keep_going ? -1 : 0;
+ bool first_round = true;
+ bool do_splitting = keep_going || max_splits > 1;
+ double remaining_cost = 0.0, proven_cost = 0.0;
+
+ if (do_splitting) {
+ remaining_cost = work.Peek().Cost;
+ }
+
+ while (work.Count > 0 || currently_running.Count > 0) {
+ bool prover_failed = false;
+ Split! s;
+
+ if (work.Count > 0 && currently_running.Count < cores) {
+ s = work.Pop();
+
+ if (first_round && max_splits > 1) {
+ prover_failed = true;
+ remaining_cost -= s.Cost;
+ } else {
+ if (CommandLineOptions.Clo.Trace && no >= 0) {
+ System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
+ s.Stats, no + 1, total, 100 * proven_cost / (proven_cost + remaining_cost));
+ }
+ callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
+
+ s.BeginCheck(callback, no,
+ (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
+ keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
+ CommandLineOptions.Clo.ProverKillTime);
+
+ no++;
+
+ currently_running.Add(s);
+ }
+ } else {
+ WaitHandle[] handles = new WaitHandle[currently_running.Count];
+ for (int i = 0; i < currently_running.Count; ++i) {
+ handles[i] = currently_running[i].ProverDone;
+ }
+ int index = WaitHandle.WaitAny(handles);
+ s = currently_running[index];
+ currently_running.RemoveAt(index);
+
+ if (do_splitting) {
+ remaining_cost -= s.Cost;
+ }
+
+ s.ReadOutcome(ref outcome, out prover_failed);
+
+ if (do_splitting) {
+ if (prover_failed) {
+ // even if the prover fails, we have learned something, i.e., it is
+ // annoying to watch Boogie say Timeout, 0.00% a couple of times
+ proven_cost += s.Cost / 100;
+ } else {
+ proven_cost += s.Cost;
+ }
+ }
+ callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
+
+ if (prover_failed && !first_round && s.LastChance) {
+ string! msg = "some timeout";
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ msg = s.reporter.resourceExceededMessage;
+ }
+ callback.OnCounterexample(s.ToCounterexample(), msg);
+ outcome = Outcome.Errors;
+ break;
+ }
+
+ assert prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors;
+ }
+
+ if (prover_failed) {
+ int splits = first_round && max_splits > 1 ? max_splits : max_kg_splits;
+
+ if (splits > 1) {
+ List<Split!> tmp = Split.DoSplit(s, max_vc_cost, splits);
+ max_vc_cost = 1.0; // for future
+ first_round = false;
+ //tmp.Sort(new Comparison<Split!>(Split.Compare));
+ foreach (Split! a in tmp) {
+ work.Push(a);
+ total++;
+ remaining_cost += a.Cost;
+ }
+ if (outcome != Outcome.Errors) {
+ outcome = Outcome.Correct;
+ }
+ } else {
+ assert outcome != Outcome.Correct;
+ if (outcome == Outcome.TimedOut) {
+ string! msg = "some timeout";
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ msg = s.reporter.resourceExceededMessage;
+ }
+ callback.OnTimeout(msg);
+ } else if (outcome == Outcome.OutOfMemory) {
+ string! msg = "out of memory";
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ msg = s.reporter.resourceExceededMessage;
+ }
+ callback.OnOutOfMemory(msg);
+ }
+
+ break;
+ }
+ }
+ }
+
+ if (outcome == Outcome.Correct && smoke_tester != null) {
+ smoke_tester.Test();
+ }
+
+ callback.OnProgress("done", 0, 0, 1.0);
+
+ return outcome;
+ }
+
+ public class ErrorReporter : ProverInterface.ErrorHandler {
+ Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins;
+ Hashtable/*<int, Absy!>*/! label2absy;
+ List<Block!>! blocks;
+ protected Dictionary<Incarnation, Absy!>! incarnationOriginMap;
+ protected VerifierCallback! callback;
+ internal string? resourceExceededMessage;
+ static private System.IO.TextWriter? modelWriter;
+
+ static protected TextWriter! ModelWriter {
+ get {
+ if (ErrorReporter.modelWriter == null)
+ ErrorReporter.modelWriter = CommandLineOptions.Clo.PrintErrorModelFile == null ? Console.Out : new StreamWriter(CommandLineOptions.Clo.PrintErrorModelFile, false);
+ return ErrorReporter.modelWriter;
+ }
+ }
+
+ public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ List<Block!>! blocks,
+ Dictionary<Incarnation, Absy!>! incarnationOriginMap,
+ VerifierCallback! callback)
+ {
+ this.gotoCmdOrigins = gotoCmdOrigins;
+ this.label2absy = label2absy;
+ this.blocks = blocks;
+ this.incarnationOriginMap = incarnationOriginMap;
+ this.callback = callback;
+ // base();
+ }
+
+ public override void OnModel(IList<string!>! labels, ErrorModel errModel) {
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {
+ errModel.Print(ErrorReporter.ModelWriter);
+ ErrorReporter.ModelWriter.Flush();
+ }
+ Hashtable traceNodes = new Hashtable();
+ foreach (string! s in labels) {
+ Absy! absy =Label2Absy(s);
+ if (traceNodes.ContainsKey(absy))
+ System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");
+ else
+ traceNodes.Add(absy, null);
+ }
+
+ BlockSeq! trace = new BlockSeq();
+ Block! entryBlock = (!) this.blocks[0];
+ assert traceNodes.Contains(entryBlock);
+ trace.Add(entryBlock);
+
+ Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap);
+
+ if (newCounterexample == null) return;
+
+ #region Map passive program errors back to original program errors
+ ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;
+ if (returnExample != null)
+ {
+ foreach (Block! b in returnExample.Trace) {
+ assume b.TransferCmd != null;
+ ReturnCmd cmd = (ReturnCmd) gotoCmdOrigins[b.TransferCmd];
+ if (cmd != null)
+ {
+ returnExample.FailingReturn = cmd;
+ break;
+ }
+ }
+ }
+ #endregion
+ callback.OnCounterexample(newCounterexample, null);
+ }
+
+ public override Absy! Label2Absy(string! label)
+ {
+ int id = int.Parse(label);
+ return (Absy!) label2absy[id];
+ }
+
+ public override void OnResourceExceeded(string! msg)
+ {
+ resourceExceededMessage = msg;
+ }
+ }
+
+ public class ErrorReporterLocal : ErrorReporter {
+ public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ List<Block!>! blocks,
+ Dictionary<Incarnation, Absy!>! incarnationOriginMap,
+ VerifierCallback! callback)
+ {
+ base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback); // here for aesthetic purposes
+ }
+
+ public override void OnModel(IList<string!>! labels, ErrorModel errModel) {
+ // We ignore the error model here for enhanced error message purposes.
+ // It is only printed to the command line.
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {
+ if (CommandLineOptions.Clo.PrintErrorModelFile != null) {
+ errModel.Print(ErrorReporter.ModelWriter);
+ ErrorReporter.ModelWriter.Flush();
+ }
+ }
+ List<Block!> traceNodes = new List<Block!>();
+ List<AssertCmd!> assertNodes = new List<AssertCmd!>();
+ foreach (string! s in labels) {
+ Absy node = Label2Absy(s);
+ if (node is Block) {
+ Block b = (Block)node;
+ traceNodes.Add(b);
+ } else {
+ AssertCmd a = (AssertCmd)node;
+ assertNodes.Add(a);
+ }
+ }
+ assert assertNodes.Count > 0;
+ assert traceNodes.Count == assertNodes.Count;
+
+ foreach (AssertCmd a in assertNodes) {
+ // find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here)
+ foreach (Block b in traceNodes) {
+ if (b.Cmds.Has(a)) {
+ BlockSeq trace = new BlockSeq();
+ trace.Add(b);
+ Counterexample newCounterexample = AssertCmdToCounterexample(a, (!)b.TransferCmd, trace, errModel, incarnationOriginMap);
+ callback.OnCounterexample(newCounterexample, null);
+ goto NEXT_ASSERT;
+ }
+ }
+ assert false; // there was no block that contains the assert
+ NEXT_ASSERT: {}
+ }
+ }
+ }
+
+ protected void ConvertCFG2DAG(Implementation! impl, Program! program)
+ {
+ impl.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
+
+ current_impl = impl;
+ variable2SequenceNumber = new Hashtable/*Variable -> int*/();
+ incarnationOriginMap = new Dictionary<Incarnation, Absy!>();
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ Console.WriteLine("original implementation");
+ EmitImpl(impl, false);
+ }
+ #endregion
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ Console.WriteLine("after desugaring sugared commands like procedure calls");
+ EmitImpl(impl, true);
+ }
+ #endregion
+
+ ComputePredecessors(impl.Blocks);
+
+ #region Convert program CFG into a DAG
+
+ #region Use the graph library to figure out where the (natural) loops are
+
+ #region Create the graph by adding the source node and each edge
+ Graph<Block>! g = GraphFromImpl(impl);
+ #endregion
+
+ g.ComputeLoops(); // this is the call that does all of the processing
+ if (!g.Reducible)
+ {
+ throw new VCGenException("Irreducible flow graphs are unsupported.");
+ }
+
+ #endregion
+
+ #region Cut the backedges, push assert/assume statements from loop header into predecessors, change them all into assume statements at top of loop, introduce havoc statements
+ foreach (Block! header in (!) g.Headers)
+ {
+ IDictionary<Block!,object> backEdgeNodes = new Dictionary<Block!,object>();
+ foreach (Block! b in (!) g.BackEdgeNodes(header)) { backEdgeNodes.Add(b, null); }
+
+ #region Find the (possibly empty) prefix of assert commands in the header, replace each assert with an assume of the same condition
+ CmdSeq prefixOfPredicateCmdsInit = new CmdSeq();
+ CmdSeq prefixOfPredicateCmdsMaintained = new CmdSeq();
+ for (int i = 0, n = header.Cmds.Length; i < n; i++)
+ {
+ PredicateCmd a = header.Cmds[i] as PredicateCmd;
+ if (a != null)
+ {
+ if (a is AssumeCmd) {
+ prefixOfPredicateCmdsInit.Add(a);
+ prefixOfPredicateCmdsMaintained.Add(a);
+ } else {
+ Bpl.AssertCmd c = (AssertCmd) a;
+ Bpl.AssertCmd b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);
+ b.ErrorData = c.ErrorData;
+ prefixOfPredicateCmdsInit.Add(b);
+ b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
+ b.ErrorData = c.ErrorData;
+ prefixOfPredicateCmdsMaintained.Add(b);
+ header.Cmds[i] = new AssumeCmd(c.tok,c.Expr);
+ }
+ }
+ else if ( header.Cmds[i] is CommentCmd )
+ {
+ // ignore
+ }
+ else
+ {
+ break; // stop when an assignment statement (or any other non-predicate cmd) is encountered
+ }
+ }
+ #endregion
+
+ #region Copy the prefix of predicate commands into each predecessor. Do this *before* cutting the backedge!!
+ for ( int predIndex = 0, n = header.Predecessors.Length; predIndex < n; predIndex++ )
+ {
+ Block! pred = (!)header.Predecessors[predIndex];
+
+ // Create a block between header and pred for the predicate commands if header has more than one successor
+ // or if pred is a back edge node
+ GotoCmd gotocmd = pred.TransferCmd as GotoCmd;
+ if ((backEdgeNodes.ContainsKey(pred)) || (gotocmd != null && gotocmd.labelNames != null && gotocmd.labelNames.Length > 1))
+ {
+ Block! newBlock = CreateBlockBetween(predIndex, header);
+ impl.Blocks.Add(newBlock);
+
+ // if pred is a back edge node, then now newBlock is the back edge node
+ if (backEdgeNodes.ContainsKey(pred))
+ {
+ backEdgeNodes.Remove(pred);
+ backEdgeNodes.Add(newBlock,null);
+ }
+
+ pred = newBlock;
+ }
+ // Add the predicate commands
+ if (backEdgeNodes.ContainsKey(pred)){
+ pred.Cmds.AddRange(prefixOfPredicateCmdsMaintained);
+ }
+ else {
+ pred.Cmds.AddRange(prefixOfPredicateCmdsInit);
+ }
+ }
+ #endregion
+
+ #region Cut the back edge
+ foreach (Block! backEdgeNode in (!)backEdgeNodes.Keys)
+ {
+ Debug.Assert(backEdgeNode.TransferCmd is GotoCmd,"An node was identified as the source for a backedge, but it does not have a goto command.");
+ GotoCmd gtc = backEdgeNode.TransferCmd as GotoCmd;
+ if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Length > 1 )
+ {
+ // then remove the backedge by removing the target block from the list of gotos
+ BlockSeq remainingTargets = new BlockSeq();
+ StringSeq remainingLabels = new StringSeq();
+ assume gtc.labelNames != null;
+ for (int i = 0, n = gtc.labelTargets.Length; i < n; i++)
+ {
+ if ( gtc.labelTargets[i] != header )
+ {
+ remainingTargets.Add(gtc.labelTargets[i]);
+ remainingLabels.Add(gtc.labelNames[i]);
+ }
+ }
+ gtc.labelTargets = remainingTargets;
+ gtc.labelNames = remainingLabels;
+ }
+ else
+ {
+ // This backedge is the only out-going edge from this node.
+ // Add an "assume false" statement to the end of the statements
+ // inside of the block and change the goto command to a return command.
+ AssumeCmd ac = new AssumeCmd(Token.NoToken,Expr.False);
+ backEdgeNode.Cmds.Add(ac);
+ backEdgeNode.TransferCmd = new ReturnCmd(Token.NoToken);
+ }
+ #region Remove the backedge node from the list of predecessor nodes in the header
+ BlockSeq newPreds = new BlockSeq();
+ foreach ( Block p in header.Predecessors )
+ {
+ if ( p != backEdgeNode )
+ newPreds.Add(p);
+ }
+ header.Predecessors = newPreds;
+ #endregion
+ }
+ #endregion
+
+ #region Collect all variables that are assigned to in all of the natural loops for which this is the header
+ VariableSeq varsToHavoc = new VariableSeq();
+ foreach (Block! backEdgeNode in (!) g.BackEdgeNodes(header))
+ {
+ foreach ( Block! b in g.NaturalLoops(header,backEdgeNode) )
+ {
+ foreach ( Cmd! c in b.Cmds )
+ {
+ c.AddAssignedVariables(varsToHavoc);
+ }
+ }
+ }
+ IdentifierExprSeq havocExprs = new IdentifierExprSeq();
+ foreach ( Variable! v in varsToHavoc )
+ {
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ if(!havocExprs.Has(ie))
+ havocExprs.Add(ie);
+ }
+ // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct
+ // the source location for this later on
+ HavocCmd hc = new HavocCmd(header.tok,havocExprs);
+ CmdSeq newCmds = new CmdSeq();
+ newCmds.Add(hc);
+ foreach ( Cmd c in header.Cmds )
+ {
+ newCmds.Add(c);
+ }
+ header.Cmds = newCmds;
+ #endregion
+ }
+ #endregion
+ #endregion Convert program CFG into a DAG
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ Console.WriteLine("after conversion into a DAG");
+ EmitImpl(impl, true);
+ }
+ #endregion
+ }
+
+ protected Hashtable/*TransferCmd->ReturnCmd*/! PassifyImpl(Implementation! impl, Program! program)
+ {
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();
+ Block/*?*/ exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ Console.WriteLine("after creating a unified exit block");
+ EmitImpl(impl, true);
+ }
+ #endregion
+
+ #region Insert pre- and post-conditions and where clauses as assume and assert statements
+ {
+ CmdSeq cc = new CmdSeq();
+ // where clauses of global variables
+ foreach (Declaration d in program.TopLevelDeclarations) {
+ GlobalVariable gvar = d as GlobalVariable;
+ if (gvar != null && gvar.TypedIdent.WhereExpr != null) {
+ Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);
+ cc.Add(c);
+ }
+ }
+ // where clauses of in- and out-parameters
+ cc.AddRange(GetParamWhereClauses(impl));
+ // where clauses of local variables
+ foreach (Variable! lvar in impl.LocVars) {
+ if (lvar.TypedIdent.WhereExpr != null) {
+ Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr);
+ cc.Add(c);
+ }
+ }
+
+ InjectPreconditions(impl);
+ //cc.AddRange(GetPre(impl));
+
+ Block! entryBlock = (!) impl.Blocks[0];
+ cc.AddRange(entryBlock.Cmds);
+ entryBlock.Cmds = cc;
+
+ InjectPostConditions(impl,exitBlock,gotoCmdOrigins);
+ //CmdSeq! post = GetPost(impl);
+ //exitBlock.Cmds.AddRange(post);
+ }
+ #endregion
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ Console.WriteLine("after inserting pre- and post-conditions");
+ EmitImpl(impl, true);
+ }
+ #endregion
+
+ AddBlocksBetween(impl);
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ Console.WriteLine("after adding empty blocks before all blocks with more than one predecessor");
+ EmitImpl(impl, true);
+ }
+ #endregion
+
+ Convert2PassiveCmd(impl);
+
+ #region Peep-hole optimizations
+ if (CommandLineOptions.Clo.RemoveEmptyBlocks){
+ #region Get rid of empty blocks
+ {
+ Block! entryBlock = (!) impl.Blocks[0];
+ RemoveEmptyBlocks(entryBlock);
+ impl.PruneUnreachableBlocks();
+ }
+ #endregion Get rid of empty blocks
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ Console.WriteLine("after peep-hole optimizations");
+ EmitImpl(impl, true);
+ }
+ #endregion
+ }
+ #endregion Peep-hole optimizations
+
+// #region Constant Folding
+// #endregion
+// #region Debug Tracing
+// if (CommandLineOptions.Clo.TraceVerify)
+// {
+// Console.WriteLine("after constant folding");
+// EmitImpl(impl, true);
+// }
+// #endregion
+
+ return gotoCmdOrigins;
+ }
+
+ static Counterexample TraceCounterexample(Block! b, Hashtable! traceNodes, BlockSeq! trace, ErrorModel errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap)
+ {
+ // After translation, all potential errors come from asserts.
+ CmdSeq! cmds = b.Cmds;
+ TransferCmd! transferCmd = (!)b.TransferCmd;
+ for (int i = 0; i < cmds.Length; i++)
+ {
+ Cmd! cmd = (!) cmds[i];
+
+ // Skip if 'cmd' not contained in the trace or not an assert
+ if (!(cmd is AssertCmd) || !traceNodes.Contains(cmd))
+ continue;
+
+ return AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, incarnationOriginMap);
+ }
+
+ GotoCmd gotoCmd = transferCmd as GotoCmd;
+ if (gotoCmd != null)
+ {
+ foreach (Block! bb in (!)gotoCmd.labelTargets)
+ {
+ if (traceNodes.Contains(bb)){
+ trace.Add(bb);
+ return TraceCounterexample(bb, traceNodes, trace, errModel, incarnationOriginMap);
+ }
+ }
+ }
+
+ return null;
+
+ // Debug.Fail("Could not find failing node.");
+ // throw new Microsoft.Contracts.AssertException();
+ }
+
+
+ static void /*return printable error!*/ ApplyEnhancedErrorPrintingStrategy (Bpl.Expr! expr, Hashtable /*Variable -> Expr*/! incarnationMap, MiningStrategy errorDataEnhanced, ErrorModel! errModel, Dictionary<Expr!, object>! exprToPrintableValue, List<string!>! relatedInformation, bool printInternalStateDumpOnce, Dictionary<Incarnation, Absy!>! incarnationOriginMap) {
+ if (errorDataEnhanced is ListOfMiningStrategies) {
+ ListOfMiningStrategies loms = (ListOfMiningStrategies) errorDataEnhanced;
+ List<MiningStrategy>! l = loms.msList;
+ for (int i = 0; i < l.Count; i++) {
+ MiningStrategy ms = l[i];
+ if (ms != null) {
+ ApplyEnhancedErrorPrintingStrategy(expr, incarnationMap, l[i], errModel, exprToPrintableValue, relatedInformation, false, incarnationOriginMap);
+ }
+ }
+ }
+ else if (errorDataEnhanced is EEDTemplate /*EDEverySubExpr*/) {
+ EEDTemplate eedT = (EEDTemplate) errorDataEnhanced;
+ string reason = eedT.reason;
+ List<Bpl.Expr!> listOfExprs = eedT.exprList;
+ if (listOfExprs != null) {
+ List<string> holeFillers = new List<string>();
+ for (int i = 0; i < listOfExprs.Count; i++) {
+ bool alreadySet = false;
+ foreach (KeyValuePair<Bpl.Expr!, object> kvp in exprToPrintableValue) {
+ Bpl.Expr! e = kvp.Key;
+ Bpl.Expr! f = listOfExprs[i];
+ // the strings are compared instead of the actual expressions because
+ // the expressions might not be identical, but their print-out strings will be
+ if (e.ToString() == f.ToString()) {
+ object o = kvp.Value;
+ if (o != null) {
+ holeFillers.Add(o.ToString());
+ alreadySet = true;
+ break;
+ }
+ }
+ }
+ if (!alreadySet) {
+ // no information about that Expression found, so put in <unknown>
+ holeFillers.Add("<unknown>");
+ }
+ }
+ reason = FormatReasonString(reason, holeFillers);
+ }
+ if (reason != null) {
+ relatedInformation.Add("(related information): "+reason);
+ }
+ } else {
+ // define new templates here!
+ }
+
+ if (printInternalStateDumpOnce) {
+ ComputeAndTreatHeapSuccessions(incarnationMap, errModel, incarnationOriginMap, relatedInformation);
+
+ // default action: print all values!
+ foreach (KeyValuePair<Bpl.Expr!, object> kvp in exprToPrintableValue) {
+ object o = kvp.Value;
+ if (o != null) {
+ // We do not want to print LiteralExprs because that gives things like 0 == 0.
+ // If both arguments to the string.Format are the same it is also useless,
+ // as that would print e.g. $a == $a.
+ if (!(kvp.Key is LiteralExpr)&& kvp.Key.ToString() != o.ToString()) {
+ string boogieExpr;
+ // check whether we are handling BPL or SSC input
+ if (CommandLineOptions.Clo.RunningBoogieOnSsc) {
+ boogieExpr = Helpers.PrettyPrintBplExpr(kvp.Key);
+ } else {
+ boogieExpr = kvp.Key.ToString();
+ }
+ relatedInformation.Add("(internal state dump): "+string.Format("{0} == {1}", boogieExpr, o));
+ }
+ }
+ }
+ }
+ }
+
+ static void ComputeAndTreatHeapSuccessions(System.Collections.Hashtable! incarnationMap, ErrorModel! errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap, List<string!>! relatedInformation) {
+ List<int> heapSuccList = ComputeHeapSuccessions(incarnationMap, errModel);
+ TreatHeapSuccessions(heapSuccList, incarnationMap, errModel, incarnationOriginMap, relatedInformation);
+ }
+
+ static List<int> ComputeHeapSuccessions(System.Collections.Hashtable! incarnationMap, ErrorModel! errModel) {
+ // find the heap variable
+ Variable heap = null;
+ ICollection ic = incarnationMap.Keys;
+ foreach (object o in ic) {
+ if (o is GlobalVariable) {
+ GlobalVariable gv = (GlobalVariable) o;
+ if (gv.Name == "$Heap") {
+ heap = gv;
+ }
+ }
+ }
+ List<int> heapIdSuccession = new List<int>();
+ if (heap == null) {
+ // without knowing the name of the current heap we cannot create a heap succession!
+ } else {
+ object oHeap = incarnationMap[heap];
+ if (oHeap != null) {
+ string currentHeap = oHeap.ToString();
+ int currentHeapId;
+ if (errModel.identifierToPartition.TryGetValue(currentHeap, out currentHeapId)) {
+ while (currentHeapId != -1) {
+ if (!heapIdSuccession.Contains(currentHeapId)) {
+ heapIdSuccession.Add(currentHeapId);
+ currentHeapId = ComputePredecessorHeapId(currentHeapId, errModel);
+ } else {
+ // looping behavior, just stop here and do not add this value (again!)
+ break;
+ }
+ }
+ }
+ }
+ }
+ if (heapIdSuccession.Count > 0) {
+ int heapId = heapIdSuccession[heapIdSuccession.Count-1];
+ List<string!> strl = errModel.partitionToIdentifiers[heapId];
+ if (strl != null && strl.Contains("$Heap")) {
+ // we have a proper succession of heaps that starts with $Heap
+ return heapIdSuccession;
+ } else {
+ // no proper heap succession, not starting with $Heap!
+ return null;
+ }
+ } else {
+ // no heap succession found because either the $Heap does not have a current incarnation
+ // or because (unlikely!) the model is somehow messed up
+ return null;
+ }
+ }
+
+ static int ComputePredecessorHeapId(int id, ErrorModel! errModel) {
+ //check "$HeapSucc" and "store2" functions:
+ List<int> heapSuccPredIdList = new List<int>();
+ List<List<int>> heapSuccFunc;
+ errModel.definedFunctions.TryGetValue("$HeapSucc", out heapSuccFunc);
+ if (heapSuccFunc != null) {
+ foreach (List<int> heapSuccFuncDef in heapSuccFunc) {
+ // do not look at the else case of the function def, so check .Count
+ if (heapSuccFuncDef != null && heapSuccFuncDef.Count == 3 && heapSuccFuncDef[1] == id) {
+ // make sure each predecessor is put into the list at most once
+ if (!heapSuccPredIdList.Contains(heapSuccFuncDef[0])) {
+ heapSuccPredIdList.Add(heapSuccFuncDef[0]);
+ }
+ }
+ }
+ }
+ List<int> store2PredIdList = new List<int>();;
+ List<List<int>> store2Func;
+ errModel.definedFunctions.TryGetValue("store2", out store2Func);
+ if (store2Func != null) {
+ foreach (List<int> store2FuncDef in store2Func) {
+ // do not look at the else case of the function def, so check .Count
+ if (store2FuncDef != null && store2FuncDef.Count == 5 && store2FuncDef[4] == id) {
+ // make sure each predecessor is put into the list at most once
+ if (!store2PredIdList.Contains(store2FuncDef[0])) {
+ store2PredIdList.Add(store2FuncDef[0]);
+ }
+ }
+ }
+ }
+ if (heapSuccPredIdList.Count + store2PredIdList.Count > 0) {
+ if (store2PredIdList.Count == 1) {
+ return store2PredIdList[0];
+ } else if (store2PredIdList.Count == 0) {
+ if (heapSuccPredIdList.Count == 1) {
+ return heapSuccPredIdList[0];
+ } else { //(heapSuccPredIdList.Count > 1)
+ if (heapSuccPredIdList.Count == 2) {
+ // if one of the 2 is a self-loop, take the other!
+ if (heapSuccPredIdList[0] == id) {
+ return heapSuccPredIdList[1];
+ } else if (heapSuccPredIdList[1] == id) {
+ return heapSuccPredIdList[0];
+ } else {
+ //no self-loop, two different predecessors, cannot choose
+ return -1;
+ }
+ } else {
+ // at least 3 different predecessors available, one of them could be a self-loop, but
+ // we cannot choose between the other 2 (or more) candidates
+ return -1;
+ }
+ }
+ } else {
+ // more than one result in the succession coming from store2, no way
+ // to decide which is right, end here
+ return -1;
+ }
+ } else {
+ // no predecessor found
+ return -1;
+ }
+ }
+
+ static void TreatHeapSuccessions (List<int> heapSuccessionList, System.Collections.Hashtable! incarnationMap, ErrorModel! errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap, List<string!>! relatedInformation) {
+ if (heapSuccessionList == null) {
+ // empty list of heap successions, nothing we can do!
+ return;
+ }
+ // primarily look for $o and $f (with skolem-id stuff) and then look where they were last changed!
+ // find the o and f variables
+ Variable dollarO = null;
+ Variable dollarF = null;
+ ICollection ic = incarnationMap.Keys;
+ foreach (object o in ic) {
+ if (o is BoundVariable) {
+ BoundVariable bv = (BoundVariable) o;
+ if (bv.Name == "$o") {
+ dollarO = bv;
+ }
+ else if (bv.Name == "$f") {
+ dollarF = bv;
+ }
+ }
+ }
+ if (dollarO == null || dollarF == null) {
+ // without knowing the name of the current incarnation of $Heap, $o and $f we don't do anything here
+ } else {
+ object objO = incarnationMap[dollarO];
+ object objF = incarnationMap[dollarF];
+ if (objO != null && objF != null) {
+ int zidO = errModel.identifierToPartition[objO.ToString()];
+ int zidF = errModel.identifierToPartition[objF.ToString()];
+
+ List<List<int>> select2Func = null;
+ if (errModel.definedFunctions.TryGetValue("select2", out select2Func) && select2Func != null) {
+ // check for all changes to $o.$f!
+ List<int> heapsChangedOFZid = new List<int>();
+ int oldValueZid = -1;
+ int newValueZid = -1;
+
+ for (int i = 0; i < heapSuccessionList.Count; i++) {
+ bool foundValue = false;
+ foreach (List<int> f in select2Func) {
+ if (f != null && f.Count == 4 && f[0] == heapSuccessionList[i] && f[1] == zidO && f[2] == zidF) {
+ newValueZid = f[3];
+ foundValue = true;
+ break;
+ }
+ }
+ if (!foundValue) {
+ // get default of the function once Leo&Nikolaj have changed it so the default is type correct
+ // for now treat it as a -1 !
+ // the last element of select2Func is the else case, it has only 1 element, so grab that:
+ // newValueZid = (select2Func[select2Func.Count-1])[0];
+ newValueZid = -1;
+ }
+
+ if (oldValueZid != newValueZid) {
+ // there was a change here, record that in the list:
+ if (oldValueZid != -1) {
+ // don't record a change at the "initial" location, which refers to the $Heap in
+ // its current incarnation, and is marked by the oldValueZid being uninitialized
+ heapsChangedOFZid.Add(heapSuccessionList[i-1]);
+ }
+ oldValueZid = newValueZid;
+ }
+ }
+
+ foreach (int id in heapsChangedOFZid) {
+ //get the heap name out of the errModel for this zid:
+ List<string!> l = errModel.partitionToIdentifiers[id];
+ List<string!> heaps = new List<string!>();
+ if (l!=null) {
+ foreach (string s in l) {
+ if (s.StartsWith("$Heap")) {
+ heaps.Add(s);
+ }
+ }
+ }
+ // easy case first:
+ if (heaps.Count == 1) {
+ string heapName = heaps[0];
+ // we have a string with the name of the heap, but we need to get the
+ // source location out of a map that uses Incarnations!
+
+ ICollection incOrgMKeys = incarnationOriginMap.Keys;
+ foreach (Incarnation inc in incOrgMKeys) {
+ if (inc!= null) {
+ if (inc.Name == heapName) {
+ Absy source = null;
+ incarnationOriginMap.TryGetValue(inc, out source);
+ if (source != null) {
+ if (source is Block) {
+ Block b = (Block) source;
+ string fileName = b.tok.filename;
+ if (fileName != null) {
+ fileName = fileName.Substring(fileName.LastIndexOf('\\') + 1);
+ }
+ relatedInformation.Add("(related information): Changed $o.$f here: " + fileName + "(" + b.tok.line + "," + b.tok.col + ")");
+ } else if (source is Cmd) {
+ Cmd c = (Cmd) source;
+ string fileName = c.tok.filename;
+ if (fileName != null) {
+ fileName = fileName.Substring(fileName.LastIndexOf('\\') + 1);
+ }
+ relatedInformation.Add("(related information) Changed $o.$f here: " + fileName + "(" + c.tok.line + "," + c.tok.col + ")");
+ } else {
+ assert false;
+ }
+ }
+ }
+ }
+ }
+ } else {
+ // more involved! best use some of the above code and try to synchronize joint parts
+ // here there is more than one "$Heap@i" in the partition, check if they all agree on one
+ // source location or maybe if some of them are joins (i.e. blocks) that should be ignored
+ }
+
+ }
+ }
+ }
+ }
+ }
+
+ static string FormatReasonString (string reason, List<string> holeFillers) {
+ if (holeFillers != null) {
+ // in case all elements of holeFillers are "<unknown>" we can not say anything useful
+ // so just say nothing and return null
+ bool allUnknown = true;
+ foreach (string s in holeFillers) {
+ if (s != "<unknown>") {
+ allUnknown = false;
+ break;
+ }
+ }
+ if (allUnknown) {
+ return null;
+ }
+ string[] a = holeFillers.ToArray();
+ reason = string.Format(reason, a);
+ }
+ return reason;
+ }
+
+ static object ValueFromZID (ErrorModel! errModel, int id) {
+ return ValueFromZID(errModel, id, null);
+ }
+
+ static object ValueFromZID (ErrorModel! errModel, int id, string searchForAlternate) {
+ object o = errModel.partitionToValue[id];
+ if (o != null) {
+ return o;
+ } else {
+ // more elaborate scheme to find something better, as in: look at the identifiers that
+ // this partition maps to, or similar things!
+
+ //treatment for 'null':
+ int idForNull = -1;
+ if (errModel.valueToPartition.TryGetValue("nullObject", out idForNull) && idForNull == id) {
+ return "nullObject";
+ }
+
+ string returnStr = null;
+
+ // "good identifiers" if there is no value found are 'unique consts' or
+ // '$in' parameters; '$in' parameters are treated, unclear how to get 'unique const' info
+ List<string!> identifiers = errModel.partitionToIdentifiers[id];
+ if (identifiers != null) {
+ foreach (string s in identifiers) {
+ //$in parameters are (more) interesting than other identifiers, return the
+ // first one found
+ if (s.EndsWith("$in")) {
+ returnStr = s;
+ break;
+ }
+ }
+ }
+
+ // try to get mappings from one identifier to another if there are exactly
+ // two identifiers in the partition, where one of them is the identifier for which
+ // we search for alternate encodings (third parameter of the method) [or an incarnation
+ // of such an identifier]
+ if (returnStr == null && searchForAlternate != null && identifiers != null && identifiers.Count == 2) {
+ if (identifiers[0] == searchForAlternate || identifiers[0].StartsWith(searchForAlternate + ".sk.")) {
+ returnStr = identifiers[1];
+ } else if (identifiers[1] == searchForAlternate || identifiers[1].StartsWith(searchForAlternate + ".sk.")) {
+ returnStr = identifiers[0];
+ }
+ }
+
+ if (returnStr != null) {
+ return Helpers.BeautifyBplString(returnStr);
+ }
+
+ return null;
+ }
+ }
+
+ static int TreatInterpretedFunction(string! functionName, List<int>! zargs, ErrorModel! errModel) {
+ if (zargs.Count != 2) {
+ //all interpreted functions are binary, so there have to be exactly two arguments
+ return -1;
+ }
+ else {
+ object arg0 = ValueFromZID(errModel, zargs[0]);
+ object arg1 = ValueFromZID(errModel, zargs[1]);
+ if (arg0 is BigNum && arg1 is BigNum) {
+ BigNum arg0i = (BigNum)arg0;
+ BigNum arg1i = (BigNum)arg1;
+ BigNum result;
+ if (functionName == "+") {
+ result = arg0i + arg1i;
+ } else if (functionName == "-") {
+ result = arg0i - arg1i;
+ } else /*if (functionName == "*")*/ {
+ result = arg0i * arg1i;
+ }
+ int returnId = -1;
+ if (errModel.valueToPartition.TryGetValue(result, out returnId)) {
+ return returnId;
+ } else {
+ return -1;
+ }
+ }
+ else {
+ //both arguments need to be integers for this to work!
+ return -1;
+ }
+ }
+ }
+
+ static int TreatFunction (string! functionName, List<int>! zargs, bool undefined, ErrorModel! errModel) {
+ List<List<int>> functionDef;
+ if ((!errModel.definedFunctions.TryGetValue(functionName, out functionDef) && functionName != "+" && functionName != "-" && functionName != "*") || undefined) {
+ // no fitting function found or one of the arguments is undefined
+ return -1;
+ } else {
+ if (functionName == "+" || functionName == "-" || functionName == "*") {
+ return TreatInterpretedFunction(functionName, zargs, errModel);
+ }
+ assert functionDef != null;
+ foreach (List<int> pWiseF in functionDef) {
+ assert pWiseF != null;
+ // else case in the function definition:
+ if (pWiseF.Count == 1) {
+ return pWiseF[0];
+ }
+ // number of arguments is exactly the right number
+ assert zargs.Count == pWiseF.Count - 1;
+ if (forall{int i in (0: zargs.Count); zargs[i] == pWiseF[i]}) {
+ return pWiseF[pWiseF.Count - 1];
+ }
+ }
+ // all functions should have an 'else ->' case defined, therefore this should be
+ // unreachable code!
+ assert false;
+ }
+ }
+
+ //returned int is zID
+ static int GetValuesFromModel (Bpl.Expr! expr, Hashtable /*Variable -> Expr*/! incarnationMap, ErrorModel! errModel, Dictionary<Bpl.Expr!, object>! exprToPrintableValue)
+ modifies exprToPrintableValue.*;
+ {
+ // call GetValuesFromModel on all proper subexpressions, returning their value,
+ // so they only have to be computed once!
+ if (expr is LiteralExpr) {
+ // nothing needs to be added to the exprToPrintableValue map, because e.g. 0 -> 0 is not interesting
+ object o = ((LiteralExpr) expr).Val;
+ if (o == null) {
+ o = "nullObject";
+ }
+ int idForExprVal;
+ if (errModel.valueToPartition.TryGetValue(o, out idForExprVal)) {
+ return idForExprVal;
+ } else {
+ return -1;
+ }
+ }
+ else if (expr is IdentifierExpr) {
+ // if the expression expr is in the incarnation map, then use its incarnation,
+ // otherwise just use the actual expression
+ string s = ((IdentifierExpr) expr).Name;
+ object o = null;
+ Variable v = ((IdentifierExpr) expr).Decl;
+ if (v != null && incarnationMap.ContainsKey(v)) {
+ if (incarnationMap[v] is IdentifierExpr!) {
+ s = ((IdentifierExpr!) incarnationMap[v]).Name;
+ } else if (incarnationMap[v] is LiteralExpr!) {
+ o = ((LiteralExpr!) incarnationMap[v]).Val;
+ }
+ }
+ // if o is not null, then we got a LiteralExpression, that needs separate treatment
+ if (o == null) {
+ // if the expression (respectively its incarnation) is mapped to some partition
+ // then return that id, else return the error code -1
+ if (errModel.identifierToPartition.ContainsKey(s)) {
+ int i = errModel.identifierToPartition[s];
+ // if the key is already in the map we can assume that it is the same map we would
+ // get now and thus just ignore it
+ if (!exprToPrintableValue.ContainsKey(expr)) {
+ exprToPrintableValue.Add(expr, ValueFromZID(errModel, i, ((IdentifierExpr) expr).Name));
+ }
+ return i;
+ } else {
+ return -1;
+ }
+ } else if (errModel.valueToPartition.ContainsKey(o)) {
+ int i = errModel.valueToPartition[o];
+ if (!exprToPrintableValue.ContainsKey(expr))
+ exprToPrintableValue.Add(expr, ValueFromZID(errModel, i));
+ return i;
+ } else {
+ return -1;
+ }
+ }
+ else if (expr is Bpl.NAryExpr) {
+ Bpl.NAryExpr e = (Bpl.NAryExpr)expr;
+ List<int> zargs = new List<int>();
+ bool undefined = false;
+ // do the recursion first
+ foreach (Expr argument in ((NAryExpr) expr).Args) {
+ int zid = -1;
+ if (argument != null) {
+ zid = GetValuesFromModel(argument, incarnationMap, errModel, exprToPrintableValue);
+ }
+ // if one of the arguments is 'undefined' then return -1 ('noZid') for this
+ // but make sure the recursion is complete first1
+ if (zid == -1) {
+ undefined = true;
+ }
+ zargs.Add(zid);
+ }
+ IAppliable! fun = e.Fun;
+ string functionName = fun.FunctionName; // PR: convert to select1, select2, etc in case of a map?
+ // same as IndexedExpr:
+ int id = TreatFunction(functionName, zargs, undefined, errModel);
+ if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {
+ exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));
+ }
+ return id;
+ }
+ else if (expr is Bpl.OldExpr) {
+ //Bpl.OldExpr e = (Bpl.OldExpr)expr;
+ // We do not know which heap is the old heap and what the latest state change was,
+ // therefore we cannot return anything useful here!
+ return -1;
+ }
+ else if (expr is Bpl.QuantifierExpr) {
+ Bpl.QuantifierExpr q = (Bpl.QuantifierExpr)expr;
+ for (int i = 0; i < q.Dummies.Length; i++) {
+ Bpl.Variable v = q.Dummies[i];
+ if (v != null) {
+ // add to the incarnation map a connection between the bound variable v
+ // of the quantifier and its skolemized incarnation, if available,
+ // i.e., search through the list of identifiers in the model and look for
+ // v.sk.(q.SkolemId), only pick those that are directly associated to a value
+ // DISCLAIMER: of course it is very well possible that one of these incarnations
+ // could be used without actually having a value, but it seems better to pick those
+ // with a value, that is they are more likely to contribute useful information to
+ // the output
+ List<Bpl.IdentifierExpr!> quantVarIncarnationList = new List<Bpl.IdentifierExpr!>();
+ List<int> incarnationZidList = new List<int>();
+ int numberOfNonNullValueIncarnations = 0;
+ for (int j = 0; j < errModel.partitionToIdentifiers.Count; j++){
+ List<string!> pti = errModel.partitionToIdentifiers[j];
+ if (pti != null) {
+ for (int k = 0; k < pti.Count; k++) {
+ // look for v.sk.(q.SkolemId)
+ // if there is more than one look at if there is exactly one with a non-null value
+ // associated, see above explanation
+ if (pti[k].StartsWith(v + ".sk." + q.SkolemId) &&
+ errModel.partitionToValue[errModel.identifierToPartition[pti[k]]] != null) {
+ quantVarIncarnationList.Add(new Bpl.IdentifierExpr(Bpl.Token.NoToken, pti[k], new Bpl.UnresolvedTypeIdentifier(Token.NoToken, "TName")));
+ incarnationZidList.Add(j);
+ if (errModel.partitionToValue[errModel.identifierToPartition[pti[k]]] != null) {
+ numberOfNonNullValueIncarnations++;
+ }
+ }
+ }
+ }
+ }
+ // only one such variable found, associate it with v
+ if (quantVarIncarnationList.Count == 1) {
+ incarnationMap[v] = quantVarIncarnationList[0];
+ } else if (quantVarIncarnationList.Count > 1 && numberOfNonNullValueIncarnations == 1) {
+ // if there are multiple candidate incarnations and exactly one of them has a value
+ // we can pick that one; otherwise it is not clear how to pick one out of multiple
+ // incarnations without a value or out of multiple incarnations with a value associated
+ for (int n = 0; n < incarnationZidList.Count; n++) {
+ if (errModel.partitionToValue[incarnationZidList[n]] != null) {
+ // quantVarIncarnationList and incarnationZidList are indexed in lockstep, so if
+ // for the associated zid the partitionToValue map is non-null then that is the one
+ // thus distinguished incarnation we want to put into the incarnationMap
+ incarnationMap[v] = quantVarIncarnationList[n];
+ break;
+ }
+ }
+ }
+ }
+ }
+ // generate the value of the body but do not return that outside
+ GetValuesFromModel(q.Body, incarnationMap, errModel, exprToPrintableValue);
+ // the quantifier cannot contribute any one value to the rest of the
+ // expression, thus just return -1
+ return -1;
+ }
+ else if (expr is Bpl.ExtractExpr) {
+ Bpl.ExtractExpr ex = (Bpl.ExtractExpr) expr;
+ Bpl.Expr e0 = ex.Bitvector;
+ Bpl.Expr e1 = new LiteralExpr(Token.NoToken, BigNum.FromInt(ex.Start));
+ Bpl.Expr e2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(ex.End));
+ string functionName = "$bv_extract";
+ List<int> zargs = new List<int>();
+ bool undefined = false;
+
+ int zid = -1;
+ zid = GetValuesFromModel(e0, incarnationMap, errModel, exprToPrintableValue);
+ if (zid == -1) {
+ undefined = true;
+ }
+ zargs.Add(zid);
+
+ zid = -1;
+ zid = GetValuesFromModel(e1, incarnationMap, errModel, exprToPrintableValue);
+ if (zid == -1) {
+ undefined = true;
+ }
+ zargs.Add(zid);
+
+ zid = -1;
+ zid = GetValuesFromModel(e2, incarnationMap, errModel, exprToPrintableValue);
+ if (zid == -1) {
+ undefined = true;
+ }
+ zargs.Add(zid);
+
+ //same as NAryExpr:
+ int id = TreatFunction(functionName, zargs, undefined, errModel);
+ if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {
+ exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));
+ }
+ return id;
+ }
+ else if (expr is Bpl.BvConcatExpr) {
+ // see comment above
+ Bpl.BvConcatExpr bvc = (Bpl.BvConcatExpr) expr;
+ string functionName = "$bv_concat";
+ List<int> zargs = new List<int>();
+ bool undefined = false;
+
+ int zid = -1;
+ zid = GetValuesFromModel(bvc.E0, incarnationMap, errModel, exprToPrintableValue);
+ if (zid == -1) {
+ undefined = true;
+ }
+ zargs.Add(zid);
+
+ zid = -1;
+ zid = GetValuesFromModel(bvc.E0, incarnationMap, errModel, exprToPrintableValue);
+ if (zid == -1) {
+ undefined = true;
+ }
+ zargs.Add(zid);
+
+ //same as NAryExpr:
+ int id = TreatFunction(functionName, zargs, undefined, errModel);
+ if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {
+ exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));
+ }
+ return id;
+ }
+ else {
+ assert false; // unexpected Bpl.Expr
+ }
+ return -1;
+ }
+
+ static Counterexample! AssertCmdToCounterexample (AssertCmd! cmd, TransferCmd! transferCmd, BlockSeq! trace, ErrorModel errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap) {
+ List<string!>! relatedInformation = new List<string!>();
+ if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) {
+ if (cmd.OrigExpr != null && cmd.IncarnationMap != null && errModel != null) {
+
+ // get all possible information first
+ Dictionary<Expr!, object> exprToPrintableValue = new Dictionary<Expr!, object>();
+ GetValuesFromModel(cmd.OrigExpr, cmd.IncarnationMap, errModel, exprToPrintableValue);
+ // then apply the strategies
+ ApplyEnhancedErrorPrintingStrategy(cmd.OrigExpr, cmd.IncarnationMap, cmd.ErrorDataEnhanced, errModel, exprToPrintableValue, relatedInformation, true, incarnationOriginMap);
+ }
+ }
+
+ // See if it is a special assert inserted in translation
+ if (cmd is AssertRequiresCmd)
+ {
+ AssertRequiresCmd! assertCmd = (AssertRequiresCmd)cmd;
+ CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires);
+ cc.relatedInformation = relatedInformation;
+ return cc;
+ }
+ else if (cmd is AssertEnsuresCmd)
+ {
+ AssertEnsuresCmd! assertCmd = (AssertEnsuresCmd)cmd;
+ ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures);
+ rc.relatedInformation = relatedInformation;
+ return rc;
+ }
+ else
+ {
+ AssertCounterexample ac = new AssertCounterexample(trace, (AssertCmd)cmd);
+ ac.relatedInformation = relatedInformation;
+ return ac;
+ }
+ }
+
+// static void EmitImpl(Implementation! impl, bool printDesugarings) {
+// 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>", Console.Out, false), 0);
+// CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;
+// CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+// }
+
+ static VCExpr! LetVC(Block! startBlock,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ ProverContext! proverCtxt)
+ {
+ Hashtable/*<Block, LetVariable!>*/! blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
+ List<VCExprLetBinding!>! bindings = new List<VCExprLetBinding!>();
+ VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt);
+ return proverCtxt.ExprGen.Let(bindings, startCorrect);
+ }
+
+ static VCExpr! LetVC(Block! block,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ Hashtable/*<Block, VCExprVar!>*/! blockVariables,
+ List<VCExprLetBinding!>! bindings,
+ ProverContext! proverCtxt)
+ {
+ VCExpressionGenerator! gen = proverCtxt.ExprGen;
+ VCExprVar v = (VCExprVar)blockVariables[block];
+ if (v == null) {
+ /*
+ * For block A (= block), generate:
+ * LET_binding A_correct = wp(A_body, (/\ S \in Successors(A) :: S_correct))
+ * with the side effect of adding the let bindings to "bindings" for any
+ * successor not yet visited.
+ */
+ VCExpr SuccCorrect;
+ GotoCmd gotocmd = block.TransferCmd as GotoCmd;
+ if (gotocmd == null) {
+ SuccCorrect = VCExpressionGenerator.True;
+ } else {
+ assert gotocmd.labelTargets != null;
+ List<VCExpr!> SuccCorrectVars = new List<VCExpr!>(gotocmd.labelTargets.Length);
+ foreach (Block! successor in gotocmd.labelTargets) {
+ VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt);
+ SuccCorrectVars.Add(s);
+ }
+ SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);
+ }
+
+ VCContext context = new VCContext(label2absy, proverCtxt);
+ VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+
+ v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
+ bindings.Add(gen.LetBinding(v, vc));
+ blockVariables.Add(block, v);
+ }
+ return v;
+ }
+
+ static VCExpr! DagVC(Block! block,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ Hashtable/*<Block, VCExpr!>*/! blockEquations,
+ ProverContext! proverCtxt)
+ {
+ VCExpressionGenerator! gen = proverCtxt.ExprGen;
+ VCExpr vc = (VCExpr)blockEquations[block];
+ if (vc != null) {
+ return vc;
+ }
+
+ /*
+ * For block A (= block), generate:
+ * wp(A_body, (/\ S \in Successors(A) :: DagVC(S)))
+ */
+ VCExpr SuccCorrect = null;
+ GotoCmd gotocmd = block.TransferCmd as GotoCmd;
+ if (gotocmd != null)
+ {
+ foreach (Block! successor in (!)gotocmd.labelTargets) {
+ VCExpr c = DagVC(successor, label2absy, blockEquations, proverCtxt);
+ SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c);
+ }
+ }
+ if (SuccCorrect == null) {
+ SuccCorrect = VCExpressionGenerator.True;
+ }
+
+ VCContext context = new VCContext(label2absy, proverCtxt);
+ vc = Wlp.Block(block, SuccCorrect, context);
+
+ // gen.MarkAsSharedFormula(vc); PR: don't know yet what to do with this guy
+
+ blockEquations.Add(block, vc);
+ return vc;
+ }
+
+ static VCExpr! FlatBlockVC(Implementation! impl,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ bool local, bool reach, bool doomed,
+ ProverContext! proverCtxt)
+ requires local ==> !reach; // "reach" must be false for local
+ {
+ VCExpressionGenerator! gen = proverCtxt.ExprGen;
+ Hashtable/* Block --> VCExprVar */ BlkCorrect = BlockVariableMap(impl.Blocks, "_correct", gen);
+ Hashtable/* Block --> VCExprVar */ BlkReached = reach ? BlockVariableMap(impl.Blocks, "_reached", gen) : null;
+
+ List<Block!> blocks = impl.Blocks;
+ // block sorting is now done on the VCExpr
+ // if (!local && ((!)CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) {
+ // blocks = SortBlocks(blocks);
+ // }
+
+ VCExpr proofObligation;
+ if (!local) {
+ proofObligation = (VCExprVar!)BlkCorrect[impl.Blocks[0]];
+ } else {
+ List<VCExpr!> conjuncts = new List<VCExpr!>(blocks.Count);
+ foreach (Block! b in blocks) {
+ VCExpr v = (VCExprVar!)BlkCorrect[b];
+ conjuncts.Add(v);
+ }
+ proofObligation = gen.NAry(VCExpressionGenerator.AndOp, conjuncts);
+ }
+
+ VCContext! context = new VCContext(label2absy, proverCtxt);
+
+ List<VCExprLetBinding!> programSemantics = new List<VCExprLetBinding!>(blocks.Count);
+ foreach (Block! b in blocks) {
+ /*
+ * In block mode,
+ * For a return block A, generate:
+ * A_correct <== wp(A_body, true) [post-condition has been translated into an assert]
+ * For all other blocks, generate:
+ * A_correct <== wp(A_body, (/\ S \in Successors(A) :: S_correct))
+ *
+ * In doomed mode, proceed as in block mode, except for a return block A, generate:
+ * A_correct <== wp(A_body, false) [post-condition has been translated into an assert]
+ *
+ * In block reach mode, the wp(A_body,...) in the equations above change to:
+ * A_reached ==> wp(A_body,...)
+ * and the conjunction above changes to:
+ * (/\ S \in Successors(A) :: S_correct \/ (\/ T \in Successors(A) && T != S :: T_reached))
+ *
+ * In local mode, generate:
+ * A_correct <== wp(A_body, true)
+ */
+ VCExpr! SuccCorrect;
+ if (local) {
+ SuccCorrect = VCExpressionGenerator.True;
+ } else {
+ SuccCorrect = SuccessorsCorrect(b, BlkCorrect, BlkReached, doomed, gen);
+ }
+
+ VCExpr wlp = Wlp.Block(b, SuccCorrect, context);
+ if (BlkReached != null) {
+ wlp = gen.Implies((VCExprVar!)BlkReached[b], wlp);
+ }
+
+ VCExprVar okVar = (VCExprVar!)BlkCorrect[b];
+ VCExprLetBinding binding = gen.LetBinding(okVar, wlp);
+ programSemantics.Add(binding);
+ }
+
+ return gen.Let(programSemantics, proofObligation);
+ }
+
+ private static Hashtable/* Block --> VCExprVar */! BlockVariableMap(List<Block!>! blocks, string! suffix,
+ Microsoft.Boogie.VCExpressionGenerator! gen)
+ {
+ Hashtable/* Block --> VCExprVar */ map = new Hashtable/* Block --> (Let)Variable */();
+ foreach (Block! b in blocks)
+ {
+ VCExprVar! v = gen.Variable(b.Label+suffix, Bpl.Type.Bool);
+ map.Add(b, v);
+ }
+ return map;
+ }
+
+ private static VCExpr! SuccessorsCorrect(
+ Block! b,
+ Hashtable/* Block --> VCExprVar */! BlkCorrect,
+ Hashtable/* Block --> VCExprVar */ BlkReached,
+ bool doomed,
+ Microsoft.Boogie.VCExpressionGenerator! gen)
+ {
+ VCExpr SuccCorrect = null;
+ GotoCmd gotocmd = b.TransferCmd as GotoCmd;
+ if (gotocmd != null)
+ {
+ foreach (Block! successor in (!)gotocmd.labelTargets)
+ {
+ // c := S_correct
+ VCExpr c = (VCExprVar!)BlkCorrect[successor];
+ if (BlkReached != null)
+ {
+ // c := S_correct \/ Sibling0_reached \/ Sibling1_reached \/ ...;
+ foreach (Block! successorSibling in gotocmd.labelTargets)
+ {
+ if (successorSibling != successor)
+ {
+ c = gen.Or(c, (VCExprVar!)BlkReached[successorSibling]);
+ }
+ }
+ }
+ SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c);
+ }
+ }
+ if (SuccCorrect == null) {
+ return VCExpressionGenerator.True;
+ } else if (doomed) {
+ return VCExpressionGenerator.False;
+ } else {
+ return SuccCorrect;
+ }
+ }
+
+ static VCExpr! NestedBlockVC(Implementation! impl,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ bool reach,
+ ProverContext! proverCtxt)
+ requires impl.Blocks.Count != 0;
+ {
+ VCExpressionGenerator! gen = proverCtxt.ExprGen;
+ Graph<Block>! g = GraphFromImpl(impl);
+
+ Hashtable/* Block --> VCExprVar */ BlkCorrect = BlockVariableMap(impl.Blocks, "_correct", gen);
+ Hashtable/* Block --> VCExprVar */ BlkReached = reach ? BlockVariableMap(impl.Blocks, "_reached", gen) : null;
+
+ Block! startBlock = (!) impl.Blocks[0];
+ VCExpr proofObligation = (VCExprVar!)BlkCorrect[startBlock];
+
+ VCContext! context = new VCContext(label2absy, proverCtxt);
+
+ Hashtable/*Block->int*/ totalOrder = new Hashtable/*Block->int*/();
+ {
+ List<Block!> blocks = impl.Blocks;
+ // block sorting is now done on the VCExpr
+ // if (((!)CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) {
+ // blocks = SortBlocks(blocks);
+ // }
+ int i = 0;
+ foreach (Block b in blocks) {
+ totalOrder[b] = i;
+ i++;
+ }
+ }
+
+ VCExprLetBinding programSemantics = NestedBlockEquation((!)impl.Blocks[0], BlkCorrect, BlkReached, totalOrder, context, g, gen);
+ List<VCExprLetBinding!> ps = new List<VCExprLetBinding!>(1);
+ ps.Add(programSemantics);
+
+ return gen.Let(ps, proofObligation);
+ }
+
+ private static VCExprLetBinding! NestedBlockEquation(Block! b,
+ Hashtable/*Block-->VCExprVar*/! BlkCorrect,
+ Hashtable/*Block-->VCExprVar*/ BlkReached,
+ Hashtable/*Block->int*/! totalOrder,
+ VCContext! context,
+ Graph<Block>! g,
+ Microsoft.Boogie.VCExpressionGenerator! gen)
+ {
+ /*
+ * For a block b, return:
+ * LET_BINDING b_correct = wp(b_body, X)
+ * where X is:
+ * LET (THOSE d \in DirectDominates(b) :: BlockEquation(d))
+ * IN (/\ s \in Successors(b) :: s_correct)
+ *
+ * When the VC-expression generator does not support LET expresions, this
+ * will eventually turn into:
+ * b_correct <== wp(b_body, X)
+ * where X is:
+ * (/\ s \in Successors(b) :: s_correct)
+ * <==
+ * (/\ d \in DirectDominatees(b) :: BlockEquation(d))
+ *
+ * In both cases above, if BlkReached is non-null, then the wp expression
+ * is instead:
+ * b_reached ==> wp(b_body, X)
+ */
+
+ VCExpr! SuccCorrect = SuccessorsCorrect(b, BlkCorrect, null, false, gen);
+
+ List<VCExprLetBinding!> bindings = new List<VCExprLetBinding!>();
+ foreach (Block! dominee in GetSortedBlocksImmediatelyDominatedBy(g, b, totalOrder))
+ {
+ VCExprLetBinding c = NestedBlockEquation(dominee, BlkCorrect, BlkReached, totalOrder, context, g, gen);
+ bindings.Add(c);
+ }
+
+ VCExpr X = gen.Let(bindings, SuccCorrect);
+ VCExpr wlp = Wlp.Block(b, X, context);
+ if (BlkReached != null) {
+ wlp = gen.Implies((VCExprVar!)BlkReached[b], wlp);
+ }
+ VCExprVar okVar = (VCExprVar!)BlkCorrect[b];
+ return gen.LetBinding(okVar, wlp);
+ }
+
+ /// <summary>
+ /// Returns a list of g.ImmediatelyDominatedBy(b), but in a sorted order, hoping to steer around
+ /// the nondeterminism problems we've been seeing by using just this call.
+ /// </summary>
+ static List<Block!>! GetSortedBlocksImmediatelyDominatedBy(Graph<Block>! g, Block! b, Hashtable/*Block->int*/! totalOrder) {
+ List<Block!> list = new List<Block!>();
+ foreach (Block! dominee in g.ImmediatelyDominatedBy(b)) {
+ list.Add(dominee);
+ }
+ list.Sort(new Comparison<Block!>(delegate (Block! x, Block! y) {return (int)(!)totalOrder[x] - (int)(!)totalOrder[y];} ));
+ return list;
+ }
+
+ static VCExpr! VCViaStructuredProgram
+ (Implementation! impl, Hashtable/*<int, Absy!>*/! label2absy,
+ ProverContext! proverCtxt)
+ {
+ #region Convert block structure back to a "regular expression"
+ RE! r = DAG2RE.Transform((!)impl.Blocks[0]);
+ #endregion
+
+ VCContext! ctxt = new VCContext(label2absy, proverCtxt);
+ #region Send wlp(program,true) to Simplify
+ return Wlp.RegExpr(r, VCExpressionGenerator.True, ctxt);
+ #endregion
+ }
+
+ /// <summary>
+ /// Remove the empty blocks reachable from the block.
+ /// It changes the visiting state of the blocks, so that if you want to visit again the blocks, you have to reset them...
+ /// </summary>
+ static BlockSeq! RemoveEmptyBlocks(Block! b)
+ {
+ assert b.TraversingStatus == Block.VisitState.ToVisit;
+ BlockSeq! retVal = removeEmptyBlocksWorker(b);
+
+ return retVal;
+ }
+
+ private static BlockSeq! removeEmptyBlocksWorker(Block! b)
+ {
+ BlockSeq bs = new BlockSeq();
+ GotoCmd gtc = b.TransferCmd as GotoCmd;
+
+ // b has no successors
+ if (gtc == null || gtc.labelTargets == null || gtc.labelTargets.Length == 0)
+ {
+ if (b.Cmds.Length != 0){ // only empty blocks are removed...
+ bs.Add(b);
+ }
+ return bs;
+ }
+ else if(b.TraversingStatus == Block.VisitState.ToVisit) // if b has some successors and we have not seen it so far...
+ {
+ b.TraversingStatus = Block.VisitState.BeingVisited;
+
+ // recursively call this method on each successor
+ // merge result into a *set* of blocks
+ Dictionary<Block,bool> mergedSuccessors = new Dictionary<Block,bool>();
+ foreach (Block! dest in gtc.labelTargets){
+ BlockSeq! ys = removeEmptyBlocksWorker(dest);
+ foreach (Block successor in ys){
+ if (!mergedSuccessors.ContainsKey(successor))
+ mergedSuccessors.Add(successor,true);
+ }
+ }
+ b.TraversingStatus = Block.VisitState.AlreadyVisited;
+
+ BlockSeq setOfSuccessors = new BlockSeq();
+ if (mergedSuccessors.Keys != null)
+ {
+ foreach (Block d in mergedSuccessors.Keys)
+ setOfSuccessors.Add(d);
+ }
+ if (b.Cmds.Length == 0)
+ return setOfSuccessors;
+ // otherwise, update the list of successors of b to be the blocks in setOfSuccessors
+ gtc.labelTargets = setOfSuccessors;
+ gtc.labelNames = new StringSeq();
+ foreach (Block! d in setOfSuccessors)
+ gtc.labelNames.Add(d.Label);
+ return new BlockSeq(b);
+ }
+ else // b has some successors, but we are already visiting it, or we have already visited it...
+ {
+ return new BlockSeq(b);
+ }
+ }
+
+ static Graph<Block>! GraphFromImpl(Implementation! impl) {
+ Graph<Block>! g = new Graph<Block>();
+ g.AddSource((!)impl.Blocks[0]); // there is always at least one node in the graph
+ foreach (Block! b in impl.Blocks)
+ {
+ GotoCmd gtc = b.TransferCmd as GotoCmd;
+ if (gtc != null)
+ {
+ foreach (Block! dest in (!)gtc.labelTargets)
+ {
+ g.AddEdge(b,dest);
+ }
+ }
+ }
+ return g;
+ }
+
+
+ static void DumpMap(Hashtable /*Variable->Expr*/! map) {
+ foreach (DictionaryEntry de in map) {
+ Variable! v = (Variable!)de.Key;
+ Expr! e = (Expr!)de.Value;
+ Console.Write(" ");
+ v.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);
+ Console.Write(" --> ");
+ e.Emit(new TokenTextWriter("<console>", Console.Out, false));
+ Console.WriteLine();
+ }
+ }
+ }
+}
diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc new file mode 100644 index 00000000..0706bf2f --- /dev/null +++ b/Source/VCGeneration/VCDoomed.ssc @@ -0,0 +1,817 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Graphing;
+using AI = Microsoft.AbstractInterpretationFramework;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace VC
+{
+ public class DCGen : ConditionGeneration
+ {
+
+ private Dictionary<Block, Variable!>! m_BlockReachabilityMap;
+
+
+ /// <summary>
+ /// Constructor. Initializes the theorem prover.
+ /// </summary>
+ public DCGen(Program! program, string/*?*/ logFilePath, bool appendLogFile)
+ {
+ base(program);
+ this.appendLogFile = appendLogFile;
+ this.logFilePath = logFilePath;
+ m_BlockReachabilityMap = new Dictionary<Block, Variable!>();
+ }
+
+ private class DummyErrorHandler : ProverInterface.ErrorHandler
+ {
+ public override void OnModel(IList<string!>! labels, ErrorModel errModel)
+ {}
+ public override void OnResourceExceeded(string! message)
+ {}
+ public override Absy! Label2Absy(string! label)
+ {
+ Absy! a = new Block();
+ return a;
+ }
+ }
+
+ /// <summary>
+ /// MSchaef: Todo: Write a good Comment
+ /// </summary>
+ public override Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)
+ throws UnexpectedProverOutputException;
+ {
+ // MSchaef: Just a Hack, errh is not used in this context, but required by the checker
+ DummyErrorHandler errh = new DummyErrorHandler();
+ callback.OnProgress("Whatever this stands for",0,0,0);
+ #region Transform the Program into loop-free passive form
+ variable2SequenceNumber = new Hashtable/*Variable -> int*/();
+ incarnationOriginMap = new Dictionary<Incarnation, Absy!>();
+ List<Block!>! cblocks = new List<Block!>();
+
+ impl.Blocks = DCProgramTransformer.Convert2Dag(impl, program, cblocks);
+ ComputePredecessors(impl.Blocks);
+
+ m_BlockReachabilityMap = new Dictionary<Block, Variable!>();
+ PassifyProgram(impl, program);
+ #endregion
+
+ Checker! checker = FindCheckerFor(impl, 1000);
+// Checker! checker = new Checker(this, program, logFilePath, false, impl, 1000);
+
+ Hashtable label2absy;
+ VCExpr! vc = GenerateEVC(impl, out label2absy, checker);
+
+ checker.PushVCExpr(vc);
+
+
+ foreach (Block! b in impl.Blocks)
+ {
+ #region Find out if one needs to check this one, or if the error is propagated (HACK)
+ if (!cblocks.Contains(b)) continue;
+
+ bool _needscheck = false;
+ foreach (Block! b_ in b.Predecessors)
+ {
+ GotoCmd gtc = b_.TransferCmd as GotoCmd;
+ if (gtc!=null && gtc.labelTargets!=null && gtc.labelTargets.Length>1)
+ {
+ _needscheck=true; break;
+ }
+ }
+ if (!_needscheck) continue;
+ #endregion
+
+ Variable v = null;
+ m_BlockReachabilityMap.TryGetValue(b, out v);
+ assert v!=null;
+
+ VCExpr! currentlabel = checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v);
+ checker.BeginCheck(b.Label, currentlabel, errh);
+ WaitHandle[] wh = new WaitHandle[1];
+ ProverInterface.Outcome o = ProverInterface.Outcome.Undetermined;
+
+ wh[0] = checker.ProverDone;
+ WaitHandle.WaitAny(wh);
+ try {
+ o = checker.ReadOutcome();
+ } catch (UnexpectedProverOutputException e)
+ {
+ Console.WriteLine(e.ToString());
+ }
+
+ switch (o)
+ {
+ case ProverInterface.Outcome.Valid:
+ {
+ Console.WriteLine("In Function {0}", impl.Name);
+ Console.WriteLine("\t Block {0} has a guaranteed error!", b.Label);
+ break;
+ }
+ case ProverInterface.Outcome.Invalid:
+ {
+ break;
+ }
+ default:
+ {
+ Console.WriteLine("I'm confused about Block {0}.", b.Label);
+ break;
+ }
+ }
+
+ }
+ checker.Close();
+ return Outcome.Correct;
+ }
+
+ protected Hashtable/*TransferCmd->ReturnCmd*/! PassifyImpl(Implementation! impl, Program! program)
+ {
+ return new Hashtable();
+ }
+
+
+ #region Loop Removal
+ /// <summary>
+ /// This class is accessed only via the static method Convert2Dag
+ /// It converts the program into a loopfree one by unrolling the loop threetimes and adding the appropriate havoc
+ /// statements. The first and the last unrolling represent the first and last iteration of the loop. The second
+ /// unrolling stands for any other iteration.
+ /// </summary>
+ private class DCProgramTransformer
+ {
+ public static List<Block!>! Convert2Dag(Implementation! impl, Program! program, List<Block!>! checkableBlocks)
+ {
+ Block! start = impl.Blocks[0];
+ Dictionary<Block,GraphNode!> gd = new Dictionary<Block,GraphNode!>();
+ Set/*Block*/! beingVisited = new Set/*Block*/();
+ GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);
+
+ DCProgramTransformer pt = new DCProgramTransformer(checkableBlocks);
+ pt.LoopUnrolling(gStart, new Dictionary<GraphNode, Block!>(), true, "");
+ pt.Blocks.Reverse();
+
+ return pt.Blocks;
+ }
+
+ List<Block!>! Blocks;
+
+ private List<Block!>! m_checkableBlocks;
+
+
+ DCProgramTransformer(List<Block!>! checkableBlocks)
+ {
+ Blocks = new List<Block!>();
+ m_checkableBlocks = checkableBlocks;
+ }
+
+
+ #region Loop Unrolling Methods
+ private Block! LoopUnrolling(GraphNode! node, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
+ {
+ Block newb;
+ if (visited.TryGetValue(node, out newb))
+ {
+ assert newb!=null;
+ return newb;
+ } else
+ {
+ if (node.IsCutPoint)
+ {
+ // compute the loop body and the blocks leaving the loop
+
+ List<GraphNode!>! loopNodes = new List<GraphNode!>();
+ GatherLoopBodyNodes(node, node, loopNodes);
+
+ List<GraphNode!>! exitNodes = GatherLoopExitNodes(loopNodes);
+
+ // Continue Unrolling after the current loop
+ Dictionary<GraphNode, Block!>! _visited = new Dictionary<GraphNode, Block!>();
+ foreach (GraphNode! g in exitNodes)
+ {
+ Block b = LoopUnrolling(g, visited, unrollable, prefix);
+ _visited.Add(g,b);
+ }
+ newb = UnrollCurrentLoop(node, _visited, loopNodes,unrollable, prefix);
+ visited.Add(node,newb);
+ } else
+ {
+ BlockSeq! newSuccs = new BlockSeq();
+ foreach(GraphNode! g in node.Succecessors)
+ {
+ newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
+ }
+ newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
+ assert newb!=null; assert newb.TransferCmd!=null;
+ if (newSuccs.Length == 0)
+ newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
+ else
+ newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
+
+ visited.Add(node, newb);
+ Blocks.Add(newb);
+ if (unrollable)
+ {
+ m_checkableBlocks.Add(newb);
+ }
+ }
+ }
+ assert newb!=null;
+ //newb.checkable = unrollable;
+ return newb;
+ }
+
+ private Block! UnrollCurrentLoop(GraphNode! cutPoint, Dictionary<GraphNode, Block!>! visited,
+ List<GraphNode!>! loopNodes, bool unrollable, String! prefix)
+ {
+ if (unrollable)
+ {
+ Dictionary<GraphNode, Block!>! visited1 = new Dictionary<GraphNode, Block!>(visited);
+ Dictionary<GraphNode, Block!>! visited2 = new Dictionary<GraphNode, Block!>(visited);
+ Dictionary<GraphNode, Block!>! visited3 = new Dictionary<GraphNode, Block!>(visited);
+
+ Block! loopend = ConstructLoopExitBlock(cutPoint, loopNodes, visited, prefix+"#Last");
+
+ Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last");
+ AddHavocCmd(last,loopNodes);
+
+
+ Block! arb = UnrollOnce(cutPoint, last,visited2,true, prefix+"#Arb");
+ AddHavocCmd(arb,loopNodes);
+
+
+ BlockSeq! succ = new BlockSeq();
+ succ.Add(last); succ.Add(arb);
+ assert arb.TransferCmd!=null;
+ Block! tmp = new Block(arb.tok, arb.Label + prefix+"#Dummy" , new CmdSeq(), new GotoCmd(arb.TransferCmd.tok, succ));
+ Blocks.Add(tmp);
+ m_checkableBlocks.Add(tmp);
+
+ Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First");
+
+ return first;
+
+ } else
+ {
+ Dictionary<GraphNode, Block!>! visited_ = new Dictionary<GraphNode, Block!>(visited);
+ Block! loopend = AbstractIteration(cutPoint, prefix+"#UR");
+ Block! ret = UnrollOnce(cutPoint, loopend,visited_,false, prefix);
+ AddHavocCmd(ret, loopNodes);
+ return ret;
+ }
+ }
+
+ private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
+ {
+ visited.Add(node, nextIter);
+ Block newb;
+ BlockSeq! newSuccs = new BlockSeq();
+ foreach(GraphNode! g in node.Succecessors)
+ {
+ newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
+ }
+ newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
+ assert newb!=null; assert newb.TransferCmd!=null;
+ if (newSuccs.Length == 0)
+ newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
+ else
+ newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
+
+ Blocks.Add(newb);
+ if (unrollable) m_checkableBlocks.Add(newb);
+ return newb;
+ }
+
+ private Block! AbstractIteration(GraphNode! node, String! prefix)
+ {
+ CmdSeq body = new CmdSeq();
+ foreach (Cmd! c in node.Body)
+ {
+ if (c is PredicateCmd || c is CommentCmd)
+ body.Add(c);
+ else
+ break;
+ }
+ body.Add(new AssumeCmd(node.Block.tok, Expr.False) );
+ TransferCmd! tcmd = new ReturnCmd(node.Block.tok);
+ Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd);
+ Blocks.Add(b);
+ return b;
+ }
+
+ private Block! ConstructLoopExitBlock(GraphNode! cutPoint, List<GraphNode!>! loopNodes,
+ Dictionary<GraphNode, Block!>! visited, String! prefix)
+ {
+ BlockSeq! newSucc = new BlockSeq();
+ Block! orig = cutPoint.Block;
+
+ // detect the block after the loop
+ // FixMe: What happens when using break commands?
+ foreach (GraphNode! g in cutPoint.Succecessors)
+ {
+ if (!loopNodes.Contains(g))
+ {
+ Block b;
+ if (visited.TryGetValue(g,out b) )
+ newSucc.Add(b);
+ }
+ }
+ TransferCmd tcmd;
+ assert orig.TransferCmd!=null;
+ if (newSucc.Length==0)
+ tcmd = new ReturnCmd(orig.TransferCmd.tok);
+ else
+ tcmd = new GotoCmd(orig.TransferCmd.tok, newSucc);
+ // FixMe: Genertate IToken for counterexample creation
+ Block! newb = new Block(orig.tok, orig.Label+prefix+"#Leave", orig.Cmds, tcmd);
+ Blocks.Add(newb);
+ m_checkableBlocks.Add(newb);
+ return newb;
+ }
+
+
+ private void GatherLoopBodyNodes(GraphNode! current, GraphNode! cutPoint, List<GraphNode!>! loopNodes)
+ {
+ loopNodes.Add(current);
+ if (false) System.Diagnostics.Debugger.Break();
+ foreach (GraphNode! g in current.Predecessors)
+ {
+ if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g) ) continue;
+ GatherLoopBodyNodes(g, cutPoint, loopNodes);
+ }
+ }
+
+ private List<GraphNode!>! GatherLoopExitNodes(List<GraphNode!>! loopNodes)
+ {
+ List<GraphNode!>! exitnodes = new List<GraphNode!>();
+
+ foreach (GraphNode! g in loopNodes)
+ {
+ foreach (GraphNode! s in g.Succecessors)
+ {
+ if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ ) exitnodes.Add(s);
+ }
+ }
+ return exitnodes;
+ }
+
+ private void AddHavocCmd(Block! b, List<GraphNode!>! loopNodes)
+ {
+ List<Block!>! loopBlocks = new List<Block!>();
+ foreach (GraphNode! g in loopNodes) loopBlocks.Add(g.Block);
+ HavocCmd! hcmd = HavocLoopTargets(loopBlocks,b.tok);
+ CmdSeq! body = new CmdSeq();
+ body.Add(hcmd);
+ body.AddRange(b.Cmds);
+ b.Cmds = body;
+ }
+
+ private HavocCmd! HavocLoopTargets(List<Block!>! bl, IToken! tok)
+ {
+ VariableSeq varsToHavoc = new VariableSeq();
+ foreach ( Block! b in bl )
+ {
+ foreach ( Cmd! c in b.Cmds )
+ {
+ c.AddAssignedVariables(varsToHavoc);
+ }
+ }
+ IdentifierExprSeq havocExprs = new IdentifierExprSeq();
+ foreach ( Variable! v in varsToHavoc )
+ {
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ if(!havocExprs.Has(ie))
+ havocExprs.Add(ie);
+ }
+ // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct
+ // the source location for this later on
+ return new HavocCmd(tok,havocExprs);
+ }
+
+ #endregion
+
+
+ #region GraphNode
+ private class GraphNode
+ {
+ public readonly Block! Block;
+ public readonly CmdSeq! Body;
+ public bool IsCutPoint; // is set during ComputeGraphInfo
+ [Rep] public readonly List<GraphNode!>! Predecessors = new List<GraphNode!>();
+ [Rep] public readonly List<GraphNode!>! Succecessors = new List<GraphNode!>();
+ public GraphNode firstPredecessor;
+
+ GraphNode(Block! b, CmdSeq! body)
+ {
+ Block = b; Body = body;
+ IsCutPoint = false;
+ }
+
+ static CmdSeq! GetOptimizedBody(CmdSeq! cmds)
+ {
+ int n = 0;
+ foreach (Cmd c in cmds)
+ {
+ n++;
+ PredicateCmd pc = c as PredicateCmd;
+ if (pc != null && pc.Expr is LiteralExpr && ((LiteralExpr)pc.Expr).IsFalse)
+ {
+ // return a sequence consisting of the commands seen so far
+ Cmd[] s = new Cmd[n];
+ for (int i = 0; i < n; i++)
+ {
+ s[i] = cmds[i];
+ }
+ return new CmdSeq(s);
+ }
+ }
+ return cmds;
+ }
+
+ public static GraphNode! ComputeGraphInfo(GraphNode from, Block! b, Dictionary<Block,GraphNode!>! gd, Set /*Block*/! beingVisited)
+ {
+ GraphNode g;
+ if (gd.TryGetValue(b, out g))
+ {
+ assume from != null;
+ assert g != null;
+ g.Predecessors.Add(from);
+ if (g.firstPredecessor==null)
+ g.firstPredecessor = from;
+
+ if (beingVisited.Contains(b))
+ g.IsCutPoint = true; // it's a cut point
+ } else
+ {
+ CmdSeq body = GetOptimizedBody(b.Cmds);
+ g = new GraphNode(b, body);
+ gd.Add(b, g);
+ if (from != null)
+ {
+ g.Predecessors.Add(from);
+ if (from==null)
+ g.firstPredecessor = g;
+
+ if (g.firstPredecessor==null)
+ g.firstPredecessor = from;
+
+ }
+ if (body != b.Cmds)
+ {
+ // the body was optimized -- there is no way through this block
+ } else
+ {
+ beingVisited.Add(b);
+ GotoCmd gcmd = b.TransferCmd as GotoCmd;
+ if (gcmd != null)
+ {
+ assume gcmd.labelTargets != null;
+ foreach (Block! succ in gcmd.labelTargets)
+ {
+ g.Succecessors.Add( ComputeGraphInfo(g, succ, gd, beingVisited) );
+ }
+ }
+ beingVisited.Remove(b);
+ }
+ }
+ return g;
+ }
+ }
+ #endregion
+
+ }
+ #endregion
+
+ #region Program Passification
+
+ private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl,
+ Program! program)
+ {
+ Hashtable gotoCmdOrigins = new Hashtable();
+ Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
+ AddBlocksBetween(impl);
+ GenerateReachabilityPredicates(impl, exitBlock);
+
+ current_impl = impl;
+ Convert2PassiveCmd(impl);
+ impl = current_impl;
+ return new Hashtable();
+ }
+
+ /// <summary>
+ /// Add additional variable to allow checking as described in the paper
+ /// "It's doomed; we can prove it"
+ /// </summary>
+ private void GenerateReachabilityPredicates(Implementation! impl, Block! exitBlock)
+ {
+ ExprSeq! es = new ExprSeq();
+ Cmd eblockcond = null;
+
+ foreach (Block! b in impl.Blocks)
+ {
+ //if (b.Predecessors.Length==0) continue;
+ //if (b.Cmds.Length == 0 ) continue;
+
+ Variable v_ = new LocalVariable(Token.NoToken,
+ new TypedIdent(b.tok, b.Label+"__ivebeenthere",new BasicType(SimpleType.Bool) ) );
+
+ impl.LocVars.Add(v_);
+
+ m_BlockReachabilityMap[b] = v_;
+
+ IdentifierExpr! lhs = new IdentifierExpr(b.tok, v_);
+
+ es.Add( new IdentifierExpr(b.tok, v_) );
+
+ List<AssignLhs!>! lhsl = new List<AssignLhs!>();
+ lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs) );
+ List<Expr!>! rhsl = new List<Expr!>();
+ rhsl.Add(Expr.True);
+
+ if (b!=exitBlock)
+ {
+ CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));
+ cs.AddRange(b.Cmds);
+ b.Cmds = cs;
+ } else
+ {
+ eblockcond = new AssignCmd(Token.NoToken, lhsl, rhsl);
+ }
+
+ //checkBlocks.Add(new CheckableBlock(v_,b));
+ }
+ if (es.Length==0) return;
+
+ Expr aexp = null;
+
+ if (es.Length==1)
+ {
+ aexp = es[0];
+ } else if (es.Length==2)
+ {
+ aexp = Expr.Binary(Token.NoToken,
+ BinaryOperator.Opcode.And,
+ (!)es[0],
+ (!)es[1]);
+ } else
+ {
+ aexp = Expr.True;
+ foreach (Expr e_ in es)
+ {
+ aexp = Expr.Binary(Token.NoToken,
+ BinaryOperator.Opcode.And,
+ (!)e_, aexp);
+ }
+ }
+ assert (aexp!=null);
+ assert (eblockcond!=null);
+
+ AssumeCmd ac = new AssumeCmd(Token.NoToken, aexp);
+
+ assert(exitBlock!=null);
+
+ CmdSeq cseq = new CmdSeq(eblockcond);
+ cseq.AddRange(exitBlock.Cmds);
+ cseq.Add(ac);
+
+ exitBlock.Cmds = cseq;
+ }
+
+ #endregion
+
+ #region Error Verification Condition Generation
+
+ VCExpr! GenerateEVC(Implementation! impl, out Hashtable label2absy, Checker! ch)
+ {
+ TypecheckingContext tc = new TypecheckingContext(null);
+ impl.Typecheck(tc);
+ label2absy = new Hashtable/*<int, Absy!>*/();
+ VCExpr! vc;
+ switch (CommandLineOptions.Clo.vcVariety) {
+ case CommandLineOptions.VCVariety.Structured:
+ //vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context);
+ //break;
+ Console.WriteLine("Not Implemented: This should be unreachable");
+ assert false;
+ case CommandLineOptions.VCVariety.Block:
+ //vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context);
+ Console.WriteLine("Not Implemented: This should be unreachable");
+ assert false;
+ break;
+ case CommandLineOptions.VCVariety.BlockReach:
+ //vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context);
+ Console.WriteLine("Not Implemented: This should be unreachable");
+ assert false;
+ break;
+ case CommandLineOptions.VCVariety.Local:
+ //vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context);
+ Console.WriteLine("Not Implemented: This should be unreachable");
+ assert false;
+ break;
+ case CommandLineOptions.VCVariety.BlockNested:
+// vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context);
+// break;
+ Console.WriteLine("Not Implemented: This should be unreachable");
+ assert false;
+ case CommandLineOptions.VCVariety.BlockNestedReach:
+// vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context);
+// break;
+ Console.WriteLine("Not Implemented: This should be unreachable");
+ assert false;
+ case CommandLineOptions.VCVariety.Dag:
+ if (((!)CommandLineOptions.Clo.TheProverFactory).SupportsDags)
+ {
+// vc = DagVC((!)impl.Blocks[0], label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context);
+ Console.WriteLine("Not Implemented: This should be unreachable");
+ assert false;
+ } else {
+ vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);
+ }
+ break;
+ case CommandLineOptions.VCVariety.Doomed:
+ //vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context);
+ vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);
+ break;
+ default:
+ assert false; // unexpected enumeration value
+ }
+ return vc;
+ }
+
+ private Hashtable/* Block --> VCExprVar */! BlockVariableMap(List<Block!>! blocks, string! suffix,
+ Microsoft.Boogie.VCExpressionGenerator! gen)
+ {
+ Hashtable/* Block --> VCExprVar */ map = new Hashtable/* Block --> (Let)Variable */();
+ foreach (Block! b in blocks)
+ {
+ VCExprVar! v = gen.Variable(b.Label+suffix, Microsoft.Boogie.Type.Bool);
+ map.Add(b, v);
+ }
+ return map;
+ }
+
+ VCExpr! FlatBlockVC(Implementation! impl,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ bool local, bool reach, bool doomed,
+ ProverContext! proverCtxt)
+ requires local ==> !reach; // "reach" must be false for local
+ {
+ VCExpressionGenerator! gen = proverCtxt.ExprGen;
+ Hashtable/* Block --> VCExprVar */ BlkCorrect = BlockVariableMap(impl.Blocks, "_correct", gen);
+ Hashtable/* Block --> VCExprVar */ BlkReached = reach ? BlockVariableMap(impl.Blocks, "_reached", gen) : null;
+
+ List<Block!> blocks = impl.Blocks;
+ // block sorting is now done on the VCExpr
+ // if (!local && ((!)CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) {
+ // blocks = SortBlocks(blocks);
+ // }
+
+ VCExpr proofObligation;
+ if (!local) {
+ proofObligation = (VCExprVar!)BlkCorrect[impl.Blocks[0]];
+ } else {
+ List<VCExpr!> conjuncts = new List<VCExpr!>(blocks.Count);
+ foreach (Block! b in blocks) {
+ VCExpr v = (VCExprVar!)BlkCorrect[b];
+ conjuncts.Add(v);
+ }
+ proofObligation = gen.NAry(VCExpressionGenerator.AndOp, conjuncts);
+ }
+
+ VCContext! context = new VCContext(label2absy, proverCtxt);
+// m_Context = context;
+
+ List<VCExprLetBinding!> programSemantics = new List<VCExprLetBinding!>(blocks.Count);
+ foreach (Block! b in blocks) {
+ VCExpr! SuccCorrect;
+ if (local) {
+ SuccCorrect = VCExpressionGenerator.False; // Martin: Changed from true to false
+ } else {
+ SuccCorrect = SuccessorsCorrect(b, BlkCorrect, BlkReached, doomed, gen);
+ }
+
+ VCExpr wlp = Wlp.Block(b, SuccCorrect, context);
+ if (BlkReached != null) {
+ //wlp = gen.Implies((VCExprVar!)BlkReached[b], wlp);
+ }
+
+ VCExprVar okVar = (VCExprVar!)BlkCorrect[b];
+ VCExprLetBinding binding = gen.LetBinding(okVar, wlp);
+ programSemantics.Add(binding);
+ }
+
+ return gen.Let(programSemantics, proofObligation);
+ }
+
+ static VCExpr! SuccessorsCorrect(
+ Block! b,
+ Hashtable/* Block --> VCExprVar */! BlkCorrect,
+ Hashtable/* Block --> VCExprVar */ BlkReached,
+ bool doomed,
+ Microsoft.Boogie.VCExpressionGenerator! gen)
+ {
+ VCExpr SuccCorrect = null;
+ GotoCmd gotocmd = b.TransferCmd as GotoCmd;
+ if (gotocmd != null)
+ {
+ foreach (Block! successor in (!)gotocmd.labelTargets)
+ {
+ // c := S_correct
+ VCExpr c = (VCExprVar!)BlkCorrect[successor];
+
+ if (BlkReached != null)
+ {
+ // c := S_correct \/ Sibling0_reached \/ Sibling1_reached \/ ...;
+ foreach (Block! successorSibling in gotocmd.labelTargets)
+ {
+ if (successorSibling != successor)
+ {
+ //don't know what this is good for
+ // c = gen.Or(c, (VCExprVar!)BlkReached[successorSibling]);
+ }
+ }
+ }
+ SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c);
+ }
+ }
+ if (SuccCorrect == null) {
+ //return VCExpressionGenerator.True;
+ return VCExpressionGenerator.False;
+ } else if (doomed) {
+ return VCExpressionGenerator.False;
+ } else {
+ return SuccCorrect;
+ }
+ }
+
+
+
+ VCExpr! LetVC(Block! startBlock,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ ProverContext! proverCtxt)
+ {
+ Hashtable/*<Block, LetVariable!>*/! blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
+ List<VCExprLetBinding!>! bindings = new List<VCExprLetBinding!>();
+ VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt);
+ //return proverCtxt.ExprGen.Let(bindings, startCorrect);
+ return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) );
+ }
+
+ VCExpr! LetVC(Block! block,
+ Hashtable/*<int, Absy!>*/! label2absy,
+ Hashtable/*<Block, VCExprVar!>*/! blockVariables,
+ List<VCExprLetBinding!>! bindings,
+ ProverContext! proverCtxt)
+ {
+ VCExpressionGenerator! gen = proverCtxt.ExprGen;
+ VCExprVar v = (VCExprVar)blockVariables[block];
+ if (v == null) {
+ /*
+ * For block A (= block), generate:
+ * LET_binding A_correct = wp(A_body, (/\ S \in Successors(A) :: S_correct))
+ * with the side effect of adding the let bindings to "bindings" for any
+ * successor not yet visited.
+ */
+ VCExpr SuccCorrect;
+ GotoCmd gotocmd = block.TransferCmd as GotoCmd;
+ if (gotocmd == null) {
+ SuccCorrect = VCExpressionGenerator.False; // FixMe: changed from true to false
+ } else {
+ assert gotocmd.labelTargets != null;
+ List<VCExpr!> SuccCorrectVars = new List<VCExpr!>(gotocmd.labelTargets.Length);
+ foreach (Block! successor in gotocmd.labelTargets) {
+ VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt);
+ SuccCorrectVars.Add(s);
+ }
+ SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);
+ }
+
+ VCContext context = new VCContext(label2absy, proverCtxt);
+// m_Context = context;
+ VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+
+ v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);
+ bindings.Add(gen.LetBinding(v, vc));
+ blockVariables.Add(block, v);
+ }
+ return v;
+ }
+
+
+
+ #endregion
+
+ }
+}
\ No newline at end of file diff --git a/Source/VCGeneration/VCGeneration.sscproj b/Source/VCGeneration/VCGeneration.sscproj new file mode 100644 index 00000000..70f4055d --- /dev/null +++ b/Source/VCGeneration/VCGeneration.sscproj @@ -0,0 +1,142 @@ +<?xml version="1.0" encoding="utf-8"?>
+<VisualStudioProject>
+ <XEN ProjectType="Local"
+ SchemaVersion="1.0"
+ Name="VCGeneration"
+ ProjectGuid="f65666de-fb56-457c-8782-09be243450fc"
+ >
+ <Build>
+ <Settings ApplicationIcon=""
+ AssemblyName="VCGeneration"
+ OutputType="Library"
+ RootNamespace="VCGeneration"
+ StartupObject=""
+ StandardLibraryLocation=""
+ TargetPlatform="v2"
+ TargetPlatformLocation=""
+ >
+ <Config Name="Debug"
+ AllowUnsafeBlocks="False"
+ BaseAddress="285212672"
+ CheckForOverflowUnderflow="False"
+ ConfigurationOverrideFile=""
+ DefineConstants="DEBUG;TRACE"
+ DocumentationFile=""
+ DebugSymbols="True"
+ FileAlignment="4096"
+ IncrementalBuild="True"
+ Optimize="False"
+ OutputPath="bin\debug"
+ RegisterForComInterop="False"
+ RemoveIntegerChecks="false"
+ TreatWarningsAsErrors="False"
+ WarningLevel="4"
+ ReferenceTypesAreNonNullByDefault="False"
+ RunProgramVerifier="False"
+ RunProgramVerifierWhileEditing="False"
+ ProgramVerifierCommandLineOptions=""
+ AllowPointersToManagedStructures="False"
+ CheckContractAdmissibility="True"
+ CheckPurity="False"
+ />
+ <Config Name="Release"
+ AllowUnsafeBlocks="false"
+ BaseAddress="285212672"
+ CheckForOverflowUnderflow="false"
+ ConfigurationOverrideFile=""
+ DefineConstants="TRACE"
+ DocumentationFile=""
+ DebugSymbols="false"
+ FileAlignment="4096"
+ IncrementalBuild="false"
+ Optimize="true"
+ OutputPath="bin\release"
+ RegisterForComInterop="false"
+ RemoveIntegerChecks="false"
+ TreatWarningsAsErrors="false"
+ WarningLevel="4"
+ />
+ </Settings>
+ <References>
+ <Reference Name="System"
+ AssemblyName="System"
+ Private="false"
+ />
+ <Reference Name="System.Data"
+ AssemblyName="System.Data"
+ Private="false"
+ />
+ <Reference Name="System.Xml"
+ AssemblyName="System.Xml"
+ Private="false"
+ />
+ <Reference Name="Core"
+ Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
+ Private="true"
+ />
+ <Reference Name="AIFramework"
+ Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
+ Private="true"
+ />
+ <Reference Name="Graph"
+ Project="{4C28FB90-630E-4B55-A937-11A011B79765}"
+ Private="true"
+ />
+ <Reference Name="Mscorlib.Contracts"
+ AssemblyName="Mscorlib.Contracts"
+ Private="false"
+ HintPath="../../Binaries/Mscorlib.Contracts.dll"
+ />
+ <Reference Name="System.Contracts"
+ AssemblyName="System.Contracts"
+ Private="false"
+ HintPath="../../Binaries/System.Contracts.dll"
+ />
+ <Reference Name="Basetypes"
+ Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
+ Private="true"
+ />
+ <Reference Name="VCExpr"
+ Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"
+ Private="true"
+ />
+ </References>
+ </Build>
+ <Files>
+ <Include>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Check.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="VC.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Wlp.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="..\version.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Context.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="OrderingAxioms.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="ConditionGeneration.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="VCDoomed.ssc"
+ />
+ </Include>
+ </Files>
+ </XEN>
+</VisualStudioProject>
\ No newline at end of file diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc new file mode 100644 index 00000000..d7692245 --- /dev/null +++ b/Source/VCGeneration/Wlp.ssc @@ -0,0 +1,131 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Contracts;
+
+namespace VC {
+ public class VCContext
+ {
+ [Rep] public readonly Hashtable/*<int, Absy!>*/! Label2absy;
+ [Rep] public readonly ProverContext! Ctxt;
+
+ public VCContext(Hashtable/*<int, Absy!>*/! label2absy, ProverContext! ctxt)
+ {
+ this.Label2absy = label2absy;
+ this.Ctxt = ctxt;
+ // base();
+ }
+ }
+
+ #region A class to compute wlp of a passive command program
+
+ public class Wlp
+ {
+ public static VCExpr! Block(Block! b, VCExpr! N, VCContext! ctxt)
+ modifies ctxt.*;
+ {
+ VCExpressionGenerator! gen = ctxt.Ctxt.ExprGen;
+ VCExpr! res = N;
+
+ for (int i = b.Cmds.Length; --i>=0; )
+ {
+ res = Cmd((!) b.Cmds[i], res, ctxt);
+ }
+
+ int id = b.UniqueId;
+ expose (ctxt) {
+ ctxt.Label2absy[id] = b;
+ return gen.Implies(gen.LabelPos((!)id.ToString(), VCExpressionGenerator.True), res);
+ }
+ }
+
+ /// <summary>
+ /// Computes the wlp for an assert or assume command "cmd".
+ /// </summary>
+ public static VCExpr! Cmd(Cmd! cmd, VCExpr! N, VCContext! ctxt)
+ {
+ VCExpressionGenerator! gen = ctxt.Ctxt.ExprGen;
+ if (cmd is AssertCmd) {
+ AssertCmd ac = (AssertCmd)cmd;
+ VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ return gen.Implies(C, N);
+ } else {
+ int id = ac.UniqueId;
+ ctxt.Label2absy[id] = ac;
+ switch (CommandLineOptions.Clo.UseSubsumption) {
+ case CommandLineOptions.SubsumptionOption.Never:
+ break;
+ case CommandLineOptions.SubsumptionOption.Always:
+ N = gen.Implies(C, N);
+ break;
+ case CommandLineOptions.SubsumptionOption.NotForQuantifiers:
+ if (!(C is VCExprQuantifier)) {
+ N = gen.Implies(C, N);
+ }
+ break;
+ default:
+ assert false; // unexpected case
+ }
+// (MSchaef) Hack: This line might be useless, but at least it is not harmfull
+// need to test it
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) return gen.Implies(C, N);
+
+ return gen.And(gen.LabelNeg((!)id.ToString(), C), N);
+ }
+
+ } else if (cmd is AssumeCmd) {
+ AssumeCmd ac = (AssumeCmd)cmd;
+ return gen.Implies(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+
+ } else {
+ assert false; // unexpected command
+ }
+ }
+
+ public static VCExpr! RegExpr(RE! r, VCExpr! N, VCContext! ctxt)
+ {
+ if ( r is AtomicRE )
+ {
+ AtomicRE ar = (AtomicRE) r;
+ return Block(ar.b, N, ctxt);
+ }
+ else if ( r is Sequential )
+ {
+ Sequential s = (Sequential) r;
+ return RegExpr(s.first, RegExpr(s.second, N, ctxt), ctxt);
+ }
+ else if ( r is Choice )
+ {
+ Choice ch = (Choice) r;
+ VCExpr! res;
+ if (ch.rs == null || ch.rs.Length==0)
+ {
+ res = N;
+ }
+ else
+ {
+ VCExpr currentWLP = RegExpr((!)ch.rs[0], N, ctxt);
+ for (int i = 1, n = ch.rs.Length; i < n; i++)
+ {
+ currentWLP = ctxt.Ctxt.ExprGen.And(currentWLP, RegExpr((!)ch.rs[i], N, ctxt));
+ }
+ res = currentWLP;
+ }
+ return res;
+ }
+ else
+ {
+ assert false; // unexpected RE subtype
+ }
+ }
+ }
+ #endregion
+
+}
|