summaryrefslogtreecommitdiff
path: root/src/Assumed.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Assumed.ml258
1 files changed, 210 insertions, 48 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml
index 9664fbc4..97cd2c78 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -33,51 +33,199 @@ module T = Types
module A = CfimAst
open TypesUtils
-(** `T -> Box<T>` *)
-let box_new_sig : A.fun_sig =
- let tvar_id_0 = T.TypeVarId.of_int 0 in
- let tvar_0 = T.TypeVar tvar_id_0 in
- {
- region_params = [];
- num_early_bound_regions = 0;
- regions_hierarchy = [];
- type_params = [ { index = tvar_id_0; name = "T" } ];
- inputs = [ tvar_0 (* T *) ];
- output = mk_box_ty tvar_0 (* Box<T> *);
- }
-
-(** Helper for `Box::deref_shared` and `Box::deref_mut`.
- Returns:
- `&'a (mut) Box<T> -> &'a (mut) T`
- *)
-let box_deref_sig (is_mut : bool) : A.fun_sig =
- let rvar_id_0 = T.RegionVarId.of_int 0 in
- let rvar_0 = T.Var rvar_id_0 in
- let rg_id_0 = T.RegionGroupId.of_int 0 in
- let tvar_id_0 = T.TypeVarId.of_int 0 in
- let tvar_0 = T.TypeVar tvar_id_0 in
- let ref_kind = if is_mut then T.Mut else T.Shared in
- (* The signature fields *)
- let region_params = [ { T.index = rvar_id_0; name = Some "'a" } ] in
- let regions_hierarchy =
- [ { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } ]
- (* <'a> *)
- in
- {
- region_params;
- num_early_bound_regions = 0;
- regions_hierarchy;
- type_params = [ { index = tvar_id_0; name = "T" } ] (* <T> *);
- inputs =
- [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) ref_kind (* &'a (mut) Box<T> *) ];
- output = mk_ref_ty rvar_0 tvar_0 ref_kind (* &'a (mut) T *);
- }
-
-(** `&'a Box<T> -> &'a T` *)
-let box_deref_shared_sig = box_deref_sig false
-
-(** `&'a mut Box<T> -> &'a mut T` *)
-let box_deref_mut_sig = box_deref_sig true
+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
+
+ (** Region 'a of id 0 *)
+ let region_param_0 : T.region_var = { T.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 = [] }
+
+ (** Type parameter `T` of id 0 *)
+ let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" }
+
+ 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
+ mk_ref_ty r ty ref_kind
+
+ (** `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 *) ]
+ in
+ let output = tvar_0 (* T *) in
+ {
+ region_params;
+ num_early_bound_regions = 0;
+ regions_hierarchy;
+ type_params;
+ 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> *);
+ inputs = [ tvar_0 (* T *) ];
+ output = mk_box_ty tvar_0 (* Box<T> *);
+ }
+
+ (** 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> *);
+ 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;
+ 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 output = mk_unit_ty (* () *) in
+ {
+ region_params;
+ num_early_bound_regions = 0;
+ regions_hierarchy;
+ type_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;
+ 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;
+ 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;
+ 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
+end
(** The list of assumed functions, and their signatures.
@@ -85,14 +233,28 @@ let box_deref_mut_sig = box_deref_sig true
*)
let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list =
[
- (BoxNew, box_new_sig);
- (BoxDeref, box_deref_shared_sig);
- (BoxDerefMut, box_deref_mut_sig);
+ (Replace, Sig.mem_replace_sig);
+ (BoxNew, Sig.box_new_sig);
+ (BoxDeref, Sig.box_deref_shared_sig);
+ (BoxDerefMut, Sig.box_deref_mut_sig);
+ (VecNew, Sig.vec_new_sig);
+ (VecPush, Sig.vec_push_sig);
+ (VecInsert, Sig.vec_insert_sig);
+ (VecLen, Sig.vec_len_sig);
+ (VecIndex, Sig.vec_index_shared_sig);
+ (VecIndexMut, Sig.vec_index_mut_sig);
]
let assumed_names : (A.assumed_fun_id * Identifiers.name) list =
[
+ (Replace, [ "core"; "mem"; "replace" ]);
(BoxNew, [ "alloc"; "boxed"; "Box"; "new" ]);
(BoxDeref, [ "core"; "ops"; "deref"; "Deref"; "deref" ]);
(BoxDerefMut, [ "core"; "ops"; "deref"; "DerefMut"; "deref_mut" ]);
+ (VecNew, [ "alloc"; "vec"; "Vec"; "new" ]);
+ (VecPush, [ "alloc"; "vec"; "Vec"; "push" ]);
+ (VecInsert, [ "alloc"; "vec"; "Vec"; "insert" ]);
+ (VecLen, [ "alloc"; "vec"; "Vec"; "len" ]);
+ (VecIndex, [ "core"; "ops"; "index"; "Index"; "index" ]);
+ (VecIndexMut, [ "core"; "ops"; "index"; "IndexMut"; "index_mut" ]);
]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 19:34:59 +0000