gen_stubs.ml 12.9 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
** Copyright (C) - Verimag.
3
** This file may only be copied under the terms of the GNU Library General
4
** Public License
5
6
**-----------------------------------------------------------------------
**
7
** File: gen_stubs.ml
8
** Author: jahier@imag.fr
9
**
10
11
*)

12
open List
13
14
open Gen_stubs_common

15

16
17
18
19
(** 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.
20

21
22
23
    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:
24

25
26
    //MODULE: <module name> n m
    //    where [n] is the input var number, and [m] the output var one
27

28
  //IN:  <C type of the first input var> <a C identifier for the first input var>
29

30
  ...
31

32
  //IN:  <C type of the nth input var> <a C identifier for the nth input var>
33

34
  //OUT: <C type of the first output var> <a C identifier for the first output var>
35
36

    ...
37

38
  //OUT: <C type of the mth output var> <a C identifier for the mth output var>
39
40
41
42
43
*)



(****************************************************************************)
44
(** Generates a fake oracle (that always returns true) so that the
45
  user does not have to write it if he does not have any assertion to
46
  check. It can also be used as a skeleton.
47
*)
48
49
let (gen_a_fake_oracle : string -> string -> string -> compiler -> string -> bool) =
  fun user_dir tmp_dir sut_node compiler sut_h ->
50
(*     try *)
51
52
      let (tdl, sut_h, sut_vi, sut_vo) =
	match compiler with
53
54
	  | VerimagV6
	  | VerimagV4 ->
55
56
57
58
59
60
61
62
63
64
65
66
67
	      let (tdl, vi, vo) = Parse_poc.get_vn_and_ct_list sut_h in
		(tdl, sut_h, vi, vo)
	  | Scade ->
	      let (tdl, vi, vo) = Parse_c_scade.get_vn_and_ct_list sut_h sut_node compiler in
		(tdl, sut_h, vi, vo)
	  | ScadeGUI ->
	      let (tdl, vi, vo) = Parse_c_scade.get_vn_and_ct_list sut_h sut_node compiler in
		(tdl, sut_h, vi, vo)
	  | Sildex -> 
	      let (tdl, vi, vo) = Parse_sildex.get_vn_and_ct_list sut_h in
		(tdl, sut_h, vi, vo)
      in
      let vn_ct_l = (List.append sut_vi sut_vo)  in
68
      let vn_st_str_l =
69
70
	List.map
	  (fun (vn, ct) ->
71
	   (vn ^ ":" ^ (c_type_to_scade_type tdl ct))
72
73
74
75
76
77
78
79
80
81
82
83
84
	  )
	  vn_ct_l
      in
      let oc = 
	open_out (Filename.concat user_dir (sut_node ^ "_always_true.lus")) 
      in
      let put s = output_string oc s in
	
	put "-- Automatically generated from ";
	put sut_h ;
	put "\n-- Migth be overrided: rename it if you modify it." ;
	put "\n\n";
	put ("node " ^ sut_node ^ "_always_true(\n\t");
85
	put (format_string_list "; \n\t" vn_st_str_l) ;
86

87
88
89
90
91
	put (") returns (" ^ sut_node ^ "__ok:bool);\n");
	put ("let \n  " ^ sut_node ^ "__ok = true ; \ntel\n");
	put "\n";
	close_out oc;
	true
92
93
94
(*     with e ->  *)
(*       output_string stderr (Printexc.to_string e); *)
(*       false *)
95

96
97


98
99
(****************************************************************************)
(****************************************************************************)
100

101
let usage = "
102
usage: gen_stub <sut> <sut_node> <sut_compiler> [<oracle> <oracle_node> \
103
<oracle_compiler>] dir
104

105
 where:
106
  o <sut> is the name of the SUT file
107
108
109
  o <sut_node> is the name of the main node
  o <sut_compiler> is the name of the lustre compiler (= \"verimag\" or \"scade\")
  o Ditto for <oracle>, <oracle_node>, and <oracle_compiler>
110
    The arguments related to the oracle are optionals.
111
112
113
114
  o <dir> is the name of the directory where to generate files

gen_stubs basically performs the following actions:
  o compile lustre/saofdm files, if necessary
115
  o generate a fake oracle (a lustre file), if not available
116
117
118
  o generate stub code (lurette__sut.c) so that lurette is
     - aware of sut variable names and types
     - able to call sut step and try functions
119

120
nb: gen_stubs is not meant to be used directly by end-users.
121
"
122

123
let compile_lustre_program_if_needed
124
125
  lustre_prog0 lustre_node compiler user_dir tmp_dir header_file =
  let prog_dir = Filename.dirname lustre_prog0 in
126
  let save_dir = Sys.getcwd () in
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
  let res =
    let (gen_c_file, gen_h_file) =
      ((Filename.chop_extension header_file) ^ ".c", header_file)
    in
    let lustre_prog_stat = 
      if Sys.file_exists lustre_prog0 then (Unix.stat lustre_prog0) else
	(
	  print_string  ("*** " ^ lustre_prog0 ^ " does not exist.\n");
	  flush stdout;
	  exit 2
	)
    in

    let lustre_prog =
      if
	(
	  (Filename.check_suffix lustre_prog0 ".etp") ||
	  (Filename.check_suffix lustre_prog0 ".vsp")
	)
      then 
	(if
148
	   Util2.etp_to_saofdm lustre_prog0 lustre_node
149
150
151
	 then
	   (Filename.chop_extension lustre_prog0) ^ ".saofdm"
	 else
152
	   exit 100
153
154
155
156
157
158
159
160
161
162
163
164
165
166
	)
      else
	lustre_prog0
    in
      Sys.chdir prog_dir;
      
      if
	(Filename.check_suffix lustre_prog ".c")
      then
	(*
	  if users provide C files for the sut and the oracle, we copy
	  them (.c and .h) to the tmp dir where they are expected to be
	*)
	(
167
	  (Util2.cp 
168
169
170
	     ((Filename.chop_suffix lustre_prog ".c") ^ ".h") 
	     tmp_dir stdout stderr
	  ) &&
171
	  (Util2.cp lustre_prog  tmp_dir stdout stderr)
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
	)
      else if
	(Filename.check_suffix lustre_prog ".saofdm")
	&&
	(
	  not (Sys.file_exists gen_c_file)
	  ||
	  not (Sys.file_exists gen_h_file)
	  ||
	  ((Unix.stat gen_c_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
	  ||
	  ((Unix.stat gen_h_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
	)
      then
	(
187
188
189
	  (* 	Util2.scade_cg lustre_prog lustre_node  tmp_dir;  *)
	  if Util2.scade2lustre lustre_prog then
	    (Util2.lustre2C
190
191
192
	       ((Filename.chop_extension lustre_prog) ^ ".lus")
	       lustre_node tmp_dir)
	  else
193
	    exit 101
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
	)
      else if
	(Filename.check_suffix lustre_prog ".lus")
	&&
	(
	  not (Sys.file_exists gen_c_file)
	  ||
	  not (Sys.file_exists gen_h_file)
	  ||
	  ((Unix.stat gen_c_file).Unix.st_mtime > lustre_prog_stat.Unix.st_mtime)
	  ||
	  ((Unix.stat gen_h_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
	)
      then
	(* if no .h or .c exists, or if they are too old, we (re)generate them. *)
	(
	  match compiler with
211
	  | VerimagV6 ->
212
213
214
215
		output_string stderr (
		  "No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
		  ".h exist(s), so I try to compile " ^ lustre_prog ^
		  " with node " ^ lustre_node ^
erwan's avatar
erwan committed
216
		  " with lv6 -ec and ec2c...\n");
217
218
219
220
221
222
223
224
225
226
		if Util2.lv62ec lustre_prog lustre_node user_dir then
		  Util2.ec2c lustre_node tmp_dir
		else
		  exit 102
	  | VerimagV4 ->
		output_string stderr (
		  "No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
		  ".h exist(s), so I try to compile " ^ lustre_prog ^
		  " with node " ^ lustre_node ^
		  " with lus2ec and ec2c...\n");
227
228
		if Util2.lus2ec lustre_prog lustre_node user_dir then
		  Util2.ec2c lustre_node tmp_dir
229
		else
230
		  exit 103
231
232
233
234
235
236
237

	    | ScadeGUI ->
		output_string stderr (
		  "No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
		  ".h exist(s), so I try to compile " ^ lustre_prog ^
		  " with node " ^ lustre_node ^
		  " with the lustre2C scade code generator.\n");
238
		Util2.lustre2C
239
240
		  ((Filename.chop_extension lustre_prog) ^ ".lus")
		  lustre_node tmp_dir
241
		
242
243
244
245
	    | Scade ->
		output_string stderr (
		  "No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
		  ".h exist(s), so I try to compile " ^ lustre_prog ^
246
		  "with node " ^ lustre_node ^
247
		  " with the lustre2C scade code generator.\n");
248
		Util2.lustre2C
249
250
251
252
253
254
255
		  ((Filename.chop_extension lustre_prog) ^ ".lus")
		  lustre_node tmp_dir
		  
	    | Sildex -> (* XXX TODO *)
		output_string stderr (
		  "Lurette do not know how to compile Sildex code " ^
		  "yet. \nPlease provide the C files (for the sut and the oracle).\n");
256
		exit 104
257
258
259
260
261
262
263
264
		  
	)
      else
	(* No compilation seems to be required *)
	true
  in
    Sys.chdir save_dir;
    res
265

266
267

(****************************************************************************)
268

269
(* Sorts oracle var w.r.t. to their order in ref_list in order to check
270
   var names constency. *)
271
let (sort_vars: string list -> vn_ct list -> vn_ct list) =
272
273
274
  fun ref_list var_list ->
    List.sort
    (fun (vn1, t1) (vn2, t2) -> Util.compare_list ref_list vn1 vn2)
275
    var_list
276

277

278

279
(****************************************************************************)
280

281
282
283
284
let (gen_stubs_file : string -> string -> compiler -> string -> compiler -> 
       string -> string -> bool -> bool) =
  fun tmp_dir sut sut_compiler oracle oracle_compiler sut_h oracle_h 
      oracle_is_present ->
285
(*     try *)
286
287
      let sut_m = (Filename.basename sut) in
      let oracle_m = (Filename.basename oracle) in
288

289
290
      (* Get var names and types of the sut *)
      let (sut_tdl, sut_vi, sut_vo) =
291
	match sut_compiler with
292
293
	  | VerimagV6 
	  | VerimagV4 ->
294
295
	      let (x1, x2, x3) = Parse_poc.get_vn_and_ct_list sut_h in
		(x1, x2, x3)
296
	  | Scade ->
297
298
299
300
301
	      let (x1, x2, x3) = Parse_c_scade.get_vn_and_ct_list sut_h sut_m sut_compiler in
		(x1, x2, x3)
	  | ScadeGUI ->
	      let (x1, x2, x3) = Parse_c_scade.get_vn_and_ct_list sut_h sut_m sut_compiler  in
		(x1, x2, x3)
302
	  | Sildex ->
303
304
	      Parse_sildex.get_vn_and_ct_list sut_h
      in
305

306
307
308
309
310
311
312
313
      (* Get var names and types of the oracle *)
      let (oracle_tdl, oracle_vi, oracle_vo) =
	if 
	  not oracle_is_present 
	then
	  ([],[],[])
	else
	  match oracle_compiler with
314
315
	    | VerimagV6
	    | VerimagV4 ->
316
317
318
319
320
321
322
323
324
325
326
		let (x1, x2, x3) = Parse_poc.get_vn_and_ct_list oracle_h in
		  (x1, x2, x3)
	    | Scade ->
		let (x1, x2, x3) = Parse_c_scade.get_vn_and_ct_list oracle_h oracle_m oracle_compiler in
		  (x1, x2, x3)
	    | ScadeGUI ->
		let (x1, x2, x3) = Parse_c_scade.get_vn_and_ct_list oracle_h oracle_m oracle_compiler in
		  (x1, x2, x3)
	    | Sildex ->
		Parse_sildex.get_vn_and_ct_list oracle_h
      in
327

328
329
330
331
332
      (* sort vars according to the ordering in the sut (useless?) *)
      let v_list_ref = append (fst (split sut_vi)) (fst (split sut_vo)) in

	(
	  match sut_compiler with
333
334
	    | VerimagV6
	    | VerimagV4 ->
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
		Gen_stubs_poc.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo
	    | ScadeGUI ->
		Gen_stubs_scade.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo sut_h
	    | Scade ->
		Gen_stubs_scade.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo sut_h
	    | Sildex ->
		Gen_stubs_sildex.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo 
	);

	(* Update the stub files iff they have changed to avoid unnecessary
	   re-compilations *)
	update_file
	  (Filename.concat tmp_dir "lurette__sut.c.new")
	  (Filename.concat tmp_dir "lurette__sut.c");
	true
350
351
352
353
(*     with e ->  *)
(*       output_string stdout (Printexc.to_string e); *)
(*       flush stdout; *)
(*       false *)
354

355
(****************************************************************************)
356

357
(** gen_stubs top-level function *)
358
let (main : unit -> 'a) =
359
  fun _ ->
360

361
    let arg_nb = (Array.length Sys.argv) - 1 in
362
363
364
365
366
367

      output_string stderr "gen_stubs ";
      Array.iter (fun x -> output_string stderr (x ^ " ")) Sys.argv;
      output_string stderr "\n";
      flush stderr;

368
369
370
371
372
373
374
      (*       if true then *)
      (* 	for i = 0 to (arg_nb-1) do *)
      (* 	  print_string ("\n\targ" ^ (string_of_int i) ^ " = " ^ (Sys.argv.(i))); *)
      (* 	  print_string "\n"; *)
      (* 	done; *)
      (*       flush stdout; *)
	   
375

376
      if
377
378
379
380
381
382
383
384
	     (
	       arg_nb >= 1
	       &&
	       ((Sys.argv.(1) = "--help") || (Sys.argv.(1) = "-help")  ||
	          (Sys.argv.(1) = "-h")
	       )
	     )
	     || arg_nb = 0
385
      then
386
387
388
389
	     (
	       output_string stdout usage;
	       true
	     )
390
      else
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
	     (
	       if Sys.argv.(1) = "lurette__sut" then
	         (
	           output_string stderr (
		          "You cannot call your file lurette__sut.lus, sorry ;" ^
		            "please rename it.\n");
	           exit 2
	         );
	       let i = 
	         (* there is an extra argument (root node header file) for ScadeGUI *)
	         (if ((string_to_compiler Sys.argv.(3)) = ScadeGUI) then 1 else 0) in
	         if
	           arg_nb = 4 + i
	         then
	           (* No oracle is provided *)
	           let sut_path = Sys.argv.(1)
	           and sut_node = Sys.argv.(2)
	           and sut_compiler = (string_to_compiler Sys.argv.(3))
	           and tmp_dir = Sys.argv.(4)
	           in
	           let user_dir = Filename.dirname sut_path in
	           let header_file =
		          if 
		            (string_to_compiler Sys.argv.(3)) = ScadeGUI
		          then
		            (Filename.concat tmp_dir  Sys.argv.(5))
		          else
		            (Filename.concat tmp_dir (sut_node ^ ".h"))
	           in
		          (
		            (sut_compiler = ScadeGUI)
		            ||
		              (compile_lustre_program_if_needed 
		                 sut_path sut_node sut_compiler user_dir tmp_dir header_file)
		          )
                  (* 		&& *)
                  (* 		gen_oracle_always_true () *)
		          &&
		            gen_stubs_file tmp_dir
		            (Filename.concat user_dir sut_node) sut_compiler
		            (Filename.concat user_dir sut_node) sut_compiler 
		            header_file header_file false
		            
	         else true
        )
436
;;
437

438
if (main ()) then () else exit 105 ;;
439
440