diff options
Diffstat (limited to 'src/ValuesUtils.ml')
-rw-r--r-- | src/ValuesUtils.ml | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml index f90a98ef..2d380ca9 100644 --- a/src/ValuesUtils.ml +++ b/src/ValuesUtils.ml @@ -3,6 +3,9 @@ open TypesUtils open Types open Values +exception FoundSymbolicValue of symbolic_value +(** Utility exception *) + let mk_unit_value : typed_value = { value = Adt { variant_id = None; field_values = [] }; ty = mk_unit_ty } @@ -16,6 +19,12 @@ let mk_box_value (v : typed_value) : typed_value = let box_v = Adt { variant_id = None; field_values = [ v ] } in mk_typed_value box_ty box_v +let is_symbolic (v : value) : bool = + match v with Symbolic _ -> true | _ -> false + +let as_symbolic (v : value) : symbolic_value = + match v with Symbolic s -> s | _ -> failwith "Unexpected" + (** Check if a value contains a borrow *) let borrows_in_value (v : typed_value) : bool = let obj = @@ -78,3 +87,23 @@ let outer_loans_in_value (v : typed_value) : bool = obj#visit_typed_value () v; false with Found -> true + +let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option + = + (* The visitor *) + let obj = + object + inherit [_] iter_typed_value + + method! visit_Symbolic _ sv = + let ty = sv.sv_ty in + if type_is_primitively_copyable ty && ty_has_regions ty then + raise (FoundSymbolicValue sv) + else () + end + in + (* Small helper *) + try + obj#visit_typed_value () v; + None + with FoundSymbolicValue sv -> Some sv |