diff options
author | Sidney Congard | 2022-06-08 12:32:14 +0200 |
---|---|---|
committer | Sidney Congard | 2022-06-08 12:32:14 +0200 |
commit | ba61ed50e7b2fdc78690de92d734a3747029f903 (patch) | |
tree | d038735ea4a263f80e1752661c1c707d21810f28 /src | |
parent | 1b3f5a15aaabf5810f07797550d1a19a55b6be3c (diff) |
read globals from LLBC JSON into functions
Diffstat (limited to 'src')
-rw-r--r-- | src/Contexts.ml | 1 | ||||
-rw-r--r-- | src/Expressions.ml | 2 | ||||
-rw-r--r-- | src/ExtractToFStar.ml | 1 | ||||
-rw-r--r-- | src/FunIdentifier.ml | 2 | ||||
-rw-r--r-- | src/FunsAnalysis.ml | 1 | ||||
-rw-r--r-- | src/Interpreter.ml | 5 | ||||
-rw-r--r-- | src/InterpreterStatements.ml | 7 | ||||
-rw-r--r-- | src/LlbcAst.ml | 5 | ||||
-rw-r--r-- | src/LlbcAstUtils.ml | 1 | ||||
-rw-r--r-- | src/LlbcOfJson.ml | 146 | ||||
-rw-r--r-- | src/Modules.ml | 1 | ||||
-rw-r--r-- | src/Print.ml | 13 | ||||
-rw-r--r-- | src/PrintPure.ml | 6 | ||||
-rw-r--r-- | src/PrintSymbolicAst.ml | 3 | ||||
-rw-r--r-- | src/Pure.ml | 2 | ||||
-rw-r--r-- | src/PureToExtract.ml | 1 | ||||
-rw-r--r-- | src/SymbolicToPure.ml | 1 | ||||
-rw-r--r-- | src/Translate.ml | 21 | ||||
-rw-r--r-- | src/TranslateCore.ml | 9 | ||||
-rw-r--r-- | src/TypesUtils.ml | 13 |
20 files changed, 161 insertions, 80 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index a4551420..bbf5b8f3 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -1,6 +1,7 @@ open Types open Values open LlbcAst +open FunIdentifier module V = Values open ValuesUtils module M = Modules diff --git a/src/Expressions.ml b/src/Expressions.ml index 6bf14c66..f1a4a8c3 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -1,5 +1,6 @@ open Types open Values +open FunIdentifier type field_proj_kind = | ProjAdt of TypeDeclId.id * VariantId.id option @@ -88,6 +89,7 @@ let all_binops = *) type operand_constant_value = | ConstantValue of constant_value + | ConstantId of FunDeclId.id | ConstantAdt of VariantId.id option * operand_constant_value list [@@deriving show] diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 0bbe591e..9766ddaf 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -6,6 +6,7 @@ open PureUtils open TranslateCore open PureToExtract open StringUtils +open FunIdentifier module F = Format (** A qualifier for a type definition. diff --git a/src/FunIdentifier.ml b/src/FunIdentifier.ml new file mode 100644 index 00000000..dd7e9318 --- /dev/null +++ b/src/FunIdentifier.ml @@ -0,0 +1,2 @@ +open Identifiers +module FunDeclId = IdGen () diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index dc205eb9..cf2e0bd6 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -9,6 +9,7 @@ open LlbcAst open Modules +open FunIdentifier type fun_info = { can_fail : bool; diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f6ae268d..702aeea6 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,4 +1,5 @@ open Cps +open FunIdentifier open InterpreterUtils open InterpreterProjectors open InterpreterBorrows @@ -255,9 +256,9 @@ module Test = struct environment. *) let test_unit_function (config : C.partial_config) (m : M.llbc_module) - (fid : A.FunDeclId.id) : unit = + (fid : FunDeclId.id) : unit = (* Retrieve the function declaration *) - let fdef = A.FunDeclId.nth m.functions fid in + let fdef = FunDeclId.nth m.functions fid in let body = Option.get fdef.body in (* Debug *) diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 1083d643..c7308720 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -7,6 +7,7 @@ module A = LlbcAst module L = Logging open TypesUtils open ValuesUtils +open FunIdentifier module Inv = Invariants module S = SynthesizeSymbolic open Errors @@ -1001,7 +1002,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = 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) +and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.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 -> @@ -1079,7 +1080,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) cc cf ctx (** 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) +and eval_local_function_call_symbolic (config : C.config) (fid : FunDeclId.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 -> @@ -1300,7 +1301,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) (** 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) +and eval_local_function_call (config : C.config) (fid : FunDeclId.id) (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 diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml index d35cd5d8..4324586d 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -1,10 +1,8 @@ -open Identifiers open Names open Types open Values open Expressions - -module FunDeclId = IdGen () +open FunIdentifier type var = { index : VarId.id; (** Unique variable identifier *) @@ -178,5 +176,6 @@ type fun_decl = { name : fun_name; signature : fun_sig; body : fun_body option; + is_global : bool; } [@@deriving show] diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml index 84e8e00f..bc4236cf 100644 --- a/src/LlbcAstUtils.ml +++ b/src/LlbcAstUtils.ml @@ -1,5 +1,6 @@ open LlbcAst open Utils +open FunIdentifier module T = Types (** Check if a [statement] contains loops *) diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 99d652ec..14333088 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -11,12 +11,14 @@ open Yojson.Basic open Names open OfJsonBasic +open FunIdentifier module T = Types module V = Values module S = Scalars module M = Modules module E = Expressions module A = LlbcAst +module TU = TypesUtils (* The default logger *) let log = Logging.llbc_of_json_logger @@ -225,6 +227,14 @@ let type_decl_of_json (js : json) : (T.type_decl, string) result = } | _ -> Error "") +(* Converts a global ID to its corresponding function ID. + To do so, it adds the global ID to the number of function declarations. +*) +let global_id_of_json (js: json) (fun_count: int) : (FunDeclId.id, string) result = + combine_error_msgs js "global_id_of_json" + (let* gid = FunDeclId.id_of_json js in + Ok (FunDeclId.of_int ((FunDeclId.to_int gid) + fun_count))) + let var_of_json (js : json) : (A.var, string) result = combine_error_msgs js "var_of_json" (match js with @@ -393,7 +403,7 @@ let binop_of_json (js : json) : (E.binop, string) result = | `String "Shr" -> Ok E.Shr | _ -> Error ("binop_of_json failed on:" ^ show js) -let rec operand_constant_value_of_json (js : json) : +let rec operand_constant_value_of_json (js : json) (fun_count : int) : (E.operand_constant_value, string) result = combine_error_msgs js "operand_constant_value_of_json" (match js with @@ -403,12 +413,15 @@ let rec operand_constant_value_of_json (js : json) : | `Assoc [ ("ConstantAdt", `List [ variant_id; field_values ]) ] -> let* variant_id = option_of_json T.VariantId.id_of_json variant_id in let* field_values = - list_of_json operand_constant_value_of_json field_values + list_of_json (fun js -> operand_constant_value_of_json js fun_count) field_values in Ok (E.ConstantAdt (variant_id, field_values)) + | `Assoc [ ("ConstantIdentifier", `List [gid]) ] -> + let* id = global_id_of_json gid fun_count in + Ok (E.ConstantId id) | _ -> Error "") -let operand_of_json (js : json) : (E.operand, string) result = +let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result = combine_error_msgs js "operand_of_json" (match js with | `Assoc [ ("Copy", place) ] -> @@ -417,9 +430,9 @@ let operand_of_json (js : json) : (E.operand, string) result = | `Assoc [ ("Move", place) ] -> let* place = place_of_json place in Ok (E.Move place) - | `Assoc [ ("Constant", `List [ ty; cv ]) ] -> + | `Assoc [ ("Const", `List [ ty; cv ]) ] -> let* ty = ety_of_json ty in - let* cv = operand_constant_value_of_json cv in + let* cv = operand_constant_value_of_json cv fun_count in Ok (E.Constant (ty, cv)) | _ -> Error "") @@ -442,11 +455,11 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result = Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys)) | _ -> Error "") -let rvalue_of_json (js : json) : (E.rvalue, string) result = +let rvalue_of_json (js : json) (fun_count : int) : (E.rvalue, string) result = combine_error_msgs js "rvalue_of_json" (match js with | `Assoc [ ("Use", op) ] -> - let* op = operand_of_json op in + let* op = operand_of_json op fun_count in Ok (E.Use op) | `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] -> let* place = place_of_json place in @@ -454,19 +467,19 @@ let rvalue_of_json (js : json) : (E.rvalue, string) result = Ok (E.Ref (place, borrow_kind)) | `Assoc [ ("UnaryOp", `List [ unop; op ]) ] -> let* unop = unop_of_json unop in - let* op = operand_of_json op in + let* op = operand_of_json op fun_count in Ok (E.UnaryOp (unop, op)) | `Assoc [ ("BinaryOp", `List [ binop; op1; op2 ]) ] -> let* binop = binop_of_json binop in - let* op1 = operand_of_json op1 in - let* op2 = operand_of_json op2 in + let* op1 = operand_of_json op1 fun_count in + let* op2 = operand_of_json op2 fun_count in Ok (E.BinaryOp (binop, op1, op2)) | `Assoc [ ("Discriminant", place) ] -> let* place = place_of_json place in Ok (E.Discriminant place) | `Assoc [ ("Aggregate", `List [ aggregate_kind; ops ]) ] -> let* aggregate_kind = aggregate_kind_of_json aggregate_kind in - let* ops = list_of_json operand_of_json ops in + let* ops = list_of_json (fun js -> operand_of_json js fun_count) ops in Ok (E.Aggregate (aggregate_kind, ops)) | _ -> Error "") @@ -489,18 +502,18 @@ let fun_id_of_json (js : json) : (A.fun_id, string) result = combine_error_msgs js "fun_id_of_json" (match js with | `Assoc [ ("Regular", id) ] -> - let* id = A.FunDeclId.id_of_json id in + let* id = FunDeclId.id_of_json id in Ok (A.Regular id) | `Assoc [ ("Assumed", fid) ] -> let* fid = assumed_fun_id_of_json fid in Ok (A.Assumed fid) | _ -> Error "") -let assertion_of_json (js : json) : (A.assertion, string) result = +let assertion_of_json (js : json) (fun_count : int) : (A.assertion, string) result = combine_error_msgs js "assertion_of_json" (match js with | `Assoc [ ("cond", cond); ("expected", expected) ] -> - let* cond = operand_of_json cond in + let* cond = operand_of_json cond fun_count in let* expected = bool_of_json expected in Ok { A.cond; expected } | _ -> Error "") @@ -534,7 +547,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result = } | _ -> Error "") -let call_of_json (js : json) : (A.call, string) result = +let call_of_json (js : json) (fun_count : int) : (A.call, string) result = combine_error_msgs js "call_of_json" (match js with | `Assoc @@ -548,17 +561,17 @@ let call_of_json (js : json) : (A.call, string) result = let* func = fun_id_of_json func 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* args = list_of_json (fun js -> operand_of_json js fun_count) args in let* dest = place_of_json dest in Ok { A.func; region_args; type_args; args; dest } | _ -> Error "") -let rec statement_of_json (js : json) : (A.statement, string) result = +let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string) result = combine_error_msgs js "statement_of_json" (match js with | `Assoc [ ("Assign", `List [ place; rvalue ]) ] -> let* place = place_of_json place in - let* rvalue = rvalue_of_json rvalue in + let* rvalue = rvalue_of_json rvalue fun_count in Ok (A.Assign (place, rvalue)) | `Assoc [ ("FakeRead", place) ] -> let* place = place_of_json place in @@ -571,10 +584,10 @@ let rec statement_of_json (js : json) : (A.statement, string) result = let* place = place_of_json place in Ok (A.Drop place) | `Assoc [ ("Assert", assertion) ] -> - let* assertion = assertion_of_json assertion in + let* assertion = assertion_of_json assertion fun_count in Ok (A.Assert assertion) | `Assoc [ ("Call", call) ] -> - let* call = call_of_json call in + let* call = call_of_json call fun_count in Ok (A.Call call) | `String "Panic" -> Ok A.Panic | `String "Return" -> Ok A.Return @@ -586,47 +599,48 @@ let rec statement_of_json (js : json) : (A.statement, string) result = Ok (A.Continue i) | `String "Nop" -> Ok A.Nop | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] -> - let* st1 = statement_of_json st1 in - let* st2 = statement_of_json st2 in + let* st1 = statement_of_json st1 fun_count in + let* st2 = statement_of_json st2 fun_count in Ok (A.Sequence (st1, st2)) | `Assoc [ ("Switch", `List [ op; tgt ]) ] -> - let* op = operand_of_json op in - let* tgt = switch_targets_of_json tgt in + let* op = operand_of_json op fun_count in + let* tgt = switch_targets_of_json tgt fun_count in Ok (A.Switch (op, tgt)) | `Assoc [ ("Loop", st) ] -> - let* st = statement_of_json st in + let* st = statement_of_json st fun_count in Ok (A.Loop st) | _ -> Error "") -and switch_targets_of_json (js : json) : (A.switch_targets, string) result = +and switch_targets_of_json (js : json) (fun_count : int) : (A.switch_targets, string) result = combine_error_msgs js "switch_targets_of_json" (match js with | `Assoc [ ("If", `List [ st1; st2 ]) ] -> - let* st1 = statement_of_json st1 in - let* st2 = statement_of_json st2 in + let* st1 = statement_of_json st1 fun_count in + let* st2 = statement_of_json st2 fun_count in Ok (A.If (st1, st2)) | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] -> let* int_ty = integer_type_of_json int_ty in let* tgts = - list_of_json - (pair_of_json (list_of_json scalar_value_of_json) statement_of_json) + list_of_json (pair_of_json + (list_of_json scalar_value_of_json) + (fun js -> statement_of_json js fun_count)) tgts in - let* otherwise = statement_of_json otherwise in + let* otherwise = statement_of_json otherwise fun_count in Ok (A.SwitchInt (int_ty, tgts, otherwise)) | _ -> Error "") -let fun_body_of_json (js : json) : (A.fun_body, string) result = +let fun_body_of_json (js : json) (fun_count : int) : (A.fun_body, string) result = combine_error_msgs js "fun_body_of_json" (match js with | `Assoc [ ("arg_count", arg_count); ("locals", locals); ("body", body) ] -> let* arg_count = int_of_json arg_count in let* locals = list_of_json var_of_json locals in - let* body = statement_of_json body in + let* body = statement_of_json body fun_count in Ok { A.arg_count; locals; body } | _ -> Error "") -let fun_decl_of_json (js : json) : (A.fun_decl, string) result = +let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result = combine_error_msgs js "fun_decl_of_json" (match js with | `Assoc @@ -636,11 +650,42 @@ let fun_decl_of_json (js : json) : (A.fun_decl, string) result = ("signature", signature); ("body", body); ] -> - let* def_id = A.FunDeclId.id_of_json def_id in + let* def_id = FunDeclId.id_of_json def_id in let* name = fun_name_of_json name in let* signature = fun_sig_of_json signature in - let* body = option_of_json fun_body_of_json body in - Ok { A.def_id; name; signature; body } + let* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in + Ok { A.def_id; name; signature; body; is_global = false; } + | _ -> Error "") + + +(* Converts a global declaration to a function declaration. + +A.fun_sig +ety_no_regions_to_rty +*) +let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) result = + combine_error_msgs js "global_decl_of_json" + (match js with + | `Assoc + [ + ("def_id", def_id); + ("name", name); + ("type_", type_); + ("body", body); + ] -> + let* def_id = global_id_of_json def_id fun_count in + let* name = fun_name_of_json name in + let* type_ = ety_of_json type_ in + let* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in + let signature : A.fun_sig = { + region_params = []; + num_early_bound_regions = 0; + regions_hierarchy = []; + type_params = []; + inputs = []; + output = TU.ety_no_regions_to_sty type_; + } in + Ok { A.def_id; name; signature; body; is_global = true; } | _ -> Error "") let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) @@ -663,9 +708,14 @@ let type_declaration_group_of_json (js : json) : let fun_declaration_group_of_json (js : json) : (M.fun_declaration_group, string) result = combine_error_msgs js "fun_declaration_group_of_json" - (g_declaration_group_of_json A.FunDeclId.id_of_json js) + (g_declaration_group_of_json FunDeclId.id_of_json js) + +let global_declaration_group_of_json (js : json) (fun_count: int) : + (M.fun_declaration_group, string) result = + combine_error_msgs js "global_declaration_group_of_json" + (g_declaration_group_of_json (fun js -> global_id_of_json js fun_count) js) -let declaration_group_of_json (js : json) : (M.declaration_group, string) result +let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_group, string) result = combine_error_msgs js "declaration_of_json" (match js with @@ -675,8 +725,17 @@ let declaration_group_of_json (js : json) : (M.declaration_group, string) result | `Assoc [ ("Fun", `List [ decl ]) ] -> let* decl = fun_declaration_group_of_json decl in Ok (M.Fun decl) + | `Assoc [ ("Global", `List [ decl ]) ] -> + let* decl = global_declaration_group_of_json decl fun_count in + Ok (M.Fun decl) | _ -> Error "") +let length_of_json_list (js: json) : (int, string) result = + combine_error_msgs js "get_json_list_len" + (match js with + | `List jsl -> Ok (List.length jsl) + | _ -> Error ("not a list: " ^ show js)) + let llbc_module_of_json (js : json) : (M.llbc_module, string) result = combine_error_msgs js "llbc_module_of_json" (match js with @@ -686,12 +745,15 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("declarations", declarations); ("types", types); ("functions", functions); + ("globals", globals); ] -> + let* fun_count = length_of_json_list functions in let* name = string_of_json name in let* declarations = - list_of_json declaration_group_of_json declarations + list_of_json (fun js -> declaration_group_of_json js fun_count) declarations in let* types = list_of_json type_decl_of_json types in - let* functions = list_of_json fun_decl_of_json functions in - Ok { M.name; declarations; types; functions } + let* functions = list_of_json (fun js -> fun_decl_of_json js fun_count) functions in + let* globals = list_of_json (fun js -> global_decl_of_json js fun_count) globals in + Ok { M.name; declarations; types; functions = functions @ globals } | _ -> Error "") diff --git a/src/Modules.ml b/src/Modules.ml index f52983c6..6d0cf70c 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -1,5 +1,6 @@ open Types open LlbcAst +open FunIdentifier type 'id g_declaration_group = NonRec of 'id | Rec of 'id list [@@deriving show] diff --git a/src/Print.ml b/src/Print.ml index 8e29bc67..28040181 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -1,4 +1,5 @@ open Names +open FunIdentifier module T = Types module TU = TypesUtils module V = Values @@ -685,7 +686,7 @@ module LlbcAst = struct var_id_to_string : V.VarId.id -> string; adt_field_names : T.TypeDeclId.id -> T.VariantId.id option -> string list option; - fun_decl_id_to_string : A.FunDeclId.id -> string; + fun_decl_id_to_string : FunDeclId.id -> string; } let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter = @@ -755,7 +756,7 @@ module LlbcAst = struct } let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t) - (fun_decls : A.fun_decl A.FunDeclId.Map.t) (fdef : A.fun_decl) : + (fun_decls : A.fun_decl FunDeclId.Map.t) (fdef : A.fun_decl) : ast_formatter = let rvar_to_string r = let rvar = T.RegionVarId.nth fdef.signature.region_params r in @@ -781,7 +782,7 @@ module LlbcAst = struct let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in let fun_decl_id_to_string def_id = - let def = A.FunDeclId.Map.find def_id fun_decls in + let def = FunDeclId.Map.find def_id fun_decls in fun_name_to_string def.name in { @@ -1138,7 +1139,7 @@ module Module = struct (** Generate an [ast_formatter] by using a definition context in combination with the variables local to a function's definition *) let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t) - (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) : + (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) : PA.ast_formatter = let rvar_to_string vid = let var = T.RegionVarId.nth def.signature.region_params vid in @@ -1157,7 +1158,7 @@ module Module = struct name_to_string def.name in let fun_decl_id_to_string def_id = - let def = A.FunDeclId.Map.find def_id fun_context in + let def = FunDeclId.Map.find def_id fun_context in fun_name_to_string def.name in let var_id_to_string vid = @@ -1186,7 +1187,7 @@ module Module = struct (** This function pretty-prints a function definition by using a definition context *) let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t) - (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) : string = + (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) : string = let fmt = def_ctx_to_ast_formatter type_context fun_context def in PA.fun_decl_to_string fmt "" " " def diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 5e817dde..8864dafe 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -2,6 +2,7 @@ open Pure open PureUtils +open FunIdentifier module T = Types module V = Values module E = Expressions @@ -12,7 +13,6 @@ module RegionId = T.RegionId module VariantId = T.VariantId module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId -module FunDeclId = A.FunDeclId type type_formatter = { type_var_id_to_string : TypeVarId.id -> string; @@ -44,7 +44,7 @@ type ast_formatter = { adt_field_to_string : TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option; adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option; - fun_decl_id_to_string : A.FunDeclId.id -> string; + fun_decl_id_to_string : FunDeclId.id -> string; } let ast_to_value_formatter (fmt : ast_formatter) : value_formatter = @@ -110,7 +110,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) Print.LlbcAst.type_ctx_to_adt_field_to_string_fun type_decls in let fun_decl_id_to_string def_id = - let def = A.FunDeclId.Map.find def_id fun_decls in + let def = FunDeclId.Map.find def_id fun_decls in fun_name_to_string def.name in { diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml index 0ab68efc..e44b422a 100644 --- a/src/PrintSymbolicAst.ml +++ b/src/PrintSymbolicAst.ml @@ -7,6 +7,7 @@ open Errors open Identifiers +open FunIdentifier module T = Types module TU = TypesUtils module V = Values @@ -20,7 +21,7 @@ module PT = Print.Types type formatting_ctx = { type_context : C.type_context; - fun_context : A.fun_decl A.FunDeclId.Map.t; + fun_context : A.fun_decl FunDeclId.Map.t; type_vars : T.type_var list; } diff --git a/src/Pure.ml b/src/Pure.ml index 5834b87f..05f78e35 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -1,5 +1,6 @@ open Identifiers open Names +open FunIdentifier module T = Types module V = Values module E = Expressions @@ -10,7 +11,6 @@ module RegionGroupId = T.RegionGroupId module VariantId = T.VariantId module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId -module FunDeclId = A.FunDeclId module SynthPhaseId = IdGen () (** We give an identifier to every phase of the synthesis (forward, backward diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 1c530011..55a8853a 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -6,6 +6,7 @@ open Pure open TranslateCore +open FunIdentifier module C = Contexts module RegionVarId = T.RegionVarId module F = Format diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 42479a6e..2b416cc1 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -2,6 +2,7 @@ open Errors open LlbcAstUtils open Pure open PureUtils +open FunIdentifier module Id = Identifiers module M = Modules module S = SymbolicAst diff --git a/src/Translate.ml b/src/Translate.ml index 57b92e44..1577753c 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -1,5 +1,6 @@ open InterpreterStatements open Interpreter +open FunIdentifier module L = Logging module T = Types module A = LlbcAst @@ -351,8 +352,8 @@ type gen_ctx = { m : M.llbc_module; extract_ctx : PureToExtract.extraction_ctx; trans_types : Pure.type_decl Pure.TypeDeclId.Map.t; - trans_funs : (bool * pure_fun_translation) Pure.FunDeclId.Map.t; - functions_with_decreases_clause : Pure.FunDeclId.Set.t; + trans_funs : (bool * pure_fun_translation) FunDeclId.Map.t; + functions_with_decreases_clause : FunDeclId.Set.t; } (** Extraction context *) @@ -388,7 +389,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool = ctx.trans_types in let has_opaque_funs = - Pure.FunDeclId.Map.exists + FunDeclId.Map.exists (fun _ ((_, (t_fwd, _)) : bool * pure_fun_translation) -> Option.is_none t_fwd.body) ctx.trans_funs @@ -427,7 +428,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) (* Utility to check a function has a decrease clause *) let has_decreases_clause (def : Pure.fun_decl) : bool = - Pure.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause + FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause in (* In case of (non-mutually) recursive functions, we use a simple procedure to @@ -523,14 +524,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) ids | Fun (NonRec id) -> (* Lookup *) - let pure_fun = Pure.FunDeclId.Map.find id ctx.trans_funs in + let pure_fun = FunDeclId.Map.find id ctx.trans_funs in (* Translate *) export_functions false [ pure_fun ] | Fun (Rec ids) -> (* General case of mutually recursive functions *) (* Lookup *) let pure_funs = - List.map (fun id -> Pure.FunDeclId.Map.find id ctx.trans_funs) ids + List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids in (* Translate *) export_functions true pure_funs @@ -622,7 +623,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* We need to compute which functions are recursive, in order to know * whether we should generate a decrease clause or not. *) let rec_functions = - Pure.FunDeclId.Set.of_list + FunDeclId.Set.of_list (List.concat (List.map (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> []) @@ -644,7 +645,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (fun ctx (keep_fwd, def) -> (* Note that we generate a decrease clause for all the recursive functions *) let gen_decr_clause = - Pure.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions + FunDeclId.Set.mem (fst def).Pure.def_id rec_functions in ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause def) @@ -674,7 +675,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types) in let trans_funs = - Pure.FunDeclId.Map.of_list + FunDeclId.Map.of_list (List.map (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) -> (fd.def_id, (keep_fwd, (fd, bdl)))) @@ -761,7 +762,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* Extract the template clauses *) let needs_clauses_module = config.extract_decreases_clauses - && not (Pure.FunDeclId.Set.is_empty rec_functions) + && not (FunDeclId.Set.is_empty rec_functions) in (if needs_clauses_module && config.extract_template_decreases_clauses then let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 17c35cbf..3d3887ce 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -1,6 +1,7 @@ (** Some utilities for the translation *) open InterpreterStatements +open FunIdentifier module L = Logging module T = Types module A = LlbcAst @@ -14,8 +15,8 @@ let log = L.translate_log type type_context = C.type_context [@@deriving show] type fun_context = { - fun_decls : A.fun_decl A.FunDeclId.Map.t; - fun_infos : FA.fun_info A.FunDeclId.Map.t; + fun_decls : A.fun_decl FunDeclId.Map.t; + fun_infos : FA.fun_info FunDeclId.Map.t; } [@@deriving show] @@ -49,6 +50,6 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in PrintPure.fun_decl_to_string fmt def -let fun_decl_id_to_string (ctx : trans_ctx) (id : Pure.FunDeclId.id) : string = +let fun_decl_id_to_string (ctx : trans_ctx) (id : FunDeclId.id) : string = Print.fun_name_to_string - (Pure.FunDeclId.Map.find id ctx.fun_context.fun_decls).name + (FunDeclId.Map.find id ctx.fun_context.fun_decls).name diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index bee7956e..8d0624ee 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -100,28 +100,31 @@ let rty_regions_intersect (ty : rty) (regions : RegionId.Set.t) : bool = let ty_regions = rty_regions ty in not (RegionId.Set.disjoint ty_regions regions) -(** Convert an [ety], containing no region variables, to an [rty]. +(** Convert an [ety], containing no region variables, to an [rty] or [sty]. In practice, it is the identity. *) -let rec ety_no_regions_to_rty (ty : ety) : rty = +let rec ety_no_regions_to_gr_ty (ty : ety) : 'a gr_ty = match ty with | Adt (type_id, regions, tys) -> assert (regions = []); - Adt (type_id, [], List.map ety_no_regions_to_rty tys) + Adt (type_id, [], List.map ety_no_regions_to_gr_ty tys) | TypeVar v -> TypeVar v | Bool -> Bool | Char -> Char | Never -> Never | Integer int_ty -> Integer int_ty | Str -> Str - | Array ty -> Array (ety_no_regions_to_rty ty) - | Slice ty -> Slice (ety_no_regions_to_rty ty) + | Array ty -> Array (ety_no_regions_to_gr_ty ty) + | Slice ty -> Slice (ety_no_regions_to_gr_ty ty) | Ref (_, _, _) -> failwith "Can't convert a ref with erased regions to a ref with non-erased \ regions" +let ety_no_regions_to_rty (ty : ety) : rty = ety_no_regions_to_gr_ty ty +let ety_no_regions_to_sty (ty : ety) : sty = ety_no_regions_to_gr_ty ty + (** Retuns true if the type contains borrows. Note that we can't simply explore the type and look for regions: sometimes |