summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterBorrows.ml1
-rw-r--r--src/InterpreterExpressions.ml1
-rw-r--r--src/InterpreterPaths.ml2
-rw-r--r--src/InterpreterProjectors.ml7
-rw-r--r--src/InterpreterUtils.ml67
-rw-r--r--src/Synthesis.ml2
-rw-r--r--src/TypesUtils.ml15
-rw-r--r--src/ValuesUtils.ml46
8 files changed, 74 insertions, 67 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 38c79b66..ca1f87f1 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -4,6 +4,7 @@ module C = Contexts
module Subst = Substitute
module L = Logging
open Utils
+open ValuesUtils
open InterpreterUtils
open InterpreterBorrowsCore
open InterpreterProjectors
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index b08c8749..e379eacd 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -6,6 +6,7 @@ open Errors
module C = Contexts
module Subst = Substitute
module L = Logging
+open TypesUtils
open ValuesUtils
module Inv = Invariants
module S = Synthesis
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 841c22cf..d4de318b 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -5,6 +5,8 @@ module C = Contexts
module Subst = Substitute
module L = Logging
module S = Synthesis
+open TypesUtils
+open ValuesUtils
open InterpreterUtils
open InterpreterBorrowsCore
open InterpreterBorrows
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 92ea6483..105adb5a 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -10,6 +10,13 @@ open Utils
open InterpreterUtils
open InterpreterBorrowsCore
+(** A symbolic expansion *)
+type symbolic_expansion =
+ | SeConcrete of V.constant_value
+ | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list)
+ | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp
+ | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp
+
(** Auxiliary function.
Apply a proj_borrows on a shared borrow.
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 0b7d8f21..5e0375d0 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -126,51 +126,6 @@ exception FoundGBorrowContent of g_borrow_content
exception FoundGLoanContent of g_loan_content
(** Utility exception *)
-(** Check if a value contains a borrow *)
-let borrows_in_value (v : V.typed_value) : bool =
- let obj =
- object
- inherit [_] V.iter_typed_value
-
- method! visit_borrow_content _env _ = raise Found
- end
- in
- (* We use exceptions *)
- try
- obj#visit_typed_value () v;
- false
- with Found -> true
-
-(** Check if a value contains inactivated mutable borrows *)
-let inactivated_in_value (v : V.typed_value) : bool =
- let obj =
- object
- inherit [_] V.iter_typed_value
-
- method! visit_InactivatedMutBorrow _env _ = raise Found
- end
- in
- (* We use exceptions *)
- try
- obj#visit_typed_value () v;
- false
- with Found -> true
-
-(** Check if a value contains a loan *)
-let loans_in_value (v : V.typed_value) : bool =
- let obj =
- object
- inherit [_] V.iter_typed_value
-
- method! visit_loan_content _env _ = raise Found
- end
- in
- (* We use exceptions *)
- try
- obj#visit_typed_value () v;
- false
- with Found -> true
-
let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
bool =
let obj =
@@ -201,13 +156,6 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
false
with Found -> true
-(** TODO: move to InterpreterSymbolic or sth *)
-type symbolic_expansion =
- | SeConcrete of V.constant_value
- | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list)
- | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp
- | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp
-
(** Check if two different projections intersect. This is necessary when
giving a symbolic value to an abstraction: we need to check that
the regions which are already ended inside the abstraction don't
@@ -319,18 +267,3 @@ let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) :
obj#visit_typed_avalue () v;
false
with Found -> true
-
-(** Return true if a type is "primitively copyable".
- *
- * "primitively copyable" means that copying instances of this type doesn't
- * require calling dedicated functions defined through the Copy trait. It
- * is the case for types like integers, shared borrows, etc.
- *)
-let rec type_is_primitively_copyable (ty : T.ety) : bool =
- match ty with
- | T.Adt ((T.AdtId _ | T.Assumed _), _, _) -> false
- | T.Adt (T.Tuple, _, tys) -> List.for_all type_is_primitively_copyable tys
- | T.TypeVar _ | T.Never | T.Str | T.Array _ | T.Slice _ -> false
- | T.Bool | T.Char | T.Integer _ -> true
- | T.Ref (_, _, T.Mut) -> false
- | T.Ref (_, _, T.Shared) -> true
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index de482b18..85834e7a 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -6,6 +6,8 @@ module Subst = Substitute
module A = CfimAst
module L = Logging
open InterpreterUtils
+open InterpreterProjectors
+(* for symbolic_expansion definition *)
(* TODO: the below functions have very "rough" signatures and do nothing: I
* defined them so that the places where we should update the synthesized
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 878ac989..a658adce 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -108,3 +108,18 @@ let ty_has_regions (ty : ety) : bool =
obj#visit_ty () ty;
false
with Found -> true
+
+(** Return true if a type is "primitively copyable".
+ *
+ * "primitively copyable" means that copying instances of this type doesn't
+ * require calling dedicated functions defined through the Copy trait. It
+ * is the case for types like integers, shared borrows, etc.
+ *)
+let rec type_is_primitively_copyable (ty : ety) : bool =
+ match ty with
+ | Adt ((AdtId _ | Assumed _), _, _) -> false
+ | Adt (Tuple, _, tys) -> List.for_all type_is_primitively_copyable tys
+ | TypeVar _ | Never | Str | Array _ | Slice _ -> false
+ | Bool | Char | Integer _ -> true
+ | Ref (_, _, Mut) -> false
+ | Ref (_, _, Shared) -> true
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 4a503a65..f4a10287 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -1,3 +1,4 @@
+open Utils
open TypesUtils
open Types
open Values
@@ -12,3 +13,48 @@ let mk_box_value (v : typed_value) : typed_value =
let box_ty = mk_box_ty v.ty in
let box_v = Adt { variant_id = None; field_values = [ v ] } in
mk_typed_value box_ty box_v
+
+(** Check if a value contains a borrow *)
+let borrows_in_value (v : typed_value) : bool =
+ let obj =
+ object
+ inherit [_] iter_typed_value
+
+ method! visit_borrow_content _env _ = raise Found
+ end
+ in
+ (* We use exceptions *)
+ try
+ obj#visit_typed_value () v;
+ false
+ with Found -> true
+
+(** Check if a value contains inactivated mutable borrows *)
+let inactivated_in_value (v : typed_value) : bool =
+ let obj =
+ object
+ inherit [_] iter_typed_value
+
+ method! visit_InactivatedMutBorrow _env _ = raise Found
+ end
+ in
+ (* We use exceptions *)
+ try
+ obj#visit_typed_value () v;
+ false
+ with Found -> true
+
+(** Check if a value contains a loan *)
+let loans_in_value (v : typed_value) : bool =
+ let obj =
+ object
+ inherit [_] iter_typed_value
+
+ method! visit_loan_content _env _ = raise Found
+ end
+ in
+ (* We use exceptions *)
+ try
+ obj#visit_typed_value () v;
+ false
+ with Found -> true