From 80d0d22f152386ffe28b48f42f42f8f736170014 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 3 Mar 2022 13:23:13 +0100 Subject: Rename CfimOfJson to LlbcOfJson --- src/CfimOfJson.ml | 682 ------------------------------------------------------ src/LlbcAst.ml | 13 ++ src/LlbcOfJson.ml | 682 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ src/Logging.ml | 4 +- src/main.ml | 2 +- 5 files changed, 698 insertions(+), 685 deletions(-) delete mode 100644 src/CfimOfJson.ml create mode 100644 src/LlbcOfJson.ml (limited to 'src') diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml deleted file mode 100644 index e293b030..00000000 --- a/src/CfimOfJson.ml +++ /dev/null @@ -1,682 +0,0 @@ -(** Functions to load CFIM ASTs from json. - - Initially, we used `ppx_derive_yojson` to automate this. - However, `ppx_derive_yojson` expects formatting to be slightly - different from what `serde_rs` generates (because it uses [Yojson.Safe.t] - and not [Yojson.Basic.t]). - - TODO: we should check all that the integer values are in the proper range - *) - -open Yojson.Basic -open Names -open OfJsonBasic -module T = Types -module V = Values -module S = Scalars -module M = Modules -module E = Expressions -module A = LlbcAst - -(* The default logger *) -let log = Logging.llbc_of_json_logger - -let path_elem_of_json (js : json) : (path_elem, string) result = - combine_error_msgs js "path_elem_of_json" - (match js with - | `Assoc [ ("Ident", name) ] -> - let* name = string_of_json name in - Ok (Ident name) - | `Assoc [ ("Disambiguator", d) ] -> - let* d = Disambiguator.id_of_json d in - Ok (Disambiguator d) - | _ -> Error "") - -let name_of_json (js : json) : (name, string) result = - combine_error_msgs js "name_of_json" (list_of_json path_elem_of_json js) - -let fun_name_of_json (js : json) : (fun_name, string) result = - combine_error_msgs js "fun_name_of_json" (name_of_json js) - -let type_var_of_json (js : json) : (T.type_var, string) result = - combine_error_msgs js "type_var_of_json" - (match js with - | `Assoc [ ("index", index); ("name", name) ] -> - let* index = T.TypeVarId.id_of_json index in - let* name = string_of_json name in - Ok { T.index; name } - | _ -> Error "") - -let region_var_of_json (js : json) : (T.region_var, string) result = - combine_error_msgs js "region_var_of_json" - (match js with - | `Assoc [ ("index", index); ("name", name) ] -> - let* index = T.RegionVarId.id_of_json index in - let* name = string_option_of_json name in - Ok { T.index; name } - | _ -> Error "") - -let region_of_json (js : json) : (T.RegionVarId.id T.region, string) result = - combine_error_msgs js "region_of_json" - (match js with - | `String "Static" -> Ok T.Static - | `Assoc [ ("Var", rid) ] -> - let* rid = T.RegionVarId.id_of_json rid in - Ok (T.Var rid) - | _ -> Error "") - -let erased_region_of_json (js : json) : (T.erased_region, string) result = - combine_error_msgs js "erased_region_of_json" - (match js with `String "Erased" -> Ok T.Erased | _ -> Error "") - -let integer_type_of_json (js : json) : (T.integer_type, string) result = - match js with - | `String "Isize" -> Ok T.Isize - | `String "I8" -> Ok T.I8 - | `String "I16" -> Ok T.I16 - | `String "I32" -> Ok T.I32 - | `String "I64" -> Ok T.I64 - | `String "I128" -> Ok T.I128 - | `String "Usize" -> Ok T.Usize - | `String "U8" -> Ok T.U8 - | `String "U16" -> Ok T.U16 - | `String "U32" -> Ok T.U32 - | `String "U64" -> Ok T.U64 - | `String "U128" -> Ok T.U128 - | _ -> Error ("integer_type_of_json failed on: " ^ show js) - -let ref_kind_of_json (js : json) : (T.ref_kind, string) result = - match js with - | `String "Mut" -> Ok T.Mut - | `String "Shared" -> Ok T.Shared - | _ -> Error ("ref_kind_of_json failed on: " ^ show js) - -let assumed_ty_of_json (js : json) : (T.assumed_ty, string) result = - combine_error_msgs js "assumed_ty_of_json" - (match js with - | `String "Box" -> Ok T.Box - | `String "Vec" -> Ok T.Vec - | `String "Option" -> Ok T.Option - | _ -> Error "") - -let type_id_of_json (js : json) : (T.type_id, string) result = - combine_error_msgs js "type_id_of_json" - (match js with - | `Assoc [ ("Adt", id) ] -> - let* id = T.TypeDeclId.id_of_json id in - Ok (T.AdtId id) - | `String "Tuple" -> Ok T.Tuple - | `Assoc [ ("Assumed", aty) ] -> - let* aty = assumed_ty_of_json aty in - Ok (T.Assumed aty) - | _ -> Error "") - -let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) : - ('r T.ty, string) result = - combine_error_msgs js "ty_of_json" - (match js with - | `Assoc [ ("Adt", `List [ id; regions; types ]) ] -> - let* id = type_id_of_json id in - let* regions = list_of_json r_of_json regions in - let* types = list_of_json (ty_of_json r_of_json) types in - (* Sanity check *) - (match id with T.Tuple -> assert (List.length regions = 0) | _ -> ()); - Ok (T.Adt (id, regions, types)) - | `Assoc [ ("TypeVar", `List [ id ]) ] -> - let* id = T.TypeVarId.id_of_json id in - Ok (T.TypeVar id) - | `String "Bool" -> Ok Bool - | `String "Char" -> Ok Char - | `String "`Never" -> Ok Never - | `Assoc [ ("Integer", `List [ int_ty ]) ] -> - let* int_ty = integer_type_of_json int_ty in - Ok (T.Integer int_ty) - | `String "Str" -> Ok Str - | `Assoc [ ("Array", `List [ ty ]) ] -> - let* ty = ty_of_json r_of_json ty in - Ok (T.Array ty) - | `Assoc [ ("Slice", `List [ ty ]) ] -> - let* ty = ty_of_json r_of_json ty in - Ok (T.Slice ty) - | `Assoc [ ("Ref", `List [ region; ty; ref_kind ]) ] -> - let* region = r_of_json region in - let* ty = ty_of_json r_of_json ty in - let* ref_kind = ref_kind_of_json ref_kind in - Ok (T.Ref (region, ty, ref_kind)) - | _ -> Error "") - -let sty_of_json (js : json) : (T.sty, string) result = - combine_error_msgs js "sty_of_json" (ty_of_json region_of_json js) - -let ety_of_json (js : json) : (T.ety, string) result = - combine_error_msgs js "ety_of_json" (ty_of_json erased_region_of_json js) - -let field_of_json (js : json) : (T.field, string) result = - combine_error_msgs js "field_of_json" - (match js with - | `Assoc [ ("name", name); ("ty", ty) ] -> - let* name = option_of_json string_of_json name in - let* ty = sty_of_json ty in - Ok { T.field_name = name; field_ty = ty } - | _ -> Error "") - -let variant_of_json (js : json) : (T.variant, string) result = - combine_error_msgs js "variant_of_json" - (match js with - | `Assoc [ ("name", name); ("fields", fields) ] -> - let* name = string_of_json name in - let* fields = list_of_json field_of_json fields in - Ok { T.variant_name = name; fields } - | _ -> Error "") - -let type_decl_kind_of_json (js : json) : (T.type_decl_kind, string) result = - combine_error_msgs js "type_decl_kind_of_json" - (match js with - | `Assoc [ ("Struct", fields) ] -> - let* fields = list_of_json field_of_json fields in - Ok (T.Struct fields) - | `Assoc [ ("Enum", variants) ] -> - let* variants = list_of_json variant_of_json variants in - Ok (T.Enum variants) - | _ -> Error "") - -let region_var_group_of_json (js : json) : (T.region_var_group, string) result = - combine_error_msgs js "region_var_group_of_json" - (match js with - | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] -> - let* id = T.RegionGroupId.id_of_json id in - let* regions = list_of_json T.RegionVarId.id_of_json regions in - let* parents = list_of_json T.RegionGroupId.id_of_json parents in - Ok { T.id; regions; parents } - | _ -> Error "") - -let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result - = - combine_error_msgs js "region_var_group_of_json" - (list_of_json region_var_group_of_json js) - -let type_decl_of_json (js : json) : (T.type_decl, string) result = - combine_error_msgs js "type_decl_of_json" - (match js with - | `Assoc - [ - ("def_id", def_id); - ("name", name); - ("region_params", region_params); - ("type_params", type_params); - ("regions_hierarchy", regions_hierarchy); - ("kind", kind); - ] -> - let* def_id = T.TypeDeclId.id_of_json def_id in - let* name = name_of_json name in - let* region_params = list_of_json region_var_of_json region_params in - let* type_params = list_of_json type_var_of_json type_params in - let* kind = type_decl_kind_of_json kind in - let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in - Ok - { - T.def_id; - name; - region_params; - type_params; - kind; - regions_hierarchy; - } - | _ -> Error "") - -let var_of_json (js : json) : (A.var, string) result = - combine_error_msgs js "var_of_json" - (match js with - | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] -> - let* index = V.VarId.id_of_json index in - let* name = string_option_of_json name in - let* var_ty = ety_of_json ty in - Ok { A.index; name; var_ty } - | _ -> Error "") - -let big_int_of_json (js : json) : (V.big_int, string) result = - combine_error_msgs js "big_int_of_json" - (match js with - | `Int i -> Ok (Z.of_int i) - | `String is -> Ok (Z.of_string is) - | _ -> Error "") - -(** Deserialize a [scalar_value] from JSON and **check the ranges**. - - Note that in practice we also check that the values are in range - in the interpreter functions. Still, it doesn't cost much to be - a bit conservative. - *) -let scalar_value_of_json (js : json) : (V.scalar_value, string) result = - let res = - combine_error_msgs js "scalar_value_of_json" - (match js with - | `Assoc [ ("Isize", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = Isize } - | `Assoc [ ("I8", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = I8 } - | `Assoc [ ("I16", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = I16 } - | `Assoc [ ("I32", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = I32 } - | `Assoc [ ("I64", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = I64 } - | `Assoc [ ("I128", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = I128 } - | `Assoc [ ("Usize", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = Usize } - | `Assoc [ ("U8", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = U8 } - | `Assoc [ ("U16", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = U16 } - | `Assoc [ ("U32", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = U32 } - | `Assoc [ ("U64", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = U64 } - | `Assoc [ ("U128", `List [ bi ]) ] -> - let* bi = big_int_of_json bi in - Ok { V.value = bi; int_ty = U128 } - | _ -> Error "") - in - match res with - | Error _ -> res - | Ok sv -> - if not (S.check_scalar_value_in_range sv) then ( - log#serror ("Scalar value not in range: " ^ V.show_scalar_value sv); - 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 - | `Assoc [ ("ProjAdt", `List [ def_id; opt_variant_id ]) ] -> - let* def_id = T.TypeDeclId.id_of_json def_id in - let* opt_variant_id = - option_of_json T.VariantId.id_of_json opt_variant_id - in - Ok (E.ProjAdt (def_id, opt_variant_id)) - | `Assoc [ ("ProjTuple", i) ] -> - let* i = int_of_json i in - Ok (E.ProjTuple i) - | `Assoc [ ("ProjOption", variant_id) ] -> - let* variant_id = T.VariantId.id_of_json variant_id in - Ok (E.ProjOption variant_id) - | _ -> Error "") - -let projection_elem_of_json (js : json) : (E.projection_elem, string) result = - combine_error_msgs js "projection_elem_of_json" - (match js with - | `String "Deref" -> Ok E.Deref - | `String "DerefBox" -> Ok E.DerefBox - | `Assoc [ ("Field", `List [ proj_kind; field_id ]) ] -> - let* proj_kind = field_proj_kind_of_json proj_kind in - let* field_id = T.FieldId.id_of_json field_id in - Ok (E.Field (proj_kind, field_id)) - | _ -> Error ("projection_elem_of_json failed on:" ^ show js)) - -let projection_of_json (js : json) : (E.projection, string) result = - combine_error_msgs js "projection_of_json" - (list_of_json projection_elem_of_json js) - -let place_of_json (js : json) : (E.place, string) result = - combine_error_msgs js "place_of_json" - (match js with - | `Assoc [ ("var_id", var_id); ("projection", projection) ] -> - let* var_id = V.VarId.id_of_json var_id in - let* projection = projection_of_json projection in - Ok { E.var_id; projection } - | _ -> Error "") - -let borrow_kind_of_json (js : json) : (E.borrow_kind, string) result = - match js with - | `String "Shared" -> Ok E.Shared - | `String "Mut" -> Ok E.Mut - | `String "TwoPhaseMut" -> Ok E.TwoPhaseMut - | _ -> Error ("borrow_kind_of_json failed on:" ^ show js) - -let unop_of_json (js : json) : (E.unop, string) result = - match js with - | `String "Not" -> Ok E.Not - | `String "Neg" -> Ok E.Neg - | _ -> Error ("unop_of_json failed on:" ^ show js) - -let binop_of_json (js : json) : (E.binop, string) result = - match js with - | `String "BitXor" -> Ok E.BitXor - | `String "BitAnd" -> Ok E.BitAnd - | `String "BitOr" -> Ok E.BitOr - | `String "Eq" -> Ok E.Eq - | `String "Lt" -> Ok E.Lt - | `String "Le" -> Ok E.Le - | `String "Ne" -> Ok E.Ne - | `String "Ge" -> Ok E.Ge - | `String "Gt" -> Ok E.Gt - | `String "Div" -> Ok E.Div - | `String "Rem" -> Ok E.Rem - | `String "Add" -> Ok E.Add - | `String "Sub" -> Ok E.Sub - | `String "Mul" -> Ok E.Mul - | `String "Shl" -> Ok E.Shl - | `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" - (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)) - | _ -> Error "") - -let operand_of_json (js : json) : (E.operand, string) result = - combine_error_msgs js "operand_of_json" - (match js with - | `Assoc [ ("Copy", place) ] -> - let* place = place_of_json place in - Ok (E.Copy place) - | `Assoc [ ("Move", place) ] -> - let* place = place_of_json place in - Ok (E.Move place) - | `Assoc [ ("Constant", `List [ ty; cv ]) ] -> - let* ty = ety_of_json ty in - let* cv = operand_constant_value_of_json cv in - Ok (E.Constant (ty, cv)) - | _ -> Error "") - -let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result = - combine_error_msgs js "operand_kind_of_json" - (match js with - | `String "AggregatedTuple" -> Ok E.AggregatedTuple - | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ] - -> - let* id = T.TypeDeclId.id_of_json id in - let* opt_variant_id = - option_of_json T.VariantId.id_of_json opt_variant_id - in - let* regions = list_of_json erased_region_of_json regions in - let* tys = list_of_json ety_of_json tys in - Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys)) - | _ -> Error "") - -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 in - Ok (E.Use op) - | `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] -> - let* place = place_of_json place in - let* borrow_kind = borrow_kind_of_json borrow_kind in - 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 - 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 - 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 - Ok (E.Aggregate (aggregate_kind, ops)) - | _ -> Error "") - -let assumed_fun_id_of_json (js : json) : (A.assumed_fun_id, string) result = - match js with - | `String "Replace" -> Ok A.Replace - | `String "BoxNew" -> Ok A.BoxNew - | `String "BoxDeref" -> Ok A.BoxDeref - | `String "BoxDerefMut" -> Ok A.BoxDerefMut - | `String "BoxFree" -> Ok A.BoxFree - | `String "VecNew" -> Ok A.VecNew - | `String "VecPush" -> Ok A.VecPush - | `String "VecInsert" -> Ok A.VecInsert - | `String "VecLen" -> Ok A.VecLen - | `String "VecIndex" -> Ok A.VecIndex - | `String "VecIndexMut" -> Ok A.VecIndexMut - | _ -> Error ("assumed_fun_id_of_json failed on:" ^ show js) - -let fun_id_of_json (js : json) : (A.fun_id, string) result = - combine_error_msgs js "fun_id_of_json" - (match js with - | `Assoc [ ("Local", id) ] -> - let* id = A.FunDeclId.id_of_json id in - Ok (A.Local 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 = - combine_error_msgs js "assertion_of_json" - (match js with - | `Assoc [ ("cond", cond); ("expected", expected) ] -> - let* cond = operand_of_json cond in - let* expected = bool_of_json expected in - Ok { A.cond; expected } - | _ -> Error "") - -let fun_sig_of_json (js : json) : (A.fun_sig, string) result = - combine_error_msgs js "fun_sig_of_json" - (match js with - | `Assoc - [ - ("region_params", region_params); - ("num_early_bound_regions", num_early_bound_regions); - ("regions_hierarchy", regions_hierarchy); - ("type_params", type_params); - ("inputs", inputs); - ("output", output); - ] -> - let* region_params = list_of_json region_var_of_json region_params in - let* num_early_bound_regions = int_of_json num_early_bound_regions in - let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in - let* type_params = list_of_json type_var_of_json type_params in - let* inputs = list_of_json sty_of_json inputs in - let* output = sty_of_json output in - Ok - { - A.region_params; - num_early_bound_regions; - regions_hierarchy; - type_params; - inputs; - output; - } - | _ -> Error "") - -let call_of_json (js : json) : (A.call, string) result = - combine_error_msgs js "call_of_json" - (match js with - | `Assoc - [ - ("func", func); - ("region_params", region_params); - ("type_params", type_params); - ("args", args); - ("dest", dest); - ] -> - let* func = fun_id_of_json func in - let* region_params = list_of_json erased_region_of_json region_params in - let* type_params = list_of_json ety_of_json type_params in - let* args = list_of_json operand_of_json args in - let* dest = place_of_json dest in - Ok { A.func; region_params; type_params; args; dest } - | _ -> Error "") - -let rec statement_of_json (js : json) : (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 - Ok (A.Assign (place, rvalue)) - | `Assoc [ ("FakeRead", place) ] -> - let* place = place_of_json place in - Ok (A.FakeRead place) - | `Assoc [ ("SetDiscriminant", `List [ place; variant_id ]) ] -> - let* place = place_of_json place in - let* variant_id = T.VariantId.id_of_json variant_id in - Ok (A.SetDiscriminant (place, variant_id)) - | `Assoc [ ("Drop", place) ] -> - let* place = place_of_json place in - Ok (A.Drop place) - | `Assoc [ ("Assert", assertion) ] -> - let* assertion = assertion_of_json assertion in - Ok (A.Assert assertion) - | `Assoc [ ("Call", call) ] -> - let* call = call_of_json call in - Ok (A.Call call) - | `String "Panic" -> Ok A.Panic - | `String "Return" -> Ok A.Return - | `Assoc [ ("Break", i) ] -> - let* i = int_of_json i in - Ok (A.Break i) - | `Assoc [ ("Continue", i) ] -> - let* i = int_of_json i in - 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 - 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 - Ok (A.Switch (op, tgt)) - | `Assoc [ ("Loop", st) ] -> - let* st = statement_of_json st in - Ok (A.Loop st) - | _ -> Error "") - -and switch_targets_of_json (js : json) : (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 - 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) - tgts - in - let* otherwise = statement_of_json otherwise in - Ok (A.SwitchInt (int_ty, tgts, otherwise)) - | _ -> Error "") - -let fun_decl_of_json (js : json) : (A.fun_decl, string) result = - combine_error_msgs js "fun_decl_of_json" - (match js with - | `Assoc - [ - ("def_id", def_id); - ("name", name); - ("signature", signature); - ("arg_count", arg_count); - ("locals", locals); - ("body", body); - ] -> - 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* 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 - Ok { A.def_id; name; signature; arg_count; locals; body } - | _ -> Error "") - -let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) - (js : json) : ('id M.g_declaration_group, string) result = - combine_error_msgs js "g_declaration_group_of_json" - (match js with - | `Assoc [ ("NonRec", `List [ id ]) ] -> - let* id = id_of_json id in - Ok (M.NonRec id) - | `Assoc [ ("Rec", `List [ ids ]) ] -> - let* ids = list_of_json id_of_json ids in - Ok (M.Rec ids) - | _ -> Error "") - -let type_declaration_group_of_json (js : json) : - (M.type_declaration_group, string) result = - combine_error_msgs js "type_declaration_group_of_json" - (g_declaration_group_of_json T.TypeDeclId.id_of_json js) - -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) - -let declaration_group_of_json (js : json) : (M.declaration_group, string) result - = - combine_error_msgs js "declaration_of_json" - (match js with - | `Assoc [ ("Type", `List [ decl ]) ] -> - let* decl = type_declaration_group_of_json decl in - Ok (M.Type decl) - | `Assoc [ ("Fun", `List [ decl ]) ] -> - let* decl = fun_declaration_group_of_json decl in - Ok (M.Fun decl) - | _ -> Error "") - -let llbc_module_of_json (js : json) : (M.llbc_module, string) result = - combine_error_msgs js "llbc_module_of_json" - (match js with - | `Assoc - [ - ("name", name); - ("declarations", declarations); - ("types", types); - ("functions", functions); - ] -> - 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 } - | _ -> Error "") diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml index f597cd27..149fb23d 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -186,3 +186,16 @@ type fun_decl = { * prevents us from computing this info in Charon (and thus exporting directly * it with the type/function defs), in which case we just have to implement special * treatment when deserializing, to move the info to a separate map. *) + +(* +type fun_body = { arg_count : int; locals : var list; body : statement } +[@@deriving show] + +type fun_decl = { + def_id : FunDeclId.id; + name : fun_name; + signature : fun_sig; + body : fun_body option; +} +[@@deriving show] +*) diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml new file mode 100644 index 00000000..e293b030 --- /dev/null +++ b/src/LlbcOfJson.ml @@ -0,0 +1,682 @@ +(** Functions to load CFIM ASTs from json. + + Initially, we used `ppx_derive_yojson` to automate this. + However, `ppx_derive_yojson` expects formatting to be slightly + different from what `serde_rs` generates (because it uses [Yojson.Safe.t] + and not [Yojson.Basic.t]). + + TODO: we should check all that the integer values are in the proper range + *) + +open Yojson.Basic +open Names +open OfJsonBasic +module T = Types +module V = Values +module S = Scalars +module M = Modules +module E = Expressions +module A = LlbcAst + +(* The default logger *) +let log = Logging.llbc_of_json_logger + +let path_elem_of_json (js : json) : (path_elem, string) result = + combine_error_msgs js "path_elem_of_json" + (match js with + | `Assoc [ ("Ident", name) ] -> + let* name = string_of_json name in + Ok (Ident name) + | `Assoc [ ("Disambiguator", d) ] -> + let* d = Disambiguator.id_of_json d in + Ok (Disambiguator d) + | _ -> Error "") + +let name_of_json (js : json) : (name, string) result = + combine_error_msgs js "name_of_json" (list_of_json path_elem_of_json js) + +let fun_name_of_json (js : json) : (fun_name, string) result = + combine_error_msgs js "fun_name_of_json" (name_of_json js) + +let type_var_of_json (js : json) : (T.type_var, string) result = + combine_error_msgs js "type_var_of_json" + (match js with + | `Assoc [ ("index", index); ("name", name) ] -> + let* index = T.TypeVarId.id_of_json index in + let* name = string_of_json name in + Ok { T.index; name } + | _ -> Error "") + +let region_var_of_json (js : json) : (T.region_var, string) result = + combine_error_msgs js "region_var_of_json" + (match js with + | `Assoc [ ("index", index); ("name", name) ] -> + let* index = T.RegionVarId.id_of_json index in + let* name = string_option_of_json name in + Ok { T.index; name } + | _ -> Error "") + +let region_of_json (js : json) : (T.RegionVarId.id T.region, string) result = + combine_error_msgs js "region_of_json" + (match js with + | `String "Static" -> Ok T.Static + | `Assoc [ ("Var", rid) ] -> + let* rid = T.RegionVarId.id_of_json rid in + Ok (T.Var rid) + | _ -> Error "") + +let erased_region_of_json (js : json) : (T.erased_region, string) result = + combine_error_msgs js "erased_region_of_json" + (match js with `String "Erased" -> Ok T.Erased | _ -> Error "") + +let integer_type_of_json (js : json) : (T.integer_type, string) result = + match js with + | `String "Isize" -> Ok T.Isize + | `String "I8" -> Ok T.I8 + | `String "I16" -> Ok T.I16 + | `String "I32" -> Ok T.I32 + | `String "I64" -> Ok T.I64 + | `String "I128" -> Ok T.I128 + | `String "Usize" -> Ok T.Usize + | `String "U8" -> Ok T.U8 + | `String "U16" -> Ok T.U16 + | `String "U32" -> Ok T.U32 + | `String "U64" -> Ok T.U64 + | `String "U128" -> Ok T.U128 + | _ -> Error ("integer_type_of_json failed on: " ^ show js) + +let ref_kind_of_json (js : json) : (T.ref_kind, string) result = + match js with + | `String "Mut" -> Ok T.Mut + | `String "Shared" -> Ok T.Shared + | _ -> Error ("ref_kind_of_json failed on: " ^ show js) + +let assumed_ty_of_json (js : json) : (T.assumed_ty, string) result = + combine_error_msgs js "assumed_ty_of_json" + (match js with + | `String "Box" -> Ok T.Box + | `String "Vec" -> Ok T.Vec + | `String "Option" -> Ok T.Option + | _ -> Error "") + +let type_id_of_json (js : json) : (T.type_id, string) result = + combine_error_msgs js "type_id_of_json" + (match js with + | `Assoc [ ("Adt", id) ] -> + let* id = T.TypeDeclId.id_of_json id in + Ok (T.AdtId id) + | `String "Tuple" -> Ok T.Tuple + | `Assoc [ ("Assumed", aty) ] -> + let* aty = assumed_ty_of_json aty in + Ok (T.Assumed aty) + | _ -> Error "") + +let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) : + ('r T.ty, string) result = + combine_error_msgs js "ty_of_json" + (match js with + | `Assoc [ ("Adt", `List [ id; regions; types ]) ] -> + let* id = type_id_of_json id in + let* regions = list_of_json r_of_json regions in + let* types = list_of_json (ty_of_json r_of_json) types in + (* Sanity check *) + (match id with T.Tuple -> assert (List.length regions = 0) | _ -> ()); + Ok (T.Adt (id, regions, types)) + | `Assoc [ ("TypeVar", `List [ id ]) ] -> + let* id = T.TypeVarId.id_of_json id in + Ok (T.TypeVar id) + | `String "Bool" -> Ok Bool + | `String "Char" -> Ok Char + | `String "`Never" -> Ok Never + | `Assoc [ ("Integer", `List [ int_ty ]) ] -> + let* int_ty = integer_type_of_json int_ty in + Ok (T.Integer int_ty) + | `String "Str" -> Ok Str + | `Assoc [ ("Array", `List [ ty ]) ] -> + let* ty = ty_of_json r_of_json ty in + Ok (T.Array ty) + | `Assoc [ ("Slice", `List [ ty ]) ] -> + let* ty = ty_of_json r_of_json ty in + Ok (T.Slice ty) + | `Assoc [ ("Ref", `List [ region; ty; ref_kind ]) ] -> + let* region = r_of_json region in + let* ty = ty_of_json r_of_json ty in + let* ref_kind = ref_kind_of_json ref_kind in + Ok (T.Ref (region, ty, ref_kind)) + | _ -> Error "") + +let sty_of_json (js : json) : (T.sty, string) result = + combine_error_msgs js "sty_of_json" (ty_of_json region_of_json js) + +let ety_of_json (js : json) : (T.ety, string) result = + combine_error_msgs js "ety_of_json" (ty_of_json erased_region_of_json js) + +let field_of_json (js : json) : (T.field, string) result = + combine_error_msgs js "field_of_json" + (match js with + | `Assoc [ ("name", name); ("ty", ty) ] -> + let* name = option_of_json string_of_json name in + let* ty = sty_of_json ty in + Ok { T.field_name = name; field_ty = ty } + | _ -> Error "") + +let variant_of_json (js : json) : (T.variant, string) result = + combine_error_msgs js "variant_of_json" + (match js with + | `Assoc [ ("name", name); ("fields", fields) ] -> + let* name = string_of_json name in + let* fields = list_of_json field_of_json fields in + Ok { T.variant_name = name; fields } + | _ -> Error "") + +let type_decl_kind_of_json (js : json) : (T.type_decl_kind, string) result = + combine_error_msgs js "type_decl_kind_of_json" + (match js with + | `Assoc [ ("Struct", fields) ] -> + let* fields = list_of_json field_of_json fields in + Ok (T.Struct fields) + | `Assoc [ ("Enum", variants) ] -> + let* variants = list_of_json variant_of_json variants in + Ok (T.Enum variants) + | _ -> Error "") + +let region_var_group_of_json (js : json) : (T.region_var_group, string) result = + combine_error_msgs js "region_var_group_of_json" + (match js with + | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] -> + let* id = T.RegionGroupId.id_of_json id in + let* regions = list_of_json T.RegionVarId.id_of_json regions in + let* parents = list_of_json T.RegionGroupId.id_of_json parents in + Ok { T.id; regions; parents } + | _ -> Error "") + +let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result + = + combine_error_msgs js "region_var_group_of_json" + (list_of_json region_var_group_of_json js) + +let type_decl_of_json (js : json) : (T.type_decl, string) result = + combine_error_msgs js "type_decl_of_json" + (match js with + | `Assoc + [ + ("def_id", def_id); + ("name", name); + ("region_params", region_params); + ("type_params", type_params); + ("regions_hierarchy", regions_hierarchy); + ("kind", kind); + ] -> + let* def_id = T.TypeDeclId.id_of_json def_id in + let* name = name_of_json name in + let* region_params = list_of_json region_var_of_json region_params in + let* type_params = list_of_json type_var_of_json type_params in + let* kind = type_decl_kind_of_json kind in + let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in + Ok + { + T.def_id; + name; + region_params; + type_params; + kind; + regions_hierarchy; + } + | _ -> Error "") + +let var_of_json (js : json) : (A.var, string) result = + combine_error_msgs js "var_of_json" + (match js with + | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] -> + let* index = V.VarId.id_of_json index in + let* name = string_option_of_json name in + let* var_ty = ety_of_json ty in + Ok { A.index; name; var_ty } + | _ -> Error "") + +let big_int_of_json (js : json) : (V.big_int, string) result = + combine_error_msgs js "big_int_of_json" + (match js with + | `Int i -> Ok (Z.of_int i) + | `String is -> Ok (Z.of_string is) + | _ -> Error "") + +(** Deserialize a [scalar_value] from JSON and **check the ranges**. + + Note that in practice we also check that the values are in range + in the interpreter functions. Still, it doesn't cost much to be + a bit conservative. + *) +let scalar_value_of_json (js : json) : (V.scalar_value, string) result = + let res = + combine_error_msgs js "scalar_value_of_json" + (match js with + | `Assoc [ ("Isize", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = Isize } + | `Assoc [ ("I8", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = I8 } + | `Assoc [ ("I16", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = I16 } + | `Assoc [ ("I32", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = I32 } + | `Assoc [ ("I64", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = I64 } + | `Assoc [ ("I128", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = I128 } + | `Assoc [ ("Usize", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = Usize } + | `Assoc [ ("U8", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = U8 } + | `Assoc [ ("U16", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = U16 } + | `Assoc [ ("U32", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = U32 } + | `Assoc [ ("U64", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = U64 } + | `Assoc [ ("U128", `List [ bi ]) ] -> + let* bi = big_int_of_json bi in + Ok { V.value = bi; int_ty = U128 } + | _ -> Error "") + in + match res with + | Error _ -> res + | Ok sv -> + if not (S.check_scalar_value_in_range sv) then ( + log#serror ("Scalar value not in range: " ^ V.show_scalar_value sv); + 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 + | `Assoc [ ("ProjAdt", `List [ def_id; opt_variant_id ]) ] -> + let* def_id = T.TypeDeclId.id_of_json def_id in + let* opt_variant_id = + option_of_json T.VariantId.id_of_json opt_variant_id + in + Ok (E.ProjAdt (def_id, opt_variant_id)) + | `Assoc [ ("ProjTuple", i) ] -> + let* i = int_of_json i in + Ok (E.ProjTuple i) + | `Assoc [ ("ProjOption", variant_id) ] -> + let* variant_id = T.VariantId.id_of_json variant_id in + Ok (E.ProjOption variant_id) + | _ -> Error "") + +let projection_elem_of_json (js : json) : (E.projection_elem, string) result = + combine_error_msgs js "projection_elem_of_json" + (match js with + | `String "Deref" -> Ok E.Deref + | `String "DerefBox" -> Ok E.DerefBox + | `Assoc [ ("Field", `List [ proj_kind; field_id ]) ] -> + let* proj_kind = field_proj_kind_of_json proj_kind in + let* field_id = T.FieldId.id_of_json field_id in + Ok (E.Field (proj_kind, field_id)) + | _ -> Error ("projection_elem_of_json failed on:" ^ show js)) + +let projection_of_json (js : json) : (E.projection, string) result = + combine_error_msgs js "projection_of_json" + (list_of_json projection_elem_of_json js) + +let place_of_json (js : json) : (E.place, string) result = + combine_error_msgs js "place_of_json" + (match js with + | `Assoc [ ("var_id", var_id); ("projection", projection) ] -> + let* var_id = V.VarId.id_of_json var_id in + let* projection = projection_of_json projection in + Ok { E.var_id; projection } + | _ -> Error "") + +let borrow_kind_of_json (js : json) : (E.borrow_kind, string) result = + match js with + | `String "Shared" -> Ok E.Shared + | `String "Mut" -> Ok E.Mut + | `String "TwoPhaseMut" -> Ok E.TwoPhaseMut + | _ -> Error ("borrow_kind_of_json failed on:" ^ show js) + +let unop_of_json (js : json) : (E.unop, string) result = + match js with + | `String "Not" -> Ok E.Not + | `String "Neg" -> Ok E.Neg + | _ -> Error ("unop_of_json failed on:" ^ show js) + +let binop_of_json (js : json) : (E.binop, string) result = + match js with + | `String "BitXor" -> Ok E.BitXor + | `String "BitAnd" -> Ok E.BitAnd + | `String "BitOr" -> Ok E.BitOr + | `String "Eq" -> Ok E.Eq + | `String "Lt" -> Ok E.Lt + | `String "Le" -> Ok E.Le + | `String "Ne" -> Ok E.Ne + | `String "Ge" -> Ok E.Ge + | `String "Gt" -> Ok E.Gt + | `String "Div" -> Ok E.Div + | `String "Rem" -> Ok E.Rem + | `String "Add" -> Ok E.Add + | `String "Sub" -> Ok E.Sub + | `String "Mul" -> Ok E.Mul + | `String "Shl" -> Ok E.Shl + | `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" + (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)) + | _ -> Error "") + +let operand_of_json (js : json) : (E.operand, string) result = + combine_error_msgs js "operand_of_json" + (match js with + | `Assoc [ ("Copy", place) ] -> + let* place = place_of_json place in + Ok (E.Copy place) + | `Assoc [ ("Move", place) ] -> + let* place = place_of_json place in + Ok (E.Move place) + | `Assoc [ ("Constant", `List [ ty; cv ]) ] -> + let* ty = ety_of_json ty in + let* cv = operand_constant_value_of_json cv in + Ok (E.Constant (ty, cv)) + | _ -> Error "") + +let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result = + combine_error_msgs js "operand_kind_of_json" + (match js with + | `String "AggregatedTuple" -> Ok E.AggregatedTuple + | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ] + -> + let* id = T.TypeDeclId.id_of_json id in + let* opt_variant_id = + option_of_json T.VariantId.id_of_json opt_variant_id + in + let* regions = list_of_json erased_region_of_json regions in + let* tys = list_of_json ety_of_json tys in + Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys)) + | _ -> Error "") + +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 in + Ok (E.Use op) + | `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] -> + let* place = place_of_json place in + let* borrow_kind = borrow_kind_of_json borrow_kind in + 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 + 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 + 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 + Ok (E.Aggregate (aggregate_kind, ops)) + | _ -> Error "") + +let assumed_fun_id_of_json (js : json) : (A.assumed_fun_id, string) result = + match js with + | `String "Replace" -> Ok A.Replace + | `String "BoxNew" -> Ok A.BoxNew + | `String "BoxDeref" -> Ok A.BoxDeref + | `String "BoxDerefMut" -> Ok A.BoxDerefMut + | `String "BoxFree" -> Ok A.BoxFree + | `String "VecNew" -> Ok A.VecNew + | `String "VecPush" -> Ok A.VecPush + | `String "VecInsert" -> Ok A.VecInsert + | `String "VecLen" -> Ok A.VecLen + | `String "VecIndex" -> Ok A.VecIndex + | `String "VecIndexMut" -> Ok A.VecIndexMut + | _ -> Error ("assumed_fun_id_of_json failed on:" ^ show js) + +let fun_id_of_json (js : json) : (A.fun_id, string) result = + combine_error_msgs js "fun_id_of_json" + (match js with + | `Assoc [ ("Local", id) ] -> + let* id = A.FunDeclId.id_of_json id in + Ok (A.Local 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 = + combine_error_msgs js "assertion_of_json" + (match js with + | `Assoc [ ("cond", cond); ("expected", expected) ] -> + let* cond = operand_of_json cond in + let* expected = bool_of_json expected in + Ok { A.cond; expected } + | _ -> Error "") + +let fun_sig_of_json (js : json) : (A.fun_sig, string) result = + combine_error_msgs js "fun_sig_of_json" + (match js with + | `Assoc + [ + ("region_params", region_params); + ("num_early_bound_regions", num_early_bound_regions); + ("regions_hierarchy", regions_hierarchy); + ("type_params", type_params); + ("inputs", inputs); + ("output", output); + ] -> + let* region_params = list_of_json region_var_of_json region_params in + let* num_early_bound_regions = int_of_json num_early_bound_regions in + let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in + let* type_params = list_of_json type_var_of_json type_params in + let* inputs = list_of_json sty_of_json inputs in + let* output = sty_of_json output in + Ok + { + A.region_params; + num_early_bound_regions; + regions_hierarchy; + type_params; + inputs; + output; + } + | _ -> Error "") + +let call_of_json (js : json) : (A.call, string) result = + combine_error_msgs js "call_of_json" + (match js with + | `Assoc + [ + ("func", func); + ("region_params", region_params); + ("type_params", type_params); + ("args", args); + ("dest", dest); + ] -> + let* func = fun_id_of_json func in + let* region_params = list_of_json erased_region_of_json region_params in + let* type_params = list_of_json ety_of_json type_params in + let* args = list_of_json operand_of_json args in + let* dest = place_of_json dest in + Ok { A.func; region_params; type_params; args; dest } + | _ -> Error "") + +let rec statement_of_json (js : json) : (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 + Ok (A.Assign (place, rvalue)) + | `Assoc [ ("FakeRead", place) ] -> + let* place = place_of_json place in + Ok (A.FakeRead place) + | `Assoc [ ("SetDiscriminant", `List [ place; variant_id ]) ] -> + let* place = place_of_json place in + let* variant_id = T.VariantId.id_of_json variant_id in + Ok (A.SetDiscriminant (place, variant_id)) + | `Assoc [ ("Drop", place) ] -> + let* place = place_of_json place in + Ok (A.Drop place) + | `Assoc [ ("Assert", assertion) ] -> + let* assertion = assertion_of_json assertion in + Ok (A.Assert assertion) + | `Assoc [ ("Call", call) ] -> + let* call = call_of_json call in + Ok (A.Call call) + | `String "Panic" -> Ok A.Panic + | `String "Return" -> Ok A.Return + | `Assoc [ ("Break", i) ] -> + let* i = int_of_json i in + Ok (A.Break i) + | `Assoc [ ("Continue", i) ] -> + let* i = int_of_json i in + 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 + 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 + Ok (A.Switch (op, tgt)) + | `Assoc [ ("Loop", st) ] -> + let* st = statement_of_json st in + Ok (A.Loop st) + | _ -> Error "") + +and switch_targets_of_json (js : json) : (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 + 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) + tgts + in + let* otherwise = statement_of_json otherwise in + Ok (A.SwitchInt (int_ty, tgts, otherwise)) + | _ -> Error "") + +let fun_decl_of_json (js : json) : (A.fun_decl, string) result = + combine_error_msgs js "fun_decl_of_json" + (match js with + | `Assoc + [ + ("def_id", def_id); + ("name", name); + ("signature", signature); + ("arg_count", arg_count); + ("locals", locals); + ("body", body); + ] -> + 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* 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 + Ok { A.def_id; name; signature; arg_count; locals; body } + | _ -> Error "") + +let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) + (js : json) : ('id M.g_declaration_group, string) result = + combine_error_msgs js "g_declaration_group_of_json" + (match js with + | `Assoc [ ("NonRec", `List [ id ]) ] -> + let* id = id_of_json id in + Ok (M.NonRec id) + | `Assoc [ ("Rec", `List [ ids ]) ] -> + let* ids = list_of_json id_of_json ids in + Ok (M.Rec ids) + | _ -> Error "") + +let type_declaration_group_of_json (js : json) : + (M.type_declaration_group, string) result = + combine_error_msgs js "type_declaration_group_of_json" + (g_declaration_group_of_json T.TypeDeclId.id_of_json js) + +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) + +let declaration_group_of_json (js : json) : (M.declaration_group, string) result + = + combine_error_msgs js "declaration_of_json" + (match js with + | `Assoc [ ("Type", `List [ decl ]) ] -> + let* decl = type_declaration_group_of_json decl in + Ok (M.Type decl) + | `Assoc [ ("Fun", `List [ decl ]) ] -> + let* decl = fun_declaration_group_of_json decl in + Ok (M.Fun decl) + | _ -> Error "") + +let llbc_module_of_json (js : json) : (M.llbc_module, string) result = + combine_error_msgs js "llbc_module_of_json" + (match js with + | `Assoc + [ + ("name", name); + ("declarations", declarations); + ("types", types); + ("functions", functions); + ] -> + 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 } + | _ -> Error "") diff --git a/src/Logging.ml b/src/Logging.ml index 7f4152a5..6dca854c 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -9,8 +9,8 @@ let main_log = L.get_logger "MainLogger" (** Below, we create subgloggers for various submodules, so that we can precisely toggle logging on/off, depending on which information we need *) -(** Logger for CfimOfJson *) -let llbc_of_json_logger = L.get_logger "MainLogger.CfimOfJson" +(** Logger for LlbcOfJson *) +let llbc_of_json_logger = L.get_logger "MainLogger.LlbcOfJson" (** Logger for PrePasses *) let pre_passes_log = L.get_logger "MainLogger.PrePasses" diff --git a/src/main.ml b/src/main.ml index 4740f14c..577ba666 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,4 +1,4 @@ -open CfimOfJson +open LlbcOfJson open Logging open Print module T = Types -- cgit v1.2.3