From ec033c30164dbc798fcb1c27fe01e541d37d3237 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 12 Dec 2024 11:23:30 +0100
Subject: [PATCH] Fix elaboration of function definitions with nested function
 types

Since commit ea3a41b, `elab_type_declarator` has a special case for function definitions, causing it to include the function parameters in the returned updated typing environment.  However, this special case was wrong for nested function types such as
```
int (*f(int y))(int x) { ... }
```
`f` is a function taking an `y` parameter and returning a function `(x: int) -> int`.  The special case causes both `x` and `y` to be included in the returned environment, while only `y` should be.

This commit makes sure that the special case for function definitions applies only to the outermost function type, i.e. the innermost `Cabs.PROTO` declarator.

A similar issue was handled correctly in the `Cabs.PROTO_OLD` case, so this commit tries to use the same code structure in the `PROTO` and `PROTO_OLD` cases.
---
 Changelog.md    |  1 +
 cparser/Elab.ml | 40 +++++++++++++++++++++++-----------------
 test            |  2 +-
 3 files changed, 25 insertions(+), 18 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index dc59898e3..62e251303 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -20,6 +20,7 @@ Code generation and optimization:
 Bug fixes:
 - More robust determination of symbols that may be defined in a shared object. (#538)
 - Escape `$NNN` identifiers in generated x86 and ARM assembly code (#541).
+- Wrong parameter scoping in function definitions such as `int (*f(int y))(int x) { ... }` (a function returning a pointer to a prototyped function).
 
 Usability:
 - Mark stack as non-executable in binaries produced by `ccomp`.
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 3060568b2..d826ca062 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -924,28 +924,34 @@ and elab_type_declarator ?(fundef = false) loc env ty = function
       elab_return_type loc env ty;
       let (ty, a) = get_nontype_attrs env ty in
       let (params', env') = elab_parameters loc env params in
-      (* For a function declaration (fundef = false), the scope introduced
-         to treat parameters ends here, so we discard the extended
-         environment env' returned by elab_parameters.
-         For a function definition (fundef = true) we return the
-         extended environment env' so that it can serve as the basis
-         to elaborating the function body. *)
-      let env'' = if fundef then env' else env in
-      elab_type_declarator ~fundef loc env'' (TFun(ty, Some params', vararg, a)) d
+      let funty = TFun(ty, Some params', vararg, a) in
+      (* For a function declaration (fundef = false or d <> JUSTBASE),
+         the scope introduced to treat parameters ends here, so we
+         discard the extended environment env' returned by
+         elab_parameters.
+         For a function definition (fundef = true and d = JUSTBASE),
+         we return the extended environment env' so that it can serve
+         as the basis to elaborating the function body. *)
+      if fundef && d = Cabs.JUSTBASE then
+        ((funty, None), env')
+      else
+        elab_type_declarator ~fundef loc env funty d
   | Cabs.PROTO_OLD(d, params) ->
       elab_return_type loc env ty;
       let (ty, a) = get_nontype_attrs env ty in
+      let funty = TFun(ty, None, false, a) in
       (* For consistency with the PROTO case above, for a function definition
-         (fundef = true) we open a new scope, even though we do not
-         add any bindings for the parameters. *)
-      let env'' = if fundef then Env.new_scope env else env in
-      match params with
-      | [] ->
-        elab_type_declarator ~fundef loc env'' (TFun(ty, None, false, a)) d
-      | _ ->
-        if not fundef || d <> Cabs.JUSTBASE then
+         (fundef = true and d = JUSTBASE) we open a new scope, even
+         though we do not add any bindings for the parameters. *)
+      if fundef && d = Cabs.JUSTBASE then begin
+        let env' = Env.new_scope env in
+        let opt_params = if params = [] then None else Some params in
+        ((funty, opt_params), env')
+      end else begin
+        if params <> [] then
           fatal_error loc "illegal old-style K&R function definition";
-        ((TFun(ty, None, false, a), Some params), env'')
+        elab_type_declarator ~fundef loc env funty d
+      end
 
 (* Elaboration of parameters in a prototype *)
 
diff --git a/test b/test
index bbfd6c8f3..154895fe4 160000
--- a/test
+++ b/test
@@ -1 +1 @@
-Subproject commit bbfd6c8f3de5d8e38988bd7f27af3a151e239bb4
+Subproject commit 154895fe439c0ca50b60a711c30464509cd72f7f