bug: NewObjE initialisation short-circuiting with mutable variables…

… is changing behaviour (#4623)

This PR extends testcase `run-drun/4611.mo` to demonstrate evaluation order problem in the presence of side-effects.

For reading mutable variables it is relevant when the read happens. If there is an assignment to the mutable cell in-between two reads (also via some call or aliased cell) then the read result will differ.

In #4611 we change the point in time when a mutable variable was read, so a test can be fabricated to create a discrepancy between the reference interpreter and the other executions.

This PR backs out the flawed logic of #4611, but keep the test.

To properly fix such an optimisation one needs a hint whether the variable we read from is mutable. If so, the variable rebinding needs to be kept.

One could (contextually) lower mutable reads to a primitive (see C compiler's `volatile` lowering) or have `VarE` with an additional type field (`ref typ`) that gets filled by the type checker.

src/ir_def/check_ir.ml

@@ -1067,7 +1067,6 @@ and type_exp_field env s f : T.field =
     with Not_found -> error env f.at "field typing for %s not found" name
   in
   assert (t <> T.Pre);
-  let t = T.(match f.note with Mut _ -> t | _ -> as_immut t) in
   check_sub env f.at t f.note;
   if not (T.is_typ t) then begin
     check env f.at ((s = T.Actor) ==> T.is_shared_func t)

src/ir_def/construct.ml

@@ -749,7 +749,8 @@ let unreachableE () =
   loopE (unitE ())
 
 let objE sort typ_flds flds =
-  let rec go ds fields fld_tys = function
+  let rec go ds fields fld_tys flds =
+    match flds with
     | [] ->
       blockE
         (List.rev ds)
@@ -758,17 +759,13 @@ let objE sort typ_flds flds =
               ((List.map (fun (id,c) -> (id, T.Typ c)) typ_flds)
                @ fld_tys)))
     | (lab, exp)::flds ->
-      let v, addv = match exp.it with
-        | VarE v -> var v (typ exp), fun _ ds -> ds
-        | _ ->
-          let v = fresh_var lab (typ exp) in
-          v, fun exp ds -> letD v exp :: ds in
+      let v = fresh_var lab (typ exp) in
       let field = {
         it = {name = lab; var = id_of_var v};
         at = no_region;
         note = typ exp
       } in
-      go (addv exp ds) (field::fields) ((lab, typ exp)::fld_tys) flds
+      go ((letD v exp)::ds) (field::fields) ((lab, typ exp)::fld_tys) flds
   in
   go [] [] [] flds
 

src/ir_interpreter/interpret_ir.ml

@@ -600,11 +600,7 @@ and interpret_fields env fs =
     let ve =
       List.fold_left
         (fun ve (f : field) ->
-         let v = match f.note, Lib.Promise.value (find f.it.var env.vals) with
-           | T.Mut _, v -> v
-           | _, V.Mut v -> !v (* immutable field, read mutable box *)
-           | _, v -> v in
-         V.Env.disjoint_add f.it.name v ve
+          V.Env.disjoint_add f.it.name (Lib.Promise.value (find f.it.var env.vals)) ve
         ) V.Env.empty fs in
     V.Obj ve
 

src/lowering/desugar.ml

@@ -592,19 +592,17 @@ and exp_field obj_typ ef =
     let id' = fresh_var id.it typ in
     let d = varD id' (exp e) in
     let f = { it = I.{ name = id.it; var = id_of_var id' }; at = no_region; note = typ } in
-    (Some d, f)
+    (d, f)
   | S.Const ->
     let typ = match T.lookup_val_field_opt id.it fts with
       | Some typ -> typ
       | None -> e.note.S.note_typ
     in
     assert (not (T.is_mut typ));
-    let e = exp e in
-    let id', d_opt = match e.it with
-    | I.VarE v -> var v typ, None
-    | _ -> let id' = fresh_var id.it typ in id', Some (letD id' e) in
+    let id' = fresh_var id.it typ in
+    let d = letD id' (exp e) in
     let f = { it = I.{ name = id.it; var = id_of_var id' }; at = no_region; note = typ } in
-    (d_opt, f)
+    (d, f)
 
 and obj obj_typ efs bases =
   let open List in
@@ -636,8 +634,7 @@ and obj obj_typ efs bases =
   let ds, fs = map (exp_field obj_typ) efs |> split in
   let ds', fs' = concat_map gap (T.as_obj obj_typ |> snd) |> split in
   let obj_e = newObjE T.Object (append fs fs') obj_typ in
-  let decs = append base_decs (append (filter_map (fun o -> o) ds) ds') in
-  (blockE decs obj_e).it
+  I.BlockE(append base_decs (append ds ds'), obj_e)
 
 and typ_binds tbs = List.map typ_bind tbs
 

test/run-drun/4611.mo

@@ -9,4 +9,7 @@ actor {
     assert mrec.bool;  // check no aliasing between bool and mrec.bool
     let summary = debug_show { rec; mrec };
     Prim.debugPrint summary;
+    // check that all executions work the same way
+    Prim.debugPrint (debug_show { bool; aool = (bool := false) });
+    Prim.debugPrint (debug_show { bool; cool = (bool := true) });
 }

test/run-drun/ok/4611.drun-run.ok

@@ -1,3 +1,5 @@
 ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101
 debug.print: {mrec = {bool = true; text = "Hello World!"}; rec = {bool = true; text = "Hello World!"}}
+debug.print: {aool = (); bool = false}
+debug.print: {bool = false; cool = ()}
 ingress Completed: Reply: 0x4449444c0000

test/run-drun/ok/4611.run-ir.ok

@@ -1 +1,3 @@
 {mrec = {bool = true; text = "Hello World!"}; rec = {bool = true; text = "Hello World!"}}
+{aool = (); bool = false}
+{bool = false; cool = ()}

test/run-drun/ok/4611.run-low.ok

@@ -1 +1,3 @@
 {mrec = {bool = true; text = "Hello World!"}; rec = {bool = true; text = "Hello World!"}}
+{aool = (); bool = false}
+{bool = false; cool = ()}

test/run-drun/ok/4611.run.ok

@@ -1 +1,3 @@
 {mrec = {bool = true; text = "Hello World!"}; rec = {bool = true; text = "Hello World!"}}
+{aool = (); bool = false}
+{bool = false; cool = ()}