summaryrefslogtreecommitdiff
path: root/src/LlbcOfJson.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/LlbcOfJson.ml')
-rw-r--r--src/LlbcOfJson.ml173
1 files changed, 82 insertions, 91 deletions
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 14333088..a074ed1e 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -11,7 +11,6 @@
open Yojson.Basic
open Names
open OfJsonBasic
-open FunIdentifier
module T = Types
module V = Values
module S = Scalars
@@ -19,6 +18,7 @@ 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
@@ -227,14 +227,6 @@ 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
@@ -308,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
@@ -403,25 +378,30 @@ 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) (fun_count : int) :
- (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
+ (* This indirection is because Charon still export the type OperandConstantValue,
+ * which had other variants than ConstantValue before.
+ *)
| `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 (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) (fun_count : int) : (E.operand, string) result =
+ (match cv 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 "")
+ | _ -> Error "")
+
+let operand_of_json (js : json) : (E.operand, string) result =
combine_error_msgs js "operand_of_json"
(match js with
| `Assoc [ ("Copy", place) ] ->
@@ -432,7 +412,7 @@ let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result =
Ok (E.Move place)
| `Assoc [ ("Const", `List [ ty; cv ]) ] ->
let* ty = ety_of_json ty in
- let* cv = operand_constant_value_of_json cv fun_count in
+ let* cv = constant_value_of_json cv in
Ok (E.Constant (ty, cv))
| _ -> Error "")
@@ -455,11 +435,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) (fun_count : int) : (E.rvalue, string) result =
+let rvalue_of_json (js : json) : (E.rvalue, string) result =
combine_error_msgs js "rvalue_of_json"
(match js with
| `Assoc [ ("Use", op) ] ->
- let* op = operand_of_json op fun_count in
+ let* op = operand_of_json op in
Ok (E.Use op)
| `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] ->
let* place = place_of_json place in
@@ -467,19 +447,19 @@ let rvalue_of_json (js : json) (fun_count : int) : (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 fun_count in
+ let* op = operand_of_json op 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 fun_count in
- let* op2 = operand_of_json op2 fun_count in
+ let* op1 = operand_of_json op1 in
+ let* op2 = operand_of_json op2 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 (fun js -> operand_of_json js fun_count) ops in
+ let* ops = list_of_json operand_of_json ops in
Ok (E.Aggregate (aggregate_kind, ops))
| _ -> Error "")
@@ -502,18 +482,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 = FunDeclId.id_of_json id in
+ let* id = A.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) (fun_count : int) : (A.assertion, string) result =
+let assertion_of_json (js : json) : (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 fun_count in
+ let* cond = operand_of_json cond in
let* expected = bool_of_json expected in
Ok { A.cond; expected }
| _ -> Error "")
@@ -547,7 +527,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
}
| _ -> Error "")
-let call_of_json (js : json) (fun_count : int) : (A.call, string) result =
+let call_of_json (js : json) : (A.call, string) result =
combine_error_msgs js "call_of_json"
(match js with
| `Assoc
@@ -561,18 +541,22 @@ let call_of_json (js : json) (fun_count : int) : (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 (fun js -> operand_of_json js fun_count) args in
+ let* args = list_of_json operand_of_json 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) (fun_count : int) : (A.statement, string) result =
+let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (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 fun_count 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)
@@ -584,10 +568,10 @@ let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string)
let* place = place_of_json place in
Ok (A.Drop place)
| `Assoc [ ("Assert", assertion) ] ->
- let* assertion = assertion_of_json assertion fun_count in
+ let* assertion = assertion_of_json assertion in
Ok (A.Assert assertion)
| `Assoc [ ("Call", call) ] ->
- let* call = call_of_json call fun_count in
+ let* call = call_of_json call in
Ok (A.Call call)
| `String "Panic" -> Ok A.Panic
| `String "Return" -> Ok A.Return
@@ -599,48 +583,48 @@ let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string)
Ok (A.Continue i)
| `String "Nop" -> Ok A.Nop
| `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
- let* st1 = statement_of_json st1 fun_count in
- let* st2 = statement_of_json st2 fun_count in
+ let* st1 = statement_of_json st1 gid_conv in
+ let* st2 = statement_of_json st2 gid_conv in
Ok (A.Sequence (st1, st2))
| `Assoc [ ("Switch", `List [ op; tgt ]) ] ->
- let* op = operand_of_json op fun_count in
- let* tgt = switch_targets_of_json tgt fun_count in
+ let* op = operand_of_json op in
+ let* tgt = switch_targets_of_json tgt gid_conv in
Ok (A.Switch (op, tgt))
| `Assoc [ ("Loop", st) ] ->
- let* st = statement_of_json st fun_count in
+ let* st = statement_of_json st gid_conv in
Ok (A.Loop st)
| _ -> Error "")
-and switch_targets_of_json (js : json) (fun_count : int) : (A.switch_targets, string) result =
+and switch_targets_of_json (js : json) (gid_conv : A.global_id_converter) : (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 fun_count in
- let* st2 = statement_of_json st2 fun_count in
+ let* st1 = statement_of_json st1 gid_conv in
+ let* st2 = statement_of_json st2 gid_conv 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)
- (fun js -> statement_of_json js fun_count))
+ (fun js -> statement_of_json js gid_conv))
tgts
in
- let* otherwise = statement_of_json otherwise fun_count in
+ let* otherwise = statement_of_json otherwise gid_conv in
Ok (A.SwitchInt (int_ty, tgts, otherwise))
| _ -> Error "")
-let fun_body_of_json (js : json) (fun_count : int) : (A.fun_body, string) result =
+let fun_body_of_json (js : json) (gid_conv : A.global_id_converter) : (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 fun_count in
+ let* body = statement_of_json body gid_conv in
Ok { A.arg_count; locals; body }
| _ -> Error "")
-let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result =
+let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
combine_error_msgs js "fun_decl_of_json"
(match js with
| `Assoc
@@ -650,20 +634,16 @@ let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result
("signature", signature);
("body", body);
] ->
- let* def_id = FunDeclId.id_of_json def_id in
+ 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 fun_count) body 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; }
| _ -> 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 =
+ *)
+let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
combine_error_msgs js "global_decl_of_json"
(match js with
| `Assoc
@@ -673,10 +653,11 @@ let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) resu
("type_", type_);
("body", body);
] ->
- let* def_id = global_id_of_json def_id fun_count in
+ 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* 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* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in
let signature : A.fun_sig = {
region_params = [];
num_early_bound_regions = 0;
@@ -708,14 +689,17 @@ 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 FunDeclId.id_of_json js)
+ (g_declaration_group_of_json A.FunDeclId.id_of_json js)
-let global_declaration_group_of_json (js : json) (fun_count: int) :
+let global_declaration_group_of_json (js : json) (gid_conv : A.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 -> global_id_of_json js fun_count) js)
+ (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)
+ ) js)
-let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_group, string) result
+let declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.declaration_group, string) result
=
combine_error_msgs js "declaration_of_json"
(match js with
@@ -726,7 +710,7 @@ let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_grou
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
+ let* decl = global_declaration_group_of_json decl gid_conv in
Ok (M.Fun decl)
| _ -> Error "")
@@ -748,12 +732,19 @@ 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* name = string_of_json name in
let* declarations =
- list_of_json (fun js -> declaration_group_of_json js fun_count) 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 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 }
+ let* functions = list_of_json (fun js -> fun_decl_of_json js gid_conv) functions in
+ let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in
+ Ok {
+ M.name;
+ declarations;
+ types;
+ functions = functions @ globals;
+ gid_conv;
+ }
| _ -> Error "")
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 16:28:12 +0000