diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Extract.ml | 45 | ||||
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 304 | ||||
| -rw-r--r-- | compiler/LlbcAstUtils.ml | 19 | ||||
| -rw-r--r-- | compiler/Translate.ml | 10 |
4 files changed, 340 insertions, 38 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index afd722e5..6b6a2686 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -234,26 +234,20 @@ let assumed_adts () : (assumed_ty * string) list = (Array, "Array"); (Slice, "Slice"); (Str, "Str"); + (RawPtr Mut, "MutRawPtr"); + (RawPtr Const, "ConstRawPtr"); ] - | Coq | FStar -> + | Coq | FStar | HOL4 -> [ (State, "state"); (Result, "result"); (Error, "error"); - (Fuel, "nat"); - (Array, "array"); - (Slice, "slice"); - (Str, "str"); - ] - | HOL4 -> - [ - (State, "state"); - (Result, "result"); - (Error, "error"); - (Fuel, "num"); + (Fuel, if !backend = HOL4 then "num" else "nat"); (Array, "array"); (Slice, "slice"); (Str, "str"); + (RawPtr Mut, "mut_raw_ptr"); + (RawPtr Const, "const_raw_ptr"); ] let assumed_struct_constructors () : (assumed_ty * string) list = @@ -1378,7 +1372,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : let def_name = match info with | None -> ctx.fmt.type_name def.name - | Some info -> String.concat "." info.rust_name + | Some info -> info.extract_name in let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in (* Compute and register: @@ -4281,16 +4275,9 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) string * (RegionGroupId.id option * string) list = let compute_fun_name (f : fun_decl) : RegionGroupId.id option * string = - (* We do something special: we use the base name but remove everything - but the crate (because [get_name] removes it) and the last ident. - This allows us to reuse the [ctx_compute_fun_decl] function. - *) - let basename : name = - match (f.basename : name) with - | Ident crate :: name -> - Ident crate :: [ Collections.List.last name ] - | _ -> raise (Failure "Unexpected") - in + (* We do something special to reuse the [ctx_compute_fun_decl] + function. TODO: make it cleaner. *) + let basename : name = [ Ident item_name ] in let f = { f with basename } in let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in let name = ctx_compute_fun_name trans f ctx in @@ -4503,6 +4490,17 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params cg_params trait_clauses; + (* Add the parent clauses as local clauses, so that we can refer to them *) + let ctx = + List.fold_left + (fun ctx clause -> + let item_name = + ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx + in + ctx_add (LocalTraitClauseId clause.clause_id) item_name ctx) + ctx decl.generics.trait_clauses + in + F.pp_print_space fmt (); (match !backend with | Lean -> F.pp_print_string fmt "where" @@ -4522,6 +4520,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx in let ty () = + F.pp_print_space fmt (); extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause in extract_trait_decl_item ctx fmt item_name ty) diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 4c6fe014..c781463e 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -121,7 +121,7 @@ let builtin_types () : builtin_type_info list = rust_name = [ "alloc"; "alloc"; "Global" ]; extract_name = (match !backend with - | Lean -> "AllocGlobal" + | Lean -> "alloc.alloc.Global" | Coq | FStar | HOL4 -> "alloc_global"); keep_params = None; body_info = None; @@ -335,7 +335,7 @@ let builtin_funs () : rg = None; extract_name = (match !backend with - | FStar | Coq | HOL4 -> "alloc_boxed_box_deref" + | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref" | Lean -> "alloc.boxed.Box.deref"); }; (* The backward function shouldn't be used *) @@ -343,7 +343,7 @@ let builtin_funs () : rg = rg0; extract_name = (match !backend with - | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_back" + | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_back" | Lean -> "alloc.boxed.Box.deref_back"); }; ] ); @@ -354,7 +354,7 @@ let builtin_funs () : rg = None; extract_name = (match !backend with - | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut" + | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_mut" | Lean -> "alloc.boxed.Box.deref_mut"); }; { @@ -365,6 +365,179 @@ let builtin_funs () : | Lean -> "alloc.boxed.Box.deref_mut_back"); }; ] ); + (* TODO: fix the same like "[T]" below *) + ( [ "core"; "slice"; "index"; "[T]"; "index" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Slice_index" + | Lean -> "core.slice.index.Slice.index"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_back" + | Lean -> "core.slice.index.Slice.index_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "[T]"; "index_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut" + | Lean -> "core.slice.index.Slice.index_mut"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut_back" + | Lean -> "core.slice.index.Slice.index_mut_back"); + }; + ] ); + ( [ "core"; "array"; "[T; N]"; "index" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_array_Array_index" + | Lean -> "core.array.Array.index"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_array_Array_index_back" + | Lean -> "core.array.Array.index_back"); + }; + ] ); + ( [ "core"; "array"; "[T; N]"; "index_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_array_Array_index_mut" + | Lean -> "core.array.Array.index_mut"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_array_Array_index_mut_back" + | Lean -> "core.array.Array.index_mut_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "get" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get" + | Lean -> "core.slice.index.Range.get"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_back" + | Lean -> "core.slice.index.Range.get_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "get_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut" + | Lean -> "core.slice.index.Range.get_mut"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut_back" + | Lean -> "core.slice.index.Range.get_mut_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "index" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_index" + | Lean -> "core.slice.index.Range.index"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_index_back" + | Lean -> "core.slice.index.Range.index_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "index_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut" + | Lean -> "core.slice.index.Range.index_mut"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut_back" + | Lean -> "core.slice.index.Range.index_mut_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "get_unchecked" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked" + | Lean -> "core.slice.index.Range.get_unchecked"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked_mut" + | Lean -> "core.slice.index.Range.get_unchecked_mut"); + }; + ] ); ] let mk_builtin_funs_map () = @@ -528,7 +701,7 @@ let builtin_trait_decls_info () = [ (match !backend with | Coq | FStar | HOL4 -> "index_inst" - | Lean -> "IndexInst"); + | Lean -> "indexInst"); ]; consts = []; types = []; @@ -547,6 +720,104 @@ let builtin_trait_decls_info () = ] ); ]; }; + { + (* Sealed *) + rust_name = "core::slice::index::private_slice_index::Sealed"; + extract_name = + (match !backend with + | Coq | FStar | HOL4 -> "core_slice_index_sealed" + | Lean -> "core.slice.index.private_slice_index.Sealed"); + parent_clauses = []; + consts = []; + types = []; + funs = []; + }; + { + (* SliceIndex *) + rust_name = "core::slice::index::SliceIndex"; + extract_name = + (match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex" + | Lean -> "core.slice.index.SliceIndex"); + parent_clauses = + [ + (match !backend with + | Coq | FStar | HOL4 -> "sealed_inst" + | Lean -> "sealedInst"); + ]; + consts = []; + types = + [ + ( "Output", + ( (match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_Output" + | Lean -> "Output"), + [] ) ); + ]; + funs = + [ + ( "get", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get" + | Lean -> "get" ); + (* The backward function shouldn't be used *) + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_back" + | Lean -> "get_back" ); + ] ); + ( "get_mut", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut" + | Lean -> "get_mut" ); + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut_back" + | Lean -> "get_mut_back" ); + ] ); + ( "get_unchecked", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked" + | Lean -> "get_unchecked" ); + ] ); + ( "get_unchecked_mut", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked_mut" + | Lean -> "get_unchecked_mut" ); + ] ); + ( "index", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_index" + | Lean -> "index" ); + (* The backward function shouldn't be used *) + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_index_back" + | Lean -> "index_back" ); + ] ); + ( "index_mut", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut" + | Lean -> "index_mut" ); + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut_back" + | Lean -> "index_mut_back" ); + ] ); + ]; + }; ] let mk_builtin_trait_decls_map () = @@ -577,6 +848,7 @@ end module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd) let builtin_trait_impls_info () : ((string list * string list) * string) list = + (* TODO: fix the names like "[T]" below *) [ (* core::ops::Deref<alloc::boxed::Box<T>> *) ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]), @@ -584,6 +856,28 @@ let builtin_trait_impls_info () : ((string list * string list) * string) list = (* core::ops::DerefMut<alloc::boxed::Box<T>> *) ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]), "alloc.boxed.Box.coreOpsDerefMutInst" ); + (* core::ops::index::Index<[T], I> *) + ( ([ "core"; "slice"; "index"; "[T]" ], [ "core"; "ops"; "index"; "Index" ]), + "core.slice.index.Slice.coreopsindexIndexInst" ); + (* core::slice::index::private_slice_index::Sealed<Range<usize>> *) + ( ( [ "core"; "slice"; "index"; "private_slice_index"; "Range" ], + [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ), + "core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst" + ); + (* core::slice::index::SliceIndex<Range<usize>, [T]> *) + ( ( [ "core"; "slice"; "index"; "Range" ], + [ "core"; "slice"; "index"; "SliceIndex" ] ), + "core.slice.index.Range.coresliceindexSliceIndexInst" ); + (* core::ops::index::IndexMut<[T], I> *) + ( ( [ "core"; "slice"; "index"; "[T]" ], + [ "core"; "ops"; "index"; "IndexMut" ] ), + "core.slice.index.Slice.coreopsindexIndexMutInst" ); + (* core::ops::index::Index<[T; N], I> *) + ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "Index" ]), + "core.array.Array.coreopsindexIndexInst" ); + (* core::ops::index::IndexMut<[T; N], I> *) + ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "IndexMut" ]), + "core.array.Array.coreopsindexIndexMutInst" ); ] let mk_builtin_trait_impls_map () = diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 2553127a..0ab4ed94 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -13,14 +13,14 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : | Regular id -> (FunDeclId.Map.find id fun_decls).name | Assumed aid -> Assumed.get_assumed_fun_name aid -(** Return the opaque declarations found in the crate. +(** Return the opaque declarations found in the crate, which are also *not builtin*. [filter_assumed]: if [true], do not consider as opaque the external definitions that we will map to definitions from the standard library. Remark: the list of functions also contains the list of opaque global bodies. *) -let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : +let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : T.type_decl list * fun_decl list = let open ExtractBuiltin in let is_opaque_fun (d : fun_decl) : bool = @@ -30,14 +30,21 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitMethodDecl _ -> false | _ -> true) && ((not filter_assumed) - || not (SimpleNameMap.mem sname builtin_globals_map)) + || (not (SimpleNameMap.mem sname builtin_globals_map)) + && not (SimpleNameMap.mem sname (builtin_funs_map ()))) + in + let is_opaque_type (d : T.type_decl) : bool = + let sname = name_to_simple_name d.name in + d.kind = T.Opaque + && ((not filter_assumed) + || not (SimpleNameMap.mem sname (builtin_types_map ()))) in - let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in (* Note that by checking the function bodies we also the globals *) ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types), List.filter is_opaque_fun (FunDeclId.Map.values k.functions) ) (** Return true if the crate contains opaque declarations, ignoring the assumed definitions. *) -let crate_has_opaque_decls (k : crate) (filter_assumed : bool) : bool = - crate_get_opaque_decls k filter_assumed <> ([], []) +let crate_has_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : + bool = + crate_get_opaque_non_builtin_decls k filter_assumed <> ([], []) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 35dff9e6..019a5c35 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -390,10 +390,10 @@ type gen_config = { [filter_assumed]: if [true], do not consider as opaque the external definitions that we will map to definitions from the standard library. *) -let crate_has_opaque_decls (ctx : gen_ctx) (filter_assumed : bool) : bool * bool - = +let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) : + bool * bool = let types, funs = - LlbcAstUtils.crate_get_opaque_decls ctx.crate filter_assumed + LlbcAstUtils.crate_get_opaque_non_builtin_decls ctx.crate filter_assumed in log#ldebug (lazy @@ -1257,7 +1257,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* Check if there are opaque types and functions - in which case we need * to split *) - let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx true in + let has_opaque_types, has_opaque_funs = + crate_has_opaque_non_builtin_decls ctx true + in let has_opaque_types = has_opaque_types || !Config.use_state in (* Extract the types *) |