Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

lurette.ml 14 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
** Copyright (C) 2001, 2002 - Verimag.
3
4
5
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
6
**
7
8
9
10
11
12
13
14
15
** File: lurette.ml
** Main author: jahier@imag.fr
*)

(*------------------------------------------------------------------------*)

open Util
open Formula
open List
16
17
18
19
20
21
22
23
open Command_line

(*------------------------------------------------------------------------*)

let (options:Command_line.optionsT) = {
  step_by_step = false ;
  display_local_var = true ;
  display_sim2chro = true ;
24
  user_seed = 0 ;
25
  verbose = false ;
26
  show_step = false ;
27
  help = false ;
28
  output = "lurette.rif" ;
29
  oracle = true 
30
31
}

32
33
34
(*------------------------------------------------------------------------*)

(** checks that 2 environments in parallel (i.e., that are not
35
    multiplied) do not share any generated variable names (i.e.,
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
    outputs and local vars).
*)
let (check_generated_vars : string list list -> unit) =
  fun env_llist -> 
    let vars_llist = 
      List.map 
	(fun env_list -> 
	   (List.fold_left
	      (fun acc env -> 
		 let (_, out, loc) = Env_state.var_names env in
		   List.rev_append acc (List.rev_append out loc)
	      )
	      []
	      env_list
	   )
	)
	env_llist
    in
    let vars_llist2 = List.map (Util.rm_dup) vars_llist in
    let vars_list = List.flatten vars_llist2 in
    let no_dup = Util.no_dup vars_list in
      if no_dup then () else
	(
	  print_string ("*** At least 2 groups of environments runned in " ^
			"parallel share a output or an local variable name, " ^
			"which is forbidden. Please fix that.\n");
	  flush stdout;
	  exit 2
	)

66

67
68
69
70
(** [check_var_decl_consistency out_env in_sut out_sut] checks the
  consistency of variable declarations made in the environment and the
  SUT. It raises an exception if the declarations are inconsistent.
*)
71
let (check_var_decl_consistency : (vn * string) list -> 
72
       (vn * string) list  -> unit) =
73
  fun in_sut out_sut ->
74
75
    let in_env_unsorted = Env_state.in_env_unsorted () in
    let out_env_unsorted = Env_state.out_env_unsorted () in
76
77
78
    let in_env = Util.sort_list_string_pair in_env_unsorted in
    let out_env = Util.sort_list_string_pair out_env_unsorted in

79
80
81
82
83
84
    let in_env2 = 
      List.map (fun (vn, vt) -> (vn, (var_type_to_string vt))) in_env 
    and out_env2 = 
      List.map (fun (vn, vt) -> (vn, (var_type_to_string vt))) out_env 
    in

85
      Env_state.set_output_var_names out_env;
86
      if not(list_are_equals out_env2 in_sut) then
87
	(
88
	  output_string stderr "\nenv outputs: ";
89
	  Print.vn_str stderr out_env2;
90
	  output_string stderr "\nsut inputs: ";
91
	  Print.vn_str stderr in_sut;
92
93
	  output_string stderr 
	    "\n*** env outputs and sut inputs should be the same.\n";
94
95
	  flush stdout ;
	  assert false
96
	)
97
      else if not(list_are_equals in_env2 out_sut) then 
98
	(
99
	  output_string stderr "\nenv inputs: ";
100
	  Print.vn_str stderr in_env2;
101
	  output_string stderr "\nsut outputs: ";
102
	  Print.vn_str stderr out_sut;
103
104
	  output_string stderr 
	    "\n*** env inputs and sut outputs should be the same.\n";
105
106
	  flush stdout ;
	  assert false
107
108
109
110
111
112
113
114
115
	)
      else 
	()


(*------------------------------------------------------------------------*)

let arg_nb = (Array.length Sys.argv) 

116
117
external random_seed: unit -> int = "sys_random_seed";;

118
119
let rec (main : unit -> 'a) =
  fun _ ->
120
121
122
    Array.iter (fun x -> output_string stderr (x ^ " ")) Sys.argv;
    output_string stderr "\n";
    flush stderr;
123
    try
124
      if (arg_nb < 5) then output_string stderr usage 
125
126
      else
	let s = (cmd_line_string_to_int Sys.argv.(1) 
127
		   ("*** int expected as first argument. " ^ Sys.argv.(1) ^ " is not an int.") ) 
128
	and n = (cmd_line_string_to_int Sys.argv.(2) 
129
		   ("*** int expected as second argument. " ^ Sys.argv.(2) ^ " is not an int.") ) 
130
	and p = (cmd_line_string_to_int Sys.argv.(3) 
131
		   ("*** int expected as third argument. " ^ Sys.argv.(3) ^ " is not an int.") ) 
132
133
134
	in
	let res = main2 s n p in
	  if (not options.step_by_step && options.display_sim2chro) 
135
	  then Sim2chro.call_sim2chro options.output
136
	  else () ; 
137
138
	  res
    with 
139
	Failure(errmsg) -> 
140
	  if Env_state.verbose () then Env_state.dump_env_state_stat stdout;
141
142
143
	  print_string errmsg;
	  flush stdout;
	  exit 2
144
      | e ->
145
	  if Env_state.verbose () then Env_state.dump_env_state_stat stdout;
146
147
148
	  print_string (Printexc.to_string e);
	  flush stdout;
	  exit 2
149

150
151
152
153
154
155
156
157
158
159
and 
  (get_lurette_options: int -> int) =
  fun n -> 
    try 
      begin
	let opt = List.assoc Sys.argv.(n) Command_line.string_to_option in
	  match opt with
	      Step -> options.step_by_step <- true ; (n+1)
	    | NoStep -> options.step_by_step <- false ; (n+1)
		
160
161
	    | DisplayLocalVar   -> options.display_local_var <- true ; (n+1)
	    | NoDisplayLocalVar -> options.display_local_var <- false ; (n+1)
162
163
		
	    | Sim2chro  -> options.display_sim2chro <- true ; (n+1)
164
	    | NoSim2chro -> options.display_sim2chro <- false ; (n+1)
165

166
	    | NoOracle -> options.oracle <- false ; (n+1)
167
	    | Verbose  -> Env_state.set_verbose true; (n+1)
168
	    | ShowStep  -> options.show_step <- true ; (n+1)
169
	    | Inside    -> Env_state.set_draw_mode  Env_state.Inside ; (n+1)
170
171
	    | Edges    -> Env_state.set_draw_mode  Env_state.Edges ; (n+1)
	    | Help   -> options.help <- true ; (n+1)
172
173
174
175
176
	    | Output -> 
		let str = (Sys.argv.(n+1)) in
		  options.output <- str ;
		  n+2

177
178
179
180
181
182
183
	    | Seed ->
		let str = (Sys.argv.(n+1)) in
		  options.user_seed <- cmd_line_string_to_int str 
		    ("*** Error when calling lurette: an " ^
		     "integer is expected after the " ^
		     "option --with-seed\n") ;
		  n+2
184
185
186
187
188
189
190
	    | Precision ->
		let str = (Sys.argv.(n+1)) in
		  Util.precision :=(cmd_line_string_to_int str
		    ("*** Error when calling lurette: an " ^
		     "integer is expected after the " ^
		     "option --precision\n")) ;
		  n+2
191
192
      end
    with Not_found -> n
193
and
194
195
196
197
  (** Returns the environment file names given at top-level into a
    list of list.  E.g., if the call [lurette 10 2 3 env1 x env2 x
    env3 env4] is done, then [get_env_from_args 10 []] (where 10 is
    the arg nb) returns [[["env1"; "env2"; "env3"]; ["env4"]]].
198

199
    Also set the lurette command line options if any.  
200
    *)
201
202
  (get_env_from_args: int -> string list list -> string list list) =
  fun n file_ll -> 
203
    if (n = arg_nb) then file_ll
204
    else
205
206
207
208
209
210
      let m = get_lurette_options n in
	(* m > n iff Sys.argv.(n) is an option *)
	if 
	  (m > n) 
	then 
	  get_env_from_args m file_ll
211
	else
212
213
214
215
216
217
218
219
220
221
222
	  let arg = Sys.argv.(m) in
	    if 
	      (arg = "x") 
	    then
	      match file_ll with
		  sl::sll -> 
		    let env = Sys.argv.(n+1) in
                      get_env_from_args (n+2) ((env::sl)::sll)
		| []  -> assert false
	    else 
	      get_env_from_args (n+1) ([arg]::file_ll)
223
224
225
and
  (main2 : int -> int -> int -> 'a) =
  fun s n p -> 
226
    (* Clean up tables as non-reg assert stuff migth have filled them *)
227
228
    let _ = Env_state.clear_all () in

229
    (* Initialisation of `Env_state.luc_state' *)
230
    let env_llist = (get_env_from_args 4 []) in
231
    let () = Env_state.read_env_state env_llist in
232

233
    let rif = open_out options.output in
234
235
236
237
238
    let local_var_name_and_type_list_unsorted0 = Env_state.loc_env_unsorted () in
    let local_var_name_and_type_list_unsorted = 
      List.map (fun (vn, vt) -> (vn, (var_type_to_string vt)))
	local_var_name_and_type_list_unsorted0
    in
239
240
241
    let local_var_name_and_type_list = 
      Util.sort_list_string_pair local_var_name_and_type_list_unsorted 
    in
242
    
243
    (* Initialisation of the random engine *)
244
245
    let seed = 
      if (options.user_seed = 0)
246
247
248
249
250
      then 
	let s =(random_seed ()) in
	  if s >= 0 then s else (-s)
	    (* XXX To turn around a bug in glade where it 
	       can not accept negative seeds... *)
251
252
      else  options.user_seed
    in
253
254
255
256
257
      check_generated_vars env_llist;
      
      check_var_decl_consistency Lurette_stub.sut_input_var_name_and_type_list 
	Lurette_stub.sut_output_var_name_and_type_list;

258
      Random.init seed ;
259
      output_string stdout 
260
	("\nThe random engine was initialized with the seed " ^
261
	 (string_of_int seed) ^  "\n ");
262
      flush stdout ;      
263

264
      (* Initialisation of the sut and the oracle *)
265
266
      Lurette_stub__sut_idl.lurette_stub__sut_init ();
      Lurette_stub__oracle_idl.lurette_stub__oracle_init ();
267
      
268
      (* Sim2chro *)
269
      if options.step_by_step then (
270
	Show_env.luc_to_dot 
271
272
273
                (flatten (Env_state.current_nodes ())) 
		[] 
		("environment" ^ (string_of_int (Hashtbl.hash Sys.argv)))
274
		(Env_state.graph ()) ;  
275
	Util.gv ("environment" ^ (string_of_int (Hashtbl.hash Sys.argv)) ^ ".ps");
276
	Sim2chro.put_var_decl 
277
278
	  ("lurette chronogram (" ^ 
	   (fold_left (fun acc str -> (acc ^ " " ^ str)) "" (flatten env_llist)) ^ ")")
279
280
	  Lurette_stub.sut_input_var_name_and_type_list 
	  Lurette_stub.sut_output_var_name_and_type_list 
281
	  local_var_name_and_type_list
282
283
	  stderr options.display_local_var;   
	flush stderr;
284
      )
285
286
287
288
289
290
291
292
293
294
      else
	(
	  Sim2chro.put_var_decl
	   ("lurette chronogram (" ^ 
	    (fold_left (fun acc str -> (acc ^ " " ^ str)) "" (flatten env_llist)) ^ ")")
	   Lurette_stub.sut_input_var_name_and_type_list 
	   Lurette_stub.sut_output_var_name_and_type_list 
	   local_var_name_and_type_list
	   rif options.display_local_var
	);
295
      (* Initializing Dd's libs. *)
296
297
      (*       Manager.disable_autodyn (Env_state.bdd_manager ()); *)
      
298
299
300
      (* Initializing the solution number table *)
      Env_state.set_sol_number 
	(Bdd.dtrue (Env_state.bdd_manager ())) (Util.one_sol, Util.zero_sol);
301

302
303
      Env_state.set_sol_number 
	(Bdd.dfalse (Env_state.bdd_manager ())) (Util.zero_sol, Util.one_sol);
304
305


306
307
      if not (options.help) 
      then main_loop 1 s n p rif (Hashtbl.create 0) ;
308

309
310
      flush stdout;
      flush rif;
311
      close_out rif; 
312
313

and
314
  main_loop t s n p rif sut_output = 
315

316
317
318
  let _ =
    if options.show_step then 
      output_string stdout ("\n--- step " ^ (string_of_int t) ^ ":\n"); 
319
    if Env_state.verbose () then
320
321
322
323
324
      List.iter  
        (fun n -> 
	   output_string stdout ("current nodes:" ^ (string_of_int n) ^ "\n "))
	(List.flatten (Env_state.current_nodes ()));
    flush stdout
325
  in  
326

327
(* Generates `n*p' inputs from the environment *)
328
  let (nl_call_inputs_loc: (Formula.node list list * Control.state * env_out * env_loc) list)
329
    = Env.env_try n p sut_output
330
331
  in

332
(* Extracts the inputs from the 4-uple *)
333
  let (inputs: env_out list) 
334
    = List.map (fun (_, _, input, _) -> input) nl_call_inputs_loc 
335
336
  in

337
(* Tries the sut `n*p'^nth times *)
338
339
340
341
342
343
344
345
346
347
348
349
350
  let input_list_ref = fst (split Lurette_stub.sut_input_var_name_and_type_list) in
  let inputs_ord = 
    map
      (fun input ->
	 (sort 
	    (fun (vn1, _) (vn2, _) -> Util.compare_list input_list_ref vn1 vn2) 
	    input)
      )
      inputs
  in
  let (sut_outputs: env_in list) = 
    List.map (Lurette_stub.sut_try) inputs_ord
  in
351

352
353
354
355
356
   let _ = 
    if options.oracle 
    then
      (* Tries the oracle `n*p'^nth times *)
      let (results: bool list) = 
357
	List.map2 (fun x y -> Lurette_stub.oracle_try x y) inputs_ord sut_outputs 
358
      in
359
	
360
	(* Aborts if at least one of the pairs (input, sut_output) breaks the oracle *)
361
362
363
	
	if (List.mem false results) 
	then (
364
	  (* print inputs and outputs of all wrong tuple *)
365
	    output_string stdout ("\n*** An assertion of the oracle has been violated" ^ 
366
			  " at step "  ^ (string_of_int t) ^
367
368
			  " with the following values:\n  ");
	    
369
370
371
372
373
374
	
	  let rec print_failures li lo lr =
	    let i = List.hd li
	    and o = List.hd lo
	    and r = List.hd lr 
	    in
375
376
		 if (not r) then
		   (
377
		     output_string stdout "\n* sut inputs:\n\t" ;
378
		     print_subst_list i stdout;
379
380
381
382
		     output_string stdout "\n* sut outputs:\n\t" ;
		     print_env_in o stdout
		       (* XXX Should I print them all?  *)
(* 		       print_failures (List.tl i, List.tl o, List.tl r) *)
383
384
		   )
		 else
385
386
387
388
389
		   print_failures (List.tl li) (List.tl lo) (List.tl lr)
	  in
	    print_failures inputs sut_outputs results ;

	    output_string stdout "\n* pre:\n\t" ;
390
391
	    print_subst_list (Env_state.pre ()) stdout;
	    flush stdout;
392
	    flush rif;
393
394
395
	    if options.display_sim2chro
	    then Sim2chro.call_sim2chro options.output
	    else () ;	
396
397
398
	    output_string stdout ("\n*** Lurette stops because the oracle has been " 
		      ^ "violated at step " ^ (string_of_int t) ^ ".\n");
	    exit 2
399
400
	)
	else ()
401
  in
402

403
  let previous_nodes = (Env_state.current_nodes ()) in
404

405
(* Chooses among the `n*p' possible pairs (input, ouput) *)
406
  let ran = Random.int (n*p) in
407
  let new_sut_output = List.nth sut_outputs ran in
408
409
  let (nll, call, _, loc) = List.nth nl_call_inputs_loc ran in
  let input = List.nth inputs_ord ran in
410
    
411
(* Performs the steps *)
412
413
414
415
416
  let _ = Lurette_stub.sut_step 
	    (sort 
	       (fun (vn1, _) (vn2, _) -> Util.compare_list input_list_ref vn1 vn2) 
	       input) 
  in
417
418
419
420
421
  let _ = 
    if (options.oracle) 
    then Lurette_stub.oracle_step input new_sut_output 
    else true 
  in
422
    Env.env_step nll call input loc ;
423
424

    let str =  
425
      if (options.step_by_step) then ( 
426
	if (previous_nodes <> Env_state.current_nodes ()) then 
427
	  Show_env.luc_to_dot (flatten (Env_state.current_nodes ()))
428
429
430
	    (flatten previous_nodes) ("environment"  
				      ^ (string_of_int (Hashtbl.hash Sys.argv))) 
	    (Env_state.graph ());
431
	Sim2chro.put_current_step_values  
432
433
	  stdout t input new_sut_output (Env_state.local ()) options.display_local_var
	  Lurette_stub.sut_output_var_name_and_type_list ; 
434
	output_string stdout 
435
436
437
438
	  "\nOne more loop ? [type any char to stop, `CR' to continue]\n";  
	read_line () 
      ) 
      else ( 
439
	Sim2chro.put_current_step_values
440
441
	       rif t input new_sut_output (Env_state.local ()) options.display_local_var
	       Lurette_stub.sut_output_var_name_and_type_list ;
442
	""
443
      ) 
444
    in
445

446
      (* Updates pre vars *)
447
      Env.update_pre new_sut_output input loc ;
448

449
450
      (* Clean-up cached info that depend on pre or inputs *)
      Env_state.clear_step ();
451
      
452
      (* Decides whether to loop once more *)
453
      if ((str = "" || str = " ") && (s > t))  
454
455
      then main_loop (t+1) s n p rif new_sut_output 
      else 
456
457
458
459
460
	(
	  output_string stdout 
	   "\n ==> The test completed; no property has been violated.\n";
	  flush stdout;
	)
461
462
463
464
465
466
;;
      

main ();;