Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[BUG] --enable=effects does not adequately clear the stack #1533

Open
JasonGross opened this issue Nov 21, 2023 · 10 comments
Open

[BUG] --enable=effects does not adequately clear the stack #1533

JasonGross opened this issue Nov 21, 2023 · 10 comments
Labels
bug stack-overflow

Comments

@JasonGross
Copy link

JasonGross commented Nov 21, 2023 •
edited

Describe the bug
https://mit-plv.github.io/fiat-crypto/?argv=%5B%22word-by-word-montgomery%22%2C%22p256%22%2C%2232%22%2C%222%5E256-2%5E224%2B2%5E192%2B2%5E96-1%22%5D&interactive
gives

Uncaught RangeError: Maximum call stack size exceeded 
with_bedrock2_fiat_crypto.ml:18450 Uncaught RangeError: Maximum call stack size exceeded
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
    at g (with_bedrock2_fiat_crypto.ml:18450:15)
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450
g @ with_bedrock2_fiat_crypto.ml:18450

fiat_crypto.tar.gz is an tar.gz of the webpage, though you'll need to run a simple server to play with it because it uses webworkers. The input into the input box is word-by-word-montgomery p256 32 2^256-2^224+2^192+2^96-1 in string mode or ["word-by-word-montgomery","p256","32","2^256-2^224+2^192+2^96-1"] in json mode, it takes a couple minutes (?) before throwing the error.

See also #1530 for more details
@JasonGross JasonGross added the bug label Nov 21, 2023
@JasonGross
Copy link
Author

Here's a faster example: https://mit-plv.github.io/fiat-crypto/?argv=%5B%22unsaturated-solinas%22%2C%22--lang%22%2C%22bedrock2%22%2C%22--no-wide-int%22%2C%22--widen-carry%22%2C%22--widen-bytes%22%2C%22--split-multiret%22%2C%22--no-select%22%2C%2225519%22%2C%2264%22%2C%225%22%2C%222%5E255-19%22%2C%22carry_mul%22%2C%22carry_square%22%2C%22carry_scmul121666%22%2C%22carry%22%2C%22add%22%2C%22sub%22%2C%22opp%22%2C%22selectznz%22%2C%22to_bytes%22%2C%22from_bytes%22%5D&interactive

@JasonGross JasonGross mentioned this issue Nov 21, 2023
Merged
@hhugo
Copy link
Member

hhugo commented Nov 21, 2023

I'm getting

Error: Cannot read properties of undefined (reading 'toString'): ["unsaturated-solinas","--lang","bedrock2","--no-wide-int","--widen-carry","--widen-bytes","--split-multiret","--no-select","25519","64","5","2^255-19","carry_mul","carry_square","carry_scmul121666","carry","add","sub","opp","selectznz","to_bytes","from_bytes"]

from your second link.

@JasonGross
Copy link
Author

Yeah, if you open the developer console you'll see the recursion error. (You might need to click "clear cache" and then "synthesize" again.). I'm not sure why webworkers aren't catching the exception

@JasonGross
Copy link
Author

I've pushed a change so that, when it redeploys, the error message should be correctly caught and cached and displayed.

@hhugo
Copy link
Member

hhugo commented Nov 21, 2023

The function causing the stack overflow is not tailrec

let rec append s1 s2 =
  match s1 with
  | [] -> s2
  | c0::s1' -> c0::(append s1' s2)

I would not be surprised if the implementation of effect decided to not cps rewrite such code.

It would be easier to investigate with --pretty enabled.

What version of ocaml are you using ? Adding [@tail_mod_cons] could help.

@JasonGross
Copy link
Author

Here are the .ml sources, if you want to investigate more. It's just one .ml file (and corresponding .mli file), should be fully standalone except for needing -package js_of_ocaml and maybe -package unix -w -20.

Adding [@tail_mod_cons] is a bit tricky, since the code is fully generated by extraction. If I can figure out where the call to append is coming from I might be able to cps it myself, though I worry that I might accumulate so many lambdas that I'd exceed the call stack size? Is there a tail-rec implementation of append that doesn't blow the stack? I guess I could reverse the list twice or something?

@OlivierNicole
Copy link
Contributor

I confirm that append will not be translated to CPS, so stack clearing is not in place on this part of the execution. So this is a “normal” stack overflow due to recursion.

My statements about this in another thread were probably too imprecise. If I’m remembering correctly, only the functions that may transitively call effect performers or continuation resumers are translated to CPS, and thus will "benefit" from regular stack clearing as a side effect.

@hhugo
Copy link
Member

hhugo commented Nov 22, 2023

We could imagine a mode that would perform cps rewriting unconditionally

@vouillon
Copy link
Member

For performance reasons, we perform a partial CPS transformation, keeping as much as we can the code in direct style. The transformation will preserve tail recursion, but non tail recursive functions can still exhaust the stack.

You can just replace your definition of function app by the following:

let rec rev_app l1 l2 =
  match l1 with
    [] -> l2
  | a :: l -> rev_app l (a :: l2)

let app l1 l2 = rev_app (rev_app l1 []) l2

@OlivierNicole
Copy link
Contributor

I don’t know how the code is generated, but for the record, the stdlib has List.rev_append which is tail-recursive, and List.append is now tail-rec since very recently (5.1).

@JasonGross JasonGross mentioned this issue Nov 23, 2023
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug stack-overflow
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@JasonGross @hhugo @vouillon @OlivierNicole