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.1 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
	    | Edges    -> Env_state.set_draw_mode  Env_state.Edges ; (n+1)
171
	    | Vertices -> Env_state.set_draw_mode  Env_state.Vertices ; (n+1)
172
	    | Help   -> options.help <- true ; (n+1)
173
174
175
176
177
	    | Output -> 
		let str = (Sys.argv.(n+1)) in
		  options.output <- str ;
		  n+2

178
179
180
181
182
183
184
	    | 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
185
186
187
188
189
190
191
	    | 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
192
193
      end
    with Not_found -> n
194
and
195
196
197
198
  (** 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"]]].
199

200
    Also set the lurette command line options if any.  
201
    *)
202
203
  (get_env_from_args: int -> string list list -> string list list) =
  fun n file_ll -> 
204
    if (n = arg_nb) then file_ll
205
    else
206
207
208
209
210
211
      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
212
	else
213
214
215
216
217
218
219
220
221
222
223
	  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)
224
225
226
and
  (main2 : int -> int -> int -> 'a) =
  fun s n p -> 
227
    (* Clean up tables as non-reg assert stuff migth have filled them *)
228
229
    let _ = Env_state.clear_all () in

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

234
    let rif = open_out options.output in
235
236
237
238
239
    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
240
241
242
    let local_var_name_and_type_list = 
      Util.sort_list_string_pair local_var_name_and_type_list_unsorted 
    in
243
    
244
    (* Initialisation of the random engine *)
245
246
    let seed = 
      if (options.user_seed = 0)
247
248
249
250
251
      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... *)
252
253
      else  options.user_seed
    in
254
255
256
257
258
      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;

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

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

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


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

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

and
315
  main_loop t s n p rif sut_output = 
316

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

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

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

338
(* Tries the sut `n*p'^nth times *)
339
340
341
342
343
344
345
346
347
348
349
350
351
  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
352

353
354
355
356
357
   let _ = 
    if options.oracle 
    then
      (* Tries the oracle `n*p'^nth times *)
      let (results: bool list) = 
358
	List.map2 (fun x y -> Lurette_stub.oracle_try x y) inputs_ord sut_outputs 
359
      in
360
	
361
	(* Aborts if at least one of the pairs (input, sut_output) breaks the oracle *)
362
363
364
	
	if (List.mem false results) 
	then (
365
	  (* print inputs and outputs of all wrong tuple *)
366
	    output_string stdout ("\n*** An assertion of the oracle has been violated" ^ 
367
			  " at step "  ^ (string_of_int t) ^
368
369
			  " with the following values:\n  ");
	    
370
371
372
373
374
375
	
	  let rec print_failures li lo lr =
	    let i = List.hd li
	    and o = List.hd lo
	    and r = List.hd lr 
	    in
376
377
		 if (not r) then
		   (
378
		     output_string stdout "\n* sut inputs:\n\t" ;
379
		     print_subst_list i stdout;
380
381
382
383
		     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) *)
384
385
		   )
		 else
386
387
388
389
390
		   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" ;
391
392
	    print_subst_list (Env_state.pre ()) stdout;
	    flush stdout;
393
	    flush rif;
394
395
396
	    if options.display_sim2chro
	    then Sim2chro.call_sim2chro options.output
	    else () ;	
397
398
399
	    output_string stdout ("\n*** Lurette stops because the oracle has been " 
		      ^ "violated at step " ^ (string_of_int t) ^ ".\n");
	    exit 2
400
401
	)
	else ()
402
  in
403

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

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

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

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

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

main ();;