runDirect.ml 20.1 KB
Newer Older
1
2
3
4

open LutExe
open LtopArg

5
type vars = (string * Data.t) list
6
7


8
(* returns a \ b *)
9
10
let list_minus a b =  List.filter (fun v -> not (List.mem v b)) a

11
(* returns a U b *)
12
13
let list_union a b =
  List.fold_left (fun acc x -> if (List.mem x acc) then acc else x::acc) a b
14

15
16
17
18
19
(* I defined mine because i need to know the seed that has been drawn by self_init. *)
let random_seed () =
  let () = Random.self_init () in
    Random.int 10000000

20
21
(* to be able to dump cov info if the exec is stopped by a ctrl-c. *)
let cov_ref = ref None
22
23
24
let gnuplot_pid_ref = ref None
let gnuplot_oc = ref None

25
(* Returns luciole io if necessary *)
26
27
let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> 
                    int * (vars * vars) option) =
28
29
30
31
32
33
  fun env_in env_out sut_in sut_out oracle_in oracle_out -> 
    (* cf lurette.set_luciole_mode_if_necessary to add a call to luciole *)
    
    let missing_sut_in = list_minus sut_in env_out
    and missing_env_in = list_minus env_in sut_out
    and missing_oracle_in = list_minus oracle_in (sut_out @env_out)  in
34
35
    let luciole_out = list_union missing_sut_in missing_env_in in 
    let luciole_in = list_minus (env_out@sut_out) luciole_out in 
36
      (*     let luciole_in = [] in  *)
37
      
38
39
40
    let vars_to_string vars = 
      String.concat "," (List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) vars) 
    in
41
42
      if missing_sut_in <> [] then (
        let missing_str = vars_to_string missing_sut_in in
43
44
45
          Printf.printf "Some variables are missing in input of the SUT: %s\n" missing_str
      ) ;
      if missing_env_in <> [] then (
46
        let missing_str = vars_to_string missing_env_in in
47
48
49
          Printf.printf "Some variables are missing in input of lutin: %s\n" missing_str
      );
      if luciole_out <> [] then (
50
51
        Printf.printf "try with luciole!\n";
        0, Some(luciole_in,luciole_out)
52
53
54
      ) 
      else if missing_oracle_in <> [] then (
        let missing_str = vars_to_string missing_oracle_in in
55
56
          Printf.printf "Some variables are missing in input of the oracle: %s\n"
                        missing_str;
57
          2,None
58
59
      ) 
      else (
60
        if List.mem ("Step") (fst(List.split luciole_in)) then (
61
62
          Printf.printf
            "*** You cannot use the name 'Step' for a variable with lurette, sorry.\n";
63
64
65
66
67
          flush stdout;
          2,None
        ) else (
          Printf.eprintf "RP Variables are compatible.\n";
          flush stderr;
68
          0, if args.luciole_mode then Some(luciole_in, ["Step",Data.Bool]) else None
69
        )
70
71
      )

72
73
type ctx = Event.t
type e = Event.t
74
open RdbgPlugin
75
76
let (make_rp_list : reactive_program list -> 
      vars list * vars list * (string -> unit) list * 
77
        (Data.subst list -> Data.subst list) list * 
78
        (Data.subst list -> ctx -> (Data.subst list -> ctx -> Event.t) ->
79
         Event.t) list * Data.subst list list * Data.subst list list) =
80
  fun rpl -> 
81
    let add_init init (a,b,c,d,e) = (a,b,c,d,e,init,init) in
82
    let aux rp = 
83
      let plugin =
84
        match rp with
85
(*           | LustreV6(prog,node) -> add_init [] (LustreRun.make_v6 prog node) *)
erwan's avatar
erwan committed
86
          | LustreV6(args) -> Lv6Run.make args
87
88
89
90
          | LustreV4(prog,node) -> LustreRun.make_v4 prog node
          | LustreEc(prog)      -> LustreRun.make_ec prog
          | LustreEcExe(prog)   -> LustreRun.make_ec_exe prog
          | Socket(addr, port)  -> LustreRun.make_socket addr port
91
          | SocketInit(addr, port) -> LustreRun.make_socket_init addr port 
92
          | Ocaml(cmxs) -> OcamlRun.make_ocaml cmxs
93
94
95
96
97
          | Lutin(args) -> LutinRun.make args
      in
      let ins, outs, kill, step, step_dbg, initin, initout =
        plugin.inputs,plugin.outputs,plugin.kill,plugin.step,plugin.step_dbg,
        plugin.init_inputs,plugin.init_outputs
98
99
100
      in
      let step = if args.debug_ltop then 
        let (string_of_subst : Data.subst -> string) =
101
          fun (str, v) -> str ^ "<-" ^ (Data.val_to_string Util.my_string_of_float v)
102
103
        in
        let sl2str sl = String.concat "," (List.map string_of_subst sl) in
104
105
106
107
108
109
          (fun sli  -> 
             let slo = step sli in
               Printf.eprintf "[%s] step(%s) = (%s) \n" 
                 (reactive_program_to_string rp) (sl2str sli) (sl2str slo);
               flush stderr;
               slo)
110
      else
111
112
        step 
      in
113
        ins, outs, kill, step, step_dbg, initin, initout     
114
    in
115
      Util.list_split7 (List.map aux rpl)
116
    
117
118
119
120
121
122
123
124

type cov_opt = 
    NO (* NoOracle *) 
  | OO (* OracleOnly *) 
  | OC of Coverage.t
exception OracleError of string
exception SutStop of cov_opt

125
126
(* Transform a map on a function list into CPS *)
let (step_dbg_sl : 
127
128
  (Data.subst list -> ctx -> 
   (Data.subst list -> ctx -> Event.t) -> Event.t) list -> 
129
130
131
132
133
134
135
136
137
138
139
140
      's list -> 'ctx  -> ('s list -> 'e) -> 'e) = 
  fun step_dbg_sl_l sl ctx cont -> 
    (* ouch! Celle-la est chevelue...  
       La difficulté, c'est de passer un 'List.map step' en CPS.
       Suis-je aller au plus simple ? En tout cas j'ai réussit :)
    *)
    let rec (iter_step  : 
               ('s list -> 'ctx  -> ('s list -> 'ctx  -> 'e) -> 'e) list -> 
              's list list -> 's list -> 'e) = 
      fun stepl res_stepl sl ->
        match stepl with
          | [] -> cont (List.flatten (res_stepl))
141
142
          | step::stepl ->
             step sl ctx (fun res_sl ctx -> iter_step stepl (res_sl::res_stepl) sl)
143
144
145
146
147
    in
      iter_step step_dbg_sl_l [] sl 



148
let (start : unit -> Event.t) =
149
150
  fun () ->
    (* Get sut info (var names, step func, etc.) *)
151
    let _ = if args.debug_ltop then LustreRun.debug := args.debug_ltop in
152
153
    let sut_in_l, sut_out_l, sut_kill_l, sut_step_sl_l, sut_step_dbg_sl_l, 
      sut_init_in_l, sut_init_out_l = make_rp_list args.suts 
154
155
156
157
    in
    let sut_kill msg = List.iter (fun f -> f msg) sut_kill_l in
    let sut_init_in = List.flatten sut_init_in_l in
    let sut_init_out = List.flatten sut_init_out_l in
158
159

    (* Get oracle info (var names, step func, etc.)*)
160
161
    let oracle_in_l, oracle_out_l, oracle_kill_l, oracle_step_sl_l, 
        oracle_step_dbg_sl_l, _, _ =
162
      make_rp_list args.oracles
163
    in
164
    let oracle_kill msg = List.iter (fun f -> f msg) oracle_kill_l in
165
    
166
    (* Get env info (var names, step func, etc.)*)
167
168
    let env_in_l, env_out_l, env_kill_l, env_step_sl_l, env_step_dbg_sl_l, 
      env_init_in_l, env_init_out_l = make_rp_list args.envs 
169
    in
170
    let env_kill msg = List.iter (fun f -> f msg) env_kill_l in
171
172
    let _env_init_in = Util.rm_dup (List.flatten env_init_in_l) in
    let _env_init_out = Util.rm_dup (List.flatten env_init_out_l) in
173

174
    let vars_to_string l = 
175
176
177
      String.concat "\n" (List.map (fun (vn,vt) -> 
        let vt = Data.type_to_string vt in
        Printf.sprintf "\t%s:%s" vn vt) l)
178
    in
179
180
181
182
183
184
    let flat_sut_in  = Util.rm_dup (List.flatten sut_in_l)
    and flat_sut_out = Util.rm_dup (List.flatten sut_out_l)
    and flat_env_in  = Util.rm_dup (List.flatten env_in_l)
    and flat_env_out = Util.rm_dup (List.flatten env_out_l)
    and flat_oracle_in  = Util.rm_dup (List.flatten  oracle_in_l)
    and flat_oracle_out = Util.rm_dup (List.flatten  oracle_out_l)
185
    in
186
    let _ = if args.verbose > 0 then
187
188
189
190
191
        let sut_input_str = vars_to_string flat_sut_in in
        let sut_output_str = vars_to_string flat_sut_out in
        let env_input_str = vars_to_string  flat_env_in in
        let env_output_str = vars_to_string flat_env_out in
        let oracle_input_str = vars_to_string flat_oracle_in in
192
        let oracle_output_str_l = List.map vars_to_string oracle_out_l in
193
        Printf.printf "sut input : \n%s\n"  sut_input_str;
194
        Printf.printf "sut output : \n%s\n" sut_output_str;
195
196
        Printf.printf "env input : \n%s\n"  env_input_str;
        Printf.printf "env output : \n%s\n"  env_output_str;
197
        Printf.printf "oracle(s) input : \n%s\n"  oracle_input_str;
198
199
        List.iter (fun str -> Printf.printf "oracle output : \n%s\n" str) 
                  oracle_output_str_l;
200
        flush stdout
201
    in
202
    (* Check var names and types compat. *)
203
    let res_compat, luciole_io_opt = 
204
205
      check_compat flat_env_in flat_env_out flat_sut_in flat_sut_out 
                   flat_oracle_in flat_oracle_out 
206
207
208
209
210
    in
    let (luciole_kill, luciole_step), luciole_outputs_vars =
      match luciole_io_opt with
        | None -> ((fun _ -> ()),(fun _ -> [])),[]
        | Some (luciole_in, luciole_out) -> 
211
212
          (LustreRun.make_luciole "./lurette_luciole.dro" luciole_in luciole_out), 
          luciole_out
213
    in
214
215
    let seed =
      match args.seed with
216
217
218
        | None -> random_seed ()
        | Some seed -> seed
    in
219
220
    let cov_init = (* XXX faut-il renommer les sorties de l'oracle ou raler en 
                     cas de clash ? *)
221
222
      if List.flatten oracle_out_l = [] then NO else 
        let oracle_out = List.flatten (List.map List.tl oracle_out_l) in
223
        if List.length oracle_out < 1 then OO else 
224
          let is_bool (_,t) = (t = Data.Bool) in
225
226
227
          let names = List.filter is_bool oracle_out in
          let names = fst (List.split names) in
          OC (Coverage.init names args.cov_file args.reset_cov_file)
228
229
    in
    let oc = open_out args.output in
230
231
232
    let sim2chro_oc = 
      if args.display_sim2chro then Util2.sim2chro_dyn () else open_out "/dev/null" 
    in
233
234
    let filter vals vars = 
      List.map (fun (n,t) -> n, 
235
236
237
238
239
240
        try List.assoc n vals
        with Not_found -> 
          let vars_str = String.concat ", " (List.map (fun (n,_) -> n) vals) in
          let msg = Printf.sprintf "Don't find %s in %s\n" n vars_str in
          failwith msg
      ) vars 
241
    in
242
243
244
245

    let rec check_oracles oracle_in_vals i oracle_out_l oracle_out_vals_l cov =
      let check_one_oracle = function 
        | [] -> assert false
246
        | (_, Data.B true)::tail -> tail
247
          
248
        | (_, Data.B false)::tail ->
249
250
251
252
253
          let msg = 
            match cov with 
                OC cov -> Coverage.dump_oracle_io oracle_in_vals tail cov 
              | _ -> ""
          in
254
255
256
          let msg = 
            Printf.sprintf "\n*** The oracle returned false at step %i\n%s" i msg 
          in
257
258
259
          print_string msg;
          flush stdout;
          if args.stop_on_oracle_error then raise (OracleError msg) else tail
260
261

        | (vn, vv)::_  -> 
262
          let vv = Data.val_to_string_type vv in
263
264
265
          let msg = Printf.sprintf 
            "The oracle first output should be a bool; but %s has type %s" vn vv in
          failwith msg
266
      in
267
268
269
270
271
272
273
274
275
276
277
278
      match cov with 
          NO -> NO
        | OO -> ignore (List.map check_one_oracle oracle_out_vals_l); OO
        | OC cov -> 
          let ll = List.map check_one_oracle oracle_out_vals_l in
          let cov =
            List.fold_left
              (fun cov other_oracle_out_vals ->
                Coverage.update_cov other_oracle_out_vals cov) cov ll
          in
          cov_ref := Some cov;
          OC cov
279
    in
280
281
282
283
284
    let update_cov cov = 
      match cov with 
        | NO -> ()
        | OO -> ()
        | OC cov -> 
285
286
287
          let str =
            String.concat ", " (List.map reactive_program_to_string args.oracles) 
          in
288
          Coverage.dump str args.output cov
289
    in
290
    (* The main loop *)
291
292
293
294
295
296
297
298
299
    let killem_all cov = 
      env_kill "quit\n";
      sut_kill "quit\n";
      luciole_kill "quit\n";
      oracle_kill "quit\n";
      close_out oc;
      close_out sim2chro_oc;
      update_cov cov;
    in
300
    let rec loop cov env_in_vals pre_env_out_vals ctx i () =
301
302
      if i > args.step_nb then (killem_all cov; raise (Event.End 0) ) 
      else
303
304
        let luciole_outs = luciole_step (env_in_vals@pre_env_out_vals) in
        let env_in_vals =  List.rev_append luciole_outs env_in_vals in
305
306
307
308
309
310
311
312
        if args.ldbg then (* XXX l'idéal serait de faire ce test à
                             l'exterieur de la boucle en passant la
                             fonction qui va bien selon le
                             mode. Apres tout, c'est l'un des
                             avantages du CPS... *)
          let edata = env_in_vals@pre_env_out_vals in
          let ctx = 
            { ctx with 
313
314
315
316
              Event.step = i;
              Event.name = "ltop";
              Event.depth = 1;
              Event.data = edata;
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
            }
          in
          let cont = loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs in
          step_dbg_sl env_step_dbg_sl_l env_in_vals ctx cont
        else
          let env_step_sl sl = List.flatten (List.map (fun f -> f sl) env_step_sl_l) in
          let env_out_vals = env_step_sl env_in_vals in
          loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs env_out_vals
    (*
      {
      step = i;
      data = [];
      next = (fun () -> loop2 cov env_in_vals pre_env_out_vals i luciole_outs env_out_vals);
      terminate = (fun () -> killem_all cov)
      }
    *)          
333
    and
334
        loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs env_out_vals =
335
336
337
338
      let env_out_vals = 
        try List.map (fun (v,vt) -> v,List.assoc v env_out_vals) flat_env_out 
        with Not_found -> env_out_vals
      in
339
      let env_out_vals = luciole_outs @ env_out_vals in
340
      let sut_in_vals = filter env_out_vals flat_sut_in in        
341
342
343
      if args.ldbg then       
        let edata = sut_in_vals@ env_out_vals in
        let ctx = { ctx with 
344
345
346
347
          Event.step = i;
          Event.name = "ltop";
          Event.depth = 1;
          Event.data = edata;
348
349
        } 
        in
350
351
352
        let cont = 
          loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs
        in
353
354
355
356
        step_dbg_sl sut_step_dbg_sl_l sut_in_vals ctx cont
      else
        let sut_step_sl sl = List.flatten (List.map (fun f -> f sl) sut_step_sl_l) in
        let sut_out_vals = sut_step_sl sut_in_vals in
357
358
359
360
        loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i
              luciole_outs sut_out_vals
    and loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i 
              luciole_outs sut_out_vals =
361
362
363
      let sut_out_vals = 
        try List.map (fun (v,vt) -> v,List.assoc v sut_out_vals) flat_sut_out 
        with Not_found -> sut_out_vals
364
365
366
367
368
369
370
371
372
      in
      let oracle_in_vals = 
        if args.delay_env_outputs 
        then List.rev_append pre_env_out_vals sut_out_vals 
        else List.rev_append     env_out_vals sut_out_vals 
      in
      let oracle_in_vals = List.rev_append luciole_outs oracle_in_vals in
      let oracle_in_vals = filter oracle_in_vals flat_oracle_in in
      let oracle_out_vals_l = List.map (fun f -> f oracle_in_vals) oracle_step_sl_l in
373
374
375
376
377
378
379
380
381
382

      (*       let oracle_out_vals = List.flatten oracle_out_vals_l in *)
      let oracle_out_vals_l = 
        try List.map2 
              (fun oracle_out oracle_out_vals -> 
                List.map (fun (v,vt) -> v,List.assoc v oracle_out_vals) oracle_out
              ) 
              oracle_out_l
              oracle_out_vals_l
        with Not_found -> oracle_out_vals_l
383
      in
384
      let print_val (vn,vv) = Data.val_to_string Util.my_string_of_float vv in
385
      Printf.fprintf oc "#step %d\n" i;
386

387
388
      if args.delay_env_outputs then (
        output_string oc (String.concat " " (List.map print_val (pre_env_out_vals)));
389
390
        output_string 
          sim2chro_oc (String.concat " " (List.map print_val (pre_env_out_vals)));
391
392
393
394
395
396
397
398
      )
      else (
        output_string oc (String.concat " " (List.map print_val env_out_vals));
        output_string sim2chro_oc (String.concat " " (List.map print_val env_out_vals));
      );
      output_string oc (if env_out_vals <> [] then " #outs " else "#outs ");
      output_string oc (String.concat " " (List.map print_val sut_out_vals));
      output_string oc "\n";
399
400
401
402
403
      List.iter (fun l -> 
        output_string oc "#oracle_outs ";
        output_string oc (String.concat " " (List.map print_val l));
        output_string oc "\n";
      ) oracle_out_vals_l;
404
      flush oc;
405

406
407
408
409
410
      output_string sim2chro_oc "#outs ";
      output_string sim2chro_oc (String.concat " " (List.map print_val sut_out_vals));
      output_string sim2chro_oc "\n";
      flush sim2chro_oc;
      
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
      if not args.go && args.display_gnuplot then (
        if  i = 0 then (
          let oc, pid = 
            GnuplotRif.terminal := GnuplotRif.Wxt;
            GnuplotRif.verbose := args.verbose>1;
            GnuplotRif.dynamic := true;
            GnuplotRif.rif_file := args.output;
            GnuplotRif.f ()
          in
          gnuplot_pid_ref := Some pid;
          gnuplot_oc := Some oc
        ) 
        else 
          (match !gnuplot_oc with
            | None -> ()
            | Some oc -> output_string oc "replot\n"; flush oc)
      );
428
      if args.ldbg then (
429
        let edata = sut_out_vals@env_out_vals@(List.flatten oracle_out_vals_l) in
430
431
432
433
434
435
436
437
438
439
        let term () = 
          (match !gnuplot_pid_ref with
            | None -> ()
            | Some pid ->
              print_string "Killing gnuplot...\n"; flush stdout;
              Unix.kill pid Sys.sigkill;
              gnuplot_oc := None;
              gnuplot_pid_ref := None); 
          killem_all cov
        in
440
        let enb = ctx.Event.nb in
441
        let ctx = { ctx with 
442
443
444
445
446
447
          Event.nb = ctx.Event.nb+1;
          Event.step = i;
          Event.name = "ltop";
          Event.depth = 1;
          Event.data = edata;
          Event.terminate = term;
448
449
450
        } 
        in
        {
451
          Event.nb = enb;
452
453
454
455
          Event.step = i;
          Event.kind = Event.Ltop;
          Event.depth = 1;
          Event.data = edata;
456
457
458
459
          Event.name = "rdbg";
          Event.lang = "";
          Event.inputs=[];
          Event.outputs=[];
460
          Event.locals = [];
461
          Event.sinfo=None;
462
463
464
465
466
467
468
469
470
471
472
          Event.next = 
            (fun () ->
              loop (check_oracles oracle_in_vals i oracle_out_l oracle_out_vals_l cov) 
                sut_out_vals env_out_vals ctx (i+1) () 
            );
          Event.terminate = term
        }
      )
      else
        loop (check_oracles oracle_in_vals i oracle_out_l oracle_out_vals_l cov) 
          sut_out_vals env_out_vals ctx (i+1) () 
473
    in
474

475
    let loc = None in
476
    let _ = 
477
478
      if args.compute_volume then Solver.set_fair_mode () 
      else Solver.set_efficient_mode ();
479
480
481
      !Solver.init_snt ();
      Random.init seed;

482
483
      Rif.write oc ("# This is lurette Version " ^ Version.str ^
                      " (\"" ^Version.sha^"\")\n");
484
485
      Rif.write oc ("#seed "^(string_of_int seed)^"\n");

486
      RifIO.write_interface oc 
487
        (luciole_outputs_vars@flat_env_out) flat_sut_out loc (Some oracle_out_l);
488
      Rif.flush oc;
489

490
      RifIO.write_interface sim2chro_oc 
491
        (luciole_outputs_vars@flat_env_out) flat_sut_out loc (Some oracle_out_l);
492
      Rif.flush sim2chro_oc;
493
494
    in
    let ctx =
495
      {
496
497
498
499
500
501
        Event.nb = 1;
        Event.step = 1;
        Event.name = "ltop";
        Event.depth = 1;
        Event.inputs = [];
        Event.outputs = [];
502
        Event.locals = [];
503
504
505
506
507
508
        Event.data = [];
        Event.terminate = (fun () -> killem_all cov_init);
        Event.lang = "";
        Event.next = (fun () -> assert false);
        Event.kind = Event.Ltop;
        Event.sinfo = None;
509
510
      }
    in
511
    let (first_event : Event.t) =
512
513
514
      let res = 
        try 
          if res_compat = 0 then
515
            loop cov_init sut_init_out sut_init_in ctx 0 ()
516
517
518
519
          else 
            raise(Event.End res_compat) 
        with 
          | SutStop cov -> 
520
521
            print_string "The SUT stopped\n";
            flush stdout;
522
523
            update_cov cov;
            raise(Event.End 1)
524
525

          | OracleError str -> 
526
527
528
            print_string str;
            flush stdout;
            raise(Event.End 2)
529
530

          | Failure str -> 
531
            print_string ("Failure occured in lurette: "^str);
532
            flush stdout;
533
            raise(Event.End 2) 
534
          | Event.End i -> raise(Event.End (10*i))
535
          | e -> 
536
537
538
            print_string (Printexc.to_string e);
            flush stdout;
            raise(Event.End 2)
539
      in
540
      res
541
    in
542
    first_event
543

544
545
(* exported *)
let (clean_terminate : unit -> unit) =
546
547
  fun () -> 
    let str = String.concat ", " (List.map reactive_program_to_string args.oracles) in
548
549
550
551
552
553
554
555
556
557
558
559
    (match !cov_ref with 
      | None -> ()
      | Some cov -> Coverage.dump str args.output cov);
    (match !gnuplot_pid_ref with
      | None -> ()
      | Some pid ->
        print_string "Killing gnuplot...\n"; 
        flush stdout;
        Unix.kill pid Sys.sigkill;
        gnuplot_pid_ref := None
    )

560