From 987dc5c25a1d5cee19f4bba2416cbfa83e6ab6de Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 7 Aug 2023 08:59:27 +0200 Subject: Change some fun id names to use "Mut"/"Shared" as a suffix --- compiler/Assumed.ml | 36 +++++++++++------------ compiler/Extract.ml | 60 +++++++++++++++++++-------------------- compiler/InterpreterStatements.ml | 8 +++--- compiler/PrintPure.ml | 20 ++++++------- compiler/PureMicroPasses.ml | 8 +++--- 5 files changed, 66 insertions(+), 66 deletions(-) diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 572b0a24..11cd5666 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -416,44 +416,44 @@ let assumed_infos : assumed_info list = true, to_name (index_pre @ [ "IndexMut"; "index_mut" ]) ); (* Array Index *) - ( ArraySharedIndex, + ( ArrayIndexShared, Sig.array_index_sig false, true, - to_name [ "@ArraySharedIndex" ] ); - (ArrayMutIndex, Sig.array_index_sig true, true, to_name [ "@ArrayMutIndex" ]); + to_name [ "@ArrayIndexShared" ] ); + (ArrayIndexMut, Sig.array_index_sig true, true, to_name [ "@ArrayIndexMut" ]); (* Array to slice*) - ( ArrayToSharedSlice, + ( ArrayToSliceShared, Sig.array_to_slice_sig false, true, - to_name [ "@ArrayToSharedSlice" ] ); - ( ArrayToMutSlice, + to_name [ "@ArrayToSliceShared" ] ); + ( ArrayToSliceMut, Sig.array_to_slice_sig true, true, - to_name [ "@ArrayToMutSlice" ] ); + to_name [ "@ArrayToSliceMut" ] ); (* Array Subslice *) - ( ArraySharedSubslice, + ( ArraySubsliceShared, Sig.array_subslice_sig false, true, - to_name [ "@ArraySharedSubslice" ] ); - ( ArrayMutSubslice, + to_name [ "@ArraySubsliceShared" ] ); + ( ArraySubsliceMut, Sig.array_subslice_sig true, true, - to_name [ "@ArrayMutSubslice" ] ); + to_name [ "@ArraySubsliceMut" ] ); (* Slice Index *) - ( SliceSharedIndex, + ( SliceIndexShared, Sig.slice_index_sig false, true, - to_name [ "@SliceSharedIndex" ] ); - (SliceMutIndex, Sig.slice_index_sig true, true, to_name [ "@SliceMutIndex" ]); + to_name [ "@SliceIndexShared" ] ); + (SliceIndexMut, Sig.slice_index_sig true, true, to_name [ "@SliceIndexMut" ]); (* Slice Subslice *) - ( SliceSharedSubslice, + ( SliceSubsliceShared, Sig.slice_subslice_sig false, true, - to_name [ "@SliceSharedSubslice" ] ); - ( SliceMutSubslice, + to_name [ "@SliceSubsliceShared" ] ); + ( SliceSubsliceMut, Sig.slice_subslice_sig true, true, - to_name [ "@SliceMutSubslice" ] ); + to_name [ "@SliceSubsliceMut" ] ); (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]); ] diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 297c182a..c4238d83 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -329,21 +329,21 @@ 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_shared"); - (ArrayMutIndex, None, "array_index_mut_fwd"); - (ArrayMutIndex, rg0, "array_index_mut_back"); - (ArrayToSharedSlice, None, "array_to_slice_shared"); - (ArrayToMutSlice, None, "array_to_slice_mut_fwd"); - (ArrayToMutSlice, rg0, "array_to_slice_mut_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_shared"); - (SliceMutSubslice, None, "slice_subslice_mut_fwd"); - (SliceMutSubslice, rg0, "slice_subslice_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"); + (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 -> @@ -360,21 +360,21 @@ let assumed_llbc_functions () : (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *); (VecIndexMut, None, "Vec.index_mut"); (VecIndexMut, rg0, "Vec.index_mut_back"); - (ArraySharedIndex, None, "Array.index_shared"); - (ArrayMutIndex, None, "Array.index_mut"); - (ArrayMutIndex, rg0, "Array.index_mut_back"); - (ArrayToSharedSlice, None, "Array.to_slice_shared"); - (ArrayToMutSlice, None, "Array.to_slice_mut"); - (ArrayToMutSlice, rg0, "Array.to_slice_mut_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"); + (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"); + (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"); ] diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 157cca38..045c4484 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -644,10 +644,10 @@ let eval_non_local_function_call_concrete (config : C.config) | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> eval_vec_function_concrete config fid region_params type_params cg_params - | ArraySharedIndex | ArrayMutIndex | ArrayToSharedSlice - | ArrayToMutSlice | ArraySharedSubslice | ArrayMutSubslice - | SliceSharedIndex | SliceMutIndex | SliceSharedSubslice - | SliceMutSubslice | SliceLen -> + | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared + | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut + | SliceIndexShared | SliceIndexMut | SliceSubsliceShared + | SliceSubsliceMut | SliceLen -> raise (Failure "Unimplemented") in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index ad7ab05f..cfb63ec2 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -506,17 +506,17 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = | A.VecLen -> "alloc::vec::Vec::len" | A.VecIndex -> "core::ops::index::Index::index" | A.VecIndexMut -> "core::ops::index::IndexMut::index_mut" - | ArraySharedIndex -> "@ArraySharedIndex" - | ArrayMutIndex -> "@ArrayMutIndex" - | ArrayToSharedSlice -> "@ArrayToSharedSlice" - | ArrayToMutSlice -> "@ArrayToMutSlice" - | ArraySharedSubslice -> "@ArraySharedSubslice" - | ArrayMutSubslice -> "@ArrayMutSubslice" + | ArrayIndexShared -> "@ArrayIndexShared" + | ArrayIndexMut -> "@ArrayIndexMut" + | ArrayToSliceShared -> "@ArrayToSliceShared" + | ArrayToSliceMut -> "@ArrayToSliceMut" + | ArraySubsliceShared -> "@ArraySubsliceShared" + | ArraySubsliceMut -> "@ArraySubsliceMut" | SliceLen -> "@SliceLen" - | SliceSharedIndex -> "@SliceSharedIndex" - | SliceMutIndex -> "@SliceMutIndex" - | SliceSharedSubslice -> "@SliceSharedSubslice" - | SliceMutSubslice -> "@SliceMutSubslice" + | 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/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 52eeee26..b6025df4 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1564,10 +1564,10 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = assert (args = []); mk_unit_rvalue | ( ( A.Replace | VecNew | VecPush | VecInsert | VecLen - | VecIndex | VecIndexMut | ArraySharedSubslice - | ArrayMutSubslice | SliceSharedIndex | SliceMutIndex - | SliceSharedSubslice | SliceMutSubslice | ArraySharedIndex - | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice + | VecIndex | VecIndexMut | ArraySubsliceShared + | ArraySubsliceMut | SliceIndexShared | SliceIndexMut + | SliceSubsliceShared | SliceSubsliceMut | ArrayIndexShared + | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | SliceLen ), _ ) -> super#visit_texpression env e) -- cgit v1.2.3