From 143a68b2c43c4302abbbd39c28cac3f9c5f52f4a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 10 Apr 2024 16:46:24 +0200
Subject: Trust rustc regarding `Copy` bounds

---
 compiler/InterpreterExpressions.ml | 10 +++++-----
 compiler/Invariants.ml             |  2 +-
 compiler/ValuesUtils.ml            |  2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'compiler')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 48a1cce6..444e5788 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -146,7 +146,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
             "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
           sanity_check __FILE__ __LINE__
-            (allow_adt_copy || ty_is_primitively_copyable ty)
+            (allow_adt_copy || ty_is_copyable ty)
             meta
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
@@ -158,7 +158,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               trait_refs = [];
             } ) ->
           exec_assert __FILE__ __LINE__
-            (ty_is_primitively_copyable ty)
+            (ty_is_copyable ty)
             meta "The type is not primitively copyable"
       | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable");
       let ctx, fields =
@@ -195,7 +195,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
        * thus requires calling the proper function. Here, we copy values
        * for very simple types such as integers, shared borrows, etc. *)
       cassert __FILE__ __LINE__
-        (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty))
+        (ty_is_copyable (Substitute.erase_regions sp.sv_ty))
         meta "Not primitively copyable";
       (* If the type is copyable, we simply return the current value. Side
        * remark: what is important to look at when copying symbolic values
@@ -529,7 +529,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
       "The arguments given to the binop don't have the same type";
     (* Equality/inequality check is primitive only for a subset of types *)
     exec_assert __FILE__ __LINE__
-      (ty_is_primitively_copyable v1.ty)
+      (ty_is_copyable v1.ty)
       meta "Type is not primitively copyable";
     let b = v1 = v2 in
     Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
@@ -622,7 +622,7 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
         sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
         (* Equality/inequality check is primitive only for a subset of types *)
         exec_assert __FILE__ __LINE__
-          (ty_is_primitively_copyable v1.ty)
+          (ty_is_copyable v1.ty)
           meta "The type is not primitively copyable";
         TLiteral TBool)
       else
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 2ccf3ad4..6e448cc4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -827,7 +827,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
       sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
     (* A duplicated symbolic value is necessarily primitively copyable *)
     sanity_check __FILE__ __LINE__
-      (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
+      (info.env_count <= 1 || ty_is_copyable info.ty)
       meta;
 
     sanity_check __FILE__ __LINE__
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 91010e07..b6ee66f5 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -160,7 +160,7 @@ let find_first_primitively_copyable_sv_with_borrows
 
       method! visit_VSymbolic _ sv =
         let ty = sv.sv_ty in
-        if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
+        if ty_is_copyable ty && ty_has_borrows type_infos ty then
           raise (FoundSymbolicValue sv)
         else ()
     end
-- 
cgit v1.2.3


From c63284e3f9d7723b24f2d226355747e91ebb06aa Mon Sep 17 00:00:00 2001
From: Son HO
Date: Thu, 11 Apr 2024 10:54:12 +0200
Subject: Update a comment

---
 compiler/Invariants.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 6e448cc4..689db0c4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -825,7 +825,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
      * it must be expanded first *)
     if ty_has_borrows ctx.type_ctx.type_infos info.ty then
       sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
-    (* A duplicated symbolic value is necessarily primitively copyable *)
+    (* A duplicated symbolic value is necessarily copyable *)
     sanity_check __FILE__ __LINE__
       (info.env_count <= 1 || ty_is_copyable info.ty)
       meta;
-- 
cgit v1.2.3