diff options
Diffstat (limited to 'Test/dafny0/Fuel.dfy')
| -rw-r--r-- | Test/dafny0/Fuel.dfy | 462 |
1 files changed, 462 insertions, 0 deletions
diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy new file mode 100644 index 00000000..a768db02 --- /dev/null +++ b/Test/dafny0/Fuel.dfy @@ -0,0 +1,462 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module TestModule1 {
+ function pos(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos(x - 1)
+ }
+
+ method test(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert pos(z) == 0;
+ assert pos(-1) == 0;
+ assert pos(y) == 3 + pos(y - 3); // error: Should fail, due to lack of fuel
+ assert pos(y) == 4 + pos(y - 4); // Succeeds, thanks to the assume from the preceding assert
+ }
+}
+
+// Test with function-level fuel boost
+module TestModule2 {
+ function {:fuel 3} pos1(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos1(x - 1)
+ }
+
+ function {:fuel 3,5} pos2(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos2(x - 1)
+ }
+
+ function {:fuel 3,5} pos3(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos3(x - 1)
+ }
+
+ function {:opaque} {:fuel 3,5} pos4(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos3(x - 1)
+ }
+
+ method test(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert pos1(z) == 0;
+ assert pos1(-1) == 0;
+ assert pos1(y) == 3 + pos1(y - 3);
+ assert pos1(y) == 4 + pos1(y - 4);
+
+ assert pos2(z) == 0;
+ assert pos2(-1) == 0;
+ assert pos2(y) == 3 + pos2(y - 3);
+ assert pos2(y) == 4 + pos2(y - 4);
+
+ if (*) {
+ assert pos3(y) == 5 + pos3(y - 5); // Just enough fuel to get here
+ } else {
+ assert pos3(y) == 6 + pos3(y - 6); // error: Should fail even with a boost, since boost is too small
+ }
+
+ if (*) {
+ assert pos4(z) == 0; // error: Fuel shouldn't overcome opaque
+ } else {
+ reveal_pos4();
+ assert pos4(y) == 5 + pos4(y - 5); // With reveal, everything should work as above
+ }
+
+
+ }
+}
+
+
+module TestModule3 {
+ // This fuel setting is equivalent to opaque, except for literals
+ function {:fuel 0,0} pos(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos(x - 1)
+ }
+
+ method test(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert pos(z) == 0; // error: Opaque setting hides body
+ assert pos(-1) == 0; // Passes, since Dafny's computation mode for lits ignore fuel
+ assert pos(y) == 3 + pos(y - 3);// error: Opaque setting hides body
+ }
+}
+
+// Test fuel settings via different contexts
+module TestModule4 {
+ function pos(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos(x - 1)
+ }
+
+ // Should pass
+ method {:fuel pos,3,5} test1(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert pos(z) == 0;
+ assert pos(-1) == 0;
+ assert pos(y) == 3 + pos(y - 3);
+ }
+
+ method {:fuel pos,0,0} test2(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert pos(z) == 0; // error: Should fail due to "opaque" fuel setting
+ assert pos(-1) == 0;
+ assert pos(y) == 3 + pos(y - 3); // error: Should fail due to "opaque" fuel setting
+ }
+
+ method test3(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert {:fuel pos,0,0} pos(z) == 0; // error: fuel can't be decreased
+ assert pos(-1) == 0;
+ if (*) {
+ assert pos(y) == 3 + pos(y - 3); // error: Should fail without extra fuel setting
+ assert pos(y) == 6 + pos(y - 6); // error: Should fail even with previous assert turned into assume
+ } else {
+ assert {:fuel pos,3,5} pos(y) == 3 + pos(y - 3); // Should succeed with extra fuel setting
+ assert pos(y) == 6 + pos(y - 6); // Should succeed thanks to previous assert turned into assume
+ }
+ }
+
+ method test4(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ forall t:int {:fuel pos,3} | t > 0
+ ensures true;
+ {
+ assert pos(y) == 3 + pos(y - 3); // Expected to pass, due to local fuel boost
+ }
+
+ if (*) {
+ calc {:fuel pos,3} {
+ pos(y);
+ 3 + pos(y - 3);
+ }
+ }
+
+ assert pos(y) == 3 + pos(y - 3); // error: Should fail, due to lack of fuel outside the forall
+ }
+}
+
+// Test fuel settings via different module contexts
+module TestModule5 {
+ // Test module level fuel settings, with nested modules
+
+ module TestModule5a {
+ module {:fuel TestModule5aiA.pos,3} TestModule5ai {
+ module TestModule5aiA {
+ function pos(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos(x - 1)
+ }
+
+ method test(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert pos(z) == 0;
+ assert pos(-1) == 0;
+ assert pos(y) == 3 + pos(y - 3); // Should pass due to intermediate module's fuel setting
+ }
+ }
+
+ method test(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert TestModule5aiA.pos(z) == 0;
+ assert TestModule5aiA.pos(-1) == 0;
+ assert TestModule5aiA.pos(y) == 3 + TestModule5aiA.pos(y - 3); // Should pass due to module level fuel
+ }
+ }
+
+ method test(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert TestModule5ai.TestModule5aiA.pos(z) == 0;
+ assert TestModule5ai.TestModule5aiA.pos(-1) == 0;
+ assert TestModule5ai.TestModule5aiA.pos(y) == 3 + TestModule5ai.TestModule5aiA.pos(y - 3); // error: Should fail, due to lack of fuel
+ }
+ }
+
+ module {:fuel TestModule5bi.TestModule5biA.pos,3} TestModule5b {
+ module TestModule5bi {
+ module TestModule5biA {
+ function pos(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos(x - 1)
+ }
+
+ method test(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert pos(z) == 0;
+ assert pos(-1) == 0;
+ assert pos(y) == 3 + pos(y - 3); // Should succceed due to outer module fuel setting
+ }
+ }
+ }
+ }
+}
+
+// Test fuel setting for multiple functions
+module TestModule6 {
+ function pos(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos(x - 1)
+ }
+
+ function neg(x:int) : int
+ decreases 1 - x;
+ {
+ if x > 0 then 0
+ else 1 + neg(x + 1)
+ }
+
+ method test1(y:int, z:int)
+ requires y > 5;
+ requires z < 5;
+ {
+ assert pos(y) == 3 + pos(y - 3); // error: Should fail, due to lack of fuel
+
+ assert neg(z) == 3 + neg(z + 3); // error: Should fail, due to lack of fuel
+ }
+
+ method {:fuel pos,3} {:fuel neg,4} test2(y:int, z:int)
+ requires y > 5;
+ requires z < -5;
+ {
+ assert pos(y) == 3 + pos(y - 3);
+
+ assert neg(z) == 3 + neg(z + 3);
+ }
+}
+
+// Test fuel settings with multiple overlapping contexts
+module TestModule7 {
+ function {:fuel 3} pos(x:int) : int
+ {
+ if x < 0 then 0
+ else 1 + pos(x - 1)
+ }
+
+ function {:fuel 0,0} neg(x:int) : int
+ decreases 1 - x;
+ {
+ if x > 0 then 0
+ else 1 + neg(x + 1)
+ }
+
+ method {:fuel neg,4} {:fuel pos,0,0} test1(y:int, z:int)
+ requires y > 5;
+ requires z < -5;
+ {
+ if (*) {
+ assert pos(y) == 3 + pos(y - 3); // error: Method fuel should override function fuel, so this should fail
+ assert neg(z) == 3 + neg(z + 3); // Method fuel should override function fuel, so this succeeds
+ }
+
+ forall t:int {:fuel pos,3} | t > 0
+ ensures true;
+ {
+ assert pos(y) == 3 + pos(y - 3); // Statement fuel should override method fuel, so this should succeed
+ }
+ }
+}
+
+// Test fuel in a slightly more complicated setting
+module TestModule8 {
+
+ newtype byte = i:int | 0 <= i < 0x100
+ newtype uint64 = i:int | 0 <= i < 0x10000000000000000
+
+ datatype G = GUint64
+ | GArray(elt:G)
+ | GTuple(t:seq<G>)
+ | GByteArray
+ | GTaggedUnion(cases:seq<G>)
+
+ datatype V = VUint64(u:uint64)
+ | VTuple(t:seq<V>)
+ | VCase(c:uint64, val:V)
+
+ predicate {:fuel 2} ValInGrammar(val:V, grammar:G)
+ {
+ match val
+ case VUint64(_) => grammar.GUint64?
+ case VTuple(t) => grammar.GTuple? && |t| == |grammar.t|
+ && forall i :: 0 <= i < |t| ==> ValInGrammar(t[i], grammar.t[i])
+ case VCase(c, val) => grammar.GTaggedUnion? && int(c) < |grammar.cases| && ValInGrammar(val, grammar.cases[c])
+ }
+
+ datatype CRequest = CRequest(client:EndPoint, seqno:uint64, request:CAppMessage) | CRequestNoOp()
+
+ type EndPoint
+ function method EndPoint_grammar() : G { GUint64 }
+ function method CRequest_grammar() : G { GTaggedUnion([ GTuple([EndPoint_grammar(), GUint64, CAppMessage_grammar()]), GUint64]) }
+
+ function method parse_EndPoint(val:V) : EndPoint
+ requires ValInGrammar(val, EndPoint_grammar());
+
+ type CAppMessage
+ function method CAppMessage_grammar() : G { GTaggedUnion([GUint64, GUint64, GUint64]) }
+ function method parse_AppMessage(val:V) : CAppMessage
+ requires ValInGrammar(val, CAppMessage_grammar());
+
+ function method {:fuel ValInGrammar,1,2} parse_Request1(val:V) : CRequest
+ requires ValInGrammar(val, CRequest_grammar());
+ {
+ if val.c == 0 then
+ var ep := parse_EndPoint(val.val.t[0]); // With default fuel, error: function precondition, destructor, index
+ CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2])) // error: index out of range, destructor
+ else
+ CRequestNoOp()
+ }
+
+ function method parse_Request2(val:V) : CRequest
+ requires ValInGrammar(val, CRequest_grammar());
+ {
+ if val.c == 0 then
+ var ep := parse_EndPoint(val.val.t[0]); // With fuel boosted to 2 this succeeds
+ CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2])) // error: destructor
+ else
+ CRequestNoOp()
+ }
+
+ function method {:fuel ValInGrammar,3} parse_Request3(val:V) : CRequest
+ requires ValInGrammar(val, CRequest_grammar());
+ {
+ if val.c == 0 then
+ var ep := parse_EndPoint(val.val.t[0]);
+ CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2])) // With one more boost, everything succeeds
+ else
+ CRequestNoOp()
+ }
+
+ // With the method, everything succeeds with one less fuel boost (i.e., 2, rather than 3, as in parse_Request3)
+ method parse_Request4(val:V) returns (req:CRequest)
+ requires ValInGrammar(val, CRequest_grammar());
+ {
+ if val.c == 0 {
+ var ep := parse_EndPoint(val.val.t[0]);
+ req := CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]));
+ } else {
+ req := CRequestNoOp();
+ }
+ }
+}
+
+
+// Test fuel when it's applied to a non-recursive function
+module TestModule9 {
+ function abs(x:int) : int
+ {
+ if x < 0 then -1 * x else x
+ }
+
+ // All should pass.
+ method test1(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert abs(z) == -1*z;
+ assert abs(y) == y;
+ assert abs(-1) == 1;
+ }
+
+ // Method-level fuel override
+ method {:fuel abs,0,0} test2(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert abs(z) == -1*z; // error: Cannot see the body of abs
+ assert abs(y) == y; // error: Cannot see the body of abs
+ assert abs(-1) == 1; // lit bypasses fuel, so this should succeed
+ }
+
+ // Statement-level fuel override
+ method test3(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert {:fuel abs,0,0} abs(z) == -1*z; // error: fuel can't be decreased
+ assert abs(y) == y; // Normal success
+ assert abs(-1) == 1; // lit bypasses fuel, so this should succeed
+ }
+
+ // Giving more fuel to a non-recursive function won't help,
+ // but it shouldn't hurt either.
+ method {:fuel abs,5,7} test4(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert abs(z) == -1*z;
+ assert abs(y) == y;
+ assert abs(-1) == 1;
+ }
+}
+
+// Test fuel when it's applied to a non-recursive function directly (to simulate opaque)
+module TestModule10 {
+ function {:fuel 0,0} abs(x:int) : int
+ {
+ if x < 0 then -1 * x else x
+ }
+
+ method test1(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert abs(z) == -1*z; // error: Cannot see the body of abs
+ assert abs(y) == y; // error: Cannot see the body of abs
+ assert abs(-1) == 1; // lit bypasses fuel, so this should succeed
+ }
+}
+
+// Test fuel when it's mentioned in other functions function to simulate a local opaque
+module TestModule11 {
+ function abs(x:int) : int
+ {
+ if x < 0 then -1 * x else x
+ }
+
+ function {:fuel abs,0,0} abs'(x:int) : int
+ {
+ abs(x)
+ }
+
+ method test1(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert abs'(z) == -1*z; // error: Cannot see the body of abs
+ assert abs'(y) == y; // error: Cannot see the body of abs
+ assert abs'(-1) == 1; // lit bypasses fuel, so this should succeed
+ }
+}
+
|