diff options
Diffstat (limited to 'src/LlbcOfJson.ml')
-rw-r--r-- | src/LlbcOfJson.ml | 146 |
1 files changed, 104 insertions, 42 deletions
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 "") |