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

Functional updates, try 2 #260

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open
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
3 changes: 3 additions & 0 deletions src/Karamel.ml
Original file line number Diff line number Diff line change
Expand Up @@ -627,6 +627,9 @@ Supported options:|}
let files = Simplify.remove_unused files in
let files = if !Options.tail_calls then Simplify.tail_calls files else files in
let files = Simplify.simplify2 files in
(* TODO: Inlining.drop_unused here, since this creates more opportunities for
elimination (see comment in functional_updates; also true for
Simplify.remove_unused). *)
let files = if Options.(!merge_variables <> No) then SimplifyMerge.simplify files else files in
if !arg_print_structs then
print PrintAst.print_files files;
Expand Down
140 changes: 130 additions & 10 deletions src/Simplify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -561,6 +561,10 @@ let functional_updates = object (self)

val mutable make_mut = []

(* The general case with >= 3 fields reveals a let-binding. This assumes we
run after `hoist` to avoid nested let-bindings. This has the disadvantage
that for the version with operators, we leave superfluous monomorphized
instances of the operators in the file without eliminating them. *)
method! visit_ELet env b e1 e2 =
let b = self#visit_binder env b in
let e1 = self#visit_expr env e1 in
Expand All @@ -573,33 +577,42 @@ let functional_updates = object (self)
true
) fields in
if List.length the_field = 1 then
let e1 = match e1.node with
| EApp ({ node = EQualified (["LowStar"; "BufferOps"], op2); _ }, [ e2 ])
when KString.starts_with op2 "op_Bang_Star" ->
with_type e1.typ (EBufRead (e2, Helpers.zerou32))
| _ -> e1
in
let the_field, the_expr = List.hd the_field in
let the_field = Option.must the_field in
let the_expr = self#visit_expr env (snd (open_binder b the_expr)) in
let the_expr = DeBruijn.subst e1 0 the_expr in
let the_expr = self#visit_expr env the_expr in
make_mut <- (assert_tlid e1.typ, the_field) :: make_mut;
k (EAssign (with_type the_expr.typ (EField (e1, the_field)), the_expr))
else
ELet (b, e1, self#visit_expr env e2)
in

match e1.node, e2.node with
| EBufRead ({ node = EBound i; _ }, j),
EBufWrite ({ node = EBound iplusone; _ }, j', { node = EFlat fields; _ })
when j = j' && iplusone = i + 1 ->
(* Not in terminal position, no shorthand operators. *)
| EBufRead (e1, j),
EBufWrite (e1', j', { node = EFlat fields; _ })
when j = j' && e1' = DeBruijn.lift 1 e1 ->
(* let uu = (Bound i)[j];
* (Bound (i + 1))[j] <- { fi = ei } with ei = e if i = k, (Bound 0).fi otherwise
* (Bound (i + 1))[j] <- { f0 = (Bound 0).f0; ... except fk = e }
* -->
* (Bound i)[j].fk <- (unlift 1 e)
*)
make_assignment fields (fun x -> x)

| EBufRead ({ node = EBound i; _ }, j),
(* In terminal position, no shorthand operators. *)
| EBufRead (e1, j),
ELet (b,
{ node = EBufWrite ({ node = EBound iplusone; _ }, j', { node = EFlat fields; _ }); _ },
{ node = EBufWrite (e1', j', { node = EFlat fields; _ }); _ },
e3)
when j = j' && iplusone = i + 1 ->
when j = j' && e1' = DeBruijn.lift 1 e1 ->
(* let uu = (Bound i)[j];
* let _ = (Bound (i + 1))[j] <- { fi = ei } with ei = e if i = k, * (Bound 0).fi otherwise in
* let _ = (Bound (i + 1))[j] <- { fi = (Bound 0).fi, except fk = e } in
* e3
* -->
* let _ = (Bound i)[j].fk <- (unlift 1 e) in
Expand All @@ -609,9 +622,102 @@ let functional_updates = object (self)
let e3 = self#visit_expr env (snd (open_binder b e3)) in
ELet (b, with_unit x, e3))

(* Not in terminal position, both shorthand operators. *)
| EApp ({ node = EQualified (["LowStar"; "BufferOps"], op2); _ }, [ e1 ]),
EApp ({ node = EQualified (["LowStar"; "BufferOps"], op1); _ },
[ e1'; { node = EFlat fields; _ } ])
when
KString.starts_with op1 "op_Star_Equals" &&
KString.starts_with op2 "op_Bang_Star" &&
e1' = DeBruijn.lift 1 e1
->
(* let uu = !* e1 in
* e1 *= { fi = uu.fi except fk = e2 } *)
make_assignment fields (fun x -> x)

(* In terminal position, both shorthand operators. *)
| EApp ({ node = EQualified (["LowStar"; "BufferOps"], op2); _ }, [ e1 ]),
ELet (b,
{ node = EApp ({ node = EQualified (["LowStar"; "BufferOps"], op1); _ },
[ e1'; { node = EFlat fields; _ } ]); _ },
e3)
when
KString.starts_with op1 "op_Star_Equals" &&
KString.starts_with op2 "op_Bang_Star" &&
e1' = DeBruijn.lift 1 e1
->
make_assignment fields (fun x ->
let e3 = self#visit_expr env (snd (open_binder b e3)) in
ELet (b, with_unit x, e3))

| _ ->
ELet (b, e1, self#visit_expr env e2)

(* The two cases below cover the case where there are only two fields in the
record, meaning that there is no intermediate variable (of the form uu_...)
being introduced for the dereference expression. *)
method! visit_EApp env e es =
let e = self#visit_expr env e in
let es = List.map (self#visit_expr env) es in
match e.node, es with
| EQualified (["LowStar"; "BufferOps"], op1),
[ e1; { node = EFlat fields; _ } ]
when KString.starts_with op1 "op_Star_Equals" ->
(* e1: (buf t) *= { fi = (!* e1).fi except fk = e } *)
let f, _ = List.partition (function
| Some f, { node =
EField ({ node =
EApp ( { node =
EQualified (["LowStar"; "BufferOps"], op2); _ },
[ e1' ]); _ }, f'); _ }
when f = f' && e1 = e1' && KString.starts_with op2 "op_Bang_Star" ->
false
| _ ->
true
) fields in
begin match f with
| [ Some f, e ] ->
let t = assert_tbuf e1.typ in
make_mut <- (assert_tlid t, f) :: make_mut;
EAssign (with_type e.typ (
EField (
with_type t (EBufRead (e1, Helpers.zerou32)),
f)),
e)
| _ ->
EApp (e, es)
end
| _ ->
EApp (e, es)

method! visit_EBufWrite env e1 e2 e3 =
let e1 = self#visit_expr env e1 in
let e2 = self#visit_expr env e2 in
let e3 = self#visit_expr env e3 in
(* bufwrite (e1, e2, { fi = bufread (e1, e2).fi except fk = e }) *)
match e3.node with
| EFlat fields ->
let f, _ = List.partition (function
| Some f, { node = EField ({ node = EBufRead (e1', e2'); _ }, f'); _ }
when f = f' && e1 = e1' && e2 = e2' ->
false
| _ ->
true
) fields in
begin match f with
| [ Some f, e ] ->
make_mut <- (assert_tlid e3.typ, f) :: make_mut;
EAssign (with_type e.typ (
EField (
with_type e3.typ (EBufRead (e1, e2)),
f)),
e)
| _ ->
EBufWrite (e1, e2, e3)
end
| _ ->
EBufWrite (e1, e2, e3)

(* The same object is called a second time with the mark_mut flag set to true
* to mark those fields that now ought to be mutable *)
method! visit_DType mark_mut name flags n def =
Expand Down Expand Up @@ -663,7 +769,7 @@ let misc_cosmetic = object (self)
| _ ->
EIfThenElse (e1, e2, e3)

(* &x[0] --> x *)
(* &(x[0]) --> x *)
method! visit_EAddrOf env e =
let e = self#visit_expr env e in
match e.node with
Expand All @@ -672,6 +778,7 @@ let misc_cosmetic = object (self)
| _ ->
EAddrOf e

(* (&x)[0] --> x *)
method! visit_EBufRead env e1 e2 =
let e1 = self#visit_expr env e1 in
let e2 = self#visit_expr env e2 in
Expand All @@ -681,6 +788,18 @@ let misc_cosmetic = object (self)
| _ ->
EBufRead (e1, e2)

(* *(&x) --> x *)
method! visit_EApp env e es =
let e = self#visit_expr env e in
let es = List.map (self#visit_expr env) es in
match e.node, es with
| EQualified (["LowStar"; "BufferOps"], op2),
[ { node = EAddrOf e2; _ } ]
when KString.starts_with op2 "op_Bang_Star" ->
e2.node
| _ ->
EApp (e, es)

method! visit_EBufWrite env e1 e2 e3 =
let e1 = self#visit_expr env e1 in
let e2 = self#visit_expr env e2 in
Expand Down Expand Up @@ -1689,6 +1808,7 @@ end
let simplify0 (files: file list): file list =
let files = remove_local_function_bindings#visit_files () files in
let files = count_and_remove_locals#visit_files [] files in
let files = misc_cosmetic#visit_files () files in
let files = remove_uu#visit_files () files in
let files = remove_proj_is#visit_files () files in
let files = combinators#visit_files () files in
Expand Down
64 changes: 64 additions & 0 deletions test/FunctionalUpdate.fst
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
module FunctionalUpdate

module B = LowStar.Buffer
open LowStar.BufferOps
open FStar.HyperStack.ST

type point = {
x: (x:Int32.t { 0 <= Int32.v x && Int32.v x <= 2 });
y: (y:Int32.t { 0 <= Int32.v y && Int32.v y <= 2 });
}

type point3d = {
x: (x:Int32.t { 0 <= Int32.v x && Int32.v x <= 2 });
y: (y:Int32.t { 0 <= Int32.v y && Int32.v y <= 2 });
z: (z:Int32.t { 0 <= Int32.v z && Int32.v z <= 2 });
}

noeq type point_indir = { point_ref : B.pointer point3d; other : Int32.t }

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

let g1 (p: B.buffer point): Stack unit
(requires (fun h -> B.live h p /\ B.length p = 1))
(ensures (fun _ _ _ -> True))
=
let open LowStar.BufferOps in
p *= ({ !*p with y = 0l })

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

let g2 (p: B.buffer point3d): Stack unit
(requires (fun h -> B.live h p /\ B.length p = 1))
(ensures (fun _ _ _ -> True))
=
let open LowStar.BufferOps in
p *= ({ !*p with y = 0l })

let test_set_field2 (r: point_indir)
: Stack unit (requires fun h -> B.live h r.point_ref) (ensures fun _ _ _ -> True)
=
r.point_ref.(0ul) <- { r.point_ref.(0ul) with z = 0l }

let main (): St Int32.t =
push_frame ();
let r1 = B.alloca (({ x = 1l; y = 2l } <: point)) 1ul in
f1 r1;
g1 r1;
let r2: B.buffer point3d = B.alloca ({ x = 1l; y = 2l; z = 2l }) 1ul in
f2 r2;
g2 r2;
test_set_field2 ({ point_ref = r2; other = 0l });
let ret = (!*r1).x `Int32.add` (!*r1).y `Int32.add` (!*r2).x `Int32.add` (!*r2).y `Int32.add` (!*r2).z in
pop_frame ();
ret
3 changes: 1 addition & 2 deletions test/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ ifneq ($(RECENT_GCC),"yes")
FILES := $(filter-out Debug.test,$(FILES))
endif

CUSTOM = count-eq count-uu check-unused check-no-constructor check-no-erased
CUSTOM = count-pointer count-eq count-uu check-unused check-no-constructor check-no-erased
WASM_FILES = \
WasmTrap.wasm-test Wasm1.wasm-test Wasm2.wasm-test Wasm3.wasm-test \
Wasm4.wasm-test Wasm5.wasm-test Wasm6.wasm-test Wasm7.wasm-test \
Expand Down Expand Up @@ -184,7 +184,6 @@ count-point: $(OUTPUT_DIR)/FunctionalUpdate.exe
[ `grep point $(OUTPUT_DIR)/FunctionalUpdate.out/FunctionalUpdate.c | wc -l` = 9 ]
[ `grep uu___ $(OUTPUT_DIR)/FunctionalUpdate.out/FunctionalUpdate.c | wc -l` = 0 ]


check-unused: $(OUTPUT_DIR)/Unused_B.exe
egrep -q 'gets_eliminated.*foobar\)' $(OUTPUT_DIR)/Unused_B.out/Unused_A.c

Expand Down