Commit ceb6ab6a authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

wrong indent and updated tests

parent 24e5ebdd
......@@ -10,5 +10,7 @@ bins:$(BIN_DIR)$(SRCS)
onnx2SMT:$(LIB_DIR)$(SRCS)
dune build $(LIB_DIR)
doc:
doc:
dune build @doc
all:
dune build @install
(library
(name nnet)
(public_name ISAIEH.output.nnet)
(preprocess (pps ppx_inline_test))
(inline_tests)
(libraries ocplib-endian piqirun.pb zarith ocamlgraph ISAIEH.ir))
(env
(dev
(flags (:standard -warn-error -A))
))
This diff is collapsed.
(** This module provide tools to convert a valid NIER
into a SMTLIB2 formula.
NIER (defined in {!module:Nier_cfg}) encapsulate
parameters in tensor
forms and a computation graph with various operations.
On the other hand, SMTLIB2 format only supports
individual variables.
This module provide tools to properly translate NIER
data into SMTLIB2
formula. Variables are stored inside of an environment,
their shape being
either provided by the NIER or inferred with the
expected result
of ONNX operations.
@author Zakaria Chihani, Julien Girard
*)
module IR = Ir.Nier_cfg
(** {1 Definition of the supported theories
for SMTLIB2 output format} *)
type theory = Real_Theory | Float_Theory | Linear_Real_Theory
(** {1 Environment utilities} *)
(** Environment stores shapes and raw data for all variables.
An environment is a list of tuple (string; vdata) representing the name
of the variable, its corresponding shape and the (potentially empty)
raw data linked to that node *)
type vdata_cfg = {shape: IR.Vertex.shape ;data : IR.Tensor.t option}
type env_cfg = (string * vdata_cfg) list ref
val env_init_cfg : env_cfg
val pp_shape_cfg : int list -> unit
val pp_env_cfg : (string * vdata_cfg) list ref -> unit
val get_declarations_cfg : (string * vdata_cfg) list ref ->
theory -> string list
(** [get_declarations_cfg env t ] build the string corresponding to the declaration
of all variables in [env] and their value if necessary
according to theory t *)
(** {1 Padding and broadcast utilities} *)
(** When computing operations with tensors of different shapes, it is sometimes
necessary to perform padding and broadcasting operations.
Padding add dimensions to an array on the left or on the right,
if necessary.
Broadcasting consists on modifying the dimensions of two arrays
to obtain compatible dimensions without changing the underlying data.
For instance, a matrix of shape [3,2] multiplied (matrix multiplication)
with a vector of shape [2] is not a valid operation, but becomes valid
if the shape of the vector is [2,1]. The operation will result on a
vector of shape [2,1]. For more information,
@see <https://github.com/onnx/onnx/blob/master/docs/Broadcasting.md> *)
val one_padding_cfg : int list -> int -> int list
val pad_left_cfg : int list -> int list
val pad_right_cfg : int list -> int list
val pad_cfg : int list -> int list -> int list * int list
val broadcast_cfg : int list -> int list -> int list
val getSerie : string -> string -> string list -> string
val get_fp_serie_node :
string list -> string -> string list -> string -> string list
(** {1 ONNX Operators pretty printers and utilities } *)
val get_unary_op : string -> string -> string -> string list -> string list
val pp_relu_cfg : string -> IR.Vertex.t -> env_cfg
-> theory -> IR.NierCFG.t -> string list
(** {2 Add } *)
val pp_add_cell_cfg :
int list ->
string ->
int list ->
string -> int list -> string -> int list -> theory ->
string list ref -> unit
(** [pp_add_cell idx a adim b bdim c cdim res] build the string
corresponding to the evaluation of the Add operation on
matrix [a] of shape [adim] and [b] of shape [bdim], with
matrix [c] of shape [cdim] storing the result *)
val pp_add_cfg : string -> IR.Vertex.t -> env_cfg ->
theory -> IR.NierCFG.t -> string list
(** {2 Mul } *)
val pp_mul_cfg : string -> IR.Vertex.t -> env_cfg->
theory -> IR.NierCFG.t -> string list
(** {2 MatMul } *)
(** Various functions here to write correct flattened matrix multiplication *)
val check_matmul_size_cfg : int list -> int list -> int * int list
val pp_matmul_cell :
int list ->
int -> int -> string -> int list -> string -> int list -> theory ->
int -> string
val mat_mul_cell :
int list ->
int list ->
string ->
int list -> string -> int list -> string -> int -> string list ref ->
theory -> unit
val pp_matmul_cfg :
string -> IR.Vertex.t -> env_cfg->
theory -> IR.NierCFG.t -> string list
(** {2 Transpose } *)
val pp_transpose_default : string -> string -> int list -> string list
val inversed_shape : int -> int list
val permute_idx_cfg : int array -> int array -> string
val perm_shape_cfg : int list -> int list -> int list
val pp_transpose_cfg :
string -> IR.Vertex.t -> env_cfg -> IR.NierCFG.t
-> string list
(** {1 Printer utilities } *)
val pp_cnode_cfg : env_cfg -> theory -> IR.NierCFG.t ->
IR.Vertex.t -> string list
val pp_IOnode_cfg : env_cfg-> IR.Vertex.t -> unit
(** [pp_graph_cfg g t] transforms the computational
graph under a string list with SMTLIB2 format,
according to theory [t].
Each element of the returned list is a line of SMTLIB2.*)
val pp_graph_cfg : IR.NierCFG.t -> theory -> string list
(library
(name onnx)
(public_name ISAIEH.output.onnx)
(preprocess (pps ppx_inline_test))
(inline_tests)
(libraries ocplib-endian piqirun.pb zarith ocamlgraph ISAIEH.ir))
(env
(dev
(flags (:standard -warn-error -A))
))
This diff is collapsed.
(** This module provide tools to convert a valid NIER
into a SMTLIB2 formula.
NIER (defined in {!module:Nier_cfg}) encapsulate
parameters in tensor
forms and a computation graph with various operations.
On the other hand, SMTLIB2 format only supports
individual variables.
This module provide tools to properly translate NIER
data into SMTLIB2
formula. Variables are stored inside of an environment,
their shape being
either provided by the NIER or inferred with the
expected result
of ONNX operations.
@author Zakaria Chihani, Julien Girard
*)
module IR = Ir.Nier_cfg
(** {1 Definition of the supported theories
for SMTLIB2 output format} *)
type theory = Real_Theory | Float_Theory | Linear_Real_Theory
(** {1 Environment utilities} *)
(** Environment stores shapes and raw data for all variables.
An environment is a list of tuple (string; vdata) representing the name
of the variable, its corresponding shape and the (potentially empty)
raw data linked to that node *)
type vdata_cfg = {shape: IR.Vertex.shape ;data : IR.Tensor.t option}
type env_cfg = (string * vdata_cfg) list ref
val env_init_cfg : env_cfg
val pp_shape_cfg : int list -> unit
val pp_env_cfg : (string * vdata_cfg) list ref -> unit
val get_declarations_cfg : (string * vdata_cfg) list ref ->
theory -> string list
(** [get_declarations_cfg env t ] build the string corresponding to the declaration
of all variables in [env] and their value if necessary
according to theory t *)
(** {1 Padding and broadcast utilities} *)
(** When computing operations with tensors of different shapes, it is sometimes
necessary to perform padding and broadcasting operations.
Padding add dimensions to an array on the left or on the right,
if necessary.
Broadcasting consists on modifying the dimensions of two arrays
to obtain compatible dimensions without changing the underlying data.
For instance, a matrix of shape [3,2] multiplied (matrix multiplication)
with a vector of shape [2] is not a valid operation, but becomes valid
if the shape of the vector is [2,1]. The operation will result on a
vector of shape [2,1]. For more information,
@see <https://github.com/onnx/onnx/blob/master/docs/Broadcasting.md> *)
val one_padding_cfg : int list -> int -> int list
val pad_left_cfg : int list -> int list
val pad_right_cfg : int list -> int list
val pad_cfg : int list -> int list -> int list * int list
val broadcast_cfg : int list -> int list -> int list
val getSerie : string -> string -> string list -> string
val get_fp_serie_node :
string list -> string -> string list -> string -> string list
(** {1 ONNX Operators pretty printers and utilities } *)
val get_unary_op : string -> string -> string -> string list -> string list
val pp_relu_cfg : string -> IR.Vertex.t -> env_cfg
-> theory -> IR.NierCFG.t -> string list
(** {2 Add } *)
val pp_add_cell_cfg :
int list ->
string ->
int list ->
string -> int list -> string -> int list -> theory ->
string list ref -> unit
(** [pp_add_cell idx a adim b bdim c cdim res] build the string
corresponding to the evaluation of the Add operation on
matrix [a] of shape [adim] and [b] of shape [bdim], with
matrix [c] of shape [cdim] storing the result *)
val pp_add_cfg : string -> IR.Vertex.t -> env_cfg ->
theory -> IR.NierCFG.t -> string list
(** {2 Mul } *)
val pp_mul_cfg : string -> IR.Vertex.t -> env_cfg->
theory -> IR.NierCFG.t -> string list
(** {2 MatMul } *)
(** Various functions here to write correct flattened matrix multiplication *)
val check_matmul_size_cfg : int list -> int list -> int * int list
val pp_matmul_cell :
int list ->
int -> int -> string -> int list -> string -> int list -> theory ->
int -> string
val mat_mul_cell :
int list ->
int list ->
string ->
int list -> string -> int list -> string -> int -> string list ref ->
theory -> unit
val pp_matmul_cfg :
string -> IR.Vertex.t -> env_cfg->
theory -> IR.NierCFG.t -> string list
(** {2 Transpose } *)
val pp_transpose_default : string -> string -> int list -> string list
val inversed_shape : int -> int list
val permute_idx_cfg : int array -> int array -> string
val perm_shape_cfg : int list -> int list -> int list
val pp_transpose_cfg :
string -> IR.Vertex.t -> env_cfg -> IR.NierCFG.t
-> string list
(** {1 Printer utilities } *)
val pp_cnode_cfg : env_cfg -> theory -> IR.NierCFG.t ->
IR.Vertex.t -> string list
val pp_IOnode_cfg : env_cfg-> IR.Vertex.t -> unit
(** [pp_graph_cfg g t] transforms the computational
graph under a string list with SMTLIB2 format,
according to theory [t].
Each element of the returned list is a line of SMTLIB2.*)
val pp_graph_cfg : IR.NierCFG.t -> theory -> string list
......@@ -98,14 +98,14 @@ let all_coords sh =
let rec ranges acc sh = match sh with
| x::y -> ranges ((List.init x (fun i -> i))::acc) y
| [] -> acc
(* a list containing a list of all possible indexes, for each dimension *)
(* a list containing a list of all possible indexes, for each dimension *)
in let xxs = ranges [] sh in
(* add to each element of the list of all possible coordinates all
* possible indexes ... *)
let aux acc xs = List.concat @@
List.map (fun x -> List.map (fun lt -> x::lt) acc) xs
(* ... for each dimension, starting from an empty list of
* possible coordinates *)
(* ... for each dimension, starting from an empty list of
* possible coordinates *)
in List.fold_left aux [[]] xxs
let get_flat_indices_cfg shape =
let coords_int = all_coords shape
......@@ -404,19 +404,19 @@ let pp_relu_cfg tname n env t g =
in
set_shape_cfg tname size env;
get_unary_op (relu_fun t) pname tname (get_flat_indices_cfg size)
(* Assigns to each cell of the input tensor the SMT formula corresponding to the application of the ReLU function *)
let pp_relu_linear tname n env t g =
let (pname,size) = match IR.NierCFG.pred_e g n with
| [(_,x,_)] -> (x, (get_shape_cfg x env))
| _ -> failwith "More than one input for ReLU"
| [(_,x,_)] -> (x, (get_shape_cfg x env))
| _ -> failwith "More than one input for ReLU"
in
set_shape_cfg tname size env;
let n_op = match n.operator_parameters with
| Some p -> (match p with
| IR.Vertex.RW_Linearized_ReLu_params x -> x
| _ -> failwith "Something is odd with the type of the operator_parameters")
| IR.Vertex.RW_Linearized_ReLu_params x -> x
| _ -> failwith "Something is odd with the type of the operator_parameters")
| None -> failwith "Something is odd with the operator_parameters"
in
let tbl = Base.fst (Base.snd n_op) in
......@@ -427,23 +427,23 @@ let pp_relu_linear tname n env t g =
let idx_1 = Base.List.nth_exn idx 3 in (* Indexes working only for CAMUS networks *)
(* let idx_0 = Base.List.nth_exn idx 1 in (* Indexes working only for ACAS Xu networks *) *)
(* let idx_1 = Base.List.nth_exn idx 0 in (* Indexes working only for ACAS Xu networks *) *)
let constraint_string =
let constraint_string =
let table = Base.List.nth_exn tbl idx_1 in
let tl = Base.Hashtbl.to_alist table in
let tl_f = fun (k,v) -> (match k with "b" -> ("b", v) | _ -> (Base.List.nth_exn (Base.String.split ~on:'x' k) 1), v) in
let table_list = Base.List.map ~f:(tl_f) tl in
Base.List.fold table_list ~init:"" ~f:(fun acc (k, v) -> match k with
| "b" -> acc^(float_of_string_accurate v t)
| _ -> acc^" (* "^"|CELL_actual_input_0_0_0_"^k^"| "^(float_of_string_accurate v t)) in
| "b" -> acc^(float_of_string_accurate v t)
| _ -> acc^" (* "^"|CELL_actual_input_0_0_0_"^k^"| "^(float_of_string_accurate v t))
in
match Base.List.nth_exn (Base.List.nth_exn to_activate idx_1) idx_0
with
| true -> "(assert (= |CELL_"^tname^idx_str^"| |CELL_"^pname^idx_str^"|))\n(assert (< 0 (+"^constraint_string^"))"
| false -> begin match t with
| Linear_Real_Theory | Real_Theory -> "(assert (= |CELL_"^tname^idx_str^"| 0))\n(assert (> 0 (+"^constraint_string^"))"
| Float_Theory -> "(assert (= |CELL_"^tname^idx_str^"| (_ +zero 11 53)))^\n(assert (> (_ +zero 11 53) (+"^constraint_string^"))"
end
in
end
in
List.map relu_cell_to_smt (all_coords size)
(* Apparently Keras puts an identity layer at the end
......
(tests
(package ISAIEH)
(names print_graph)
(libraries ISAIEH.onnx_parser ISAIEH.piqi_interface ISAIEH.output.smt))
(libraries ISAIEH.onnx_parser ISAIEH.piqi_interface ISAIEH.output.smt
ISAIEH.ir))
(env
(dev
......
module Parser = Onnx_parser
module Onnxpq = Piqi_interface.Onnx_piqi
module NCFG = Ir.Nier_cfg
module T = Ir.Nier_cfg.Tensor
module V = Ir.Nier_cfg.Vertex
module N = Ir.Nier_cfg.NierCFG
exception Nograph of string
(* Reads the ONNX model from a file, print graph within*)
let printf = Printf.printf
let unpack x = match x with
| Some x -> x
| None -> (T.create [0;])
(* printf "%s" (Sys.getcwd ());; *)
let _ =
(* let input_file = "../../../test/onnx/test_simple.onnx" in *)
......@@ -13,7 +19,7 @@ let _ =
| Some g -> g
| None -> raise (Nograph "No graph in ONNX input file!") in
(* let nir_graph = Parser.node_graph graph in *)
(* Array.iter (fun x -> NG.pp_node x) nir_graph *)
let cfg = Parser.produce_cfg graph in
N.iter_vertex (fun x -> printf "%s\n" (T.show (unpack x.V.tensor))) cfg;
NCFG.print_cfg_graph cfg; NCFG.out_cfg_graph cfg
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