diff --git a/lib/action.ml b/lib/action.ml
index cdb2460b4553e3883a52c490d12050206253b8bb..aff73f56a9a046036db37edd98e443f5f85380eb 100644
--- a/lib/action.ml
+++ b/lib/action.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 14/06/2024 (at 14:10) by Erwan Jahier> *)
+(** Time-stamp: <modified the 19/06/2024 (at 17:49) by Erwan Jahier> *)
(* exported *)
type rhs = Soc.var_expr list
@@ -33,7 +33,7 @@ let to_string: (t -> string) =
let string_of_operation = function
| Soc.Assign -> ""
| Soc.Method((n, _sk),_sname,_) -> n
- | Soc.Procedure((name,_,_),_) -> name
+ | Soc.Procedure((name,_,_),_,_) -> name
in
let string_of_params p = String.concat ", " (List.map SocUtils.string_of_filter p) in
diff --git a/lib/actionsDeps.mli b/lib/actionsDeps.mli
index 2ef0d92042ab2d284803539af348dd48c1d70843..bf7e2db1cb05e1b476f9cf664170ccf9b3a96690 100644
--- a/lib/actionsDeps.mli
+++ b/lib/actionsDeps.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 20/03/2022 (at 22:19) by Erwan Jahier> *)
+(** Time-stamp: <modified the 19/06/2024 (at 14:54) by Erwan Jahier> *)
(** Compute dependencies between actions *)
@@ -13,7 +13,7 @@ val concat: t -> t -> t
(** Compute the action dependencies that comes from the equations
I/O.
- Ajoute à une liste de dépendances existante celles issues d'une
+ Ajoute à une liste de dépendances existantes celles issues d'une
liste d'actions (dont les entrées dépendent des sorties).
Lic2soc.lic_to_soc_type is passed in argument to break a dep loop
@@ -36,4 +36,3 @@ val remove_dep : t -> Action.t -> t
val depends_on : t -> Action.t -> Action.t -> bool
val to_string: t -> string
-
diff --git a/lib/lic2soc.ml b/lib/lic2soc.ml
index b577f593d927e7e669038d6df1d10e1431e6aed4..f5368cb39d28a822099dd22ba201242772005247 100644
--- a/lib/lic2soc.ml
+++ b/lib/lic2soc.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 17/06/2024 (at 14:28) by Erwan Jahier> *)
+(** Time-stamp: <modified the 20/06/2024 (at 09:01) by Erwan Jahier> *)
(* XXX ce module est mal écrit. A reprendre. (R1) *)
@@ -256,6 +256,29 @@ let build_step: Lxm.t -> string -> Lic.node_exp -> Soc.var list -> Soc.gao list
Soc.impl = Soc.Gaol (locals, gaol)
}
+(* In multi-task mode, we need 2 steps *)
+let build_step_mt: Lxm.t -> string -> Lic.node_exp -> Soc.var list -> Soc.gao list ->
+ Soc.step_method * Soc.step_method =
+ fun lxm name node locals gaol ->
+ let convert_node_interface = fun l ->
+ fst (List.fold_left (fun (a, i) _ -> a @ [i], i+1) ([], 0) l)
+ in
+ {
+ Soc.name = name^"0"; (* cf naming convention in
+ Soc2cIdent.is_step_method_preambule *)
+ Soc.lxm = lxm;
+ Soc.idx_ins = convert_node_interface node.Lic.inlist_eff;
+ Soc.idx_outs = [];
+ Soc.impl = Soc.Gaol ([], [])
+ },
+ {
+ Soc.name = name;
+ Soc.lxm = lxm;
+ Soc.idx_ins = [];
+ Soc.idx_outs = convert_node_interface node.Lic.outlist_eff;
+ Soc.impl = Soc.Gaol (locals, gaol)
+ }
+
let build_extern_step: Lxm.t -> string -> Lic.node_exp -> Soc.step_method =
fun lxm name node ->
(* Converti les entrées/sorties d'un noeud en index
@@ -467,7 +490,7 @@ let soc_step_to_operation:
Soc.ident -> Soc.t -> Soc.instance option -> Soc.task option -> Soc.atomic_operation =
fun name comp i_opt t_opt ->
match i_opt with
- | None -> Soc.Procedure (comp.Soc.key, t_opt)
+ | None -> Soc.Procedure (comp.Soc.key, name, t_opt)
| Some (i) -> Soc.Method(i,name, t_opt)
let (action_of_step : Lxm.t -> Soc.t -> Lic.clock -> Soc.var_expr list ->
@@ -781,6 +804,7 @@ let (actions_of_equation: Lxm.t -> Soc.tbl -> ctx -> Lic.eq_info ->
let is_task = is_a_task lxm in
let ctx, actions, _, instances, tasks, deps =
actions_of_expression lxm soc_tbl ctx clk left_loc is_task right_part
+ (* XXX c'est ici qu'on coupe l'action en 2 *)
in
(* let tasks = if not is_task then tasks else xxx:: tasks in *)
ctx, actions, instances, tasks, deps
@@ -792,155 +816,210 @@ let profile_info = Lv6Verbose.profile_info
let f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
fun prog mnk ->
- let rec (process_node : Lic.node_key -> Soc.tbl -> Soc.key * Soc.tbl) =
- fun nk soc_tbl ->
- profile_info ("Lic2soc.process_node "^(Lic.string_of_node_key nk)^"\n");
- let node =
- match LicPrg.find_node prog nk with
- | None ->
- prerr_string (
- "*** "^ (LicDump.string_of_node_key_rec false false nk) ^
- " not defined (as lic).\n" ^
- "*** Defined nodes are:"^
- (String.concat
- ",\n"
- (List.map (fun (nk,_) ->
- "\""^LicDump.string_of_node_key_rec false false nk ^"\"")
- (LicPrg.list_nodes prog)))
- );
- assert false
- | Some node_exp -> node_exp
- in
- let sk = soc_key_of_node_exp node in
- let soc_tbl =
- if SocMap.mem sk soc_tbl then soc_tbl else
- try
- (match LicPrg.find_node prog nk with
- | None -> assert false
- | Some node_def ->
- (match soc_of_node prog node_def soc_tbl with
- | Some(_,soc,soc_tbl) -> SocUtils.add sk soc soc_tbl
- | None ->
- print_string ("Undefined soc : " ^ (string_of_node_key nk) ^ "\n");
- flush stdout;
- soc_tbl
- )
- )
- with
- | Undef_soc (_sk,_lxm,Lic.CALL { it = nk2 ;_}, _types,_) ->
- (* Il manque une dépendance, on essaie de la
- traduire puis de retraduire le noeud courant.
- ZZZ ca part facilement en vrille ici si une erreur
- a été faite en amont...
- *)
- let soc_tbl = snd (process_node nk2 soc_tbl) in
- snd (process_node nk soc_tbl)
-
- | Undef_soc (sk,lxm,pos_op, types, fby_init_opt) -> (
- let soc =
- SocPredef.soc_interface_of_pos_op lxm pos_op types fby_init_opt
- in
- if (sk<>soc.key) then (
- print_string ("Soc key mismatch :\n\t" ^
- (SocUtils.string_of_soc_key sk) ^ "\n<>\n\t" ^
- (SocUtils.string_of_soc_key soc.key) ^ "\n");
+ let rec (process_node : Lic.node_key -> Soc.tbl -> Soc.key * Soc.tbl) =
+ fun nk soc_tbl ->
+ profile_info ("Lic2soc.process_node "^(Lic.string_of_node_key nk)^"\n");
+ let node =
+ match LicPrg.find_node prog nk with
+ | None ->
+ prerr_string (
+ "*** "^ (LicDump.string_of_node_key_rec false false nk) ^
+ " not defined (as lic).\n" ^
+ "*** Defined nodes are:"^
+ (String.concat
+ ",\n"
+ (List.map (fun (nk,_) ->
+ "\""^LicDump.string_of_node_key_rec false false nk ^"\"")
+ (LicPrg.list_nodes prog)))
+ );
+ assert false
+ | Some node_exp -> node_exp
+ in
+ let sk = soc_key_of_node_exp node in
+ let soc_tbl =
+ if SocMap.mem sk soc_tbl then soc_tbl else
+ try
+ (match LicPrg.find_node prog nk with
+ | None -> assert false
+ | Some node_def ->
+ (match soc_of_node prog node_def soc_tbl with
+ | Some(_,soc,soc_tbl) -> SocUtils.add sk soc soc_tbl
+ | None ->
+ print_string ("Undefined soc : " ^ (string_of_node_key nk) ^ "\n");
flush stdout;
- assert false
- );
- let soc_tbl = SocUtils.add soc.key soc soc_tbl in
- snd (process_node nk soc_tbl)
- )
- | Polymorphic ->
- let msg = (Lxm.details node.lxm) ^
- ": cannot infer the type of this polymorphic node."^
- " Please be more specific.\n"
- in
- raise (Lv6errors.Global_error msg)
+ soc_tbl
+ )
+ )
+ with
+ | Undef_soc (_sk,_lxm,Lic.CALL { it = nk2 ;_}, _types,_) ->
+ (* Il manque une dépendance, on essaie de la
+ traduire puis de retraduire le noeud courant.
+ ZZZ ca part facilement en vrille ici si une erreur
+ a été faite en amont...
+ *)
+ let soc_tbl = snd (process_node nk2 soc_tbl) in
+ snd (process_node nk soc_tbl)
- in
- sk, soc_tbl
+ | Undef_soc (sk,lxm,pos_op, types, fby_init_opt) -> (
+ let soc =
+ SocPredef.soc_interface_of_pos_op lxm pos_op types fby_init_opt
+ in
+ if (sk<>soc.key) then (
+ print_string ("Soc key mismatch :\n\t" ^
+ (SocUtils.string_of_soc_key sk) ^ "\n<>\n\t" ^
+ (SocUtils.string_of_soc_key soc.key) ^ "\n");
+ flush stdout;
+ assert false
+ );
+ let soc_tbl = SocUtils.add soc.key soc soc_tbl in
+ snd (process_node nk soc_tbl)
+ )
+ | Polymorphic ->
+ let msg = (Lxm.details node.lxm) ^
+ ": cannot infer the type of this polymorphic node."^
+ " Please be more specific.\n"
+ in
+ raise (Lv6errors.Global_error msg)
- and make_condact_soc node condact_node soc_key soc_tbl ctx lxm vel =
- let nsk, soc_tbl = process_node condact_node soc_tbl in
- let nsoc = SocUtils.find lxm nsk soc_tbl in
- let nsoc_step = match nsoc.step with [s] -> s
- | _ -> assert false (* hmm. Iterating on a pre will not work. XXX fixme ! *)
- in
- let _ctx,inst =
- match make_instance lxm Lic.BaseLic ctx nsoc with
- | ctx,Some inst -> ctx,[inst]
- | ctx,None -> ctx,[]
- in
- let soc_key =
- let x,y,_=soc_key in
- x,y, Soc.MemInit(Soc.Const("_true", Data.Bool)) (* the first step flag *)
in
- let soc = {
- Soc.key = soc_key ;
- Soc.profile = soc_profile_of_node node;
- Soc.clock_profile = [];
- Soc.instances = inst ;
- Soc.tasks = [] ;
- Soc.step = [
- {
- name = "step";
- lxm = lxm;
- idx_ins = nsoc_step.idx_ins@[List.length nsoc_step.idx_ins];
- idx_outs = nsoc_step.idx_outs;
- impl = Condact(nsk, List.flatten (List.map lic2soc_const vel));
- }
- ];
- Soc.memory = Soc.Mem Data.Bool; (* to hold the first step flag *)
- Soc.precedences = [];
- Soc.assertions = [ (* something to do? *)];
- }
- in
- soc_tbl, soc
-
- (* Produit des soc de noeuds. *)
- and (soc_of_node: LicPrg.t -> Lic.node_exp -> Soc.tbl ->
- (ctx * Soc.t * Soc.tbl) option) =
- fun licprg node soc_tbl ->
- profile_info ("Lic2soc.soc_of_node "^
- (Lic.string_of_node_key node.node_key_eff)^"\n");
- let io_list = node.Lic.inlist_eff @ node.Lic.outlist_eff in
- let io_type = List.map (fun vi -> lic_to_data_type vi.var_type_eff) io_list in
- let soc_key = make_soc_key_of_node_key node.Lic.node_key_eff None io_type in
- let lxm = node.Lic.lxm in
- let ctx = create_context licprg in
- let (soc_of_body: Lic.node_body -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
- fun b soc_tbl ->
- profile_info " Lic2soc.soc_of_node: computing actions...\n";
- let ctx, actions, instances, tasks, deps =
- (* on itere sur la liste des équations *)
- List.fold_left
- (fun (c, a, i, t, d) eq ->
- let nc, na, ni, nt, nd = actions_of_equation eq.src soc_tbl c eq.it in
- nc, List.rev_append na a,
- List.rev_append ni i,
- List.rev_append nt t,
- (ActionsDeps.concat nd d)
+ sk, soc_tbl
+
+ and make_condact_soc node condact_node soc_key soc_tbl ctx lxm vel =
+ let nsk, soc_tbl = process_node condact_node soc_tbl in
+ let nsoc = SocUtils.find lxm nsk soc_tbl in
+ let nsoc_step = match nsoc.step with [s] -> s
+ | _ -> assert false (* hmm. Iterating on a pre will not work. XXX fixme ! *)
+ in
+ let _ctx,inst =
+ match make_instance lxm Lic.BaseLic ctx nsoc with
+ | ctx,Some inst -> ctx,[inst]
+ | ctx,None -> ctx,[]
+ in
+ let soc_key =
+ let x,y,_=soc_key in
+ x,y, Soc.MemInit(Soc.Const("_true", Data.Bool)) (* the first step flag *)
+ in
+ let soc = {
+ Soc.key = soc_key ;
+ Soc.profile = soc_profile_of_node node;
+ Soc.clock_profile = [];
+ Soc.instances = inst ;
+ Soc.tasks = [] ;
+ Soc.step = [
+ {
+ name = "step";
+ lxm = lxm;
+ idx_ins = nsoc_step.idx_ins@[List.length nsoc_step.idx_ins];
+ idx_outs = nsoc_step.idx_outs;
+ impl = Condact(nsk, List.flatten (List.map lic2soc_const vel));
+ }
+ ];
+ Soc.memory = Soc.Mem Data.Bool; (* to hold the first step flag *)
+ Soc.precedences = [];
+ Soc.assertions = [ (* something to do? *)];
+ }
+ in
+ soc_tbl, soc
+
+ (* Produit des soc de noeuds. *)
+ and (soc_of_node: LicPrg.t -> Lic.node_exp -> Soc.tbl ->
+ (ctx * Soc.t * Soc.tbl) option) =
+ fun licprg node soc_tbl ->
+ profile_info ("Lic2soc.soc_of_node "^
+ (Lic.string_of_node_key node.node_key_eff)^"\n");
+ let io_list = node.Lic.inlist_eff @ node.Lic.outlist_eff in
+ let io_type = List.map (fun vi -> lic_to_data_type vi.var_type_eff) io_list in
+ let soc_key = make_soc_key_of_node_key node.Lic.node_key_eff None io_type in
+ let lxm = node.Lic.lxm in
+ let ctx = create_context licprg in
+ let (soc_of_body: Lic.node_body -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
+ fun b soc_tbl ->
+ profile_info " Lic2soc.soc_of_node: computing actions...\n";
+ let ctx, actions, instances, tasks, deps =
+ (* on itere sur la liste des équations *)
+ List.fold_left
+ (fun (c, a, i, t, d) eq ->
+ let nc, na, ni, nt, nd = actions_of_equation eq.src soc_tbl c eq.it in
+ nc, List.rev_append na a,
+ List.rev_append ni i,
+ List.rev_append nt t,
+ (ActionsDeps.concat nd d)
+ )
+ (ctx, [], [], [], ActionsDeps.empty)
+ b.eqs_eff
+ in
+ let actions =
+ (* We sort the actions so that TASK_START are scheduled as soon as
+ Possible, and TASK_JOIN are scheduled as late as possible *)
+ let l1, l2 =
+ List.partition
+ (fun (_,_,_,gao, _) ->
+ match gao with
+ | Assign
+ | Method ((_,(_,_,_)),_, None)
+ | Procedure(_, _, None)
+ -> false
+ | Method ((_,(_,_,_)), sname, Some _)
+ | Procedure(_, sname, Some _)
+ ->
+ Soc2cIdent.is_step_method_preambule sname
)
- (ctx, [], [], [], ActionsDeps.empty)
- b.eqs_eff
- in
- (* Construction des dépendances entre les expressions *)
- profile_info " Lic2soc.soc_of_node: computing dependencies...\n";
- let all_deps =
- ActionsDeps.build_data_deps_from_actions lic_to_data_type deps actions
- in
- Lv6Verbose.exe ~flag:dbg
- (fun () -> print_string (ActionsDeps.to_string all_deps); flush stdout);
- profile_info " SortActions.f: sorting actions...\n";
- let gaol = SortActions.f actions all_deps lxm in
+ actions
+ in (* put all the <node>_step0 methods run in a task into l1 *)
+ let l2, l3 =
+ List.partition
+ (fun (_,_,_,gao, _) ->
+ match gao with
+ | Assign
+ | Method ((_,(_,_,_)),_, None)
+ | Procedure(_, _, None)
+ -> true
+ | Method ((_,(_,_,_)),_, Some _)
+ | Procedure(_, _, Some _)
+ -> false
+ )
+ l2
+ in (* put all the <node>_step methods run in a task into l3 *)
+ l1 @ l2 @l3
+ in
+ (* Construction des dépendances entre les expressions *)
+ profile_info " Lic2soc.soc_of_node: computing dependencies...\n";
+ let all_deps =
+ ActionsDeps.build_data_deps_from_actions lic_to_data_type deps actions
+ in
+ Lv6Verbose.exe ~flag:dbg
+ (fun () -> print_string (ActionsDeps.to_string all_deps); flush stdout);
+ profile_info " SortActions.f: sorting actions...\n";
+ let gaol = SortActions.f actions all_deps lxm in
- profile_info " Lic2soc.soc_of_node: actions sorted. \n";
- let (locals: Soc.var list) =
- match node.Lic.loclist_eff with
- | None -> []
- | Some l -> List.map (lic_to_soc_var) l
+ profile_info " Lic2soc.soc_of_node: actions sorted. \n";
+ let (locals: Soc.var list) =
+ match node.Lic.loclist_eff with
+ | None -> []
+ | Some l -> List.map (lic_to_soc_var) l
+ in
+ if Lv6MainArgs.global_opt.Lv6MainArgs.multi_task then
+ let step1, step2 = build_step_mt lxm "step" node (locals @ ctx.locals) gaol in
+ let soc = {
+ Soc.key = soc_key;
+ Soc.profile = soc_profile_of_node node;
+ Soc.clock_profile = [];
+ Soc.instances = instances ;
+ Soc.tasks = tasks;
+ Soc.step = [step1;step2 ] ;
+ Soc.memory = Soc.No_mem;
+ Soc.precedences = [ "step", ["step0"]] ;
+ Soc.assertions =
+ if Lv6MainArgs.global_opt.Lv6MainArgs.gen_autotest then
+ [] (* In this mode no code is generated and the var creation
+ is inhibited in L2Lsplit *)
+ else
+ List.map (lic_val_exp_to_soc_var licprg) b.asserts_eff;
+ }
in
+ Some(ctx, soc, soc_tbl)
+ else
let step = build_step lxm "step" node (locals @ ctx.locals) gaol in
let soc = {
Soc.key = soc_key;
@@ -948,9 +1027,9 @@ let f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
Soc.clock_profile = [];
Soc.instances = instances ;
Soc.tasks = tasks;
- Soc.step = [step];
+ Soc.step = [step (* XXX c'est ici qu'on doire generer 2 step en mode multi-task *)] ;
Soc.memory = Soc.No_mem;
- Soc.precedences = [];
+ Soc.precedences = [ (*["step1", ["step2"]] *)];
Soc.assertions =
if Lv6MainArgs.global_opt.Lv6MainArgs.gen_autotest then
[] (* In this mode no code is generated and the var creation
@@ -960,127 +1039,127 @@ let f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
}
in
Some(ctx, soc, soc_tbl)
- in
- let (soc_of_metaop: Lic.node_key -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
- fun nk soc_tbl ->
- profile_info "Lic2soc.soc_of_metaop...\n";
- match snd (fst nk), List.sort compare (snd nk) with
- | ("map"|"red"|"fill"|"fillred"|"fold"),[
- ConstStaticArgLic(_,Int_const_eff(c)); NodeStaticArgLic(_,iter_node)]
- | ("map"|"red"|"fill"|"fillred"|"fold"),[
- ConstStaticArgLic(_,Int_const_eff(c)); TypeStaticArgLic(_);
- NodeStaticArgLic(_,iter_node)] -> ( (*red, fill, fillred, map *)
- let nsk, soc_tbl = process_node iter_node soc_tbl in
- let nsoc = SocUtils.find lxm nsk soc_tbl in
- let nsoc_step = match nsoc.step with
- [s] -> s
- | _ -> assert false (* Iterating on a pre will not work. XXX fixme ! *)
- in
- let rec make_n_instance ctx acc n =
- if n=0 then ctx, List.rev acc else
- match make_instance lxm Lic.BaseLic ctx nsoc with
- | ctx,Some inst -> make_n_instance ctx (inst::acc) (n-1)
- | ctx,None -> ctx,[]
- in
- let c = int_of_string c in
- let ctx, instances = make_n_instance ctx [] c in
+ in
+ let (soc_of_metaop: Lic.node_key -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
+ fun nk soc_tbl ->
+ profile_info "Lic2soc.soc_of_metaop...\n";
+ match snd (fst nk), List.sort compare (snd nk) with
+ | ("map"|"red"|"fill"|"fillred"|"fold"),[
+ ConstStaticArgLic(_,Int_const_eff(c)); NodeStaticArgLic(_,iter_node)]
+ | ("map"|"red"|"fill"|"fillred"|"fold"),[
+ ConstStaticArgLic(_,Int_const_eff(c)); TypeStaticArgLic(_);
+ NodeStaticArgLic(_,iter_node)] -> ( (*red, fill, fillred, map *)
+ let nsk, soc_tbl = process_node iter_node soc_tbl in
+ let nsoc = SocUtils.find lxm nsk soc_tbl in
+ let nsoc_step = match nsoc.step with
+ [s] -> s
+ | _ -> assert false (* Iterating on a pre will not work. XXX fixme ! *)
+ in
+ let rec make_n_instance ctx acc n =
+ if n=0 then ctx, List.rev acc else
+ match make_instance lxm Lic.BaseLic ctx nsoc with
+ | ctx,Some inst -> make_n_instance ctx (inst::acc) (n-1)
+ | ctx,None -> ctx,[]
+ in
+ let c = int_of_string c in
+ let ctx, instances = make_n_instance ctx [] c in
+ let soc = {
+ Soc.key = soc_key;
+ Soc.profile = soc_profile_of_node node;
+ Soc.clock_profile = [];
+ Soc.instances = instances ;
+ Soc.tasks = [] ;
+ Soc.step = [
+ {
+ name = "step";
+ lxm = lxm;
+ idx_ins = nsoc_step.idx_ins;
+ idx_outs = nsoc_step.idx_outs;
+ impl = Iterator(snd (fst nk), nsk, c);
+ }
+ ];
+ Soc.memory = Soc.No_mem;
+ Soc.precedences = [];
+ Soc.assertions = [];
+ }
+
+ in
+ Some(ctx, soc, soc_tbl)
+ )
+ | ("condact"), [
+ ConstStaticArgLic("dflt",Tuple_const_eff vel);
+ NodeStaticArgLic("oper",condact_node)
+ ] -> (
+ let soc_tbl,soc =
+ make_condact_soc node condact_node soc_key soc_tbl ctx lxm vel
+ in
+ Some(ctx, soc, soc_tbl)
+ )
+ | ("condact"), [
+ ConstStaticArgLic("dflt",const); NodeStaticArgLic ("oper",condact_node)
+ ] -> (
+ let soc_tbl,soc =
+ make_condact_soc node condact_node soc_key soc_tbl ctx lxm [const] in
+ Some(ctx, soc, soc_tbl)
+ )
+ | _e ->
+ match (nk) with
+ | ("Lustre","boolred"), [ConstStaticArgLic(_,Int_const_eff(i));
+ ConstStaticArgLic(_,Int_const_eff(j));
+ ConstStaticArgLic(_,Int_const_eff(k)) ] -> (
+ let i,j,k = int_of_string i, int_of_string j, int_of_string k in
let soc = {
Soc.key = soc_key;
Soc.profile = soc_profile_of_node node;
Soc.clock_profile = [];
- Soc.instances = instances ;
+ Soc.instances = [] ;
Soc.tasks = [] ;
Soc.step = [
{
name = "step";
lxm = lxm;
- idx_ins = nsoc_step.idx_ins;
- idx_outs = nsoc_step.idx_outs;
- impl = Iterator(snd (fst nk), nsk, c);
+ idx_ins = [0];
+ idx_outs = [0];
+ impl = Boolred(i,j,k);
}
];
- Soc.memory = Soc.No_mem;
+ Soc.memory = Soc.No_mem;
Soc.precedences = [];
Soc.assertions = [];
}
-
in
Some(ctx, soc, soc_tbl)
)
- | ("condact"), [
- ConstStaticArgLic("dflt",Tuple_const_eff vel);
- NodeStaticArgLic("oper",condact_node)
- ] -> (
- let soc_tbl,soc =
- make_condact_soc node condact_node soc_key soc_tbl ctx lxm vel
- in
- Some(ctx, soc, soc_tbl)
- )
- | ("condact"), [
- ConstStaticArgLic("dflt",const); NodeStaticArgLic ("oper",condact_node)
- ] -> (
- let soc_tbl,soc =
- make_condact_soc node condact_node soc_key soc_tbl ctx lxm [const] in
- Some(ctx, soc, soc_tbl)
- )
- | _e ->
- match (nk) with
- | ("Lustre","boolred"), [ConstStaticArgLic(_,Int_const_eff(i));
- ConstStaticArgLic(_,Int_const_eff(j));
- ConstStaticArgLic(_,Int_const_eff(k)) ] -> (
- let i,j,k = int_of_string i, int_of_string j, int_of_string k in
- let soc = {
- Soc.key = soc_key;
- Soc.profile = soc_profile_of_node node;
- Soc.clock_profile = [];
- Soc.instances = [] ;
- Soc.tasks = [] ;
- Soc.step = [
- {
- name = "step";
- lxm = lxm;
- idx_ins = [0];
- idx_outs = [0];
- impl = Boolred(i,j,k);
- }
- ];
- Soc.memory = Soc.No_mem;
- Soc.precedences = [];
- Soc.assertions = [];
- }
- in
- Some(ctx, soc, soc_tbl)
- )
- | _ -> assert false
- in
- let (soc_of_extern: Lic.node_exp -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
- fun node soc_tbl ->
- try
- let soc = SocPredef.of_soc_key lxm soc_key in
- Some(ctx, soc, soc_tbl)
- with _ ->
- (* This extern node is not a predef *)
- let step = build_extern_step lxm "step" node in
- let soc = {
- Soc.key = soc_key;
- Soc.profile = soc_profile_of_node node;
- Soc.clock_profile = [];
- Soc.instances = [] ;
- Soc.tasks = [] ;
- Soc.step = [step];
- Soc.memory =
- if node.Lic.has_mem_eff then Soc.Mem_hidden else Soc.No_mem;
- Soc.precedences = [];
- Soc.assertions = [];
- }
- in
- Some(ctx, soc, soc_tbl)
- in
- match node.Lic.def_eff with
- | AbstractLic None -> assert false (* None if extern in the provide part *)
- | AbstractLic (Some node_exp) -> soc_of_node licprg node_exp soc_tbl
- | MetaOpLic -> soc_of_metaop node.Lic.node_key_eff soc_tbl
- | BodyLic b -> soc_of_body b soc_tbl
- | ExternLic -> soc_of_extern node soc_tbl
- in
- process_node mnk SocMap.empty
+ | _ -> assert false
+ in
+ let (soc_of_extern: Lic.node_exp -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
+ fun node soc_tbl ->
+ try
+ let soc = SocPredef.of_soc_key lxm soc_key in
+ Some(ctx, soc, soc_tbl)
+ with _ ->
+ (* This extern node is not a predef *)
+ let step = build_extern_step lxm "step" node in
+ let soc = {
+ Soc.key = soc_key;
+ Soc.profile = soc_profile_of_node node;
+ Soc.clock_profile = [];
+ Soc.instances = [] ;
+ Soc.tasks = [] ;
+ Soc.step = [step];
+ Soc.memory =
+ if node.Lic.has_mem_eff then Soc.Mem_hidden else Soc.No_mem;
+ Soc.precedences = [];
+ Soc.assertions = [];
+ }
+ in
+ Some(ctx, soc, soc_tbl)
+ in
+ match node.Lic.def_eff with
+ | AbstractLic None -> assert false (* None if extern in the provide part *)
+ | AbstractLic (Some node_exp) -> soc_of_node licprg node_exp soc_tbl
+ | MetaOpLic -> soc_of_metaop node.Lic.node_key_eff soc_tbl
+ | BodyLic b -> soc_of_body b soc_tbl
+ | ExternLic -> soc_of_extern node soc_tbl
+ in
+ process_node mnk SocMap.empty
diff --git a/lib/soc.ml b/lib/soc.ml
index bbe3fadde42b55bd17f78b9b4c09f89be6dd9ff8..e5e3c0d7e0100c432be9da0099e3f455d55f6cb6 100644
--- a/lib/soc.ml
+++ b/lib/soc.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/06/2024 (at 11:20) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2024 (at 17:46) by Erwan Jahier> *)
(** Synchronous Object Components
@@ -49,7 +49,7 @@ let (data_type_of_var_expr : var_expr -> Data.t) =
type atomic_operation =
| Assign (* Wire *)
| Method of instance * ident * task option (* node step call ; the ident is the step name *)
- | Procedure of key * task option (* memoryless method made explicit (a good idea?) *)
+ | Procedure of key * ident * task option (* memoryless method made explicit (a good idea?) *)
(* Guarded Atomic Operation *)
diff --git a/lib/soc2c.ml b/lib/soc2c.ml
index f51a58dbc0a2b4bb67d63212f6716ec21a44912c..6f97c2e254b349ec077e93e3123967337802e8f4 100644
--- a/lib/soc2c.ml
+++ b/lib/soc2c.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 18/06/2024 (at 16:19) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/06/2024 (at 09:26) by Erwan Jahier> *)
(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
@@ -117,7 +117,7 @@ let (gao2c : Soc.tbl -> 'a soc_pp -> Soc.gao -> unit) =
List.iter (fun ve -> assert(var_expr_is_not_a_slice ve)) vel_out;
Soc2cDep.gen_step_call sp.soc called_soc (task_opt <> None) vel_out vel_in ctx sname step_arg
)
- | Call(vel_out, Procedure (sk, task_opt), vel_in, lxm) -> (
+ | Call(vel_out, Procedure (sk, sname, task_opt), vel_in, lxm) -> (
let called_soc = SocUtils.find lxm sk stbl in
let ctx, step_arg =
if
@@ -144,7 +144,7 @@ let (gao2c : Soc.tbl -> 'a soc_pp -> Soc.gao -> unit) =
flush stdout;
raise Delete_C_files
);
- Soc2cDep.gen_step_call sp.soc called_soc (task_opt <> None) vel_out vel_in ctx "step" step_arg
+ Soc2cDep.gen_step_call sp.soc called_soc (task_opt <> None) vel_out vel_in ctx sname step_arg
)
in
sp.cput (gao2str gao)
@@ -154,6 +154,7 @@ let (step2c : Soc.tbl -> 'a soc_pp -> Soc.step_method -> unit) =
if inlined_soc sp.soc.key then () (* don't generate code if inlined *) else
(* let sname = Soc2cDep.step_name sp.soc.key sm.name in *)
let sname = Soc2cDep.step_name sp.soc.key sm.name in
+ if Soc2cIdent.is_step_method_preambule sname then () else
if sm.impl<>Extern then (
let decl, def, ctype = Soc2cDep.get_step_prototype sm sp.soc in
sp.hput (Printf.sprintf "%s\n" decl);
@@ -271,7 +272,7 @@ let (get_used_soc : Soc.t -> KeySet.t) =
(fun acc (_,gaol) -> List.fold_left get_soc_of_gao acc gaol) acc l
| Call(_,Assign,_,_) -> acc
| Call(_,Method((_,sk),_,_),_,_)
- | Call(_,Procedure (sk,_),_,_) -> KeySet.add sk acc
+ | Call(_,Procedure (sk,_,_),_,_) -> KeySet.add sk acc
in
let get_soc_of_step acc sm =
match sm.impl with
diff --git a/lib/soc2cIdent.ml b/lib/soc2cIdent.ml
index 151f2ba5e2ff66468d83afa131a07c08764daaa4..9f5c6d7cca05914ab28995d3c580641598b9232a 100644
--- a/lib/soc2cIdent.ml
+++ b/lib/soc2cIdent.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/06/2024 (at 15:34) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2024 (at 23:16) by Erwan Jahier> *)
let colcol = Str.regexp "::"
let prime = Str.regexp "'"
@@ -100,3 +100,9 @@ let (get_ctx_name : Soc.key -> string) =
(* This function is injective *)
let (get_soc_name : Soc.key -> string) =
fun sk -> (get_base_name sk)
+
+(* Naming Convention TASK_START corresponds to gao which step_name
+ ends with "_step0" (nb possible step names are "get", "set",
+ "<node>_step0" and "<node>_step" *)
+let is_step_method_preambule step_name =
+ step_name.[String.length step_name - 1] = '0'
diff --git a/lib/soc2cIoCtx.ml b/lib/soc2cIoCtx.ml
index 1282d6589ff47f6e69023e4dc4140c12ea924ff3..186f0d6e3af685559e8bb2e5f0deb1668f72c57d 100644
--- a/lib/soc2cIoCtx.ml
+++ b/lib/soc2cIoCtx.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 18/06/2024 (at 15:15) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2024 (at 23:17) by Erwan Jahier> *)
open Soc2cUtil
open Soc2cIdent
@@ -179,7 +179,9 @@ let (gen_step_call : Soc.t -> Soc.t -> bool -> Soc.var_expr list -> Soc.var_expr
in
(String.concat "" l) ^"\n"
in
- let call_step_str = (if para then "//" else " ") ^ Printf.sprintf " %s(%s);\n"
+ let call_step_str =
+ (if para || Soc2cIdent.is_step_method_preambule sname then "//" else " ")
+ ^ Printf.sprintf " %s(%s);\n"
(step_name called_soc.key sname) step_arg in
(set_inputs_str ^ call_step_str ^get_output_str)
@@ -188,12 +190,14 @@ let (get_procedures: Soc.t -> Soc.key list) =
fun soc ->
let rec of_gao = function
| Case (_, id_gaol_l, _) ->
- id_gaol_l |> List.map (fun (_, gaol) -> List.map of_gao gaol) |> List.flatten |> List.flatten
- | Call (_, Procedure (k, None), _,_) ->
- if not Lv6MainArgs.global_opt.Lv6MainArgs.gen_c_inline_predef || not (Soc2cPredef.is_call_supported k) then
+ id_gaol_l |> List.map (fun (_, gaol) -> List.map of_gao gaol) |>
+ List.flatten |> List.flatten
+ | Call (_, Procedure (k, _, None), _,_) ->
+ if not Lv6MainArgs.global_opt.Lv6MainArgs.gen_c_inline_predef
+ || not (Soc2cPredef.is_call_supported k) then
[k]
else
- []
+ []
| Call (_, _, _,_) -> []
in
soc.step |> List.map (fun sm -> match sm.impl with
diff --git a/lib/soc2cUtil.ml b/lib/soc2cUtil.ml
index 802aee324dfa960fcf7183c8da94f9331fc97ebb..d6c9e5425c9632ca3b3c71d0dcb8571c90777f72 100644
--- a/lib/soc2cUtil.ml
+++ b/lib/soc2cUtil.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 14/06/2024 (at 14:09) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2024 (at 17:50) by Erwan Jahier> *)
open Soc2cIdent
open Data
@@ -80,47 +80,47 @@ let string_of_flow_decl_w7annot gaol (id, t) =
let input_list = List.map SocUtils.lustre_string_of_var_expr ins in
match ao, input_list with
| Assign,_ -> None
- | Procedure (("Lustre::ruminus",_,_),_), [a] -> Some (Printf.sprintf "-%s" a)
- | Procedure (("Lustre::iuminus",_,_),_), [a] -> Some (Printf.sprintf "-%s" a)
- | Procedure (("Lustre::uminus",_,_),_), [a] -> Some (Printf.sprintf "-%s" a)
- | Procedure (("Lustre::not",_,_),_), [a] -> Some (Printf.sprintf "not(%s)" a)
- | Procedure (("Lustre::real2int",_,_),_), [a] -> Some (Printf.sprintf "real2int(%s)" a)
- | Procedure (("Lustre::int2real",_,_),_), [a] -> Some (Printf.sprintf "int2real(%s)" a)
- | Procedure (("Lustre::mod",_,_),_), [a;b] -> Some (Printf.sprintf "%s mod %s" a b)
- | Procedure (("Lustre::iplus" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s+%s" a b)
- | Procedure (("Lustre::rplus" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s+%s" a b)
- | Procedure (("Lustre::plus" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s+%s" a b)
- | Procedure (("Lustre::times",_,_),_), [a;b] -> Some (Printf.sprintf "%s*%s" a b)
- | Procedure (("Lustre::itimes",_,_),_), [a;b] -> Some (Printf.sprintf "%s*%s" a b)
- | Procedure (("Lustre::rtimes",_,_),_), [a;b] -> Some (Printf.sprintf "%s*%s" a b)
- | Procedure (("Lustre::slash",_,_),_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
- | Procedure (("Lustre::islash",_,_),_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
- | Procedure (("Lustre::rslash",_,_),_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
- | Procedure (("Lustre::div",_,_),_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
- | Procedure (("Lustre::idiv",_,_),_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
- | Procedure (("Lustre::rdiv",_,_),_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
- | Procedure (("Lustre::minus",_,_),_), [a;b] -> Some (Printf.sprintf "%s-%s" a b)
- | Procedure (("Lustre::iminus",_,_),_), [a;b] -> Some (Printf.sprintf "%s-%s" a b)
- | Procedure (("Lustre::rminus",_,_),_), [a;b] -> Some (Printf.sprintf "%s-%s" a b)
- | Procedure (("Lustre::lt" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s<%s" a b)
- | Procedure (("Lustre::gt" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s>%s" a b)
- | Procedure (("Lustre::lte",_,_),_), [a;b] -> Some (Printf.sprintf "%s<=%s" a b)
- | Procedure (("Lustre::gte",_,_),_), [a;b] -> Some (Printf.sprintf "%s>=%s" a b)
- | Procedure (("Lustre::ilt" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s<%s" a b)
- | Procedure (("Lustre::igt" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s>%s" a b)
- | Procedure (("Lustre::ilte",_,_),_), [a;b] -> Some (Printf.sprintf "%s<=%s" a b)
- | Procedure (("Lustre::igte",_,_),_), [a;b] -> Some (Printf.sprintf "%s>=%s" a b)
- | Procedure (("Lustre::rlt" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s<%s" a b)
- | Procedure (("Lustre::rgt" ,_,_),_), [a;b] -> Some (Printf.sprintf "%s>%s" a b)
- | Procedure (("Lustre::rlte",_,_),_), [a;b] -> Some (Printf.sprintf "%s<=%s" a b)
- | Procedure (("Lustre::rgte",_,_),_), [a;b] -> Some (Printf.sprintf "%s>=%s" a b)
- | Procedure (("Lustre::impl",_,_),_), [a;b] -> Some (Printf.sprintf "%s=>%s" a b)
- | Procedure (("Lustre::xor",_,_),_), [a;b] -> Some (Printf.sprintf "%s xor %s" a b)
- | Procedure (("Lustre::neq",_,_),_), [a;b] -> Some (Printf.sprintf "not(%s=%s)" a b)
- | Procedure (("Lustre::eq",_,_),_), [a;b] -> Some (Printf.sprintf "%s=%s" a b)
- | Procedure (("Lustre::or",_,_),_), [a;b] -> Some (Printf.sprintf "%s or %s" a b)
- | Procedure (("Lustre::and",_,_),_), [a;b] -> Some (Printf.sprintf "%s and %s" a b)
- | Procedure (("Lustre::if",_,_),_),[c;t;e] ->
+ | Procedure (("Lustre::ruminus",_,_),_,_), [a] -> Some (Printf.sprintf "-%s" a)
+ | Procedure (("Lustre::iuminus",_,_),_,_), [a] -> Some (Printf.sprintf "-%s" a)
+ | Procedure (("Lustre::uminus",_,_),_,_), [a] -> Some (Printf.sprintf "-%s" a)
+ | Procedure (("Lustre::not",_,_),_,_), [a] -> Some (Printf.sprintf "not(%s)" a)
+ | Procedure (("Lustre::real2int",_,_),_,_), [a] -> Some (Printf.sprintf "real2int(%s)" a)
+ | Procedure (("Lustre::int2real",_,_),_,_), [a] -> Some (Printf.sprintf "int2real(%s)" a)
+ | Procedure (("Lustre::mod",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s mod %s" a b)
+ | Procedure (("Lustre::iplus" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s+%s" a b)
+ | Procedure (("Lustre::rplus" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s+%s" a b)
+ | Procedure (("Lustre::plus" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s+%s" a b)
+ | Procedure (("Lustre::times",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s*%s" a b)
+ | Procedure (("Lustre::itimes",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s*%s" a b)
+ | Procedure (("Lustre::rtimes",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s*%s" a b)
+ | Procedure (("Lustre::slash",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
+ | Procedure (("Lustre::islash",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
+ | Procedure (("Lustre::rslash",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
+ | Procedure (("Lustre::div",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
+ | Procedure (("Lustre::idiv",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
+ | Procedure (("Lustre::rdiv",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s/%s" a b)
+ | Procedure (("Lustre::minus",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s-%s" a b)
+ | Procedure (("Lustre::iminus",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s-%s" a b)
+ | Procedure (("Lustre::rminus",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s-%s" a b)
+ | Procedure (("Lustre::lt" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s<%s" a b)
+ | Procedure (("Lustre::gt" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s>%s" a b)
+ | Procedure (("Lustre::lte",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s<=%s" a b)
+ | Procedure (("Lustre::gte",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s>=%s" a b)
+ | Procedure (("Lustre::ilt" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s<%s" a b)
+ | Procedure (("Lustre::igt" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s>%s" a b)
+ | Procedure (("Lustre::ilte",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s<=%s" a b)
+ | Procedure (("Lustre::igte",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s>=%s" a b)
+ | Procedure (("Lustre::rlt" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s<%s" a b)
+ | Procedure (("Lustre::rgt" ,_,_),_,_), [a;b] -> Some (Printf.sprintf "%s>%s" a b)
+ | Procedure (("Lustre::rlte",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s<=%s" a b)
+ | Procedure (("Lustre::rgte",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s>=%s" a b)
+ | Procedure (("Lustre::impl",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s=>%s" a b)
+ | Procedure (("Lustre::xor",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s xor %s" a b)
+ | Procedure (("Lustre::neq",_,_),_,_), [a;b] -> Some (Printf.sprintf "not(%s=%s)" a b)
+ | Procedure (("Lustre::eq",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s=%s" a b)
+ | Procedure (("Lustre::or",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s or %s" a b)
+ | Procedure (("Lustre::and",_,_),_,_), [a;b] -> Some (Printf.sprintf "%s and %s" a b)
+ | Procedure (("Lustre::if",_,_),_,_),[c;t;e] ->
Some (Printf.sprintf "if %s then %s else %s" c t e)
| Method((_,("Lustre::arrow",_,_)),_,_), [a;b] -> Some (Printf.sprintf "%s -> %s" a b)
@@ -132,7 +132,7 @@ let string_of_flow_decl_w7annot gaol (id, t) =
Some (Printf.sprintf "pre(%s)" id)
| Method((_,(id,_,_)),_,_),_
- | Procedure((id,_,_),_),_ ->
+ | Procedure((id,_,_),_,_),_ ->
let inputs = String.concat "," input_list in
let id = if String.length id > 8 && String.sub id 0 8 = "Lustre::" then
String.sub id 8 ((String.length id) - 8) else id
diff --git a/lib/socExec.ml b/lib/socExec.ml
index f9e15329c7c01f7fb6c4d046afaa60630473af23..7799b1baa291020277fa5e062d31125f4451b91d 100644
--- a/lib/socExec.ml
+++ b/lib/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 14/06/2024 (at 14:11) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2024 (at 17:47) by Erwan Jahier> *)
open Soc
open Data
@@ -170,7 +170,7 @@ and (do_gao : Lxm.t -> Soc.tbl -> SocExecValue.ctx -> gao -> SocExecValue.ctx) =
in
ctx
)
- | Call(vel_out, Procedure (sk,_), vel_in,lxm) -> (
+ | Call(vel_out, Procedure (sk,_,_), vel_in,lxm) -> (
let (proc_name,_,_) = sk in
let path_saved = ctx.cpath in
let ctx = { ctx with cpath = proc_name::ctx.cpath } in
diff --git a/lib/socExecDbg.ml b/lib/socExecDbg.ml
index 4111a8b631e47c1e779112df8c51ce466d62e284..43aa96e7e0b0255f59ddecb6ae347289c7e71724 100644
--- a/lib/socExecDbg.ml
+++ b/lib/socExecDbg.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 14/06/2024 (at 14:09) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2024 (at 17:50) by Erwan Jahier> *)
open Soc
open Data
open SocExecValue
@@ -495,7 +495,7 @@ and (do_gao : Soc.tbl -> RdbgEvent.t -> gao -> SocExecValue.ctx ->
in
fcont ectx val_ctx
)
- | Call(vel_out, Procedure (sk,_), vel_in, lxm) -> (
+ | Call(vel_out, Procedure (sk,_,_), vel_in, lxm) -> (
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
diff --git a/lib/socNameC.ml b/lib/socNameC.ml
index 10b6766680cc17a159bc44be2355a008d7aebf82..764c831aed7aa53cc3bcb956a1b0029cddbcabc0 100644
--- a/lib/socNameC.ml
+++ b/lib/socNameC.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 14/06/2024 (at 13:57) by Erwan Jahier> *)
+(** Time-stamp: <modified the 19/06/2024 (at 17:50) by Erwan Jahier> *)
type variable_type = {
id: int;
@@ -54,13 +54,17 @@ open Soc
let get_variables_assoc : Soc.t -> (string * variable_type) list = fun soc ->
let i,o = soc.profile in
let io_nb = List.length i + (List.length o) in
- let step_impl =
+ let step_impl_list =
match soc.step with
- | [sm] -> sm.impl
+ | [sm] -> [sm.impl]
+ | [sm1; sm2] ->
+ assert(Lv6MainArgs.global_opt.Lv6MainArgs.multi_task);
+ [sm1.impl; sm2.impl]
+
| [] -> assert false
- | _::_ -> assert false
+ | _::_::_ -> assert false
in
- let lvars =
+ let lvars step_impl =
match step_impl with
| Gaol (vl,_) -> vl
| Predef
@@ -69,19 +73,20 @@ let get_variables_assoc : Soc.t -> (string * variable_type) list = fun soc ->
| Condact _
| Extern -> []
in
- List.mapi (var_to_variable_type io_nb) lvars
+ List.mapi (var_to_variable_type io_nb) (List.map lvars step_impl_list |> List.flatten)
let get_variables : Soc.t -> variable_type list = fun soc ->
snd(List.split (get_variables_assoc soc))
let get_gaol soc =
- let step_impl =
+ let step_impl_list =
match soc.step with
- | [sm] -> sm.impl
+ | [sm] -> [sm.impl]
+ | [sm1; sm2] -> [sm1.impl; sm2.impl]
| [] -> assert false
- | _::_ -> assert false
+ | _::_::_ -> assert false
in
- let gaol =
+ let gaol step_impl =
match step_impl with
| Gaol (_,gaol) -> gaol
| Predef -> assert false
@@ -90,7 +95,7 @@ let get_gaol soc =
| Condact _ -> assert false
| Extern -> assert false
in
- gaol
+ List.map gaol step_impl_list |> List.flatten
let get_nodes : Soc.t -> node_type list = fun soc ->
let gaol = get_gaol soc in
@@ -100,7 +105,7 @@ let get_nodes : Soc.t -> node_type list = fun soc ->
let is_method, k = match ao with
| Assign -> assert false
| Method((_,k),_,_) -> true, k
- | Procedure (k,_) -> false, k
+ | Procedure (k,_,_) -> false, k
in
if Hashtbl.mem tbl k then
cpt, acc
@@ -145,7 +150,7 @@ let get_instances : Soc.t -> instance_type list = fun soc ->
match gao with
| Call(_,Assign,_,_) -> assert false
| Call(args_out, Method((_,k), _,_), args_in, _)
- | Call(args_out, Procedure (k,_) , args_in, _) ->
+ | Call(args_out, Procedure (k,_,_) , args_in, _) ->
let node_cpt, _inst_cpt = match Hashtbl.find_opt ltbl k with
| None -> incr node_cpt_ref; Hashtbl.add ltbl k (!node_cpt_ref, 0); !node_cpt_ref, 0
| Some (node_cpt, inst_cpt) ->
diff --git a/lib/socUtils.ml b/lib/socUtils.ml
index 76e213537ee420c595d35dfb54b80cbd25805850..2eccd72928a4298f123f1dced408b5912be539dc 100644
--- a/lib/socUtils.ml
+++ b/lib/socUtils.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 17/06/2024 (at 15:38) by Erwan Jahier> *)
+(** Time-stamp: <modified the 19/06/2024 (at 17:50) by Erwan Jahier> *)
open Soc
@@ -94,7 +94,7 @@ let string_of_operation_ff: (atomic_operation -> Format.formatter -> unit) =
fun v ff -> match v with
| Assign -> () (* On suppose qu'il est déjà affiché dans string_of_gao *)
| Method((n, _sk),sname,_) -> fprintf ff "%s.%s" n sname
- | Procedure(proc,_) -> fprintf ff "%s" (string_of_soc_key proc)
+ | Procedure(proc,_,_) -> fprintf ff "%s" (string_of_soc_key proc)
let string_of_operation: (atomic_operation -> string) = fun v ->
call_fun_ff (string_of_operation_ff v)
diff --git a/lib/topoSort.ml b/lib/topoSort.ml
index 91ef8b364c4663b4ec872c8b5bc702a9efb5f2a0..6c84ec4995dc63776edaf15a4c36ed82d4287dca 100644
--- a/lib/topoSort.ml
+++ b/lib/topoSort.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 17/07/2017 (at 16:55) by Erwan Jahier> *)
+(** Time-stamp: <modified the 19/06/2024 (at 14:30) by Erwan Jahier> *)
module type PartialOrder =
@@ -36,7 +36,7 @@ module Make(PO: PartialOrder) = struct
type color_table = color Mapt.t
let (grey_actions : color_table -> elt list) =
- fun ct ->
+ fun ct ->
Mapt.fold
(fun x color acc -> if color=Grey then x::acc else acc) ct []
@@ -66,27 +66,27 @@ module Make(PO: PartialOrder) = struct
List.rev res
in
f x []
-
+
let rec (visit : store -> color_table -> elt -> color_table) =
- fun store color_t n ->
+ fun store color_t n ->
if not (PO.have_dep store n) then Mapt.add n Black color_t else
let color_t =
- List.fold_left
- (fun color_t nt ->
- try
- match Mapt.find nt color_t with
- | Grey ->
+ List.fold_left
+ (fun color_t nt ->
+ try
+ match Mapt.find nt color_t with
+ | Grey ->
let c = smallest_cycle store n (grey_actions color_t) in
raise (DependencyCycle (n, c))
- | Black -> color_t
- with
- (* The node [nt] is white *)
- Not_found -> visit store color_t nt
- )
- (Mapt.add n Grey color_t)
- (PO.find_dep store n)
+ | Black -> color_t
+ with
+ (* The node [nt] is white *)
+ Not_found -> visit store color_t nt
+ )
+ (Mapt.add n Grey color_t)
+ (PO.find_dep store n)
in
- Mapt.add n Black color_t
+ Mapt.add n Black color_t
(* TEDLT *)
let (check_there_is_no_cycle : store -> elt list -> unit) =
@@ -94,28 +94,27 @@ let (check_there_is_no_cycle : store -> elt list -> unit) =
ignore (List.fold_left (fun acc x -> visit store acc x) Mapt.empty l)
let (f : store -> elt list -> elt list) =
- fun store l ->
- let visited_init =
- List.fold_left (fun acc x -> Mapt.add x false acc) Mapt.empty l
- in
- let rec aux (store:store) (acc:elt list) (l:elt list) (visited:bool Mapt.t) =
- (* The graph contains no cycle! *)
- match l with
- | [] -> List.rev acc
- | x::tail ->
- if (try Mapt.find x visited
- with Not_found ->
- true (* migth occur if a dep is not the list to be sorted *))
- then
- aux store acc tail visited
- else
- let x_succ = PO.find_dep store x in
- if x_succ = [] then
- aux store (x::acc) tail (Mapt.add x true visited)
- else
- aux (PO.remove_dep store x) acc (x_succ @ l) visited
- in
- check_there_is_no_cycle store l;
- aux store [] l visited_init
+ fun store l ->
+ let visited_init =
+ List.fold_left (fun acc x -> Mapt.add x false acc) Mapt.empty l
+ in
+ let rec aux (store:store) (acc:elt list) (l:elt list) (visited:bool Mapt.t) =
+ (* The graph contains no cycle! *)
+ match l with
+ | [] -> List.rev acc
+ | x::tail ->
+ if
+ (try Mapt.find x visited with Not_found (* migth occur if a dep is not the list to be sorted *) -> true)
+ then
+ aux store acc tail visited
+ else
+ let x_succ = PO.find_dep store x in
+ if x_succ = [] then
+ aux store (x::acc) tail (Mapt.add x true visited)
+ else
+ aux (PO.remove_dep store x) acc (x_succ @ l) visited
+ in
+ check_there_is_no_cycle store l;
+ aux store [] l visited_init
end
diff --git a/lib/topoSort.mli b/lib/topoSort.mli
index 192670778c395ca1bee4d5ffac98b6d59038eec0..e975574902f803c8f157719e91cbf516f518e25e 100644
--- a/lib/topoSort.mli
+++ b/lib/topoSort.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 03/02/2016 (at 10:04) by Erwan Jahier> *)
+(** Time-stamp: <modified the 19/06/2024 (at 14:38) by Erwan Jahier> *)
module type PartialOrder =
@@ -6,7 +6,7 @@ module type PartialOrder =
type elt
type store
val have_dep : store -> elt -> bool
- val find_dep : store -> elt -> elt list
+ val find_dep : store -> elt -> elt list (* elt at the beginning of the list have higher priotity *)
val remove_dep:store -> elt -> store
end
@@ -20,6 +20,6 @@ module type S =
end
-module Make(PO: PartialOrder) : S
+module Make(PO: PartialOrder) : S
with type elt = PO.elt
with type store = PO.store
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index c84aaf16e205d02eb4fd4929d2359765efe1ea4e..08446a6bcd791cd549c069a84da19ae1a49bd0c2 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test run by jahier on Tue Jun 18 15:52:59
+Test run by jahier on Thu Jun 20 09:25:19
Native configuration is x86_64-pc-linux-gnu
=== lus2lic0 tests ===
@@ -66,7 +66,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 Jun 18 15:53:00
+Test run by jahier on Thu Jun 20 09:25:20
Native configuration is x86_64-pc-linux-gnu
=== lus2lic1 tests ===
@@ -738,7 +738,7 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_lv6_and_lv6_en multipar.lus {}
PASS: /home/jahier/lus2lic/test/../utils/compare_gcc_and_clang multipar.lus {}
==> lus2lic2.sum <==
-Test run by jahier on Tue Jun 18 15:59:06
+Test run by jahier on Thu Jun 20 09:31:36
Native configuration is x86_64-pc-linux-gnu
=== lus2lic2 tests ===
@@ -1386,7 +1386,7 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_gcc_and_clang zzz2.lus {}
PASS: /home/jahier/lus2lic/test/../utils/compare_2ch_and_2cs zzz2.lus {}
==> lus2lic3.sum <==
-Test run by jahier on Tue Jun 18 16:06:01
+Test run by jahier on Thu Jun 20 09:37:51
Native configuration is x86_64-pc-linux-gnu
=== lus2lic3 tests ===
@@ -2013,7 +2013,7 @@ PASS: /home/jahier/lus2lic/test/../utils/check_knc multipar.lus {}
==> lus2lic4.sum <==
-Test run by jahier on Tue Jun 18 16:08:08
+Test run by jahier on Thu Jun 20 09:40:08
Native configuration is x86_64-pc-linux-gnu
=== lus2lic4 tests ===
@@ -2639,11 +2639,11 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_2ch_and_2cs multipar.lus {}
===============================
# Total number of failures: 29
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 366 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 414 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 127 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 114 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 376 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 374 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 136 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 132 seconds
* Ref time:
-435.18user 137.98system 17:02.91elapsed 56%CPU (0avgtext+0avgdata 94892maxresident)k
-247408inputs+907320outputs (1170major+35412857minor)pagefaults 0swaps
+442.11user 147.30system 17:01.02elapsed 57%CPU (0avgtext+0avgdata 99320maxresident)k
+271488inputs+906648outputs (2566major+35369759minor)pagefaults 0swaps
* Quick time (-j 4):