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": {