Project

General

Profile

Revision c7c6ef4c

View differences:

src/backends/Horn/horn_backend.ml
65 65
let get_machine machines node_name =
66 66
  List.find (fun m  -> m.mname.node_id = node_name) machines
67 67

  
68

  
68 69
let full_memory_vars machines machine =
69 70
  let rec aux fst prefix m =
70 71
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
......
77 78
  in
78 79
  aux true machine.mname.node_id machine
79 80

  
81

  
80 82
let stateless_vars machines m =
81 83
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
82 84
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
......
338 340
       (*   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)
339 341

  
340 342

  
341
        (* Adding assertions *)
343
      (* Adding assertions *)
342 344
       (match m.mstep.step_asserts with
343 345
       | [] ->
344 346
          begin
347
            (* Rule for init *)
348
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
349
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
350
	                   pp_machine_init_name m.mname.node_id
351
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
352
            (* Rule for step*)
345 353
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
346 354
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
347 355
                           pp_machine_step_name m.mname.node_id
......
349 357
          end
350 358
       | assertsl ->
351 359
          begin
352

  
353 360
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
354 361
            (* print_string pp_val; *)
355 362
            let instrs_concat = m.mstep.step_instrs in
356
            Format.fprintf fmt "; with Invariants @.";
363
            Format.fprintf fmt "; with Assertions @.";
364
            (*Rule for init*)
365
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
366
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
367
                           (pp_conj pp_val) assertsl
368
                           pp_machine_init_name m.mname.node_id
369
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
370
            (*Rule for step*)
357 371
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
358 372
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
359 373
                           (pp_conj pp_val) assertsl
360 374
                           pp_machine_step_name m.mname.node_id
361 375
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
362

  
363

  
364 376
	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
365 377
            (*                 (pp_conj pp_val) assertsl; *)
366 378

  
367 379
          end
368 380
       );
369 381

  
370
       (* (\* Adding assertions *\) *)
371
       (* (match m.mstep.step_asserts with *)
372
       (* | [] -> () *)
373
       (* | assertsl -> begin *)
374
       (*   let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in *)
375

  
376
       (*   Format.fprintf fmt "; Asserts@."; *)
377
       (*   Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@." *)
378
       (*     (pp_conj pp_val) assertsl; *)
379

  
380
       (*   (\** TEME: the following code is the one we described. But it generates a segfault in z3 *)
381
       (*   Format.fprintf fmt "; Asserts for init@."; *)
382
       (*   Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@." *)
383
       (*     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs *)
384
       (*     pp_machine_init_name m.mname.node_id *)
385
       (*     (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m) *)
386
       (*     (pp_conj pp_val) assertsl; *)
387

  
388
       (*   Format.fprintf fmt "; Asserts for step@."; *)
389
       (*   Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@." *)
390
       (*     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
391

  
392
       (*     pp_machine_step_name m.mname.node_id *)
393
       (*     (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m) *)
394
       (*     (pp_conj pp_val) assertsl *)
395
       (*   *\) *)
396
       (* end *)
397
       (* ); *)
398

  
399
(*
400
       match m.mspec with
401
	 None -> () (* No node spec; we do nothing *)
402
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
403
	 (
404
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
405
	   ()
406 382

  
407
	 )
408
       | _ -> () (* Other cases give nothing *)
409
*)
410 383
     end
411 384
    end
412 385

  
......
472 445
    (pp_conj pp_var) main_output
473 446
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
474 447
    ;
475
  if !Options.horn_queries then
476
    Format.fprintf fmt "(query ERR)@."
448
   Format.fprintf fmt "(query ERR)@."
477 449

  
478 450

  
479 451
let cex_computation machines fmt node machine =
......
543 515
    (pp_conj pp_var) cex_output
544 516
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
545 517
    ;
546
  if !Options.horn_queries then
547
    Format.fprintf fmt "(query CEXTRACE)@."
518
  Format.fprintf fmt "(query CEXTRACE)@."
548 519

  
549 520

  
550 521
let main_print machines fmt =
src/main_lustre_compiler.ml
42 42
    ignore (Modules.load_header ISet.empty header);
43 43
    ignore (check_top_decls header);
44 44
    create_dest_dir ();
45
    Log.report ~level:1 
45
    Log.report ~level:1
46 46
      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
47 47
    Lusic.write_lusic true header destname lusic_ext;
48 48
    Lusic.print_lusic_to_h destname lusic_ext;
......
84 84

  
85 85
(* compile a .lus source file *)
86 86
let rec compile_source dirname basename extension =
87
  let source_name = (*dirname ^ "/" ^ *) basename ^ extension in
87
  let source_name = dirname ^ "/" ^ basename ^ extension in
88 88

  
89 89
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
90 90

  
91 91
  (* Parsing source *)
92 92
  let prog = parse_source source_name in
93 93

  
94
  (* Removing automata *) 
94
  (* Removing automata *)
95 95
  let prog = Automata.expand_decls prog in
96 96

  
97 97
  (* Importing source *)
......
105 105

  
106 106
  (* Typing *)
107 107
  let computed_types_env = type_decls type_env prog in
108
  
108

  
109 109
  (* Clock calculus *)
110 110
  let computed_clocks_env = clock_decls clock_env prog in
111 111

  
......
124 124

  
125 125
  (* Perform global inlining *)
126 126
  let prog =
127
    if !Options.global_inline && 
127
    if !Options.global_inline &&
128 128
      (match !Options.main_node with | "" -> false | _ -> true) then
129 129
      Inliner.global_inline basename prog type_env clock_env
130 130
    else
......
197 197
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
198 198
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
199 199

  
200
 (* Optimization of prog: 
201
    - Unfold consts 
200
 (* Optimization of prog:
201
    - Unfold consts
202 202
    - eliminate trivial expressions
203 203
 *)
204
  let prog = 
205
    if !Options.optimization >= 4 then 
206
      Optimize_prog.prog_unfold_consts prog 
204
  let prog =
205
    if !Options.optimization >= 4 then
206
      Optimize_prog.prog_unfold_consts prog
207 207
    else
208 208
      prog
209 209
  in
......
212 212
  let machine_code = Machine_code.translate_prog prog node_schs in
213 213

  
214 214
  (* Optimize machine code *)
215
  let machine_code = 
215
  let machine_code =
216 216
    if !Options.optimization >= 2 && !Options.output <> "horn" then
217 217
      begin
218 218
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@,");
......
220 220
      end
221 221
    else
222 222
      machine_code
223
 in  
223
 in
224 224
  (* Optimize machine code *)
225
  let machine_code = 
225
  let machine_code =
226 226
    if !Options.optimization >= 3 && !Options.output <> "horn" then
227 227
      begin
228 228
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@,");
......
239 239
  let basename    =  Filename.basename basename in
240 240
  let destname = !Options.dest_dir ^ "/" ^ basename in
241 241
  let _ = match !Options.output with
242
      "C" -> 
242
      "C" ->
243 243
	begin
244 244
	  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
245 245
	  let source_lib_file = destname ^ ".c" in (* Could be changed *)
246 246
	  let source_main_file = destname ^ "_main.c" in (* Could be changed *)
247 247
	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
248 248
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
249
	  C_backend.translate_to_c 
249
	  C_backend.translate_to_c
250 250
	    alloc_header_file source_lib_file source_main_file makefile_file
251 251
	    basename prog machine_code dependencies
252 252
	end
......
271 271
	let traces_file = destname ^ ".traces" in (* Could be changed *)
272 272
	let traces_out = open_out traces_file in
273 273
	let fmt = formatter_of_out_channel traces_out in
274
	Horn_backend.traces_file fmt basename prog machine_code	  
274
	Horn_backend.traces_file fmt basename prog machine_code
275 275
	)
276 276
      end
277
    | "lustre" -> 
277
    | "lustre" ->
278 278
      begin
279 279
	let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
280 280
	let source_out = open_out source_file in
......
299 299
  | _        -> assert false
300 300

  
301 301
let anonymous filename =
302
  let ok_ext, ext = List.fold_left 
303
    (fun (ok, ext) ext' -> 
304
      if not ok && Filename.check_suffix filename ext' then 
305
	true, ext' 
302
  let ok_ext, ext = List.fold_left
303
    (fun (ok, ext) ext' ->
304
      if not ok && Filename.check_suffix filename ext' then
305
	true, ext'
306 306
      else
307
	ok, ext) 
307
	ok, ext)
308 308
    (false, "") extensions in
309 309
  if ok_ext then
310 310
    let dirname = Filename.dirname filename in
......
319 319
    Printexc.record_backtrace true;
320 320
    Arg.parse Options.options anonymous usage
321 321
  with
322
  | Parse.Syntax_err _ | Lexer_lustre.Error _ 
322
  | Parse.Syntax_err _ | Lexer_lustre.Error _
323 323
  | Types.Error (_,_) | Clocks.Error (_,_)
324
  | Corelang.Error _ (*| Task_set.Error _*) 
324
  | Corelang.Error _ (*| Task_set.Error _*)
325 325
  | Causality.Cycle _ -> exit 1
326 326
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
327 327
  | exc -> (Utils.track_exception (); raise exc)

Also available in: Unified diff