Project

General

Profile

« Previous | Next » 

Revision 2dd3d358

Added by Teme Kahsai about 5 years ago

making library statically link to horn backend

View differences:

autom4te.cache/requests
14 14
                        'configure.ac'
15 15
                      ],
16 16
                      {
17
                        '_AM_MAKEFILE_INCLUDE' => 1,
18
                        'AM_ENABLE_MULTILIB' => 1,
17
                        'AM_PROG_MOC' => 1,
18
                        'AM_XGETTEXT_OPTION' => 1,
19
                        'AC_CANONICAL_BUILD' => 1,
19 20
                        'm4_sinclude' => 1,
20
                        'AC_CONFIG_FILES' => 1,
21
                        'AM_AUTOMAKE_VERSION' => 1,
22
                        'AM_CONDITIONAL' => 1,
21
                        'AM_PROG_CC_C_O' => 1,
22
                        '_AM_MAKEFILE_INCLUDE' => 1,
23
                        'AM_PROG_F77_C_O' => 1,
24
                        'm4_include' => 1,
25
                        'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
23 26
                        '_AM_COND_IF' => 1,
24
                        'AM_POT_TOOLS' => 1,
27
                        '_LT_AC_TAGCONFIG' => 1,
25 28
                        'AM_PROG_AR' => 1,
26
                        'AM_PROG_F77_C_O' => 1,
29
                        'AM_CONDITIONAL' => 1,
30
                        'AM_MAINTAINER_MODE' => 1,
27 31
                        'LT_INIT' => 1,
28
                        'AC_LIBSOURCE' => 1,
29
                        'AC_REQUIRE_AUX_FILE' => 1,
30
                        'AC_SUBST_TRACE' => 1,
31
                        'AM_GNU_GETTEXT' => 1,
32
                        '_AM_SUBST_NOTMAKE' => 1,
32
                        '_AM_COND_ELSE' => 1,
33
                        'AC_CONFIG_LIBOBJ_DIR' => 1,
34
                        '_AM_COND_ENDIF' => 1,
35
                        'AM_SILENT_RULES' => 1,
33 36
                        'AM_PROG_CXX_C_O' => 1,
34
                        'AC_DEFINE_TRACE_LITERAL' => 1,
35
                        'AM_PROG_MOC' => 1,
37
                        'AC_INIT' => 1,
38
                        'AC_CONFIG_FILES' => 1,
39
                        'AM_NLS' => 1,
40
                        'AC_CANONICAL_TARGET' => 1,
41
                        'AC_CANONICAL_HOST' => 1,
42
                        'm4_pattern_allow' => 1,
43
                        'AM_GNU_GETTEXT' => 1,
36 44
                        'AC_FC_PP_SRCEXT' => 1,
37
                        'AM_MAKEFILE_INCLUDE' => 1,
45
                        'AC_FC_FREEFORM' => 1,
46
                        'AC_FC_PP_DEFINE' => 1,
47
                        'LT_SUPPORTED_TAG' => 1,
48
                        'AM_PATH_GUILE' => 1,
49
                        'AM_ENABLE_MULTILIB' => 1,
50
                        'AM_POT_TOOLS' => 1,
51
                        'sinclude' => 1,
52
                        'AC_DEFINE_TRACE_LITERAL' => 1,
38 53
                        'm4_pattern_forbid' => 1,
39
                        'AC_CANONICAL_BUILD' => 1,
40
                        'AC_SUBST' => 1,
41
                        'AC_CONFIG_SUBDIRS' => 1,
42 54
                        'AC_CONFIG_HEADERS' => 1,
43
                        'AC_CONFIG_AUX_DIR' => 1,
44
                        'AC_CONFIG_LIBOBJ_DIR' => 1,
45
                        'AC_FC_PP_DEFINE' => 1,
55
                        'AC_REQUIRE_AUX_FILE' => 1,
46 56
                        'AC_CONFIG_LINKS' => 1,
47
                        'AH_OUTPUT' => 1,
48
                        '_LT_AC_TAGCONFIG' => 1,
49
                        'AM_XGETTEXT_OPTION' => 1,
50
                        'AM_SILENT_RULES' => 1,
51
                        'AC_CANONICAL_HOST' => 1,
52
                        'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
53
                        '_m4_warn' => 1,
54
                        'AC_INIT' => 1,
55
                        'm4_include' => 1,
56
                        'AM_MAINTAINER_MODE' => 1,
57
                        'AM_NLS' => 1,
58
                        'AC_FC_SRCEXT' => 1,
57
                        'AC_SUBST_TRACE' => 1,
58
                        'AC_LIBSOURCE' => 1,
59 59
                        'AC_PROG_LIBTOOL' => 1,
60
                        'AM_PATH_GUILE' => 1,
61
                        'AC_CANONICAL_SYSTEM' => 1,
62
                        'include' => 1,
60
                        'AC_FC_SRCEXT' => 1,
61
                        'AM_AUTOMAKE_VERSION' => 1,
63 62
                        'LT_CONFIG_LTDL_DIR' => 1,
63
                        'AM_MAKEFILE_INCLUDE' => 1,
64
                        'include' => 1,
64 65
                        'AM_INIT_AUTOMAKE' => 1,
65
                        '_AM_COND_ENDIF' => 1,
66
                        'AM_PROG_FC_C_O' => 1,
67
                        'sinclude' => 1,
68
                        'm4_pattern_allow' => 1,
69
                        'AM_PROG_CC_C_O' => 1,
70
                        'AC_FC_FREEFORM' => 1,
71
                        'LT_SUPPORTED_TAG' => 1,
72
                        '_AM_COND_ELSE' => 1,
73
                        'AC_CANONICAL_TARGET' => 1
66
                        'AC_CANONICAL_SYSTEM' => 1,
67
                        '_AM_SUBST_NOTMAKE' => 1,
68
                        'AC_SUBST' => 1,
69
                        'AC_CONFIG_SUBDIRS' => 1,
70
                        'AH_OUTPUT' => 1,
71
                        'AC_CONFIG_AUX_DIR' => 1,
72
                        '_m4_warn' => 1,
73
                        'AM_PROG_FC_C_O' => 1
74 74
                      }
75 75
                    ], 'Autom4te::Request' )
76 76
           );
src/backends/C/c_backend.ml
29 29
  let destname = !Options.dest_dir ^ "/" ^ basename in
30 30
  let source_main_file = destname ^ "_main.c" in (* Could be changed *)
31 31
  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
32
  
32

  
33 33
  let print_header, print_lib_c, print_main_c, print_makefile = funs in
34 34

  
35 35
  (* Generating H file *)
......
38 38
  let header_fmt = formatter_of_out_channel header_out in
39 39
  print_header header_fmt basename prog machines dependencies;
40 40
  close_out header_out;
41
  
41

  
42 42
  (* Generating Lib C file *)
43 43
  let source_lib_file = destname ^ ".c" in (* Could be changed *)
44 44
  let source_lib_out = open_out source_lib_file in
......
63 63

  
64 64
      (* Generating Main C file *)
65 65
      print_main_c source_main_fmt m basename prog machines dependencies;
66
      
66

  
67 67
      (* Generating Makefile *)
68 68
      print_makefile basename main_node dependencies makefile_fmt;
69 69

  
......
86 86
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
87 87
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
88 88

  
89
    let funs = 
90
      Header.print_alloc_header, 
91
      Source.print_lib_c, 
92
      SourceMain.print_main_c, 
93
      Makefile.print_makefile 
89
    let funs =
90
      Header.print_alloc_header,
91
      Source.print_lib_c,
92
      SourceMain.print_main_c,
93
      Makefile.print_makefile
94 94
    in
95
    gen_files funs basename prog machines dependencies 
95
    gen_files funs basename prog machines dependencies
96 96

  
97 97
  end
98 98
  | "acsl" -> begin
......
107 107
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
108 108
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
109 109

  
110
    let funs = 
111
      Header.print_alloc_header, 
110
    let funs =
111
      Header.print_alloc_header,
112 112
      Source.print_lib_c,
113 113
      SourceMain.print_main_c,
114
      Makefile.print_makefile 
114
      Makefile.print_makefile
115 115
    in
116
    gen_files funs basename prog machines dependencies 
116
    gen_files funs basename prog machines dependencies
117 117

  
118 118
  end
119 119
  | "c" -> begin
src/backends/Horn/horn_backend.ml
48 48
    )
49 49
end
50 50

  
51

  
52
let load_file f =
53
  let ic = open_in f in
54
  let n = in_channel_length ic in
55
  let s = String.create n in
56
  really_input ic s 0 n;
57
  close_in ic;
58
  (s)
59

  
51 60
let print_type_definitions fmt =
52 61
  let cpt_type = ref 0 in
53 62
  Hashtbl.iter (fun typ decl ->
......
68 77
    | _        -> ()) type_table
69 78

  
70 79

  
71
let translate fmt basename prog machines =
80

  
81

  
82
let print_dep fmt prog =
83
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,");
84
  fprintf fmt "; Statically linked libraries@";
85
  let dependencies = Corelang.get_dependencies prog in
86
  List.iter
87
    (fun dep ->
88
      let (local, s) = Corelang.dependency_of_top dep in
89
      let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in
90
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);
91
      let horn = load_file basename in
92
      fprintf fmt "@.%s@." horn;
93
    )
94
    dependencies
95

  
96
let translate fmt basename prog machines=
72 97
  (* We print typedef *)
98
  print_dep fmt prog;
73 99
  print_type_definitions fmt;
74 100
  List.iter (print_machine machines fmt) (List.rev machines);
75 101
  main_print machines fmt
src/compiler_common.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open Format 
13
open Format
14 14
open LustreSpec
15 15
open Corelang
16 16

  
......
50 50
      close_in h_in;
51 51
      header
52 52
    with
53
    | (Parse.Error err) as exc -> 
53
    | (Parse.Error err) as exc ->
54 54
      Parse.report_error err;
55 55
      raise exc
56 56
    | Corelang.Error (loc, err) as exc -> (
......
68 68
  Location.init lexbuf source_name;
69 69

  
70 70
  (* Parsing *)
71
  Log.report ~level:1 
71
  Log.report ~level:1
72 72
    (fun fmt -> fprintf fmt ".. parsing source file %s@," source_name);
73 73
  try
74 74
    let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in
......
76 76
    close_in s_in;
77 77
    prog
78 78
  with
79
  | (Parse.Error err) as exc -> 
79
  | (Parse.Error err) as exc ->
80 80
    Parse.report_error err;
81 81
    raise exc
82 82
  | Corelang.Error (loc, err) as exc ->
......
115 115
      Location.pp_loc loc;
116 116
    raise exc
117 117

  
118
let type_decls env decls =  
118
let type_decls env decls =
119 119
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
120
  let new_env = 
120
  let new_env =
121 121
    begin
122 122
      try
123 123
	Typing.type_prog env decls
......
126 126
	  Types.pp_error err
127 127
	  Location.pp_loc loc;
128 128
	raise exc
129
    end 
129
    end
130 130
  in
131 131
  if !Options.print_types then
132 132
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
133 133
  new_env
134
      
135
let clock_decls env decls = 
134

  
135
let clock_decls env decls =
136 136
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ ");
137 137
  let new_env =
138 138
    begin
......
221 221
let is_stateful topdecl =
222 222
  match topdecl.top_decl_desc with
223 223
  | Node nd -> (match nd.node_stateless with Some b -> not b | None -> not nd.node_dec_stateless)
224
  | ImportedNode nd -> not nd.nodei_stateless 
224
  | ImportedNode nd -> not nd.nodei_stateless
225 225
  | _ -> false
226 226

  
227 227

  
......
248 248
    Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
249 249
    deps
250 250
  end
251

  
src/main_lustre_compiler.ml
15 15
open Utils
16 16
open LustreSpec
17 17
open Compiler_common
18
 
18

  
19 19
exception StopPhase1 of program
20 20

  
21 21
let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
......
88 88
  end
89 89

  
90 90

  
91
let functional_backend () = 
91
let functional_backend () =
92 92
  match !Options.output with
93 93
  | "horn" | "lustre" | "acsl" -> true
94 94
  | _ -> false
95 95

  
96 96
(* From prog to prog *)
97 97
let stage1 prog dirname basename =
98
  (* Removing automata *) 
98
  (* Removing automata *)
99 99
  let prog = expand_automata prog in
100 100

  
101 101
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
......
137 137
       exported as a lusi *)
138 138
    raise (StopPhase1 prog);
139 139

  
140
 (* Optimization of prog: 
141
     - Unfold consts 
140
 (* Optimization of prog:
141
     - Unfold consts
142 142
     - eliminate trivial expressions
143 143
 *)
144 144
  (*
145
  let prog = 
145
  let prog =
146 146
    if !Options.const_unfold || !Options.optimization >= 5 then
147 147
      begin
148 148
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
......
193 193
	!Options.main_node
194 194
	orig prog type_env clock_env
195 195
    end;
196
  
196

  
197 197
  (* Computes and stores generic calls for each node,
198 198
     only useful for ANSI C90 compliant generic node compilation *)
199 199
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
......
233 233
  prog, dependencies
234 234

  
235 235
(* from source to machine code, with optimization *)
236
let stage2 prog =    
236
let stage2 prog =
237 237
  (* Computation of node equation scheduling. It also breaks dependency cycles
238 238
     and warns about unused input or memory variables *)
239 239
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
......
245 245
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
246 246

  
247 247

  
248
  (* TODO Salsa optimize prog: 
248
  (* TODO Salsa optimize prog:
249 249
     - emits warning for programs with pre inside expressions
250 250
     - make sure each node arguments and memory is bounded by a local annotation
251 251
     - introduce fresh local variables for each real pure subexpression
......
269 269
      machine_code
270 270
  in
271 271
  (* Optimize machine code *)
272
  let machine_code, removed_table = 
272
  let machine_code, removed_table =
273 273
    if !Options.optimization >= 2 && !Options.output <> "horn" then
274 274
      begin
275 275
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: constants inlining@,");
......
277 277
      end
278 278
    else
279 279
      machine_code, IMap.empty
280
  in  
280
  in
281 281
  (* Optimize machine code *)
282
  let machine_code = 
282
  let machine_code =
283 283
    if !Options.optimization >= 3 && !Options.output <> "horn" then
284 284
      begin
285 285
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
......
290 290
    else
291 291
      machine_code
292 292
  in
293
  
293

  
294 294
  (* Salsa optimize machine code *)
295 295
  (*
296
  let machine_code = 
296
  let machine_code =
297 297
    if !Options.salsa_enabled then
298 298
      begin
299 299
	check_main ();
......
305 305
	    | Const c when Types.is_real_type c.const_type  ->
306 306
	      (c.const_id, c.const_value) :: accu
307 307
	    | _ -> accu
308
	) [] (Corelang.get_consts prog) 
308
	) [] (Corelang.get_consts prog)
309 309
	in
310
	List.map 
311
	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) 
312
	  machine_code 
310
	List.map
311
	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)
312
	  machine_code
313 313
      end
314 314
    else
315 315
      machine_code
......
325 325
let stage3 prog machine_code dependencies basename =
326 326
  let basename    =  Filename.basename basename in
327 327
  match !Options.output with
328
    "C" -> 
328
    "C" ->
329 329
      begin
330 330
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
331 331
	C_backend.translate_to_c
......
387 387
    else
388 388
      prog
389 389
  in
390
  let prog, dependencies = 
391
    try 
390
  let prog, dependencies =
391
    try
392 392
      stage1 prog dirname basename
393 393
    with StopPhase1 prog -> (
394 394
      if !Options.lusi then
......
404 404
    )
405 405
  in
406 406

  
407
  let machine_code = 
408
    stage2 prog 
407
  let machine_code =
408
    stage2 prog
409 409
  in
410 410
  if Scopes.Plugin.show_scopes () then
411 411
    begin
......
415 415
	Format.printf "Possible scopes are:@   ";
416 416
      Format.printf "@[<v>%a@ @]@.@?" Scopes.print_scopes all_scopes;
417 417
      exit 0
418
	
418

  
419 419
    end;
420 420

  
421
  let machine_code = 
421
  let machine_code =
422 422
    if Scopes.Plugin.is_active () then
423 423
      Scopes.Plugin.process_scopes !Options.main_node prog machine_code
424 424
    else
425 425
      machine_code
426 426
  in
427
  
427

  
428 428
  stage3 prog machine_code dependencies basename;
429 429
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
430 430
    (* We stop the process here *)
......
457 457
  try
458 458
    Printexc.record_backtrace true;
459 459

  
460
    let options = Options.options @ 
460
    let options = Options.options @
461 461
      List.flatten (
462 462
	List.map Options.plugin_opt [
463 463
	  Scopes.Plugin.name, Scopes.Plugin.activate, Scopes.Plugin.options
464 464
	]
465 465
      )
466 466
    in
467
    
467

  
468 468
    Arg.parse options anonymous usage
469 469
  with
470 470
  | Parse.Error _

Also available in: Unified diff