diff options
31 files changed, 1602 insertions, 1436 deletions
@@ -115,7 +115,7 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA # Add specific options to some tests trans-no_nested_borrows trans-paper: \ - OPTIONS += -test-units -test-trans-units -no-split-files -no-state + OPTIONS += -test-trans-units -no-split-files -no-state trans-no_nested_borrows trans-paper: SUBDIR := misc tfstar-no_nested_borrows tfstar-paper: tlean-no_nested_borrows: SUBDIR := @@ -157,7 +157,7 @@ tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state +transp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state transp-polonius_list: SUBDIR := misc tfstarp-polonius_list: OPTIONS += tcoqp-polonius_list: OPTIONS += diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index 6b7b0792..22378af7 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -2,3 +2,5 @@ import Base.Primitives.Base import Base.Primitives.Scalar import Base.Primitives.Array import Base.Primitives.Vec +import Base.Primitives.Alloc +import Base.Primitives.CoreOpsDeref diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean new file mode 100644 index 00000000..0580421f --- /dev/null +++ b/backends/lean/Base/Primitives/Alloc.lean @@ -0,0 +1,37 @@ +import Lean +import Base.Primitives.Base +import Base.Primitives.CoreOpsDeref + +open Primitives +open Result + +namespace alloc + +namespace boxed -- alloc.boxed + +namespace Box -- alloc.boxed.Box + +def deref (T : Type) (x : T) : Result T := ret x +def deref_mut (T : Type) (x : T) : Result T := ret x +def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x + +/-- Trait instance -/ +def coreOpsDerefInst (Self : Type) : + core.ops.deref.Deref Self := { + Target := Self + deref := deref Self +} + +/-- Trait instance -/ +def coreOpsDerefMutInst (Self : Type) : + core.ops.deref.DerefMut Self := { + derefInst := coreOpsDerefInst Self + deref_mut := deref_mut Self + deref_mut_back := deref_mut_back Self +} + +end Box -- alloc.boxed.Box + +end boxed -- alloc.boxed + +end alloc diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 7c0fa3bb..2bd081c0 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -120,8 +120,8 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := -- MISC -- ---------- -@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x -@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y +@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : Result a := ret x +@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : Result a := ret y /-- Aeneas-translated function -- useful to reduce non-recursive definitions. Use with `simp [ aeneas ]` -/ diff --git a/backends/lean/Base/Primitives/CoreOpsDeref.lean b/backends/lean/Base/Primitives/CoreOpsDeref.lean new file mode 100644 index 00000000..2b540012 --- /dev/null +++ b/backends/lean/Base/Primitives/CoreOpsDeref.lean @@ -0,0 +1,18 @@ +import Lean +import Base.Primitives.Base + +open Primitives +open Result + +namespace core.ops.deref + +structure Deref (Self : Type) where + Target : Type + deref : Self → Result Target + +structure DerefMut (Self : Type) where + derefInst : Deref Self + deref_mut : Self → Result derefInst.Target + deref_mut_back : Self → derefInst.Target → Result Self + +end core.ops.deref 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/Config.ml b/compiler/Config.ml index 62f6c300..cd0903b6 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -306,13 +306,6 @@ let filter_useless_monadic_calls = ref true *) let filter_useless_functions = ref true -(** Obsolete. TODO: remove. - - For Lean we used to parameterize the entire development by a section variable - called opaque_defs, of type OpaqueDefs. - *) -let wrap_opaque_in_sig = ref false - (** Use short names for the record fields. Some backends can't disambiguate records when their field names have collisions. diff --git a/compiler/Extract.ml b/compiler/Extract.ml index e24cae16..91827a31 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -229,12 +229,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 -> [ @@ -242,12 +239,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 -> [ @@ -255,20 +249,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 @@ -280,8 +271,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 -> [ @@ -291,8 +280,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 -> [ @@ -301,8 +288,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 -> [ @@ -311,8 +296,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 () : @@ -321,66 +304,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"); ] @@ -814,12 +761,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) fname ^ lp_suffix ^ suffix in - let opaque_pre () = - match !Config.backend with - | FStar | Coq | HOL4 -> "" - | Lean -> if !Config.wrap_opaque_in_sig then "opaque_defs." else "" - in - let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty) : string = (* Small helper to derive var names from ADT type names. @@ -853,12 +794,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 @@ -927,10 +865,12 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* We need to add parentheses if the value is negative *) if sv.PV.value >= Z.of_int 0 then F.pp_print_string fmt (Z.to_string sv.PV.value) - else + else if !backend = Lean then + (* TODO: parsing issues with Lean because there are ambiguous + interpretations between int values and nat values *) F.pp_print_string fmt - ("(" ^ Z.to_string sv.PV.value - ^ if !backend = Lean then ":Int" else "" ^ ")"); + ("(-(" ^ Z.to_string (Z.neg sv.PV.value) ^ ":Int))") + else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")"); (match !backend with | Coq -> let iname = int_name sv.PV.int_ty in @@ -993,7 +933,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) trait_type_name; trait_method_name; trait_type_clause_name; - opaque_pre; var_basename; type_var_basename; const_generic_var_basename; @@ -1042,11 +981,8 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter) (* In HOL4, opaque functions have a special treatment *) if is_single_opaque_fun_decl_group dg then () else - let with_opaque_pre = false in let compute_fun_def_name (def : Pure.fun_decl) : string = - ctx_get_local_function with_opaque_pre def.def_id def.loop_id - def.back_id ctx - ^ "_def" + ctx_get_local_function def.def_id def.loop_id def.back_id ctx ^ "_def" in let names = List.map compute_fun_def_name dg in (* Add a break before *) @@ -1169,7 +1105,7 @@ let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (cg : const_generic) : unit = match cg with | ConstGenericGlobal id -> - let s = ctx_get_global ctx.use_opaque_pre id ctx in + let s = ctx_get_global id ctx in F.pp_print_string fmt s | ConstGenericValue v -> ctx.fmt.extract_literal fmt inside v | ConstGenericVar id -> @@ -1237,14 +1173,33 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) In HOL4 we would write: `('a, 'b) tree` *) - let with_opaque_pre = false in match !backend with | FStar | Coq | Lean -> let print_paren = inside && has_params in if print_paren then F.pp_print_string fmt "("; (* TODO: for now, only the opaque *functions* are extracted in the opaque module. The opaque *types* are assumed. *) - F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx); + F.pp_print_string fmt (ctx_get_type type_id ctx); + (* We might need to filter the type arguments, if the type + is builtin (for instance, we filter the global allocator type + argument for `Vec`). *) + let generics = + match type_id with + | AdtId id -> ( + match + TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map + with + | None -> generics + | Some filter -> + let types = List.combine filter generics.types in + let types = + List.filter_map + (fun (b, ty) -> if b then Some ty else None) + types + in + { generics with types }) + | _ -> generics + in extract_generic_args ctx fmt no_params_tys generics; if print_paren then F.pp_print_string fmt ")" | HOL4 -> @@ -1267,7 +1222,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (extract_rec true) types; if print_paren then F.pp_print_string fmt ")"; F.pp_print_space fmt ()); - F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx); + F.pp_print_string fmt (ctx_get_type type_id ctx); if trait_refs <> [] then ( F.pp_print_space fmt (); Collections.List.iter_link (F.pp_print_space fmt) @@ -1332,11 +1287,13 @@ and extract_trait_decl_ref (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_decl_ref) : unit = let use_brackets = tr.decl_generics <> empty_generic_args && inside in - let is_opaque = false in - let name = ctx_get_trait_decl is_opaque tr.trait_decl_id ctx in + let name = ctx_get_trait_decl tr.trait_decl_id ctx in if use_brackets then F.pp_print_string fmt "("; F.pp_print_string fmt name; - extract_generic_args ctx fmt no_params_tys tr.decl_generics; + (* There is something subtle here: the trait obligations for the implemented + trait are put inside the parent clauses, so we must ignore them here *) + let generics = { tr.decl_generics with trait_refs = [] } in + extract_generic_args ctx fmt no_params_tys generics; if use_brackets then F.pp_print_string fmt ")" and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter) @@ -1363,14 +1320,13 @@ and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter) and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) (id : trait_instance_id) : unit = - let with_opaque_pre = false in match id with | Self -> (* This has specific treatment depending on the item we're extracting (associated type, etc.). We should have caught this elsewhere. *) raise (Failure "Unexpected") | TraitImpl id -> - let name = ctx_get_trait_impl with_opaque_pre id ctx in + let name = ctx_get_trait_impl id ctx in F.pp_print_string fmt name | Clause id -> let name = ctx_get_local_trait_clause id ctx in @@ -1400,8 +1356,28 @@ 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 + (* Register the filtering information, if there is *) + let ctx = + match info with + | Some { keep_params = Some keep; _ } -> + { + ctx with + types_filter_type_args_map = + TypeDeclId.Map.add def.def_id keep ctx.types_filter_type_args_map; + } + | _ -> ctx + 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 -> String.concat "." info.rust_name + in + let ctx = ctx_add (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 @@ -1409,18 +1385,77 @@ 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 | Some { body_info = 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) + | Some info -> + raise + (Failure + ("Invalid builtin information: " + ^ show_builtin_type_info info)) + 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 (FieldId (AdtId def.def_id, fid)) name ctx) + ctx field_names in (* Add the constructor name *) - fst (ctx_add_struct def ctx) + ctx_add (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 (VariantId (AdtId def.def_id, vid)) vname ctx) + ctx variant_names | Opaque -> (* Nothing to do *) ctx @@ -1622,9 +1657,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) (* If Coq: print the constructor name *) (* TODO: remove superfluous test not is_rec below *) if !backend = Coq && not is_rec then ( - let with_opaque_pre = false in - F.pp_print_string fmt - (ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx); + F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx); F.pp_print_string fmt " "); (match !backend with | Lean -> () @@ -1668,16 +1701,14 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) (* We extract for Coq or Lean, and we have a recursive record, or a record in a group of mutually recursive types: we extract it as an inductive type *) assert (is_rec && (!backend = Coq || !backend = Lean)); - let with_opaque_pre = false in (* Small trick: in Lean we use namespaces, meaning we don't need to prefix the constructor name with the name of the type at definition site, i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq we generate `inductive Foo := | mk ... *) let cons_name = - if !backend = Lean then "mk" - else ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx + if !backend = Lean then "mk" else ctx_get_struct (AdtId def.def_id) ctx in - let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in + let def_name = ctx_get_local_type def.def_id ctx in extract_type_decl_variant ctx fmt type_decl_group def_name type_params cg_params cons_name fields) in @@ -1707,8 +1738,7 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit = let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit = - let with_opaque_pre = false in - let trait_name = ctx_get_trait_decl with_opaque_pre clause.trait_id ctx in + let trait_name = ctx_get_trait_decl clause.trait_id ctx in F.pp_print_string fmt trait_name; extract_generic_args ctx fmt no_params_tys clause.generics @@ -1730,8 +1760,7 @@ let extract_trait_self_clause (insert_req_space : unit -> unit) F.pp_print_space fmt (); F.pp_print_string fmt ":"; F.pp_print_space fmt (); - let with_opaque_pre = false in - let trait_id = ctx_get_trait_decl with_opaque_pre trait_decl.def_id ctx in + let trait_id = ctx_get_trait_decl trait_decl.def_id ctx in F.pp_print_string fmt trait_id; List.iter (fun p -> @@ -1900,8 +1929,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) let is_opaque_coq = !backend = Coq && is_opaque in let use_forall = is_opaque_coq && def.generics <> empty_generic_params in (* Retrieve the definition name *) - let with_opaque_pre = false in - let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in + let def_name = ctx_get_local_type def.def_id ctx in (* Add the type and const generic params - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx_body, type_params, cg_params, trait_clauses = @@ -1988,8 +2016,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) (def : type_decl) : unit = (* Retrieve the definition name *) - let with_opaque_pre = false in - let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in + let def_name = ctx_get_local_type def.def_id ctx in (* Generic parameters are unsupported *) assert (def.generics.const_generics = []); (* Trait clauses on type definitions are unsupported *) @@ -2014,8 +2041,7 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) let extract_type_decl_hol4_empty_record (ctx : extraction_ctx) (fmt : F.formatter) (def : type_decl) : unit = (* Retrieve the definition name *) - let with_opaque_pre = false in - let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in + let def_name = ctx_get_local_type def.def_id ctx in (* Sanity check *) assert (def.generics = empty_generic_params); (* Generate the declaration *) @@ -2098,8 +2124,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) | Struct fields -> let adt_id = AdtId decl.def_id in (* Generate the instruction for the record constructor *) - let with_opaque_pre = false in - let cons_name = ctx_get_struct with_opaque_pre adt_id ctx in + let cons_name = ctx_get_struct adt_id ctx in extract_arguments_info cons_name fields; (* Generate the instruction for the record projectors, if there are *) let is_rec = decl_is_from_rec_group kind in @@ -2143,11 +2168,8 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) in let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in let ctx, field_var = ctx_add_var "x" (VarId.of_int 1) ctx in - let with_opaque_pre = false in - let def_name = ctx_get_local_type with_opaque_pre decl.def_id ctx in - let cons_name = - ctx_get_struct with_opaque_pre (AdtId decl.def_id) ctx - in + let def_name = ctx_get_local_type decl.def_id ctx in + let cons_name = ctx_get_struct (AdtId decl.def_id) ctx in let extract_field_proj (field_id : FieldId.id) (_ : field) : unit = F.pp_print_space fmt (); (* Outer box for the projector definition *) @@ -2359,33 +2381,81 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) let extract_fun_decl_register_names (ctx : extraction_ctx) (has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) : extraction_ctx = - let fwd = def.fwd in - let backs = def.backs in - (* Register the decrease clauses, if necessary *) - let register_decreases ctx def = - if has_decreases_clause def then - (* Add the termination measure *) - let ctx = ctx_add_termination_measure def ctx in - (* Add the decreases proof for Lean only *) - match !Config.backend with - | Coq | FStar -> ctx - | HOL4 -> raise (Failure "Unexpected") - | Lean -> ctx_add_decreases_proof def ctx - else ctx - in - let ctx = List.fold_left register_decreases ctx (fwd.f :: fwd.loops) in - let register_fun ctx f = ctx_add_fun_decl def f ctx in - let register_funs ctx fl = List.fold_left register_fun ctx fl in - (* Register the names of the forward functions *) - let ctx = - if def.keep_fwd then register_funs ctx (fwd.f :: fwd.loops) else ctx - in - (* Register the names of the backward functions *) - List.fold_left - (fun ctx { f = back; loops = loop_backs } -> - let ctx = register_fun ctx back in - register_funs ctx loop_backs) - ctx backs + (* Ignore the trait methods **declarations** (rem.: we do not ignore the trait + method implementations): we do not need to refer to them directly. We will + only use their type for the fields of the records we generate for the trait + declarations *) + match def.fwd.f.kind with + | TraitMethodDecl _ -> ctx + | _ -> ( + (* Check if the function is builtin *) + let builtin = + let open ExtractBuiltin in + let funs_map = builtin_funs_map () in + let sname = name_to_simple_name def.fwd.f.basename in + SimpleNameMap.find_opt sname funs_map + in + (* Use the builtin names if necessary *) + match builtin with + | Some (filter_info, info) -> + (* Register the filtering information, if there is *) + let ctx = + match filter_info with + | Some keep -> + { + ctx with + funs_filter_type_args_map = + FunDeclId.Map.add def.fwd.f.def_id keep + ctx.funs_filter_type_args_map; + } + | _ -> ctx + in + let backs = List.map (fun f -> f.f) def.backs in + let funs = if def.keep_fwd then def.fwd.f :: backs else backs in + List.fold_left + (fun ctx (f : fun_decl) -> + let open ExtractBuiltin in + let fun_id = + (Pure.FunId (Regular f.def_id), f.loop_id, f.back_id) + in + let fun_name = + (List.find + (fun (x : builtin_fun_info) -> x.rg = f.back_id) + info) + .extract_name + in + ctx_add (FunId (FromLlbc fun_id)) fun_name ctx) + ctx funs + | None -> + let fwd = def.fwd in + let backs = def.backs in + (* Register the decrease clauses, if necessary *) + let register_decreases ctx def = + if has_decreases_clause def then + (* Add the termination measure *) + let ctx = ctx_add_termination_measure def ctx in + (* Add the decreases proof for Lean only *) + match !Config.backend with + | Coq | FStar -> ctx + | HOL4 -> raise (Failure "Unexpected") + | Lean -> ctx_add_decreases_proof def ctx + else ctx + in + let ctx = + List.fold_left register_decreases ctx (fwd.f :: fwd.loops) + in + let register_fun ctx f = ctx_add_fun_decl def f ctx in + let register_funs ctx fl = List.fold_left register_fun ctx fl in + (* Register the names of the forward functions *) + let ctx = + if def.keep_fwd then register_funs ctx (fwd.f :: fwd.loops) else ctx + in + (* Register the names of the backward functions *) + List.fold_left + (fun ctx { f = back; loops = loop_backs } -> + let ctx = register_fun ctx back in + register_funs ctx loop_backs) + ctx backs) (** Simply add the global name to the context. *) let extract_global_decl_register_names (ctx : extraction_ctx) @@ -2459,18 +2529,14 @@ let extract_adt_g_value * [{ field0=...; ...; fieldn=...; }] in case of structures. *) let cons = - (* The ADT shouldn't be opaque *) - let with_opaque_pre = false in match variant_id with | Some vid -> ( (* In the case of Lean, we might have to add the type name as a prefix *) match (!backend, adt_id) with | Lean, Assumed _ -> - ctx_get_type with_opaque_pre adt_id ctx - ^ "." - ^ ctx_get_variant adt_id vid ctx + ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx | _ -> ctx_get_variant adt_id vid ctx) - | None -> ctx_get_struct with_opaque_pre adt_id ctx + | None -> ctx_get_struct adt_id ctx in let use_parentheses = inside && field_values <> [] in if use_parentheses then F.pp_print_string fmt "("; @@ -2489,8 +2555,7 @@ let extract_adt_g_value (* Extract globals in the same way as variables *) let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (id : A.GlobalDeclId.id) : unit = - let with_opaque_pre = ctx.use_opaque_pre in - F.pp_print_string fmt (ctx_get_global with_opaque_pre id ctx) + F.pp_print_string fmt (ctx_get_global id ctx) (** [inside]: see {!extract_ty}. @@ -2626,9 +2691,9 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) if inside then F.pp_print_string fmt "("; (* Open a box for the function call *) F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the function name *) - let with_opaque_pre = ctx.use_opaque_pre in - (* For the function name: the id is not the same depending on whether + (* Print the function name. + + For the function name: the id is not the same depending on whether we call a trait method and a "regular" function (remark: trait method *implementations* are considered as regular functions here; only calls to method of traits which are parameterized in a where @@ -2701,7 +2766,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) let fun_id = FromLlbc (FunId (Regular method_id.id), lp_id, rg_id) in - let fun_name = ctx_get_function with_opaque_pre fun_id ctx in + let fun_name = ctx_get_function fun_id ctx in F.pp_print_string fmt fun_name; (* Note that we do not need to print the generics for the trait @@ -2712,12 +2777,32 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref | _ -> - let fun_name = ctx_get_function with_opaque_pre fun_id ctx in + let fun_name = ctx_get_function fun_id ctx in F.pp_print_string fmt fun_name); (* Sanity check: HOL4 doesn't support const generics *) assert (generics.const_generics = [] || !backend <> HOL4); - (* Print the generics *) + (* Print the generics. + + We might need to filter some of the type arguments, if the type + is builtin (for instance, we filter the global allocator type + argument for `Vec::new`). + *) + let generics = + match fun_id with + | FromLlbc (FunId (Regular id), _, _) -> ( + match FunDeclId.Map.find_opt id ctx.funs_filter_type_args_map with + | None -> generics + | Some filter -> + let types = List.combine filter generics.types in + let types = + List.filter_map + (fun (b, ty) -> if b then Some ty else None) + types + in + { generics with types }) + | _ -> generics + in extract_generic_args ctx fmt TypeDeclId.Set.empty generics; (* Print the arguments *) List.iter @@ -3210,7 +3295,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) (* Open the box for `Array.replicate T N [` *) F.pp_open_hovbox fmt ctx.indent_incr; (* Print the array constructor *) - let cs = ctx_get_struct false (Assumed Array) ctx in + let cs = ctx_get_struct (Assumed Array) ctx in F.pp_print_string fmt cs; (* Print the parameters *) let _, generics = ty_as_adt e_ty in @@ -3563,10 +3648,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit = assert (not def.is_global_decl_body); (* Retrieve the function name *) - let with_opaque_pre = false in let def_name = - ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id - ctx + ctx_get_local_function def.def_id def.loop_id def.back_id ctx in (* Add a break before *) if !backend <> HOL4 || not (decl_is_first_from_group kind) then @@ -3594,19 +3677,13 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) let use_forall = is_opaque_coq && def.signature.generics <> empty_generic_params in - (* Print the qualifier ("assume", etc.). - - if `wrap_opaque_in_sig`: we generate a record of assumed funcions. - TODO: this is obsolete. - *) - (if not (!Config.wrap_opaque_in_sig && (kind = Assumed || kind = Declared)) - then - let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in - match qualif with - | Some qualif -> - F.pp_print_string fmt qualif; - F.pp_print_space fmt () - | None -> ()); + (* Print the qualifier ("assume", etc.). *) + let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in + (match qualif with + | Some qualif -> + F.pp_print_string fmt qualif; + F.pp_print_space fmt () + | None -> ()); F.pp_print_string fmt def_name; F.pp_print_space fmt (); if use_forall then ( @@ -3817,10 +3894,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = (* Retrieve the definition name *) - let with_opaque_pre = false in let def_name = - ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id - ctx + ctx_get_local_function def.def_id def.loop_id def.back_id ctx in assert (def.signature.generics.const_generics = []); (* Add the type/const gen parameters - note that we need those bindings @@ -4015,10 +4090,9 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) extract_comment fmt [ "[" ^ Print.global_name_to_string global.name ^ "]" ]; F.pp_print_space fmt (); - let with_opaque_pre = false in - let decl_name = ctx_get_global with_opaque_pre global.def_id ctx in + let decl_name = ctx_get_global global.def_id ctx in let body_name = - ctx_get_function with_opaque_pre + ctx_get_function (FromLlbc (Pure.FunId (Regular global.body_id), None, None)) ctx in @@ -4056,73 +4130,263 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break to insert lines between declarations *) F.pp_print_break fmt 0 0 -(** Register the names for one trait method item *) -let extract_trait_decl_method_register_names (ctx : extraction_ctx) - (trait_decl : trait_decl) (name : string) (id : fun_decl_id) : +(** Similar to {!extract_trait_decl_register_names} *) +let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) + (trait_decl : trait_decl) + (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) : extraction_ctx = - (* We add one field per required forward/backward function *) - let trans = A.FunDeclId.Map.find id ctx.trans_funs in - - let register_fun ctx f = ctx_add_trait_method trait_decl name f.f ctx in + let generics = trait_decl.generics in + (* Compute the clause names *) + let clause_names = + match builtin_info with + | None -> + List.map + (fun (c : trait_clause) -> + let name = ctx.fmt.trait_parent_clause_name trait_decl c in + (* Add a prefix if necessary *) + let name = + if !Config.record_fields_short_names then name + else ctx.fmt.trait_decl_name trait_decl ^ name + in + (c.clause_id, name)) + generics.trait_clauses + | Some info -> + List.map + (fun (c, name) -> (c.clause_id, name)) + (List.combine generics.trait_clauses info.parent_clauses) + in + (* Register the names *) + List.fold_left + (fun ctx (cid, cname) -> + ctx_add (TraitParentClauseId (trait_decl.def_id, cid)) cname ctx) + ctx clause_names + +(** Similar to {!extract_trait_decl_register_names} *) +let extract_trait_decl_register_constant_names (ctx : extraction_ctx) + (trait_decl : trait_decl) + (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) : + extraction_ctx = + let consts = trait_decl.consts in + (* Compute the names *) + let constant_names = + match builtin_info with + | None -> + List.map + (fun (item_name, _) -> + let name = ctx.fmt.trait_const_name trait_decl item_name in + (* Add a prefix if necessary *) + let name = + if !Config.record_fields_short_names then name + else ctx.fmt.trait_decl_name trait_decl ^ name + in + (item_name, name)) + consts + | Some info -> + let const_map = StringMap.of_list info.consts in + List.map + (fun (item_name, _) -> + (item_name, StringMap.find item_name const_map)) + consts + in + (* Register the names *) + List.fold_left + (fun ctx (item_name, name) -> + ctx_add (TraitItemId (trait_decl.def_id, item_name)) name ctx) + ctx constant_names + +(** Similar to {!extract_trait_decl_register_names} *) +let extract_trait_decl_type_names (ctx : extraction_ctx) + (trait_decl : trait_decl) + (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) : + extraction_ctx = + let types = trait_decl.types in + (* Compute the names *) + let type_names = + match builtin_info with + | None -> + let compute_type_name (item_name : string) : string = + let type_name = ctx.fmt.trait_type_name trait_decl item_name in + if !Config.record_fields_short_names then type_name + else ctx.fmt.trait_decl_name trait_decl ^ type_name + in + let compute_clause_name (item_name : string) (clause : trait_clause) : + TraitClauseId.id * string = + let name = + ctx.fmt.trait_type_clause_name trait_decl item_name clause + in + (* Add a prefix if necessary *) + let name = + if !Config.record_fields_short_names then name + else ctx.fmt.trait_decl_name trait_decl ^ name + in + (clause.clause_id, name) + in + List.map + (fun (item_name, (item_clauses, _)) -> + (* Type name *) + let type_name = compute_type_name item_name in + (* Clause names *) + let clauses = + List.map (compute_clause_name item_name) item_clauses + in + (item_name, (type_name, clauses))) + types + | Some info -> + let type_map = StringMap.of_list info.types in + List.map + (fun (item_name, (item_clauses, _)) -> + let type_name, clauses_info = StringMap.find item_name type_map in + let clauses = + List.map + (fun (clause, clause_name) -> (clause.clause_id, clause_name)) + (List.combine item_clauses clauses_info) + in + (item_name, (type_name, clauses))) + types + in + (* Register the names *) + List.fold_left + (fun ctx (item_name, (type_name, clauses)) -> + let ctx = + ctx_add (TraitItemId (trait_decl.def_id, item_name)) type_name ctx + in + List.fold_left + (fun ctx (clause_id, clause_name) -> + ctx_add + (TraitItemClauseId (trait_decl.def_id, item_name, clause_id)) + clause_name ctx) + ctx clauses) + ctx type_names + +(** Similar to {!extract_trait_decl_register_names} *) +let extract_trait_decl_method_names (ctx : extraction_ctx) + (trait_decl : trait_decl) + (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) : + extraction_ctx = + let required_methods = trait_decl.required_methods in + (* Compute the names *) + let method_names = + (* We add one field per required forward/backward function *) + let get_funs_for_id (id : fun_decl_id) : fun_decl list = + let trans : pure_fun_translation = FunDeclId.Map.find id ctx.trans_funs in + List.map (fun f -> f.f) (trans.fwd :: trans.backs) + in + match builtin_info with + | None -> + (* We add one field per required forward/backward function *) + let compute_item_names (item_name : string) (id : fun_decl_id) : + string * (RegionGroupId.id option * string) list = + let compute_fun_name (f : fun_decl) : RegionGroupId.id option * string + = + (* We do something special: we use the base name but remove everything + but the crate (because [get_name] removes it) and the last ident. + This allows us to reuse the [ctx_compute_fun_decl] function. + *) + let basename : name = + match (f.basename : name) with + | Ident crate :: name -> + Ident crate :: [ Collections.List.last name ] + | _ -> raise (Failure "Unexpected") + in + let f = { f with basename } in + let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in + let name = ctx_compute_fun_name trans f ctx in + (* Add a prefix if necessary *) + let name = + if !Config.record_fields_short_names then name + else ctx.fmt.trait_decl_name trait_decl ^ "_" ^ name + in + (f.back_id, name) + in + let funs = get_funs_for_id id in + (item_name, List.map compute_fun_name funs) + in + List.map (fun (name, id) -> compute_item_names name id) required_methods + | Some info -> + let funs_map = StringMap.of_list info.funs in + List.map + (fun (item_name, fun_id) -> + let info = StringMap.find item_name funs_map in + let trans_funs = get_funs_for_id fun_id in + let rg_with_name_list = + List.map + (fun (trans_fun : fun_decl) -> + List.find (fun (rg, _) -> rg = trans_fun.back_id) info) + trans_funs + in + (item_name, rg_with_name_list)) + required_methods + in (* Register the names *) - let funs = trans.fwd :: trans.backs in - List.fold_left register_fun ctx funs + List.fold_left + (fun ctx (item_name, funs) -> + (* We add one field per required forward/backward function *) + List.fold_left + (fun ctx (rg, fun_name) -> + ctx_add + (TraitMethodId (trait_decl.def_id, item_name, rg)) + fun_name ctx) + ctx funs) + ctx method_names (** Similar to {!extract_type_decl_register_names} *) let extract_trait_decl_register_names (ctx : extraction_ctx) (trait_decl : trait_decl) : extraction_ctx = - let { - def_id = _; - name = _; - generics; - preds = _; - all_trait_clauses = _; - consts; - types; - required_methods; - provided_methods = _; - } = - trait_decl + (* Lookup the information if this is a builtin trait *) + let open ExtractBuiltin in + let sname = name_to_simple_name trait_decl.name in + let builtin_info = + SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) + in + let ctx = + let trait_name = + match builtin_info with + | None -> ctx.fmt.trait_decl_name trait_decl + | Some info -> info.extract_name + in + ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx in - let ctx = ctx_add_trait_decl trait_decl ctx in (* Parent clauses *) let ctx = - List.fold_left - (fun ctx clause -> ctx_add_trait_parent_clause trait_decl clause ctx) - ctx generics.trait_clauses + extract_trait_decl_register_parent_clause_names ctx trait_decl builtin_info in (* Constants *) let ctx = - List.fold_left - (fun ctx (name, (_, _)) -> ctx_add_trait_const trait_decl name ctx) - ctx consts + extract_trait_decl_register_constant_names ctx trait_decl builtin_info in (* Types *) - let ctx = - List.fold_left - (fun ctx (name, (clauses, _)) -> - let ctx = ctx_add_trait_type trait_decl name ctx in - List.fold_left - (fun ctx clause -> - ctx_add_trait_type_clause trait_decl name clause ctx) - ctx clauses) - ctx types - in + let ctx = extract_trait_decl_type_names ctx trait_decl builtin_info in (* Required methods *) - List.fold_left - (fun ctx (name, id) -> - (* We add one field per required forward/backward function *) - extract_trait_decl_method_register_names ctx trait_decl name id) - ctx required_methods + let ctx = extract_trait_decl_method_names ctx trait_decl builtin_info in + ctx (** Similar to {!extract_type_decl_register_names} *) let extract_trait_impl_register_names (ctx : extraction_ctx) (trait_impl : trait_impl) : extraction_ctx = + let trait_decl = + TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id + ctx.trans_trait_decls + in + (* Check if the trait implementation is builtin *) + let builtin_info = + let open ExtractBuiltin in + let type_sname = name_to_simple_name trait_impl.name in + let trait_sname = name_to_simple_name trait_decl.name in + SimpleNamePairMap.find_opt (type_sname, trait_sname) + (builtin_trait_impls_map ()) + in + (* For now we do not support overriding provided methods *) assert (trait_impl.provided_methods = []); (* Everything is taken care of by {!extract_trait_decl_register_names} *but* the name of the implementation itself *) - ctx_add_trait_impl trait_impl ctx + (* Compute the name *) + let name = + match builtin_info with + | None -> ctx.fmt.trait_impl_name trait_decl trait_impl + | Some name -> name + in + ctx_add (TraitImplId trait_impl.def_id) name ctx (** Small helper. @@ -4198,8 +4462,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) (decl : trait_decl) : unit = (* Retrieve the trait name *) - let with_opaque_pre = false in - let decl_name = ctx_get_trait_decl with_opaque_pre decl.def_id ctx in + let decl_name = ctx_get_trait_decl decl.def_id ctx in (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) @@ -4344,7 +4607,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) if use_forall then F.pp_print_string fmt ","; (* Extract the function call *) F.pp_print_space fmt (); - let id = ctx_get_local_function false f.def_id None f.back_id ctx in + let id = ctx_get_local_function f.def_id None f.back_id ctx in F.pp_print_string fmt id; let all_generics = let i_tys, i_cgs, i_tcs = impl_generics in @@ -4363,9 +4626,9 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) (** Extract a trait implementation *) let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (impl : trait_impl) : unit = + log#ldebug (lazy ("extract_trait_impl: " ^ Names.name_to_string impl.name)); (* Retrieve the impl name *) - let with_opaque_pre = false in - let impl_name = ctx_get_trait_impl with_opaque_pre impl.def_id ctx in + let impl_name = ctx_get_trait_impl impl.def_id ctx in (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) @@ -4389,9 +4652,11 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (* `let (....) : Trait ... =` *) (* Open the box for the name + generics *) F.pp_open_hovbox fmt ctx.indent_incr; - let qualif = Option.get (ctx.fmt.fun_decl_kind_to_qualif SingleNonRec) in - F.pp_print_string fmt qualif; - F.pp_print_space fmt (); + (match ctx.fmt.fun_decl_kind_to_qualif SingleNonRec with + | Some qualif -> + F.pp_print_string fmt qualif; + F.pp_print_space fmt () + | None -> ()); F.pp_print_string fmt impl_name; (* Print the generics *) @@ -4439,7 +4704,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) let item_name = ctx_get_trait_const trait_decl_id name ctx in let ty () = F.pp_print_space fmt (); - F.pp_print_string fmt (ctx_get_global false id ctx) + F.pp_print_string fmt (ctx_get_global id ctx) in extract_trait_impl_item ctx fmt item_name ty) @@ -4525,12 +4790,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "assert_norm"; F.pp_print_space fmt (); F.pp_print_string fmt "("; - (* Note that if the function is opaque, the unit test will fail - because the normalizer will get stuck *) - let with_opaque_pre = ctx.use_opaque_pre in let fun_name = - ctx_get_local_function with_opaque_pre def.def_id def.loop_id - def.back_id ctx + ctx_get_local_function def.def_id def.loop_id def.back_id ctx in F.pp_print_string fmt fun_name; if sg.inputs <> [] then ( @@ -4545,12 +4806,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "Check"; F.pp_print_space fmt (); F.pp_print_string fmt "("; - (* Note that if the function is opaque, the unit test will fail - because the normalizer will get stuck *) - let with_opaque_pre = ctx.use_opaque_pre in let fun_name = - ctx_get_local_function with_opaque_pre def.def_id def.loop_id - def.back_id ctx + ctx_get_local_function def.def_id def.loop_id def.back_id ctx in F.pp_print_string fmt fun_name; if sg.inputs <> [] then ( @@ -4562,12 +4819,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "#assert"; F.pp_print_space fmt (); F.pp_print_string fmt "("; - (* Note that if the function is opaque, the unit test will fail - because the normalizer will get stuck *) - let with_opaque_pre = ctx.use_opaque_pre in let fun_name = - ctx_get_local_function with_opaque_pre def.def_id def.loop_id - def.back_id ctx + ctx_get_local_function def.def_id def.loop_id def.back_id ctx in F.pp_print_string fmt fun_name; if sg.inputs <> [] then ( @@ -4581,12 +4834,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) | HOL4 -> F.pp_print_string fmt "val _ = assert_return ("; F.pp_print_string fmt "“"; - (* Note that if the function is opaque, the unit test will fail - because the normalizer will get stuck *) - let with_opaque_pre = ctx.use_opaque_pre in let fun_name = - ctx_get_local_function with_opaque_pre def.def_id def.loop_id - def.back_id ctx + ctx_get_local_function def.def_id def.loop_id def.back_id ctx in F.pp_print_string fmt fun_name; if sg.inputs <> [] then ( 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..e004aba8 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 @@ -251,37 +251,6 @@ type formatter = { trait_type_name : trait_decl -> string -> string; trait_method_name : trait_decl -> string -> string; trait_type_clause_name : trait_decl -> string -> trait_clause -> string; - opaque_pre : unit -> string; - (** TODO: obsolete, remove. - - The prefix to use for opaque definitions. - - We need this because for some backends like Lean and Coq, we group - opaque definitions in module signatures, meaning that using those - definitions requires to prefix them with a module parameter name (such - as "opaque_defs."). - - For instance, if we have an opaque function [f : int -> int], which - is used by the non-opaque function [g], we would generate (in Coq): - {[ - (* The module signature declaring the opaque definitions *) - module type OpaqueDefs = { - f_fwd : int -> int - ... (* Other definitions *) - } - - (* The definitions generated for the non-opaque definitions *) - module Funs (opaque: OpaqueDefs) = { - let g ... = - ... - opaque_defs.f_fwd - ... - } - ]} - - Upon using [f] in [g], we don't directly use the the name "f_fwd", - but prefix it with the "opaque_defs." identifier. - *) var_basename : StringSet.t -> string option -> ty -> string; (** Generates a variable basename. @@ -498,20 +467,6 @@ type names_map = { precisely which identifiers are mapped to the same name... *) names_set : StringSet.t; - opaque_ids : IdSet.t; - (** TODO: this is obsolete. Remove. - - The set of opaque definitions. - - See {!formatter.opaque_pre} for detailed explanations about why - we need to know which definitions are opaque to compute names. - - Also note that the opaque ids don't contain the ids of the assumed - definitions. In practice, assumed definitions are opaque_defs. However, they - are not grouped in the opaque module, meaning we never need to - prefix them (with, say, "opaque_defs."): we thus consider them as non-opaque - with regards to the names map. - *) } let empty_names_map : names_map = @@ -519,7 +474,6 @@ let empty_names_map : names_map = id_to_name = IdMap.empty; name_to_id = StringMap.empty; names_set = StringSet.empty; - opaque_ids = IdSet.empty; } (** Small helper to report name collision *) @@ -547,8 +501,8 @@ let names_map_check_collision (id_to_string : id -> string) (id : id) (* There is a clash: print a nice debugging message for the user *) report_name_collision id_to_string clash id name -let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id) - (name : string) (nm : names_map) : names_map = +let names_map_add (id_to_string : id -> string) (id : id) (name : string) + (nm : names_map) : names_map = (* Check if there is a clash *) names_map_check_collision id_to_string id name nm; (* Sanity check *) @@ -564,32 +518,24 @@ let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id) let id_to_name = IdMap.add id name nm.id_to_name in let name_to_id = StringMap.add name id nm.name_to_id in let names_set = StringSet.add name nm.names_set in - let opaque_ids = - if is_opaque then IdSet.add id nm.opaque_ids else nm.opaque_ids - in - { id_to_name; name_to_id; names_set; opaque_ids } + { id_to_name; name_to_id; names_set } let names_map_add_assumed_type (id_to_string : id -> string) (id : assumed_ty) (name : string) (nm : names_map) : names_map = - let is_opaque = false in - names_map_add id_to_string is_opaque (TypeId (Assumed id)) name nm + names_map_add id_to_string (TypeId (Assumed id)) name nm let names_map_add_assumed_struct (id_to_string : id -> string) (id : assumed_ty) (name : string) (nm : names_map) : names_map = - let is_opaque = false in - names_map_add id_to_string is_opaque (StructId (Assumed id)) name nm + names_map_add id_to_string (StructId (Assumed id)) name nm let names_map_add_assumed_variant (id_to_string : id -> string) (id : assumed_ty) (variant_id : VariantId.id) (name : string) (nm : names_map) : names_map = - let is_opaque = false in - names_map_add id_to_string is_opaque - (VariantId (Assumed id, variant_id)) - name nm + names_map_add id_to_string (VariantId (Assumed id, variant_id)) name nm -let names_map_add_function (id_to_string : id -> string) (is_opaque : bool) - (fid : fun_id) (name : string) (nm : names_map) : names_map = - names_map_add id_to_string is_opaque (FunId fid) name nm +let names_map_add_function (id_to_string : id -> string) (fid : fun_id) + (name : string) (nm : names_map) : names_map = + names_map_add id_to_string (FunId fid) name nm (** The unsafe names map stores mappings from identifiers to names which might collide. For some backends and some names, it might be acceptable to have @@ -667,14 +613,6 @@ type extraction_ctx = { fmt : formatter; indent_incr : int; (** The indent increment we insert whenever we need to indent more *) - use_opaque_pre : bool; - (** Do we use the "opaque_defs." prefix for the opaque definitions? - - Opaque function definitions might refer opaque types: if we are in the - opaque module, we musn't use the "opaque_defs." prefix, otherwise we - use it. - Also see {!names_map.opaque_ids}. - *) use_dep_ite : bool; (** For Lean: do we use dependent-if then else expressions? @@ -702,6 +640,19 @@ type extraction_ctx = { functions_with_decreases_clause : PureUtils.FunLoopIdSet.t; trans_trait_decls : Pure.trait_decl Pure.TraitDeclId.Map.t; trans_trait_impls : Pure.trait_impl Pure.TraitImplId.Map.t; + types_filter_type_args_map : bool list TypeDeclId.Map.t; + (** The map to filter the type arguments for the builtin type + definitions. + + We need this for type `Vec`, for instance, which takes a useless + (in the context of the type translation) type argument for the + allocator which is used, and which we want to remove. + + TODO: it would be cleaner to filter those types in a micro-pass, + rather than at code generation time. + *) + funs_filter_type_args_map : bool list FunDeclId.Map.t; + (** Same as {!types_filter_type_args_map}, but for functions *) } (** Debugging function, used when communicating name collisions to the user, @@ -803,15 +754,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 +777,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 -> ( @@ -890,8 +835,7 @@ let allow_collisions (id : id) : bool = !Config.record_fields_short_names | _ -> false -let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx) - : extraction_ctx = +let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = (* The id_to_string function to print nice debugging messages if there are * collisions *) let id_to_string (id : id) : string = id_to_string id ctx in @@ -908,7 +852,6 @@ let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx) others (ex.: fields and keywords). *) if allow_collisions id then ( - assert (not is_opaque); (* Check with the ids which are considered to be strict on collisions *) names_map_check_collision id_to_string id name ctx.strict_names_map; { @@ -922,16 +865,13 @@ let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx) *) let strict_names_map = if strict_collisions id then - names_map_add id_to_string is_opaque id name ctx.strict_names_map + names_map_add id_to_string id name ctx.strict_names_map else ctx.strict_names_map in - let names_map = - names_map_add id_to_string is_opaque id name ctx.names_map - in + let names_map = names_map_add id_to_string id name ctx.names_map in { ctx with strict_names_map; names_map } -(** [with_opaque_pre]: if [true] and the definition is opaque, add the opaque prefix *) -let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string = +let ctx_get (id : id) (ctx : extraction_ctx) : string = (* We do not use the same name map if we allow/disallow collisions *) let map_to_string (m : string IdMap.t) : string = "[\n" @@ -957,9 +897,7 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string = else let m = ctx.names_map.id_to_name in match IdMap.find_opt id m with - | Some s -> - let is_opaque = IdSet.mem id ctx.names_map.opaque_ids in - if with_opaque_pre && is_opaque then ctx.fmt.opaque_pre () ^ s else s + | Some s -> s | None -> let err = "Could not find: " ^ id_to_string id ctx ^ "\nNames map:\n" @@ -969,53 +907,38 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string = if !Config.extract_fail_hard then raise (Failure err) else "(ERROR: \"" ^ id_to_string id ctx ^ "\")" -let ctx_get_global (with_opaque_pre : bool) (id : A.GlobalDeclId.id) - (ctx : extraction_ctx) : string = - ctx_get with_opaque_pre (GlobalId id) ctx +let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = + ctx_get (GlobalId id) ctx -let ctx_get_function (with_opaque_pre : bool) (id : fun_id) - (ctx : extraction_ctx) : string = - ctx_get with_opaque_pre (FunId id) ctx +let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string = + ctx_get (FunId id) ctx -let ctx_get_local_function (with_opaque_pre : bool) (id : A.FunDeclId.id) - (lp : LoopId.id option) (rg : RegionGroupId.id option) - (ctx : extraction_ctx) : string = - ctx_get_function with_opaque_pre (FromLlbc (FunId (Regular id), lp, rg)) ctx +let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option) + (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = + ctx_get_function (FromLlbc (FunId (Regular id), lp, rg)) ctx -let ctx_get_type (with_opaque_pre : bool) (id : type_id) (ctx : extraction_ctx) - : string = +let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string = assert (id <> Tuple); - ctx_get with_opaque_pre (TypeId id) ctx + ctx_get (TypeId id) ctx -let ctx_get_local_type (with_opaque_pre : bool) (id : TypeDeclId.id) - (ctx : extraction_ctx) : string = - ctx_get_type with_opaque_pre (AdtId id) ctx +let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string = + ctx_get_type (AdtId id) ctx let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string = - (* In practice, the assumed types are opaque. However, assumed types - are never grouped in the opaque module, meaning we never need to - prefix them: we thus consider them as non-opaque with regards to the - names map. - *) - let is_opaque = false in - ctx_get_type is_opaque (Assumed id) ctx + ctx_get_type (Assumed id) ctx let ctx_get_trait_self_clause (ctx : extraction_ctx) : string = - let with_opaque_pre = false in - ctx_get with_opaque_pre TraitSelfClauseId ctx + ctx_get TraitSelfClauseId ctx -let ctx_get_trait_decl (with_opaque_pre : bool) (id : trait_decl_id) - (ctx : extraction_ctx) : string = - ctx_get with_opaque_pre (TraitDeclId id) ctx +let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string = + ctx_get (TraitDeclId id) ctx -let ctx_get_trait_impl (with_opaque_pre : bool) (id : trait_impl_id) - (ctx : extraction_ctx) : string = - ctx_get with_opaque_pre (TraitImplId id) ctx +let ctx_get_trait_impl (id : trait_impl_id) (ctx : extraction_ctx) : string = + ctx_get (TraitImplId id) ctx let ctx_get_trait_item (id : trait_decl_id) (item_name : string) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (TraitItemId (id, item_name)) ctx + ctx_get (TraitItemId (id, item_name)) ctx let ctx_get_trait_const (id : trait_decl_id) (item_name : string) (ctx : extraction_ctx) : string = @@ -1027,83 +950,69 @@ let ctx_get_trait_type (id : trait_decl_id) (item_name : string) let ctx_get_trait_method (id : trait_decl_id) (item_name : string) (rg_id : T.RegionGroupId.id option) (ctx : extraction_ctx) : string = - let with_opaque_pre = false in - ctx_get with_opaque_pre (TraitMethodId (id, item_name, rg_id)) ctx + ctx_get (TraitMethodId (id, item_name, rg_id)) ctx let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id) (ctx : extraction_ctx) : string = - let with_opaque_pre = false in - ctx_get with_opaque_pre (TraitParentClauseId (id, clause)) ctx + ctx_get (TraitParentClauseId (id, clause)) ctx let ctx_get_trait_item_clause (id : trait_decl_id) (item : string) (clause : trait_clause_id) (ctx : extraction_ctx) : string = - let with_opaque_pre = false in - ctx_get with_opaque_pre (TraitItemClauseId (id, item, clause)) ctx + ctx_get (TraitItemClauseId (id, item, clause)) ctx let ctx_get_var (id : VarId.id) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (VarId id) ctx + ctx_get (VarId id) ctx let ctx_get_type_var (id : TypeVarId.id) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (TypeVarId id) ctx + ctx_get (TypeVarId id) ctx let ctx_get_const_generic_var (id : ConstGenericVarId.id) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (ConstGenericVarId id) ctx + ctx_get (ConstGenericVarId id) ctx let ctx_get_local_trait_clause (id : TraitClauseId.id) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (LocalTraitClauseId id) ctx + ctx_get (LocalTraitClauseId id) ctx let ctx_get_field (type_id : type_id) (field_id : FieldId.id) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (FieldId (type_id, field_id)) ctx + ctx_get (FieldId (type_id, field_id)) ctx -let ctx_get_struct (with_opaque_pre : bool) (def_id : type_id) - (ctx : extraction_ctx) : string = - ctx_get with_opaque_pre (StructId def_id) ctx +let ctx_get_struct (def_id : type_id) (ctx : extraction_ctx) : string = + ctx_get (StructId def_id) ctx let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (VariantId (def_id, variant_id)) ctx + ctx_get (VariantId (def_id, variant_id)) ctx let ctx_get_decreases_proof (def_id : A.FunDeclId.id) (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (DecreasesProofId (Regular def_id, loop_id)) ctx + ctx_get (DecreasesProofId (Regular def_id, loop_id)) ctx let ctx_get_termination_measure (def_id : A.FunDeclId.id) (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = - let is_opaque = false in - ctx_get is_opaque (TerminationMeasureId (Regular def_id, loop_id)) ctx + ctx_get (TerminationMeasureId (Regular def_id, loop_id)) ctx (** Generate a unique type variable name and add it to the context *) let ctx_add_type_var (basename : string) (id : TypeVarId.id) (ctx : extraction_ctx) : extraction_ctx * string = - let is_opaque = false in let name = ctx.fmt.type_var_basename ctx.names_map.names_set basename in let name = basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name in - let ctx = ctx_add is_opaque (TypeVarId id) name ctx in + let ctx = ctx_add (TypeVarId id) name ctx in (ctx, name) (** Generate a unique const generic variable name and add it to the context *) let ctx_add_const_generic_var (basename : string) (id : ConstGenericVarId.id) (ctx : extraction_ctx) : extraction_ctx * string = - let is_opaque = false in let name = ctx.fmt.const_generic_var_basename ctx.names_map.names_set basename in let name = basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name in - let ctx = ctx_add is_opaque (ConstGenericVarId id) name ctx in + let ctx = ctx_add (ConstGenericVarId id) name ctx in (ctx, name) (** See {!ctx_add_type_var} *) @@ -1116,31 +1025,28 @@ let ctx_add_type_vars (vars : (string * TypeVarId.id) list) (** Generate a unique variable name and add it to the context *) let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) : extraction_ctx * string = - let is_opaque = false in let name = basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename in - let ctx = ctx_add is_opaque (VarId id) name ctx in + let ctx = ctx_add (VarId id) name ctx in (ctx, name) (** Generate a unique variable name for the trait self clause and add it to the context *) let ctx_add_trait_self_clause (ctx : extraction_ctx) : extraction_ctx * string = - let is_opaque = false in let basename = ctx.fmt.trait_self_clause_basename in let name = basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename in - let ctx = ctx_add is_opaque TraitSelfClauseId name ctx in + let ctx = ctx_add TraitSelfClauseId name ctx in (ctx, name) (** Generate a unique trait clause name and add it to the context *) let ctx_add_local_trait_clause (basename : string) (id : TraitClauseId.id) (ctx : extraction_ctx) : extraction_ctx * string = - let is_opaque = false in let name = basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename in - let ctx = ctx_add is_opaque (LocalTraitClauseId id) name ctx in + let ctx = ctx_add (LocalTraitClauseId id) name ctx in (ctx, name) (** See {!ctx_add_var} *) @@ -1186,107 +1092,41 @@ 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 let name = ctx.fmt.decreases_proof_name def.def_id def.basename def.num_loops def.loop_id in - ctx_add is_opaque - (DecreasesProofId (Regular def.def_id, def.loop_id)) - name ctx + ctx_add (DecreasesProofId (Regular def.def_id, def.loop_id)) name ctx let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = - let is_opaque = false in let name = ctx.fmt.termination_measure_name def.def_id def.basename def.num_loops def.loop_id in - ctx_add is_opaque - (TerminationMeasureId (Regular def.def_id, def.loop_id)) - name ctx + ctx_add (TerminationMeasureId (Regular def.def_id, def.loop_id)) name ctx let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = (* TODO: update once the body id can be an option *) - let is_opaque = false in let decl = GlobalId def.def_id in (* Check if the global corresponds to an assumed global that we should map 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 + ctx_add decl name ctx | None -> (* Not the case: "standard" registration *) let name = ctx.fmt.global_name def.name in let body = FunId (FromLlbc (FunId (Regular def.body_id), None, None)) in - let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in - let ctx = ctx_add is_opaque body (name ^ "_body") ctx in + let ctx = ctx_add decl (name ^ "_c") ctx in + let ctx = ctx_add body (name ^ "_body") ctx in ctx let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl) @@ -1314,6 +1154,7 @@ let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl) ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info (keep_fwd, num_backs) +(* TODO: move to Extract *) let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = (* Sanity check: the function should not be a global body - those are handled @@ -1323,11 +1164,10 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl) let def_id = def.def_id in let { keep_fwd; fwd = _; backs } = trans_group in let num_backs = List.length backs in - let is_opaque = def.body = None in (* Add the function name *) let def_name = ctx_compute_fun_name trans_group def ctx in let fun_id = (Pure.FunId (Regular def_id), def.loop_id, def.back_id) in - let ctx = ctx_add is_opaque (FunId (FromLlbc fun_id)) def_name ctx in + let ctx = ctx_add (FunId (FromLlbc fun_id)) def_name ctx in (* Add the name info *) { ctx with @@ -1336,91 +1176,6 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl) ctx.fun_name_info; } -let ctx_add_trait_decl (d : trait_decl) (ctx : extraction_ctx) : extraction_ctx - = - let is_opaque = false in - let name = ctx.fmt.trait_decl_name d in - ctx_add is_opaque (TraitDeclId d.def_id) name ctx - -let ctx_add_trait_impl (d : trait_impl) (ctx : extraction_ctx) : extraction_ctx - = - (* We need to lookup the trait decl that is implemented by the trait impl *) - let decl = - Pure.TraitDeclId.Map.find d.impl_trait.trait_decl_id ctx.trans_trait_decls - in - (* Compute the name *) - let is_opaque = false in - let name = ctx.fmt.trait_impl_name decl d in - ctx_add is_opaque (TraitImplId d.def_id) name ctx - -let ctx_add_trait_const (d : trait_decl) (item : string) (ctx : extraction_ctx) - : extraction_ctx = - let is_opaque = false in - let name = ctx.fmt.trait_const_name d item in - (* Add a prefix if necessary *) - let name = - if !Config.record_fields_short_names then name - else ctx.fmt.trait_decl_name d ^ name - in - ctx_add is_opaque (TraitItemId (d.def_id, item)) name ctx - -let ctx_add_trait_type (d : trait_decl) (item : string) (ctx : extraction_ctx) : - extraction_ctx = - let is_opaque = false in - let name = ctx.fmt.trait_type_name d item in - (* Add a prefix if necessary *) - let name = - if !Config.record_fields_short_names then name - else ctx.fmt.trait_decl_name d ^ name - in - ctx_add is_opaque (TraitItemId (d.def_id, item)) name ctx - -let ctx_add_trait_method (d : trait_decl) (item_name : string) (f : fun_decl) - (ctx : extraction_ctx) : extraction_ctx = - (* We do something special: we use the base name but remove everything - but the crate (because [get_name] removes it) and the last ident. - This allows us to reuse the [ctx_compute_fun_decl] function. - *) - let basename : name = - match (f.basename : name) with - | Ident crate :: name -> Ident crate :: [ Collections.List.last name ] - | _ -> raise (Failure "Unexpected") - in - let f = { f with basename } in - let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in - let name = ctx_compute_fun_name trans f ctx in - (* Add a prefix if necessary *) - let name = - if !Config.record_fields_short_names then name - else ctx.fmt.trait_decl_name d ^ "_" ^ name - in - let is_opaque = false in - ctx_add is_opaque (TraitMethodId (d.def_id, item_name, f.back_id)) name ctx - -let ctx_add_trait_parent_clause (d : trait_decl) (clause : trait_clause) - (ctx : extraction_ctx) : extraction_ctx = - let is_opaque = false in - let name = ctx.fmt.trait_parent_clause_name d clause in - (* Add a prefix if necessary *) - let name = - if !Config.record_fields_short_names then name - else ctx.fmt.trait_decl_name d ^ name - in - ctx_add is_opaque (TraitParentClauseId (d.def_id, clause.clause_id)) name ctx - -let ctx_add_trait_type_clause (d : trait_decl) (item : string) - (clause : trait_clause) (ctx : extraction_ctx) : extraction_ctx = - let is_opaque = false in - let name = ctx.fmt.trait_type_clause_name d item clause in - (* Add a prefix if necessary *) - let name = - if !Config.record_fields_short_names then name - else ctx.fmt.trait_decl_name d ^ name - in - ctx_add is_opaque - (TraitItemClauseId (d.def_id, item, clause.clause_id)) - name ctx - type names_map_init = { keywords : string list; assumed_adts : (assumed_ty * string) list; @@ -1445,12 +1200,11 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map = let name_to_id = StringMap.of_list (List.map (fun x -> (x, UnknownId)) keywords) in - let opaque_ids = IdSet.empty in (* We fist initialize [id_to_name] as empty, because the id of a keyword is [UnknownId]. * Also note that we don't need this mapping for keywords: we insert keywords only * to check collisions. *) let id_to_name = IdMap.empty in - let nm = { id_to_name; name_to_id; names_set; opaque_ids } in + let nm = { id_to_name; name_to_id; names_set } in (* For debugging - we are creating bindings for assumed types and functions, so * it is ok if we simply use the "show" function (those aren't simply identified * by numbers) *) @@ -1487,15 +1241,8 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map = @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions in let nm = - (* In practice, the assumed function are opaque. However, assumed functions - are never grouped in the opaque module, meaning we never need to - prefix them: we thus consider them as non-opaque with regards to the - names map. - *) - let is_opaque = false in List.fold_left - (fun nm (fid, name) -> - names_map_add_function id_to_string is_opaque fid name nm) + (fun nm (fid, name) -> names_map_add_function id_to_string fid name nm) nm assumed_functions in (* Return *) diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml new file mode 100644 index 00000000..9cc7c226 --- /dev/null +++ b/compiler/ExtractBuiltin.ml @@ -0,0 +1,560 @@ +(** This file declares external identifiers that we catch to map them to + definitions coming from the standard libraries in our backends. + + TODO: there misses trait **implementations** + *) + +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) +module SimpleNameSet = Collections.MakeSet (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 } +[@@deriving show] + +type builtin_enum_variant_info = { + rust_variant_name : string; + extract_variant_name : string; + fields : string list option; +} +[@@deriving show] + +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 *) +[@@deriving show] + +type builtin_type_info = { + rust_name : string list; + 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; +} +[@@deriving show] + +(** 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 -> (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; +} +[@@deriving show] + +(** 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 list * 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 -> "core_mem_replace_fwd" + | Lean -> "core.mem.replace"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_mem_replace_back" + | Lean -> "core.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"); + }; + ] ); + ( [ "alloc"; "boxed"; "Box"; "deref" ], + Some [ true; false ], + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "alloc_boxed_box_deref" + | Lean -> "alloc.boxed.Box.deref"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_back" + | Lean -> "alloc.boxed.Box.deref_back"); + }; + ] ); + ( [ "alloc"; "boxed"; "Box"; "deref_mut" ], + Some [ true; false ], + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut" + | Lean -> "alloc.boxed.Box.deref_mut"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut_back" + | Lean -> "alloc.boxed.Box.deref_mut_back"); + }; + ] ); + ] + +let mk_builtin_funs_map () = + SimpleNameMap.of_list + (List.map + (fun (name, filter, info) -> (name, (filter, info))) + (builtin_funs ())) + +let builtin_funs_map = mk_memoized mk_builtin_funs_map + +let builtin_non_fallible_funs = + [ "alloc::boxed::Box::deref"; "alloc::boxed::Box::deref_mut" ] + +let builtin_non_fallible_funs_set = + SimpleNameSet.of_list + (List.map string_to_simple_name builtin_non_fallible_funs) + +type builtin_trait_decl_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) list; +} +[@@deriving show] + +let builtin_trait_decls_info () = + 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" ); + ( 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" ); + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back" + | Lean -> "index_mut_back" ); + ] ); + ]; + }; + ] + +let mk_builtin_trait_decls_map () = + SimpleNameMap.of_list + (List.map + (fun info -> (string_to_simple_name info.rust_name, info)) + (builtin_trait_decls_info ())) + +let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map + +(* TODO: generalize this. + + For now, the key is: + - name of the impl (ex.: "alloc.boxed.Boxed") + - name of the implemented trait (ex.: "core.ops.deref.Deref" +*) +type simple_name_pair = simple_name * simple_name [@@deriving show, ord] + +module SimpleNamePairOrd = struct + type t = simple_name_pair + + let compare = compare_simple_name_pair + let to_string = show_simple_name_pair + let pp_t = pp_simple_name_pair + let show_t = show_simple_name_pair +end + +module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd) + +let builtin_trait_impls_info () : ((string list * string list) * string) list = + [ + (* core::ops::Deref<alloc::boxed::Box<T>> *) + ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]), + "alloc.boxed.Box.coreOpsDerefInst" ); + (* core::ops::DerefMut<alloc::boxed::Box<T>> *) + ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]), + "alloc.boxed.Box.coreOpsDerefMutInst" ); + ] + +let mk_builtin_trait_impls_map () = + SimpleNamePairMap.of_list (builtin_trait_impls_info ()) + +let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 9f82b5c9..1273f57d 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -106,7 +106,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..e0c4703b 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 @@ -1196,6 +1108,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) match call.func.func with | FunId (Regular fid) -> let def = C.ctx_lookup_fun_decl ctx fid in + log#ldebug + (lazy + ("fun call:\n- call: " ^ call_to_string ctx call + ^ "\n- call.generics:\n" + ^ egeneric_args_to_string ctx call.func.generics + ^ "\n- def.signature:\n" + ^ fun_sig_to_string ctx def.A.signature)); let tr_self = T.UnknownTrait __FUNCTION__ in let inst_sg = instantiate_fun_sig ctx call.func.generics tr_self def.A.signature @@ -1531,7 +1450,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..f3e6cbe2 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,44 @@ 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_no_disambiguators_to_string def.name, rg_id) + with + | "alloc::boxed::Box::deref", None -> (* [Box::deref] forward is the identity *) let arg, args = Collections.List.pop args in mk_apps arg args - | BoxDeref, Some _ -> + | "alloc::boxed::Box::deref", Some _ -> (* [Box::deref] backward is [()] (doesn't give back anything) *) assert (args = []); mk_unit_rvalue - | BoxDerefMut, None -> + | "alloc::boxed::Box::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::boxed::Box::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 +1569,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..35dff9e6 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 @@ -631,91 +654,133 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) *) let export_functions_group (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit = - (* Utility to check a function has a decrease clause *) - let has_decreases_clause (def : Pure.fun_decl) : bool = - PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id) - ctx.functions_with_decreases_clause + (* 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 funs_map = builtin_funs_map () in + List.map + (fun (trans : pure_fun_translation) -> + let sname = name_to_simple_name trans.fwd.f.basename in + SimpleNameMap.find_opt sname funs_map <> None) + pure_ls in - (* Extract the decrease clauses template bodies *) - if config.extract_template_decreases_clauses then - List.iter - (fun { fwd; _ } -> - (* We only generate decreases clauses for the forward functions, because - the termination argument should only depend on the forward inputs. - The backward functions thus use the same decreases clauses as the - forward function. - - Rem.: we might filter backward functions in {!PureMicroPasses}, but - we don't remove forward functions. Instead, we remember if we should - filter those functions at extraction time with a boolean (see the - type of the [pure_ls] input parameter). - *) - let extract_decrease decl = - let has_decr_clause = has_decreases_clause decl in - if has_decr_clause then - match !Config.backend with - | Lean -> - Extract.extract_template_lean_termination_and_decreasing ctx fmt - decl - | FStar -> - Extract.extract_template_fstar_decreases_clause ctx fmt decl - | Coq -> - raise (Failure "Coq doesn't have decreases/termination clauses") - | HOL4 -> - raise - (Failure "HOL4 doesn't have decreases/termination clauses") - in - extract_decrease fwd.f; - List.iter extract_decrease fwd.loops) - pure_ls; - - (* Concatenate the function definitions, filtering the useless forward - * functions. *) - let decls = - List.concat - (List.map - (fun { keep_fwd; fwd; backs } -> - let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in - let backs : Pure.fun_decl list = - List.concat - (List.map (fun back -> List.append back.loops [ back.f ]) backs) - in - List.append fwd backs) - pure_ls) - in + if List.exists (fun b -> b) builtin then + (* Sanity check *) + assert (List.for_all (fun b -> b) builtin) + else + (* Utility to check a function has a decrease clause *) + let has_decreases_clause (def : Pure.fun_decl) : bool = + PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id) + ctx.functions_with_decreases_clause + in - (* Extract the function definitions *) - (if config.extract_fun_decls then - (* Group the mutually recursive definitions *) - let subgroups = ReorderDecls.group_reorder_fun_decls decls in + (* Extract the decrease clauses template bodies *) + if config.extract_template_decreases_clauses then + List.iter + (fun { fwd; _ } -> + (* We only generate decreases clauses for the forward functions, because + the termination argument should only depend on the forward inputs. + The backward functions thus use the same decreases clauses as the + forward function. + + Rem.: we might filter backward functions in {!PureMicroPasses}, but + we don't remove forward functions. Instead, we remember if we should + filter those functions at extraction time with a boolean (see the + type of the [pure_ls] input parameter). + *) + let extract_decrease decl = + let has_decr_clause = has_decreases_clause decl in + if has_decr_clause then + match !Config.backend with + | Lean -> + Extract.extract_template_lean_termination_and_decreasing ctx + fmt decl + | FStar -> + Extract.extract_template_fstar_decreases_clause ctx fmt decl + | Coq -> + raise + (Failure "Coq doesn't have decreases/termination clauses") + | HOL4 -> + raise + (Failure "HOL4 doesn't have decreases/termination clauses") + in + extract_decrease fwd.f; + List.iter extract_decrease fwd.loops) + pure_ls; + + (* Concatenate the function definitions, filtering the useless forward + * functions. *) + let decls = + List.concat + (List.map + (fun { keep_fwd; fwd; backs } -> + let fwd = + if keep_fwd then List.append fwd.loops [ fwd.f ] else [] + in + let backs : Pure.fun_decl list = + List.concat + (List.map + (fun back -> List.append back.loops [ back.f ]) + backs) + in + List.append fwd backs) + pure_ls) + in - (* Extract the subgroups *) - let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit = - export_functions_group_scc fmt config ctx is_rec decls - in - List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups); - - (* Insert unit tests if necessary *) - if config.test_trans_unit_functions then - List.iter - (fun trans -> - if trans.keep_fwd then - Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f) - pure_ls + (* Extract the function definitions *) + (if config.extract_fun_decls then + (* Group the mutually recursive definitions *) + let subgroups = ReorderDecls.group_reorder_fun_decls decls in + + (* Extract the subgroups *) + let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit = + export_functions_group_scc fmt config ctx is_rec decls + in + List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups); + + (* Insert unit tests if necessary *) + if config.test_trans_unit_functions then + List.iter + (fun trans -> + if trans.keep_fwd then + Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f) + pure_ls (** Export a trait declaration. *) let export_trait_decl (fmt : Format.formatter) (_config : gen_config) (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit = let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in - let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in - Extract.extract_trait_decl ctx fmt trait_decl + (* Check if the trait declaration is builtin, in which case we ignore it *) + let open ExtractBuiltin in + let sname = name_to_simple_name trait_decl.name in + if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then + let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in + Extract.extract_trait_decl ctx fmt trait_decl + else () (** Export a trait implementation. *) let export_trait_impl (fmt : Format.formatter) (_config : gen_config) (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit = + (* Lookup the definition *) let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in - Extract.extract_trait_impl ctx fmt trait_impl + let trait_decl = + Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id + ctx.trans_trait_decls + in + (* Check if the trait implementation is builtin *) + let builtin_info = + let open ExtractBuiltin in + let type_sname = name_to_simple_name trait_impl.name in + let trait_sname = name_to_simple_name trait_decl.name in + SimpleNamePairMap.find_opt (type_sname, trait_sname) + (builtin_trait_impls_map ()) + in + match builtin_info with + | None -> Extract.extract_trait_impl ctx fmt trait_impl + | Some _ -> () (** A generic utility to generate the extracted definitions: as we may want to split the definitions between different files (or not), we can control @@ -786,37 +851,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if config.extract_state_type && config.extract_fun_decls then export_state_type (); - (* Obsolete: (TODO: remove) For Lean we parameterize the entire development by a section - variable called opaque_defs, of type OpaqueDefs. The code below emits the type - definition for OpaqueDefs, which is a structure, in which each field is one of the - functions marked as Opaque. We emit the `structure ...` bit here, then rely on - `extract_fun_decl` to be aware of this, and skip the keyword (e.g. "axiom" or "val") - so as to generate valid syntax for records. - - We also generate such a structure only if there actually are opaque definitions. *) - let wrap_in_sig = - config.extract_opaque && config.extract_fun_decls - && !Config.wrap_opaque_in_sig - && - let _, opaque_funs = crate_has_opaque_decls ctx true in - opaque_funs - in - if wrap_in_sig then ( - (* We change the name of the structure depending on whether we *only* - extract opaque definitions, or if we extract all definitions *) - let struct_name = - if config.extract_transparent then "Definitions" else "OpaqueDefs" - in - Format.pp_print_break fmt 0 0; - Format.pp_open_vbox fmt ctx.indent_incr; - Format.pp_print_string fmt ("structure " ^ struct_name ^ " where"); - Format.pp_print_break fmt 0 0); List.iter export_decl_group ctx.crate.declarations; if config.extract_state_type && not config.extract_fun_decls then - export_state_type (); - - if wrap_in_sig then Format.pp_close_box fmt () + export_state_type () type extract_file_info = { filename : string; @@ -964,10 +1002,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (fun (id, _) -> strict_collisions id) (IdMap.bindings names_map.id_to_name) in - let is_opaque = false in List.fold_left (* id_to_string: we shouldn't need to use it *) - (fun m (id, n) -> names_map_add show_id is_opaque id n m) + (fun m (id, n) -> names_map_add show_id id n m) empty_names_map ids in @@ -1028,7 +1065,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : strict_names_map; fmt; indent_incr = 2; - use_opaque_pre = !Config.split_files; use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses; fun_name_info = PureUtils.RegularFunIdMap.empty; trait_decl_id = None (* None by default *); @@ -1038,6 +1074,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : trans_types; trans_funs; functions_with_decreases_clause = rec_functions; + types_filter_type_args_map = Pure.TypeDeclId.Map.empty; + funs_filter_type_args_map = Pure.FunDeclId.Map.empty; } in @@ -1324,7 +1362,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : interface = true; } in - let ctx = { ctx with use_opaque_pre = false } in let file_info = { filename = opaque_filename; 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 diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 884e62c4..a90d6ea2 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -54,7 +54,7 @@ def div_test (x : U32) (y : U32) : Result U32 := /- [no_nested_borrows::div_test1]: forward function -/ def div_test1 (x : U32) : Result U32 := - x / (U32.ofInt 2) + x / 2#u32 /- [no_nested_borrows::rem_test]: forward function -/ def rem_test (x : U32) (y : U32) : Result U32 := @@ -67,7 +67,7 @@ def cast_test (x : U32) : Result I32 := /- [no_nested_borrows::test2]: forward function -/ def test2 : Result Unit := do - let _ ← (U32.ofInt 23) + (U32.ofInt 44) + let _ ← 23#u32 + 44#u32 Result.ret () /- Unit test for [no_nested_borrows::test2] -/ @@ -82,10 +82,10 @@ def get_max (x : U32) (y : U32) : Result U32 := /- [no_nested_borrows::test3]: forward function -/ def test3 : Result Unit := do - let x ← get_max (U32.ofInt 4) (U32.ofInt 3) - let y ← get_max (U32.ofInt 10) (U32.ofInt 11) + let x ← get_max 4#u32 3#u32 + let y ← get_max 10#u32 11#u32 let z ← x + y - if not (z = (U32.ofInt 15)) + if not (z = 15#u32) then Result.fail Error.panic else Result.ret () @@ -95,8 +95,8 @@ def test3 : Result Unit := /- [no_nested_borrows::test_neg1]: forward function -/ def test_neg1 : Result Unit := do - let y ← - (I32.ofInt 3) - if not (y = (I32.ofInt (-(3:Int)))) + let y ← - 3#i32 + if not (y = (-(3:Int))#i32) then Result.fail Error.panic else Result.ret () @@ -105,7 +105,7 @@ def test_neg1 : Result Unit := /- [no_nested_borrows::refs_test1]: forward function -/ def refs_test1 : Result Unit := - if not ((I32.ofInt 1) = (I32.ofInt 1)) + if not (1#i32 = 1#i32) then Result.fail Error.panic else Result.ret () @@ -114,16 +114,16 @@ def refs_test1 : Result Unit := /- [no_nested_borrows::refs_test2]: forward function -/ def refs_test2 : Result Unit := - if not ((I32.ofInt 2) = (I32.ofInt 2)) + if not (2#i32 = 2#i32) then Result.fail Error.panic else - if not ((I32.ofInt 0) = (I32.ofInt 0)) + if not (0#i32 = 0#i32) then Result.fail Error.panic else - if not ((I32.ofInt 2) = (I32.ofInt 2)) + if not (2#i32 = 2#i32) then Result.fail Error.panic else - if not ((I32.ofInt 2) = (I32.ofInt 2)) + if not (2#i32 = 2#i32) then Result.fail Error.panic else Result.ret () @@ -167,8 +167,8 @@ def test_panic (b : Bool) : Result Unit := /- [no_nested_borrows::test_copy_int]: forward function -/ def test_copy_int : Result Unit := do - let y ← copy_int (I32.ofInt 0) - if not ((I32.ofInt 0) = y) + let y ← copy_int 0#i32 + if not (0#i32 = y) then Result.fail Error.panic else Result.ret () @@ -185,7 +185,7 @@ def is_cons (T : Type) (l : List T) : Result Bool := def test_is_cons : Result Unit := do let l := List.Nil - let b ← is_cons I32 (List.Cons (I32.ofInt 0) l) + let b ← is_cons I32 (List.Cons 0#i32 l) if not b then Result.fail Error.panic else Result.ret () @@ -203,9 +203,9 @@ def split_list (T : Type) (l : List T) : Result (T × (List T)) := def test_split_list : Result Unit := do let l := List.Nil - let p ← split_list I32 (List.Cons (I32.ofInt 0) l) + let p ← split_list I32 (List.Cons 0#i32 l) let (hd, _) := p - if not (hd = (I32.ofInt 0)) + if not (hd = 0#i32) then Result.fail Error.panic else Result.ret () @@ -228,19 +228,18 @@ def choose_back /- [no_nested_borrows::choose_test]: forward function -/ def choose_test : Result Unit := do - let z ← choose I32 true (I32.ofInt 0) (I32.ofInt 0) - let z0 ← z + (I32.ofInt 1) - if not (z0 = (I32.ofInt 1)) + let z ← choose I32 true 0#i32 0#i32 + let z0 ← z + 1#i32 + if not (z0 = 1#i32) then Result.fail Error.panic else do - let (x, y) ← choose_back I32 true (I32.ofInt 0) (I32.ofInt 0) z0 - if not (x = (I32.ofInt 1)) + let (x, y) ← choose_back I32 true 0#i32 0#i32 z0 + if not (x = 1#i32) then Result.fail Error.panic - else - if not (y = (I32.ofInt 0)) - then Result.fail Error.panic - else Result.ret () + else if not (y = 0#i32) + then Result.fail Error.panic + else Result.ret () /- Unit test for [no_nested_borrows::choose_test] -/ #assert (choose_test == .ret ()) @@ -268,17 +267,17 @@ divergent def list_length (T : Type) (l : List T) : Result U32 := match l with | List.Cons t l1 => do let i ← list_length T l1 - (U32.ofInt 1) + i - | List.Nil => Result.ret (U32.ofInt 0) + 1#u32 + i + | List.Nil => Result.ret 0#u32 /- [no_nested_borrows::list_nth_shared]: forward function -/ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T := match l with | List.Cons x tl => - if i = (U32.ofInt 0) + if i = 0#u32 then Result.ret x else do - let i0 ← i - (U32.ofInt 1) + let i0 ← i - 1#u32 list_nth_shared T tl i0 | List.Nil => Result.fail Error.panic @@ -286,10 +285,10 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T := divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T := match l with | List.Cons x tl => - if i = (U32.ofInt 0) + if i = 0#u32 then Result.ret x else do - let i0 ← i - (U32.ofInt 1) + let i0 ← i - 1#u32 list_nth_mut T tl i0 | List.Nil => Result.fail Error.panic @@ -298,11 +297,11 @@ divergent def list_nth_mut_back (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) := match l with | List.Cons x tl => - if i = (U32.ofInt 0) + if i = 0#u32 then Result.ret (List.Cons ret0 tl) else do - let i0 ← i - (U32.ofInt 1) + let i0 ← i - 1#u32 let tl0 ← list_nth_mut_back T tl i0 ret0 Result.ret (List.Cons x tl0) | List.Nil => Result.fail Error.panic @@ -324,47 +323,42 @@ def list_rev (T : Type) (l : List T) : Result (List T) := def test_list_functions : Result Unit := do let l := List.Nil - let l0 := List.Cons (I32.ofInt 2) l - let l1 := List.Cons (I32.ofInt 1) l0 - let i ← list_length I32 (List.Cons (I32.ofInt 0) l1) - if not (i = (U32.ofInt 3)) + let l0 := List.Cons 2#i32 l + let l1 := List.Cons 1#i32 l0 + let i ← list_length I32 (List.Cons 0#i32 l1) + if not (i = 3#u32) then Result.fail Error.panic else do - let i0 ← - list_nth_shared I32 (List.Cons (I32.ofInt 0) l1) (U32.ofInt 0) - if not (i0 = (I32.ofInt 0)) + let i0 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32 + if not (i0 = 0#i32) then Result.fail Error.panic else do - let i1 ← - list_nth_shared I32 (List.Cons (I32.ofInt 0) l1) (U32.ofInt 1) - if not (i1 = (I32.ofInt 1)) + let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32 + if not (i1 = 1#i32) then Result.fail Error.panic else do - let i2 ← - list_nth_shared I32 (List.Cons (I32.ofInt 0) l1) - (U32.ofInt 2) - if not (i2 = (I32.ofInt 2)) + let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32 + if not (i2 = 2#i32) then Result.fail Error.panic else do let ls ← - list_nth_mut_back I32 (List.Cons (I32.ofInt 0) l1) - (U32.ofInt 1) (I32.ofInt 3) - let i3 ← list_nth_shared I32 ls (U32.ofInt 0) - if not (i3 = (I32.ofInt 0)) + list_nth_mut_back I32 (List.Cons 0#i32 l1) 1#u32 3#i32 + let i3 ← list_nth_shared I32 ls 0#u32 + if not (i3 = 0#i32) then Result.fail Error.panic else do - let i4 ← list_nth_shared I32 ls (U32.ofInt 1) - if not (i4 = (I32.ofInt 3)) + let i4 ← list_nth_shared I32 ls 1#u32 + if not (i4 = 3#i32) then Result.fail Error.panic else do - let i5 ← list_nth_shared I32 ls (U32.ofInt 2) - if not (i5 = (I32.ofInt 2)) + let i5 ← list_nth_shared I32 ls 2#u32 + if not (i5 = 2#i32) then Result.fail Error.panic else Result.ret () @@ -427,15 +421,15 @@ structure StructWithTuple (T1 T2 : Type) where /- [no_nested_borrows::new_tuple1]: forward function -/ def new_tuple1 : Result (StructWithTuple U32 U32) := - Result.ret { p := ((U32.ofInt 1), (U32.ofInt 2)) } + Result.ret { p := (1#u32, 2#u32) } /- [no_nested_borrows::new_tuple2]: forward function -/ def new_tuple2 : Result (StructWithTuple I16 I16) := - Result.ret { p := ((I16.ofInt 1), (I16.ofInt 2)) } + Result.ret { p := (1#i16, 2#i16) } /- [no_nested_borrows::new_tuple3]: forward function -/ def new_tuple3 : Result (StructWithTuple U64 I64) := - Result.ret { p := ((U64.ofInt 1), (I64.ofInt 2)) } + Result.ret { p := (1#u64, 2#i64) } /- [no_nested_borrows::StructWithPair] -/ structure StructWithPair (T1 T2 : Type) where @@ -443,31 +437,31 @@ structure StructWithPair (T1 T2 : Type) where /- [no_nested_borrows::new_pair1]: forward function -/ def new_pair1 : Result (StructWithPair U32 U32) := - Result.ret { p := { x := (U32.ofInt 1), y := (U32.ofInt 2) } } + Result.ret { p := { x := 1#u32, y := 2#u32 } } /- [no_nested_borrows::test_constants]: forward function -/ def test_constants : Result Unit := do let swt ← new_tuple1 let (i, _) := swt.p - if not (i = (U32.ofInt 1)) + if not (i = 1#u32) then Result.fail Error.panic else do let swt0 ← new_tuple2 let (i0, _) := swt0.p - if not (i0 = (I16.ofInt 1)) + if not (i0 = 1#i16) then Result.fail Error.panic else do let swt1 ← new_tuple3 let (i1, _) := swt1.p - if not (i1 = (U64.ofInt 1)) + if not (i1 = 1#u64) then Result.fail Error.panic else do let swp ← new_pair1 - if not (swp.p.x = (U32.ofInt 1)) + if not (swp.p.x = 1#u32) then Result.fail Error.panic else Result.ret () @@ -492,21 +486,21 @@ def test_mem_replace (px : U32) : Result U32 := /- [no_nested_borrows::test_shared_borrow_bool1]: forward function -/ def test_shared_borrow_bool1 (b : Bool) : Result U32 := if b - then Result.ret (U32.ofInt 0) - else Result.ret (U32.ofInt 1) + then Result.ret 0#u32 + else Result.ret 1#u32 /- [no_nested_borrows::test_shared_borrow_bool2]: forward function -/ def test_shared_borrow_bool2 : Result U32 := - Result.ret (U32.ofInt 0) + Result.ret 0#u32 /- [no_nested_borrows::test_shared_borrow_enum1]: forward function -/ def test_shared_borrow_enum1 (l : List U32) : Result U32 := match l with - | List.Cons i l0 => Result.ret (U32.ofInt 1) - | List.Nil => Result.ret (U32.ofInt 0) + | List.Cons i l0 => Result.ret 1#u32 + | List.Nil => Result.ret 0#u32 /- [no_nested_borrows::test_shared_borrow_enum2]: forward function -/ def test_shared_borrow_enum2 : Result U32 := - Result.ret (U32.ofInt 0) + Result.ret 0#u32 end no_nested_borrows |