From 958ac548a586beb6374fa54bb6d4484f40e91729 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Fri, 23 Sep 2022 12:11:28 +0200
Subject: [PATCH] Added meta nn filename for compatibility.
---
src/transformations/actual_net_apply.ml | 18 +++++++++++-------
1 file changed, 11 insertions(+), 7 deletions(-)
diff --git a/src/transformations/actual_net_apply.ml b/src/transformations/actual_net_apply.ml
index c6febc8..c07d551 100644
--- a/src/transformations/actual_net_apply.ml
+++ b/src/transformations/actual_net_apply.ml
@@ -6,6 +6,7 @@
open Why3
open Base
+open Utils
module IR = Ir.Nier_cfg
module G = Onnx.G
@@ -307,12 +308,13 @@ let terms_of_nier g ty_inputs env ~net_output_vars ~net_input_vars =
(* Create logic symbols for input variables and replace
* nnet_apply by control flow terms. *)
let actual_nn_flow env =
- let rec substitute_net_apply (term : Term.term) =
+ let rec substitute_net_apply meta (term : Term.term) =
match term.t_node with
| Term.Tapp (ls, args) -> (
match Language.lookup_loaded_nets ls with
- | None -> Term.t_map substitute_net_apply term
+ | None -> Term.t_map (substitute_net_apply meta) term
| Some nn ->
+ meta := nn.filename :: !meta;
let g =
match nn.nier with
| Some g -> g
@@ -333,24 +335,26 @@ let actual_nn_flow env =
]
~net_input_vars
in
- Stdio.printf "\nObtained term: \n%!";
- Pretty.print_term Fmt.stdout cfg_term;
- Stdio.printf "\n%!";
cfg_term)
- | _ -> Term.t_map substitute_net_apply term
+ | _ -> Term.t_map (substitute_net_apply meta) term
in
Trans.fold
(fun task_hd task ->
match task_hd.task_decl.td_node with
| Use _ | Clone _ | Meta _ -> Task.add_tdecl task task_hd.task_decl
| Decl decl ->
+ let meta = ref [] in
let decl =
Decl.decl_map
(fun term ->
- let term = substitute_net_apply term in
+ let term = substitute_net_apply meta term in
term)
decl
in
+ let task =
+ List.fold !meta ~init:task ~f:(fun task s ->
+ Task.add_meta task meta_nn_filename [ MAstr s ])
+ in
Task.add_decl task decl)
None
--
GitLab