From 5b3dcd0c09a7ea8a34e7f5e4b8800015b3b07e96 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Wed, 1 Jul 2015 12:37:54 -0700 Subject: Add the ability to specify how much "fuel" a function should have, i.e., how many times Z3 is permitted to unfold it's definition. The new {:fuel} annotation can be added to the function itself, it which case it will apply to all uses of that function, or it can overridden within the scope of a module, function, method, iterator, calc, forall, while, assert, or assume. The general format is: {:fuel functionName,lowFuel,highFuel} When applied as an annotation to the function itself, omit functionName. If highFuel is omitted, it defaults to lowFuel + 1. The default fuel setting for recursive functions is 1,2. Setting the fuel higher, say, to 3,4, will give more unfoldings, which may make some proofs go through with less programmer assistance (e.g., with fewer assert statements), but it may also increase verification time, so use it with care. Setting the fuel to 0,0 is similar to making the definition opaque, except when used with all literal arguments. --- Test/dafny0/Fuel.dfy | 423 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 423 insertions(+) create mode 100644 Test/dafny0/Fuel.dfy (limited to 'Test/dafny0/Fuel.dfy') diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy new file mode 100644 index 00000000..c8a1fc2f --- /dev/null +++ b/Test/dafny0/Fuel.dfy @@ -0,0 +1,423 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%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: Should fail due to "opaque" fuel setting + 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) + | GByteArray + | GTaggedUnion(cases:seq) + + datatype V = VUint64(u:uint64) + | VTuple(t:seq) + | 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: Cannot see the body of abs + 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; + } +} + -- cgit v1.2.3 From 88f5ac86bda56381f81be032a0011e34aeca50a8 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Mon, 19 Oct 2015 22:53:41 -0700 Subject: Improve Dafny's ability to find fueled functions by checking the function itself, as well as the signature and body of other functions. --- Source/Dafny/DafnyAst.cs | 20 ++++++++++++++++++++ Source/Dafny/Resolver.cs | 7 +++++++ Test/dafny0/Fuel.dfy | 39 +++++++++++++++++++++++++++++++++++++++ Test/dafny0/Fuel.dfy.expect | 14 +++++++++++++- 4 files changed, 79 insertions(+), 1 deletion(-) (limited to 'Test/dafny0/Fuel.dfy') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 667f8407..871d644d 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3202,7 +3202,27 @@ namespace Microsoft.Dafny { this.Decreases = decreases; this.Body = body; this.SignatureEllipsis = signatureEllipsis; + + if (attributes != null) { + List args = Attributes.FindExpressions(attributes, "fuel"); + if (args != null) { + if (args.Count == 1) { + LiteralExpr literal = args[0] as LiteralExpr; + if (literal != null && literal.Value is BigInteger) { + this.IsFueled = true; + } + } else if (args.Count == 2) { + LiteralExpr literalLow = args[0] as LiteralExpr; + LiteralExpr literalHigh = args[1] as LiteralExpr; + + if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) { + this.IsFueled = true; + } + } + } + } } + bool ICodeContext.IsGhost { get { return this.IsGhost; } } List ICodeContext.TypeArgs { get { return this.TypeArgs; } } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 1798243c..6ded74d5 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -444,6 +444,13 @@ namespace Microsoft.Dafny } else if (clbl is IteratorDecl) { body = ((IteratorDecl)clbl).Body; CheckForFuelAdjustments(clbl.Tok, ((IteratorDecl)clbl).Attributes, module); + } else if (clbl is Function) { + CheckForFuelAdjustments(clbl.Tok, ((Function)clbl).Attributes, module); + var c = new FuelAdjustment_Visitor(this); + var bodyExpr = ((Function)clbl).Body; + if (bodyExpr != null) { + c.Visit(bodyExpr, new FuelAdjustment_Context(module)); + } } if (body != null) { var c = new FuelAdjustment_Visitor(this); diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy index c8a1fc2f..abbc831e 100644 --- a/Test/dafny0/Fuel.dfy +++ b/Test/dafny0/Fuel.dfy @@ -421,3 +421,42 @@ module TestModule9 { } } +// 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 + } +} + diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect index 90fe877d..0c128941 100644 --- a/Test/dafny0/Fuel.dfy.expect +++ b/Test/dafny0/Fuel.dfy.expect @@ -89,7 +89,19 @@ Fuel.dfy(398,22): Error: assertion violation Execution trace: (0,0): anon0 Fuel.dfy(407,38): Error: assertion violation +Execution trace: + (0,0): anon0 +Fuel.dfy(435,22): Error: assertion violation +Execution trace: + (0,0): anon0 +Fuel.dfy(436,22): Error: assertion violation +Execution trace: + (0,0): anon0 +Fuel.dfy(457,23): Error: assertion violation +Execution trace: + (0,0): anon0 +Fuel.dfy(458,23): Error: assertion violation Execution trace: (0,0): anon0 -Dafny program verifier finished with 51 verified, 24 errors +Dafny program verifier finished with 56 verified, 28 errors -- cgit v1.2.3 From acbc126c01fee3ab71647a7b16f4dcfc80eee2ea Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 18 Mar 2016 09:48:26 -0700 Subject: Fix issue 93. Add per-function fuel setting that can be adjusted locally based on context. --- Source/Dafny/Translator.cs | 224 +++++++++++++++++++++++++++++++++++++------ Test/dafny0/Fuel.dfy | 4 +- Test/dafny0/Fuel.dfy.expect | 10 +- Test/dafny4/Bug93.dfy | 37 +++++++ Test/dafny4/Bug93.dfy.expect | 8 ++ 5 files changed, 249 insertions(+), 34 deletions(-) create mode 100644 Test/dafny4/Bug93.dfy create mode 100644 Test/dafny4/Bug93.dfy.expect (limited to 'Test/dafny0/Fuel.dfy') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 28077842..9466f18a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -113,6 +113,7 @@ namespace Microsoft.Dafny { readonly Dictionary/*!*/ classConstants = new Dictionary(); readonly Dictionary functionConstants = new Dictionary(); readonly Dictionary functionHandles = new Dictionary(); + readonly static List FunctionFuel = new List(); readonly Dictionary/*!*/ fields = new Dictionary(); readonly Dictionary/*!*/ fieldFunctions = new Dictionary(); readonly Dictionary fieldConstants = new Dictionary(); @@ -488,6 +489,9 @@ namespace Microsoft.Dafny { return new Bpl.Program(); } + // compute which function needs fuel constants. + ComputeFunctionFuel(); + foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) { currentDeclaration = d; if (d is OpaqueTypeDecl) { @@ -577,6 +581,37 @@ namespace Microsoft.Dafny { return sink; } + private void ComputeFunctionFuel() { + foreach (ModuleDefinition m in program.Modules) { + foreach (TopLevelDecl d in m.TopLevelDecls) { + if (d is ClassDecl) { + ClassDecl c = (ClassDecl)d; + foreach (MemberDecl member in c.Members) { + if (member is Function) { + Function f = (Function)member; + // declare the fuel constant + if (f.IsFueled) { + // const BaseFuel_FunctionA : LayerType + Bpl.Constant baseFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "BaseFuel_" + f.FullName, predef.LayerType), false); + sink.AddTopLevelDeclaration(baseFuel); + Bpl.Expr baseFuel_expr = new Bpl.IdentifierExpr(f.tok, baseFuel); + // const StartFuel_FunctionA : LayerType + Bpl.Constant startFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuel_" + f.FullName, predef.LayerType), false); + sink.AddTopLevelDeclaration(startFuel); + Bpl.Expr startFuel_expr = new Bpl.IdentifierExpr(f.tok, startFuel); + // const StartFuelAssert_FunctionA : LayerType + Bpl.Constant startFuelAssert = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuelAssert_" + f.FullName, predef.LayerType), false); + sink.AddTopLevelDeclaration(startFuelAssert); + Bpl.Expr startFuelAssert_expr = new Bpl.IdentifierExpr(f.tok, startFuelAssert); + Translator.FunctionFuel.Add(new FuelConstant(f, baseFuel_expr, startFuel_expr, startFuelAssert_expr)); + } + } + } + } + } + } + } + /// /// adding TraitParent axioms /// if a class A extends trait J and B does not extend anything, then this method adds the followings to the sink: @@ -2755,6 +2790,7 @@ namespace Microsoft.Dafny { Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder(); builder.Add(new CommentCmd("AddMethodImpl: " + m + ", " + proc)); ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok); + InitializeFuelConstant(m.tok, builder, etran); List localVariables = new List(); GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables); @@ -2934,6 +2970,52 @@ namespace Microsoft.Dafny { Reset(); } + void InitializeFuelConstant(IToken tok, Bpl.StmtListBuilder builder, ExpressionTranslator etran) { + builder.Add(new CommentCmd("initialize fuel constant")); + FuelContext fuelContext = this.fuelContext; + foreach (FuelConstant fuelConstant in Translator.FunctionFuel) { + Function f = fuelConstant.f; + Bpl.Expr baseFuel = fuelConstant.baseFuel; + Bpl.Expr startFuel = fuelConstant.startFuel; + Bpl.Expr startFuelAssert = fuelConstant.startFuelAssert; + // find out what the initial value should be + FuelSettingPair settings; + var found = fuelContext.TryGetValue(f, out settings); + if (!found) { + // If the context doesn't define fuel for this function, check for a fuel attribute (which supplies a default value if none is found) + settings = FuelSetting.FuelAttrib(f, out found); + } + + Bpl.Expr layer = etran.layerInterCluster.LayerN(settings.low, baseFuel); + Bpl.Expr layerAssert = etran.layerInterCluster.LayerN(settings.high, baseFuel); + builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuel, layer))); + builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuelAssert, layerAssert))); + } + } + + bool DefineFuelConstant(IToken tok, Attributes attribs, Bpl.StmtListBuilder builder, ExpressionTranslator etran) { + bool defineFuel = false; + builder.Add(new CommentCmd("Assume Fuel Constant")); + FuelContext fuelContext = new FuelContext(); + FuelSetting.FindFuelAttributes(attribs, fuelContext); + foreach (KeyValuePair fuel in fuelContext) { + Function f = fuel.Key; + FuelSettingPair settings = fuel.Value; + FuelConstant fuelConstant = Translator.FunctionFuel.Find(x => x.f == f); + if (fuelConstant != null) { + Bpl.Expr startFuel = fuelConstant.startFuel; + Bpl.Expr startFuelAssert = fuelConstant.startFuelAssert; + Bpl.Expr moreFuel_expr = fuelConstant.MoreFuel(sink, predef, f.IdGenerator); + Bpl.Expr layer = etran.layerInterCluster.LayerN(settings.low, moreFuel_expr); + Bpl.Expr layerAssert = etran.layerInterCluster.LayerN(settings.high, moreFuel_expr); + builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuel, layer))); + builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuelAssert, layerAssert))); + defineFuel = true; + } + } + return defineFuel; + } + internal static AssumeCmd optimizeExpr(bool minimize, Expression expr, IToken tok, ExpressionTranslator etran) { Contract.Requires(expr != null); @@ -4032,7 +4114,7 @@ namespace Microsoft.Dafny { builder.Add(CaptureState(f.tok, false, "initial state")); DefineFrame(f.tok, f.Reads, builder, locals, null); - + InitializeFuelConstant(f.tok, builder, etran); // Check well-formedness of the preconditions (including termination), and then // assume each one of them. After all that (in particular, after assuming all // of them), do the postponed reads checks. @@ -7113,11 +7195,14 @@ namespace Microsoft.Dafny { Contract.Requires(codeContext != null && predef != null); Contract.Ensures(fuelContext == Contract.OldValue(fuelContext)); if (stmt is PredicateStmt) { - this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext); + var stmtBuilder = new Bpl.StmtListBuilder(); + this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter); + var defineFuel = DefineFuelConstant(stmt.Tok, stmt.Attributes, stmtBuilder, etran); + var b = defineFuel ? stmtBuilder : builder; if (stmt is AssertStmt || DafnyOptions.O.DisallowSoundnessCheating) { - AddComment(builder, stmt, "assert statement"); + AddComment(b, stmt, "assert statement"); PredicateStmt s = (PredicateStmt)stmt; - TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false); + TrStmt_CheckWellformed(s.Expr, b, locals, etran, false); IToken enclosingToken = null; if (Attributes.Contains(stmt.Attributes, "prependAssertToken")) { enclosingToken = stmt.Tok; @@ -7126,14 +7211,21 @@ namespace Microsoft.Dafny { var ss = TrSplitExpr(s.Expr, etran, true, out splitHappened); if (!splitHappened) { var tok = enclosingToken == null ? s.Expr.tok : new NestedToken(enclosingToken, s.Expr.tok); - builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null))); + b.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null))); } else { foreach (var split in ss) { if (split.IsChecked) { var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.E.tok); - builder.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split + b.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split } } + if (!defineFuel) { + b.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr))); + } + } + if (defineFuel) { + var ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), null, null); + builder.Add(ifCmd); builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr))); } } else if (stmt is AssumeStmt) { @@ -7381,7 +7473,8 @@ namespace Microsoft.Dafny { } else if (stmt is WhileStmt) { AddComment(builder, stmt, "while statement"); - this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext); + this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter); + DefineFuelConstant(stmt.Tok, stmt.Attributes, builder, etran); var s = (WhileStmt)stmt; BodyTranslator bodyTr = null; if (s.Body != null) { @@ -7434,7 +7527,8 @@ namespace Microsoft.Dafny { } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; - this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext); + this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter); + if (s.Kind == ForallStmt.ParBodyKind.Assign) { AddComment(builder, stmt, "forall statement (assign)"); Contract.Assert(s.Ens.Count == 0); @@ -7444,6 +7538,7 @@ namespace Microsoft.Dafny { var s0 = (AssignStmt)s.S0; var definedness = new Bpl.StmtListBuilder(); var updater = new Bpl.StmtListBuilder(); + DefineFuelConstant(stmt.Tok, stmt.Attributes, definedness, etran); TrForallAssign(s, s0, definedness, updater, locals, etran); // All done, so put the two pieces together builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, updater.Collect(s.Tok))); @@ -7459,6 +7554,7 @@ namespace Microsoft.Dafny { } else { var s0 = (CallStmt)s.S0; var definedness = new Bpl.StmtListBuilder(); + DefineFuelConstant(stmt.Tok, stmt.Attributes, definedness, etran); var exporter = new Bpl.StmtListBuilder(); TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s.ForallExpressions, s0, definedness, exporter, locals, etran); // All done, so put the two pieces together @@ -7470,6 +7566,7 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "forall statement (proof)"); var definedness = new Bpl.StmtListBuilder(); var exporter = new Bpl.StmtListBuilder(); + DefineFuelConstant(stmt.Tok, stmt.Attributes, definedness, etran); TrForallProof(s, definedness, exporter, locals, etran); // All done, so put the two pieces together builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok))); @@ -7504,7 +7601,8 @@ namespace Microsoft.Dafny { var s = (CalcStmt)stmt; Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver AddComment(builder, stmt, "calc statement"); - this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext); + this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter); + DefineFuelConstant(stmt.Tok, stmt.Attributes, builder, etran); CurrentIdGenerator.Push(); // put the entire calc statement within its own sub-branch if (s.Lines.Count > 0) { Bpl.IfCmd ifCmd = null; @@ -10312,31 +10410,58 @@ namespace Microsoft.Dafny { // C#'s version of a type alias internal class FuelContext : Dictionary { } + internal class FuelConstant + { + public Function f; + public Bpl.Expr baseFuel; + public Bpl.Expr startFuel; + public Bpl.Expr startFuelAssert; + + public FuelConstant(Function f, Bpl.Expr baseFuel, Bpl.Expr startFuel, Bpl.Expr startFuelAssert) { + this.f = f; + this.baseFuel = baseFuel; + this.startFuel = startFuel; + this.startFuelAssert = startFuelAssert; + } + + public Bpl.Expr MoreFuel(Bpl.Program sink, PredefinedDecls predef, FreshIdGenerator idGen) { + string uniqueId = idGen.FreshId("MoreFuel_" + f.FullName); + Bpl.Constant moreFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, uniqueId, predef.LayerType), false); + sink.AddTopLevelDeclaration(moreFuel); + Bpl.Expr moreFuel_expr = new Bpl.IdentifierExpr(f.tok, moreFuel); + return moreFuel_expr; + } + } + internal class FuelSetting { public enum FuelAmount { NONE, LOW, HIGH }; public static Stack SavedContexts = new Stack(); - private static FuelSettingPair FuelAttrib(Function f) { + public static FuelSettingPair FuelAttrib(Function f, out bool found) { Contract.Requires(f != null); Contract.Ensures(Contract.Result() != null); FuelSettingPair setting = new FuelSettingPair(); + found = false; if (f.Attributes != null) { List args = Attributes.FindExpressions(f.Attributes, "fuel"); - if (args != null && args.Count >= 2) { - LiteralExpr literalLow = args[0] as LiteralExpr; - LiteralExpr literalHigh = args[1] as LiteralExpr; - - if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) { - setting.low = (int)((BigInteger)literalLow.Value); - setting.high = (int)((BigInteger)literalHigh.Value); - } - } else if (args != null && args.Count >= 1) { - LiteralExpr literal = args[0] as LiteralExpr; - if (literal != null && literal.Value is BigInteger) { - setting.low = (int)((BigInteger)literal.Value); - setting.high = setting.low + 1; + if (args != null) { + found = true; + if (args.Count >= 2) { + LiteralExpr literalLow = args[0] as LiteralExpr; + LiteralExpr literalHigh = args[1] as LiteralExpr; + + if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) { + setting.low = (int)((BigInteger)literalLow.Value); + setting.high = (int)((BigInteger)literalHigh.Value); + } + } else if (args.Count >= 1) { + LiteralExpr literal = args[0] as LiteralExpr; + if (literal != null && literal.Value is BigInteger) { + setting.low = (int)((BigInteger)literal.Value); + setting.high = setting.low + 1; + } } } } @@ -10369,6 +10494,12 @@ namespace Microsoft.Dafny { return translator.LayerSucc(LayerZero(), n); } + public Bpl.Expr LayerN(int n, Bpl.Expr baseLayer) { + Contract.Requires(0 <= n); + Contract.Ensures(Contract.Result() != null); + return translator.LayerSucc(baseLayer, n); + } + private Bpl.Expr ToExpr(int amount) { if (start == null) { return LayerN(amount); @@ -10394,13 +10525,14 @@ namespace Microsoft.Dafny { var found = translator.fuelContext.TryGetValue(f, out setting); if (!found) { // If the context doesn't define fuel for this function, check for a fuel attribute (which supplies a default value if none is found) - setting = FuelAttrib(f); + setting = FuelAttrib(f, out found); } + FuelConstant fuelConstant = Translator.FunctionFuel.Find(x => x.f == f); if (this.amount == (int)FuelAmount.LOW) { - return ToExpr(setting.low); + return GetFunctionFuel(setting.low, found, fuelConstant); } else if (this.amount == (int)FuelAmount.HIGH) { - return ToExpr(setting.high); + return GetFunctionFuel(setting.high, found, fuelConstant); } else { Contract.Assert(false); // Should not reach here return null; @@ -10408,13 +10540,30 @@ namespace Microsoft.Dafny { } } + private Bpl.Expr GetFunctionFuel(int amount, bool hasFuel, FuelConstant fuelConstant) { + if (fuelConstant != null) { + if (hasFuel) { + // it has fuel context + return LayerN(amount, fuelConstant.baseFuel); + } else { + // startfuel + if (amount == (int)FuelAmount.LOW) { + return fuelConstant.startFuel; + } else { + return fuelConstant.startFuelAssert; + } + } + } else { + return ToExpr(amount); + } + } /// /// Finds all fuel related attributes of the form {:fuel function low [high]} /// Adds the setting to the context _if_ the context does not already have a setting for that function. /// In other words, it should be called in order from most to least specific contenxt scope. /// - private static void FindFuelAttributes(Attributes attribs, FuelContext fuelContext) { + public static void FindFuelAttributes(Attributes attribs, FuelContext fuelContext) { Function f = null; FuelSettingPair setting = null; @@ -10495,20 +10644,35 @@ namespace Microsoft.Dafny { /// /// Extends the given fuel context with any new fuel settings found in attribs /// - public static FuelContext ExpandFuelContext(Attributes attribs, FuelContext oldFuelContext) { + public static FuelContext ExpandFuelContext(Attributes attribs, IToken tok, FuelContext oldFuelContext, ErrorReporter reporter) { Contract.Ensures(SavedContexts.Count == Contract.OldValue(SavedContexts.Count) + 1); FuelContext newContext = new FuelContext(); FindFuelAttributes(attribs, newContext); if (newContext.Count > 0) { + // first make sure that the fuel only increase relative to the oldContext + foreach (var pair in newContext) { + FuelSettingPair newSetting = pair.Value; + FuelSettingPair oldSetting; + var found = oldFuelContext.TryGetValue(pair.Key, out oldSetting); + if (!found) { // the default is {:fuel, 1, 2} + oldSetting = new FuelSettingPair(); + } + // make sure that the fuel can only increase within a given scope + if (newSetting.low < oldSetting.low || newSetting.high < oldSetting.high) { + reporter.Error(MessageSource.Translator, tok, "Fuel can only increase within a given scope."); + } + } + // add oldContext to newContext if it doesn't exist already foreach (var pair in oldFuelContext) { if (!newContext.ContainsKey(pair.Key)) { // Local setting takes precedence over old context - newContext.Add(pair.Key, pair.Value); + newContext.Add(pair.Key, pair.Value); } - } + } } else { newContext = oldFuelContext; } SavedContexts.Push(oldFuelContext); + return newContext; } diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy index abbc831e..6347e134 100644 --- a/Test/dafny0/Fuel.dfy +++ b/Test/dafny0/Fuel.dfy @@ -126,7 +126,7 @@ module TestModule4 { requires y > 5; requires z < 0; { - assert {:fuel pos,0,0} pos(z) == 0; // error: Should fail due to "opaque" fuel setting + 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 @@ -404,7 +404,7 @@ module TestModule9 { requires y > 5; requires z < 0; { - assert {:fuel abs,0,0} abs(z) == -1*z; // error: Cannot see the body of abs + 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 } diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect index 0c128941..275be237 100644 --- a/Test/dafny0/Fuel.dfy.expect +++ b/Test/dafny0/Fuel.dfy.expect @@ -1,3 +1,5 @@ +Fuel.dfy(129,8): Error: Fuel can only increase within a given scope. +Fuel.dfy(407,8): Error: Fuel can only increase within a given scope. Fuel.dfy(17,22): Error: assertion violation Execution trace: (0,0): anon0 @@ -25,14 +27,17 @@ Execution trace: Fuel.dfy(129,38): Error: assertion violation Execution trace: (0,0): anon0 + (0,0): anon7_Then Fuel.dfy(132,26): Error: assertion violation Execution trace: (0,0): anon0 - (0,0): anon3_Then + Fuel.dfy(129,9): anon7_Else + (0,0): anon8_Then Fuel.dfy(133,26): Error: assertion violation Execution trace: (0,0): anon0 - (0,0): anon3_Then + Fuel.dfy(129,9): anon7_Else + (0,0): anon8_Then Fuel.dfy(157,22): Error: assertion violation Execution trace: (0,0): anon0 @@ -91,6 +96,7 @@ Execution trace: Fuel.dfy(407,38): Error: assertion violation Execution trace: (0,0): anon0 + (0,0): anon3_Then Fuel.dfy(435,22): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny4/Bug93.dfy b/Test/dafny4/Bug93.dfy new file mode 100644 index 00000000..5a1dd27f --- /dev/null +++ b/Test/dafny4/Bug93.dfy @@ -0,0 +1,37 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Fuel { + function FunctionA(x:int) : int + { + x + 2 + } + + function FunctionB(y:int) : int + { + FunctionA(y - 2) + } + + method {:fuel FunctionA,0,0} MethodX(z:int) + { + assert FunctionB(z) == z; // error: Cannot see the body of FunctionA + } +} + +module Opaque { + function {:opaque} FunctionA(x:int) : int + { + x + 2 + } + + function FunctionB(y:int) : int + { + FunctionA(y - 2) + } + + method MethodX(z:int) + { + assert FunctionB(z) == z; + } +} + diff --git a/Test/dafny4/Bug93.dfy.expect b/Test/dafny4/Bug93.dfy.expect new file mode 100644 index 00000000..d0baf877 --- /dev/null +++ b/Test/dafny4/Bug93.dfy.expect @@ -0,0 +1,8 @@ +Bug93.dfy(17,28): Error: assertion violation +Execution trace: + (0,0): anon0 +Bug93.dfy(34,28): Error: assertion violation +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 7 verified, 2 errors -- cgit v1.2.3 From 91cee1c2028f9ad995df863f2a4568d95f4ea1a8 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 28 Mar 2016 12:02:37 -0700 Subject: Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. --- Source/Dafny/DafnyOptions.cs | 6 ++-- Source/DafnyServer/Utilities.cs | 2 +- Test/VSI-Benchmarks/b8.dfy | 2 +- Test/VerifyThis2015/Problem3.dfy | 2 +- Test/cloudmake/CloudMake-CachedBuilds.dfy | 2 +- Test/cloudmake/CloudMake-ConsistentBuilds.dfy | 2 +- Test/cloudmake/CloudMake-ParallelBuilds.dfy | 2 +- Test/dafny0/Basics.dfy | 2 +- Test/dafny0/Calculations.dfy | 2 +- Test/dafny0/Compilation.dfy | 2 +- Test/dafny0/ForallCompilation.dfy | 2 +- Test/dafny0/Fuel.dfy | 2 +- Test/dafny0/LetExpr.dfy | 2 +- Test/dafny0/LetExpr.dfy.expect | 1 + Test/dafny0/LhsDuplicates.dfy | 2 +- Test/dafny0/Parallel.dfy | 2 +- Test/dafny0/SmallTests.dfy.expect | 1 + Test/dafny1/MoreInduction.dfy | 2 +- Test/dafny1/SchorrWaite-stages.dfy | 2 +- Test/dafny1/SchorrWaite.dfy | 2 +- Test/dafny1/Substitution.dfy | 2 +- Test/dafny1/UltraFilter.dfy | 2 +- Test/dafny2/SnapshotableTrees.dfy | 2 +- Test/dafny3/Filter.dfy | 2 +- Test/dafny4/GHC-MergeSort.dfy | 2 +- Test/dafny4/NumberRepresentations.dfy | 2 +- Test/dafny4/Primes.dfy | 2 +- Test/server/simple-session.transcript.expect | 41 +++++++++++++++++++++++++++ Test/vstte2012/BreadthFirstSearch.dfy | 2 +- 29 files changed, 71 insertions(+), 28 deletions(-) (limited to 'Test/dafny0/Fuel.dfy') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index f3b38a84..607090eb 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; - public bool AutoTriggers = false; + public bool AutoTriggers = true; public bool RewriteFocalPredicates = true; public bool PrintTooltips = false; public bool PrintStats = false; @@ -386,8 +386,8 @@ namespace Microsoft.Dafny 1 (default) - If preprocessing succeeds, set exit code to the number of verification errors. /autoTriggers: - 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. - 1 - Add a {:trigger} to each user-level quantifier. Existing + 0 - Do not generate {:trigger} annotations for user-level quantifiers. + 1 (default) - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. /rewriteFocalPredicates: 0 - Don't rewrite predicates in the body of prefix lemmas. diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 30d779e7..48bea01a 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -51,7 +51,7 @@ namespace Microsoft.Dafny { DafnyOptions.O.VerifySnapshots = 2; // Use caching DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout - DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs + //DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification } else { throw new ServerException("Invalid command line options"); diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index ea1911fe..a44ff5c3 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Benchmark 8 diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 21bdd4ed..60506a33 100644 --- a/Test/VerifyThis2015/Problem3.dfy +++ b/Test/VerifyThis2015/Problem3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy index 9e1b511e..5f16da90 100644 --- a/Test/cloudmake/CloudMake-CachedBuilds.dfy +++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This module proves the correctness of the algorithms. It leaves a number of things undefined. diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy index 6d86607b..c2fa4205 100644 --- a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy +++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" /******* State *******/ diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy index 07cae317..5cc70994 100644 --- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy +++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This module proves the correctness of the algorithms. It leaves a number of things undefined. diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 89b0f02a..7b8b632b 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Global { diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy index a7c8e06c..eb4ff1b9 100644 --- a/Test/dafny0/Calculations.dfy +++ b/Test/dafny0/Calculations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" /autoTriggers:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 7a443e47..213ace54 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %dafny /compile:3 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The tests in this file are designed to run through the compiler. They contain diff --git a/Test/dafny0/ForallCompilation.dfy b/Test/dafny0/ForallCompilation.dfy index c812983a..4d89f70d 100644 --- a/Test/dafny0/ForallCompilation.dfy +++ b/Test/dafny0/ForallCompilation.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy index 6347e134..a768db02 100644 --- a/Test/dafny0/Fuel.dfy +++ b/Test/dafny0/Fuel.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" module TestModule1 { diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index 000fce53..6a0ca66b 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" /autoTriggers:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect index f0f51274..8f365da3 100644 --- a/Test/dafny0/LetExpr.dfy.expect +++ b/Test/dafny0/LetExpr.dfy.expect @@ -35,5 +35,6 @@ Execution trace: (0,0): anon10_Then Dafny program verifier finished with 39 verified, 9 errors +LetExpr.dfy.tmp.dprint.dfy(162,2): Warning: /!\ No terms found to trigger on. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Test/dafny0/LhsDuplicates.dfy b/Test/dafny0/LhsDuplicates.dfy index 6a84c5a5..8a57f6ce 100644 --- a/Test/dafny0/LhsDuplicates.dfy +++ b/Test/dafny0/LhsDuplicates.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class MyClass { diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 93a16475..00a1514c 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 6161c3dd..746e978a 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -197,5 +197,6 @@ Execution trace: (0,0): anon0 Dafny program verifier finished with 104 verified, 35 errors +SmallTests.dfy.tmp.dprint.dfy(369,4): Warning: /!\ No trigger covering all quantified variables found. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index bd654db5..2b5187a4 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype List = Nil | Cons(Node, List) diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 0eaed68c..a6e5e3aa 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Schorr-Waite algorithms, written and verified in Dafny. diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 50210eb1..b0877f9f 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index da64d004..b9c83aff 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype List = Nil | Cons(Expr, List) diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index a32e6e0b..7ac4e749 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // ultra filter diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy index 2bdfb83b..033c5db0 100644 --- a/Test/dafny2/SnapshotableTrees.dfy +++ b/Test/dafny2/SnapshotableTrees.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:2 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:2 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino, September 2011. diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy index 4f8b35ec..7473a580 100644 --- a/Test/dafny3/Filter.dfy +++ b/Test/dafny3/Filter.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" codatatype Stream = Cons(head: T, tail: Stream) diff --git a/Test/dafny4/GHC-MergeSort.dfy b/Test/dafny4/GHC-MergeSort.dfy index 976b8a27..24903d87 100644 --- a/Test/dafny4/GHC-MergeSort.dfy +++ b/Test/dafny4/GHC-MergeSort.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 0d6cffa1..c15f4987 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // We consider a number representation that consists of a sequence of digits. The least diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy index fd64b45e..0c2a64dd 100644 --- a/Test/dafny4/Primes.dfy +++ b/Test/dafny4/Primes.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" predicate IsPrime(n: int) diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect index 1aadca7f..a5f841bc 100644 --- a/Test/server/simple-session.transcript.expect +++ b/Test/server/simple-session.transcript.expect @@ -346,6 +346,7 @@ transcript(10,27): Error: invalid UnaryExpression Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -366,6 +367,7 @@ Execution trace: Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -383,6 +385,7 @@ Verifying Impl$$_module.__default.M_k ... Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -406,6 +409,7 @@ transcript(12,0): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -423,6 +427,7 @@ Verifying Impl$$_module.__default.M_k ... Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -498,6 +503,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -538,6 +547,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -584,6 +597,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -638,6 +655,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -685,6 +706,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -729,6 +754,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -796,6 +825,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -861,6 +894,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -905,6 +942,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index b111a438..375f4a09 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class BreadthFirstSearch -- cgit v1.2.3