Skip to content

GitLab

Commit 47b07b9e authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Support all lutin command-line options from lurette. In order to 

that, I've modified Lutin/mainArg.ml so that all globals are inside a
big structure. Indeed, Lurette has its own Arg.argv, on it may call
several lutin programs.
parent ce1f871a
Expand all Hide whitespace changes
Inline Side-by-side
examples/lutin/crazy-rabbit/Makefile
View file @ 47b07b9e
......@@ -24,7 +24,7 @@ test: rabbit.cmxs
rm -f test.rif0 .lurette_rc
$(NEW_LURETTETOP) -go --output test.rif0 \
-rp "sut:ocaml:rabbit.cmxs:" \
-rp "env:lutin:rabbit.lut:rabbit" && \
-rp 'env:lutin:rabbit.lut:-main:rabbit:-L:libm.so:-loc' && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
......
source/Lurettetop/ltopArg.ml
View file @ 47b07b9e
......@@ -83,7 +83,7 @@ type reactive_program =
| LustreV6 of string * string
| LustreEc of string
| LustreEcExe of string
| Lutin of string list * string
| Lutin of string array
| Socket of string * int
| SocketInit of string * int
| Ocaml of string
......@@ -105,10 +105,10 @@ let reactive_program_to_string = function
| LustreV6(f,node) -> "v6:"^f^":"^node
| LustreEc(f) -> "ec:"^f^":"
| LustreEcExe(f) -> "ec_exe:"^f^":"
| Lutin(f,node) -> "lutin:"^(String.concat "," f)^":"^node
| Lutin(args) -> "lutin:"^(String.concat ":" (Array.to_list args))
| Socket(addr,port) -> "socket:"^addr^":"^(string_of_int port)
| SocketInit(addr,port) -> "socket_init:"^addr^":"^(string_of_int port)
| Ocaml(str) -> "ocaml:" ^ str
type t = {
mutable suts : reactive_program list ;
......@@ -368,27 +368,42 @@ let string_to_step_mode = function
let (parse_rp_string : string -> unit) =
fun str ->
(* try *)
let l = (Str.split (Str.regexp ":") str) in
let rp =
match List.tl l with
| ["lutin"; prog; node] -> Lutin(Str.split (Str.regexp ",") prog, node)
| ["v6"; prog; node] -> LustreV6(prog, node)
| ["ec_exe"; prog] -> LustreEcExe(prog)
| ["ec"; prog] -> LustreEc(prog)
| ["ec"; prog; _] -> LustreEc(prog)
| ["v4"; prog; node] -> LustreV4(prog, node)
| ["ocaml"; cmxs] -> Ocaml(cmxs)
| ["socket"; addr; port] -> Socket(addr, int_of_string port)
| ["socket_init"; addr; port] -> SocketInit(addr, int_of_string port)
| _ -> failwith ("*** Error: Unsupported kind of reactive program: \""
^ str ^ "\"\n" ^ rp_help)
in
match program_kind_of_string (List.hd l) with
| SUT -> if not (List.mem rp args.suts) then args.suts <- rp::args.suts
| Env -> if not (List.mem rp args.envs) then args.envs <- rp::args.envs
| Oracle -> if not (List.mem rp args.oracles) then args.oracles <- rp::args.oracles
| PK_error msg -> failwith msg
(* try *)
let l = (Str.split (Str.regexp ":") str) in
let rp_args = List.tl l in
let rp =
match rp_args with
| ["lutin";prog; node] ->
(* for backward compatibility *)
let rp_args = Array.of_list("lutin"::prog::"-main"::node::[]) in
Lutin(rp_args)
| "lutin"::_ ->
let rp_args = Array.of_list rp_args in
Lutin(rp_args)
(*
for lutin programs we accept:
"lutin:toto.luc::"
"lutin:toto.luc:toto:"
"lutin:toto.luc:-main toto:"
*)
| ["v6"; prog; node] -> LustreV6(prog, node)
| ["ec_exe"; prog] -> LustreEcExe(prog)
| ["ec"; prog] -> LustreEc(prog)
| ["ec"; prog; _] -> LustreEc(prog)
| ["v4"; prog; node] -> LustreV4(prog, node)
| ["ocaml"; cmxs] -> Ocaml(cmxs)
| ["socket"; addr; port] -> Socket(addr, int_of_string port)
| ["socket_init"; addr; port] -> SocketInit(addr, int_of_string port)
| _ -> failwith ("*** Error: Unsupported kind of reactive program: \""
^ str ^ "\"\n" ^ rp_help)
in
match program_kind_of_string (List.hd l) with
| SUT -> if not (List.mem rp args.suts) then args.suts <- rp::args.suts
| Env -> if not (List.mem rp args.envs) then args.envs <- rp::args.envs
| Oracle -> if not (List.mem rp args.oracles) then args.oracles <- rp::args.oracles
| PK_error msg -> failwith msg
(* with *)
(* e -> failwith ("error in --reactive-program: " ^ Printexc.to_string e *)
(* ) *)
......
source/Lurettetop/lurettetop.ml
View file @ 47b07b9e
......@@ -231,7 +231,7 @@ let main_loop_start () =
Unix.chdir args.sut_dir;
let res = Run.f () in
if (res) <> 0 then (
Printf.fprintf args.ocr "Lurette failed (%d).\n \n \n" res;
Printf.fprintf args.ocr "\nLurette launched a process that failed (exit %d).\n \n" res;
flush args.ocr;
lurettetop_quit ();
exit 2
......
source/Lurettetop/runDirect.ml
View file @ 47b07b9e
......@@ -61,19 +61,9 @@ let (make_rp_list : reactive_program list ->
(Data.subst list -> Data.subst list) list *
Data.subst list list * Data.subst list list) =
fun rpl ->
let make_lut prog node =
(* ~libs: XXX *)
LutinRun.make_lut ~verb:args.verbose (* ~step_mode: args.step_mode *)
~seed: args.seed
~fair_mode:args.compute_volume
~show_locals:args.display_local_var
~precision: args.precision
prog node
in
let add_init init (a,b,c,d) = (a,b,c,d,init,init) in
let aux rp =
match rp with
| Lutin(prog,node) -> add_init [] (make_lut prog node)
| LustreV6(prog,node) -> add_init [] (LustreRun.make_v6 prog node)
| LustreV4(prog,node) -> add_init [] (LustreRun.make_v4 prog node)
| LustreEc(prog) -> add_init [] (LustreRun.make_ec prog)
......@@ -81,6 +71,7 @@ let (make_rp_list : reactive_program list ->
| Socket(addr, port) -> add_init [] (LustreRun.make_socket addr port)
| SocketInit(addr, port) -> LustreRun.make_socket_init addr port
| Ocaml(cmxs) -> LustreRun.make_ocaml cmxs
| Lutin(args) -> LutinRun.make_lut args
in
let res = Util.list_split6 (List.map aux rpl) in
......
source/Lutin/lutExe.ml
View file @ 47b07b9e
......@@ -239,7 +239,7 @@ let make ?(libs: string list option = None) infile mnode = (
one, but I'm sure that list will be useful in the future... R1.*)
let mnode = if all_nodes = [] then
(* shouldn't that be checked before? *)
raise (Errors.Global_error ((String.concat "," infile)^ " contains no node"))
raise (Errors.Global_error ("'"^(String.concat "," infile)^ "' contains no node"))
else List.hd all_nodes
in
Verbose.put ~level:1 "# No node is specified: will use %s \n" mnode;
......
source/Lutin/main.ml
View file @ 47b07b9e
......@@ -19,16 +19,16 @@ exception Stop
(* selection du fichier de sortie *)
let outchannel nodename = (
if (MainArg.outpipe ()) then (
let outchannel nodename opt = (
if (MainArg.outpipe opt) then (
Pervasives.stdout
) else (
let outname = (
match MainArg.outfile() with
match MainArg.outfile opt with
Some outf -> outf
| None -> (
let inbase = Filename.chop_extension (
Filename.basename (List.hd (MainArg.infile ()))
Filename.basename (List.hd (MainArg.infile opt))
) in
(inbase)^"-"^(nodename)^".luc"
)
......@@ -38,12 +38,12 @@ Verbose.put "#OUTFILE: %s\n" outname;
)
)
let to_luc mainprg tlenv = (
let to_luc mainprg tlenv opt = (
(* --> la fct qui traite un noeud *)
let compile_node mnode = (
Verbose.put "#COMPILING %s\n" mnode;
let exped = Expand.make tlenv mainprg mnode in
if (MainArg.test_expand()) then (
if (MainArg.test_expand opt) then (
Verbose.put "#EXPANDING %s\n" mnode;
Expand.dump exped
) else (
......@@ -51,20 +51,20 @@ let to_luc mainprg tlenv = (
(* let auto = AutoGen.make exped in *)
let auto = AutoGen.make exped in
let srcname =
if (MainArg.infile() = []) then ["stdin"] else (MainArg.infile())
if (MainArg.infile opt = []) then ["stdin"] else (MainArg.infile opt)
in
if (MainArg.test_auto()) then (
if (MainArg.test_auto opt) then (
(* AutoGen.dump auto *)
AutoGen.dump auto
) else (
(* gnration d'un fichier lucky *)
let oc = outchannel mnode in
let oc = outchannel mnode opt in
List.iter (fun f -> Auto2Lucky.make f mnode auto oc) srcname
)
)
) in
(* --> recherche du ou des mains *)
let nodearg = MainArg.main_node () in
let nodearg = MainArg.main_node opt in
if (nodearg = "") then (
(* expanse et compile tous les "mains" *)
let nl = (Syntaxe.pack_node_list mainprg) in
......@@ -118,25 +118,25 @@ let dump_prog p = (
(* simu *)
let rec to_simu oc infile mnode = (
let rec to_simu oc infile mnode opt = (
(* Parse and build the internal structure *)
let (zelutprog, zeprog) = LutProg.make ~libs:(MainArg.libs()) infile mnode in
let (zelutprog, zeprog) = LutProg.make ~libs:(MainArg.libs opt) infile mnode in
(* zelutprog is necessary for extracting initial data store *)
let state0 = LutProg.get_init_state zelutprog zeprog in
let init_state_dyn = { state0.Prog.d with Prog.verbose = Verbose.level () } in
let init_state = { state0 with Prog.d = init_state_dyn } in
let loc = if (MainArg.show_locals ()) then Some init_state.Prog.s.Prog.loc_vars else None in
let loc = if (MainArg.show_locals opt) then Some init_state.Prog.s.Prog.loc_vars else None in
let seed = MainArg.seed () in
let seed = MainArg.seed opt in
let msg =
Printf.sprintf
"# This is lutin Version %s (%s)\n# The random engine was initialized with the seed %d\n"
Version.str Version.sha seed
in
let noo = not (MainArg.only_outputs()) in
let noo = not (MainArg.only_outputs opt) in
Random.init seed;
if MainArg.compute_volume () then Solver.set_fair_mode () else Solver.set_efficient_mode ();
if MainArg.compute_volume opt then Solver.set_fair_mode () else Solver.set_efficient_mode ();
!Solver.init_snt ();
if noo then (
......@@ -146,26 +146,26 @@ let rec to_simu oc infile mnode = (
);
let next_state = init_state in
let lut_memories =
if MainArg.load_mem () then (
if MainArg.load_mem opt then (
output_string oc "#lutin_outputs_memories ";
Rif.read stdin (if noo then Some oc else None) init_state.Prog.s.Prog.out_vars)
else
Value.OfIdent.empty
in
(* first main_loop : no pre context *)
main_loop oc 1 next_state lut_memories
main_loop oc opt 1 next_state lut_memories
)
and main_loop oc t state pre_lut_output = (
and main_loop oc opt t state pre_lut_output = (
Verbose.exe ( fun () ->
let csnme = (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state) in
Verbose.put "#Main.main_loop ctrl_state=%s\n" csnme;
);
if state.Prog.s.Prog.is_final state.Prog.d.Prog.ctrl_state
then ()
else main_loop_core oc t state pre_lut_output
else main_loop_core oc opt t state pre_lut_output
)
and main_loop_core oc t state pre_lut_output = (
and main_loop_core oc opt t state pre_lut_output = (
let step_str =
("#step " ^ (string_of_int t)) ^
(if state.Prog.d.Prog.verbose >= 1
......@@ -173,7 +173,7 @@ and main_loop_core oc t state pre_lut_output = (
else ""
) ^ "\n"
in
let noo = not (MainArg.only_outputs ()) in
let noo = not (MainArg.only_outputs opt) in
let _ = if noo then Rif.write oc step_str in
let lut_input = Rif.read stdin (if noo then Some oc else None) state.Prog.s.Prog.in_vars in
......@@ -184,7 +184,7 @@ and main_loop_core oc t state pre_lut_output = (
where type solution = Var.env_out * Var.env_loc
*)
let (next_state, (lut_output, loc)) = try (
Lucky.env_step (MainArg.step_mode()) lut_input state generator
Lucky.env_step (MainArg.step_mode opt) lut_input state generator
) with
| FGen.NoMoreFormula ->
Rif.write oc ("# " ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state));
......@@ -211,7 +211,7 @@ and main_loop_core oc t state pre_lut_output = (
if noo then Rif.write oc " #outs ";
Rif.write_outputs oc next_state.Prog.s.Prog.out_vars lut_output;
if noo && MainArg.show_locals () then (
if noo && MainArg.show_locals opt then (
Rif.write oc "\n#locs ";
Rif.write_outputs oc next_state.Prog.s.Prog.loc_vars loc;
);
......@@ -223,13 +223,13 @@ and main_loop_core oc t state pre_lut_output = (
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
match MainArg.max_steps () with
| None -> main_loop oc (t+1) next_state lut_output
match MainArg.max_steps opt with
| None -> main_loop oc opt (t+1) next_state lut_output
| Some max -> (
if (t < max) then (
(* next pre's are current vals *)
(* let next_state = LutProg.memorize_data next_state lut_input lut_output loc in *)
main_loop oc (t+1) next_state lut_output
main_loop oc opt(t+1) next_state lut_output
) else (
Rif.write oc "\n#end\n";
Rif.flush oc
......@@ -240,20 +240,20 @@ and main_loop_core oc t state pre_lut_output = (
let dbgexe = Verbose.get_flag "LutExe"
(* simu with LutExe *)
let to_exe oc infile mnode = (
let exe = LutExe.make ~libs:(MainArg.libs()) infile mnode in
let to_exe oc infile mnode opt = (
let exe = LutExe.make ~libs:(MainArg.libs opt) infile mnode in
Verbose.exe ~flag:dbgexe (fun _ -> LutExe.dump exe);
let in_vars = LutExe.in_var_list exe in
let out_vars = LutExe.out_var_list exe in
let loc_vars = LutExe.loc_var_list exe in
let do_stop = match MainArg.max_steps () with
let do_stop = match MainArg.max_steps opt with
| None -> (fun _ -> false)
| Some max -> (fun c -> (c >= max))
in
let noo = not (MainArg.only_outputs ()) in
let noo = not (MainArg.only_outputs opt) in
let rec do_step cpt ctrl ins pres = (
Verbose.put "#Main.to_exe: step %d\n" cpt;
......@@ -282,7 +282,7 @@ let to_exe oc infile mnode = (
if noo then Rif.write oc " #outs ";
Rif.write_outputs oc out_vars outs ;
if noo && MainArg.show_locals () then (
if noo && MainArg.show_locals opt then (
Rif.write oc "\n#locs ";
Rif.write_outputs oc loc_vars locs
);
......@@ -317,7 +317,7 @@ let to_exe oc infile mnode = (
)
) in
let seed = MainArg.seed () in
let seed = MainArg.seed opt in
let msg =
Printf.sprintf
"# This is lutin Version %s (%s)\n# The random engine was initialized with the seed %d\n"
......@@ -327,7 +327,7 @@ let to_exe oc infile mnode = (
if noo then (
Rif.write oc msg;
Rif.write_interface oc in_vars out_vars
(if (MainArg.show_locals ()) then Some loc_vars else None) None;
(if (MainArg.show_locals opt) then Some loc_vars else None) None;
Rif.flush oc
);
......@@ -348,52 +348,54 @@ let to_exe oc infile mnode = (
let main () = (
(try
MainArg.parse () ;
let infile = MainArg.infile() in
let mnode = MainArg.main_node () in
let opt = MainArg.parse Sys.argv in
let infile = MainArg.infile opt in
let mnode = MainArg.main_node opt in
let _ =
if (infile = []) then
if MainArg.see_all_options () then
(MainArg.full_usage stderr; exit 0)
if MainArg.see_all_options opt then
(MainArg.full_usage stderr opt; exit 0)
else
(
MainArg.usage stderr;
MainArg.usage stderr opt;
raise (Global_error "no input file")
)
in
let oc =
match (MainArg.riffile()) with
match (MainArg.riffile opt) with
| None -> stdout
| Some file -> open_out file
in
match MainArg.gen_mode () with
match MainArg.gen_mode opt with
| Simu ->
if (MainArg.test_exe ()) then to_exe oc infile mnode else to_simu oc infile mnode
if (MainArg.test_exe opt)
then to_exe oc infile mnode opt
else to_simu oc infile mnode opt
| Cstubs -> (
Luc2c.option.Luc2c.output <- MainArg.outfile () ;
Luc2c.option.Luc2c.seed <- (Some(MainArg.seed ()));
Luc2c.option.Luc2c.output <- MainArg.outfile (opt) ;
Luc2c.option.Luc2c.seed <- (Some(MainArg.seed (opt)));
Luc2c.option.Luc2c.step_mode <- (
match (MainArg.step_mode ()) with
match (MainArg.step_mode (opt)) with
| Lucky.StepInside -> Luc2c.Inside
| Lucky.StepEdges -> Luc2c.Edges
| Lucky.StepVertices -> Luc2c.Vertices)
;
Luc2c.option.Luc2c.env <- (MainArg.infile());
Luc2c.option.Luc2c.env <- (MainArg.infile(opt));
Luc2c.main ()
)
| GenLuc -> (
let mainprg = Parsers.read_lut infile in
let tlenv = CheckType.check_pack (MainArg.libs ()) mainprg in
let tlenv = CheckType.check_pack (MainArg.libs (opt)) mainprg in
(* type/binding check *)
if MainArg.test_lex() then (
if MainArg.test_lex opt then (
List.iter (Parsers.lexemize_lut) infile
) else if (MainArg.test_parse()) then (
) else if (MainArg.test_parse opt) then (
(* analyse syntaxique *)
SyntaxeDump.dump_pack mainprg;
) else if (MainArg.test_check()) then (
) else if (MainArg.test_check opt) then (
CheckEnv.dbg_dump tlenv;
) else (
to_luc mainprg tlenv
to_luc mainprg tlenv opt
)
)
......
source/Lutin/mainArg.ml
View file @ 47b07b9e
This diff is collapsed.
source/Lutin/mainArg.mli
View file @ 47b07b9e
(** LUTIN2 : arguments de la commande
*)
type t
(* La ``mthode'' principale *)
val parse : unit -> unit
val usage : out_channel -> unit
val full_usage : out_channel -> unit
val parse : string array -> t
val usage : out_channel -> t -> unit
val full_usage : out_channel -> t -> unit
(* Paramtres statiques *)
val version : string
......@@ -12,52 +16,52 @@ val tool_name : string
val usage_msg : string
(* Accs aux arguments *)
val infile : unit -> string list
val test_lex : unit -> bool
val test_parse : unit -> bool
val test_check : unit -> bool
val test_expand : unit -> bool
val test_auto : unit -> bool
val main_node : unit -> string
val infile : t -> string list
val test_lex : t -> bool
val test_parse : t -> bool
val test_check : t -> bool
val test_expand : t -> bool
val test_auto : t -> bool
val main_node : t -> string
val test_exe : unit -> bool
val test_exe : t -> bool
(* Simulation *)
val max_steps : unit -> int option
val max_steps : t -> int option
type gen_mode =
Simu (* Simulate the Lutin file *)
| GenLuc (* Generate a lucky file *)
| Cstubs (* Generate C stubs files *)
val gen_mode : unit -> gen_mode
val gen_mode : t -> gen_mode
val load_mem : unit -> bool
val load_mem : t -> bool
val seed : unit -> int
val set_seed : int option -> unit
val seed : t -> int
val set_seed : t -> int option -> unit
(* n.b. if "Some l", l is certainly non-empty ! *)
val libs : unit -> string list option
val libs : t -> string list option
(* Output *)
val outfile : unit -> string option
val outpipe : unit -> bool
val outfile : t -> string option
val outpipe : t -> bool
(* Rif *)
val riffile : unit -> string option
val only_outputs : unit -> bool
val riffile : t -> string option
val only_outputs : t -> bool
val show_locals : unit -> bool
val set_show_locals : bool -> unit
val show_locals : t -> bool
val set_show_locals : t -> bool -> unit
val see_all_options : unit -> bool
val see_all_options : t -> bool
(* Options du solver *)
val step_mode : unit -> Lucky.step_mode
val set_step_mode : Lucky.step_mode -> unit
val step_mode : t -> Lucky.step_mode
val set_step_mode : t -> Lucky.step_mode -> unit
val compute_volume : unit -> bool
val set_compute_volume : bool -> unit
val compute_volume : t -> bool
val set_compute_volume : t -> bool -> unit
val set_precision : int -> unit
......
source/common/lutinRun.ml
View file @ 47b07b9e
......@@ -14,18 +14,11 @@ let (to_vals : Data.subst list -> Value.OfIdent.t) =
Value.OfIdent.empty
let make_lut
?(verb = 0) ?(libs = None) ?(step_mode = Lucky.StepInside)
?(seed: int option = None) ?(fair_mode:bool = false)
?(show_locals: bool = false) ?(precision: int = 2)
prog node =
let _ =
Verbose.set verb;
MainArg.set_seed seed;
MainArg.set_compute_volume fair_mode;
MainArg.set_show_locals show_locals;
MainArg.set_step_mode step_mode;
MainArg.set_precision precision
let make_lut argv =
let opt = MainArg.parse argv in
let libs = MainArg.libs opt
and prog = MainArg.infile opt
and node = MainArg.main_node opt
in
let lut_mach = LutExe.make ~libs:libs prog node in
let lut_in = List.map var_to_string_pair (LutExe.in_var_list lut_mach) in
......@@ -33,7 +26,6 @@ let make_lut
let lut_memories =
if LtopArg.args.LtopArg.delay_env_outputs then
LutExe.get_init_pres lut_mach
(* XXX Lire les valeurs des mémoires des programmes lutin dans fichier. *)
else
Value.OfIdent.empty
in
......@@ -51,4 +43,26 @@ let make_lut
data_state := new_ds;
to_subst_list lut_out new_ds.LutExe.outs
in
lut_in, lut_out, (fun _ -> ()), lut_step
let mems_in =
List.fold_left
(fun acc (vn,_vt) ->
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
)
[]
lut_in
in
let mems_out =
List.fold_left
(fun acc (vn,_vt) ->
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
)
[]
lut_out
in
lut_in, lut_out, (fun _ -> ()), lut_step, mems_in, mems_out
source/common/lutinRun.mli
View file @ 47b07b9e
......@@ -6,7 +6,6 @@
type vars = (string * string) list
val make_lut: ?verb:int -> ?libs:string list option -> ?step_mode: Lucky.step_mode ->
?seed: int option -> ?fair_mode:bool -> ?show_locals: bool -> ?