Skip to content
Snippets Groups Projects
Commit 211510b0 authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

[tests] Modified JSON test to handle the new API

parent c06c46e9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
flake.lock
+ 12
− 12
View file @ 211510b0
......@@ -11,11 +11,11 @@
"locked": {
"lastModified": 1,
"narHash": "sha256-/UVOUsDr/tqXgJ0lzS4jfpMR36E19IUtb3+yJvGCS3s=",
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/abcrown",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/abcrown",
"type": "path"
},
"original": {
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/abcrown",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/abcrown",
"type": "path"
}
},
......@@ -24,11 +24,11 @@
"locked": {
"lastModified": 1,
"narHash": "sha256-FgO4U0EDYd0ynnZDpEVO2yzMIO7y8/e6S+WBzypz/Z0=",
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/VERSION",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/VERSION",
"type": "path"
},
"original": {
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/VERSION",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/VERSION",
"type": "path"
}
},
......@@ -150,11 +150,11 @@
"locked": {
"lastModified": 1,
"narHash": "sha256-V7BK+6EXtF0DjfYJZqIg1wS2khculp4riRVqM/+MHGE=",
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/marabou",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/marabou",
"type": "path"
},
"original": {
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/marabou",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/marabou",
"type": "path"
}
},
......@@ -244,11 +244,11 @@
"locked": {
"lastModified": 1,
"narHash": "sha256-2cKWbmrFOGsX6nY0xyeTtU7oG61zWXTv313xSayNd18=",
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/nnenum",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/nnenum",
"type": "path"
},
"original": {
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/nnenum",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/nnenum",
"type": "path"
}
},
......@@ -263,11 +263,11 @@
"locked": {
"lastModified": 1,
"narHash": "sha256-POrh9c/ov+89Py2tO0Qp53PZ4So/9AcrMsHKGevXrdU=",
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/pyrat_compiled",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/pyrat_compiled",
"type": "path"
},
"original": {
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/pyrat_compiled",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/pyrat_compiled",
"type": "path"
}
},
......@@ -294,11 +294,11 @@
"locked": {
"lastModified": 1,
"narHash": "sha256-2KmAnZFkmfOAvp40iktsRB9H6Mo6Jv0dZveWHIeBRrA=",
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/saver",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/saver",
"type": "path"
},
"original": {
"path": "/nix/store/7cgkla26si6az5mca17dwrr239zw2d9j-source/vendor/saver",
"path": "/nix/store/1bfblf88w3w9vfcljw4v23g606alirdq-source/vendor/saver",
"type": "path"
}
},
......
src/main.ml
+ 4
− 7
View file @ 211510b0
......@@ -127,12 +127,9 @@ let log_theory_answer =
(id, prover_answer, additional_info)
| {
problem_answer =
LegacyDatasetAnswer { prover_answer; additional_info; _ };
LegacyDatasetAnswer { id; prover_answer; additional_info; _ };
_;
} ->
let id =
Why3.(Decl.create_prsymbol (Ident.id_fresh "LegacyDatasetProof"))
in
(id, prover_answer, additional_info)
in
Logs.app (fun m ->
......@@ -170,13 +167,13 @@ let record_json_output answer file =
let record_verification_result verification_result file =
Why3.Wstdlib.Mstr.iter
(fun name (answers : Verification.verification_result list) ->
(fun _th_name (answers : Verification.verification_result list) ->
let rec aux answers file =
match answers with
| answer :: tl ->
record_json_output answer file;
aux tl file
| _ -> failwith (Fmt.str "Unexpected answers for theory '%s'" name)
| [] -> ()
in
aux answers file)
verification_result
......@@ -206,7 +203,7 @@ let verify_json ?memlimit ?timelimit ?outfile json =
| Some f -> f
| None -> failwith "should support stdlib output")
in
let verification_results = Verification.verify query in
let verification_results = Verification.verify ~format:"whyml" query in
record_verification_result verification_results outfile
let verify_xgboost ?memlimit ?timelimit xgboost dataset prover =
......
src/verification.ml
+ 9
− 2
View file @ 211510b0
......@@ -88,6 +88,7 @@ let write_ovo_as_onnx onnx_out_dir =
m "@[Cannot write SVM as ONNX in folder '%s': '%s'@]" onnx_out_dir msg))
let answer_saver_on_dataset limit config env config_prover ~dataset task =
let id = Task.task_goal task in
let dataset_predicate =
let on_model ls =
Option.value_or_thunk
......@@ -118,6 +119,7 @@ let answer_saver_on_dataset limit config env config_prover ~dataset task =
in
Verification_types.Answer.LegacyDatasetAnswer
{
id;
prover_answer = Call_provers.Unknown "";
percentage_valid = percentage_valid answer.nb_proved answer.nb_total;
dataset_results = [];
......@@ -131,6 +133,7 @@ let answer_saver_on_dataset limit config env config_prover ~dataset task =
in
Verification_types.Answer.LegacyDatasetAnswer
{
id;
prover_answer;
percentage_valid = percentage_valid answer.nb_proved answer.nb_total;
dataset_results = [];
......@@ -138,6 +141,7 @@ let answer_saver_on_dataset limit config env config_prover ~dataset task =
}
let answer_aimos limit config env config_prover dataset task =
let id = Task.task_goal task in
let predicate =
let on_model ls =
Option.value_or_thunk
......@@ -162,6 +166,7 @@ let answer_aimos limit config env config_prover dataset task =
let prover_answer = Aimos.call_prover limit config config_prover predicate in
Verification_types.Answer.LegacyDatasetAnswer
{
id;
prover_answer;
percentage_valid = None;
dataset_results = [];
......@@ -204,6 +209,7 @@ let combine_prover_answers answers =
| Valid, Valid -> Valid)
let answer_dataset limit config env prover config_prover driver dataset task =
let id = Task.task_goal task in
let dataset_predicate =
let on_model ls =
Option.value_or_thunk
......@@ -260,6 +266,7 @@ let answer_dataset limit config env prover config_prover driver dataset task =
in
Verification_types.Answer.LegacyDatasetAnswer
{
id;
prover_answer;
percentage_valid = None;
dataset_results;
......@@ -268,6 +275,7 @@ let answer_dataset limit config env prover config_prover driver dataset task =
let answer_saver limit config env config_prover ~proof_strategy task =
let tasks = proof_strategy task in
let id = Task.task_goal task in
let answers =
List.map tasks ~f:(fun task ->
let svm, abstraction =
......@@ -331,6 +339,7 @@ let answer_saver limit config env config_prover ~proof_strategy task =
let prover_answer = combine_prover_answers answers in
Verification_types.Answer.LegacyDatasetAnswer
{
id;
prover_answer;
percentage_valid = None;
dataset_results = [];
......@@ -499,8 +508,6 @@ let verify ?format (query : Verification_types.Query.t) =
Driver.load_driver_file_and_extras main env ~extra_dir:None driver
config_prover.extra_drivers
in
(*not using the "?format" argument here as it was always set to WhyML
anyway *)
let filepath =
match query.problem with GenericProblem { filepath; _ } -> filepath
in
......
src/verification_types.ml
+ 2
− 0
View file @ 211510b0
......@@ -130,6 +130,8 @@ module Answer = struct
and problem_answer =
| LegacyDatasetAnswer of {
id : Why3.Decl.prsymbol;
[@to_yojson prsymbol_to_yojson] [@printer pp_prsymbol]
prover_answer : prover_answer;
percentage_valid : float option;
dataset_results : prover_answer list;
......
src/verification_types.mli
+ 1
− 0
View file @ 211510b0
......@@ -138,6 +138,7 @@ module Answer : sig
and problem_answer =
| LegacyDatasetAnswer of {
id : Why3.Decl.prsymbol;
prover_answer : prover_answer;
percentage_valid : float option;
dataset_results : prover_answer list;
......
tests/dune
+ 2
− 0
View file @ 211510b0
......@@ -16,6 +16,8 @@
../examples/onnx_rewrite/sequencing.mlw
../examples/acasxu/nets/onnx/ACASXU_1_1.onnx
../examples/acasxu/nets/onnx/ACASXU_1_9.onnx
../examples/mnist/mnist.why
../examples/mnist/nets/MNIST_256_2.onnx
../examples/mnist/nets/pruned/FNN_28x28_s42.onnx
../examples/mnist/nets/pruned/FNN_28x28_pruned_s42.onnx
../examples/mnist/nets/splitted/FNN_28x28_pre_s42.onnx
......
tests/verify_json.t
+ 16
− 78
View file @ 211510b0
Test verify-json
$ . ./setup_env.sh
$ cat - > test_data.csv << EOF
> 1,0.0,1.0,0.784313725,0.019607843,0.776470588
> EOF
......@@ -16,12 +19,10 @@ Test verify-json
> "loadpath":["."],
> "model":"TestNetwork.nnet",
> "problem":["GenericProblem",
> {"filepath":["File","../examples/onnx_rewrite/sequencing.mlw"],
> "definitions":[["model_filename_2",
> "../mnist/nets/splitted/FNN_28x28_post_s42.onnx"],
> ["model_filename_1",
> "../mnist/nets/splitted/FNN_28x28_pre_s42.onnx"],
> ["dataset_filename","../mnist/csv/single_image.csv"]],
> {"filepath":["File","../examples/arithmetic/arithmetic.why"],
> "definitions":[
> ["model_filename", "FNN_s42.onnx"]
> ],
> "goals":null,
> "theories":[]}]
> }
......@@ -34,75 +35,12 @@ Test verify-json
$ caisar verify-json --ltag=ProverSpec config.json
[DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
(declare-const X_0 Real)
;; X_1
(declare-const X_1 Real)
;; X_2
(declare-const X_2 Real)
;; X_3
(declare-const X_3 Real)
;; X_4
(declare-const X_4 Real)
;; Y_0
(declare-const Y_0 Real)
;; Y_1
(declare-const Y_1 Real)
;; Y_2
(declare-const Y_2 Real)
;; Y_3
(declare-const Y_3 Real)
;; Y_4
(declare-const Y_4 Real)
;; axiom_ge_x0
(assert (>= X_0 0.0))
;; axiom_le_x0
(assert (<= X_0 0.299999999999999988897769753748434595763683319091796875))
;; axiom_ge_x1
(assert (>= X_1 0.6999999999999999555910790149937383830547332763671875))
;; axiom_le_x1
(assert (<= X_1 1.0))
;; axiom_ge_x2
(assert (>= X_2 0.484313724999999972720132745962473563849925994873046875))
;; axiom_le_x2
(assert (<= X_2 1.0))
;; axiom_ge_x3
(assert (>= X_3 0.0))
;; axiom_le_x3
(assert (<= X_3 0.319607843000000002575688995420932769775390625))
;; axiom_ge_x4
(assert (>= X_4 0.476470588000000028205960234117810614407062530517578125))
;; axiom_le_x4
(assert (<= X_4 1.0))
;; Goal robust_record0_y1
(assert
(or
(and (>= Y_0 Y_1))
(and (>= Y_2 Y_1))
(and (>= Y_3 Y_1))
(and (>= Y_4 Y_1))
))
Goal property: Unknown ()
-5.0 <= x0
x0 <= 5.0
-5.0 <= x1
x1 <= 5.0
-5.0 <= x2
x2 <= 5.0
y0 <= 0.5
$ jq '.problem_answer[1].prover_answer[0]' out.json
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