From 6541ac9ebb538c339f818e9d473e09c5207f23ae Mon Sep 17 00:00:00 2001 From: akashlal Date: Sat, 4 Sep 2010 20:17:06 +0000 Subject: Fix for extractLoops --- Source/BoogieDriver/BoogieDriver.cs | 5 +- Source/Core/Absy.cs | 37 +++++++++++++-- Source/VCGeneration/VC.cs | 93 ++++++++++++++----------------------- 3 files changed, 71 insertions(+), 64 deletions(-) (limited to 'Source') 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> 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 newBlocksCreated = new Dictionary(); + IEnumerable sortedHeaders = g.SortHeadersByDominance(); foreach (Block/*!*/ header in sortedHeaders) { Contract.Assert(header != null); LoopProcedure loopProc = loopHeaderToLoopProc[header]; Dictionary blockMap = new Dictionary(); + Set dummyBlocks = new Set(); 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> 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(); + var inlinedProcs = new Dictionary(); 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()), + mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample; } - private Counterexample extractLoopTraceRec(Counterexample cex, string currProc, Dictionary inlinedProcs) + private CalleeCounterexampleInfo extractLoopTraceRec( + CalleeCounterexampleInfo cexInfo, string currProc, + Dictionary inlinedProcs, + Dictionary> 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(); @@ -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())); + 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 inlinedProcs, string callee) + private int getCallCmdPosition(Block block, int i, Dictionary 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> 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( -- cgit v1.2.3