From 7ad66dba7e6c00f90f71040b0ef5f3742eb13c12 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 13 May 2026 08:14:01 +0000 Subject: [PATCH 1/3] Allow return parameters in preconditions of outline blocks and closures When checking preconditions, we used to reject every reference to an output parameter, regardless of which function-like construct introduced it. This was too strict: output parameters of the surrounding function already have a meaningful value by the time an outline statement or a nested closure literal is entered, so referencing them in the precondition of those constructs is legitimate. The check now only rejects references to output parameters declared by the spec's own owner (function, method, closure literal, interface method, or method implementation proof). For outline statements - which do not declare their own outputs - no output parameter reference is rejected. Fixes #1029. --- .../typing/ghost/GhostMiscTyping.scala | 24 ++++++-- .../resources/regressions/issues/001029.gobra | 60 +++++++++++++++++++ 2 files changed, 79 insertions(+), 5 deletions(-) create mode 100644 src/test/resources/regressions/issues/001029.gobra diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index d384fbaf6..e4722936b 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala @@ -152,9 +152,20 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => implicit lazy val wellDefSpec: WellDefinedness[PSpecification] = createWellDef { case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, isPure, _, isOpaque, _) => + // Collect the named output parameters of the spec's owner so that we only + // reject references to those (and not to outputs of an enclosing function, + // method, or closure - which is relevant for outline statements and nested + // closure literals). + val ownOutParams: Vector[PNamedParameter] = tree.parent(n).head match { + case p: PCodeRootWithResult => p.result.outs.collect { + case np: PNamedParameter => np + case PExplicitGhostParameter(np: PNamedParameter) => np + } + case _ => Vector.empty + } pres.flatMap(assignableToSpec) ++ preserves.flatMap(assignableToSpec) ++ posts.flatMap(assignableToSpec) ++ - preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ - pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ + preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode(_, ownOutParams))) ++ + pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode(_, ownOutParams))) ++ terminationMeasures.flatMap(wellDefTerminationMeasure) ++ // if has conditional clause, all clauses must be conditional // can only have one non-conditional clause @@ -229,13 +240,16 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => isExpr(e).out ++ assignableTo.errors(exprType(e), AssertionT, mayInit)(e) ++ isWeaklyPureExpr(e) } - private def illegalPreconditionNode(n: PNode): Messages = { + private def illegalPreconditionNode(n: PNode, ownOutParams: Vector[PNamedParameter]): Messages = { n match { case PLabeledOld(PLabelUse(PLabelNode.lhsLabel), _) => noMessages case n@ (_: POld | _: PLabeledOld) => message(n, s"old not permitted in precondition") case n@ (_: PBefore) => message(n, s"old not permitted in precondition") - case id: PIdnUse if entity(id).isInstanceOf[SymbolTable.OutParameter] => - message(id, s"output parameter '${id.name}' cannot be referenced in a precondition") + case id: PIdnUse => entity(id) match { + case op: SymbolTable.OutParameter if ownOutParams.exists(_ eq op.decl) => + message(id, s"output parameter '${id.name}' cannot be referenced in a precondition") + case _ => noMessages + } case _ => noMessages } } diff --git a/src/test/resources/regressions/issues/001029.gobra b/src/test/resources/regressions/issues/001029.gobra new file mode 100644 index 000000000..67bf01dd8 --- /dev/null +++ b/src/test/resources/regressions/issues/001029.gobra @@ -0,0 +1,60 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue001029 + +// Output parameters of the surrounding function may be referenced in the +// precondition of an outline statement, because they have a meaningful value +// at the entry of the outline block. (Issue #1029) + +ensures acc(r) && *r == 42 +func foo() (r *int) { + i@ := 0 + r = &i + + requires acc(r) + ensures acc(r) && *r == 42 + outline ( + *r = 42 + ) +} + +// The outer function's output is also accepted in `preserves` clauses of an +// outline statement. +ensures acc(r) && *r == 42 +func foo2() (r *int) { + i@ := 42 + r = &i + + preserves acc(r) && *r == 42 + outline ( + // nothing + ) +} + +// The check still rejects references to a closure's own output parameter in +// the closure's own precondition. +func bad() { + //:: ExpectedOutput(type_error) + c := requires s == 0 + ensures s == 1 + func nested() (s int) { + return 1 + } + _ = c +} + +// An outline block in a function without named output parameters keeps +// type-checking. +func unnamedOut() *int { + i@ := 0 + p := &i + + requires acc(p) + ensures acc(p) && *p == 42 + outline ( + *p = 42 + ) + + return p +} From 2adf85c2213eb5d413f970ddde740aadeca6f745 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 13 May 2026 08:23:11 +0000 Subject: [PATCH 2/3] Address PR review on 001029.gobra - Reword the header comment to refer to outlines and closures. - Add explicit return statements in the positive examples. - Add a positive test case where a nested closure literal's precondition references the outer function's named output parameter. - Drop the redundant outline-with-unnamed-output example. --- .../resources/regressions/issues/001029.gobra | 36 ++++++++++--------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/src/test/resources/regressions/issues/001029.gobra b/src/test/resources/regressions/issues/001029.gobra index 67bf01dd8..b7f64d4b2 100644 --- a/src/test/resources/regressions/issues/001029.gobra +++ b/src/test/resources/regressions/issues/001029.gobra @@ -4,8 +4,7 @@ package issue001029 // Output parameters of the surrounding function may be referenced in the -// precondition of an outline statement, because they have a meaningful value -// at the entry of the outline block. (Issue #1029) +// precondition of an outline statement and closures. ensures acc(r) && *r == 42 func foo() (r *int) { @@ -17,6 +16,7 @@ func foo() (r *int) { outline ( *r = 42 ) + return } // The outer function's output is also accepted in `preserves` clauses of an @@ -30,6 +30,22 @@ func foo2() (r *int) { outline ( // nothing ) + return +} + +// A closure literal declared inside a function may reference the outer +// function's named output parameter in its precondition. +ensures acc(r) && *r == 42 +func foo3() (r *int) { + i@ := 42 + r = &i + + c := requires acc(r) && *r == 42 + func nested() { + // nothing + } + _ = c + return } // The check still rejects references to a closure's own output parameter in @@ -42,19 +58,5 @@ func bad() { return 1 } _ = c -} - -// An outline block in a function without named output parameters keeps -// type-checking. -func unnamedOut() *int { - i@ := 0 - p := &i - - requires acc(p) - ensures acc(p) && *p == 42 - outline ( - *p = 42 - ) - - return p + return } From bd8a52bfb2cd31937d62a3c7c687b2dcbbc4802d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 13 May 2026 10:26:31 +0200 Subject: [PATCH 3/3] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- src/test/resources/regressions/issues/001029.gobra | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/test/resources/regressions/issues/001029.gobra b/src/test/resources/regressions/issues/001029.gobra index b7f64d4b2..7d6de6560 100644 --- a/src/test/resources/regressions/issues/001029.gobra +++ b/src/test/resources/regressions/issues/001029.gobra @@ -44,7 +44,6 @@ func foo3() (r *int) { func nested() { // nothing } - _ = c return } @@ -57,6 +56,5 @@ func bad() { func nested() (s int) { return 1 } - _ = c return }