diff --git a/lib/socPredef.ml b/lib/socPredef.ml
index d4848811cef35cfbfcd47c05225e7c0a345e7a46..390d67bb7ffc16d007dd4dc6f80807c1633baa37 100644
--- a/lib/socPredef.ml
+++ b/lib/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/06/2020 (at 16:27) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/05/2022 (at 23:31) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -129,145 +129,147 @@ let of_soc_key : Lxm.t -> Soc.key -> Soc.t =
let sp_nary = soc_profile_of_types_nary in
match id with
| "Lustre::ruminus"
- | "Lustre::iuminus"
- | "Lustre::uminus" -> (make_soc sk (sp tl) [step11 lxm id])
- | "Lustre::not" -> (make_soc sk (sp tl) [step11 lxm id])
- | "Lustre::real2int" -> (make_soc sk (sp tl) [step11 lxm id])
- | "Lustre::int2real" -> (make_soc sk (sp tl) [step11 lxm id])
-
- | "Lustre::mod" -> (make_soc sk (sp tl) [step21 lxm None id])
+ | "Lustre::iuminus"
+ | "Lustre::uminus"
+ | "Lustre::not"
+ | "Lustre::real2int"
+ | "Lustre::int2real"
+ | "Lustre::random_int"
+ -> (make_soc sk (sp tl) [step11 lxm id])
+
+ | "Lustre::mod"
| "Lustre::iplus"
- | "Lustre::rplus"
- | "Lustre::plus" -> (make_soc sk (sp tl) [step21 lxm None id])
+ | "Lustre::rplus"
+ | "Lustre::plus"
| "Lustre::times"
- | "Lustre::itimes"
- | "Lustre::rtimes" -> (make_soc sk (sp tl) [step21 lxm None id])
+ | "Lustre::itimes"
+ | "Lustre::rtimes"
| "Lustre::slash"
- | "Lustre::islash"
- | "Lustre::rslash" -> (make_soc sk (sp tl) [step21 lxm None id])
+ | "Lustre::islash"
+ | "Lustre::rslash"
| "Lustre::div"
- | "Lustre::idiv"
- | "Lustre::rdiv" -> (make_soc sk (sp tl) [step21 lxm None id])
+ | "Lustre::idiv"
+ | "Lustre::rdiv"
| "Lustre::minus"
- | "Lustre::iminus"
- | "Lustre::rminus" -> (make_soc sk (sp tl) [step21 lxm None id])
-
- | "Lustre::lt" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::gt" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::lte" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::gte" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::ilt" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::igt" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::ilte" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::igte" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::rlt" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::rgt" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::rlte" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::rgte" -> (make_soc sk (sp tl) [step21 lxm None id])
-
- | "Lustre::and" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::eq" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::neq" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::or" -> (make_soc sk (sp tl) [step21 lxm None id])
- | "Lustre::xor" -> (make_soc sk (sp tl) [step21 lxm None id])
+ | "Lustre::iminus"
+ | "Lustre::rminus"
+
+ | "Lustre::lt"
+ | "Lustre::gt"
+ | "Lustre::lte"
+ | "Lustre::gte"
+ | "Lustre::ilt"
+ | "Lustre::igt"
+ | "Lustre::ilte"
+ | "Lustre::igte"
+ | "Lustre::rlt"
+ | "Lustre::rgt"
+ | "Lustre::rlte"
+ | "Lustre::rgte"
+
+ | "Lustre::and"
+ | "Lustre::eq"
+ | "Lustre::neq"
+ | "Lustre::or"
+ | "Lustre::xor"
| "Lustre::impl" -> (make_soc sk (sp tl) [step21 lxm None id])
-
+
(* Those have instances *)
| "Lustre::current" -> (
- match sk with
- | _,tl, Curr(cc) -> (
- assert(tl<>[]);
- let t = List.hd (List.tl tl) in
- let mem:var = (get_mem_name sk t, t) in
- let prof:var list * var list = sp tl in
- let cv,vin,vout =
- match prof with ([cv;vin],[vout]) -> cv,vin,vout | _ -> assert false
- in
- {
- key = sk;
- profile = (sp tl);
- clock_profile = [];
- instances = [];
- memory = Mem (t);
- step = [
- {
- name = "step";
- lxm = lxm;
- idx_ins = [0;1];
- idx_outs = [0];
- impl =
- Gaol([],
- [Case((fst cv),[
- (Lv6Id.string_of_long false cc, [Call([Var(mem)],
- Assign, [Var(vin)],
- lxm)])],
- lxm);
- Call([Var(vout)], Assign, [Var(mem)], lxm )])
- };
- ];
- precedences = [];
- assertions = [];
- }
+ match sk with
+ | _,tl, Curr(cc) -> (
+ assert(tl<>[]);
+ let t = List.hd (List.tl tl) in
+ let mem:var = (get_mem_name sk t, t) in
+ let prof:var list * var list = sp tl in
+ let cv,vin,vout =
+ match prof with ([cv;vin],[vout]) -> cv,vin,vout | _ -> assert false
+ in
+ {
+ key = sk;
+ profile = (sp tl);
+ clock_profile = [];
+ instances = [];
+ memory = Mem (t);
+ step = [
+ {
+ name = "step";
+ lxm = lxm;
+ idx_ins = [0;1];
+ idx_outs = [0];
+ impl =
+ Gaol([],
+ [Case((fst cv),[
+ (Lv6Id.string_of_long false cc, [Call([Var(mem)],
+ Assign, [Var(vin)],
+ lxm)])],
+ lxm);
+ Call([Var(vout)], Assign, [Var(mem)], lxm )])
+ };
+ ];
+ precedences = [];
+ assertions = [];
+ }
+ )
+ | _,_tl, Nomore -> (* current is applied to something on the base clock *)
+ raise (Lv6errors.Compile_error(lxm, "current applied on the base clock"))
+ | _,_, _ -> assert false
)
- | _,_tl, Nomore -> (* current is applied to something on the base clock *)
- raise (Lv6errors.Compile_error(lxm, "current applied on the base clock"))
- | _,_, _ -> assert false
- )
| "Lustre::pre" ->
- let _,tl,_ = sk in
- let t = List.hd tl in
- let pre_mem:var = (get_mem_name sk t, t) in
- let prof = sp tl in
- let v1,vout = match prof with ([v1],[vout]) -> v1,vout | _ -> assert false in
- {
- key = sk;
- profile = (sp tl);
- clock_profile = [];
- instances = [];
- memory = Mem (t); (* so that pre_mem exist *)
- step = [
- {
- name = "get";
- lxm = lxm;
- idx_ins = [];
- idx_outs = [0];
- (* impl = Predef; *)
- impl = Gaol([],[Call([Var(vout)], Assign, [Var(pre_mem)], lxm)]);
- (*impl = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]); *)
- };
- {
- name = "set";
- lxm = lxm;
- idx_ins = [0];
- idx_outs = [];
- (* impl = Predef; *)
- impl = Gaol([],[Call([Var(pre_mem)], Assign, [Var(v1)], lxm )]);
- (* impl = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]); *)
- };
- ];
- precedences = ["set", ["get"]];
- assertions = [];
- }
+ let _,tl,_ = sk in
+ let t = List.hd tl in
+ let pre_mem:var = (get_mem_name sk t, t) in
+ let prof = sp tl in
+ let v1,vout = match prof with ([v1],[vout]) -> v1,vout | _ -> assert false in
+ {
+ key = sk;
+ profile = (sp tl);
+ clock_profile = [];
+ instances = [];
+ memory = Mem (t); (* so that pre_mem exist *)
+ step = [
+ {
+ name = "get";
+ lxm = lxm;
+ idx_ins = [];
+ idx_outs = [0];
+ (* impl = Predef; *)
+ impl = Gaol([],[Call([Var(vout)], Assign, [Var(pre_mem)], lxm)]);
+ (*impl = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]); *)
+ };
+ {
+ name = "set";
+ lxm = lxm;
+ idx_ins = [0];
+ idx_outs = [];
+ (* impl = Predef; *)
+ impl = Gaol([],[Call([Var(pre_mem)], Assign, [Var(v1)], lxm )]);
+ (* impl = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]); *)
+ };
+ ];
+ precedences = ["set", ["get"]];
+ assertions = [];
+ }
| "Lustre::arrow" ->
- let prof = sp tl in
- {
- key = sk;
- profile = prof;
- clock_profile = [];
- instances = [];
- step = [
- {
- name = "step";
- lxm = lxm;
- idx_ins = [0;1];
- idx_outs = [0];
- impl = Predef;
- }
- ];
- precedences = [];
- assertions = [];
- memory = Mem Bool;
- }
+ let prof = sp tl in
+ {
+ key = sk;
+ profile = prof;
+ clock_profile = [];
+ instances = [];
+ step = [
+ {
+ name = "step";
+ lxm = lxm;
+ idx_ins = [0;1];
+ idx_outs = [0];
+ impl = Predef;
+ }
+ ];
+ precedences = [];
+ assertions = [];
+ memory = Mem Bool;
+ }
| "Lustre::if" -> {
key = sk;
profile = (sp tl);
@@ -278,70 +280,70 @@ let of_soc_key : Lxm.t -> Soc.key -> Soc.t =
assertions = [];
memory = No_mem;
step = [
- {
- name = "step";
- lxm = lxm;
- idx_ins = [0; 1; 2];
- idx_outs = [0];
- impl = Predef;
+ {
+ name = "step";
+ lxm = lxm;
+ idx_ins = [0; 1; 2];
+ idx_outs = [0];
+ impl = Predef;
} ];
}
| "Lustre::nor" ->
- let size = match sk with
- | _,[Array(Bool,size);_],_ -> size
- | _,bools,_ ->
- if List.exists (fun t -> t<>Bool) bools then
- failwith "type error in nor"
- else
- List.length bools
- in
- {
- Soc.key = sk;
- Soc.profile = sp_nary tl;
- Soc.clock_profile = [];
- Soc.instances = [] ;
- Soc.step = [
- {
- name = "step";
- lxm = lxm;
- idx_ins = [0];
- idx_outs = [0];
- impl = Boolred(0, 0, size);
- }
- ];
- Soc.memory = No_mem;
- Soc.precedences = [];
- Soc.assertions = [];
- }
+ let size = match sk with
+ | _,[Array(Bool,size);_],_ -> size
+ | _,bools,_ ->
+ if List.exists (fun t -> t<>Bool) bools then
+ failwith "type error in nor"
+ else
+ List.length bools
+ in
+ {
+ Soc.key = sk;
+ Soc.profile = sp_nary tl;
+ Soc.clock_profile = [];
+ Soc.instances = [] ;
+ Soc.step = [
+ {
+ name = "step";
+ lxm = lxm;
+ idx_ins = [0];
+ idx_outs = [0];
+ impl = Boolred(0, 0, size);
+ }
+ ];
+ Soc.memory = No_mem;
+ Soc.precedences = [];
+ Soc.assertions = [];
+ }
| "Lustre::diese" ->
- let size = match sk with
- | _,[Array(Bool,size);_],_ -> size
- | _,bools,_ ->
- if List.exists (fun t -> t<>Bool) bools then
- failwith "type error in #"
- else
- List.length bools
- in
- {
- Soc.key = sk;
- Soc.profile = sp_nary tl;
- Soc.clock_profile = [];
- Soc.instances = [] ;
- Soc.step = [
- {
- name = "step";
- lxm = lxm;
- idx_ins = [0];
- idx_outs = [0];
- impl = Boolred(0,1, size);
- }
- ];
- Soc.memory = No_mem;
- Soc.precedences = [];
- Soc.assertions = [];
- }
+ let size = match sk with
+ | _,[Array(Bool,size);_],_ -> size
+ | _,bools,_ ->
+ if List.exists (fun t -> t<>Bool) bools then
+ failwith "type error in #"
+ else
+ List.length bools
+ in
+ {
+ Soc.key = sk;
+ Soc.profile = sp_nary tl;
+ Soc.clock_profile = [];
+ Soc.instances = [] ;
+ Soc.step = [
+ {
+ name = "step";
+ lxm = lxm;
+ idx_ins = [0];
+ idx_outs = [0];
+ impl = Boolred(0,1, size);
+ }
+ ];
+ Soc.memory = No_mem;
+ Soc.precedences = [];
+ Soc.assertions = [];
+ }
| _ ->
- failwith ("*** The soc of "^id ^ " is not defined! \n")
+ failwith ("*** The soc of "^id ^ " is not defined! \n")
@@ -514,8 +516,11 @@ let output_type_of_op op tl =
| "Lustre::nor"
| "Lustre::diese"
-> Bool
- | "Lustre::real2int" -> Int
- | "Lustre::int2real" -> Real
+ | "Lustre::real2int"
+ | "Lustre::random_int"
+ -> Int
+ | "Lustre::int2real"
+ -> Real
| "Lustre::if" -> assert(tl<>[]);List.hd (List.tl tl)
| "Lustre::hat" -> assert false (* sno? *)
| "Lustre::array" -> assert false (* sno? *)
diff --git a/lib/socPredef2cStack.ml b/lib/socPredef2cStack.ml
index 9aa506c9f6eb1c238392747a8e27741c808446f0..d1970f240967f80c4a88ba4743f6580200a6a228 100644
--- a/lib/socPredef2cStack.ml
+++ b/lib/socPredef2cStack.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 15/03/2021 (at 18:06) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/05/2022 (at 23:35) by Erwan Jahier> *)
open Data
open Soc
@@ -185,6 +185,8 @@ let (get_predef_op: Soc.key -> string) =
| "Lustre::not" -> lustre_unop sk "!"
| "Lustre::real2int" -> lustre_unop sk "(_integer)"
| "Lustre::int2real" -> lustre_unop sk "(_real)"
+
+ | "Lustre::random_int" -> lustre_unop sk "rand() % "
| "Lustre::lt"
| "Lustre::rlt"
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index ce6f5e4d1a96985811612bbc6496422031397417..954e3f8dab3bc7d625c8a7ef98a2ddef915c0e41 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test run by jahier on Thu May 12 10:47:08
+Test run by jahier on Wed Jun 15 15:01:24
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 Thu May 12 10:47:09
+Test run by jahier on Wed Jun 15 15:01:25
Native configuration is x86_64-pc-linux-gnu
=== lus2lic1 tests ===
@@ -626,7 +626,7 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
PASS: /home/jahier/lus2lic/test/../utils/compare_lv6_and_lv6_en multipar.lus {}
==> lus2lic2.sum <==
-Test run by jahier on Thu May 12 10:51:44
+Test run by jahier on Wed Jun 15 15:07:17
Native configuration is x86_64-pc-linux-gnu
=== lus2lic2 tests ===
@@ -1171,7 +1171,7 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_lv6_and_lv6_en zzz2.lus {}
PASS: /home/jahier/lus2lic/test/../utils/compare_gcc_and_clang zzz2.lus {}
==> lus2lic3.sum <==
-Test run by jahier on Thu May 12 10:56:36
+Test run by jahier on Wed Jun 15 15:13:46
Native configuration is x86_64-pc-linux-gnu
=== lus2lic3 tests ===
@@ -1686,7 +1686,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
-Test run by jahier on Thu May 12 10:58:05
+Test run by jahier on Wed Jun 15 15:14:57
Native configuration is x86_64-pc-linux-gnu
=== lus2lic4 tests ===
@@ -2211,11 +2211,11 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_gcc_and_clang multipar.lus {}
===============================
# Total number of failures: 17
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 274 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 292 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 89 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 43 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 352 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 389 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 71 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 89 seconds
* Ref time:
-234.87user 64.78system 11:39.53elapsed 42%CPU (0avgtext+0avgdata 73968maxresident)k
-7627992inputs+462696outputs (22736major+19473366minor)pagefaults 0swaps
+323.65user 78.07system 15:01.63elapsed 44%CPU (0avgtext+0avgdata 77252maxresident)k
+143424inputs+458920outputs (454major+19444018minor)pagefaults 0swaps
* Quick time (-j 4):