Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

bug: NewObjE initialisation short-circuiting with mutable variables is changing behaviour #4623

Merged
merged 5 commits into from
Jul 19, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion src/ir_def/check_ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
11 changes: 4 additions & 7 deletions src/ir_def/construct.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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

Expand Down
6 changes: 1 addition & 5 deletions src/ir_interpreter/interpret_ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
13 changes: 5 additions & 8 deletions src/lowering/desugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
3 changes: 3 additions & 0 deletions test/run-drun/4611.mo
Original file line number Diff line number Diff line change
Expand Up @@ -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) });
}
2 changes: 2 additions & 0 deletions test/run-drun/ok/4611.drun-run.ok
Original file line number Diff line number Diff line change
@@ -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
2 changes: 2 additions & 0 deletions test/run-drun/ok/4611.run-ir.ok
Original file line number Diff line number Diff line change
@@ -1 +1,3 @@
{mrec = {bool = true; text = "Hello World!"}; rec = {bool = true; text = "Hello World!"}}
{aool = (); bool = false}
{bool = false; cool = ()}
2 changes: 2 additions & 0 deletions test/run-drun/ok/4611.run-low.ok
Original file line number Diff line number Diff line change
@@ -1 +1,3 @@
{mrec = {bool = true; text = "Hello World!"}; rec = {bool = true; text = "Hello World!"}}
{aool = (); bool = false}
{bool = false; cool = ()}
2 changes: 2 additions & 0 deletions test/run-drun/ok/4611.run.ok
Original file line number Diff line number Diff line change
@@ -1 +1,3 @@
{mrec = {bool = true; text = "Hello World!"}; rec = {bool = true; text = "Hello World!"}}
{aool = (); bool = false}
{bool = false; cool = ()}