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

[JasonGross]

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]

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

[hhugo]

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]

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]

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

[hhugo]

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]

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]

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]

We could imagine a mode that would perform cps rewriting unconditionally

[vouillon]

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]

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).