diff options
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterBorrows.ml | 8 | ||||
| -rw-r--r-- | src/Print.ml | 2 | ||||
| -rw-r--r-- | src/PrintPure.ml | 13 | ||||
| -rw-r--r-- | src/Pure.ml | 36 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 94 | ||||
| -rw-r--r-- | src/PureUtils.ml | 6 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 42 | ||||
| -rw-r--r-- | src/Values.ml | 20 | ||||
| -rw-r--r-- | src/main.ml | 32 |
9 files changed, 152 insertions, 101 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 065a39b9..89dfb274 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1202,12 +1202,12 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) ^ aborrow_content_to_string ctx bc)); let ctx = match bc with - | V.AMutBorrow (mv, bid, av) -> + | V.AMutBorrow (_mv, bid, av) -> (* First, convert the avalue to a (fresh symbolic) value *) let sv = convert_avalue_to_given_back_value abs.kind av in (* Replace the mut borrow to register the fact that we ended * it and store with it the freshly generated given back value *) - let ended_borrow = V.ABorrow (V.AEndedMutBorrow (mv, sv, av)) in + let ended_borrow = V.ABorrow (V.AEndedMutBorrow (sv, av)) in let ctx = update_aborrow ek_all bid ended_borrow ctx in (* Give the value back *) let sv = mk_typed_value_from_symbolic_value sv in @@ -1256,9 +1256,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (* Generate a fresh symbolic value *) let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in (* Replace the proj_borrows - there should be exactly one *) - let ended_borrow = - V.AEndedProjBorrows { original = sv; given_back = nsv } - in + let ended_borrow = V.AEndedProjBorrows nsv in let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in (* Give back the symbolic value *) let ctx = diff --git a/src/Print.ml b/src/Print.ml index 69379bf9..5ccba517 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -457,7 +457,7 @@ module Values = struct ^ ", " ^ typed_avalue_to_string fmt av ^ ")" - | AEndedMutBorrow (_mv, _msv, child) -> + | AEndedMutBorrow (_mv, child) -> "@ended_mut_borrow(" ^ typed_avalue_to_string fmt child ^ ")" | AEndedIgnoredMutBorrow { child; given_back_loans_proj; given_back_meta = _ } -> diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 9ca0c064..e962c27c 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -318,15 +318,10 @@ let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string let var_or_dummy_to_string (fmt : ast_formatter) (v : var_or_dummy) : string = match v with - | Var (v, { place = None; from_rvalue = None }) -> - var_to_string (ast_to_type_formatter fmt) v - | Var (v, { place; from_rvalue }) -> - let dest = Print.option_to_string (mplace_to_string fmt) place in - let from_rvalue = - Print.option_to_string (typed_rvalue_to_string fmt) from_rvalue - in - "(" ^ var_to_varname v ^ " @meta[@dest=" ^ dest ^ ", from_rvalue=" - ^ from_rvalue ^ "] : " + | Var (v, None) -> var_to_string (ast_to_type_formatter fmt) v + | Var (v, Some mp) -> + let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in + "(" ^ var_to_varname v ^ " " ^ mp ^ " : " ^ ty_to_string (ast_to_type_formatter fmt) v.ty ^ ")" | Dummy -> "_" diff --git a/src/Pure.ml b/src/Pure.ml index dbc6421c..f0e43115 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -12,6 +12,16 @@ module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId module FunDeclId = A.FunDeclId +module MPlaceId = IdGen () +(** A meta-place identifier. See [mplace]. *) + +(** Some global counters - TODO: remove *) + +let mplace_id_counter, fresh_mplace_id = MPlaceId.fresh_stateful_generator () + +(** Reset the mplace counter *) +let reset_pure_counters () = mplace_id_counter := MPlaceId.generator_zero + module SynthPhaseId = IdGen () (** We give an identifier to every phase of the synthesis (forward, backward for group of regions 0, etc.) *) @@ -283,14 +293,14 @@ and typed_rvalue = { value : rvalue; ty : ty } polymorphic = false; }] -type mdplace = { place : mplace option; from_rvalue : typed_rvalue option } -[@@deriving show] -(** "Meta" destination place. +(** Meta destination place. Meta information for places used as assignment destinations. - This is useful for the values given back by the backward functions: in such - situations, we link the output variables to the input arguments, to derive - names for the output variables from the input variables. + Either a regular mplace, or an mplace derived from another mplace. + + The second case is used for values given back by backward function: we + remember the identifier of the place from which the input argument was + taken from. Ex.: ==== @@ -302,17 +312,21 @@ type mdplace = { place : mplace option; from_rvalue : typed_rvalue option } ``` gets translated to: ``` - let y = f_fwd x in + let y = f_fwd xv in ... - let s = f_back x y_i in // we want the introduced variable to be name "x1" + let s = f_back xv y_i in // we want the introduced variable to be name "x" ... ``` In order to compute a proper name for the variable introduced by the backward call, we need to link `s` to `x`. However, because of desugaring, it may happen that the fact `f` takes `x` as argument may have to be computed by propagating - naming information. This is why we link the output variables to the input arguments: - it allows us to propagate such naming constraints "across" function calls. + naming information. We use place identifiers to link the output variables to the + input arguments: it allows us to propagate naming constraints "across" function + calls. + + The full details are given in [PureMicroPasses.compute_pretty_names] *) +type mdplace = Regular of mplace | From of MPlaceId.id [@@deriving show] (** Ancestor for [iter_var_or_dummy] visitor *) class ['self] iter_var_or_dummy_base = @@ -348,7 +362,7 @@ class virtual ['self] mapreduce_var_or_dummy_base = end type var_or_dummy = - | Var of var * mdplace + | Var of var * mplace option (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections). We use [mplace] because it leads to a more uniform treatment of the meta diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index abdeb41e..ceaaa129 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -85,7 +85,9 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator = (* Find the max id in the input variables - some of them may have been * filtered from the body *) let min_input_id = - List.fold_left (fun id var -> VarId.max id var.id) VarId.zero body.inputs + List.fold_left + (fun id (var : var) -> VarId.max id var.id) + VarId.zero body.inputs in let obj = object @@ -119,9 +121,12 @@ type pn_ctx = string VarId.Map.t - whenever we see an rvalue/lvalue which is exactly an unnamed variable, and this value is linked to some meta-place information which contains a name and an empty path, we consider we should use this name + - for the values given back by backward functions, we link the given back + values to the places (identified by unique indices) where the input + arguments come from (see examples below) Something important is that, for every variable we find, the name of this - variable is influenced by the information we find *below* in the AST. + variable can be influenced by the information we find *below* in the AST. For instance, the following situations happen: @@ -139,8 +144,8 @@ type pn_ctx = string VarId.Map.t tmp := discriminant(ls); switch tmp { 0 => { - x := (ls as Cons).0; - hd := (ls as Cons).1; + x := (ls as Cons).0; // (i) + hd := (ls as Cons).1; // (ii) ... } } @@ -149,8 +154,10 @@ type pn_ctx = string VarId.Map.t mode, we expand this value upon evaluating `tmp = discriminant(ls)`. However, at this point, we don't know which should be the names of the symbolic values we introduce for the fields of `Cons`! + Let's imagine we have (for the `Cons` branch): `s0 ~~> Cons s1 s2`. - The assigments lead to the following binding in the evaluation context: + The assigments at (i) and (ii) lead to the following binding in the + evaluation context: ``` x -> s1 hd -> s2 @@ -165,7 +172,44 @@ type pn_ctx = string VarId.Map.t | Cons x hd -> ... | ... ``` + - Given back values (introduced by backward functions): + Let's say we have the following Rust code: + ``` + let py = id(&mut x); + *py = 2; + assert!(x == 2); + ``` + + After desugaring, we get the following MIR: + ``` + ^0 = &mut x; // anonymous variable + py = id(move ^0); + *py += 2; + assert!(x == 2); + ``` + + We want this to be translated as: + ``` + let py = id_fwd x in + let py1 = py + 2 in + let x1 = id_back x py1 in // <-- x1 is "given back": doesn't appear in the original MIR + assert(x1 = 2); + ``` + + We want to notice that the value given back by `id_back` is given back for "x", + so we should use "x" as the basename (hence the resulting name "x1"). However, + this is non-trivial, because after desugaring the input argument given to `id` + is not `&mut x` but `move ^0` (i.e., it comes from a temporary, anonymous + variable). For this reason, we give unique identifiers to places, link + given back values to the places where the input arguments come from, and + propagate naming information between the places. + + This way, because of `^0 = &mut x`, we can propagate the name "x" to the place + `^0`, then to the given back variable across the function call. + - TODO: inputs and end abstraction... + + *) let compute_pretty_names (def : fun_decl) : fun_decl = (* Small helpers *) @@ -217,6 +261,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = in let add_constraint (mp : mplace) (var_id : VarId.id) (ctx : pn_ctx) : pn_ctx = + (* Update the variable name *) match (mp.name, mp.projection) with | Some name, [] -> (* Check if the variable already has a name - if not: insert the new name *) @@ -242,19 +287,39 @@ let compute_pretty_names (def : fun_decl) : fun_decl = method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ()) - method! visit_Var _ v mdp () = + method! visit_Var _ v mp () = (* Register the variable *) let ctx = add_var (self#zero ()) v in (* Register the mplace information if there is such information *) - match mdp.place with - | None -> ctx - | Some mp -> add_constraint mp v.id ctx + match mp with Some mp -> add_constraint mp v.id ctx | None -> ctx end in let ctx1 = obj#visit_typed_lvalue () lv () in merge_ctxs ctx ctx1 in + (* This is used to propagate constraint information about places in case of + * assignments *) + let add_left_right_constraint (lv : typed_lvalue) (re : texpression) + (ctx : pn_ctx) : pn_ctx = + (* We propagate constraints across variable reassignments: `^0 = x` *) + match (lv.value, re.e) with + | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))), + Value (_, Some ({ name = Some _; projection = [] } as rmp)) ) -> + (* Use the meta-information on the right *) + add_constraint rmp lvar.id ctx + | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))), + Value ({ value = RvPlace { var = rvar_id; projection = [] }; ty = _ }, _) + ) -> ( + (* Use the variable name *) + match + (VarId.Map.find_opt lvar.id ctx, VarId.Map.find_opt rvar_id ctx) + with + | None, Some name -> VarId.Map.add lvar.id name ctx + | _ -> ctx) + | _ -> (* Nothing to propagate *) ctx + in + (* *) let rec update_texpression (e : texpression) (ctx : pn_ctx) : pn_ctx * texpression = @@ -286,6 +351,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = and update_let (monadic : bool) (lv : typed_lvalue) (re : texpression) (e : texpression) (ctx : pn_ctx) : pn_ctx * expression = let ctx = add_left_constraint lv ctx in + let ctx = add_left_right_constraint lv re ctx in let ctx, re = update_texpression re ctx in let ctx, e = update_texpression e ctx in let lv = update_typed_lvalue ctx lv in @@ -822,7 +888,7 @@ let to_monadic (config : config) (def : fun_decl) : fun_decl = let id, _ = VarId.fresh var_cnt in let var = { id; basename = None; ty = unit_ty } in let inputs = [ var ] in - let input_lv = mk_typed_lvalue_from_var var None None in + let input_lv = mk_typed_lvalue_from_var var None in let inputs_lvs = [ input_lv ] in Some { body with inputs; inputs_lvs } in @@ -980,7 +1046,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : * monadic binding *) let vid = fresh_id () in let tmp : var = { id = vid; basename = None; ty = lv.ty } in - let ltmp = mk_typed_lvalue_from_var tmp None None in + let ltmp = mk_typed_lvalue_from_var tmp None in let rtmp = mk_typed_rvalue_from_var tmp in let rtmp = mk_value_expression rtmp None in (* Visit the next expression *) @@ -1058,9 +1124,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx) in (* The `Success` branch introduces a fresh state variable *) let state_var = fresh_state_var () in - let state_value = - mk_typed_lvalue_from_var state_var None None - in + let state_value = mk_typed_lvalue_from_var state_var None in let success_pat = mk_result_return_lvalue (mk_simpl_tuple_lvalue [ state_value; lv ]) @@ -1131,7 +1195,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx) let sg = { sg with inputs = sg_inputs; outputs = sg_outputs } in (* Update the inputs list *) let inputs = body.inputs @ [ input_state_var ] in - let input_lv = mk_typed_lvalue_from_var input_state_var None None in + let input_lv = mk_typed_lvalue_from_var input_state_var None in let inputs_lvs = body.inputs_lvs @ [ input_lv ] in (* Update the body *) let body = { body with inputs; inputs_lvs } in diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 78ddf8aa..23bffa1d 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -64,10 +64,8 @@ let mk_typed_rvalue_from_var (v : var) : typed_rvalue = let ty = v.ty in { value; ty } -let mk_typed_lvalue_from_var (v : var) (mp : mplace option) - (mfrom_rvalue : typed_rvalue option) : typed_lvalue = - let mdplace = { place = mp; from_rvalue = mfrom_rvalue } in - let value = LvVar (Var (v, mdplace)) in +let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue = + let value = LvVar (Var (v, mp)) in let ty = v.ty in { value; ty } diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 87e86e69..163ddde8 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -736,7 +736,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : match bc with | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> failwith "Unreachable" - | AEndedMutBorrow (_, _, _) -> + | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) None | AEndedIgnoredMutBorrow _ -> @@ -804,9 +804,6 @@ let translate_opt_mplace (p : S.mplace option) : mplace option = [mp]: it is possible to provide some meta-place information, to guide the heuristics which later find pretty names for the variables. - - TODO: - *) let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) (ctx : bs_ctx) : bs_ctx * typed_lvalue option = @@ -878,13 +875,10 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) match bc with | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> failwith "Unreachable" - | AEndedMutBorrow (consumed_mv, msv, _) -> - (* We use the originally consumed value (which is stored as a meta-value) - * to help with propagating naming constraints. *) - let consumed = typed_value_to_rvalue ctx consumed_mv in + | AEndedMutBorrow (msv, _) -> (* Return the meta-symbolic-value *) let ctx, var = fresh_var_for_symbolic_value msv ctx in - (ctx, Some (mk_typed_lvalue_from_var var mp (Some consumed))) + (ctx, Some (mk_typed_lvalue_from_var var mp)) | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -903,15 +897,10 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) child_projs); (ctx, None) - | AEndedProjBorrows { original; given_back = mv } -> - (* We use the original symbolic value to help propagate the naming constraints *) - let original = - InterpreterUtils.mk_typed_value_from_symbolic_value original - in - let original = typed_value_to_rvalue ctx original in + | AEndedProjBorrows mv -> (* Return the meta-value *) let ctx, var = fresh_var_for_symbolic_value mv ctx in - (ctx, Some (mk_typed_lvalue_from_var var mp (Some original))) + (ctx, Some (mk_typed_lvalue_from_var var mp)) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> failwith "Unreachable" @@ -1050,7 +1039,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression) (fun (arg, mp) -> mk_value_expression arg mp) (List.combine args args_mplaces) in - let dest_v = mk_typed_lvalue_from_var dest dest_mplace None in + let dest_v = mk_typed_lvalue_from_var dest dest_mplace in let call = { func; type_params; args } in let call = Call call in let call_ty = if monadic then mk_result_ty dest_v.ty else dest_v.ty in @@ -1115,7 +1104,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) List.fold_right (fun (var, value) (e : texpression) -> mk_let monadic - (mk_typed_lvalue_from_var var None None) + (mk_typed_lvalue_from_var var None) (mk_value_expression value None) e) variables_values next_e @@ -1287,7 +1276,7 @@ and translate_expansion (config : config) (p : S.mplace option) let next_e = translate_expression config e ctx in let monadic = false in mk_let monadic - (mk_typed_lvalue_from_var var None None) + (mk_typed_lvalue_from_var var None) (mk_value_expression scrutinee scrutinee_mplace) next_e | SeAdt _ -> @@ -1311,7 +1300,7 @@ and translate_expansion (config : config) (p : S.mplace option) (* This is an enumeration: introduce an [ExpandEnum] let-binding *) let variant_id = Option.get variant_id in let lvars = - List.map (fun v -> mk_typed_lvalue_from_var v None None) vars + List.map (fun v -> mk_typed_lvalue_from_var v None) vars in let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in let monadic = false in @@ -1340,13 +1329,13 @@ and translate_expansion (config : config) (p : S.mplace option) (fun (fid, var) e -> let field_proj = gen_field_proj fid var in mk_let monadic - (mk_typed_lvalue_from_var var None None) + (mk_typed_lvalue_from_var var None) (mk_value_expression field_proj None) e) id_var_pairs branch | T.Tuple -> let vars = - List.map (fun x -> mk_typed_lvalue_from_var x None None) vars + List.map (fun x -> mk_typed_lvalue_from_var x None) vars in let monadic = false in mk_let monadic @@ -1362,7 +1351,7 @@ and translate_expansion (config : config) (p : S.mplace option) * identity when extracted (`box a == a`) *) let monadic = false in mk_let monadic - (mk_typed_lvalue_from_var var None None) + (mk_typed_lvalue_from_var var None) (mk_value_expression scrutinee scrutinee_mplace) branch | T.Assumed T.Vec -> @@ -1383,7 +1372,7 @@ and translate_expansion (config : config) (p : S.mplace option) let variant_id = Option.get variant_id in let ctx, vars = fresh_vars_for_symbolic_values svl ctx in let vars = - List.map (fun x -> mk_typed_lvalue_from_var x None None) vars + List.map (fun x -> mk_typed_lvalue_from_var x None) vars in let pat_ty = scrutinee.ty in let pat = mk_adt_lvalue pat_ty variant_id vars in @@ -1456,6 +1445,9 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression) let translate_fun_decl (config : config) (ctx : bs_ctx) (body : S.expression option) : fun_decl = + (* Reset the counters *) + reset_pure_counters (); + (* Translate *) let def = ctx.fun_decl in let bid = ctx.bid in log#ldebug @@ -1492,7 +1484,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) in let inputs = List.append ctx.forward_inputs backward_inputs in let inputs_lvs = - List.map (fun v -> mk_typed_lvalue_from_var v None None) inputs + List.map (fun v -> mk_typed_lvalue_from_var v None) inputs in (* Sanity check *) assert ( diff --git a/src/Values.ml b/src/Values.ml index a3dfb84a..3314defb 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -329,16 +329,10 @@ type aproj = Note that we keep the original symbolic value as a meta-value. *) - | AEndedProjBorrows of { - original : msymbolic_value; - given_back : msymbolic_value; - } + | AEndedProjBorrows of msymbolic_value (** The only purpose of [AEndedProjBorrows] is to store, for synthesis - purposes, the symbolic value which was originally in the borrow projection, - and the symbolic value which was generated and given back upon ending the borrow. - - The given back value is necessary for the synthesis. The orignal value is - useful to propagate naming constraints. + purposes, the symbolic value which was generated and given back upon + ending the borrow. *) | AIgnoredProjBorrows [@@deriving @@ -681,13 +675,9 @@ and aborrow_content = abstraction so that we can properly call the backward functions when generating the pure translation. *) - | AEndedMutBorrow of mvalue * msymbolic_value * typed_avalue + | AEndedMutBorrow of msymbolic_value * typed_avalue (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value - that we gave back as a meta-value, to help with the synthesis, together - with the initial consumed value (also as a meta-value). - - The given back value is necessary for the synthesis. The orignal consumed - value is useful to propagate naming constraints. + that we gave back as a meta-value, to help with the synthesis. We also remember the child [avalue] because this structural information is useful for the synthesis (but not for the symbolic execution): diff --git a/src/main.ml b/src/main.ml index 00693890..943689be 100644 --- a/src/main.ml +++ b/src/main.ml @@ -122,22 +122,22 @@ let () = (* Set up the logging - for now we use default values - TODO: use the * command-line arguments *) - Easy_logging.Handlers.set_level main_logger_handler EL.Info; - main_log#set_level EL.Info; - llbc_of_json_logger#set_level EL.Info; - pre_passes_log#set_level EL.Info; - interpreter_log#set_level EL.Info; - statements_log#set_level EL.Info; - paths_log#set_level EL.Info; - expressions_log#set_level EL.Info; - expansion_log#set_level EL.Info; - borrows_log#set_level EL.Info; - invariants_log#set_level EL.Info; - pure_utils_log#set_level EL.Info; - symbolic_to_pure_log#set_level EL.Info; - pure_micro_passes_log#set_level EL.Info; - pure_to_extract_log#set_level EL.Info; - translate_log#set_level EL.Info; + Easy_logging.Handlers.set_level main_logger_handler EL.Debug; + main_log#set_level EL.Debug; + llbc_of_json_logger#set_level EL.Debug; + pre_passes_log#set_level EL.Debug; + interpreter_log#set_level EL.Debug; + statements_log#set_level EL.Debug; + paths_log#set_level EL.Debug; + expressions_log#set_level EL.Debug; + expansion_log#set_level EL.Debug; + borrows_log#set_level EL.Debug; + invariants_log#set_level EL.Debug; + pure_utils_log#set_level EL.Debug; + symbolic_to_pure_log#set_level EL.Debug; + pure_micro_passes_log#set_level EL.Debug; + pure_to_extract_log#set_level EL.Debug; + translate_log#set_level EL.Debug; (* Load the module *) let json = Yojson.Basic.from_file filename in match llbc_module_of_json json with |