Skip to content
GitLab
Commit ffcb1947 authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

added files and instructions to reproduce results from CAMUS

parent 51901aeb
Hide whitespace changes
Inline Side-by-side
ISAIEH.opam
View file @ ffcb1947
......@@ -12,7 +12,7 @@ license: "LGPL-2.0-only WITH OCaml-LGPL-linking-exception"
homepage: "https://git.frama-c.com/pub/isaieh"
depends: [
"dune" {>= "2.1"}
"ocaml" {>= "4.07.0"}
"ocaml" {>= "4.11.0"}
"ocplib-endian" {>= "1.0"}
"piqilib" {>= "0.6.14"}
"piqi" {>= "0.7.6"}
......
README.md
View file @ ffcb1947
......@@ -44,6 +44,7 @@ to compile it from source.
### Dependencies:
The list of OCaml dependencies is available under the
`dune-project` file at the root of the project.
We require OCaml 4.11.1 at least.
The simplest way to get all dependencies is by using the
OCaml package manager, `opam`,
version 2.0 or higher.
......@@ -102,6 +103,9 @@ with no biases. Input is of size 2x2.
with 100 neurons width for the first layer and 1 neuron
for the second. Input is of size 500x100.
* `test_linreg_points` is a linear regressor trained to output a pair of parameters (real numbers) $a$ and $b$, given a vector $[a+b,a-b,c]$
* `CAMUS_53` is a network used for the publication _CAMUS_. The property
to verify is in `test/smtlib/property_CAMUS.smt2`. To test ISAIEH on this
problem, execute the script `check_camus.sh`.
## Basic structure of project
ONNX format is parsed into a
......
bin/converter/converter.ml
View file @ ffcb1947
......@@ -25,7 +25,7 @@ let t_cfg input_file theory =
let nier_cfg = Parser.produce_cfg graph in
Printf.printf "NIER CFG build successful\n";
SMT.pp_graph_cfg nier_cfg theory
let theory_v = ref SMT.Linear_Real_Theory
let theory_v = ref SMT.Real_Theory
let output_dir = ref ""
let set_theory s = match s with
| "QF_FP" -> theory_v := SMT.Float_Theory
......
check_camus.sh 0 → 100755
View file @ ffcb1947
echo "Converting a CAMUS ONNX network to SMTLIB2 format."
dune exec -- bin/converter/converter.exe test/onnx/CAMUS_53.onnx
echo "Adding a property to check."
cat CAMUS_53_QF_NRA.smt2 test/smtlib/property_CAMUS.smt2 > out.smt2
echo "Launching z3. This should take about 15s and return UNSAT."
z3 -st out.smt2
dune-project
View file @ ffcb1947
......@@ -9,7 +9,7 @@
(package
(name ISAIEH)
(depends
(ocaml (>= 4.07.0))
(ocaml (>= 4.11.0))
(ocplib-endian (>= 1.0))
(piqilib (>= 0.6.14))
(piqi (>= 0.7.6))
......
lib/output/smt/test_smtifyer.ml deleted 100644 → 0
View file @ 51901aeb
(*Bunch of unit tests*)
let _ =
Printf.printf "toto\n"
(*let test_relu =
let v = NG.create_vertex 1 NG.ReLu [no_attr] "C_NODE" (i64ify [2;3;4]) "" ["A"] ["C"] in
env := [("A",{size = i64ify [2;3;4]; raw_data = ""})];
"Testing ReLu"::(SMT.pp_cnode env v)
let test_add =
let v = NG.create_vertex 1 NG.Add [no_attr] "C_NODE" (i64ify [2;3;4]) "" ["A";"B"] ["C"] in
env := [("A",{size = i64ify [2;3;4]; raw_data = ""});("B",{size = i64ify [2;3;4]; raw_data = ""})];
"Testing Add"::(SMT.pp_cnode env v)
let test_mul =
let v = NG.create_vertex 1 NG.Mul [no_attr] "C_NODE" (i64ify [2;3;4]) "" ["A";"B"] ["C"] in
env := [("A",{size = i64ify [2;3;4]; raw_data = ""});("B",{size = i64ify [2;3;4]; raw_data = ""})];
"Testing Mul \n"::(SMT.pp_cnode env v)
let test_matmul = function
| 1 -> []
(*Printf.printf "Testing old Matmul (for 2D only) \n" ;
List.iter (Printf.printf "%s \n") (SMT.pp_matmul_2D ("A", (4,2)) ("B",
(2,3)) "C")*)
| 2 ->
let v = NG.create_vertex 1 NG.Matmul [no_attr] "C_NODE" (i64ify [4;3]) "" ["A";"B"] ["C"] in
Printf.printf "Testing Matmul for simple matrices \n" ;
env := [("A",{size = i64ify [4;2]; raw_data = ""});("B",{size = i64ify [2;3]; raw_data = ""})];
SMT.pp_cnode env v
| 3 ->
let v = NG.create_vertex 1 NG.Matmul [no_attr] "C_NODE" (i64ify [1;1]) "" ["A";"B"] ["C"] in
Printf.printf "Testing Matmul of 2 VECTORS of shape[2] \n" ;
env := [("A",{size = i64ify [2]; raw_data = ""});("B",{size = i64ify [2]; raw_data = ""})];
SMT.pp_cnode env v
| 4 ->
let v = NG.create_vertex 1 NG.Matmul [no_attr] "C_NODE" (i64ify [1;4]) "" ["A";"B"] ["C"] in
Printf.printf "Testing Matmul (3).(3,4): \n" ;
env := [("A",{size = i64ify [3]; raw_data = ""});("B",{size = i64ify [3;4]; raw_data = ""})];
SMT.pp_cnode env v
| 5 ->
let v = NG.create_vertex 1 NG.Matmul [no_attr] "C_NODE" (i64ify [4;1]) "" ["A";"B"] ["C"] in
Printf.printf "Testing Matmul (4,).(3): \n" ;
env := [("A",{size = i64ify [4;3]; raw_data = ""});("B",{size = i64ify [3]; raw_data = ""})];
SMT.pp_cnode env v
| 6 ->
let v = NG.create_vertex 1 NG.Matmul [no_attr] "C_NODE" (i64ify [5;4;1;3]) "" ["A";"B"] ["C"] in
Printf.printf "Testing Matmul (2).(5,4,2,3): \n" ;
env := [("A",{size = i64ify [2]; raw_data = ""});("B",{size = i64ify [5;4;2;3]; raw_data = ""})];
SMT.pp_cnode env v
| 7 ->
let v = NG.create_vertex 1 NG.Matmul [no_attr] "C_NODE" (i64ify [2;4;2;1]) "" ["A";"B"] ["C"] in
Printf.printf "Testing Matmul (3,4,2,2).(2): \n" ;
env := [("A", {size = i64ify [3;4;2;2]; raw_data = ""});("B", {size = i64ify [2]; raw_data = ""})];
SMT.pp_cnode env v
| 8 ->
let v = NG.create_vertex 1 NG.Matmul [no_attr] "C_NODE" (i64ify [2;4;2;2]) "" ["A";"B"] ["C"] in
Printf.printf "Testing Matmul (4;2;3).(2;1;3;2): \n" ;
env := [("A", {size = i64ify [4;2;3]; raw_data = ""});("B", {size = i64ify [2;1;3;2]; raw_data = ""})];
SMT.pp_cnode env v
| _ -> []
*)
(* let test = function
* (\* | 1 -> test_relu
* * | 2 -> old_test
* * | 3 -> test_add
* * | 4 -> test_mul *\)
* | NG.Matmul ->
* List.map test_matmul [(\* 1; 2; 3; 4; 5;6;7; *\)8]
* | _ -> failwith "No tests available with that number"
* *)
(* let test_transpose = *)
(* let v = NG.create_vertex 1 NG.Transpose [ints_attribute [1;2;0]] "C_NODE" *)
(* (i64ify [4;2;3]) "" ["A"] ["Res"] in *)
(* env := [("A",{size = i64ify [3;4;2]; raw_data = ""})]; *)
(* "Testing Transpose 120\n"::(SMT.pp_cnode env v ) *)
test/smtlib/property_CAMUS.smt2 0 → 100644
View file @ ffcb1947
;;;; We want to ensure that for any obstacle within the danger zone,
;;;; the output corresponding to the CHANGE DIRECTION order will always
;;;; be higher than the NO CHANGE order
;;;; Formulate constraint on inputs:
;; Inputs can be only between 0 and 1
(assert (or (= |CELL_actual_input_0_0_0_0| 0) (= |CELL_actual_input_0_0_0_0| 1)))
(assert (or (= |CELL_actual_input_0_0_0_1| 0) (= |CELL_actual_input_0_0_0_1| 1)))
(assert (or (= |CELL_actual_input_0_0_0_2| 0) (= |CELL_actual_input_0_0_0_2| 1)))
(assert (or (= |CELL_actual_input_0_0_0_3| 0) (= |CELL_actual_input_0_0_0_3| 1)))
(assert (or (= |CELL_actual_input_0_0_0_4| 0) (= |CELL_actual_input_0_0_0_4| 1)))
(assert (or (= |CELL_actual_input_0_0_0_5| 0) (= |CELL_actual_input_0_0_0_5| 1)))
(assert (or (= |CELL_actual_input_0_0_0_6| 0) (= |CELL_actual_input_0_0_0_6| 1)))
(assert (or (= |CELL_actual_input_0_0_0_7| 0) (= |CELL_actual_input_0_0_0_7| 1)))
(assert (or (= |CELL_actual_input_0_0_0_8| 0) (= |CELL_actual_input_0_0_0_8| 1)))
(assert (or (= |CELL_actual_input_0_0_0_9| 0) (= |CELL_actual_input_0_0_0_9| 1)))
(assert (or (= |CELL_actual_input_0_0_0_10| 0) (= |CELL_actual_input_0_0_0_10| 1)))
(assert (or (= |CELL_actual_input_0_0_0_11| 0) (= |CELL_actual_input_0_0_0_11| 1)))
(assert (or (= |CELL_actual_input_0_0_0_12| 0) (= |CELL_actual_input_0_0_0_12| 1)))
(assert (or (= |CELL_actual_input_0_0_0_13| 0) (= |CELL_actual_input_0_0_0_13| 1)))
(assert (or (= |CELL_actual_input_0_0_0_14| 0) (= |CELL_actual_input_0_0_0_14| 1)))
(assert (or (= |CELL_actual_input_0_0_0_15| 0) (= |CELL_actual_input_0_0_0_15| 1)))
(assert (or (= |CELL_actual_input_0_0_0_16| 0) (= |CELL_actual_input_0_0_0_16| 1)))
(assert (or (= |CELL_actual_input_0_0_0_17| 0) (= |CELL_actual_input_0_0_0_17| 1)))
(assert (or (= |CELL_actual_input_0_0_0_18| 0) (= |CELL_actual_input_0_0_0_18| 1)))
(assert (or (= |CELL_actual_input_0_0_0_19| 0) (= |CELL_actual_input_0_0_0_19| 1)))
(assert (or (= |CELL_actual_input_0_0_0_20| 0) (= |CELL_actual_input_0_0_0_20| 1)))
(assert (or (= |CELL_actual_input_0_0_0_21| 0) (= |CELL_actual_input_0_0_0_21| 1)))
(assert (or (= |CELL_actual_input_0_0_0_22| 0) (= |CELL_actual_input_0_0_0_22| 1)))
(assert (or (= |CELL_actual_input_0_0_0_23| 0) (= |CELL_actual_input_0_0_0_23| 1)))
(assert (or (= |CELL_actual_input_0_0_0_24| 0) (= |CELL_actual_input_0_0_0_24| 1)))
;; There is at least one input within the danger zone (pixels from 10)
;; that is equal to 1
(assert (or (= |CELL_actual_input_0_0_0_11| 1)
(= |CELL_actual_input_0_0_0_12| 1)
(= |CELL_actual_input_0_0_0_13| 1)
(= |CELL_actual_input_0_0_0_14| 1)
(= |CELL_actual_input_0_0_0_15| 1)
(= |CELL_actual_input_0_0_0_16| 1)
(= |CELL_actual_input_0_0_0_17| 1)
(= |CELL_actual_input_0_0_0_18| 1)
(= |CELL_actual_input_0_0_0_19| 1)
(= |CELL_actual_input_0_0_0_20| 1)
(= |CELL_actual_input_0_0_0_21| 1)
(= |CELL_actual_input_0_0_0_22| 1)
(= |CELL_actual_input_0_0_0_23| 1)
(= |CELL_actual_input_0_0_0_24| 1)
)
)
;; Formulate constraint on outputs:
;; Always fire such that the danger is detected
;; Fire such that no danger is detected
;; (assert (> actual_output_0_0_0_0 actual_output_0_0_0_1))
;; Alternate formulation
;; since we see that outputs are always of different signs,
;; we look that x0 > 0 (since it would mean x1 < 0 thus x0 > x1
(assert (> |CELL_actual_output_0_0_0_0| 0))
;; Only 3 pixels are white at maximum
(assert (> 3
(+ |CELL_actual_input_0_0_0_0| |CELL_actual_input_0_0_0_1|
|CELL_actual_input_0_0_0_2| |CELL_actual_input_0_0_0_3|
|CELL_actual_input_0_0_0_4| |CELL_actual_input_0_0_0_5|
|CELL_actual_input_0_0_0_6| |CELL_actual_input_0_0_0_7|
|CELL_actual_input_0_0_0_8| |CELL_actual_input_0_0_0_9|
|CELL_actual_input_0_0_0_10| |CELL_actual_input_0_0_0_11|
|CELL_actual_input_0_0_0_12| |CELL_actual_input_0_0_0_13|
|CELL_actual_input_0_0_0_14| |CELL_actual_input_0_0_0_15|
|CELL_actual_input_0_0_0_16| |CELL_actual_input_0_0_0_17|
|CELL_actual_input_0_0_0_18| |CELL_actual_input_0_0_0_19|
|CELL_actual_input_0_0_0_20| |CELL_actual_input_0_0_0_21|
|CELL_actual_input_0_0_0_22| |CELL_actual_input_0_0_0_23|
|CELL_actual_input_0_0_0_24|
)))
;; Check satisfiability
(check-sat)
(get-value (|CELL_actual_input_0_0_0_0|))
(get-value (|CELL_actual_input_0_0_0_1|))
(get-value (|CELL_actual_input_0_0_0_2|))
(get-value (|CELL_actual_input_0_0_0_3|))
(get-value (|CELL_actual_input_0_0_0_4|))
(get-value (|CELL_actual_input_0_0_0_5|))
(get-value (|CELL_actual_input_0_0_0_6|))
(get-value (|CELL_actual_input_0_0_0_7|))
(get-value (|CELL_actual_input_0_0_0_8|))
(get-value (|CELL_actual_input_0_0_0_9|))
(get-value (|CELL_actual_input_0_0_0_10|))
(get-value (|CELL_actual_input_0_0_0_11|))
(get-value (|CELL_actual_input_0_0_0_12|))
(get-value (|CELL_actual_input_0_0_0_13|))
(get-value (|CELL_actual_input_0_0_0_14|))
(get-value (|CELL_actual_input_0_0_0_15|))
(get-value (|CELL_actual_input_0_0_0_16|))
(get-value (|CELL_actual_input_0_0_0_17|))
(get-value (|CELL_actual_input_0_0_0_18|))
(get-value (|CELL_actual_input_0_0_0_19|))
(get-value (|CELL_actual_input_0_0_0_20|))
(get-value (|CELL_actual_input_0_0_0_21|))
(get-value (|CELL_actual_input_0_0_0_22|))
(get-value (|CELL_actual_input_0_0_0_23|))
(get-value (|CELL_actual_input_0_0_0_24|))
Supports Markdown
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