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

Change the nonreg test scheme by inverting the role of v4 and v6 in the sut and the oracle. 

The rationale is to avoid local vars blow-up on some
examples. Indeed, the generated oracle blows-up (e.g., on left.lus)
if we execute it via v4, whereas via v6 it works fine.

This change triggers a couple of bugs that ware easy to fix
(confusion between div and slash) that I've fixed along the way.
For the others, I'll see later.

Overall it's a progress albeit
  #fail: 80 -> 83

indeed:
  #unresolved: 20 -> 12
  #passes		878 -> 883
  time: 335 -> 228
parent bbc7931a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/astPredef.ml
+ 4
− 4
View file @ 06ddb863
(* Time-stamp: <modified the 26/03/2013 (at 15:35) by Erwan Jahier> *)
(* Time-stamp: <modified the 28/05/2013 (at 10:47) by Erwan Jahier> *)
(** Predefined operators Type definition *)
......@@ -126,17 +126,17 @@ let op2string_long = function
| UMINUS_n -> "uminus"
| MINUS_n -> "minus"
| PLUS_n -> "plus"
| SLASH_n -> "div"
| SLASH_n -> "slash"
| TIMES_n -> "times"
| IUMINUS_n -> "iuminus"
| IMINUS_n -> "iminus"
| IPLUS_n -> "iplus"
| ISLASH_n -> "idiv"
| ISLASH_n -> "islash"
| ITIMES_n -> "itimes"
| RUMINUS_n -> "ruminus"
| RMINUS_n -> "rminus"
| RPLUS_n -> "rplus"
| RSLASH_n -> "rdiv"
| RSLASH_n -> "rslash"
| RTIMES_n -> "rtimes"
| op -> op2string op
......
src/data.ml
+ 2
− 1
View file @ 06ddb863
......@@ -111,7 +111,8 @@ let rec (update_val : v -> v -> access list -> v) =
S (List.map
(fun (fn2,v2) -> if fn=fn2 then fn,update_val v2 v access else (fn2,v2))
fl)
| _,_ -> assert false (* finish me (field struct) *)
| U,_ -> assert false (* finish me *)
| _,_ -> assert false (* finish me *)
(* exported *)
......
src/licDump.ml
+ 1
− 1
View file @ 06ddb863
(* Time-stamp: <modified the 15/05/2013 (at 09:48) by Erwan Jahier> *)
(* Time-stamp: <modified the 28/05/2013 (at 10:42) by Erwan Jahier> *)
open Lv6errors
open Printf
......
src/rif_base.ml
+ 2
− 2
View file @ 06ddb863
......@@ -159,8 +159,8 @@ and (parse_rif_stream : in_channel -> out_channel option -> vntl -> stream ->
parse_rif_stream ic oc
vntl (get_stream ic oc) tbl pragma
)
| (Genlex.Kwd (_,"#"))::(Genlex.Kwd (_,"ERROR"))::_ ->
print_string "#ERROR value read. bye!\n"; raise Bye
| (Genlex.Kwd (_,"#"))::(Genlex.Kwd (_,"ERROR"))::_ ->
print_string "#ERROR value read. bye!\n"; raise Bye
| (Genlex.Kwd (_,"#"))::_ ->
Stream.junk stream ;
parse_rif_stream ic oc vntl (get_stream ic oc)
......
src/socExecEvalPredef.ml
+ 12
− 1
View file @ 06ddb863
(* Time-stamp: <modified the 10/05/2013 (at 16:21) by Erwan Jahier> *)
(* Time-stamp: <modified the 28/05/2013 (at 15:03) by Erwan Jahier> *)
open SocExecValue
open Data
......@@ -39,6 +39,16 @@ let lustre_div ctx =
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_slash ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2)
| [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_minus ctx =
let (vn,vv) =
......@@ -306,6 +316,7 @@ let (get: Soc.key -> (ctx -> ctx)) =
| "Lustre::idiv"
| "Lustre::rdiv"
| "Lustre::div" -> lustre_div
| "Lustre::slash" | "Lustre::islash" | "Lustre::rslash" -> lustre_slash
| "Lustre::iminus"
| "Lustre::rminus"
| "Lustre::minus"-> lustre_minus
......
src/socPredef.ml
+ 2
− 1
View file @ 06ddb863
(* Time-stamp: <modified the 17/05/2013 (at 17:44) by Erwan Jahier> *)
(* Time-stamp: <modified the 28/05/2013 (at 10:48) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
......@@ -124,6 +124,7 @@ let of_soc_key : Soc.key -> Soc.t =
| "Lustre::iplus"
| "Lustre::plus" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::times" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::slash" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::div" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::minus" -> (make_soc sk (sp tl) [step21 None])
......
test/lus2lic.sum
+ 20
− 20
View file @ 06ddb863
Test Run By jahier on Tue May 28 08:35:55 2013
Test Run By jahier on Tue May 28 15:04:10 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
......@@ -28,7 +28,7 @@ UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/assertion.lus
PASS: ./lus2lic {-o /tmp/normal.lic should_work/normal.lus}
PASS: ./lus2lic {-ec -o /tmp/normal.ec should_work/normal.lus}
PASS: ./ec2c {-o /tmp/normal.c /tmp/normal.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/normal.lus
PASS: ../utils/test_lus2lic_no_node should_work/normal.lus
PASS: ./lus2lic {-o /tmp/nodeparam.lic should_work/nodeparam.lus}
PASS: ./lus2lic {-ec -o /tmp/nodeparam.ec should_work/nodeparam.lus}
PASS: ./ec2c {-o /tmp/nodeparam.c /tmp/nodeparam.ec}
......@@ -36,7 +36,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/nodeparam.lus
PASS: ./lus2lic {-o /tmp/enum0.lic should_work/enum0.lus}
PASS: ./lus2lic {-ec -o /tmp/enum0.ec should_work/enum0.lus}
PASS: ./ec2c {-o /tmp/enum0.c /tmp/enum0.ec}
PASS: ../utils/test_lus2lic_no_node should_work/enum0.lus
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/enum0.lus
PASS: ./lus2lic {-o /tmp/ck6.lic should_work/ck6.lus}
PASS: ./lus2lic {-ec -o /tmp/ck6.ec should_work/ck6.lus}
PASS: ./ec2c {-o /tmp/ck6.c /tmp/ck6.ec}
......@@ -56,7 +56,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/dep.lus
PASS: ./lus2lic {-o /tmp/ELMU.lic should_work/ELMU.lus}
PASS: ./lus2lic {-ec -o /tmp/ELMU.ec should_work/ELMU.lus}
PASS: ./ec2c {-o /tmp/ELMU.c /tmp/ELMU.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/ELMU.lus
PASS: ../utils/test_lus2lic_no_node should_work/ELMU.lus
PASS: ./lus2lic {-o /tmp/testPilote.lic should_work/testPilote.lus}
PASS: ./lus2lic {-ec -o /tmp/testPilote.ec should_work/testPilote.lus}
PASS: ./ec2c {-o /tmp/testPilote.c /tmp/testPilote.ec}
......@@ -170,7 +170,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/mm1.lus
PASS: ./lus2lic {-o /tmp/predef03.lic should_work/predef03.lus}
PASS: ./lus2lic {-ec -o /tmp/predef03.ec should_work/predef03.lus}
PASS: ./ec2c {-o /tmp/predef03.c /tmp/predef03.ec}
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/predef03.lus
PASS: ../utils/test_lus2lic_no_node should_work/predef03.lus
PASS: ./lus2lic {-o /tmp/iter.lic should_work/iter.lus}
PASS: ./lus2lic {-ec -o /tmp/iter.ec should_work/iter.lus}
PASS: ./ec2c {-o /tmp/iter.c /tmp/iter.ec}
......@@ -272,7 +272,7 @@ UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/alarme.lus
PASS: ./lus2lic {-o /tmp/onlyroll2.lic should_work/onlyroll2.lus}
PASS: ./lus2lic {-ec -o /tmp/onlyroll2.ec should_work/onlyroll2.lus}
PASS: ./ec2c {-o /tmp/onlyroll2.c /tmp/onlyroll2.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/onlyroll2.lus
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/onlyroll2.lus
PASS: ./lus2lic {-o /tmp/X6.lic should_work/X6.lus}
PASS: ./lus2lic {-ec -o /tmp/X6.ec should_work/X6.lus}
PASS: ./ec2c {-o /tmp/X6.c /tmp/X6.ec}
......@@ -352,7 +352,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou
PASS: ./lus2lic {-o /tmp/sincos.lic should_work/sincos.lus}
PASS: ./lus2lic {-ec -o /tmp/sincos.ec should_work/sincos.lus}
PASS: ./ec2c {-o /tmp/sincos.c /tmp/sincos.ec}
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/sincos.lus
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/sincos.lus
PASS: ./lus2lic {-o /tmp/newpacks.lic should_work/newpacks.lus}
PASS: ./lus2lic {-ec -o /tmp/newpacks.ec should_work/newpacks.lus}
PASS: ./ec2c {-o /tmp/newpacks.c /tmp/newpacks.ec}
......@@ -364,7 +364,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/morel5.lus
PASS: ./lus2lic {-o /tmp/bred.lic should_work/bred.lus}
PASS: ./lus2lic {-ec -o /tmp/bred.ec should_work/bred.lus}
PASS: ./ec2c {-o /tmp/bred.c /tmp/bred.ec}
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/bred.lus
PASS: ../utils/test_lus2lic_no_node should_work/bred.lus
PASS: ./lus2lic {-o /tmp/tri.lic should_work/tri.lus}
PASS: ./lus2lic {-ec -o /tmp/tri.ec should_work/tri.lus}
PASS: ./ec2c {-o /tmp/tri.c /tmp/tri.ec}
......@@ -403,7 +403,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/bad_call03.lus
PASS: ./lus2lic {-o /tmp/onlyroll.lic should_work/onlyroll.lus}
PASS: ./lus2lic {-ec -o /tmp/onlyroll.ec should_work/onlyroll.lus}
PASS: ./ec2c {-o /tmp/onlyroll.c /tmp/onlyroll.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/onlyroll.lus
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/onlyroll.lus
PASS: ./lus2lic {-o /tmp/produitBool.lic should_work/produitBool.lus}
PASS: ./lus2lic {-ec -o /tmp/produitBool.ec should_work/produitBool.lus}
PASS: ./ec2c {-o /tmp/produitBool.c /tmp/produitBool.ec}
......@@ -431,7 +431,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/mapinf.lus
PASS: ./lus2lic {-o /tmp/integrator.lic should_work/integrator.lus}
PASS: ./lus2lic {-ec -o /tmp/integrator.ec should_work/integrator.lus}
PASS: ./ec2c {-o /tmp/integrator.c /tmp/integrator.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/integrator.lus
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/integrator.lus
PASS: ./lus2lic {-o /tmp/nc4.lic should_work/nc4.lus}
PASS: ./lus2lic {-ec -o /tmp/nc4.ec should_work/nc4.lus}
PASS: ./ec2c {-o /tmp/nc4.c /tmp/nc4.ec}
......@@ -443,7 +443,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/mm3.lus
PASS: ./lus2lic {-o /tmp/over2.lic should_work/over2.lus}
PASS: ./lus2lic {-ec -o /tmp/over2.ec should_work/over2.lus}
PASS: ./ec2c {-o /tmp/over2.c /tmp/over2.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/over2.lus
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/over2.lus
PASS: ./lus2lic {-o /tmp/over3.lic should_work/over3.lus}
PASS: ./lus2lic {-ec -o /tmp/over3.ec should_work/over3.lus}
PASS: ./ec2c {-o /tmp/over3.c /tmp/over3.ec}
......@@ -523,7 +523,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou
PASS: ./lus2lic {-o /tmp/test_enum.lic should_work/test_enum.lus}
PASS: ./lus2lic {-ec -o /tmp/test_enum.ec should_work/test_enum.lus}
PASS: ./ec2c {-o /tmp/test_enum.c /tmp/test_enum.ec}
PASS: ../utils/test_lus2lic_no_node should_work/test_enum.lus
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/test_enum.lus
PASS: ./lus2lic {-o /tmp/predef01.lic should_work/predef01.lus}
PASS: ./lus2lic {-ec -o /tmp/predef01.ec should_work/predef01.lus}
PASS: ./ec2c {-o /tmp/predef01.c /tmp/predef01.ec}
......@@ -539,7 +539,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou
PASS: ./lus2lic {-o /tmp/left.lic should_work/left.lus}
PASS: ./lus2lic {-ec -o /tmp/left.ec should_work/left.lus}
PASS: ./ec2c {-o /tmp/left.c /tmp/left.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/left.lus
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/left.lus
PASS: ./lus2lic {-o /tmp/ts04.lic should_work/ts04.lus}
PASS: ./lus2lic {-ec -o /tmp/ts04.ec should_work/ts04.lus}
PASS: ./ec2c {-o /tmp/ts04.c /tmp/ts04.ec}
......@@ -681,7 +681,7 @@ UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/aux1.lus
PASS: ./lus2lic {-o /tmp/moyenne.lic should_work/moyenne.lus}
PASS: ./lus2lic {-ec -o /tmp/moyenne.ec should_work/moyenne.lus}
PASS: ./ec2c {-o /tmp/moyenne.c /tmp/moyenne.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/moyenne.lus
PASS: ../utils/test_lus2lic_no_node should_work/moyenne.lus
PASS: ./lus2lic {-o /tmp/activation1.lic should_work/activation1.lus}
PASS: ./lus2lic {-ec -o /tmp/activation1.ec should_work/activation1.lus}
PASS: ./ec2c {-o /tmp/activation1.c /tmp/activation1.ec}
......@@ -725,7 +725,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/minmax4.lus
PASS: ./lus2lic {-o /tmp/nested.lic should_work/nested.lus}
PASS: ./lus2lic {-ec -o /tmp/nested.ec should_work/nested.lus}
PASS: ./ec2c {-o /tmp/nested.c /tmp/nested.ec}
UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/nested.lus
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/nested.lus
PASS: ./lus2lic {-o /tmp/Gyroscope.lic should_work/Gyroscope.lus}
PASS: ./lus2lic {-ec -o /tmp/Gyroscope.ec should_work/Gyroscope.lus}
PASS: ./ec2c {-o /tmp/Gyroscope.c /tmp/Gyroscope.ec}
......@@ -797,7 +797,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/X2.lus
PASS: ./lus2lic {-o /tmp/alias.lic should_work/alias.lus}
PASS: ./lus2lic {-ec -o /tmp/alias.ec should_work/alias.lus}
PASS: ./ec2c {-o /tmp/alias.c /tmp/alias.ec}
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/alias.lus
PASS: ../utils/test_lus2lic_no_node should_work/alias.lus
PASS: ./lus2lic {-o /tmp/hanane.lic should_work/hanane.lus}
PASS: ./lus2lic {-ec -o /tmp/hanane.ec should_work/hanane.lus}
PASS: ./ec2c {-o /tmp/hanane.c /tmp/hanane.ec}
......@@ -953,7 +953,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou
PASS: ./lus2lic {-o /tmp/bred_lv4.lic should_work/bred_lv4.lus}
PASS: ./lus2lic {-ec -o /tmp/bred_lv4.ec should_work/bred_lv4.lus}
PASS: ./ec2c {-o /tmp/bred_lv4.c /tmp/bred_lv4.ec}
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/bred_lv4.lus
PASS: ../utils/test_lus2lic_no_node should_work/bred_lv4.lus
PASS: ./lus2lic {-o /tmp/trivial2.lic should_work/trivial2.lus}
PASS: ./lus2lic {-ec -o /tmp/trivial2.ec should_work/trivial2.lus}
PASS: ./ec2c {-o /tmp/trivial2.c /tmp/trivial2.ec}
......@@ -1039,8 +1039,8 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
=== lus2lic Summary ===
# of expected passes 878
# of unexpected failures 80
# of expected passes 883
# of unexpected failures 83
# of unexpected successes 12
# of expected failures 37
# of unresolved testcases 20
# of unresolved testcases 12
test/lus2lic.time
+ 1
− 1
View file @ 06ddb863
testcase ./lus2lic.tests/non-reg.exp completed in 335 seconds
testcase ./lus2lic.tests/non-reg.exp completed in 228 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds
todo.org
+ 19
− 0
View file @ 06ddb863
......@@ -3,6 +3,12 @@
* lus2lic -exec
** oops: lus2lic internal error
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]
File "objlinux/lic2soc.ml", line 680, column 18
......@@ -53,6 +59,7 @@ et aussi :
../utils/test_lus2lic_no_node should_work/over2.lus
../utils/test_lus2lic_no_node should_work/mapiter.lus
../utils/test_lus2lic_no_node should_work/arrays.lus
../utils/test_lus2lic_no_node should_work/nested.lus
** TODO Lurette trouve un mismatch sur ce prog au step 1
- State "TODO" from "" [2013-05-10 Fri 17:08]
......@@ -129,6 +136,18 @@ file:test/should_fail/type/parametric_node.lus
* Testing process
** TODO Testing node with enums don't work
- State "TODO" from "" [2013-05-28 Tue 14:46]
indeed, ec requires they are extern const, and lus2lic requires to have int
- one solution would be that -eei generates correct ec, by inlining constant
- I could also add enums in Lutin
Actually, I should do both...
../utils/test_lus2lic_no_node should_work/enum0.lus
** TODO Écrire un test qui mette en jeu exhaustivement tous les operateurs
- State "TODO" from "" [2013-03-19 Tue 10:38]
** TODO try to compile the C code resulting from ec2c at some point
......
utils/test_lus2lic_no_node
+ 21
− 12
View file @ 06ddb863
......@@ -5,6 +5,9 @@ lustre_file=$1
node=`basename $lustre_file .lus`
_oracle=_"$node"_oracle.lus
oracle="$node"_oracle
lv4="$node"_lv4.lus
ec="$node".ec
lv4_node="$node__$node"
env=_"$node"_env.lut
set -x verbose #echo on
......@@ -24,7 +27,8 @@ cat $lustre_file >> $_oracle;
if
./lus2lic $_oracle -n $oracle -lv4 -eei -en --no-prefix -o lv4$_oracle;
./lus2lic $lustre_file -n $node -ec -o $ec;
# ./lus2lic $lustre_file -n $node -en -lv4 -eei --no-prefix -o $lv4;
then
echo "lus2lic -lv4 done"
else
......@@ -34,18 +38,23 @@ fi
export PATH=/usr/local/tools/lustre/bin/:$PATH
# if
# ./lus2lic $_oracle -n $oracle -ec -o $oracle.ec
# # ./lus2lic lv4$_oracle -n $oracle -ec -o $oracle.ec
# # lus2ec $_oracle $oracle -o $oracle.ec;
# then
# echo "ec generation done"
# else
# echo "Error"
# exit 2
# fi
if
# ./lus2lic $_oracle -n $oracle -ec -o $oracle.ec
./lus2lic lv4$_oracle -n $oracle -ec -o $oracle.ec
# lus2ec $_oracle $oracle -o $oracle.ec;
then
echo "ec generation done"
else
echo "Error"
exit 2
fi
if
./lurettetop -p 6 -v 1 -seed 42 -rp "sut:v6:$lustre_file:$node" -rp "env:lutin:$env" -rp "oracle:ec:$oracle.ec:$oracle" -go -l 10 -ns2c --stop-on-oracle-error;
# -rp "sut:v4:$lv4:$lv4_node" \
./lurettetop -p 6 -seed 42 \
-rp "sut:ec:$ec:$lv4_node" \
-rp "env:lutin:$env" \
-rp "oracle:v6:$_oracle:$oracle" \
-go -l 10 -ns2c --stop-on-oracle-error;
then
echo "lurettetop ok"
else
......
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