From 2aa66aff9bfe31fd7fb9c064dff99474d0a02043 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Mon, 21 Nov 2016 11:26:28 +0100
Subject: [PATCH] V6 rdbg-plugin: add code to be able to debug sub-nodes from
rdbg.
I have duplicated the interpretation function SocExec.soc_step
into a CPS SocExecDbg.soc_step
One day I migth only keep the dbg one.
---
_oasis | 2 +-
src/lv6version.ml | 4 +-
src/socExec.ml | 8 +-
src/socExecDbg.ml | 283 ++++++++++++++++++++++++++++++++++++++++++--
src/socExecValue.ml | 8 +-
test/lus2lic.sum | 28 ++---
6 files changed, 297 insertions(+), 36 deletions(-)
diff --git a/_oasis b/_oasis
index e2683a14..ffe1b62b 100644
--- a/_oasis
+++ b/_oasis
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.670
+Version: 1.671
Synopsis: The Lustre V6 Verimag compiler
Description: This package contains:
(1) lus2lic: the (current) name of the compiler (and interpreter via -exec).
diff --git a/src/lv6version.ml b/src/lv6version.ml
index 3d806088..49988583 100644
--- a/src/lv6version.ml
+++ b/src/lv6version.ml
@@ -1,7 +1,7 @@
(** Automatically generated from Makefile *)
let tool = "lus2lic"
let branch = "master"
-let commit = "670"
-let sha_1 = "c84a83cb0164d9b63917cc5dc2d8bdb869e8fd74"
+let commit = "671"
+let sha_1 = "480ff8adfdc23a03f88ab2796a74a7ecb75975f1"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
diff --git a/src/socExec.ml b/src/socExec.ml
index 04f27735..d308b453 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/10/2016 (at 16:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 18/11/2016 (at 16:18) by Erwan Jahier> *)
open Soc
open Data
@@ -10,8 +10,10 @@ let profile_info = Lv6Verbose.profile_info
let (assign_expr : ctx -> var_expr -> var_expr -> ctx) =
fun ctx ve_in ve_out -> (* ve_out := ve_in (in ctx) *)
Lv6Verbose.exe ~flag:dbg
- (fun () -> print_string ("\nAssigning "^(SocUtils.string_of_filter ve_out) ^
- " to " ^(SocUtils.string_of_filter ve_in) ^ "\n"); flush stdout);
+ (fun () ->
+ print_string ("\nAssigning "^(SocUtils.string_of_filter ve_out) ^
+ " to " ^(SocUtils.string_of_filter ve_in) ^ "\n");
+ flush stdout);
{ ctx with s =
let v = SocExecValue.get_value ctx ve_in in
sadd_partial ctx.s ve_out ctx.cpath v
diff --git a/src/socExecDbg.ml b/src/socExecDbg.ml
index 6e3b79d3..3f46123d 100644
--- a/src/socExecDbg.ml
+++ b/src/socExecDbg.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 10/02/2016 (at 14:34) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/11/2016 (at 11:23) by Erwan Jahier> *)
open Soc
open Data
open SocExecValue
@@ -10,15 +10,273 @@ let rec (do_step : Soc.tbl -> Soc.t -> SocExecValue.ctx -> SocExecValue.ctx) =
let ctx = SocExec.soc_step step soc_tbl soc ctx in
ctx
-type ctx = Event.t
+(****************************************************************************)
+(* XXX duplication of SocExec !
+Maybe this code below, that is more general, is as (in)efficient ?
+
+*)
+let dbg = Lv6Verbose.get_flag "execDbg"
+let profile_info = Lv6Verbose.profile_info
+
+let (assign_expr : SocExecValue.ctx -> var_expr -> var_expr -> SocExecValue.ctx) =
+ fun ctx ve_in ve_out -> (* ve_out := ve_in (in ctx) *)
+ Lv6Verbose.exe
+ ~flag:dbg
+ (fun () ->
+ print_string ("\nAssigning "^(SocUtils.string_of_filter ve_out) ^
+ " to " ^(SocUtils.string_of_filter ve_in) ^ "... ");
+ flush stdout);
+ let res =
+ { ctx with s =
+ let v = SocExecValue.get_value ctx ve_in in
+ sadd_partial ctx.s ve_out ctx.cpath v
+ }
+ in
+ Lv6Verbose.exe ~flag:dbg (fun () -> print_string (" Done!"); flush stdout);
+ res
+
+(* [array_index i v] returns the var_expr v[i] *)
+let (array_index : int -> var -> var_expr) =
+ fun i (vn,vt) ->
+ let vt_elt =
+ match vt with
+ | Array(vt_elt,_) -> vt_elt
+ | _ -> assert false
+ in
+ Index(Var(vn,vt),i,vt_elt)
+
+let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> Event.t -> SocExecValue.ctx ->
+ (Event.t -> SocExecValue.ctx -> Event.t) -> Event.t) =
+ fun step soc_tbl soc ectx val_ctx cont ->
+ profile_info ("SocExecDbg.soc_step \n");
+ let soc_name,_,_ = soc.key in
+ let event =
+ match step.impl with
+ | Extern -> assert false (* fixme !!! *)
+ | Predef -> (
+ try
+ let val_ctx = SocExecEvalPredef.get soc.key val_ctx in
+ cont ectx val_ctx
+ with Not_found -> (* Not a predef op *) print_string (
+ "*** internal error in "^soc_name^". Is it defined in SocExecEvalPredef?\n");
+ flush stdout; assert false
+ )
+ | Gaol(vl,gaol) -> do_gaol step.lxm soc_tbl ectx gaol val_ctx cont
+
+ | Boolred(i,j,k) -> (
+ (* XXX mettre ce code dans socPredef ? (ou socMetaopPredef)*)
+ let inputs, outputs = soc.profile in
+ let b_array = (List.hd inputs) in
+ let cpt = ref 0 in
+ for i = 0 to k-1 do
+ let a_i = array_index i b_array in
+ let v = SocExecValue.get_value val_ctx a_i in
+ if v = B true then incr cpt;
+ done;
+ let res = B (!cpt >= i && !cpt <= j) in
+ let res_var = fst (List.hd outputs) in
+ let s = sadd val_ctx.s (res_var::val_ctx.cpath) res in
+ cont ectx { val_ctx with s = s }
+ )
+ | Condact(node_sk, dft_cst) -> (
+ let clk = SocExecValue.get_value val_ctx (Var ("i0",Bool)) in
+ let vel_in, vel_out = soc.profile in
+ let vel_in = List.map (fun x -> Var x) (List.tl vel_in) in
+ let vel_out = List.map (fun x -> Var x) vel_out in
+ let node_soc = SocUtils.find step.lxm node_sk soc_tbl in
+ let inst_name =
+ match soc.instances with
+ | [] -> let (proc_name,_,_) = node_soc.key in proc_name
+ | [inst] -> fst inst
+ | _ -> assert false
+ in
+ let path_saved = val_ctx.cpath in
+ let val_ctx = { val_ctx with cpath=inst_name::val_ctx.cpath } in
+ if clk = B true then (
+ let node_step = match node_soc.step with
+ [step] -> step
+ | _ -> assert false
+ in
+ let cont ectx val_ctx =
+ let val_ctx =
+ {
+ cpath=path_saved;
+ s = sadd val_ctx.s ("_memory"::val_ctx.cpath) (B false)
+ }
+ in
+ cont ectx val_ctx
+ in
+ do_soc_step inst_name node_step val_ctx soc_tbl node_soc
+ vel_in vel_out ectx cont
+ ) else (
+ let first_step = Var ("_memory",Bool) in
+ let val_ctx = { val_ctx with cpath=path_saved } in
+ let v = get_value val_ctx first_step in
+ let val_ctx =
+ if v = U || v = B true then
+ (* We are on the first step of node_soc;
+ - we assign the output var to the default values *)
+ (assert (List.length dft_cst = List.length vel_out);
+ List.fold_left2 assign_expr val_ctx dft_cst vel_out)
+ else
+ (* We are not on the first step of node_soc; hence we do nothing
+ and the output will keep their previous value. *)
+ val_ctx
+ in
+ let val_ctx = { val_ctx with
+ s = sadd val_ctx.s ("_memory"::val_ctx.cpath) (B false) }
+ in
+ cont ectx val_ctx
+ )
+ )
+ | Iterator(iter, node_sk, n) ->
+ let node_soc = SocUtils.find step.lxm node_sk soc_tbl in
+ let node_step = match node_soc.step with [step] -> step | _ -> assert false in
+ let iter_inputs,iter_outputs = soc.profile in
+ let (proc_name,_,_) = node_soc.key in
+ let inst_name =
+ match soc.instances with
+ | [] -> Array.make n proc_name
+ | _ -> Array.of_list (List.map fst soc.instances)
+ in
+ (* As we need to iterate on an (instance) array, we locally switch
+ to the evildark side *)
+ let rval_ctx = ref val_ctx in
+ let ref_event = ref ectx (* XXX dummy ?? *) in
+ for i = 0 to n-1 do
+ rval_ctx := { !rval_ctx with cpath = inst_name.(i)::val_ctx.cpath };
+ let vel_in, vel_out =
+ match iter with
+ | "map" -> (List.map (array_index i) iter_inputs,
+ List.map (array_index i) iter_outputs)
+ | "fold" | "red" | "fill" | "fillred" ->
+ let a_in = Var (List.hd iter_inputs) in
+ ( a_in::(List.map (array_index i) (List.tl iter_inputs)),
+ a_in::(List.map (array_index i) (List.tl iter_outputs)))
+ | _ -> assert false (* should not occur *)
+ in
+ let cont ectx val_ctx = (* necessary? correct? *)
+ rval_ctx := val_ctx;
+ ref_event := ectx;
+ cont ectx val_ctx
+ in
+ ref_event := do_soc_step inst_name.(i) node_step !rval_ctx soc_tbl
+ node_soc vel_in vel_out !ref_event cont;
+
+ rval_ctx := { !rval_ctx with cpath = List.tl !rval_ctx.cpath };
+ done;
+ if iter <> "map" then (
+ let a_in = Var (List.hd iter_inputs) in
+ let a_out = Var (List.hd iter_outputs) in
+ rval_ctx := assign_expr !rval_ctx a_in a_out); (* a_out=a_n *)
+ cont !ref_event !rval_ctx
+ in
+ event
+
+and (do_gaol : Lxm.t -> Soc.tbl -> Event.t -> gao list -> SocExecValue.ctx ->
+ (Event.t -> SocExecValue.ctx -> Event.t) -> Event.t) =
+ fun lxm soc_tbl ectx gaol val_ctx cont -> match gaol with
+ | [] -> assert false
+ | [gao] -> do_gao lxm soc_tbl ectx gao val_ctx cont
+ | gao::gaol ->
+ let cont ectx val_ctx = do_gaol lxm soc_tbl ectx gaol val_ctx cont in
+ do_gao lxm soc_tbl ectx gao val_ctx cont
+
+and (do_gao : Lxm.t -> Soc.tbl -> Event.t -> gao -> SocExecValue.ctx ->
+ (Event.t -> SocExecValue.ctx -> Event.t) -> Event.t) =
+ fun lxm soc_tbl ectx gao val_ctx cont ->
+ match gao with
+ | Case(id, id_gao_l) -> (
+ try
+ let id_val = get_enum id val_ctx in
+ let gaol = List.assoc id_val id_gao_l in
+ do_gaol lxm soc_tbl ectx gaol val_ctx cont
+ with Not_found -> cont ectx val_ctx
+ )
+ | Call(vel_out, Assign, vel_in) -> (
+ let val_ctx =
+ assert (List.length vel_in = List.length vel_out);
+ List.fold_left2 assign_expr val_ctx vel_in vel_out
+ in
+ let new_data = SocExecValue.filter_top_subst val_ctx.s in
+ let ectx = { ectx with Event.data = new_data } in (* useless ? *)
+ cont ectx val_ctx
+ )
+ | Call(vel_out, Procedure sk, vel_in) -> (
+ let (proc_name,_,_) = sk in
+ let path_saved = val_ctx.cpath in
+ let val_ctx = { val_ctx with cpath = proc_name::val_ctx.cpath } in
+ let soc = SocUtils.find lxm sk soc_tbl in
+ let step = match soc.step with [step] -> step | _ -> assert false in
+ let cont ectx val_ctx =
+ let val_ctx = { val_ctx with cpath = path_saved } in
+ cont ectx val_ctx
+ in
+ let cont ectx val_ctx =
+ do_soc_step proc_name step val_ctx soc_tbl soc vel_in vel_out ectx cont
+ in
+ cont ectx val_ctx
+ )
+ | Call(vel_out, Method((inst_name,sk),step_name), vel_in) -> (
+ let path_saved = val_ctx.cpath in
+ let val_ctx = { val_ctx with cpath = inst_name::val_ctx.cpath } in
+ let soc = SocUtils.find lxm sk soc_tbl in
+ let step = try List.find (fun sm -> sm.name = step_name) soc.step
+ with Not_found -> assert false
+ in
+ let cont ectx val_ctx =
+ let val_ctx = { val_ctx with cpath = path_saved } in
+ cont ectx val_ctx
+ in
+ let cont ectx val_ctx =
+ do_soc_step inst_name step val_ctx soc_tbl soc vel_in vel_out ectx cont
+ in
+ cont ectx val_ctx
+ )
+and (do_soc_step : Lv6Id.t -> step_method -> SocExecValue.ctx -> Soc.tbl -> Soc.t ->
+ var_expr list -> var_expr list -> Event.t ->
+ (Event.t -> SocExecValue.ctx -> Event.t) -> Event.t) =
+ fun name step val_ctx soc_tbl soc vel_in vel_out ectx cont ->
+ profile_info ("SocExecDbg.do_soc_step "^name^"\n");
+ let soc_in_vars, soc_out_vars = soc.profile in
+ let step_in_vars = filter_params soc soc_in_vars step.idx_ins in
+ let step_out_vars = filter_params soc soc_out_vars step.idx_outs in
+ let new_s = substitute_args_and_params vel_in step_in_vars val_ctx in
+ let cont ectx val_ctx =
+ let s_out = substitute_params_and_args step_out_vars vel_out val_ctx in
+ cont ectx { val_ctx with s = s_out }
+ in
+ soc_step step soc_tbl soc ectx { val_ctx with s=new_s } cont
+
+(* get the step params from its soc params *)
+and (filter_params : Soc.t -> Soc.var list -> int list -> Soc.var list) =
+ fun soc el il ->
+ let local_nth i l =
+ try List.nth l i
+ with _ ->
+ print_string (
+ "\n*** Cannot get the " ^ (string_of_int (i+1)) ^
+ "the element of a list of size " ^ (string_of_int (List.length l))^"\n");
+ flush stdout;
+ assert false
+ in
+ let res = List.map (fun i -> local_nth i el) il in
+ res
+
+(* End of XXX duplication of SocExec ! *)
+(****************************************************************************)
+
+type ectx = Event.t
+
+
(* exported *)
-let rec (do_step_dbg : Soc.tbl -> Soc.t -> ctx -> SocExecValue.ctx ->
- (ctx -> SocExecValue.ctx -> Event.t) -> Event.t) =
- fun soc_tbl soc ectx ctx cont ->
+let rec (do_step_dbg : Soc.tbl -> Soc.t -> ectx -> SocExecValue.ctx ->
+ (ectx -> SocExecValue.ctx -> Event.t) -> Event.t) =
+ fun soc_tbl soc ectx val_ctx cont ->
(* XXX un peu exegéré de mettre tout ?*)
-(* let (datal:Data.subst list) = SocExecValue.substs_to_data_subst ctx.s in *)
- let (datal:Data.subst list) = SocExecValue.filter_top_subst ctx.s in
+(* let (datal:Data.subst list) = SocExecValue.substs_to_data_subst val_ctx.s in *)
+ let (datal:Data.subst list) = SocExecValue.filter_top_subst val_ctx.s in
let (soc_name,_,_) = soc.key in
let ectx = {
ectx with
@@ -29,7 +287,8 @@ let rec (do_step_dbg : Soc.tbl -> Soc.t -> ctx -> SocExecValue.ctx ->
Event.outputs = snd soc.profile;
}
in
- let cont2 ectx ctx =
+ let cont2 ectx val_ctx =
+ let (datal:Data.subst list) = SocExecValue.filter_top_subst val_ctx.s in
{
Event.step = ectx.Event.step;
Event.nb = ectx.Event.nb;
@@ -40,8 +299,8 @@ let rec (do_step_dbg : Soc.tbl -> Soc.t -> ctx -> SocExecValue.ctx ->
Event.inputs = ectx.Event.inputs;
Event.outputs = ectx.Event.outputs;
Event.sinfo = None;
- Event.data = ectx.Event.data;
- Event.next = (fun () -> cont (Event.incr_event_nb ectx) ctx);
+ Event.data = datal;
+ Event.next = (fun () -> cont (Event.incr_event_nb ectx) val_ctx);
Event.terminate = ectx.Event.terminate;
}
in
@@ -59,9 +318,7 @@ let rec (do_step_dbg : Soc.tbl -> Soc.t -> ctx -> SocExecValue.ctx ->
Event.next = (fun () ->
let step = match soc.step with [step] -> step | _ -> assert false in
let ectx = Event.incr_event_nb ectx in
- let ctx = SocExec.soc_step step soc_tbl soc ctx in
- cont2 ectx ctx
+ soc_step step soc_tbl soc ectx val_ctx cont2
);
Event.terminate = ectx.Event.terminate;
}
-
diff --git a/src/socExecValue.ml b/src/socExecValue.ml
index d0409593..4839eb72 100644
--- a/src/socExecValue.ml
+++ b/src/socExecValue.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 14/01/2016 (at 10:43) by Erwan Jahier> *)
+(* Time-stamp: <modified the 18/11/2016 (at 15:43) by Erwan Jahier> *)
let dbg = (Lv6Verbose.get_flag "exec")
@@ -323,7 +323,9 @@ let rec (get_value : ctx -> var_expr -> Data.v) =
let (substitute_args_and_params : var_expr list -> var list -> ctx -> substs) =
fun args params ctx ->
assert (List.length args = List.length params);
- let arg_ctx = { ctx with cpath = List.tl ctx.cpath } in
+ let arg_ctx =
+ try { ctx with cpath = List.tl ctx.cpath } with _ -> assert false
+ in
let s =
assert (List.length args = List.length params);
List.fold_left2
@@ -339,7 +341,7 @@ let (substitute_params_and_args : var list -> var_expr list -> ctx -> substs) =
assert (List.length args = List.length params);
List.fold_left2
(fun acc arg (pn,_) ->
- let path = List.tl ctx.cpath in
+ let path = try List.tl ctx.cpath with _ -> assert false in
let v = get_val pn ctx in
sadd_partial acc arg path v
)
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index e748f86d..f1b5d559 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test Run By jahier on Tue Oct 25 17:15:37
+Test Run By jahier on Mon Nov 21 11:19:33
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic0 tests ===
@@ -64,7 +64,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
==> lus2lic1.sum <==
-Test Run By jahier on Tue Oct 25 17:15:38
+Test Run By jahier on Mon Nov 21 11:19:33
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic1 tests ===
@@ -397,7 +397,7 @@ PASS: sh multipar.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
==> lus2lic2.sum <==
-Test Run By jahier on Tue Oct 25 17:15:58
+Test Run By jahier on Mon Nov 21 11:19:52
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic2 tests ===
@@ -743,7 +743,7 @@ PASS: sh zzz2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
-Test Run By jahier on Tue Oct 25 17:16:40
+Test Run By jahier on Mon Nov 21 11:20:31
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic3 tests ===
@@ -1249,7 +1249,7 @@ PASS: ./myec2c {-o multipar.c multipar.ec}
PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
-Test Run By jahier on Tue Oct 25 17:16:51
+Test Run By jahier on Mon Nov 21 11:20:43
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic4 tests ===
@@ -1773,14 +1773,14 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
# of unexpected failures 4
===============================
# Total number of failures: 26
-lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 20 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 42 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 11 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 33 seconds
+lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 18 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 39 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 12 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 32 seconds
* Ref time:
-0.06user 0.02system 1:46.62elapsed 0%CPU (0avgtext+0avgdata 5676maxresident)k
-96inputs+0outputs (0major+6036minor)pagefaults 0swaps
+0.06user 0.03system 1:42.49elapsed 0%CPU (0avgtext+0avgdata 5668maxresident)k
+96inputs+0outputs (0major+6150minor)pagefaults 0swaps
* Quick time (-j 4):
-0.06user 0.02system 0:58.31elapsed 0%CPU (0avgtext+0avgdata 5700maxresident)k
-96inputs+0outputs (0major+6022minor)pagefaults 0swaps
+0.06user 0.02system 0:50.01elapsed 0%CPU (0avgtext+0avgdata 5724maxresident)k
+96inputs+0outputs (0major+6186minor)pagefaults 0swaps
--
GitLab