Added a way of recovering counterexample paths after loop extraction. Stable, but still buggy.

4 files changed, 322 insertions, 31 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 588b2289..a24347f2 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -656,6 +656,14 @@ namespace Microsoft.Boogie {
                 // BP4xxx: Abstract interpretation errors (Is there such a thing?)

                 // BP5xxx: Verification errors

 

+                if (CommandLineOptions.Clo.ExtractLoops && (vcgen is VCGen))

+                {

+                    for (int i = 0; i < errors.Count; i++)

+                    {

+                        errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], program);

+                    }

+                }

+

                 errors.Sort(new CounterexampleComparer());

                 foreach (Counterexample error in errors) {

                   if (error is CallCounterexample) {

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 664fcdb9..c2ef05f9 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -446,6 +446,7 @@ namespace Microsoft.Boogie {
         LoopProcedure loopProc = new LoopProcedure(impl, header, inputs, outputs, globalMods);

         if (CommandLineOptions.Clo.LazyInlining > 0 || CommandLineOptions.Clo.StratifiedInlining > 0) {

           loopProc.AddAttribute("inline", Expr.Literal(1));

+          loopProc.AddAttribute("verify", Expr.Literal(false));

         }

         loopHeaderToLoopProc[header] = loopProc;

         CallCmd callCmd = new CallCmd(Token.NoToken, loopProc.Name, callInputs, callOutputs);

@@ -457,6 +458,8 @@ namespace Microsoft.Boogie {
         Contract.Assert(header != null);

         LoopProcedure loopProc = loopHeaderToLoopProc[header];

         Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();

+        Set<Block> dummyBlocks = new Set<Block>();

+

         CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]);  // fix me

         VariableSeq inputs = loopHeaderToInputs[header];

         VariableSeq outputs = loopHeaderToOutputs[header];

@@ -489,6 +492,8 @@ namespace Microsoft.Boogie {
           Block/*!*/ block2 = new Block(Token.NoToken, block1.Label,

                               new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));

           impl.Blocks.Add(block1);

+          dummyBlocks.Add(block1);

+          dummyBlocks.Add(block2);

 

           GotoCmd gotoCmd = source.TransferCmd as GotoCmd;

           Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Length >= 1);

@@ -505,6 +510,7 @@ namespace Microsoft.Boogie {
           gotoCmd.labelNames = newLabels;

           gotoCmd.labelTargets = newTargets;

 

+            

           blockMap[block1] = block2;

         }

         List<Block/*!*/>/*!*/ blocks = new List<Block/*!*/>();

@@ -569,9 +575,10 @@ namespace Microsoft.Boogie {
         Dictionary<Block, Block> reverseBlockMap = new Dictionary<Block, Block>();

         foreach (Block block in blockMap.Keys)

         {

+            if (dummyBlocks.Contains(block)) continue;

             reverseBlockMap[blockMap[block]] = block;

         }

-        loopProc.blockMap = reverseBlockMap;

+        loopProc.setBlockMap(reverseBlockMap);

       }

     }

 

@@ -2110,7 +2117,8 @@ namespace Microsoft.Boogie {
   public class LoopProcedure : Procedure

   {

       public Implementation enclosingImpl;

-      public Dictionary<Block, Block> blockMap;

+      private Dictionary<Block, Block> blockMap;

+      private Dictionary<string, Block> blockLabelMap;

 

       public LoopProcedure(Implementation impl, Block header,

                            VariableSeq inputs, VariableSeq outputs, IdentifierExprSeq globalMods)

@@ -2120,6 +2128,22 @@ namespace Microsoft.Boogie {
       {

           enclosingImpl = impl;

       }

+

+      public void setBlockMap(Dictionary<Block, Block> bm)

+      {

+          blockMap = bm;

+          blockLabelMap = new Dictionary<string, Block>();

+          foreach (var kvp in bm)

+          {

+              blockLabelMap.Add(kvp.Key.Label, kvp.Value);

+          }

+      }

+

+      public Block getBlock(string label)

+      {

+          if (blockLabelMap.ContainsKey(label)) return blockLabelMap[label];

+          return null;

+      }

   }

 

   public class Implementation : DeclWithFormals {

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 90ed5d5c..a99fb320 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -36,6 +36,35 @@ namespace Microsoft.Boogie {
     }

   }

 

+  public class TraceLocation : IEquatable<TraceLocation>

+  {

+      public int numBlock;

+      public int numInstr;

+

+      public TraceLocation(int numBlock, int numInstr)

+      {

+          this.numBlock = numBlock;

+          this.numInstr = numInstr;

+      }

+

+      public override bool Equals(object obj)

+      {

+          TraceLocation that = obj as TraceLocation;

+          if (that == null) return false;

+          return (numBlock == that.numBlock && numInstr == that.numInstr);

+      }

+

+      public bool Equals(TraceLocation that)

+      {

+          return (numBlock == that.numBlock && numInstr == that.numInstr);

+      }

+

+      public override int GetHashCode()

+      {

+          return numBlock.GetHashCode() ^ 131 * numInstr.GetHashCode();

+      }

+  }

+

   public abstract class Counterexample {

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -49,32 +78,73 @@ namespace Microsoft.Boogie {
     [Peer]

     public List<string>/*!>!*/ relatedInformation;

 

-    public Dictionary<Absy, CalleeCounterexampleInfo> calleeCounterexamples;

+    public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

     internal Counterexample(BlockSeq trace) {

       Contract.Requires(trace != null);

       this.Trace = trace;

       this.relatedInformation = new List<string>();

-      this.calleeCounterexamples = new Dictionary<Absy, CalleeCounterexampleInfo>();

+      this.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

       // base();

     }

 

-    public void AddCalleeCounterexample(Absy absy, CalleeCounterexampleInfo cex) {

-      Contract.Requires(absy != null);

+    // Create a shallow copy of the counterexample

+    public abstract Counterexample Clone();

+

+    public void AddCalleeCounterexample(TraceLocation loc, CalleeCounterexampleInfo cex)

+    {

       Contract.Requires(cex != null);

-      calleeCounterexamples[absy] = cex;

+      calleeCounterexamples[loc] = cex;

     }

 

-    public void AddCalleeCounterexample(Dictionary<Absy, CalleeCounterexampleInfo> cs) {

+    public void AddCalleeCounterexample(int numBlock, int numInstr, CalleeCounterexampleInfo cex)

+    {

+        Contract.Requires(cex != null);

+        calleeCounterexamples[new TraceLocation(numBlock, numInstr)] = cex;

+    }

+

+    public void AddCalleeCounterexample(Dictionary<TraceLocation, CalleeCounterexampleInfo> cs)

+    {

       Contract.Requires(cce.NonNullElements(cs));

-      foreach (Absy absy in cs.Keys) {

-        AddCalleeCounterexample(absy, cs[absy]);

+      foreach (TraceLocation loc in cs.Keys)

+      {

+          AddCalleeCounterexample(loc, cs[loc]);

       }

     }

 

+    // Looks up the Cmd at a given index into the trace

+    public Cmd getTraceCmd(TraceLocation loc)

+    {

+        Debug.Assert(loc.numBlock < Trace.Length);

+        Block b = Trace[loc.numBlock];

+        Debug.Assert(loc.numInstr < b.Cmds.Length);

+        return b.Cmds[loc.numInstr];

+    }

+

+    // Looks up the name of the called procedure. 

+    // Asserts that the name exists

+    public string getCalledProcName(Cmd cmd)

+    {

+        // There are two options:

+        // 1. cmd is a CallCmd

+        // 2. cmd is an AssumeCmd (passified version of a CallCmd)

+        if(cmd is CallCmd) {

+            return (cmd as CallCmd).Proc.Name;

+        }

+        AssumeCmd assumeCmd = cmd as AssumeCmd;

+        Debug.Assert(assumeCmd != null);

+

+        NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;

+        Debug.Assert(naryExpr != null);

+

+        return naryExpr.Fun.FunctionName;

+    }

+

     public void Print(int spaces) {

+      int numBlock = -1;

       foreach (Block b in Trace) {

         Contract.Assert(b != null);

+        numBlock++;

         if (b.tok == null) {

           Console.WriteLine("    <intermediate block>");

         } else {

@@ -85,19 +155,20 @@ namespace Microsoft.Boogie {
             for (int i = 0; i < spaces + 4; i++)

               Console.Write(" ");

             Console.WriteLine("{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);

-            foreach (Cmd cmd in b.Cmds) {

-              Contract.Assert(cmd != null);

-              if (calleeCounterexamples.ContainsKey(cmd)) {

-                AssumeCmd assumeCmd = cce.NonNull((AssumeCmd)cmd);

-                NAryExpr naryExpr = (NAryExpr)cce.NonNull(assumeCmd.Expr);

-                for (int i = 0; i < spaces + 4; i++)

-                  Console.Write(" ");

-                Console.WriteLine("Inlined call to procedure {0} begins", naryExpr.Fun.FunctionName);

-                calleeCounterexamples[cmd].counterexample.Print(spaces + 4);

-                for (int i = 0; i < spaces + 4; i++)

-                  Console.Write(" ");

-                Console.WriteLine("Inlined call to procedure {0} ends", naryExpr.Fun.FunctionName);

-              }

+            for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)

+            {

+                var loc = new TraceLocation(numBlock, numInstr);

+                if (calleeCounterexamples.ContainsKey(loc))

+                {

+                    var cmd = getTraceCmd(loc);

+                    for (int i = 0; i < spaces + 4; i++)

+                        Console.Write(" ");

+                    Console.WriteLine("Inlined call to procedure {0} begins", getCalledProcName(cmd));

+                    calleeCounterexamples[loc].counterexample.Print(spaces + 4);

+                    for (int i = 0; i < spaces + 4; i++)

+                        Console.Write(" ");

+                    Console.WriteLine("Inlined call to procedure {0} ends", getCalledProcName(cmd));

+                }

             }

           }

         }

@@ -139,6 +210,13 @@ namespace Microsoft.Boogie {
     public override int GetLocation() {

       return FailingAssert.tok.line * 1000 + FailingAssert.tok.col;

     }

+

+    public override Counterexample Clone()

+    {

+        var ret = new AssertCounterexample(Trace, FailingAssert);

+        ret.calleeCounterexamples = calleeCounterexamples;

+        return ret;

+    }

   }

 

   public class CallCounterexample : Counterexample {

@@ -165,6 +243,13 @@ namespace Microsoft.Boogie {
     public override int GetLocation() {

       return FailingCall.tok.line * 1000 + FailingCall.tok.col;

     }

+

+    public override Counterexample Clone()

+    {

+        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires);

+        ret.calleeCounterexamples = calleeCounterexamples;

+        return ret;

+    }

   }

 

   public class ReturnCounterexample : Counterexample {

@@ -191,6 +276,13 @@ namespace Microsoft.Boogie {
     public override int GetLocation() {

       return FailingReturn.tok.line * 1000 + FailingReturn.tok.col;

     }

+

+    public override Counterexample Clone()

+    {

+        var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures);

+        ret.calleeCounterexamples = calleeCounterexamples;

+        return ret;

+    }

   }

 

   public class VerifierCallback {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index a053a153..348c2ca9 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2932,7 +2932,7 @@ namespace VC {
         Contract.Assert(traceNodes.Contains(entryBlock));

         trace.Add(entryBlock);

 

-        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<Absy, CalleeCounterexampleInfo>());

+        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());

 

         if (newCounterexample == null)

           return;

@@ -3185,7 +3185,7 @@ namespace VC {
         Contract.Assert(traceNodes.Contains(entryBlock));

         trace.Add(entryBlock);

 

-        Dictionary<Absy, CalleeCounterexampleInfo> calleeCounterexamples = new Dictionary<Absy, CalleeCounterexampleInfo>();

+        var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

         Counterexample newCounterexample = GenerateTraceRec(labels, errModel, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples);

 

         return newCounterexample;

@@ -3195,7 +3195,7 @@ namespace VC {
       private Counterexample GenerateTraceRec(

                             IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, int candidateId,

                             Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,

-                            Dictionary<Absy/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {

+                            Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {

         Contract.Requires(cce.NonNullElements(labels));

         Contract.Requires(errModel != null);

         Contract.Requires(b != null);

@@ -3234,7 +3234,7 @@ namespace VC {
                 Contract.Assert(calls != null);

                 int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)];

 

-                calleeCounterexamples[assumeCmd] =

+                calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

                     new CalleeCounterexampleInfo(

                         cce.NonNull(GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),

                         new List<object>());

@@ -3670,6 +3670,173 @@ namespace VC {
       return gotoCmdOrigins;

     }

 

+    public Counterexample extractLoopTrace(Counterexample cex, Program program)

+    {

+        // Sanity checks: we must only be using one of lazy or stratified inlining

+        if (implName2LazyInliningInfo.Count == 0 && implName2StratifiedInliningInfo.Count == 0)

+            return cex;

+

+        Debug.Assert(implName2LazyInliningInfo.Count == 0 || implName2StratifiedInliningInfo.Count == 0);

+

+        // Construct the set of inlined procs in the original program

+        var inlinedProcs = new Dictionary<string, Implementation>();

+        foreach (var decl in program.TopLevelDeclarations)

+        {

+            if (decl is Implementation)

+            {

+                var name = (decl as Implementation).Name;

+                if (!elIsLoop(name))

+                {

+                    inlinedProcs.Add(name, decl as Implementation);

+                }

+            }

+        }

+

+        return extractLoopTraceRec(cex, null, inlinedProcs);

+    }

+

+    private Counterexample extractLoopTraceRec(Counterexample cex, string currProc, Dictionary<string, Implementation> inlinedProcs)

+    {

+        // Go through all blocks in the trace, map them back to blocks in the original programs (if there is one)

+        var ret = cex.Clone();

+        ret.Trace = new BlockSeq();

+        ret.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

+

+        for (int numBlock = 0; numBlock < cex.Trace.Length; numBlock ++ )

+        {

+            Block block = cex.Trace[numBlock];

+            var origBlock = elGetBlock(currProc, block);

+            if (origBlock != null) ret.Trace.Add(origBlock);

+            var callCnt = 1;

+            for (int numInstr = 0; numInstr < block.Cmds.Length; numInstr ++) {

+                Cmd cmd = block.Cmds[numInstr];

+                var loc = new TraceLocation(numBlock, numInstr);

+                if (!cex.calleeCounterexamples.ContainsKey(loc)) continue;

+                string callee = cex.getCalledProcName(cex.getTraceCmd(loc));

+                var calleeTrace = cex.calleeCounterexamples[loc].counterexample as AssertCounterexample;

+                Debug.Assert(calleeTrace != null);

+

+                var origTrace = extractLoopTraceRec(calleeTrace, callee, inlinedProcs);

+

+                if (elIsLoop(callee))

+                {

+                    // Absorb the trace into the current trace

+

+                    // We have to add the new trace at last but one position in case 

+                    // we're not already inside a loop

+

+                    int currLen = 0;

+                    Block last = null;

+                    bool inloop = elIsLoop(currProc);

+

+                    if (!inloop)

+                    {

+                        last = (Block)ret.Trace.Last();

+                        ret.Trace.Remove();

+                    }

+

+                    currLen = ret.Trace.Length;

+                    ret.Trace.AddRange(origTrace.Trace);

+

+                    foreach (var kvp in origTrace.calleeCounterexamples)

+                    {

+                        var newloc = new TraceLocation(kvp.Key.numBlock + currLen, kvp.Key.numInstr);

+                        ret.calleeCounterexamples.Add(newloc, kvp.Value);

+                    }

+

+                    if (!inloop)

+                    {

+                        ret.Trace.Add(last);

+                    }

+

+                }

+                else

+                {

+                    var origLoc = new TraceLocation(ret.Trace.Length - 1, getCallCmdPosition(origBlock, callCnt, inlinedProcs, callee));

+                    ret.calleeCounterexamples.Add(origLoc, new CalleeCounterexampleInfo(origTrace, new List<object>()));

+                    callCnt++;

+                }

+            }

+        }

+        return ret;

+    }

+

+    // return the position of the i^th CallCmd in the block (count only those Calls that call a procedure in inlinedProcs). 

+    // Assert failure if there isn't any.

+    // Assert that the CallCmd found calls "callee"

+    private int getCallCmdPosition(Block block, int i, Dictionary<string, Implementation> inlinedProcs, string callee)

+    {

+        Debug.Assert(i >= 1);

+        for (int pos = 0; pos < block.Cmds.Length; pos++)

+        {

+            Cmd cmd = block.Cmds[pos];

+            if (cmd is CallCmd)

+            {

+                var cc = (CallCmd)cmd;

+                if (inlinedProcs.ContainsKey(cc.Proc.Name))

+                {

+                    if (i == 1)

+                    {

+                        Debug.Assert(cc.Proc.Name == callee);

+                        return pos;

+                    }

+                    i--;

+                }

+            }

+        }

+        Debug.Assert(false, "Didn't find the i^th call cmd");

+        return -1;

+    }

+

+    private bool elIsLoop(string procname)

+    {

+        if (procname == null)

+        {

+            // we're in main

+            return false;

+        }

+

+        LazyInliningInfo info = null;

+        if (implName2LazyInliningInfo.ContainsKey(procname))

+        {

+            info = implName2LazyInliningInfo[procname];

+        }

+        else if (implName2StratifiedInliningInfo.ContainsKey(procname))

+        {

+            info = implName2StratifiedInliningInfo[procname] as LazyInliningInfo;

+        }

+

+        if (info == null) return false;

+

+        var lp = info.impl.Proc as LoopProcedure;

+

+        if (lp == null) return false;

+        return true;

+    }

+

+    private Block elGetBlock(string procname, Block block)

+    {

+        if (!elIsLoop(procname)) return block;

+

+        LazyInliningInfo info = null;

+        if (implName2LazyInliningInfo.ContainsKey(procname))

+        {

+            info = implName2LazyInliningInfo[procname];

+        }

+        else if (implName2StratifiedInliningInfo.ContainsKey(procname))

+        {

+            info = implName2StratifiedInliningInfo[procname] as LazyInliningInfo;

+        }

+

+        if (info == null) return null;

+

+        var lp = info.impl.Proc as LoopProcedure;

+

+        if(lp == null) return null;

+

+        return lp.getBlock(block.Label);

+    }

+

     private static Counterexample LazyCounterexample(

                                        ErrorModel/*!*/ errModel,

                                        Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

@@ -3697,7 +3864,7 @@ namespace VC {
       int cfcPartition = errModel.LookupSkolemFunctionAt(cfcName + "!" + info.uniqueId, values);

       int cfcValue = errModel.LookupPartitionValue(cfcPartition);

       

-      Dictionary<Absy, CalleeCounterexampleInfo> calleeCounterexamples = new Dictionary<Absy, CalleeCounterexampleInfo>();

+      var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

       while (true) {

         CmdSeq cmds = b.Cmds;Contract.Assert(cmds != null);

         TransferCmd transferCmd = cce.NonNull(b.TransferCmd);

@@ -3787,7 +3954,7 @@ namespace VC {
             name = context.Lookup(exprVar);

             args.Add(errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values));

           }

-          calleeCounterexamples[assumeCmd] = 

+          calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = 

             new CalleeCounterexampleInfo(

               LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args),

               errModel.PartitionsToValues(args));

@@ -3817,7 +3984,7 @@ namespace VC {
                           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

                           Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

                           ProverContext/*!*/ context, Program/*!*/ program,

-                          Dictionary<Absy/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)

+                          Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)

     {

       Contract.Requires(b != null);

       Contract.Requires(traceNodes != null);

@@ -3874,7 +4041,7 @@ namespace VC {
           Contract.Assert(name != null);

           args.Add(errModel.identifierToPartition[name]);

         }

-        calleeCounterexamples[assumeCmd] = 

+        calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = 

             new CalleeCounterexampleInfo(

                 LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args),

                 errModel.PartitionsToValues(args));