diff options
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 33 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 68 |
2 files changed, 72 insertions, 29 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 85ceb8e3..0b76387d 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2485,6 +2485,39 @@ namespace VC }
}
+ public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
+ {
+ // Construct the set of inlined procs in the original program
+ var inlinedProcs = new HashSet<string>();
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ // Implementations
+ if (decl is Implementation)
+ {
+ var impl = decl as Implementation;
+ if (!(impl.Proc is LoopProcedure))
+ {
+ inlinedProcs.Add(impl.Name);
+ }
+ }
+
+ // And recording procedures
+ if (decl is Procedure)
+ {
+ var proc = decl as Procedure;
+ if (proc.Name.StartsWith(recordProcName))
+ {
+ Debug.Assert(!(decl is LoopProcedure));
+ inlinedProcs.Add(proc.Name);
+ }
+ }
+ }
+
+ return extractLoopTraceRec(
+ new CalleeCounterexampleInfo(cex, new List<object>()),
+ mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
+ }
+
protected override bool elIsLoop(string procname)
{
LazyInliningInfo info = null;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 11db59b0..7c981a0c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2463,18 +2463,18 @@ namespace VC { }
}
- public Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
+ public virtual Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
{
// Construct the set of inlined procs in the original program
- var inlinedProcs = new Dictionary<string, Procedure>();
+ var inlinedProcs = new HashSet<string>();
foreach (var decl in program.TopLevelDeclarations)
{
if (decl is Procedure)
- {
+ {
if (!(decl is LoopProcedure))
{
var p = decl as Procedure;
- inlinedProcs.Add(p.Name, p);
+ inlinedProcs.Add(p.Name);
}
}
}
@@ -2484,9 +2484,9 @@ namespace VC { mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
}
- private CalleeCounterexampleInfo extractLoopTraceRec(
+ protected CalleeCounterexampleInfo extractLoopTraceRec(
CalleeCounterexampleInfo cexInfo, string currProc,
- Dictionary<string, Procedure> inlinedProcs,
+ HashSet<string> inlinedProcs,
Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
{
Contract.Requires(currProc != null);
@@ -2507,7 +2507,11 @@ namespace VC { 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;
+ if (!cex.calleeCounterexamples.ContainsKey(loc))
+ {
+ if (getCallee(cex.getTraceCmd(loc), inlinedProcs) != null) callCnt++;
+ continue;
+ }
string callee = cex.getCalledProcName(cex.getTraceCmd(loc));
Contract.Assert(callee != null);
var calleeTrace = cex.calleeCounterexamples[loc];
@@ -2543,33 +2547,13 @@ namespace VC { // 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, Procedure> inlinedProcs, string callee)
+ private int getCallCmdPosition(Block block, int i, HashSet<string> inlinedProcs, string callee)
{
Debug.Assert(i >= 1);
for (int pos = 0; pos < block.Cmds.Length; pos++)
{
Cmd cmd = block.Cmds[pos];
- string procCalled = null;
- if (cmd is CallCmd)
- {
- var cc = (CallCmd)cmd;
- if (inlinedProcs.ContainsKey(cc.Proc.Name))
- {
- procCalled = cc.Proc.Name;
- }
- }
-
- if (cmd is AssumeCmd)
- {
- var expr = (cmd as AssumeCmd).Expr as NAryExpr;
- if (expr != null)
- {
- if (inlinedProcs.ContainsKey(expr.Fun.FunctionName))
- {
- procCalled = expr.Fun.FunctionName;
- }
- }
- }
+ string procCalled = getCallee(cmd, inlinedProcs);
if (procCalled != null)
{
@@ -2586,6 +2570,32 @@ namespace VC { return -1;
}
+ private string getCallee(Cmd cmd, HashSet<string> inlinedProcs)
+ {
+ string procCalled = null;
+ if (cmd is CallCmd)
+ {
+ var cc = (CallCmd)cmd;
+ if (inlinedProcs.Contains(cc.Proc.Name))
+ {
+ procCalled = cc.Proc.Name;
+ }
+ }
+
+ if (cmd is AssumeCmd)
+ {
+ var expr = (cmd as AssumeCmd).Expr as NAryExpr;
+ if (expr != null)
+ {
+ if (inlinedProcs.Contains(expr.Fun.FunctionName))
+ {
+ procCalled = expr.Fun.FunctionName;
+ }
+ }
+ }
+ return procCalled;
+ }
+
protected virtual bool elIsLoop(string procname)
{
Contract.Requires(procname != null);
|