Skip to content

Commit

Permalink
Merge pull request #93 from AeneasVerif/protz_poly_array
Browse files Browse the repository at this point in the history
Proper treatment of slice_index when the type of elements is an array
msprotz authored Nov 22, 2024
2 parents 4cc8626 + 6ae5ff3 commit 567f390
Showing 5 changed files with 20 additions and 43 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -8,7 +8,7 @@ TEST_DIRS = $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxd

.PHONY: all
all: format-check
@ocamlfind list | grep -q charon || test -L lib/charon || echo "⚠️⚠️⚠️ Charon not found; we suggest cd lib && ln -s path/to/charon-ml charon"
@ocamlfind list | grep -q charon || test -L lib/charon || echo "⚠️⚠️⚠️ Charon not found; we suggest cd lib && ln -s path/to/charon charon"
@ocamlfind list | grep -q krml || test -L lib/krml || echo "⚠️⚠️⚠️ krml not found; we suggest cd lib && ln -s path/to/karamel/lib krml"
$(MAKE) build

3 changes: 1 addition & 2 deletions bin/main.ml
Original file line number Diff line number Diff line change
@@ -229,12 +229,11 @@ Supported options:|}
let files = Eurydice.Cleanup2.remove_trivial_into#visit_files () files in
let files = Krml.Structs.pass_by_ref files in
Eurydice.Logging.log "Phase2.5" "%a" pfiles files;
let files = Eurydice.Cleanup2.detect_array_returning_builtins#visit_files () files in
Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
let files = Eurydice.Cleanup2.remove_literals#visit_files () files in
(* Eurydice does something more involved than krml and performs a conservative
approximation of functions that are known to be pure readonly (i.e.,
functions that do not write to memory). *)
Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
fill_readonly_table files;
let files = Krml.Simplify.optimize_lets files in
(* let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in *)
26 changes: 13 additions & 13 deletions flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

6 changes: 5 additions & 1 deletion lib/Builtin.ml
Original file line number Diff line number Diff line change
@@ -110,6 +110,10 @@ let step_by : K.lident = [ "core"; "iter"; "adapters"; "step_by" ], "StepBy"
let mk_step_by t = K.TApp (step_by, [ t ])
let mk_range_step_by_iterator t = mk_iterator (mk_step_by t)

(* This is incorrect: the function receives e.g.
- Range<usize> as its type argument,
- &StepBy<Range<usize>> for the type of its argument,
then returns Option<usize> for its return value. Which we can't really type. *)
let range_iterator_step_by =
{
name = [ "Eurydice" ], "range_iterator_step_by";
@@ -125,7 +129,7 @@ let range_step_by_iterator_next =
name = [ "Eurydice" ], "range_step_by_iterator_next";
typ =
Krml.Helpers.fold_arrow
[ TBuf (mk_range_step_by_iterator (TBound 0), false) ]
[ TBuf (mk_step_by (mk_range (TBound 0)), false) ]
(mk_option (TBound 0));
n_type_args = 1;
cg_args = [];
26 changes: 0 additions & 26 deletions lib/Cleanup2.ml
Original file line number Diff line number Diff line change
@@ -618,32 +618,6 @@ let resugar_loops =
end
[@ocamlformat "disable"]

let detect_array_returning_builtins =
object
inherit [_] map as super

method! visit_ELet ((), _ as env) b e1 e2 =
match e1.node, e2.node with
| EAny, ESequence [
{ node = EApp (
{ node = ETApp ({ node = EQualified (["Eurydice"], "slice_index"); _ }, [], [], [ t_elements ]) as hd; _ },
[ e_slice; e_index; { node = EBound 0; _ } ]); _ };
{ node = EBound 0; _ }
] ->
(* let ret = $any;
Eurydice_slice_index (e_slice, e_index, ret);
ret *)
let shift1 = Krml.DeBruijn.subst Krml.Helpers.eunit 0 in
let e_slice = shift1 e_slice in
let e_index = shift1 e_index in
let t_hd = Krml.DeBruijn.subst_t t_elements 0 Builtin.slice_index.typ in
EApp (with_type t_hd hd, [ e_slice; e_index ])

| _ ->
super#visit_ELet env b e1 e2
end
[@ocamlformat "disable"]

let improve_names files =
let renamed = Hashtbl.create 41 in
let allocated = Hashtbl.create 41 in

0 comments on commit 567f390

Please sign in to comment.