From 80c172c3ca62cccd2fa2394ca27d2de4dffb6f4b Mon Sep 17 00:00:00 2001 From: jjcnn <38888011+jjcnn@users.noreply.github.com> Date: Wed, 5 Oct 2022 10:40:23 +0200 Subject: [PATCH] Remove non-validating json parser (#1177) * Removed flags for json validation * fmt * Improve JSON parser error message * Reenabling json validation, which was disabled by default by accident * Remove gen_parser from JSONParser, move unused helpers to Disambiguator.ml * fmt --- src/base/GlobalConfig.ml | 6 +- src/base/GlobalConfig.mli | 2 - src/base/JSON.ml | 3 +- src/base/JSONParser.ml | 195 -------------------------------------- src/base/JSONParser.mli | 25 ----- src/base/RunnerUtil.ml | 5 - src/eval/Disambiguator.ml | 31 +++++- src/eval/RunnerCLI.ml | 4 - 8 files changed, 30 insertions(+), 241 deletions(-) diff --git a/src/base/GlobalConfig.ml b/src/base/GlobalConfig.ml index 7048ac100..6507be1d5 100644 --- a/src/base/GlobalConfig.ml +++ b/src/base/GlobalConfig.ml @@ -75,9 +75,6 @@ let get_pp_lit () = !pp_lit let json_errors = ref false let set_use_json_errors b = json_errors := b let use_json_errors () = !json_errors -let validate_json_b = ref false -let set_validate_json b = validate_json_b := b -let validate_json () = !validate_json_b module StdlibTracker = struct (* Environment variable: where to look for stdlib. @@ -139,5 +136,4 @@ let reset () = trace_level := Trace_None; trace_file := ""; pp_lit := true; - json_errors := false; - validate_json_b := false + json_errors := false diff --git a/src/base/GlobalConfig.mli b/src/base/GlobalConfig.mli index ff13ec964..0875c2cd5 100644 --- a/src/base/GlobalConfig.mli +++ b/src/base/GlobalConfig.mli @@ -39,8 +39,6 @@ val set_use_json_errors : bool -> unit val use_json_errors : unit -> bool (* Should input JSONs be validated? *) -val set_validate_json : bool -> unit -val validate_json : unit -> bool val reset : unit -> unit module StdlibTracker : sig diff --git a/src/base/JSON.ml b/src/base/JSON.ml index 592622b8b..6de10a65b 100644 --- a/src/base/JSON.ml +++ b/src/base/JSON.ml @@ -276,8 +276,7 @@ let rec jobj_to_statevar json = else let tstring = member_exn "type" json |> to_string_exn in let t = parse_typ_exn tstring in - if GlobalConfig.validate_json () then ThisContr (n, t, json_to_lit_exn t v) - else ThisContr (n, t, JSONParser.parse_json t v) + ThisContr (n, t, json_to_lit_exn t v) (****************************************************************) (* JSON printing *) diff --git a/src/base/JSONParser.ml b/src/base/JSONParser.ml index 02ac8c715..242c62356 100644 --- a/src/base/JSONParser.ml +++ b/src/base/JSONParser.ml @@ -17,7 +17,6 @@ *) (* A fast JSON parser for states that performs no validations. *) - open Core open Yojson open ErrorUtils @@ -73,197 +72,3 @@ let lookup_adt_name_exn name = match DataTypeDictionary.lookup_name (JSONIdentifier.get_id name) with | Error emsg -> raise (Invalid_json emsg) | Ok s -> s - -(*************************************) -(*********** ADT parsers *************) -(*************************************) - -type adt_parser_entry = - | Incomplete (* Parser not completely constructed. *) - | Parser of (Basic.t -> JSONLiteral.t) - -let adt_parsers = - let open Caml in - let ht : (string, adt_parser_entry) Hashtbl.t = Hashtbl.create 10 in - ht - -let add_adt_parser adt_name parser = - let open Caml in - let _ = Hashtbl.replace adt_parsers adt_name parser in - () - -let lookup_adt_parser_opt adt_name = - let open Caml in - Hashtbl.find_opt adt_parsers adt_name - -let lookup_adt_parser adt_name = - let open Caml in - match Hashtbl.find_opt adt_parsers adt_name with - | None -> raise (mk_invalid_json ~kind:"ADT not found" ~inst:adt_name) - | Some p -> p - -(*************************************) -(******** Parser Generator ***********) -(*************************************) - -(* Generate a parser. *) -let gen_parser (t' : JSONType.t) : Basic.t -> JSONLiteral.t = - let open Basic in - let open TUType in - let open TULiteral in - let rec recurser t = - match t with - | PrimType pt -> ( - match pt with - | String_typ -> fun j -> StringLit (to_string_exn j) - | Bnum_typ -> fun j -> BNum (Literal.bnum_create_exn (to_string_exn j)) - | Bystr_typ -> fun j -> ByStr (Bystr.parse_hex (to_string_exn j)) - | Bystrx_typ _ -> fun j -> ByStrX (Bystrx.parse_hex (to_string_exn j)) - | Int_typ Bits32 -> - fun j -> IntLit (Int32L (Int32.of_string (to_string_exn j))) - | Int_typ Bits64 -> - fun j -> IntLit (Int64L (Int64.of_string (to_string_exn j))) - | Int_typ Bits128 -> - fun j -> - IntLit (Int128L (Stdint.Int128.of_string (to_string_exn j))) - | Int_typ Bits256 -> - fun j -> - IntLit (Int256L (Integer256.Int256.of_string (to_string_exn j))) - | Uint_typ Bits32 -> - fun j -> - UintLit (Uint32L (Stdint.Uint32.of_string (to_string_exn j))) - | Uint_typ Bits64 -> - fun j -> - UintLit (Uint64L (Stdint.Uint64.of_string (to_string_exn j))) - | Uint_typ Bits128 -> - fun j -> - UintLit (Uint128L (Stdint.Uint128.of_string (to_string_exn j))) - | Uint_typ Bits256 -> - fun j -> - UintLit - (Uint256L (Integer256.Uint256.of_string (to_string_exn j))) - | _ -> raise (mk_invalid_json ~kind:"Invalid primitive type" ?inst:None) - ) - | MapType (kt, vt) -> ( - let kp = recurser kt in - let vp = recurser vt in - fun j -> - match j with - | `List jlist -> - let m = Caml.Hashtbl.create (List.length jlist) in - List.iter jlist ~f:(fun first -> - let kjson = member_exn "key" first in - let keylit = kp kjson in - let vjson = member_exn "val" first in - let vallit = vp vjson in - Caml.Hashtbl.replace m keylit vallit); - Map ((kt, vt), m) - | _ -> raise (mk_invalid_json ~kind:"Invalid map in JSON" ?inst:None)) - | ADT (name, tlist) -> - (* Add a dummy entry for "t" in our table, to prevent recursive calls. *) - let _ = add_adt_parser (pp_typ t) Incomplete in - - let a = lookup_adt_name_exn name in - (* Build a parser for each constructor of this ADT. *) - let cn_parsers = - List.fold a.tconstr ~init:(AssocDictionary.make_dict ()) - ~f:(fun maps cn -> - let tmap = constr_pattern_arg_types_exn t cn.cname in - let arg_parsers = - List.map tmap ~f:(fun t -> - match lookup_adt_parser_opt (pp_typ t) with - | Some _ -> - (* Lazy lookup, to avoid using dummy parsers set above. *) - fun () -> lookup_adt_parser (pp_typ t) - | None -> - let p = recurser t in - fun () -> Parser p) - in - let parser j = - match j with - | `Assoc _ -> - let arguments = member_exn "arguments" j |> Util.to_list in - if List.length tmap <> List.length arguments then - raise - (mk_invalid_json - ~kind:"Invalid arguments to ADT in JSON" ?inst:None) - else - let arg_lits = - List.map2_exn arg_parsers arguments ~f:(fun p a -> - (* Apply thunk, and then apply to argument *) - match p () with - | Incomplete -> - raise - (mk_invalid_json - ~kind: - "Attempt to call an incomplete JSON \ - parser" - ?inst:None) - | Parser p' -> p' a) - in - ADTValue (cn.cname, tlist, arg_lits) - | `List vli -> - (* We make an exception for Lists, allowing them to be stored flatly. *) - if - not - (Datatypes.is_list_adt_name - (JSONIdentifier.get_id name)) - then - raise - (mk_invalid_json - ~kind: - "ADT value is a JSON array, but type is not List" - ?inst:None) - else - let eparser = List.nth_exn arg_parsers 0 in - let eparser' = - match eparser () with - | Incomplete -> - raise - (mk_invalid_json - ~kind: - "Attempt to call an incomplete JSON parser" - ?inst:None) - | Parser p' -> p' - in - let etyp = List.nth_exn tmap 0 in - List.fold_right vli - ~f:(fun vl acc -> - (* Apply eparser thunk, and then apply to argument *) - build_cons_lit (eparser' vl) etyp acc) - ~init:(build_nil_lit etyp) - | _ -> - raise - (mk_invalid_json ~kind:"Invalid ADT in JSON" ?inst:None) - in - AssocDictionary.insert (JSONName.as_string cn.cname) parser maps) - in - let adt_parser cn_parsers j = - let cn = - match j with - | `Assoc _ -> member_exn "constructor" j |> to_string_exn - | `List _ -> - "Cons" (* for efficiency, Lists can be stored flatly. *) - | _ -> - raise - (mk_invalid_json ~kind:"Invalid construct in ADT JSON" - ?inst:None) - in - match AssocDictionary.lookup cn cn_parsers with - | Some parser -> parser j - | None -> - raise - (mk_invalid_json ~kind:"Unknown constructor in ADT JSON" - ~inst:cn) - in - (* Create parser *) - let p = adt_parser cn_parsers in - (* Add parser to hashtable *) - let _ = add_adt_parser (pp_typ t) (Parser p) in - (* Return parser *) - p - | _ -> raise (mk_invalid_json ~kind:"Invalid type" ?inst:None) - in - recurser t' - -let parse_json t j = (gen_parser t) j diff --git a/src/base/JSONParser.mli b/src/base/JSONParser.mli index e2088aabf..7332822b0 100644 --- a/src/base/JSONParser.mli +++ b/src/base/JSONParser.mli @@ -16,7 +16,6 @@ scilla. If not, see . *) -open Core open Yojson module JSONTypeUtilities = TypeUtil.TypeUtilities module JSONIdentifier = TypeUtil.TUIdentifier @@ -42,27 +41,3 @@ val constr_pattern_arg_types_exn : JSONType.t -> JSONName.t -> JSONType.t list (* Wrapper for DataTypeDictionary.lookup_name *) val lookup_adt_name_exn : 'a JSONIdentifier.t -> Datatypes.adt - -(*************************************) -(*********** ADT parsers *************) -(*************************************) - -type adt_parser_entry = Incomplete | Parser of (Basic.t -> JSONLiteral.t) - -(* ADT parsers table *) -val adt_parsers : (string, adt_parser_entry) Caml.Hashtbl.t - -(* Put an ADT parser to the table *) -val add_adt_parser : string -> adt_parser_entry -> unit - -(* Safe lookup of an ADT parser in the table *) -val lookup_adt_parser_opt : string -> adt_parser_entry option - -(* Look up an ADT parser in the table, throws if not found *) -val lookup_adt_parser : string -> adt_parser_entry - -(* Generate a parser *) -val gen_parser : JSONType.t -> Basic.t -> JSONLiteral.t - -(* Parse JSON *) -val parse_json : JSONType.t -> Basic.t -> JSONLiteral.t diff --git a/src/base/RunnerUtil.ml b/src/base/RunnerUtil.ml index c0f156a9c..c1463884b 100644 --- a/src/base/RunnerUtil.ml +++ b/src/base/RunnerUtil.ml @@ -217,7 +217,6 @@ let parse_cli args ~exe_name = let r_type_info = ref false in let r_cf = ref false in let r_cf_token_fields = ref [] in - let r_validate_json = ref true in let r_disable_analy_warn = ref false in let r_dump_callgraph = ref false in let r_dump_callgraph_stdout = ref false in @@ -276,9 +275,6 @@ let parse_cli args ~exe_name = | "verbose" -> GlobalConfig.set_debug_level Debug_Verbose | _ -> raise (ErrorUtils.FatalError "Invalid debug log level") ), "Set debug logging level" ); - ( "-disable-validate-json", - Arg.Unit (fun () -> r_validate_json := false), - "Disable validation of input JSONs" ); ( "-disable-developer-warnings", Arg.Unit (fun () -> r_disable_analy_warn := true), "Disable analyses' warnings" ); @@ -319,7 +315,6 @@ let parse_cli args ~exe_name = in if not @@ List.is_empty !r_cf_token_fields then r_cf := true; GlobalConfig.set_use_json_errors !r_json_errors; - GlobalConfig.set_validate_json !r_validate_json; { input_file = !r_input_file; stdlib_dirs = !r_stdlib_dir; diff --git a/src/eval/Disambiguator.ml b/src/eval/Disambiguator.ml index a6ee0d610..f14242069 100644 --- a/src/eval/Disambiguator.ml +++ b/src/eval/Disambiguator.ml @@ -262,9 +262,34 @@ let member_exn = JSONParser.member_exn let to_string_exn = JSONParser.to_string_exn let constr_pattern_arg_types_exn = JSONParser.constr_pattern_arg_types_exn let lookup_adt_name_exn = JSONParser.lookup_adt_name_exn -let add_adt_parser = JSONParser.add_adt_parser -let lookup_adt_parser_opt = JSONParser.lookup_adt_parser_opt -let lookup_adt_parser = JSONParser.lookup_adt_parser + +(*************************************) +(*********** ADT parsers *************) +(*************************************) + +type adt_parser_entry = + | Incomplete (* Parser not completely constructed. *) + | Parser of (Basic.t -> OutputLiteral.t) + +let adt_parsers = + let open Caml in + let ht : (string, adt_parser_entry) Hashtbl.t = Hashtbl.create 10 in + ht + +let add_adt_parser adt_name parser = + let open Caml in + let _ = Hashtbl.replace adt_parsers adt_name parser in + () + +let lookup_adt_parser_opt adt_name = + let open Caml in + Hashtbl.find_opt adt_parsers adt_name + +let lookup_adt_parser adt_name = + let open Caml in + match Hashtbl.find_opt adt_parsers adt_name with + | None -> raise (mk_invalid_json ~kind:"ADT not found" ~inst:adt_name) + | Some p -> p (* Generate a parser. Parse directly into OutputLiteral *) let gen_parser (t' : OutputType.t) (this_address : string) : diff --git a/src/eval/RunnerCLI.ml b/src/eval/RunnerCLI.ml index faeafb2e0..cde2af997 100644 --- a/src/eval/RunnerCLI.ml +++ b/src/eval/RunnerCLI.ml @@ -48,7 +48,6 @@ let v_balance = ref None let b_pp_lit = ref true let b_json_errors = ref false let b_pp_json = ref true -let b_validate_json = ref true let i_ipc_address = ref "" let b_reinit = ref false @@ -67,7 +66,6 @@ let reset () = b_pp_lit := true; b_json_errors := false; b_pp_json := true; - b_validate_json := true; i_ipc_address := ""; b_reinit := false @@ -83,7 +81,6 @@ let process_trace () = let process_pplit () = GlobalConfig.set_pp_lit !b_pp_lit let process_json_errors () = GlobalConfig.set_use_json_errors !b_json_errors -let process_json_validation () = GlobalConfig.set_validate_json true let validate_main usage = (* not mandatory file name input, but if provided, should be valid *) @@ -272,7 +269,6 @@ let parse args ~exe_name = let () = process_trace () in let () = process_pplit () in let () = process_json_errors () in - let () = process_json_validation () in let () = validate_main usage in { input_init = !f_input_init;