From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 31 Aug 2023 12:47:43 +0200 Subject: Start adding support for traits --- compiler/FunsAnalysis.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index b72fa078..f4406653 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -70,14 +70,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_rvalue _env rv = match rv with - | Use _ | Ref _ | Global _ | Discriminant _ | Aggregate _ -> () + | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ -> () | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail | BinaryOp (bop, _, _) -> can_fail := EU.binop_can_fail bop || !can_fail method! visit_Call env call = (match call.func with - | Regular id -> + | FunId (Regular id) -> if FunDeclId.Set.mem id fun_ids then ( can_diverge := true; is_rec := true) @@ -86,9 +86,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) self#may_fail info.can_fail; stateful := !stateful || info.stateful; can_diverge := !can_diverge || info.can_diverge - | Assumed id -> + | FunId (Assumed id) -> (* None of the assumed functions can diverge nor are considered stateful *) - can_fail := !can_fail || Assumed.assumed_can_fail id); + can_fail := !can_fail || Assumed.assumed_can_fail id + | TraitMethod _ -> + (* We consider trait functions can fail, diverge, and are not stateful *) + can_fail := true; + can_diverge := true); super#visit_Call env call method! visit_Panic env = @@ -141,7 +145,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let rec analyze_decl_groups (decls : declaration_group list) : unit = match decls with | [] -> () - | Type _ :: decls' -> analyze_decl_groups decls' + | (Type _ | TraitDecl _ | TraitImpl _) :: decls' -> + analyze_decl_groups decls' | Fun decl :: decls' -> analyze_fun_decl_group decl; analyze_decl_groups decls' -- cgit v1.3.1 From f11d5186b467df318f7c09eedf8b5629c165b453 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 20 Oct 2023 15:05:00 +0200 Subject: Start updating to handle function pointers --- compiler/AssociatedTypes.ml | 12 +++++- compiler/Assumed.ml | 2 +- compiler/Extract.ml | 4 +- compiler/ExtractBase.ml | 2 +- compiler/FunsAnalysis.ml | 2 +- compiler/InterpreterExpansion.ml | 2 +- compiler/InterpreterExpressions.ml | 9 +++-- compiler/InterpreterStatements.ml | 78 +++++++++++++++++++++----------------- compiler/InterpreterUtils.ml | 5 +++ compiler/Print.ml | 23 +++++++++++ compiler/PrintPure.ml | 22 +++++------ compiler/PureMicroPasses.ml | 32 ++++++++-------- compiler/SymbolicToPure.ml | 50 +++++++++++++----------- compiler/SynthesizeSymbolic.ml | 2 +- compiler/Translate.ml | 10 ++--- compiler/TypesAnalysis.ml | 8 ++++ 16 files changed, 163 insertions(+), 100 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 992dade9..022aad2f 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -157,7 +157,8 @@ let ctx_add_norm_trait_types_from_preds (ctx : C.eval_ctx) let rec trait_instance_id_is_local_clause (id : 'r T.trait_instance_id) : bool = match id with | T.Self | Clause _ -> true - | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ -> false + | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _ -> + false | ParentClause (id, _, _) | ItemClause (id, _, _, _) -> trait_instance_id_is_local_clause id @@ -187,6 +188,10 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty = | Ref (r, ty, rkind) -> let ty = ctx_normalize_ty ctx ty in T.Ref (r, ty, rkind) + | Arrow (inputs, output) -> + let inputs = List.map (ctx_normalize_ty ctx) inputs in + let output = ctx_normalize_ty ctx output in + Arrow (inputs, output) | TraitType (trait_ref, generics, type_name) -> ( log#ldebug (lazy @@ -401,6 +406,11 @@ and ctx_normalize_trait_instance_id : assert (trait_instance_id_is_local_clause trait_ref.trait_id); assert (trait_ref.generics = TypesUtils.mk_empty_generic_args); (trait_ref.trait_id, None) + | FnPointer ty -> + let ty = ctx_normalize_ty ctx ty in + (* TODO: we might want to return the ref to the function pointer, + in order to later normalize a call to this function pointer *) + (FnPointer ty, None) | UnknownTrait _ -> (* This is actually an error case *) (id, None) diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 109175af..b1ec0660 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -347,7 +347,7 @@ let assumed_infos : assumed_info list = let vec_pre = [ "alloc"; "vec"; "Vec" ] in let index_pre = [ "core"; "ops"; "index" ] in [ - (A.Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]); + (Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]); (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]); ( BoxFree, Sig.box_free_sig, diff --git a/compiler/Extract.ml b/compiler/Extract.ml index ac81d6f3..688f6ce3 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2696,7 +2696,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) (* Provided method: we see it as a regular function call, and use the function name *) let fun_id = - FromLlbc (FunId (A.Regular method_id.id), lp_id, rg_id) + FromLlbc (FunId (Regular method_id.id), lp_id, rg_id) in let fun_name = ctx_get_function with_opaque_pre fun_id ctx in F.pp_print_string fmt fun_name; @@ -3519,7 +3519,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = let { keep_fwd; num_backs } = PureUtils.RegularFunIdMap.find - (Pure.FunId (A.Regular def.def_id), def.loop_id, def.back_id) + (Pure.FunId (Regular def.def_id), def.loop_id, def.back_id) ctx.fun_name_info in let comment_pre = "[" ^ Print.fun_name_to_string def.basename ^ "]: " in diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 1586e6ed..a921515b 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1482,7 +1482,7 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map = let assumed_functions = List.map (fun (fid, rg, name) -> - (FromLlbc (Pure.FunId (A.Assumed fid), None, rg), name)) + (FromLlbc (Pure.FunId (Assumed fid), None, rg), name)) init.assumed_llbc_functions @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions in diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f4406653..a09a6d05 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -76,7 +76,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) can_fail := EU.binop_can_fail bop || !can_fail method! visit_Call env call = - (match call.func with + (match call.func.func with | FunId (Regular id) -> if FunDeclId.Set.mem id fun_ids then ( can_diverge := true; diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index ea692386..c1041fa3 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -709,7 +709,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = raise (Failure "Attempted to greedily expand an ADT which can't be expanded ") - | T.TypeVar _ | T.Literal _ | Never | T.TraitType _ -> + | T.TypeVar _ | T.Literal _ | Never | T.TraitType _ | T.Arrow _ -> raise (Failure "Unreachable") in (* Compose and continue *) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 29826233..a42c552a 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -271,7 +271,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) match cv.value with | E.CLiteral lit -> cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx - | E.TraitConst (trait_ref, generics, const_name) -> ( + | E.CTraitConst (trait_ref, generics, const_name) -> ( assert (generics = TypesUtils.mk_empty_generic_args); match trait_ref.trait_id with | T.TraitImpl _ -> @@ -329,7 +329,8 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) None, value_as_symbolic v.value, SymbolicAst.ConstGenericValue vid, - e )))) + e ))) + | E.CFnPtr _ -> raise (Failure "TODO")) | E.Copy p -> (* Access the value *) let access = Read in @@ -426,7 +427,7 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand) match mk_scalar sv.int_ty i with | Error _ -> cf (Error EPanic) | Ok sv -> cf (Ok { v with V.value = V.Literal (PV.Scalar sv) })) - | E.Cast (src_ty, tgt_ty), V.Literal (PV.Scalar sv) -> ( + | E.Cast (E.CastInteger (src_ty, tgt_ty)), V.Literal (PV.Scalar sv) -> ( assert (src_ty = sv.int_ty); let i = sv.PV.value in match mk_scalar tgt_ty i with @@ -452,7 +453,7 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand) match (unop, v.V.ty) with | E.Not, (T.Literal Bool as lty) -> lty | E.Neg, (T.Literal (Integer _) as lty) -> lty - | E.Cast (_, tgt_ty), _ -> T.Literal (Integer tgt_ty) + | E.Cast (E.CastInteger (_, tgt_ty)), _ -> T.Literal (Integer tgt_ty) | _ -> raise (Failure "Invalid input for unop") in let res_sv = diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 36bc3492..9f35c6f2 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -306,7 +306,7 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id) assert (generics.trait_refs = []); (* [Box::free] has a special treatment *) match fid with - | A.BoxFree -> + | BoxFree -> assert (generics.regions = []); assert (List.length generics.types = 1); assert (generics.const_generics = []); @@ -583,7 +583,7 @@ let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : C.config) (fid : A.assumed_fun_id) (call : A.call) : cm_fun = - let generics = call.generics in + let generics = call.func.generics in let args = call.args in let dest = call.dest in (* Sanity check: we don't fully handle the const generic vars environment @@ -595,7 +595,7 @@ let eval_assumed_function_call_concrete (config : C.config) See {!eval_box_free} *) match fid with - | A.BoxFree -> + | BoxFree -> (* Degenerate case: box_free *) eval_box_free config generics args dest | _ -> @@ -636,7 +636,7 @@ let eval_assumed_function_call_concrete (config : C.config) * access to a body. *) let cf_eval_body : cm_fun = match fid with - | A.Replace -> eval_replace_concrete config generics + | Replace -> eval_replace_concrete config generics | BoxNew -> eval_box_new_concrete config generics | BoxDeref -> eval_box_deref_concrete config generics | BoxDerefMut -> eval_box_deref_mut_concrete config generics @@ -854,15 +854,14 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id) match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body (without arguments) *) - let call = + let func = { - A.func = A.FunId (A.Regular global.body_id); + E.func = FunId (Regular global.body_id); generics = TypesUtils.mk_empty_generic_args; trait_and_method_generic_args = None; - args = []; - dest; } in + let call = { A.func; args = []; dest } in (eval_transparent_function_call_concrete config global.body_id call) cf ctx | SymbolicMode -> @@ -1019,29 +1018,28 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = and eval_function_call_concrete (config : C.config) (call : A.call) : st_cm_fun = fun cf ctx -> - match call.func with - | A.FunId (A.Regular fid) -> + match call.func.func with + | FunId (Regular fid) -> eval_transparent_function_call_concrete config fid call cf ctx - | A.FunId (A.Assumed fid) -> + | FunId (Assumed fid) -> (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) eval_assumed_function_call_concrete config fid call (cf Unit) ctx - | A.TraitMethod _ -> raise (Failure "Unimplemented") + | TraitMethod _ -> raise (Failure "Unimplemented") and eval_function_call_symbolic (config : C.config) (call : A.call) : st_cm_fun = - match call.func with - | A.FunId (A.Regular _) | A.TraitMethod _ -> + match call.func.func with + | FunId (Regular _) | TraitMethod _ -> eval_transparent_function_call_symbolic config call - | A.FunId (A.Assumed fid) -> - eval_assumed_function_call_symbolic config fid call + | FunId (Assumed fid) -> eval_assumed_function_call_symbolic config fid call (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_transparent_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (call : A.call) : st_cm_fun = - let generics = call.A.generics in + let generics = call.func.generics in let args = call.A.args in let dest = call.A.dest in (* Sanity check: we don't fully handle the const generic vars environment @@ -1195,29 +1193,29 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) to a trait clause but directly to the method provided in the trait declaration. *) let func, generics, def, inst_sg = - match call.func with - | A.FunId (A.Regular fid) -> + match call.func.func with + | FunId (Regular fid) -> let def = C.ctx_lookup_fun_decl ctx fid in let tr_self = T.UnknownTrait __FUNCTION__ in let inst_sg = - instantiate_fun_sig ctx call.generics tr_self def.A.signature + instantiate_fun_sig ctx call.func.generics tr_self def.A.signature in - (call.func, call.generics, def, inst_sg) - | A.FunId (A.Assumed _) -> + (call.func.func, call.func.generics, def, inst_sg) + | FunId (Assumed _) -> (* Unreachable: must be a transparent function *) raise (Failure "Unreachable") - | A.TraitMethod (trait_ref, method_name, _) -> ( + | TraitMethod (trait_ref, method_name, _) -> ( log#ldebug (lazy ("trait method call:\n- call: " ^ call_to_string ctx call ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" - ^ egeneric_args_to_string ctx call.generics + ^ egeneric_args_to_string ctx call.func.generics ^ "\n- trait and method generics:\n" ^ egeneric_args_to_string ctx - (Option.get call.trait_and_method_generic_args))); + (Option.get call.func.trait_and_method_generic_args))); (* When instantiating, we need to group the generics for the trait ref and the method *) - let generics = Option.get call.trait_and_method_generic_args in + let generics = Option.get call.func.trait_and_method_generic_args in (* Lookup the trait method signature - there are several possibilities depending on whethere we call a top-level trait method impl or the method from a local clause *) @@ -1251,7 +1249,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) which implements the method. In order to do this properly, we also need to update the generics. *) - let func = A.FunId (A.Regular id) in + let func = E.FunId (Regular id) in (func, generics, method_def, inst_sg) | None -> (* If not found, lookup the methods provided by the trait *declaration* @@ -1287,7 +1285,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) *) let all_generics = TypesUtils.merge_generic_args - trait_ref.trait_decl_ref.decl_generics call.generics + trait_ref.trait_decl_ref.decl_generics call.func.generics in log#ldebug (lazy @@ -1304,7 +1302,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) instantiate_fun_sig ctx all_generics tr_self method_def.A.signature in - (call.func, call.generics, method_def, inst_sg)) + (call.func.func, call.func.generics, method_def, inst_sg)) | _ -> (* We are using a local clause - we lookup the trait decl *) let trait_decl = @@ -1333,7 +1331,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx generics tr_self method_def.A.signature in - (call.func, call.generics, method_def, inst_sg)) + (call.func.func, call.func.generics, method_def, inst_sg)) in (* Sanity check *) assert (List.length call.args = List.length def.A.signature.inputs); @@ -1357,6 +1355,18 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> + log#ldebug + (lazy + ("eval_function_call_symbolic_from_inst_sig:\n- fid: " + ^ fun_id_or_trait_method_ref_to_string ctx fid + ^ "\n- inst_sg:\n" + ^ inst_fun_sig_to_string ctx inst_sg + ^ "\n- call.generics:\n" + ^ egeneric_args_to_string ctx generics + ^ "\n- args:\n" + ^ String.concat ", " (List.map (operand_to_string ctx) args) + ^ "\n- dest:\n" ^ place_to_string ctx dest)); + (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in @@ -1487,7 +1497,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) and eval_assumed_function_call_symbolic (config : C.config) (fid : A.assumed_fun_id) (call : A.call) : st_cm_fun = fun cf ctx -> - let generics = call.generics in + let generics = call.func.generics in let args = call.args in let dest = call.dest in (* Sanity check: make sure the type parameters don't contain regions - @@ -1503,7 +1513,7 @@ and eval_assumed_function_call_symbolic (config : C.config) See {!eval_box_free} *) match fid with - | A.BoxFree -> + | BoxFree -> (* Degenerate case: box_free - note that this is not really a function * call: no need to call a "synthesize_..." function *) eval_box_free config generics args dest (cf Unit) ctx @@ -1514,7 +1524,7 @@ and eval_assumed_function_call_symbolic (config : C.config) * instantiated signatures, and delegate the work to an auxiliary function *) let inst_sig = match fid with - | A.BoxFree -> + | BoxFree -> (* should have been treated above *) raise (Failure "Unreachable") | _ -> @@ -1525,7 +1535,7 @@ and eval_assumed_function_call_symbolic (config : C.config) in (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config (A.FunId (A.Assumed fid)) + eval_function_call_symbolic_from_inst_sig config (FunId (Assumed fid)) inst_sig generics args dest cf ctx (** Evaluate a statement seen as a function body *) diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 7aaee6ff..6e08e553 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -46,6 +46,11 @@ let operand_to_string = PA.operand_to_string let egeneric_args_to_string = PA.egeneric_args_to_string let rtrait_instance_id_to_string = PA.rtrait_instance_id_to_string let fun_sig_to_string = PA.fun_sig_to_string +let inst_fun_sig_to_string = PA.inst_fun_sig_to_string + +let fun_id_or_trait_method_ref_to_string = + PA.fun_id_or_trait_method_ref_to_string + let fun_decl_to_string = PA.fun_decl_to_string let call_to_string = PA.call_to_string diff --git a/compiler/Print.ml b/compiler/Print.ml index 5d5c16ee..1d5ddc50 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -359,6 +359,18 @@ module Values = struct ^ "}" ^ "{regions=" ^ T.RegionId.Set.to_string None abs.regions ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}" + + let inst_fun_sig_to_string (fmt : value_formatter) (sg : LlbcAst.inst_fun_sig) + : string = + (* TODO: print the trait type constraints? *) + let ty_fmt = value_to_rtype_formatter fmt in + let ty_to_string = PT.ty_to_string ty_fmt in + + let inputs = + "(" ^ String.concat ", " (List.map ty_to_string sg.inputs) ^ ")" + in + let output = ty_to_string sg.output in + inputs ^ " -> " ^ output end module PV = Values (* local module *) @@ -755,6 +767,17 @@ module EvalCtxLlbcAst = struct let fmt = PC.eval_ctx_to_ast_formatter ctx in PA.fun_sig_to_string fmt "" " " x + let inst_fun_sig_to_string (ctx : C.eval_ctx) (x : LlbcAst.inst_fun_sig) : + string = + let fmt = PC.eval_ctx_to_ast_formatter ctx in + let fmt = PC.ast_to_value_formatter fmt in + PV.inst_fun_sig_to_string fmt x + + let fun_id_or_trait_method_ref_to_string (ctx : C.eval_ctx) + (x : E.fun_id_or_trait_method_ref) : string = + let fmt = PC.eval_ctx_to_ast_formatter ctx in + PE.fun_id_or_trait_method_ref_to_string fmt x "..." + let statement_to_string (ctx : C.eval_ctx) (indent : string) (indent_incr : string) (e : A.statement) : string = let fmt = PC.eval_ctx_to_ast_formatter ctx in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 5fb5978b..be7b3cb4 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -593,17 +593,17 @@ let fun_suffix (lp_id : LoopId.id option) (rg_id : T.RegionGroupId.id option) : let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = match fid with - | A.Replace -> "core::mem::replace" - | A.BoxNew -> "alloc::boxed::Box::new" - | A.BoxDeref -> "core::ops::deref::Deref::deref" - | A.BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut" - | A.BoxFree -> "alloc::alloc::box_free" - | A.VecNew -> "alloc::vec::Vec::new" - | A.VecPush -> "alloc::vec::Vec::push" - | A.VecInsert -> "alloc::vec::Vec::insert" - | A.VecLen -> "alloc::vec::Vec::len" - | A.VecIndex -> "core::ops::index::Index::index" - | A.VecIndexMut -> "core::ops::index::IndexMut::index_mut" + | Replace -> "core::mem::replace" + | BoxNew -> "alloc::boxed::Box::new" + | BoxDeref -> "core::ops::deref::Deref::deref" + | BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut" + | BoxFree -> "alloc::alloc::box_free" + | VecNew -> "alloc::vec::Vec::new" + | VecPush -> "alloc::vec::Vec::push" + | VecInsert -> "alloc::vec::Vec::insert" + | VecLen -> "alloc::vec::Vec::len" + | VecIndex -> "core::ops::index::Index::index" + | VecIndexMut -> "core::ops::index::IndexMut::index_mut" | ArrayIndexShared -> "@ArrayIndexShared" | ArrayIndexMut -> "@ArrayIndexMut" | ArrayToSliceShared -> "@ArrayToSliceShared" diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index cedc3559..b00509a6 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -791,7 +791,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) let id0 = match id0 with | FunId fun_id -> fun_id - | TraitMethod (_, _, fun_decl_id) -> A.Regular fun_decl_id + | TraitMethod (_, _, fun_decl_id) -> Regular fun_decl_id in LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls in @@ -1523,29 +1523,29 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = match opt_destruct_function_call e with | Some (fun_id, _tys, args) -> ( match fun_id with - | Fun (FromLlbc (FunId (A.Assumed aid), _lp_id, rg_id)) -> ( + | Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> ( (* Below, when dealing with the arguments: we consider the very * general case, where functions could be boxed (meaning we * could have: [box_new f x]) * *) match (aid, rg_id) with - | A.BoxNew, _ -> + | BoxNew, _ -> assert (rg_id = None); let arg, args = Collections.List.pop args in mk_apps arg args - | A.BoxDeref, None -> + | BoxDeref, None -> (* [Box::deref] forward is the identity *) let arg, args = Collections.List.pop args in mk_apps arg args - | A.BoxDeref, Some _ -> + | BoxDeref, Some _ -> (* [Box::deref] backward is [()] (doesn't give back anything) *) assert (args = []); mk_unit_rvalue - | A.BoxDerefMut, None -> + | BoxDerefMut, None -> (* [Box::deref_mut] forward is the identity *) let arg, args = Collections.List.pop args in mk_apps arg args - | A.BoxDerefMut, Some _ -> + | BoxDerefMut, Some _ -> (* [Box::deref_mut] back is almost the identity: * let box_deref_mut (x_init : t) (x_back : t) : t = x_back * *) @@ -1555,15 +1555,15 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = | _ -> raise (Failure "Unreachable") in mk_apps arg args - | A.BoxFree, _ -> + | BoxFree, _ -> assert (args = []); mk_unit_rvalue - | ( ( A.Replace | VecNew | VecPush | VecInsert | VecLen - | VecIndex | VecIndexMut | ArraySubsliceShared - | ArraySubsliceMut | SliceIndexShared | SliceIndexMut - | SliceSubsliceShared | SliceSubsliceMut | ArrayIndexShared - | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut - | ArrayRepeat | SliceLen ), + | ( ( Replace | VecNew | VecPush | VecInsert | VecLen | VecIndex + | VecIndexMut | ArraySubsliceShared | ArraySubsliceMut + | SliceIndexShared | SliceIndexMut | SliceSubsliceShared + | SliceSubsliceMut | ArrayIndexShared | ArrayIndexMut + | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat + | SliceLen ), _ ) -> super#visit_texpression env e) | _ -> super#visit_texpression env e) @@ -2046,7 +2046,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) : let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in assert (Option.is_some decl.loop_id); - let fun_id = (A.Regular decl.def_id, decl.loop_id) in + let fun_id = (E.Regular decl.def_id, decl.loop_id) in let set_used vid = used := List.map (fun (vid', b) -> (vid', b || vid = vid')) !used @@ -2130,7 +2130,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) : (* We then apply the filtering to all the function definitions at once *) let filter_in_one (decl : fun_decl) : fun_decl = (* Filter the function signature *) - let fun_id = (A.Regular decl.def_id, decl.loop_id) in + let fun_id = (E.Regular decl.def_id, decl.loop_id) in let decl = match FunLoopIdMap.find_opt fun_id !used_map with | None -> (* Nothing to filter *) decl diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 429198ad..54221cb1 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -343,7 +343,7 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : (* TODO: move *) let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id) (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig = - let id = (A.Regular def_id, back_id) in + let id = (E.Regular def_id, back_id) in (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg (* Some generic translation functions (we need to translate different "flavours" @@ -390,6 +390,7 @@ and translate_trait_instance_id (translate_ty : 'r T.ty -> ty) let inst_id = translate_trait_instance_id inst_id in ItemClause (inst_id, decl_id, item_name, clause_id) | TraitRef tr -> TraitRef (translate_trait_ref translate_ty tr) + | FnPointer _ -> raise (Failure "TODO") | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s)) let rec translate_sty (ty : T.sty) : ty = @@ -427,6 +428,7 @@ let rec translate_sty (ty : T.sty) : ty = let trait_ref = translate_strait_ref trait_ref in let generics = translate_sgeneric_args generics in TraitType (trait_ref, generics, type_name) + | Arrow _ -> raise (Failure "TODO") and translate_sgeneric_args (generics : T.sgeneric_args) : generic_args = translate_generic_args translate_sty generics @@ -569,6 +571,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty = let trait_ref = translate_fwd_trait_ref type_infos trait_ref in let generics = translate_fwd_generic_args type_infos generics in TraitType (trait_ref, generics, type_name) + | Arrow _ -> raise (Failure "TODO") and translate_fwd_generic_args (type_infos : TA.type_infos) (generics : 'r T.generic_args) : generic_args = @@ -658,6 +661,7 @@ let rec translate_back_ty (type_infos : TA.type_infos) let trait_ref = translate_fwd_trait_ref type_infos trait_ref in let generics = translate_fwd_generic_args type_infos generics in Some (TraitType (trait_ref, generics, type_name)) + | Arrow _ -> raise (Failure "TODO") (** Simply calls [translate_back_ty] *) let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) @@ -694,7 +698,7 @@ let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit = let translate_fun_id_or_trait_method_ref (ctx : bs_ctx) (id : A.fun_id_or_trait_method_ref) : fun_id_or_trait_method_ref = match id with - | A.FunId fun_id -> FunId fun_id + | FunId fun_id -> FunId fun_id | TraitMethod (trait_ref, method_name, fun_decl_id) -> let type_infos = ctx.type_context.type_infos in let trait_ref = translate_fwd_trait_ref type_infos trait_ref in @@ -795,7 +799,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option) (gid : T.RegionGroupId.id option) : fun_effect_info = match fun_id with - | A.TraitMethod (_, _, fid) | A.FunId (A.Regular fid) -> + | TraitMethod (_, _, fid) | FunId (Regular fid) -> let info = A.FunDeclId.Map.find fid fun_infos in let stateful_group = info.stateful in let stateful = @@ -808,7 +812,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t) can_diverge = info.can_diverge; is_rec = info.is_rec || Option.is_some lid; } - | A.FunId (A.Assumed aid) -> + | FunId (Assumed aid) -> assert (lid = None); { can_fail = Assumed.assumed_can_fail aid; @@ -841,7 +845,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id) in (* Is the function stateful, and can it fail? *) let lid = None in - let effect_info = get_fun_effect_info fun_infos (A.FunId fun_id) lid bid in + let effect_info = get_fun_effect_info fun_infos (FunId fun_id) lid bid in (* We need an evaluation context to normalize the types (to normalize the associated types, etc. - for instance it may happen that the types refer to the types associated to a trait ref, but where the trait ref @@ -1706,18 +1710,20 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : in (ctx, Unop (Neg int_ty), effect_info, args, None) | _ -> raise (Failure "Unreachable")) - | S.Unop (E.Cast (src_ty, tgt_ty)) -> - (* Note that cast can fail *) - let effect_info = - { - can_fail = true; - stateful_group = false; - stateful = false; - can_diverge = false; - is_rec = false; - } - in - (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None) + | S.Unop (E.Cast cast_kind) -> ( + match cast_kind with + | CastInteger (src_ty, tgt_ty) -> + (* Note that cast can fail *) + let effect_info = + { + can_fail = true; + stateful_group = false; + stateful = false; + can_diverge = false; + is_rec = false; + } + in + (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)) | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> @@ -1925,7 +1931,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) (* Sanity check: there is the proper number of inputs and outputs, and they have the proper type *) (if (* TODO: normalize the types *) !Config.type_check_pure_code then match fun_id with - | A.FunId fun_id -> + | FunId fun_id -> let inst_sg = get_instantiated_fun_sig fun_id (Some rg_id) generics ctx in @@ -2088,9 +2094,9 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) (* Actually the same case as [SynthInput] *) translate_end_abstraction_synth_input ectx abs e ctx rg_id | V.LoopCall -> - let fun_id = A.Regular ctx.fun_decl.A.def_id in + let fun_id = E.Regular ctx.fun_decl.A.def_id in let effect_info = - get_fun_effect_info ctx.fun_context.fun_infos (A.FunId fun_id) + get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id) (Some vloop_id) (Some rg_id) in let loop_info = LoopId.Map.find loop_id ctx.loops in @@ -2553,9 +2559,9 @@ and translate_forward_end (ectx : C.eval_ctx) let org_args = args in (* Lookup the effect info for the loop function *) - let fid = A.Regular ctx.fun_decl.A.def_id in + let fid = E.Regular ctx.fun_decl.A.def_id in let effect_info = - get_fun_effect_info ctx.fun_context.fun_infos (A.FunId fid) None ctx.bid + get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid in (* Introduce a fresh output value for the forward function *) diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index aeb6899f..9084f2b3 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -85,7 +85,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> raise (Failure "Ill-formed borrow expansion")) - | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ -> + | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ | T.Arrow _ -> raise (Failure "Ill-formed symbolic expansion") in Some (Expansion (place, sv, expansion)) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index e69abee1..8e01c869 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -61,7 +61,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Initialize the context *) let forward_sig = - RegularFunIdNotLoopMap.find (A.Regular def_id, None) fun_sigs + RegularFunIdNotLoopMap.find (E.Regular def_id, None) fun_sigs in let sv_to_var = V.SymbolicValueId.Map.empty in let var_counter = Pure.VarId.generator_zero in @@ -200,7 +200,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Initialize the context - note that the ret_ty is not really * useful as we don't translate a body *) let backward_sg = - RegularFunIdNotLoopMap.find (A.Regular def_id, Some back_id) fun_sigs + RegularFunIdNotLoopMap.find (Regular def_id, Some back_id) fun_sigs in let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in @@ -211,7 +211,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) variables required by the backward function. *) let backward_sg = - RegularFunIdNotLoopMap.find (A.Regular def_id, Some back_id) fun_sigs + RegularFunIdNotLoopMap.find (Regular def_id, Some back_id) fun_sigs in (* We need to ignore the forward inputs, and the state input (if there is) *) let backward_inputs = @@ -298,7 +298,7 @@ let translate_crate_to_pure (crate : A.crate) : let assumed_sigs = List.map (fun (id, sg, _, _) -> - (A.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg)) + (E.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg)) Assumed.assumed_infos in let local_sigs = @@ -312,7 +312,7 @@ let translate_crate_to_pure (crate : A.crate) : (fun (v : A.var) -> v.name) (LlbcAstUtils.fun_body_get_input_vars body) in - (A.Regular fdef.def_id, input_names, fdef.signature)) + (E.Regular fdef.def_id, input_names, fdef.signature)) (A.FunDeclId.Map.values crate.functions) in let sigs = List.append assumed_sigs local_sigs in diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index 95c7206a..4a187893 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -232,6 +232,14 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref) in (* Return *) ty_info + | Arrow (inputs, output) -> + (* Just dive into the arrow *) + let ty_info = + List.fold_left + (fun ty_info ty -> analyze expl_info ty_info ty) + ty_info inputs + in + analyze expl_info ty_info output in (* Explore *) analyze expl_info_init ty_info ty -- cgit v1.3.1 From c27c3052ec3f9a093b06a41f56b3a361cb65e950 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Sun, 22 Oct 2023 16:34:46 -0700 Subject: Add more support for numeric operations, xor, rotate --- backends/fstar/Primitives.fst | 23 ++++++++++++++++++++++- compiler/Extract.ml | 11 +++++++---- compiler/FunsAnalysis.ml | 24 +++++++++++++++++++++--- 3 files changed, 50 insertions(+), 8 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index e9391834..7d0845ed 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -100,6 +100,11 @@ type scalar_ty = | U64 | U128 +let is_unsigned = function +| Isize | I8 | I16 | I32 | I64 | I128 -> false +| Usize | U8 | U16 | U32 | U64 | U128 -> true + + let scalar_min (ty : scalar_ty) : int = match ty with | Isize -> isize_min @@ -162,6 +167,15 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x * y) +let scalar_lxor (#ty : scalar_ty { is_unsigned ty && ty <> Usize }) + (x : scalar ty) (y : scalar ty) : scalar ty = + match ty with + | U8 -> FStar.UInt.logxor #8 x y + | U16 -> FStar.UInt.logxor #16 x y + | U32 -> FStar.UInt.logxor #32 x y + | U64 -> FStar.UInt.logxor #64 x y + | U128 -> FStar.UInt.logxor #128 x y + (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = @@ -258,7 +272,7 @@ let u32_add = scalar_add #U32 let u64_add = scalar_add #U64 let u128_add = scalar_add #U128 -/// Substraction +/// Subtraction let isize_sub = scalar_sub #Isize let i8_sub = scalar_sub #I8 let i16_sub = scalar_sub #I16 @@ -286,6 +300,13 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +/// Logical operators, defined for unsigned types only, so far +let u8_xor = scalar_lxor #U8 +let u16_xor = scalar_lxor #U16 +let u32_xor = scalar_lxor #U32 +let u64_xor = scalar_lxor #U64 +let u128_xor = scalar_lxor #U128 + (*** Range *) type range (a : Type0) = { start : a; diff --git a/compiler/Extract.ml b/compiler/Extract.ml index ac81d6f3..b842aea1 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -3,7 +3,6 @@ the formatter everywhere... *) -open Utils open Pure open PureUtils open TranslateCore @@ -61,6 +60,11 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string = | Le -> "le" | Ge -> "ge" | Gt -> "gt" + | BitXor -> "xor" + | BitAnd -> "and" + | BitOr -> "or" + | Shl -> "lsl" + | Shr -> "asr" (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *) | _ -> raise (Failure "Unreachable") in (* Remark: the Lean case is actually not used *) @@ -498,14 +502,13 @@ let extract_binop (extract_expr : bool -> texpression -> unit) F.pp_print_string fmt binop; F.pp_print_space fmt (); extract_expr false arg1 - | _, (Lt | Le | Ge | Gt | Div | Rem | Add | Sub | Mul) -> + | _ -> let binop = named_binop_name binop int_ty in F.pp_print_string fmt binop; F.pp_print_space fmt (); extract_expr true arg0; F.pp_print_space fmt (); - extract_expr true arg1 - | _, (BitXor | BitAnd | BitOr | Shl | Shr) -> raise Unimplemented); + extract_expr true arg1); if inside then F.pp_print_string fmt ")" let type_decl_kind_to_qualif (kind : decl_kind) diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f4406653..f8aa06dc 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -58,6 +58,24 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let can_diverge = ref false in let is_rec = ref false in + (* We have some specialized knowledge of some library functions; we don't + have any more custom treatment than this, and these functions can be modeled + suitably in Primitives.fst, rather than special-casing for them all the + way. *) + let module M = struct type opaque_info = { fallible: bool; stateful: bool } end in + let open M in + let opaque_info (f: fun_decl) = + match f.name with + | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "wrapping_add" ] + | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "rotate_left" ] -> + { fallible = false; stateful = false } + | _ -> + (* Opaque function: we consider they fail by default *) + { fallible = true; stateful = true } + in + + (* JP: Why not use a reduce visitor here with a tuple of the values to be + computed? *) let visit_fun (f : fun_decl) : unit = let obj = object (self) @@ -108,9 +126,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) assert ((not f.is_global_decl_body) || not !stateful); match f.body with | None -> - (* Opaque function: we consider they fail by default *) - obj#may_fail true; - stateful := (not f.is_global_decl_body) && use_state + let info = opaque_info f in + obj#may_fail info.fallible; + stateful := (not f.is_global_decl_body) && use_state && info.stateful | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; -- cgit v1.3.1 From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 23 Oct 2023 13:47:39 +0200 Subject: Remove some assumed types and add more support for builtin definitions --- compiler/Assumed.ml | 254 +++++--------------- compiler/Extract.ml | 145 ++++++------ compiler/ExtractAssumed.ml | 61 ----- compiler/ExtractBase.ml | 73 +----- compiler/ExtractBuiltin.ml | 468 +++++++++++++++++++++++++++++++++++++ compiler/FunsAnalysis.ml | 2 +- compiler/InterpreterExpansion.ml | 15 +- compiler/InterpreterExpressions.ml | 100 +++----- compiler/InterpreterPaths.ml | 31 +-- compiler/InterpreterPaths.mli | 4 - compiler/InterpreterStatements.ml | 100 +------- compiler/Invariants.ml | 15 +- compiler/LlbcAstUtils.ml | 8 +- compiler/PrePasses.ml | 2 +- compiler/Print.ml | 11 - compiler/PrintPure.ml | 57 +---- compiler/Pure.ml | 12 +- compiler/PureMicroPasses.ml | 42 ++-- compiler/PureTypeCheck.ml | 13 +- compiler/Substitute.ml | 14 +- compiler/SymbolicToPure.ml | 31 +-- compiler/Translate.ml | 107 +++++---- compiler/TypesAnalysis.ml | 4 +- compiler/dune | 2 +- 24 files changed, 763 insertions(+), 808 deletions(-) delete mode 100644 compiler/ExtractAssumed.ml create mode 100644 compiler/ExtractBuiltin.ml (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index b1ec0660..94fb7a72 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -80,8 +80,6 @@ module Sig = struct let mk_slice_ty (ty : T.sty) : T.sty = Adt (Assumed Slice, mk_generic_args [] [ ty ] []) - let range_ty : T.sty = Adt (Assumed Range, mk_generic_args [] [ usize_ty ] []) - let mk_sig generics regions_hierarchy inputs output : A.fun_sig = let preds : T.predicates = { regions_outlive = []; types_outlive = []; trait_type_constraints = [] } @@ -95,19 +93,6 @@ module Sig = struct output; } - (** [fn(&'a mut T, T) -> T] *) - let mem_replace_sig : A.fun_sig = - (* The signature fields *) - let regions = [ region_param_0 ] (* <'a> *) in - let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in - let types = [ type_param_0 ] (* *) in - let generics = mk_generic_params regions types [] in - let inputs = - [ mk_ref_ty rvar_0 tvar_0 true (* &'a mut T *); tvar_0 (* T *) ] - in - let output = tvar_0 (* T *) in - mk_sig generics regions_hierarchy inputs output - (** [fn(T) -> Box] *) let box_new_sig : A.fun_sig = let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in @@ -124,101 +109,6 @@ module Sig = struct let output = mk_unit_ty (* () *) in mk_sig generics regions_hierarchy inputs output - (** Helper for [Box::deref_shared] and [Box::deref_mut]. - Returns: - [fn<'a, T>(&'a (mut) Box) -> &'a (mut) T] - *) - let box_deref_gen_sig (is_mut : bool) : A.fun_sig = - let generics = - mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) - in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let inputs = - [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box *) ] - in - let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in - mk_sig generics regions_hierarchy inputs output - - (** [fn<'a, T>(&'a Box) -> &'a T] *) - let box_deref_shared_sig = box_deref_gen_sig false - - (** [fn<'a, T>(&'a mut Box) -> &'a mut T] *) - let box_deref_mut_sig = box_deref_gen_sig true - - (** [fn() -> Vec] *) - let vec_new_sig : A.fun_sig = - let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in - let regions_hierarchy = [] in - let inputs = [] in - let output = mk_vec_ty tvar_0 (* Vec *) in - mk_sig generics regions_hierarchy inputs output - - (** [fn(&'a mut Vec, T)] *) - let vec_push_sig : A.fun_sig = - let generics = - mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) - in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let inputs = - [ - mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec *); - tvar_0 (* T *); - ] - in - let output = mk_unit_ty (* () *) in - mk_sig generics regions_hierarchy inputs output - - (** [fn(&'a mut Vec, usize, T)] *) - let vec_insert_sig : A.fun_sig = - let generics = - mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) - in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let inputs = - [ - mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec *); - mk_usize_ty (* usize *); - tvar_0 (* T *); - ] - in - let output = mk_unit_ty (* () *) in - mk_sig generics regions_hierarchy inputs output - - (** [fn(&'a Vec) -> usize] *) - let vec_len_sig : A.fun_sig = - let generics = - mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) - in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let inputs = - [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) false (* &'a Vec *) ] - in - let output = mk_usize_ty (* usize *) in - mk_sig generics regions_hierarchy inputs output - - (** Helper: - [fn(&'a (mut) Vec, usize) -> &'a (mut) T] - *) - let vec_index_gen_sig (is_mut : bool) : A.fun_sig = - let generics = - mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) - in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let inputs = - [ - mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec *); - mk_usize_ty (* usize *); - ] - in - let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in - mk_sig generics regions_hierarchy inputs output - - (** [fn(&'a Vec, usize) -> &'a T] *) - let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false - - (** [fn(&'a mut Vec, usize) -> &'a mut T] *) - let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true - (** Array/slice functions *) (** Small helper. @@ -281,23 +171,6 @@ module Sig = struct let cgs = [ cg_param_0 ] in mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut - let mk_array_slice_subslice_sig (is_array : bool) (is_mut : bool) : A.fun_sig - = - (* Array *) - let input_ty id = - if is_array then mk_array_ty (T.TypeVar id) cgvar_0 - else mk_slice_ty (T.TypeVar id) - in - (* Range *) - let index_ty = range_ty in - (* Slice *) - let output_ty id = mk_slice_ty (T.TypeVar id) in - let cgs = if is_array then [ cg_param_0 ] else [] in - mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut - - let array_subslice_sig (is_mut : bool) = - mk_array_slice_subslice_sig true is_mut - let array_repeat_sig = let generics = (* *) @@ -311,9 +184,6 @@ module Sig = struct in mk_sig generics regions_hierarchy inputs output - let slice_subslice_sig (is_mut : bool) = - mk_array_slice_subslice_sig false is_mut - (** Helper: [fn(&'a [T]) -> usize] *) @@ -329,7 +199,25 @@ module Sig = struct mk_sig generics regions_hierarchy inputs output end -type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name +type raw_assumed_fun_info = + A.assumed_fun_id * A.fun_sig * bool * name * bool list option + +type assumed_fun_info = { + fun_id : A.assumed_fun_id; + fun_sig : A.fun_sig; + can_fail : bool; + name : name; + keep_types : bool list option; + (** We may want to filter some type arguments. + + For instance, all the `Vec` functions (and the `Vec` type itself) take + an `Allocator` type as argument, that we ignore. + *) +} + +let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info = + let fun_id, fun_sig, can_fail, name, keep_types = raw in + { fun_id; fun_sig; can_fail; name; keep_types } (** The list of assumed functions and all their information: - their signature @@ -342,96 +230,72 @@ type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name a [usize], we have to make sure that vectors are bounded by the max usize. As a consequence, [Vec::push] is monadic. *) -let assumed_infos : assumed_info list = - let deref_pre = [ "core"; "ops"; "deref" ] in - let vec_pre = [ "alloc"; "vec"; "Vec" ] in - let index_pre = [ "core"; "ops"; "index" ] in +let raw_assumed_fun_infos : raw_assumed_fun_info list = [ - (Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]); - (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]); + ( BoxNew, + Sig.box_new_sig, + false, + to_name [ "alloc"; "boxed"; "Box"; "new" ], + Some [ true; false ] ); + (* BoxFree shouldn't be used *) ( BoxFree, Sig.box_free_sig, false, - to_name [ "alloc"; "boxed"; "Box"; "free" ] ); - ( BoxDeref, - Sig.box_deref_shared_sig, - false, - to_name (deref_pre @ [ "Deref"; "deref" ]) ); - ( BoxDerefMut, - Sig.box_deref_mut_sig, - false, - to_name (deref_pre @ [ "DerefMut"; "deref_mut" ]) ); - (VecNew, Sig.vec_new_sig, false, to_name (vec_pre @ [ "new" ])); - (VecPush, Sig.vec_push_sig, true, to_name (vec_pre @ [ "push" ])); - (VecInsert, Sig.vec_insert_sig, true, to_name (vec_pre @ [ "insert" ])); - (VecLen, Sig.vec_len_sig, false, to_name (vec_pre @ [ "len" ])); - ( VecIndex, - Sig.vec_index_shared_sig, - true, - to_name (index_pre @ [ "Index"; "index" ]) ); - ( VecIndexMut, - Sig.vec_index_mut_sig, - true, - to_name (index_pre @ [ "IndexMut"; "index_mut" ]) ); + to_name [ "alloc"; "boxed"; "Box"; "free" ], + Some [ true; false ] ); (* Array Index *) ( ArrayIndexShared, Sig.array_index_sig false, true, - to_name [ "@ArrayIndexShared" ] ); - (ArrayIndexMut, Sig.array_index_sig true, true, to_name [ "@ArrayIndexMut" ]); + to_name [ "@ArrayIndexShared" ], + None ); + ( ArrayIndexMut, + Sig.array_index_sig true, + true, + to_name [ "@ArrayIndexMut" ], + None ); (* Array to slice*) ( ArrayToSliceShared, Sig.array_to_slice_sig false, true, - to_name [ "@ArrayToSliceShared" ] ); + to_name [ "@ArrayToSliceShared" ], + None ); ( ArrayToSliceMut, Sig.array_to_slice_sig true, true, - to_name [ "@ArrayToSliceMut" ] ); - (* Array Subslice *) - ( ArraySubsliceShared, - Sig.array_subslice_sig false, - true, - to_name [ "@ArraySubsliceShared" ] ); - ( ArraySubsliceMut, - Sig.array_subslice_sig true, - true, - to_name [ "@ArraySubsliceMut" ] ); + to_name [ "@ArrayToSliceMut" ], + None ); (* Array Repeat *) - (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ]); + (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ], None); (* Slice Index *) ( SliceIndexShared, Sig.slice_index_sig false, true, - to_name [ "@SliceIndexShared" ] ); - (SliceIndexMut, Sig.slice_index_sig true, true, to_name [ "@SliceIndexMut" ]); - (* Slice Subslice *) - ( SliceSubsliceShared, - Sig.slice_subslice_sig false, + to_name [ "@SliceIndexShared" ], + None ); + ( SliceIndexMut, + Sig.slice_index_sig true, true, - to_name [ "@SliceSubsliceShared" ] ); - ( SliceSubsliceMut, - Sig.slice_subslice_sig true, - true, - to_name [ "@SliceSubsliceMut" ] ); - (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]); + to_name [ "@SliceIndexMut" ], + None ); + (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ], None); ] -let get_assumed_info (id : A.assumed_fun_id) : assumed_info = - match List.find_opt (fun (id', _, _, _) -> id = id') assumed_infos with +let assumed_fun_infos : assumed_fun_info list = + List.map mk_assumed_fun_info raw_assumed_fun_infos + +let get_assumed_fun_info (id : A.assumed_fun_id) : assumed_fun_info = + match List.find_opt (fun x -> id = x.fun_id) assumed_fun_infos with | Some info -> info | None -> raise - (Failure ("get_assumed_info: not found: " ^ A.show_assumed_fun_id id)) + (Failure ("get_assumed_fun_info: not found: " ^ A.show_assumed_fun_id id)) -let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig = - let _, sg, _, _ = get_assumed_info id in - sg +let get_assumed_fun_sig (id : A.assumed_fun_id) : A.fun_sig = + (get_assumed_fun_info id).fun_sig -let get_assumed_name (id : A.assumed_fun_id) : fun_name = - let _, _, _, name = get_assumed_info id in - name +let get_assumed_fun_name (id : A.assumed_fun_id) : fun_name = + (get_assumed_fun_info id).name -let assumed_can_fail (id : A.assumed_fun_id) : bool = - let _, _, b, _ = get_assumed_info id in - b +let assumed_fun_can_fail (id : A.assumed_fun_id) : bool = + (get_assumed_fun_info id).can_fail diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 688f6ce3..30c4c27d 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -225,12 +225,9 @@ let assumed_adts () : (assumed_ty * string) list = (Result, "Result"); (Error, "Error"); (Fuel, "Nat"); - (Option, "Option"); - (Vec, "Vec"); (Array, "Array"); (Slice, "Slice"); (Str, "Str"); - (Range, "Range"); ] | Coq | FStar -> [ @@ -238,12 +235,9 @@ let assumed_adts () : (assumed_ty * string) list = (Result, "result"); (Error, "error"); (Fuel, "nat"); - (Option, "option"); - (Vec, "vec"); (Array, "array"); (Slice, "slice"); (Str, "str"); - (Range, "range"); ] | HOL4 -> [ @@ -251,20 +245,17 @@ let assumed_adts () : (assumed_ty * string) list = (Result, "result"); (Error, "error"); (Fuel, "num"); - (Option, "option"); - (Vec, "vec"); (Array, "array"); (Slice, "slice"); (Str, "str"); - (Range, "range"); ] let assumed_struct_constructors () : (assumed_ty * string) list = match !backend with - | Lean -> [ (Range, "Range.mk"); (Array, "Array.make") ] - | Coq -> [ (Range, "mk_range"); (Array, "mk_array") ] - | FStar -> [ (Range, "Mkrange"); (Array, "mk_array") ] - | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ] + | Lean -> [ (Array, "Array.make") ] + | Coq -> [ (Array, "mk_array") ] + | FStar -> [ (Array, "mk_array") ] + | HOL4 -> [ (Array, "mk_array") ] let assumed_variants () : (assumed_ty * VariantId.id * string) list = match !backend with @@ -276,8 +267,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = (Error, error_out_of_fuel_id, "OutOfFuel"); (* No Fuel::Zero on purpose *) (* No Fuel::Succ on purpose *) - (Option, option_some_id, "Some"); - (Option, option_none_id, "None"); ] | Coq -> [ @@ -287,8 +276,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = (Error, error_out_of_fuel_id, "OutOfFuel"); (Fuel, fuel_zero_id, "O"); (Fuel, fuel_succ_id, "S"); - (Option, option_some_id, "Some"); - (Option, option_none_id, "None"); ] | Lean -> [ @@ -297,8 +284,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = (Error, error_failure_id, "panic"); (* No Fuel::Zero on purpose *) (* No Fuel::Succ on purpose *) - (Option, option_some_id, "some"); - (Option, option_none_id, "none"); ] | HOL4 -> [ @@ -307,8 +292,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = (Error, error_failure_id, "Failure"); (* No Fuel::Zero on purpose *) (* No Fuel::Succ on purpose *) - (Option, option_some_id, "SOME"); - (Option, option_none_id, "NONE"); ] let assumed_llbc_functions () : @@ -317,66 +300,30 @@ let assumed_llbc_functions () : match !backend with | FStar | Coq | HOL4 -> [ - (Replace, None, "mem_replace_fwd"); - (Replace, rg0, "mem_replace_back"); - (VecNew, None, "vec_new"); - (VecPush, None, "vec_push_fwd") (* Shouldn't be used *); - (VecPush, rg0, "vec_push_back"); - (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *); - (VecInsert, rg0, "vec_insert_back"); - (VecLen, None, "vec_len"); - (VecIndex, None, "vec_index_fwd"); - (VecIndex, rg0, "vec_index_back") (* shouldn't be used *); - (VecIndexMut, None, "vec_index_mut_fwd"); - (VecIndexMut, rg0, "vec_index_mut_back"); (ArrayIndexShared, None, "array_index_shared"); (ArrayIndexMut, None, "array_index_mut_fwd"); (ArrayIndexMut, rg0, "array_index_mut_back"); (ArrayToSliceShared, None, "array_to_slice_shared"); (ArrayToSliceMut, None, "array_to_slice_mut_fwd"); (ArrayToSliceMut, rg0, "array_to_slice_mut_back"); - (ArraySubsliceShared, None, "array_subslice_shared"); - (ArraySubsliceMut, None, "array_subslice_mut_fwd"); - (ArraySubsliceMut, rg0, "array_subslice_mut_back"); (ArrayRepeat, None, "array_repeat"); (SliceIndexShared, None, "slice_index_shared"); (SliceIndexMut, None, "slice_index_mut_fwd"); (SliceIndexMut, rg0, "slice_index_mut_back"); - (SliceSubsliceShared, None, "slice_subslice_shared"); - (SliceSubsliceMut, None, "slice_subslice_mut_fwd"); - (SliceSubsliceMut, rg0, "slice_subslice_mut_back"); (SliceLen, None, "slice_len"); ] | Lean -> [ - (Replace, None, "mem.replace"); - (Replace, rg0, "mem.replace_back"); - (VecNew, None, "Vec.new"); - (VecPush, None, "Vec.push_fwd") (* Shouldn't be used *); - (VecPush, rg0, "Vec.push"); - (VecInsert, None, "Vec.insert_fwd") (* Shouldn't be used *); - (VecInsert, rg0, "Vec.insert"); - (VecLen, None, "Vec.len"); - (VecIndex, None, "Vec.index_shared"); - (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *); - (VecIndexMut, None, "Vec.index_mut"); - (VecIndexMut, rg0, "Vec.index_mut_back"); (ArrayIndexShared, None, "Array.index_shared"); (ArrayIndexMut, None, "Array.index_mut"); (ArrayIndexMut, rg0, "Array.index_mut_back"); (ArrayToSliceShared, None, "Array.to_slice_shared"); (ArrayToSliceMut, None, "Array.to_slice_mut"); (ArrayToSliceMut, rg0, "Array.to_slice_mut_back"); - (ArraySubsliceShared, None, "Array.subslice_shared"); - (ArraySubsliceMut, None, "Array.subslice_mut"); - (ArraySubsliceMut, rg0, "Array.subslice_mut_back"); (ArrayRepeat, None, "Array.repeat"); (SliceIndexShared, None, "Slice.index_shared"); (SliceIndexMut, None, "Slice.index_mut"); (SliceIndexMut, rg0, "Slice.index_mut_back"); - (SliceSubsliceShared, None, "Slice.subslice_shared"); - (SliceSubsliceMut, None, "Slice.subslice_mut"); - (SliceSubsliceMut, rg0, "Slice.subslice_mut_back"); (SliceLen, None, "Slice.len"); ] @@ -850,12 +797,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | Assumed Result -> "r" | Assumed Error -> ConstStrings.error_basename | Assumed Fuel -> ConstStrings.fuel_basename - | Assumed Option -> "opt" - | Assumed Vec -> "v" | Assumed Array -> "a" | Assumed Slice -> "s" | Assumed Str -> "s" - | Assumed Range -> "r" | Assumed State -> ConstStrings.state_basename | AdtId adt_id -> let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in @@ -1397,8 +1341,18 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : extraction_ctx = + (* Lookup the builtin information, if there is *) + let open ExtractBuiltin in + let sname = name_to_simple_name def.name in + let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in (* Compute and register the type def name *) - let ctx = ctx_add_type_decl def ctx in + let def_name = + match info with + | None -> ctx.fmt.type_name def.name + | Some info -> info.rust_name + in + let is_opaque = def.kind = Opaque in + let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in (* Compute and register: * - the variant names, if this is an enumeration * - the field names, if this is a structure @@ -1406,18 +1360,73 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : let ctx = match def.kind with | Struct fields -> + (* Compute the names *) + let field_names, cons_name = + match info with + | None -> + let field_names = + FieldId.mapi + (fun fid (field : field) -> + (fid, ctx.fmt.field_name def.name fid field.field_name)) + fields + in + let cons_name = ctx.fmt.struct_constructor def.name in + (field_names, cons_name) + | Some { body_info = Some (Struct (cons_name, field_names)); _ } -> + let field_names = + FieldId.mapi + (fun fid (_, name) -> (fid, name)) + (List.combine fields field_names) + in + (field_names, cons_name) + | _ -> raise (Failure "Invalid builtin information") + in (* Add the fields *) let ctx = - fst - (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx) + List.fold_left + (fun ctx (fid, name) -> + ctx_add is_opaque (FieldId (AdtId def.def_id, fid)) name ctx) + ctx field_names in (* Add the constructor name *) - fst (ctx_add_struct def ctx) + ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx | Enum variants -> - fst - (ctx_add_variants def - (VariantId.mapi (fun id v -> (id, v)) variants) - ctx) + let variant_names = + match info with + | None -> + VariantId.mapi + (fun variant_id (variant : variant) -> + let name = + ctx.fmt.variant_name def.name variant.variant_name + in + (* Add the type name prefix for Lean *) + let name = + if !Config.backend = Lean then + let type_name = ctx.fmt.type_name def.name in + type_name ^ "." ^ name + else name + in + (variant_id, name)) + variants + | Some { body_info = Some (Enum variant_infos); _ } -> + (* We need to compute the map from variant to variant *) + let variant_map = + StringMap.of_list + (List.map + (fun (info : builtin_enum_variant_info) -> + (info.rust_variant_name, info.extract_variant_name)) + variant_infos) + in + VariantId.mapi + (fun variant_id (variant : variant) -> + (variant_id, StringMap.find variant.variant_name variant_map)) + variants + | _ -> raise (Failure "Invalid builtin information") + in + List.fold_left + (fun ctx (vid, vname) -> + ctx_add is_opaque (VariantId (AdtId def.def_id, vid)) vname ctx) + ctx variant_names | Opaque -> (* Nothing to do *) ctx diff --git a/compiler/ExtractAssumed.ml b/compiler/ExtractAssumed.ml deleted file mode 100644 index 7f094b24..00000000 --- a/compiler/ExtractAssumed.ml +++ /dev/null @@ -1,61 +0,0 @@ -(** This file declares external identifiers that we catch to map them to - definitions coming from the standard libraries in our backends. *) - -open Names - -type simple_name = string list [@@deriving show, ord] - -let name_to_simple_name (s : name) : simple_name = - (* We simply ignore the disambiguators *) - List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s - -(** Small helper which cuts a string at the occurrences of "::" *) -let string_to_simple_name (s : string) : simple_name = - (* No function to split by using string separator?? *) - let name = String.split_on_char ':' s in - List.filter (fun s -> s <> "") name - -module SimpleNameOrd = struct - type t = simple_name - - let compare = compare_simple_name - let to_string = show_simple_name - let pp_t = pp_simple_name - let show_t = show_simple_name -end - -module SimpleNameMap = Collections.MakeMap (SimpleNameOrd) - -let assumed_globals : (string * string) list = - [ - (* Min *) - ("core::num::usize::MIN", "core_usize_min"); - ("core::num::u8::MIN", "core_u8_min"); - ("core::num::u16::MIN", "core_u16_min"); - ("core::num::u32::MIN", "core_u32_min"); - ("core::num::u64::MIN", "core_u64_min"); - ("core::num::u128::MIN", "core_u128_min"); - ("core::num::isize::MIN", "core_isize_min"); - ("core::num::i8::MIN", "core_i8_min"); - ("core::num::i16::MIN", "core_i16_min"); - ("core::num::i32::MIN", "core_i32_min"); - ("core::num::i64::MIN", "core_i64_min"); - ("core::num::i128::MIN", "core_i128_min"); - (* Max *) - ("core::num::usize::MAX", "core_usize_max"); - ("core::num::u8::MAX", "core_u8_max"); - ("core::num::u16::MAX", "core_u16_max"); - ("core::num::u32::MAX", "core_u32_max"); - ("core::num::u64::MAX", "core_u64_max"); - ("core::num::u128::MAX", "core_u128_max"); - ("core::num::isize::MAX", "core_isize_max"); - ("core::num::i8::MAX", "core_i8_max"); - ("core::num::i16::MAX", "core_i16_max"); - ("core::num::i32::MAX", "core_i32_max"); - ("core::num::i64::MAX", "core_i64_max"); - ("core::num::i128::MAX", "core_i128_max"); - ] - -let assumed_globals_map : string SimpleNameMap.t = - SimpleNameMap.of_list - (List.map (fun (x, y) -> (string_to_simple_name x, y)) assumed_globals) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index a921515b..54f69735 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -5,7 +5,7 @@ open TranslateCore module C = Contexts module RegionVarId = T.RegionVarId module F = Format -open ExtractAssumed +open ExtractBuiltin (** The local logger *) let log = L.pure_to_extract_log @@ -803,15 +803,11 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = if variant_id = error_failure_id then "@error::Failure" else if variant_id = error_out_of_fuel_id then "@error::OutOfFuel" else raise (Failure "Unreachable") - | Assumed Option -> - if variant_id = option_some_id then "@option::Some" - else if variant_id = option_none_id then "@option::None" - else raise (Failure "Unreachable") | Assumed Fuel -> if variant_id = fuel_zero_id then "@fuel::0" else if variant_id = fuel_succ_id then "@fuel::Succ" else raise (Failure "Unreachable") - | Assumed (State | Vec | Array | Slice | Str | Range) -> + | Assumed (State | Array | Slice | Str) -> raise (Failure ("Unreachable: variant id (" @@ -830,9 +826,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let field_name = match id with | Tuple -> raise (Failure "Unreachable") - | Assumed - ( State | Result | Error | Fuel | Option | Vec | Array | Slice | Str - | Range ) -> + | Assumed (State | Result | Error | Fuel | Array | Slice | Str) -> (* We can't directly have access to the fields of those types *) raise (Failure "Unreachable") | AdtId id -> ( @@ -1186,65 +1180,6 @@ let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) : let ctx, tcs = ctx_add_local_trait_clauses trait_clauses ctx in (ctx, tys, cgs, tcs) -let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) : - extraction_ctx * string = - assert (match def.kind with Struct _ -> true | _ -> false); - let is_opaque = false in - let cons_name = ctx.fmt.struct_constructor def.name in - let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx in - (ctx, cons_name) - -let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx - = - let is_opaque = def.kind = Opaque in - let def_name = ctx.fmt.type_name def.name in - let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in - ctx - -let ctx_add_field (def : type_decl) (field_id : FieldId.id) (field : field) - (ctx : extraction_ctx) : extraction_ctx * string = - let is_opaque = false in - let name = ctx.fmt.field_name def.name field_id field.field_name in - let ctx = ctx_add is_opaque (FieldId (AdtId def.def_id, field_id)) name ctx in - (ctx, name) - -let ctx_add_fields (def : type_decl) (fields : (FieldId.id * field) list) - (ctx : extraction_ctx) : extraction_ctx * string list = - List.fold_left_map - (fun ctx (vid, v) -> ctx_add_field def vid v ctx) - ctx fields - -let ctx_add_variant (def : type_decl) (variant_id : VariantId.id) - (variant : variant) (ctx : extraction_ctx) : extraction_ctx * string = - let is_opaque = false in - let name = ctx.fmt.variant_name def.name variant.variant_name in - (* Add the type name prefix for Lean *) - let name = - if !Config.backend = Lean then - let type_name = ctx.fmt.type_name def.name in - type_name ^ "." ^ name - else name - in - let ctx = - ctx_add is_opaque (VariantId (AdtId def.def_id, variant_id)) name ctx - in - (ctx, name) - -let ctx_add_variants (def : type_decl) - (variants : (VariantId.id * variant) list) (ctx : extraction_ctx) : - extraction_ctx * string list = - List.fold_left_map - (fun ctx (vid, v) -> ctx_add_variant def vid v ctx) - ctx variants - -let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) : - extraction_ctx * string = - assert (match def.kind with Struct _ -> true | _ -> false); - let is_opaque = false in - let name = ctx.fmt.struct_constructor def.name in - let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) name ctx in - (ctx, name) - let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = let is_opaque = false in @@ -1277,7 +1212,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : to a custom definition in our standard library (for instance, happens with "core::num::usize::MAX") *) let sname = name_to_simple_name def.name in - match SimpleNameMap.find_opt sname assumed_globals_map with + match SimpleNameMap.find_opt sname builtin_globals_map with | Some name -> (* Yes: register the custom binding *) ctx_add is_opaque decl name ctx diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml new file mode 100644 index 00000000..cf5cc70d --- /dev/null +++ b/compiler/ExtractBuiltin.ml @@ -0,0 +1,468 @@ +(** This file declares external identifiers that we catch to map them to + definitions coming from the standard libraries in our backends. *) + +open Names +open Config + +type simple_name = string list [@@deriving show, ord] + +let name_to_simple_name (s : name) : simple_name = + (* We simply ignore the disambiguators *) + List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s + +(** Small helper which cuts a string at the occurrences of "::" *) +let string_to_simple_name (s : string) : simple_name = + (* No function to split by using string separator?? *) + let name = String.split_on_char ':' s in + List.filter (fun s -> s <> "") name + +module SimpleNameOrd = struct + type t = simple_name + + let compare = compare_simple_name + let to_string = show_simple_name + let pp_t = pp_simple_name + let show_t = show_simple_name +end + +module SimpleNameMap = Collections.MakeMap (SimpleNameOrd) + +(** Small utility to memoize some computations *) +let mk_memoized (f : unit -> 'a) : unit -> 'a = + let r = ref None in + let g () = + match !r with + | Some x -> x + | None -> + let x = f () in + r := Some x; + x + in + g + +let builtin_globals : (string * string) list = + [ + (* Min *) + ("core::num::usize::MIN", "core_usize_min"); + ("core::num::u8::MIN", "core_u8_min"); + ("core::num::u16::MIN", "core_u16_min"); + ("core::num::u32::MIN", "core_u32_min"); + ("core::num::u64::MIN", "core_u64_min"); + ("core::num::u128::MIN", "core_u128_min"); + ("core::num::isize::MIN", "core_isize_min"); + ("core::num::i8::MIN", "core_i8_min"); + ("core::num::i16::MIN", "core_i16_min"); + ("core::num::i32::MIN", "core_i32_min"); + ("core::num::i64::MIN", "core_i64_min"); + ("core::num::i128::MIN", "core_i128_min"); + (* Max *) + ("core::num::usize::MAX", "core_usize_max"); + ("core::num::u8::MAX", "core_u8_max"); + ("core::num::u16::MAX", "core_u16_max"); + ("core::num::u32::MAX", "core_u32_max"); + ("core::num::u64::MAX", "core_u64_max"); + ("core::num::u128::MAX", "core_u128_max"); + ("core::num::isize::MAX", "core_isize_max"); + ("core::num::i8::MAX", "core_i8_max"); + ("core::num::i16::MAX", "core_i16_max"); + ("core::num::i32::MAX", "core_i32_max"); + ("core::num::i64::MAX", "core_i64_max"); + ("core::num::i128::MAX", "core_i128_max"); + ] + +let builtin_globals_map : string SimpleNameMap.t = + SimpleNameMap.of_list + (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals) + +type builtin_variant_info = { fields : (string * string) list } + +type builtin_enum_variant_info = { + rust_variant_name : string; + extract_variant_name : string; + fields : string list option; +} + +type builtin_type_body_info = + | Struct of string * string list + (* The constructor name and the map for the field names *) + | Enum of builtin_enum_variant_info list +(* For every variant, a map for the field names *) + +type builtin_type_info = { + rust_name : string; + extract_name : string; + keep_params : bool list option; + (** We might want to filter some of the type parameters. + + For instance, `Vec` type takes a type parameter for the allocator, + which we want to ignore. + *) + body_info : builtin_type_body_info option; +} + +(** The assumed types. + + The optional list of booleans is filtering information for the type + parameters. For instance, in the case of the `Vec` functions, there is + a type parameter for the allocator to use, which we want to filter. + *) +let builtin_types () : builtin_type_info list = + [ + (* Alloc *) + { + rust_name = "alloc::alloc::Global"; + extract_name = + (match !backend with + | Lean -> "AllocGlobal" + | Coq | FStar | HOL4 -> "alloc_global"); + keep_params = None; + body_info = None; + }; + (* Vec *) + { + rust_name = "alloc::vec::Vec"; + extract_name = + (match !backend with Lean -> "Vec" | Coq | FStar | HOL4 -> "vec"); + keep_params = Some [ true; false ]; + body_info = None; + }; + (* Option *) + { + rust_name = "core::option::Option"; + extract_name = + (match !backend with + | Lean -> "Option" + | Coq | FStar | HOL4 -> "option"); + keep_params = None; + body_info = + Some + (Enum + [ + { + rust_variant_name = "None"; + extract_variant_name = + (match !backend with + | FStar | Coq -> "None" + | Lean -> "none" + | HOL4 -> "NONE"); + fields = None; + }; + { + rust_variant_name = "Some"; + extract_variant_name = + (match !backend with + | FStar | Coq -> "Some" + | Lean -> "some" + | HOL4 -> "SOME"); + fields = None; + }; + ]); + }; + (* Range *) + { + rust_name = "core::ops::range::Range"; + extract_name = + (match !backend with Lean -> "Range" | Coq | FStar | HOL4 -> "range"); + keep_params = None; + body_info = + Some + (Struct + ( (match !backend with + | Lean -> "Range.mk" + | Coq | HOL4 -> "mk_range" + | FStar -> "Mkrange"), + [ "start"; "end_" ] )); + }; + ] + +let mk_builtin_types_map () = + SimpleNameMap.of_list + (List.map + (fun info -> (string_to_simple_name info.rust_name, info)) + (builtin_types ())) + +let builtin_types_map = mk_memoized mk_builtin_types_map + +type builtin_fun_info = { + rg : Types.RegionGroupId.id option; + extract_name : string; +} + +(** The assumed functions. + + The optional list of booleans is filtering information for the type + parameters. For instance, in the case of the `Vec` functions, there is + a type parameter for the allocator to use, which we want to filter. + *) +let builtin_funs () : (string * bool list option * builtin_fun_info list) list = + let rg0 = Some Types.RegionGroupId.zero in + [ + ( "core::mem::replace", + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "mem_replace_fwd" + | Lean -> "mem.replace"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "mem_replace_back" + | Lean -> "mem.replace_back"); + }; + ] ); + ( "alloc::vec::Vec::new", + Some [ true; false ], + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_new" + | Lean -> "Vec.new"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_new_back" + | Lean -> "Vec.new_back"); + }; + ] ); + ( "alloc::vec::Vec::push", + Some [ true; false ], + [ + (* The forward function shouldn't be used *) + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_push_fwd" + | Lean -> "Vec.push_fwd"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_push_back" + | Lean -> "Vec.push"); + }; + ] ); + ( "alloc::vec::Vec::insert", + Some [ true; false ], + [ + (* The forward function shouldn't be used *) + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_insert_fwd" + | Lean -> "Vec.insert_fwd"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_insert_back" + | Lean -> "Vec.insert"); + }; + ] ); + ( "alloc::vec::Vec::len", + Some [ true; false ], + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_len" + | Lean -> "Vec.len"); + }; + ] ); + ( "alloc::vec::Vec::index", + Some [ true; false ], + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_index_fwd" + | Lean -> "Vec.index_shared"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_index_back" + | Lean -> "Vec.index_shared_back"); + }; + ] ); + ( "alloc::vec::Vec::index_mut", + Some [ true; false ], + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_index_mut_fwd" + | Lean -> "Vec.index_mut"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "vec_index_mut_back" + | Lean -> "Vec.index_mut_back"); + }; + ] ); + ] + +let mk_builtin_funs_map () = + SimpleNameMap.of_list + (List.map + (fun (name, filter, info) -> + (string_to_simple_name name, (filter, info))) + (builtin_funs ())) + +let builtin_funs_map () = mk_memoized mk_builtin_funs_map + +type builtin_trait_info = { + rust_name : string; + extract_name : string; + parent_clauses : string list; + consts : (string * string) list; + types : (string * string * string list) list; + (** Every type has: + - a Rust name + - an extraction name + - a list of clauses *) + funs : (string * Types.RegionGroupId.id option * string) list; +} + +let builtin_traits () = + let rg0 = Some Types.RegionGroupId.zero in + [ + { + (* Deref *) + rust_name = "core::ops::deref::Deref"; + extract_name = + (match !backend with + | Coq | FStar | HOL4 -> "core_ops_deref_Deref" + | Lean -> "core.ops.deref.Deref"); + parent_clauses = []; + consts = []; + types = + [ + ( "Target", + (match !backend with + | Coq | FStar | HOL4 -> "core_ops_deref_Deref_Target" + | Lean -> "Target"), + [] ); + ]; + funs = + [ + ( "deref", + None, + match !backend with + | Coq | FStar | HOL4 -> "core_ops_deref_Deref_deref" + | Lean -> "deref" ); + ]; + }; + { + (* DerefMut *) + rust_name = "core::ops::deref::DerefMut"; + extract_name = + (match !backend with + | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut" + | Lean -> "core.ops.deref.DerefMut"); + parent_clauses = + [ + (match !backend with + | Coq | FStar | HOL4 -> "deref_inst" + | Lean -> "DerefInst"); + ]; + consts = []; + types = []; + funs = + [ + ( "deref_mut", + None, + match !backend with + | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut" + | Lean -> "deref_mut" ); + ( "deref_mut", + rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut_back" + | Lean -> "deref_mut_back" ); + ]; + }; + { + (* Index *) + rust_name = "core::ops::index::Index"; + extract_name = + (match !backend with + | Coq | FStar | HOL4 -> "core_ops_index_Index" + | Lean -> "core.ops.index.Index"); + parent_clauses = []; + consts = []; + types = + [ + ( "Output", + (match !backend with + | Coq | FStar | HOL4 -> "core_ops_index_Index_Output" + | Lean -> "Output"), + [] ); + ]; + funs = + [ + ( "index", + None, + match !backend with + | Coq | FStar | HOL4 -> "core_ops_index_Index_index" + | Lean -> "index" ); + ]; + }; + { + (* IndexMut *) + rust_name = "core::ops::index::IndexMut"; + extract_name = + (match !backend with + | Coq | FStar | HOL4 -> "core_ops_index_IndexMut" + | Lean -> "core.ops.index.IndexMut"); + parent_clauses = + [ + (match !backend with + | Coq | FStar | HOL4 -> "index_inst" + | Lean -> "IndexInst"); + ]; + consts = []; + types = []; + funs = + [ + ( "index_mut", + None, + match !backend with + | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut" + | Lean -> "index_mut" ); + ( "index_mut", + rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back" + | Lean -> "index_mut_back" ); + ]; + }; + ] + +let mk_builtin_traits_map () = + SimpleNameMap.of_list + (List.map + (fun info -> (string_to_simple_name info.rust_name, info)) + (builtin_traits ())) + +let builtin_traits_map () = mk_memoized mk_builtin_traits_map diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index a09a6d05..5e849ba7 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -88,7 +88,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) can_diverge := !can_diverge || info.can_diverge | FunId (Assumed id) -> (* None of the assumed functions can diverge nor are considered stateful *) - can_fail := !can_fail || Assumed.assumed_can_fail id + can_fail := !can_fail || Assumed.assumed_fun_can_fail id | TraitMethod _ -> (* We consider trait functions can fail, diverge, and are not stateful *) can_fail := true; diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index c1041fa3..167e3d58 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -241,17 +241,6 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool) (* Initialize all the expanded values of all the variants *) List.map initialize variants_fields_types -(** Compute the expansion of an Option value. - *) -let compute_expanded_symbolic_option_value (expand_enumerations : bool) - (kind : V.sv_kind) (ty : T.rty) : V.symbolic_expansion list = - assert expand_enumerations; - let some_se = - V.SeAdt (Some T.option_some_id, [ mk_fresh_symbolic_value kind ty ]) - in - let none_se = V.SeAdt (Some T.option_none_id, []) in - [ none_se; some_se ] - let compute_expanded_symbolic_tuple_value (kind : V.sv_kind) (field_types : T.rty list) : V.symbolic_expansion = (* Generate the field values *) @@ -286,8 +275,6 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) def_id generics ctx | T.Tuple, [], _ -> [ compute_expanded_symbolic_tuple_value kind generics.types ] - | T.Assumed T.Option, [], [ ty ] -> - compute_expanded_symbolic_option_value expand_enumerations kind ty | T.Assumed T.Box, [], [ boxed_ty ] -> [ compute_expanded_symbolic_box_value kind boxed_ty ] | _ -> @@ -704,7 +691,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = | T.Adt ((Tuple | Assumed Box), _) | T.Ref (_, _, _) -> (* Ok *) expand_symbolic_value_no_branching config sv None - | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _) -> + | T.Adt (Assumed (Array | Slice | Str), _) -> (* We can't expand those *) raise (Failure diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index a42c552a..341e97eb 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -142,10 +142,10 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) | V.Adt av -> (* Sanity check *) (match v.V.ty with - | T.Adt (T.Assumed (T.Box | Vec), _) -> + | T.Adt (T.Assumed T.Box, _) -> raise (Failure "Can't copy an assumed value other than Option") | T.Adt (T.AdtId _, _) -> assert allow_adt_copy - | T.Adt ((T.Assumed Option | T.Tuple), _) -> () (* Ok *) + | T.Adt (T.Tuple, _) -> () (* Ok *) | T.Adt ( T.Assumed (Slice | T.Array), { @@ -722,70 +722,38 @@ let eval_rvalue_aggregate (config : C.config) fun ctx -> (* Match on the aggregate kind *) match aggregate_kind with - | E.AggregatedTuple -> - let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in - let v = V.Adt { variant_id = None; field_values = values } in - let generics = TypesUtils.mk_generic_args [] tys [] [] in - let ty = T.Adt (T.Tuple, generics) in - let aggregated : V.typed_value = { V.value = v; ty } in - (* Call the continuation *) - cf aggregated ctx - | E.AggregatedOption (variant_id, ty) -> - (* Sanity check *) - if variant_id = T.option_none_id then assert (values = []) - else if variant_id = T.option_some_id then - assert (List.length values = 1) - else raise (Failure "Unreachable"); - (* Construt the value *) - let generics = TypesUtils.mk_generic_args [] [ ty ] [] [] in - let aty = T.Adt (T.Assumed T.Option, generics) in - let av : V.adt_value = - { V.variant_id = Some variant_id; V.field_values = values } - in - let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in - (* Call the continuation *) - cf aggregated ctx - | E.AggregatedAdt (def_id, opt_variant_id, generics) -> - (* Sanity checks *) - let type_decl = C.ctx_lookup_type_decl ctx def_id in - assert ( - List.length type_decl.generics.regions = List.length generics.regions); - let expected_field_types = - Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id - generics - in - assert ( - expected_field_types - = List.map (fun (v : V.typed_value) -> v.V.ty) values); - (* Construct the value *) - let av : V.adt_value = - { V.variant_id = opt_variant_id; V.field_values = values } - in - let aty = T.Adt (T.AdtId def_id, generics) in - let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in - (* Call the continuation *) - cf aggregated ctx - | E.AggregatedRange ety -> - (* There should be two fields exactly *) - let v0, v1 = - match values with - | [ v0; v1 ] -> (v0, v1) - | _ -> raise (Failure "Unreachable") - in - (* Ranges are parametric over the type of indices. For now we only - support scalars, which can be of any type *) - assert (literal_type_is_integer (ty_as_literal ety)); - assert (v0.ty = ety); - assert (v1.ty = ety); - (* Construct the value *) - let av : V.adt_value = - { V.variant_id = None; V.field_values = values } - in - let generics = TypesUtils.mk_generic_args_from_types [ ety ] in - let aty = T.Adt (T.Assumed T.Range, generics) in - let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in - (* Call the continuation *) - cf aggregated ctx + | E.AggregatedAdt (type_id, opt_variant_id, generics) -> ( + match type_id with + | Tuple -> + let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in + let v = V.Adt { variant_id = None; field_values = values } in + let generics = TypesUtils.mk_generic_args [] tys [] [] in + let ty = T.Adt (T.Tuple, generics) in + let aggregated : V.typed_value = { V.value = v; ty } in + (* Call the continuation *) + cf aggregated ctx + | AdtId def_id -> + (* Sanity checks *) + let type_decl = C.ctx_lookup_type_decl ctx def_id in + assert ( + List.length type_decl.generics.regions + = List.length generics.regions); + let expected_field_types = + Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id + generics + in + assert ( + expected_field_types + = List.map (fun (v : V.typed_value) -> v.V.ty) values); + (* Construct the value *) + let av : V.adt_value = + { V.variant_id = opt_variant_id; V.field_values = values } + in + let aty = T.Adt (T.AdtId def_id, generics) in + let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in + (* Call the continuation *) + cf aggregated ctx + | Assumed _ -> raise (Failure "Unreachable")) | E.AggregatedArray (ety, cg) -> ( (* Sanity check: all the values have the proper type *) assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values); diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 465d0028..2a277c91 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -96,7 +96,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) | pe :: p' -> ( (* Match on the projection element and the value *) match (pe, v.V.value, v.V.ty) with - | ( Field (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id), + | ( Field ((ProjAdt (_, _) as proj_kind), field_id), V.Adt adt, T.Adt (type_id, _) ) -> ( (* Check consistency *) @@ -104,8 +104,6 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' -> assert (def_id = def_id'); assert (opt_variant_id = adt.variant_id) - | ProjOption variant_id, T.Assumed T.Option -> - assert (Some variant_id = adt.variant_id) | _ -> raise (Failure "Unreachable")); (* Actually project *) let fv = T.FieldId.nth adt.field_values field_id in @@ -136,7 +134,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) Ok (ctx, { res with updated }) (* If we reach Bottom, it may mean we need to expand an uninitialized * enumeration value *)) - | Field ((ProjAdt (_, _) | ProjTuple _ | ProjOption _), _), V.Bottom, _ -> + | Field ((ProjAdt (_, _) | ProjTuple _), _), V.Bottom, _ -> Error (FailBottom (1 + List.length p', pe, v.ty)) (* Symbolic value: needs to be expanded *) | _, Symbolic sp, _ -> @@ -376,20 +374,6 @@ let compute_expanded_bottom_adt_value (ctx : C.eval_ctx) let ty = T.Adt (T.AdtId def_id, generics) in { V.value = av; V.ty } -let compute_expanded_bottom_option_value (variant_id : T.VariantId.id) - (param_ty : T.ety) : V.typed_value = - (* Note that the variant can be [Some] or [None]: we expand bottom values - * when writing to fields or setting discriminants *) - let field_values = - if variant_id = T.option_some_id then [ mk_bottom param_ty ] - else if variant_id = T.option_none_id then [] - else raise (Failure "Unreachable") - in - let av = V.Adt { variant_id = Some variant_id; field_values } in - let generics = TypesUtils.mk_generic_args [] [ param_ty ] [] [] in - let ty = T.Adt (T.Assumed T.Option, generics) in - { V.value = av; ty } - let compute_expanded_bottom_tuple_value (field_types : T.ety list) : V.typed_value = (* Generate the field values *) @@ -451,17 +435,6 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place) T.Adt (T.AdtId def_id', generics) ) -> assert (def_id = def_id'); compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics - (* Option *) - | ( Field (ProjOption variant_id, _), - T.Adt - ( T.Assumed T.Option, - { - T.regions = []; - types = [ ty ]; - const_generics = []; - trait_refs = []; - } ) ) -> - compute_expanded_bottom_option_value variant_id ty (* Tuples *) | ( Field (ProjTuple arity, _), T.Adt diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index 041b0a97..0ff8063f 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -63,10 +63,6 @@ val compute_expanded_bottom_adt_value : T.egeneric_args -> V.typed_value -(** Compute an expanded [Option] ⊥ value *) -val compute_expanded_bottom_option_value : - T.VariantId.id -> T.ety -> V.typed_value - (** Drop (end) outer loans at a given place, which should be seen as an l-value (we will write to it later, but need to drop the loans before writing). diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 9f35c6f2..2aced79f 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -10,7 +10,6 @@ open TypesUtils open ValuesUtils module Inv = Invariants module S = SynthesizeSymbolic -open Utils open Cps open InterpreterUtils open InterpreterProjectors @@ -233,8 +232,7 @@ let set_discriminant (config : C.config) (p : E.place) let update_value cf (v : V.typed_value) : m_fun = fun ctx -> match (v.V.ty, v.V.value) with - | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Adt av - -> ( + | T.Adt ((T.AdtId _ as type_id), generics), V.Adt av -> ( (* There are two situations: - either the discriminant is already the proper one (in which case we don't do anything) @@ -253,24 +251,15 @@ let set_discriminant (config : C.config) (p : E.place) | T.AdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics - | T.Assumed T.Option -> - assert (generics.regions = []); - compute_expanded_bottom_option_value variant_id - (Collections.List.to_cons_nil generics.types) | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx) - | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Bottom - -> + | T.Adt ((T.AdtId _ as type_id), generics), V.Bottom -> let bottom_v = match type_id with | T.AdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics - | T.Assumed T.Option -> - assert (generics.regions = []); - compute_expanded_bottom_option_value variant_id - (Collections.List.to_cons_nil generics.types) | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx @@ -313,7 +302,7 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id) mk_unit_ty | _ -> (* Retrieve the function's signature *) - let sg = Assumed.get_assumed_sig fid in + let sg = Assumed.get_assumed_fun_sig fid in (* Instantiate the return type *) (* There shouldn't be any reference to Self *) let tr_self : T.erased_region T.trait_instance_id = @@ -426,11 +415,6 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun = in comp cf_pop cf_assign -(** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) : - cm_fun = - fun _cf _ctx -> raise Unimplemented - (** Auxiliary function - see {!eval_assumed_function_call} *) let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) : cm_fun = @@ -475,67 +459,6 @@ let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) : comp cf_move cf_create cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function which factorizes code to evaluate [std::Deref::deref] - and [std::DerefMut::deref_mut] - see {!eval_assumed_function_call} *) -let eval_box_deref_mut_or_shared_concrete (config : C.config) - (generics : T.egeneric_args) (is_mut : bool) : cm_fun = - fun cf ctx -> - (* Check the arguments *) - match - (generics.regions, generics.types, generics.const_generics, ctx.env) - with - | ( [], - [ boxed_ty ], - [], - Var (VarBinder input_var, input_value) - :: Var (_ret_var, _) - :: C.Frame :: _ ) -> - (* Required type checking. We must have: - - input_value.ty = & (mut) Box - - boxed_ty = ty - for some ty - *) - (let _, input_ty, ref_kind = ty_get_ref input_value.V.ty in - assert (match ref_kind with T.Shared -> not is_mut | T.Mut -> is_mut); - let input_ty = ty_get_box input_ty in - assert (input_ty = boxed_ty)); - - (* Borrow the boxed value *) - let p = - { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] } - in - let borrow_kind = if is_mut then E.Mut else E.Shared in - let rv = E.RvRef (p, borrow_kind) in - let cf_borrow = eval_rvalue_not_global config rv in - - (* Move the borrow to its destination *) - let cf_move cf res : m_fun = - match res with - | Error EPanic -> - (* We can't get there by borrowing a value *) - raise (Failure "Unreachable") - | Ok borrowed_value -> - (* Move and continue *) - let destp = mk_place_from_var_id E.VarId.zero in - assign_to_place config borrowed_value destp cf - in - - (* Compose and apply *) - comp cf_borrow cf_move cf ctx - | _ -> raise (Failure "Inconsistent state") - -(** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) : - cm_fun = - let is_mut = false in - eval_box_deref_mut_or_shared_concrete config generics is_mut - -(** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args) - : cm_fun = - let is_mut = true in - eval_box_deref_mut_or_shared_concrete config generics is_mut - (** Auxiliary function - see {!eval_assumed_function_call}. [Box::free] is not handled the same way as the other assumed functions: @@ -575,11 +498,6 @@ let eval_box_free (config : C.config) (generics : T.egeneric_args) cc cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) - (_generics : T.egeneric_args) : cm_fun = - fun _cf _ctx -> raise Unimplemented - (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : C.config) (fid : A.assumed_fun_id) (call : A.call) : cm_fun = @@ -636,18 +554,12 @@ let eval_assumed_function_call_concrete (config : C.config) * access to a body. *) let cf_eval_body : cm_fun = match fid with - | Replace -> eval_replace_concrete config generics | BoxNew -> eval_box_new_concrete config generics - | BoxDeref -> eval_box_deref_concrete config generics - | BoxDerefMut -> eval_box_deref_mut_concrete config generics | BoxFree -> (* Should have been treated above *) raise (Failure "Unreachable") - | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> - eval_vec_function_concrete config fid generics | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared - | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut - | ArrayRepeat | SliceIndexShared | SliceIndexMut | SliceSubsliceShared - | SliceSubsliceMut | SliceLen -> + | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut + | SliceLen -> raise (Failure "Unimplemented") in @@ -1531,7 +1443,7 @@ and eval_assumed_function_call_symbolic (config : C.config) (* There shouldn't be any reference to Self *) let tr_self = T.UnknownTrait __FUNCTION__ in instantiate_fun_sig ctx generics tr_self - (Assumed.get_assumed_sig fid) + (Assumed.get_assumed_fun_sig fid) in (* Evaluate the function call *) diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 9ac5ce13..5c8ec7af 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -447,7 +447,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = fields_with_types (* Assumed type case *) | V.Adt av, T.Adt (T.Assumed aty_id, generics) -> ( - assert (av.V.variant_id = None || aty_id = T.Option); + assert (av.V.variant_id = None); match ( aty_id, av.V.field_values, @@ -456,19 +456,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = generics.const_generics ) with (* Box *) - | T.Box, [ inner_value ], [], [ inner_ty ], [] - | T.Option, [ inner_value ], [], [ inner_ty ], [] -> + | T.Box, [ inner_value ], [], [ inner_ty ], [] -> assert (inner_value.V.ty = inner_ty) - | T.Option, _, [], [ _ ], [] -> - (* Option::None: nothing to check *) - () - | T.Vec, fvs, [], [ vec_ty ], [] -> - List.iter - (fun (v : V.typed_value) -> assert (v.ty = vec_ty)) - fvs - | T.Range, [ v0; v1 ], [], [ inner_ty ], [] -> - assert (v0.V.ty = inner_ty); - assert (v1.V.ty = inner_ty) | T.Array, inner_values, _, [ inner_ty ], [ cg ] -> (* *) assert ( diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index a982af30..2553127a 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -5,13 +5,13 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = match fun_id with | Regular id -> (FunDeclId.Map.find id fun_decls).signature - | Assumed aid -> Assumed.get_assumed_sig aid + | Assumed aid -> Assumed.get_assumed_fun_sig aid let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : Names.fun_name = match fun_id with | Regular id -> (FunDeclId.Map.find id fun_decls).name - | Assumed aid -> Assumed.get_assumed_name aid + | Assumed aid -> Assumed.get_assumed_fun_name aid (** Return the opaque declarations found in the crate. @@ -22,7 +22,7 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : *) let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : T.type_decl list * fun_decl list = - let open ExtractAssumed in + let open ExtractBuiltin in let is_opaque_fun (d : fun_decl) : bool = let sname = name_to_simple_name d.name in d.body = None @@ -30,7 +30,7 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitMethodDecl _ -> false | _ -> true) && ((not filter_assumed) - || not (SimpleNameMap.mem sname assumed_globals_map)) + || not (SimpleNameMap.mem sname builtin_globals_map)) in let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in (* Note that by checking the function bodies we also the globals *) diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 1058fab0..ee06fa07 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -108,7 +108,7 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl = | Assign (_, rv) -> ( match rv with | Use _ | RvRef _ -> not must_end_with_exit - | Aggregate (AggregatedTuple, []) -> not must_end_with_exit + | Aggregate (AggregatedAdt (Tuple, _, _), []) -> not must_end_with_exit | _ -> false) | FakeRead _ | Drop _ | Nop -> not must_end_with_exit | Panic | Return -> true diff --git a/compiler/Print.ml b/compiler/Print.ml index 1d5ddc50..aeacfbf0 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -127,17 +127,6 @@ module Values = struct (* Assumed type *) match (aty, field_values) with | Box, [ bv ] -> "@Box(" ^ bv ^ ")" - | Option, _ -> - if av.variant_id = Some T.option_some_id then - "@Option::Some(" - ^ Collections.List.to_cons_nil field_values - ^ ")" - else if av.variant_id = Some T.option_none_id then ( - assert (field_values = []); - "@Option::None") - else raise (Failure "Unreachable") - | Range, _ -> "@Range{ " ^ String.concat ", " field_values ^ "}" - | Vec, _ -> "@Vec[" ^ String.concat ", " field_values ^ "]" | Array, _ -> (* Happens when we aggregate values *) "@Array[" ^ String.concat ", " field_values ^ "]" diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index be7b3cb4..6396fe96 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -195,12 +195,9 @@ let assumed_ty_to_string (aty : assumed_ty) : string = | Result -> "Result" | Error -> "Error" | Fuel -> "Fuel" - | Option -> "Option" - | Vec -> "Vec" | Array -> "Array" | Slice -> "Slice" | Str -> "Str" - | Range -> "Range" let type_id_to_string (fmt : type_formatter) (id : type_id) : string = match id with @@ -354,10 +351,6 @@ let rec mprojection_to_string (fmt : ast_formatter) (inside : string) | pe :: p' -> ( let s = mprojection_to_string fmt inside p' in match pe.pkind with - | E.ProjOption variant_id -> - assert (variant_id = T.option_some_id); - assert (pe.field_id = T.FieldId.zero); - "(" ^ s ^ "as Option::Some)." ^ T.FieldId.to_string pe.field_id | E.ProjTuple _ -> "(" ^ s ^ ")." ^ T.FieldId.to_string pe.field_id | E.ProjAdt (adt_id, opt_variant_id) -> ( let field_name = @@ -395,8 +388,6 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id) | State | Array | Slice | Str -> (* Those types are opaque: we can't get there *) raise (Failure "Unreachable") - | Vec -> "@Vec" - | Range -> "@Range" | Result -> let variant_id = Option.get variant_id in if variant_id = result_return_id then "@Result::Return" @@ -412,13 +403,7 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id) let variant_id = Option.get variant_id in if variant_id = fuel_zero_id then "@Fuel::Zero" else if variant_id = fuel_succ_id then "@Fuel::Succ" - else raise (Failure "Unreachable: improper variant id for fuel type") - | Option -> - let variant_id = Option.get variant_id in - if variant_id = option_some_id then "@Option::Some " - else if variant_id = option_none_id then "@Option::None" - else - raise (Failure "Unreachable: improper variant id for result type")) + else raise (Failure "Unreachable: improper variant id for fuel type")) let adt_field_to_string (fmt : value_formatter) (adt_id : type_id) (field_id : FieldId.id) : string = @@ -435,11 +420,10 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id) | Assumed aty -> ( (* Assumed type *) match aty with - | Range -> FieldId.to_string field_id - | State | Fuel | Vec | Array | Slice | Str -> + | State | Fuel | Array | Slice | Str -> (* Opaque types: we can't get there *) raise (Failure "Unreachable") - | Result | Error | Option -> + | Result | Error -> (* Enumerations: we can't get there *) raise (Failure "Unreachable")) @@ -510,31 +494,13 @@ let adt_g_value_to_string (fmt : value_formatter) | [ v ] -> "@Fuel::Succ " ^ v | _ -> raise (Failure "@Fuel::Succ takes exactly one value") else raise (Failure "Unreachable: improper variant id for fuel type") - | Option -> - let variant_id = Option.get variant_id in - if variant_id = option_some_id then - match field_values with - | [ v ] -> "@Option::Some " ^ v - | _ -> raise (Failure "Option::Some takes exactly one value") - else if variant_id = option_none_id then ( - assert (field_values = []); - "@Option::None") - else - raise (Failure "Unreachable: improper variant id for result type") - | Vec | Array | Slice | Str -> - assert (variant_id = None); - let field_values = - List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values - in - let id = assumed_ty_to_string aty in - id ^ " [" ^ String.concat "; " field_values ^ "]" - | Range -> + | Array | Slice | Str -> assert (variant_id = None); let field_values = List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values in let id = assumed_ty_to_string aty in - id ^ " {" ^ String.concat "; " field_values ^ "}") + id ^ " [" ^ String.concat "; " field_values ^ "]") | _ -> let fmt = value_to_type_formatter fmt in raise @@ -593,29 +559,16 @@ let fun_suffix (lp_id : LoopId.id option) (rg_id : T.RegionGroupId.id option) : let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = match fid with - | Replace -> "core::mem::replace" | BoxNew -> "alloc::boxed::Box::new" - | BoxDeref -> "core::ops::deref::Deref::deref" - | BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut" | BoxFree -> "alloc::alloc::box_free" - | VecNew -> "alloc::vec::Vec::new" - | VecPush -> "alloc::vec::Vec::push" - | VecInsert -> "alloc::vec::Vec::insert" - | VecLen -> "alloc::vec::Vec::len" - | VecIndex -> "core::ops::index::Index::index" - | VecIndexMut -> "core::ops::index::IndexMut::index_mut" | ArrayIndexShared -> "@ArrayIndexShared" | ArrayIndexMut -> "@ArrayIndexMut" | ArrayToSliceShared -> "@ArrayToSliceShared" | ArrayToSliceMut -> "@ArrayToSliceMut" - | ArraySubsliceShared -> "@ArraySubsliceShared" - | ArraySubsliceMut -> "@ArraySubsliceMut" | ArrayRepeat -> "@ArrayRepeat" | SliceLen -> "@SliceLen" | SliceIndexShared -> "@SliceIndexShared" | SliceIndexMut -> "@SliceIndexMut" - | SliceSubsliceShared -> "@SliceSubsliceShared" - | SliceSubsliceMut -> "@SliceSubsliceMut" let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string = match fid with diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 47c7beb4..81e13af7 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -64,17 +64,7 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord] this state is opaque to Aeneas (the user can define it, or leave it as assumed) *) -type assumed_ty = - | State - | Result - | Error - | Fuel - | Vec - | Option - | Array - | Slice - | Str - | Range +type assumed_ty = State | Result | Error | Fuel | Array | Slice | Str [@@deriving show, ord] (* TODO: we should never directly manipulate [Return] and [Fail], but rather diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index b00509a6..a326d19e 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1513,7 +1513,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl = function calls, and when translating end abstractions. Here, we can do something simpler, in one micro-pass. *) -let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = +let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = (* The map visitor *) let obj = object @@ -1522,30 +1522,42 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = method! visit_texpression env e = match opt_destruct_function_call e with | Some (fun_id, _tys, args) -> ( + (* Below, when dealing with the arguments: we consider the very + * general case, where functions could be boxed (meaning we + * could have: [box_new f x]) + * *) match fun_id with | Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> ( - (* Below, when dealing with the arguments: we consider the very - * general case, where functions could be boxed (meaning we - * could have: [box_new f x]) - * *) match (aid, rg_id) with | BoxNew, _ -> assert (rg_id = None); let arg, args = Collections.List.pop args in mk_apps arg args - | BoxDeref, None -> + | BoxFree, _ -> + assert (args = []); + mk_unit_rvalue + | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared + | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut + | ArrayRepeat | SliceLen ), + _ ) -> + super#visit_texpression env e) + | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> ( + (* Lookup the function name *) + let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in + match (Names.name_to_string def.name, rg_id) with + | "alloc::box::Boxed::deref", None -> (* [Box::deref] forward is the identity *) let arg, args = Collections.List.pop args in mk_apps arg args - | BoxDeref, Some _ -> + | "alloc::box::Boxed::deref", Some _ -> (* [Box::deref] backward is [()] (doesn't give back anything) *) assert (args = []); mk_unit_rvalue - | BoxDerefMut, None -> + | "alloc::box::Boxed::deref_mut", None -> (* [Box::deref_mut] forward is the identity *) let arg, args = Collections.List.pop args in mk_apps arg args - | BoxDerefMut, Some _ -> + | "alloc::box::Boxed::deref_mut", Some _ -> (* [Box::deref_mut] back is almost the identity: * let box_deref_mut (x_init : t) (x_back : t) : t = x_back * *) @@ -1555,17 +1567,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = | _ -> raise (Failure "Unreachable") in mk_apps arg args - | BoxFree, _ -> - assert (args = []); - mk_unit_rvalue - | ( ( Replace | VecNew | VecPush | VecInsert | VecLen | VecIndex - | VecIndexMut | ArraySubsliceShared | ArraySubsliceMut - | SliceIndexShared | SliceIndexMut | SliceSubsliceShared - | SliceSubsliceMut | ArrayIndexShared | ArrayIndexMut - | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat - | SliceLen ), - _ ) -> - super#visit_texpression env e) + | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index b80ff72f..d31f0cf9 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -46,18 +46,7 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t) if variant_id = fuel_zero_id then [] else if variant_id = fuel_succ_id then [ mk_fuel_ty ] else raise (Failure "Unreachable: improper variant id for fuel type") - | Option -> - let ty = Collections.List.to_cons_nil generics.types in - let variant_id = Option.get variant_id in - if variant_id = option_some_id then [ ty ] - else if variant_id = option_none_id then [] - else - raise (Failure "Unreachable: improper variant id for option type") - | Range -> - let ty = Collections.List.to_cons_nil generics.types in - assert (variant_id = None); - [ ty; ty ] - | Vec | Array | Slice | Str -> + | Array | Slice | Str -> (* Array: when not symbolic values (for instance, because of aggregates), the array expressions are introduced as struct updates *) raise (Failure "Attempting to access the fields of an opaque type")) diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index b1680282..6d9b9e15 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -305,19 +305,7 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx) generics.types | T.Assumed aty -> ( match aty with - | T.Box | T.Vec -> - assert (generics.regions = []); - assert (List.length generics.types = 1); - assert (generics.const_generics = []); - generics.types - | T.Option -> - assert (generics.regions = []); - assert (List.length generics.types = 1); - assert (generics.const_generics = []); - if adt.V.variant_id = Some T.option_some_id then generics.types - else if adt.V.variant_id = Some T.option_none_id then [] - else raise (Failure "Unreachable") - | T.Range -> + | T.Box -> assert (generics.regions = []); assert (List.length generics.types = 1); assert (generics.const_generics = []); diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 54221cb1..9c698b51 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -405,8 +405,6 @@ let rec translate_sty (ty : T.sty) : ty = mk_simpl_tuple_ty generics.types | T.Assumed aty -> ( match aty with - | T.Vec -> Adt (Assumed Vec, generics) - | T.Option -> Adt (Assumed Option, generics) | T.Box -> ( (* Eliminate the boxes *) match generics.types with @@ -418,8 +416,7 @@ let rec translate_sty (ty : T.sty) : ty = ) | T.Array -> Adt (Assumed Array, generics) | T.Slice -> Adt (Assumed Slice, generics) - | T.Str -> Adt (Assumed Str, generics) - | T.Range -> Adt (Assumed Range, generics))) + | T.Str -> Adt (Assumed Str, generics))) | TypeVar vid -> TypeVar vid | Literal ty -> Literal ty | Never -> raise (Failure "Unreachable") @@ -510,12 +507,9 @@ let translate_type_id (id : T.type_id) : type_id = | T.Assumed aty -> let aty = match aty with - | T.Vec -> Vec - | T.Option -> Option | T.Array -> Array | T.Slice -> Slice | T.Str -> Str - | T.Range -> Range | T.Box -> (* Boxes have to be eliminated: this type id shouldn't be translated *) @@ -534,8 +528,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty = let t_generics = translate_fwd_generic_args type_infos generics in (* Eliminate boxes and simplify tuples *) match type_id with - | AdtId _ - | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) -> + | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) -> (* No general parametricity for now *) assert ( not @@ -610,8 +603,7 @@ let rec translate_back_ty (type_infos : TA.type_infos) match ty with | T.Adt (type_id, generics) -> ( match type_id with - | T.AdtId _ - | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) -> + | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) -> (* Don't accept ADTs (which are not tuples) with borrows for now *) assert (not (TypesUtils.ty_has_borrows type_infos ty)); let type_id = translate_type_id type_id in @@ -815,7 +807,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t) | FunId (Assumed aid) -> assert (lid = None); { - can_fail = Assumed.assumed_can_fail aid; + can_fail = Assumed.assumed_fun_can_fail aid; stateful_group = false; stateful = false; can_diverge = false; @@ -1221,9 +1213,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (* For now, only tuples can contain borrows *) let adt_id, _ = TypesUtils.ty_as_adt av.ty in match adt_id with - | T.AdtId _ - | T.Assumed - (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) -> + | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) -> assert (field_values = []); None | T.Tuple -> @@ -1368,9 +1358,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) * vector value upon visiting the "abstraction borrow" node *) let adt_id, _ = TypesUtils.ty_as_adt av.ty in match adt_id with - | T.AdtId _ - | T.Assumed - (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) -> + | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) -> assert (field_values = []); (ctx, None) | T.Tuple -> @@ -2441,17 +2429,12 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) (mk_typed_pattern_from_var var None) (mk_opt_mplace_texpression scrutinee_mplace scrutinee) branch - | T.Assumed (T.Vec | T.Array | T.Slice | T.Str) -> + | T.Assumed (T.Array | T.Slice | T.Str) -> (* We can't expand those values: we can access the fields only * through the functions provided by the API (note that we don't * know how to expand values like vectors or arrays, because they have a variable number * of fields!) *) raise (Failure "Attempt to expand a non-expandable value") - | T.Assumed Range -> raise (Failure "Unimplemented") - | T.Assumed T.Option -> - (* We shouldn't get there in the "one-branch" case: options have - * two variants *) - raise (Failure "Unreachable") and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 8e01c869..15297770 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -297,9 +297,11 @@ let translate_crate_to_pure (crate : A.crate) : (* Translate all the function *signatures* *) let assumed_sigs = List.map - (fun (id, sg, _, _) -> - (E.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg)) - Assumed.assumed_infos + (fun (info : Assumed.assumed_fun_info) -> + ( E.Assumed info.fun_id, + List.map (fun _ -> None) info.fun_sig.inputs, + info.fun_sig )) + Assumed.assumed_fun_infos in let local_sigs = List.map @@ -425,11 +427,15 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (true, kind) in (* Extract, if the config instructs to do so (depending on whether the type - * is opaque or not) *) - if + is opaque or not). Remark: we don't check if the definitions are builtin + here but in the function [export_types_group]: the reason is that if one + definition in the group is builtin, then we must check that all the + definitions are marked builtin *) + let extract = (is_opaque && config.extract_opaque) || ((not is_opaque) && config.extract_transparent) - then ( + in + if extract then ( if extract_decl then Extract.extract_type_decl ctx fmt type_decl_group kind def; if extract_extra_info then @@ -464,41 +470,58 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids in - (* Extract the type declarations. - - Because some declaration groups are delimited, we wrap the declarations - between [{start,end}_type_decl_group]. + (* Check if the definition are builtin - if yes they must be ignored. + Note that if one definition in the group is builtin, then all the + definitions must be builtin *) + let builtin = + let open ExtractBuiltin in + let types_map = builtin_types_map () in + List.map + (fun (def : Pure.type_decl) -> + let sname = name_to_simple_name def.name in + SimpleNameMap.find_opt sname types_map <> None) + defs + in - Ex.: - ==== - When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate - the [Datatype] and [End] delimiters in the snippet of code below: + if List.exists (fun b -> b) builtin then + (* Sanity check *) + assert (List.for_all (fun b -> b) builtin) + else ( + (* Extract the type declarations. + + Because some declaration groups are delimited, we wrap the declarations + between [{start,end}_type_decl_group]. + + Ex.: + ==== + When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate + the [Datatype] and [End] delimiters in the snippet of code below: + + {[ + Datatype: + tree = + TLeaf 'a + | TNode node ; + + node = + Node (tree list) + End + ]} + *) + Extract.start_type_decl_group ctx fmt is_rec defs; + List.iteri + (fun i def -> + let kind = kind_from_index i in + export_type_decl kind def) + defs; + Extract.end_type_decl_group fmt is_rec defs; - {[ - Datatype: - tree = - TLeaf 'a - | TNode node ; - - node = - Node (tree list) - End - ]} - *) - Extract.start_type_decl_group ctx fmt is_rec defs; - List.iteri - (fun i def -> - let kind = kind_from_index i in - export_type_decl kind def) - defs; - Extract.end_type_decl_group fmt is_rec defs; - - (* Export the extra information (ex.: [Arguments] instructions in Coq) *) - List.iteri - (fun i def -> - let kind = kind_from_index i in - export_type_extra_info kind def) - defs + (* Export the extra information (ex.: [Arguments] instructions in Coq) *) + List.iteri + (fun i def -> + let kind = kind_from_index i in + export_type_extra_info kind def) + defs) (** Export a global declaration. @@ -520,12 +543,12 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) && (((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque)) in - (* Check if it is an assumed global - if yes, we ignore it because we + (* Check if it is a builtin global - if yes, we ignore it because we map the definition to one in the standard library *) - let open ExtractAssumed in + let open ExtractBuiltin in let sname = name_to_simple_name global.name in let extract = - extract && SimpleNameMap.find_opt sname assumed_globals_map = None + extract && SimpleNameMap.find_opt sname builtin_globals_map = None in if extract then (* We don't wrap global declaration groups between calls to functions diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index 4a187893..16f8c5f9 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -168,9 +168,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref) in (* Continue exploring *) analyze expl_info ty_info rty - | Adt - ( (Tuple | Assumed (Box | Vec | Option | Slice | Array | Str | Range)), - generics ) -> + | Adt ((Tuple | Assumed (Box | Slice | Array | Str)), generics) -> (* Nothing to update: just explore the type parameters *) List.fold_left (fun ty_info ty -> analyze expl_info ty_info ty) diff --git a/compiler/dune b/compiler/dune index 2f5a0a44..4ec46b70 100644 --- a/compiler/dune +++ b/compiler/dune @@ -22,8 +22,8 @@ Expressions ExpressionsUtils Extract - ExtractAssumed ExtractBase + ExtractBuiltin FunsAnalysis Identifiers InterpreterBorrowsCore -- cgit v1.3.1 From 9c230dddebb171ee1b3e0176838441163836b875 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 24 Oct 2023 18:16:53 +0200 Subject: Handle properly the builtin, non fallible functions --- backends/lean/Base/Primitives/Base.lean | 4 ++-- compiler/ExtractBase.ml | 4 ++-- compiler/ExtractBuiltin.ml | 34 ++++++++++++++++++++++++++++++++- compiler/FunsAnalysis.ml | 34 ++++++++++++++++++--------------- tests/lean/NoNestedBorrows.lean | 12 ++++++------ 5 files changed, 62 insertions(+), 26 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 2bd081c0..10af8f67 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -120,8 +120,8 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := -- MISC -- ---------- -@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : Result a := ret x -@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : Result a := ret y +@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a := x +@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : a := y /-- Aeneas-translated function -- useful to reduce non-recursive definitions. Use with `simp [ aeneas ]` -/ diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index e004aba8..8f32ba44 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -22,8 +22,8 @@ type region_group_info = { *) } -module StringSet = Collections.MakeSet (Collections.OrderedString) -module StringMap = Collections.MakeMap (Collections.OrderedString) +module StringSet = Collections.StringSet +module StringMap = Collections.StringMap type name = Names.name type type_name = Names.type_name diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 9cc7c226..4c6fe014 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -376,7 +376,39 @@ let mk_builtin_funs_map () = let builtin_funs_map = mk_memoized mk_builtin_funs_map let builtin_non_fallible_funs = - [ "alloc::boxed::Box::deref"; "alloc::boxed::Box::deref_mut" ] + let int_names = + [ + "usize"; + "u8"; + "u16"; + "u32"; + "u64"; + "u128"; + "isize"; + "i8"; + "i16"; + "i32"; + "i64"; + "i128"; + ] + in + let int_ops = + [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ] + in + let int_funs = + List.map + (fun int_name -> + List.map (fun op -> "core::num::" ^ int_name ^ "::" ^ op) int_ops) + int_names + in + let int_funs = List.concat int_funs in + [ + "alloc::boxed::Box::deref"; + "alloc::boxed::Box::deref_mut"; + "core::mem::replace"; + "core::mem::take"; + ] + @ int_funs let builtin_non_fallible_funs_set = SimpleNameSet.of_list diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 1273f57d..3ba5d35d 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -57,21 +57,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let stateful = ref false in let can_diverge = ref false in let is_rec = ref false in + let is_builtin_non_fallible_group = ref false in (* We have some specialized knowledge of some library functions; we don't have any more custom treatment than this, and these functions can be modeled suitably in Primitives.fst, rather than special-casing for them all the way. *) - let module M = struct type opaque_info = { fallible: bool; stateful: bool } end in - let open M in - let opaque_info (f: fun_decl) = - match f.name with - | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "wrapping_add" ] - | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "rotate_left" ] -> - { fallible = false; stateful = false } - | _ -> - (* Opaque function: we consider they fail by default *) - { fallible = true; stateful = true } + let is_builtin_non_fallible (f : fun_decl) : bool = + let open ExtractBuiltin in + let name = name_to_simple_name f.name in + SimpleNameSet.mem name builtin_non_fallible_funs_set in (* JP: Why not use a reduce visitor here with a tuple of the values to be @@ -124,11 +119,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) in (* Sanity check: global bodies don't contain stateful calls *) assert ((not f.is_global_decl_body) || not !stateful); + let is_builtin_non_fallible = is_builtin_non_fallible f in + is_builtin_non_fallible_group := + !is_builtin_non_fallible_group || is_builtin_non_fallible; match f.body with | None -> - let info = opaque_info f in - obj#may_fail info.fallible; - stateful := (not f.is_global_decl_body) && use_state && info.stateful + obj#may_fail (not is_builtin_non_fallible); + stateful := + (not f.is_global_decl_body) + && use_state + && not is_builtin_non_fallible | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; @@ -136,12 +136,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) * groups containing globals contain exactly one declaration *) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in assert ((not is_global_decl_body) || List.length d = 1); + assert ((not !is_builtin_non_fallible_group) || List.length d = 1); (* We ignore on purpose functions that cannot fail and consider they *can* * fail: the result of the analysis is not used yet to adjust the translation * so that the functions which syntactically can't fail don't use an error monad. - * However, we do keep the result of the analysis for global bodies. + * However, we do keep the result of the analysis for global bodies and for + * builtin functions which are marked as non-fallible. * *) - can_fail := (not is_global_decl_body) || !can_fail; + can_fail := + ((not is_global_decl_body) && not !is_builtin_non_fallible_group) + || !can_fail; { can_fail = !can_fail; stateful = !stateful; diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index a90d6ea2..d6d603ce 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -139,9 +139,9 @@ def test_list1 : Result Unit := /- [no_nested_borrows::test_box1]: forward function -/ def test_box1 : Result Unit := - let b := (I32.ofInt 1) + let b := 1#i32 let x := b - if not (x = (I32.ofInt 1)) + if not (x = 1#i32) then Result.fail Error.panic else Result.ret () @@ -316,7 +316,7 @@ divergent def list_rev_aux /- [no_nested_borrows::list_rev]: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ def list_rev (T : Type) (l : List T) : Result (List T) := - let li := mem.replace (List T) l List.Nil + let li := core.mem.replace (List T) l List.Nil list_rev_aux T li List.Nil /- [no_nested_borrows::test_list_functions]: forward function -/ @@ -478,10 +478,10 @@ def test_weird_borrows1 : Result Unit := /- [no_nested_borrows::test_mem_replace]: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ def test_mem_replace (px : U32) : Result U32 := - let y := mem.replace U32 px (U32.ofInt 1) - if not (y = (U32.ofInt 0)) + let y := core.mem.replace U32 px 1#u32 + if not (y = 0#u32) then Result.fail Error.panic - else Result.ret (U32.ofInt 2) + else Result.ret 2#u32 /- [no_nested_borrows::test_shared_borrow_bool1]: forward function -/ def test_shared_borrow_bool1 (b : Bool) : Result U32 := -- cgit v1.3.1 From 005ad3cc03745bc9211defa481d5e45738a6d832 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 26 Oct 2023 14:37:34 +0200 Subject: Improve the handling of saved function effects in ExtractBuiltin.ml --- compiler/ExtractBuiltin.ml | 40 +++++++++++++++++++++++++++------------- compiler/FunsAnalysis.ml | 28 +++++++++++++++++----------- 2 files changed, 44 insertions(+), 24 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index afa0dd6f..363955bf 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -350,7 +350,9 @@ let mk_builtin_funs_map () = let builtin_funs_map = mk_memoized mk_builtin_funs_map -let builtin_non_fallible_funs = +type effect_info = { can_fail : bool; stateful : bool } + +let builtin_fun_effects = let int_names = [ "usize"; @@ -377,19 +379,31 @@ let builtin_non_fallible_funs = int_names in let int_funs = List.concat int_funs in - [ - "alloc::vec::Vec::new"; - "alloc::vec::Vec::len"; - "alloc::boxed::Box::deref"; - "alloc::boxed::Box::deref_mut"; - "core::mem::replace"; - "core::mem::take"; - ] - @ int_funs + let no_fail_no_state_funs = + [ + "alloc::vec::Vec::new"; + "alloc::vec::Vec::len"; + "alloc::boxed::Box::deref"; + "alloc::boxed::Box::deref_mut"; + "core::mem::replace"; + "core::mem::take"; + ] + @ int_funs + in + let no_fail_no_state_funs = + List.map + (fun n -> (n, { can_fail = false; stateful = false })) + no_fail_no_state_funs + in + let no_state_funs = [ "alloc::vec::Vec::push" ] in + let no_state_funs = + List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs + in + no_fail_no_state_funs @ no_state_funs -let builtin_non_fallible_funs_set = - SimpleNameSet.of_list - (List.map string_to_simple_name builtin_non_fallible_funs) +let builtin_fun_effects_map = + SimpleNameMap.of_list + (List.map (fun (n, x) -> (string_to_simple_name n, x)) builtin_fun_effects) type builtin_trait_decl_info = { rust_name : string; diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 3ba5d35d..9eac3e6f 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -57,16 +57,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let stateful = ref false in let can_diverge = ref false in let is_rec = ref false in - let is_builtin_non_fallible_group = ref false in + let group_has_builtin_info = ref false in (* We have some specialized knowledge of some library functions; we don't have any more custom treatment than this, and these functions can be modeled suitably in Primitives.fst, rather than special-casing for them all the way. *) - let is_builtin_non_fallible (f : fun_decl) : bool = + let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option = let open ExtractBuiltin in let name = name_to_simple_name f.name in - SimpleNameSet.mem name builtin_non_fallible_funs_set + SimpleNameMap.find_opt name builtin_fun_effects_map in (* JP: Why not use a reduce visitor here with a tuple of the values to be @@ -119,16 +119,21 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) in (* Sanity check: global bodies don't contain stateful calls *) assert ((not f.is_global_decl_body) || not !stateful); - let is_builtin_non_fallible = is_builtin_non_fallible f in - is_builtin_non_fallible_group := - !is_builtin_non_fallible_group || is_builtin_non_fallible; + let builtin_info = get_builtin_info f in + let has_builtin_info = builtin_info <> None in + group_has_builtin_info := !group_has_builtin_info || has_builtin_info; match f.body with | None -> - obj#may_fail (not is_builtin_non_fallible); + let info_can_fail, info_stateful = + match builtin_info with + | None -> (true, false) + | Some { can_fail; stateful } -> (can_fail, stateful) + in + obj#may_fail info_can_fail; stateful := (not f.is_global_decl_body) && use_state - && not is_builtin_non_fallible + && not (has_builtin_info && not info_stateful) | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; @@ -136,7 +141,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) * groups containing globals contain exactly one declaration *) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in assert ((not is_global_decl_body) || List.length d = 1); - assert ((not !is_builtin_non_fallible_group) || List.length d = 1); + assert ((not !group_has_builtin_info) || List.length d = 1); (* We ignore on purpose functions that cannot fail and consider they *can* * fail: the result of the analysis is not used yet to adjust the translation * so that the functions which syntactically can't fail don't use an error monad. @@ -144,8 +149,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) * builtin functions which are marked as non-fallible. * *) can_fail := - ((not is_global_decl_body) && not !is_builtin_non_fallible_group) - || !can_fail; + if is_global_decl_body then !can_fail + else if !group_has_builtin_info then !can_fail + else true; { can_fail = !can_fail; stateful = !stateful; -- cgit v1.3.1 From 7ffcb8e9c5c03f198362fd27bd42f30064541509 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 26 Oct 2023 15:06:36 +0200 Subject: Fix some issues and regenerate the HashmapMain example for Lean --- compiler/ExtractBuiltin.ml | 11 +- compiler/FunsAnalysis.ml | 11 +- compiler/InterpreterExpressions.ml | 3 +- tests/lean/HashmapMain/Funs.lean | 226 +++++++++++++++++++++---------------- tests/lean/HashmapMain/Types.lean | 2 +- 5 files changed, 147 insertions(+), 106 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 363955bf..2dbacce3 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -381,6 +381,7 @@ let builtin_fun_effects = let int_funs = List.concat int_funs in let no_fail_no_state_funs = [ + (* TODO: redundancy with the funs information below *) "alloc::vec::Vec::new"; "alloc::vec::Vec::len"; "alloc::boxed::Box::deref"; @@ -395,7 +396,15 @@ let builtin_fun_effects = (fun n -> (n, { can_fail = false; stateful = false })) no_fail_no_state_funs in - let no_state_funs = [ "alloc::vec::Vec::push" ] in + let no_state_funs = + [ + (* TODO: redundancy with the funs information below *) + "alloc::vec::Vec::push"; + "alloc::vec::Vec::index"; + "alloc::vec::Vec::index_mut"; + "alloc::vec::Vec::index_mut_back"; + ] + in let no_state_funs = List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs in diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 9eac3e6f..69c0df71 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -76,6 +76,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) object (self) inherit [_] iter_statement as super method may_fail b = can_fail := !can_fail || b + method maybe_stateful b = stateful := !stateful || b method! visit_Assert env a = self#may_fail true; @@ -126,14 +127,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) | None -> let info_can_fail, info_stateful = match builtin_info with - | None -> (true, false) + | None -> (true, use_state) | Some { can_fail; stateful } -> (can_fail, stateful) in obj#may_fail info_can_fail; - stateful := - (not f.is_global_decl_body) - && use_state - && not (has_builtin_info && not info_stateful) + obj#maybe_stateful + (if f.is_global_decl_body then false + else if not use_state then false + else info_stateful) | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 341e97eb..245f3b77 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -144,7 +144,8 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) (match v.V.ty with | T.Adt (T.Assumed T.Box, _) -> raise (Failure "Can't copy an assumed value other than Option") - | T.Adt (T.AdtId _, _) -> assert allow_adt_copy + | T.Adt (T.AdtId _, _) as ty -> + assert (allow_adt_copy || ty_is_primitively_copyable ty) | T.Adt (T.Tuple, _) -> () (* Ok *) | T.Adt ( T.Assumed (Slice | T.Array), diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 848b1a35..74fa8653 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -13,21 +13,21 @@ def hashmap.hash_key (k : Usize) : Result Usize := /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function -/ divergent def hashmap.HashMap.allocate_slots_loop - (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : - Result (Vec (hashmap.List T)) + (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) : + Result (alloc.vec.Vec (hashmap.List T)) := - if n > (Usize.ofInt 0) + if n > 0#usize then do - let slots0 ← Vec.push (hashmap.List T) slots hashmap.List.Nil - let n0 ← n - (Usize.ofInt 1) + let slots0 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil + let n0 ← n - 1#usize hashmap.HashMap.allocate_slots_loop T slots0 n0 else Result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function -/ def hashmap.HashMap.allocate_slots - (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : - Result (Vec (hashmap.List T)) + (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) : + Result (alloc.vec.Vec (hashmap.List T)) := hashmap.HashMap.allocate_slots_loop T slots n @@ -38,13 +38,13 @@ def hashmap.HashMap.new_with_capacity Result (hashmap.HashMap T) := do - let v := Vec.new (hashmap.List T) + let v := alloc.vec.Vec.new (hashmap.List T) let slots ← hashmap.HashMap.allocate_slots T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor Result.ret { - num_entries := (Usize.ofInt 0), + num_entries := 0#usize, max_load_factor := (max_load_dividend, max_load_divisor), max_load := i0, slots := slots @@ -52,22 +52,23 @@ def hashmap.HashMap.new_with_capacity /- [hashmap_main::hashmap::HashMap::{0}::new]: forward function -/ def hashmap.HashMap.new (T : Type) : Result (hashmap.HashMap T) := - hashmap.HashMap.new_with_capacity T (Usize.ofInt 32) (Usize.ofInt 4) - (Usize.ofInt 5) + hashmap.HashMap.new_with_capacity T 32#usize 4#usize 5#usize /- [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ divergent def hashmap.HashMap.clear_loop - (T : Type) (slots : Vec (hashmap.List T)) (i : Usize) : - Result (Vec (hashmap.List T)) + (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) : + Result (alloc.vec.Vec (hashmap.List T)) := - let i0 := Vec.len (hashmap.List T) slots + let i0 := alloc.vec.Vec.len (hashmap.List T) slots if i < i0 then do - let i1 ← i + (Usize.ofInt 1) + let i1 ← i + 1#usize let slots0 ← - Vec.index_mut_back (hashmap.List T) slots i hashmap.List.Nil + alloc.vec.Vec.index_mut_back (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List + T)) slots i hashmap.List.Nil hashmap.HashMap.clear_loop T slots0 i1 else Result.ret slots @@ -76,8 +77,8 @@ divergent def hashmap.HashMap.clear_loop def hashmap.HashMap.clear (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do - let v ← hashmap.HashMap.clear_loop T self.slots (Usize.ofInt 0) - Result.ret { self with num_entries := (Usize.ofInt 0), slots := v } + let v ← hashmap.HashMap.clear_loop T self.slots 0#usize + Result.ret { self with num_entries := 0#usize, slots := v } /- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/ def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize := @@ -130,21 +131,30 @@ def hashmap.HashMap.insert_no_resize := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.slots + let i := alloc.vec.Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod + let l ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T)) + self.slots hash_mod let inserted ← hashmap.HashMap.insert_in_list T key value l if inserted then do - let i0 ← self.num_entries + (Usize.ofInt 1) + let i0 ← self.num_entries + 1#usize let l0 ← hashmap.HashMap.insert_in_list_back T key value l - let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + let v ← + alloc.vec.Vec.index_mut_back (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List + T)) self.slots hash_mod l0 Result.ret { self with num_entries := i0, slots := v } else do let l0 ← hashmap.HashMap.insert_in_list_back T key value l - let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + let v ← + alloc.vec.Vec.index_mut_back (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List + T)) self.slots hash_mod l0 Result.ret { self with slots := v } /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function @@ -171,29 +181,35 @@ def hashmap.HashMap.move_elements_from_list /- [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ divergent def hashmap.HashMap.move_elements_loop - (T : Type) (ntable : hashmap.HashMap T) (slots : Vec (hashmap.List T)) - (i : Usize) : - Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) + (T : Type) (ntable : hashmap.HashMap T) + (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) : + Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T))) := - let i0 := Vec.len (hashmap.List T) slots + let i0 := alloc.vec.Vec.len (hashmap.List T) slots if i < i0 then do - let l ← Vec.index_mut (hashmap.List T) slots i - let ls := mem.replace (hashmap.List T) l hashmap.List.Nil + let l ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List + T)) slots i + let ls := core.mem.replace (hashmap.List T) l hashmap.List.Nil let ntable0 ← hashmap.HashMap.move_elements_from_list T ntable ls - let i1 ← i + (Usize.ofInt 1) - let l0 := mem.replace_back (hashmap.List T) l hashmap.List.Nil - let slots0 ← Vec.index_mut_back (hashmap.List T) slots i l0 + let i1 ← i + 1#usize + let l0 := core.mem.replace_back (hashmap.List T) l hashmap.List.Nil + let slots0 ← + alloc.vec.Vec.index_mut_back (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List + T)) slots i l0 hashmap.HashMap.move_elements_loop T ntable0 slots0 i1 else Result.ret (ntable, slots) /- [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ def hashmap.HashMap.move_elements - (T : Type) (ntable : hashmap.HashMap T) (slots : Vec (hashmap.List T)) - (i : Usize) : - Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) + (T : Type) (ntable : hashmap.HashMap T) + (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) : + Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T))) := hashmap.HashMap.move_elements_loop T ntable slots i @@ -203,17 +219,17 @@ def hashmap.HashMap.try_resize (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let max_usize ← Scalar.cast .Usize core_u32_max - let capacity := Vec.len (hashmap.List T) self.slots - let n1 ← max_usize / (Usize.ofInt 2) + let capacity := alloc.vec.Vec.len (hashmap.List T) self.slots + let n1 ← max_usize / 2#usize let (i, i0) := self.max_load_factor let i1 ← n1 / i if capacity <= i1 then do - let i2 ← capacity * (Usize.ofInt 2) + let i2 ← capacity * 2#usize let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - hashmap.HashMap.move_elements T ntable self.slots (Usize.ofInt 0) + hashmap.HashMap.move_elements T ntable self.slots 0#usize Result.ret { ntable0 @@ -255,9 +271,12 @@ def hashmap.HashMap.contains_key (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.slots + let i := alloc.vec.Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_shared (hashmap.List T) self.slots hash_mod + let l ← + alloc.vec.Vec.index (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T)) + self.slots hash_mod hashmap.HashMap.contains_key_in_list T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/ @@ -280,9 +299,12 @@ def hashmap.HashMap.get (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.slots + let i := alloc.vec.Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_shared (hashmap.List T) self.slots hash_mod + let l ← + alloc.vec.Vec.index (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T)) + self.slots hash_mod hashmap.HashMap.get_in_list T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/ @@ -327,9 +349,12 @@ def hashmap.HashMap.get_mut (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.slots + let i := alloc.vec.Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod + let l ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T)) + self.slots hash_mod hashmap.HashMap.get_mut_in_list T l key /- [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 -/ @@ -339,11 +364,17 @@ def hashmap.HashMap.get_mut_back := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.slots + let i := alloc.vec.Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod + let l ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T)) + self.slots hash_mod let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0 - let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + let v ← + alloc.vec.Vec.index_mut_back (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T)) + self.slots hash_mod l0 Result.ret { self with slots := v } /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/ @@ -354,13 +385,13 @@ divergent def hashmap.HashMap.remove_from_list_loop if ckey = key then let mv_ls := - mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) + core.mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) hashmap.List.Nil match mv_ls with - | hashmap.List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | hashmap.List.Cons i cvalue tl0 => Result.ret (some cvalue) | hashmap.List.Nil => Result.fail Error.panic else hashmap.HashMap.remove_from_list_loop T key tl - | hashmap.List.Nil => Result.ret Option.none + | hashmap.List.Nil => Result.ret none /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function -/ def hashmap.HashMap.remove_from_list @@ -375,7 +406,7 @@ divergent def hashmap.HashMap.remove_from_list_loop_back if ckey = key then let mv_ls := - mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) + core.mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) hashmap.List.Nil match mv_ls with | hashmap.List.Cons i cvalue tl0 => Result.ret tl0 @@ -396,16 +427,18 @@ def hashmap.HashMap.remove (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.slots + let i := alloc.vec.Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod + let l ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T)) + self.slots hash_mod let x ← hashmap.HashMap.remove_from_list T key l match x with - | Option.none => Result.ret Option.none - | Option.some x0 => - do - let _ ← self.num_entries - (Usize.ofInt 1) - Result.ret (Option.some x0) + | none => Result.ret none + | some x0 => do + let _ ← self.num_entries - 1#usize + Result.ret (some x0) /- [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 -/ def hashmap.HashMap.remove_back @@ -414,75 +447,75 @@ def hashmap.HashMap.remove_back := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.slots + let i := alloc.vec.Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod + let l ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T)) + self.slots hash_mod let x ← hashmap.HashMap.remove_from_list T key l match x with - | Option.none => + | none => do let l0 ← hashmap.HashMap.remove_from_list_back T key l - let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + let v ← + alloc.vec.Vec.index_mut_back (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List + T)) self.slots hash_mod l0 Result.ret { self with slots := v } - | Option.some x0 => + | some x0 => do - let i0 ← self.num_entries - (Usize.ofInt 1) + let i0 ← self.num_entries - 1#usize let l0 ← hashmap.HashMap.remove_from_list_back T key l - let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + let v ← + alloc.vec.Vec.index_mut_back (hashmap.List T) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List + T)) self.slots hash_mod l0 Result.ret { self with num_entries := i0, slots := v } /- [hashmap_main::hashmap::test1]: forward function -/ def hashmap.test1 : Result Unit := do let hm ← hashmap.HashMap.new U64 - let hm0 ← hashmap.HashMap.insert U64 hm (Usize.ofInt 0) (U64.ofInt 42) - let hm1 ← hashmap.HashMap.insert U64 hm0 (Usize.ofInt 128) (U64.ofInt 18) - let hm2 ← - hashmap.HashMap.insert U64 hm1 (Usize.ofInt 1024) (U64.ofInt 138) - let hm3 ← - hashmap.HashMap.insert U64 hm2 (Usize.ofInt 1056) (U64.ofInt 256) - let i ← hashmap.HashMap.get U64 hm3 (Usize.ofInt 128) - if not (i = (U64.ofInt 18)) + let hm0 ← hashmap.HashMap.insert U64 hm 0#usize 42#u64 + let hm1 ← hashmap.HashMap.insert U64 hm0 128#usize 18#u64 + let hm2 ← hashmap.HashMap.insert U64 hm1 1024#usize 138#u64 + let hm3 ← hashmap.HashMap.insert U64 hm2 1056#usize 256#u64 + let i ← hashmap.HashMap.get U64 hm3 128#usize + if not (i = 18#u64) then Result.fail Error.panic else do - let hm4 ← - hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024) - (U64.ofInt 56) - let i0 ← hashmap.HashMap.get U64 hm4 (Usize.ofInt 1024) - if not (i0 = (U64.ofInt 56)) + let hm4 ← hashmap.HashMap.get_mut_back U64 hm3 1024#usize 56#u64 + let i0 ← hashmap.HashMap.get U64 hm4 1024#usize + if not (i0 = 56#u64) then Result.fail Error.panic else do - let x ← hashmap.HashMap.remove U64 hm4 (Usize.ofInt 1024) + let x ← hashmap.HashMap.remove U64 hm4 1024#usize match x with - | Option.none => Result.fail Error.panic - | Option.some x0 => - if not (x0 = (U64.ofInt 56)) + | none => Result.fail Error.panic + | some x0 => + if not (x0 = 56#u64) then Result.fail Error.panic else do - let hm5 ← - hashmap.HashMap.remove_back U64 hm4 (Usize.ofInt 1024) - let i1 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 0) - if not (i1 = (U64.ofInt 42)) + let hm5 ← hashmap.HashMap.remove_back U64 hm4 1024#usize + let i1 ← hashmap.HashMap.get U64 hm5 0#usize + if not (i1 = 42#u64) then Result.fail Error.panic else do - let i2 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 128) - if not (i2 = (U64.ofInt 18)) + let i2 ← hashmap.HashMap.get U64 hm5 128#usize + if not (i2 = 18#u64) then Result.fail Error.panic else do - let i3 ← - hashmap.HashMap.get U64 hm5 (Usize.ofInt 1056) - if not (i3 = (U64.ofInt 256)) + let i3 ← hashmap.HashMap.get U64 hm5 1056#usize + if not (i3 = 256#u64) then Result.fail Error.panic else Result.ret () -/- Unit test for [hashmap_main::hashmap::test1] -/ -#assert (hashmap.test1 == .ret ()) - /- [hashmap_main::insert_on_disk]: forward function -/ def insert_on_disk (key : Usize) (value : U64) (st : State) : Result (State × Unit) := @@ -496,7 +529,4 @@ def insert_on_disk def main : Result Unit := Result.ret () -/- Unit test for [hashmap_main::main] -/ -#assert (main == .ret ()) - end hashmap_main diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean index 2b5cbd6c..065c109b 100644 --- a/tests/lean/HashmapMain/Types.lean +++ b/tests/lean/HashmapMain/Types.lean @@ -15,7 +15,7 @@ structure hashmap.HashMap (T : Type) where num_entries : Usize max_load_factor : (Usize × Usize) max_load : Usize - slots : Vec (hashmap.List T) + slots : alloc.vec.Vec (hashmap.List T) /- The state type used in the state-error monad -/ axiom State : Type -- cgit v1.3.1 From 3a22c56e026ee4488bc5e2d16d2066853ae7ccb9 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 16:22:09 +0100 Subject: Make the traits work for Coq --- Makefile | 2 +- compiler/Extract.ml | 391 +++++++++++++++++++++++++++++---------------- compiler/ExtractBase.ml | 8 + compiler/ExtractBuiltin.ml | 12 +- compiler/ExtractTypes.ml | 106 +++++++----- compiler/FunsAnalysis.ml | 7 +- compiler/Translate.ml | 22 ++- 7 files changed, 354 insertions(+), 194 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/Makefile b/Makefile index b67bd08b..427a5751 100644 --- a/Makefile +++ b/Makefile @@ -134,7 +134,7 @@ thol4-array: OPTIONS += test-traits: OPTIONS += test-traits: SUBDIR := traits tfstar-traits: OPTIONS += -decreases-clauses -template-clauses -tcoq-traits: OPTIONS += -use-fuel +tcoq-traits: OPTIONS += tlean-traits: SUBDIR := tlean-traits: OPTIONS += thol4-traits: OPTIONS += diff --git a/compiler/Extract.ml b/compiler/Extract.ml index e22f1385..d04f5c1d 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -320,8 +320,11 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id const_name ctx in + let add_brackets (s : string) = + if !backend = Coq then "(" ^ s ^ ")" else s + in if use_brackets then F.pp_print_string fmt ")"; - F.pp_print_string fmt ("." ^ name)) + F.pp_print_string fmt ("." ^ add_brackets name)) | _ -> (* "Regular" expression *) (* Open parentheses *) @@ -430,7 +433,10 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) ctx_get_trait_method trait_ref.trait_decl_ref.trait_decl_id method_name rg_id ctx in - F.pp_print_string fmt ("." ^ fun_name)) + let add_brackets (s : string) = + if !backend = Coq then "(" ^ s ^ ")" else s + in + F.pp_print_string fmt ("." ^ add_brackets fun_name)) else (* Provided method: we see it as a regular function call, and use the function name *) @@ -2021,12 +2027,15 @@ let extract_trait_decl_register_names (ctx : extraction_ctx) SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) in let ctx = - let trait_name = + let trait_name, trait_constructor = match builtin_info with - | None -> ctx.fmt.trait_decl_name trait_decl - | Some info -> info.extract_name + | None -> + ( ctx.fmt.trait_decl_name trait_decl, + ctx.fmt.trait_decl_constructor trait_decl ) + | Some info -> (info.extract_name, info.constructor) in - ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx + let ctx = ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx in + ctx_add (TraitDeclConstructorId trait_decl.def_id) trait_constructor ctx in (* Parent clauses *) let ctx = @@ -2108,7 +2117,7 @@ let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter) let extract_trait_impl_item (ctx : extraction_ctx) (fmt : F.formatter) (item_name : string) (ty : unit -> unit) : unit = - let assign = match !Config.backend with Lean -> ":=" | _ -> "=" in + let assign = match !Config.backend with Lean | Coq -> ":=" | _ -> "=" in extract_trait_item ctx fmt item_name assign ty (** Small helper - TODO: move *) @@ -2215,87 +2224,173 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) cg_params trait_clauses; F.pp_print_space fmt (); - (match !backend with - | Lean -> F.pp_print_string fmt "where" - | FStar -> if not is_empty then F.pp_print_string fmt "= {" - | _ -> F.pp_print_string fmt "{"); - if !backend = FStar && is_empty then F.pp_print_string fmt "= unit"; + if is_empty && !backend = FStar then ( + F.pp_print_string fmt "= unit"; + (* Outer box *) + F.pp_close_box fmt ()) + else if is_empty && !backend = Coq then ( + (* Coq is not very good at infering constructors *) + let cons = ctx_get_trait_constructor decl.def_id ctx in + F.pp_print_string fmt (":= " ^ cons ^ "{}."); + (* Outer box *) + F.pp_close_box fmt ()) + else ( + (match !backend with + | Lean -> F.pp_print_string fmt "where" + | FStar -> F.pp_print_string fmt "= {" + | Coq -> + let cons = ctx_get_trait_constructor decl.def_id ctx in + F.pp_print_string fmt (":= " ^ cons ^ " {") + | _ -> F.pp_print_string fmt "{"); - (* Close the box for the name + generics *) - F.pp_close_box fmt (); + (* Close the box for the name + generics *) + F.pp_close_box fmt (); - (* - * Extract the items - *) + (* + * Extract the items + *) - (* The constants *) - List.iter - (fun (name, (ty, _)) -> - let item_name = ctx_get_trait_const decl.def_id name ctx in - let ty () = - let inside = false in - F.pp_print_space fmt (); - extract_ty ctx fmt TypeDeclId.Set.empty inside ty - in - extract_trait_decl_item ctx fmt item_name ty) - decl.consts; + (* The constants *) + List.iter + (fun (name, (ty, _)) -> + let item_name = ctx_get_trait_const decl.def_id name ctx in + let ty () = + let inside = false in + F.pp_print_space fmt (); + extract_ty ctx fmt TypeDeclId.Set.empty inside ty + in + extract_trait_decl_item ctx fmt item_name ty) + decl.consts; - (* The types *) - List.iter - (fun (name, (clauses, _)) -> - (* Extract the type *) - let item_name = ctx_get_trait_type decl.def_id name ctx in - let ty () = - F.pp_print_space fmt (); - F.pp_print_string fmt (type_keyword ()) - in - extract_trait_decl_item ctx fmt item_name ty; - (* Extract the clauses *) - List.iter - (fun clause -> - let item_name = - ctx_get_trait_item_clause decl.def_id name clause.clause_id ctx - in - let ty () = - F.pp_print_space fmt (); - extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause - in - extract_trait_decl_item ctx fmt item_name ty) - clauses) - decl.types; + (* The types *) + List.iter + (fun (name, (clauses, _)) -> + (* Extract the type *) + let item_name = ctx_get_trait_type decl.def_id name ctx in + let ty () = + F.pp_print_space fmt (); + F.pp_print_string fmt (type_keyword ()) + in + extract_trait_decl_item ctx fmt item_name ty; + (* Extract the clauses *) + List.iter + (fun clause -> + let item_name = + ctx_get_trait_item_clause decl.def_id name clause.clause_id ctx + in + let ty () = + F.pp_print_space fmt (); + extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause + in + extract_trait_decl_item ctx fmt item_name ty) + clauses) + decl.types; - (* The parent clauses - note that the parent clauses may refer to the types - and const generics: for this reason we extract them *after* *) - List.iter - (fun clause -> - let item_name = - ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx - in - let ty () = - F.pp_print_space fmt (); - extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause - in - extract_trait_decl_item ctx fmt item_name ty) - decl.parent_clauses; + (* The parent clauses - note that the parent clauses may refer to the types + and const generics: for this reason we extract them *after* *) + List.iter + (fun clause -> + let item_name = + ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx + in + let ty () = + F.pp_print_space fmt (); + extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause + in + extract_trait_decl_item ctx fmt item_name ty) + decl.parent_clauses; - (* The required methods *) - List.iter - (fun (name, id) -> extract_trait_decl_method_items ctx fmt decl name id) - decl.required_methods; - - (* Close the outer boxes for the definition *) - if !Config.backend <> Lean then F.pp_close_box fmt (); - (* Close the brackets *) - (match !Config.backend with - | Lean -> () - | _ -> - if (not (!backend = FStar)) || not is_empty then ( + (* The required methods *) + List.iter + (fun (name, id) -> extract_trait_decl_method_items ctx fmt decl name id) + decl.required_methods; + + (* Close the outer boxes for the definition *) + if !Config.backend <> Lean then F.pp_close_box fmt (); + (* Close the brackets *) + match !Config.backend with + | Lean -> () + | Coq -> + F.pp_print_space fmt (); + F.pp_print_string fmt "}." + | _ -> F.pp_print_space fmt (); - F.pp_print_string fmt "}")); + F.pp_print_string fmt "}"); F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 +(** Generate the [Arguments] instructions for the trait declarationsin Coq, so + that we don't have to provide the implicit arguments when projecting the fields. *) +let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) + (decl : trait_decl) : unit = + (* Generating the [Arguments] instructions is useful only if there are parameters *) + let num_params = + List.length decl.generics.types + + List.length decl.generics.const_generics + + List.length decl.generics.trait_clauses + in + if num_params > 0 then ( + (* The constructor *) + let cons_name = ctx_get_trait_constructor decl.def_id ctx in + extract_coq_arguments_instruction ctx fmt cons_name num_params; + (* The constants *) + List.iter + (fun (name, _) -> + let item_name = ctx_get_trait_const decl.def_id name ctx in + extract_coq_arguments_instruction ctx fmt item_name num_params) + decl.consts; + (* The types *) + List.iter + (fun (name, (clauses, _)) -> + (* The type *) + let item_name = ctx_get_trait_type decl.def_id name ctx in + extract_coq_arguments_instruction ctx fmt item_name num_params; + (* The type clauses *) + List.iter + (fun clause -> + let item_name = + ctx_get_trait_item_clause decl.def_id name clause.clause_id ctx + in + extract_coq_arguments_instruction ctx fmt item_name num_params) + clauses) + decl.types; + (* The parent clauses *) + List.iter + (fun clause -> + let item_name = + ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx + in + extract_coq_arguments_instruction ctx fmt item_name num_params) + decl.parent_clauses; + (* The required methods *) + List.iter + (fun (item_name, id) -> + (* Lookup the definition *) + let trans = A.FunDeclId.Map.find id ctx.trans_funs in + (* Extract the items *) + let funs = + if trans.keep_fwd then trans.fwd :: trans.backs else trans.backs + in + let extract_for_method (f : fun_and_loops) = + let f = f.f in + let item_name = + ctx_get_trait_method decl.def_id item_name f.back_id ctx + in + extract_coq_arguments_instruction ctx fmt item_name num_params + in + List.iter extract_for_method funs) + decl.required_methods; + (* Add a space *) + F.pp_print_space fmt ()) + +(** See {!extract_trait_decl_coq_arguments} *) +let extract_trait_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) + (trait_decl : trait_decl) : unit = + match !backend with + | Coq -> extract_trait_decl_coq_arguments ctx fmt trait_decl + | _ -> () + (** Small helper. Extract the items for a method in a trait impl. @@ -2425,76 +2520,92 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) let is_empty = trait_impl_is_empty { impl with provided_methods = [] } in F.pp_print_space fmt (); - if !Config.backend = Lean then F.pp_print_string fmt ":= {" - else if !Config.backend = FStar && is_empty then F.pp_print_string fmt "= ()" - else F.pp_print_string fmt "= {"; + if is_empty && !Config.backend = FStar then ( + F.pp_print_string fmt "= ()"; + (* Outer box *) + F.pp_close_box fmt ()) + else if is_empty && !Config.backend = Coq then ( + (* Coq is not very good at infering constructors *) + let cons = ctx_get_trait_constructor impl.impl_trait.trait_decl_id ctx in + F.pp_print_string fmt (":= " ^ cons ^ "."); + (* Outer box *) + F.pp_close_box fmt ()) + else ( + if !Config.backend = Lean then F.pp_print_string fmt ":= {" + else if !Config.backend = Coq then F.pp_print_string fmt ":= {|" + else F.pp_print_string fmt "= {"; - (* Close the box for the name + generics *) - F.pp_close_box fmt (); + (* Close the box for the name + generics *) + F.pp_close_box fmt (); - (* - * Extract the items - *) - let trait_decl_id = impl.impl_trait.trait_decl_id in + (* + * Extract the items + *) + let trait_decl_id = impl.impl_trait.trait_decl_id in - (* The constants *) - List.iter - (fun (name, (_, id)) -> - let item_name = ctx_get_trait_const trait_decl_id name ctx in - let ty () = - F.pp_print_space fmt (); - F.pp_print_string fmt (ctx_get_global id ctx) - in + (* The constants *) + List.iter + (fun (name, (_, id)) -> + let item_name = ctx_get_trait_const trait_decl_id name ctx in + let ty () = + F.pp_print_space fmt (); + F.pp_print_string fmt (ctx_get_global id ctx) + in - extract_trait_impl_item ctx fmt item_name ty) - impl.consts; + extract_trait_impl_item ctx fmt item_name ty) + impl.consts; - (* The types *) - List.iter - (fun (name, (trait_refs, ty)) -> - (* Extract the type *) - let item_name = ctx_get_trait_type trait_decl_id name ctx in - let ty () = - F.pp_print_space fmt (); - extract_ty ctx fmt TypeDeclId.Set.empty false ty - in - extract_trait_impl_item ctx fmt item_name ty; - (* Extract the clauses *) - TraitClauseId.iteri - (fun clause_id trait_ref -> - let item_name = - ctx_get_trait_item_clause trait_decl_id name clause_id ctx - in - let ty () = - F.pp_print_space fmt (); - extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref - in - extract_trait_impl_item ctx fmt item_name ty) - trait_refs) - impl.types; - - (* The parent clauses *) - TraitClauseId.iteri - (fun clause_id trait_ref -> - let item_name = ctx_get_trait_parent_clause trait_decl_id clause_id ctx in - let ty () = - F.pp_print_space fmt (); - extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref - in - extract_trait_impl_item ctx fmt item_name ty) - impl.parent_trait_refs; + (* The types *) + List.iter + (fun (name, (trait_refs, ty)) -> + (* Extract the type *) + let item_name = ctx_get_trait_type trait_decl_id name ctx in + let ty () = + F.pp_print_space fmt (); + extract_ty ctx fmt TypeDeclId.Set.empty false ty + in + extract_trait_impl_item ctx fmt item_name ty; + (* Extract the clauses *) + TraitClauseId.iteri + (fun clause_id trait_ref -> + let item_name = + ctx_get_trait_item_clause trait_decl_id name clause_id ctx + in + let ty () = + F.pp_print_space fmt (); + extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref + in + extract_trait_impl_item ctx fmt item_name ty) + trait_refs) + impl.types; + + (* The parent clauses *) + TraitClauseId.iteri + (fun clause_id trait_ref -> + let item_name = + ctx_get_trait_parent_clause trait_decl_id clause_id ctx + in + let ty () = + F.pp_print_space fmt (); + extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref + in + extract_trait_impl_item ctx fmt item_name ty) + impl.parent_trait_refs; - (* The required methods *) - List.iter - (fun (name, id) -> - extract_trait_impl_method_items ctx fmt impl name id all_generics) - impl.required_methods; + (* The required methods *) + List.iter + (fun (name, id) -> + extract_trait_impl_method_items ctx fmt impl name id all_generics) + impl.required_methods; - (* Close the outer boxes for the definition, as well as the brackets *) - F.pp_close_box fmt (); - if (not (!backend = FStar)) || not is_empty then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "}"); + (* Close the outer boxes for the definition, as well as the brackets *) + F.pp_close_box fmt (); + if !backend = Coq then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "|}.") + else if (not (!backend = FStar)) || not is_empty then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "}")); F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 55b1bca3..31b1a447 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -246,6 +246,7 @@ type formatter = { *) trait_decl_name : trait_decl -> string; trait_impl_name : trait_decl -> trait_impl -> string; + trait_decl_constructor : trait_decl -> string; trait_parent_clause_name : trait_decl -> trait_clause -> string; trait_const_name : trait_decl -> string -> string; trait_type_name : trait_decl -> string -> string; @@ -388,6 +389,7 @@ type id = | TraitDeclId of TraitDeclId.id | TraitImplId of TraitImplId.id | LocalTraitClauseId of TraitClauseId.id + | TraitDeclConstructorId of TraitDeclId.id | TraitMethodId of TraitDeclId.id * string * T.RegionGroupId.id option (** Something peculiar with trait methods: because we have to take into account forward/backward functions, we may need to generate fields @@ -801,6 +803,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | TraitImplId id -> "trait_impl_id: " ^ TraitImplId.to_string id | LocalTraitClauseId id -> "local_trait_clause_id: " ^ TraitClauseId.to_string id + | TraitDeclConstructorId id -> + "trait_decl_constructor: " ^ trait_decl_id_to_string id | TraitParentClauseId (id, clause_id) -> "trait_parent_clause_id: " ^ trait_decl_id_to_string id ^ ", clause_id: " ^ TraitClauseId.to_string clause_id @@ -959,6 +963,10 @@ let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string = let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string = ctx_get_type (Assumed id) ctx +let ctx_get_trait_constructor (id : trait_decl_id) (ctx : extraction_ctx) : + string = + ctx_get (TraitDeclConstructorId id) ctx + let ctx_get_trait_self_clause (ctx : extraction_ctx) : string = ctx_get TraitSelfClauseId ctx diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index c6bde9c2..a54ab604 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -420,6 +420,7 @@ let builtin_fun_effects_map = type builtin_trait_decl_info = { rust_name : string; extract_name : string; + constructor : string; parent_clauses : string list; consts : (string * string) list; types : (string * (string * string list)) list; @@ -444,6 +445,7 @@ let builtin_trait_decls_info () = | Coq | FStar | HOL4 -> String.concat "_" rust_name | Lean -> String.concat "." rust_name) in + let constructor = mk_struct_constructor extract_name in let consts = [] in let types = let mk_type item_name = @@ -479,7 +481,15 @@ let builtin_trait_decls_info () = List.map mk_method methods in let rust_name = String.concat "::" rust_name in - { rust_name; extract_name; parent_clauses; consts; types; methods } + { + rust_name; + extract_name; + constructor; + parent_clauses; + consts; + types; + methods; + } in [ (* Deref *) diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index a294d4ca..77f76bb4 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -697,6 +697,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | Coq | HOL4 | Lean -> name in + let trait_decl_constructor (trait_decl : trait_decl) : string = + let name = trait_decl_name trait_decl in + ExtractBuiltin.mk_struct_constructor name + in + let trait_parent_clause_name (trait_decl : trait_decl) (clause : trait_clause) : string = (* TODO: improve - it would be better to not use indices *) @@ -937,6 +942,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) decreases_proof_name; trait_decl_name; trait_impl_name; + trait_decl_constructor; trait_parent_clause_name; trait_const_name; trait_type_name; @@ -1254,6 +1260,9 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id type_name ctx in + let add_brackets (s : string) = + if !backend = Coq then "(" ^ s ^ ")" else s + in (* There may be a special treatment depending on the instance id. See the comments for {!extract_trait_instance_id_with_dot}. TODO: there should be a cleaner way to do. The annoying thing @@ -1276,7 +1285,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) extract_trait_ref ctx fmt no_params_tys false trait_ref; extract_generic_args ctx fmt no_params_tys generics; if use_brackets then F.pp_print_string fmt ")"; - F.pp_print_string fmt ("." ^ type_name)) + F.pp_print_string fmt ("." ^ add_brackets type_name)) and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_ref) : unit = @@ -1376,6 +1385,7 @@ and extract_trait_instance_id_with_dot (ctx : extraction_ctx) and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) (id : trait_instance_id) : unit = + let add_brackets (s : string) = if !backend = Coq then "(" ^ s ^ ")" else s in match id with | Self -> (* This has a specific treatment depending on the item we're extracting @@ -1393,12 +1403,12 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter) (* Use the trait decl id to lookup the name *) let name = ctx_get_trait_parent_clause decl_id clause_id ctx in extract_trait_instance_id_with_dot ctx fmt no_params_tys true inst_id; - F.pp_print_string fmt name + F.pp_print_string fmt (add_brackets name) | ItemClause (inst_id, decl_id, item_name, clause_id) -> (* Use the trait decl id to lookup the name *) let name = ctx_get_trait_item_clause decl_id item_name clause_id ctx in extract_trait_instance_id_with_dot ctx fmt no_params_tys true inst_id; - F.pp_print_string fmt name + F.pp_print_string fmt (add_brackets name) | TraitRef trait_ref -> extract_trait_ref ctx fmt no_params_tys inside trait_ref | UnknownTrait _ -> @@ -2156,49 +2166,59 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) extract_type_decl_gen ctx fmt type_decl_group kind def extract_body | HOL4 -> extract_type_decl_hol4_opaque ctx fmt def +(** Generate a [Argument] instruction in Coq to allow omitting implicit + arguments for variants, fields, etc.. + + For instance, provided we have this definition: + {[ + Inductive result A := + | Return : A -> result A + | Fail_ : error -> result A. + ]} + + We may want to generate those instructions: + {[ + Arguments Return {_} a. + Arguments Fail_ {_}. + ]} + *) +let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter) + (cons_name : string) (num_implicit_params : int) : unit = + (* Add a break before *) + F.pp_print_break fmt 0 0; + (* Open a box *) + F.pp_open_hovbox fmt ctx.indent_incr; + F.pp_print_break fmt 0 0; + F.pp_print_string fmt "Arguments"; + F.pp_print_space fmt (); + F.pp_print_string fmt cons_name; + (* Print the type/const params and the trait clauses (`{T}`) *) + F.pp_print_space fmt (); + F.pp_print_string fmt "{"; + Collections.List.iter_times num_implicit_params (fun () -> + F.pp_print_space fmt (); + F.pp_print_string fmt "_"); + F.pp_print_space fmt (); + F.pp_print_string fmt "}."; + + (* Close the box *) + F.pp_close_box fmt () + (** Auxiliary function. - Generate [Arguments] instructions in Coq. + Generate [Arguments] instructions in Coq for type definitions. *) let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = assert (!backend = Coq); - (* Generating the [Arguments] instructions is useful only if there are type parameters *) - if decl.generics.types = [] && decl.generics.const_generics = [] then () + (* Generating the [Arguments] instructions is useful only if there are parameters *) + let num_params = + List.length decl.generics.types + + List.length decl.generics.const_generics + + List.length decl.generics.trait_clauses + in + if num_params = 0 then () else - (* Add the type params - note that we need those bindings only for the - * body translation (they are not top-level) *) - let _ctx_body, type_params, cg_params, trait_clauses = - ctx_add_generic_params decl.generics ctx - in - (* Auxiliary function to extract an [Arguments Cons {T} _ _.] instruction *) - let extract_arguments_info (cons_name : string) (fields : 'a list) : unit = - (* Add a break before *) - F.pp_print_break fmt 0 0; - (* Open a box *) - F.pp_open_hovbox fmt ctx.indent_incr; - F.pp_print_break fmt 0 0; - F.pp_print_string fmt "Arguments"; - F.pp_print_space fmt (); - F.pp_print_string fmt cons_name; - (* Print the type/const params and the trait clauses (`{T}`) *) - List.iter - (fun (var : string) -> - F.pp_print_space fmt (); - F.pp_print_string fmt ("{" ^ var ^ "}")) - (List.concat [ type_params; cg_params; trait_clauses ]); - (* Print the fields (`_`) *) - List.iter - (fun _ -> - F.pp_print_space fmt (); - F.pp_print_string fmt "_") - fields; - F.pp_print_string fmt "."; - - (* Close the box *) - F.pp_close_box fmt () - in - (* Generate the [Arguments] instruction *) match decl.kind with | Opaque -> () @@ -2206,23 +2226,23 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) let adt_id = AdtId decl.def_id in (* Generate the instruction for the record constructor *) let cons_name = ctx_get_struct adt_id ctx in - extract_arguments_info cons_name fields; + extract_coq_arguments_instruction ctx fmt cons_name num_params; (* Generate the instruction for the record projectors, if there are *) let is_rec = decl_is_from_rec_group kind in if not is_rec then FieldId.iteri (fun fid _ -> let cons_name = ctx_get_field adt_id fid ctx in - extract_arguments_info cons_name []) + extract_coq_arguments_instruction ctx fmt cons_name num_params) fields; (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 | Enum variants -> (* Generate the instructions *) VariantId.iteri - (fun vid (v : variant) -> + (fun vid (_ : variant) -> let cons_name = ctx_get_variant (AdtId decl.def_id) vid ctx in - extract_arguments_info cons_name v.fields) + extract_coq_arguments_instruction ctx fmt cons_name num_params) variants; (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 69c0df71..e17ea16f 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -104,9 +104,10 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* None of the assumed functions can diverge nor are considered stateful *) can_fail := !can_fail || Assumed.assumed_fun_can_fail id | TraitMethod _ -> - (* We consider trait functions can fail, diverge, and are not stateful *) - can_fail := true; - can_diverge := true); + (* We consider trait functions can fail, but can not diverge and are not stateful. + TODO: this may cause issues if we use use a fuel parameter. + *) + can_fail := true); super#visit_Call env call method! visit_Panic env = diff --git a/compiler/Translate.ml b/compiler/Translate.ml index cb23198a..a3d96023 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -751,14 +751,17 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) (** Export a trait declaration. *) let export_trait_decl (fmt : Format.formatter) (_config : gen_config) - (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit = + (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) (extract_decl : bool) + (extract_extra_info : bool) : unit = let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in (* Check if the trait declaration is builtin, in which case we ignore it *) let open ExtractBuiltin in let sname = name_to_simple_name trait_decl.name in - if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then + if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then ( let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in - Extract.extract_trait_decl ctx fmt trait_decl + if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl; + if extract_extra_info then + Extract.extract_trait_decl_extra_info ctx fmt trait_decl) else () (** Export a trait implementation. *) @@ -796,7 +799,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) let export_functions_group = export_functions_group fmt config ctx in let export_global = export_global fmt config ctx in let export_types_group = export_types_group fmt config ctx in - let export_trait_decl = export_trait_decl fmt config ctx in + let export_trait_decl_group id = + export_trait_decl fmt config ctx id true false + in + let export_trait_decl_group_extra_info id = + export_trait_decl fmt config ctx id false true + in let export_trait_impl = export_trait_impl fmt config ctx in let export_state_type () : unit = @@ -833,8 +841,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) export_functions_group pure_funs | Global id -> export_global id | TraitDecl id -> - if config.extract_trait_decls && config.extract_transparent then - export_trait_decl id + (* TODO: update to extract groups *) + if config.extract_trait_decls && config.extract_transparent then ( + export_trait_decl_group id; + export_trait_decl_group_extra_info id) | TraitImpl id -> if config.extract_trait_impls && config.extract_transparent then export_trait_impl id -- cgit v1.3.1