diff options
| -rw-r--r-- | src/Contexts.ml | 11 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 11 | ||||
| -rw-r--r-- | src/FunsAnalysis.ml | 6 | ||||
| -rw-r--r-- | src/Interpreter.ml | 44 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 3 | ||||
| -rw-r--r-- | src/LlbcAst.ml | 21 | ||||
| -rw-r--r-- | src/LlbcOfJson.ml | 73 | ||||
| -rw-r--r-- | src/Modules.ml | 11 | ||||
| -rw-r--r-- | src/Names.ml | 2 | ||||
| -rw-r--r-- | src/Print.ml | 23 | ||||
| -rw-r--r-- | src/PrintPure.ml | 9 | ||||
| -rw-r--r-- | src/Pure.ml | 2 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 7 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 23 | ||||
| -rw-r--r-- | src/Translate.ml | 21 | ||||
| -rw-r--r-- | src/TranslateCore.ml | 17 |
16 files changed, 172 insertions, 112 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 1fbc916b..4f1e1506 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -219,13 +219,18 @@ type type_context = { type fun_context = { fun_decls : fun_decl FunDeclId.Map.t; - gid_conv : global_id_converter; +} +[@@deriving show] + +type global_context = { + global_decls : global_decl GlobalDeclId.Map.t; } [@@deriving show] type eval_ctx = { type_context : type_context; fun_context : fun_context; + global_context : global_context; type_vars : type_var list; env : env; ended_regions : RegionId.Set.t; @@ -260,8 +265,8 @@ let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl = FunDeclId.Map.find fid ctx.fun_context.fun_decls (** TODO: make this more efficient with maps *) -let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : fun_decl = - ctx_lookup_fun_decl ctx (global_to_fun_id ctx.fun_context.gid_conv gid) +let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl = + GlobalDeclId.Map.find gid ctx.global_context.global_decls (** Retrieve a variable's value in an environment *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 5b39b0b7..2c53e45b 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -907,9 +907,12 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | Func fun_id -> extract_function_call ctx fmt inside fun_id qualif.type_args args | Global global_id -> + failwith "TODO ExtractToFStar.ml:911" + (* Previous code: let fid = A.global_to_fun_id ctx.trans_ctx.fun_context.gid_conv global_id in let fun_id = Regular (A.Regular fid, None) in 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_args args | Proj proj -> @@ -1485,7 +1488,7 @@ let global_decl_to_body_name (decl : string) : string = assert (String.sub decl base_len 2 = "_c"); (String.sub decl 0 base_len) ^ "_body" -(** Print a definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *) +(** Extract a global definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *) let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (name : string) (ty : ty) (extract_body : (F.formatter -> unit) Option.t) @@ -1550,8 +1553,11 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (def : fun_decl) : unit = + (* TODO Lookup LLBC decl *) (* Sanity checks for globals *) - assert (def.is_global); + assert (def.is_global_body); + failwith "TODO ExtractToFStar.ml:1559" + (* Previous code: assert (Option.is_none def.back_id); assert (List.length def.signature.inputs = 0); assert (List.length def.signature.doutputs = 1); @@ -1578,6 +1584,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ("eval_global " ^ body_name) )); F.pp_print_break fmt 0 0 + *) (** Extract a unit test, if the function is a unit function (takes no parameters, returns unit). diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index b1b8ccc2..034575c0 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -61,7 +61,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) * (we check that it is successful in the extracted code: if it is * not, it leads to a type-checking error in the generated files) *) - if f.is_global then () else + if f.is_global_body then () else can_fail := !can_fail || b method! visit_Assert env a = @@ -98,7 +98,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) super#visit_Loop env loop end in - assert (not f.is_global || not use_state); + assert (not f.is_global_body || not use_state); (match f.body with | None -> (* Opaque function *) @@ -108,7 +108,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) (* We ignore on purpose functions that cannot 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. *) - can_fail := not f.is_global + can_fail := not f.is_global_body in List.iter visit_fun d; { can_fail = !can_fail; stateful = !stateful; divergent = !divergent } diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f4f01ff8..3610d486 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -14,9 +14,9 @@ module SA = SymbolicAst let log = L.interpreter_log let compute_type_fun_contexts (m : M.llbc_module) : - C.type_context * C.fun_context = + C.type_context * C.fun_context * C.global_context = let type_decls_list, _ = M.split_declarations m.declarations in - let type_decls, fun_decls = M.compute_defs_maps m in + let type_decls, fun_decls, global_decls = M.compute_defs_maps m in let type_decls_groups, _funs_defs_groups = M.split_declarations_to_group_maps m.declarations in @@ -24,15 +24,20 @@ let compute_type_fun_contexts (m : M.llbc_module) : TypesAnalysis.analyze_type_declarations type_decls type_decls_list in let type_context = { C.type_decls_groups; type_decls; type_infos } in - let fun_context = { C.fun_decls; gid_conv = m.gid_conv } in - (type_context, fun_context) - -let initialize_eval_context (type_context : C.type_context) - (fun_context : C.fun_context) (type_vars : T.type_var list) : C.eval_ctx = + let fun_context = { C.fun_decls } in + let global_context = { C.global_decls } in + (type_context, fun_context, global_context) + +let initialize_eval_context + (type_context : C.type_context) + (fun_context : C.fun_context) + (global_context : C.global_context) + (type_vars : T.type_var list) : C.eval_ctx = C.reset_global_counters (); { C.type_context; C.fun_context; + C.global_context; C.type_vars; C.env = [ C.Frame ]; C.ended_regions = T.RegionId.Set.empty; @@ -51,8 +56,11 @@ let initialize_eval_context (type_context : C.type_context) - the list of symbolic values introduced for the input values - the instantiated function signature *) -let initialize_symbolic_context_for_fun (type_context : C.type_context) - (fun_context : C.fun_context) (fdef : A.fun_decl) : +let initialize_symbolic_context_for_fun + (type_context : C.type_context) + (fun_context : C.fun_context) + (global_context : C.global_context) + (fdef : A.fun_decl) : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig = (* The abstractions are not initialized the same way as for function * calls: they contain *loan* projectors, because they "provide" us @@ -67,7 +75,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) * *) let sg = fdef.signature in (* Create the context *) - let ctx = initialize_eval_context type_context fun_context sg.type_params in + let ctx = initialize_eval_context type_context fun_context global_context sg.type_params in (* Instantiate the signature *) let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in let inst_sg = instantiate_fun_sig type_params sg in @@ -204,7 +212,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return - the symbolic AST generated by the symbolic execution *) let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) + (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) : V.symbolic_value list * SA.expression option = (* Debug *) @@ -218,7 +226,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) (* Create the evaluation context *) let ctx, input_svs, inst_sg = - initialize_symbolic_context_for_fun type_context fun_context fdef + initialize_symbolic_context_for_fun type_context fun_context global_context fdef in (* Create the continuation to finish the evaluation *) @@ -285,8 +293,8 @@ module Test = struct assert (body.A.arg_count = 0); (* Create the evaluation context *) - let type_context, fun_context = compute_type_fun_contexts m in - let ctx = initialize_eval_context type_context fun_context [] in + let type_context, fun_context, global_context = compute_type_fun_contexts m in + let ctx = initialize_eval_context type_context fun_context global_context [] in (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in @@ -330,7 +338,7 @@ module Test = struct (** Execute the symbolic interpreter on a function. *) let test_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) + (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) (fdef : A.fun_decl) : unit = (* Debug *) log#ldebug @@ -338,7 +346,7 @@ module Test = struct (* Evaluate *) let evaluate = - evaluate_function_symbolic config synthesize type_context fun_context fdef + evaluate_function_symbolic config synthesize type_context fun_context global_context fdef in (* Execute the forward function *) let _ = evaluate None in @@ -368,12 +376,12 @@ module Test = struct in (* Filter the opaque functions *) let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in - let type_context, fun_context = compute_type_fun_contexts m in + let type_context, fun_context, global_context = compute_type_fun_contexts m in let test_fun (def : A.fun_decl) : unit = (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) - test_function_symbolic config synthesize type_context fun_context def + test_function_symbolic config synthesize type_context fun_context global_context def in List.iter test_fun no_loop_funs end diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 8f981174..6a0b81f3 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -832,8 +832,9 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx | A.AssignGlobal { dst; global } -> + (* What codegen do we want ? *) let call : A.call = { - func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global); + func = A.Regular (failwith "TODO InterpretStatements.ml:837"); region_args = []; type_args = []; args = []; diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml index 16733e20..aa9b0665 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -7,17 +7,6 @@ open Identifiers module FunDeclId = IdGen () module GlobalDeclId = IdGen () -(* Strict type for the number of function declarations (see [global_to_fun_id] below) *) -type global_id_converter = { fun_count : int } -[@@deriving show] - -(** Converts a global id to its corresponding function id. - To do so, it adds the global id to the number of function declarations : - We have the bijection `global_id <=> fun_id + fun_id_count`. -*) -let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : FunDeclId.id = - FunDeclId.of_int ((GlobalDeclId.to_int gid) + conv.fun_count) - type var = { index : VarId.id; (** Unique variable identifier *) name : string option; @@ -201,6 +190,14 @@ type fun_decl = { name : fun_name; signature : fun_sig; body : fun_body option; - is_global : bool; + is_global_body : bool; +} +[@@deriving show] + +type global_decl = { + def_id : GlobalDeclId.id; + body_id: FunDeclId.id; + name : global_name; + ty: ety; } [@@deriving show] diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index c157b667..f51c15be 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -540,7 +540,7 @@ let call_of_json (js : json) : (A.call, string) result = Ok { A.func; region_args; type_args; args; dest } | _ -> Error "") -let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.statement, string) result = +let rec statement_of_json (js : json) : (A.statement, string) result = combine_error_msgs js "statement_of_json" (match js with | `Assoc [ ("Assign", `List [ place; rvalue ]) ] -> @@ -577,48 +577,49 @@ let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.st Ok (A.Continue i) | `String "Nop" -> Ok A.Nop | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] -> - let* st1 = statement_of_json st1 gid_conv in - let* st2 = statement_of_json st2 gid_conv in + let* st1 = statement_of_json st1 in + let* st2 = statement_of_json st2 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 gid_conv in + let* tgt = switch_targets_of_json tgt in Ok (A.Switch (op, tgt)) | `Assoc [ ("Loop", st) ] -> - let* st = statement_of_json st gid_conv in + let* st = statement_of_json st in Ok (A.Loop st) | _ -> Error "") -and switch_targets_of_json (js : json) (gid_conv : A.global_id_converter) : (A.switch_targets, string) result = +and switch_targets_of_json (js : json) : (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 gid_conv in - let* st2 = statement_of_json st2 gid_conv in + let* st1 = statement_of_json st1 in + let* st2 = statement_of_json st2 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 ( + pair_of_json (list_of_json scalar_value_of_json) - (fun js -> statement_of_json js gid_conv)) + statement_of_json) tgts in - let* otherwise = statement_of_json otherwise gid_conv in + let* otherwise = statement_of_json otherwise in Ok (A.SwitchInt (int_ty, tgts, otherwise)) | _ -> Error "") -let fun_body_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_body, string) result = +let fun_body_of_json (js : json) : (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 gid_conv in + let* body = statement_of_json body in Ok { A.arg_count; locals; body } | _ -> Error "") -let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result = +let fun_decl_of_json (js : json) : (A.fun_decl, string) result = combine_error_msgs js "fun_decl_of_json" (match js with | `Assoc @@ -631,13 +632,24 @@ let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_dec let* def_id = A.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 js -> fun_body_of_json js gid_conv) body in - Ok { A.def_id; name; signature; body; is_global = false; } + let* body = option_of_json fun_body_of_json body in + Ok { A.def_id; name; signature; body; is_global_body = false; } | _ -> Error "") +(* Strict type for the number of function declarations (see [global_to_fun_id] below) *) +type global_id_converter = { fun_count : int } +[@@deriving show] + +(** Converts a global id to its corresponding function id. + To do so, it adds the global id to the number of function declarations : + We have the bijection `global_id <=> fun_id + fun_id_count`. +*) +let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : A.FunDeclId.id = + A.FunDeclId.of_int ((A.GlobalDeclId.to_int gid) + conv.fun_count) + (* Converts a global declaration to a function declaration. *) -let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result = +let global_decl_of_json (js : json) (gid_conv : global_id_converter) : (A.global_decl * A.fun_decl, string) result = combine_error_msgs js "global_decl_of_json" (match js with | `Assoc @@ -648,10 +660,10 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_ ("body", body); ] -> let* global_id = A.GlobalDeclId.id_of_json def_id in - let def_id = A.global_to_fun_id gid_conv global_id in + let fun_id = global_to_fun_id gid_conv global_id in let* name = fun_name_of_json name in let* ty = ety_of_json ty in - let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in + let* body = option_of_json fun_body_of_json body in let signature : A.fun_sig = { region_params = []; num_early_bound_regions = 0; @@ -660,7 +672,8 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_ inputs = []; output = TU.ety_no_regions_to_sty ty; } in - Ok { A.def_id; name; signature; body; is_global = true; } + Ok ({ A.def_id = global_id; body_id = fun_id; name; ty; }, + { A.def_id = fun_id; name; signature; body; is_global_body = true; }) | _ -> Error "") let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) @@ -685,15 +698,18 @@ let fun_declaration_group_of_json (js : json) : combine_error_msgs js "fun_declaration_group_of_json" (g_declaration_group_of_json A.FunDeclId.id_of_json js) -let global_declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : +(* TODO Should a global declaration group be converted to its function bodies ? + It does not seems very clean. +*) +let global_declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.fun_declaration_group, string) result = combine_error_msgs js "global_declaration_group_of_json" (g_declaration_group_of_json (fun js -> let* id = A.GlobalDeclId.id_of_json js in - Ok (A.global_to_fun_id gid_conv id) + Ok (global_to_fun_id gid_conv id) ) js) -let declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.declaration_group, string) result +let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.declaration_group, string) result = combine_error_msgs js "declaration_of_json" (match js with @@ -726,19 +742,20 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("globals", globals); ] -> let* fun_count = length_of_json_list functions in - let gid_conv = { A.fun_count = fun_count } in + let gid_conv = { fun_count } in let* name = string_of_json name in let* declarations = list_of_json (fun js -> declaration_group_of_json js gid_conv) declarations in - let* types = list_of_json type_decl_of_json types in - let* functions = list_of_json (fun js -> fun_decl_of_json js gid_conv) functions in + let* types = list_of_json type_decl_of_json types in + let* functions = list_of_json fun_decl_of_json functions in let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in + let globals, global_bodies = List.split globals in Ok { M.name; declarations; types; - functions = functions @ globals; - gid_conv; + functions = functions @ global_bodies; + globals; } | _ -> Error "") diff --git a/src/Modules.ml b/src/Modules.ml index 149de020..2f640636 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -21,12 +21,12 @@ type llbc_module = { declarations : declaration_group list; types : type_decl list; functions : fun_decl list; - gid_conv : global_id_converter; + globals : global_decl list; } (** LLBC module - TODO: rename to crate *) let compute_defs_maps (m : llbc_module) : - type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t = + type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t = let types_map = List.fold_left (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m) @@ -37,7 +37,12 @@ let compute_defs_maps (m : llbc_module) : (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m) FunDeclId.Map.empty m.functions in - (types_map, funs_map) + let globals_map = + List.fold_left + (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m) + GlobalDeclId.Map.empty m.globals + in + (types_map, funs_map, globals_map) (** Split a module's declarations between types and functions *) let split_declarations (decls : declaration_group list) : diff --git a/src/Names.ml b/src/Names.ml index 1308eccc..0db5291a 100644 --- a/src/Names.ml +++ b/src/Names.ml @@ -54,6 +54,8 @@ type type_name = name [@@deriving show, ord] type fun_name = name [@@deriving show, ord] +type global_name = name [@@deriving show, ord] + (** Filter the disambiguators equal to 0 in a name *) let filter_disambiguators_zero (n : name) : name = let pred (pe : path_elem) : bool = diff --git a/src/Print.ml b/src/Print.ml index 337116ec..6b11a3ff 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -13,6 +13,7 @@ let option_to_string (to_string : 'a -> string) (x : 'a option) : string = let name_to_string (name : name) : string = Names.name_to_string name let fun_name_to_string (name : fun_name) : string = name_to_string name +let global_name_to_string (name : global_name) : string = name_to_string name (** Pretty-printing for types *) module Types = struct @@ -744,7 +745,8 @@ module LlbcAst = struct fun_name_to_string def.name in let global_decl_id_to_string def_id = - fun_decl_id_to_string (A.global_to_fun_id ctx.fun_context.gid_conv def_id) + let def = C.ctx_lookup_global_decl ctx def_id in + global_name_to_string def.name in { rvar_to_string = ctx_fmt.PV.rvar_to_string; @@ -762,7 +764,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) - (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (global_decls : A.global_decl A.GlobalDeclId.Map.t) (fdef : A.fun_decl) : ast_formatter = let rvar_to_string r = @@ -793,7 +795,8 @@ module LlbcAst = struct fun_name_to_string def.name in let global_decl_id_to_string def_id = - fun_decl_id_to_string (global_to_fun_id def_id) + let def = A.GlobalDeclId.Map.find def_id global_decls in + global_name_to_string def.name in { rvar_to_string; @@ -1132,7 +1135,7 @@ module Module = struct let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t) (fun_context : A.fun_decl A.FunDeclId.Map.t) - (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) : PA.ast_formatter = let rvar_to_string vid = @@ -1156,7 +1159,8 @@ module Module = struct fun_name_to_string def.name in let global_decl_id_to_string def_id = - fun_decl_id_to_string (global_to_fun_id def_id) + let def = A.GlobalDeclId.Map.find def_id global_context in + global_name_to_string def.name in let var_id_to_string vid = let var = V.VarId.nth (Option.get def.body).locals vid in @@ -1187,21 +1191,20 @@ module Module = struct let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t) (fun_context : A.fun_decl A.FunDeclId.Map.t) - (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) : string = - let fmt = def_ctx_to_ast_formatter type_context fun_context global_to_fun_id def in + let fmt = def_ctx_to_ast_formatter type_context fun_context global_context def in PA.fun_decl_to_string fmt "" " " def let module_to_string (m : M.llbc_module) : string = - let types_defs_map, funs_defs_map = M.compute_defs_maps m in + let types_defs_map, funs_defs_map, globals_defs_map = M.compute_defs_maps m in (* The types *) let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in (* The functions *) let fun_decls = - let gid_to_fid = fun gid -> A.global_to_fun_id m.gid_conv gid in - List.map (fun_decl_to_string types_defs_map funs_defs_map gid_to_fid) m.M.functions + List.map (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map) m.M.functions in (* Put everything together *) diff --git a/src/PrintPure.ml b/src/PrintPure.ml index c13f967f..597330bf 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -62,6 +62,7 @@ let ast_to_type_formatter (fmt : ast_formatter) : type_formatter = let name_to_string = Print.name_to_string let fun_name_to_string = Print.fun_name_to_string +let global_name_to_string = Print.global_name_to_string let option_to_string = Print.option_to_string let type_var_to_string = Print.Types.type_var_to_string let integer_type_to_string = Print.Types.integer_type_to_string @@ -85,9 +86,10 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t) functions (there is a difference between the forward/backward functions...) while we only need those definitions to lookup proper names for the def ids. *) -let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) +let mk_ast_formatter + (type_decls : T.type_decl TypeDeclId.Map.t) (fun_decls : A.fun_decl A.FunDeclId.Map.t) - (gid_conv : A.global_id_converter) + (global_decls : A.global_decl A.GlobalDeclId.Map.t) (type_params : type_var list) : ast_formatter = let type_var_id_to_string vid = @@ -116,7 +118,8 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) fun_name_to_string def.name in let global_decl_id_to_string def_id = - fun_decl_id_to_string (A.global_to_fun_id gid_conv def_id) + let def = A.GlobalDeclId.Map.find def_id global_decls in + global_name_to_string def.name in { type_var_id_to_string; diff --git a/src/Pure.ml b/src/Pure.ml index b3be2040..5244b0bc 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -575,6 +575,6 @@ type fun_decl = { (to identify the forward/backward functions) later. *) signature : fun_sig; - is_global : bool; + is_global_body : bool; body : fun_body option; } diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index e58fec2a..7a10bb6b 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -83,14 +83,15 @@ type formatter = { - function id: this is especially useful to identify whether the function is an assumed function or a local function - function basename + - flag indicating if the function is a global - number of region groups + - region group information in case of a backward function + (`None` if forward function) - pair: - do we generate the forward function (it may have been filtered)? - the number of extracted backward functions (not necessarily equal to the number of region groups, because we may have filtered some of them) - - region group information in case of a backward function - (`None` if forward function) TODO: use the fun id for the assumed functions. *) decreases_clause_name : A.FunDeclId.id -> fun_name -> string; @@ -599,7 +600,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let def_id = A.Regular def_id in let name = - ctx.fmt.fun_name def_id def.basename def.is_global num_rgs rg_info (keep_fwd, num_backs) + ctx.fmt.fun_name def_id def.basename def.is_global_body num_rgs rg_info (keep_fwd, num_backs) in (* Add the function name *) let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index a057b015..7d9e2906 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -70,7 +70,10 @@ type fun_context = { llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_sigs : fun_sig_named_outputs RegularFunIdMap.t; (** *) fun_infos : FA.fun_info A.FunDeclId.Map.t; - gid_conv : A.global_id_converter; +} + +type global_context = { + llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t; } type call_info = { @@ -96,6 +99,7 @@ type call_info = { type bs_ctx = { type_context : type_context; fun_context : fun_context; + global_context : global_context; fun_decl : A.fun_decl; bid : T.RegionGroupId.id option; (** TODO: rename *) sg : fun_sig; @@ -137,15 +141,15 @@ let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.LlbcAst.ast_formatter = Print.LlbcAst.fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls ctx.fun_context.llbc_fun_decls - (A.global_to_fun_id ctx.fun_context.gid_conv) + ctx.global_context.llbc_global_decls ctx.fun_decl let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter = let type_params = ctx.fun_decl.signature.type_params in let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls in - let gid_conv = ctx.fun_context.gid_conv in - PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params + let global_decls = ctx.global_context.llbc_global_decls in + PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params let ty_to_string (ctx : bs_ctx) (ty : ty) : string = let fmt = bs_ctx_to_pp_ast_formatter ctx in @@ -166,16 +170,16 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string = let type_params = sg.type_params in let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls in - let gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.llbc_global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in PrintPure.fun_sig_to_string fmt sg let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = let type_params = def.signature.type_params in let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls in - let gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.llbc_global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in PrintPure.fun_decl_to_string fmt def (* TODO: move *) @@ -1666,7 +1670,6 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) (* Lookup the signature *) let signature = bs_ctx_lookup_local_function_sig def_id bid ctx in (* Translate the body, if there is *) - let is_global = def.A.is_global in let body = match body with | None -> None @@ -1727,7 +1730,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) Some { inputs; inputs_lvs; body } in (* Assemble the declaration *) - let def = { def_id; back_id = bid; basename; signature; is_global; body } in + let def = { def_id; back_id = bid; basename; signature; is_global_body = def.is_global_body; body } in (* Debugging *) log#ldebug (lazy diff --git a/src/Translate.ml b/src/Translate.ml index 9412b8b8..a6477e7f 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -63,10 +63,9 @@ let translate_function_to_symbolics (config : C.partial_config) ("translate_function_to_symbolics: " ^ Print.fun_name_to_string fdef.A.name)); - let { type_context; fun_context } = trans_ctx in + let { type_context; fun_context; global_context } = trans_ctx in let fun_context = { C.fun_decls = fun_context.fun_decls; - C.gid_conv = fun_context.gid_conv; } in match fdef.body with @@ -76,7 +75,8 @@ let translate_function_to_symbolics (config : C.partial_config) let synthesize = true in let evaluate gid = let inputs, symb = - evaluate_function_symbolic config synthesize type_context fun_context + evaluate_function_symbolic config synthesize + type_context fun_context global_context fdef gid in (inputs, Option.get symb) @@ -110,7 +110,7 @@ let translate_function_to_pure (config : C.partial_config) (lazy ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name)); - let { type_context; fun_context } = trans_ctx in + let { type_context; fun_context; global_context } = trans_ctx in let def_id = fdef.def_id in (* Compute the symbolic ASTs, if the function is transparent *) @@ -142,7 +142,10 @@ let translate_function_to_pure (config : C.partial_config) SymbolicToPure.llbc_fun_decls = fun_context.fun_decls; fun_sigs; fun_infos = fun_context.fun_infos; - gid_conv = fun_context.gid_conv; + } + in + let global_context = { + SymbolicToPure.llbc_global_decls = global_context.global_decls } in let ctx = @@ -156,6 +159,7 @@ let translate_function_to_pure (config : C.partial_config) state_var; type_context; fun_context; + global_context; fun_decl = fdef; forward_inputs = []; (* Empty for now *) @@ -293,14 +297,13 @@ let translate_module_to_pure (config : C.partial_config) log#ldebug (lazy "translate_module_to_pure"); (* Compute the type and function contexts *) - let type_context, fun_context = compute_type_fun_contexts m in + let type_context, fun_context, global_context = compute_type_fun_contexts m in let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in let fun_context = { fun_decls = fun_context.fun_decls; fun_infos; - gid_conv = m.gid_conv; } in - let trans_ctx = { type_context; fun_context } in + let trans_ctx = { type_context; fun_context; global_context } in (* Translate all the type definitions *) let type_decls = SymbolicToPure.translate_type_decls m.types in @@ -495,7 +498,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) - then if def.is_global + then if def.is_global_body then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def ) diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 047219ad..e77445cd 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -16,11 +16,16 @@ 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; - gid_conv : A.global_id_converter; } [@@deriving show] -type trans_ctx = { type_context : type_context; fun_context : fun_context } +type global_context = C.global_context [@@deriving show] + +type trans_ctx = { + type_context : type_context; + fun_context : fun_context; + global_context : global_context +} type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list @@ -40,16 +45,16 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = let type_params = sg.type_params in let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in - let gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in PrintPure.fun_sig_to_string fmt sg let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let type_params = def.signature.type_params in let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in - let gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in PrintPure.fun_decl_to_string fmt def let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string = |