diff options
| -rw-r--r-- | Source/Core/Absy.cs | 10 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.cs | 12 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 22 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 17 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 19 | ||||
| -rw-r--r-- | Test/snapshots/Snapshots22.v0.bpl | 15 | ||||
| -rw-r--r-- | Test/snapshots/Snapshots22.v1.bpl | 15 | ||||
| -rw-r--r-- | Test/snapshots/runtest.snapshot | 2 | ||||
| -rw-r--r-- | Test/snapshots/runtest.snapshot.expect | 8 |
9 files changed, 77 insertions, 43 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 6568eb75..7950feed 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2682,15 +2682,15 @@ namespace Microsoft.Boogie { public ISet<byte[]> AssertionChecksumsInPreviousSnapshot { get; set; }
- public IList<AssertCmd> CannedFailingAssertions { get; protected set; }
+ public IList<AssertCmd> RecycledFailingAssertions { get; protected set; }
- public void AddCannedFailingAssertion(AssertCmd assertion)
+ public void AddRecycledFailingAssertion(AssertCmd assertion)
{
- if (CannedFailingAssertions == null)
+ if (RecycledFailingAssertions == null)
{
- CannedFailingAssertions = new List<AssertCmd>();
+ RecycledFailingAssertions = new List<AssertCmd>();
}
- CannedFailingAssertions.Add(assertion);
+ RecycledFailingAssertions.Add(assertion);
}
// Strongly connected components
diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index 81da2cce..2230db91 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -14,13 +14,13 @@ namespace Microsoft.Boogie { using Set = GSet<object>; // for the purposes here, "object" really means "either Variable or TypeVariable"
public static class LambdaHelper {
- public static Absy Desugar(Absy node, out List<Expr/*!*/>/*!*/ axioms, out List<Function/*!*/>/*!*/ functions) {
- Contract.Requires(node != null);
+ public static Program Desugar(Program program, out List<Expr/*!*/>/*!*/ axioms, out List<Function/*!*/>/*!*/ functions) {
+ Contract.Requires(program != null);
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out functions)));
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out axioms)));
- Contract.Ensures(Contract.Result<Absy>() != null);
+ Contract.Ensures(Contract.Result<Program>() != null);
LambdaVisitor v = new LambdaVisitor();
- node = v.Visit(node);
+ program = v.VisitProgram(program);
axioms = v.lambdaAxioms;
functions = v.lambdaFunctions;
if (CommandLineOptions.Clo.TraceVerify) {
@@ -34,7 +34,7 @@ namespace Microsoft.Boogie { Console.WriteLine();
}
}
- return node;
+ return program;
}
public static void ExpandLambdas(Program prog) {
@@ -60,7 +60,7 @@ namespace Microsoft.Boogie { Contract.Invariant(cce.NonNullElements(lambdaFunctions));
}
- static int lambdaid = 0;
+ int lambdaid = 0;
public override Expr VisitLambdaExpr(LambdaExpr lambda) {
var baseResult = base.VisitLambdaExpr(lambda);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 04726cff..ea69b29e 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -216,12 +216,12 @@ namespace Microsoft.Boogie public class ErrorInformationFactory
{
- public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string category = null)
+ public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string originalRequestId = null, string category = null)
{
Contract.Requires(1 <= tok.line && 1 <= tok.col);
Contract.Requires(msg != null);
- return ErrorInformation.CreateErrorInformation(tok, msg, requestId, category);
+ return ErrorInformation.CreateErrorInformation(tok, msg, requestId, originalRequestId, category);
}
}
@@ -233,6 +233,7 @@ namespace Microsoft.Boogie public string Category { get; set; }
public string BoogieErrorCode { get; set; }
public readonly List<AuxErrorInfo> Aux = new List<AuxErrorInfo>();
+ public string OriginalRequestId { get; set; }
public string RequestId { get; set; }
public ErrorKind Kind { get; set; }
public string ImplementationName { get; set; }
@@ -284,10 +285,11 @@ namespace Microsoft.Boogie Msg = CleanUp(msg);
}
- internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string category = null)
+ internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string originalRequestId = null, string category = null)
{
var result = new ErrorInformation(tok, msg);
result.RequestId = requestId;
+ result.OriginalRequestId = originalRequestId;
result.Category = category;
return result;
}
@@ -1564,39 +1566,39 @@ namespace Microsoft.Boogie var assertError = error as AssertCounterexample;
if (callError != null)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.", callError.RequestId, cause);
+ errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.", callError.RequestId, callError.OriginalRequestId, cause);
errorInfo.BoogieErrorCode = "BP5002";
errorInfo.Kind = ErrorKind.Precondition;
errorInfo.AddAuxInfo(callError.FailingRequires.tok, callError.FailingRequires.ErrorData as string ?? "This is the precondition that might not hold.", "Related location");
if (!CommandLineOptions.Clo.ForceBplErrors && callError.FailingRequires.ErrorMessage != null)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, callError.RequestId, cause);
+ errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, callError.RequestId, callError.OriginalRequestId, cause);
}
}
else if (returnError != null)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, "A postcondition might not hold on this return path.", returnError.RequestId, cause);
+ errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, "A postcondition might not hold on this return path.", returnError.RequestId, returnError.OriginalRequestId, cause);
errorInfo.BoogieErrorCode = "BP5003";
errorInfo.Kind = ErrorKind.Postcondition;
errorInfo.AddAuxInfo(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorData as string ?? "This is the postcondition that might not hold.", "Related location");
if (!CommandLineOptions.Clo.ForceBplErrors && returnError.FailingEnsures.ErrorMessage != null)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, cause);
+ errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, returnError.OriginalRequestId, cause);
}
}
else // error is AssertCounterexample
{
if (assertError.FailingAssert is LoopInitAssertCmd)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not hold on entry.", assertError.RequestId, cause);
+ errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not hold on entry.", assertError.RequestId, assertError.OriginalRequestId, cause);
errorInfo.BoogieErrorCode = "BP5004";
errorInfo.Kind = ErrorKind.InvariantEntry;
}
else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not be maintained by the loop.", assertError.RequestId, cause);
+ errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not be maintained by the loop.", assertError.RequestId, assertError.OriginalRequestId, cause);
errorInfo.BoogieErrorCode = "BP5005";
errorInfo.Kind = ErrorKind.InvariantMaintainance;
}
@@ -1620,7 +1622,7 @@ namespace Microsoft.Boogie bec = "BP5001";
}
- errorInfo = errorInformationFactory.CreateErrorInformation(tok, msg, assertError.RequestId, cause);
+ errorInfo = errorInformationFactory.CreateErrorInformation(tok, msg, assertError.RequestId, assertError.OriginalRequestId, cause);
errorInfo.BoogieErrorCode = bec;
errorInfo.Kind = ErrorKind.Assertion;
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 33f36a31..cdeb6c2c 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -81,6 +81,7 @@ namespace Microsoft.Boogie { public ProverContext Context;
[Peer]
public List<string>/*!>!*/ relatedInformation;
+ public string OriginalRequestId;
public string RequestId;
public abstract byte[] Checksum { get; }
@@ -1103,6 +1104,10 @@ namespace VC { {
ce.RequestId = RequestId;
}
+ if (ce.OriginalRequestId == null)
+ {
+ ce.OriginalRequestId = RequestId;
+ }
examples.Add(ce);
}
@@ -1420,10 +1425,10 @@ namespace VC { byte[] currentChecksum = null;
foreach (Block p in b.Predecessors) {
p.succCount--;
- if (b.Checksum != null)
+ if (p.Checksum != null)
{
// Compute the checksum based on the checksums of the predecessor. The order should not matter.
- currentChecksum = ChecksumHelper.CombineChecksums(b.Checksum, currentChecksum, true);
+ currentChecksum = ChecksumHelper.CombineChecksums(p.Checksum, currentChecksum, true);
}
if (p.succCount == 0)
block2Incarnation.Remove(p);
@@ -1532,11 +1537,13 @@ namespace VC { && currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)
&& (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
{
+ // TODO(wuestholz): Do the same for assertions if they have been proved in the previous snapshot.
+
// Turn it into an assume statement.
- // TODO(wuestholz): Uncomment this once the canned errors are reported.
+ // TODO(wuestholz): Uncomment this.
// pc = new AssumeCmd(ac.tok, copy);
- pc.Attributes = new QKeyValue(Token.NoToken, "canned_failing_assertion", new List<object>(), pc.Attributes);
- currentImplementation.AddCannedFailingAssertion(ac);
+ pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);
+ currentImplementation.AddRecycledFailingAssertion(ac);
}
}
else if (pc is AssumeCmd
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 3e601511..239cecdb 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1620,30 +1620,18 @@ namespace VC { Outcome outcome = Outcome.Correct;
- // Report all canned failing assertions for this implementation.
- if (impl.CannedFailingAssertions != null && impl.CannedFailingAssertions.Any())
+ // Report all recycled failing assertions for this implementation.
+ if (impl.RecycledFailingAssertions != null && impl.RecycledFailingAssertions.Any())
{
// TODO(wuestholz): Uncomment this.
// outcome = Outcome.Errors;
- foreach (var a in impl.CannedFailingAssertions)
+ foreach (var a in impl.RecycledFailingAssertions)
{
var oldCex = impl.ErrorChecksumToCachedError[a.Checksum] as Counterexample;
if (oldCex != null)
{
- // TODO(wuestholz): Maybe we could create a "fresh" counterexample instead.
- // TransferCmd trCmd = null;
- // var oldRetCex = oldCex as ReturnCounterexample;
- // if (oldRetCex != null)
- // {
- // trCmd = oldRetCex.FailingReturn;
- // }
- // var cex = AssertCmdToCounterexample(a, trCmd, oldCex.Trace, oldCex.Model, oldCex.MvInfo, oldCex.Context);
- // cex.RequestId = oldCex.RequestId;
-
// TODO(wuestholz): Uncomment this.
- // var oldReqId = oldCex.RequestId;
// callback.OnCounterexample(oldCex, null);
- // oldCex.RequestId = oldReqId;
}
}
}
@@ -2677,7 +2665,6 @@ namespace VC { #region Get rid of empty blocks
{
RemoveEmptyBlocksIterative(impl.Blocks);
- // TODO(wuestholz): Update impl.AssertionChecksums and maybe impl.CannedFailingAssertions.
impl.PruneUnreachableBlocks();
}
#endregion Get rid of empty blocks
diff --git a/Test/snapshots/Snapshots22.v0.bpl b/Test/snapshots/Snapshots22.v0.bpl new file mode 100644 index 00000000..c2be13de --- /dev/null +++ b/Test/snapshots/Snapshots22.v0.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+ if (*)
+ {
+ assert 1 != 1; // error
+ }
+ else
+ {
+ assert 2 == 2;
+ }
+
+ assert 3 == 3;
+}
diff --git a/Test/snapshots/Snapshots22.v1.bpl b/Test/snapshots/Snapshots22.v1.bpl new file mode 100644 index 00000000..9d43f2c2 --- /dev/null +++ b/Test/snapshots/Snapshots22.v1.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+ if (*)
+ {
+ assert 1 == 1;
+ }
+ else
+ {
+ assert 2 == 2;
+ }
+
+ assert 3 == 3;
+}
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index e73e4eba..e3c00eee 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl > "%t" +// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index daabfca9..f4ee0ca9 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -227,3 +227,11 @@ Execution trace: Snapshots21.v1.bpl(14,5): anon3
Boogie program verifier finished with 0 verified, 2 errors
+Snapshots22.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+Execution trace:
+ Snapshots22.v0.bpl(5,5): anon0
+ Snapshots22.v0.bpl(7,9): anon4_Then
+
+Boogie program verifier finished with 0 verified, 1 error
+
+Boogie program verifier finished with 1 verified, 0 errors
|