From 0fd85a0f63d4ebf48a86843f8d365563e8116b78 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 7 Jun 2024 17:14:17 +0200
Subject: [PATCH] [trans] Use NIR whenever available.
---
src/transformations/native_nn_prover.ml | 16 +-
tests/acasxu.t | 321 +++++++++++++++++++++++-
tests/acasxu_ci.t | 8 +-
3 files changed, 325 insertions(+), 20 deletions(-)
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index f3c364b..0f8f05c 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -99,14 +99,16 @@ let create_new_nn env input_vars outputs : string =
Logging.user_error ?loc (fun m ->
m "Neural network applied with the wrong number of arguments");
let old_nn_nir =
- match Onnx.Reader.from_file old_nn.Language.nn_filename with
- | Error s ->
- Logging.code_error ~src (fun m ->
- m "No parsed NN '%s': %s" old_nn.nn_filename s)
- | Ok { nir = Error s; _ } ->
+ let nir_opt =
+ match old_nn.Language.nn_format with
+ | NNet nir_opt -> nir_opt
+ | ONNX nir_opt -> nir_opt
+ in
+ match nir_opt with
+ | None ->
Logging.code_error ~src (fun m ->
- m "No NIR available for NN '%s': %s" old_nn.nn_filename s)
- | Ok { nir = Ok g; _ } -> g
+ m "No NIR available for NN '%s'" old_nn.nn_filename)
+ | Some g -> g
in
(* Create the graph to replace the old input of the nn *)
let input () =
diff --git a/tests/acasxu.t b/tests/acasxu.t
index 9b8aaea..4889b82 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -648,9 +648,110 @@ Test verify on acasxu
nn_filename = "./TestNetwork.nnet";
nn_format = <nir> }))
[DEBUG]{NN-Gen-Term} new goal:le y10 (1500.0:t)
- [ERROR]{NN-Gen} No parsed NN './TestNetwork.nnet': Cannot read protobuf
- Unrecoverable error: please report the issue at
- https://git.frama-c.com/pub/caisar/issues
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ -0.328421367053318091766556108268559910356998443603515625 <= x0
+ x0 <= 0.67985927880386987087746319957659579813480377197265625
+ -0.499999999999967081887319864108576439321041107177734375 <= x1
+ x1 <= 0.499999999999967081887319864108576439321041107177734375
+ -0.499999999999967081887319864108576439321041107177734375 <= x2
+ x2 <= 0.499999999999967081887319864108576439321041107177734375
+ -0.5 <= x3
+ x3 <= 0.5
+ -0.5 <= x4
+ x4 <= 0.5
+ 0.60000151009774149724051994780893437564373016357421875 <= x0
+ 0.450000000000000011102230246251565404236316680908203125 <= x3
+ x4 <= -0.450000000000000011102230246251565404236316680908203125
+ y0 <= 1500.0
+
+ [DEBUG]{InterpretGoal} Interpreted formula for goal 'P3':
+ forall x:t, x1:t, x2:t, x3:t, x4:t.
+ ((le (0.0:t) (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) /\
+ le (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) (60760.0:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t))
+ (add RNE
+ (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t))
+ (add RNE
+ (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (100.0:t) (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) /\
+ le (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) (1200.0:t)) /\
+ le (0.0:t) (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) /\
+ le (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) (1200.0:t)) /\
+ ((le (1500.0:t) (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) /\
+ le (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) (1800.0:t)) /\
+ le (neg (0.059999999999999997779553950749686919152736663818359375:t))
+ (add RNE
+ (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (0.059999999999999997779553950749686919152736663818359375:t)) /\
+ le (3.100000000000000088817841970012523233890533447265625:t)
+ (add RNE
+ (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le (980.0:t) (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) /\
+ le (960.0:t) (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) ->
+ not (((lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
+ (nn_nnet @@ vector x x1 x2 x3 x4)[1] /\
+ lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
+ (nn_nnet @@ vector x x1 x2 x3 x4)[2]) /\
+ lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
+ (nn_nnet @@ vector x x1 x2 x3 x4)[3]) /\
+ lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
+ (nn_nnet @@ vector x x1 x2 x3 x4)[4])
+ vector, 5
+ nn_nnet,
+ (Interpreter_types.Model
+ (Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
+ nn_ty_elt = t;
+ nn_filename = "./TestNetwork.nnet";
+ nn_format = <nir> }))
+ [DEBUG]{NN-Gen-Term} new goal:not (((lt y11 y12 /\ lt y11 y13) /\ lt y11 y14) /\
+ lt y11 y15)
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ -0.328421367053318091766556108268559910356998443603515625 <= x0
+ x0 <= 0.67985927880386987087746319957659579813480377197265625
+ -0.499999999999967081887319864108576439321041107177734375 <= x1
+ x1 <= 0.499999999999967081887319864108576439321041107177734375
+ -0.499999999999967081887319864108576439321041107177734375 <= x2
+ x2 <= 0.499999999999967081887319864108576439321041107177734375
+ -0.5 <= x3
+ x3 <= 0.5
+ -0.5 <= x4
+ x4 <= 0.5
+ -0.303529646039727207806890874053351581096649169921875 <= x0
+ x0 <= -0.298551301837009008810497334707179106771945953369140625
+ -0.0095492965855130916563719978285007528029382228851318359375 <= x1
+ x1 <= 0.0095492965855130916563719978285007528029382228851318359375
+ 0.493380323584843072382000173092819750308990478515625 <= x2
+ 0.299999999999999988897769753748434595763683319091796875 <= x3
+ 0.299999999999999988897769753748434595763683319091796875 <= x4
+ (((y0 >= y1 or y0 >= y2) or y0 >= y3) or y0 >= y4)
+
+ Goal runP1'vc: Unknown ()
+ Goal runP1v2'vc: Unknown ()
+ Goal run2'vc: Unknown ()
+ Goal run2v2'vc: Unknown ()
+ Goal run3'vc: Unknown ()
+ Goal robust_output'vc: Unknown ()
+ Goal P1: Unknown ()
+ Goal P3: Unknown ()
$ caisar verify --prover PyRAT --prover-altern VNNLIB --ltag=ProverSpec file.mlw
[DEBUG]{ProverSpec} Prover-tailored specification:
@@ -954,9 +1055,167 @@ Test verify on acasxu
(and (>= Y_0 0.0))
))
- [ERROR]{NN-Gen} No parsed NN './TestNetwork.nnet': Cannot read protobuf
- Unrecoverable error: please report the issue at
- https://git.frama-c.com/pub/caisar/issues
+ [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)
+
+ ;; H
+ (assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
+
+ ;; H
+ (assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
+
+ ;; H
+ (assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
+
+ ;; H
+ (assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
+
+ ;; H
+ (assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
+
+ ;; H
+ (assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
+
+ ;; H
+ (assert (>= X_3 -0.5))
+
+ ;; H
+ (assert (<= X_3 0.5))
+
+ ;; H
+ (assert (>= X_4 -0.5))
+
+ ;; H
+ (assert (<= X_4 0.5))
+
+ ;; H
+ (assert (>= X_0 0.60000151009774149724051994780893437564373016357421875))
+
+ ;; H
+ (assert (>= X_3 0.450000000000000011102230246251565404236316680908203125))
+
+ ;; H
+ (assert (<= X_4 -0.450000000000000011102230246251565404236316680908203125))
+
+ ;; Y_0
+ (declare-const Y_0 Real)
+
+ ;; Goal P1
+ (assert (>= Y_0 1500.0))
+
+ [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)
+
+ ;; H
+ (assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
+
+ ;; H
+ (assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
+
+ ;; H
+ (assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
+
+ ;; H
+ (assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
+
+ ;; H
+ (assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
+
+ ;; H
+ (assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
+
+ ;; H
+ (assert (>= X_3 -0.5))
+
+ ;; H
+ (assert (<= X_3 0.5))
+
+ ;; H
+ (assert (>= X_4 -0.5))
+
+ ;; H
+ (assert (<= X_4 0.5))
+
+ ;; H
+ (assert (>= X_0 -0.303529646039727207806890874053351581096649169921875))
+
+ ;; H
+ (assert (<= X_0 -0.298551301837009008810497334707179106771945953369140625))
+
+ ;; H
+ (assert (>= X_1 -0.0095492965855130916563719978285007528029382228851318359375))
+
+ ;; H
+ (assert (<= X_1 0.0095492965855130916563719978285007528029382228851318359375))
+
+ ;; H
+ (assert (>= X_2 0.493380323584843072382000173092819750308990478515625))
+
+ ;; H
+ (assert (>= X_3 0.299999999999999988897769753748434595763683319091796875))
+
+ ;; H
+ (assert (>= X_4 0.299999999999999988897769753748434595763683319091796875))
+
+ ;; 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)
+
+ ;; Goal P3
+ (assert (<= Y_0 Y_1))
+ (assert (<= Y_0 Y_2))
+ (assert (<= Y_0 Y_3))
+ (assert (<= Y_0 Y_4))
+
+ Goal runP1'vc: Unknown ()
+ Goal runP1v2'vc: Unknown ()
+ Goal run2'vc: Unknown ()
+ Goal run2v2'vc: Unknown ()
+ Goal run3'vc: Unknown ()
+ Goal robust_output'vc: Unknown ()
+ Goal P1: Unknown ()
+ Goal P3: Unknown ()
$ caisar verify --prover Marabou --ltag=ProverSpec file.mlw
[DEBUG]{ProverSpec} Prover-tailored specification:
@@ -1143,6 +1402,50 @@ Test verify on acasxu
x5 <= 0.375
y0 >= 0.0
- [ERROR]{NN-Gen} No parsed NN './TestNetwork.nnet': Cannot read protobuf
- Unrecoverable error: please report the issue at
- https://git.frama-c.com/pub/caisar/issues
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= -0.328421367053318091766556108268559910356998443603515625
+ x0 <= 0.67985927880386987087746319957659579813480377197265625
+ x1 >= -0.499999999999967081887319864108576439321041107177734375
+ x1 <= 0.499999999999967081887319864108576439321041107177734375
+ x2 >= -0.499999999999967081887319864108576439321041107177734375
+ x2 <= 0.499999999999967081887319864108576439321041107177734375
+ x3 >= -0.5
+ x3 <= 0.5
+ x4 >= -0.5
+ x4 <= 0.5
+ x0 >= 0.60000151009774149724051994780893437564373016357421875
+ x3 >= 0.450000000000000011102230246251565404236316680908203125
+ x4 <= -0.450000000000000011102230246251565404236316680908203125
+ y0 >= 1500.0
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= -0.328421367053318091766556108268559910356998443603515625
+ x0 <= 0.67985927880386987087746319957659579813480377197265625
+ x1 >= -0.499999999999967081887319864108576439321041107177734375
+ x1 <= 0.499999999999967081887319864108576439321041107177734375
+ x2 >= -0.499999999999967081887319864108576439321041107177734375
+ x2 <= 0.499999999999967081887319864108576439321041107177734375
+ x3 >= -0.5
+ x3 <= 0.5
+ x4 >= -0.5
+ x4 <= 0.5
+ x0 >= -0.303529646039727207806890874053351581096649169921875
+ x0 <= -0.298551301837009008810497334707179106771945953369140625
+ x1 >= -0.0095492965855130916563719978285007528029382228851318359375
+ x1 <= 0.0095492965855130916563719978285007528029382228851318359375
+ x2 >= 0.493380323584843072382000173092819750308990478515625
+ x3 >= 0.299999999999999988897769753748434595763683319091796875
+ x4 >= 0.299999999999999988897769753748434595763683319091796875
+ +y0 -y1 <= 0
+ +y0 -y2 <= 0
+ +y0 -y3 <= 0
+ +y0 -y4 <= 0
+
+ Goal runP1'vc: Unknown ()
+ Goal runP1v2'vc: Unknown ()
+ Goal run2'vc: Unknown ()
+ Goal run2v2'vc: Unknown ()
+ Goal run3'vc: Unknown ()
+ Goal robust_output'vc: Unknown ()
+ Goal P1: Unknown ()
+ Goal P3: Unknown ()
diff --git a/tests/acasxu_ci.t b/tests/acasxu_ci.t
index f274c7e..b4ea0da 100644
--- a/tests/acasxu_ci.t
+++ b/tests/acasxu_ci.t
@@ -934,11 +934,11 @@ Test verify on acasxu
out/caisar_0.onnx has 1 input nodes
{'name': '38', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
out/caisar_1.onnx has 1 input nodes
- {'name': '221', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
+ {'name': '183', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
out/caisar_2.onnx has 1 input nodes
- {'name': '439', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
+ {'name': '325', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
out/caisar_3.onnx has 1 input nodes
- {'name': '587', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '6'}]}}}}
+ {'name': '435', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '6'}]}}}}
out/caisar_4.onnx has 1 input nodes
- {'name': '814', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
+ {'name': '586', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
5 files checked
--
GitLab