Add -goto_for_early_return transformation

[nikswamy]

Adds a new -goto_for_early_return CLI option that rewrites functions
containing early returns to use goto-based control flow. When enabled,
functions with non-tail return statements are transformed so that:

• A return variable (result) is declared at the top with a type-specific
  initializer (e.g. 0 for int32_t, 0U for uint32_t, NULL for pointers;
  omitted for void functions).
• Each return is replaced by an assignment to result followed by goto exit.
• The original body is wrapped in an inner compound to avoid VLA scope
  issues with goto.
• An exit label and final return result are appended at the end.

Fresh name generation avoids collisions with existing identifiers.

This is useful for targets that do not support early returns or where
goto-based control flow is preferred (e.g., certain embedded C dialects).

Changes:

• lib/C11.ml: Add Goto and Label constructors to the stmt type.
• lib/Options.ml: Add goto_for_early_return option.
• lib/GotoForEarlyReturn.ml: New pass implementing the transformation.
• lib/PrintC.ml: Print Goto and Label statements.
• src/Karamel.ml: Wire up CLI flag and pipeline integration.
• test/goto_return/: Diff-based regression test.
• test/Makefile: Add goto-return-test to all target.

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

[protz]

Thanks for the PR. Before I review this in detail, two questions:

• how much of this is AI-generated? we've had AI-generated contributions that turned out to be spurious ([DeepTest] Signed integer division uses C truncation instead of F* Euclidean semantics #706, [DeepTest] Chained bitwise XOR/OR after wrapping arithmetic produces wrong results #693) so knowing would help me adjust my level of scrutiny
• you most likely need to add your new subdirectory into test/Makefile as is done for e.g. sepcomp-test

Let me know once this is ready for review -- I'm assuming draft means draft. Thanks!

[nikswamy]

It is AI co-authored (the commit message is tagged as such).

I have been testing this in EverParse and it seems to work well. I have a couple of small patches coming and then I'll mark it ready for review.

Thanks for the heads-up on including the test ... will do.

[nikswamy]

ping @protz

Would be great to have your feedback and get this to a mergeable state ASAP. We have some clients waiting on the feature.

[protz]

Thanks for the ping. I am at a workshop until tomorrow but expect to have time to review this before the end of the week. Thanks!

[protz]

High-level points.

• I think it this transformation would be easier on CStar instead of C11. C11 is just an abstract syntax tree ready for pretty-printing. I expected this to operate over CStar because 1) we have no transformations currently operating on C11, because it's very low-level and hard to work with, 2) there are already helpers that exist on CStar, such as vars_of and 3) it would save you the contortions you're doing in replace_ident where you have to unpeel the spec-and-decl in a convoluted way (see point 1). Also, returns are already explicit in CStar so it sounds like you'd be better off there, and I don't think it's a big deal to add Label and Goto to CStar for such purposes (it's not type-checked).
• Why do multiple returns imply early return? (comment on has_early_return): void f() { if (true) return; else return; } does not have early returns in my opinion, because both are in terminal position (they do not happen before we reach the end of the function). Perhaps this is a terminology thing, or perhaps the check needs to be updated. Can you clarify? I expected has_early_return would take an extra parameter that indicates whether you're in terminal position, and throw Found when hitting a Return node.
• It might be that you can achieve better code quality by operating on CStar. I notice that you rewrite Return e into { ret_var = e; goto exit } with an additional C.Compound. It feels like it'd be easier to write flatten_compounds on CStar than C11.
• I would error out if a void function returns a value (line 120). Actually, I'd be curious to see what let f (x: unit) = if true then x else () -- I suspect unit-to-void elimination will kick in, but a test case would be helpful
• Another instance of point 3) above: I don't think it's super clear what is_void_return does on the C11 syntactic structure, and this function would be crystal clear in CStar -- also you would avoid matching on bool vs BOOLEAN, etc.
• Your zero-initializer can be { 0 } for all types. This works:

int main() {
  _Bool x = { 0 };
  return x;
}

• Would it make sense to have your test be a pulse test? It would then automatically track the generated C. (And I don't think it has to use pulse.)

Requested changes: switch the pass to operate over CStar + answers to questions above. Thank you!

[nikswamy]

Thanks! A quick response to this part:

Your zero-initializer can be { 0 } for all types.

This was the initial version. I then had it changed to use a type-specific initializer, as this is more idiomatic in the context where we are using it. Would you be okay with retaining a type-specific initializer?

[tahina-pro]

FYI, I force-pushed to 7c5f9cc (with no diffs from e67ac84) because I needed to rebase @nikswamy 's work to the everparse-fstar1 branch, currently used with EverParse master (project-everest/everparse@1afaebb), which is still using F* fstar1. I pushed a corresponding branch accordingly: _goto_for_early_return_fstar1

[protz]

Would you be okay with retaining a type-specific initializer?

Yes absolutely. It also sounds like it would lend itself well to a general-purpose helper at the CStar level, to compute a default value for a type, if possible.

[nikswamy]

hi Jonathan, Thanks for taking a look, much appreciated.

I think it this transformation would be easier on CStar instead of C11. C11 is just an abstract syntax tree ready for pretty-printing.

It is now implemented on the CStar AST

Why do multiple returns imply early return? (comment on has_early_return): void f() { if (true) return; else return; } does not have early returns in my opinion, because both are in terminal position (they do not happen before we reach the end of the function). Perhaps this is a terminology thing, or perhaps the check needs to be updated. Can you clarify? I expected has_early_return would take an extra parameter that indicates whether you're in terminal position, and throw Found when hitting a Return node.

I think the main point of this transformation is to produce code that has a single return point in the function, e.g., so that one can insert cleanup code, debug code etc. at that one point. Do you have a suggestion for what to call this transformation?

Actually, I'd be curious to see what let f (x: unit) = if true then x else () -- I suspect unit-to-void elimination will kick in, but a test case would be helpful

Such a test case is added.

Would it make sense to have your test be a pulse test? It would then automatically track the generated C. (And I don't think it has to use pulse.)

"It would then automatically track the generated C": I'm not sure what you mean by this.

[protz]

"It would then automatically track the generated C": I'm not sure what you mean by this.

Tests in this directory https://github.com/FStarLang/karamel/blob/master/test/pulse/Makefile have their corresponding C output under version control, without the need for a separate subfolder and Makefile. I think it'd be a nice simplification to move your test to that subdirectory, so that you can get rid of your custom test/goto_return/Makefile -- @mtzguido set up that new test infrastructure and can confirm

Thanks for your response to the other comments. I'll do another round of review shortly, but first question from a quick glance: what prevents you from reusing vars_of, in CStarToC11.ml? It seems to do essentially the same thing as your collect_names

[mtzguido]

Tests in this directory https://github.com/FStarLang/karamel/blob/master/test/pulse/Makefile have their corresponding C output under version control, without the need for a separate subfolder and Makefile. I think it'd be a nice simplification to move your test to that subdirectory, so that you can get rid of your custom test/goto_return/Makefile -- @mtzguido set up that new test infrastructure and can confirm

Yes I think putting the .fst and .ml.expected there and adding $(OUTPUT_DIR)/GotoReturn.c: KRML_FLAGS += -goto_for_early_return should be enough. (btw should this flag also be named -fsomething?)

[protz]

(btw should this flag also be named -fsomething?)

yes