diff --git a/Makefile b/Makefile index c9473b7..b3acf48 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,10 @@ CHARON_HOME ?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../charon -KRML_HOME ?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel +KRML_HOME ?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel EURYDICE ?= ./eurydice $(EURYDICE_FLAGS) CHARON ?= $(CHARON_HOME)/bin/charon -CHARON_TEST_FILES = arrays -TEST_DIRS = array const_generics traits array2d int_switch nested_arrays # step_by +BROKEN_TESTS = step_by where_clauses chunks mutable_slice_range +TEST_DIRS = $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxdepth 1 -mindepth 1 -type d))) .PHONY: all all: @@ -14,21 +14,8 @@ all: CFLAGS := -Wall -Werror -Wno-unused-variable $(CFLAGS) -I$(KRML_HOME)/include -test: $(addprefix charon-test-,$(CHARON_TEST_FILES)) $(addprefix test-,$(TEST_DIRS)) +test: $(addprefix test-,$(TEST_DIRS)) -# Tests relying on Charon's test infrastructure - -$(CHARON_HOME)/tests/llbc/%.llbc: $(CHARON_HOME)/tests/src/%.rs - RUST_BACKTRACE=1 $(MAKE) -C $(CHARON_HOME)/tests test-$* - -.PRECIOUS: $(CHARON_HOME)/tests/llbc/%.llbc -charon-test-%: $(CHARON_HOME)/tests/llbc/%.llbc | out/test-% all - mkdir -p out/charon-test-$* - $(EURYDICE) --output out/charon-test-$* $< - # These tests do not have a main - cd out/charon-test-$* && $(CC) $(CFLAGS) -I. -I../../include $*.c -c - -# Tests checked into the current repository .PHONY: phony .PRECIOUS: test/%/out.llbc test/%/out.llbc: phony @@ -38,9 +25,12 @@ out/test-%/main.c: test/main.c mkdir -p out/test-$* sed 's/__NAME__/$*/g' $< > $@ +test-partial_eq: EXTRA_C = ../../test/partial_eq/stubs.c +test-nested_arrays: EXTRA = -funroll-loops 0 + test-%: test/%/out.llbc out/test-%/main.c | all - $(EURYDICE) --output out/test-$* $< - cd out/test-$* && $(CC) $(CFLAGS) -I. -I../../include $*.c main.c && ./a.out + $(EURYDICE) $(EXTRA) --output out/test-$* $< + cd out/test-$* && $(CC) $(CFLAGS) -I. -I../../include $(EXTRA_C) $*.c main.c && ./a.out .PRECIOUS: out/% out/%: diff --git a/bin/main.ml b/bin/main.ml index 9db10b2..b50520c 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -12,11 +12,13 @@ Supported options:|} in let module O = Eurydice.Options in let debug s = Krml.Options.debug_modules := Krml.KString.split_on_char ',' s @ !Krml.Options.debug_modules in + let funroll_loops = ref 16 in let spec = [ "--log", Arg.Set_string O.log_level, " log level, use * for everything"; "--debug", Arg.String debug, " debug options, to be passed to krml"; "--output", Arg.Set_string Krml.Options.tmpdir, " output directory in which to write files"; "--config", Arg.Set_string O.config, " YAML configuration file"; + "-funroll-loops", Arg.Set_int funroll_loops, " unrool loops up to N"; ] in let spec = Arg.align spec in let files = ref [] in @@ -38,10 +40,14 @@ Supported options:|} if !files = [] then fatal_error "%s" (Arg.usage_string spec usage); - let terminal_width = (* Terminal.Size.(match get_dimensions () with Some d -> d.columns | None -> 80) *) 100 in + let terminal_width = Terminal.Size.(match get_dimensions () with Some d -> d.columns | None -> 80) in let pfiles b files = PPrint.(ToBuffer.pretty 0.95 terminal_width b (Krml.PrintAst.print_files files ^^ hardline)) in + let fail file line = + Printf.printf "%s:%d exiting" file line; + exit 1 + in (* This is where the action happens *) Eurydice.Logging.enable_logging !O.log_level; @@ -56,6 +62,7 @@ Supported options:|} parentheses := true; no_shadow := true; extern_c := true; + unroll_loops := !funroll_loops; static_header := [ Bundle.Prefix [ "core"; "convert" ]; Bundle.Prefix [ "core"; "num" ]; @@ -76,10 +83,10 @@ Supported options:|} false ); - let files = Eurydice.Builtin.files @ List.map (fun filename -> + let files = Eurydice.Builtin.files @ [ Eurydice.PreCleanup.merge (List.map (fun filename -> let llbc = Eurydice.LoadLlbc.load_file filename in Eurydice.Builtin.adjust (Eurydice.AstOfLlbc.file_of_crate llbc) - ) !files in + ) !files) ] in Eurydice.Builtin.check (); Printf.printf "1️⃣ LLBC ➡️ AST\n"; @@ -88,74 +95,98 @@ Supported options:|} Eurydice.Logging.log "Phase1" "%a" pfiles files; let errors, files = Krml.Checker.check_everything ~warn:true files in if errors then - exit 1; + fail __FILE__ __LINE__; Printf.printf "2️⃣ Cleanup\n"; - let files = + let config = if !O.config = "" then - files + None else - let config = Eurydice.Bundles.load_config !O.config in - let config = Eurydice.Bundles.parse_config config in - let files = Eurydice.Bundles.bundle files config in - let files = Krml.Bundles.topological_sort files in - Krml.KPrint.bprintf "File order after topological sort: %s\n" - (String.concat ", " (List.map fst files)); - files + Some (Eurydice.Bundles.parse_config (Eurydice.Bundles.load_config !O.config)) + in + let files = + match config with + | None -> files + | Some config -> + let config = config in + let files = Eurydice.Bundles.bundle files config in + let files = Eurydice.Bundles.libraries files in + let files = Krml.Bundles.topological_sort files in + Krml.KPrint.bprintf "File order after topological sort: %s\n" + (String.concat ", " (List.map fst files)); + files in let files = Eurydice.Cleanup1.cleanup files in Eurydice.Logging.log "Phase2" "%a" pfiles files; let errors, files = Krml.Checker.check_everything ~warn:true files in if errors then - exit 1; + fail __FILE__ __LINE__; Printf.printf "3️⃣ Monomorphization, datatypes\n"; let files = Eurydice.Cleanup2.resugar_loops#visit_files () files in (* Sanity check for the big rewriting above. *) let errors, files = Krml.Checker.check_everything ~warn:true files in if errors then - exit 1; + fail __FILE__ __LINE__; Eurydice.Logging.log "Phase2.1" "%a" pfiles files; let files = Krml.Monomorphization.functions files in let files = Krml.Monomorphization.datatypes files in + let files = + match config with + | None -> files + | Some config -> + let files = Eurydice.Bundles.reassign_monomorphizations files config in + Eurydice.Logging.log "Phase2.15" "%a" pfiles files; + let files = Krml.Bundles.topological_sort files in + files + in Eurydice.Logging.log "Phase2.2" "%a" pfiles files; + (* Sanity check for the big rewriting above. *) + let errors, files = Krml.Checker.check_everything ~warn:true files in + if errors then + fail __FILE__ __LINE__; let files = Krml.Inlining.drop_unused files in - Eurydice.Logging.log "Phase2.3" "%a" pfiles files; let files = Eurydice.Cleanup2.remove_array_temporaries#visit_files () files in let files = Eurydice.Cleanup2.remove_array_repeats#visit_files () files in let files = Eurydice.Cleanup2.rewrite_slice_to_array#visit_files () files in let files = Krml.DataTypes.simplify files in let files = Krml.DataTypes.optimize files in let _, files = Krml.DataTypes.everything files in + Eurydice.Logging.log "Phase2.3" "%a" pfiles files; let files = Eurydice.Cleanup2.remove_trivial_ite#visit_files () files in + Eurydice.Logging.log "Phase2.4" "%a" pfiles files; 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 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.6" "%a" pfiles files; + let files = Eurydice.Cleanup2.remove_array_from_fn files in let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in let files = Krml.Simplify.sequence_to_let#visit_files () files in let files = Krml.Simplify.hoist#visit_files [] files in let files = Krml.Simplify.fixup_hoist#visit_files () files in let files = Krml.Simplify.misc_cosmetic#visit_files () files in - Eurydice.Logging.log "Phase2.4" "%a" pfiles files; let files = Krml.Simplify.let_to_sequence#visit_files () files in - Eurydice.Logging.log "Phase2.5" "%a" pfiles files; let files = Krml.Inlining.cross_call_analysis files in - Eurydice.Logging.log "Phase2.6" "%a" pfiles files; let files = Krml.Simplify.remove_unused files in - let files = Eurydice.Cleanup2.remove_array_from_fn#visit_files () files in + Eurydice.Logging.log "Phase2.7" "%a" pfiles files; + Eurydice.Logging.log "Phase2.8" "%a" pfiles files; (* Macros stemming from globals *) let files, macros = Eurydice.Cleanup2.build_macros 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; + fail __FILE__ __LINE__; 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 files = Eurydice.Cleanup3.add_extra_type_to_slice_index#visit_files () files in + Eurydice.Logging.log "Phase3.1" "%a" pfiles files; let macros = let cg_macros = Eurydice.Cleanup3.build_cg_macros#visit_files () files in Krml.Idents.LidSet.(union (union macros cg_macros) Eurydice.Builtin.macros) @@ -186,6 +217,7 @@ Supported options:|} Some d ) ds ) files in + Eurydice.Logging.log "Phase3.2" "%a" pfiles files; 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/dune-project b/dune-project index a571420..c7104e0 100644 --- a/dune-project +++ b/dune-project @@ -18,6 +18,12 @@ (synopsis "A Rust to C translator") (description "Eurydice builds upon Charon to take existing Rust code and translate it to C") - (depends ocaml dune terminal yaml)) + (depends + ocaml + dune + yaml + (terminal (>= 0.4.0)) + ) +) (using menhir 2.1) diff --git a/eurydice.opam b/eurydice.opam index aaf5e18..a040837 100644 --- a/eurydice.opam +++ b/eurydice.opam @@ -12,8 +12,8 @@ bug-reports: "https://github.com/AeneasVerif/eurydice/issues" depends: [ "ocaml" "dune" {>= "3.7"} - "terminal" "yaml" + "terminal" {>= "0.4.0"} "odoc" {with-doc} ] build: [ diff --git a/flake.lock b/flake.lock index 3471407..d4502e4 100644 --- a/flake.lock +++ b/flake.lock @@ -11,11 +11,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1713981450, - "narHash": "sha256-QsYlA+DPOofaqQz2U4LGzHLLEpxT6TlxkkcdR66X6pI=", + "lastModified": 1717443886, + "narHash": "sha256-6tX6AgXQlIIuiKLOij0H2mf00rhU02hbQhs3lTARgMk=", "owner": "AeneasVerif", "repo": "charon", - "rev": "e3974871787a2f4082884964bf3e67d905381ce2", + "rev": "ae610b59b337b191d23f4f1c738ed290b8edd0d2", "type": "github" }, "original": { @@ -136,11 +136,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1714001266, - "narHash": "sha256-4AFdmCMByknNyN3z7qyawavMRqwz0Zz97UvsY+OtCq8=", + "lastModified": 1716897445, + "narHash": "sha256-Ytz9l3PjhBHULVZphHoUj15Ad8Wq3cIK6Paus32NB1w=", "owner": "FStarLang", "repo": "fstar", - "rev": "22e11f7b0084805d10373bef8239865c61baffa7", + "rev": "9820798dcc31cd1ea5c164611a67f58ade0b7655", "type": "github" }, "original": { @@ -155,11 +155,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1714001266, - "narHash": "sha256-4AFdmCMByknNyN3z7qyawavMRqwz0Zz97UvsY+OtCq8=", + "lastModified": 1716897445, + "narHash": "sha256-Ytz9l3PjhBHULVZphHoUj15Ad8Wq3cIK6Paus32NB1w=", "owner": "fstarlang", "repo": "fstar", - "rev": "22e11f7b0084805d10373bef8239865c61baffa7", + "rev": "9820798dcc31cd1ea5c164611a67f58ade0b7655", "type": "github" }, "original": { @@ -183,11 +183,11 @@ ] }, "locked": { - "lastModified": 1714008528, - "narHash": "sha256-pqoqG6JLTYI553gzYUdUPspgsqcRDRsHgOmfIm1ke1s=", + "lastModified": 1717454922, + "narHash": "sha256-3yseAxgtqchKisDIWvU2hxC5rqNbQd7HDAPo28Gnzpk=", "owner": "FStarLang", "repo": "karamel", - "rev": "1282f04f16a4e193f329708b22e0a4577d5dd092", + "rev": "749859845fed65d9391f4ba318c8cf27292a85ce", "type": "github" }, "original": { diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index c8b0825..4189011 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -34,7 +34,12 @@ typedef struct { // remark above about how pointer arithmetic works in C), meaning either pointer or array type. #define EURYDICE_SLICE(x, start, end) ((Eurydice_slice){ .ptr = (void*)(x + start), .len = end - start }) #define EURYDICE_SLICE_LEN(s, _) s.len -#define Eurydice_slice_index(s, i, t, _ret_t) (((t*) s.ptr)[i]) +// This macro is a pain because in case the dereferenced element type is an +// array, you cannot simply write `t x` as it would yield `int[4] x` instead, +// which is NOT correct C syntax, so we add a dedicated phase in Eurydice that +// adds an extra argument to this macro at the last minute so that we have the +// correct type of *pointers* to elements. +#define Eurydice_slice_index(s, i, t, t_ptr_t, _ret_t) (((t_ptr_t) s.ptr)[i]) #define Eurydice_slice_subslice(s, r, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, r.start, r.end) #define Eurydice_slice_subslice_to(s, subslice_end_pos, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, 0, subslice_end_pos) #define Eurydice_slice_subslice_from(s, subslice_start_pos, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, subslice_start_pos, s.len) @@ -47,6 +52,8 @@ typedef struct { #define core_slice___Slice_T___copy_from_slice(dst, src, t, _ret_t) memcpy(dst.ptr, src.ptr, dst.len * sizeof(t)) #define core_array___Array_T__N__23__as_slice(len_, ptr_, t, _ret_t) ((Eurydice_slice){ .ptr = ptr_, .len = len_ }) +#define core_array___core__clone__Clone_for__Array_T__N___20__clone(len, src, dst, elem_type, _ret_t) \ + (memcpy(dst, src, len * sizeof(elem_type))) #define core_array_TryFromSliceError uint8_t #define Eurydice_array_eq(sz, a1, a2, t, _, _ret_t) (memcmp(a1, a2, sz * sizeof(t)) == 0) @@ -56,6 +63,11 @@ typedef struct { ((ret_t){ \ .fst = EURYDICE_SLICE((element_type*)slice.ptr, 0, mid), \ .snd = EURYDICE_SLICE((element_type*)slice.ptr, mid, slice.len)}) +#define core_slice___Slice_T___split_at_mut(slice, mid, element_type, ret_t) \ + ((ret_t){ \ + .fst = { .ptr = slice.ptr, .len = mid }, \ + .snd = { .ptr = (char*)slice.ptr + mid * sizeof(element_type), .len = slice.len - mid }}) + // Can't have a flexible array as a member of a union -- this violates strict aliasing rules. typedef struct @@ -80,12 +92,20 @@ static inline void core_num__u32_8__to_be_bytes(uint32_t src, uint8_t dst[4]) { memcpy(dst, &x, 4); } +static inline void core_num__u64_9__to_le_bytes(uint64_t v,uint8_t buf[8]) { + store64_le(buf,v); +} +static inline uint64_t core_num__u64_9__from_le_bytes(uint8_t buf[8]) { + return load64_le(buf); +} + static inline int64_t -core_convert_num___core__convert__From_i32__for_i64__59__from(int32_t x) -{ +core_convert_num___core__convert__From_i32__for_i64__59__from(int32_t x) { return x; } +static inline uint32_t core_num__u8_6__count_ones(uint8_t x0) { return __builtin_popcount(x0); } + // unsigned overflow wraparound semantics in C static inline uint16_t core_num__u16_7__wrapping_add(uint16_t x, uint16_t y) { return x + y; } static inline uint8_t core_num__u8_6__wrapping_sub(uint8_t x, uint8_t y) { return x - y; } @@ -160,12 +180,18 @@ typedef struct { .tag = core_option_Some, \ .f0 = ((iter)->index++, &((t*)((iter)->s.ptr))[(iter)->index-1]) })) -// MISC +// STRINGS + +typedef const char *Prims_string; -#define core_fmt_Formatter void +// MISC (UNTESTED) +typedef void *core_fmt_Formatter; +typedef void *core_fmt_Arguments; +typedef void *core_fmt_rt_Argument; +#define core_fmt_rt__core__fmt__rt__Argument__a__1__new_display(x1, x2, x3, x4) NULL -// VECTORS +// VECTORS (ANCIENT, POSSIBLY UNTESTED) /* For now these are passed by value -- three words. We could conceivably change * the representation to heap-allocate this struct and only pass around the diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 9c1e373..32600c6 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -24,23 +24,62 @@ module K = Krml.Ast module L = Logging +open Krml.PrintAst.Ops + (** Environment *) +(* The various kinds of binders we insert in the expression scope. Usually come + in this order, the first two being only ever inserted upon entering a function + definition. *) +type var_id = + | TraitClauseMethod of C.trait_clause_id * string * K.type_scheme + | ConstGenericVar of C.const_generic_var_id + | Var of C.var_id * C.ety (* the ety aids code-generation, sometimes *) + type env = { (* Lookup functions to resolve various id's into actual declarations. *) get_nth_function: C.FunDeclId.id -> C.fun_decl; get_nth_type: C.TypeDeclId.id -> C.type_decl; get_nth_global: C.GlobalDeclId.id -> C.global_decl; get_nth_trait_impl: C.TraitImplId.id -> C.trait_impl; + get_nth_trait_decl: C.TraitDeclId.id -> C.trait_decl; (* Needed by the name matching logic *) name_ctx: Charon.NameMatcher.ctx; generic_params: C.generic_params; - (* To compute DeBruijn indices *) + (* When in a function such as fn f>, we need to remember that Foo is instantiated over + 42 so as to pass the correct arguments. *) + clause_arguments: (C.TraitClauseId.id * C.const_generic list) list; + + (* We have three binding scopes, all in DeBruijn indices. + - const-generic ("cg") binders + - type binders + - expression binders, which typically starts with a repeat of the cg + binders (at the top-level function), followed by trait bounds method + binders, followed by regular expression binders (function arguments, local + variables, etc.) + In the target AST, we retain these three binding scopes. However, + - in types, CgVar and TCgArray contain DeBruijn indices referring to the cg + scope, while + - in expressions, there is no ECgVar, and we rely on a regular EBound node + that refers to the repeat of the cg var as a regular argument var. + + Example: fn f(x: [T; N]) -> usize { N } + Upon entering the body of f, we have: + - cg_binders: [ N, usize ] + - type_binders: [ T ] + - binders: [ `Cg (N, usize); `Clause (T: Copy, "copy"); `Var (x: [T; N]) ] + + After translation, we get: + DFunction (..., 1 (* one type var *), 2 (* one cg var *), [ + "N": TInt usize; + "x": TCgArray (TBound 0, 0); (* types use the cg scope *) + ], EBound 2 (* expressions refer to the copy of the cg var as an expression var *) + *) cg_binders: (C.const_generic_var_id * K.typ) list; type_binders: C.type_var_id list; - binders: (C.var_id * K.typ * C.ety) list; + binders: (var_id * K.typ) list; (* For printing. *) format_env: Charon.PrintLlbcAst.fmt_env; @@ -64,9 +103,12 @@ let findi p l = in findi 0 l -(* Suitable in types -- in expressions, add List.length env.binders to get a correct de bruijn index - suitable in expressions. *) -let lookup_cg env v1 = +let fst3 (x, _, _) = x +let snd3 (_, x, _) = x +let thd3 (_, _, x) = x + +(* Suitable in types -- in expressions, use lookup_cg_in_expressions. *) +let lookup_cg_in_types env v1 = let i, (_, t) = findi (fun (v2, _) -> v1 = v2) env.cg_binders in i, t @@ -90,7 +132,7 @@ let assert_slice (t: K.typ) = | TApp (lid, [ t ]) when lid = Builtin.slice -> t | _ -> - Krml.Warn.fatal_error "Not a slice: %a" Krml.PrintAst.Ops.ptyp t + Krml.Warn.fatal_error "Not a slice: %a" ptyp t let string_of_path_elem (env: env) (p: Charon.Types.path_elem): string = match p with @@ -172,6 +214,25 @@ module RustNames = struct let from = parse_pattern "core::convert::From<@T, @U>::from" + let into_u16 = + parse_pattern "core::convert::Into<@U, u16>::into" + let into_u32 = + parse_pattern "core::convert::Into<@U, u32>::into" + let into_u64 = + parse_pattern "core::convert::Into<@U, u64>::into" + let into_u128 = + parse_pattern "core::convert::Into<@U, u128>::into" + let into_i16 = + parse_pattern "core::convert::Into<@U, i16>::into" + let into_i32 = + parse_pattern "core::convert::Into<@U, i32>::into" + let into_i64 = + parse_pattern "core::convert::Into<@U, i64>::into" + let into_i128 = + parse_pattern "core::convert::Into<@U, i128>::into" + let into = + parse_pattern "core::convert::Into<@U, @T>::into" + let is_vec env = match_pattern_with_type_id env.name_ctx config (mk_empty_maps ()) vec @@ -242,7 +303,7 @@ let assert_cg_scalar = function let cg_of_const_generic env cg = match cg with - | C.CgVar id -> K.CgVar (fst (lookup_cg env id)) + | C.CgVar id -> K.CgVar (fst (lookup_cg_in_types env id)) | C.CgValue (VScalar sv) -> CgConst (constant_of_scalar_value sv) | _ -> failwith ("cg_of_const_generic: " ^ Charon.PrintTypes.const_generic_to_string env.format_env cg) @@ -279,6 +340,12 @@ let rec typ_of_ty (env: env) (ty: Charon.Types.ty): K.typ = types and pointer types. *) K.TBuf (typ_of_ty env t, false) + | TRef (_, TAdt (TAssumed TStr, { types = []; _ }), _) -> + (* We perform on-the-fly elimination of addresses of strings (just like we + do for arrays) so as to type-check them correctly vis à vis krml's + Checker expectations. This means &'str translates to c_string *) + Krml.Checker.c_string + | TRef (_, t, _) -> (* Normal reference *) K.TBuf (typ_of_ty env t, false) @@ -296,14 +363,14 @@ let rec typ_of_ty (env: env) (ty: Charon.Types.ty): K.typ = assert (const_generics = []); begin match args with | [] -> TUnit - | [ t ] -> typ_of_ty env t (* happens with closures *) + | [ t ] -> typ_of_ty env t (* charon issue #205 *) | _ -> TTuple (List.map (typ_of_ty env) args) end | TAdt (TAssumed TArray, { types = [ t ]; const_generics = [ cg ]; _ }) -> maybe_cg_array env t cg - | TAdt (TAssumed TSlice, _) -> + | TAdt (TAssumed TSlice, { types = [ _t ]; _ }) -> (* Slice values cannot be materialized since their storage space cannot be computed at compile-time; we should never encounter this case. *) assert false @@ -311,13 +378,17 @@ let rec typ_of_ty (env: env) (ty: Charon.Types.ty): K.typ = | TAdt (TAssumed TBox, { types = [ t ]; _ }) -> K.TBuf (typ_of_ty env t, false) + | TAdt (TAssumed TStr, { types = []; _ }) -> + failwith "Impossible -- strings always behind a pointer" + | TAdt (TAssumed f, { types = args; const_generics; _ }) -> List.iter (fun x -> print_endline (C.show_const_generic x)) const_generics; Krml.Warn.fatal_error "TODO: Adt/Assumed %s (%d) %d " (C.show_assumed_ty f) (List.length args) (List.length const_generics) - | TRawPtr _ -> - failwith "TODO: TRawPtr" + | TRawPtr (t, _) -> + (* Appears in some trait methods, so let's try to handle that. *) + K.TBuf (typ_of_ty env t, false) | TTraitType _ -> failwith ("TODO: TraitTypes " ^ Charon.PrintTypes.ty_to_string env.format_env ty) @@ -330,7 +401,7 @@ and maybe_cg_array env t cg = | CgValue _ -> K.TArray (typ_of_ty env t, constant_of_scalar_value (assert_cg_scalar cg)) | CgVar id -> - let id, cg_t = lookup_cg env id in + let id, cg_t = lookup_cg_in_types env id in assert (cg_t = K.TInt SizeT); K.TCgArray (typ_of_ty env t, id) | _ -> @@ -348,26 +419,73 @@ let mk_deep_copy (e: K.expr) (l: K.expr) = (* Environment: expressions *) +let is_var v2 v1 = + match v2 with + | Var (v2, _) -> v2 = v1 + | _ -> false + +let assert_var = function + | Var (v2, ty) -> v2, ty + | _ -> assert false + +let assert_trait_clause_method = function + | TraitClauseMethod (clause_id, item_name, signature) -> clause_id, item_name, signature + | _ -> assert false + +(* Regular binders *) + let lookup env v1 = - let i, (_, t, _) = findi (fun (v2, _, _) -> v1 = v2) env.binders in + let i, (_, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in i, t let lookup_with_original_type env v1 = - let i, (_, t, ty) = findi (fun (v2, _, _) -> v1 = v2) env.binders in + let i, (v, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in + let _, ty = assert_var v in i, t, ty +(* Const generic binders *) + let push_cg_binder env (t: C.const_generic_var) = - { env with cg_binders = (t.index, typ_of_literal_ty env t.ty) :: env.cg_binders } + { env with + cg_binders = (t.index, typ_of_literal_ty env t.ty) :: env.cg_binders; + binders = (ConstGenericVar t.index, typ_of_literal_ty env t.ty) :: env.binders; + } let push_cg_binders env (ts: C.const_generic_var list) = List.fold_left push_cg_binder env ts let push_binder env (t: C.var) = - { env with binders = (t.index, typ_of_ty env t.var_ty, t.var_ty) :: env.binders } + { env with binders = (Var (t.index, t.var_ty), typ_of_ty env t.var_ty) :: env.binders } let push_binders env (ts: C.var list) = List.fold_left push_binder env ts +(* Clause binders, which only appear as function parameters, and hold an unknown + trait method (dictionary-style). *) + +type clause_binder = { + clause_id: C.trait_clause_id; + item_name: string; + pretty_name: string; + ts: K.type_scheme; + t: K.typ; +} + +let push_clause_binder env { clause_id; item_name; t; ts; _ } = + { env with + binders = (TraitClauseMethod (clause_id, item_name, ts), t) :: env.binders } + +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 + in + i, t, thd3 (assert_trait_clause_method v) (** Translation of expressions (statements, operands, rvalues, places) *) @@ -397,9 +515,13 @@ let rec with_locals (env: env) (t: K.typ) (locals: C.var list) (k: env -> 'a): ' let b = binder_of_var env l in K.(with_type t (ELet (b, Krml.Helpers.any, with_locals env t locals k))) -let expression_of_cg_var_id (env: env) (v: C.const_generic_var_id): K.expr = - let i, t = lookup_cg env v in - K.(with_type t (EBound (i + List.length env.binders))) +let lookup_cg_in_expressions (env: env) (v1: C.const_generic_var_id) = + let i, (_, t) = findi (fun (v2, _) -> v2 = ConstGenericVar v1) env.binders in + i, t + +let expression_of_cg_var_id env v = + let i, t = lookup_cg_in_expressions env v in + K.(with_type t (EBound i)) let expression_of_var_id (env: env) (v: C.var_id): K.expr = let i, t = lookup env v in @@ -419,6 +541,8 @@ let expression_of_literal (_env: env) (l: C.literal): K.expr = expression_of_scalar_value sv | VBool b -> K.(with_type TBool (EBool b)) + | VStr s -> + K.(with_type Krml.Checker.c_string (EString s)) | _ -> failwith "TODO: expression_of_literal" @@ -434,7 +558,9 @@ let expression_of_place (env: env) (p: C.place): K.expr * C.ety = (* We construct a target expression, but retain the original type so that callers can tell arrays and references apart, since their *uses* (e.g. addr-of) compile in a type-directed way based on the *original* rust type *) + L.log "AstOfLlbc" "expression of place: %s" (C.show_place p); List.fold_left (fun (e, (ty: C.ety)) pe -> + L.log "AstOfLlbc" "e=%a\nty=%s\npe=%s\n" pexpr e (C.show_ty ty) (C.show_projection_elem pe); match pe, ty with | C.Deref, TRef (_, (TAdt (TAssumed TArray, { types = [ t ]; _ }) as ty), _) -> (* Array is passed by reference; when appearing in a place, it'll automatically decay in C *) @@ -490,21 +616,28 @@ let expression_of_place (env: env) (p: C.place): K.expr * C.ety = assert (cgs = []); (* match e with (_, ..., _, x, _, ..., _) -> x *) let i = Charon.Types.FieldId.to_int i in - let ts, t_i = - match e.typ with - | TTuple ts -> - assert (List.length ts = n); - ts, List.nth ts i - | _ -> - failwith "impossible: mismatch ProjTuple/TTuple" - in - let binders = [ Krml.Helpers.fresh_binder (uu ()) t_i ] in - let pattern = - K.with_type e.typ (K.PTuple (List.mapi (fun i' t -> - K.with_type t (if i = i' then K.PBound 0 else PWild)) ts)) - in - let expr = K.with_type t_i (K.EBound 0) in - K.with_type t_i (K.EMatch (Unchecked, e, [ binders, pattern, expr ])), List.nth tys i + if List.length tys = 1 then begin + assert (i = 0); + (* Normalized one-element tuple *) + e, List.hd tys + end else + let ts, t_i = + match e.typ with + | TTuple ts -> + assert (List.length ts = n); + ts, List.nth ts i + | _ -> + assert (List.length tys = 1); + L.log "AstOfLlbc" "typ is: %a" ptyp e.typ; + failwith "impossible: mismatch ProjTuple/TTuple" + in + let binders = [ Krml.Helpers.fresh_binder (uu ()) t_i ] in + let pattern = + K.with_type e.typ (K.PTuple (List.mapi (fun i' t -> + K.with_type t (if i = i' then K.PBound 0 else PWild)) ts)) + in + let expr = K.with_type t_i (K.EBound 0) in + K.with_type t_i (K.EMatch (Unchecked, e, [ binders, pattern, expr ])), List.nth tys i | _ -> failwith "unexpected / ill-typed projection" @@ -540,7 +673,7 @@ let mk_op_app (op: K.op) (first: K.expr) (rest: K.expr list): K.expr = let w = match first.typ with | K.TInt w -> w | K.TBool -> Bool - | t -> Krml.Warn.fatal_error "Not an operator type: %a" Krml.PrintAst.Ops.ptyp t + | t -> Krml.Warn.fatal_error "Not an operator type: %a" ptyp t in let op = if op = Not && first.typ <> K.TBool then Krml.Constant.BNot else op in let op_t = Krml.Helpers.type_of_op op w in @@ -566,47 +699,227 @@ let maybe_addrof (env: env) (ty: C.ty) (e: K.expr) = | _ -> K.(with_type (TBuf (e.typ, false)) (EAddrOf e)) + +(** Handling trait clauses as dictionaries *) + +(* There are two ways that we skip synthesis of trait methods in function calls. The first one is if + a trait declaration is blocklisted. This happens if the trait has built-in support (e.g. + FnMut), or if the trait relies on unsupported features. The second way we skip trait methods + (further down) is if the function is a known builtin implementation. *) +let blocklisted_trait_decls = [ + (* Handled primitively. *) + "core::ops::function::FnMut"; + "core::cmp::PartialEq"; + (* The traits below *should* be handled properly ASAP. But for now, we have specific *instances* + of those trait methods in the builtin lookup table, which we then implement by hand with + macros. *) + "core::iter::traits::iterator::Iterator"; + "core::iter::range::Step"; + (* TODO: for now, we leave into as-is in the AST, do a later pass that eliminates all identity + calls to into (post-monomorphization), and error our if there are any left that do not operate + on primitive types. We should probably remove the special-case in this file and treat it + generically with a dedicated pass over the krml ast. *) + "core::convert::From"; + (* TODO: figure out what to do with those *) + "core::clone::Clone"; + "core::marker::Copy"; + "core::fmt::Debug"; +] + +(* Using tests/where_clauses_simple as an example. + + fn double (...) + + this gets desugared to fn double where + T: Ops, <-- ClauseId 0 (required_methods: add, of_u32) + T: Copy, <-- ClauseId 1 (builtin, so neither required nor provided methods) + U: Ops, <-- ClauseId 2 (required_methods: add, of_u32) + U: Copy, <-- ClauseId 3 (builtin, so neither required nor provided methods) + + the types we obtain by looking up the trait declaration have Self as 0 + (DeBruijn). + *) +let build_trait_clause_mapping env (trait_clauses: C.trait_clause list) = + List.concat_map (fun tc -> + let { C.clause_id; trait_id; clause_generics; _ } = tc in + let trait_decl = env.get_nth_trait_decl trait_id in + + let name = string_of_name env trait_decl.name in + if List.mem name blocklisted_trait_decls then + [] + + else begin + (* FYI, some clauses like Copy have neither required nor provided methods. *) + L.log "TraitClauses" "clause decl %s\n \ + id %d:\n \ + clause_generic type is %s\n \ + clause_generic const_generics is %s\n \ + required: %d\n \ + provided: %d\n" + name + (C.TraitClauseId.to_int clause_id) + (String.concat " ++ " (List.map C.show_ty (clause_generics.C.types))) + (String.concat " ++ " (List.map C.show_const_generic (clause_generics.C.const_generics))) + (List.length trait_decl.C.required_methods) + (List.length trait_decl.C.provided_methods); + + List.map (fun (item_name, decl_id) -> + let decl = env.get_nth_function decl_id in + let ts = { K.n = List.length trait_decl.generics.types; n_cgs = List.length trait_decl.generics.const_generics } in + (clause_id, item_name), (clause_generics, ts, trait_decl.C.name, decl.C.signature) + ) trait_decl.C.required_methods @ + List.map (fun (item_name, decl_id) -> + match decl_id with + | Some decl_id -> + let decl = env.get_nth_function decl_id in + let ts = { K.n = List.length trait_decl.generics.types; n_cgs = List.length trait_decl.generics.const_generics } in + (clause_id, item_name), (clause_generics, ts, trait_decl.C.name, decl.C.signature) + | None -> + failwith ("TODO: handle provided trait methods, like " ^ item_name) + ) trait_decl.C.provided_methods + end + ) trait_clauses + +(* Interpret a Rust function type, with trait bounds, into the krml Ast, providing: + - the type scheme (fields may be zero) + - the cg types, which only contains the original Rust const generic variables (not trait methods) + - the argument types, prefixed by the dictionary-style passing of trait clause methods + - the return type + - whether the function is assumed, or not. *) type lookup_result = { - name: K.lident; - n_type_args: int; (* just for a sanity check *) + ts: K.type_scheme; (* just for a sanity check *) cg_types: K.typ list; arg_types: K.typ list; ret_type: K.typ; - is_assumed: bool; + is_known_builtin: bool; } -let lookup_fun (env: env) (f: C.fn_ptr): lookup_result = +let maybe_ts ts t = + if ts.K.n <> 0 || ts.n_cgs <> 0 then + K.TPoly (ts, t) + else + t + +let rec lookup_signature env depth signature = + let { C.generics = { types = type_params; const_generics; trait_clauses; _ }; inputs; output; _ } = signature in + L.log "Calls" "%s--> args: %s, ret: %s" depth + (String.concat " ++ " (List.map (Charon.PrintTypes.ty_to_string env.format_env) inputs)) + (Charon.PrintTypes.ty_to_string env.format_env output); + let env = push_cg_binders env const_generics in + let env = push_type_binders env type_params in + + let clause_mapping = build_trait_clause_mapping env trait_clauses in + debug_trait_clause_mapping env clause_mapping; + let clause_binders = mk_clause_binders_and_args env clause_mapping in + let clause_ts = List.map (fun { t; _ } -> t) clause_binders in + + { + ts = { n = List.length type_params; n_cgs = List.length const_generics }; + cg_types = List.map (fun (v: C.const_generic_var) -> typ_of_literal_ty env v.ty) const_generics; + arg_types = clause_ts @ List.map (typ_of_ty env) inputs @ (if inputs = [] then [ K.TUnit ] else []); + ret_type = typ_of_ty env output; + is_known_builtin = false + } + +(* Assumes type variables have been suitably bound in the environment *) +and mk_clause_binders_and_args env clause_mapping: clause_binder list = + List.map (fun ((clause_id, item_name), ((clause_generics: C.generic_args), trait_ts, trait_name, (signature: C.fun_sig))) -> + (* Polymorphic signature for trait method has const generic for BOTH + trait-level generics and fn-level generics. Consider: + + trait Hash + fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN]; K]; + + which gives the signature: + + size_t -> size_t -> uint8_t[33size_t]* -> uint8_t[$0][$1] + *) + let _, t = typ_of_signature env signature in + (* We are in a function that has a trait clause of the form e.g. Hash. + cgs contains FOO, that's it. *) + let cgs = List.map (cg_of_const_generic env) clause_generics.C.const_generics in + let ts = List.map (typ_of_ty env) clause_generics.C.types in + (* A little bit of math to compute how many of these are on the method + itself *) + let f_ts = { + K.n_cgs = List.length signature.C.generics.const_generics - List.length cgs; + n = List.length signature.C.generics.types - List.length ts + } in + L.log "TraitClauses" "%s has %d fn-level const generics" item_name f_ts.n_cgs; + L.log "TraitClauses" "%s has %d fn-level type params" item_name f_ts.n; + L.log "TraitClauses" "About to substitute cgs=%a, ts=%a into %a" pcgs cgs ptyps ts ptyp t; + let t = Krml.DeBruijn.(subst_tn' f_ts.n ts (subst_ctn'' f_ts.n_cgs cgs t)) in + L.log "TraitClauses" "After subtitution t=%a" ptyp t; + let ret, args = Krml.Helpers.flatten_arrow t in + let _, args = Krml.KList.split trait_ts.K.n_cgs args in + let t = Krml.Helpers.fold_arrow args ret in + L.log "TraitClauses" "After chopping t=%a" ptyp t; + let t = maybe_ts f_ts t in + L.log "TraitClauses" "After ts addition t=%a" ptyp t; + + let pretty_name = string_of_name env trait_name ^ "_" ^ item_name in + let ts = { + K.n = List.length signature.generics.types - trait_ts.n; + K.n_cgs = List.length signature.generics.const_generics - trait_ts.n_cgs; + } in + { pretty_name; t; clause_id; item_name; ts } + ) clause_mapping + + +(* Transforms a lookup result into a usable type, taking into account the fact that the internal Ast + is ML-style and does not have zero-argument functions. *) +and typ_of_signature env signature = + let { cg_types = const_generics_ts; arg_types = inputs; ret_type = output; ts; _ } = + lookup_signature env "" signature + in + + let adjusted_inputs = const_generics_ts @ inputs in + + let t = Krml.Helpers.fold_arrow adjusted_inputs output in + ts, t + + +and debug_trait_clause_mapping env mapping = + if mapping <> [] then + L.log "TraitClauses" "In this function, calls to trait bound methods are as follows:"; + List.iter (fun ((clause_id, item_name), (_, ts, trait_name, signature)) -> + let _, t = typ_of_signature env signature in + L.log "TraitClauses" "TraitClause %d (a.k.a. %s)::%s: %a has trait-level %d const generics, %d type vars" + (C.TraitClauseId.to_int clause_id) (string_of_name env trait_name) item_name ptyp t ts.K.n_cgs ts.n + ) mapping + + +(** Compiling function instantiations into krml application nodes. *) + +(* First step: produce an expression for the un-instantiated function reference, along with all the + type information required to build a proper instantiation. The function reference is an expression + that is either a reference to a variable in scope (trait methods), or to a top-level qualified + name, which encompasses both externally-defined function (builtins), or regular functions. *) +let lookup_fun (env: env) depth (f: C.fn_ptr): K.expr' * lookup_result = let open RustNames in let matches p = Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config p f in let builtin b = let { Builtin.name; typ; n_type_args; cg_args; _ } = b in let ret_type, arg_types = Krml.Helpers.flatten_arrow typ in - { name; n_type_args; arg_types; ret_type; cg_types = cg_args; is_assumed = true } + let ts = { K.n = n_type_args; K.n_cgs = List.length cg_args } in + K.EQualified name, { ts; arg_types; ret_type; cg_types = cg_args; is_known_builtin = true } in match List.find_opt (fun (p, _) -> matches p) known_builtins with | Some (_, b) -> builtin b | None -> - let regular f = - let { C.name; signature = { generics = { types = type_params; const_generics; _ }; inputs; output; _ }; _ } = env.get_nth_function f in - L.log "Calls" "--> name: %s" (string_of_name env name); - L.log "Calls" "--> args: %s, ret: %s" - (String.concat " ++ " (List.map (Charon.PrintTypes.ty_to_string env.format_env) inputs)) - (Charon.PrintTypes.ty_to_string env.format_env output); - let env = push_cg_binders env const_generics in - let env = push_type_binders env type_params in - { - name = lid_of_name env name; - n_type_args = List.length type_params; - cg_types = List.map (fun (v: C.const_generic_var) -> typ_of_literal_ty env v.ty) const_generics; - arg_types = List.map (typ_of_ty env) inputs; - ret_type = typ_of_ty env output; - is_assumed = false - } + + let lookup_result_of_fun_id fun_id = + let { C.name; signature; _ } = env.get_nth_function fun_id in + let lid = lid_of_name env name in + L.log "Calls" "%s--> name: %a" depth plid lid; + K.EQualified lid, + lookup_signature env depth signature in + match f.func with | FunId (FRegular f) -> - regular f + lookup_result_of_fun_id f | FunId (FAssumed f) -> Krml.Warn.fatal_error "unknown assumed function: %s" (C.show_assumed_fun_id f) @@ -615,8 +928,21 @@ let lookup_fun (env: env) (f: C.fn_ptr): lookup_result = match trait_ref.trait_id with | TraitImpl id -> let trait = env.get_nth_trait_impl id in - let f = List.assoc method_name trait.required_methods in - regular f + let f = List.assoc method_name (trait.required_methods @ trait.provided_methods) in + lookup_result_of_fun_id f + | Clause tcid -> + let f, t, sig_info = lookup_clause_binder env tcid method_name in + (* the sig_info is kind of redundant here *) + let t = match t with TPoly (_, t) -> t | _ -> t in + let ret_type, arg_types = Krml.Helpers.flatten_arrow t in + let cg_types, arg_types = Krml.KList.split sig_info.n_cgs arg_types in + EBound f, { + ts = sig_info; + cg_types; + arg_types; + ret_type; + is_known_builtin = false + } | _ -> Krml.Warn.fatal_error "Error looking trait ref: %s %s" (Charon.PrintTypes.trait_ref_to_string env.format_env trait_ref) method_name @@ -628,7 +954,10 @@ let fn_ptr_is_opaque env (fn_ptr: C.fn_ptr) = | _ -> false -let expression_of_fn_ptr env (fn_ptr: C.fn_ptr) = +(* This is a very core piece of logic that transforms a Rust fn_ptr into a krml AST node that + contains type application, const generic applications, and application of trait methods to + implement the dictionary-passing style. *) +let rec expression_of_fn_ptr env depth (fn_ptr: C.fn_ptr) = let { C.generics = { types = type_args; const_generics = const_generic_args; trait_refs; _ }; func; @@ -636,61 +965,163 @@ let expression_of_fn_ptr env (fn_ptr: C.fn_ptr) = } = fn_ptr in (* General case for function calls and trait method calls. *) - L.log "Calls" "Visiting call: %s" (Charon.PrintExpressions.fn_ptr_to_string env.format_env fn_ptr); - L.log "Calls" "is_array_map: %b" (RustNames.is_array_map env fn_ptr); - L.log "Calls" "--> %d type_args, %d const_generics, %d trait_refs" + L.log "Calls" "%sVisiting call: %s" depth (Charon.PrintExpressions.fn_ptr_to_string env.format_env fn_ptr); + L.log "Calls" "%sis_array_map: %b" depth (RustNames.is_array_map env fn_ptr); + L.log "Calls" "%s--> %d type_args, %d const_generics, %d trait_refs" depth (List.length type_args) (List.length const_generic_args) (List.length trait_refs); let type_args, const_generic_args, trait_refs = match func with - | TraitMethod ({ generics = { types; const_generics; trait_refs; _ }; _ }, _, _) -> - types @ type_args, const_generics @ const_generic_args, trait_refs @ trait_refs + | TraitMethod ({ trait_id; generics = { types; const_generics; trait_refs = trait_refs'; _ }; _ }, _, _) -> + L.log "Calls" "%s--> this is a trait method" depth; + let clause_const_generics = + match trait_id with + | Clause id when false -> + List.assoc id env.clause_arguments + | _ -> + [] + in + types @ type_args, clause_const_generics @ const_generics @ const_generic_args, trait_refs' @ trait_refs | _ -> type_args, const_generic_args, trait_refs in - L.log "Calls" "--> %d type_args, %d const_generics, %d trait_refs" + L.log "Calls" "%s--> %d type_args, %d const_generics, %d trait_refs" depth (List.length type_args) (List.length const_generic_args) (List.length trait_refs); - L.log "Calls" "--> trait_refs: %s\n" + L.log "Calls" "%s--> trait_refs: %s\n" depth (String.concat " ++ " (List.map (Charon.PrintTypes.trait_ref_to_string env.format_env) trait_refs)); - L.log "Calls" "--> pattern: %s" (string_of_fn_ptr env fn_ptr); - L.log "Calls" "--> type_args: %s" (String.concat ", " (List.map (Charon.PrintTypes.ty_to_string env.format_env) type_args)); + L.log "Calls" "%s--> pattern: %s" depth (string_of_fn_ptr env fn_ptr); + L.log "Calls" "%s--> type_args: %s" depth (String.concat ", " (List.map (Charon.PrintTypes.ty_to_string env.format_env) type_args)); let type_args = List.map (typ_of_ty env) type_args in let const_generic_args = List.map (expression_of_const_generic env) const_generic_args in - let { name; n_type_args = n_type_params; arg_types = inputs; ret_type = output; cg_types = cg_inputs; is_assumed } = - lookup_fun env fn_ptr + let f, { ts; arg_types = inputs; ret_type = output; cg_types = cg_inputs; is_known_builtin } = + lookup_fun env depth fn_ptr + in + L.log "Calls" "%s--> inputs: %a" depth ptyps inputs; + + (* Handling trait implementations for generic trait bounds in the callee. *) + let fn_ptrs = + if is_known_builtin then + (* If this is a known builtin implementation, we do not materialize trait methods, on the + basis that this is likely something from the standard library that exercises more features + that we can support, and that since we hand-write it, we don't need this level of precision + anyhow. *) + [] + else + List.concat_map (fun (trait_ref: C.trait_ref) -> + let name = string_of_name env (env.get_nth_trait_decl trait_ref.trait_decl_ref.trait_decl_id).name in + + match trait_ref.trait_id with + | _ when List.mem name blocklisted_trait_decls -> + (* Trait not supported -- don't synthesize arguments *) + [] + + | TraitImpl impl_id -> + (* Call-site has resolved trait clauses into a concrete trait implementation. *) + let trait_impl: C.trait_impl = env.get_nth_trait_impl impl_id in + + (* This must be in agreement, and in the same order as build_trait_clause_mapping *) + List.map (fun (item_name, decl_id) -> + let fn_ptr: C.fn_ptr = { + func = TraitMethod (trait_ref, item_name, decl_id); + generics = Charon.TypesUtils.empty_generic_args + } in + let fn_ptr = fst3 (expression_of_fn_ptr env (depth ^ " ") fn_ptr) in + fn_ptr + ) (trait_impl.required_methods @ trait_impl.provided_methods) + + | Clause clause_id -> + (* Caller it itself polymorphic and refers to one of its own clauses to synthesize + the clause arguments at call-site. *) + List.rev (Krml.KList.filter_mapi (fun i (var, t) -> + match var with + | TraitClauseMethod (clause_id', _, _) when clause_id = clause_id' -> + Some K.(with_type t (EBound i)) + | _ -> + None + ) env.binders) + + | ParentClause (_instance_id, decl_id, clause_id) -> + let trait_decl = env.get_nth_trait_decl decl_id in + let name = string_of_name env trait_decl.name in + let clause_id = C.TraitClauseId.to_int clause_id in + let parent_clause = List.nth trait_decl.parent_clauses clause_id in + let parent_clause_decl = env.get_nth_trait_decl parent_clause.trait_id in + let parent_name = string_of_name env parent_clause_decl.name in + Krml.KPrint.bprintf "looking up parent clause #%d of decl=%s = %s\n" clause_id name + parent_name; + if List.mem parent_name blocklisted_trait_decls then + [] + else + failwith ("Don't know how to resolve trait_ref " ^ C.show_trait_ref trait_ref) + + | _ -> + failwith ("Don't know how to resolve trait_ref " ^ C.show_trait_ref trait_ref) + + ) trait_refs in + L.log "Calls" "%s--> trait method impls: %d" depth (List.length fn_ptrs); (* This needs to match what is done in the FunGroup case (i.e. when we extract a definition). There are two behaviors depending on whether the function is assumed or not. *) let inputs = - if fn_ptr_is_opaque env fn_ptr then - if const_generic_args = [] && inputs = [] then [ K.TUnit ] else inputs - else - if inputs = [] then [ K.TUnit ] else inputs + if inputs = [] then [ K.TUnit ] else inputs in - if not (n_type_params = List.length type_args) then - Krml.Warn.fatal_error "%a: n_type_params %d != type_args %d" - Krml.PrintAst.Ops.plid name - n_type_params (List.length type_args); - let poly_t_sans_cgs = Krml.Helpers.fold_arrow inputs output in - let poly_t = Krml.Helpers.fold_arrow cg_inputs poly_t_sans_cgs in - let output, t = - Krml.DeBruijn.(subst_ctn (List.length env.binders) const_generic_args (subst_tn type_args output)), - Krml.DeBruijn.(subst_ctn (List.length env.binders) const_generic_args (subst_tn type_args poly_t_sans_cgs)) + let t_unapplied = maybe_ts ts (Krml.Helpers.fold_arrow (cg_inputs @ inputs) output) in + let offset = List.length env.binders - List.length env.cg_binders in + L.log "Calls" "%s--> t_unapplied: %a" depth ptyp t_unapplied; + L.log "Calls" "%s--> inputs: %a" depth ptyps inputs; + L.log "Calls" "%s--> const_generic_args: %a (offset: %d)" depth pexprs const_generic_args offset; + L.log "Calls" "%s--> fn_ptrs: %a (offset: %d)" depth (fun k e -> + List.iter (fun e -> + pexpr k e; Buffer.add_string k ": "; ptyp k e.typ + ) e + ) fn_ptrs offset; + + let t_applied = match t_unapplied with + | TPoly ({ n; n_cgs }, t) -> + let ts = { K.n = n - List.length type_args; n_cgs = n_cgs - List.length const_generic_args } in + if ts.n > 0 || ts.n_cgs > 0 then + K.TPoly (ts, t) + else + t + | t -> + t in + L.log "Calls" "%s--> t_applied (1): %a" depth ptyp t_applied; + let t_applied = Krml.DeBruijn.(subst_tn type_args (subst_ctn offset const_generic_args t_applied)) in + L.log "Calls" "%s--> t_applied (2): %a" depth ptyp t_applied; + let t_applied = + match t_applied with + | TPoly (ts, t) -> + assert (fn_ptrs = []); + let ret, args = Krml.Helpers.flatten_arrow t in + let _, args = Krml.KList.split (List.length const_generic_args) args in + K.TPoly (ts, Krml.Helpers.fold_arrow args ret) + | t -> + let ret, args = Krml.Helpers.flatten_arrow t in + let _, args = Krml.KList.split (List.length const_generic_args + List.length fn_ptrs) args in + Krml.Helpers.fold_arrow args ret + in + L.log "Calls" "%s--> t_applied: %a" depth ptyp t_applied; let hd = - let hd = K.with_type poly_t (K.EQualified name) in - if type_args <> [] || const_generic_args <> [] then - K.with_type t (K.ETApp (hd, const_generic_args, type_args)) + let hd = K.with_type t_unapplied f in + if type_args <> [] || const_generic_args <> [] || fn_ptrs <> [] then + K.with_type t_applied (K.ETApp (hd, const_generic_args, fn_ptrs, type_args)) else hd in - hd, is_assumed, output + L.log "Calls" "%s--> hd: %a" depth pexpr hd; + hd, is_known_builtin, + match t_applied with + | TPoly (ts, t) -> K.TPoly (ts, fst (Krml.Helpers.flatten_arrow t)) + | t -> fst (Krml.Helpers.flatten_arrow t) +let expression_of_fn_ptr env (fn_ptr: C.fn_ptr) = + expression_of_fn_ptr env "" fn_ptr let expression_of_operand (env: env) (p: C.operand): K.expr = match p with @@ -716,11 +1147,25 @@ let expression_of_operand (env: env) (p: C.operand): K.expr = Krml.Warn.fatal_error "expression_of_operand Constant: %s" (Charon.PrintExpressions.operand_to_string env.format_env p) +let is_str env var_id = + match lookup_with_original_type env var_id with + | _, _, TRef (_, TAdt (TAssumed TStr, { types = []; _ }), _) -> + true + | _ -> + false let expression_of_rvalue (env: env) (p: C.rvalue): K.expr = match p with | Use op -> expression_of_operand env op + + | RvRef ({ var_id; projection = [ Deref ]}, _) when is_str env var_id -> + (* Because we do not materialize the address of a string, we also have to + avoid dereferencing it. For now, we simply avoid reborrows and treat + them as simply passing the same constant string around (which in C is + passed by address naturally). *) + expression_of_var_id env var_id + | RvRef (p, _) -> let e, ty = expression_of_place env p in (* Arrays and ref to arrays are compiled as pointers in C; we allow on implicit array decay to @@ -764,24 +1209,38 @@ let expression_of_rvalue (env: env) (p: C.rvalue): K.expr = failwith "unsupported: AggregatedAdt / TAssume" | Aggregate (AggregatedClosure (func, generics), ops) -> - if ops <> [] then - failwith (Printf.sprintf "unsupported: AggregatedClosure (TODO: closure conversion): %d" (List.length ops)) - else - let fun_ptr = { C.func = C.FunId (FRegular func); generics } in - let e, _, _ = expression_of_fn_ptr env fun_ptr in - begin match e.typ with - | TArrow (TBuf (TUnit, _) as t_state, t) -> - (* Empty closure block, passed by address...? TBD *) - K.(with_type t (EApp (e, [ with_type t_state (EAddrOf Krml.Helpers.eunit) ]))) - | _ -> - assert false - end + let fun_ptr = { C.func = C.FunId (FRegular func); generics } in + let e, _, _ = expression_of_fn_ptr env fun_ptr in + begin match e.typ with + | TArrow (TBuf (TUnit, _) as t_state, t) -> + (* Empty closure block, passed by address...? TBD *) + K.(with_type t (EApp (e, [ with_type t_state (EAddrOf Krml.Helpers.eunit) ]))) + | TArrow (TBuf _ as t', t) -> + let ops = List.map (expression_of_operand env) ops in + let ops = + if List.length ops > 1 then + K.(with_type (TTuple (List.map (fun o -> o.typ) ops)) (ETuple ops)) + else + List.hd ops + in + let ops = [ K.(with_type t' (EAddrOf ops)) ] in + L.log "AstOfLlbc" "t'=%a t=%a closure ops are %a (typ: %a)" + ptyp t' ptyp t pexprs ops ptyp (List.hd ops).typ; + K.(with_type t (EApp (e, ops))) + | _ -> + Krml.KPrint.bprintf "Unknown closure\ntype: %a\nexpr: %a" + ptyp e.typ + pexpr e; + failwith "Can't handle arbitrary closures" + end | Aggregate (AggregatedArray (t, cg), ops) -> K.with_type (TArray (typ_of_ty env t, constant_of_scalar_value (assert_cg_scalar cg))) (K.EBufCreateL (Stack, List.map (expression_of_operand env) ops)) | Global (id, _generic_args) -> let global = env.get_nth_global id in K.with_type (typ_of_ty env global.ty) (K.EQualified (lid_of_name env global.name)) + | Len _ -> + failwith "unsupported: Len" let expression_of_assertion (env: env) ({ cond; expected }: C.assertion): K.expr = let cond = @@ -801,7 +1260,7 @@ let lesser t1 t2 = else if t2 = K.TAny then t2 else if t1 <> t2 then - Krml.Warn.fatal_error "lesser t1=%a t2=%a" Krml.PrintAst.Ops.ptyp t1 Krml.PrintAst.Ops.ptyp t2 + Krml.Warn.fatal_error "lesser t1=%a t2=%a" ptyp t1 ptyp t2 else t1 @@ -846,11 +1305,10 @@ let rec expression_of_raw_statement (env: env) (ret_var: C.var_id) (s: C.raw_sta let len = expression_of_const_generic env c in let dest, _ = expression_of_place env dest in let repeat = K.(with_type (Krml.Helpers.fold_arrow Builtin.array_repeat.cg_args Builtin.array_repeat.typ) (EQualified Builtin.array_repeat.name)) in - let diff = List.length env.binders in + let diff = List.length env.binders - List.length env.cg_binders in let repeat = K.(with_type (Krml.DeBruijn.( - subst_ct diff len 0 ( - subst_t t 0 (Builtin.array_repeat.typ)))) - (ETApp (repeat, [ len ], [ t ]))) in + subst_t t 0 (subst_ct diff len 0 (Builtin.array_repeat.typ)))) + (ETApp (repeat, [ len ], [], [ t ]))) in Krml.Helpers.with_unit K.( EAssign (dest, with_type dest.typ (EApp (repeat, [ e ])))) @@ -868,55 +1326,42 @@ let rec expression_of_raw_statement (env: env) (ret_var: C.var_id) (s: C.raw_sta Krml.Helpers.with_unit K.(EAssign (dest, maybe_addrof env ty (with_type t (EBufRead (e1, e2))))) | Call { func = FnOpRegular fn_ptr; args; dest; _ } - when false && Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from fn_ptr -> - (* Special treatment: From becomes a cast. *) + when ( + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from_u16 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from_u32 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from_u64 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from_i16 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from_i32 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from_i64 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.into_u16 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.into_u32 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.into_u64 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.into_i16 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.into_i32 fn_ptr || + Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.into_i64 fn_ptr || + false + ) -> + (* TODO: this can now be properly represented in the AST, this should go + away! there is *one* case in Kyber that is not caught by + Cleanup2.remove_trivial_into, and we need to figure out why. *) let matches p = Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config p fn_ptr in let w: Krml.Constant.width = - if matches RustNames.from_u16 then UInt16 - else if matches RustNames.from_u32 then UInt32 - else if matches RustNames.from_u64 then UInt64 - else if matches RustNames.from_i16 then Int16 - else if matches RustNames.from_i32 then Int32 - else if matches RustNames.from_i64 then Int64 + if matches RustNames.from_u16 || matches RustNames.into_u16 then UInt16 + else if matches RustNames.from_u32 || matches RustNames.into_u32 then UInt32 + else if matches RustNames.from_u64 || matches RustNames.into_u64 then UInt64 + else if matches RustNames.from_i16 || matches RustNames.into_i16 then Int16 + else if matches RustNames.from_i32 || matches RustNames.into_i32 then Int32 + else if matches RustNames.from_i64 || matches RustNames.into_i64 then Int64 else Krml.Warn.fatal_error "Unknown from-cast: %s" (string_of_fn_ptr env fn_ptr) in let dest, _ = expression_of_place env dest in let e = expression_of_operand env (Krml.KList.one args) in Krml.Helpers.with_unit K.(EAssign (dest, with_type (TInt w) (ECast (e, TInt w)))) - | Call { func = FnOpRegular fn_ptr; args; dest; _ } when RustNames.is_array_map env fn_ptr -> - (* Special treatment: bug in NameMatcher + avoid allocating a temporary array and directly - write the result in the destination. *) - let t_src = List.hd fn_ptr.generics.types in - let t_fun = List.nth fn_ptr.generics.types 1 in - let n = List.hd fn_ptr.generics.const_generics in - let src = List.hd args in - let f = List.nth args 1 in - - let n = expression_of_const_generic env n in - let t_src = typ_of_ty env t_src in - let t_fun = typ_of_ty env t_fun in - let t_dst = match t_fun with TArrow (t_src', t_dst) when t_src = t_src' -> t_dst | _ -> assert false in - let dest, _ = expression_of_place env dest in - let src = expression_of_operand env src in - let f = expression_of_operand env f in - - (* for (let i = 0; i < n; ++i) - dst[i] = f(src[i]); - *) - let module H = Krml.Helpers in - H.with_unit (K.EFor (Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *), - H.mk_lt_usize (Krml.DeBruijn.lift 1 n) (* i < n *), - H.mk_incr_usize (* i++ *), - let i = K.with_type H.usize (K.EBound 0) in - H.with_unit (K.EBufWrite (Krml.DeBruijn.lift 1 dest, i, - K.with_type t_dst ( - K.EApp (f, [ K.with_type t_src (K.EBufRead (Krml.DeBruijn.lift 1 src, i))])))))) - | Call { func = FnOpRegular fn_ptr; args; dest; _ } -> (* For now, we take trait type arguments to be part of the code-gen *) - let hd, _is_assumed, output_t = expression_of_fn_ptr env fn_ptr in + let hd, _is_known_builtin, output_t = expression_of_fn_ptr env fn_ptr in let dest, _ = expression_of_place env dest in let args = List.map (expression_of_operand env) args in (* This needs to match what is done in the FunGroup case (i.e. when we extract @@ -924,10 +1369,7 @@ let rec expression_of_raw_statement (env: env) (ret_var: C.var_id) (s: C.raw_sta assumed or not. *) (* Krml.KPrint.bprintf "Call to %s is assumed %b\n" (string_of_fn_ptr env fn_ptr) is_assumed; *) let args = - if fn_ptr_is_opaque env fn_ptr then - if fn_ptr.generics.const_generics = [] && args = [] then [ Krml.Helpers.eunit ] else args - else - if args = [] then [ Krml.Helpers.eunit ] else args + if args = [] then [ Krml.Helpers.eunit ] else args in let rhs = if args = [] then hd else K.with_type output_t (K.EApp (hd, args)) in @@ -1028,6 +1470,8 @@ let rec expression_of_raw_statement (env: env) (ret_var: C.var_id) (s: C.raw_sta (** Top-level declarations: orchestration *) + + let of_declaration_group (dg: 'id C.g_declaration_group) (f: 'id -> 'a): 'a list = (* We do not care about recursion as in C, everything is mutually recursive thanks to header inclusion. *) @@ -1086,22 +1530,15 @@ let decls_of_declarations (env: env) (d: C.declaration_group): K.decl list = (Charon.PrintLlbcAst.Ast.fun_decl_to_string env.format_env " " " " decl); assert (def_id = id); + let name = lid_of_name env name in match body with | None -> begin try (* Opaque function *) - let { C.generics = { types = type_params; const_generics; _ }; inputs; output ; _ } = signature in - let const_generics_ts = List.map (fun (c: C.const_generic_var) -> typ_of_literal_ty env c.ty) const_generics in - let env = push_cg_binders env const_generics in - let env = push_type_binders env type_params in - let inputs = List.map (typ_of_ty env) inputs in - let output = typ_of_ty env output in - let adjusted_inputs = if const_generics_ts = [] && inputs = [] then [ K.TUnit ] else const_generics_ts @ inputs in - let t = Krml.Helpers.fold_arrow adjusted_inputs output in - let name = lid_of_name env name in - Some (K.DExternal (None, [], List.length const_generics_ts, List.length type_params, name, t, [])) + let { K.n_cgs; n }, t = typ_of_signature env signature in + Some (K.DExternal (None, [], n_cgs, n, name, t, [])) with e -> - L.log "AstOfLLbc" "ERROR translating %s: %s\n%s" (string_of_name env decl.name) + L.log "AstOfLlbc" "ERROR translating %s: %s\n%s" (string_of_name env decl.name) (Printexc.to_string e) (Printexc.get_backtrace ()); None @@ -1113,7 +1550,24 @@ let decls_of_declarations (env: env) (d: C.declaration_group): K.decl list = else let env = push_cg_binders env signature.C.generics.const_generics in let env = push_type_binders env signature.C.generics.types in - let name = lid_of_name env name in + + L.log "AstOfLlbc" "ty of locals: %s" + (String.concat " ++ " (List.map (fun (local: C.var) -> + Charon.PrintTypes.ty_to_string env.format_env local.var_ty) locals)); + L.log "AstOfLlbc" "ty of inputs: %s" + (String.concat " ++ " (List.map (fun t -> + Charon.PrintTypes.ty_to_string env.format_env t) signature.C.inputs)); + + let clause_mapping = build_trait_clause_mapping env signature.C.generics.trait_clauses in + debug_trait_clause_mapping env clause_mapping; + + (* In definition fn f>, associates [ 42 ] to clause Foo *) + let env = { env with clause_arguments = + List.map (fun (tc: C.trait_clause) -> + tc.clause_id, tc.clause_generics.const_generics + ) signature.C.generics.trait_clauses + } in + (* `locals` contains, in order: special return variable; function arguments; local variables *) let args, locals = Krml.KList.split (arg_count + 1) locals in @@ -1123,18 +1577,36 @@ let decls_of_declarations (env: env) (d: C.declaration_group): K.decl list = let return_type = typ_of_ty env return_var.var_ty in (* Note: Rust allows zero-argument functions but the krml internal - representation wants a unit there. *) + representation wants a unit there. This is aligned with typ_of_signature. *) let t_unit = C.(TAdt (TTuple, { types = []; const_generics = []; regions = []; trait_refs = [] })) in let v_unit = { C.index = Charon.Expressions.VarId.of_int max_int; name = None; var_ty = t_unit } in let args = if args = [] then [ v_unit ] else args in - let arg_binders = List.map (fun (arg: C.const_generic_var) -> - Krml.Helpers.fresh_binder ~mut:true arg.name (typ_of_literal_ty env arg.ty) - ) signature.C.generics.const_generics @ List.map (fun (arg: C.var) -> - let name = Option.value ~default:"_" arg.name in - Krml.Helpers.fresh_binder ~mut:true name (typ_of_ty env arg.var_ty) - ) args in + (* At this stage, env has: + cg_binders = <> + type_binders = <> + binders = <> + *) + let clause_binders = mk_clause_binders_and_args env clause_mapping in + (* Now we turn it into: + binders = <> ++ <> ++ <> + *) + let env = push_clause_binders env clause_binders in let env = push_binders env args in + + let arg_binders = + List.map (fun (arg: C.const_generic_var) -> + Krml.Helpers.fresh_binder ~mut:true arg.name (typ_of_literal_ty env arg.ty) + ) signature.C.generics.const_generics @ + List.map (fun { pretty_name; t; _ } -> + Krml.Helpers.fresh_binder pretty_name t + ) clause_binders @ + List.map (fun (arg: C.var) -> + let name = Option.value ~default:"_" arg.name in + Krml.Helpers.fresh_binder ~mut:true name (typ_of_ty env arg.var_ty) + ) args + in + L.log "AstOfLlbc" "type of binders: %a" ptyps (List.map (fun o -> o.K.typ) arg_binders); let body = with_locals env return_type (return_var :: locals) (fun env -> expression_of_raw_statement env return_var.index body.content) @@ -1144,8 +1616,14 @@ let decls_of_declarations (env: env) (d: C.declaration_group): K.decl list = | Some (Hint | Always) -> [ Krml.Common.Inline ] | _ -> [] in - Some (K.DFunction (None, flags, List.length signature.C.generics.const_generics, - List.length signature.C.generics.types, return_type, name, arg_binders, body)) + (* This is kind of a hack here: we indicate that this function is intended to be + specialized, at monomorphization-time (which happens quite early on), on the cg + binders but also on the clause binders... This is ok because even though the + clause binders are not in env.cg_binders, well, types don't refer to clause + binders, so we won't have translation errors. *) + let n_cg = List.length signature.C.generics.const_generics in + let n = List.length signature.C.generics.types in + Some (K.DFunction (None, flags, n_cg, n, return_type, name, arg_binders, body)) ) | GlobalGroup id -> @@ -1182,6 +1660,7 @@ let file_of_crate (crate: Charon.LlbcAst.crate): Krml.Ast.file = let get_nth_type = fun id -> C.TypeDeclId.Map.find id type_decls in let get_nth_global = fun id -> C.GlobalDeclId.Map.find id global_decls in let get_nth_trait_impl = fun id -> C.TraitImplId.Map.find id trait_impls in + let get_nth_trait_decl = fun id -> C.TraitDeclId.Map.find id trait_decls in let format_env = Charon.PrintLlbcAst.Crate.crate_to_fmt_env crate in let name_ctx: Charon.NameMatcher.ctx = { type_decls; global_decls; trait_decls; fun_decls; trait_impls } in let env = { @@ -1189,12 +1668,14 @@ let file_of_crate (crate: Charon.LlbcAst.crate): Krml.Ast.file = get_nth_type; get_nth_global; get_nth_trait_impl; + get_nth_trait_decl; cg_binders = []; binders = []; type_binders = []; format_env; crate_name = name; name_ctx; - generic_params = { regions = []; types = []; const_generics = []; trait_clauses = [] } + generic_params = { regions = []; types = []; const_generics = []; trait_clauses = [] }; + clause_arguments = []; } in name, List.concat_map (decls_of_declarations env) declarations diff --git a/lib/Builtin.ml b/lib/Builtin.ml index e869c31..f49076d 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -51,6 +51,9 @@ type builtin = { arg_names: string list; } +let expr_of_builtin { name; typ; _ } = + K.(with_type typ (EQualified name)) + let array_to_slice = { name = ["Eurydice"], "array_to_slice"; typ = Krml.Helpers.fold_arrow [ @@ -156,6 +159,18 @@ let slice_index = { arg_names = ["s"; "i"] } +let slice_index_outparam = { + name = ["Eurydice"], "slice_index_outparam"; + typ = Krml.Helpers.fold_arrow [ + mk_slice (TBound 0); + TInt SizeT; + TBound 0 + ] TUnit; + n_type_args = 1; + cg_args = []; + arg_names = ["s"; "i"; "dst"] +} + let slice_subslice = { name = ["Eurydice"], "slice_subslice"; typ = Krml.Helpers.fold_arrow [ @@ -348,6 +363,7 @@ let files = [ array_repeat; array_into_iter; slice_index; + slice_index_outparam; slice_subslice; slice_subslice_to; slice_subslice_from; diff --git a/lib/Bundles.ml b/lib/Bundles.ml index 3250d32..bd9b374 100644 --- a/lib/Bundles.ml +++ b/lib/Bundles.ml @@ -1,15 +1,29 @@ (* A more modern version of the krml facility that matches on lids (instead of file names), and relies on a YAML file for configuration (rather than the cryptic syntax). *) +module L = Logging + +module K = Krml.Ast + +open Krml.Ast + type pattern = | Prefix of string list | Exact of string list + | Lid of lident + [@@deriving show] + +type visibility = Api | Internal | Private + [@@deriving show] type file = { name: string; - api: pattern list; - private_: pattern list; inline_static: bool; + library: bool; + definitions: (pattern * visibility) list; + monomorphizations_using: (pattern * visibility) list; + monomorphizations_of: (pattern * visibility) list; + monomorphizations_exact: (pattern * visibility) list; } type config = file list @@ -41,11 +55,18 @@ let parse_pattern (v: Yaml.value): pattern = | _ -> parsing_error "pattern not a list" +let parse_exact v: pattern = + match parse_pattern v with + | Exact lid -> Lid (Krml.KList.split_at_last lid) + | _ -> parsing_error "monomorphizations_exact does not take wildcards" + + let parse_file (v: Yaml.value): file = match v with | `O ls -> let count = ref 0 in let lookup k = try let r = List.assoc k ls in incr count; Some r with Not_found -> None in + let lookup_ k ls = try let r = List.assoc k ls in incr count; Some r with Not_found -> None in let name = match lookup "name" with | Some (`String name) -> name @@ -58,17 +79,43 @@ let parse_file (v: Yaml.value): file = | Some _ -> parsing_error "inline_static not a bool" | None -> false in - let api = - match lookup "api" with - | None -> [] - | Some (`A api) -> List.map parse_pattern api - | Some _ -> parsing_error "api not a list" + let library = + match lookup "library" with + | Some (`Bool library) -> library + | Some _ -> parsing_error "library not a bool" + | None -> false in - let private_ = - match lookup "private" with + let map_or f o k = + match lookup_ k o with | None -> [] - | Some (`A private_) -> List.map parse_pattern private_ - | Some _ -> parsing_error "private not a list" + | Some (`A l) -> List.map f l + | Some _ -> failwith (k ^ " is not a list") + in + (* TODO: fix copy-pasting *) + let definitions, monomorphizations_of, monomorphizations_using, monomorphizations_exact = + (* Preserve order *) + let rec parse ls = + match ls with + | [] -> [], [], [], [] + | (("api" | "internal" | "private") as k, o) :: ls -> + incr count; + let vis = match k with "api" -> Api | "internal" -> Internal | "private" -> Private | _ -> assert false in + let parse_pattern_vis p = parse_pattern p, vis in + let parse_exact_vis p = parse_exact p, vis in + let defs, m_of, m_using, m_exact = parse ls in + begin match o with + | `A pats -> List.map parse_pattern_vis pats @ defs, m_of, m_using, m_exact + | `O o -> + map_or parse_pattern_vis o "patterns" @ map_or parse_exact_vis o "exact" @ defs, + map_or parse_pattern_vis o "monomorphizations_of" @ m_of, + map_or parse_pattern_vis o "monomorphizations_using" @ m_using, + map_or parse_exact_vis o "monomorphizations_exact" @ m_exact + | _ -> failwith (k ^ " neither a list nor object") + end + | _ :: ls -> + parse ls + in + parse ls in let include_ = match lookup "include_in_h" with @@ -84,8 +131,8 @@ let parse_file (v: Yaml.value): file = in if !count < List.length ls then parsing_error "extraneous fields in file"; - Krml.Options.(add_include := include_ @ c_include_ @ !add_include); - { name; api; private_; inline_static } + Krml.Options.(add_early_include := include_ @ c_include_ @ !add_early_include); + { name; definitions; inline_static; library; monomorphizations_using; monomorphizations_of; monomorphizations_exact } | _ -> parsing_error "file must be an object" @@ -100,8 +147,6 @@ let parse_config (v: Yaml.value): config = | _ -> parsing_error "YAML file must be an object with key files" -open Krml.Ast - (** Constructing bundles *) let starts_with l prefix = @@ -115,8 +160,41 @@ let matches lid p = m = fst lid | Prefix prefix -> starts_with (fst lid) prefix + | Lid lid' -> + lid = lid' + +let find_map f l = + List.find_map (fun (arg, ret) -> if f arg then Some ret else None) l + +let mark_internal = + let add_if name flags = + let is_internal = List.mem Krml.Common.Internal flags in + if not is_internal && not (Krml.Inlining.always_live name) then + Krml.Common.Internal :: List.filter ((<>) Krml.Common.Private) flags + else + List.filter ((<>) Krml.Common.Private) flags + in + function + | DFunction (cc, flags, n_cgs, n, typ, name, binders, body) -> + Krml.KPrint.bprintf "Marking %a as internal\n" Krml.PrintAst.Ops.plid name; + DFunction (cc, add_if name flags, n_cgs, n, typ, name, binders, body) + | DGlobal (flags, name, n, typ, body) -> + DGlobal (add_if name flags, name, n, typ, body) + | DType (lid, flags, n_cgs, n, def) -> + DType (lid, add_if lid flags, n_cgs, n, def) + | DExternal (cc, flags, n_cg, n, lid, t, pp) -> + DExternal (cc, add_if lid flags, n_cg, n, lid, t, pp) -let bundle (files: file list) (c: config): files = +let adjust vis decl = + match vis with + | Api -> decl + | Private -> Krml.Bundles.mark_private decl + | Internal -> mark_internal decl + +let record_inline_static lid = + Krml.Options.(static_header := Lid lid :: !static_header) + +let bundle (files: Krml.Ast.file list) (c: config): files = let bundled = Hashtbl.create 137 in let bundle name decl = if Hashtbl.mem bundled name then @@ -124,32 +202,36 @@ let bundle (files: file list) (c: config): files = else Hashtbl.add bundled name [ decl ] in - let record_inline_static lid = - Krml.Options.(static_header := Lid lid :: !static_header) + let record_library lid = + Krml.Options.(library := Lid lid :: !library) in - let files = List.map (fun (filename, decls) -> + let files = List.map (fun ((filename: string), (decls: Krml.Ast.decl list)) -> filename, List.filter_map (fun decl -> let lid = lid_of_decl decl in - let rec find files = - match files with + let rec find config = + match config with | [] -> Krml.(KPrint.bprintf "%a doesn't go anywhere\n" PrintAst.Ops.plid lid); false - | { name; api; private_; inline_static } :: files -> - if List.exists (matches lid) api then begin - (* Krml.(KPrint.bprintf "%a goes (api) into %s\n" PrintAst.Ops.plid lid name); *) - bundle name decl; - if inline_static then - record_inline_static lid; - true - end else if List.exists (matches lid) private_ then begin - (* Krml.(KPrint.bprintf "%a goes (private) into %s\n" PrintAst.Ops.plid lid name); *) - bundle name (Krml.Bundles.mark_private decl); - if inline_static then - record_inline_static lid; - true - end else - find files + | { name; definitions; inline_static; library; _ } :: config -> + (* Krml.KPrint.bprintf "for %s, definitions are :\n" name; *) + (* List.iter (fun (p, vis) -> *) + (* Krml.KPrint.bprintf "%s: %s\n" (show_visibility vis) (show_pattern p) *) + (* ) definitions; *) + match List.find_map (fun (pat, vis) -> if matches lid pat then Some vis else None) definitions with + | None -> + find config + | Some vis -> + (* Krml.(KPrint.bprintf "%a goes into %s at vis %s\n" PrintAst.Ops.plid lid name (show_visibility vis)); *) + (* if List.length vis_ > 1 then *) + (* Krml.(KPrint.bprintf "vis_ was: %s\n" (String.concat ", " (List.map show_visibility vis_))); *) + let decl = adjust vis decl in + bundle name decl; + if inline_static then + record_inline_static lid; + if library then + record_library lid; + true in if find c then None @@ -171,3 +253,175 @@ let bundle (files: file list) (c: config): files = ) bundled (List.filter (fun (_, decls) -> decls <> []) files) +let libraries (files: Krml.Ast.file list): files = + List.map (fun (f, decls) -> + f, List.filter_map (fun d -> + let lid = Krml.Ast.lid_of_decl d in + if List.exists (fun p -> Krml.(Bundle.pattern_matches_lid p lid)) !Krml.Options.library then begin + Logging.log "Libraries" "%a becomes abstract\n" Krml.PrintAst.Ops.plid lid; + match d with + | DType (_, _, _, _, Abbrev _) as t -> + Some t + | DType _ -> + None + | d -> + Krml.Builtin.make_abstract_function_or_global d + end else + Some d + ) decls + ) files + +let topological_sort decls = + let module T = struct type color = White | Gray | Black end in + let open T in + let graph = Hashtbl.create 41 in + List.iter (fun decl -> + let deps = object (self) + inherit [_] reduce + method zero = [] + method plus = (@) + method! visit_EQualified _ lid = + [ lid ] + method! visit_TQualified _ lid = + [ lid ] + method! visit_TApp _ lid ts = + [ lid ] @ List.concat_map (self#visit_typ ()) ts + end#visit_decl () decl + in + Hashtbl.add graph (lid_of_decl decl) (ref White, deps, decl) + ) decls; + let stack = ref [] in + let rec dfs lid = + if Hashtbl.mem graph lid then + let r, deps, decl = Hashtbl.find graph lid in + match !r with + | Black -> () + | Gray -> failwith "dependency cycle" + | White -> + r := Gray; + List.iter dfs deps; + r := Black; + stack := decl :: !stack + in + List.iter (fun decl -> dfs (lid_of_decl decl)) decls; + List.rev !stack + +(* Second phase of bundling, post-monomorphization. This is Eurydice-specific, + as we oftentimes need to move definitions that have been /specialized/ using + e.g. a platform-specific trait into their own file. *) +let reassign_monomorphizations (files: Krml.Ast.file list) (config: config) = + let open Krml.Ast in + let open Krml.PrintAst.Ops in + (* Pure sanity check *) + let count_decls files = + List.fold_left (fun acc (_, decls) -> List.length decls + acc) 0 files + in + let c0 = count_decls files in + let target_of_lid = Hashtbl.create 41 in + let (|||) o1 o2 = + match o1 with + | Some _ -> o1 + | None -> o2 + in + let uses monomorphizations_using t = + object + inherit [_] reduce as super + method zero = None + method plus o1 o2 = if o1 = None then o2 else o1 + method! visit_TQualified _ lid' = + find_map (matches lid') monomorphizations_using + method! visit_TApp _ lid' ts = + find_map (matches lid') monomorphizations_using ||| super#visit_TApp () lid' ts + end#visit_typ () t + in + (* Review the function monomorphization state. + Semantics of `monomorphizations_using`: + if `lid`, below, is the result of a (function) monomorphization that + *uses* (in its arguments, `cgs`, below) an `lid'` that matches a + `monomorphizations_using` clause of file `name`, then `lid` moves to + `name`. + Semantics of `monomorphizations_of`: unlike above, this matches a + generic lid (e.g., we want all the monomorphized instances of `Result` to + go into a single file) + Semantics of `monomorphizations_exact`: self-explanatory + *) + Hashtbl.iter (fun (generic_lid, cgs, ts) monomorphized_lid -> + match List.find_map (fun { name; inline_static; monomorphizations_using; monomorphizations_of; monomorphizations_exact; _ } -> + (* Monomorphization resulting in exactly this name *) + find_map (matches monomorphized_lid) monomorphizations_exact ||| + (* Monomorphization using given trait name, amongst the arguments *) + List.find_map (fun e -> + match e.node with + | EQualified lid' -> find_map (matches lid') monomorphizations_using + | _ -> None + ) cgs ||| + (* Monomorphization using given type name *) + List.find_map (uses monomorphizations_using) ts ||| + (* Monomorphization of a given polymorphic name *) + find_map (matches generic_lid) monomorphizations_of |> + Option.map (fun vis -> name, inline_static, vis) + ) config with + | Some name -> + Hashtbl.add target_of_lid monomorphized_lid name + | None -> + () + ) Krml.MonomorphizationState.generated_lids; + (* Review the type monomorphization state. *) + Hashtbl.iter (fun (generic_lid, ts, _) (_, monomorphized_lid) -> + (* Krml.KPrint.bprintf "generic=%a, monomorphized=%a\n" plid generic_lid plid monomorphized_lid; *) + match List.find_map (fun { name; inline_static; monomorphizations_of; monomorphizations_using; monomorphizations_exact; _ } -> + find_map (matches monomorphized_lid) monomorphizations_exact ||| + List.find_map (uses monomorphizations_using) ts ||| + find_map (matches generic_lid) monomorphizations_of |> + Option.map (fun vis -> name, inline_static, vis) + ) config with + | Some name -> + Hashtbl.add target_of_lid monomorphized_lid name + | None -> + () + ) Krml.Monomorphization.state; + (* Debug *) + Hashtbl.iter (fun lid (target, _inline_static, vis) -> + L.log "Reassign" "%a goes into %s (vis: %s)" plid lid target (show_visibility vis) + ) target_of_lid; + (* Filter the files, plucking out those that move and registering them under + the right file name in `reassigned`. We maintain the invariant of one entry + per key in the table. *) + let reassigned = Hashtbl.create 41 in + let files = List.map (fun (f, decls) -> + f, List.filter (fun decl -> + let lid = lid_of_decl decl in + match Hashtbl.find_opt target_of_lid lid with + | None -> true + | Some (target, inline_static, vis) -> + let decl = adjust vis decl in + if inline_static then + record_inline_static lid; + if Hashtbl.mem reassigned target then + Hashtbl.replace reassigned target (decl :: Hashtbl.find reassigned target) + else + Hashtbl.add reassigned target [ decl ]; + false + ) decls + ) files in + (* Extend each file with the definitions that are moving into it. *) + let files = List.map (fun (f, decls) -> + let reassigned = + if Hashtbl.mem reassigned f then + let r = Hashtbl.find reassigned f in + Hashtbl.remove reassigned f; + r + else + [] + in + f, decls @ reassigned + ) files in + (* A quick topological sort to make sure type declarations come *before* + functions that use them. *) + let files = List.map (fun (f, decls) -> f, topological_sort decls) files in + + (* Deal with files that did not exist previously. *) + let files = files @ Hashtbl.fold (fun f reassigned acc -> (f, reassigned) :: acc) reassigned [] in + let c1 = count_decls files in + assert (c0 = c1); + files diff --git a/lib/Cleanup1.ml b/lib/Cleanup1.ml index 36c40e8..6949e26 100644 --- a/lib/Cleanup1.ml +++ b/lib/Cleanup1.ml @@ -77,12 +77,13 @@ let remove_assignments = object(self) control-flow (match, if, while); otherwise, just close everything now and move on (wildcard case). *) let rec recurse_or_close not_yet_closed e = + let t = e.typ in match e.node with | ELet _ -> (* let node: restart logic and jump back to match below *) self#visit_expr_w not_yet_closed e | EIfThenElse (e, e', e'') -> - with_type e.typ @@ close_now_over not_yet_closed ( + with_type t @@ close_now_over not_yet_closed ( (* We must now bind: *) (count e) ++ (* whichever variables were in the condition *) AtomSet.empty) (* unlike below, we are in terminal position, so we do not need to @@ -94,12 +95,12 @@ let remove_assignments = object(self) recurse_or_close not_yet_closed e', recurse_or_close not_yet_closed e'')) | EWhile (e, e') -> - with_type e.typ @@ close_now_over not_yet_closed + with_type t @@ close_now_over not_yet_closed (count e) (fun not_yet_closed -> EWhile (self#visit_expr_w not_yet_closed e, recurse_or_close not_yet_closed e')) | ESwitch (e, branches) -> - with_type e.typ @@ close_now_over not_yet_closed ( + with_type t @@ close_now_over not_yet_closed ( (* We must now bind: *) (count e) ++ (* i.e., whichever variables were in the condition *) AtomSet.empty) (* see above *) @@ -110,7 +111,7 @@ let remove_assignments = object(self) p, recurse_or_close not_yet_closed e ) branches)) | EMatch (c, e, branches) -> - with_type e.typ @@ close_now_over not_yet_closed ( + with_type t @@ close_now_over not_yet_closed ( (* We must now bind: *) (count e) ++ (* i.e., whichever variables were in the condition *) AtomSet.empty) (* see above *) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index a11ca45..6718572 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -2,6 +2,9 @@ open Krml.Ast open Krml.DeBruijn module H = Krml.Helpers +module L = Logging + +open Krml.PrintAst.Ops (* Target cleanups invoked from bin/main.ml *) @@ -111,7 +114,7 @@ let remove_array_repeats = object(self) method! visit_EApp env e es = match e.node, es with - | ETApp ({ node = EQualified lid; _ }, [ len ], [ _ ]), [ init ] when lid = Builtin.array_repeat.name -> + | ETApp ({ node = EQualified lid; _ }, [ len ], _, [ _ ]), [ init ] when lid = Builtin.array_repeat.name -> let l = match len.node with EConstant (_, s) -> int_of_string s | _ -> failwith "impossible" in let init = self#visit_expr env init in EBufCreateL (Stack, List.init l (fun _ -> init)) @@ -123,13 +126,13 @@ let remove_array_repeats = object(self) match e.node with | EConstant _ -> true - | EApp ({ node = ETApp ({ node = EQualified lid; _ }, [ _ ], [ _ ]); _ }, [ init ]) when lid = Builtin.array_repeat.name -> + | EApp ({ node = ETApp ({ node = EQualified lid; _ }, [ _ ], _, [ _ ]); _ }, [ init ]) when lid = Builtin.array_repeat.name -> all_repeats init | _ -> false in match e1.node with - | EApp ({ node = ETApp ({ node = EQualified lid; _ }, [ len ], [ _ ]); _ }, [ init ]) when lid = Builtin.array_repeat.name -> + | EApp ({ node = ETApp ({ node = EQualified lid; _ }, [ len ], _, [ _ ]); _ }, [ init ]) when lid = Builtin.array_repeat.name -> if all_repeats e1 then (* Further code-gen can handle nested ebufcreatel's by using nested static initializer lists, possiblye shortening to { 0 } if @@ -160,40 +163,118 @@ let remove_array_repeats = object(self) super#visit_ELet env b e1 e2 end -let remove_array_from_fn = object - inherit [_] map as super - - val mutable defs = Hashtbl.create 41 - - method! visit_DFunction _ cc flags n_cgs n t name bs e = - assert (n_cgs = 0 && n = 0); - match bs with - | [{ typ = TInt SizeT; _ }] -> - Hashtbl.add defs name e - | _ -> - () - ; ; - super#visit_DFunction () cc flags n_cgs n t name bs e +let remove_array_from_fn files = + let defs = Krml.Helpers.build_map files (fun tbl d -> + match d with + | DFunction (_, _, _, _, _, name, _, body) -> Hashtbl.add tbl name body + | _ -> ()) + in + object + inherit [_] map as super + + method! visit_DFunction _ cc flags n_cgs n t name bs e = + assert (n_cgs = 0 && n = 0); + Hashtbl.add defs name e; + super#visit_DFunction () cc flags n_cgs n t name bs e + + method! visit_EApp env e es = + match e.node with + | ETApp ({ node = EQualified (["core"; "array"], "from_fn"); _ }, + [ len ], + _, + [ t_elements; TArrow (t_index, TArrow (t_elements', TUnit)) ]) -> + (* Same as below, but catching the case where the type of elements is an + array and has undergone outparam optimization (i.e. the closure, + instead of having type size_t -> t_element, has type size_t -> t_element -> + unit *) + L.log "Cleanup2" "%a %a" ptyp t_elements ptyp t_elements'; + assert (t_elements' = t_elements); + assert (t_index = TInt SizeT); + assert (List.length es = 2); + let closure_lid, state = match (List.hd es).node with + | EQualified _ -> + List.hd es, [] + | EApp ({ node = EQualified lid; _ } as hd, [ e_state ]) -> + L.log "Cleanup2" "closure=%a" pexpr (Krml.DeBruijn.subst e_state 0 (Hashtbl.find defs lid)); + hd, [ e_state ] + | _ -> + L.log "Cleanup2" "closure=%a" pexpr (List.hd es); + failwith "unexpected closure shape" + in + (* First argument = closure, second argument = destination. Note that + the closure may itself be an application of the closure to the state + (but not always... is this unit argument elimination kicking in? not + sure). *) + let dst = List.nth es 1 in + EFor (Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *), + H.mk_lt_usize (Krml.DeBruijn.lift 1 len) (* i < len *), + H.mk_incr_usize (* i++ *), + let i = with_type H.usize (EBound 0) in + Krml.Helpers.with_unit (EApp (closure_lid, state @ [ i; with_type t_elements (EBufRead (Krml.DeBruijn.lift 1 dst, i)) ]))) + + | ETApp ({ node = EQualified (["core"; "array"], "from_fn"); _ }, + [ len ], + _, + [ t_elements; TArrow (t_index, t_elements') ]) -> + (* Not sure why this one inlines the body, but not above. *) + L.log "Cleanup2" "%a %a" ptyp t_elements ptyp t_elements'; + assert (t_elements' = t_elements); + assert (t_index = TInt SizeT); + assert (List.length es = 2); + let closure = match (List.hd es).node with + | EQualified lid -> + Hashtbl.find defs lid + | EApp ({ node = EQualified lid; _ }, [ e_state ]) -> + L.log "Cleanup2" "closure=%a" pexpr (Krml.DeBruijn.subst e_state 0 (Hashtbl.find defs lid)); + Krml.DeBruijn.subst e_state 1 (Hashtbl.find defs lid) + | _ -> + L.log "Cleanup2" "closure=%a" pexpr (List.hd es); + failwith "unexpected closure shape" + in + let dst = List.nth es 1 in + EFor (Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *), + H.mk_lt_usize (Krml.DeBruijn.lift 1 len) (* i < len *), + H.mk_incr_usize (* i++ *), + let i = with_type H.usize (EBound 0) in + Krml.Helpers.with_unit (EBufWrite (Krml.DeBruijn.lift 1 dst, i, closure))) + + | ETApp ({ node = EQualified ("core" :: "array" :: _, "map"); _ }, + [ len ], + _, + ts) -> + let t_src, t_dst = match ts with + | [ t_src; t_closure; t_dst ] -> + assert (t_closure = TArrow (t_src, t_dst)); + L.log "Cleanup2" "found array map from %a to %a" ptyp t_src ptyp t_dst; + t_src, t_dst + | _ -> + failwith "TODO: unknown map closure shape; is it an array outparam? (see above)" + in + let e_src, e_closure, e_dst = match es with + | [ e_src; e_closure; e_dst ] -> e_src, e_closure, e_dst + | _ -> failwith "unknown shape of arguments to array map" + in + let closure_lid, state = match e_closure.node with + | EQualified _ -> + e_closure, [] + | EApp ({ node = EQualified lid; _ } as hd, [ e_state ]) -> + L.log "Cleanup2" "map closure=%a" pexpr (Krml.DeBruijn.subst e_state 0 (Hashtbl.find defs lid)); + hd, [ e_state ] + | _ -> + L.log "Cleanup2" "map closure=%a" pexpr (List.hd es); + failwith "unexpected map closure shape" + in + EFor (Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *), + H.mk_lt_usize (Krml.DeBruijn.lift 1 len) (* i < len *), + H.mk_incr_usize (* i++ *), + let i = with_type H.usize (EBound 0) in + let e_src_i = with_type t_src (EBufRead (Krml.DeBruijn.lift 1 e_src, i)) in + Krml.Helpers.with_unit (EBufWrite (Krml.DeBruijn.lift 1 e_dst, i, + with_type t_dst (EApp (closure_lid, state @ [ e_src_i ]))))) - method! visit_EApp env e es = - match e.node with - | ETApp ({ node = EQualified (["core"; "array"], "from_fn"); _ }, - [ len ], - [ t_elements; TArrow (t_index, t_elements') ]) -> - assert (t_elements' = t_elements); - assert (t_index = TInt SizeT); - assert (List.length es = 2); - let closure = Krml.Helpers.assert_elid (List.nth es 0).node in - assert (Hashtbl.mem defs closure); - let dst = List.nth es 1 in - EFor (Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *), - H.mk_lt_usize (Krml.DeBruijn.lift 1 len) (* i < len *), - H.mk_incr_usize (* i++ *), - let i = with_type H.usize (EBound 0) in - Krml.Helpers.with_unit (EBufWrite (Krml.DeBruijn.lift 1 dst, i, Hashtbl.find defs closure))) - | _ -> - super#visit_EApp env e es -end + | _ -> + super#visit_EApp env e es + end#visit_files () files let rewrite_slice_to_array = object(_self) @@ -201,12 +282,13 @@ let rewrite_slice_to_array = object(_self) method! visit_expr ((), _ as env) e = match e.node with - | EApp ({ node = ETApp ({ node = EQualified lid; _ }, _, ts); _ }, es) when lid = Builtin.slice_to_array.name -> + | EApp ({ node = ETApp ({ node = EQualified lid; _ }, _, _, ts); _ }, es) when lid = Builtin.slice_to_array.name -> let src = Krml.KList.one es in (* src = slice ..., dst = array ... *) let result_t = e.typ in let slice_to_array2 = with_type Builtin.slice_to_array2.typ (EQualified Builtin.slice_to_array2.name) in - let slice_to_array2 = with_type (subst_tn ts Builtin.slice_to_array2.typ) (ETApp (slice_to_array2, [], ts)) in + let slice_to_array2 = with_type + (Krml.MonomorphizationState.resolve (subst_tn ts Builtin.slice_to_array2.typ)) (ETApp (slice_to_array2, [], [], ts)) in (* let dst = *) with_type result_t (ELet (H.fresh_binder "dst" result_t, H.any, (* let _ = *) @@ -230,8 +312,10 @@ 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 -> + | ETApp ({ node = EQualified (["core"; "convert"; _ ], "into"); _ }, [], _, [ t1; t2 ]), [ e1 ] when t1 = t2 -> e1.node + | ETApp ({ node = EQualified (["core"; "convert"; _ ], "into"); _ }, [], _, [ TInt _ ; TInt _ as t2 ]), [ e1 ] -> + ECast (e1, t2) | _ -> EApp (e, es) end @@ -352,6 +436,7 @@ let resugar_loops = object(self) EApp ({ node = ETApp ( { node = EQualified (["core"; "iter"; "traits"; "collect"; _], "into_iter"); _ }, [], + _, [ TApp ((["core"; "ops"; "range"], "Range"), _t') ] ); _ }, [ { node = EFlat [ Some "start", e_start; Some "end", e_end ]; _ } @@ -363,7 +448,7 @@ let resugar_loops = object(self) node = EApp ({ node = ETApp ({ node = EQualified (["core";"iter";"range";_], "next"); _ - }, [], [ t' ]); + }, [], [], [ t' ]); _ }, [{ node = EAddrOf({ @@ -401,6 +486,7 @@ let resugar_loops = object(self) EApp ({ node = ETApp ( { node = EQualified (["core"; "iter"; "traits"; "collect"; _], "into_iter"); _ }, [], + _, [ TApp ((["core"; "ops"; "range"], "Range"), _t') ] ); _ }, [ { node = EFlat [ Some "start", e_start; Some "end", e_end ]; _ } @@ -412,7 +498,7 @@ let resugar_loops = object(self) node = EApp ({ node = ETApp ({ node = EQualified (["core";"iter";"range";_], "next"); _ - }, [], [ t' ]); + }, [], [], [ t' ]); _ }, [{ node = EAddrOf({ @@ -450,3 +536,28 @@ let resugar_loops = object(self) end + +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 + diff --git a/lib/Cleanup3.ml b/lib/Cleanup3.ml index 7229e73..98c9bb2 100644 --- a/lib/Cleanup3.ml +++ b/lib/Cleanup3.ml @@ -82,3 +82,13 @@ let build_cg_macros = object(self) else self#zero end + +let add_extra_type_to_slice_index = object(_self) + inherit [_] map as super + method! visit_ETApp ((), _ as env) e cgs cgs' ts = + match e.node, cgs, cgs', ts with + | EQualified (["Eurydice"], "slice_index"), [], [], [ t_elements ] -> + ETApp (e, cgs, cgs', ts @ [ TBuf (t_elements, false) ]) + | _ -> + super#visit_ETApp env e cgs cgs' ts +end diff --git a/lib/PreCleanup.ml b/lib/PreCleanup.ml index f83b14f..07c1732 100644 --- a/lib/PreCleanup.ml +++ b/lib/PreCleanup.ml @@ -72,3 +72,51 @@ let precleanup files = let files = flatten_sequences files in let files = adjust_shifts files in files + +let merge files = + let open Krml.Idents in + let open Krml.PrintAst.Ops in + let merge_decl lid d1 d2 = + match d1, d2 with + | Some d1, None + | None, Some d1 -> + Some d1 + | None, None -> + assert false + | Some d1, Some d2 -> + let is_external = function DExternal _ -> true | _ -> false in + let check_equal () = + if d1 <> d2 then begin + Krml.KPrint.bprintf "%a is:\n%a\n\nVS\n\n%a\n" plid lid pdecl d1 pdecl d2; + failwith "can't reconcile these two definitions" + end + in + match d1, d2 with + | DExternal _, d2 + | d2, DExternal _ -> + if is_external d2 then + check_equal (); + Some d2 + | _ -> + check_equal (); + Some d1 + in + let decl_map decls = + LidMap.of_seq (List.to_seq (List.map (fun d -> lid_of_decl d, d) decls)) + in + let merge_decls decls1 decls2 = + LidMap.merge merge_decl decls1 decls2 + in + let concat_filenames f1 f2 = + if f1 = "" then f2 else f1 ^ "_" ^ f2 + in + let merge_files (f1, decls1) (f2, decls2) = + concat_filenames f1 f2, merge_decls decls1 (decl_map decls2) + in + let f, decls = + List.fold_left merge_files ("", LidMap.empty) files + in + let decls = List.map snd (List.of_seq (LidMap.to_seq decls)) in + let decls = Bundles.topological_sort decls in + f, decls + diff --git a/lib/dune b/lib/dune index 754ee4f..c8a437a 100644 --- a/lib/dune +++ b/lib/dune @@ -1,3 +1,8 @@ (library (name eurydice) - (libraries charon krml yaml)) + (libraries charon krml yaml) + + (preprocess + (pps ppx_deriving.std) + ) +) diff --git a/test/closure/Cargo.lock b/test/closure/Cargo.lock new file mode 100644 index 0000000..cda8226 --- /dev/null +++ b/test/closure/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "closure" +version = "0.1.0" diff --git a/test/closure/Cargo.toml b/test/closure/Cargo.toml new file mode 100644 index 0000000..a375fdc --- /dev/null +++ b/test/closure/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "closure" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/closure/src/main.rs b/test/closure/src/main.rs new file mode 100644 index 0000000..d600668 --- /dev/null +++ b/test/closure/src/main.rs @@ -0,0 +1,11 @@ +fn f() -> [usize; 1] { + let s = [0; 1]; + let a: [usize; 1] = core::array::from_fn(|i| s[0]+i); + a +} + +fn main() { + let actual = f()[0]; + let expected = 0; + assert_eq!(actual, expected); +} diff --git a/test/mutable_slice_range/Cargo.lock b/test/mutable_slice_range/Cargo.lock new file mode 100644 index 0000000..8f65554 --- /dev/null +++ b/test/mutable_slice_range/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "mutable_slice_range" +version = "0.1.0" diff --git a/test/mutable_slice_range/Cargo.toml b/test/mutable_slice_range/Cargo.toml new file mode 100644 index 0000000..8e90357 --- /dev/null +++ b/test/mutable_slice_range/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "mutable_slice_range" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/mutable_slice_range/src/main.rs b/test/mutable_slice_range/src/main.rs new file mode 100644 index 0000000..78d4abc --- /dev/null +++ b/test/mutable_slice_range/src/main.rs @@ -0,0 +1,10 @@ +fn test(x: &mut [u8]) -> u8 { + x[0] +} + +fn main() { + let mut x = [ 0; 8 ]; + let result = test(&mut x[..]); + let expected = 0; + assert_eq!(result, expected); +} diff --git a/test/nested_arrays2/Cargo.lock b/test/nested_arrays2/Cargo.lock new file mode 100644 index 0000000..a4cf398 --- /dev/null +++ b/test/nested_arrays2/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "nested_arrays2" +version = "0.1.0" diff --git a/test/nested_arrays2/Cargo.toml b/test/nested_arrays2/Cargo.toml new file mode 100644 index 0000000..f7a51da --- /dev/null +++ b/test/nested_arrays2/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "nested_arrays2" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/nested_arrays2/src/main.rs b/test/nested_arrays2/src/main.rs new file mode 100644 index 0000000..231f1a0 --- /dev/null +++ b/test/nested_arrays2/src/main.rs @@ -0,0 +1,4 @@ +const TABLE: [[u8; 1]; 1] = [[1]]; + +fn main() { +} diff --git a/test/partial_eq/Cargo.lock b/test/partial_eq/Cargo.lock new file mode 100644 index 0000000..77a19b2 --- /dev/null +++ b/test/partial_eq/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "partial_eq" +version = "0.1.0" diff --git a/test/partial_eq/Cargo.toml b/test/partial_eq/Cargo.toml new file mode 100644 index 0000000..c92fafd --- /dev/null +++ b/test/partial_eq/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "partial_eq" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/partial_eq/src/main.rs b/test/partial_eq/src/main.rs new file mode 100644 index 0000000..7c6edba --- /dev/null +++ b/test/partial_eq/src/main.rs @@ -0,0 +1,8 @@ +#[derive(PartialEq, Debug)] +#[repr(u32)] +pub enum Enum { A = 0 } + +fn main() { + let expected = Enum::A; + assert_eq!(expected, expected) +} diff --git a/test/partial_eq/stubs.c b/test/partial_eq/stubs.c new file mode 100644 index 0000000..dbc3af5 --- /dev/null +++ b/test/partial_eq/stubs.c @@ -0,0 +1,6 @@ +#include "partial_eq.h" + +extern core_result_Result_____core_fmt_Error +core_fmt__core__fmt__Formatter__a__7__write_str(core_fmt_Formatter *x0, Prims_string x1) { + return ((core_result_Result_____core_fmt_Error){ .tag = core_result_Ok, .f0 = NULL }); +} diff --git a/test/slice_array/Cargo.lock b/test/slice_array/Cargo.lock new file mode 100644 index 0000000..da68b67 --- /dev/null +++ b/test/slice_array/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "slice_array" +version = "0.1.0" diff --git a/test/slice_array/Cargo.toml b/test/slice_array/Cargo.toml new file mode 100644 index 0000000..ff9bc7a --- /dev/null +++ b/test/slice_array/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "slice_array" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/slice_array/src/main.rs b/test/slice_array/src/main.rs new file mode 100644 index 0000000..cb7daa9 --- /dev/null +++ b/test/slice_array/src/main.rs @@ -0,0 +1,24 @@ +fn f1() { + let mut x = [[0u8; 4]; 4]; + let (y0, _y1) = x.split_at_mut(2); + y0[0][0] = 1; + let actual = x[0][0]; + let expected = 1; + assert_eq!(actual, expected); +} + +fn f2() { + let mut x = [[0u8; 4]; 4]; + let (y0, _y1) = x.split_at_mut(2); + // generates a copy + let mut z = y0[0]; + z[0] = 1; + let actual = x[0][0]; + let expected = 0; + assert_eq!(actual, expected); +} + +fn main() { + f1(); + f2(); +} diff --git a/test/where_clauses/Cargo.lock b/test/where_clauses/Cargo.lock new file mode 100644 index 0000000..d60ba4d --- /dev/null +++ b/test/where_clauses/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "where_clauses" +version = "0.1.0" diff --git a/test/where_clauses/Cargo.toml b/test/where_clauses/Cargo.toml new file mode 100644 index 0000000..26a0c14 --- /dev/null +++ b/test/where_clauses/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "where_clauses" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/where_clauses/src/main.rs b/test/where_clauses/src/main.rs new file mode 100644 index 0000000..daff183 --- /dev/null +++ b/test/where_clauses/src/main.rs @@ -0,0 +1,25 @@ +trait Mul2 { + fn mul2 (x: Self) -> Self; + fn add (x: Self, y: Self) -> Self; +} + +trait MyImpl { + fn mul4 (x: T, y: T) -> T { + T::add(T::mul2(x), T::mul2(y)) + } +} + +struct Foo { } + +impl Mul2 for u64 { + fn mul2(x: u64) -> u64 { x << 2 } + fn add(x: u64, y: u64) -> u64 { x + y } +} + +impl MyImpl for Foo { +} + +fn main() { + let x = Foo::mul4(0u64, 0u64); + assert_eq!(x, 0u64); +} diff --git a/test/where_clauses_closures/Cargo.lock b/test/where_clauses_closures/Cargo.lock new file mode 100644 index 0000000..58db8b3 --- /dev/null +++ b/test/where_clauses_closures/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "where_clauses_closures" +version = "0.1.0" diff --git a/test/where_clauses_closures/Cargo.toml b/test/where_clauses_closures/Cargo.toml new file mode 100644 index 0000000..24c3bfc --- /dev/null +++ b/test/where_clauses_closures/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "where_clauses_closures" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/where_clauses_closures/src/main.rs b/test/where_clauses_closures/src/main.rs new file mode 100644 index 0000000..134f10a --- /dev/null +++ b/test/where_clauses_closures/src/main.rs @@ -0,0 +1,17 @@ +trait Ops { + fn zero() -> Self; + fn of_usize(x: usize) -> Self; +} + +impl Ops<1> for usize { + fn zero() -> Self { 0 } + fn of_usize(x: usize) -> Self { x.into() } +} + +fn test+Copy>() -> (T, T) { + let x: [ T; 1 ] = core::array::from_fn(|i| T::of_usize(i)); + let y = T::zero(); + (x[0], y) +} + +fn main() { let (x, y) = test::<1,usize>(); assert_eq!(x, y); } diff --git a/test/where_clauses_fncg/Cargo.lock b/test/where_clauses_fncg/Cargo.lock new file mode 100644 index 0000000..a41a6aa --- /dev/null +++ b/test/where_clauses_fncg/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "where_clauses_fncg" +version = "0.1.0" diff --git a/test/where_clauses_fncg/Cargo.toml b/test/where_clauses_fncg/Cargo.toml new file mode 100644 index 0000000..6125c9b --- /dev/null +++ b/test/where_clauses_fncg/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "where_clauses_fncg" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/where_clauses_fncg/src/main.rs b/test/where_clauses_fncg/src/main.rs new file mode 100644 index 0000000..e1b8ae0 --- /dev/null +++ b/test/where_clauses_fncg/src/main.rs @@ -0,0 +1,17 @@ +trait Foo { + fn bar(x: [[u8; L]; K], y: [[u8; K]; L]) -> Self; +} + +impl Foo for u64 { + fn bar(x: [[u8; L]; K], _: [[u8; K]; L]) -> Self { x[0][0].into() } +} + +fn f>() -> T { + T::bar([[0; 4]; L], [[0; L]; 4]) +} + +fn main() { + let r = f::<6, 8, 10, u64>(); + let expected = 0; + assert_eq!(r, expected); +} diff --git a/test/where_clauses_simple/Cargo.lock b/test/where_clauses_simple/Cargo.lock new file mode 100644 index 0000000..01f5ddb --- /dev/null +++ b/test/where_clauses_simple/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "where_clauses_simple" +version = "0.1.0" diff --git a/test/where_clauses_simple/Cargo.toml b/test/where_clauses_simple/Cargo.toml new file mode 100644 index 0000000..40b9144 --- /dev/null +++ b/test/where_clauses_simple/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "where_clauses_simple" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/where_clauses_simple/src/main.rs b/test/where_clauses_simple/src/main.rs new file mode 100644 index 0000000..f3f2598 --- /dev/null +++ b/test/where_clauses_simple/src/main.rs @@ -0,0 +1,93 @@ +// The difficulty with implementing traits as dictionaries is the mismatch in terms of const +// generics (types are less of an issue somewhat). + +// In this trait decl, method signatures (as found in the trait_decl) are all parametric over K +trait Ops { + // usize -> Self -> Self -> Self + fn add (x: [u16; K], y: Self) -> Self; + // usize -> u16 -> Self + fn of_u16 (x: u16) -> Self; +} + +// Here, however, the signatures in this trait impl are NOT parametric over K +impl Ops<1> for u64 { + // [u16; 1] -> u64 -> u64 + fn add (x: [u16; 1], y: u64) -> u64 { Into::::into(x[0]) + y } + // u16 -> u64 + fn of_u16 (x: u16) -> u64 { x.into() } +} + +impl Ops for usize { + // usize -> [u16; 1] -> usize -> usize + fn add (x: [u16; K], y: usize) -> usize { Into::::into(x[0]) + y + K } + // usize -> u16 -> usize + fn of_u16 (x: u16) -> usize { x.into() } +} + +fn fn_k>() -> T { + // NO CONST GENERICS PROVIDED AT THIS CALL-SITE + // The call sites only have the the method-level const generics. + let x = T::of_u16(0); + T::add([0; K], x) +} + +fn fn_1+Copy>() -> T { + // NO CONST GENERICS PROVIDED AT THIS CALL-SITE + let x = T::of_u16(0); + T::add([0; 1], x) +} + +fn k_calls_k() { + // fn_k receives an add function that starts with size_t -> ... (for the impl-level const + // generic) + let r = fn_k::<3, usize>(); + let r_expected = 3; + assert_eq!(r, r_expected); +} + +fn k_calls_one() { + // fn_k receives an add function that DOES NOT start with size_t -> ... + let r = fn_k::<1, u64>(); + let r_expected = 0; + assert_eq!(r, r_expected); +} + +fn one_calls_k() { + let r = fn_1::(); + let r_expected = 1; + assert_eq!(r, r_expected); +} + +fn one_calls_one() { + let r = fn_1::(); + let r_expected = 0; + assert_eq!(r, r_expected); +} + +fn double + Copy, U: Ops<1>+Copy> (x: T, y: U) -> (T, U) { + (T::add([0; 1], x), U::add([0; 1], y)) +} + +fn double_k + Copy, U: Ops<1>+Copy> (x: T, y: U) -> (T, U) { + (T::add([0; K], x), U::add([0; 1], y)) +} + +fn main() { + // The four common situations with const generics in bounds. + k_calls_k(); + k_calls_one(); + one_calls_k(); + one_calls_one(); + + // Slightly more involved tests. + let x = double(1u64, 1usize); + let y = double_k::<3usize, usize, u64>(1usize, 1u64); + let x_0 = 1u64; + let x_1 = 2usize; + assert_eq!(x.0, x_0); + assert_eq!(x.1, x_1); + let y_0 = 4usize; + let y_1 = 1u64; + assert_eq!(y.0, y_0); + assert_eq!(y.1, y_1); +}