Project

General

Profile

Revision 7dedc5f0

View differences:

src/corelang.ml
194 194
  if is_user_type typ_def then typ else typ_def
195 195

  
196 196
let rec coretype_equal ty1 ty2 =
197
  let res = 
197
  (*let res =*) 
198 198
  match ty1, ty2 with
199
  | Tydec_any       , _
200
  | _               , Tydec_any        -> assert false
201
  | Tydec_const _   , Tydec_const _    -> get_repr_type ty1 = get_repr_type ty2
202
  | Tydec_const _   , _                -> let ty1' = Hashtbl.find type_table ty1
203
					  in (not (is_user_type ty1')) && coretype_equal ty1' ty2
204
  | _               , Tydec_const _    -> coretype_equal ty2 ty1
205
  | Tydec_int       , Tydec_int
206
  | Tydec_real      , Tydec_real
207
  | Tydec_float     , Tydec_float
208
  | Tydec_bool      , Tydec_bool       -> true
209
  | Tydec_clock ty1 , Tydec_clock ty2  -> coretype_equal ty1 ty2
210
  | Tydec_enum tl1  , Tydec_enum tl2   -> List.sort compare tl1 = List.sort compare tl2
211
  | Tydec_struct fl1, Tydec_struct fl2 ->
199
  | Tydec_any           , _
200
  | _                   , Tydec_any             -> assert false
201
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
202
  | Tydec_const _       , _                     -> let ty1' = Hashtbl.find type_table ty1
203
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
204
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
205
  | Tydec_int           , Tydec_int
206
  | Tydec_real          , Tydec_real
207
  | Tydec_float         , Tydec_float
208
  | Tydec_bool          , Tydec_bool            -> true
209
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
210
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
211
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
212
  | Tydec_struct fl1    , Tydec_struct fl2      ->
212 213
       List.length fl1 = List.length fl2
213 214
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
214 215
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
215 216
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
216 217
  | _                                  -> false
217
  in ((*Format.eprint "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
218
  (*in (Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res; res)*)
218 219

  
219 220
let tag_true = "true"
220 221
let tag_false = "false"
......
422 423
	| Node _ | ImportedNode _ | Open _ | Consts _ -> types  
423 424
  ) [] prog
424 425

  
426
let get_node_interface nd =
427
 {nodei_id = nd.node_id;
428
  nodei_type = nd.node_type;
429
  nodei_clock = nd.node_clock;
430
  nodei_inputs = nd.node_inputs;
431
  nodei_outputs = nd.node_outputs;
432
  nodei_stateless = nd.node_dec_stateless;
433
  nodei_spec = nd.node_spec;
434
  nodei_prototype = None;
435
  nodei_in_lib = None;
436
 }
437

  
425 438
(************************************************************************)
426 439
(*        Renaming                                                      *)
427 440

  
src/corelang.mli
61 61
val get_node_vars: node_desc -> var_decl list
62 62
val get_node_var: ident -> node_desc -> var_decl
63 63
val get_node_eq: ident -> node_desc -> eq
64
val get_node_interface: node_desc -> imported_node_desc
64 65

  
65 66
(* val get_const: ident -> constant *)
66 67

  
src/dimension.ml
285 285
let rec instantiate inst_dim_vars dim =
286 286
  let dim = repr dim in
287 287
  match dim.dim_desc with
288
  | Dvar _
288
  | Dvar
289 289
  | Dident _
290 290
  | Dint _
291 291
  | Dbool _ -> dim
src/liveness.ml
105 105
      end
106 106
  done
107 107
 
108
(* checks whether a variable is aliasable,
109
   depending on its (address) type *)
110
let is_aliasable var =
111
 Types.is_address_type var.var_type
112
 
108 113
(* checks whether a variable [v] is an input of the [var] equation, with an address type.
109 114
   if so, [var] could not safely reuse/alias [v], should [v] be dead in the caller node,
110 115
   because [v] may not be dead in the callee node when [var] is assigned *)
src/main_lustre_compiler.ml
131 131
      eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a@."
132 132
	Stateless.pp_error err;
133 133
      raise exc
134
    
134

  
135
let extract_interface prog =
136
 List.fold_right
137
   (fun decl header ->
138
    match decl.top_decl_desc with
139
    | Node nd        -> { decl with top_decl_desc = ImportedNode (Corelang.get_node_interface nd) } :: header 
140
    | ImportedNode _ -> header
141
    | Consts _
142
    | Type _
143
    | Open _         -> decl :: header)
144
   prog []
145

  
146
let write_compiled_header (header : top_decl list) basename extension =
147
  let target_name = basename^extension in
148
  let outchan = open_out_bin target_name in
149
  begin
150
    Marshal.to_channel outchan header [];
151
    close_out outchan
152
  end
153

  
154
let read_compiled_header basename extension =
155
  let source_name = basename^extension in
156
  let inchan = open_in_bin source_name in
157
  let header = (Marshal.from_channel inchan : top_decl list) in
158
  begin
159
    close_in inchan;
160
    header
161
  end
162

  
163
let compile_header basename extension =
164
   let header_name = basename^extension in
165
   let header = load_lusi true header_name in
166
   begin
167
     ignore (check_lusi header);
168
     write_compiled_header header basename (extension^"c")
169
   end
170

  
171
let compile_prog basename extension =
172

  
135 173
let rec compile basename extension =
136 174

  
137 175
  (* Loading the input file *)
src/options.ml
25 25
let global_inline = ref false
26 26
let witnesses = ref false
27 27
let optimization = ref 2
28
let lusi = ref false
28 29

  
29 30
let horntraces = ref false
30 31
let horn_cex = ref false
......
34 35
  [ "-d", Arg.Set_string dest_dir,
35 36
    "produces code in the specified directory (default: .)";
36 37
    "-node", Arg.Set_string main_node, "specifies the main node";
37
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes";
38
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node (default: static)";
39
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default: C99)";
40
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";
41

  
38
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
39
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
40
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant <default: C99>";
41
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
42
    "-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
42 43
    "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
43 44
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend (default)";
44 45
    "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
src/printers.ml
316 316
  | Node nd ->  
317 317
    fprintf fmt 
318 318
      "@[<v>%s %s (%a) returns (%a);@ @]@ "
319
      (if Stateless.check_node decl then "function" else "node")
319
      (if nd.node_dec_stateless then "function" else "node")
320 320
      nd.node_id
321 321
      pp_node_args nd.node_inputs
322 322
      pp_node_args nd.node_outputs

Also available in: Unified diff