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 +- flake.lock | 7 ++++--- flake.nix | 2 +- 5 files changed, 12 insertions(+), 11 deletions(-) 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 diff --git a/flake.lock b/flake.lock index 27a555ad..f35ddf2e 100644 --- a/flake.lock +++ b/flake.lock @@ -8,15 +8,16 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1712233083, - "narHash": "sha256-KR4UwlgUzLWObSzQ1LIKITjRrYe4AuZXdvCK78qrip8=", + "lastModified": 1712760963, + "narHash": "sha256-KV8ZSHfnAn9bx1JA4k7Vj8yntfxMjjqIH05yHV9IDH0=", "owner": "aeneasverif", "repo": "charon", - "rev": "6e31313fdfd4830aa0fc795f6ab8b27600fcbbfb", + "rev": "763aa8c3d308be619829939170af93624e4561f4", "type": "github" }, "original": { "owner": "aeneasverif", + "ref": "generic-copy", "repo": "charon", "type": "github" } diff --git a/flake.nix b/flake.nix index 36910f45..e1bafc6b 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { # Remark: when adding inputs here, don't forget to also add them in the list # of outputs below! - charon.url = "github:aeneasverif/charon"; + charon.url = "github:aeneasverif/charon/generic-copy"; flake-utils.follows = "charon/flake-utils"; nixpkgs.follows = "charon/nixpkgs"; hacl-nix.url = "github:hacl-star/hacl-nix"; -- 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(-) 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 From 2f43c95253de73fce3207a7e6895f257b857f566 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 11 Apr 2024 11:00:35 +0200 Subject: Use charon main --- flake.lock | 7 +++---- flake.nix | 2 +- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index f35ddf2e..1eaf1375 100644 --- a/flake.lock +++ b/flake.lock @@ -8,16 +8,15 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1712760963, - "narHash": "sha256-KV8ZSHfnAn9bx1JA4k7Vj8yntfxMjjqIH05yHV9IDH0=", + "lastModified": 1712825631, + "narHash": "sha256-YC0QArtso4Z9iBgd63FXHsSopMtWof0kC7ZrYpE6yzg=", "owner": "aeneasverif", "repo": "charon", - "rev": "763aa8c3d308be619829939170af93624e4561f4", + "rev": "657de2521c285401d706ec69d588bb5778b18109", "type": "github" }, "original": { "owner": "aeneasverif", - "ref": "generic-copy", "repo": "charon", "type": "github" } diff --git a/flake.nix b/flake.nix index e1bafc6b..36910f45 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { # Remark: when adding inputs here, don't forget to also add them in the list # of outputs below! - charon.url = "github:aeneasverif/charon/generic-copy"; + charon.url = "github:aeneasverif/charon"; flake-utils.follows = "charon/flake-utils"; nixpkgs.follows = "charon/nixpkgs"; hacl-nix.url = "github:hacl-star/hacl-nix"; -- cgit v1.2.3