diff options
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.ssc | 299 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomCheck.ssc | 692 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomErrorHandler.ssc | 46 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 291 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.ssc | 947 | ||||
| -rw-r--r-- | Source/VCGeneration/VCGeneration.sscproj | 8 | ||||
| -rw-r--r-- | Test/doomed/doomed.bpl | 27 | ||||
| -rw-r--r-- | Test/doomed/notdoomed.bpl | 28 | ||||
| -rw-r--r-- | Test/doomed/runtest.bat | 7 |
9 files changed, 1432 insertions, 913 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc index 836d8c0a..77df5476 100644 --- a/Source/VCGeneration/ConditionGeneration.ssc +++ b/Source/VCGeneration/ConditionGeneration.ssc @@ -195,6 +195,305 @@ namespace VC /////////////////////////////////// Common Methods and Classes //////////////////////////////////////////
+#region Methods for injecting pre- and postconditions
+ 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>
+ protected 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>
+ protected 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>
+ protected 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>
+ protected 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;
+ }
+
+ /// <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>
+ protected 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;
+ }
+
+#endregion
+
+
protected Checker! FindCheckerFor(Implementation! impl, int timeout)
{
int i = 0;
diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc new file mode 100644 index 00000000..e888d115 --- /dev/null +++ b/Source/VCGeneration/DoomCheck.ssc @@ -0,0 +1,692 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+/*
+ Todo:
+ - Inject Pre- and Postcondition
+*/
+
+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
+{
+ internal class Evc {
+
+ public DoomErrorHandler ErrorHandler {
+ set {
+ m_ErrorHandler = value;
+ }
+ }
+
+ private Checker! m_Checker;
+ private DoomErrorHandler m_ErrorHandler;
+
+ [NotDelayed]
+ public Evc(Checker! check) {
+ m_Checker = check;
+ base();
+ }
+
+ public void Initialize(VCExpr! evc) {
+ m_Checker.PushVCExpr(evc);
+ }
+
+ public bool CheckReachvar(Variable! reachvar, out ProverInterface.Outcome outcome) {
+ VCExpr! vc = m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(reachvar);
+ // Todo: Check if vc is trivial true or false
+ outcome = ProverInterface.Outcome.Undetermined;
+ assert m_ErrorHandler !=null;
+ m_Checker.BeginCheck(reachvar.Name, vc, m_ErrorHandler);
+ m_Checker.ProverDone.WaitOne();
+
+ try {
+ outcome = m_Checker.ReadOutcome();
+ } catch (UnexpectedProverOutputException e)
+ {
+ if (CommandLineOptions.Clo.TraceVerify) {
+ Console.WriteLine("Prover is unable to check {0}! Reason:", reachvar.Name);
+ Console.WriteLine(e.ToString());
+ }
+ return false;
+ }
+ return true;
+ }
+ }
+
+ internal class DoomCheck {
+
+ #region Attributes
+ public Hashtable! Label2Absy;
+ public DoomErrorHandler ErrorHandler {
+ set {
+ m_ErrHandler = value;
+ m_Evc.ErrorHandler = value;
+ }
+
+ get {
+ return m_ErrHandler;
+ }
+ }
+
+ private DoomErrorHandler m_ErrHandler;
+ private Implementation! m_PassiveImpl;
+ private Checker! m_Check;
+ private InclusionOrder! m_Order;
+ private Evc! m_Evc;
+ #endregion
+
+ [NotDelayed]
+ public DoomCheck (Implementation! passive_impl, Checker! check) {
+ m_PassiveImpl = passive_impl;
+ m_Check = check;
+ m_Order = new InclusionOrder(passive_impl);
+ Label2Absy = new Hashtable(); // This is only a dummy
+ m_Evc = new Evc(check);
+ base();
+ Hashtable l2a = null;
+ VCExpr! vce = this.GenerateEVC(passive_impl, out l2a, check);
+ assert l2a!=null;
+ Label2Absy = l2a;
+ m_Evc.Initialize(vce);
+ }
+
+ /* - Set b to the next block that needs to be checked.
+ - Returns false and set b to null if all blocks are checked.
+ - Has to be alternated with CheckLabel; might crash otherwise
+ */
+ public bool GetNextBlock(out Block b) {
+ return m_Order.GetNextBlock(out b);
+ }
+
+ /* - Checking a label means to ask the prover if |= ( rvar=false -> vc ) holds.
+ - outcome is set to Outcome.Invalid if the Block denoted by reachvar is doomed.
+ - returns false if the theorem prover throws an exception, otherwise true.
+ */
+ public bool CheckLabel(Variable! reachvar, out ProverInterface.Outcome outcome) {
+
+ outcome = ProverInterface.Outcome.Undetermined;
+ if (m_Evc.CheckReachvar(reachvar, out outcome) ) {
+ if (!m_Order.SetCurrentResult(reachvar, outcome, m_ErrHandler)) {
+ outcome = ProverInterface.Outcome.Undetermined;
+ }
+ return true;
+ } else {
+ m_Order.SetCurrentResult(reachvar, ProverInterface.Outcome.Undetermined, m_ErrHandler);
+ return false;
+ }
+ }
+
+ public List<List<Block!>!>! DoomedSequences {
+ get {
+ return m_Order.DetectedBlock;
+ }
+ }
+
+
+ #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.Doomed:
+ vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);
+ break;
+ default:
+ assert false; // unexpected enumeration value
+ }
+ return vc;
+ }
+
+ 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);
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) );
+ } else {
+ return proverCtxt.ExprGen.Let(bindings, 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) {
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ SuccCorrect = VCExpressionGenerator.False;
+ } else {
+ 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);
+ // 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
+
+
+ #region Build Inclusion Order to minimize the number of checks
+ class InclusionOrder
+ {
+
+ #region Attributes
+ public List<List<Block!>!>! DetectedBlock = new List<List<Block!>!>();
+ Implementation! m_Impl;
+ InclusionTree! RootNode = new InclusionTree(null);
+ InclusionTree currentNode = null;
+
+ #endregion
+
+ [NotDelayed]
+ public InclusionOrder(Implementation! impl) {
+ /*
+ We now compute for each block the set of blocks that
+ are reached on every execution reaching this block.
+ We first compute it form the start block to the current
+ block and second from the Term block to the current one.
+ Finally we build the union.
+ */
+ m_Impl = impl;
+ base();
+ Dictionary<Block!,TraceNode!>! map2 = new Dictionary<Block!,TraceNode!>();
+ Dictionary<Block!,TraceNode!>! map = new Dictionary<Block!,TraceNode!>();
+
+ Dictionary<Block!, List<Block!>!>! unavoidablemap = new Dictionary<Block!, List<Block!>!>();
+
+ Block! exitblock = BreadthFirst(impl.Blocks[0], map2);
+ BreadthFirstBwd(exitblock, map);
+
+ foreach (KeyValuePair<Block!, TraceNode!> kvp in map) {
+ List<Block!>! blist = new List<Block!>();
+ foreach (TraceNode tn in kvp.Value.Unavoidables ) {
+ blist.Add(tn.block);
+ }
+ unavoidablemap.Add(kvp.Key, blist);
+ }
+ foreach (KeyValuePair<Block!, List<Block!>!> kvp in unavoidablemap) {
+ TraceNode tn = null;
+ if (map2.TryGetValue(kvp.Key, out tn) ) {
+ assert tn!=null;
+ foreach (TraceNode! t0 in tn.Unavoidables) {
+ if (!kvp.Value.Contains(t0.block))
+ kvp.Value.Add(t0.block);
+ }
+ } else {
+ assert false;
+ }
+ }
+
+ foreach (KeyValuePair<Block!, List<Block!>!> kvp in unavoidablemap) {
+ Insert2Tree(RootNode,kvp);
+ }
+ InitCurrentNode(RootNode);
+ //printtree(RootNode, "",0);
+ }
+
+ void InitCurrentNode(InclusionTree! n) {
+ if (n.Children.Count>0) {
+ InitCurrentNode(n.Children[0]);
+ } else {
+ currentNode = n;
+ }
+ }
+
+ public bool GetNextBlock(out Block b) {
+ if (currentNode!=null && currentNode.EquivBlock.Count>0) {
+ b = currentNode.EquivBlock[0];
+ return true;
+ }
+ b = null;
+ return false;
+ }
+
+ // Takes the outcome for the current reachvar and marks all blocks
+ // the do not need any further checking because they share the same
+ // desteny
+ // returns false if an explicite assert false was found.
+ public bool SetCurrentResult(Variable! reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) {
+ if (outcome!=ProverInterface.Outcome.Valid) {
+ if (currentNode != null) {
+ currentNode.IsDoomed = false;
+ currentNode.HasBeenChecked = true;
+ MarkUndoomedParents(currentNode);
+ currentNode = FindNextNode(currentNode);
+ }
+ } else {
+ if (currentNode != null) {
+
+ // Check if there is an assert false in this node or in one of its parents
+ // if so do not report anything
+ if (ECContainsAssertFalse(currentNode.EquivBlock)) {
+ Console.WriteLine("Assert false was detected, but ignored");
+ currentNode.HasBeenChecked = true;
+ currentNode.IsDoomed = false;
+ currentNode = currentNode.Parent;
+ return false;
+ }
+
+ List<Block!>! traceblocks = new List<Block!>();
+
+ TracedChildern(currentNode, traceblocks);
+ TracedParents(currentNode, traceblocks);
+
+// cb.OnWarning("Doomed program points found!");
+ if (cb != null) {
+ cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);
+ }
+
+ if (currentNode.EquivBlock.Count>0) {
+
+ foreach (InclusionTree! n in currentNode.Children) {
+ if (DetectedBlock.Contains(n.EquivBlock) ) {
+ DetectedBlock.Remove(n.EquivBlock);
+ }
+ }
+
+ DetectedBlock.Add(currentNode.EquivBlock);
+ // Todo: Remove all doomed blocks that are found
+ // in children.
+ // Maybe one should remove them only if all children
+ // are doomed, but this does not affect soundness
+ } else {
+ Console.WriteLine("An empty equivalence class has been detected");
+ assert false;
+ }
+
+ currentNode.IsDoomed = true;
+ currentNode.HasBeenChecked = true;
+ MarkDoomedChildren(currentNode);
+ currentNode = currentNode.Parent;
+ }
+ }
+ return true;
+ }
+
+ private bool ECContainsAssertFalse(List<Block!>! equiv) {
+ foreach (Block! b in equiv) {
+ if (BlockContainsAssertFalse(b)) return true;
+ }
+ return false;
+ }
+
+ private bool BlockContainsAssertFalse(Block! b) {
+ foreach (Cmd! c in b.Cmds) {
+ AssertCmd ac = c as AssertCmd;
+ if (ac!=null) {
+ if (IsFalse(ac.Expr) ) {
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
+ // 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;
+ }
+
+ private void TracedChildern(InclusionTree! node, List<Block!>! blist) {
+ foreach (Block! b in node.EquivBlock) {
+ if (!blist.Contains(b)) blist.Add(b);
+ }
+ foreach (InclusionTree! n in node.Children) {
+ TracedChildern(n, blist);
+ }
+ }
+
+ private void TracedParents(InclusionTree! node, List<Block!>! blist) {
+ foreach (Block! b in node.EquivBlock) {
+ if (!blist.Contains(b)) blist.Add(b);
+ }
+ if (node.Parent!=null) {
+ TracedParents(node.Parent, blist);
+ }
+ }
+
+ InclusionTree FindNextNode(InclusionTree! n) {
+ assert n!=n.Parent;
+ InclusionTree next = n.Parent;
+ if (next!=null) {
+ foreach (InclusionTree! n0 in next.Children) {
+ if (!n0.HasBeenChecked) {
+ return n0;
+ }
+ }
+ return FindNextNode(next);
+ }
+ return next;
+ }
+
+ void MarkUndoomedParents(InclusionTree! n) {
+ if (n.Parent != null) {
+ n.Parent.HasBeenChecked = true;
+ n.Parent.IsDoomed = false;
+ MarkUndoomedParents(n.Parent);
+ }
+ }
+
+ void MarkDoomedChildren(InclusionTree! n) {
+ foreach (InclusionTree! t in n.Children) {
+ t.IsDoomed = true;
+ t.HasBeenChecked = true;
+ MarkDoomedChildren(t);
+ }
+ }
+
+ bool Insert2Tree(InclusionTree! node, KeyValuePair<Block!, List<Block!>!> kvp) {
+ if (IsSubset(node.PathBlocks, kvp.Value) ) {
+ if (IsSubset(kvp.Value, node.PathBlocks) ) {
+ // The set of unavoidable blocks is equal, so
+ // we can put the block in the same node.
+ node.EquivBlock.Add(kvp.Key);
+ return true;
+ } else {
+ foreach (InclusionTree! n in node.Children) {
+ if (Insert2Tree(n,kvp) ) {
+ return true;
+ }
+ }
+ // we have not been able to add the block to one of
+ // the children, so we have to create a new child.
+ InclusionTree! it = new InclusionTree(node);
+ it.EquivBlock.Add(kvp.Key);
+ it.PathBlocks.AddRange(kvp.Value);
+ node.Children.Add(it);
+ return true;
+ }
+ // If we reached this point, we have to add a new node since
+ // our current set of pathnodes is not a subset of anything else
+ } else {
+ // seems, that we have reached a new leaf.
+ }
+ return false;
+ }
+
+ bool IsSubset(List<Block!>! sub, List<Block!>! super ) {
+ foreach (Block! b in sub) {
+ if (!super.Contains(b) ) return false;
+ }
+ return true;
+ }
+
+ void printtree(InclusionTree! n, string indent, int level) {
+ Console.Write("{0}Level {1}: Blocks ", indent, level);
+ foreach (Block! b in n.EquivBlock) {
+ Console.Write("{0}, ", b.Label);
+ }
+ Console.WriteLine();
+
+ foreach (InclusionTree! t in n.Children) {
+ printtree(t, indent+" ", level+1);
+ }
+ }
+
+ private class InclusionTree {
+ public InclusionTree(InclusionTree p) {
+ Parent = p;
+ HasBeenChecked=false;
+ IsDoomed = false;
+ }
+
+ public bool HasBeenChecked;
+ public bool IsDoomed;
+ public InclusionTree Parent;
+ public List<Block!>! EquivBlock = new List<Block!>();
+ public List<Block!>! PathBlocks = new List<Block!>();
+ public List<InclusionTree!>! Children = new List<InclusionTree!>();
+ }
+
+ #region Collect Unavoidable Blocks
+ private Block! BreadthFirst(Block! start, Dictionary<Block!, TraceNode!>! blockmap) {
+ List<Block!>! JobList = new List<Block!>();
+ List<Block!>! DoneList = new List<Block!>();
+ Block exitblock=null;
+ JobList.Add(start);
+ Block! currentBlock = JobList[0];
+ // Travers the Graph Breadth First and collect all
+ // predecessors of each node that are reached on any
+ // path to this node
+ while (JobList.Count>0)
+ {
+ currentBlock = JobList[0];
+ TraceNode! tn = new TraceNode(currentBlock);
+
+ if (currentBlock.Predecessors.Length>0 ) {
+ TraceNode t0 =null;
+ Block firstpred = currentBlock.Predecessors[0];
+
+ assert firstpred!=null;
+ if (blockmap.TryGetValue(firstpred, out t0)) {
+ assert t0 !=null;
+ tn.Unavoidables.AddRange(t0.Unavoidables);
+ }
+ }
+
+ foreach (Block! b0 in currentBlock.Predecessors) {
+ TraceNode t = null;
+ if (blockmap.TryGetValue(b0, out t)) {
+ assert t!=null;
+ tn.Predecessors.Add(t);
+ IntersectUnavoidables(t,tn);
+ if (!t.Successors.Contains(tn)) t.Successors.Add(tn);
+ blockmap[b0]=t;
+ }
+ }
+ if (!tn.Unavoidables.Contains(tn)) {
+ tn.Unavoidables.Add(tn);
+ } else
+ {
+ assert false;
+ }
+
+
+ blockmap.Add(currentBlock, tn);
+
+ GotoCmd gc = currentBlock.TransferCmd as GotoCmd;
+ if (gc!=null) {
+ assert gc.labelTargets!=null;
+ foreach (Block! b0 in gc.labelTargets) {
+ if (!JobList.Contains(b0) && !DoneList.Contains(b0)) {
+
+ JobList.Add(b0);
+ }
+ }
+ } else {
+ exitblock=currentBlock;
+ }
+ DoneList.Add(currentBlock);
+ JobList.RemoveAt(0);
+ }
+ assert exitblock!=null;
+ return exitblock;
+ }
+
+ // WARNING: It is only for testing reasons that
+ // BreadthFirstBwd and BreadthFirst and separat functions
+ // it should be implemented using one function later on.
+ private void BreadthFirstBwd(Block! start, Dictionary<Block!, TraceNode!>! blockmap) {
+ List<Block!>! JobList = new List<Block!>();
+ List<Block!>! DoneList = new List<Block!>();
+ JobList.Add(start);
+ Block! currentBlock = JobList[0];
+ // Travers the Graph Breadth First and collect all
+ // predecessors of each node that are reached on any
+ // path to this node
+ while (JobList.Count>0)
+ {
+ currentBlock = JobList[0];
+ TraceNode! tn = new TraceNode(currentBlock);
+
+ GotoCmd gc = currentBlock.TransferCmd as GotoCmd;
+ BlockSeq preds = null;
+ if (gc!=null) {
+ preds = gc.labelTargets;
+ }
+
+ if (preds != null ) {
+
+ TraceNode t0 =null;
+ Block firstpred = preds[0];
+
+ assert firstpred!=null;
+ if (blockmap.TryGetValue(firstpred, out t0)) {
+ assert t0 !=null;
+ tn.Unavoidables.AddRange(t0.Unavoidables);
+ }
+
+
+ foreach (Block! b0 in preds) {
+ TraceNode t = null;
+ if (blockmap.TryGetValue(b0, out t)) {
+ assert t!=null;
+ tn.Successors.Add(t);
+ IntersectUnavoidables(t,tn);
+ if (!t.Predecessors.Contains(tn)) t.Predecessors.Add(tn);
+ blockmap[b0]=t;
+ }
+ }
+ }
+ if (!tn.Unavoidables.Contains(tn)) {
+ tn.Unavoidables.Add(tn);
+ } else
+ {
+ assert false;
+ }
+ blockmap.Add(currentBlock, tn);
+
+ if (currentBlock.Predecessors.Length>0) {
+ foreach (Block! b0 in currentBlock.Predecessors) {
+ if (!JobList.Contains(b0) && !DoneList.Contains(b0) )
+ JobList.Add(b0);
+ }
+ }
+ DoneList.Add(currentBlock);
+ JobList.RemoveAt(0);
+ }
+ }
+
+ private void IntersectUnavoidables(TraceNode! parent, TraceNode! child) {
+ List<TraceNode!>! ret = new List<TraceNode!>();
+ List<TraceNode!>! tmp = new List<TraceNode!>();
+ tmp.AddRange(parent.Unavoidables);
+ tmp.AddRange(child.Unavoidables);
+
+ foreach (TraceNode! tn in tmp) {
+ if (parent.Unavoidables.Contains(tn) && child.Unavoidables.Contains(tn)
+ && !ret.Contains(tn) ) {
+ ret.Add(tn);
+ }
+ }
+ assert ret.Count <= parent.Unavoidables.Count && ret.Count <= child.Unavoidables.Count;
+ child.Unavoidables = ret;
+
+ }
+
+ #region TraceNode Class
+ // We assume that the program is already loopfree, otherwise we will
+ // not terminate
+ private class TraceNode {
+ public List<TraceNode!>! Predecessors = new List<TraceNode!>();
+ public List<TraceNode!>! Successors = new List<TraceNode!>();
+ public List<TraceNode!>! Unavoidables = new List<TraceNode!>();
+ public Block! block;
+
+
+ public TraceNode(Block! b) {
+ block=b;
+ }
+
+ }
+ #endregion
+ #endregion
+ }
+ #endregion
+
+
+ }
+}
diff --git a/Source/VCGeneration/DoomErrorHandler.ssc b/Source/VCGeneration/DoomErrorHandler.ssc new file mode 100644 index 00000000..6c8a7ec7 --- /dev/null +++ b/Source/VCGeneration/DoomErrorHandler.ssc @@ -0,0 +1,46 @@ +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
+{
+ internal class DoomErrorHandler : ProverInterface.ErrorHandler {
+
+ protected Hashtable! label2Absy;
+ protected VerifierCallback! callback;
+
+ public Variable m_Reachvar;
+ public List<Block!> m_DoomedBlocks, m_TraceBlocks;
+
+
+ public DoomErrorHandler(Hashtable! label2Absy, VerifierCallback! callback) {
+ this.label2Absy = label2Absy;
+ this.callback = callback;
+ }
+
+ public override Absy! Label2Absy(string! label) {
+ int id = int.Parse(label);
+ return (Absy!) label2Absy[id];
+ }
+
+ public override void OnProverWarning(string! msg) {
+ this.callback.OnWarning(msg);
+ }
+
+ public void OnDoom(Variable! reachvar, List<Block!>! doomedblocks, List<Block!>! traceblocks) {
+ m_Reachvar = reachvar;
+ m_DoomedBlocks = doomedblocks;
+ m_TraceBlocks = traceblocks;
+ }
+ }
+
+}
\ No newline at end of file diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index a5590b2c..6e5b147b 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -58,299 +58,8 @@ namespace VC 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
diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc index 8594606c..84df1be4 100644 --- a/Source/VCGeneration/VCDoomed.ssc +++ b/Source/VCGeneration/VCDoomed.ssc @@ -20,10 +20,11 @@ namespace VC {
public class DCGen : ConditionGeneration
{
-
+ #region Attributes
private Dictionary<Block, Variable!>! m_BlockReachabilityMap;
-
-
+ Dictionary<Block!, Block!>! m_copiedBlocks = new Dictionary<Block!, Block!>();
+ const string reachvarsuffix = "__ivebeenthere";
+ #endregion
/// <summary>
/// Constructor. Initializes the theorem prover.
/// </summary>
@@ -35,31 +36,6 @@ namespace VC m_BlockReachabilityMap = new Dictionary<Block, Variable!>();
}
- private class DummyErrorHandler : ProverInterface.ErrorHandler
- {
- Hashtable! label2Absy;
- VerifierCallback! callback;
-
- public DummyErrorHandler(Hashtable! label2Absy, VerifierCallback! callback) {
- this.label2Absy = label2Absy;
- this.callback = callback;
- }
-
- public override Absy! Label2Absy(string! label) {
- int id = int.Parse(label);
- return (Absy!) label2Absy[id];
- }
-
- public override void OnProverWarning(string! msg) {
- this.callback.OnWarning(msg);
- }
-
- public override void OnModel(IList<string!>! labels, ErrorModel errModel)
- {}
- public override void OnResourceExceeded(string! message)
- {}
- }
-
/// <summary>
/// MSchaef:
/// - remove loops and add reach variables
@@ -74,139 +50,262 @@ namespace VC if (CommandLineOptions.Clo.TraceVerify) {
Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);
}
- // MSchaef: The error handler errh can only be used to emmit warnings
-
+ Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);
callback.OnProgress("doomdetector",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);
+
+ //List<Block!>! orig_blocks = new List<Block!>(impl.Blocks);
+
+ Dictionary<Block!, Block!> copiedblocks;
+ impl.Blocks = DCProgramTransformer.Convert2Dag(impl, program, cblocks, out copiedblocks);
+ assert copiedblocks!=null;
ComputePredecessors(impl.Blocks);
m_BlockReachabilityMap = new Dictionary<Block, Variable!>();
PassifyProgram(impl, program);
#endregion
-
- int totalblocks = impl.Blocks.Count;
+ //EmitImpl(impl,false);
Checker! checker = FindCheckerFor(impl, 1000);
-
- Hashtable label2absy;
-
- VCExpr! vc = GenerateEVC(impl, out label2absy, checker);
- assert label2absy!=null;
- DummyErrorHandler errh = new DummyErrorHandler(label2absy, callback );
- checker.PushVCExpr(vc);
- checkimplsanity(impl.Blocks[0]);
-
- InclusionOrder incorder = new InclusionOrder(impl);
- incorder.ToString();
- int totalchecks=0;
-
+ DoomCheck dc = new DoomCheck(impl, checker);
- Block b=null;
- while ( incorder.GetNextBlock(out b) )
- {
-
+ Block b = null;
+ ProverInterface.Outcome outcome;
+ dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
+ bool doomfound = false;
+ while (dc.GetNextBlock(out b) && !doomfound) {
assert b!=null;
- if (CommandLineOptions.Clo.TraceVerify) {
- totalchecks++;
- Console.WriteLine("Checking Block {0}", b.Label);
- }
+ outcome = ProverInterface.Outcome.Undetermined;
+
Variable v = null;
m_BlockReachabilityMap.TryGetValue(b, out v);
assert v!=null;
-
- VCExpr! currentlabel = checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v);
- ProverInterface.Outcome o = AskProver(b.Label, checker, currentlabel, errh);
- switch (o)
- {
- case ProverInterface.Outcome.Valid:
- {
+ if (!dc.CheckLabel(v, out outcome) ) {
+ return Outcome.Inconclusive;
+ }
+
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid: {
+ Console.WriteLine("[x] {0} is doomed", v.Name);
+ doomfound=true;
+ break;
+ }
+ case ProverInterface.Outcome.Invalid: {
- incorder.SetCurrentResult(true, callback, impl);
-
- // TODO: remove this return and make sure that the CE generation does not change the program
- checker.Close();
- return Outcome.Errors;
- break;
- }
- case ProverInterface.Outcome.Invalid:
- {
- // Todo: Try to use the counter example to minimize the number of checks needed
- incorder.SetCurrentResult(false, callback, null);
- break;
- }
- default:
- {
- incorder.SetCurrentResult(false, callback, null);
- if (CommandLineOptions.Clo.TraceVerify) {
- Console.WriteLine("I'm confused about Block {0}.", b.Label);
+ break;
}
- break;
- }
- }
- }
- if (CommandLineOptions.Clo.TraceVerify) {
- Console.WriteLine("total doomed points: {0}", incorder.DetectedBlock.Count );
- Console.WriteLine("We had to ask {0} blocks out of {1}.\n \n", totalchecks, totalblocks );
+ default: {
+
+ break;
+ }
+ }
+
}
-
checker.Close();
-
- //Todo: Implement dead code detection -> see smoke tester
- //Console.WriteLine(">>> Starting Dead Code Detection ");
-
+
+ if (dc.DoomedSequences.Count>0 ) {
+ SearchCounterexample(impl, dc.ErrorHandler, callback);
+ }
+ Console.WriteLine();
return Outcome.Correct;
}
-
- private void checkimplsanity(Block! b) {
- GotoCmd gc = b.TransferCmd as GotoCmd;
- if (gc!=null) {
- assert gc.labelTargets != null;
- foreach (Block! b0 in gc.labelTargets) {
- bool sane=false;
- foreach (Block! b1 in b0.Predecessors) {
- if (b1==b) {
- sane=true;
- break;
- }
- }
- if (!sane)
- Console.WriteLine("{{{{{{{{{{{{ {0} is not marked as pred of {1}", b.Label, b0.Label );
+
+ private void SearchCounterexample(Implementation! impl, DoomErrorHandler! errh, VerifierCallback! callback) {
+ if (errh.m_Reachvar==null) {
+ assert false;
+ return;
+ }
+ Console.WriteLine("{0} is doomed due to the following statements:", errh.m_Reachvar.Name );
+
+ // modify the impl
+
+ assert errh.m_TraceBlocks != null;
+ assert errh.m_DoomedBlocks !=null;
+ List<Block!>! nondoomed = new List<Block!>();
+ foreach (Block! b in errh.m_DoomedBlocks) {
+ if (!errh.m_TraceBlocks.Contains(b) ) {
+ nondoomed.Add(b);
+ }
+ }
+
+ Dictionary<Block!, CmdSeq!>! cmdbackup = new Dictionary<Block!, CmdSeq!>();
+
+ BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count/2-1);
+ BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count/2,impl.Blocks.Count-1);
- checkimplsanity(b0);
+
+ #region Undo all modifications
+ foreach (KeyValuePair<Block!, CmdSeq!> kvp in cmdbackup) {
+ kvp.Key.Cmds = kvp.Value;
+ }
+ #endregion
+ }
+
+ bool BruteForceCESearch(Variable! reachvar, Implementation! impl, VerifierCallback! callback,
+ Dictionary<Block!, CmdSeq!>! cmdbackup, int startidx, int endidx) {
+ #region Modify implementation
+ for (int i=startidx; i<=endidx; i++) {
+ CmdSeq! cs = new CmdSeq();
+ cmdbackup.Add(impl.Blocks[i],impl.Blocks[i].Cmds);
+ foreach (Cmd! c in impl.Blocks[i].Cmds) {
+ if (ContainsReachVariable(c)) {
+ cs.Add(c);
+ continue;
+ }
+ AssertCmd ac = c as AssertCmd;
+ AssumeCmd uc = c as AssumeCmd;
+ if (ac!=null) {
+ cs.Add(new AssertCmd(ac.tok, Expr.True) );
+ } else if (uc!=null) {
+ cs.Add(new AssertCmd(uc.tok, Expr.True) );
+ } else {
+ cs.Add(c);
+ }
}
+ impl.Blocks[i].Cmds = cs;
}
+ #endregion
+
+ ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined;
+ if (!ReCheckImpl(reachvar, impl, callback, out outcome) ) {
+ UndoBlockModifications(impl, cmdbackup, startidx, endidx);
+ return false;
+ }
+ if (outcome == ProverInterface.Outcome.Valid) {
+ return true;
+ } else if (outcome == ProverInterface.Outcome.Invalid) {
+ UndoBlockModifications(impl, cmdbackup, startidx, endidx);
+ int mid = startidx + (endidx-startidx)/2;
+ if (startidx>=endidx) {
+ // Now we found an interesting Block and we have to
+ // search for the interesting statements.
+ int cmdcount = impl.Blocks[endidx].Cmds.Length-1;
+ BruteForceCmd(impl.Blocks[endidx],0,cmdcount/2 -1,reachvar, impl, callback);
+ BruteForceCmd(impl.Blocks[endidx],cmdcount/2,cmdcount,reachvar, impl, callback);
+ return true;
+ } else {
+ BruteForceCESearch(reachvar,impl, callback, cmdbackup, startidx, mid);
+ //if (startidx+mid+1>=endidx) mid--; //Hack
+ BruteForceCESearch(reachvar,impl, callback, cmdbackup, mid+1, endidx);
+ return true;
+ }
+ } else {
+ UndoBlockModifications(impl, cmdbackup, startidx, endidx);
+ return false;
+ }
}
+
+ bool BruteForceCmd(Block! b, int startidx, int endidx, Variable! reachvar,
+ Implementation! impl, VerifierCallback! callback) {
+ #region Modify Cmds
+ CmdSeq! backup = b.Cmds;
+ CmdSeq! cs = new CmdSeq();
+ for (int i=0;i<startidx;i++) {
+ cs.Add(b.Cmds[i]);
+ }
+ for (int i=startidx; i<=endidx; i++) {
+ Cmd! c = b.Cmds[i];
+ if (ContainsReachVariable(c)) {
+ cs.Add(c);
+ continue;
+ }
+ cs.Add(new AssertCmd(c.tok, Expr.True));
+ }
+ for (int i=endidx+1; i<b.Cmds.Length;i++) {
+ cs.Add(b.Cmds[i]);
+ }
- private ProverInterface.Outcome AskProver(string! label, Checker! checker, VCExpr! vc, ProverInterface.ErrorHandler! errh) {
- checker.BeginCheck(label, vc, errh);
- WaitHandle[] wh = new WaitHandle[1];
- ProverInterface.Outcome o = ProverInterface.Outcome.Undetermined;
+ b.Cmds = cs;
+ #endregion
- wh[0] = checker.ProverDone;
- WaitHandle.WaitAny(wh);
- try {
- o = checker.ReadOutcome();
- } catch (UnexpectedProverOutputException e)
- {
- Console.WriteLine(e.ToString());
+ #region Recheck
+ ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined;
+ if (!ReCheckImpl(reachvar, impl, callback, out outcome) ) {
+ b.Cmds = backup;
+ return false;
+ }
+ #endregion
+
+ if (outcome == ProverInterface.Outcome.Valid) {
+ return true;
+ } else if (outcome == ProverInterface.Outcome.Invalid) {
+ b.Cmds = backup;
+ if (startidx>=endidx) {
+ if (!ContainsReachVariable(b.Cmds[endidx])) {
+ Console.Write("Candidate L{0}: ", b.Cmds[endidx].tok.line );
+ b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);
+ return true;
+ } else {
+ return false;
+ }
+ } else {
+ int mid = startidx + (endidx-startidx)/2;
+ BruteForceCmd(b, startidx, mid, reachvar, impl, callback);
+ BruteForceCmd(b, mid+1, endidx, reachvar, impl, callback);
+ return false; // This is pure random
+ }
+ } else {
+ b.Cmds = backup;
+ return false;
}
- return o;
+
+ return false;
+ }
+
+ void UndoBlockModifications(Implementation! impl, Dictionary<Block!, CmdSeq!>! cmdbackup,
+ int startidx, int endidx) {
+ for (int i=startidx; i<=endidx; i++) {
+ CmdSeq cs = null;
+ if (cmdbackup.TryGetValue(impl.Blocks[i], out cs) ) {
+ assert cs!=null;
+ impl.Blocks[i].Cmds = cs;
+ cmdbackup.Remove(impl.Blocks[i]);
+ }
+ }
+ }
+
+ bool ReCheckImpl(Variable! reachvar, Implementation! impl, VerifierCallback! callback,
+ out ProverInterface.Outcome outcome) {
+ Checker! checker = FindCheckerFor(impl, 1000);
+ DoomCheck dc = new DoomCheck(impl, checker);
+ dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
+ outcome = ProverInterface.Outcome.Undetermined;
+ if (!dc.CheckLabel(reachvar, out outcome)) {
+ checker.Close();
+ return false;
+ }
+ checker.Close();
+ return true;
}
-
-
- protected Hashtable/*TransferCmd->ReturnCmd*/! PassifyImpl(Implementation! impl, Program! program)
- {
- return new Hashtable();
+
+
+ bool ContainsReachVariable(Cmd! c) {
+ AssertCmd artc = c as AssertCmd;
+ AssumeCmd amec = c as AssumeCmd;
+ Expr e;
+ if (artc!=null) {
+ e = artc.Expr;
+ } else if (amec!=null) {
+ e = amec.Expr;
+ } else {
+ return false;
+ }
+ Set! freevars = new Set();
+ e.ComputeFreeVariables(freevars);
+ foreach (Variable! v in freevars) {
+ if (v.Name.Contains(reachvarsuffix)) return true;
+ }
+ return false;
}
+
#region Loop Removal
/// <summary>
/// This class is accessed only via the static method Convert2Dag
@@ -216,24 +315,25 @@ namespace VC /// </summary>
private class DCProgramTransformer
{
- public static List<Block!>! Convert2Dag(Implementation! impl, Program! program, List<Block!>! checkableBlocks)
+ private List<Block!>! Blocks;
+ private List<Block!>! m_checkableBlocks;
+ private Dictionary<Block!, Block!>! m_copyMap = new Dictionary<Block!, Block!>();
+
+ public static List<Block!>! Convert2Dag(Implementation! impl, Program! program, List<Block!>! checkableBlocks,
+ out Dictionary<Block!, Block!> copiedblocks)
{
- 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);
+ 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();
-
+ pt.LoopUnrolling(gStart, new Dictionary<GraphNode, Block!>(), true, "");
+ pt.Blocks.Reverse();
+ copiedblocks = pt.m_copyMap;
return pt.Blocks;
}
-
- List<Block!>! Blocks;
-
- private List<Block!>! m_checkableBlocks;
-
+
DCProgramTransformer(List<Block!>! checkableBlocks)
{
@@ -242,7 +342,7 @@ namespace VC }
- #region Loop Unrolling Methods
+#region Loop Unrolling Methods
private Block! LoopUnrolling(GraphNode! node, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
{
@@ -278,7 +378,16 @@ namespace VC {
newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
}
- newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
+ newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
+ Block b;
+ if (m_copyMap.TryGetValue(node.Block, out b) ) {
+ assert b!=null;
+ m_copyMap.Add(newb, b);
+ } else {
+ m_copyMap.Add(newb, node.Block);
+ }
+
+
assert newb!=null; assert newb.TransferCmd!=null;
if (newSuccs.Length == 0)
newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
@@ -312,8 +421,8 @@ namespace VC Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last");
AddHavocCmd(last,loopNodes);
-
- Block! arb = UnrollOnce(cutPoint, last,visited2,true, prefix+"#Arb");
+ // You might use true for the unrollable flag as well.
+ Block! arb = UnrollOnce(cutPoint, last,visited2,false, prefix+"#Arb");
AddHavocCmd(arb,loopNodes);
@@ -324,6 +433,17 @@ namespace VC Blocks.Add(tmp);
m_checkableBlocks.Add(tmp);
+ // check if arb is already a copy of something else
+ // if not then write to m_copyMap that tmp is a copy
+ // of arb
+ Block b = null;
+ if (m_copyMap.TryGetValue(arb,out b) ) {
+ assert b!=null;
+ m_copyMap.Add(tmp, b);
+ } else {
+ m_copyMap.Add(tmp, arb);
+ }
+
Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First");
return first;
@@ -341,13 +461,20 @@ namespace VC private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
{
visited.Add(node, nextIter);
- Block newb;
+ Block newb,b;
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);
+ newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
+ if (m_copyMap.TryGetValue(node.Block, out b) ) {
+ assert b!=null;
+ m_copyMap.Add(newb, b);
+ } else {
+ m_copyMap.Add(newb, node.Block);
+ }
+
assert newb!=null; assert newb.TransferCmd!=null;
if (newSuccs.Length == 0)
newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
@@ -365,7 +492,7 @@ namespace VC foreach (Cmd! c in node.Body)
{
if (c is PredicateCmd || c is CommentCmd)
- body.Add(c);
+ body.Add(c );
else
break;
}
@@ -373,6 +500,14 @@ namespace VC TransferCmd! tcmd = new ReturnCmd(node.Block.tok);
Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd);
Blocks.Add(b);
+ Block tmp;
+ if (m_copyMap.TryGetValue(node.Block, out tmp) ) {
+ assert tmp!=null;
+ m_copyMap.Add(b, tmp);
+ } else {
+ m_copyMap.Add(b, node.Block);
+ }
+
return b;
}
@@ -577,16 +712,57 @@ namespace VC #endregion
#endregion
-
-
+
#region Program Passification
- private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl,
+ private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl,
Program! program)
{
Hashtable gotoCmdOrigins = new Hashtable();
Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
AddBlocksBetween(impl);
+
+ #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);
+ }
+ // Check If a new Unified Exit has been generated
+ GotoCmd gc = exitBlock.TransferCmd as GotoCmd;
+ if (gc!=null) {
+ assert gc.labelTargets !=null;
+ assert gc.labelTargets.Length==1;
+ assert gc.labelTargets[0]!=null;
+ exitBlock = (!)gc.labelTargets[0];
+ }
+ #endregion
GenerateReachabilityPredicates(impl, exitBlock);
current_impl = impl;
@@ -610,7 +786,7 @@ namespace VC //if (b.Cmds.Length == 0 ) continue;
Variable v_ = new LocalVariable(Token.NoToken,
- new TypedIdent(b.tok, b.Label+"__ivebeenthere",new BasicType(SimpleType.Bool) ) );
+ new TypedIdent(b.tok, b.Label+reachvarsuffix,new BasicType(SimpleType.Bool) ) );
impl.LocVars.Add(v_);
@@ -676,476 +852,5 @@ namespace VC #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.Doomed:
- 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! 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);
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
- return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) );
- } else {
- return proverCtxt.ExprGen.Let(bindings, 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) {
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
- SuccCorrect = VCExpressionGenerator.False;
- } else {
- 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);
-// 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
-
- #region Build Inclusion Order to minimize the number of checks
-
- class InclusionOrder
- {
- [NotDelayed]
- public InclusionOrder(Implementation! impl) {
- /*
- We now compute for each block the set of blocks that
- are reached on every execution reaching this block.
- We first compute it form the start block to the current
- block and second from the Term block to the current one.
- Finally we build the union.
- */
-
-
- Dictionary<Block!,TraceNode!>! map2 = new Dictionary<Block!,TraceNode!>();
- Dictionary<Block!,TraceNode!>! map = new Dictionary<Block!,TraceNode!>();
-
- Dictionary<Block!, List<Block!>!>! unavoidablemap = new Dictionary<Block!, List<Block!>!>();
-
- Block! exitblock = BreadthFirst(impl.Blocks[0], map2);
- BreadthFirstBwd(exitblock, map);
-
- foreach (KeyValuePair<Block!, TraceNode!> kvp in map) {
- List<Block!>! blist = new List<Block!>();
- foreach (TraceNode tn in kvp.Value.Unavoidables ) {
- blist.Add(tn.block);
- }
- unavoidablemap.Add(kvp.Key, blist);
- }
- foreach (KeyValuePair<Block!, List<Block!>!> kvp in unavoidablemap) {
- TraceNode tn = null;
- if (map2.TryGetValue(kvp.Key, out tn) ) {
- assert tn!=null;
- foreach (TraceNode! t0 in tn.Unavoidables) {
- if (!kvp.Value.Contains(t0.block))
- kvp.Value.Add(t0.block);
- }
- } else {
- assert false;
- }
- }
-
- foreach (KeyValuePair<Block!, List<Block!>!> kvp in unavoidablemap) {
- Insert2Tree(RootNode,kvp);
- }
- InitCurrentNode(RootNode);
- //printtree(RootNode, "",0);
- }
-
- InclusionTree! RootNode = new InclusionTree(null);
-
- InclusionTree currentNode = null;
-
- void InitCurrentNode(InclusionTree! n) {
- if (n.Children.Count>0) {
- InitCurrentNode(n.Children[0]);
- } else {
- currentNode = n;
- }
- }
-
- public bool GetNextBlock(out Block b) {
- if (currentNode!=null) {
- b = currentNode.EquivBlock[0];
- return true;
- }
- b = null;
- return false;
- }
-
- public List<Block!>! DetectedBlock = new List<Block!>();
-
- public void SetCurrentResult(bool isDoomed, VerifierCallback! cb, Implementation? impl) {
- if (!isDoomed) {
- if (currentNode != null) {
- currentNode.IsDoomed = false;
- currentNode.HasBeenChecked = true;
- MarkUndoomedParents(currentNode);
- currentNode = FindNextNode(currentNode);
- }
- } else {
- if (currentNode != null) {
- string dblocks = "Doomed Blocks: ";
- // WARNING THIS IS A HACK:
- assert impl!=null;
- impl.Blocks.Clear();
-
- foreach (Block! b in currentNode.EquivBlock) {
- impl.Blocks.Add(b);
- dblocks += String.Format("{0}, ", b.Label);
- }
- cb.OnWarning("Doomed program points found!");
- cb.OnWarning(dblocks);
- cb.OnUnreachableCode(impl);
-
-
- if (currentNode.EquivBlock.Count>0) {
- DetectedBlock.Add(currentNode.EquivBlock[0]);
- // Todo: Remove all doomed blocks that are found
- // in children.
- // Maybe on should remove them only if all children
- // are doomed, but this does not affect soundness
- } else {
- Console.WriteLine("An empty equivalence class has been detected");
- assert false;
- }
-
- currentNode.IsDoomed = true;
- currentNode.HasBeenChecked = true;
- MarkDoomedChildren(currentNode);
- currentNode = currentNode.Parent;
- }
- }
- }
-
- InclusionTree FindNextNode(InclusionTree! n) {
- assert n!=n.Parent;
- InclusionTree next = n.Parent;
- if (next!=null) {
- foreach (InclusionTree! n0 in next.Children) {
- if (!n0.HasBeenChecked) {
- return n0;
- }
- }
- return FindNextNode(next);
- }
- return next;
- }
-
- void MarkUndoomedParents(InclusionTree! n) {
- if (n.Parent != null) {
- n.Parent.HasBeenChecked = true;
- n.Parent.IsDoomed = false;
- MarkUndoomedParents(n.Parent);
- }
- }
-
- void MarkDoomedChildren(InclusionTree! n) {
- foreach (InclusionTree! t in n.Children) {
- t.IsDoomed = true;
- t.HasBeenChecked = true;
- MarkDoomedChildren(t);
- }
- }
-
-
- void printtree(InclusionTree! n, string indent, int level) {
- Console.Write("{0}Level {1}: Blocks ", indent, level);
- foreach (Block! b in n.EquivBlock) {
- Console.Write("{0}, ", b.Label);
- }
- Console.WriteLine();
-
- foreach (InclusionTree! t in n.Children) {
- printtree(t, indent+" ", level+1);
- }
- }
-
- bool Insert2Tree(InclusionTree! node, KeyValuePair<Block!, List<Block!>!> kvp) {
- if (IsSubset(node.PathBlocks, kvp.Value) ) {
- if (IsSubset(kvp.Value, node.PathBlocks) ) {
- // The set of unavoidable blocks is equal, so
- // we can put the block in the same node.
- node.EquivBlock.Add(kvp.Key);
- return true;
- } else {
- foreach (InclusionTree! n in node.Children) {
- if (Insert2Tree(n,kvp) ) {
- return true;
- }
- }
- // we have not been able to add the block to one of
- // the children, so we have to create a new child.
- InclusionTree! it = new InclusionTree(node);
- it.EquivBlock.Add(kvp.Key);
- it.PathBlocks.AddRange(kvp.Value);
- node.Children.Add(it);
- return true;
- }
- // If we reached this point, we have to add a new node since
- // our current set of pathnodes is not a subset of anything else
- } else {
- // seems, that we have reached a new leaf.
- }
- return false;
- }
-
-
- bool IsSubset(List<Block!>! sub, List<Block!>! super ) {
- foreach (Block! b in sub) {
- if (!super.Contains(b) ) return false;
- }
- return true;
- }
-
-
- private class InclusionTree {
- public InclusionTree(InclusionTree p) {
- Parent = p;
- HasBeenChecked=false;
- IsDoomed = false;
- }
-
- public bool HasBeenChecked;
- public bool IsDoomed;
- public InclusionTree Parent;
- public List<Block!>! EquivBlock = new List<Block!>();
- public List<Block!>! PathBlocks = new List<Block!>();
- public List<InclusionTree!>! Children = new List<InclusionTree!>();
- }
-
- #region Collect Unavoidable Blocks
- private Block! BreadthFirst(Block! start, Dictionary<Block!, TraceNode!>! blockmap) {
- List<Block!>! JobList = new List<Block!>();
- List<Block!>! DoneList = new List<Block!>();
- Block exitblock=null;
- JobList.Add(start);
- Block! currentBlock = JobList[0];
- // Travers the Graph Breadth First and collect all
- // predecessors of each node that are reached on any
- // path to this node
- while (JobList.Count>0)
- {
- currentBlock = JobList[0];
- TraceNode! tn = new TraceNode(currentBlock);
-
- if (currentBlock.Predecessors.Length>0 ) {
- TraceNode t0 =null;
- Block firstpred = currentBlock.Predecessors[0];
-
- assert firstpred!=null;
- if (blockmap.TryGetValue(firstpred, out t0)) {
- assert t0 !=null;
- tn.Unavoidables.AddRange(t0.Unavoidables);
- }
- }
-
- foreach (Block! b0 in currentBlock.Predecessors) {
- TraceNode t = null;
- if (blockmap.TryGetValue(b0, out t)) {
- assert t!=null;
- tn.Predecessors.Add(t);
- IntersectUnavoidables(t,tn);
- if (!t.Successors.Contains(tn)) t.Successors.Add(tn);
- blockmap[b0]=t;
- }
- }
- if (!tn.Unavoidables.Contains(tn)) {
- tn.Unavoidables.Add(tn);
- } else
- {
- assert false;
- }
-
-
- blockmap.Add(currentBlock, tn);
-
- GotoCmd gc = currentBlock.TransferCmd as GotoCmd;
- if (gc!=null) {
- assert gc.labelTargets!=null;
- foreach (Block! b0 in gc.labelTargets) {
- if (!JobList.Contains(b0) && !DoneList.Contains(b0)) {
-
- JobList.Add(b0);
- }
- }
- } else {
- exitblock=currentBlock;
- }
- DoneList.Add(currentBlock);
- JobList.RemoveAt(0);
- }
- assert exitblock!=null;
- return exitblock;
- }
-
- // WARNING: It is only for testing reasons that
- // BreadthFirstBwd and BreadthFirst and separat functions
- // it should be implemented using one function later on.
- private void BreadthFirstBwd(Block! start, Dictionary<Block!, TraceNode!>! blockmap) {
- List<Block!>! JobList = new List<Block!>();
- List<Block!>! DoneList = new List<Block!>();
- JobList.Add(start);
- Block! currentBlock = JobList[0];
- // Travers the Graph Breadth First and collect all
- // predecessors of each node that are reached on any
- // path to this node
- while (JobList.Count>0)
- {
- currentBlock = JobList[0];
- TraceNode! tn = new TraceNode(currentBlock);
-
- GotoCmd gc = currentBlock.TransferCmd as GotoCmd;
- BlockSeq preds = null;
- if (gc!=null) {
- preds = gc.labelTargets;
- }
-
- if (preds != null ) {
-
- TraceNode t0 =null;
- Block firstpred = preds[0];
-
- assert firstpred!=null;
- if (blockmap.TryGetValue(firstpred, out t0)) {
- assert t0 !=null;
- tn.Unavoidables.AddRange(t0.Unavoidables);
- }
-
-
- foreach (Block! b0 in preds) {
- TraceNode t = null;
- if (blockmap.TryGetValue(b0, out t)) {
- assert t!=null;
- tn.Successors.Add(t);
- IntersectUnavoidables(t,tn);
- if (!t.Predecessors.Contains(tn)) t.Predecessors.Add(tn);
- blockmap[b0]=t;
- }
- }
- }
- if (!tn.Unavoidables.Contains(tn)) {
- tn.Unavoidables.Add(tn);
- } else
- {
- assert false;
- }
- blockmap.Add(currentBlock, tn);
-
- if (currentBlock.Predecessors.Length>0) {
- foreach (Block! b0 in currentBlock.Predecessors) {
- if (!JobList.Contains(b0) && !DoneList.Contains(b0) )
- JobList.Add(b0);
- }
- }
- DoneList.Add(currentBlock);
- JobList.RemoveAt(0);
- }
- }
-
-
- private void IntersectUnavoidables(TraceNode! parent, TraceNode! child) {
- List<TraceNode!>! ret = new List<TraceNode!>();
- List<TraceNode!>! tmp = new List<TraceNode!>();
- tmp.AddRange(parent.Unavoidables);
- tmp.AddRange(child.Unavoidables);
-
- foreach (TraceNode! tn in tmp) {
- if (parent.Unavoidables.Contains(tn) && child.Unavoidables.Contains(tn)
- && !ret.Contains(tn) ) {
- ret.Add(tn);
- }
- }
- assert ret.Count <= parent.Unavoidables.Count && ret.Count <= child.Unavoidables.Count;
- child.Unavoidables = ret;
-
- }
-
- #region TraceNode Class
- // We assume that the program is already loopfree, otherwise we will
- // not terminate
- private class TraceNode {
- public List<TraceNode!>! Predecessors = new List<TraceNode!>();
- public List<TraceNode!>! Successors = new List<TraceNode!>();
- public List<TraceNode!>! Unavoidables = new List<TraceNode!>();
- public Block! block;
-
-
- public TraceNode(Block! b) {
- block=b;
- }
-
- }
- #endregion
- #endregion
- }
- #endregion
-
}
-}
\ No newline at end of file +}
diff --git a/Source/VCGeneration/VCGeneration.sscproj b/Source/VCGeneration/VCGeneration.sscproj index 2db480f6..768c44bc 100644 --- a/Source/VCGeneration/VCGeneration.sscproj +++ b/Source/VCGeneration/VCGeneration.sscproj @@ -140,6 +140,14 @@ SubType="Code"
RelPath="AssemblyInfo.ssc"
/>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="DoomErrorHandler.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="DoomCheck.ssc"
+ />
</Include>
</Files>
</XEN>
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl new file mode 100644 index 00000000..a153e468 --- /dev/null +++ b/Test/doomed/doomed.bpl @@ -0,0 +1,27 @@ +
+procedure a(x:int)
+ requires x>0;
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+
+procedure b(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+ assert y!=2;
+}
+
+
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl new file mode 100644 index 00000000..86bf76d1 --- /dev/null +++ b/Test/doomed/notdoomed.bpl @@ -0,0 +1,28 @@ +procedure a(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+
+procedure b(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ assert false;
+ }
+}
+
+
+
+
+
diff --git a/Test/doomed/runtest.bat b/Test/doomed/runtest.bat index 215804cf..9dda44cf 100644 --- a/Test/doomed/runtest.bat +++ b/Test/doomed/runtest.bat @@ -4,7 +4,12 @@ setlocal set BOOGIEDIR=..\..\Binaries
set BGEXE=%BOOGIEDIR%\Boogie.exe
-for %%f in (smoke0.bpl) do (
+for %%f in (doomed.bpl) do (
+ echo -------------------- %%f --------------------
+ %BGEXE% /vc:doomed %* %%f
+)
+
+for %%f in (notdoomed.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% /vc:doomed %* %%f
)
|