Extend the non-reg test with a lurette-based comparison of the -exec and -ec modes.

112 tests failed, and 127 passed !!

src/main.ml

-(* Time-stamp: <modified the 17/04/2013 (at 11:19) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/04/2013 (at 13:53) by Erwan Jahier> *)
 
 open Verbose
 open AstV6
@@ -20,49 +20,83 @@ let rec first_pack_in =
     | (AstV6.NSModel _)::tail -> first_pack_in tail
     | [] -> raise (Global_error "No package has been provided")
 
-let (gen_lutin : LicPrg.t -> Ident.idref option -> unit) =
-  fun lic_prg main_node  -> 
-    (match main_node with
-      | None -> (print_string "No node is specified\n"; flush stdout)
-      | Some main_node -> 
-        let msk, zesoc = Lic2soc.f lic_prg (Lic.node_key_of_idref main_node) in
-        let soc = try Soc.SocMap.find msk zesoc with Not_found -> assert false in
-        let invars,outvars=soc.Soc.profile in
-        let invars = SocExec.expand_profile invars in
-        let outvars = SocExec.expand_profile outvars in
-        let invars_str  = List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) invars in
-        let outvars_str = List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) outvars in
-        let name = main_node.Ident.id_id in
-        let lutin_file_name = ("_"^name^"_env.lut") in
-        let oc = open_out lutin_file_name in
-        Lv6util.dump_entete oc; 
-        output_string oc ("node " ^ (name) ^ "_env("^ (String.concat ";" outvars_str) ^ 
+(* try to use the filenale to guess the dft node *)
+let find_a_node opt =
+  let first_file = List.hd opt.infiles in
+  let name = 
+    try Filename.chop_extension (Filename.basename first_file) 
+    with _ -> 
+		print_string ("*** '"^first_file^"': bad file name.\n"); exit 1
+  in
+  name
+
+
+(* Generates a lutin env and a lustre oracle for the node *)
+let (gen_autotest_files : LicPrg.t -> Ident.idref option -> Lv6MainArgs.t -> unit) =
+  fun lic_prg main_node opt -> 
+    let msk, zesoc, main_node = 
+      match main_node with
+        | None -> (
+          let name = find_a_node opt in
+          let main_node = Ident.to_idref name in
+          let nk = (Lic.node_key_of_idref main_node) in
+          if LicPrg.node_exists lic_prg nk then (
+            output_string stdout ("WARNING: No main node is specified. I'll try with " ^ name ^"\n");
+            flush stdout;
+            let msk, zesoc = Lic2soc.f lic_prg nk in
+            msk, zesoc, main_node
+          ) else (
+            print_string ("Error: no node is specified, cannot exec.\n");
+            flush stdout;
+            exit 1
+          )
+        )
+        | Some main_node -> 
+          let msk, zesoc = Lic2soc.f lic_prg (Lic.node_key_of_idref main_node) in
+          msk, zesoc, main_node
+    in
+    let soc = try Soc.SocMap.find msk zesoc with Not_found -> assert false in
+    let invars,outvars=soc.Soc.profile in
+    let invars = SocExec.expand_profile invars in
+    let outvars = SocExec.expand_profile outvars in
+    let invars_str  = List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) invars in
+    let outvars_str = List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) outvars in
+    let name = main_node.Ident.id_id in
+    let lutin_file_name = ("_"^name^"_env.lut") in
+    let oc = open_out lutin_file_name in
+    Lv6util.dump_entete oc; 
+    output_string oc ("node " ^ (name) ^ "_env("^ (String.concat ";" outvars_str) ^ 
                          ") returns(" ^ (String.concat ";" invars_str) ^ ") =\n   loop true \n");
-        flush oc; 
-        close_out oc;
-        output_string stdout (lutin_file_name ^" generated.\n"); 
-        
-        let oracle_file_name = ("_"^name^"_oracle.lus") in
-        let oc = open_out oracle_file_name in
-        let locals = List.map (fun (n,t) -> n^"_bis",t) outvars in
-        let prg = "node "^name^"_oracle("^(String.concat ";" (invars_str@outvars_str)) in
-        let prg = prg ^") returns(ok:bool);\n" in
-        let locals_str = List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) locals in
-        let prg = prg ^ "var\n  " ^ (String.concat ";\n  " locals_str) ^ ";\nlet\n" in
-        let locals_name  = List.map fst locals in
-        let invars_name  = List.map fst invars in
-        let outvars_name = List.map fst outvars in
-        let prg = prg^"  ("^(String.concat "," locals_name)^") = "^name in
-        let prg = prg^"("^(String.concat "," invars_name)^");\n" in
-        let prg = prg^"  ok = ("^ (String.concat "," outvars_name) ^ "=" in
-        let prg = prg^ (String.concat "," locals_name) ^ ");\ntel;\n"  in
-        Lv6util.dump_entete oc; 
-        output_string oc prg;
-        flush oc; 
-        close_out oc;
-        output_string stdout (oracle_file_name ^" generated.\n"); 
-        flush stdout
-    )
+    flush oc; 
+    close_out oc;
+    output_string stdout (lutin_file_name ^" generated.\n"); 
+    
+    let oracle_file_name = ("_"^name^"_oracle.lus") in
+    let oc = open_out oracle_file_name in
+    let locals = List.map (fun (n,t) -> n^"_bis",t) outvars in
+    let prg = "node "^name^"_oracle("^(String.concat ";" (invars_str@outvars_str)) in
+    let locals_str = List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) locals in
+    let ok = (* avoid name clash*)
+      let all_vars = List.map fst (List.rev_append (List.rev_append locals invars) outvars) in
+      let rec gen_ok str = if List.mem str all_vars then gen_ok ("_"^str) else str in
+      gen_ok "ok" 
+    in 
+    let prg = prg ^") returns("^ok^":bool;"^(String.concat ";" locals_str)^");\nlet\n" in
+    let locals_name  = List.map fst locals in
+    let invars_name  = List.map fst invars in
+    let outvars_name = List.map fst outvars in
+    let prg = prg^"  ("^(String.concat "," locals_name)^") = "^name in
+    let prg = prg^"("^(String.concat "," invars_name)^");\n  "^ok^" = (" in
+    let prg = prg^(String.concat " and\n \t\t  " (List.map2 (fun x y -> x^"="^y)
+                                           outvars_name locals_name)) ^ ");\ntel;\n"  
+    in
+    Lv6util.dump_entete oc; 
+    output_string oc prg;
+    flush oc; 
+    close_out oc;
+    output_string stdout (oracle_file_name ^" generated.\n"); 
+    flush stdout
+
 
 let main  = (
   (* Compile.init_appli () ; *)
@@ -91,16 +125,11 @@ let main  = (
     let nsl = Compile.get_source_list opt opt.infiles in
     let lic_prg = Compile.doit opt nsl main_node in
     if opt.Lv6MainArgs.gen_autotest then 
-      gen_lutin lic_prg main_node
+      gen_autotest_files lic_prg main_node opt
     else if opt.exec then
       (match main_node with
         | None -> (
-          let first_file = List.hd opt.infiles in
-          let name = 
-            try Filename.chop_extension (Filename.basename first_file) 
-            with _ -> 
-		        print_string ("*** '"^first_file^"': bad file name.\n"); exit 1
-          in
+          let name = find_a_node opt in
           let nk = (Lic.node_key_of_idref (Ident.to_idref name)) in
           if LicPrg.node_exists lic_prg nk then (
             print_string ("WARNING: No main node is specified. I'll try with " ^ name ^"\n");

test/Makefile

@@ -36,5 +36,7 @@ nonreg:
 prog:
 	ssh triglav "cd  $(testdir) ; runtest --all 	--tool lus2lic --ignore non-reg.exp" || true
 
+clean:
+	rm -f *.ec *.lus *.lut *.cov *.gp *.rif *.out 
 
 

test/lus2lic.tests/non-reg.exp

@@ -18,6 +18,9 @@ foreach f $ok_files {
         set id3 [should_work "Try ec2c on the result" "$ec2c" "-o $bf.c $bf.ec"]
         wait -i $id3
     }
+    if { [emptyfile "$bf.c"] } {
+        set id4 [should_work "Try to compare lus2lic -exec and ecexe" "$test_lus2lic_no_node" "$f"]
+    }
 }
 
 

test/lus2lic.time

-testcase ./lus2lic.tests/non-reg.exp completed in 60 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 62 seconds
 testcase ./lus2lic.tests/progression.exp completed in 0 seconds

test/site.exp

 set lus2lic "./lus2lic"
 set ec2c "./ec2c"
-
+set ec2c "./ec2c"
+set test_lus2lic_no_node "../utils/test_lus2lic_no_node"
 proc should_work { test_name command_line args } {
     global verbose
 
@@ -45,6 +46,9 @@ proc should_work { test_name command_line args } {
             set failed 1
             exp_continue
         }
+        "lurettetop: bye!" {
+            pass "$cl $args"
+        }
         # to avoid that match_max (the expect buffer size) is reached 
         # which truncate the outputs
         "\n" {

todo.org

@@ -14,12 +14,43 @@ que de lancer luciole
 
 Un truc de ce gout là semble fonctionner :
 
+
+ ./lus2lic  _trivial3_condact_oracle.lus -n trivial3_condact_oracle -ec > trivial3_condact_oracl
+
+
 ./lus2lic trivial3.lus -n trivial3_condact --gen-autotest
- ./lus2lic trivial3.lus -n trivial3_condact -ec >> _trivial3_condact_oracle.lus
- ~/lurette/bin/lurettetop -rp "sut:v6:trivial3.lus:trivial3_condact" -rp "env:lutin:_trivial3_condact_env.lut" -rp "oracle:ec:trivial3_condact_oracle.ec:"
+./lus2lic trivial3.lus -n trivial3_condact -ec >> _trivial3_condact_oracle.lus
+./lus2lic  _trivial3_condact_oracle.lus -n trivial3_condact_oracle -ec > trivial3_condact_oracle.ec
+~/lurette/bin/lurettetop -rp "sut:v6:trivial3.lus:trivial3_condact" -rp "env:lutin:_trivial3_condact_env.lut" -rp "oracle:ec:trivial3_condact_oracle.ec:" -go 
 
 Reste à l'integrer dans file:test/lus2lic.tests/non-reg.exp
 
+** TODO ce noeud ne compile pas en mode -ec
+   - State "TODO"       from ""           [2013-04-17 Wed 15:51]
+
+#+begin_src lustre
+node trivial3(e: int ^2) returns (x: int ^6);
+var
+  c: int ^6;
+let
+  c = e|e|e;
+  x[0..2] = c[3..5];
+  x[3..5] = c[0..2];
+ 
+tel
+#+end_src
+
+** TODO msg d'erreur un peu mavais sur ce programme
+
+#+begin_src lustre
+node argos_oracle(a:bool;b:bool;s0:bool;s1:bool;s2:bool) returns(ok:bool;s0_bis:bool;s1_bis:bool;s2_bis:bool);
+let
+  (s0_bis,s1_bis,s2_bis) = argos(a,b);
+s0=s0_bis;
+  s1=s1_bis;
+  s2=s2_bis;
+tel;
+#+end_src
 
 ** TODO Écrire un test qui mette en jeu exhaustivement tous les operateurs
    - State "TODO"       from ""           [2013-03-19 Tue 10:38]

utils/test_lus2lic

+#!/bin/sh
+
+lustre_file=$1
+node=$2
+_oracle=_"$node"_oracle.lus
+oracle="$node"_oracle
+env=_"$node"_env.lut
+
+echo "LAUCHING ./lus2lic $lustre_file -n $node --gen-autotest"
+./lus2lic                $lustre_file -n $node --gen-autotest
+
+echo "LAUCHING ./lus2lic $lustre_file -n $node -ec >> $_oracle"
+./lus2lic                $lustre_file -n $node -ec >> $_oracle
+
+echo "LAUCHING ./lus2lic  $_oracle -n $oracle -ec > $oracle.ec"
+./lus2lic                 $_oracle -n $oracle -ec > $oracle.ec
+
+echo "~/lurette/bin/lurettetop -rp \"sut:v6:$lustre_file:$node\" -rp \"env:lutin:$env\" -rp \"oracle:ec:$oracle.ec:\" -go -l 100 -ns2c"
+~/lurette/bin/lurettetop -rp "sut:v6:$lustre_file:$node" -rp "env:lutin:$env" -rp "oracle:ec:$oracle.ec:" -go -l 100 -ns2c

utils/test_lus2lic_no_node

+#!/bin/sh
+
+
+lustre_file=$1
+node=`basename $lustre_file .lus`
+_oracle=_"$node"_oracle.lus
+oracle="$node"_oracle
+env=_"$node"_env.lut
+
+set -x verbose #echo on
+
+./lus2lic $lustre_file -n $node --gen-autotest || exit 2
+./lus2lic $lustre_file -n $node -ec >> $_oracle || exit 2
+./lus2lic  $_oracle -n $oracle -ec -o $oracle.ec || exit 2
+./lurettetop -rp "sut:v6:$lustre_file:$node" -rp "env:lutin:$env" -rp "oracle:ec:$oracle.ec:$oracle" -go -l 10 -ns2c --stop-on-oracle-error || exit 2
+
+return 0