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