Skip to content
Snippets Groups Projects
Commit cc99ad76 authored by Michele Alberti's avatar Michele Alberti
Browse files

[json] Proper independent file for json handling.

parent e7feb6a3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/JSON.ml 0 → 100644
+ 149
− 0
View file @ cc99ad76
(**************************************************************************)
(* *)
(* This file is part of CAISAR. *)
(* *)
(* Copyright (C) 2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* You can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Why3
open Base
type input = {
id : string;
prover : Prover.t;
model : string;
property : property;
time_limit : int option;
memory_limit : int option;
output_file : string option;
}
and property = {
dataset : string;
normalization : Dataset.normalization option;
kind : Dataset.property;
}
[@@deriving yojson, show]
type output = {
id : string;
result : prover_answer;
percentage_valid : float;
dataset_results : string;
}
and prover_answer = Call_provers.prover_answer =
| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of string
| Failure of string
| HighFailure
[@@deriving yojson, show]
let input_of_string s =
match input_of_yojson (Yojson.Safe.from_file s) with
| Ok t -> t
| Error msg ->
invalid_arg
(Fmt.str "Unrecognized JSON configuration in file '%s' (%s)" s msg)
| exception Yojson.Json_error msg ->
failwith
(Fmt.str "Unexpected error while parsing JSON file '%s' (%s)" s msg)
let pretty_input fmt = Fmt.fmt "%a" fmt pp_input
let pretty_output fmt = Fmt.fmt "%a" fmt pp_output
let theory_of_input env input =
let th_as_array =
let model_parser =
let extension = Caml.Filename.(extension (basename input.model)) in
match String.lowercase extension with
| ".nnet" -> Language.nnet_parser
| ".onnx" -> Language.onnx_parser
| ".ovo" -> Language.ovo_parser
| "" -> invalid_arg "Cannot find the model file extension"
| _ -> invalid_arg (Fmt.str "Unrecognized model extension '%s'" extension)
in
let pmod = model_parser env (Unix.realpath input.model) in
(Wstdlib.Mstr.find "AsArray" pmod).mod_theory
in
let th_float64 = Env.read_theory env [ "ieee_float" ] "Float64" in
let th_dsc = Pmodule.read_module env [ "caisar" ] "DatasetClassification" in
let th_dsc_props =
Pmodule.read_module env [ "caisar" ] "DatasetClassificationProps"
in
let name = "JSON" in
let th_uc = Theory.create_theory (Ident.id_fresh name) in
let th_uc = Theory.use_export th_uc th_as_array in
let th_uc = Theory.use_export th_uc th_float64 in
let th_uc = Theory.use_export th_uc th_dsc.mod_theory in
let th_uc = Theory.use_export th_uc th_dsc_props.mod_theory in
let t_dataset =
let ls_dataset =
Theory.ns_find_ls th_dsc.mod_theory.th_export [ "dataset" ]
in
Term.t_app_infer ls_dataset []
in
let t_model =
let ls_model = Theory.ns_find_ls th_as_array.th_export [ "model" ] in
Term.t_app_infer ls_model []
in
(* Add dataset normalization. *)
let t_dataset, th_uc =
match input.property.normalization with
| None -> (t_dataset, th_uc)
| Some n ->
let t_normalization = Dataset.term_of_normalization env n in
let ls_dataset_norm =
let ty =
Ty.ty_app
(Theory.ns_find_ts th_dsc.mod_theory.th_export [ "dataset" ])
[]
in
Term.create_fsymbol (Ident.id_fresh "dataset'") [] ty
in
let ld_dataset_norm =
Decl.make_ls_defn ls_dataset_norm [] t_normalization
in
( Term.t_app_infer ls_dataset_norm [],
Theory.add_logic_decl th_uc [ ld_dataset_norm ] )
in
(* Create goal formula about specified property. *)
let th_uc =
let t_property =
match input.property.kind with
| Dataset.Correct ->
let ls_correct =
Theory.ns_find_ls th_dsc_props.mod_theory.th_export [ "correct" ]
in
Term.t_app_infer ls_correct [ t_model; t_dataset ]
| Robust eps ->
let ls_robust =
Theory.ns_find_ls th_dsc_props.mod_theory.th_export [ "robust" ]
in
let t_eps = Dataset.term_of_eps env eps in
Term.t_app_infer ls_robust [ t_model; t_dataset; t_eps ]
| CondRobust _ -> invalid_arg "Not yet supported property"
in
let prsymbol = Decl.create_prsymbol (Ident.id_fresh "property") in
Theory.add_prop_decl th_uc Decl.Pgoal prsymbol t_property
in
Theory.close_theory th_uc
src/JSON.mli 0 → 100644
+ 75
− 0
View file @ cc99ad76
(**************************************************************************)
(* *)
(* This file is part of CAISAR. *)
(* *)
(* Copyright (C) 2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* You can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Why3
type input = private {
id : string;
prover : Prover.t;
model : string;
property : property;
time_limit : int option;
memory_limit : int option;
output_file : string option;
}
and property = private {
dataset : string;
normalization : Dataset.normalization option;
kind : Dataset.property;
}
[@@deriving yojson { strict = false }, show]
type output = {
id : string;
result : prover_answer;
percentage_valid : float;
dataset_results : string;
}
and prover_answer = Call_provers.prover_answer =
| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of string
| Failure of string
| HighFailure
[@@deriving yojson, show]
val input_of_string : string -> input
(** [input_of_string filename] builds a {!JSON.input} given a [filename].
@raise Invalid_argument whenever the content of [filename] is unrecognized.
@raise Failure whenever the parsing of [filename] fails. *)
val theory_of_input : Env.env -> input -> Theory.theory
(** [theory_of_input env input] builds a {!Theory.theory} from the given
{!JSON.input}.
@raise Invalid_argument
whenever the model in {!JSON.input} has either no extension or an
unrecognized one. *)
val pretty_input : Format.formatter -> input -> unit
val pretty_output : Format.formatter -> output -> unit
src/main.ml
+ 7
− 11
View file @ cc99ad76
......@@ -170,11 +170,9 @@ let record_dataset_results id result dataset outfile =
Csv.close_out csv_out_channel;
dataset_results
in
let output =
{ Verification.JSON.id; result; percentage_valid; dataset_results }
in
let output = { JSON.id; result; percentage_valid; dataset_results } in
let out_channel = Stdlib.open_out outfile in
Yojson.Safe.to_channel out_channel (Verification.JSON.output_to_yojson output);
Yojson.Safe.to_channel out_channel (JSON.output_to_yojson output);
Logs.info (fun m -> m "@[Results recorded in file '%s'@]" outfile);
Stdlib.close_out out_channel
......@@ -186,10 +184,7 @@ let record_theory_answers id outfile =
| _ -> failwith (Fmt.str "Unexpected answers for theory '%s'" theory_name))
let verify_json ?memlimit ?timelimit ?outfile json =
let jin = Result.ok_exn (Verification.JSON.input_of_string json) in
let id = jin.id in
let prover = jin.prover in
let dataset = jin.property.dataset in
let jin = JSON.input_of_string json in
let memlimit =
(* Precedence to the command line option, if any. *)
match memlimit with
......@@ -208,14 +203,15 @@ let verify_json ?memlimit ?timelimit ?outfile json =
in
let file = Result.ok_or_failwith (Verification.File.of_json_input jin) in
let theory_answers =
verify ~loadpath:[] ?memlimit ?timelimit ~dataset prover [ file ]
verify ~loadpath:[] ?memlimit ?timelimit ~dataset:jin.property.dataset
jin.prover [ file ]
in
match theory_answers with
| [] -> assert false (* We always build one theory from the provided JSON. *)
| [ theory_answer ] ->
Option.iter outfile ~f:(fun outfile ->
record_theory_answers id outfile theory_answer)
| _ -> failwith "Unexpected more than one theory from a JSON file."
record_theory_answers jin.id outfile theory_answer)
| _ -> failwith "Unexpected more than one theory from a JSON file"
let exec_cmd cmdname cmd =
Logs.debug (fun m -> m "Execution of command '%s'" cmdname);
......
src/verification.ml
+ 15
− 143
View file @ cc99ad76
......@@ -24,167 +24,37 @@ open Why3
open Base
module Filename = Caml.Filename
module JSON = struct
type input = {
id : string;
prover : Prover.t;
model : string;
property : property;
time_limit : int option;
memory_limit : int option;
output_file : string option;
}
and property = {
dataset : string;
normalization : Dataset.normalization option;
kind : Dataset.property;
}
[@@deriving yojson, show]
type output = {
id : string;
result : prover_answer;
percentage_valid : float;
dataset_results : string;
}
and prover_answer = Call_provers.prover_answer =
| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of string
| Failure of string
| HighFailure
[@@deriving yojson]
let input_of_string s =
match input_of_yojson (Yojson.Safe.from_file s) with
| Ok t -> Ok t
| Error msg ->
Error
(invalid_arg
(Fmt.str "Unrecognized JSON configuration in file '%s' (%s)" s msg))
| exception Yojson.Json_error msg ->
Error
(failwith
(Fmt.str "Unexpected error while parsing JSON file '%s' (%s)" s msg))
let pretty fmt t = Fmt.fmt "%a" fmt pp_input t
let mstr_theory_of_json env t =
let th_as_array =
let model_parser =
let extension = Filename.(extension (basename t.model)) in
match String.lowercase extension with
| ".nnet" -> Language.nnet_parser
| ".onnx" -> Language.onnx_parser
| ".ovo" -> Language.ovo_parser
| "" -> invalid_arg "Cannot find model file extension"
| _ ->
invalid_arg (Fmt.str "Unrecognized model extension '%s'" extension)
in
let pmod = model_parser env (Unix.realpath t.model) in
(Wstdlib.Mstr.find "AsArray" pmod).mod_theory
in
let th_float64 = Env.read_theory env [ "ieee_float" ] "Float64" in
let th_dsc = Pmodule.read_module env [ "caisar" ] "DatasetClassification" in
let th_dsc_props =
Pmodule.read_module env [ "caisar" ] "DatasetClassificationProps"
in
let name = "JSON" in
let th_uc = Theory.create_theory (Ident.id_fresh name) in
let th_uc = Theory.use_export th_uc th_as_array in
let th_uc = Theory.use_export th_uc th_float64 in
let th_uc = Theory.use_export th_uc th_dsc.mod_theory in
let th_uc = Theory.use_export th_uc th_dsc_props.mod_theory in
let t_dataset =
let ls_dataset =
Theory.ns_find_ls th_dsc.mod_theory.th_export [ "dataset" ]
in
Term.t_app_infer ls_dataset []
in
let t_model =
let ls_model = Theory.ns_find_ls th_as_array.th_export [ "model" ] in
Term.t_app_infer ls_model []
in
(* Add dataset normalization. *)
let t_dataset, th_uc =
match t.property.normalization with
| None -> (t_dataset, th_uc)
| Some n ->
let t_normalization = Dataset.term_of_normalization env n in
let ls_dataset_norm =
let ty =
Ty.ty_app
(Theory.ns_find_ts th_dsc.mod_theory.th_export [ "dataset" ])
[]
in
Term.create_fsymbol (Ident.id_fresh "dataset'") [] ty
in
let ld_dataset_norm =
Decl.make_ls_defn ls_dataset_norm [] t_normalization
in
( Term.t_app_infer ls_dataset_norm [],
Theory.add_logic_decl th_uc [ ld_dataset_norm ] )
in
(* Create goal formula about specified property. *)
let th_uc =
let t_property =
match t.property.kind with
| Dataset.Correct ->
let ls_correct =
Theory.ns_find_ls th_dsc_props.mod_theory.th_export [ "correct" ]
in
Term.t_app_infer ls_correct [ t_model; t_dataset ]
| Robust eps ->
let ls_robust =
Theory.ns_find_ls th_dsc_props.mod_theory.th_export [ "robust" ]
in
let t_eps = Dataset.term_of_eps env eps in
Term.t_app_infer ls_robust [ t_model; t_dataset; t_eps ]
| CondRobust _ -> invalid_arg "Not yet supported property"
in
let prsymbol = Decl.create_prsymbol (Ident.id_fresh "property") in
Theory.add_prop_decl th_uc Decl.Pgoal prsymbol t_property
in
let th = Theory.close_theory th_uc in
Wstdlib.Mstr.singleton name th
end
module File = struct
type t =
| Stdin
| File of string
| Json of JSON.input
| JSON of JSON.input
let of_json_input jc =
if Caml.Sys.file_exists jc.JSON.model
let of_json_input jin =
if Caml.Sys.file_exists jin.JSON.model
then
if Caml.Sys.file_exists jc.JSON.property.dataset
if Caml.Sys.file_exists jin.property.dataset
then
if String.is_suffix jc.JSON.property.dataset ~suffix:".csv"
then Ok (Json jc)
if String.is_suffix jin.property.dataset ~suffix:".csv"
then Ok (JSON jin)
else
Error
(Fmt.str "file '%s' has an unsupported extension"
jc.property.dataset)
else Error (Fmt.str "no '%s' file or directory" jc.property.dataset)
else Error (Fmt.str "no '%s' file or directory" jc.model)
(Fmt.str "Unrecognized file extension in file '%s'"
jin.property.dataset)
else Error (Fmt.str "No '%s' file or directory" jin.property.dataset)
else Error (Fmt.str "No '%s' file or directory" jin.model)
let of_string s =
if String.equal s "-"
then Ok Stdin
else if Caml.Sys.file_exists s
then Ok (File s)
else Error (Fmt.str "no '%s' file or directory" s)
else Error (Fmt.str "No '%s' file or directory" s)
let pretty fmt = function
| Stdin -> Fmt.string fmt "-"
| File f -> Fmt.string fmt f
| Json j -> JSON.pretty fmt j
| JSON jin -> JSON.pretty_input fmt jin
end
type theory_answer = answer list Wstdlib.Mstr.t
......@@ -397,7 +267,9 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
| File file ->
let mlw_files, _ = Env.(read_file ?format base_language env file) in
mlw_files
| Json json -> JSON.mstr_theory_of_json env json
| JSON jin ->
let th = JSON.theory_of_input env jin in
Wstdlib.Mstr.singleton th.th_name.id_string th
in
Wstdlib.Mstr.map
(fun theory ->
......
src/verification.mli
+ 0
− 40
View file @ cc99ad76
......@@ -22,46 +22,6 @@
open Why3
module JSON : sig
type input = private {
id : string;
prover : Prover.t;
model : string;
property : property;
time_limit : int option;
memory_limit : int option;
output_file : string option;
}
and property = private {
dataset : string;
normalization : Dataset.normalization option;
kind : Dataset.property;
}
[@@deriving yojson { strict = false }, show]
type output = {
id : string;
result : prover_answer;
percentage_valid : float;
dataset_results : string;
}
and prover_answer = Call_provers.prover_answer =
| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of string
| Failure of string
| HighFailure
[@@deriving yojson]
val input_of_string : string -> (input, exn) result
val pretty : Format.formatter -> input -> unit
end
module File : sig
type t
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment