From a030a9cd291e5d17d09a8d1921ae5a9c9c01c2dd Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 20 Jul 2015 07:12:43 +0200 Subject: Added more tests. --- Test/snapshots/Snapshots38.v0.bpl | 13 ++++++++ Test/snapshots/Snapshots38.v1.bpl | 14 ++++++++ Test/snapshots/Snapshots38.v2.bpl | 14 ++++++++ Test/snapshots/Snapshots39.v0.bpl | 13 ++++++++ Test/snapshots/Snapshots39.v1.bpl | 14 ++++++++ Test/snapshots/Snapshots39.v2.bpl | 14 ++++++++ Test/snapshots/runtest.snapshot | 2 +- Test/snapshots/runtest.snapshot.expect | 60 ++++++++++++++++++++++++++++++++++ 8 files changed, 143 insertions(+), 1 deletion(-) create mode 100644 Test/snapshots/Snapshots38.v0.bpl create mode 100644 Test/snapshots/Snapshots38.v1.bpl create mode 100644 Test/snapshots/Snapshots38.v2.bpl create mode 100644 Test/snapshots/Snapshots39.v0.bpl create mode 100644 Test/snapshots/Snapshots39.v1.bpl create mode 100644 Test/snapshots/Snapshots39.v2.bpl diff --git a/Test/snapshots/Snapshots38.v0.bpl b/Test/snapshots/Snapshots38.v0.bpl new file mode 100644 index 00000000..496a75a9 --- /dev/null +++ b/Test/snapshots/Snapshots38.v0.bpl @@ -0,0 +1,13 @@ +procedure {:checksum "-1"} Callee(); + +implementation {:id "Callee"} {:checksum "0"} Callee() +{ + var r: int; + + call r := Sum(42); + assert r != 0; +} + +procedure {:checksum "1"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures n != 0 ==> 1 <= r; diff --git a/Test/snapshots/Snapshots38.v1.bpl b/Test/snapshots/Snapshots38.v1.bpl new file mode 100644 index 00000000..062b22ea --- /dev/null +++ b/Test/snapshots/Snapshots38.v1.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "-1"} Callee(); + +implementation {:id "Callee"} {:checksum "2"} Callee() +{ + var r: int; + + call r := Sum(42); + assert r != 0; + assert 42 <= r; +} + +procedure {:checksum "1"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures n != 0 ==> 1 <= r; diff --git a/Test/snapshots/Snapshots38.v2.bpl b/Test/snapshots/Snapshots38.v2.bpl new file mode 100644 index 00000000..5c4b69d6 --- /dev/null +++ b/Test/snapshots/Snapshots38.v2.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "-1"} Callee(); + +implementation {:id "Callee"} {:checksum "2"} Callee() +{ + var r: int; + + call r := Sum(42); + assert r != 0; + assert 42 <= r; +} + +procedure {:checksum "3"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures n != 0 ==> n <= r; diff --git a/Test/snapshots/Snapshots39.v0.bpl b/Test/snapshots/Snapshots39.v0.bpl new file mode 100644 index 00000000..083d497e --- /dev/null +++ b/Test/snapshots/Snapshots39.v0.bpl @@ -0,0 +1,13 @@ +procedure {:checksum "-1"} Callee(); + +implementation {:id "Callee"} {:checksum "0"} Callee() +{ + var r: int; + + call r := Sum(42); + assert r != 0; +} + +procedure {:checksum "1"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures n <= r; diff --git a/Test/snapshots/Snapshots39.v1.bpl b/Test/snapshots/Snapshots39.v1.bpl new file mode 100644 index 00000000..09850bfc --- /dev/null +++ b/Test/snapshots/Snapshots39.v1.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "-1"} Callee(); + +implementation {:id "Callee"} {:checksum "2"} Callee() +{ + var r: int; + + call r := Sum(42); + assert r != 0; + assert r == (42 * 43) div 2; +} + +procedure {:checksum "1"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures n <= r; diff --git a/Test/snapshots/Snapshots39.v2.bpl b/Test/snapshots/Snapshots39.v2.bpl new file mode 100644 index 00000000..4bdc4b6e --- /dev/null +++ b/Test/snapshots/Snapshots39.v2.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "-1"} Callee(); + +implementation {:id "Callee"} {:checksum "2"} Callee() +{ + var r: int; + + call r := Sum(42); + assert r != 0; + assert r == (42 * 43) div 2; +} + +procedure {:checksum "3"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures r == (n * (n + 1)) div 2; diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index d4e18910..4baa5edb 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer 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 Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl Snapshots37.bpl > "%t" +// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer 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 Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl Snapshots37.bpl Snapshots38.bpl Snapshots39.bpl > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 4ef6bd20..b3c08d3b 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -666,3 +666,63 @@ Processing command (at Snapshots37.v1.bpl(8,5)) assert l[0]; Snapshots37.v1.bpl(8,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots38.v0.bpl(7,5)) assert 0 <= call0formal#AT#n; + >>> DoNothingToAssert +Processing command (at Snapshots38.v0.bpl(8,5)) assert r != 0; + >>> DoNothingToAssert + +Boogie program verifier finished with 1 verified, 0 errors +Processing command (at Snapshots38.v1.bpl(7,5)) assert 0 <= call0formal#AT#n; + >>> MarkAsFullyVerified +Processing command (at Snapshots38.v1.bpl(8,5)) assert r != 0; + >>> MarkAsFullyVerified +Processing command (at Snapshots38.v1.bpl(9,5)) assert 42 <= r; + >>> DoNothingToAssert +Snapshots38.v1.bpl(9,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing call to procedure Sum in implementation Callee (at Snapshots38.v2.bpl(7,5)): + >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n)) + >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n != 0 ==> 1 <= call1formal#AT#r)) + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r); +Processing command (at Snapshots38.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> MarkAsFullyVerified +Processing command (at Snapshots38.v2.bpl(7,5)) assert 0 <= call0formal#AT#n; + >>> MarkAsFullyVerified +Processing command (at Snapshots38.v2.bpl(8,5)) assert r != 0; + >>> MarkAsPartiallyVerified +Processing command (at Snapshots38.v2.bpl(9,5)) assert 42 <= r; + >>> DoNothingToAssert + +Boogie program verifier finished with 1 verified, 0 errors +Processing command (at Snapshots39.v0.bpl(7,5)) assert 0 <= call0formal#AT#n; + >>> DoNothingToAssert +Processing command (at Snapshots39.v0.bpl(8,5)) assert r != 0; + >>> DoNothingToAssert + +Boogie program verifier finished with 1 verified, 0 errors +Processing command (at Snapshots39.v1.bpl(7,5)) assert 0 <= call0formal#AT#n; + >>> MarkAsFullyVerified +Processing command (at Snapshots39.v1.bpl(8,5)) assert r != 0; + >>> MarkAsFullyVerified +Processing command (at Snapshots39.v1.bpl(9,5)) assert r == 42 * 43 div 2; + >>> DoNothingToAssert +Snapshots39.v1.bpl(9,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing call to procedure Sum in implementation Callee (at Snapshots39.v2.bpl(7,5)): + >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n)) + >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r)) + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r); +Processing command (at Snapshots39.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> MarkAsFullyVerified +Processing command (at Snapshots39.v2.bpl(7,5)) assert 0 <= call0formal#AT#n; + >>> MarkAsFullyVerified +Processing command (at Snapshots39.v2.bpl(8,5)) assert r != 0; + >>> MarkAsPartiallyVerified +Processing command (at Snapshots39.v2.bpl(9,5)) assert r == 42 * 43 div 2; + >>> DoNothingToAssert + +Boogie program verifier finished with 1 verified, 0 errors -- cgit v1.2.3 From e73f2c6d74853664b935096ec832cab4cb474ca8 Mon Sep 17 00:00:00 2001 From: Akash Lal Date: Mon, 20 Jul 2015 11:00:48 +0530 Subject: Minor additions to VC gen --- Source/VCGeneration/StratifiedVC.cs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 0e598267..789f86f5 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -584,9 +584,6 @@ namespace VC { vcgen.ConvertCFG2DAG(impl); vcgen.PassifyImpl(impl, out mvInfo); - if (PassiveImplInstrumentation != null) - PassiveImplInstrumentation(impl); - VCExpressionGenerator gen = proverInterface.VCExprGen; var exprGen = proverInterface.Context.ExprGen; var translator = proverInterface.Context.BoogieExprTranslator; @@ -599,6 +596,9 @@ namespace VC { vcgen.InstrumentCallSites(impl); + if (PassiveImplInstrumentation != null) + PassiveImplInstrumentation(impl); + label2absy = new Dictionary(); VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context); translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition); @@ -639,6 +639,7 @@ namespace VC { public abstract class StratifiedVCGenBase : VCGen { public readonly static string recordProcName = "boogie_si_record"; + public readonly static string callSiteVarAttr = "callSiteVar"; public Dictionary implName2StratifiedInliningInfo; public ProverInterface prover; @@ -699,7 +700,9 @@ namespace VC { if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue; Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "SICS" + callSiteId, Microsoft.Boogie.Type.Bool)); implementation.LocVars.Add(callSiteVar); - newCmds.Add(new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar))); + var toInsert = new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar), + new QKeyValue(Token.NoToken, callSiteVarAttr, new List(), null)); + newCmds.Add(toInsert); callSiteId++; } block.Cmds = newCmds; -- cgit v1.2.3 From 740f004792b49e59f3980150cb8d543737adbc4b Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 20 Jul 2015 18:43:27 +0200 Subject: Added another test. --- Test/snapshots/Snapshots40.v0.bpl | 14 ++++++++++++ Test/snapshots/Snapshots40.v1.bpl | 15 +++++++++++++ Test/snapshots/Snapshots40.v2.bpl | 15 +++++++++++++ Test/snapshots/runtest.snapshot | 2 +- Test/snapshots/runtest.snapshot.expect | 39 ++++++++++++++++++++++++++++++++++ 5 files changed, 84 insertions(+), 1 deletion(-) create mode 100644 Test/snapshots/Snapshots40.v0.bpl create mode 100644 Test/snapshots/Snapshots40.v1.bpl create mode 100644 Test/snapshots/Snapshots40.v2.bpl diff --git a/Test/snapshots/Snapshots40.v0.bpl b/Test/snapshots/Snapshots40.v0.bpl new file mode 100644 index 00000000..27839752 --- /dev/null +++ b/Test/snapshots/Snapshots40.v0.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "-1"} Foo(b: bool); + +implementation {:id "Foo"} {:checksum "0"} Foo(b: bool) +{ + var r: int; + + assert b; + call r := Sum(42); + assert r != 0; +} + +procedure {:checksum "1"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures n <= r; diff --git a/Test/snapshots/Snapshots40.v1.bpl b/Test/snapshots/Snapshots40.v1.bpl new file mode 100644 index 00000000..e1c505f8 --- /dev/null +++ b/Test/snapshots/Snapshots40.v1.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "-1"} Foo(b: bool); + +implementation {:id "Foo"} {:checksum "2"} Foo(b: bool) +{ + var r: int; + + assert b; + call r := Sum(42); + assert r != 0; + assert r == (42 * 43) div 2; +} + +procedure {:checksum "1"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures n <= r; diff --git a/Test/snapshots/Snapshots40.v2.bpl b/Test/snapshots/Snapshots40.v2.bpl new file mode 100644 index 00000000..842d33f5 --- /dev/null +++ b/Test/snapshots/Snapshots40.v2.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "-1"} Foo(b: bool); + +implementation {:id "Foo"} {:checksum "2"} Foo(b: bool) +{ + var r: int; + + assert b; + call r := Sum(42); + assert r != 0; + assert r == (42 * 43) div 2; +} + +procedure {:checksum "3"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures r == (n * (n + 1)) div 2; diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index 4baa5edb..f410a885 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer 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 Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl Snapshots37.bpl Snapshots38.bpl Snapshots39.bpl > "%t" +// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer 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 Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl Snapshots37.bpl Snapshots38.bpl Snapshots39.bpl Snapshots40.bpl > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index b3c08d3b..c398de78 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -726,3 +726,42 @@ Processing command (at Snapshots39.v2.bpl(9,5)) assert r == 42 * 43 div 2; >>> DoNothingToAssert Boogie program verifier finished with 1 verified, 0 errors +Processing command (at Snapshots40.v0.bpl(7,5)) assert b; + >>> DoNothingToAssert +Processing command (at Snapshots40.v0.bpl(8,5)) assert 0 <= call0formal#AT#n; + >>> DoNothingToAssert +Processing command (at Snapshots40.v0.bpl(9,5)) assert r != 0; + >>> DoNothingToAssert +Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots40.v1.bpl(7,5)) assert b; + >>> RecycleError +Processing command (at Snapshots40.v1.bpl(8,5)) assert 0 <= call0formal#AT#n; + >>> MarkAsFullyVerified +Processing command (at Snapshots40.v1.bpl(9,5)) assert r != 0; + >>> MarkAsFullyVerified +Processing command (at Snapshots40.v1.bpl(10,5)) assert r == 42 * 43 div 2; + >>> DoNothingToAssert +Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold. +Snapshots40.v1.bpl(10,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 2 errors +Processing call to procedure Sum in implementation Foo (at Snapshots40.v2.bpl(8,5)): + >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n)) + >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r)) + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r); +Processing command (at Snapshots40.v2.bpl(7,5)) assert b; + >>> RecycleError +Processing command (at Snapshots40.v2.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> MarkAsFullyVerified +Processing command (at Snapshots40.v2.bpl(8,5)) assert 0 <= call0formal#AT#n; + >>> MarkAsFullyVerified +Processing command (at Snapshots40.v2.bpl(9,5)) assert r != 0; + >>> MarkAsPartiallyVerified +Processing command (at Snapshots40.v2.bpl(10,5)) assert r == 42 * 43 div 2; + >>> DoNothingToAssert +Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error -- cgit v1.2.3