search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
714 stars 147 forks source link

Overeager substitution in dead code elimination? #1604

Closed andres-erbsen closed 9 months ago

andres-erbsen commented 1 year ago

It looks like "DCE" inlines a let binder that is in fact used, causing synthesis to fail with Invalid identifier in arithmetic expression Z.zselect. @JasonGross do you have a guess for what is going on here?

After rewriting RewriteArith_0: let x15 := Z.zselect(x13₁, (0, 38)) in

After rewriting DCE after RewriteArith_0: let x14 := Z.add_with_get_carry((2^64), (0, ((Z.zselect(x12₁, (0, 38))), ((x12₂ << 0x140) + x8₁)))) in

Log: https://gist.github.com/andres-erbsen/bbfb1994c4e8294be35c5ab59966faf2#file-sat_add-log-L249-L281 Source: https://github.com/andres-erbsen/fiat-crypto/commit/48c3e62f83241a7ed7538c28c7f32c20ae94d440#diff-fc27e1c96d797f696a0116daf62647b093f90d5f4cf52eba7896076151990554

JasonGross commented 1 year ago

I do not. I guess the DCE calculation is buggy? Strange that it hasn't shown up before this...

JasonGross commented 1 year ago

Hmm, it's possible that the DCE code does not know how to handle lambdas, and the thunked branches of the if statements are messing it up?

JasonGross commented 1 year ago

Nope, the code seems to handle lambdas fine. If you can paste valid Coq code that computes to the expression before DCE, such that vm_compute on DCE results in the mis-inlining, I can try single-stepping it and see what's going on

andres-erbsen commented 1 year ago

There you go: https://github.com/andres-erbsen/fiat-crypto/commit/811460bc3f1fd1952a25258c09f72d2147f73a8e Thank you!

andres-erbsen commented 1 year ago

See also https://github.com/mit-plv/fiat-crypto/pull/1601#issuecomment-1552616795

JasonGross commented 1 year ago

I've tracked down the issue, and indeed it is what I originally suspected: DCE cannot handle code branching that contains lambdas, so it's the if-statements that are causing trouble. The code at https://github.com/mit-plv/fiat-crypto/blob/1cce2381793fde5706f461df6b0174c9dd5ba9d9/src/MiscCompilerPasses.v#L93-L94 and https://github.com/mit-plv/fiat-crypto/blob/1cce2381793fde5706f461df6b0174c9dd5ba9d9/src/MiscCompilerPasses.v#L58-L60 does not propagate the index update from underneath the lambda, and so indices end up being incorrectly reused.

I can think of two solutions:

  1. Thread a boolean of "is in head position", so that we recurse under the initial lambdas, but not under lambdas in the arguments to any App, nor under lambdas in the variable-bindings of let-in
  2. Adjust subst0n' to recurse over the PHOAS expression at two different var arguments, one for tracking the current index, and the other for tracking the returned expression.

Thoughts? (And do you feel confident implementing either of these fixes?)