diff options
Diffstat (limited to '')
| -rw-r--r-- | src/ExtractToFStar.ml | 7 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 60 | ||||
| -rw-r--r-- | src/LlbcAst.ml | 4 | ||||
| -rw-r--r-- | src/LlbcOfJson.ml | 10 | ||||
| -rw-r--r-- | src/Print.ml | 34 | ||||
| -rw-r--r-- | src/PrintPure.ml | 2 | ||||
| -rw-r--r-- | src/Pure.ml | 6 | ||||
| -rw-r--r-- | src/PureUtils.ml | 14 | ||||
| -rw-r--r-- | src/Substitute.ml | 6 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 16 |
10 files changed, 76 insertions, 83 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 19e17260..e00a4e53 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -872,12 +872,11 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (* Top-level qualifier *) match qualif.id with | Func fun_id -> - extract_function_call ctx fmt inside fun_id qualif.type_params args + extract_function_call ctx fmt inside fun_id qualif.type_args args | AdtCons adt_cons_id -> - extract_adt_cons ctx fmt inside adt_cons_id qualif.type_params args + extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args | Proj proj -> - extract_field_projector ctx fmt inside app proj qualif.type_params - args) + extract_field_projector ctx fmt inside app proj qualif.type_args args) | _ -> (* "Regular" expression *) (* Open parentheses *) diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index c3331de5..e8e9c6c4 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -994,18 +994,18 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = *) match call.func with | A.Regular fid -> - eval_local_function_call config fid call.region_params call.type_params + eval_local_function_call config fid call.region_args call.type_args call.args call.dest | A.Assumed fid -> - eval_non_local_function_call config fid call.region_params - call.type_params call.args call.dest + eval_non_local_function_call config fid call.region_args call.type_args + call.args call.dest (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) - (region_params : T.erased_region list) (type_params : T.ety list) + (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> - assert (region_params = []); + assert (region_args = []); (* Retrieve the (correctly instantiated) body *) let def = C.ctx_lookup_fun_decl ctx fid in @@ -1022,7 +1022,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) let tsubst = Subst.make_type_subst (List.map (fun v -> v.T.index) def.A.signature.type_params) - type_params + type_args in let locals, body_st = Subst.fun_body_substitute_in_body tsubst body in @@ -1080,7 +1080,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) - (region_params : T.erased_region list) (type_params : T.ety list) + (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Retrieve the (correctly instantiated) signature *) @@ -1088,12 +1088,12 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) let sg = def.A.signature in (* Instantiate the signature and introduce fresh abstraction and region ids * while doing so *) - let inst_sg = instantiate_fun_sig type_params sg in + let inst_sg = instantiate_fun_sig type_args sg in (* Sanity check *) assert (List.length args = List.length def.A.signature.inputs); (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg - region_params type_params args dest cf ctx + region_args type_args args dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -1102,10 +1102,10 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) *) and eval_function_call_symbolic_from_inst_sig (config : C.config) (fid : A.fun_id) (inst_sg : A.inst_fun_sig) - (region_params : T.erased_region list) (type_params : T.ety list) + (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> - assert (region_params = []); + assert (region_args = []); (* 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 @@ -1169,7 +1169,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (* Synthesize the symbolic AST *) let abs_ids = List.map (fun rg -> rg.T.id) inst_sg.regions_hierarchy in - S.synthesize_regular_function_call fid call_id abs_ids type_params args + S.synthesize_regular_function_call fid call_id abs_ids type_args args args_places ret_spc dest_place expr in let cc = comp cc cf_call in @@ -1185,8 +1185,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (** Evaluate a non-local function call in symbolic mode *) and eval_non_local_function_call_symbolic (config : C.config) - (fid : A.assumed_fun_id) (region_params : T.erased_region list) - (type_params : T.ety list) (args : E.operand list) (dest : E.place) : + (fid : A.assumed_fun_id) (region_args : T.erased_region list) + (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Sanity check: make sure the type parameters don't contain regions - @@ -1194,7 +1194,7 @@ and eval_non_local_function_call_symbolic (config : C.config) assert ( List.for_all (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty)) - type_params); + type_args); (* There are two cases (and this is extremely annoying): - the function is not box_free @@ -1205,7 +1205,7 @@ and eval_non_local_function_call_symbolic (config : C.config) | A.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 region_params type_params args dest (cf Unit) ctx + eval_box_free config region_args type_args args dest (cf Unit) ctx | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined @@ -1216,55 +1216,53 @@ and eval_non_local_function_call_symbolic (config : C.config) | A.BoxFree -> (* should have been treated above *) raise (Failure "Unreachable") - | _ -> instantiate_fun_sig type_params (Assumed.get_assumed_sig fid) + | _ -> instantiate_fun_sig type_args (Assumed.get_assumed_sig fid) in (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig - region_params type_params args dest cf ctx + region_args type_args args dest cf ctx (** Evaluate a non-local (i.e, assumed) function call such as `Box::deref` (auxiliary helper for [eval_statement]) *) and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) - (region_params : T.erased_region list) (type_params : T.ety list) + (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Debug *) log#ldebug (lazy - (let type_params = - "[" - ^ String.concat ", " (List.map (ety_to_string ctx) type_params) - ^ "]" + (let type_args = + "[" ^ String.concat ", " (List.map (ety_to_string ctx) type_args) ^ "]" in let args = "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]" in let dest = place_to_string ctx dest in "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid - ^ "\n- type_params: " ^ type_params ^ "\n- args: " ^ args ^ "\n- dest: " + ^ "\n- type_args: " ^ type_args ^ "\n- args: " ^ args ^ "\n- dest: " ^ dest)); match config.mode with | C.ConcreteMode -> - eval_non_local_function_call_concrete config fid region_params type_params + eval_non_local_function_call_concrete config fid region_args type_args args dest (cf Unit) ctx | C.SymbolicMode -> - eval_non_local_function_call_symbolic config fid region_params type_params + eval_non_local_function_call_symbolic config fid region_args type_args args dest cf ctx (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id) - (region_params : T.erased_region list) (type_params : T.ety list) + (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = match config.mode with | ConcreteMode -> - eval_local_function_call_concrete config fid region_params type_params - args dest + eval_local_function_call_concrete config fid region_args type_args args + dest | SymbolicMode -> - eval_local_function_call_symbolic config fid region_params type_params - args dest + eval_local_function_call_symbolic config fid region_args type_args args + dest (** Evaluate a statement seen as a function body (auxiliary helper for [eval_statement]) *) diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml index 6e77cadb..d35cd5d8 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -65,8 +65,8 @@ type inst_fun_sig = { type call = { func : fun_id; - region_params : erased_region list; - type_params : ety list; + region_args : erased_region list; + type_args : ety list; args : operand list; dest : place; } diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 7604ec2b..75e9cbf7 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -532,17 +532,17 @@ let call_of_json (js : json) : (A.call, string) result = | `Assoc [ ("func", func); - ("region_params", region_params); - ("type_params", type_params); + ("region_args", region_args); + ("type_args", type_args); ("args", args); ("dest", dest); ] -> let* func = fun_id_of_json func in - let* region_params = list_of_json erased_region_of_json region_params in - let* type_params = list_of_json ety_of_json type_params in + let* region_args = list_of_json erased_region_of_json region_args in + let* type_args = list_of_json ety_of_json type_args in let* args = list_of_json operand_of_json args in let* dest = place_of_json dest in - Ok { A.func; region_params; type_params; args; dest } + Ok { A.func; region_args; type_args; args; dest } | _ -> Error "") let rec statement_of_json (js : json) : (A.statement, string) result = diff --git a/src/Print.ml b/src/Print.ml index 98e9dd74..fedc4122 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -953,41 +953,41 @@ module LlbcAst = struct else indent ^ "assert(¬" ^ cond ^ ")" | A.Call call -> let ty_fmt = ast_to_etype_formatter fmt in - let params = - if List.length call.A.type_params > 0 then + let t_params = + if List.length call.A.type_args > 0 then "<" ^ String.concat "," - (List.map (PT.ty_to_string ty_fmt) call.A.type_params) + (List.map (PT.ty_to_string ty_fmt) call.A.type_args) ^ ">" else "" in let args = List.map (operand_to_string fmt) call.A.args in let args = "(" ^ String.concat ", " args ^ ")" in - let name_params = + let name_args = match call.A.func with - | A.Regular fid -> fmt.fun_decl_id_to_string fid ^ params + | A.Regular fid -> fmt.fun_decl_id_to_string fid ^ t_params | A.Assumed fid -> ( match fid with - | A.Replace -> "core::mem::replace" ^ params - | A.BoxNew -> "alloc::boxed::Box" ^ params ^ "::new" + | A.Replace -> "core::mem::replace" ^ t_params + | A.BoxNew -> "alloc::boxed::Box" ^ t_params ^ "::new" | A.BoxDeref -> - "core::ops::deref::Deref<Box" ^ params ^ ">::deref" + "core::ops::deref::Deref<Box" ^ t_params ^ ">::deref" | A.BoxDerefMut -> - "core::ops::deref::DerefMut" ^ params ^ "::deref_mut" - | A.BoxFree -> "alloc::alloc::box_free" ^ params - | A.VecNew -> "alloc::vec::Vec" ^ params ^ "::new" - | A.VecPush -> "alloc::vec::Vec" ^ params ^ "::push" - | A.VecInsert -> "alloc::vec::Vec" ^ params ^ "::insert" - | A.VecLen -> "alloc::vec::Vec" ^ params ^ "::len" + "core::ops::deref::DerefMut" ^ t_params ^ "::deref_mut" + | A.BoxFree -> "alloc::alloc::box_free" ^ t_params + | A.VecNew -> "alloc::vec::Vec" ^ t_params ^ "::new" + | A.VecPush -> "alloc::vec::Vec" ^ t_params ^ "::push" + | A.VecInsert -> "alloc::vec::Vec" ^ t_params ^ "::insert" + | A.VecLen -> "alloc::vec::Vec" ^ t_params ^ "::len" | A.VecIndex -> - "core::ops::index::Index<alloc::vec::Vec" ^ params + "core::ops::index::Index<alloc::vec::Vec" ^ t_params ^ ">::index" | A.VecIndexMut -> - "core::ops::index::IndexMut<alloc::vec::Vec" ^ params + "core::ops::index::IndexMut<alloc::vec::Vec" ^ t_params ^ ">::index_mut") in let dest = place_to_string fmt call.A.dest in - indent ^ dest ^ " := move " ^ name_params ^ args + indent ^ dest ^ " := move " ^ name_args ^ args | A.Panic -> indent ^ "panic" | A.Return -> indent ^ "return" | A.Break i -> indent ^ "break " ^ string_of_int i diff --git a/src/PrintPure.ml b/src/PrintPure.ml index e40a7b8b..b29f6e70 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -516,7 +516,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string) in (* Convert the type instantiation *) let ty_fmt = ast_to_type_formatter fmt in - let tys = List.map (ty_to_string ty_fmt) qualif.type_params in + let tys = List.map (ty_to_string ty_fmt) qualif.type_args in (* *) (qualif_s, tys) | _ -> diff --git a/src/Pure.ml b/src/Pure.ml index 05f7e199..3798c555 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -373,11 +373,7 @@ type qualif_id = | Proj of proj_kind (** Field projector *) [@@deriving show] -type qualif = { - id : qualif_id; - type_params : ty list; (* TODO: rename to type_args *) -} -[@@deriving show] +type qualif = { id : qualif_id; type_args : ty list } [@@deriving show] (** An instantiated qualified. Note that for now we have a clear separation between types and expressions, diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 0d941079..96d84fb1 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -260,7 +260,7 @@ let opt_destruct_function_call (e : texpression) : | None -> None | Some (qualif, args) -> ( match qualif.id with - | Func fun_id -> Some (fun_id, qualif.type_params, args) + | Func fun_id -> Some (fun_id, qualif.type_args, args) | _ -> None) let opt_destruct_result (ty : ty) : ty option = @@ -344,7 +344,7 @@ let unit_ty : ty = Adt (Tuple, []) (** TODO: rename to "mk_unit_texpression" *) let unit_rvalue : texpression = let id = AdtCons { adt_id = Tuple; variant_id = None } in - let qualif = { id; type_params = [] } in + let qualif = { id; type_args = [] } in let e = Qualif qualif in let ty = unit_ty in { e; ty } @@ -395,7 +395,7 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression = let ty = mk_arrows tys ty in (* Construct the tuple constructor qualifier *) let id = AdtCons { adt_id = Tuple; variant_id = None } in - let qualif = { id; type_params = tys } in + let qualif = { id; type_args = tys } in (* Put everything together *) let cons = { e = Qualif qualif; ty } in mk_apps cons vl @@ -423,7 +423,7 @@ let mk_result_fail_rvalue (ty : ty) : texpression = let id = AdtCons { adt_id = Assumed Result; variant_id = Some result_fail_id } in - let qualif = { id; type_params = type_args } in + let qualif = { id; type_args } in let cons_e = Qualif qualif in let cons_ty = ty in let cons = { e = cons_e; ty = cons_ty } in @@ -436,7 +436,7 @@ let mk_result_return_rvalue (v : texpression) : texpression = let id = AdtCons { adt_id = Assumed Result; variant_id = Some result_return_id } in - let qualif = { id; type_params = type_args } in + let qualif = { id; type_args } in let cons_e = Qualif qualif in let cons_ty = mk_arrow v.ty ty in let cons = { e = cons_e; ty = cons_ty } in @@ -597,7 +597,7 @@ module TypeCheck = struct let variant_id = None in let expected_field_tys = get_adt_field_types ctx.type_decls adt_id variant_id - qualif.type_params + qualif.type_args in let expected_field_ty = FieldId.nth expected_field_tys field_id in let _adt_ty, field_ty = destruct_arrow e.ty in @@ -607,7 +607,7 @@ module TypeCheck = struct (* TODO: we might also want to check the out type *) let expected_field_tys = get_adt_field_types ctx.type_decls id.adt_id id.variant_id - qualif.type_params + qualif.type_args in let field_tys, _ = destruct_arrows e.ty in assert (expected_field_tys = field_tys)) diff --git a/src/Substitute.ml b/src/Substitute.ml index 81f6985b..7cb0e8c2 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -262,15 +262,15 @@ let assertion_substitute (tsubst : T.TypeVarId.id -> T.ety) (a : A.assertion) : let call_substitute (tsubst : T.TypeVarId.id -> T.ety) (call : A.call) : A.call = let rsubst x = x in - let type_params = List.map (ty_substitute rsubst tsubst) call.A.type_params in + let type_args = List.map (ty_substitute rsubst tsubst) call.A.type_args in let args = List.map (operand_substitute tsubst) call.A.args in let dest = place_substitute tsubst call.A.dest in (* Putting all the paramters on purpose: we want to get a compiler error if something moves - we may add a field on which we need to apply a substitution *) { func = call.A.func; - region_params = call.A.region_params; - A.type_params; + region_args = call.A.region_args; + A.type_args; args; dest; } diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index e8f37f1e..64b3929f 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -648,7 +648,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) : in (* Create the constructor *) let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in - let qualif = { id = qualif_id; type_params = type_args } in + let qualif = { id = qualif_id; type_args } in let cons_e = Qualif qualif in let field_tys = List.map (fun (v : texpression) -> v.ty) field_values @@ -1088,7 +1088,7 @@ and translate_return (config : config) (opt_v : V.typed_value option) and translate_function_call (config : config) (call : S.call) (e : S.expression) (ctx : bs_ctx) : texpression = (* Translate the function call *) - let type_params = List.map (ctx_translate_fwd_ty ctx) call.type_params in + let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in let args = List.map (typed_value_to_texpression ctx) call.args in let args_mplaces = List.map translate_opt_mplace call.args_places in let dest_mplace = translate_opt_mplace call.dest_place in @@ -1127,7 +1127,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression) (List.combine args args_mplaces) in let dest_v = mk_typed_pattern_from_var dest dest_mplace in - let func = { id = Func fun_id; type_params } in + let func = { id = Func fun_id; type_args } in let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in let ret_ty = mk_function_ret_ty config monadic state_monad dest_v.ty in let func_ty = mk_arrows input_tys ret_ty in @@ -1197,7 +1197,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) | V.FunCall -> let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in let call = call_info.forward in - let type_params = List.map (ctx_translate_fwd_ty ctx) call.type_params in + let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in (* Retrive the orignal call and the parent abstractions *) let forward, backwards = get_abs_ancestors ctx abs in (* Retrieve the values consumed when we called the forward function and @@ -1232,7 +1232,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) in let inst_sg = - get_instantiated_fun_sig fun_id (Some abs.back_id) type_params ctx + get_instantiated_fun_sig fun_id (Some abs.back_id) type_args ctx in List.iter (fun (x, ty) -> assert ((x : texpression).ty = ty)) @@ -1262,7 +1262,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in let ret_ty = mk_function_ret_ty config monadic state_monad output.ty in let func_ty = mk_arrows input_tys ret_ty in - let func = { id = Func func; type_params } in + let func = { id = Func func; type_args } in let func = { e = Qualif func; ty = func_ty } in let call = mk_apps func args in (* **Optimization**: @@ -1401,7 +1401,7 @@ and translate_expansion (config : config) (p : S.mplace option) * field. * We use the [dest] variable in order not to have to recompute * the type of the result of the projection... *) - let adt_id, type_params = + let adt_id, type_args = match scrutinee.ty with | Adt (adt_id, tys) -> (adt_id, tys) | _ -> raise (Failure "Unreachable") @@ -1409,7 +1409,7 @@ and translate_expansion (config : config) (p : S.mplace option) let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression = let proj_kind = { adt_id; field_id } in - let qualif = { id = Proj proj_kind; type_params } in + let qualif = { id = Proj proj_kind; type_args } in let proj_e = Qualif qualif in let proj_ty = mk_arrow scrutinee.ty dest.ty in let proj = { e = proj_e; ty = proj_ty } in |