summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Assumed.ml254
-rw-r--r--compiler/Extract.ml145
-rw-r--r--compiler/ExtractAssumed.ml61
-rw-r--r--compiler/ExtractBase.ml73
-rw-r--r--compiler/ExtractBuiltin.ml468
-rw-r--r--compiler/FunsAnalysis.ml2
-rw-r--r--compiler/InterpreterExpansion.ml15
-rw-r--r--compiler/InterpreterExpressions.ml100
-rw-r--r--compiler/InterpreterPaths.ml31
-rw-r--r--compiler/InterpreterPaths.mli4
-rw-r--r--compiler/InterpreterStatements.ml100
-rw-r--r--compiler/Invariants.ml15
-rw-r--r--compiler/LlbcAstUtils.ml8
-rw-r--r--compiler/PrePasses.ml2
-rw-r--r--compiler/Print.ml11
-rw-r--r--compiler/PrintPure.ml57
-rw-r--r--compiler/Pure.ml12
-rw-r--r--compiler/PureMicroPasses.ml42
-rw-r--r--compiler/PureTypeCheck.ml13
-rw-r--r--compiler/Substitute.ml14
-rw-r--r--compiler/SymbolicToPure.ml31
-rw-r--r--compiler/Translate.ml107
-rw-r--r--compiler/TypesAnalysis.ml4
-rw-r--r--compiler/dune2
24 files changed, 763 insertions, 808 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index b1ec0660..94fb7a72 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -80,8 +80,6 @@ module Sig = struct
let mk_slice_ty (ty : T.sty) : T.sty =
Adt (Assumed Slice, mk_generic_args [] [ ty ] [])
- let range_ty : T.sty = Adt (Assumed Range, mk_generic_args [] [ usize_ty ] [])
-
let mk_sig generics regions_hierarchy inputs output : A.fun_sig =
let preds : T.predicates =
{ regions_outlive = []; types_outlive = []; trait_type_constraints = [] }
@@ -95,19 +93,6 @@ module Sig = struct
output;
}
- (** [fn<T>(&'a mut T, T) -> T] *)
- let mem_replace_sig : A.fun_sig =
- (* The signature fields *)
- let regions = [ region_param_0 ] (* <'a> *) in
- let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in
- let types = [ type_param_0 ] (* <T> *) in
- let generics = mk_generic_params regions types [] in
- let inputs =
- [ mk_ref_ty rvar_0 tvar_0 true (* &'a mut T *); tvar_0 (* T *) ]
- in
- let output = tvar_0 (* T *) in
- mk_sig generics regions_hierarchy inputs output
-
(** [fn<T>(T) -> Box<T>] *)
let box_new_sig : A.fun_sig =
let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
@@ -124,101 +109,6 @@ module Sig = struct
let output = mk_unit_ty (* () *) in
mk_sig generics regions_hierarchy inputs output
- (** 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 =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
- let inputs =
- [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ]
- in
- let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
- mk_sig generics regions_hierarchy inputs output
-
- (** [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 generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
- let regions_hierarchy = [] in
- let inputs = [] in
- let output = mk_vec_ty tvar_0 (* Vec<T> *) in
- mk_sig generics regions_hierarchy inputs output
-
- (** [fn<T>(&'a mut Vec<T>, T)] *)
- let vec_push_sig : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) 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
- mk_sig generics regions_hierarchy inputs output
-
- (** [fn<T>(&'a mut Vec<T>, usize, T)] *)
- let vec_insert_sig : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) 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
- mk_sig generics regions_hierarchy inputs output
-
- (** [fn<T>(&'a Vec<T>) -> usize] *)
- let vec_len_sig : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) 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
- mk_sig generics regions_hierarchy inputs output
-
- (** Helper:
- [fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T]
- *)
- let vec_index_gen_sig (is_mut : bool) : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) 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
- mk_sig generics regions_hierarchy 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
-
(** Array/slice functions *)
(** Small helper.
@@ -281,23 +171,6 @@ module Sig = struct
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)
- 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 array_repeat_sig =
let generics =
(* <T, N> *)
@@ -311,9 +184,6 @@ module Sig = struct
in
mk_sig generics regions_hierarchy inputs output
- let slice_subslice_sig (is_mut : bool) =
- mk_array_slice_subslice_sig false is_mut
-
(** Helper:
[fn<T>(&'a [T]) -> usize]
*)
@@ -329,7 +199,25 @@ module Sig = struct
mk_sig generics regions_hierarchy inputs output
end
-type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
+type raw_assumed_fun_info =
+ A.assumed_fun_id * A.fun_sig * bool * name * bool list option
+
+type assumed_fun_info = {
+ fun_id : A.assumed_fun_id;
+ fun_sig : A.fun_sig;
+ can_fail : bool;
+ name : name;
+ 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
@@ -342,96 +230,72 @@ 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 =
[
- (Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]);
- (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]);
+ ( BoxNew,
+ Sig.box_new_sig,
+ false,
+ to_name [ "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" ]) );
+ to_name [ "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" ]);
+ to_name [ "@ArrayIndexShared" ],
+ None );
+ ( ArrayIndexMut,
+ Sig.array_index_sig true,
+ true,
+ to_name [ "@ArrayIndexMut" ],
+ None );
(* Array to slice*)
( ArrayToSliceShared,
Sig.array_to_slice_sig false,
true,
- to_name [ "@ArrayToSliceShared" ] );
+ to_name [ "@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" ] );
+ to_name [ "@ArrayToSliceMut" ],
+ None );
(* Array Repeat *)
- (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ]);
+ (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@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,
+ to_name [ "@SliceIndexShared" ],
+ None );
+ ( SliceIndexMut,
+ Sig.slice_index_sig true,
true,
- to_name [ "@SliceSubsliceShared" ] );
- ( SliceSubsliceMut,
- Sig.slice_subslice_sig true,
- true,
- to_name [ "@SliceSubsliceMut" ] );
- (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]);
+ to_name [ "@SliceIndexMut" ],
+ None );
+ (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ], 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 : A.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: " ^ A.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 : A.assumed_fun_id) : A.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 : A.assumed_fun_id) : fun_name =
+ (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 : A.assumed_fun_id) : bool =
+ (get_assumed_fun_info id).can_fail
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 688f6ce3..30c4c27d 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -225,12 +225,9 @@ let assumed_adts () : (assumed_ty * string) list =
(Result, "Result");
(Error, "Error");
(Fuel, "Nat");
- (Option, "Option");
- (Vec, "Vec");
(Array, "Array");
(Slice, "Slice");
(Str, "Str");
- (Range, "Range");
]
| Coq | FStar ->
[
@@ -238,12 +235,9 @@ let assumed_adts () : (assumed_ty * string) list =
(Result, "result");
(Error, "error");
(Fuel, "nat");
- (Option, "option");
- (Vec, "vec");
(Array, "array");
(Slice, "slice");
(Str, "str");
- (Range, "range");
]
| HOL4 ->
[
@@ -251,20 +245,17 @@ let assumed_adts () : (assumed_ty * string) list =
(Result, "result");
(Error, "error");
(Fuel, "num");
- (Option, "option");
- (Vec, "vec");
(Array, "array");
(Slice, "slice");
(Str, "str");
- (Range, "range");
]
let assumed_struct_constructors () : (assumed_ty * string) list =
match !backend with
- | Lean -> [ (Range, "Range.mk"); (Array, "Array.make") ]
- | Coq -> [ (Range, "mk_range"); (Array, "mk_array") ]
- | FStar -> [ (Range, "Mkrange"); (Array, "mk_array") ]
- | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ]
+ | Lean -> [ (Array, "Array.make") ]
+ | Coq -> [ (Array, "mk_array") ]
+ | FStar -> [ (Array, "mk_array") ]
+ | HOL4 -> [ (Array, "mk_array") ]
let assumed_variants () : (assumed_ty * VariantId.id * string) list =
match !backend with
@@ -276,8 +267,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_out_of_fuel_id, "OutOfFuel");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
- (Option, option_some_id, "Some");
- (Option, option_none_id, "None");
]
| Coq ->
[
@@ -287,8 +276,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_out_of_fuel_id, "OutOfFuel");
(Fuel, fuel_zero_id, "O");
(Fuel, fuel_succ_id, "S");
- (Option, option_some_id, "Some");
- (Option, option_none_id, "None");
]
| Lean ->
[
@@ -297,8 +284,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_failure_id, "panic");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
- (Option, option_some_id, "some");
- (Option, option_none_id, "none");
]
| HOL4 ->
[
@@ -307,8 +292,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_failure_id, "Failure");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
- (Option, option_some_id, "SOME");
- (Option, option_none_id, "NONE");
]
let assumed_llbc_functions () :
@@ -317,66 +300,30 @@ let assumed_llbc_functions () :
match !backend with
| FStar | Coq | HOL4 ->
[
- (Replace, None, "mem_replace_fwd");
- (Replace, rg0, "mem_replace_back");
- (VecNew, None, "vec_new");
- (VecPush, None, "vec_push_fwd") (* Shouldn't be used *);
- (VecPush, rg0, "vec_push_back");
- (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *);
- (VecInsert, rg0, "vec_insert_back");
- (VecLen, None, "vec_len");
- (VecIndex, None, "vec_index_fwd");
- (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
- (VecIndexMut, None, "vec_index_mut_fwd");
- (VecIndexMut, rg0, "vec_index_mut_back");
(ArrayIndexShared, None, "array_index_shared");
(ArrayIndexMut, None, "array_index_mut_fwd");
(ArrayIndexMut, rg0, "array_index_mut_back");
(ArrayToSliceShared, None, "array_to_slice_shared");
(ArrayToSliceMut, None, "array_to_slice_mut_fwd");
(ArrayToSliceMut, rg0, "array_to_slice_mut_back");
- (ArraySubsliceShared, None, "array_subslice_shared");
- (ArraySubsliceMut, None, "array_subslice_mut_fwd");
- (ArraySubsliceMut, rg0, "array_subslice_mut_back");
(ArrayRepeat, None, "array_repeat");
(SliceIndexShared, None, "slice_index_shared");
(SliceIndexMut, None, "slice_index_mut_fwd");
(SliceIndexMut, rg0, "slice_index_mut_back");
- (SliceSubsliceShared, None, "slice_subslice_shared");
- (SliceSubsliceMut, None, "slice_subslice_mut_fwd");
- (SliceSubsliceMut, rg0, "slice_subslice_mut_back");
(SliceLen, None, "slice_len");
]
| Lean ->
[
- (Replace, None, "mem.replace");
- (Replace, rg0, "mem.replace_back");
- (VecNew, None, "Vec.new");
- (VecPush, None, "Vec.push_fwd") (* Shouldn't be used *);
- (VecPush, rg0, "Vec.push");
- (VecInsert, None, "Vec.insert_fwd") (* Shouldn't be used *);
- (VecInsert, rg0, "Vec.insert");
- (VecLen, None, "Vec.len");
- (VecIndex, None, "Vec.index_shared");
- (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *);
- (VecIndexMut, None, "Vec.index_mut");
- (VecIndexMut, rg0, "Vec.index_mut_back");
(ArrayIndexShared, None, "Array.index_shared");
(ArrayIndexMut, None, "Array.index_mut");
(ArrayIndexMut, rg0, "Array.index_mut_back");
(ArrayToSliceShared, None, "Array.to_slice_shared");
(ArrayToSliceMut, None, "Array.to_slice_mut");
(ArrayToSliceMut, rg0, "Array.to_slice_mut_back");
- (ArraySubsliceShared, None, "Array.subslice_shared");
- (ArraySubsliceMut, None, "Array.subslice_mut");
- (ArraySubsliceMut, rg0, "Array.subslice_mut_back");
(ArrayRepeat, None, "Array.repeat");
(SliceIndexShared, None, "Slice.index_shared");
(SliceIndexMut, None, "Slice.index_mut");
(SliceIndexMut, rg0, "Slice.index_mut_back");
- (SliceSubsliceShared, None, "Slice.subslice_shared");
- (SliceSubsliceMut, None, "Slice.subslice_mut");
- (SliceSubsliceMut, rg0, "Slice.subslice_mut_back");
(SliceLen, None, "Slice.len");
]
@@ -850,12 +797,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
| Assumed Result -> "r"
| Assumed Error -> ConstStrings.error_basename
| Assumed Fuel -> ConstStrings.fuel_basename
- | Assumed Option -> "opt"
- | Assumed Vec -> "v"
| Assumed Array -> "a"
| Assumed Slice -> "s"
| Assumed Str -> "s"
- | Assumed Range -> "r"
| Assumed State -> ConstStrings.state_basename
| AdtId adt_id ->
let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
@@ -1397,8 +1341,18 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
extraction_ctx =
+ (* Lookup the builtin information, if there is *)
+ let open ExtractBuiltin in
+ let sname = name_to_simple_name def.name in
+ let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in
(* Compute and register the type def name *)
- let ctx = ctx_add_type_decl def ctx in
+ let def_name =
+ match info with
+ | None -> ctx.fmt.type_name def.name
+ | Some info -> info.rust_name
+ in
+ let is_opaque = def.kind = Opaque in
+ let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in
(* Compute and register:
* - the variant names, if this is an enumeration
* - the field names, if this is a structure
@@ -1406,18 +1360,73 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
let ctx =
match def.kind with
| Struct fields ->
+ (* Compute the names *)
+ let field_names, cons_name =
+ match info with
+ | None ->
+ let field_names =
+ FieldId.mapi
+ (fun fid (field : field) ->
+ (fid, ctx.fmt.field_name def.name fid field.field_name))
+ fields
+ in
+ let cons_name = ctx.fmt.struct_constructor def.name in
+ (field_names, cons_name)
+ | Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
+ let field_names =
+ FieldId.mapi
+ (fun fid (_, name) -> (fid, name))
+ (List.combine fields field_names)
+ in
+ (field_names, cons_name)
+ | _ -> raise (Failure "Invalid builtin information")
+ in
(* Add the fields *)
let ctx =
- fst
- (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
+ List.fold_left
+ (fun ctx (fid, name) ->
+ ctx_add is_opaque (FieldId (AdtId def.def_id, fid)) name ctx)
+ ctx field_names
in
(* Add the constructor name *)
- fst (ctx_add_struct def ctx)
+ ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx
| Enum variants ->
- fst
- (ctx_add_variants def
- (VariantId.mapi (fun id v -> (id, v)) variants)
- ctx)
+ let variant_names =
+ match info with
+ | None ->
+ VariantId.mapi
+ (fun variant_id (variant : variant) ->
+ let name =
+ ctx.fmt.variant_name def.name variant.variant_name
+ in
+ (* Add the type name prefix for Lean *)
+ let name =
+ if !Config.backend = Lean then
+ let type_name = ctx.fmt.type_name def.name in
+ type_name ^ "." ^ name
+ else name
+ in
+ (variant_id, name))
+ variants
+ | Some { body_info = Some (Enum variant_infos); _ } ->
+ (* We need to compute the map from variant to variant *)
+ let variant_map =
+ StringMap.of_list
+ (List.map
+ (fun (info : builtin_enum_variant_info) ->
+ (info.rust_variant_name, info.extract_variant_name))
+ variant_infos)
+ in
+ VariantId.mapi
+ (fun variant_id (variant : variant) ->
+ (variant_id, StringMap.find variant.variant_name variant_map))
+ variants
+ | _ -> raise (Failure "Invalid builtin information")
+ in
+ List.fold_left
+ (fun ctx (vid, vname) ->
+ ctx_add is_opaque (VariantId (AdtId def.def_id, vid)) vname ctx)
+ ctx variant_names
| Opaque ->
(* Nothing to do *)
ctx
diff --git a/compiler/ExtractAssumed.ml b/compiler/ExtractAssumed.ml
deleted file mode 100644
index 7f094b24..00000000
--- a/compiler/ExtractAssumed.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-(** This file declares external identifiers that we catch to map them to
- definitions coming from the standard libraries in our backends. *)
-
-open Names
-
-type simple_name = string list [@@deriving show, ord]
-
-let name_to_simple_name (s : name) : simple_name =
- (* We simply ignore the disambiguators *)
- List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s
-
-(** Small helper which cuts a string at the occurrences of "::" *)
-let string_to_simple_name (s : string) : simple_name =
- (* No function to split by using string separator?? *)
- let name = String.split_on_char ':' s in
- List.filter (fun s -> s <> "") name
-
-module SimpleNameOrd = struct
- type t = simple_name
-
- let compare = compare_simple_name
- let to_string = show_simple_name
- let pp_t = pp_simple_name
- let show_t = show_simple_name
-end
-
-module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
-
-let assumed_globals : (string * string) list =
- [
- (* Min *)
- ("core::num::usize::MIN", "core_usize_min");
- ("core::num::u8::MIN", "core_u8_min");
- ("core::num::u16::MIN", "core_u16_min");
- ("core::num::u32::MIN", "core_u32_min");
- ("core::num::u64::MIN", "core_u64_min");
- ("core::num::u128::MIN", "core_u128_min");
- ("core::num::isize::MIN", "core_isize_min");
- ("core::num::i8::MIN", "core_i8_min");
- ("core::num::i16::MIN", "core_i16_min");
- ("core::num::i32::MIN", "core_i32_min");
- ("core::num::i64::MIN", "core_i64_min");
- ("core::num::i128::MIN", "core_i128_min");
- (* Max *)
- ("core::num::usize::MAX", "core_usize_max");
- ("core::num::u8::MAX", "core_u8_max");
- ("core::num::u16::MAX", "core_u16_max");
- ("core::num::u32::MAX", "core_u32_max");
- ("core::num::u64::MAX", "core_u64_max");
- ("core::num::u128::MAX", "core_u128_max");
- ("core::num::isize::MAX", "core_isize_max");
- ("core::num::i8::MAX", "core_i8_max");
- ("core::num::i16::MAX", "core_i16_max");
- ("core::num::i32::MAX", "core_i32_max");
- ("core::num::i64::MAX", "core_i64_max");
- ("core::num::i128::MAX", "core_i128_max");
- ]
-
-let assumed_globals_map : string SimpleNameMap.t =
- SimpleNameMap.of_list
- (List.map (fun (x, y) -> (string_to_simple_name x, y)) assumed_globals)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index a921515b..54f69735 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -5,7 +5,7 @@ open TranslateCore
module C = Contexts
module RegionVarId = T.RegionVarId
module F = Format
-open ExtractAssumed
+open ExtractBuiltin
(** The local logger *)
let log = L.pure_to_extract_log
@@ -803,15 +803,11 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
if variant_id = error_failure_id then "@error::Failure"
else if variant_id = error_out_of_fuel_id then "@error::OutOfFuel"
else raise (Failure "Unreachable")
- | Assumed Option ->
- if variant_id = option_some_id then "@option::Some"
- else if variant_id = option_none_id then "@option::None"
- else raise (Failure "Unreachable")
| Assumed Fuel ->
if variant_id = fuel_zero_id then "@fuel::0"
else if variant_id = fuel_succ_id then "@fuel::Succ"
else raise (Failure "Unreachable")
- | Assumed (State | Vec | Array | Slice | Str | Range) ->
+ | Assumed (State | Array | Slice | Str) ->
raise
(Failure
("Unreachable: variant id ("
@@ -830,9 +826,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
let field_name =
match id with
| Tuple -> raise (Failure "Unreachable")
- | Assumed
- ( State | Result | Error | Fuel | Option | Vec | Array | Slice | Str
- | Range ) ->
+ | Assumed (State | Result | Error | Fuel | Array | Slice | Str) ->
(* We can't directly have access to the fields of those types *)
raise (Failure "Unreachable")
| AdtId id -> (
@@ -1186,65 +1180,6 @@ let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
let ctx, tcs = ctx_add_local_trait_clauses trait_clauses ctx in
(ctx, tys, cgs, tcs)
-let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) :
- extraction_ctx * string =
- assert (match def.kind with Struct _ -> true | _ -> false);
- let is_opaque = false in
- let cons_name = ctx.fmt.struct_constructor def.name in
- let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx in
- (ctx, cons_name)
-
-let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx
- =
- let is_opaque = def.kind = Opaque in
- let def_name = ctx.fmt.type_name def.name in
- let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in
- ctx
-
-let ctx_add_field (def : type_decl) (field_id : FieldId.id) (field : field)
- (ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
- let name = ctx.fmt.field_name def.name field_id field.field_name in
- let ctx = ctx_add is_opaque (FieldId (AdtId def.def_id, field_id)) name ctx in
- (ctx, name)
-
-let ctx_add_fields (def : type_decl) (fields : (FieldId.id * field) list)
- (ctx : extraction_ctx) : extraction_ctx * string list =
- List.fold_left_map
- (fun ctx (vid, v) -> ctx_add_field def vid v ctx)
- ctx fields
-
-let ctx_add_variant (def : type_decl) (variant_id : VariantId.id)
- (variant : variant) (ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
- let name = ctx.fmt.variant_name def.name variant.variant_name in
- (* Add the type name prefix for Lean *)
- let name =
- if !Config.backend = Lean then
- let type_name = ctx.fmt.type_name def.name in
- type_name ^ "." ^ name
- else name
- in
- let ctx =
- ctx_add is_opaque (VariantId (AdtId def.def_id, variant_id)) name ctx
- in
- (ctx, name)
-
-let ctx_add_variants (def : type_decl)
- (variants : (VariantId.id * variant) list) (ctx : extraction_ctx) :
- extraction_ctx * string list =
- List.fold_left_map
- (fun ctx (vid, v) -> ctx_add_variant def vid v ctx)
- ctx variants
-
-let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
- extraction_ctx * string =
- assert (match def.kind with Struct _ -> true | _ -> false);
- let is_opaque = false in
- let name = ctx.fmt.struct_constructor def.name in
- let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) name ctx in
- (ctx, name)
-
let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
let is_opaque = false in
@@ -1277,7 +1212,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
to a custom definition in our standard library (for instance, happens
with "core::num::usize::MAX") *)
let sname = name_to_simple_name def.name in
- match SimpleNameMap.find_opt sname assumed_globals_map with
+ match SimpleNameMap.find_opt sname builtin_globals_map with
| Some name ->
(* Yes: register the custom binding *)
ctx_add is_opaque decl name ctx
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
new file mode 100644
index 00000000..cf5cc70d
--- /dev/null
+++ b/compiler/ExtractBuiltin.ml
@@ -0,0 +1,468 @@
+(** This file declares external identifiers that we catch to map them to
+ definitions coming from the standard libraries in our backends. *)
+
+open Names
+open Config
+
+type simple_name = string list [@@deriving show, ord]
+
+let name_to_simple_name (s : name) : simple_name =
+ (* We simply ignore the disambiguators *)
+ List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s
+
+(** Small helper which cuts a string at the occurrences of "::" *)
+let string_to_simple_name (s : string) : simple_name =
+ (* No function to split by using string separator?? *)
+ let name = String.split_on_char ':' s in
+ List.filter (fun s -> s <> "") name
+
+module SimpleNameOrd = struct
+ type t = simple_name
+
+ let compare = compare_simple_name
+ let to_string = show_simple_name
+ let pp_t = pp_simple_name
+ let show_t = show_simple_name
+end
+
+module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
+
+(** Small utility to memoize some computations *)
+let mk_memoized (f : unit -> 'a) : unit -> 'a =
+ let r = ref None in
+ let g () =
+ match !r with
+ | Some x -> x
+ | None ->
+ let x = f () in
+ r := Some x;
+ x
+ in
+ g
+
+let builtin_globals : (string * string) list =
+ [
+ (* Min *)
+ ("core::num::usize::MIN", "core_usize_min");
+ ("core::num::u8::MIN", "core_u8_min");
+ ("core::num::u16::MIN", "core_u16_min");
+ ("core::num::u32::MIN", "core_u32_min");
+ ("core::num::u64::MIN", "core_u64_min");
+ ("core::num::u128::MIN", "core_u128_min");
+ ("core::num::isize::MIN", "core_isize_min");
+ ("core::num::i8::MIN", "core_i8_min");
+ ("core::num::i16::MIN", "core_i16_min");
+ ("core::num::i32::MIN", "core_i32_min");
+ ("core::num::i64::MIN", "core_i64_min");
+ ("core::num::i128::MIN", "core_i128_min");
+ (* Max *)
+ ("core::num::usize::MAX", "core_usize_max");
+ ("core::num::u8::MAX", "core_u8_max");
+ ("core::num::u16::MAX", "core_u16_max");
+ ("core::num::u32::MAX", "core_u32_max");
+ ("core::num::u64::MAX", "core_u64_max");
+ ("core::num::u128::MAX", "core_u128_max");
+ ("core::num::isize::MAX", "core_isize_max");
+ ("core::num::i8::MAX", "core_i8_max");
+ ("core::num::i16::MAX", "core_i16_max");
+ ("core::num::i32::MAX", "core_i32_max");
+ ("core::num::i64::MAX", "core_i64_max");
+ ("core::num::i128::MAX", "core_i128_max");
+ ]
+
+let builtin_globals_map : string SimpleNameMap.t =
+ SimpleNameMap.of_list
+ (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals)
+
+type builtin_variant_info = { fields : (string * string) list }
+
+type builtin_enum_variant_info = {
+ rust_variant_name : string;
+ extract_variant_name : string;
+ fields : string list option;
+}
+
+type builtin_type_body_info =
+ | Struct of string * string list
+ (* The constructor name and the map for the field names *)
+ | Enum of builtin_enum_variant_info list
+(* For every variant, a map for the field names *)
+
+type builtin_type_info = {
+ rust_name : string;
+ extract_name : string;
+ keep_params : bool list option;
+ (** We might want to filter some of the type parameters.
+
+ For instance, `Vec` type takes a type parameter for the allocator,
+ which we want to ignore.
+ *)
+ body_info : builtin_type_body_info option;
+}
+
+(** The assumed types.
+
+ The optional list of booleans is filtering information for the type
+ parameters. For instance, in the case of the `Vec` functions, there is
+ a type parameter for the allocator to use, which we want to filter.
+ *)
+let builtin_types () : builtin_type_info list =
+ [
+ (* Alloc *)
+ {
+ rust_name = "alloc::alloc::Global";
+ extract_name =
+ (match !backend with
+ | Lean -> "AllocGlobal"
+ | Coq | FStar | HOL4 -> "alloc_global");
+ keep_params = None;
+ body_info = None;
+ };
+ (* Vec *)
+ {
+ rust_name = "alloc::vec::Vec";
+ extract_name =
+ (match !backend with Lean -> "Vec" | Coq | FStar | HOL4 -> "vec");
+ keep_params = Some [ true; false ];
+ body_info = None;
+ };
+ (* Option *)
+ {
+ rust_name = "core::option::Option";
+ extract_name =
+ (match !backend with
+ | Lean -> "Option"
+ | Coq | FStar | HOL4 -> "option");
+ keep_params = None;
+ body_info =
+ Some
+ (Enum
+ [
+ {
+ rust_variant_name = "None";
+ extract_variant_name =
+ (match !backend with
+ | FStar | Coq -> "None"
+ | Lean -> "none"
+ | HOL4 -> "NONE");
+ fields = None;
+ };
+ {
+ rust_variant_name = "Some";
+ extract_variant_name =
+ (match !backend with
+ | FStar | Coq -> "Some"
+ | Lean -> "some"
+ | HOL4 -> "SOME");
+ fields = None;
+ };
+ ]);
+ };
+ (* Range *)
+ {
+ rust_name = "core::ops::range::Range";
+ extract_name =
+ (match !backend with Lean -> "Range" | Coq | FStar | HOL4 -> "range");
+ keep_params = None;
+ body_info =
+ Some
+ (Struct
+ ( (match !backend with
+ | Lean -> "Range.mk"
+ | Coq | HOL4 -> "mk_range"
+ | FStar -> "Mkrange"),
+ [ "start"; "end_" ] ));
+ };
+ ]
+
+let mk_builtin_types_map () =
+ SimpleNameMap.of_list
+ (List.map
+ (fun info -> (string_to_simple_name info.rust_name, info))
+ (builtin_types ()))
+
+let builtin_types_map = mk_memoized mk_builtin_types_map
+
+type builtin_fun_info = {
+ rg : Types.RegionGroupId.id option;
+ extract_name : string;
+}
+
+(** The assumed functions.
+
+ The optional list of booleans is filtering information for the type
+ parameters. For instance, in the case of the `Vec` functions, there is
+ a type parameter for the allocator to use, which we want to filter.
+ *)
+let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
+ let rg0 = Some Types.RegionGroupId.zero in
+ [
+ ( "core::mem::replace",
+ None,
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "mem_replace_fwd"
+ | Lean -> "mem.replace");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "mem_replace_back"
+ | Lean -> "mem.replace_back");
+ };
+ ] );
+ ( "alloc::vec::Vec::new",
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_new"
+ | Lean -> "Vec.new");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_new_back"
+ | Lean -> "Vec.new_back");
+ };
+ ] );
+ ( "alloc::vec::Vec::push",
+ Some [ true; false ],
+ [
+ (* The forward function shouldn't be used *)
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_push_fwd"
+ | Lean -> "Vec.push_fwd");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_push_back"
+ | Lean -> "Vec.push");
+ };
+ ] );
+ ( "alloc::vec::Vec::insert",
+ Some [ true; false ],
+ [
+ (* The forward function shouldn't be used *)
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_insert_fwd"
+ | Lean -> "Vec.insert_fwd");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_insert_back"
+ | Lean -> "Vec.insert");
+ };
+ ] );
+ ( "alloc::vec::Vec::len",
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_len"
+ | Lean -> "Vec.len");
+ };
+ ] );
+ ( "alloc::vec::Vec::index",
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_index_fwd"
+ | Lean -> "Vec.index_shared");
+ };
+ (* The backward function shouldn't be used *)
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_index_back"
+ | Lean -> "Vec.index_shared_back");
+ };
+ ] );
+ ( "alloc::vec::Vec::index_mut",
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_index_mut_fwd"
+ | Lean -> "Vec.index_mut");
+ };
+ (* The backward function shouldn't be used *)
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_index_mut_back"
+ | Lean -> "Vec.index_mut_back");
+ };
+ ] );
+ ]
+
+let mk_builtin_funs_map () =
+ SimpleNameMap.of_list
+ (List.map
+ (fun (name, filter, info) ->
+ (string_to_simple_name name, (filter, info)))
+ (builtin_funs ()))
+
+let builtin_funs_map () = mk_memoized mk_builtin_funs_map
+
+type builtin_trait_info = {
+ rust_name : string;
+ extract_name : string;
+ parent_clauses : string list;
+ consts : (string * string) list;
+ types : (string * string * string list) list;
+ (** Every type has:
+ - a Rust name
+ - an extraction name
+ - a list of clauses *)
+ funs : (string * Types.RegionGroupId.id option * string) list;
+}
+
+let builtin_traits () =
+ let rg0 = Some Types.RegionGroupId.zero in
+ [
+ {
+ (* Deref *)
+ rust_name = "core::ops::deref::Deref";
+ extract_name =
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_Deref"
+ | Lean -> "core.ops.deref.Deref");
+ parent_clauses = [];
+ consts = [];
+ types =
+ [
+ ( "Target",
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_Deref_Target"
+ | Lean -> "Target"),
+ [] );
+ ];
+ funs =
+ [
+ ( "deref",
+ None,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_Deref_deref"
+ | Lean -> "deref" );
+ ];
+ };
+ {
+ (* DerefMut *)
+ rust_name = "core::ops::deref::DerefMut";
+ extract_name =
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut"
+ | Lean -> "core.ops.deref.DerefMut");
+ parent_clauses =
+ [
+ (match !backend with
+ | Coq | FStar | HOL4 -> "deref_inst"
+ | Lean -> "DerefInst");
+ ];
+ consts = [];
+ types = [];
+ funs =
+ [
+ ( "deref_mut",
+ None,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut"
+ | Lean -> "deref_mut" );
+ ( "deref_mut",
+ rg0,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut_back"
+ | Lean -> "deref_mut_back" );
+ ];
+ };
+ {
+ (* Index *)
+ rust_name = "core::ops::index::Index";
+ extract_name =
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_Index"
+ | Lean -> "core.ops.index.Index");
+ parent_clauses = [];
+ consts = [];
+ types =
+ [
+ ( "Output",
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_Index_Output"
+ | Lean -> "Output"),
+ [] );
+ ];
+ funs =
+ [
+ ( "index",
+ None,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_Index_index"
+ | Lean -> "index" );
+ ];
+ };
+ {
+ (* IndexMut *)
+ rust_name = "core::ops::index::IndexMut";
+ extract_name =
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_IndexMut"
+ | Lean -> "core.ops.index.IndexMut");
+ parent_clauses =
+ [
+ (match !backend with
+ | Coq | FStar | HOL4 -> "index_inst"
+ | Lean -> "IndexInst");
+ ];
+ consts = [];
+ types = [];
+ funs =
+ [
+ ( "index_mut",
+ None,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut"
+ | Lean -> "index_mut" );
+ ( "index_mut",
+ rg0,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back"
+ | Lean -> "index_mut_back" );
+ ];
+ };
+ ]
+
+let mk_builtin_traits_map () =
+ SimpleNameMap.of_list
+ (List.map
+ (fun info -> (string_to_simple_name info.rust_name, info))
+ (builtin_traits ()))
+
+let builtin_traits_map () = mk_memoized mk_builtin_traits_map
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index a09a6d05..5e849ba7 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -88,7 +88,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
can_diverge := !can_diverge || info.can_diverge
| FunId (Assumed id) ->
(* None of the assumed functions can diverge nor are considered stateful *)
- can_fail := !can_fail || Assumed.assumed_can_fail id
+ can_fail := !can_fail || Assumed.assumed_fun_can_fail id
| TraitMethod _ ->
(* We consider trait functions can fail, diverge, and are not stateful *)
can_fail := true;
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index c1041fa3..167e3d58 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -241,17 +241,6 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
(* Initialize all the expanded values of all the variants *)
List.map initialize variants_fields_types
-(** Compute the expansion of an Option value.
- *)
-let compute_expanded_symbolic_option_value (expand_enumerations : bool)
- (kind : V.sv_kind) (ty : T.rty) : V.symbolic_expansion list =
- assert expand_enumerations;
- let some_se =
- V.SeAdt (Some T.option_some_id, [ mk_fresh_symbolic_value kind ty ])
- in
- let none_se = V.SeAdt (Some T.option_none_id, []) in
- [ none_se; some_se ]
-
let compute_expanded_symbolic_tuple_value (kind : V.sv_kind)
(field_types : T.rty list) : V.symbolic_expansion =
(* Generate the field values *)
@@ -286,8 +275,6 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
def_id generics ctx
| T.Tuple, [], _ ->
[ compute_expanded_symbolic_tuple_value kind generics.types ]
- | T.Assumed T.Option, [], [ ty ] ->
- compute_expanded_symbolic_option_value expand_enumerations kind ty
| T.Assumed T.Box, [], [ boxed_ty ] ->
[ compute_expanded_symbolic_box_value kind boxed_ty ]
| _ ->
@@ -704,7 +691,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
| T.Adt ((Tuple | Assumed Box), _) | T.Ref (_, _, _) ->
(* Ok *)
expand_symbolic_value_no_branching config sv None
- | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _) ->
+ | T.Adt (Assumed (Array | Slice | Str), _) ->
(* We can't expand those *)
raise
(Failure
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index a42c552a..341e97eb 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -142,10 +142,10 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
| V.Adt av ->
(* Sanity check *)
(match v.V.ty with
- | T.Adt (T.Assumed (T.Box | Vec), _) ->
+ | T.Adt (T.Assumed T.Box, _) ->
raise (Failure "Can't copy an assumed value other than Option")
| T.Adt (T.AdtId _, _) -> assert allow_adt_copy
- | T.Adt ((T.Assumed Option | T.Tuple), _) -> () (* Ok *)
+ | T.Adt (T.Tuple, _) -> () (* Ok *)
| T.Adt
( T.Assumed (Slice | T.Array),
{
@@ -722,70 +722,38 @@ let eval_rvalue_aggregate (config : C.config)
fun ctx ->
(* Match on the aggregate kind *)
match aggregate_kind with
- | E.AggregatedTuple ->
- let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
- let v = V.Adt { variant_id = None; field_values = values } in
- let generics = TypesUtils.mk_generic_args [] tys [] [] in
- let ty = T.Adt (T.Tuple, generics) in
- let aggregated : V.typed_value = { V.value = v; ty } in
- (* Call the continuation *)
- cf aggregated ctx
- | E.AggregatedOption (variant_id, ty) ->
- (* Sanity check *)
- if variant_id = T.option_none_id then assert (values = [])
- else if variant_id = T.option_some_id then
- assert (List.length values = 1)
- else raise (Failure "Unreachable");
- (* Construt the value *)
- let generics = TypesUtils.mk_generic_args [] [ ty ] [] [] in
- let aty = T.Adt (T.Assumed T.Option, generics) in
- let av : V.adt_value =
- { V.variant_id = Some variant_id; V.field_values = values }
- in
- let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
- (* Call the continuation *)
- cf aggregated ctx
- | E.AggregatedAdt (def_id, opt_variant_id, generics) ->
- (* Sanity checks *)
- let type_decl = C.ctx_lookup_type_decl ctx def_id in
- assert (
- List.length type_decl.generics.regions = List.length generics.regions);
- let expected_field_types =
- Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
- generics
- in
- assert (
- expected_field_types
- = List.map (fun (v : V.typed_value) -> v.V.ty) values);
- (* Construct the value *)
- let av : V.adt_value =
- { V.variant_id = opt_variant_id; V.field_values = values }
- in
- let aty = T.Adt (T.AdtId def_id, generics) in
- let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
- (* Call the continuation *)
- cf aggregated ctx
- | E.AggregatedRange ety ->
- (* There should be two fields exactly *)
- let v0, v1 =
- match values with
- | [ v0; v1 ] -> (v0, v1)
- | _ -> raise (Failure "Unreachable")
- in
- (* Ranges are parametric over the type of indices. For now we only
- support scalars, which can be of any type *)
- assert (literal_type_is_integer (ty_as_literal ety));
- assert (v0.ty = ety);
- assert (v1.ty = ety);
- (* Construct the value *)
- let av : V.adt_value =
- { V.variant_id = None; V.field_values = values }
- in
- let generics = TypesUtils.mk_generic_args_from_types [ ety ] in
- let aty = T.Adt (T.Assumed T.Range, generics) in
- let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
- (* Call the continuation *)
- cf aggregated ctx
+ | E.AggregatedAdt (type_id, opt_variant_id, generics) -> (
+ match type_id with
+ | Tuple ->
+ let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
+ let v = V.Adt { variant_id = None; field_values = values } in
+ let generics = TypesUtils.mk_generic_args [] tys [] [] in
+ let ty = T.Adt (T.Tuple, generics) in
+ let aggregated : V.typed_value = { V.value = v; ty } in
+ (* Call the continuation *)
+ cf aggregated ctx
+ | AdtId def_id ->
+ (* Sanity checks *)
+ let type_decl = C.ctx_lookup_type_decl ctx def_id in
+ assert (
+ List.length type_decl.generics.regions
+ = List.length generics.regions);
+ let expected_field_types =
+ Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
+ generics
+ in
+ assert (
+ expected_field_types
+ = List.map (fun (v : V.typed_value) -> v.V.ty) values);
+ (* Construct the value *)
+ let av : V.adt_value =
+ { V.variant_id = opt_variant_id; V.field_values = values }
+ in
+ let aty = T.Adt (T.AdtId def_id, generics) in
+ let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
+ (* Call the continuation *)
+ cf aggregated ctx
+ | Assumed _ -> raise (Failure "Unreachable"))
| E.AggregatedArray (ety, cg) -> (
(* Sanity check: all the values have the proper type *)
assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values);
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 465d0028..2a277c91 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -96,7 +96,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
| pe :: p' -> (
(* Match on the projection element and the value *)
match (pe, v.V.value, v.V.ty) with
- | ( Field (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id),
+ | ( Field ((ProjAdt (_, _) as proj_kind), field_id),
V.Adt adt,
T.Adt (type_id, _) ) -> (
(* Check consistency *)
@@ -104,8 +104,6 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
| ProjAdt (def_id, opt_variant_id), T.AdtId def_id' ->
assert (def_id = def_id');
assert (opt_variant_id = adt.variant_id)
- | ProjOption variant_id, T.Assumed T.Option ->
- assert (Some variant_id = adt.variant_id)
| _ -> raise (Failure "Unreachable"));
(* Actually project *)
let fv = T.FieldId.nth adt.field_values field_id in
@@ -136,7 +134,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
Ok (ctx, { res with updated })
(* If we reach Bottom, it may mean we need to expand an uninitialized
* enumeration value *))
- | Field ((ProjAdt (_, _) | ProjTuple _ | ProjOption _), _), V.Bottom, _ ->
+ | Field ((ProjAdt (_, _) | ProjTuple _), _), V.Bottom, _ ->
Error (FailBottom (1 + List.length p', pe, v.ty))
(* Symbolic value: needs to be expanded *)
| _, Symbolic sp, _ ->
@@ -376,20 +374,6 @@ let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
let ty = T.Adt (T.AdtId def_id, generics) in
{ V.value = av; V.ty }
-let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
- (param_ty : T.ety) : V.typed_value =
- (* Note that the variant can be [Some] or [None]: we expand bottom values
- * when writing to fields or setting discriminants *)
- let field_values =
- if variant_id = T.option_some_id then [ mk_bottom param_ty ]
- else if variant_id = T.option_none_id then []
- else raise (Failure "Unreachable")
- in
- let av = V.Adt { variant_id = Some variant_id; field_values } in
- let generics = TypesUtils.mk_generic_args [] [ param_ty ] [] [] in
- let ty = T.Adt (T.Assumed T.Option, generics) in
- { V.value = av; ty }
-
let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
V.typed_value =
(* Generate the field values *)
@@ -451,17 +435,6 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
T.Adt (T.AdtId def_id', generics) ) ->
assert (def_id = def_id');
compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
- (* Option *)
- | ( Field (ProjOption variant_id, _),
- T.Adt
- ( T.Assumed T.Option,
- {
- T.regions = [];
- types = [ ty ];
- const_generics = [];
- trait_refs = [];
- } ) ) ->
- compute_expanded_bottom_option_value variant_id ty
(* Tuples *)
| ( Field (ProjTuple arity, _),
T.Adt
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 041b0a97..0ff8063f 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -63,10 +63,6 @@ val compute_expanded_bottom_adt_value :
T.egeneric_args ->
V.typed_value
-(** Compute an expanded [Option] ⊥ value *)
-val compute_expanded_bottom_option_value :
- T.VariantId.id -> T.ety -> V.typed_value
-
(** Drop (end) outer loans at a given place, which should be seen as an l-value
(we will write to it later, but need to drop the loans before writing).
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 9f35c6f2..2aced79f 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -10,7 +10,6 @@ open TypesUtils
open ValuesUtils
module Inv = Invariants
module S = SynthesizeSymbolic
-open Utils
open Cps
open InterpreterUtils
open InterpreterProjectors
@@ -233,8 +232,7 @@ let set_discriminant (config : C.config) (p : E.place)
let update_value cf (v : V.typed_value) : m_fun =
fun ctx ->
match (v.V.ty, v.V.value) with
- | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Adt av
- -> (
+ | T.Adt ((T.AdtId _ as type_id), generics), V.Adt av -> (
(* There are two situations:
- either the discriminant is already the proper one (in which case we
don't do anything)
@@ -253,24 +251,15 @@ let set_discriminant (config : C.config) (p : E.place)
| T.AdtId def_id ->
compute_expanded_bottom_adt_value ctx def_id
(Some variant_id) generics
- | T.Assumed T.Option ->
- assert (generics.regions = []);
- compute_expanded_bottom_option_value variant_id
- (Collections.List.to_cons_nil generics.types)
| _ -> raise (Failure "Unreachable")
in
assign_to_place config bottom_v p (cf Unit) ctx)
- | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Bottom
- ->
+ | T.Adt ((T.AdtId _ as type_id), generics), V.Bottom ->
let bottom_v =
match type_id with
| T.AdtId def_id ->
compute_expanded_bottom_adt_value ctx def_id (Some variant_id)
generics
- | T.Assumed T.Option ->
- assert (generics.regions = []);
- compute_expanded_bottom_option_value variant_id
- (Collections.List.to_cons_nil generics.types)
| _ -> raise (Failure "Unreachable")
in
assign_to_place config bottom_v p (cf Unit) ctx
@@ -313,7 +302,7 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id)
mk_unit_ty
| _ ->
(* Retrieve the function's signature *)
- let sg = Assumed.get_assumed_sig fid in
+ let sg = Assumed.get_assumed_fun_sig fid in
(* Instantiate the return type *)
(* There shouldn't be any reference to Self *)
let tr_self : T.erased_region T.trait_instance_id =
@@ -427,11 +416,6 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
comp cf_pop cf_assign
(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) :
- cm_fun =
- fun _cf _ctx -> raise Unimplemented
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
cm_fun =
fun cf ctx ->
@@ -475,67 +459,6 @@ let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
comp cf_move cf_create cf ctx
| _ -> raise (Failure "Inconsistent state")
-(** Auxiliary function which factorizes code to evaluate [std::Deref::deref]
- and [std::DerefMut::deref_mut] - see {!eval_assumed_function_call} *)
-let eval_box_deref_mut_or_shared_concrete (config : C.config)
- (generics : T.egeneric_args) (is_mut : bool) : cm_fun =
- fun cf ctx ->
- (* Check the arguments *)
- match
- (generics.regions, generics.types, generics.const_generics, ctx.env)
- with
- | ( [],
- [ boxed_ty ],
- [],
- Var (VarBinder input_var, input_value)
- :: Var (_ret_var, _)
- :: C.Frame :: _ ) ->
- (* Required type checking. We must have:
- - input_value.ty = & (mut) Box<ty>
- - boxed_ty = ty
- for some ty
- *)
- (let _, input_ty, ref_kind = ty_get_ref input_value.V.ty in
- assert (match ref_kind with T.Shared -> not is_mut | T.Mut -> is_mut);
- let input_ty = ty_get_box input_ty in
- assert (input_ty = boxed_ty));
-
- (* Borrow the boxed value *)
- let p =
- { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] }
- in
- let borrow_kind = if is_mut then E.Mut else E.Shared in
- let rv = E.RvRef (p, borrow_kind) in
- let cf_borrow = eval_rvalue_not_global config rv in
-
- (* Move the borrow to its destination *)
- let cf_move cf res : m_fun =
- match res with
- | Error EPanic ->
- (* We can't get there by borrowing a value *)
- raise (Failure "Unreachable")
- | Ok borrowed_value ->
- (* Move and continue *)
- let destp = mk_place_from_var_id E.VarId.zero in
- assign_to_place config borrowed_value destp cf
- in
-
- (* Compose and apply *)
- comp cf_borrow cf_move cf ctx
- | _ -> raise (Failure "Inconsistent state")
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) :
- cm_fun =
- let is_mut = false in
- eval_box_deref_mut_or_shared_concrete config generics is_mut
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args)
- : cm_fun =
- let is_mut = true in
- eval_box_deref_mut_or_shared_concrete config generics is_mut
-
(** Auxiliary function - see {!eval_assumed_function_call}.
[Box::free] is not handled the same way as the other assumed functions:
@@ -575,11 +498,6 @@ let eval_box_free (config : C.config) (generics : T.egeneric_args)
cc cf ctx
| _ -> raise (Failure "Inconsistent state")
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
- (_generics : T.egeneric_args) : cm_fun =
- fun _cf _ctx -> raise Unimplemented
-
(** Evaluate a non-local function call in concrete mode *)
let eval_assumed_function_call_concrete (config : C.config)
(fid : A.assumed_fun_id) (call : A.call) : cm_fun =
@@ -636,18 +554,12 @@ let eval_assumed_function_call_concrete (config : C.config)
* access to a body. *)
let cf_eval_body : cm_fun =
match fid with
- | Replace -> eval_replace_concrete config generics
| BoxNew -> eval_box_new_concrete config generics
- | BoxDeref -> eval_box_deref_concrete config generics
- | BoxDerefMut -> eval_box_deref_mut_concrete config generics
| BoxFree ->
(* Should have been treated above *) raise (Failure "Unreachable")
- | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
- eval_vec_function_concrete config fid generics
| ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
- | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
- | ArrayRepeat | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
- | SliceSubsliceMut | SliceLen ->
+ | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut
+ | SliceLen ->
raise (Failure "Unimplemented")
in
@@ -1531,7 +1443,7 @@ and eval_assumed_function_call_symbolic (config : C.config)
(* There shouldn't be any reference to Self *)
let tr_self = T.UnknownTrait __FUNCTION__ in
instantiate_fun_sig ctx generics tr_self
- (Assumed.get_assumed_sig fid)
+ (Assumed.get_assumed_fun_sig fid)
in
(* Evaluate the function call *)
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 9ac5ce13..5c8ec7af 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -447,7 +447,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
fields_with_types
(* Assumed type case *)
| V.Adt av, T.Adt (T.Assumed aty_id, generics) -> (
- assert (av.V.variant_id = None || aty_id = T.Option);
+ assert (av.V.variant_id = None);
match
( aty_id,
av.V.field_values,
@@ -456,19 +456,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
generics.const_generics )
with
(* Box *)
- | T.Box, [ inner_value ], [], [ inner_ty ], []
- | T.Option, [ inner_value ], [], [ inner_ty ], [] ->
+ | T.Box, [ inner_value ], [], [ inner_ty ], [] ->
assert (inner_value.V.ty = inner_ty)
- | T.Option, _, [], [ _ ], [] ->
- (* Option::None: nothing to check *)
- ()
- | T.Vec, fvs, [], [ vec_ty ], [] ->
- List.iter
- (fun (v : V.typed_value) -> assert (v.ty = vec_ty))
- fvs
- | T.Range, [ v0; v1 ], [], [ inner_ty ], [] ->
- assert (v0.V.ty = inner_ty);
- assert (v1.V.ty = inner_ty)
| T.Array, inner_values, _, [ inner_ty ], [ cg ] ->
(* *)
assert (
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index a982af30..2553127a 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -5,13 +5,13 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
fun_sig =
match fun_id with
| Regular id -> (FunDeclId.Map.find id fun_decls).signature
- | Assumed aid -> Assumed.get_assumed_sig aid
+ | Assumed aid -> Assumed.get_assumed_fun_sig aid
let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
Names.fun_name =
match fun_id with
| Regular id -> (FunDeclId.Map.find id fun_decls).name
- | Assumed aid -> Assumed.get_assumed_name aid
+ | Assumed aid -> Assumed.get_assumed_fun_name aid
(** Return the opaque declarations found in the crate.
@@ -22,7 +22,7 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
*)
let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
T.type_decl list * fun_decl list =
- let open ExtractAssumed in
+ let open ExtractBuiltin in
let is_opaque_fun (d : fun_decl) : bool =
let sname = name_to_simple_name d.name in
d.body = None
@@ -30,7 +30,7 @@ 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 assumed_globals_map))
+ || not (SimpleNameMap.mem sname builtin_globals_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 *)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 1058fab0..ee06fa07 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -108,7 +108,7 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
| Assign (_, rv) -> (
match rv with
| Use _ | RvRef _ -> not must_end_with_exit
- | Aggregate (AggregatedTuple, []) -> not must_end_with_exit
+ | Aggregate (AggregatedAdt (Tuple, _, _), []) -> not must_end_with_exit
| _ -> false)
| FakeRead _ | Drop _ | Nop -> not must_end_with_exit
| Panic | Return -> true
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 1d5ddc50..aeacfbf0 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -127,17 +127,6 @@ module Values = struct
(* Assumed type *)
match (aty, field_values) with
| Box, [ bv ] -> "@Box(" ^ bv ^ ")"
- | Option, _ ->
- if av.variant_id = Some T.option_some_id then
- "@Option::Some("
- ^ Collections.List.to_cons_nil field_values
- ^ ")"
- else if av.variant_id = Some T.option_none_id then (
- assert (field_values = []);
- "@Option::None")
- else raise (Failure "Unreachable")
- | Range, _ -> "@Range{ " ^ String.concat ", " field_values ^ "}"
- | Vec, _ -> "@Vec[" ^ String.concat ", " field_values ^ "]"
| Array, _ ->
(* Happens when we aggregate values *)
"@Array[" ^ String.concat ", " field_values ^ "]"
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index be7b3cb4..6396fe96 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -195,12 +195,9 @@ let assumed_ty_to_string (aty : assumed_ty) : string =
| Result -> "Result"
| Error -> "Error"
| Fuel -> "Fuel"
- | Option -> "Option"
- | Vec -> "Vec"
| Array -> "Array"
| Slice -> "Slice"
| Str -> "Str"
- | Range -> "Range"
let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
match id with
@@ -354,10 +351,6 @@ let rec mprojection_to_string (fmt : ast_formatter) (inside : string)
| pe :: p' -> (
let s = mprojection_to_string fmt inside p' in
match pe.pkind with
- | E.ProjOption variant_id ->
- assert (variant_id = T.option_some_id);
- assert (pe.field_id = T.FieldId.zero);
- "(" ^ s ^ "as Option::Some)." ^ T.FieldId.to_string pe.field_id
| E.ProjTuple _ -> "(" ^ s ^ ")." ^ T.FieldId.to_string pe.field_id
| E.ProjAdt (adt_id, opt_variant_id) -> (
let field_name =
@@ -395,8 +388,6 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
| State | Array | Slice | Str ->
(* Those types are opaque: we can't get there *)
raise (Failure "Unreachable")
- | Vec -> "@Vec"
- | Range -> "@Range"
| Result ->
let variant_id = Option.get variant_id in
if variant_id = result_return_id then "@Result::Return"
@@ -412,13 +403,7 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then "@Fuel::Zero"
else if variant_id = fuel_succ_id then "@Fuel::Succ"
- else raise (Failure "Unreachable: improper variant id for fuel type")
- | Option ->
- let variant_id = Option.get variant_id in
- if variant_id = option_some_id then "@Option::Some "
- else if variant_id = option_none_id then "@Option::None"
- else
- raise (Failure "Unreachable: improper variant id for result type"))
+ else raise (Failure "Unreachable: improper variant id for fuel type"))
let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
(field_id : FieldId.id) : string =
@@ -435,11 +420,10 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
| Assumed aty -> (
(* Assumed type *)
match aty with
- | Range -> FieldId.to_string field_id
- | State | Fuel | Vec | Array | Slice | Str ->
+ | State | Fuel | Array | Slice | Str ->
(* Opaque types: we can't get there *)
raise (Failure "Unreachable")
- | Result | Error | Option ->
+ | Result | Error ->
(* Enumerations: we can't get there *)
raise (Failure "Unreachable"))
@@ -510,31 +494,13 @@ let adt_g_value_to_string (fmt : value_formatter)
| [ v ] -> "@Fuel::Succ " ^ v
| _ -> raise (Failure "@Fuel::Succ takes exactly one value")
else raise (Failure "Unreachable: improper variant id for fuel type")
- | Option ->
- let variant_id = Option.get variant_id in
- if variant_id = option_some_id then
- match field_values with
- | [ v ] -> "@Option::Some " ^ v
- | _ -> raise (Failure "Option::Some takes exactly one value")
- else if variant_id = option_none_id then (
- assert (field_values = []);
- "@Option::None")
- else
- raise (Failure "Unreachable: improper variant id for result type")
- | Vec | Array | Slice | Str ->
- assert (variant_id = None);
- let field_values =
- List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
- in
- let id = assumed_ty_to_string aty in
- id ^ " [" ^ String.concat "; " field_values ^ "]"
- | Range ->
+ | Array | Slice | Str ->
assert (variant_id = None);
let field_values =
List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
in
let id = assumed_ty_to_string aty in
- id ^ " {" ^ String.concat "; " field_values ^ "}")
+ id ^ " [" ^ String.concat "; " field_values ^ "]")
| _ ->
let fmt = value_to_type_formatter fmt in
raise
@@ -593,29 +559,16 @@ let fun_suffix (lp_id : LoopId.id option) (rg_id : T.RegionGroupId.id option) :
let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
match fid with
- | Replace -> "core::mem::replace"
| BoxNew -> "alloc::boxed::Box::new"
- | BoxDeref -> "core::ops::deref::Deref::deref"
- | BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut"
| BoxFree -> "alloc::alloc::box_free"
- | 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<alloc::vec::Vec>::index"
- | VecIndexMut -> "core::ops::index::IndexMut<alloc::vec::Vec>::index_mut"
| ArrayIndexShared -> "@ArrayIndexShared"
| ArrayIndexMut -> "@ArrayIndexMut"
| ArrayToSliceShared -> "@ArrayToSliceShared"
| ArrayToSliceMut -> "@ArrayToSliceMut"
- | ArraySubsliceShared -> "@ArraySubsliceShared"
- | ArraySubsliceMut -> "@ArraySubsliceMut"
| ArrayRepeat -> "@ArrayRepeat"
| SliceLen -> "@SliceLen"
| SliceIndexShared -> "@SliceIndexShared"
| SliceIndexMut -> "@SliceIndexMut"
- | SliceSubsliceShared -> "@SliceSubsliceShared"
- | SliceSubsliceMut -> "@SliceSubsliceMut"
let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string =
match fid with
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 47c7beb4..81e13af7 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -64,17 +64,7 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
this state is opaque to Aeneas (the user can define it, or leave it as
assumed)
*)
-type assumed_ty =
- | State
- | Result
- | Error
- | Fuel
- | Vec
- | Option
- | Array
- | Slice
- | Str
- | Range
+type assumed_ty = State | Result | Error | Fuel | Array | Slice | Str
[@@deriving show, ord]
(* TODO: we should never directly manipulate [Return] and [Fail], but rather
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b00509a6..a326d19e 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1513,7 +1513,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
function calls, and when translating end abstractions. Here, we can do
something simpler, in one micro-pass.
*)
-let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
+let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
(* The map visitor *)
let obj =
object
@@ -1522,30 +1522,42 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
method! visit_texpression env e =
match opt_destruct_function_call e with
| Some (fun_id, _tys, args) -> (
+ (* Below, when dealing with the arguments: we consider the very
+ * general case, where functions could be boxed (meaning we
+ * could have: [box_new f x])
+ * *)
match fun_id with
| Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> (
- (* Below, when dealing with the arguments: we consider the very
- * general case, where functions could be boxed (meaning we
- * could have: [box_new f x])
- * *)
match (aid, rg_id) with
| BoxNew, _ ->
assert (rg_id = None);
let arg, args = Collections.List.pop args in
mk_apps arg args
- | BoxDeref, None ->
+ | BoxFree, _ ->
+ assert (args = []);
+ mk_unit_rvalue
+ | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared
+ | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
+ | ArrayRepeat | SliceLen ),
+ _ ) ->
+ super#visit_texpression env e)
+ | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> (
+ (* Lookup the function name *)
+ let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
+ match (Names.name_to_string def.name, rg_id) with
+ | "alloc::box::Boxed::deref", None ->
(* [Box::deref] forward is the identity *)
let arg, args = Collections.List.pop args in
mk_apps arg args
- | BoxDeref, Some _ ->
+ | "alloc::box::Boxed::deref", Some _ ->
(* [Box::deref] backward is [()] (doesn't give back anything) *)
assert (args = []);
mk_unit_rvalue
- | BoxDerefMut, None ->
+ | "alloc::box::Boxed::deref_mut", None ->
(* [Box::deref_mut] forward is the identity *)
let arg, args = Collections.List.pop args in
mk_apps arg args
- | BoxDerefMut, Some _ ->
+ | "alloc::box::Boxed::deref_mut", Some _ ->
(* [Box::deref_mut] back is almost the identity:
* let box_deref_mut (x_init : t) (x_back : t) : t = x_back
* *)
@@ -1555,17 +1567,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
| _ -> raise (Failure "Unreachable")
in
mk_apps arg args
- | BoxFree, _ ->
- assert (args = []);
- mk_unit_rvalue
- | ( ( Replace | VecNew | VecPush | VecInsert | VecLen | VecIndex
- | VecIndexMut | ArraySubsliceShared | ArraySubsliceMut
- | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
- | SliceSubsliceMut | ArrayIndexShared | ArrayIndexMut
- | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat
- | SliceLen ),
- _ ) ->
- super#visit_texpression env e)
+ | _ -> super#visit_texpression env e)
| _ -> super#visit_texpression env e)
| _ -> super#visit_texpression env e
end
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index b80ff72f..d31f0cf9 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -46,18 +46,7 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
if variant_id = fuel_zero_id then []
else if variant_id = fuel_succ_id then [ mk_fuel_ty ]
else raise (Failure "Unreachable: improper variant id for fuel type")
- | Option ->
- let ty = Collections.List.to_cons_nil generics.types in
- let variant_id = Option.get variant_id in
- if variant_id = option_some_id then [ ty ]
- else if variant_id = option_none_id then []
- else
- raise (Failure "Unreachable: improper variant id for option type")
- | Range ->
- let ty = Collections.List.to_cons_nil generics.types in
- assert (variant_id = None);
- [ ty; ty ]
- | Vec | Array | Slice | Str ->
+ | Array | Slice | Str ->
(* Array: when not symbolic values (for instance, because of aggregates),
the array expressions are introduced as struct updates *)
raise (Failure "Attempting to access the fields of an opaque type"))
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index b1680282..6d9b9e15 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -305,19 +305,7 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
generics.types
| T.Assumed aty -> (
match aty with
- | T.Box | T.Vec ->
- assert (generics.regions = []);
- assert (List.length generics.types = 1);
- assert (generics.const_generics = []);
- generics.types
- | T.Option ->
- assert (generics.regions = []);
- assert (List.length generics.types = 1);
- assert (generics.const_generics = []);
- if adt.V.variant_id = Some T.option_some_id then generics.types
- else if adt.V.variant_id = Some T.option_none_id then []
- else raise (Failure "Unreachable")
- | T.Range ->
+ | T.Box ->
assert (generics.regions = []);
assert (List.length generics.types = 1);
assert (generics.const_generics = []);
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 54221cb1..9c698b51 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -405,8 +405,6 @@ let rec translate_sty (ty : T.sty) : ty =
mk_simpl_tuple_ty generics.types
| T.Assumed aty -> (
match aty with
- | T.Vec -> Adt (Assumed Vec, generics)
- | T.Option -> Adt (Assumed Option, generics)
| T.Box -> (
(* Eliminate the boxes *)
match generics.types with
@@ -418,8 +416,7 @@ let rec translate_sty (ty : T.sty) : ty =
)
| T.Array -> Adt (Assumed Array, generics)
| T.Slice -> Adt (Assumed Slice, generics)
- | T.Str -> Adt (Assumed Str, generics)
- | T.Range -> Adt (Assumed Range, generics)))
+ | T.Str -> Adt (Assumed Str, generics)))
| TypeVar vid -> TypeVar vid
| Literal ty -> Literal ty
| Never -> raise (Failure "Unreachable")
@@ -510,12 +507,9 @@ let translate_type_id (id : T.type_id) : type_id =
| T.Assumed aty ->
let aty =
match aty with
- | T.Vec -> Vec
- | T.Option -> Option
| T.Array -> Array
| T.Slice -> Slice
| T.Str -> Str
- | T.Range -> Range
| T.Box ->
(* Boxes have to be eliminated: this type id shouldn't
be translated *)
@@ -534,8 +528,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
let t_generics = translate_fwd_generic_args type_infos generics in
(* Eliminate boxes and simplify tuples *)
match type_id with
- | AdtId _
- | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+ | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) ->
(* No general parametricity for now *)
assert (
not
@@ -610,8 +603,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
match ty with
| T.Adt (type_id, generics) -> (
match type_id with
- | T.AdtId _
- | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+ | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) ->
(* Don't accept ADTs (which are not tuples) with borrows for now *)
assert (not (TypesUtils.ty_has_borrows type_infos ty));
let type_id = translate_type_id type_id in
@@ -815,7 +807,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
| FunId (Assumed aid) ->
assert (lid = None);
{
- can_fail = Assumed.assumed_can_fail aid;
+ can_fail = Assumed.assumed_fun_can_fail aid;
stateful_group = false;
stateful = false;
can_diverge = false;
@@ -1221,9 +1213,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
(* For now, only tuples can contain borrows *)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
- | T.AdtId _
- | T.Assumed
- (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+ | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
assert (field_values = []);
None
| T.Tuple ->
@@ -1368,9 +1358,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
* vector value upon visiting the "abstraction borrow" node *)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
- | T.AdtId _
- | T.Assumed
- (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+ | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
assert (field_values = []);
(ctx, None)
| T.Tuple ->
@@ -2441,17 +2429,12 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
(mk_typed_pattern_from_var var None)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
branch
- | T.Assumed (T.Vec | T.Array | T.Slice | T.Str) ->
+ | T.Assumed (T.Array | T.Slice | T.Str) ->
(* We can't expand those values: we can access the fields only
* through the functions provided by the API (note that we don't
* know how to expand values like vectors or arrays, because they have a variable number
* of fields!) *)
raise (Failure "Attempt to expand a non-expandable value")
- | T.Assumed Range -> raise (Failure "Unimplemented")
- | T.Assumed T.Option ->
- (* We shouldn't get there in the "one-branch" case: options have
- * two variants *)
- raise (Failure "Unreachable")
and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
(sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8e01c869..15297770 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -297,9 +297,11 @@ let translate_crate_to_pure (crate : A.crate) :
(* Translate all the function *signatures* *)
let assumed_sigs =
List.map
- (fun (id, sg, _, _) ->
- (E.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg))
- Assumed.assumed_infos
+ (fun (info : Assumed.assumed_fun_info) ->
+ ( E.Assumed info.fun_id,
+ List.map (fun _ -> None) info.fun_sig.inputs,
+ info.fun_sig ))
+ Assumed.assumed_fun_infos
in
let local_sigs =
List.map
@@ -425,11 +427,15 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
(true, kind)
in
(* Extract, if the config instructs to do so (depending on whether the type
- * is opaque or not) *)
- if
+ is opaque or not). Remark: we don't check if the definitions are builtin
+ here but in the function [export_types_group]: the reason is that if one
+ definition in the group is builtin, then we must check that all the
+ definitions are marked builtin *)
+ let extract =
(is_opaque && config.extract_opaque)
|| ((not is_opaque) && config.extract_transparent)
- then (
+ in
+ if extract then (
if extract_decl then
Extract.extract_type_decl ctx fmt type_decl_group kind def;
if extract_extra_info then
@@ -464,41 +470,58 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids
in
- (* Extract the type declarations.
-
- Because some declaration groups are delimited, we wrap the declarations
- between [{start,end}_type_decl_group].
+ (* Check if the definition are builtin - if yes they must be ignored.
+ Note that if one definition in the group is builtin, then all the
+ definitions must be builtin *)
+ let builtin =
+ let open ExtractBuiltin in
+ let types_map = builtin_types_map () in
+ List.map
+ (fun (def : Pure.type_decl) ->
+ let sname = name_to_simple_name def.name in
+ SimpleNameMap.find_opt sname types_map <> None)
+ defs
+ in
- Ex.:
- ====
- When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
- the [Datatype] and [End] delimiters in the snippet of code below:
+ if List.exists (fun b -> b) builtin then
+ (* Sanity check *)
+ assert (List.for_all (fun b -> b) builtin)
+ else (
+ (* Extract the type declarations.
+
+ Because some declaration groups are delimited, we wrap the declarations
+ between [{start,end}_type_decl_group].
+
+ Ex.:
+ ====
+ When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
+ the [Datatype] and [End] delimiters in the snippet of code below:
+
+ {[
+ Datatype:
+ tree =
+ TLeaf 'a
+ | TNode node ;
+
+ node =
+ Node (tree list)
+ End
+ ]}
+ *)
+ Extract.start_type_decl_group ctx fmt is_rec defs;
+ List.iteri
+ (fun i def ->
+ let kind = kind_from_index i in
+ export_type_decl kind def)
+ defs;
+ Extract.end_type_decl_group fmt is_rec defs;
- {[
- Datatype:
- tree =
- TLeaf 'a
- | TNode node ;
-
- node =
- Node (tree list)
- End
- ]}
- *)
- Extract.start_type_decl_group ctx fmt is_rec defs;
- List.iteri
- (fun i def ->
- let kind = kind_from_index i in
- export_type_decl kind def)
- defs;
- Extract.end_type_decl_group fmt is_rec defs;
-
- (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
- List.iteri
- (fun i def ->
- let kind = kind_from_index i in
- export_type_extra_info kind def)
- defs
+ (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
+ List.iteri
+ (fun i def ->
+ let kind = kind_from_index i in
+ export_type_extra_info kind def)
+ defs)
(** Export a global declaration.
@@ -520,12 +543,12 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
&& (((not is_opaque) && config.extract_transparent)
|| (is_opaque && config.extract_opaque))
in
- (* Check if it is an assumed global - if yes, we ignore it because we
+ (* Check if it is a builtin global - if yes, we ignore it because we
map the definition to one in the standard library *)
- let open ExtractAssumed in
+ let open ExtractBuiltin in
let sname = name_to_simple_name global.name in
let extract =
- extract && SimpleNameMap.find_opt sname assumed_globals_map = None
+ extract && SimpleNameMap.find_opt sname builtin_globals_map = None
in
if extract then
(* We don't wrap global declaration groups between calls to functions
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 4a187893..16f8c5f9 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -168,9 +168,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
in
(* Continue exploring *)
analyze expl_info ty_info rty
- | Adt
- ( (Tuple | Assumed (Box | Vec | Option | Slice | Array | Str | Range)),
- generics ) ->
+ | Adt ((Tuple | Assumed (Box | Slice | Array | Str)), generics) ->
(* Nothing to update: just explore the type parameters *)
List.fold_left
(fun ty_info ty -> analyze expl_info ty_info ty)
diff --git a/compiler/dune b/compiler/dune
index 2f5a0a44..4ec46b70 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -22,8 +22,8 @@
Expressions
ExpressionsUtils
Extract
- ExtractAssumed
ExtractBase
+ ExtractBuiltin
FunsAnalysis
Identifiers
InterpreterBorrowsCore
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 02:50:39 +0000