diff options
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.ssc')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.ssc | 790 |
1 files changed, 790 insertions, 0 deletions
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 |