Skip to content
Snippets Groups Projects
Commit 53e5bb83 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Fix an internal error that was actually occuring on faulty programs 

when the arity of an alias node was wrong.
parent 3c009166
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/socExec.ml
+ 4
− 2
View file @ 53e5bb83
(* Time-stamp: <modified the 24/05/2013 (at 09:55) by Erwan Jahier> *) (* Time-stamp: <modified the 31/05/2013 (at 13:59) by Erwan Jahier> *)
open Soc open Soc
open Data open Data
...@@ -199,7 +199,9 @@ and expand_var enum_flag var = match var with ...@@ -199,7 +199,9 @@ and expand_var enum_flag var = match var with
done; done;
(expand_profile enum_flag !res) (expand_profile enum_flag !res)
| (vn,Struct(name,fl)) -> expand_profile enum_flag (List.map (fun (fn,t) -> vn^"_"^fn,t ) fl) | (vn,Struct(name,fl)) -> expand_profile enum_flag (List.map (fun (fn,t) -> vn^"_"^fn,t ) fl)
| (vn,Extern id) -> assert false (* finish me! *) | (vn,Extern id) ->
print_string "Extern node not yet supported, sorry\n"; flush stdout;
assert false (* finish me! *)
| (vn,Alpha _) -> assert false (* should not occur *) | (vn,Alpha _) -> assert false (* should not occur *)
let (int_to_enum : Data.v -> Soc.ident list -> Data.v) = let (int_to_enum : Data.v -> Soc.ident list -> Data.v) =
......
src/unifyType.ml
+ 45
− 43
View file @ 53e5bb83
(* Time-stamp: <modified the 17/05/2013 (at 10:56) by Erwan Jahier> *) (* Time-stamp: <modified the 31/05/2013 (at 15:43) by Erwan Jahier> *)
(* (*
12/07. Premier pas vers une méthode un peu plus standard : 12/07. Premier pas vers une méthode un peu plus standard :
...@@ -59,62 +59,64 @@ Inutile d'essayer de ressembler à un vrai algo d'unification de type : ...@@ -59,62 +59,64 @@ Inutile d'essayer de ressembler à un vrai algo d'unification de type :
et un given, et on doit arriver à s'en sortir ... et un given, et on doit arriver à s'en sortir ...
*) *)
let f (l1: Lic.type_ list) (l2: Lic.type_ list): t = let f (l1: Lic.type_ list) (l2: Lic.type_ list): t =
let rec unify_type_eff (t1:Lic.type_) (t2: Lic.type_) : t = let rec unify_type_eff (t1:Lic.type_) (t2: Lic.type_) : t =
if t1 = t2 then Equal else if t1 = t2 then Equal else
match (t1,t2) with match (t1,t2) with
| Array_type_eff(teff_ext1,i1), Array_type_eff(teff_ext2,i2) -> | Array_type_eff(teff_ext1,i1), Array_type_eff(teff_ext2,i2) ->
if i1 <> i2 then Ko "\n*** incompatible array size" if i1 <> i2 then Ko "\n*** incompatible array size"
else unify_type_eff teff_ext1 teff_ext2 else unify_type_eff teff_ext1 teff_ext2
| Struct_type_eff(l1, fl1), Struct_type_eff(l2, fl2) -> | Struct_type_eff(l1, fl1), Struct_type_eff(l2, fl2) ->
if l1 <> l2 then Ko "\n*** incompatible structure" else if l1 <> l2 then Ko "\n*** incompatible structure" else
(** USELESS ??? *) (** USELESS ??? *)
let fl1 = List.map (fun (_,(te,_)) -> te) fl1 let fl1 = List.map (fun (_,(te,_)) -> te) fl1
and fl2 = List.map (fun (_,(te,_)) -> te) fl2 in and fl2 = List.map (fun (_,(te,_)) -> te) fl2 in
assert(List.length fl1 = List.length fl1); assert(List.length fl1 = List.length fl1);
List.fold_left2 unify_do_acc Equal fl1 fl2 List.fold_left2 unify_do_acc Equal fl1 fl2
| TypeVar AnyNum, TypeVar Any | TypeVar AnyNum, TypeVar Any
| TypeVar Any, TypeVar AnyNum -> Unif (TypeVar AnyNum) | TypeVar Any, TypeVar AnyNum -> Unif (TypeVar AnyNum)
| t, TypeVar Any | (TypeVar Any), t -> | t, TypeVar Any | (TypeVar Any), t ->
if contains t (TypeVar Any) || contains t (TypeVar AnyNum) then if contains t (TypeVar Any) || contains t (TypeVar AnyNum) then
Ko(("\n*** " ^ teff2str t1) ^ " and " ^ (teff2str t2) ^ Ko(("\n*** " ^ teff2str t1) ^ " and " ^ (teff2str t2) ^
" are not unifiable (there is a cycle)") " are not unifiable (there is a cycle)")
else Unif t else Unif t
| t, TypeVar AnyNum | t, TypeVar AnyNum
| TypeVar AnyNum, t -> | TypeVar AnyNum, t ->
if contains t (TypeVar Any) || contains t (TypeVar AnyNum) then if contains t (TypeVar Any) || contains t (TypeVar AnyNum) then
Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^ Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
" are not unifiable (there is a cycle)") " are not unifiable (there is a cycle)")
else if is_overloadable t then Unif t else if is_overloadable t then Unif t
else else
Ko("\n*** get '" ^ (teff2str t) ^ "' where 'int' or 'real' was expected") Ko("\n*** get '" ^ (teff2str t) ^ "' where 'int' or 'real' was expected")
| _ -> | _ ->
Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^ Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
" are not unifiable") " are not unifiable")
and (unify_do_acc: t -> Lic.type_ -> Lic.type_ -> t) = and (unify_do_acc: t -> Lic.type_ -> Lic.type_ -> t) =
fun acc te1 te2 -> fun acc te1 te2 ->
match acc, unify_type_eff te1 te2 with match acc, unify_type_eff te1 te2 with
| Equal, Equal -> Equal | Equal, Equal -> Equal
| Ko msg, _ | Ko msg, _
| _, Ko msg -> Ko msg | _, Ko msg -> Ko msg
| Unif t, Equal | Unif t, Equal
| Equal, Unif t -> Unif t | Equal, Unif t -> Unif t
| Unif t1, Unif t2 -> if t1 = t2 then acc else | Unif t1, Unif t2 -> if t1 = t2 then acc else
Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^ Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
" are not unifiable") " are not unifiable")
in in
Verbose.printf ~flag:dbg let l1_str = Lic.string_of_type_list l1 in
"#DBG: UnifyType.f (%s) with (%s) \n" let l2_str = Lic.string_of_type_list l2 in
(Lic.string_of_type_list l1)
(Lic.string_of_type_list l2); Verbose.printf ~flag:dbg "#DBG: UnifyType.f (%s) with (%s) \n" l1_str l2_str;
assert (List.length l1 = List.length l2); if (List.length l1 <> List.length l2) then
let res = List.fold_left2 unify_do_acc Equal l1 l2 in Ko("\n** "^ l1_str ^ " and " ^ l2_str ^ " are not unifiable (bad arity)")
Verbose.printf ~flag:dbg else
"#DBG: UnifyType.f (%s) with (%s) gives %s\n" let res = List.fold_left2 unify_do_acc Equal l1 l2 in
(Lic.string_of_type_list l1) Verbose.printf ~flag:dbg
(Lic.string_of_type_list l2) "#DBG: UnifyType.f (%s) with (%s) gives %s\n"
(string_of_t res); (Lic.string_of_type_list l1)
res (Lic.string_of_type_list l2)
(string_of_t res);
res
(****** MATCH ASSYMETRIQUE (****** MATCH ASSYMETRIQUE
On le fait avec un fold_left2 On le fait avec un fold_left2
......
test/lus2lic.sum
+ 11
− 6
View file @ 53e5bb83
Test Run By jahier on Fri May 31 11:27:00 2013 Test Run By jahier on Fri May 31 15:50:19 2013
Native configuration is i686-pc-linux-gnu Native configuration is i686-pc-linux-gnu
=== lus2lic tests === === lus2lic tests ===
...@@ -145,8 +145,10 @@ PASS: ./lus2lic {-o /tmp/predefOp.lic should_work/predefOp.lus} ...@@ -145,8 +145,10 @@ PASS: ./lus2lic {-o /tmp/predefOp.lic should_work/predefOp.lus}
PASS: ./lus2lic {-ec -o /tmp/predefOp.ec should_work/predefOp.lus} PASS: ./lus2lic {-ec -o /tmp/predefOp.ec should_work/predefOp.lus}
PASS: ./myec2c {-o /tmp/predefOp.c /tmp/predefOp.ec} PASS: ./myec2c {-o /tmp/predefOp.c /tmp/predefOp.ec}
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/predefOp.lus FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/predefOp.lus
FAIL: without any option: ./lus2lic {-o /tmp/t1.lic should_work/t1.lus} PASS: ./lus2lic {-o /tmp/t1.lic should_work/t1.lus}
FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/t1.ec should_work/t1.lus} PASS: ./lus2lic {-ec -o /tmp/t1.ec should_work/t1.lus}
PASS: ./myec2c {-o /tmp/t1.c /tmp/t1.ec}
PASS: ../utils/test_lus2lic_no_node should_work/t1.lus
PASS: ./lus2lic {-o /tmp/nc9.lic should_work/nc9.lus} PASS: ./lus2lic {-o /tmp/nc9.lic should_work/nc9.lus}
PASS: ./lus2lic {-ec -o /tmp/nc9.ec should_work/nc9.lus} PASS: ./lus2lic {-ec -o /tmp/nc9.ec should_work/nc9.lus}
PASS: ./myec2c {-o /tmp/nc9.c /tmp/nc9.ec} PASS: ./myec2c {-o /tmp/nc9.c /tmp/nc9.ec}
...@@ -982,6 +984,7 @@ XFAIL: Test bad programs (syntax): lus2lic {-o /tmp/old_style_and_pack.lic shoul ...@@ -982,6 +984,7 @@ XFAIL: Test bad programs (syntax): lus2lic {-o /tmp/old_style_and_pack.lic shoul
XFAIL: Test bad programs (syntax): lus2lic {-o /tmp/record.lic should_fail/syntax/record.lus} XFAIL: Test bad programs (syntax): lus2lic {-o /tmp/record.lic should_fail/syntax/record.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/parametric_node3.lic should_fail/type/parametric_node3.lus} XFAIL: Test bad programs (type): lus2lic {-o /tmp/parametric_node3.lic should_fail/type/parametric_node3.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/parametric_node.lic should_fail/type/parametric_node.lus} XFAIL: Test bad programs (type): lus2lic {-o /tmp/parametric_node.lic should_fail/type/parametric_node.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/t1.lic should_fail/type/t1.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/merge_bad_enum.lic should_fail/type/merge_bad_enum.lus} XFAIL: Test bad programs (type): lus2lic {-o /tmp/merge_bad_enum.lic should_fail/type/merge_bad_enum.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/condact2.lic should_fail/type/condact2.lus} XFAIL: Test bad programs (type): lus2lic {-o /tmp/condact2.lic should_fail/type/condact2.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/merge_bad_type.lic should_fail/type/merge_bad_type.lus} XFAIL: Test bad programs (type): lus2lic {-o /tmp/merge_bad_type.lic should_fail/type/merge_bad_type.lus}
...@@ -1039,8 +1042,10 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman ...@@ -1039,8 +1042,10 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
=== lus2lic Summary === === lus2lic Summary ===
# of expected passes 879 # of expected passes 883
# of unexpected failures 87 # of unexpected failures 85
# of unexpected successes 12 # of unexpected successes 12
# of expected failures 37 # of expected failures 38
# of unresolved testcases 12 # of unresolved testcases 12
testcase ./lus2lic.tests/non-reg.exp completed in 217 seconds
testcase ./lus2lic.tests/progression.exp completed in 1 seconds
test/lus2lic.time
+ 2
− 2
View file @ 53e5bb83
testcase ./lus2lic.tests/non-reg.exp completed in 210 seconds testcase ./lus2lic.tests/non-reg.exp completed in 217 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds testcase ./lus2lic.tests/progression.exp completed in 1 seconds
test/should_fail/type/t1.lus 0 → 100644
+ 44
− 0
View file @ 53e5bb83
node consensus << const n : int >>
( T : bool^n) returns ( a : bool);
let
a = with (n = 1)
then T[0]
else T[0] and consensus << n-1 >> (T[1..n-1]);
tel
(*
Et pourquoi pas tendre la notion de params statiques ???
*)
node consensus4 = consensus<<4>>;
node fold_left <<
type t1;
type t2;
const n : int;
node treat (x:t1; y:t2) returns (z:t1)
>>
(a : t1; X : t2^n) returns (c : t1);
let
c = with (n = 1) then a
else
fold_left << t1, t2, n-1, treat >> (
treat(a, X[0]),
X[1..n-1]
);
tel
node bt_void<<const n: int>>(t : bool^n) returns (x : bool);
let
x = fold_left<<Lustre::or>>(false, t);
tel
(* il manque un argument boolean a ce noeud... *)
node bt_void_bis<<const n: int>>(t : bool^n) returns (o: bool) =
fold_left<<bool,bool,n,Lustre::or>>;
node t1 = bt_void_bis<<8>>
(* node bt_void(t : bool array) = fold<<operator or>>(false, t); *)
test/should_work/t1.lus
+ 3
− 7
View file @ 53e5bb83
...@@ -19,12 +19,8 @@ node fold_left << ...@@ -19,12 +19,8 @@ node fold_left <<
type t2; type t2;
const n : int; const n : int;
node treat (x:t1; y:t2) returns (z:t1) node treat (x:t1; y:t2) returns (z:t1)
>> >>
( (a : t1; X : t2^n) returns (c : t1);
a : t1; X : t2^n
) returns (
c : t1
);
let let
c = with (n = 1) then a c = with (n = 1) then a
else else
...@@ -40,7 +36,7 @@ let ...@@ -40,7 +36,7 @@ let
tel tel
(* devrait marcher ? *) (* devrait marcher ? *)
node bt_void_bis<<const n: int>>(t : bool^n) returns (o: bool) = node bt_void_bis<<const n: int>>(i : bool; t : bool^n) returns (o: bool) =
fold_left<<bool,bool,n,Lustre::or>>; fold_left<<bool,bool,n,Lustre::or>>;
node t1 = bt_void_bis<<8>> node t1 = bt_void_bis<<8>>
......
todo.org
+ 5
− 22
View file @ 53e5bb83
...@@ -3,37 +3,20 @@ ...@@ -3,37 +3,20 @@
* lus2lic -exec * lus2lic -exec
** oops: lus2lic internal error ** TODO Extern node not yet supported
File "objlinux/data.ml", line 114, column 15
when compiling lustre program should_work/left.lus
./lus2lic should_work/left.lus -exec oops: lus2lic internal error
** TODO oops: lus2lic internal error
- State "TODO" from "" [2013-05-10 Fri 18:05]
File "objlinux/lic2soc.ml", line 680, column 18
when compiling lustre program should_work/left.lus
** TODO oops: lus2lic internal error
- State "TODO" from "" [2013-05-13 Mon 08:11] - State "TODO" from "" [2013-05-13 Mon 08:11]
../utils/test_lus2lic_no_node should_work/decl.lus
File "objlinux/lic2soc.ml", line 870, column 14 File "objlinux/lic2soc.ml", line 870, column 14
when compiling lustre program should_work/decl.lus when compiling lustre program should_work/decl.lus
../utils/test_lus2lic_no_node should_work/decl.lus
** TODO oops: lus2lic internal error ../utils/test_lus2lic_no_node should_work/simple.lus
- State "TODO" from "" [2013-05-14 Tue 14:35]
File "objlinux/socExec.ml", line 202, column 22 File "objlinux/socExec.ml", line 202, column 22
when compiling lustre program should_work/simple.lus when compiling lustre program should_work/simple.lus
../utils/test_lus2lic_no_node should_work/simple.lus
** TODO internal error
- State "TODO" from "" [2013-05-10 Fri 17:19]
File "objlinux/unifyType.ml", line 106, column 3
../utils/test_lus2lic_no_node should_work/t1.lus
** pb gen-autotest ** pb gen-autotest
../utils/test_lus2lic_no_node should_work/plus.lus ../utils/test_lus2lic_no_node should_work/plus.lus
+ ./lus2lic _plus_oracle.lus -n plus_oracle -lv4 -eei -en --no-prefix -o lv4_plus_oracle.lus + ./lus2lic _plus_oracle.lus -n plus_oracle -lv4 -eei -en --no-prefix -o lv4_plus_oracle.lus
......
todo.org_archive
+ 55
− 0
View file @ 53e5bb83
...@@ -763,6 +763,61 @@ Bon, finalement, j'oblige les gens a ecrire Lustre::gt et puis ca marre. ...@@ -763,6 +763,61 @@ Bon, finalement, j'oblige les gens a ecrire Lustre::gt et puis ca marre.
:END: :END:
./lus2lic _ck5_oracle.lus -n ck5_oracle -en ./lus2lic _ck5_oracle.lus -n ck5_oracle -en
* oops: lus2lic internal error
:PROPERTIES:
:ARCHIVE_TIME: 2013-05-31 Fri 13:55
:ARCHIVE_FILE: ~/lus2lic/todo.org
:ARCHIVE_OLPATH: lus2lic -exec
:ARCHIVE_CATEGORY: lv6
:END:
File "objlinux/data.ml", line 114, column 15
when compiling lustre program should_work/left.lus
./lus2lic should_work/left.lus -exec
* oops: lus2lic internal error
:PROPERTIES:
:ARCHIVE_TIME: 2013-05-31 Fri 13:56
:ARCHIVE_FILE: ~/lus2lic/todo.org
:ARCHIVE_OLPATH: lus2lic -exec
:ARCHIVE_CATEGORY: lv6
:END:
File "objlinux/data.ml", line 114, column 15
when compiling lustre program should_work/left.lus
./lus2lic should_work/left.lus -exec
* TODO oops: lus2lic internal error
- State "TODO" from "" [2013-05-10 Fri 18:05]
:PROPERTIES:
:ARCHIVE_TIME: 2013-05-31 Fri 13:56
:ARCHIVE_FILE: ~/lus2lic/todo.org
:ARCHIVE_OLPATH: lus2lic -exec
:ARCHIVE_CATEGORY: lv6
:ARCHIVE_TODO: TODO
:END:
File "objlinux/lic2soc.ml", line 680, column 18
when compiling lustre program should_work/left.lus
* TODO internal error
- State "TODO" from "" [2013-05-10 Fri 17:19]
:PROPERTIES:
:ARCHIVE_TIME: 2013-05-31 Fri 15:52
:ARCHIVE_FILE: ~/lus2lic/todo.org
:ARCHIVE_OLPATH: lus2lic -exec
:ARCHIVE_CATEGORY: lv6
:ARCHIVE_TODO: TODO
:END:
File "objlinux/unifyType.ml", line 106, column 3
../utils/test_lus2lic_no_node should_work/t1.lus
file:src/unifyType.ml::110
......
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