Skip to content

Commit

Permalink
Remove non-validating json parser (#1177)
Browse files Browse the repository at this point in the history
* 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
  • Loading branch information
jjcnn authored Oct 5, 2022
1 parent 10ff036 commit 80c172c
Show file tree
Hide file tree
Showing 8 changed files with 30 additions and 241 deletions.
6 changes: 1 addition & 5 deletions src/base/GlobalConfig.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
2 changes: 0 additions & 2 deletions src/base/GlobalConfig.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions src/base/JSON.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
195 changes: 0 additions & 195 deletions src/base/JSONParser.ml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@
*)

(* A fast JSON parser for states that performs no validations. *)

open Core
open Yojson
open ErrorUtils
Expand Down Expand Up @@ -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
25 changes: 0 additions & 25 deletions src/base/JSONParser.mli
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@
scilla. If not, see <http://www.gnu.org/licenses/>.
*)

open Core
open Yojson
module JSONTypeUtilities = TypeUtil.TypeUtilities
module JSONIdentifier = TypeUtil.TUIdentifier
Expand All @@ -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
5 changes: 0 additions & 5 deletions src/base/RunnerUtil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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" );
Expand Down Expand Up @@ -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;
Expand Down
31 changes: 28 additions & 3 deletions src/eval/Disambiguator.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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) :
Expand Down
4 changes: 0 additions & 4 deletions src/eval/RunnerCLI.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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

Expand All @@ -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 *)
Expand Down Expand Up @@ -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;
Expand Down

0 comments on commit 80c172c

Please sign in to comment.