FStarLang / FStarLang/karamel

krml redeclares variables in adjacent #if branches

Open
#293 0 comments 0 reactions 0 assignees View on GitHub
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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.