diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ExtractToFStar.ml | 6 | ||||
| -rw-r--r-- | src/FunsAnalysis.ml | 10 | ||||
| -rw-r--r-- | src/Interpreter.ml | 52 | ||||
| -rw-r--r-- | src/LlbcAst.ml | 31 | ||||
| -rw-r--r-- | src/LlbcOfJson.ml | 11 | ||||
| -rw-r--r-- | src/Pure.ml | 2 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 26 | ||||
| -rw-r--r-- | src/Substitute.ml | 6 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 62 | ||||
| -rw-r--r-- | src/Translate.ml | 59 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 1 |
11 files changed, 135 insertions, 131 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index eb88b916..ec0f88a4 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -800,7 +800,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) (** Simply add the global name to the context. *) let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl) : extraction_ctx = - ctx_add_global_decl_body def ctx + ctx_add_global_decl_and_body def ctx (** The following function factorizes the extraction of ADT values. @@ -1364,7 +1364,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) : unit = - assert (not def.is_global_body); + assert (not def.is_global_decl_body); (* Retrieve the function name *) let def_name = ctx_get_local_function def.def_id def.back_id ctx in (* (* Add the type parameters - note that we need those bindings only for the @@ -1552,7 +1552,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = - assert body.is_global_body; + assert body.is_global_decl_body; assert (Option.is_none body.back_id); assert (List.length body.signature.inputs = 0); assert (List.length body.signature.doutputs = 1); diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index 2aebc144..615f45b3 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -92,25 +92,25 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - assert ((not f.is_global_body) || not !stateful); + 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_body) && use_state + stateful := (not f.is_global_decl_body) && use_state | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; (* We need to know if the declaration group contains a global - note that * groups containing globals contain exactly one declaration *) - let is_global_body = List.exists (fun f -> f.is_global_body) d in - assert ((not is_global_body) || List.length d == 1); + 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); (* 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. * *) - can_fail := (not is_global_body) || !can_fail; + can_fail := (not is_global_decl_body) || !can_fail; { can_fail = !can_fail; stateful = !stateful; divergent = !divergent } in diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 51144ba2..3a2939ef 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -13,7 +13,7 @@ module SA = SymbolicAst (** The local logger *) let log = L.interpreter_log -let compute_type_fun_contexts (m : M.llbc_module) : +let compute_type_fun_global_contexts (m : M.llbc_module) : C.type_context * C.fun_context * C.global_context = let type_decls_list, _, _ = M.split_declarations m.declarations in let type_decls, fun_decls, global_decls = M.compute_defs_maps m in @@ -28,10 +28,8 @@ let compute_type_fun_contexts (m : M.llbc_module) : 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) +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 (); { @@ -56,12 +54,9 @@ let initialize_eval_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) - (global_context : C.global_context) - (fdef : A.fun_decl) : - C.eval_ctx * V.symbolic_value list * A.inst_fun_sig = +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 * with the input values (which behave as if they had been returned @@ -75,7 +70,10 @@ let initialize_symbolic_context_for_fun * *) let sg = fdef.signature in (* Create the context *) - let ctx = initialize_eval_context type_context fun_context global_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 @@ -212,8 +210,9 @@ 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) (global_context : C.global_context) - (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) : + (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 *) let name_to_string () = @@ -226,7 +225,8 @@ 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 global_context fdef + initialize_symbolic_context_for_fun type_context fun_context global_context + fdef in (* Create the continuation to finish the evaluation *) @@ -293,8 +293,12 @@ module Test = struct assert (body.A.arg_count = 0); (* Create the evaluation context *) - 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 + let type_context, fun_context, global_context = + compute_type_fun_global_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 @@ -338,15 +342,16 @@ 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) (global_context : C.global_context) - (fdef : A.fun_decl) : unit = + (type_context : C.type_context) (fun_context : C.fun_context) + (global_context : C.global_context) (fdef : A.fun_decl) : unit = (* Debug *) log#ldebug (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name)); (* Evaluate *) let evaluate = - evaluate_function_symbolic config synthesize type_context fun_context global_context fdef + evaluate_function_symbolic config synthesize type_context fun_context + global_context fdef in (* Execute the forward function *) let _ = evaluate None in @@ -376,12 +381,15 @@ 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, global_context = compute_type_fun_contexts m in + let type_context, fun_context, global_context = + compute_type_fun_global_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 global_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/LlbcAst.ml b/src/LlbcAst.ml index 94566f9b..ccc870dc 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -3,7 +3,6 @@ open Types open Values open Expressions open Identifiers - module FunDeclId = IdGen () module GlobalDeclId = IdGen () @@ -37,10 +36,7 @@ type assumed_fun_id = type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id [@@deriving show, ord] -type global_assignment = { - dst : VarId.id; - global : GlobalDeclId.id; -} +type global_assignment = { dst : VarId.id; global : GlobalDeclId.id } [@@deriving show] type assertion = { cond : operand; expected : bool } [@@deriving show] @@ -84,22 +80,16 @@ class ['self] iter_statement_base = object (_self : 'self) inherit [_] VisitorsRuntime.iter - method visit_global_assignment : 'env -> global_assignment -> unit = fun _ _ -> () + method visit_global_assignment : 'env -> global_assignment -> unit = + fun _ _ -> () method visit_place : 'env -> place -> unit = fun _ _ -> () - method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> () - method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> () - method visit_assertion : 'env -> assertion -> unit = fun _ _ -> () - method visit_operand : 'env -> operand -> unit = fun _ _ -> () - method visit_call : 'env -> call -> unit = fun _ _ -> () - method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> () - method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> () end @@ -108,18 +98,15 @@ class ['self] map_statement_base = object (_self : 'self) inherit [_] VisitorsRuntime.map - method visit_global_assignment : 'env -> global_assignment -> global_assignment = fun _ x -> x + method visit_global_assignment + : 'env -> global_assignment -> global_assignment = + fun _ x -> x method visit_place : 'env -> place -> place = fun _ x -> x - method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x - method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x - method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x - method visit_operand : 'env -> operand -> operand = fun _ x -> x - method visit_call : 'env -> call -> call = fun _ x -> x method visit_integer_type : 'env -> integer_type -> integer_type = @@ -190,14 +177,14 @@ type fun_decl = { name : fun_name; signature : fun_sig; body : fun_body option; - is_global_body : bool; + is_global_decl_body : bool; } [@@deriving show] type global_decl = { def_id : GlobalDeclId.id; - body_id: FunDeclId.id; + body_id : FunDeclId.id; name : global_name; - ty: ety; + ty : ety; } [@@deriving show] diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 846d7232..4e10c642 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -631,7 +631,7 @@ let fun_decl_of_json (js : json) : (A.fun_decl, string) result = 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; is_global_body = false } + Ok { A.def_id; name; signature; body; is_global_decl_body = false } | _ -> Error "") (* Strict type for the number of function declarations (see [global_to_fun_id] below) *) @@ -670,8 +670,13 @@ let global_decl_of_json (js : json) (gid_conv : global_id_converter) : in Ok ( { A.def_id = global_id; body_id = fun_id; name; ty }, - { A.def_id = fun_id; name; signature; body; is_global_body = true } - ) + { + A.def_id = fun_id; + name; + signature; + body; + is_global_decl_body = true; + } ) | _ -> Error "") let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) diff --git a/src/Pure.ml b/src/Pure.ml index 5244b0bc..ced56c6a 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_body : bool; + is_global_decl_body : bool; body : fun_body option; } diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index b7d45deb..255d4e1b 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -29,11 +29,8 @@ module StringSet = Collections.MakeSet (Collections.OrderedString) module StringMap = Collections.MakeMap (Collections.OrderedString) type name = Names.name - type type_name = Names.type_name - type global_name = Names.global_name - type fun_name = Names.fun_name (* TODO: this should a module we give to a functor! *) @@ -229,11 +226,8 @@ module IdOrderedType = struct type t = id let compare = compare_id - let to_string = show_id - let pp_t = pp_id - let show_t = show_id end @@ -452,13 +446,11 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string = let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = ctx_get (GlobalId id) ctx -let ctx_get_function (id : A.fun_id) - (rg : RegionGroupId.id option) +let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get (FunId (id, rg)) ctx -let ctx_get_local_function (id : A.FunDeclId.id) - (rg : RegionGroupId.id option) +let ctx_get_local_function (id : A.FunDeclId.id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get_function (A.Regular id) rg ctx @@ -582,7 +574,7 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) : let name = ctx.fmt.decreases_clause_name def.def_id def.basename in ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx -let ctx_add_global_decl_body (def : A.global_decl) (ctx : extraction_ctx) : +let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = let name = ctx.fmt.global_name def.name in let decl = GlobalId def.def_id in @@ -622,9 +614,8 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) in (* Add the function name if it's not a global *) - if def.is_global_body - then ctx - else ctx_add (FunId (def_id, def.back_id)) name ctx + if def.is_global_decl_body then ctx + else ctx_add (FunId (def_id, def.back_id)) name ctx type names_map_init = { keywords : string list; @@ -690,11 +681,8 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = information. TODO: move all those helpers. *) -let default_fun_suffix - (num_region_groups : int) - (rg : region_group_info option) - ((keep_fwd, num_backs) : bool * int) - : string = +let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) + ((keep_fwd, num_backs) : bool * int) : string = (* There are several cases: - [rg] is `Some`: this is a forward function: - we add "_fwd" diff --git a/src/Substitute.ml b/src/Substitute.ml index 4b0a04ca..5a21e637 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -219,7 +219,7 @@ let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) : | E.Move p -> E.Move (p_subst p) | E.Constant (ety, cv) -> let rsubst x = x in - E.Constant ( ty_substitute rsubst tsubst ety, cv ) + E.Constant (ty_substitute rsubst tsubst ety, cv) (** Apply a type substitution to an rvalue *) let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) : @@ -281,7 +281,9 @@ let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety) let p = place_substitute tsubst p in let rvalue = rvalue_substitute tsubst rvalue in A.Assign (p, rvalue) - | A.AssignGlobal g -> A.AssignGlobal g + | A.AssignGlobal g -> + (* Globals don't have type parameters *) + A.AssignGlobal g | A.FakeRead p -> let p = place_substitute tsubst p in A.FakeRead p diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 81af6a8b..f321ce8c 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -72,9 +72,7 @@ type fun_context = { fun_infos : FA.fun_info A.FunDeclId.Map.t; } -type global_context = { - llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t; -} +type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t } type call_info = { forward : S.call; @@ -127,29 +125,31 @@ type bs_ctx = { let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit = let env = VarId.Map.empty in - let ctx = { - PureTypeCheck.type_decls = ctx.type_context.type_decls; - global_decls = ctx.global_context.llbc_global_decls; - env - } in + let ctx = + { + PureTypeCheck.type_decls = ctx.type_context.type_decls; + global_decls = ctx.global_context.llbc_global_decls; + env; + } + in let _ = PureTypeCheck.check_typed_pattern ctx v in () let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit = let env = VarId.Map.empty in - let ctx = { - PureTypeCheck.type_decls = ctx.type_context.type_decls; - global_decls = ctx.global_context.llbc_global_decls; - env - } in + let ctx = + { + PureTypeCheck.type_decls = ctx.type_context.type_decls; + global_decls = ctx.global_context.llbc_global_decls; + env; + } + in PureTypeCheck.check_texpression ctx e (* TODO: move *) 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 - ctx.global_context.llbc_global_decls + Print.LlbcAst.fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls + ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls ctx.fun_decl let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter = @@ -179,7 +179,9 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string = let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls 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 + 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 = @@ -187,7 +189,9 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls 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 + let fmt = + PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params + in PrintPure.fun_decl_to_string fmt def (* TODO: move *) @@ -214,8 +218,8 @@ let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl = TypeDeclId.Map.find id ctx.type_context.llbc_type_decls -let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : A.fun_decl - = +let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : + A.fun_decl = A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls (* TODO: move *) @@ -1462,9 +1466,8 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) given_back_inputs next_e and translate_global_eval (config : config) (gid : A.GlobalDeclId.id) - (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) - : texpression = - let (ctx, var) = fresh_var_for_symbolic_value sval ctx in + (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression = + let ctx, var = fresh_var_for_symbolic_value sval ctx in let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in let global_expr = { id = Global gid; type_args = [] } in (* We use translate_fwd_ty to translate the global type *) @@ -1751,7 +1754,16 @@ 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 = def.is_global_body; body } in + let def = + { + def_id; + back_id = bid; + basename; + signature; + is_global_decl_body = def.is_global_decl_body; + body; + } + in (* Debugging *) log#ldebug (lazy diff --git a/src/Translate.ml b/src/Translate.ml index 25aff2b2..c9dc7943 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -64,9 +64,7 @@ let translate_function_to_symbolics (config : C.partial_config) ^ Print.fun_name_to_string fdef.A.name)); let { type_context; fun_context; global_context } = trans_ctx in - let fun_context = { - C.fun_decls = fun_context.fun_decls; - } in + let fun_context = { C.fun_decls = fun_context.fun_decls } in match fdef.body with | None -> None @@ -75,9 +73,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 global_context - fdef gid + evaluate_function_symbolic config synthesize type_context fun_context + global_context fdef gid in (inputs, Option.get symb) in @@ -102,8 +99,7 @@ let translate_function_to_symbolics (config : C.partial_config) let translate_function_to_pure (config : C.partial_config) (mp_config : Micro.config) (trans_ctx : trans_ctx) (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t) - (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) - (fdef : A.fun_decl) + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) : pure_fun_translation = (* Debug *) log#ldebug @@ -144,9 +140,8 @@ let translate_function_to_pure (config : C.partial_config) fun_infos = fun_context.fun_infos; } in - let global_context = { - SymbolicToPure.llbc_global_decls = global_context.global_decls - } + let global_context = + { SymbolicToPure.llbc_global_decls = global_context.global_decls } in let ctx = { @@ -297,12 +292,14 @@ 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, global_context = compute_type_fun_contexts m in - let fun_infos = FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls use_state in - let fun_context = { - fun_decls = fun_context.fun_decls; - fun_infos; - } in + let type_context, fun_context, global_context = + compute_type_fun_global_contexts m + in + let fun_infos = + FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls + use_state + in + let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in let trans_ctx = { type_context; fun_context; global_context } in (* Translate all the type definitions *) @@ -498,8 +495,9 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) - then ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def - ) + then + ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif + has_decr_clause def) fls); (* Insert unit tests if necessary *) if config.test_unit_functions then @@ -514,13 +512,18 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) let export_global (id : A.GlobalDeclId.id) : unit = let global_decls = ctx.extract_ctx.trans_ctx.global_context.global_decls in let global = A.GlobalDeclId.Map.find id global_decls in - let (_, (body, body_backs)) = A.FunDeclId.Map.find global.body_id ctx.trans_funs in + let _, (body, body_backs) = + A.FunDeclId.Map.find global.body_id ctx.trans_funs + in assert (List.length body_backs = 0); - + let is_opaque = Option.is_none body.Pure.body in - if ((not is_opaque) && config.extract_transparent) - || (is_opaque && config.extract_opaque) - then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body config.interface + if + ((not is_opaque) && config.extract_transparent) + || (is_opaque && config.extract_opaque) + then + ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body + config.interface in let export_state_type () : unit = @@ -558,8 +561,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) in (* Translate *) export_functions true pure_funs - | Global id -> - export_global id + | Global id -> export_global id in (* If we need to export the state type: we try to export it after we defined @@ -677,8 +679,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config) ctx trans_funs in - let ctx = List.fold_left - ExtractToFStar.extract_global_decl_register_names ctx m.globals + let ctx = + List.fold_left ExtractToFStar.extract_global_decl_register_names ctx + m.globals in (* Open the output file *) diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index 8088be7f..b5ea6fca 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -87,7 +87,6 @@ let rty_regions (ty : rty) : RegionId.Set.t = let obj = object inherit [_] iter_ty - method! visit_'r _env r = add_region r end in |