From 1d1f6fdb75a79b39e2b8a46a362112da144bc43f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 28 Aug 2024 13:28:18 +0200 Subject: [PATCH 1/4] Update charon --- charon-pin | 2 +- compiler/FunsAnalysis.ml | 11 +++++++++-- compiler/InterpreterExpressions.ml | 3 +++ compiler/InterpreterStatements.ml | 18 +++++++++++------- compiler/InterpreterUtils.ml | 10 ++++++++-- compiler/Print.ml | 4 ++++ compiler/SymbolicToPure.ml | 9 +++++++-- flake.lock | 12 ++++++------ 8 files changed, 49 insertions(+), 20 deletions(-) diff --git a/charon-pin b/charon-pin index cab9e427d..11d1fc205 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -13502d2f3bd477ee86acafe5974016dc7707db83 +597fe150c3952fd197e37bc7b5ae2cb2f0d07c81 diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 6a439dc14..a5d918de8 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -104,8 +104,15 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_rvalue _env rv = match rv with - | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ | Len _ - -> () + | Use _ + | RvRef _ + | Global _ + | Discriminant _ + | Aggregate _ + | Len _ + | NullaryOp _ + | RawPtr _ + | ShallowInitBox _ -> () | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail | BinaryOp (bop, _, _) -> can_fail := binop_can_fail bop || !can_fail diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 4cad6a989..af3a4958e 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -862,6 +862,9 @@ let eval_rvalue_not_global (config : config) (span : Meta.span) AST" | Global _ -> craise __FILE__ __LINE__ span "Unreachable" | Len _ -> craise __FILE__ __LINE__ span "Unhandled Len" + | _ -> + craise __FILE__ __LINE__ span + ("Unsupported operation: " ^ Print.EvalCtx.rvalue_to_string ctx rvalue) let eval_fake_read (config : config) (span : Meta.span) (p : place) : cm_fun = fun ctx -> diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 09d654534..310d4bd17 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -952,18 +952,22 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun = | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable" | Len _ -> craise __FILE__ __LINE__ st.span "Len is not handled yet" + | ShallowInitBox _ -> + craise __FILE__ __LINE__ st.span "ShallowInitBox" | Use _ | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) - | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> + | NullaryOp _ + | UnaryOp _ + | BinaryOp _ + | Discriminant _ + | Aggregate _ + | RawPtr _ -> + let p = S.mk_mplace st.span p ctx in let rp = rvalue_get_place rvalue in let rp = - match rp with - | Some rp -> Some (S.mk_mplace st.span rp ctx) - | None -> None + Option.map (fun rp -> S.mk_mplace st.span rp ctx) rp in - S.synthesize_assignment ctx - (S.mk_mplace st.span p ctx) - rv rp + S.synthesize_assignment ctx p rv rp in let ctx, cc = comp cc (assign_to_place config st.span rv p ctx) diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index f577153f3..f3aee8ff3 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -293,8 +293,14 @@ let rvalue_get_place (rv : rvalue) : place option = match rv with | Use (Copy p | Move p) -> Some p | Use (Constant _) -> None - | Len (p, _, _) | RvRef (p, _) -> Some p - | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None + | Len (p, _, _) | RvRef (p, _) | RawPtr (p, _) -> Some p + | NullaryOp _ + | UnaryOp _ + | BinaryOp _ + | Global _ + | Discriminant _ + | Aggregate _ -> None + | ShallowInitBox _ -> failwith "ShallowInitBox" (** See {!ValuesUtils.symbolic_value_has_borrows} *) let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool = diff --git a/compiler/Print.ml b/compiler/Print.ml index 90dadbccd..b91a069b8 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -613,6 +613,10 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in operand_to_string env op + let rvalue_to_string (ctx : eval_ctx) (rval : rvalue) : string = + let env = eval_ctx_to_fmt_env ctx in + rvalue_to_string env rval + let call_to_string (ctx : eval_ctx) (call : call) : string = let env = eval_ctx_to_fmt_env ctx in call_to_string env "" call diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 9ad5bd23c..6009c497a 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2325,7 +2325,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Neg int_ty), effect_info, args, dest) | _ -> craise __FILE__ __LINE__ ctx.span "Unreachable") - | S.Unop (E.Cast cast_kind) -> ( + | S.Unop (E.Cast cast_kind) -> begin match cast_kind with | CastScalar (src_ty, tgt_ty) -> (* Note that cast can fail *) @@ -2344,7 +2344,12 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | CastFnPtr _ -> craise __FILE__ __LINE__ ctx.span "TODO: function casts" | CastUnsize _ -> - craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions") + craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions" + | CastRawPtr _ -> + craise __FILE__ __LINE__ ctx.span "Unsupported: raw ptr casts" + | CastTransmute _ -> + craise __FILE__ __LINE__ ctx.span "Unsupported: transmute" + end | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> diff --git a/flake.lock b/flake.lock index 783e603f1..95540854c 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724768110, - "narHash": "sha256-PPjuaIQa9srw64rDeaatDf3CHPNgLbqwfE0DSdEU37Q=", + "lastModified": 1724838996, + "narHash": "sha256-N8eoK78blhH2HRGenQbTrTxwc9W1JcSe3agcl2yj1AA=", "owner": "aeneasverif", "repo": "charon", - "rev": "13502d2f3bd477ee86acafe5974016dc7707db83", + "rev": "597fe150c3952fd197e37bc7b5ae2cb2f0d07c81", "type": "github" }, "original": { @@ -272,11 +272,11 @@ ] }, "locked": { - "lastModified": 1724725307, - "narHash": "sha256-gnu8JrUFQoy7b927EPuwmWpvk8MSroFl07pplmVueYA=", + "lastModified": 1724811750, + "narHash": "sha256-PvhVgQ1rm3gfhK7ts4emprhh/KMkFwXogmgsQ3srR7g=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "f56076b216c266cd855b0811ceb86802e834cdb9", + "rev": "6a1c4915dca7149e7258d8c7f3ac634d8c65f6c6", "type": "github" }, "original": { From c670b775cc1127247f6b49d2ae82f8aaef43cb20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 28 Aug 2024 13:29:19 +0200 Subject: [PATCH 2/4] Revert accidental push This reverts commit 1d1f6fdb75a79b39e2b8a46a362112da144bc43f. --- charon-pin | 2 +- compiler/FunsAnalysis.ml | 11 ++--------- compiler/InterpreterExpressions.ml | 3 --- compiler/InterpreterStatements.ml | 18 +++++++----------- compiler/InterpreterUtils.ml | 10 ++-------- compiler/Print.ml | 4 ---- compiler/SymbolicToPure.ml | 9 ++------- flake.lock | 12 ++++++------ 8 files changed, 20 insertions(+), 49 deletions(-) diff --git a/charon-pin b/charon-pin index 11d1fc205..cab9e427d 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -597fe150c3952fd197e37bc7b5ae2cb2f0d07c81 +13502d2f3bd477ee86acafe5974016dc7707db83 diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index a5d918de8..6a439dc14 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -104,15 +104,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_rvalue _env rv = match rv with - | Use _ - | RvRef _ - | Global _ - | Discriminant _ - | Aggregate _ - | Len _ - | NullaryOp _ - | RawPtr _ - | ShallowInitBox _ -> () + | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ | Len _ + -> () | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail | BinaryOp (bop, _, _) -> can_fail := binop_can_fail bop || !can_fail diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index af3a4958e..4cad6a989 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -862,9 +862,6 @@ let eval_rvalue_not_global (config : config) (span : Meta.span) AST" | Global _ -> craise __FILE__ __LINE__ span "Unreachable" | Len _ -> craise __FILE__ __LINE__ span "Unhandled Len" - | _ -> - craise __FILE__ __LINE__ span - ("Unsupported operation: " ^ Print.EvalCtx.rvalue_to_string ctx rvalue) let eval_fake_read (config : config) (span : Meta.span) (p : place) : cm_fun = fun ctx -> diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 310d4bd17..09d654534 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -952,22 +952,18 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun = | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable" | Len _ -> craise __FILE__ __LINE__ st.span "Len is not handled yet" - | ShallowInitBox _ -> - craise __FILE__ __LINE__ st.span "ShallowInitBox" | Use _ | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) - | NullaryOp _ - | UnaryOp _ - | BinaryOp _ - | Discriminant _ - | Aggregate _ - | RawPtr _ -> - let p = S.mk_mplace st.span p ctx in + | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> let rp = rvalue_get_place rvalue in let rp = - Option.map (fun rp -> S.mk_mplace st.span rp ctx) rp + match rp with + | Some rp -> Some (S.mk_mplace st.span rp ctx) + | None -> None in - S.synthesize_assignment ctx p rv rp + S.synthesize_assignment ctx + (S.mk_mplace st.span p ctx) + rv rp in let ctx, cc = comp cc (assign_to_place config st.span rv p ctx) diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index f3aee8ff3..f577153f3 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -293,14 +293,8 @@ let rvalue_get_place (rv : rvalue) : place option = match rv with | Use (Copy p | Move p) -> Some p | Use (Constant _) -> None - | Len (p, _, _) | RvRef (p, _) | RawPtr (p, _) -> Some p - | NullaryOp _ - | UnaryOp _ - | BinaryOp _ - | Global _ - | Discriminant _ - | Aggregate _ -> None - | ShallowInitBox _ -> failwith "ShallowInitBox" + | Len (p, _, _) | RvRef (p, _) -> Some p + | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None (** See {!ValuesUtils.symbolic_value_has_borrows} *) let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool = diff --git a/compiler/Print.ml b/compiler/Print.ml index b91a069b8..90dadbccd 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -613,10 +613,6 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in operand_to_string env op - let rvalue_to_string (ctx : eval_ctx) (rval : rvalue) : string = - let env = eval_ctx_to_fmt_env ctx in - rvalue_to_string env rval - let call_to_string (ctx : eval_ctx) (call : call) : string = let env = eval_ctx_to_fmt_env ctx in call_to_string env "" call diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 6009c497a..9ad5bd23c 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2325,7 +2325,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Neg int_ty), effect_info, args, dest) | _ -> craise __FILE__ __LINE__ ctx.span "Unreachable") - | S.Unop (E.Cast cast_kind) -> begin + | S.Unop (E.Cast cast_kind) -> ( match cast_kind with | CastScalar (src_ty, tgt_ty) -> (* Note that cast can fail *) @@ -2344,12 +2344,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | CastFnPtr _ -> craise __FILE__ __LINE__ ctx.span "TODO: function casts" | CastUnsize _ -> - craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions" - | CastRawPtr _ -> - craise __FILE__ __LINE__ ctx.span "Unsupported: raw ptr casts" - | CastTransmute _ -> - craise __FILE__ __LINE__ ctx.span "Unsupported: transmute" - end + craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions") | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> diff --git a/flake.lock b/flake.lock index 95540854c..783e603f1 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724838996, - "narHash": "sha256-N8eoK78blhH2HRGenQbTrTxwc9W1JcSe3agcl2yj1AA=", + "lastModified": 1724768110, + "narHash": "sha256-PPjuaIQa9srw64rDeaatDf3CHPNgLbqwfE0DSdEU37Q=", "owner": "aeneasverif", "repo": "charon", - "rev": "597fe150c3952fd197e37bc7b5ae2cb2f0d07c81", + "rev": "13502d2f3bd477ee86acafe5974016dc7707db83", "type": "github" }, "original": { @@ -272,11 +272,11 @@ ] }, "locked": { - "lastModified": 1724811750, - "narHash": "sha256-PvhVgQ1rm3gfhK7ts4emprhh/KMkFwXogmgsQ3srR7g=", + "lastModified": 1724725307, + "narHash": "sha256-gnu8JrUFQoy7b927EPuwmWpvk8MSroFl07pplmVueYA=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "6a1c4915dca7149e7258d8c7f3ac634d8c65f6c6", + "rev": "f56076b216c266cd855b0811ceb86802e834cdb9", "type": "github" }, "original": { From 5ff9ef2fed81d860df837eaa311cc82f142220c1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 28 Aug 2024 13:28:18 +0200 Subject: [PATCH 3/4] Update charon --- charon-pin | 2 +- compiler/FunsAnalysis.ml | 11 +++++++++-- compiler/InterpreterExpressions.ml | 3 +++ compiler/InterpreterStatements.ml | 18 +++++++++++------- compiler/InterpreterUtils.ml | 10 ++++++++-- compiler/Print.ml | 4 ++++ compiler/SymbolicToPure.ml | 9 +++++++-- flake.lock | 12 ++++++------ 8 files changed, 49 insertions(+), 20 deletions(-) diff --git a/charon-pin b/charon-pin index cab9e427d..11d1fc205 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -13502d2f3bd477ee86acafe5974016dc7707db83 +597fe150c3952fd197e37bc7b5ae2cb2f0d07c81 diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 6a439dc14..a5d918de8 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -104,8 +104,15 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_rvalue _env rv = match rv with - | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ | Len _ - -> () + | Use _ + | RvRef _ + | Global _ + | Discriminant _ + | Aggregate _ + | Len _ + | NullaryOp _ + | RawPtr _ + | ShallowInitBox _ -> () | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail | BinaryOp (bop, _, _) -> can_fail := binop_can_fail bop || !can_fail diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 4cad6a989..af3a4958e 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -862,6 +862,9 @@ let eval_rvalue_not_global (config : config) (span : Meta.span) AST" | Global _ -> craise __FILE__ __LINE__ span "Unreachable" | Len _ -> craise __FILE__ __LINE__ span "Unhandled Len" + | _ -> + craise __FILE__ __LINE__ span + ("Unsupported operation: " ^ Print.EvalCtx.rvalue_to_string ctx rvalue) let eval_fake_read (config : config) (span : Meta.span) (p : place) : cm_fun = fun ctx -> diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 09d654534..310d4bd17 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -952,18 +952,22 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun = | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable" | Len _ -> craise __FILE__ __LINE__ st.span "Len is not handled yet" + | ShallowInitBox _ -> + craise __FILE__ __LINE__ st.span "ShallowInitBox" | Use _ | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) - | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> + | NullaryOp _ + | UnaryOp _ + | BinaryOp _ + | Discriminant _ + | Aggregate _ + | RawPtr _ -> + let p = S.mk_mplace st.span p ctx in let rp = rvalue_get_place rvalue in let rp = - match rp with - | Some rp -> Some (S.mk_mplace st.span rp ctx) - | None -> None + Option.map (fun rp -> S.mk_mplace st.span rp ctx) rp in - S.synthesize_assignment ctx - (S.mk_mplace st.span p ctx) - rv rp + S.synthesize_assignment ctx p rv rp in let ctx, cc = comp cc (assign_to_place config st.span rv p ctx) diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index f577153f3..f3aee8ff3 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -293,8 +293,14 @@ let rvalue_get_place (rv : rvalue) : place option = match rv with | Use (Copy p | Move p) -> Some p | Use (Constant _) -> None - | Len (p, _, _) | RvRef (p, _) -> Some p - | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None + | Len (p, _, _) | RvRef (p, _) | RawPtr (p, _) -> Some p + | NullaryOp _ + | UnaryOp _ + | BinaryOp _ + | Global _ + | Discriminant _ + | Aggregate _ -> None + | ShallowInitBox _ -> failwith "ShallowInitBox" (** See {!ValuesUtils.symbolic_value_has_borrows} *) let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool = diff --git a/compiler/Print.ml b/compiler/Print.ml index 90dadbccd..b91a069b8 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -613,6 +613,10 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in operand_to_string env op + let rvalue_to_string (ctx : eval_ctx) (rval : rvalue) : string = + let env = eval_ctx_to_fmt_env ctx in + rvalue_to_string env rval + let call_to_string (ctx : eval_ctx) (call : call) : string = let env = eval_ctx_to_fmt_env ctx in call_to_string env "" call diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 9ad5bd23c..6009c497a 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2325,7 +2325,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Neg int_ty), effect_info, args, dest) | _ -> craise __FILE__ __LINE__ ctx.span "Unreachable") - | S.Unop (E.Cast cast_kind) -> ( + | S.Unop (E.Cast cast_kind) -> begin match cast_kind with | CastScalar (src_ty, tgt_ty) -> (* Note that cast can fail *) @@ -2344,7 +2344,12 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | CastFnPtr _ -> craise __FILE__ __LINE__ ctx.span "TODO: function casts" | CastUnsize _ -> - craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions") + craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions" + | CastRawPtr _ -> + craise __FILE__ __LINE__ ctx.span "Unsupported: raw ptr casts" + | CastTransmute _ -> + craise __FILE__ __LINE__ ctx.span "Unsupported: transmute" + end | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> diff --git a/flake.lock b/flake.lock index 783e603f1..95540854c 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724768110, - "narHash": "sha256-PPjuaIQa9srw64rDeaatDf3CHPNgLbqwfE0DSdEU37Q=", + "lastModified": 1724838996, + "narHash": "sha256-N8eoK78blhH2HRGenQbTrTxwc9W1JcSe3agcl2yj1AA=", "owner": "aeneasverif", "repo": "charon", - "rev": "13502d2f3bd477ee86acafe5974016dc7707db83", + "rev": "597fe150c3952fd197e37bc7b5ae2cb2f0d07c81", "type": "github" }, "original": { @@ -272,11 +272,11 @@ ] }, "locked": { - "lastModified": 1724725307, - "narHash": "sha256-gnu8JrUFQoy7b927EPuwmWpvk8MSroFl07pplmVueYA=", + "lastModified": 1724811750, + "narHash": "sha256-PvhVgQ1rm3gfhK7ts4emprhh/KMkFwXogmgsQ3srR7g=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "f56076b216c266cd855b0811ceb86802e834cdb9", + "rev": "6a1c4915dca7149e7258d8c7f3ac634d8c65f6c6", "type": "github" }, "original": { From 5ecf716882392ad631b87c56a01aa0cbe952f6bf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 28 Aug 2024 14:29:10 +0200 Subject: [PATCH 4/4] Update charon --- charon-pin | 2 +- compiler/Assumed.ml | 6 - compiler/InterpreterStatements.ml | 237 ++++++++++-------------------- compiler/PrintPure.ml | 1 - compiler/PureMicroPasses.ml | 4 - compiler/SymbolicToPure.ml | 1 - flake.lock | 6 +- 7 files changed, 81 insertions(+), 176 deletions(-) diff --git a/charon-pin b/charon-pin index 11d1fc205..ea1ad5753 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -597fe150c3952fd197e37bc7b5ae2cb2f0d07c81 +79355ca1a90eccd7e3c3ded0fe3d1473a91f20ac diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index d1f6da940..9aa71216f 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -240,12 +240,6 @@ let raw_assumed_fun_infos : raw_assumed_fun_info list = false, "alloc::boxed::Box::new", Some [ true; false ] ); - (* BoxFree shouldn't be used *) - ( BoxFree, - Sig.box_free_sig, - false, - "alloc::boxed::Box::free", - Some [ true; false ] ); (* Array Index *) ( ArrayIndexShared, Sig.array_index_sig false, diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 310d4bd17..6e82b4cdc 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -281,28 +281,20 @@ let push_frame (ctx : eval_ctx) : eval_ctx = ctx_push_frame ctx let get_assumed_function_return_type (span : Meta.span) (ctx : eval_ctx) (fid : assumed_fun_id) (generics : generic_args) : ety = sanity_check __FILE__ __LINE__ (generics.trait_refs = []) span; - (* [Box::free] has a special treatment *) - match fid with - | BoxFree -> - sanity_check __FILE__ __LINE__ (generics.regions = []) span; - sanity_check __FILE__ __LINE__ (List.length generics.types = 1) span; - sanity_check __FILE__ __LINE__ (generics.const_generics = []) span; - mk_unit_ty - | _ -> - (* Retrieve the function's signature *) - let sg = Assumed.get_assumed_fun_sig fid in - (* Instantiate the return type *) - (* There shouldn't be any reference to Self *) - let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in - let generics = Subst.generic_args_erase_regions generics in - let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = - Subst.make_subst_from_generics sg.generics generics tr_self - in - let ty = - Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self - sg.output - in - AssociatedTypes.ctx_normalize_erase_ty span ctx ty + (* Retrieve the function's signature *) + let sg = Assumed.get_assumed_fun_sig fid in + (* Instantiate the return type *) + (* There shouldn't be any reference to Self *) + let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in + let generics = Subst.generic_args_erase_regions generics in + let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = + Subst.make_subst_from_generics sg.generics generics tr_self + in + let ty = + Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self + sg.output + in + AssociatedTypes.ctx_normalize_erase_ty span ctx ty let move_return_value (config : config) (span : Meta.span) (pop_return_value : bool) (ctx : eval_ctx) : @@ -434,45 +426,6 @@ let eval_box_new_concrete (config : config) (span : Meta.span) comp cc (assign_to_place config span box_v dest ctx) | _ -> craise __FILE__ __LINE__ span "Inconsistent state" -(** Auxiliary function - see {!eval_assumed_function_call}. - - [Box::free] is not handled the same way as the other assumed functions: - - in the regular case, whenever we need to evaluate an assumed function, - we evaluate the operands, push a frame, call a dedicated function - to correctly update the variables in the frame (and mimic the execution - of a body) and finally pop the frame - - in the case of [Box::free]: the value given to this function is often - of the form [Box(⊥)] because we can move the value out of the - box before freeing the box. It makes it invalid to see box_free as a - "regular" function: it is not valid to call a function with arguments - which contain [⊥]. For this reason, we execute [Box::free] as drop_value, - but this is a bit annoying with regards to the semantics... - - Followingly this function doesn't behave like the others: it does not expect - a stack frame to have been pushed, but rather simply behaves like {!drop_value}. - It thus updates the box value (by calling {!drop_value}) and updates - the destination (by setting it to [()]). -*) -let eval_box_free (config : config) (span : Meta.span) (generics : generic_args) - (args : operand list) (dest : place) : cm_fun = - fun ctx -> - match (generics.regions, generics.types, generics.const_generics, args) with - | [], [ boxed_ty ], [], [ Move input_box_place ] -> - (* Required type checking *) - let input_box = - InterpreterPaths.read_place span Write input_box_place ctx - in - (let input_ty = ty_get_box input_box.ty in - sanity_check __FILE__ __LINE__ (input_ty = boxed_ty)) - span; - - (* Drop the value *) - let ctx, cc = drop_value config span input_box_place ctx in - - (* Update the destination by setting it to [()] *) - comp cc (assign_to_place config span mk_unit_value dest ctx) - | _ -> craise __FILE__ __LINE__ span "Inconsistent state" - (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : config) (span : Meta.span) (fid : assumed_fun_id) (call : call) : cm_fun = @@ -483,72 +436,59 @@ let eval_assumed_function_call_concrete (config : config) (span : Meta.span) | FnOpMove _ -> (* Closure case: TODO *) craise __FILE__ __LINE__ span "Closures are not supported yet" - | FnOpRegular func -> ( + | FnOpRegular func -> let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) sanity_check __FILE__ __LINE__ (generics.const_generics = []) span; - (* There are two cases (and this is extremely annoying): - - the function is not box_free - - the function is box_free - See {!eval_box_free} - *) - match fid with - | BoxFree -> - (* Degenerate case: box_free *) - eval_box_free config span generics args dest ctx - | _ -> - (* "Normal" case: not box_free *) - (* Evaluate the operands *) - (* let ctx, args_vl = eval_operands config ctx args in *) - let args_vl, ctx, cc = eval_operands config span args ctx in - - (* Evaluate the call - * - * Style note: at some point we used {!comp_transmit} to - * transmit the result of {!eval_operands} above down to {!push_vars} - * below, without having to introduce an intermediary function call, - * but it made it less clear where the computed values came from, - * so we reversed the modifications. *) - (* Push the stack frame: we initialize the frame with the return variable, - and one variable per input argument *) - let ctx = push_frame ctx in - - (* Create and push the return variable *) - let ret_vid = VarId.zero in - let ret_ty = get_assumed_function_return_type span ctx fid generics in - let ret_var = mk_var ret_vid (Some "@return") ret_ty in - let ctx = push_uninitialized_var span ret_var ctx in - - (* Create and push the input variables *) - let input_vars = - VarId.mapi_from1 - (fun id (v : typed_value) -> (mk_var id None v.ty, v)) - args_vl - in - let ctx = push_vars span input_vars ctx in - - (* "Execute" the function body. As the functions are assumed, here we call - * custom functions to perform the proper manipulations: we don't have - * access to a body. *) - let ctx, cf_eval_body = - match fid with - | BoxNew -> eval_box_new_concrete config span generics ctx - | BoxFree -> - (* Should have been treated above *) - craise __FILE__ __LINE__ span "Unreachable" - | ArrayIndexShared - | ArrayIndexMut - | ArrayToSliceShared - | ArrayToSliceMut - | ArrayRepeat - | SliceIndexShared - | SliceIndexMut -> craise __FILE__ __LINE__ span "Unimplemented" - in - let cc = cc_comp cc cf_eval_body in - (* Pop the frame *) - comp cc (pop_frame_assign config span dest ctx)) + (* Evaluate the operands *) + (* let ctx, args_vl = eval_operands config ctx args in *) + let args_vl, ctx, cc = eval_operands config span args ctx in + + (* Evaluate the call + * + * Style note: at some point we used {!comp_transmit} to + * transmit the result of {!eval_operands} above down to {!push_vars} + * below, without having to introduce an intermediary function call, + * but it made it less clear where the computed values came from, + * so we reversed the modifications. *) + (* Push the stack frame: we initialize the frame with the return variable, + and one variable per input argument *) + let ctx = push_frame ctx in + + (* Create and push the return variable *) + let ret_vid = VarId.zero in + let ret_ty = get_assumed_function_return_type span ctx fid generics in + let ret_var = mk_var ret_vid (Some "@return") ret_ty in + let ctx = push_uninitialized_var span ret_var ctx in + + (* Create and push the input variables *) + let input_vars = + VarId.mapi_from1 + (fun id (v : typed_value) -> (mk_var id None v.ty, v)) + args_vl + in + let ctx = push_vars span input_vars ctx in + + (* "Execute" the function body. As the functions are assumed, here we call + * custom functions to perform the proper manipulations: we don't have + * access to a body. *) + let ctx, cf_eval_body = + match fid with + | BoxNew -> eval_box_new_concrete config span generics ctx + | ArrayIndexShared + | ArrayIndexMut + | ArrayToSliceShared + | ArrayToSliceMut + | ArrayRepeat + | SliceIndexShared + | SliceIndexMut -> craise __FILE__ __LINE__ span "Unimplemented" + in + let cc = cc_comp cc cf_eval_body in + + (* Pop the frame *) + comp cc (pop_frame_assign config span dest ctx) (** Helper @@ -1552,45 +1492,22 @@ and eval_assumed_function_call_symbolic (config : config) (span : Meta.span) generics.types) span; - (* There are two cases (and this is extremely annoying): - - the function is not box_free - - the function is box_free - See {!eval_box_free} - *) - match fid with - | BoxFree -> - (* Degenerate case: box_free - note that this is not really a function - * call: no need to call a "synthesize_..." function *) - let ctx, cc = eval_box_free config span generics args dest ctx in - ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc) - | _ -> - (* "Normal" case: not box_free *) - (* In symbolic mode, the behaviour of a function call is completely defined - * by the signature of the function: we thus simply generate correctly - * instantiated signatures, and delegate the work to an auxiliary function *) - let sg, regions_hierarchy, inst_sig = - match fid with - | BoxFree -> - (* Should have been treated above *) - craise __FILE__ __LINE__ span "Unreachable" - | _ -> - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FAssumed fid) - ctx.fun_ctx.regions_hierarchies - in - (* There shouldn't be any reference to Self *) - let tr_self = UnknownTrait __FUNCTION__ in - let sg = Assumed.get_assumed_fun_sig fid in - let inst_sg = - instantiate_fun_sig span ctx generics tr_self sg regions_hierarchy - in - (sg, regions_hierarchy, inst_sg) - in + (* In symbolic mode, the behaviour of a function call is completely defined + * by the signature of the function: we thus simply generate correctly + * instantiated signatures, and delegate the work to an auxiliary function *) + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FAssumed fid) ctx.fun_ctx.regions_hierarchies + in + (* There shouldn't be any reference to Self *) + let tr_self = UnknownTrait __FUNCTION__ in + let sg = Assumed.get_assumed_fun_sig fid in + let inst_sig = + instantiate_fun_sig span ctx generics tr_self sg regions_hierarchy + in - (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config span - (FunId (FAssumed fid)) sg regions_hierarchy inst_sig generics None args - dest ctx + (* Evaluate the function call *) + eval_function_call_symbolic_from_inst_sig config span (FunId (FAssumed fid)) + sg regions_hierarchy inst_sig generics None args dest ctx (** Evaluate a statement seen as a function body *) and eval_function_body (config : config) (body : statement) : stl_cm_fun = diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index d8fd18ba7..3de4e0d2d 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -491,7 +491,6 @@ let fun_suffix (lp_id : LoopId.id option) : string = let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = match fid with | BoxNew -> "alloc::boxed::Box::new" - | BoxFree -> "alloc::alloc::box_free" | ArrayIndexShared -> "@ArrayIndexShared" | ArrayIndexMut -> "@ArrayIndexMut" | ArrayToSliceShared -> "@ArrayToSliceShared" diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index a85f90af2..c613bdbfd 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1587,10 +1587,6 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = | BoxNew -> let arg, args = Collections.List.pop args in mk_apps def.item_meta.span arg args - | BoxFree -> - sanity_check __FILE__ __LINE__ (args = []) - def.item_meta.span; - mk_unit_rvalue | SliceIndexShared | SliceIndexMut | ArrayIndexShared diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 6009c497a..6235c2856 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2195,7 +2195,6 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | FunId (FAssumed fid) -> ( match fid with | BoxNew -> "box_new" - | BoxFree -> "box_free" | ArrayRepeat -> "array_repeat" | ArrayIndexShared -> "index_shared" | ArrayIndexMut -> "index_mut" diff --git a/flake.lock b/flake.lock index 95540854c..223ba62b9 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724838996, - "narHash": "sha256-N8eoK78blhH2HRGenQbTrTxwc9W1JcSe3agcl2yj1AA=", + "lastModified": 1724846699, + "narHash": "sha256-m/dXyJzTroHxLWWWxOp+6kpGSc3UsYXz3DaHVklR8xY=", "owner": "aeneasverif", "repo": "charon", - "rev": "597fe150c3952fd197e37bc7b5ae2cb2f0d07c81", + "rev": "79355ca1a90eccd7e3c3ded0fe3d1473a91f20ac", "type": "github" }, "original": {