Commit 1c8385d0 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.29 Fri, 30 Apr 2004 16:43:39 +0200 by jahier

Parent-Version:      1.28
Version-Log:

source/ocaml2c.idl:
source/lurette.ml:
source/gen_stubs_poc.ml:
source/gen_stubs_scade.ml:
  Fix a bug where the step and the tries in the sut were completely
  wrong.

source/store.ml
  Fix a bug where, if only the ~min or the ~max options were used,
  they were ignored ...

source/parse_luc.ml:
  Make sure that ~min and ~max are fed with values, not complex expressions.

  pre-process lucky files with cpp.

source/sim2chro.ml:
  put the locals after the outputs because it is the order into
  which their values appear.

source/gen_stubs.ml:
  Do not change the oracle compiler if it is provided.

Project-Description: Lurette
parent 6de2c0e9
This diff is collapsed.
......@@ -18,10 +18,28 @@ et je ne suis plus oblig
ne sont pas mis a jour) -> le retester
* PB ne trouve pas ec2c, etc...
*********** A faire
* quand un saofdm est selectionné, passer en mode scade
* Préciser dans le manuel le role des 2 fenetres + mettre
un message dans chaque fenetres du style
"This is the standard output window"
"This is the standard error window"
???
* Rajouter une section "Add Environement variables "
+ faire une passe sur toutes les parametres que l'on peut positionné
depuis la fenetre principale.
* plot a besion de gnu-awk ... Je devrais ecrire moi-meme en caml
le programme qui genere le bon format pour gnuplot...
En plus, Pour les gros fichier, ca rame à donf !
* Faire une section <<Testing programs that are not lustre or scade programs>>
que je pourrais appeler aussi <<Compiling versus interpreting>>
voire <<compiled modes and pipeline mode>>
......@@ -43,8 +61,6 @@ et je ne suis plus oblig
ou mettre tous les .so dans un repertoire (comme matlab) ???
* plot a besion de gnu-awk ... Je devrais ecrire moi-meme en caml
le programme qui genere le bon format pour gnuplot...
* Finir le ocaml-lutin (.mluc)
......
......@@ -534,7 +534,7 @@ verimag
<handler>on_extra_var_button_clicked</handler>
<last_modification_time>Mon, 16 Jun 2003 11:56:14 GMT</last_modification_time>
</signal>
<label> Extra Environment Varibles </label>
<label> Extra Environment Variables </label>
<relief>GTK_RELIEF_NORMAL</relief>
<child>
<left_attach>1</left_attach>
......
......@@ -347,7 +347,7 @@ let button97 = GButton.button
~shrink:`NONE
~fill:`X
)
~label: " Extra Environment Varibles "
~label: " Extra Environment Variables "
()
in
let _ = GtkBase.Widget.set_can_focus button97#as_widget true in
......
This diff is collapsed.
This diff is collapsed.
......@@ -274,10 +274,13 @@ fi
AC_CHECK_PROG(GV,gv,gv,no)
if test "$GV" = no ; then
AC_CHECK_PROG(GV,gv,gv,gv)
AC_MSG_WARN(Cannot find gv. You will not be able to use show_luc)
fi
AC_PROG_AWK
AC_SUBST(AWK)
source ../VERSION
AC_SUBST(VERSION)
......
......@@ -33,6 +33,7 @@ if test -f $FILE ;
-e 's/:int/ | /g' \
-e 's/:real/ | /g' \
-e 's/#step/#/g' \
-e 's/# seed = /@ seed = /g' \
-e 's/# step/#/g' \
-e 's/@#//g' \
-e 's/#program/#@program/' \
......
......@@ -20,7 +20,7 @@
"Regular expression used by Font-lock mode.")
(setq lucky-font-lock-keywords
'(("--.*$" . font-lock-comment-face)
'(("--.*$\\|//.*$" . font-lock-comment-face)
("\\<\\(weight\\|max\\|min\\|default\\|alias\\|init\\|cond\\|max\\|With\\)\\>" . font-lock-string-face)
("\\<\\(+\\|*\\|-\\|/\\|mod\\)\\>"
......@@ -28,6 +28,7 @@
("[][;,()|{}@^!:#*=<>&/%+~?---]\\.?\\|\\.\\." . font-lock-function-name-face)
("\\<\\(true\\|abs\\|and\\|or\\|if\\|then\\|else\\|pre\\|||\\|not\\|false\\|!\\)\\>" . font-lock-reference-face)
("\\<\\(bool\\|int\\|real\\|float\\)\\(\\^.+\\)?\\>" . font-lock-variable-name-face)
("\\<\\(define\\|include\\)\\(\\^.+\\)?\\>" 0 'font-lock-preprocessor-face nil)
("\\(\\<\\(inputs\\|outputs\\|typedef\\|start_node\\|nodes\\|locals\\|transitions\\|transient\\|final\\|stable\\|arcs_nb\\|nodes_nb\\|=\\)\\>\\|->\\)" .
font-lock-function-name-face)))
......
#!/bin/sh
# $Id: plot 1.10 Wed, 21 Apr 2004 09:38:03 +0200 jahier $
# $Id: plot 1.11 Fri, 30 Apr 2004 16:43:39 +0200 jahier $
#
# pl: general wrapper script for plotting with gnuplot from shell cmdline
#
......@@ -49,6 +49,11 @@
# improved -dif handling (boxes)
#
if [$AWK == ""] ; then
AWK=awk
fi
OWD=`pwd`
DIR=/tmp
DATA=pl$$ # files to place data columns in
......@@ -66,6 +71,8 @@ GNUPLOT="gnuplot -geometry +100+100"
LOCAL_RCFILE=.plrc
HOME_RCFILE=$HOME/.plrc
# init this.gnuplot.commands file; first: hard-coded defaults
if [ -f $CODE ]; then rm $CODE; fi
cat > $CODE << EOT
......@@ -262,11 +269,11 @@ FILENO=1
for i
do
# generate .nnn suffix
# IRIX printf(1) is useless for anything but %s; thus use gawk
FILENNN=`gawk 'BEGIN{printf "%03d", '$FILENO'; exit}'`
# IRIX printf(1) is useless for anything but %s; thus use $AWK
FILENNN=`$AWK 'BEGIN{printf "%03d", '$FILENO'; exit}'`
echo "# file: $i - $FILENO of $#" > $DIR/$DATA.$FILENNN # used for key
gawk "$AWKDATA" $i | $COLUMN_OPERATOR >> $DIR/$DATA.$FILENNN || {
$AWK "$AWKDATA" $i | $COLUMN_OPERATOR >> $DIR/$DATA.$FILENNN || {
echo skipping $i\; 1>&2 ; continue;
}
FILENO=`expr $FILENO + 1`
......@@ -292,7 +299,7 @@ do
case "$USING1" in
'') # no -using given; plot all columns (traditional)
COLPLOT=`gawk '
COLPLOT=`$AWK '
BEGIN { DATANAME="'$i'" }
#NR==1 { FNAME="'\''" $3 "'\''" } # put '' around file name in key
......@@ -337,7 +344,7 @@ do
' $i` # end COLPLOT=``
;;
*) # -using was set; apply all(?) using-specs on each file
FNAME=`gawk 'NR==1 {print $3; exit;}' $i`
FNAME=`$AWK 'NR==1 {print $3; exit;}' $i`
COLPLOT=" '$i' us $USING1 ti '$FNAME $USING1'"
;;
esac # on $USING1
......
......@@ -4,11 +4,15 @@
VERSION=@VERSION@
export VERSION
LURETTE_PATH=@LURETTEPATH@
export LURETTE_PATH
if test -z "$LURETTE_PATH" ; then
LURETTE_PATH=@LURETTEPATH@
export LURETTE_PATH
fi
PIXMAP_DIR=@PIXMAP_DIR@
export PIXMAP_DIR
if test -z "$PIXMAP_DIR" ; then
PIXMAP_DIR=@PIXMAP_DIR@
export PIXMAP_DIR
fi
path=@LURETTEPATH@/@HOST_TYPE@/bin:$path
export path
......@@ -20,53 +24,85 @@ export LD_LIBRARY_PATH
PATH=@LURETTEPATH@/@HOST_TYPE@/bin:$PATH
export PATH
PS_VIEWER=@GV@
export PS_VIEWER
if test -z "$PS_VIEWER" ; then
PS_VIEWER=@GV@
export PS_VIEWER
fi
DOT=dot
export DOT
if test -z "$DOT" ; then
DOT=dot
export DOT
fi
LUS2EC=@LUS2EC@
export LUS2EC
if test -z "$LUS2EC" ; then
LUS2EC=@LUS2EC@
export LUS2EC
fi
EC2C=@EC2C@
export EC2C
if test -z "$EC2C" ; then
EC2C=@EC2C@
export EC2C
fi
SIM2CHRO=@LURETTEPATH@/@HOST_TYPE@/bin/sim2chrogtk
export SIM2CHRO
if test -z "$SIM2CHRO" ; then
SIM2CHRO=@LURETTEPATH@/@HOST_TYPE@/bin/sim2chrogtk
export SIM2CHRO
fi
HOST_TYPE=@HOST_TYPE@
export HOST_TYPE
if test -z "$HOST_TYPE" ; then
HOST_TYPE=@HOST_TYPE@
export HOST_TYPE
fi
GNUPLOTRIF=@LURETTEPATH@/share/gnuplot-rif
export GNUPLOTRIF
if test -z "$GNUPLOTRIF" ; then
GNUPLOTRIF=@LURETTEPATH@/share/gnuplot-rif
export GNUPLOTRIF
fi
GNUPLOT_TERM=@GNUPLOT_TERM@
if test -z "$GNUPLOT_TERM" ; then
GNUPLOT_TERM=@GNUPLOT_TERM@
fi
PLOT=@LURETTEPATH@/share/plot
export PLOT
# scade
SCADE2LUSTRE=@SCADE2LUSTRE@
export SCADE2LUSTRE
SCADE_CG=@SCADE_CG@
export SCADE_CG
LUSTRE2C=@LUSTRE2C@
export LUSTRE2C
SCADE_INSTALL_DIR=@SCADE_INSTALL_DIR@
export SCADE_INSTALL_DIR
SCADE_COMPIL_OPTION=" -noexp @ALL@ "
export SCADE_COMPIL_OPTION
if test -z "$AWK" ; then
AWK=@AWK@
export AWK
fi
if test -z "$PLOT" ; then
PLOT=@LURETTEPATH@/share/plot
export PLOT
fi
# scade
if test -z "$SCADE2LUSTRE" ; then
SCADE2LUSTRE=@SCADE2LUSTRE@
export SCADE2LUSTRE
fi
if test -z "$SCADE_CG" ; then
SCADE_CG=@SCADE_CG@
export SCADE_CG
fi
if test -z "$LUSTRE2C" ; then
LUSTRE2C=@LUSTRE2C@
export LUSTRE2C
fi
if test -z "$SCADE_INSTALL_DIR" ; then
SCADE_INSTALL_DIR=@SCADE_INSTALL_DIR@
export SCADE_INSTALL_DIR
fi
if test -z "$SCADE_COMPIL_OPTION" ; then
SCADE_COMPIL_OPTION=" -noexp @ALL@ "
export SCADE_COMPIL_OPTION
fi
# Other options migth also work.
# e.g., " -exp @ALL@ " also works, but not " -blockexp "
......@@ -66,7 +66,12 @@ let rec (lookup: Var.env_in -> Env_state.t -> Exp.var -> Value.t option) =
| Some _ ->
(* Structured expression ougth to have been
flattened before *)
assert false
print_string (
"*** Error: the initial value of variable "
^ (Prevar.get_var_name (Var.name var)) ^
" is not valid.\n");
flush stdout;
exit 1
| None ->
let cnl = List.flatten state.d.current_nodes in
let nodes_str = String.concat " " cnl in
......@@ -305,12 +310,6 @@ and (translate_do : Var.env_in -> Env_state.t -> Exp.formula ->
in
(Bdd.xor bdd1 bdd2, dep1 || dep2)
| EqB(f1, f2) ->
let (bdd1, dep1) = (translate_do input state f1)
and (bdd2, dep2) = (translate_do input state f2)
in
(Bdd.eq bdd1 bdd2, dep1 || dep2)
| IteB(f1, f2, f3) ->
let (bdd1, dep1) = (translate_do input state f1)
and (bdd2, dep2) = (translate_do input state f2)
......@@ -348,6 +347,12 @@ and (translate_do : Var.env_in -> Env_state.t -> Exp.formula ->
)
)
| EqB(f1, f2) ->
let (bdd1, dep1) = (translate_do input state f1)
and (bdd2, dep2) = (translate_do input state f2)
in
(Bdd.eq bdd1 bdd2, dep1 || dep2)
| Eq(e1, e2) ->
let gne = expr_to_gne (Diff(e1, e2)) input state in
(gne_to_bdd gne EqZero)
......
......@@ -164,7 +164,7 @@ let compile_lustre_program_if_needed
(* Util.scade_cg lustre_prog lustre_node tmp_dir; *)
Util.scade2lustre lustre_prog ;
Util.lustre2C
((Filename.chop_extension lustre_prog) ^ ".lus")
((Filename.chop_extension lustre_prog) ^ ".lus")
lustre_node tmp_dir;
)
else if
......@@ -199,7 +199,7 @@ let compile_lustre_program_if_needed
" with node " ^ lustre_node ^
" with the lustre2C scade code generator.\n");
Util.lustre2C
((Filename.chop_extension lustre_prog) ^ ".lus")
((Filename.chop_extension lustre_prog) ^ ".lus")
lustre_node tmp_dir
)
else
......@@ -389,19 +389,10 @@ let (main : unit -> 'a) =
"please rename it.\n");
exit 1
);
compile_lustre_program_if_needed
sut sut_node sut_compiler user_dir tmp_dir;
compile_lustre_program_if_needed
oracle oracle_node
(if
(oracle_node = "always_true") || (oracle_node = " ")
then
(* make it sure we use a compiler that is installed *)
sut_compiler
else
oracle_compiler
)
user_dir tmp_dir
compile_lustre_program_if_needed sut sut_node
sut_compiler user_dir tmp_dir;
compile_lustre_program_if_needed oracle oracle_node
oracle_compiler user_dir tmp_dir
in
gen_stubs_file tmp_dir
(Filename.concat user_dir sut_node) sut_compiler
......
......@@ -73,6 +73,21 @@ let (go: module_name -> string -> typedef list -> vn_ct list -> vn_ct list ->
put "\n" ;
(*
** Save and restore the state
*)
put " // Save and restore the state \n";
put ("void " ^ str ^ "_save_state ()\n{\n");
put (" " ^ mod_name ^ "_copy_ctx(prg_copy, prg);\n") ;
put "}\n";
put ("void " ^ str ^ "_restore_state ()\n{\n");
put (" " ^ mod_name ^ "_copy_ctx(prg, prg_copy);\n") ;
put "}\n\n";
(*
** Output procedures
*)
......@@ -289,27 +304,6 @@ let (go: module_name -> string -> typedef list -> vn_ct list -> vn_ct list ->
put "}\n" ;
(*
** Try
*)
put "\n" ;
put "// Try \n" ;
(* Function header *)
put ("void " ^ str ^ "_try(void) \n{\n");
(* Function body *)
put "\n // Save the current context. \n";
put (" " ^ mod_name ^ "_copy_ctx(prg_copy, prg);\n\n") ;
put "\n // Performs the step. \n";
put (" " ^ str ^ "_step(); \n") ;
put "\n // Restore the context. \n";
put (" " ^ mod_name ^ "_copy_ctx(prg, prg_copy);\n") ;
put "}\n" ;
(*
** Variable number
......
......@@ -115,12 +115,26 @@ let (go: module_name -> string -> typedef list -> vn_ct list -> vn_ct list ->
put "// Program state initialisation \n" ;
put ("void " ^ str ^ "_init() \n{\n" ^
" " ^ mod_name ^ "_init(_C_); \n") ;
put (" " ^ mod_name ^ "_init(_C_copy); \n}\n") ;
put "\n" ;
put (" memcpy(_C_copy, _C_, sizeof(_C_" ^ mod_name ^ ")); ") ;
put "\n}\n\n" ;
put "\n" ;
(*
** Save and restore the state
*)
put " // Save and restore the state \n";
put ("void " ^ str ^ "_save_state ()\n{\n");
put (" memcpy(_C_copy, _C_, sizeof(_C_" ^ mod_name ^ "));\n") ;
put "}\n\n";
put ("void " ^ str ^ "_restore_state ()\n{\n");
put (" memcpy(_C_, _C_copy, sizeof(_C_" ^ mod_name ^ "));\n") ;
put "}\n\n";
(*
** Set and get int values from caml
*)
......@@ -311,6 +325,7 @@ let (go: module_name -> string -> typedef list -> vn_ct list -> vn_ct list ->
put "}\n" ;
(*
** Step
*)
......@@ -318,31 +333,22 @@ let (go: module_name -> string -> typedef list -> vn_ct list -> vn_ct list ->
put "// Step \n" ;
(* Function header *)
put ("void " ^ str ^ "_step(void) \n{\n");
put (" " ^ mod_name ^ "(_C_);\n") ;
put (" _copy_mem(sizeof(_C_" ^ mod_name ^ "), _C_, _C_copy);\n\n") ;
put "}\n" ;
(*
** Try
*)
put "\n" ;
put "// Try \n" ;
(* Function header *)
put ("void " ^ str ^ "_try(void) \n{\n");
(* Function body *)
(* put ("printf(\"step" ^ str ^ " \");\n"); *)
(* put (" memcpy( _C_copy, _C_, sizeof(_C_" ^ mod_name ^ "));\n\n") ; *)
put "\n // Restore the previous context. \n";
put (" _copy_mem(sizeof(_C_" ^ mod_name ^ "), _C_copy, _C_);\n\n") ;
put "\n // Performs the step. \n";
put (" " ^ mod_name ^ "(_C_);\n") ;
put "}\n" ;
(*
** Variable number
*)
......
......@@ -242,6 +242,8 @@ let check_oracle inputs sut_outputs locals memory t rif state =
print_subst_list i stdout;
output_string stdout "\n* sut outputs:\n\t" ;
print_env_in o stdout;
output_string stdout "\n* env locals:\n\t" ;
print_subst_list l stdout;
output_string rif "\n#oracle_failure at\n";
Sim2chro.put_current_step_values
......@@ -506,7 +508,7 @@ and
("lurette chronogram (" ^
(fold_left
(fun acc str ->
(acc ^ " " ^ str)) (hd env_list) (tl env_list)) ^ ")"
(acc ^ " " ^ str)) (hd env_list) (tl env_list)) ^ " )"
)
sut_i_vntl
sut_o_vntl
......@@ -596,15 +598,14 @@ and
(* Performs the steps *)
let (next_state, (output, loc)) = Lucky.env_step (options.step_mode) input state in
let new_input = Sut.trie output in
let new_input = Sut.step output in
let _ = check_oracle [output] [new_input] [loc] state.d.memory t rif next_state in
let _ =
Sut.step output ;
if (options.oracle) then Oracle.step output new_input ;
in
let str =
if (options.step_by_step) then (
if (state.d.current_nodes <> next_state.d.current_nodes) then
......@@ -649,7 +650,7 @@ and
"\n ==> The test completed; no property has been violated.\n\n";
print_string (
" The Test Thickness average was " ^
(string_of_float (!l_average /. (float_of_int t))) ^ "\n");
(string_of_float (1.0 +. !l_average /. (float_of_int t))) ^ "\n");
flush stdout;
next_state
)
......
......@@ -9,6 +9,12 @@ typedef struct vn_t
void lurette__sut_init();
void lurette__oracle_init();
void lurette__sut_save_state();
void lurette__sut_restore_state();
void lurette__oracle_save_state();
void lurette__oracle_restore_state();
int lurette__sut_get_val_int(int arg_nb);
double lurette__sut_get_val_float(int arg_nb);
......@@ -28,9 +34,7 @@ void lurette__oracle_set_val_float(int arg_nb, double f);
void lurette__oracle_set_val_bool(int arg_nb, boolean b);
void lurette__sut_step(void);
void lurette__sut_try(void);
void lurette__oracle_step(void);
void lurette__oracle_try(void);
int lurette__sut_input_arg_nb(void);
int lurette__sut_output_arg_nb(void);
......
......@@ -85,8 +85,10 @@ let (set_oracle_input: env_out -> env_in -> unit) =
let (trie : env_out -> env_in -> bool) =
fun input output ->
set_oracle_input input output;
Ocaml2c.lurette__oracle_try () ;
Ocaml2c.lurette__oracle_restore_state ();
set_oracle_input input;
Ocaml2c.lurette__oracle_step () ;
match oracle_o_vntl with
[(vn, "bool")] ->
let res = Ocaml2c.lurette__oracle_get_val_bool 0 in
......@@ -96,6 +98,5 @@ let (trie : env_out -> env_in -> bool) =
let (step : env_out -> env_in -> unit) =
fun input output ->
set_oracle_input input output;
Ocaml2c.lurette__oracle_step ()
Ocaml2c.lurette__oracle_save_state ();
......@@ -819,7 +819,7 @@ and (reject_unsupported_exp : Lexing.lexbuf -> Exp.t -> Type.t -> Exp.t option)
Util.from_char_pos_to_line_and_col (ic.lex_buffer) ic.lex_curr_pos
in
print_string (
"*** Type error: at character " ^
"*** Type error around character " ^
(string_of_int ic.lex_curr_pos) ^ " (i.e., " ^
"line " ^ line ^ ", column " ^ col ^ "), " ^
" " ^ (Exp.to_string exp)
......@@ -827,6 +827,42 @@ and (reject_unsupported_exp : Lexing.lexbuf -> Exp.t -> Type.t -> Exp.t option)
failwith " "
)
(* it is the same as reject_unsupported_exp, but for options that necessarily
numeric (eg, min and max *)
and (reject_unsupported_simple_exp : Lexing.lexbuf -> Exp.t -> Type.t ->
Exp.t option) =
fun ic exp vt ->
let _ = print_debug_no_tok ic ("reject_unsupported_simple_exp \n") in
( match (exp, vt) with
| (Numer (Ival(_)), IntT) -> Some exp
| (Numer (Fval(_)), FloatT) -> Some exp
| (Formu True, BoolT) -> Some exp
| (Formu False, BoolT) -> Some exp
| ((Numer (Ival v)), UT(EnumT(el))) -> Some exp
| (Liste l, UT(ArrayT(size, t))) ->
Some exp
| (Liste l, UT(StructT(_))) ->
Some exp
| _ ->
let (line, col) =
Util.from_char_pos_to_line_and_col (ic.lex_buffer) ic.lex_curr_pos
in
print_string (
"*** Error around character " ^
(string_of_int ic.lex_curr_pos) ^ " (i.e., " ^
"line " ^ line ^ ", column " ^ col ^ "), " ^
" " ^ (Exp.to_string exp)
^ " is not of type " ^ (Type.to_string vt) ^
"\n or it is not a supported expression at this location."
);
failwith ""
)
and (var_options_to_var : Lexing.lexbuf -> typedef list -> string -> Type.t ->
Var.mode -> (string * (Exp.t * Type.t)) list -> var) =
fun ic tdl vn vt vm options ->
......@@ -842,7 +878,7 @@ and (var_options_to_var : Lexing.lexbuf -> typedef list -> string -> Type.t ->
Util.from_char_pos_to_line_and_col (ic.lex_buffer) ic.lex_curr_pos
in
print_string (
"*** Type error: at character " ^