summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterExpansion.ml2
-rw-r--r--src/InterpreterExpressions.ml10
-rw-r--r--src/InterpreterStatements.ml5
-rw-r--r--src/InterpreterUtils.ml2
-rw-r--r--src/Invariants.ml3
-rw-r--r--src/TypesAnalysis.ml21
-rw-r--r--src/TypesUtils.ml23
-rw-r--r--src/ValuesUtils.ml7
8 files changed, 34 insertions, 39 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 8b039510..0842dee7 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -535,7 +535,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx)
inherit [_] C.iter_eval_ctx
method! visit_Symbolic _ sv =
- if ty_has_regions (Subst.erase_regions sv.V.sv_ty) then
+ if ty_has_borrows ctx.type_context.type_infos sv.V.sv_ty then
raise (FoundSymbolicValue sv)
else ()
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index f15c7558..60918bac 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -35,7 +35,10 @@ let expand_primitively_copyable_at_place (config : C.config)
(* Small helper *)
let rec expand ctx =
let v = read_place_unwrap config access p ctx in
- match find_first_primitively_copyable_sv v with
+ match
+ find_first_primitively_copyable_sv_with_borrows
+ ctx.type_context.type_infos v
+ with
| None -> ctx
| Some sv ->
let ctx = expand_symbolic_value_no_branching config sv ctx in
@@ -178,7 +181,10 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
(* Copy the value *)
assert (not (bottom_in_value ctx.ended_regions v));
- assert (Option.is_none (find_first_primitively_copyable_sv v));
+ assert (
+ Option.is_none
+ (find_first_primitively_copyable_sv_with_borrows
+ ctx.type_context.type_infos v));
let allow_adt_copy = false in
copy_value allow_adt_copy config ctx v
| Expressions.Move p -> (
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 85c3acb4..74886bf9 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -945,7 +945,10 @@ and eval_non_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
C.eval_ctx =
(* Sanity check: make sure the type parameters don't contain regions -
* this is a current limitation of our synthesis *)
- assert (List.for_all (fun ty -> not (ty_has_regions ty)) type_params);
+ assert (
+ List.for_all
+ (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty))
+ type_params);
(* There are two cases (and this is extremely annoying):
- the function is not box_free
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index e00e7dcf..ca437593 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -81,6 +81,8 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
Checks if the projector will actually project some regions. If not,
returns [AIgnored] (`_`).
+
+ TODO: update to handle 'static
*)
let mk_aproj_loans_value_from_symbolic_value (regions : T.RegionId.Set.t)
(svalue : V.symbolic_value) : V.typed_avalue =
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 5b77e13c..67084684 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -707,7 +707,8 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
(* Check *)
let check_info _id info =
assert (info.env_count = 0 || info.aproj_borrows = []);
- if ty_has_regions info.ty then assert (info.env_count <= 1);
+ if ty_has_borrows ctx.type_context.type_infos info.ty then
+ assert (info.env_count <= 1);
assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
in
M.iter check_info !infos
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index f49b49ac..acb0f963 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -80,8 +80,9 @@ let partial_type_info_to_ty_info (info : partial_type_info) : ty_info =
param_infos = ();
}
-let analyze_full_ty (updated : bool ref) (infos : type_infos)
- (ty_info : partial_type_info) (ty : 'r gr_ty) : partial_type_info =
+let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
+ (infos : type_infos) (ty_info : partial_type_info) (ty : 'r ty) :
+ partial_type_info =
(* Small utility *)
let check_update_bool (original : bool) (nv : bool) : bool =
if nv && not original then (
@@ -107,7 +108,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
(* The recursive function which explores the type *)
let rec analyze (expl_info : expl_info) (ty_info : partial_type_info)
- (ty : 'r gr_ty) : partial_type_info =
+ (ty : 'r ty) : partial_type_info =
match ty with
| Bool | Char | Never | Integer _ | Str -> ty_info
| TypeVar var_id -> (
@@ -142,7 +143,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
in
(* Set `contains_static` *)
let contains_static =
- check_update_bool ty_info.contains_static (r = Static)
+ check_update_bool ty_info.contains_static (r_is_static r)
in
let ty_info = { ty_info with contains_static } in
(* Update the type info *)
@@ -164,7 +165,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
{
ty_info with
contains_static =
- check_update_bool ty_info.contains_static (r = Static);
+ check_update_bool ty_info.contains_static (r_is_static r);
})
ty_info regions
in
@@ -207,11 +208,13 @@ let analyze_type_def (updated : bool ref) (infos : type_infos) (def : type_def)
(List.map (fun v -> List.map (fun f -> f.field_ty) v.fields) variants)
in
(* Explore the types and accumulate information *)
+ let r_is_static r = r = Static in
let type_def_info = TypeDefId.Map.find def.def_id infos in
let type_def_info = type_def_info_to_partial_type_info type_def_info in
let type_def_info =
List.fold_left
- (fun type_def_info ty -> analyze_full_ty updated infos type_def_info ty)
+ (fun type_def_info ty ->
+ analyze_full_ty r_is_static updated infos type_def_info ty)
type_def_info fields_tys
in
let type_def_info = partial_type_info_to_type_def_info type_def_info in
@@ -263,10 +266,12 @@ let analyze_type_declarations (type_defs : type_def TypeDefId.Map.t)
(** Analyze a type to check whether it contains borrows, etc., provided
we have already analyzed the type definitions in the context.
*)
-let analyze_ty (infos : type_infos) (ty : 'r gr_ty) : ty_info =
+let analyze_ty (infos : type_infos) (ty : 'r ty) : ty_info =
(* We don't use `updated` but need to give it as parameter *)
let updated = ref false in
+ (* We don't need to compute whether the type contains 'static or not *)
+ let r_is_static _ = false in
let ty_info = initialize_g_type_info None in
- let ty_info = analyze_full_ty updated infos ty_info ty in
+ let ty_info = analyze_full_ty r_is_static updated infos ty_info ty in
(* Convert the ty_info *)
partial_type_info_to_ty_info ty_info
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 10bd286c..ef260830 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -92,29 +92,6 @@ let rec ety_no_regions_to_rty (ty : ety) : rty =
"Can't convert a ref with erased regions to a ref with non-erased \
regions"
-(** Check if a [ty] contains regions.
-
- TODO: rename to "has_borrows"?
- TODO: update, and check the usage.
- *)
-let ty_has_regions (ty : 'r ty) : bool =
- let obj =
- object
- inherit [_] iter_ty as super
-
- method! visit_Adt env type_id regions tys =
- if regions = [] then super#visit_Adt env type_id regions tys
- else raise Found
-
- method! visit_Ref _ _ _ _ = raise Found
- end
- in
- raise Errors.Unimplemented;
- try
- obj#visit_ty () ty;
- false
- with Found -> true
-
(** Retuns true if a type contains borrows.
Note that we can't simply explore the type and look for regions: sometimes
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 4555fd50..f3876f53 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -2,6 +2,7 @@ open Utils
open TypesUtils
open Types
open Values
+module TA = TypesAnalysis
exception FoundSymbolicValue of symbolic_value
(** Utility exception *)
@@ -88,8 +89,8 @@ let outer_loans_in_value (v : typed_value) : bool =
false
with Found -> true
-let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option
- =
+let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
+ (v : typed_value) : symbolic_value option =
(* The visitor *)
let obj =
object
@@ -97,7 +98,7 @@ let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option
method! visit_Symbolic _ sv =
let ty = sv.sv_ty in
- if ty_is_primitively_copyable ty && ty_has_regions ty then
+ if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
raise (FoundSymbolicValue sv)
else ()
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 12:26:33 +0000