diff options
Diffstat (limited to '')
| -rw-r--r-- | src/LlbcOfJson.ml | 141 |
1 files changed, 108 insertions, 33 deletions
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 99d652ec..4e10c642 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -17,6 +17,8 @@ module S = Scalars module M = Modules module E = Expressions module A = LlbcAst +module TU = TypesUtils +module AU = LlbcAstUtils (* The default logger *) let log = Logging.llbc_of_json_logger @@ -298,23 +300,6 @@ let scalar_value_of_json (js : json) : (V.scalar_value, string) result = raise (Failure ("Scalar value not in range: " ^ V.show_scalar_value sv))); res -let constant_value_of_json (js : json) : (V.constant_value, string) result = - combine_error_msgs js "constant_value_of_json" - (match js with - | `Assoc [ ("Scalar", scalar_value) ] -> - let* scalar_value = scalar_value_of_json scalar_value in - Ok (V.Scalar scalar_value) - | `Assoc [ ("Bool", v) ] -> - let* v = bool_of_json v in - Ok (V.Bool v) - | `Assoc [ ("Char", v) ] -> - let* v = char_of_json v in - Ok (V.Char v) - | `Assoc [ ("String", v) ] -> - let* v = string_of_json v in - Ok (V.String v) - | _ -> Error "") - let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result = combine_error_msgs js "field_proj_kind_of_json" (match js with @@ -393,19 +378,21 @@ 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) : - (E.operand_constant_value, string) result = - combine_error_msgs js "operand_constant_value_of_json" +let constant_value_of_json (js : json) : (V.constant_value, string) result = + combine_error_msgs js "constant_value_of_json" (match js with - | `Assoc [ ("ConstantValue", `List [ cv ]) ] -> - let* cv = constant_value_of_json cv in - Ok (E.ConstantValue cv) - | `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 - in - Ok (E.ConstantAdt (variant_id, field_values)) + | `Assoc [ ("Scalar", scalar_value) ] -> + let* scalar_value = scalar_value_of_json scalar_value in + Ok (V.Scalar scalar_value) + | `Assoc [ ("Bool", v) ] -> + let* v = bool_of_json v in + Ok (V.Bool v) + | `Assoc [ ("Char", v) ] -> + let* v = char_of_json v in + Ok (V.Char v) + | `Assoc [ ("String", v) ] -> + let* v = string_of_json v in + Ok (V.String v) | _ -> Error "") let operand_of_json (js : json) : (E.operand, string) result = @@ -417,9 +404,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 = constant_value_of_json cv in Ok (E.Constant (ty, cv)) | _ -> Error "") @@ -560,6 +547,10 @@ let rec statement_of_json (js : json) : (A.statement, string) result = let* place = place_of_json place in let* rvalue = rvalue_of_json rvalue in Ok (A.Assign (place, rvalue)) + | `Assoc [ ("AssignGlobal", `List [ dst; global ]) ] -> + let* dst = V.VarId.id_of_json dst in + let* global = A.GlobalDeclId.id_of_json global in + Ok (A.AssignGlobal { dst; global }) | `Assoc [ ("FakeRead", place) ] -> let* place = place_of_json place in Ok (A.FakeRead place) @@ -640,7 +631,52 @@ 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 } + 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) *) +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_fun_id <=> global_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 : global_id_converter) : + (A.global_decl * A.fun_decl, string) result = + combine_error_msgs js "global_decl_of_json" + (match js with + | `Assoc [ ("def_id", def_id); ("name", name); ("ty", ty); ("body", body) ] + -> + let* global_id = A.GlobalDeclId.id_of_json def_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_body_of_json 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 ty; + } + in + Ok + ( { A.def_id = global_id; body_id = fun_id; name; ty }, + { + 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) @@ -665,6 +701,16 @@ 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) : + (A.GlobalDeclId.id, string) result = + combine_error_msgs js "global_declaration_group_of_json" + (match js with + | `Assoc [ ("NonRec", `List [ id ]) ] -> + let* id = A.GlobalDeclId.id_of_json id in + Ok id + | `Assoc [ ("Rec", `List [ _ ]) ] -> Error "got mutually dependent globals" + | _ -> Error "") + let declaration_group_of_json (js : json) : (M.declaration_group, string) result = combine_error_msgs js "declaration_of_json" @@ -675,8 +721,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* id = global_declaration_group_of_json decl in + Ok (M.Global id) | _ -> 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 +741,32 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("declarations", declarations); ("types", types); ("functions", functions); + ("globals", globals); ] -> + (* We first deserialize the declaration groups (which simply contain ids) + * and all the declarations *butù* the globals *) let* name = string_of_json name in let* declarations = list_of_json declaration_group_of_json 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 } + (* When deserializing the globals, we split the global declarations + * between the globals themselves and their bodies, which are simply + * functions with no arguments. We add the global bodies to the list + * of function declarations: the (fresh) ids we use for those bodies + * are simply given by: `num_functions + global_id` *) + let gid_conv = { fun_count = List.length 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 @ global_bodies; + globals; + } | _ -> Error "") |