summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon HO2024-05-29 07:46:40 +0200
committerGitHub2024-05-29 07:46:40 +0200
commitdc6737c2a74c2c5caa054c84f39b0f1edea2d1c2 (patch)
tree674356fb329c7646460db6f8d0bdd2798f0f662e /compiler
parent6d024213541c0f87f1fde991d860c35cd4e5747b (diff)
parent23747e8fff162170fa1108cc609db1a0f8f5fc96 (diff)
Merge pull request #221 from AeneasVerif/son/builtins
Factor out code in ExtractBuiltin.ml
Diffstat (limited to '')
-rw-r--r--compiler/ExtractBuiltin.ml284
-rw-r--r--compiler/FunsAnalysis.ml3
2 files changed, 124 insertions, 163 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index a7ab6da0..ff936d2f 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -233,7 +233,12 @@ let mk_builtin_types_map () =
let builtin_types_map = mk_memoized mk_builtin_types_map
-type builtin_fun_info = { extract_name : string } [@@deriving show]
+type builtin_fun_info = {
+ extract_name : string;
+ can_fail : bool;
+ stateful : bool;
+}
+[@@deriving show]
let int_and_smaller_list : (string * string) list =
let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in
@@ -257,16 +262,17 @@ let int_and_smaller_list : (string * string) list =
]
@ compute_pairs uint_names @ compute_pairs int_names
-(** The assumed functions.
+(** The builtin 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 () : (pattern * bool list option * builtin_fun_info) list =
+let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
(* Small utility *)
- let mk_fun (rust_name : string) (extract_name : string option)
- (filter : bool list option) :
+ let mk_fun (rust_name : string) ?(filter : bool list option = None)
+ ?(can_fail = true) ?(stateful = false)
+ ?(extract_name : string option = None) () :
pattern * bool list option * builtin_fun_info =
let rust_name =
try parse_pattern rust_name
@@ -279,124 +285,151 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
| Some name -> split_on_separator name
in
let basename = flatten_name extract_name in
- let f = { extract_name = basename } in
+ let f = { extract_name = basename; can_fail; stateful } in
(rust_name, filter, f)
in
let mk_scalar_fun (rust_name : string -> string)
- (extract_name : string -> string) :
+ (extract_name : string -> string) ?(can_fail = true) () :
(pattern * bool list option * builtin_fun_info) list =
List.map
- (fun ty -> mk_fun (rust_name ty) (Some (extract_name ty)) None)
+ (fun ty ->
+ mk_fun (rust_name ty)
+ ~extract_name:(Some (extract_name ty))
+ ~can_fail ())
all_int_names
in
[
- mk_fun "core::mem::replace" None None;
+ mk_fun "core::mem::replace" ~can_fail:false ();
+ mk_fun "core::mem::take" ~can_fail:false ();
mk_fun "core::slice::{[@T]}::len"
- (Some (backend_choice "slice::len" "Slice::len"))
- None;
+ ~extract_name:(Some (backend_choice "slice::len" "Slice::len"))
+ ~can_fail:false ();
mk_fun "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new"
- (Some "alloc::vec::Vec::new") None;
- mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push" None
- (Some [ true; false ]);
- mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert" None
- (Some [ true; false ]);
- mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" None
- (Some [ true; false ]);
+ ~extract_name:(Some "alloc::vec::Vec::new") ~can_fail:false ();
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push"
+ ~filter:(Some [ true; false ])
+ ();
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert"
+ ~filter:(Some [ true; false ])
+ ();
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len"
+ ~filter:(Some [ true; false ])
+ ~can_fail:false ();
mk_fun
"alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
@I>}::index"
- (Some "alloc.vec.Vec.index")
- (Some [ true; true; false ]);
+ ~extract_name:(Some "alloc.vec.Vec.index")
+ ~filter:(Some [ true; true; false ])
+ ();
mk_fun
"alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
@I>}::index_mut"
- (Some "alloc.vec.Vec.index_mut")
- (Some [ true; true; false ]);
+ ~extract_name:(Some "alloc.vec.Vec.index_mut")
+ ~filter:(Some [ true; true; false ])
+ ();
mk_fun "alloc::boxed::{core::ops::deref::Deref<Box<@T>>}::deref"
- (Some "alloc.boxed.Box.deref")
- (Some [ true; false ]);
+ ~extract_name:(Some "alloc.boxed.Box.deref")
+ ~filter:(Some [ true; false ])
+ ();
mk_fun "alloc::boxed::{core::ops::deref::DerefMut<Box<@T>>}::deref_mut"
- (Some "alloc.boxed.Box.deref_mut")
- (Some [ true; false ]);
+ ~extract_name:(Some "alloc.boxed.Box.deref_mut")
+ ~filter:(Some [ true; false ])
+ ();
mk_fun "core::slice::index::{core::ops::index::Index<[@T], @I>}::index"
- (Some "core.slice.index.Slice.index") None;
+ ~extract_name:(Some "core.slice.index.Slice.index") ();
mk_fun
"core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut"
- (Some "core.slice.index.Slice.index_mut") None;
+ ~extract_name:(Some "core.slice.index.Slice.index_mut") ();
mk_fun "core::array::{core::ops::index::Index<[@T; @N], @I>}::index"
- (Some "core.array.Array.index") None;
+ ~extract_name:(Some "core.array.Array.index") ();
mk_fun "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut"
- (Some "core.array.Array.index_mut") None;
+ ~extract_name:(Some "core.array.Array.index_mut") ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
[@T]>}::get"
- (Some "core::slice::index::RangeUsize::get") None;
+ ~extract_name:(Some "core::slice::index::RangeUsize::get") ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
[@T]>}::get_mut"
- (Some "core::slice::index::RangeUsize::get_mut") None;
+ ~extract_name:(Some "core::slice::index::RangeUsize::get_mut") ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
[@T]>}::index"
- (Some "core::slice::index::RangeUsize::index") None;
+ ~extract_name:(Some "core::slice::index::RangeUsize::index") ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
[@T]>}::index_mut"
- (Some "core::slice::index::RangeUsize::index_mut") None;
+ ~extract_name:(Some "core::slice::index::RangeUsize::index_mut") ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
[@T]>}::get_unchecked"
- (Some "core::slice::index::RangeUsize::get_unchecked") None;
+ ~extract_name:(Some "core::slice::index::RangeUsize::get_unchecked") ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
[@T]>}::get_unchecked_mut"
- (Some "core::slice::index::RangeUsize::get_unchecked_mut") None;
+ ~extract_name:(Some "core::slice::index::RangeUsize::get_unchecked_mut")
+ ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<usize, [@T]>}::get"
- None None;
+ ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<usize, \
[@T]>}::get_mut"
- None None;
+ ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<usize, \
[@T]>}::get_unchecked"
- None None;
+ ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<usize, \
[@T]>}::get_unchecked_mut"
- None None;
+ ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<usize, [@T]>}::index"
- (Some "core_slice_index_Slice_index") None;
+ ~extract_name:(Some "core_slice_index_Slice_index") ();
mk_fun
"core::slice::index::{core::slice::index::SliceIndex<usize, \
[@T]>}::index_mut"
- (Some "core_slice_index_Slice_index_mut") None;
- mk_fun "alloc::slice::{[@T]}::to_vec" (Some "alloc.slice.Slice.to_vec") None;
+ ~extract_name:(Some "core_slice_index_Slice_index_mut") ();
+ mk_fun "alloc::slice::{[@T]}::to_vec"
+ ~extract_name:(Some "alloc.slice.Slice.to_vec") ();
mk_fun
"alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity"
- (Some "alloc.vec.Vec.with_capacity") None;
- mk_fun "core::slice::{[@T]}::reverse" (Some "core.slice.Slice.reverse") None;
+ ~extract_name:(Some "alloc.vec.Vec.with_capacity") ~can_fail:false ();
+ mk_fun "core::slice::{[@T]}::reverse"
+ ~extract_name:(Some "core.slice.Slice.reverse") ~can_fail:false ();
mk_fun
"alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref"
- (Some "alloc.vec.DerefVec.deref")
- (Some [ true; false ]);
+ ~extract_name:(Some "alloc.vec.DerefVec.deref")
+ ~filter:(Some [ true; false ])
+ ~can_fail:false ();
mk_fun
"alloc::vec::{core::ops::deref::DerefMut<alloc::vec::Vec<@T, \
@A>>}::deref_mut"
- (Some "alloc.vec.DerefMutVec.deref_mut")
- (Some [ true; false ]);
+ ~extract_name:(Some "alloc.vec.DerefMutVec.deref_mut")
+ ~filter:(Some [ true; false ])
+ ();
mk_fun "core::option::{core::option::Option<@T>}::unwrap"
- (Some "core.option.Option.unwrap") None;
+ ~extract_name:(Some "core.option.Option.unwrap") ();
]
@ List.flatten
(List.map
+ (fun int_name ->
+ List.map
+ (fun op ->
+ mk_fun
+ ("core::num::" ^ "{" ^ int_name ^ "}::" ^ op)
+ ~can_fail:false ())
+ [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ])
+ all_int_names)
+ @ List.flatten
+ (List.map
(fun op ->
mk_scalar_fun
(fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op)
(fun ty ->
- StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op))
+ StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op)
+ ~can_fail:false ())
[ "add"; "sub"; "mul"; "div"; "rem" ])
(* From<INT, bool> *)
@ mk_scalar_fun
@@ -406,44 +439,50 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
"core.convert.num.From"
^ StringUtils.capitalize_first_letter ty
^ "Bool.from")
+ ~can_fail:false ()
(* From<INT, INT> *)
@ List.map
(fun (big, small) ->
mk_fun
("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
^ ">}::from")
- (Some
- ("core.convert.num.From"
- ^ StringUtils.capitalize_first_letter big
- ^ StringUtils.capitalize_first_letter small
- ^ ".from"))
- None)
+ ~extract_name:
+ (Some
+ ("core.convert.num.From"
+ ^ StringUtils.capitalize_first_letter big
+ ^ StringUtils.capitalize_first_letter small
+ ^ ".from"))
+ ~can_fail:false ())
int_and_smaller_list
(* Leading zeros *)
@ mk_scalar_fun
(fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
(fun ty ->
"core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros")
+ ~can_fail:false ()
(* to_le_bytes *)
@ mk_scalar_fun
(fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes")
(fun ty ->
"core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes")
+ ~can_fail:false ()
(* to_be_bytes *)
@ mk_scalar_fun
(fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes")
(fun ty ->
"core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes")
+ ~can_fail:false ()
(* Clone<bool> *)
@ [
mk_fun "core::clone::impls::{core::clone::Clone<bool>}::clone"
- (Some "core.clone.CloneBool.clone") None;
+ ~extract_name:(Some "core.clone.CloneBool.clone") ~can_fail:false ();
]
(* Clone<INT> *)
@ mk_scalar_fun
(fun ty -> "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone")
(fun ty ->
"core.clone.Clone" ^ StringUtils.capitalize_first_letter ty ^ ".clone")
+ ~can_fail:false ()
(* Lean-only definitions *)
@ mk_lean_only
[
@@ -451,15 +490,19 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
By construction, we cannot write down that parameter in the output
in this list
*)
- mk_fun "core::mem::swap" None None;
+ mk_fun "core::mem::swap" ~can_fail:false ();
mk_fun "core::option::{core::option::Option<@T>}::take"
- (Some (backend_choice "" "Option::take"))
- None;
+ ~extract_name:(Some (backend_choice "" "Option::take"))
+ ~can_fail:false ();
mk_fun "core::option::{core::option::Option<@T>}::is_none"
- (Some (backend_choice "" "Option::isNone"))
- (Some [ false ]);
+ ~extract_name:(Some (backend_choice "" "Option::isNone"))
+ ~filter:(Some [ false ]) ~can_fail:false ();
]
+let builtin_funs : unit -> (pattern * bool list option * builtin_fun_info) list
+ =
+ mk_memoized mk_builtin_funs
+
let mk_builtin_funs_map () =
let m =
NameMatcherMap.of_list
@@ -475,106 +518,20 @@ let builtin_funs_map = mk_memoized mk_builtin_funs_map
type effect_info = { can_fail : bool; stateful : bool }
-let builtin_fun_effects =
- let int_ops =
- [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ]
- in
- let int_funs =
- List.map
- (fun int_name ->
- List.map (fun op -> "core::num::" ^ "{" ^ int_name ^ "}::" ^ op) int_ops)
- all_int_names
- @ List.map
- (fun op ->
- List.map
- (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op)
- all_int_names)
- [ "add"; "sub"; "mul"; "div"; "rem" ]
- (* From<INT, bool> *)
- @ [
- List.map
- (fun int_name ->
- "core::convert::num::{core::convert::From<" ^ int_name
- ^ ", bool>}::from")
- all_int_names;
- ]
- (* From<INT, INT> *)
- @ [
- List.map
- (fun (big, small) ->
- "core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
- ^ ">}::from")
- int_and_smaller_list;
- ]
- (* Leading zeros *)
- @ [
- List.map
- (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
- all_int_names;
- ]
- (* to_{le,be}_bytes *)
- @ List.map
- (fun ty ->
- let pre = "core::num::{" ^ ty ^ "}::" in
- [ pre ^ "to_le_bytes"; pre ^ "to_be_bytes" ])
- all_int_names
- (* clone *)
- @ [
- List.map
- (fun ty ->
- "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone")
- all_int_names;
- ]
+let mk_builtin_fun_effects () : (pattern * effect_info) list =
+ let builtin_funs : (pattern * bool list option * builtin_fun_info) list =
+ builtin_funs ()
in
+ List.map
+ (fun ((pattern, _, info) : _ * _ * builtin_fun_info) ->
+ let info = { can_fail = info.can_fail; stateful = info.stateful } in
+ (pattern, info))
+ builtin_funs
- let int_funs = List.concat int_funs in
- let no_fail_no_state_funs =
- [
- (* TODO: redundancy with the funs information above *)
- "core::slice::{[@T]}::len";
- "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new";
- "alloc::vec::{alloc::vec::Vec<@T, @A>}::len";
- "core::mem::replace";
- "core::mem::take";
- "core::clone::impls::{core::clone::Clone<bool>}::clone";
- "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity";
- "core::slice::{[@T]}::reverse";
- "alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref";
- ]
- @ int_funs
- @ mk_lean_only
- [
- "core::mem::swap";
- "core::option::{core::option::Option<@T>}::take";
- "core::option::{core::option::Option<@T>}::is_none";
- ]
- in
- let no_fail_no_state_funs =
- List.map
- (fun n -> (n, { can_fail = false; stateful = false }))
- no_fail_no_state_funs
- in
- (* TODO: all the functions registered in the [builtin_funs] above should
- be considered as not using a state. There is a lot of redundancy
- right now. *)
- let no_state_funs =
- [
- "alloc::vec::{alloc::vec::Vec<@T, @A>}::push";
- "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
- @I>}::index";
- "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
- @I>}::index_mut";
- "core::option::{core::option::Option<@T>}::unwrap";
- ]
- in
- let no_state_funs =
- List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs
- in
- no_fail_no_state_funs @ no_state_funs
+let mk_builtin_fun_effects_map () =
+ NameMatcherMap.of_list (mk_builtin_fun_effects ())
-let builtin_fun_effects_map =
- NameMatcherMap.of_list
- (List.map (fun (n, x) -> (parse_pattern n, x)) builtin_fun_effects)
+let builtin_fun_effects_map = mk_memoized mk_builtin_fun_effects_map
type builtin_trait_decl_info = {
rust_name : pattern;
@@ -632,13 +589,16 @@ let builtin_trait_decls_info () =
if !record_fields_short_names then item_name
else extract_name ^ "_" ^ item_name
in
- let fwd = { extract_name = basename } in
+ let fwd =
+ { extract_name = basename; can_fail = true; stateful = false }
+ in
(item_name, fwd)
in
List.map mk_method methods
| Some methods ->
List.map
- (fun (item_name, extract_name) -> (item_name, { extract_name }))
+ (fun (item_name, extract_name) ->
+ (item_name, { extract_name; can_fail = true; stateful = false }))
methods
in
{
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index a11eab87..eadd8f8a 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -74,7 +74,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
way. *)
let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option =
let open ExtractBuiltin in
- NameMatcherMap.find_opt name_matcher_ctx f.name builtin_fun_effects_map
+ NameMatcherMap.find_opt name_matcher_ctx f.name
+ (builtin_fun_effects_map ())
in
(* JP: Why not use a reduce visitor here with a tuple of the values to be