Project

General

Profile

« Previous | Next » 

Revision 782742b6

Added by Pierre-Loïc Garoche about 5 years ago

Merged unstable with seahorn

View differences:

src/compiler_common.ml
188 188
   (Env.initial, Env.initial)
189 189
 *)
190 190

  
191
let generate_lusic_header destname lusic_ext =	
192
  match !Options.output with
193
  | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
194
  | _ -> ()
195
	 
196

  
197
    
191 198
let check_compatibility (prog, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
192 199
  try
193 200
    (* checking defined types are compatible with declared types*)
src/lusic.ml
25 25
  contents  : top_decl list;
26 26
}
27 27

  
28
module HeaderMod = C_backend_header.EmptyMod
29
module Header = C_backend_header.Main (HeaderMod)
30 28

  
31 29
(* extracts a header from a program representing module owner = dirname/basename *)
32 30
let extract_header dirname basename prog =
......
83 81
      }
84 82
    end
85 83

  
86
let print_lusic_to_h basename extension =
87
  let lusic = read_lusic basename extension in
88
  let header_name = basename ^ ".h" in
89
  let h_out = open_out header_name in
90
  let h_fmt = formatter_of_out_channel h_out in
91
  begin
92
    assert (not lusic.obsolete);
93
    (*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*)
94
    Typing.uneval_prog_generics lusic.contents;
95
    Clock_calculus.uneval_prog_generics lusic.contents;
96
    Header.print_header_from_header h_fmt (Filename.basename basename) lusic.contents;
97
    close_out h_out
98
  end
99

  
100 84

  
src/main_lustre_compiler.ml
49 49
    Log.report ~level:1
50 50
      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
51 51
    Lusic.write_lusic true header destname lusic_ext;
52
    Lusic.print_lusic_to_h destname lusic_ext;
52
    generate_lusic_header destname lusic_ext;
53 53
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.")
54 54
  end
55 55

  
......
59 59
  let destname = !Options.dest_dir ^ "/" ^ basename in
60 60
  let lusic_ext = extension ^ "c" in
61 61
  let header_name = destname ^ lusic_ext in
62
  begin
62
  let do_generate_lusic, lusic_opt =
63 63
    if not (Sys.file_exists header_name) then
64
      begin
65
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
66
	Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
67
	Lusic.print_lusic_to_h destname lusic_ext
68
      end
64
      true, None
69 65
    else
70 66
      let lusic = Lusic.read_lusic destname lusic_ext in
71
      if not lusic.Lusic.from_lusi then
72
	begin
73
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
74
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
75
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
76
	  Lusic.print_lusic_to_h destname lusic_ext
77
	end
78
      else
79
	begin
80
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
81
	  Modules.check_dependency lusic destname;
82
	  let header = lusic.Lusic.contents in
83
	  let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
84
	  check_compatibility
85
	    (prog, computed_types_env, computed_clocks_env)
86
	    (header, declared_types_env, declared_clocks_env)
87
	end
88
  end
67
      not lusic.Lusic.from_lusi, Some lusic
68
  in
69
  if do_generate_lusic then
70
    begin
71
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
72
      Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
73
      generate_lusic_header destname lusic_ext
74
    end
75
  else
76
    begin
77
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
78
      let lusic = desome lusic_opt in
79
      Modules.check_dependency lusic destname;
80
      let header = lusic.Lusic.contents in
81
      let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
82
      check_compatibility
83
	(prog, computed_types_env, computed_clocks_env)
84
	(header, declared_types_env, declared_clocks_env)
85
    end
86
      
87
      
88
      
89
      (* begin *)
90
      (* 	if not (Sys.file_exists header_name) then *)
91
      (* 	  begin *)
92
      (* 	    Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); *)
93
      (* 	    Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; *)
94
      (* 	    Lusic.print_lusic_to_h destname lusic_ext *)
95
      (* 	  end *)
96
      (* 	else *)
97
      (* 	  let lusic = Lusic.read_lusic destname lusic_ext in *)
98
      (* 	  if not lusic.Lusic.from_lusi then *)
99
      (* 	    begin *)
100
      (* 	      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); *)
101
      (*  	      Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; *)
102
      (* 	      (\*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*\) *)
103
      (* 	      Lusic.print_lusic_to_h destname lusic_ext *)
104
      (* 	    end *)
105
      (* 	  else *)
106
      (* 	    begin *)
107
      (* 	      Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name); *)
108
      (* 	      Modules.check_dependency lusic destname; *)
109
      (* 	      let header = lusic.Lusic.contents in *)
110
      (* 	      let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in *)
111
      (* 	      check_compatibility *)
112
      (* 		(prog, computed_types_env, computed_clocks_env) *)
113
      (* 		(header, declared_types_env, declared_clocks_env) *)
114
      (* 	    end *)
115
      (* end *)
89 116

  
90 117

  
91 118

  
......
215 242
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
216 243
  (* Special treatment of arrows in lustre backend. We want to keep them *)
217 244
  if !Options.output = "lustre" then
218
    Normalization.unfold_arrow_active := false;
245
    Normalization_common.unfold_arrow_active := false;
219 246
  let prog = Normalization.normalize_prog prog in
220 247
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
221 248

  
src/main_lustre_testgen.ml
81 81
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
82 82
  (* Special treatment of arrows in lustre backend. We want to keep them *)
83 83
  if !Options.output = "lustre" then
84
    Normalization.unfold_arrow_active := false;
84
    Normalization_common.unfold_arrow_active := false;
85 85
  let prog = Normalization.normalize_prog prog in
86 86
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
87 87

  
src/mpfr.ml
12 12
open Utils
13 13
open LustreSpec
14 14
open Corelang
15
open Normalization
15
open Normalization_common
16 16
open Machine_code
17 17

  
18 18
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
src/normalization.ml
13 13
open LustreSpec
14 14
open Corelang
15 15
open Format
16

  
17
let expr_true loc ck =
18
{ expr_tag = Utils.new_tag ();
19
  expr_desc = Expr_const (Const_tag tag_true);
20
  expr_type = Type_predef.type_bool;
21
  expr_clock = ck;
22
  expr_delay = Delay.new_var ();
23
  expr_annot = None;
24
  expr_loc = loc }
25

  
26
let expr_false loc ck =
27
{ expr_tag = Utils.new_tag ();
28
  expr_desc = Expr_const (Const_tag tag_false);
29
  expr_type = Type_predef.type_bool;
30
  expr_clock = ck;
31
  expr_delay = Delay.new_var ();
32
  expr_annot = None;
33
  expr_loc = loc }
34

  
35
let expr_once loc ck =
36
 { expr_tag = Utils.new_tag ();
37
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
38
  expr_type = Type_predef.type_bool;
39
  expr_clock = ck;
40
  expr_delay = Delay.new_var ();
41
  expr_annot = None;
42
  expr_loc = loc }
43

  
44
let is_expr_once =
45
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
46
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
47

  
48
let unfold_arrow expr =
49
 match expr.expr_desc with
50
 | Expr_arrow (e1, e2) ->
51
    let loc = expr.expr_loc in
52
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
53
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
54
 | _                   -> assert false
55

  
56
let unfold_arrow_active = ref true
57
let cpt_fresh = ref 0
58

  
59
(* Generate a new local [node] variable *)
60
let mk_fresh_var node loc ty ck =
61
  let vars = get_node_vars node in
62
  let rec aux () =
63
  incr cpt_fresh;
64
  let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
65
  if List.exists (fun v -> v.var_id = s) vars then aux () else
66
  {
67
    var_id = s;
68
    var_orig = false;
69
    var_dec_type = dummy_type_dec;
70
    var_dec_clock = dummy_clock_dec;
71
    var_dec_const = false;
72
    var_dec_value = None;
73
    var_type = ty;
74
    var_clock = ck;
75
    var_loc = loc
76
  }
77
  in aux ()
78

  
79
(* Get the equation in [defs] with [expr] as rhs, if any *)
80
let get_expr_alias defs expr =
81
 try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
82
 with
83
 | Not_found -> None
84
  
85
(* Replace [expr] with (tuple of) [locals] *)
86
let replace_expr locals expr =
87
 match locals with
88
 | []  -> assert false
89
 | [v] -> { expr with
90
   expr_tag = Utils.new_tag ();
91
   expr_desc = Expr_ident v.var_id }
92
 | _   -> { expr with
93
   expr_tag = Utils.new_tag ();
94
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
95

  
96
let unfold_offsets e offsets =
97
  let add_offset e d =
98
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
99
    let res = *)
100
    { e with
101
      expr_tag = Utils.new_tag ();
102
      expr_loc = d.Dimension.dim_loc;
103
      expr_type = Types.array_element_type e.expr_type;
104
      expr_desc = Expr_access (e, d) }
105
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
106
  in
107
 List.fold_left add_offset e offsets
108

  
109
(* Create an alias for [expr], if none exists yet *)
110
let mk_expr_alias node (defs, vars) expr =
111
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
112
  match get_expr_alias defs expr with
113
  | Some eq ->
114
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
115
    (defs, vars), replace_expr aliases expr
116
  | None    ->
117
    let new_aliases =
118
      List.map2
119
	(mk_fresh_var node expr.expr_loc)
120
	(Types.type_list_of_type expr.expr_type)
121
	(Clocks.clock_list_of_clock expr.expr_clock) in
122
    let new_def =
123
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
124
    in
125
    (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
126
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
127

  
128
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
129
   and [opt] is true *)
130
let mk_expr_alias_opt opt node (defs, vars) expr =
131
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
132
  match expr.expr_desc with
133
  | Expr_ident alias ->
134
    (defs, vars), expr
135
  | _                ->
136
    match get_expr_alias defs expr with
137
    | Some eq ->
138
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
139
      (defs, vars), replace_expr aliases expr
140
    | None    ->
141
      if opt
142
      then
143
	let new_aliases =
144
	  List.map2
145
	    (mk_fresh_var node expr.expr_loc)
146
	    (Types.type_list_of_type expr.expr_type)
147
	    (Clocks.clock_list_of_clock expr.expr_clock) in
148
	let new_def =
149
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
150
	in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
151
      else
152
	(defs, vars), expr
16
open Normalization_common
153 17

  
154 18
(* Create a (normalized) expression from [ref_e],
155 19
   replacing description with [norm_d],
src/options.ml
78 78
  [ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>";
79 79
    "-I", Arg.Set_string include_dir, "sets include \x1b[4mdirectory\x1b[0m";
80 80
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
81
    "-print-types", Arg.Set print_types, "prints node types";
82
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
83
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
84
    "-version", Arg.Unit print_version, " displays the version";
85
  ]
86

  
87
let lustrec_options =
88
   common_options @
89
  [ 
81 90
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
82 91
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
83 92
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
src/plugins.ml
2 2

  
3 3
open PluginList
4 4

  
5

  
6 5
let options () = 
7 6
  List.flatten (
8 7
    List.map Options.plugin_opt (

Also available in: Unified diff