summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/ExecutionEngine/VerificationResultCache.cs19
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs49
2 files changed, 33 insertions, 35 deletions
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 7f33ecef..ee9a7f73 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Boogie
var wr = new StringWriter();
if (runs.Any())
{
- wr.WriteLine("\nCached verification result injector statistics as CSV:");
+ wr.WriteLine("Cached verification result injector statistics as CSV:");
if (printTime)
{
wr.WriteLine("Request ID, Time (ms), Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");
@@ -206,7 +206,7 @@ namespace Microsoft.Boogie
var precond = node.CheckedPrecondition(oldProc, Program);
if (precond != null)
{
- var assume = new AssumeCmd(Token.NoToken, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
+ var assume = new AssumeCmd(node.tok, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
beforePrecondtionCheck.Add(assume);
}
@@ -240,7 +240,7 @@ namespace Microsoft.Boogie
currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);
var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);
- var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
+ var assumed = new AssignCmd(node.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
after.Add(assumed);
}
@@ -249,20 +249,21 @@ namespace Microsoft.Boogie
{
using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
{
- Console.Out.WriteLine("\nFor call to {0} in {1}:", node.Proc.Name, currentImplementation.Name);
+ var loc = node.tok != null && node.tok != Token.NoToken ? string.Format("{0}({1},{2})", node.tok.filename, node.tok.line, node.tok.col) : "<unknown location>";
+ Console.Out.WriteLine("Processing call to procedure {0} in implementation {1} (at {2}):", node.Proc.Name, currentImplementation.Name, loc);
foreach (var b in before)
{
- Console.Out.Write("+ Added before: ");
+ Console.Out.Write(" >>> added before: ");
b.Emit(tokTxtWr, 0);
}
foreach (var b in beforePrecondtionCheck)
{
- Console.Out.Write("+ Added before precondition check: ");
+ Console.Out.Write(" >>> added before precondition check: ");
b.Emit(tokTxtWr, 0);
}
foreach (var a in after)
{
- Console.Out.Write("+ Added after: ");
+ Console.Out.Write(" >>> added after: ");
a.Emit(tokTxtWr, 0);
}
}
@@ -294,7 +295,7 @@ namespace Microsoft.Boogie
var end = DateTime.UtcNow;
if (3 <= CommandLineOptions.Clo.TraceCaching)
{
- Console.Out.WriteLine("\nCollected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
+ Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
}
}
@@ -342,7 +343,7 @@ namespace Microsoft.Boogie
var end = DateTime.UtcNow;
if (3 <= CommandLineOptions.Clo.TraceCaching)
{
- Console.Out.WriteLine("\nCollected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
+ Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
}
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 6fa26967..64a85171 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1336,10 +1336,10 @@ namespace VC {
Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
var end = DateTime.UtcNow;
+
if (3 <= CommandLineOptions.Clo.TraceCaching)
{
- Console.Out.WriteLine("\nTurned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds);
-
+ Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds);
}
if (2 <= CommandLineOptions.Clo.TraceCaching)
@@ -1470,22 +1470,23 @@ namespace VC {
return Substituter.SubstitutionFromHashtable(oldFrameMap);
}
- void TraceCachingTransformation(Cmd from, string message, Cmd to = null)
+ void TraceCaching(Cmd from, string message, Cmd to = null)
{
if (1 <= CommandLineOptions.Clo.TraceCaching)
{
- Console.WriteLine("");
using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
{
+ var loc = from.tok != null && from.tok != Token.NoToken ? string.Format("{0}({1},{2})", from.tok.filename, from.tok.line, from.tok.col) : "<unknown location>";
+ Console.Write("Processing command (at {0}) ", loc);
from.Emit(tokTxtWr, 0);
- Console.Write(message);
+ Console.Out.Write(" {0}", message);
if (to != null)
{
to.Emit(tokTxtWr, 0);
}
else
{
- Console.WriteLine("");
+ Console.Out.WriteLine();
}
}
}
@@ -1538,11 +1539,11 @@ namespace VC {
&& !currentImplementation.AnyErrorsInCachedSnapshot
&& currentImplementation.InjectedAssumptionVariables.Count == 1)
{
- TraceCachingTransformation(pc, "==> did nothing\n");
+ TraceCaching(pc, ">>> did nothing");
}
else if (relevantDoomedAssumpVars.Any())
{
- TraceCachingTransformation(pc, "==> did nothing\n");
+ TraceCaching(pc, ">>> did nothing");
}
else if (currentImplementation != null
&& currentImplementation.HasCachedSnapshot
@@ -1561,19 +1562,17 @@ namespace VC {
ac.IncarnationMap[incarnation] = identExpr;
passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));
copy = identExpr;
- var a = new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr));
- passiveCmds.Add(a);
- TraceCachingTransformation(pc, "== marked as partially verified ==> ", a);
+ passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));
+ TraceCaching(pc, string.Format(">>> added assume statement for assertion that has been partially verified under \"{0}\"", assmVars));
}
else if (isTrue)
{
if (alwaysUseSubsumption)
{
// Turn it into an assume statement.
- var a = new AssumeCmd(ac.tok, copy);
- a.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), a.Attributes);
- TraceCachingTransformation(pc, "== marked as fully verified ==> ", a);
- pc = a;
+ TraceCaching(pc, ">>> turned assertion into assume statement");
+ pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
}
dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
}
@@ -1588,10 +1587,9 @@ namespace VC {
if (alwaysUseSubsumption)
{
// Turn it into an assume statement.
- var a = new AssumeCmd(ac.tok, copy);
- a.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), a.Attributes);
- TraceCachingTransformation(pc, "== recycled error ==> ", a);
- pc = a;
+ TraceCaching(pc, ">>> recycled error and turned assertion into assume statement");
+ pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);
}
dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
if (dropCmd || alwaysUseSubsumption)
@@ -1601,7 +1599,7 @@ namespace VC {
}
else
{
- TraceCachingTransformation(pc, "==> did nothing\n");
+ TraceCaching(pc, ">>> did nothing");
}
}
else if (pc is AssumeCmd
@@ -1618,11 +1616,11 @@ namespace VC {
if (!isTrue)
{
copy = LiteralExpr.Imp(assmVars, copy);
- TraceCachingTransformation(pc, "==> marked as partially verified\n");
+ TraceCaching(pc, string.Format(">>> marked as partially verified under \"{0}\"", assmVars));
}
else
{
- TraceCachingTransformation(pc, "==> marked as full verified\n");
+ TraceCaching(pc, ">>> marked as full verified");
}
}
else
@@ -1637,7 +1635,7 @@ namespace VC {
}
else
{
- TraceCachingTransformation(pc, "==> dropped\n");
+ TraceCaching(pc, ">>> dropped");
}
}
#endregion
@@ -1720,9 +1718,8 @@ namespace VC {
Expr incarnation;
if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && incarnationMap.TryGetValue(identExpr.Decl, out incarnation))
{
- var a = new AssumeCmd(c.tok, Expr.Not(incarnation));
- TraceCachingTransformation(assign, "== assumed negation of single assumption variable ==> ", a);
- passiveCmds.Add(a);
+ TraceCaching(assign, string.Format(">>> added assume statement for negation of single assumption variable \"{0}\"", identExpr.Decl.Name));
+ passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation)));
}
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 08:46:47 +0000