diff --git a/bin/main.ml b/bin/main.ml index 3f0f9b1..dcd182a 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -243,15 +243,16 @@ Supported options:|} let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in (* These two need to come before... *) let files = Krml.Inlining.cross_call_analysis files in - Eurydice.Logging.log "Phase2.7" "%a" pfiles files; let files = Krml.Simplify.remove_unused files in (* This chunk which reuses key elements of simplify2 *) let files = Krml.Simplify.sequence_to_let#visit_files () files in + Eurydice.Logging.log "Phase2.7" "%a" pfiles files; let files = Krml.Simplify.hoist#visit_files [] files in + Eurydice.Logging.log "Phase2.75" "%a" pfiles files; let files = Krml.Simplify.fixup_hoist#visit_files () files in + Eurydice.Logging.log "Phase2.8" "%a" pfiles files; let files = Krml.Simplify.misc_cosmetic#visit_files () files in let files = Krml.Simplify.let_to_sequence#visit_files () files in - Eurydice.Logging.log "Phase2.8" "%a" pfiles files; let files = Eurydice.Cleanup3.bonus_cleanups#visit_files [] files in (* Macros stemming from globals *) let files, macros = Eurydice.Cleanup2.build_macros files in @@ -330,9 +331,15 @@ Supported options:|} in Eurydice.Logging.log "Phase3.3" "%a" pfiles files; - let files = List.map (fun (f, ds) -> f, List.filter (fun d -> - not (Krml.Idents.LidSet.mem (Krml.Ast.lid_of_decl d) Eurydice.Builtin.skip)) - ds) files in + let files = + List.map + (fun (f, ds) -> + ( f, + List.filter + (fun d -> not (Krml.Idents.LidSet.mem (Krml.Ast.lid_of_decl d) Eurydice.Builtin.skip)) + ds )) + files + in let files = AstToCStar.mk_files files c_name_map Idents.LidSet.empty macros in let headers = CStarToC11.mk_headers c_name_map files in diff --git a/flake.lock b/flake.lock index c386049..3bfbe15 100644 --- a/flake.lock +++ b/flake.lock @@ -11,11 +11,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1725887770, + "lastModified": 1725889400, "narHash": "sha256-qmSOicZMXJwJ2tsfeF5h6WGZ0ZYJfDoNRk+sjpqWEYk=", - "owner": "aeneasverif", + "owner": "AeneasVerif", "repo": "charon", - "rev": "92a3a80cb9283f018498cd81ce9c5bb94c73b8bd", + "rev": "e43b806912ff9e473e2d6ee37f8ab75af792d497", "type": "github" }, "original": { @@ -136,11 +136,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1724957201, - "narHash": "sha256-q8XaJiiErxDXFWhsOVN//WFSXPFmR3W8LvRL4Sov68c=", + "lastModified": 1725898168, + "narHash": "sha256-FWiQDIBVOxHHFlzT8yaTkYXdkFRoC7bD+wIPteP1mNw=", "owner": "FStarLang", "repo": "fstar", - "rev": "d93417723d03781d0d3b4969eb7f0d6b9671ef6d", + "rev": "c7a1cf5220fdc8517213910f275e575cb1cf748c", "type": "github" }, "original": { @@ -155,11 +155,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1724957201, - "narHash": "sha256-q8XaJiiErxDXFWhsOVN//WFSXPFmR3W8LvRL4Sov68c=", + "lastModified": 1725898168, + "narHash": "sha256-FWiQDIBVOxHHFlzT8yaTkYXdkFRoC7bD+wIPteP1mNw=", "owner": "fstarlang", "repo": "fstar", - "rev": "d93417723d03781d0d3b4969eb7f0d6b9671ef6d", + "rev": "c7a1cf5220fdc8517213910f275e575cb1cf748c", "type": "github" }, "original": { @@ -183,11 +183,11 @@ ] }, "locked": { - "lastModified": 1724965512, - "narHash": "sha256-4QrNXTaIS3BxIB5XwkjC2SoOBfkqWZ66UkKPhasHIto=", + "lastModified": 1725774056, + "narHash": "sha256-W5EpRxTuUuAZc6A7hPrXdH6E6FPoW9CtoGrdFUDhXvk=", "owner": "FStarLang", "repo": "karamel", - "rev": "fa19d3771e6745dac67e834cd077438905ce7720", + "rev": "97ced7728b3a3964a9c42c4b2b5b409ec41e9ce4", "type": "github" }, "original": { @@ -246,11 +246,11 @@ ] }, "locked": { - "lastModified": 1725848835, - "narHash": "sha256-u4lCr+tOEWhsFiww5G04U5jUNzaQJi0/ZMIDGiLeT14=", + "lastModified": 1723429325, + "narHash": "sha256-4x/32xTCd+xCwFoI/kKSiCr5LQA2ZlyTRYXKEni5HR8=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "2ef910a6276a2f34513d18f2f826a8dea72c3b3f", + "rev": "65e3dc0fe079fe8df087cd38f1fe6836a0373aad", "type": "github" }, "original": { diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index c7702ee..9b302ee 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -18,13 +18,13 @@ extern "C" { #include "krml/lowstar_endianness.h" #define LowStar_Ignore_ignore(e, t, _ret_t) ((void)e) -#define EURYDICE_ASSERT(test, msg) do { \ - if (!(test)) { \ - fprintf(stderr, \ - "assertion \"%s\" failed: file \"%s\", line %d\n", \ - msg, __FILE__, __LINE__); \ - } \ -} while (0) +#define EURYDICE_ASSERT(test, msg) \ + do { \ + if (!(test)) { \ + fprintf(stderr, "assertion \"%s\" failed: file \"%s\", line %d\n", msg, \ + __FILE__, __LINE__); \ + } \ + } while (0) // SLICES, ARRAYS, ETC. diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 0248a33..d7c883b 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -449,12 +449,16 @@ let push_clause_binders env bs = List.fold_left push_clause_binder env bs let lookup_clause_binder env clause_id item_name = let i, (v, t) = - findi - (function - | TraitClauseMethod (clause_id2, item_name2, _), _ -> - clause_id2 = clause_id && item_name2 = item_name - | _ -> false) - env.binders + try + findi + (function + | TraitClauseMethod (clause_id2, item_name2, _), _ -> + clause_id2 = clause_id && item_name2 = item_name + | _ -> false) + env.binders + with Not_found -> + Krml.KPrint.bprintf "Error looking up %s.%s\n" (C.show_trait_instance_id clause_id) item_name; + raise Not_found in i, t, thd3 (assert_trait_clause_method v) @@ -726,7 +730,10 @@ let blocklisted_trait_decls = the types we obtain by looking up the trait declaration have Self as 0 (DeBruijn). *) -let rec build_trait_clause_mapping env (trait_clauses : C.trait_clause list) = +let rec build_trait_clause_mapping env (trait_clauses : C.trait_clause list) : + ((C.trait_instance_id * string) + * (C.generic_args * K.type_scheme * Charon.Types.name * C.fun_sig)) + list = List.concat_map (fun tc -> let { C.clause_id; trait = { trait_decl_id; decl_generics }; _ } = tc in @@ -765,13 +772,20 @@ let rec build_trait_clause_mapping env (trait_clauses : C.trait_clause list) = (trait_decl.C.required_methods @ trait_decl.C.provided_methods) @ List.flatten (List.mapi - (fun i (parent_clause : C.trait_clause) -> + (fun _i (parent_clause : C.trait_clause) -> (* Mapping of the methods of the parent clause *) let m = build_trait_clause_mapping env [ parent_clause ] in List.map - (fun ((clause_id, m), v) -> - (* This is the parent clause `i` of `clause_id` -- see comments in charon/types.rs *) - let id = C.(ParentClause (clause_id, trait_decl_id, TraitClauseId.of_int i)) in + (fun (((clause_id' : C.trait_instance_id), m), v) -> + (* This is the parent clause `clause_id'` of `clause_id` -- see comments in charon/types.rs *) + let clause_id' = + match clause_id' with + | Clause clause_id' -> clause_id' + | _ -> fail "not a clause??" + in + let id : C.trait_instance_id = + ParentClause (Clause clause_id, trait_decl_id, clause_id') + in (id, m), v) m) trait_decl.C.parent_clauses) diff --git a/lib/Builtin.ml b/lib/Builtin.ml index a097a14..c840c56 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -18,9 +18,10 @@ let option : K.lident = [ "core"; "option" ], "Option" let mk_option (t : K.typ) : K.typ = K.TApp (option, [ t ]) let array_copy = [ "Eurydice" ], "array_copy" let macros = Krml.Idents.LidSet.of_list [] + (* Things that could otherwise be emitted as an extern prototype, but for some reason ought to be skipped. *) -let skip = Krml.Idents.LidSet.of_list [ ["Eurydice"], "assert" ] +let skip = Krml.Idents.LidSet.of_list [ [ "Eurydice" ], "assert" ] let result = [ "core"; "result" ], "Result" let mk_result t1 t2 = K.TApp (result, [ t1; t2 ]) let nonzero = [ "core"; "num"; "nonzero" ], "NonZero" @@ -305,16 +306,16 @@ let min_u32 = (* Not fully general *) let static_assert, static_assert_ref = let name = [ "Eurydice" ], "assert" in - let typ =Krml.Helpers.fold_arrow [ TBool; - Krml.Checker.c_string ] TUnit in - K.DExternal (None, [ Krml.Common.Private; Macro ], 0, 0, - name, typ, - [ "test"; "msg" ]), K.(with_type typ (EQualified name)) + let typ = Krml.Helpers.fold_arrow [ TBool; Krml.Checker.c_string ] TUnit in + ( K.DExternal (None, [ Krml.Common.Private; Macro ], 0, 0, name, typ, [ "test"; "msg" ]), + K.(with_type typ (EQualified name)) ) let unwrap : K.decl = let open Krml in let open Ast in - let lid = [ "core"; "result"; "{core::result::Result}" ], "unwrap" in + let lid = + [ "core"; "result"; "{core::result::Result[TraitClause@0, TraitClause@1]}" ], "unwrap" + in let t_T = TBound 1 in let t_E = TBound 0 in let t_result = mk_result t_T t_E in diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 2bcda10..b42d6fd 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -702,9 +702,8 @@ let recognize_asserts = match e1.typ, e2.node, e3.node with | TBool, EUnit, EAbort (_, msg) -> (* if not (e1) then abort msg else () --> static_assert(e1, msg) *) - EApp (Builtin.static_assert_ref, [ e1; with_type - Krml.Checker.c_string (EString (Option.value ~default:"" msg)) ]) - | _ -> - super#visit_EIfThenElse env e1 e2 e3 - + EApp + ( Builtin.static_assert_ref, + [ e1; with_type Krml.Checker.c_string (EString (Option.value ~default:"" msg)) ] ) + | _ -> super#visit_EIfThenElse env e1 e2 e3 end diff --git a/lib/Cleanup3.ml b/lib/Cleanup3.ml index 0b5189f..b3fb7ec 100644 --- a/lib/Cleanup3.ml +++ b/lib/Cleanup3.ml @@ -9,7 +9,6 @@ *) module B = Builtin - open Krml open Ast