Commit 8734f2da authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Remove in Rif the "replace env dynamically" wart.

parent a3c512b6
......@@ -46,8 +46,7 @@ test:
###############################
# a few git shortcuts
cia: test cia_notest
cia_notest:
cia:
git commit -a -F log && make gen_version
amend-a:
......
......@@ -157,17 +157,18 @@ let (string_of_subst_list : subst list -> string) =
(***********************************************************************)
let (rif_read : in_channel -> state -> inputs * state) =
let (rif_read : in_channel -> state -> inputs) =
fun ic st ->
let (i,st') = Rif.read (LucProg.make_state None ) ic st in
(map2list i, st')
let i = Rif.read ic st.s.in_vars in
map2list i
let local_cpt = ref 1
let (rif_write_interface : out_channel -> state -> bool -> unit) =
fun oc st b ->
local_cpt := 1;
Rif.write_interface
Rif.write_interface oc st.s.in_vars st.s.out_vars (if b then Some st.s.in_vars else None)
let (rif_write : out_channel -> state -> subst list -> subst list -> unit) =
fun oc state inputs outputs ->
......
(** Time-stamp: <modified the 25/11/2010 (at 11:16) by Erwan Jahier> *)
(** Time-stamp: <modified the 03/02/2011 (at 09:50) by Erwan Jahier> *)
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
......@@ -62,7 +62,7 @@ val step_se : ?mode:(step_mode) -> state ref -> inputs -> solution
It is the input/output format of most Lustre/verimag tools.
*)
val rif_read : in_channel -> state -> inputs * state
val rif_read : in_channel -> state -> inputs
......
......@@ -259,7 +259,8 @@ and
(* Initializing the solution number table *)
!Solver.init_snt ();
Rif.write_interface stdout init_state options.locals;
Rif.write_interface stdout init_state.s.in_vars init_state.s.out_vars
(if options.locals then Some init_state.s.loc_vars else None);
let next_state =
if options.boot then
......@@ -314,12 +315,12 @@ and
Rif.write stdout step_str;
)
in
let (input, state') = Rif.read (LucProg.make_state None) stdin state in
let input = Rif.read stdin state.s.in_vars in
(* let input_list = Hashtbl.fold (fun vn x acc -> (vn,x)::acc) input [] in *)
let ral = LucFGen.get input state' in
let ral = LucFGen.get input state in
let (next_state, (out, loc)) =
try
Lucky.env_step options.draw_mode input state' ral
Lucky.env_step options.draw_mode input state ral
with
FGen.NoMoreFormula ->
Rif.write stdout ("# " ^ (Prog.ctrl_state_to_string_long state.d.ctrl_state));
......
......@@ -116,6 +116,7 @@ let dump_prog p = (
Printf.fprintf stderr "\n";
)
(* simu *)
let rec to_simu infile mnode = (
(* Parse and build the internal structure *)
......@@ -167,7 +168,8 @@ let rec to_simu infile mnode = (
Solver.set_efficient_mode ();
!Solver.init_snt ();
Rif.write_interface stdout init_state (MainArg.show_locals ()) ;
Rif.write_interface stdout init_state.Prog.s.Prog.in_vars init_state.Prog.s.Prog.out_vars
(if (MainArg.show_locals ()) then Some init_state.Prog.s.Prog.loc_vars else None);
Rif.flush stdout;
let next_state = init_state in
(* first main_loop : no pre context *)
......@@ -189,29 +191,18 @@ and main_loop_core ?(boot=false) t state = (
Utils.time_C "main_loop";
Utils.time_C "main_loop1";
let step_str = (
let step_str =
("#step " ^ (string_of_int t)) ^
(if state.Prog.d.Prog.verbose >= 1
then (" (" ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state) ^ "):")
else ""
) ^ "\n"
) in
(* FORBIDS TO Rif reader TO DYNAMICALLY CHANGE LUT PROGRAM *)
Verbose.put "#Main.main_loop call Rif.read\n";
let make_prog _ =
(*
function
| [infile ; mnode] -> LutProg.make_state ~libs:(MainArg.libs()) infile mnode
| _ ->
*)
assert false
) ^ "\n"
in
Rif.write stdout step_str;
(* IF BOOT -> don't ask for input *)
let (input, state') =
if boot then (Value.OfIdent.empty, state)
else Rif.read make_prog stdin state
let input =
if boot then Value.OfIdent.empty
else Rif.read stdin state.Prog.s.Prog.in_vars
in
(* let input_list = Hashtbl.fold (fun vn x acc -> (vn,x)::acc) input [] in *)
......@@ -220,7 +211,7 @@ Utils.time_C "main_loop1";
Utils.time_R "main_loop1";
Utils.time_C "main_loop2";
let generator = LucFGen.get input state' in
let generator = LucFGen.get input state in
Utils.time_R "main_loop2";
......@@ -231,7 +222,7 @@ Utils.time_R "main_loop2";
*)
let (next_state, (out, loc)) = try (
Verbose.put "#Main.main_loop call Lucky.env_step\n";
Lucky.env_step (MainArg.draw_mode()) input state' generator
Lucky.env_step (MainArg.draw_mode()) input state generator
) with
| FGen.NoMoreFormula ->
Rif.write stdout ("# " ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state));
......
......@@ -78,14 +78,6 @@ and
and simple_tbl
= simple Util.StringMap.t
let value_of_exp e = (
match e with
| Formu True -> B true
| Formu False -> B false
)
(*******************************************************************************)
let (ext_func_type_to_string : ext_func_type -> string) =
fun tl ->
......
......@@ -13,16 +13,17 @@ open List
open Gen_stubs_common
(** Generates stub files for calling poc C programs from lurette. Its main
function takes as input the name of the sut and the name of the oracle
(file names without extension), and outputs all the necessary stub files.
(** Parses a C header file and to generate stub files for calling poc
C programs from lurette. Its main function takes as input the name
of the sut and the name of the oracle (file names without
extension), and outputs all the necessary stub files.
Note that the C files should follows the poc convention (e.g., generated
by a lustre compiler). For instance, the header files should contain
the following pragmas:
Note that the C files should follows the poc convention (e.g., generated
by a lustre compiler). For instance, the header files should contain
the following pragmas:
//MODULE: <module name> n m
(* where [n] is the input var number, and [m] the output var one *)
//MODULE: <module name> n m
// where [n] is the input var number, and [m] the output var one
//IN: <C type of the first input var> <a C identifier for the first input var>
......@@ -98,7 +99,7 @@ let (gen_a_fake_oracle : string -> string -> string -> compiler -> string -> boo
(****************************************************************************)
let usage = "
usage: gen_stub <sut_path> <sut_node> <sut_compiler> [<oracle> <oracle_node> \
usage: gen_stub <sut> <sut_node> <sut_compiler> [<oracle> <oracle_node> \
<oracle_compiler>] dir
where:
......
......@@ -49,38 +49,6 @@ let rec (parse_string_list : stream -> string list -> string list) =
sl
(*
Dynamically change the current Lucky automata.
Will work <=> the interface does not change.
*)
let (replace_env_dynamically: (string list -> Prog.state) ->
bool -> stream -> Prog.state) =
fun make_prog is_reactive stream ->
let luc_files = parse_string_list stream [] in
let _ =
Formula_to_bdd.clear_all ();
output_string stderr "loading ";
List.iter (fun x -> output_string stderr (x ^ " ")) luc_files;
output_string stderr " ...\n"
in
let state = make_prog luc_files in
output_string stderr " ... ok\n";
print_string "#inputs ";
List.iter
(fun var ->
print_string ((Var.name var) ^ ":" ^
(Type.to_string2 (Var.typ var)) ^ " ")
)
state.s.out_vars;
print_string "\n";
flush stdout;
flush stderr;
state
(*------------------------------------------------------------------------*)
let read_line ic =
......@@ -89,120 +57,101 @@ let read_line ic =
str
(* exported *)
let rec (read : (string list -> Prog.state) -> in_channel -> Prog.state ->
Var.env_in * Prog.state) =
fun make_prog ic state ->
let vntl = state.s.in_vars in
(**
Reads input values on ic. It should follow the rif format.
*)
let rec (read : in_channel -> Exp.var list -> Var.env_in) =
fun ic vntl ->
(** Reads input values on ic. It should follow the rif format. *)
let tbl = Value.OfIdent.empty in
if vntl = [] then (tbl, state) else
if vntl = [] then tbl else
let line = read_line ic in
let stream = lexer (Stream.of_string line) in
parse_rif_stream make_prog ic vntl stream tbl state
and (parse_rif_stream : (string list -> Prog.state) -> in_channel ->
Exp.var list -> stream -> Var.env_in -> Prog.state -> Var.env_in * Prog.state) =
fun make_prog ic vntl stream tbl state ->
if
vntl = []
then
(tbl, state)
else
parse_rif_stream ic vntl stream tbl
and (parse_rif_stream : in_channel -> Exp.var list -> stream -> Var.env_in -> Var.env_in) =
fun ic vntl stream tbl ->
if vntl = [] then tbl else
let tok_list = Stream.npeek 2 stream in
match tok_list with
| [Genlex.Kwd (_,"#"); Genlex.Ident (_,id)] ->
if List.mem id rif_pragmas then (
Stream.junk stream ;
Stream.junk stream ;
parse_rif_stream make_prog ic vntl
(lexer (Stream.of_string (read_line ic))) tbl state
) else (
match tok_list with
| [Genlex.Kwd (_,"#"); Genlex.Ident (_,id)] ->
if List.mem id rif_pragmas then (
Stream.junk stream ;
Stream.junk stream ;
parse_rif_stream ic vntl
(lexer (Stream.of_string (read_line ic))) tbl
) else (
(* We skip everything that occurs after a [#] not followed by a
member of [rif_pragmas], until the next eol. *)
Stream.junk stream ;
parse_rif_stream make_prog ic
vntl (lexer (Stream.of_string (read_line ic))) tbl state
)
| [Genlex.Kwd (_,"#") ; Genlex.Kwd (_,"load_file")] ->
(* dynamically change the environment *)
(
Stream.junk stream ;
Stream.junk stream ;
let state' = replace_env_dynamically make_prog state.s.reactive stream in
parse_rif_stream make_prog ic
state.s.in_vars
(lexer (Stream.of_string (read_line ic))) tbl state'
)
| (Genlex.Kwd (_,"#"))::_ ->
Stream.junk stream ;
parse_rif_stream ic
vntl (lexer (Stream.of_string (read_line ic))) tbl
)
| (Genlex.Kwd (_,"#"))::_ ->
Stream.junk stream ;
parse_rif_stream make_prog ic vntl (lexer (Stream.of_string (read_line ic)))
tbl state
| (Genlex.Kwd (_,"q"))::_ -> print_string "# bye!\n"; exit 0
| (Genlex.Kwd (_,"#@"))::_ ->
parse_rif_stream ic vntl (lexer (Stream.of_string (read_line ic)))
tbl
| (Genlex.Kwd (_,"q"))::_ -> print_string "# bye!\n"; exit 0
| (Genlex.Kwd (_,"#@"))::_ ->
(* Beginning of multi-line comment. Note that here,
unlike the rif format, we ignore multi line pragmas;
namely, we handle them as a multi-line comment. *)
(
Stream.junk stream ;
ignore_toks_until_end_of_pragmas make_prog ic vntl stream tbl state
ignore_toks_until_end_of_pragmas ic vntl stream tbl
)
| (Genlex.Float (_,f))::_ ->
| (Genlex.Float (_,f))::_ ->
(
Stream.junk stream ;
(* Hashtbl.add tbl (Var.name (hd vntl)) (N(F(f))) ; *)
let tbl' = Value.OfIdent.add tbl (Var.name (hd vntl), N(F(f))) in
parse_rif_stream make_prog ic (tl vntl) stream tbl' state
parse_rif_stream ic (tl vntl) stream tbl'
)
| (Genlex.Int (_,i))::_ -> (
Stream.junk stream ;
let v =
if ((Type.to_string (Var.typ (hd vntl))) = "bool") then (
if (i = 0) then B(false) else B(true)
) else N(I(i))
in
let tbl' = Value.OfIdent.add tbl (Var.name (hd vntl), v) in
parse_rif_stream make_prog ic (tl vntl) stream tbl' state
)
| (Genlex.Ident (_,b))::_ -> (
Stream.junk stream ;
let v = if mem b ["f"; "F";"false"] then B(false)
else if mem b ["t"; "T";"true"] then B(true)
else failwith ("### parse error: `" ^ b ^ "' is not expected.\n")
in
let tbl' = Value.OfIdent.add tbl (Var.name (hd vntl), v) in
parse_rif_stream make_prog ic (tl vntl) stream tbl' state
)
| [] ->
| (Genlex.Int (_,i))::_ -> (
Stream.junk stream ;
let v =
if ((Type.to_string (Var.typ (hd vntl))) = "bool") then (
if (i = 0) then B(false) else B(true)
) else N(I(i))
in
let tbl' = Value.OfIdent.add tbl (Var.name (hd vntl), v) in
parse_rif_stream ic (tl vntl) stream tbl'
)
| (Genlex.Ident (_,b))::_ -> (
Stream.junk stream ;
let v = if mem b ["f"; "F";"false"] then B(false)
else if mem b ["t"; "T";"true"] then B(true)
else failwith ("### parse error: `" ^ b ^ "' is not expected.\n")
in
let tbl' = Value.OfIdent.add tbl (Var.name (hd vntl), v) in
parse_rif_stream ic (tl vntl) stream tbl'
)
| [] ->
(* Eol is is reached; proceed with the next one *)
parse_rif_stream make_prog ic vntl (lexer (Stream.of_string (read_line ic)))
tbl state
| _ -> failwith ("### parse error: not in RIF format.\n")
and (ignore_toks_until_end_of_pragmas : (string list -> Prog.state) ->
in_channel -> Exp.var list -> stream -> Var.env_in -> Prog.state -> Var.env_in * Prog.state) =
fun make_prog ic vntl stream tbl state ->
parse_rif_stream ic vntl (lexer (Stream.of_string (read_line ic)))
tbl
| _ -> failwith ("### parse error: not in RIF format.\n")
and (ignore_toks_until_end_of_pragmas :
in_channel -> Exp.var list -> stream -> Var.env_in -> Var.env_in) =
fun ic vntl stream tbl ->
(* ignore all tokens until "@#" is reached *)
let tok_opt = Stream.peek stream in
match tok_opt with
| Some(Genlex.Kwd (_,"@#")) ->
(
Stream.junk stream ;
parse_rif_stream make_prog ic vntl stream tbl state
parse_rif_stream ic vntl stream tbl
)
| Some(_) ->
(
Stream.junk stream ;
ignore_toks_until_end_of_pragmas make_prog ic vntl stream tbl state
ignore_toks_until_end_of_pragmas ic vntl stream tbl
)
| None ->
(* Eol is is reached; proceed with the next one *)
(ignore_toks_until_end_of_pragmas make_prog ic vntl
(lexer (Stream.of_string (read_line ic))) tbl state)
(ignore_toks_until_end_of_pragmas ic vntl
(lexer (Stream.of_string (read_line ic))) tbl)
(*------------------------------------------------------------------------*)
......@@ -219,14 +168,14 @@ let (flush : out_channel -> unit) =
(*------------------------------------------------------------------------*)
(* exported *)
let (write_interface : out_channel -> Prog.state -> bool -> unit) =
fun oc state print_locals ->
let (write_interface : out_channel -> Exp.var list -> Exp.var list -> Exp.var list option -> unit) =
fun oc in_vars out_vars loc_vars_opt ->
let str =
(List.fold_left
(fun acc v ->
acc ^ "\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
"#inputs "
state.s.in_vars) ^
in_vars) ^
"\n#outputs " ^
......@@ -234,17 +183,18 @@ let (write_interface : out_channel -> Prog.state -> bool -> unit) =
(fun acc v ->
acc ^ "\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
""
state.s.out_vars) ^
out_vars) ^
(if print_locals then
((List.fold_left
(fun acc v ->
acc^"\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
"\n#locals "
(fst (List.partition (fun v -> (Var.alias v) = None) state.s.loc_vars ))
) ^ "\n")
else
"\n")
(match loc_vars_opt with
| None -> "\n"
| Some loc_vars ->
((List.fold_left
(fun acc v ->
acc^"\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
"\n#locals "
(fst (List.partition (fun v -> (Var.alias v) = None) loc_vars ))
) ^ "\n")
)
in
write oc str
......
......@@ -11,27 +11,21 @@
(** RIF (Reactive Input Format) utilities *)
(** [open_rif_file f] will record *all* the data that are read/write
on the in_channel/out_channel into the f file. *)
(** if [open_rif_file f] is called, *all* the data that are read/write
on the in_channel/out_channel will be recorded into the f file. *)
val open_rif_file : string -> unit
(** Reads from stdin the inputs
The first parameter is used to dynamically change the env.
- if the env is in Lutin, the string list is made the file and the node
- if it is in Lucky, its just a list of files.
*)
val read : (string list -> Prog.state) -> in_channel ->
Prog.state -> Var.env_in * Prog.state
(** Reads from stdin the inputs *)
val read : in_channel -> Exp.var list -> Var.env_in
val write : out_channel -> string -> unit
(** [write_outputs oc outputs ] writes the Lucky outputs *)
val write_outputs : out_channel -> Exp.var list -> Value.OfIdent.t -> unit
(** writes the input and output var names and types *)
val write_interface : out_channel -> Prog.state -> bool -> unit
(** [write_interface oc in_vars_ out_vars out_vars] writes the input
and output var names and types *)
val write_interface : out_channel -> Exp.var list -> Exp.var list -> Exp.var list option -> unit
val flush : out_channel -> unit
Supports Markdown
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