From e815f2358965c2ad815f07da65d52966cefeae6e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 5 Nov 2024 20:31:16 -0800 Subject: [PATCH] fix: Omit type antecedents for unassigned variables (#5877) In let expressions and named function results, the bound variable was previously introduced with an assumption that the variable satisfied its type. That is not sound, since the type may be empty. This PR removes those premature type assumptions. Fixes #1958 By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../BoogieGenerator.ExpressionWellformed.cs | 4 +- ...oogieGenerator.Functions.Wellformedness.cs | 11 +- .../dafny0/CoinductiveProofs.dfy.expect | 2 +- .../LitTest/dafny0/Fuel.legacy.dfy.expect | 18 +- .../LitTest/dafny0/SubsetTypes.dfy.expect | 2 +- .../LitTest/dafny1/SchorrWaite.dfy.expect | 2 +- .../dafny1/SchorrWaite.dfy.refresh.expect | 2 +- .../LitTest/git-issues/git-issue-1958.dfy | 178 ++++++++++++++++++ .../git-issues/git-issue-1958.dfy.expect | 19 ++ .../separate-verification/Inputs/seq.dfy | 4 +- docs/dev/news/5877.fix | 1 + 11 files changed, 223 insertions(+), 20 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy.expect create mode 100644 docs/dev/news/5877.fix diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 328841500bb..3dc3789b4c7 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1483,7 +1483,9 @@ void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bp void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Variables locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs, AddResultCommands addResultCommands) { if (e.Exact) { - var substMap = SetupBoundVarsAsLocals(e.BoundVars.ToList(), builder, locals, etran, "#Z"); + // Note, in the following line, we do NOT add an assumption about the type antecedent, because we don't yet know that a value even + // exists; rather, we ignore the type antecedent. + var substMap = SetupBoundVarsAsLocals(e.BoundVars.ToList(), out _, builder, locals, etran, "#Z"); Contract.Assert(e.LHSs.Count == e.RHSs.Count); // checked by resolution var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("let#"); for (int i = 0; i < e.LHSs.Count; i++) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index b0005c0cdcb..481128d6f89 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -313,6 +313,11 @@ private BoogieStmtListBuilder GetPostCheckBuilder(Function f, ExpressionTranslat var wh = generator.GetWhereClause(f.tok, funcAppl, f.ResultType, etran, NOALLOC); if (wh != null) { postCheckBuilder.Add(TrAssumeCmd(f.tok, wh)); + if (f.Result != null) { + var resultVarId = new Bpl.IdentifierExpr(f.Result.tok, f.Result.AssignUniqueName(f.IdGenerator), generator.TrType(f.Result.Type)); + wh = generator.GetWhereClause(f.Result.tok, resultVarId, f.Result.Type, etran, NOALLOC); + postCheckBuilder.Add(TrAssumeCmd(f.Result.tok, wh)); + } } // Now for the ensures clauses foreach (AttributedExpression p in f.Ens) { @@ -356,10 +361,8 @@ private List GetWellformednessProcedureOutParameters(Function f, Expre Formal p = f.Result; Contract.Assert(!p.IsOld); Bpl.Type varType = generator.TrType(p.Type); - Expr wh = generator.GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), varType), - p.Type, etran, NOALLOC); - outParams.Add(new Bpl.Formal(p.tok, new TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), varType, wh), - true)); + // Note, this variable should NOT have a "where" clause, because it gets assumed already at the beginning of the CheckWellformed procedure + outParams.Add(new Bpl.Formal(p.tok, new TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), varType), true)); } return outParams; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect index b944b274059..a377a047f95 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect @@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved Dafny program verifier finished with 23 verified, 12 errors -Total resources used is 779029 +Total resources used is 777854 Max resources used by VC is 66829 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect index a13a5837473..522dd947e44 100755 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect @@ -18,7 +18,7 @@ Fuel.legacy.dfy(247,22): Error: assertion might not hold Fuel.legacy.dfy(280,26): Error: assertion might not hold Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(313,41): Related location +Fuel.legacy.dfy(314,93): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location Fuel.legacy.dfy(312,43): Related location @@ -27,13 +27,13 @@ Fuel.legacy.dfy(324,21): Related location Fuel.legacy.dfy(312,58): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,46): Related location +Fuel.legacy.dfy(313,41): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,72): Related location +Fuel.legacy.dfy(314,46): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,93): Related location +Fuel.legacy.dfy(314,72): Related location Fuel.legacy.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple' Fuel.legacy.dfy(335,50): Error: index out of range Fuel.legacy.dfy(336,38): Error: index out of range @@ -43,19 +43,19 @@ Fuel.legacy.dfy(329,21): Related location Fuel.legacy.dfy(311,43): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(312,43): Related location +Fuel.legacy.dfy(313,41): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(313,41): Related location +Fuel.legacy.dfy(314,72): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(312,58): Related location +Fuel.legacy.dfy(314,93): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,72): Related location +Fuel.legacy.dfy(312,58): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,93): Related location +Fuel.legacy.dfy(312,43): Related location Fuel.legacy.dfy(336,71): Error: index out of range Fuel.legacy.dfy(397,22): Error: assertion might not hold Fuel.legacy.dfy(398,22): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect index 6bcabe0f591..8ec3ceb78f0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect @@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold SubsetTypes.dfy(464,13): Error: assertion might not hold Dafny program verifier finished with 13 verified, 91 errors -Total resources used is 775600 +Total resources used is 775200 Max resources used by VC is 101900 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect index f4c5425f64b..06ac196ec16 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect @@ -1,4 +1,4 @@ Dafny program verifier finished with 272 verified, 0 errors -Total resources used is 30526126 +Total resources used is 30525479 Max resources used by VC is 2048364 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect index 8d3900fd2b2..2e3c4a6c7f6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect @@ -1,4 +1,4 @@ Dafny program verifier finished with 276 verified, 0 errors -Total resources used is 28791320 +Total resources used is 28790607 Max resources used by VC is 974212 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy new file mode 100644 index 00000000000..bed0b6dc725 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy @@ -0,0 +1,178 @@ +// RUN: %exits-with 4 %verify --type-system-refresh --general-traits=datatype "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Example0 { + datatype BaseType = Ctor(x: int) + { + predicate i() + } + + type R = r: BaseType | r.i() witness * + + function F0(v: nat): R { // anonymous result value + var o: R := Ctor(v); // error: this BaseType might not be an R + o + } + + function F1(v: nat): (r: R) { // named result value + var o: R := Ctor(v); // error: this BaseType might not be an R + o + } +} + +module Example1 { + datatype BaseType = Ctor(x: int) + { + predicate i() + } + + type R = r: BaseType | r.i() witness * + + function G0(v: nat): R { // anonymous result value + Ctor(v) // error: this BaseType might not be an R + } + + function G1(v: nat): (r: R) { // named result value + Ctor(v) // error: this BaseType might not be an R + } +} + +module Example2 { + type BaseType(!new) + { + predicate i() + } + + type R = r: BaseType | r.i() witness * + + ghost function Ctor(x: nat): R + requires exists b: BaseType :: b.i() + { + var b: BaseType :| b.i(); + b + } + + ghost function F(v: nat): R { + var o: R := Ctor(v); // error: precondition failure (***) as reported in issue 1958, this was once not reported + o + } + + ghost function G0(v: nat): R { // anonymous result value + Ctor(v) // error: precondition failure + } + + ghost function G1(v: nat): (r: R) { // named result value + Ctor(v) // error: precondition failure (***) as reported in issue 1958, this was once not reported + } + + method MF(v: nat) returns (ghost r: R) { + ghost var o: R; + o := Ctor(v); // error: precondition failure + return o; + } + + predicate IsR(r: R) { true } + + method AssignSuchThat() { + var r: R :| IsR(r); // error: cannot establish existence of r + } + + ghost function LetSuchThat(): R { + var r: R :| IsR(r); // error: cannot establish existence of r + r + } +} + +module Example3 { + datatype BaseType = BaseType + { + predicate i() { + false + } + } + + type R = r: BaseType | r.i() witness * + + function Ctor(x: nat): R + requires exists b: BaseType :: b.i() + { + var b: BaseType :| b.i(); + b + } + + function F(v: nat): R { + var o: R := Ctor(v); // error: precondition failure (***) as reported in issue 1958, this was once not reported + o + } + + method Main() { + var r := F(15); + print r, "\n"; + } +} + +// The following tests make sure that the appropriate type information (without allocatedness information) is available +// when checking the _postcondition_ of functions. +module FunctionResultType { + datatype Option = None | Some(value: X) + + function Search0(s: seq, x: T): (o: Option) + ensures + o.Some? && o.value < |s| ==> + s[o.value] == x // in order to prove ".value" is non-negative, the type of "o" is necessary + { + if |s| < 12 then + None + else if s[9] == x then + Some(9) + else if s[2] == x then + Some(2) + else + None + } + + function Search1(s: seq, x: T): Option + ensures var o := Search1(s, x); + o.Some? && o.value < |s| ==> + s[o.value] == x // in order to prove ".value" is non-negative, the type of "Search1(s, x)" and "o" is necessary + { + if |s| < 12 then + None + else if s[9] == x then + Some(9) + else if s[2] == x then + Some(2) + else + None + } + + function Search2(s: seq, x: T): Option + ensures + Search2(s, x).Some? && Search2(s, x).value < |s| ==> + s[Search2(s, x).value] == x // in order to prove ".value" is non-negative, the type of "Search2(s, x)" is necessary + { + if |s| < 12 then + None + else if s[9] == x then + Some(9) + else if s[2] == x then + Some(2) + else + None + } + + function Search4(s: seq, x: T): (o: Option) + ensures + o.Some? && o.value < |s| ==> + s[o.value] == x // error: ".value" may be negative + { + if |s| < 12 then + None + else if s[9] == x then + Some(9) + else if s[2] == x then + Some(2) + else + None + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy.expect new file mode 100644 index 00000000000..7b3eb340bf6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy.expect @@ -0,0 +1,19 @@ +git-issue-1958.dfy(13,16): Error: value does not satisfy the subset constraints of 'R' +git-issue-1958.dfy(18,16): Error: value does not satisfy the subset constraints of 'R' +git-issue-1958.dfy(32,4): Error: value does not satisfy the subset constraints of 'R' +git-issue-1958.dfy(36,4): Error: value does not satisfy the subset constraints of 'R' +git-issue-1958.dfy(56,16): Error: function precondition could not be proved +git-issue-1958.dfy(49,13): Related location: this proposition could not be proved +git-issue-1958.dfy(61,4): Error: function precondition could not be proved +git-issue-1958.dfy(49,13): Related location: this proposition could not be proved +git-issue-1958.dfy(65,4): Error: function precondition could not be proved +git-issue-1958.dfy(49,13): Related location: this proposition could not be proved +git-issue-1958.dfy(70,9): Error: function precondition could not be proved +git-issue-1958.dfy(49,13): Related location: this proposition could not be proved +git-issue-1958.dfy(77,13): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +git-issue-1958.dfy(81,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +git-issue-1958.dfy(104,16): Error: function precondition could not be proved +git-issue-1958.dfy(97,13): Related location: this proposition could not be proved +git-issue-1958.dfy(167,7): Error: index out of range + +Dafny program verifier finished with 6 verified, 12 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/Inputs/seq.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/Inputs/seq.dfy index 47c41a7e993..04fbd516f7c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/Inputs/seq.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/Inputs/seq.dfy @@ -9,9 +9,9 @@ module Seq { { } - function {:opaque} IndexOfOption(s: seq, v: T): (o: Option) + opaque function IndexOfOption(s: seq, v: T): (o: Option) ensures if o.Some? then o.value < |s| && s[o.value] == v && - forall j {:trigger s[j]} :: 0 <= j < o.value ==> s[j] != v + forall j :: 0 <= j < o.value ==> s[j] != v else v !in s { if |s| == 0 then None() diff --git a/docs/dev/news/5877.fix b/docs/dev/news/5877.fix new file mode 100644 index 00000000000..e5744b9787e --- /dev/null +++ b/docs/dev/news/5877.fix @@ -0,0 +1 @@ +Don't assume type information before binding variables (for let expressions and named function results)