Skip to content

Commit

Permalink
Myriad of small things
Browse files Browse the repository at this point in the history
  • Loading branch information
@protz
protz committed Apr 8, 2024
1 parent 402f38f commit 95f0615
Show file tree
Hide file tree
Showing 3 changed files with 82 additions and 21 deletions.
13 changes: 12 additions & 1 deletion bin/main.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ Supported options:|}
];
));
Krml.(Warn.parse_warn_error !Options.warn_error);
Krml.(Warn.parse_warn_error "-6");

Krml.Helpers.is_readonly_builtin_lid_ :=
(let is_readonly_pure_lid_ = !Krml.Helpers.is_readonly_builtin_lid_ in
Expand Down Expand Up @@ -120,6 +121,7 @@ Supported options:|}
Printf.printf "3️⃣ Monomorphization, datatypes\n";
let files = if runtime_cg then Eurydice.RuntimeCg.disable_cg_monomorphization#visit_files () files else files in
let files = Krml.Monomorphization.functions files in
Eurydice.Logging.log "Phase2.4" "%a" pfiles files;
let files = Krml.Monomorphization.datatypes files in
Eurydice.Logging.log "Phase2.5" "%a" pfiles files;
let files =
Expand All @@ -144,30 +146,39 @@ Supported options:|}
let files = Krml.DataTypes.optimize files in
let _, files = Krml.DataTypes.everything files in
let files = Eurydice.Cleanup2.remove_trivial_ite#visit_files () files in
Eurydice.Logging.log "Phase2.65" "%a" pfiles files;
let files = Eurydice.Cleanup2.remove_trivial_into#visit_files () files in
let files = Krml.Structs.pass_by_ref files in
let files = Eurydice.Cleanup2.remove_literals#visit_files () files in
let files = Krml.Simplify.optimize_lets files in
(* let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in *)
Eurydice.Logging.log "Phase2.7" "%a" pfiles files;
let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files (0, 0) files in
Eurydice.Logging.log "Phase2.71" "%a" pfiles files;
let files = Krml.Simplify.sequence_to_let#visit_files () files in
Eurydice.Logging.log "Phase2.72" "%a" pfiles files;
let files = Krml.Simplify.hoist#visit_files [] files in
let files = Krml.Simplify.fixup_hoist#visit_files () files in
Eurydice.Logging.log "Phase2.75" "%a" pfiles files;
let files = Krml.Simplify.misc_cosmetic#visit_files () files in
let files = Krml.Simplify.let_to_sequence#visit_files () files in
let files = Krml.Inlining.cross_call_analysis files in
Eurydice.Logging.log "Phase2.8" "%a" pfiles files;
let files = Krml.Simplify.remove_unused files in
let files = Eurydice.Cleanup2.remove_array_from_fn#visit_files () files in
(* Macros stemming from globals *)
let files, macros = Eurydice.Cleanup2.build_macros files in
let files = if runtime_cg then Eurydice.RuntimeCg.erase_and_decay_cgs#visit_files (0, 0) files else files in
Eurydice.Logging.log "Phase2.9" "%a" pfiles files;
let files = if runtime_cg then Eurydice.RuntimeCg.decay_cgs#visit_files (0, 0) files else files in


Eurydice.Logging.log "Phase3" "%a" pfiles files;
let errors, files = Krml.Checker.check_everything ~warn:true files in
if errors then
exit 1;

let files = if runtime_cg then Eurydice.RuntimeCg.erase_cgs#visit_files (0, 0) files else files in

let scope_env = Krml.Simplify.allocate_c_env files in
let files = Eurydice.Cleanup3.decay_cg_externals#visit_files (scope_env, false) files in
let macros =
Expand Down
28 changes: 25 additions & 3 deletions lib/Cleanup2.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,11 @@ let expr_of_array_length (n_cgs, i) = function
| TCgArray (_, n) -> with_type (TInt SizeT) (expr_of_cg n_cgs i n)
| _ -> failwith "impossible"

let decay x =
match x.typ with
| TArray (t, _) | TCgArray (t, _) -> { x with typ = TBuf (t, false) }
| _ -> x

let remove_implicit_array_copies = object(self)

inherit Krml.DeBruijn.map_counting_cg as super
Expand All @@ -53,10 +58,16 @@ let remove_implicit_array_copies = object(self)
in
(nest 0 es).node
| _ ->
(* We need to decay the types because the cg-runtime compilation scheme
sometimes is too smart for its own good, and ends up finding the only
suitable monomorphization, which combined with single-field data type
elimination, tells us *statically* that we have an array for this
subexpression, which is stronger than what the type-checker
concludes... *)
let zero = Krml.(Helpers.zero Constant.SizeT) in
(* let _ = *)
ELet (H.sequence_binding (),
H.with_unit (EBufBlit (rhs, zero, lhs, zero, n)),
H.with_unit (EBufBlit (decay rhs, zero, decay lhs, zero, n)),
lift 1 (self#visit_expr_w env e2))

method! visit_ELet env b e1 e2 =
Expand All @@ -72,6 +83,7 @@ let remove_implicit_array_copies = object(self)
let env = self#extend (fst env) b in
(* let _ = blit e1 (a.k.a. src) b (a.k.a. dst) in *)
ELet (H.sequence_binding (),
(* TODO: possibly need decay here *)
H.with_unit (EBufBlit (lift 1 e1, zero, with_type b.typ (EBound 0), zero, n)),
(* -- crossing second binder, not #extending since this is going to be lifted by one *)
(* e2 *)
Expand Down Expand Up @@ -230,8 +242,18 @@ let remove_trivial_into = object(self)
let e = self#visit_expr_w () e in
let es = List.map (self#visit_expr env) es in
match e.node, es with
| ETApp ({ node = EQualified (["core"; "convert"; _ ], "into"); _ }, [], [ t1; t2 ]), [ e1 ] when t1 = t2 ->
e1.node
| ETApp ({ node = EQualified (["core"; "convert"; _ ], "into"); _ }, [], [ t1; t2 ]), [ e1 ] ->
begin match t1, t2 with
| _ when t1 = t2 ->
e1.node
| TCgArray (t1', _), TArray (t2', _) when t1' = t2' ->
(* Resolution of runtime cg found only a single choice that,
in combination with single-element data type elimination, now
gives us knowledge that there's only possible choice... *)
ECast (e1, t2)
| _ ->
EApp (e, es)
end
| _ ->
EApp (e, es)
end
Expand Down
62 changes: 45 additions & 17 deletions lib/RuntimeCg.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@


open Krml.Ast
open Krml.PrintAst.Ops

module H = Krml.Helpers

Expand Down Expand Up @@ -72,9 +73,9 @@ let enumerate_cg_monomorphizations files =
let known = Hashtbl.mem Krml.MonomorphizationState.state (t, ts, cgs) in
let builtin = match List.hd (fst t) with "Eurydice" | "core" -> true | _ -> false in
if known then
Krml.(let open PrintAst.Ops in KPrint.bprintf "KNOWN: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
Krml.(KPrint.bprintf "KNOWN: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
else if not builtin then begin
Krml.(let open PrintAst.Ops in KPrint.bprintf "RUNTIME_MONOMORPHIZATION: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
Krml.(KPrint.bprintf "RUNTIME_MONOMORPHIZATION: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
if Hashtbl.mem known_concrete_arguments t then begin
let existing = Hashtbl.find known_concrete_arguments t in
if not (List.mem (ts, cgs) existing) then
Expand All @@ -98,11 +99,11 @@ let enumerate_cg_monomorphizations files =
match decl with
| DFunction (_, _, n_cgs, n, _, _, _, _) ->
if n_cgs = 0 && n = 0 then
let _ = Krml.(KPrint.bprintf "Visiting %a\n" PrintAst.Ops.plid (lid_of_decl decl)) in
let _ = Krml.(KPrint.bprintf "Visiting %a\n" plid (lid_of_decl decl)) in
super#visit_decl env decl
| DGlobal (_, _, n, _, _) ->
if n = 0 then
let _ = Krml.(KPrint.bprintf "Visiting %a\n" PrintAst.Ops.plid (lid_of_decl decl)) in
let _ = Krml.(KPrint.bprintf "Visiting %a\n" plid (lid_of_decl decl)) in
super#visit_decl env decl
| _ ->
()
Expand All @@ -124,7 +125,7 @@ let enumerate_cg_monomorphizations files =
let cgs, _ = Krml.KList.split n_cgs es in
if not (Hashtbl.mem seen (lid, (cgs, ts))) then begin
Krml.KPrint.bprintf "Visiting (recursive): %a\n"
Krml.PrintAst.Ops.pexpr (with_type TUnit (ETApp (e, cgs, ts)));
pexpr (with_type TUnit (ETApp (e, cgs, ts)));
assert (n_cgs = List.length cgs && n = List.length ts);
Hashtbl.add seen (lid, (cgs, ts)) ();
let body = Krml.DeBruijn.(subst_cen (List.length binders - n_cgs) cgs (subst_ten ts body)) in
Expand Down Expand Up @@ -174,7 +175,6 @@ let debug missing =
Krml.KPrint.bprintf "DEBUG RUNTIME MONOMORPHIZATION:\n";
Hashtbl.iter (fun lid args ->
let open Krml in
let open PrintAst.Ops in
KPrint.bprintf "%a:\n" plid lid;
List.iter (fun (ts, cgs) ->
KPrint.bprintf " %a ++ %a\n" ptyps ts pcgs cgs
Expand Down Expand Up @@ -211,7 +211,7 @@ let replace =
| TCgArray (t1, cg1), TCgArray (t2, cg2) ->
matches_t t1 t2 && cg1 = cg2
| TArray (t1, _), TCgArray (t2, _) ->
(* TODO: compute mappings and check they coincide *)
(* TODO: compute mgus and check they coincide *)
matches_t t1 t2
| TCgApp (t1, cg1), TCgApp (t2, cg2) ->
matches_t t1 t2 && matches_cg cg1 cg2
Expand All @@ -222,7 +222,7 @@ let replace =
| t1, t2 ->
t1 = t2
in
Krml.(let open PrintAst.Ops in KPrint.bprintf " MATCH: %a | %a ? %b\n" ptyp t1 ptyp t2 r);
Krml.(KPrint.bprintf " MATCH: %a | %a ? %b\n" ptyp t1 ptyp t2 r);
r

and matches_cg cg1 cg2 =
Expand All @@ -235,7 +235,7 @@ let replace =
let replace t ts cgs =
let builtin = match List.hd (fst t) with "Eurydice" | "core" -> true | _ -> false in
if not builtin then begin
Krml.(let open PrintAst.Ops in KPrint.bprintf "REPLACE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
Krml.(KPrint.bprintf "REPLACE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
(* let candidates = Hashtbl.find missing t in *)
(* Pull ALL the candidates from monomorphization *)
let candidates = Hashtbl.fold (fun (lid, ts, cgs) (_, mono_lid) acc ->
Expand All @@ -248,12 +248,12 @@ let replace =
match candidates with
| [] -> fold_tapp (t, ts, cgs)
| [ ts', cgs', lid ] ->
Krml.(let open PrintAst.Ops in KPrint.bprintf " FOUND: %a: %a ++ %a\n" plid t ptyps ts' pcgs cgs');
Krml.(let open PrintAst.Ops in KPrint.bprintf " AKA: %a\n" plid lid);
Krml.(KPrint.bprintf " FOUND: %a: %a ++ %a\n" plid t ptyps ts' pcgs cgs');
Krml.(KPrint.bprintf " AKA: %a\n" plid lid);
TQualified lid
| _ ->
List.iter (fun (ts, cgs, _) ->
Krml.(let open PrintAst.Ops in KPrint.bprintf " CANDIDATE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
Krml.(KPrint.bprintf " CANDIDATE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
) candidates;
failwith "TODO: multiple candidates, need to be subtler"
end else
Expand All @@ -279,15 +279,28 @@ let replace =
arguments of TCgArray's to runtime expressions, in order to implement blit
operations to materialize array copies. We now remove those, and manually
decay TCgArrays into TBufs, relying on Checker to validate this pass. *)
let erase_and_decay_cgs = object(self)
let decay_cgs = object(self)
inherit Krml.DeBruijn.map_counting_cg as super

method! visit_ELet env b e1 e2 =
match b.typ, e1.node with
| TCgArray (t, _), EAny ->
let n = Cleanup2.expr_of_array_length (fst env) b.typ in
let typ = TBuf (t, false) in
ELet ({ b with typ }, with_type typ (EBufCreate (Stack, H.any, n)),
| TCgArray _, EAny ->
let rec convert t0 =
match t0 with
| TCgArray (t, _) ->
(* Krml.KPrint.bprintf "n_cgs=%d, n=%d, i_cg=%d\n" (fst (fst env)) (snd (fst env)) i_cg; *)
let n = Cleanup2.expr_of_array_length (fst env) t0 in
let t, init = convert t in
let typ = TBuf (t, false) in
typ, with_type typ (EBufCreate (Stack, init, n))
| TArray (_, _) ->
let n = Cleanup2.expr_of_array_length (fst env) t0 in
t0, with_type t0 (EBufCreate (Stack, H.any, n))
| _ ->
t0, H.any
in
let typ, init = convert b.typ in
ELet ({ b with typ }, init,
self#visit_expr_w (self#extend (fst env) { b with typ }) e2)
| _ ->
super#visit_ELet env b e1 e2
Expand All @@ -296,6 +309,21 @@ let erase_and_decay_cgs = object(self)
super#visit_TBuf env t false

method! visit_DFunction _ cc flags n_cgs n t name bs e =
(* Setting up environment properly *)
super#visit_DFunction (n_cgs, 0) cc flags n_cgs n t name bs e
end


(* This happens much later. The previous phases left n_cgs in place over
DFunctions so that remove_implicit_array_copies could convert length
arguments of TCgArray's to runtime expressions, in order to implement blit
operations to materialize array copies. We now remove those, and manually
decay TCgArrays into TBufs, relying on Checker to validate this pass. *)
let erase_cgs = object(_self)
inherit Krml.DeBruijn.map_counting_cg as super

method! visit_DFunction _ cc flags n_cgs n t name bs e =
(* Discarding n_cgs *)
super#visit_DFunction (n_cgs, 0) cc flags 0 n t name bs e

end
Expand Down

0 comments on commit 95f0615

Please sign in to comment.