diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 8 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 28 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 134 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 183 |
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));
|