diff options
author | Son Ho | 2023-11-29 14:26:04 +0100 |
---|---|---|
committer | Son Ho | 2023-11-29 14:26:04 +0100 |
commit | 0273fee7f6b74da1d3b66c3c6a2158c012d04197 (patch) | |
tree | 5f6db32814f6f0b3a98f2de1db39225ff2c7645d /compiler/Assumed.ml | |
parent | f4e2c2bb09d9d7b54afc0692b7f690f5ec2eb029 (diff) | |
parent | 90e42e0e1c1889aabfa66283fb15b43a5852a02a (diff) |
Merge branch 'main' into afromher_shifts
Diffstat (limited to '')
-rw-r--r-- | compiler/Assumed.ml | 445 |
1 files changed, 127 insertions, 318 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 11cd5666..48b7ee2b 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -29,234 +29,81 @@ ]} *) -open Names +open Types open TypesUtils -module T = Types -module A = LlbcAst +open LlbcAst module Sig = struct (** A few utilities *) - let rvar_id_0 = T.RegionVarId.of_int 0 - let rvar_0 : T.RegionVarId.id T.region = T.Var rvar_id_0 - let rg_id_0 = T.RegionGroupId.of_int 0 - let tvar_id_0 = T.TypeVarId.of_int 0 - let tvar_0 : T.sty = T.TypeVar tvar_id_0 - let cgvar_id_0 = T.ConstGenericVarId.of_int 0 - let cgvar_0 : T.const_generic = T.ConstGenericVar cgvar_id_0 + let rvar_id_0 = RegionId.of_int 0 + let rvar_0 : region = RVar rvar_id_0 + let rg_id_0 = RegionGroupId.of_int 0 + let tvar_id_0 = TypeVarId.of_int 0 + let tvar_0 : ty = TVar tvar_id_0 + let cgvar_id_0 = ConstGenericVarId.of_int 0 + let cgvar_0 : const_generic = CgVar cgvar_id_0 (** Region 'a of id 0 *) - let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" } + let region_param_0 : region_var = { index = rvar_id_0; name = Some "'a" } (** Region group: [{ parent={}; regions:{'a of id 0} }] *) - let region_group_0 : T.region_var_group = - { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } + let region_group_0 : region_group = + { id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } (** Type parameter [T] of id 0 *) - let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" } + let type_param_0 : type_var = { index = tvar_id_0; name = "T" } - let usize_ty : T.sty = T.Literal (Integer Usize) + let usize_ty : ty = TLiteral (TInteger Usize) (** Const generic parameter [const N : usize] of id 0 *) - let cg_param_0 : T.const_generic_var = - { T.index = cgvar_id_0; name = "N"; ty = Integer Usize } + let cg_param_0 : const_generic_var = + { index = cgvar_id_0; name = "N"; ty = TInteger Usize } - let empty_const_generic_params : T.const_generic_var list = [] + let empty_const_generic_params : const_generic_var list = [] - let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) : - T.sty = - let ref_kind = if is_mut then T.Mut else T.Shared in + let mk_generic_args regions types const_generics : generic_args = + { regions; types; const_generics; trait_refs = [] } + + let mk_generic_params regions types const_generics : generic_params = + { regions; types; const_generics; trait_clauses = [] } + + let mk_ref_ty (r : region) (ty : ty) (is_mut : bool) : ty = + let ref_kind = if is_mut then RMut else RShared in mk_ref_ty r ty ref_kind - let mk_array_ty (ty : T.sty) (cg : T.const_generic) : T.sty = - Adt (Assumed Array, [], [ ty ], [ cg ]) + let mk_array_ty (ty : ty) (cg : const_generic) : ty = + TAdt (TAssumed TArray, mk_generic_args [] [ ty ] [ cg ]) - let mk_slice_ty (ty : T.sty) : T.sty = Adt (Assumed Slice, [], [ ty ], []) - let range_ty : T.sty = Adt (Assumed Range, [], [ usize_ty ], []) + let mk_slice_ty (ty : ty) : ty = + TAdt (TAssumed TSlice, mk_generic_args [] [ ty ] []) - (** [fn<T>(&'a mut T, T) -> T] *) - let mem_replace_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] (* <'a> *) in - let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in - let type_params = [ type_param_0 ] (* <T> *) in - let inputs = - [ mk_ref_ty rvar_0 tvar_0 true (* &'a mut T *); tvar_0 (* T *) ] + let mk_sig generics inputs output : fun_sig = + let preds : predicates = + { regions_outlive = []; types_outlive = []; trait_type_constraints = [] } in - let output = tvar_0 (* T *) in { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; + is_unsafe = false; + generics; + preds; + parent_params_info = None; inputs; output; } (** [fn<T>(T) -> Box<T>] *) - let box_new_sig : A.fun_sig = - { - region_params = []; - num_early_bound_regions = 0; - regions_hierarchy = []; - type_params = [ type_param_0 ] (* <T> *); - const_generic_params = empty_const_generic_params; - inputs = [ tvar_0 (* T *) ]; - output = mk_box_ty tvar_0 (* Box<T> *); - } + let box_new_sig : fun_sig = + let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in + let inputs = [ tvar_0 (* T *) ] in + let output = mk_box_ty tvar_0 (* Box<T> *) in + mk_sig generics inputs output (** [fn<T>(Box<T>) -> ()] *) - let box_free_sig : A.fun_sig = - { - region_params = []; - num_early_bound_regions = 0; - regions_hierarchy = []; - type_params = [ type_param_0 ] (* <T> *); - const_generic_params = empty_const_generic_params; - inputs = [ mk_box_ty tvar_0 (* Box<T> *) ]; - output = mk_unit_ty (* () *); - } - - (** Helper for [Box::deref_shared] and [Box::deref_mut]. - Returns: - [fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T] - *) - let box_deref_gen_sig (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params = [ type_param_0 ] (* <T> *); - const_generic_params = empty_const_generic_params; - inputs = - [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ]; - output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *); - } - - (** [fn<'a, T>(&'a Box<T>) -> &'a T] *) - let box_deref_shared_sig = box_deref_gen_sig false - - (** [fn<'a, T>(&'a mut Box<T>) -> &'a mut T] *) - let box_deref_mut_sig = box_deref_gen_sig true - - (** [fn<T>() -> Vec<T>] *) - let vec_new_sig : A.fun_sig = - let region_params = [] in - let regions_hierarchy = [] in - let type_params = [ type_param_0 ] (* <T> *) in - let inputs = [] in - let output = mk_vec_ty tvar_0 (* Vec<T> *) in - { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } - - (** [fn<T>(&'a mut Vec<T>, T)] *) - let vec_push_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in - let inputs = - [ - mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *); - tvar_0 (* T *); - ] - in + let box_free_sig : fun_sig = + let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in + let inputs = [ mk_box_ty tvar_0 (* Box<T> *) ] in let output = mk_unit_ty (* () *) in - { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } - - (** [fn<T>(&'a mut Vec<T>, usize, T)] *) - let vec_insert_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in - let inputs = - [ - mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *); - mk_usize_ty (* usize *); - tvar_0 (* T *); - ] - in - let output = mk_unit_ty (* () *) in - { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } - - (** [fn<T>(&'a Vec<T>) -> usize] *) - let vec_len_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in - let inputs = - [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) false (* &'a Vec<T> *) ] - in - let output = mk_usize_ty (* usize *) in - { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } - - (** Helper: - [fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T] - *) - let vec_index_gen_sig (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in - let inputs = - [ - mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec<T> *); - mk_usize_ty (* usize *); - ] - in - let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in - { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } - - (** [fn<T>(&'a Vec<T>, usize) -> &'a T] *) - let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false - - (** [fn<T>(&'a mut Vec<T>, usize) -> &'a mut T] *) - let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true + mk_sig generics inputs output (** Array/slice functions *) @@ -272,13 +119,12 @@ module Sig = struct The [mut_borrow] boolean controls whether we use a shared or a mutable borrow. *) - let mk_array_slice_borrow_sig (cgs : T.const_generic_var list) - (input_ty : T.TypeVarId.id -> T.sty) (index_ty : T.sty option) - (output_ty : T.TypeVarId.id -> T.sty) (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in + let mk_array_slice_borrow_sig (cgs : const_generic_var list) + (input_ty : TypeVarId.id -> ty) (index_ty : ty option) + (output_ty : TypeVarId.id -> ty) (is_mut : bool) : fun_sig = + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *) + in let inputs = [ mk_ref_ty rvar_0 @@ -294,84 +140,76 @@ module Sig = struct (output_ty type_param_0.index) is_mut (* &'a (mut) output_ty<T> *) in - { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params; - const_generic_params = cgs; - inputs; - output; - } + mk_sig generics inputs output - let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig = + let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : fun_sig = (* Array<T, N> *) let input_ty id = - if is_array then mk_array_ty (T.TypeVar id) cgvar_0 - else mk_slice_ty (T.TypeVar id) + if is_array then mk_array_ty (TVar id) cgvar_0 else mk_slice_ty (TVar id) in (* usize *) let index_ty = usize_ty in (* T *) - let output_ty id = T.TypeVar id in + let output_ty id = TVar id in let cgs = if is_array then [ cg_param_0 ] else [] in mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut let array_index_sig (is_mut : bool) = mk_array_slice_index_sig true is_mut let slice_index_sig (is_mut : bool) = mk_array_slice_index_sig false is_mut - let array_to_slice_sig (is_mut : bool) : A.fun_sig = + let array_to_slice_sig (is_mut : bool) : fun_sig = (* Array<T, N> *) - let input_ty id = mk_array_ty (T.TypeVar id) cgvar_0 in + let input_ty id = mk_array_ty (TVar id) cgvar_0 in (* Slice<T> *) - let output_ty id = mk_slice_ty (T.TypeVar id) in + let output_ty id = mk_slice_ty (TVar id) in let cgs = [ cg_param_0 ] in mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut - let mk_array_slice_subslice_sig (is_array : bool) (is_mut : bool) : A.fun_sig - = - (* Array<T, N> *) - let input_ty id = - if is_array then mk_array_ty (T.TypeVar id) cgvar_0 - else mk_slice_ty (T.TypeVar id) + let array_repeat_sig = + let generics = + (* <T, N> *) + mk_generic_params [] [ type_param_0 ] [ cg_param_0 ] in - (* Range *) - let index_ty = range_ty in - (* Slice<T> *) - let output_ty id = mk_slice_ty (T.TypeVar id) in - let cgs = if is_array then [ cg_param_0 ] else [] in - mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut - - let array_subslice_sig (is_mut : bool) = - mk_array_slice_subslice_sig true is_mut - - let slice_subslice_sig (is_mut : bool) = - mk_array_slice_subslice_sig false is_mut + let inputs = [ tvar_0 (* T *) ] in + let output = + (* [T; N] *) + mk_array_ty tvar_0 cgvar_0 + in + mk_sig generics inputs output (** Helper: [fn<T>(&'a [T]) -> usize] *) - let slice_len_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in + let slice_len_sig : fun_sig = + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let inputs = [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ] in let output = mk_usize_ty (* usize *) in - { - region_params; - num_early_bound_regions = 0; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics inputs output end -type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name +type raw_assumed_fun_info = + assumed_fun_id * fun_sig * bool * string * bool list option + +type assumed_fun_info = { + fun_id : assumed_fun_id; + fun_sig : fun_sig; + can_fail : bool; + name : string; + keep_types : bool list option; + (** We may want to filter some type arguments. + + For instance, all the `Vec` functions (and the `Vec` type itself) take + an `Allocator` type as argument, that we ignore. + *) +} + +let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info = + let fun_id, fun_sig, can_fail, name, keep_types = raw in + { fun_id; fun_sig; can_fail; name; keep_types } (** The list of assumed functions and all their information: - their signature @@ -384,94 +222,65 @@ type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name a [usize], we have to make sure that vectors are bounded by the max usize. As a consequence, [Vec::push] is monadic. *) -let assumed_infos : assumed_info list = - let deref_pre = [ "core"; "ops"; "deref" ] in - let vec_pre = [ "alloc"; "vec"; "Vec" ] in - let index_pre = [ "core"; "ops"; "index" ] in +let raw_assumed_fun_infos : raw_assumed_fun_info list = [ - (A.Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]); - (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]); + (* TODO: the names are not correct ("Box" should be an impl elem for instance) + but it's not important) *) + ( BoxNew, + Sig.box_new_sig, + false, + "alloc::boxed::Box::new", + Some [ true; false ] ); + (* BoxFree shouldn't be used *) ( BoxFree, Sig.box_free_sig, false, - to_name [ "alloc"; "boxed"; "Box"; "free" ] ); - ( BoxDeref, - Sig.box_deref_shared_sig, - false, - to_name (deref_pre @ [ "Deref"; "deref" ]) ); - ( BoxDerefMut, - Sig.box_deref_mut_sig, - false, - to_name (deref_pre @ [ "DerefMut"; "deref_mut" ]) ); - (VecNew, Sig.vec_new_sig, false, to_name (vec_pre @ [ "new" ])); - (VecPush, Sig.vec_push_sig, true, to_name (vec_pre @ [ "push" ])); - (VecInsert, Sig.vec_insert_sig, true, to_name (vec_pre @ [ "insert" ])); - (VecLen, Sig.vec_len_sig, false, to_name (vec_pre @ [ "len" ])); - ( VecIndex, - Sig.vec_index_shared_sig, - true, - to_name (index_pre @ [ "Index"; "index" ]) ); - ( VecIndexMut, - Sig.vec_index_mut_sig, - true, - to_name (index_pre @ [ "IndexMut"; "index_mut" ]) ); + "alloc::boxed::Box::free", + Some [ true; false ] ); (* Array Index *) ( ArrayIndexShared, Sig.array_index_sig false, true, - to_name [ "@ArrayIndexShared" ] ); - (ArrayIndexMut, Sig.array_index_sig true, true, to_name [ "@ArrayIndexMut" ]); + "@ArrayIndexShared", + None ); + (ArrayIndexMut, Sig.array_index_sig true, true, "@ArrayIndexMut", None); (* Array to slice*) ( ArrayToSliceShared, Sig.array_to_slice_sig false, true, - to_name [ "@ArrayToSliceShared" ] ); + "@ArrayToSliceShared", + None ); ( ArrayToSliceMut, Sig.array_to_slice_sig true, true, - to_name [ "@ArrayToSliceMut" ] ); - (* Array Subslice *) - ( ArraySubsliceShared, - Sig.array_subslice_sig false, - true, - to_name [ "@ArraySubsliceShared" ] ); - ( ArraySubsliceMut, - Sig.array_subslice_sig true, - true, - to_name [ "@ArraySubsliceMut" ] ); + "@ArrayToSliceMut", + None ); + (* Array Repeat *) + (ArrayRepeat, Sig.array_repeat_sig, false, "@ArrayRepeat", None); (* Slice Index *) ( SliceIndexShared, Sig.slice_index_sig false, true, - to_name [ "@SliceIndexShared" ] ); - (SliceIndexMut, Sig.slice_index_sig true, true, to_name [ "@SliceIndexMut" ]); - (* Slice Subslice *) - ( SliceSubsliceShared, - Sig.slice_subslice_sig false, - true, - to_name [ "@SliceSubsliceShared" ] ); - ( SliceSubsliceMut, - Sig.slice_subslice_sig true, - true, - to_name [ "@SliceSubsliceMut" ] ); - (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]); + "@SliceIndexShared", + None ); + (SliceIndexMut, Sig.slice_index_sig true, true, "@SliceIndexMut", None); ] -let get_assumed_info (id : A.assumed_fun_id) : assumed_info = - match List.find_opt (fun (id', _, _, _) -> id = id') assumed_infos with +let assumed_fun_infos : assumed_fun_info list = + List.map mk_assumed_fun_info raw_assumed_fun_infos + +let get_assumed_fun_info (id : assumed_fun_id) : assumed_fun_info = + match List.find_opt (fun x -> id = x.fun_id) assumed_fun_infos with | Some info -> info | None -> raise - (Failure ("get_assumed_info: not found: " ^ A.show_assumed_fun_id id)) + (Failure ("get_assumed_fun_info: not found: " ^ show_assumed_fun_id id)) -let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig = - let _, sg, _, _ = get_assumed_info id in - sg +let get_assumed_fun_sig (id : assumed_fun_id) : fun_sig = + (get_assumed_fun_info id).fun_sig -let get_assumed_name (id : A.assumed_fun_id) : fun_name = - let _, _, _, name = get_assumed_info id in - name +let get_assumed_fun_name (id : assumed_fun_id) : string = + (get_assumed_fun_info id).name -let assumed_can_fail (id : A.assumed_fun_id) : bool = - let _, _, b, _ = get_assumed_info id in - b +let assumed_fun_can_fail (id : assumed_fun_id) : bool = + (get_assumed_fun_info id).can_fail |