From d7dc94ef488b21601e641eedbcbf41bc03f918c6 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Fri, 22 May 2015 16:10:37 +0200
Subject: [PATCH] --gen-autotest: also generates an arocle to compare lustre
programs with lesar
+ the utils/lustrequiv script that tries to state that 2 nodes a equivalent or not
using lesar and lurette.
---
src/main.ml | 41 ++++++++++++++++++++++++--
utils/lustrequiv | 76 ++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 114 insertions(+), 3 deletions(-)
create mode 100755 utils/lustrequiv
diff --git a/src/main.ml b/src/main.ml
index 44d6a181..a35829a5 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/02/2015 (at 11:22) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/05/2015 (at 14:55) by Erwan Jahier> *)
open Verbose
open AstV6
@@ -148,7 +148,8 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni
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 prg = "-- oracle to compare Lustre compilers\n" ^ prg in
+ let prg = prg ^") \nreturns("^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 prg = prg^" ("^(String.concat "," locals_name)^") = "^name in
@@ -176,10 +177,44 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni
(List.flatten (List.map2 var_to_equals locals outvars))) ^");\ntel;\n"
with _ -> assert false
in
+ let prg = prg^"\n-- oracle to compare two programs \n" in
+ let prg = prg^"node "^name^"_oracle_prog("^(String.concat ";" (invars_str)) in
+ let prg = prg ^") \nreturns("^ok^":bool;"^(String.concat ";" locals_str) in
+ let prg = prg ^");\nvar\n"^(String.concat ";" outvars_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 "," outvars_name)^") = P1" in
+ let prg = prg^"("^(String.concat "," invars_name)^");\n" in
+ let prg = prg^" ("^(String.concat "," locals_name)^") = P2" in
+ let prg = prg^"("^(String.concat "," invars_name)^");\n "^ok^" = (" in
+ let (var_to_equals : Soc.var -> Soc.var -> string list) =
+ fun (x,t) (y,_) ->
+ let rec aux x y t =
+ match t with
+ | Data.Real -> ["r_equal("^x^","^y^")"]
+ | Data.Array(t,n) ->
+ let res = ref [] in
+ for i = 0 to n-1 do
+ let istr = string_of_int i in
+ res := !res @ aux (x^"["^istr^"]") (y^"["^istr^"]") t
+ done;
+ !res
+ | Data.Struct(n,fl) ->
+ let do_field (fn,ft) = aux (x^"."^fn) (y^"."^fn) ft in
+ List.flatten (List.map do_field fl)
+ | _ -> [x^"="^y]
+ in
+ aux x y t
+ in
+ let prg = try prg^(String.concat " and\n \t\t "
+ (List.flatten (List.map2 var_to_equals locals outvars))) ^");\ntel;\n"
+ with _ -> assert false
+ in
let prg = prg ^ "
node r_abs(x:real) returns (res:real);
let
- res = if x > 0.0 then x else -x;
+ res = if x < 0.0 then -x else x;
tel
const seuil = 0.0001;
diff --git a/utils/lustrequiv b/utils/lustrequiv
new file mode 100755
index 00000000..c2d1c522
--- /dev/null
+++ b/utils/lustrequiv
@@ -0,0 +1,76 @@
+#!/bin/sh
+# compares with lesar and lurette the behavior of 2 lustre programs
+
+
+EXPECTED_ARGS=4
+
+if [ $# -ne $EXPECTED_ARGS ]
+then
+ echo "usage: $0 lustrefile1 node1 lustrefile2 node2
+
+ Uses lurette and lesar to state if node1 and node2 are equivalent or not.
+ "
+else
+ file1=$1
+ node1=$2
+ file2=$3
+ node2=$4
+ oracle_node=${node1}_oracle
+ oracle_file=_${oracle_node}.lus
+ env=_${node1}_env.lut
+
+ echo " Are nodes $node1@$file1 and $node2@$file2 equivalent?"
+ echo " let's check it with lurette... "
+ set -x #echo on
+
+ if
+ lus2lic $file1 -n $node1 --gen-autotest -np;
+ then
+ echo "lus2lic --gen-autotest done"
+ else
+ echo "Error when calling 'lus2lic $file1 -n $node1 --gen-autotest -np'"
+ exit 2
+ fi
+
+
+ lus2lic $file1 -n $node1 -ec >> $oracle_file ;
+ lus2lic $file2 -n $node2 -ec >> $oracle_file ;
+ echo "node P1 = ${node1}" >> $oracle_file;
+ echo "node P2 = ${node2}" >> $oracle_file;
+
+ lurettetop -p 6 -seed 42 \
+ -rp "sut:v6:$file2:$node2" \
+ -rp "env:lutin:$env" \
+ -rp "oracle:v6:$oracle_file:$oracle_node" \
+ -go -l 100 -ns2c --stop-on-oracle-error;
+
+ set - #echo off
+ if [ $? -eq 0 ] # Test du code de sortie de la commande "lurettetop".
+ then
+ echo " ===> nodes $node1@$file1 and $node2@$file2 _SEEMS_ to be equivalent"
+ echo " let's check it with lesar... "
+ else if [ $? -eq 1 ]
+ then
+ echo " ===> nodes $node1@$file1 and $node2@$file2 _ARE NOT_ equivalent (cf lurette.rif)"
+ exit
+ else
+ echo " A pb occured in lurettop (exit $?)"
+ exit
+ fi
+ fi
+ set -x #echo on
+ lus2lic -ec ${oracle_file} -n ${node1}_oracle_prog -o ${node1}_oracle_prog.ec
+ ecverif ${node1}_oracle_prog.ec
+
+ set - #echo off
+ if [ $? -eq 0 ] # Test du code de sortie de la commande "lurettetop".
+ then
+ echo
+ echo " ===> nodes $node1@$file1 and $node2@$file2 _ARE_ equivalent"
+ else
+ echo " ===> nodes $node1@$file1 and $node2@$file2 _seems_ to differ"
+ fi
+
+
+ exit 0
+fi
\ No newline at end of file
--
GitLab