Functional update optimization is not performed

[857b]

According to the KaRaMeL user manual, the following repro should be compiled to a C struct mutation x->fld_a = 1:

module Main
module B = LowStar.Buffer
module U32 = FStar.UInt32
open LowStar.BufferOps
open FStar.HyperStack.ST

type test_struct = { fld_a : U32.t; fld_b : U32.t }

let test_set_field (x : B.pointer test_struct)
  : Stack unit (requires fun h -> B.live h x) (ensures fun _ _ _ -> True)
  =
    x.(0ul) <- { x.(0ul) with fld_a = 1ul }

However krml (70084646) generates the following output:

// Main.c: $KRML_HOME/krml -skip-compilation Main.fst -bundle Main=*
#include "Main.h"

void Main_test_set_field(Main_test_struct *x)
{
  x[0U] = ((Main_test_struct){ .fld_a = (uint32_t)1U, .fld_b = x->fld_b });
}

Replacing the buffer read and update with the pointer operators !* and *= does not trigger the optimization either.

[857b]

The optimization is performed if one writes:

let xv = x.(0ul) in
x.(0ul) <- { xv with fld_a = 1ul }

Using !* or *= inhibits it.

[msprotz]

So it turns out that this optimization disappeared because of another optimization broke its pattern-matching. I re-instated the optimization to begin with so that this now works:

let f (p: B.buffer point): Stack unit
  (requires (fun h -> B.live h p /\ B.length p = 1))
  (ensures (fun _ _ _ -> True))
=
  p.(0ul) <- ({ p.(0ul) with x = 0l })

I need to extend the pattern-matching to recognize the version with the short operators.

[857b]

9ed0675 works for nearly all the examples I have.
However I encountered this example for which the optimization is not performed:

type test_struct = { fld_a : U32.t; fld_b : U32.t; fld_c : U32.t }
noeq type indir = { ind_ref : B.pointer test_struct; other : U32.t }

let test_set_field2 (r : indir)
  : Stack unit (requires fun h -> B.live h r.ind_ref) (ensures fun _ _ _ -> True)
  =
    r.ind_ref.(0ul) <- { r.ind_ref.(0ul) with fld_a = 1ul }

krml outputs:

Main_test_struct uu____0 = r.ind_ref[0U];
r.ind_ref[0U] =
  ((Main_test_struct){ .fld_a = (uint32_t)1U, .fld_b = uu____0.fld_b, .fld_c = uu____0.fld_c });

whereas it outputs r.ind_ref->fld_a = 1 for a structure with only two fields.
One can let-bind the updated pointer:

let p = r.ind_ref in
p.(0ul) <- { p.(0ul) with fld_a = 1ul }

to obtain

Main_test_struct *p = r.ind_ref;
p->fld_a = (uint32_t)1U;

[msprotz]

Thanks, I generalized the earlier optimization to take this case into account too. Your example should now work with 4adf42e and I've updated the test file accordingly. Thanks.