krml redeclares variables in adjacent #if branches
- Dominant language
- OCaml
- Stars
- 519
- Forks
- 73
- Avg merge
- 2h 58m
- Merged PRs (30d)
- 1
Description
Here's a small example:
```
module IfDefKrml
open FStar.HyperStack.ST
open LowStar.Buffer
[@@CIfDef]
assume
val flag : bool
let something_effectful (x:bool) : Stack bool (requires λ _ → ⊤) (ensures (λ _ _ _ → ⊤)) = x
let test (x y:bool) =
let z =
if flag
then false
else let aa = something_effectful x in
aa
in
let z =
if flag
then false
else let aa = something_effectful z in
aa
in z
```
I run `fstar --codegen krml IfDefKrml.fst` to get an `out.krml`. Note, I can repro this behavior even if i use several krml files, instead of a single `out.krml`.
Then, running `krml out.krml` produces the following C code:
```
/*
This file was generated by KaRaMeL
KaRaMeL invocation: ../../clean/everest/everest/karamel/krml out.krml
F* version: 2fd88658
KaRaMeL version: d08eab25
*/
#include "IfDefKrml.h"
bool IfDefKrml_something_effectful(bool x)
{
return x;
}
bool IfDefKrml_test(bool x, bool y)
{
bool z;
#if IFDEFKRML_FLAG
z = false;
#else
bool aa = IfDefKrml_something_effectful(x);
z = aa;
#endif
#if IFDEFKRML_FLAG
return false;
#else
bool aa = IfDefKrml_something_effectful(z);
return aa;
#endif
}
```
But, the C compiler fails with:
```
⚡ Generating object files
✘ [CC,./IfDefKrml.c] (use -verbose to see the output)
./IfDefKrml.c: In function ‘IfDefKrml_test’:
./IfDefKrml.c:29:8: error: redefinition of ‘aa’
29 | bool aa = IfDefKrml_something_effectful(z);
| ^~
./IfDefKrml.c:23:8: note: previous definition of ‘aa’ was here
23 | bool aa = IfDefKrml_something_effectful(x);
| ^~
./IfDefKrml.c: At top level:
cc1: error: unrecognized command line option ‘-Wno-unknown-warning-option’ [-Werror]
cc1: all warnings being treated as errors
Warning 3: run_or_warn: the following command failed:
gcc-9 -I /home/nswamy/clean/everest/everest/karamel/krmllib/dist/minimal -I /home/nswamy/clean/everest/everest/karamel/krmllib -I /home/nswamy/clean/everest/everest/karamel/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-function -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 -c ./IfDefKrml.c -o ./IfDefKrml.o
Warning 3 is fatal, exiting.
```
My hunch is that krml is treating a #if/#else as if it were a scope similar to a regular if/else?
A simple fix could be to emit the code in the #if/#else block delimited within a `{ }`? At least that seems to work fine for me on this example, though I don't know if there are some broader implications of doing that.
Contributor guide
No contributing guide indexed for this repository
Research direction
Reproduce the issue from IfDefKrml.fst with `fstar --codegen krml`, then run `krml out.krml` and inspect the generated IfDefKrml.c. Trace how krml emits the adjacent conditional branches; done means the resulting C compiles without redeclaring `aa`, while preserving the conditional behavior.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- c, ocaml
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 45/100