Deeply nested conditionals and branch polarity flips

[nikswamy]

I have some code that looks like this in F*:

module NestedIfReturn

module B = LowStar.Buffer
open FStar.HyperStack.ST
open LowStar.BufferOps
let error_case () : ST unit (requires fun h -> True) (ensures fun _ _ _ -> True) = ()
let do_something (b:B.pointer bool) 
: ST unit
  (requires fun h -> B.live h b)
  (ensures fun _ _ h -> B.live h b)
= ()

let test (b:B.pointer bool)
: ST unit (requires fun h -> B.live h b) (ensures fun _ _ _ -> True)
= let has_failed = !*b in
  if has_failed then (error_case(); ())
  else (
    do_something b;
    let has_failed = !*b in
    if has_failed then (error_case(); ())
    else (
      do_something b;
      let has_failed = !*b in
      if has_failed then (error_case(); ())
      else ()
    )
  )

I run krml with -fnoreturn-else and it produces nice looking C code like this:

void NestedIfReturn_test(bool *b)
{
  bool has_failed = *b;
  if (has_failed)
  {
    NestedIfReturn_error_case();
    return;
  }
  NestedIfReturn_do_something(b);
  bool has_failed1 = *b;
  if (has_failed1)
  {
    NestedIfReturn_error_case();
    return;
  }
  NestedIfReturn_do_something(b);
  if (has_failed1)
  {
    NestedIfReturn_error_case();
    return;
  }
}

However, if I remove the calls to error_case like so:

let test (b:B.pointer bool)
: ST unit (requires fun h -> B.live h b) (ensures fun _ _ _ -> True)
= let has_failed = !*b in
  if has_failed then (())
  else (
    do_something b;
    let has_failed = !*b in
    if has_failed then (())
    else (
      do_something b;
      if has_failed then (())
      else ()
    )
  )

And run krml again with the same -fnoreturn-else option, I get code like this:

void NestedIfReturn_test(bool *b)
{
  bool has_failed = *b;
  if (!has_failed)
  {
    NestedIfReturn_do_something(b);
    bool has_failed1 = *b;
    if (!has_failed1)
    {
      NestedIfReturn_do_something(b);
      return;
    }
    return;
  }
}

Note how the branch condition is flipped and the ifs are now nested.

Without the -fnoreturn-else, I get something similar:

void NestedIfReturn_test(bool *b)
{
  bool has_failed = *b;
  if (!has_failed)
  {
    NestedIfReturn_do_something(b);
    bool has_failed1 = *b;
    if (!has_failed1)
      NestedIfReturn_do_something(b);
  }
}

Is this expected? Could it be possible to have the same nice non-nested code even if I don't call some other function like error_case in the if branch?

[msprotz]

I think this: https://github.com/FStarLang/karamel/blob/master/lib/Simplify.ml#L888-L899 is probably preventing the -fnoreturn-else from triggering afterwards.

If this is important, you could make this optimization disabled under -fnoreturn-else...?