diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 11 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 11 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 3 |
3 files changed, 18 insertions, 7 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 363955bf..2dbacce3 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -381,6 +381,7 @@ let builtin_fun_effects = let int_funs = List.concat int_funs in let no_fail_no_state_funs = [ + (* TODO: redundancy with the funs information below *) "alloc::vec::Vec::new"; "alloc::vec::Vec::len"; "alloc::boxed::Box::deref"; @@ -395,7 +396,15 @@ let builtin_fun_effects = (fun n -> (n, { can_fail = false; stateful = false })) no_fail_no_state_funs in - let no_state_funs = [ "alloc::vec::Vec::push" ] in + let no_state_funs = + [ + (* TODO: redundancy with the funs information below *) + "alloc::vec::Vec::push"; + "alloc::vec::Vec::index"; + "alloc::vec::Vec::index_mut"; + "alloc::vec::Vec::index_mut_back"; + ] + in let no_state_funs = List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs in diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 9eac3e6f..69c0df71 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -76,6 +76,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) object (self) inherit [_] iter_statement as super method may_fail b = can_fail := !can_fail || b + method maybe_stateful b = stateful := !stateful || b method! visit_Assert env a = self#may_fail true; @@ -126,14 +127,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) | None -> let info_can_fail, info_stateful = match builtin_info with - | None -> (true, false) + | None -> (true, use_state) | Some { can_fail; stateful } -> (can_fail, stateful) in obj#may_fail info_can_fail; - stateful := - (not f.is_global_decl_body) - && use_state - && not (has_builtin_info && not info_stateful) + obj#maybe_stateful + (if f.is_global_decl_body then false + else if not use_state then false + else info_stateful) | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 341e97eb..245f3b77 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -144,7 +144,8 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) (match v.V.ty with | 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.AdtId _, _) as ty -> + assert (allow_adt_copy || ty_is_primitively_copyable ty) | T.Adt (T.Tuple, _) -> () (* Ok *) | T.Adt ( T.Assumed (Slice | T.Array), |