Fix for extractLoops

3 files changed, 71 insertions, 64 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index a24347f2..3bf7b624 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -529,9 +529,10 @@ namespace Microsoft.Boogie {
         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

 

+      Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;

       if (CommandLineOptions.Clo.ExtractLoops)

       {

-          program.ExtractLoops();

+          extractLoopMappingInfo = program.ExtractLoops();

       }

 

       if (CommandLineOptions.Clo.PrintInstrumented) {

@@ -660,7 +661,7 @@ namespace Microsoft.Boogie {
                 {

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

                     {

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

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

                     }

                 }

 

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 1d4380bf..8daf39df 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -460,12 +460,17 @@ namespace Microsoft.Boogie {
         loopHeaderToCallCmd[header] = callCmd;

       }

 

+      // Keep track of the new blocks created: maps a header node to the

+      // header_last block that was created because of splitting header.

+      Dictionary<Block, Block> newBlocksCreated = new Dictionary<Block, Block>();

+

       IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance();

       foreach (Block/*!*/ header in sortedHeaders)

       {

         Contract.Assert(header != null);

         LoopProcedure loopProc = loopHeaderToLoopProc[header];

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

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

 

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

         VariableSeq inputs = loopHeaderToInputs[header];

@@ -480,6 +485,13 @@ namespace Microsoft.Boogie {
             newBlock.Label = block.Label;

             newBlock.Cmds = codeCopier.CopyCmdSeq(block.Cmds);

             blockMap[block] = newBlock;

+            if (newBlocksCreated.ContainsKey(block))

+            {

+                Block newBlock2 = new Block();

+                newBlock2.Label = newBlocksCreated[block].Label;

+                newBlock2.Cmds = codeCopier.CopyCmdSeq(newBlocksCreated[block].Cmds);

+                blockMap[newBlocksCreated[block]] = newBlock2;

+            }

           }

           string callee = loopHeaderToLoopProc[header].Name;

           ExprSeq ins = new ExprSeq();

@@ -499,6 +511,7 @@ 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.Label);

 

           GotoCmd gotoCmd = source.TransferCmd as GotoCmd;

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

@@ -571,20 +584,36 @@ namespace Microsoft.Boogie {
         loopImpl.Proc = loopProc;

         loopImpls.Add(loopImpl);

 

+        // Make a (shallow) copy of the header before splitting it

+        Block origHeader = new Block(header.tok, header.Label, header.Cmds, header.TransferCmd);

+

         // Finally, add call to the loop in the containing procedure

         string lastIterBlockName = header.Label + "_last";

         Block lastIterBlock = new Block(Token.NoToken, lastIterBlockName, header.Cmds, header.TransferCmd);

+        newBlocksCreated[header] = lastIterBlock;

         header.Cmds = new CmdSeq(loopHeaderToCallCmd[header]);

         header.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(lastIterBlockName), new BlockSeq(lastIterBlock));

         impl.Blocks.Add(lastIterBlock);

-        blockMap[lastIterBlock] = blockMap[header];

+        blockMap[origHeader] = blockMap[header];

         blockMap.Remove(header);

-        fullMap[impl.Name].Remove(header.Label);

-        fullMap[impl.Name][lastIterBlockName] = lastIterBlock;

+

+        Contract.Assert(fullMap[impl.Name][header.Label] == header);

+        fullMap[impl.Name][header.Label] = origHeader;

+

         foreach (Block block in blockMap.Keys)

         {

-            AddToFullMap(fullMap, loopProc.Name, blockMap[block].Label, block);

+            // Don't add dummy blocks to the map

+            if (dummyBlocks.Contains(blockMap[block].Label)) continue;

+

+            // Following two statements are for nested loops: compose map

+            if (!fullMap[impl.Name].ContainsKey(block.Label)) continue;

+            var target = fullMap[impl.Name][block.Label];

+

+            AddToFullMap(fullMap, loopProc.Name, blockMap[block].Label, target);

         }

+

+        fullMap[impl.Name].Remove(header.Label);

+        fullMap[impl.Name][lastIterBlockName] = origHeader;

       }

     }

 

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index a906f137..4591691a 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -3670,7 +3670,7 @@ namespace VC {
       return gotoCmdOrigins;

     }

 

-    public Counterexample extractLoopTrace(Counterexample cex, Program program)

+    public Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)

     {

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

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

@@ -3679,25 +3679,33 @@ namespace VC {
         Debug.Assert(implName2LazyInliningInfo.Count == 0 || implName2StratifiedInliningInfo.Count == 0);

 

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

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

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

         foreach (var decl in program.TopLevelDeclarations)

         {

-            if (decl is Implementation)

+            if (decl is Procedure)

             {

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

-                if (!elIsLoop(name))

+                if (!(decl is LoopProcedure))

                 {

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

+                    var p = decl as Procedure;

+                    inlinedProcs.Add(p.Name, p);

                 }

             }

         }

 

-        return extractLoopTraceRec(cex, null, inlinedProcs);

+        return extractLoopTraceRec(

+            new CalleeCounterexampleInfo(cex, new List<object>()),

+            mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;

     }

 

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

+    private CalleeCounterexampleInfo extractLoopTraceRec(

+        CalleeCounterexampleInfo cexInfo, string currProc,

+        Dictionary<string, Procedure> inlinedProcs, 

+        Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)

     {

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

+        Contract.Requires(currProc != null);

+

+        var cex = cexInfo.counterexample;

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

         var ret = cex.Clone();

         ret.Trace = new BlockSeq();

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

@@ -3705,7 +3713,7 @@ namespace VC {
         for (int numBlock = 0; numBlock < cex.Trace.Length; numBlock ++ )

         {

             Block block = cex.Trace[numBlock];

-            var origBlock = elGetBlock(currProc, block);

+            var origBlock = elGetBlock(currProc, block, extractLoopMappingInfo);

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

             var callCnt = 1;

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

@@ -3713,58 +3721,41 @@ namespace VC {
                 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;

+                Contract.Assert(callee != null);

+                var calleeTrace = cex.calleeCounterexamples[loc];

                 Debug.Assert(calleeTrace != null);

 

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

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

 

                 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);

+                    int currLen = ret.Trace.Length;

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

 

-                    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)

+                    foreach (var kvp in origTrace.counterexample.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>()));

+                    ret.calleeCounterexamples.Add(origLoc, origTrace);

                     callCnt++;

                 }

             }

         }

-        return ret;

+        return new CalleeCounterexampleInfo(ret, cexInfo.args);

     }

 

     // 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)

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

     {

         Debug.Assert(i >= 1);

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

@@ -3809,11 +3800,7 @@ namespace VC {
 

     private bool elIsLoop(string procname)

     {

-        if (procname == null)

-        {

-            // we're in main

-            return false;

-        }

+        Contract.Requires(procname != null);

 

         LazyInliningInfo info = null;

         if (implName2LazyInliningInfo.ContainsKey(procname))

@@ -3833,27 +3820,17 @@ namespace VC {
         return true;

     }

 

-    private Block elGetBlock(string procname, Block block)

+    private Block elGetBlock(string procname, Block block, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)

     {

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

+        Contract.Requires(procname != null);

 

-        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;

+        if (!extractLoopMappingInfo.ContainsKey(procname))

+            return block;

 

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

-

-        if(lp == null) return null;

+        if (!extractLoopMappingInfo[procname].ContainsKey(block.Label))

+            return null;

 

-        return lp.getBlock(block.Label);

+        return extractLoopMappingInfo[procname][block.Label];

     }

 

     private static Counterexample LazyCounterexample(