summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Assumed.ml33
-rw-r--r--compiler/Extract.ml58
-rw-r--r--compiler/InterpreterStatements.ml2
-rw-r--r--compiler/PrintPure.ml1
-rw-r--r--compiler/PureMicroPasses.ml3
5 files changed, 62 insertions, 35 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index e0a2efea..572b0a24 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -347,20 +347,42 @@ module Sig = struct
let slice_subslice_sig (is_mut : bool) =
mk_array_slice_subslice_sig false is_mut
+
+ (** Helper:
+ [fn<T>(&'a [T]) -> usize]
+ *)
+ let slice_len_sig : A.fun_sig =
+ (* The signature fields *)
+ let region_params = [ region_param_0 ] in
+ let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
+ let type_params = [ type_param_0 ] (* <T> *) in
+ let inputs =
+ [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ]
+ in
+ let output = mk_usize_ty (* usize *) in
+ {
+ region_params;
+ num_early_bound_regions = 0;
+ regions_hierarchy;
+ type_params;
+ const_generic_params = empty_const_generic_params;
+ inputs;
+ output;
+ }
end
type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
(** The list of assumed functions and all their information:
- their signature
- - a boolean indicating whether the function can fail or not
+ - a boolean indicating whether the function can fail or not (if true: can fail)
- their name
Rk.: following what is written above, we don't include [Box::free].
-
+
Remark about the vector functions: for [Vec::len] to be correct and return
a [usize], we have to make sure that vectors are bounded by the max usize.
- Followingly, [Vec::push] is monadic.
+ As a consequence, [Vec::push] is monadic.
*)
let assumed_infos : assumed_info list =
let deref_pre = [ "core"; "ops"; "deref" ] in
@@ -402,11 +424,11 @@ let assumed_infos : assumed_info list =
(* Array to slice*)
( ArrayToSharedSlice,
Sig.array_to_slice_sig false,
- false,
+ true,
to_name [ "@ArrayToSharedSlice" ] );
( ArrayToMutSlice,
Sig.array_to_slice_sig true,
- false,
+ true,
to_name [ "@ArrayToMutSlice" ] );
(* Array Subslice *)
( ArraySharedSubslice,
@@ -432,6 +454,7 @@ let assumed_infos : assumed_info list =
Sig.slice_subslice_sig true,
true,
to_name [ "@SliceMutSubslice" ] );
+ (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]);
]
let get_assumed_info (id : A.assumed_fun_id) : assumed_info =
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1de7d68b..84d11895 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -261,7 +261,7 @@ let assumed_adts () : (assumed_ty * string) list =
let assumed_struct_constructors () : (assumed_ty * string) list =
match !backend with
- | Lean -> [ (Range, "Range.mk"); (Array, "Array.mk") ]
+ | Lean -> [ (Range, "Range.mk"); (Array, "Array.make") ]
| Coq -> [ (Range, "range.mk"); (Array, "array.mk") ]
| FStar -> [ (Range, "mkrange"); (Array, "mkarray") ]
| HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ]
@@ -329,21 +329,22 @@ let assumed_llbc_functions () :
(VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
(VecIndexMut, None, "vec_index_mut_fwd");
(VecIndexMut, rg0, "vec_index_mut_back");
- (ArraySharedIndex, None, "array_index");
- (ArrayMutIndex, None, "array_mut_index_fwd");
- (ArrayMutIndex, rg0, "array_mut_index_back");
+ (ArraySharedIndex, None, "array_index_shared");
+ (ArrayMutIndex, None, "array_index_mut_fwd");
+ (ArrayMutIndex, rg0, "array_index_mut_back");
(ArrayToSharedSlice, None, "array_to_slice");
(ArrayToMutSlice, None, "array_to_mut_slice_fwd");
(ArrayToMutSlice, rg0, "array_to_mut_slice_back");
- (ArraySharedSubslice, None, "array_subslice");
- (ArrayMutSubslice, None, "array_mut_subslice_fwd");
- (ArrayMutSubslice, rg0, "array_mut_subslice_back");
- (SliceSharedIndex, None, "slice_index");
- (SliceMutIndex, None, "slice_mut_index_fwd");
- (SliceMutIndex, rg0, "slice_mut_index_back");
- (SliceSharedSubslice, None, "slice_subslice");
- (SliceMutSubslice, None, "slice_mut_subslice_fwd");
- (SliceMutSubslice, rg0, "slice_mut_subslice_back");
+ (ArraySharedSubslice, None, "array_subslice_shared");
+ (ArrayMutSubslice, None, "array_subslice_mut_fwd");
+ (ArrayMutSubslice, rg0, "array_subslice_mut_back");
+ (SliceSharedIndex, None, "slice_index_shared");
+ (SliceMutIndex, None, "slice_index_mut_fwd");
+ (SliceMutIndex, rg0, "slice_index_mut_back");
+ (SliceSharedSubslice, None, "slice_subslice_mut");
+ (SliceMutSubslice, None, "slice_subslice_mut_fwd");
+ (SliceMutSubslice, rg0, "slice_subslice_mut_back");
+ (SliceLen, None, "slice_len_fwd");
]
| Lean ->
[
@@ -355,27 +356,28 @@ let assumed_llbc_functions () :
(VecInsert, None, "Vec.insert_fwd") (* Shouldn't be used *);
(VecInsert, rg0, "Vec.insert");
(VecLen, None, "Vec.len");
- (VecIndex, None, "Vec.index");
- (VecIndex, rg0, "Vec.index_back") (* shouldn't be used *);
+ (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");
- (* TODO: it would be good to only use Array.index (no Array.mut_index)
+ (* TODO: it would be good to only use Array.index (no Array.index_mut)
(same for subslice, etc.) *)
- (ArraySharedIndex, None, "Array.index");
- (ArrayMutIndex, None, "Array.mut_index");
- (ArrayMutIndex, rg0, "Array.mut_index_back");
+ (ArraySharedIndex, None, "Array.index_shared");
+ (ArrayMutIndex, None, "Array.index_mut");
+ (ArrayMutIndex, rg0, "Array.index_mut_back");
(ArrayToSharedSlice, None, "Array.to_slice");
(ArrayToMutSlice, None, "Array.to_mut_slice");
(ArrayToMutSlice, rg0, "Array.to_mut_slice_back");
- (ArraySharedSubslice, None, "Array.subslice");
- (ArrayMutSubslice, None, "Array.mut_subslice");
- (ArrayMutSubslice, rg0, "Array.mut_subslice_back");
- (SliceSharedIndex, None, "Slice.index");
- (SliceMutIndex, None, "Slice.mut_index");
- (SliceMutIndex, rg0, "Slice.mut_index_back");
- (SliceSharedSubslice, None, "Slice.subslice");
- (SliceMutSubslice, None, "Slice.mut_subslice");
- (SliceMutSubslice, rg0, "Slice.mut_subslice_back");
+ (ArraySharedSubslice, None, "Array.subslice_shared");
+ (ArrayMutSubslice, None, "Array.subslice_mut");
+ (ArrayMutSubslice, rg0, "Array.subslice_mut_back");
+ (SliceSharedIndex, None, "Slice.index_shared");
+ (SliceMutIndex, None, "Slice.index_mut");
+ (SliceMutIndex, rg0, "Slice.index_mut_back");
+ (SliceSharedSubslice, None, "Slice.subslice_shared");
+ (SliceMutSubslice, None, "Slice.subslice_mut");
+ (SliceMutSubslice, rg0, "Slice.subslice_mut_back");
+ (SliceLen, None, "Slice.len");
]
let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 207acef6..157cca38 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -647,7 +647,7 @@ let eval_non_local_function_call_concrete (config : C.config)
| ArraySharedIndex | ArrayMutIndex | ArrayToSharedSlice
| ArrayToMutSlice | ArraySharedSubslice | ArrayMutSubslice
| SliceSharedIndex | SliceMutIndex | SliceSharedSubslice
- | SliceMutSubslice ->
+ | SliceMutSubslice | SliceLen ->
raise (Failure "Unimplemented")
in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 43b11aa5..ad7ab05f 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -512,6 +512,7 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
| ArrayToMutSlice -> "@ArrayToMutSlice"
| ArraySharedSubslice -> "@ArraySharedSubslice"
| ArrayMutSubslice -> "@ArrayMutSubslice"
+ | SliceLen -> "@SliceLen"
| SliceSharedIndex -> "@SliceSharedIndex"
| SliceMutIndex -> "@SliceMutIndex"
| SliceSharedSubslice -> "@SliceSharedSubslice"
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 58a5f9e2..52eeee26 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1567,7 +1567,8 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
| VecIndex | VecIndexMut | ArraySharedSubslice
| ArrayMutSubslice | SliceSharedIndex | SliceMutIndex
| SliceSharedSubslice | SliceMutSubslice | ArraySharedIndex
- | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice ),
+ | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice
+ | SliceLen ),
_ ) ->
super#visit_texpression env e)
| _ -> super#visit_texpression env e)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 12:08:42 +0000