From 677a727707906c9e2601458617186ce8f6ac81f7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 5 Apr 2024 13:31:22 +0200
Subject: [PATCH] [NN_prover] Add $CAISAR_ONNX_OUTPUT_DIR for specifying output
directory
- todo use the onnx-out-dir option
---
lib/onnx/tests/print.expected | 2 +-
src/transformations/native_nn_prover.ml | 3 ++-
tests/acasxu.t | 6 ++++++
tests/bin/inspect_onnx.py | 17 +++++------------
tests/nier_to_onnx.t | 2 +-
5 files changed, 15 insertions(+), 15 deletions(-)
diff --git a/lib/onnx/tests/print.expected b/lib/onnx/tests/print.expected
index e5444a6..8088b70 100644
--- a/lib/onnx/tests/print.expected
+++ b/lib/onnx/tests/print.expected
@@ -1,4 +1,4 @@
true
ok
ok
-Input name 0
+1 files checked
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 7cd8fd9..3bac141 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -185,7 +185,8 @@ let create_new_nn env input_vars outputs : string =
assert (
IR.Shape.equal output.shape (IR.Shape.of_array [| List.length outputs |]));
let nn = IR.create output in
- let filename = Stdlib.Filename.temp_file "caisar" ".onnx" in
+ let temp_dir = Sys.getenv "CAISAR_ONNX_OUTPUT_DIR" in
+ let filename = Stdlib.Filename.temp_file ?temp_dir "caisar" ".onnx" in
Onnx.Simple.write nn filename;
filename
diff --git a/tests/acasxu.t b/tests/acasxu.t
index aaec5a8..2612b32 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -4,6 +4,9 @@ Test verify on acasxu
$ bin/pyrat.py --version
PyRAT 1.1
+ $ mkdir out
+ $ export CAISAR_ONNX_OUTPUT_DIR=out
+
$ cat > file.mlw <<EOF
> theory T
> use ieee_float.Float64
@@ -1179,3 +1182,6 @@ Test verify on acasxu
Goal run3'vc: Unknown ()
Goal test'vc: Unknown ()
Goal P3: Unknown ()
+
+ $ python3 bin/inspect_onnx.py
+ 12 files checked
diff --git a/tests/bin/inspect_onnx.py b/tests/bin/inspect_onnx.py
index a109a49..800f144 100644
--- a/tests/bin/inspect_onnx.py
+++ b/tests/bin/inspect_onnx.py
@@ -1,17 +1,10 @@
import onnx
import os
-for file in os.listdir("out"):
+l = os.listdir("out")
+
+for file in l:
m = onnx.load(os.path.join("out", file))
- if len(m.graph.initializer) >= 1:
- initi = m.graph.initializer[0]
- print(
- "Initializer name {name} has data {val:3.3f}".format(
- name=initi.name, val=initi.float_data[2]
- )
- )
- if len(m.graph.input) >= 1:
- print(
- f"Input name {m.graph.input[0].name}"
- )
onnx.checker.check_model(m)
+
+print(len(l),"files checked")
\ No newline at end of file
diff --git a/tests/nier_to_onnx.t b/tests/nier_to_onnx.t
index e062cca..d754d03 100644
--- a/tests/nier_to_onnx.t
+++ b/tests/nier_to_onnx.t
@@ -26,4 +26,4 @@ Test verify
Data should be 0.135
$ python3 bin/inspect_onnx.py
- Input name 0
+ 1 files checked
--
GitLab