summaryrefslogtreecommitdiff
path: root/compiler/Assumed.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Assumed.ml')
-rw-r--r--compiler/Assumed.ml447
1 files changed, 129 insertions, 318 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 11cd5666..1807add5 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -29,234 +29,83 @@
]}
*)
-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 = RegionVarId.of_int 0
+ let rvar_0 : region = RBVar (0, 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_var_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;
+ is_closure = false;
+ closure_info = None;
+ 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 +121,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 +142,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 +224,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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 17:23:48 +0000