krml redeclares variables in adjacent #if branches

[nikswamy]

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 <https://github.com/FStarLang/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.