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

Merge branch 'facets' into 'master'

Facets

See merge request !1
parents 66a013e1 777b1949
......@@ -20,3 +20,5 @@ logs
*.merlin*
*.ipynb_checkpoints
*__pycache__*
.vscode/bookmarks.json
.vscode/settings.json
......@@ -243,6 +243,7 @@ module Vertex = struct
| Conv
| Identity
| NO_OP
| RW_Linearized_ReLu
let str_op o = match o with
| Add -> "Add"
| Mul -> "Mul"
......@@ -255,6 +256,7 @@ module Vertex = struct
| Conv -> "Conv"
| Identity -> "Identity"
| NO_OP -> "NO_OP"
| RW_Linearized_ReLu -> "RW_Linearized_ReLu"
let str_shape sh = match sh with
| [] -> "[]"
| _ -> "["^(Int.to_string (hd_id sh))^
......@@ -270,6 +272,7 @@ module Vertex = struct
| Pool_params of (ksize*stride option*pads option*dilations option)
| Conv_params of (ksize*stride option*pads option*dilations option)
| Transpose_params of shape
| RW_Linearized_ReLu_params of ((bool list list) * ((string, float) Base.Hashtbl.t list * int))
let str_op_params p = match p with
| Transpose_params s ->
let str_sh = str_shape s
......@@ -288,6 +291,12 @@ module Vertex = struct
in "Pool params: KSIZE: "^str_k^
", Pads: "^str_p^", Stride: "^str_s^
", Dilations: "^str_d
| RW_Linearized_ReLu_params l -> (* Only displays the activation scheme on the ReLU node *)
let activations = fst l in
let act' = List.map ~f:(fun l1 -> List.map ~f:(fun b -> match b with true -> "true" | false -> "false") l1) activations in
let act'' = List.map ~f:(fun l -> "["^(String.concat ~sep:";" l)^"]") act' in
let act''' = "["^(String.concat ~sep:";" act'')^"]" in
"RW_Linearized_ReLu_params: "^act'''
type t = {
id: id;
name: string option;
......
......@@ -124,6 +124,7 @@ module Vertex : sig
| Conv
| Identity
| NO_OP
| RW_Linearized_ReLu
(** Type describing the different operations handled.
Those operations are defined in the ONNX documentation.
......@@ -143,6 +144,8 @@ module Vertex : sig
| Pool_params of (ksize*stride option*pads option*dilations option)
| Conv_params of (ksize*stride option*pads option*dilations option)
| Transpose_params of shape
| RW_Linearized_ReLu_params of ((bool list list) * ((string, float) Base.Hashtbl.t list * int))
val str_op_params : operator_parameters -> string
(** Type encapsulating parameters for operations.
......
......@@ -9,8 +9,14 @@ let ilist_to_string l =
(List.fold_left (fun acc e -> acc^", "^(string_of_int e)) "" l)
^ "]"
let print_ints l = Printf.printf "%s" (ilist_to_string l)
let print_strs l = List.iter
(fun s -> Printf.printf "%s," s)
let print_int i = Printf.printf "%d" i
let print_bool = Printf.printf "%B"
let print_strs l = List.iter (fun s -> Printf.printf "%s," s) l
let print_str com s = Printf.printf "%s: %s" com s
let i64ify = List.map (Int64.of_int)
let intify = List.map (Int64.to_int)
(* let print_i64s l = List.iter (fun x -> printf " %d" (Int64.to_int x)) l *)
......@@ -37,7 +43,8 @@ let rec stringify = function
(* Header of the SMTLIB2 file *)
let pp_header t =
let logic_str = match t with
| Linear_Real_Theory | Real_Theory -> "QF_NRA"
| Linear_Real_Theory -> "QF_LRA"
| Real_Theory -> "QF_NRA"
| Float_Theory -> "QF_FP"
in
[";;This file has been generated with onnx2SMTtool";
......@@ -397,6 +404,48 @@ 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"
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")
| None -> failwith "Something is odd with the operator_parameters"
in
let tbl = Base.fst (Base.snd n_op) in
let to_activate = Base.fst n_op in
let relu_cell_to_smt idx =
let idx_str = stringify_int idx in
let idx_0 = Base.List.nth_exn idx 2 in (* Indexes working only for CAMUS networks *)
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 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
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
List.map relu_cell_to_smt (all_coords size)
(* Apparently Keras puts an identity layer at the end
* of its imported model, so we need to deal with them
* as well *)
......@@ -967,15 +1016,16 @@ let pp_cnode_cfg env (t:theory) g n =
| _ -> failwith "Only one output for C_Nodes, for now"
in
match n.IR.Vertex.operator with
| IR.Vertex.ReLu -> pp_relu_cfg succ_name n env t g
| IR.Vertex.Add -> pp_add_cfg succ_name n env t g
| IR.Vertex.Mul -> pp_mul_cfg succ_name n env t g
| IR.Vertex.Matmul -> pp_matmul_cfg succ_name n env t g
| IR.Vertex.Transpose -> pp_transpose_cfg succ_name n env g
| IR.Vertex.MaxPool -> pp_maxpool_cfg succ_name n env g
| IR.Vertex.Conv -> pp_conv_cfg succ_name n env g
| IR.Vertex.Identity -> pp_id_cfg succ_name n env g
|_ -> failwith "TODO operator in smtifyer.cnode"
| IR.Vertex.ReLu -> pp_relu_cfg succ_name n env t g
| IR.Vertex.Add -> pp_add_cfg succ_name n env t g
| IR.Vertex.Mul -> pp_mul_cfg succ_name n env t g
| IR.Vertex.Matmul -> pp_matmul_cfg succ_name n env t g
| IR.Vertex.Transpose -> pp_transpose_cfg succ_name n env g
| IR.Vertex.MaxPool -> pp_maxpool_cfg succ_name n env g
| IR.Vertex.Conv -> pp_conv_cfg succ_name n env g
| IR.Vertex.Identity -> pp_id_cfg succ_name n env g
| IR.Vertex.RW_Linearized_ReLu -> pp_relu_linear succ_name n env t g
| _ -> failwith "TODO operator in smtifyer.cnode"
(* Initialiser nodes are already in nier_graph.
So in addition of inputs and ouptus, the NAMED vertices may come from them
......
......@@ -71,6 +71,8 @@ val get_fp_serie_node :
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
val pp_relu_linear : string -> IR.Vertex.t -> env_cfg
-> theory -> IR.NierCFG.t -> string list
(** {2 Add } *)
......@@ -93,6 +95,7 @@ val pp_add_cfg : string -> IR.Vertex.t -> env_cfg ->
val pp_mul_cfg : string -> IR.Vertex.t -> env_cfg->
theory -> IR.NierCFG.t -> string list
val all_coords : int list -> int list list
(** {2 MatMul } *)
(** Various functions here to write correct flattened matrix multiplication *)
......@@ -121,6 +124,8 @@ val pp_transpose_cfg :
string -> IR.Vertex.t -> env_cfg -> IR.NierCFG.t
-> string list
(* val pp_linearize_cfg : string -> IR.Vertex.t -> (string * vdata_cfg) list ref -> IR.NierCFG.t -> IR.Vertex.operator *)
(** {1 Printer utilities } *)
val pp_cnode_cfg : env_cfg -> theory -> IR.NierCFG.t ->
......
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