From 98f9df489564be1d581288a94882320fecd17781 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Thu, 22 Sep 2022 14:30:19 +0200
Subject: [PATCH] [TRANS] Provided backward NIER traversal.
---
src/transformations/actual_net_apply.ml | 209 ++++++++++--------------
1 file changed, 88 insertions(+), 121 deletions(-)
diff --git a/src/transformations/actual_net_apply.ml b/src/transformations/actual_net_apply.ml
index d188b5c..5eb9e9e 100644
--- a/src/transformations/actual_net_apply.ml
+++ b/src/transformations/actual_net_apply.ml
@@ -7,27 +7,7 @@
open Why3
open Base
module IR = Ir.Nier_cfg
-
module G = Onnx.G
-(** TODO: * declare function symbols in caisar stdlib: * * relu * * addition
-
- * variables definitions: * * build a homemade environment that stores all
- met variables * * use default floating points precision settings for now
-
- * NIER traversal: * * traverse in correct order * * given a NIER node,
- register new variables
-
- The goal is to be able to plug to other existing transforms: given
- net_apply, replace it by a neural network control flow (with all operations
- replaced by identity for now). *)
-
-(** TODO:
-
- - 09-09-2022: ensure that the graph traversal operations are properly done
- - 14-09-2022: build floating point value if input_types is indeed float
- point values
- - 16-09-2022: figure out how to accumulate terms and bind them, and how to
- declare the semantic of net_apply in the formula *)
exception UnsupportedOperator of string
@@ -57,9 +37,7 @@ let term_of_data d ty =
let rl =
if String.equal d_s "0x0p+0"
then Number.real_literal ~radix:16 ~neg:false ~int:"0" ~frac:"0" ~exp:None
- else (
- Stdio.printf "onche\n%!";
- Stdio.printf "%s\n" d_s;
+ else
(* Thanks to a similar function in Frama-C's WP plugin *)
let re_float =
Re__Pcre.regexp "-?0x([0-9a-f]+).([0-9a-f]+)?0*p?([+-]?[0-9a-f]+)?$"
@@ -74,7 +52,7 @@ let term_of_data d ty =
in
let exp = if String.equal exp "" then None else Some exp in
let is_neg = Float.( <= ) d 0. in
- Number.real_literal ~radix:16 ~neg:is_neg ~int ~frac ~exp)
+ Number.real_literal ~radix:16 ~neg:is_neg ~int ~frac ~exp
in
Term.t_const
(Constant.real_const ~pow2:rl.rl_real.rv_pow2 ~pow5:rl.rl_real.rv_pow5
@@ -113,38 +91,28 @@ let mul v1 v2 ty_vars env =
let bind v ~t ~e = Term.t_let_close v t e
let _register_data_env _g _env = ()
-(* create terms defining the equality between two list of variables.
+(* Create terms defining the equality between two list of variables.
* Assuming equal size between in_vars and out_vars,
* resulting terms declare the equality between in_vars[i]
* and out_vars[i]*)
-let id_on in_vars out_vars expr =
- Stdio.printf "%d%!\n" (List.length in_vars);
- Stdio.printf "%d%!\n" (List.length out_vars);
+let id_on ~in_vars ~out_vars expr =
if List.length in_vars <> List.length out_vars
then
failwith
"Error, expecting same amount of variables before declaring equality"
else
- let eq_terms =
- List.foldi ~init:expr in_vars ~f:(fun i in_var e ->
- Stdio.printf "\nin_var:%!";
- Pretty.print_term Fmt.stdout in_var;
- Stdio.printf "\nexpression:%!";
- Pretty.print_term Fmt.stdout e;
- Stdio.printf "\nout_var:%!";
- Pretty.print_term Fmt.stdout (Term.t_var @@ List.nth_exn out_vars i);
- bind (List.nth_exn out_vars i) ~t:in_var ~e)
+ let eq_term =
+ List.foldi ~init:expr in_vars ~f:(fun i e in_var ->
+ bind (List.nth_exn out_vars i) ~t:(Term.t_var in_var) ~e)
in
- eq_terms
+ eq_term
-(* create terms defining the ReLU activation function
+(* Create terms defining the ReLU activation function
* application between two list of variables.
* Assuming equal size between in_vars and out_vars,
* resulting terms defines in_vars[i] = relu(out_vars[i])
* *)
-let relu in_vars out_vars env expr =
- Stdio.printf "%d%!\n" (List.length in_vars);
- Stdio.printf "%d%!\n" (List.length out_vars);
+let relu ~in_vars ~out_vars env expr =
if List.length in_vars <> List.length out_vars
then
failwith
@@ -154,40 +122,47 @@ let relu in_vars out_vars env expr =
let nn = Pmodule.read_module env [ "caisar" ] "NN" in
Theory.(ns_find_ls nn.mod_theory.th_export [ "relu" ])
in
- let eq_terms =
- List.foldi ~init:expr in_vars ~f:(fun i in_var e ->
- let relu_on = Term.t_app_infer relu_s [ in_var ] in
- bind (List.nth_exn out_vars i) ~t:relu_on ~e)
+ let eq_term =
+ List.foldi ~init:expr in_vars ~f:(fun i e in_var ->
+ let relu_on = Term.t_app_infer relu_s [ Term.t_var in_var ] in
+ bind (List.nth_exn in_vars i) ~t:relu_on ~e)
in
- eq_terms
+ eq_term
-(* create terms defining the element-wise addition between
+(* Create terms defining the element-wise addition between
* two list of variables and a data_node. Assuming equal size between
* in_vars and out_vars, resulting term declares out_vars[i]
* = in_vars + data[i] *)
-let eltw_sum in_vars out_vars data_node ty_vars env expr =
+let eltw_sum ~in_vars ~out_vars data_node ty_vars env expr =
let data =
match IR.Node.get_tensor data_node with Some t -> t | None -> assert false
in
let data_vars =
List.map ~f:(fun v -> term_of_data v ty_vars) (IR.Tensor.flatten data)
in
- Stdio.printf "in_vars of eltw_sum %d\n%!" (List.length in_vars);
- Stdio.printf "out_vars of eltw_sum %d\n%!" (List.length out_vars);
- Stdio.printf "data_vars of eltw_sum %d\n%!" (List.length data_vars);
match
List.fold2 ~init:(expr, 0) in_vars data_vars ~f:(fun (e, i) in_var d ->
- (bind (List.nth_exn out_vars i) ~t:(sum in_var d ty_vars env) ~e, i + 1))
+ ( bind (List.nth_exn out_vars i)
+ ~t:(sum (Term.t_var in_var) d ty_vars env)
+ ~e,
+ i + 1 ))
with
| List.Or_unequal_lengths.Ok (e, _) -> e
| List.Or_unequal_lengths.Unequal_lengths ->
failwith "Error in element-wise sum: incoherent list length."
-(* create terms defining the matrix multiplication between
- * two list of variables and a data_node. Assuming equal size between
- * in_vars and out_vars, resulting term declares
- * out_vars[i,j] = sum_k in_vars[i,k] * data[k,j] *)
-let matmul in_vars out_vars data_node in_shape out_shape ty_vars env expr =
+(* Expected semantic:
+ * Matrices A [n;m] B [m;p] C [n;p]
+ * C = AB
+ * C[i,j] = sum_k A[i;k] * B[k;j]
+ *
+ * Create terms defining the matrix multiplication between
+ * two list of variables a_vars, c_vars and a data_node.
+ * b_vars is built using datas stored in data_node.
+ * a_vars are the input variables
+ * c_vars the output variables
+ * c_vars[i,j] = sum_k a_vars[i,k] * b_vars[k,j] *)
+let matmul ~in_vars ~out_vars data_node ~in_shape ~out_shape ty_vars env expr =
let data =
match IR.Node.get_tensor data_node with Some t -> t | None -> assert false
in
@@ -195,133 +170,118 @@ let matmul in_vars out_vars data_node in_shape out_shape ty_vars env expr =
let data_vars =
List.map ~f:(fun v -> term_of_data v ty_vars) (IR.Tensor.flatten data)
in
- Stdio.printf "in_vars of matmul %d\n%!" (List.length in_vars);
- Stdio.printf "out_vars of matmul %d\n%!" (List.length out_vars);
- Stdio.printf "data_vars of matmul %d\n%!" (List.length data_vars);
- let rec matmul_terms (i, j, t) ~y_var ~a_var ~b_var ~y_shape ~a_shape ~b_shape
+ let rec matmul_terms (i, j, t) ~c_var ~a_var ~b_var ~c_shape ~a_shape ~b_shape
=
- match y_var with
+ match c_var with
| [] -> (i, j, t)
| x :: y ->
- (* y[i,j] = sum_k a[i,k]*b[k,j]*)
+ (* c[i,j] = sum_k a[i,k]*b[k,j]*)
(*a_var_range: all line of a *)
(*b_var_range: all column of b *)
(* TODO: be sure that the common dimension is indeed
* b_shape[0] *)
let k_dim = Array.get b_shape 0 in
let a_var_range =
- Stdio.printf "We are in a_var_range\n%!";
- Stdio.printf "a_shape: %s \n%!" (IR.Node.show_shape a_shape);
List.init
~f:(fun k ->
- let idx = [| i; k |] in
- Stdio.printf "idx_to_get: %s \n%!" (IR.Node.show_shape idx);
- IR.Tensor.get_flatnd_idx ~idx ~sh:b_shape b_var)
+ let idx = [| 0; 0; i; k |] in
+ IR.Tensor.get_flatnd_idx ~idx ~sh:a_shape a_var)
k_dim
and b_var_range =
- Stdio.printf "We are in b_var_range\n%!";
- Stdio.printf "b_shape: %s \n%!" (IR.Node.show_shape b_shape);
List.init
~f:(fun k ->
let idx = [| k; j |] in
- Stdio.printf "idx_to_get: %s \n%!" (IR.Node.show_shape idx);
let data = IR.Tensor.get data idx in
- Stdio.printf "%f\n" data;
term_of_data data ty_vars)
k_dim
in
let muls =
match
- List.map2 a_var_range b_var_range ~f:(fun a b -> mul a b ty_vars env)
+ List.map2 a_var_range b_var_range ~f:(fun a b ->
+ mul (Term.t_var a) b ty_vars env)
with
| List.Or_unequal_lengths.Ok l -> l
| List.Or_unequal_lengths.Unequal_lengths ->
failwith "Wrong inferred common dimension"
in
let new_term =
- List.fold
- ~init:(Term.t_real_const BigInt.zero)
+ List.fold ~init:(term_of_data 0.0 ty_vars)
~f:(fun term mul -> sum term mul ty_vars env)
muls
in
let new_term = bind x ~t:new_term ~e:t in
- matmul_terms (i, j, new_term) ~y_var:y ~a_var ~b_var ~y_shape ~a_shape
+ matmul_terms (i, j, new_term) ~c_var:y ~a_var ~b_var ~c_shape ~a_shape
~b_shape
in
let _, _, terms =
- matmul_terms (0, 0, expr) ~y_var:out_vars ~b_var:data_vars ~a_var:in_vars
- ~y_shape:out_shape ~b_shape:data_shape ~a_shape:in_shape
+ matmul_terms (0, 0, expr) ~c_var:out_vars ~b_var:data_vars ~a_var:in_vars
+ ~c_shape:out_shape ~b_shape:data_shape ~a_shape:in_shape
in
terms
-let terms_of_nier g ty_inputs env starting_term =
+let terms_of_nier g ty_inputs env ~output_vars ~input_vars =
IR.out_cfg_graph g;
+ let vs =
+ let l = G.vertex_list g in
+ List.drop_while ~f:(fun n -> not (IR.Node.is_output_node n)) l
+ in
let _, expr =
- (* folding goes by increasing id order.
+ (* folding goes by decreasing id order, backward.
* Only accumulate new terms while going through the
- * control flow; once the output node has been reached,
+ * control flow; once the input node has been reached,
* only return the terms. *)
- G.fold_vertex
- (fun n ((in_vars, in_shape, is_finished), expr) ->
+ List.fold vs
+ ~init:
+ ( (output_vars, IR.Node.get_shape @@ List.nth_exn vs 0, false),
+ Term.t_tuple @@ List.map ~f:Term.t_var output_vars )
+ ~f:(fun ((out_vars, out_shape, is_finished), expr) n ->
if is_finished
then (([], [||], true), expr)
else
let open IR in
- Stdio.printf "\n%s\n" (Node.show n Float.to_string);
- Stdio.printf "in_shape: %s\n" (Node.show_shape in_shape);
- let out_shape =
+ let in_shape =
match Node.get_shape n with
- | [||] -> G.infer_shape g n in_shape ~on_backward:true
+ | [||] -> G.infer_shape g n out_shape ~on_backward:true
| a -> a
in
let node_id = n.id in
- Stdio.printf "\nInferred shape: %s\n" (Node.show_shape out_shape);
- let node_vs_out =
+ let node_vs_in =
List.init
~f:(fun i ->
- create_var ("out_" ^ Int.to_string node_id) i ty_inputs vars)
- (List.length (Tensor.all_coords out_shape))
+ create_var ("in_id_" ^ Int.to_string node_id) i ty_inputs vars)
+ (List.length (Tensor.all_coords in_shape))
in
- let (node_compute_terms : Term.term) =
+ let node_compute_term =
(* TODO: axiomatize the resulting term using
* let d = Decl.create_prop_decl Paxiom ps t *)
match IR.Node.get_op n with
| Node.Matmul -> (
match G.data_node_of n g with
| Some d_n ->
- matmul in_vars node_vs_out d_n in_shape out_shape ty_inputs env
- expr
+ matmul ~in_vars:node_vs_in ~out_vars d_n ~in_shape ~out_shape
+ ty_inputs env expr
| None -> failwith "Error, Matmul operator lacks a data node")
| Node.Add -> (
match G.data_node_of n g with
- | Some d_n -> eltw_sum in_vars node_vs_out d_n ty_inputs env expr
+ | Some d_n ->
+ eltw_sum ~out_vars ~in_vars:node_vs_in d_n ty_inputs env expr
| None -> failwith "Error, Add operator lacks a data node")
| Node.NO_OP ->
(* If it is the input node, build variables
* using neuron input node *)
if Node.is_input_node n
then
- let net_in_vars =
- List.init
- ~f:(fun i -> Term.t_var @@ create_var "x" i ty_inputs vars)
- (List.length @@ IR.Tensor.all_coords out_shape)
- in
- id_on net_in_vars node_vs_out expr
- (* If it is the output node, build variables
- * using neuron output node *)
+ id_on ~out_vars:input_vars ~in_vars:node_vs_in expr
+ (* If it is the output node, the resulting
+ * term is the tuple of the output variables
+ * of the net;
+ * backpropagate those to the previous layer*)
else if Node.is_output_node n
then
- let net_out_vars =
- List.init
- ~f:(fun i -> Term.t_var @@ create_var "y" i ty_inputs vars)
- (List.length @@ IR.Tensor.all_coords out_shape)
- in
-
- id_on net_out_vars node_vs_out expr
- (* We folded over all vertex with operators,
- * stop accumulating terms *)
+ id_on ~out_vars:output_vars ~in_vars:node_vs_in
+ (Term.t_tuple @@ List.map ~f:Term.t_var output_vars)
else expr
- | IR.Node.ReLu -> relu in_vars node_vs_out env expr
+ | IR.Node.ReLu -> relu ~out_vars ~in_vars:node_vs_in env expr
| op ->
raise
(UnsupportedOperator
@@ -329,11 +289,7 @@ let terms_of_nier g ty_inputs env starting_term =
"Operator %s is not implemented for actual_net_apply."
(IR.Node.str_op op)))
in
- Stdio.printf "Finished dealing with this node%!\n";
- ( (List.map ~f:Term.t_var node_vs_out, out_shape, false),
- node_compute_terms ))
- g
- (([], [||], false), starting_term)
+ ((node_vs_in, out_shape, false), node_compute_term))
in
expr
@@ -342,7 +298,7 @@ let terms_of_nier g ty_inputs env starting_term =
let actual_nn_flow env =
let rec aux (term : Term.term) =
match term.t_node with
- | Term.Tapp (ls, _) -> (
+ | Term.Tapp (ls, _args) -> (
match Language.lookup_loaded_nets ls with
| None -> Term.t_map aux term
| Some nn ->
@@ -354,9 +310,20 @@ let actual_nn_flow env =
let ty_inputs = nn.ty_data in
let cfg_term =
terms_of_nier g ty_inputs env
- (Term.t_var @@ create_var "dummy" 0 ty_inputs vars)
+ ~output_vars:
+ [
+ create_var "y" 1 ty_inputs vars; create_var "y" 2 ty_inputs vars;
+ ]
+ ~input_vars:
+ [
+ create_var "x" 1 ty_inputs vars;
+ create_var "x" 2 ty_inputs vars;
+ create_var "x" 3 ty_inputs vars;
+ ]
in
+ Stdio.printf "\nObtained term: \n%!";
Pretty.print_term Fmt.stdout cfg_term;
+ Stdio.printf "\n%!";
cfg_term)
| _ -> Term.t_map aux term
in
--
GitLab