Skip to content

GitLab

Commit 6e10b5ef authored by erwan's avatar erwan
Browse files

Fix: raise a proper error when current is used on the base clock

parent d4748be6
Pipeline #45740 passed with stages
in 4 minutes and 8 seconds
Hide whitespace changes
Inline Side-by-side
lib/evalClock.ml
View file @ 6e10b5ef
(* Time-stamp: <modified the 19/06/2020 (at 14:43) by Erwan Jahier> *)
(* Time-stamp: <modified the 19/06/2020 (at 16:09) by Erwan Jahier> *)
open LicEvalConst
......
lib/socPredef.ml
View file @ 6e10b5ef
(* Time-stamp: <modified the 19/06/2020 (at 14:56) by Erwan Jahier> *)
(* Time-stamp: <modified the 19/06/2020 (at 16:27) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
......@@ -124,223 +124,224 @@ let of_fby_soc_key :Lxm.t -> Soc.var_expr -> Soc.key -> Soc.t =
(* exported *)
let of_soc_key : Lxm.t -> Soc.key -> Soc.t =
fun lxm sk ->
let (id, tl, _) = sk in
let sp = soc_profile_of_types in
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::iplus"
| "Lustre::rplus"
| "Lustre::plus" -> (make_soc sk (sp tl) [step21 lxm None id])
| "Lustre::times"
| "Lustre::itimes"
| "Lustre::rtimes" -> (make_soc sk (sp tl) [step21 lxm None id])
| "Lustre::slash"
| "Lustre::islash"
| "Lustre::rslash" -> (make_soc sk (sp tl) [step21 lxm None id])
| "Lustre::div"
| "Lustre::idiv"
| "Lustre::rdiv" -> (make_soc sk (sp tl) [step21 lxm None id])
| "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::impl" -> (make_soc sk (sp tl) [step21 lxm None id])
(* Those have instances *)
| "Lustre::current" -> (
let tl,cc = match sk with
| _,tl, Curr(cc) -> tl,cc
| _,_,_ -> assert false
in
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 = [];
}
)
| "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 = [];
}
| "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;
}
| "Lustre::if" -> {
key = sk;
profile = (sp tl);
let (id, tl, _) = sk in
let sp = soc_profile_of_types in
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::iplus"
| "Lustre::rplus"
| "Lustre::plus" -> (make_soc sk (sp tl) [step21 lxm None id])
| "Lustre::times"
| "Lustre::itimes"
| "Lustre::rtimes" -> (make_soc sk (sp tl) [step21 lxm None id])
| "Lustre::slash"
| "Lustre::islash"
| "Lustre::rslash" -> (make_soc sk (sp tl) [step21 lxm None id])
| "Lustre::div"
| "Lustre::idiv"
| "Lustre::rdiv" -> (make_soc sk (sp tl) [step21 lxm None id])
| "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::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 = [];
(* init = None; *)
precedences = [];
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 = [];
memory = No_mem;
step = [
}
)
| _,_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 = [];
}
| "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;
}
| "Lustre::if" -> {
key = sk;
profile = (sp tl);
clock_profile = [];
instances = [];
(* init = None; *)
precedences = [];
assertions = [];
memory = No_mem;
step = [
{
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 = [];
}
| "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 = [];
}
| _ ->
failwith ("*** The soc of "^id ^ " is not defined! \n")
} ];
}
| "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 = [];
}
| "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 = [];
}
| _ ->
failwith ("*** The soc of "^id ^ " is not defined! \n")
......@@ -556,8 +557,10 @@ let (soc_interface_of_pos_op:
let concrete_type = try List.nth types 1 with _ -> assert false in
let soc = of_soc_key lxm (("Lustre::current"), types@[concrete_type], Curr(cc)) in
instanciate_soc soc concrete_type
| Lic.CURRENT _, _, _ ->
assert false (* sno *)
| Lic.CURRENT None, _, _ ->
let concrete_type = try List.nth types 0 with _ -> assert false in
let soc = of_soc_key lxm (("Lustre::current"), types@[concrete_type], Nomore) in
instanciate_soc soc concrete_type
| Lic.ARROW, _, _ ->
let concrete_type = List.nth types 0 in
let soc = of_soc_key lxm (("Lustre::arrow"), types@[concrete_type],
......
test/lus2lic.sum
View file @ 6e10b5ef
==> lus2lic0.sum <==
Test run by jahier on Fri Jun 19 15:04:42
Test run by jahier on Fri Jun 19 16:31:25
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 Fri Jun 19 15:04:43
Test run by jahier on Fri Jun 19 16:31:26
Native configuration is x86_64-pc-linux-gnu
=== lus2lic1 tests ===
......@@ -413,7 +413,7 @@ PASS: ./lus2lic {-2c multipar.lus -n multipar}
PASS: sh multipar.sh
==> lus2lic2.sum <==
Test run by jahier on Fri Jun 19 15:05:07
Test run by jahier on Fri Jun 19 16:31:48
Native configuration is x86_64-pc-linux-gnu
=== lus2lic2 tests ===
......@@ -753,7 +753,7 @@ PASS: sh zzz2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
Test run by jahier on Fri Jun 19 15:05:38
Test run by jahier on Fri Jun 19 16:32:18
Native configuration is x86_64-pc-linux-gnu
=== lus2lic3 tests ===
......@@ -1267,7 +1267,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
Test run by jahier on Fri Jun 19 15:06:23
Test run by jahier on Fri Jun 19 16:33:00
Native configuration is x86_64-pc-linux-gnu
=== lus2lic4 tests ===
......@@ -1759,7 +1759,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
# of expected failures 54
==> lus2lic1.sum <==
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus 34137 {}
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus 33923 {}
=== lus2lic1 Summary ===
......@@ -1788,13 +1788,13 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus 34137
===============================
# Total number of failures: 10
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 24 seconds
lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 31 seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 45 seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 22 seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 22 seconds
lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 30 seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 42 seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 20 seconds
* Ref time:
74.43user 16.16system 2:02.49elapsed 73%CPU (0avgtext+0avgdata 42080maxresident)k
0inputs+151648outputs (0major+8408595minor)pagefaults 0swaps
69.10user 14.89system 1:55.13elapsed 72%CPU (0avgtext+0avgdata 42100maxresident)k
0inputs+151576outputs (0major+8407303minor)pagefaults 0swaps
* Quick time (-j 4):
86.00user 16.60system 1:10.17elapsed 146%CPU (0avgtext+0avgdata 42096maxresident)k
0inputs+146640outputs (0major+8181699minor)pagefaults 0swaps
83.76user 16.48system 1:23.56elapsed 119%CPU (0avgtext+0avgdata 42296maxresident)k
0inputs+150184outputs (0major+8362589minor)pagefaults 0swaps
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment