search

querycert / qcert

Compilation and Verification of Data-Centric Languages
https://querycert.github.io/
Apache License 2.0
56 stars 9 forks source link

WASM: Variable Scoping #145

Closed pkel closed 4 years ago

pkel commented 4 years ago

In its current state, the WASM backend does not correctly handle variable scoping: Wasm variables are function-scoped and the translation assumes that Imp variable names are unique. In case of nested variables with the same name we will run into unexpected behaviour.

This is not yet fixed because we were unsure about the best way of solving the problem.

I claim it's feasible (and fun) to implement scoping in the OCaml code that translates Imp to Wasm. This would have the additional benefit, that local (function scoped) variables could be reused for multiple block-scoped Imp variables, e.g. after leaving a block. Currently there is one function scoped variable per variable name occurring in the Imp function.

On the other hand, it probably makes sense to do this error prone step in the proof assistant. For that, we would probably want to have another intermediate representation that is more Wasm-like (See #146).

pkel commented 4 years ago

Addressed in 8766b38ed12 using OCaml. At some point it will be moved to Coq as part of #146.