Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/backends/C/c_backend_spec.ml
31 31
  pp_acsl_type id.var_id fmt id.var_type
32 32

  
33 33

  
34
let pp_econst fmt c = 
35
  match c with
36
    | EConst_int i -> pp_print_int fmt i
37
    | EConst_real r -> pp_print_string fmt r
38
    | EConst_float r -> pp_print_float fmt r
39
    | EConst_bool b -> pp_print_bool fmt b
40
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
41

  
42 34
let rec pp_eexpr is_output fmt eexpr = 
43 35
  let pp_eexpr = pp_eexpr is_output in
44 36
  match eexpr.eexpr_desc with
45
    | EExpr_const c -> pp_econst fmt c
37
    | EExpr_const c -> Printers.pp_econst fmt c
46 38
    | EExpr_ident id -> 
47 39
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
48 40
    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
src/corelang.ml
495 495

  
496 496
let rename_node f_node f_var f_const nd =
497 497
  let rename_var v = { v with var_id = f_var v.var_id } in
498
  let rename_eq eq = { eq with
499
      eq_lhs = List.map f_var eq.eq_lhs; 
500
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
501
    } 
502
  in
498 503
  let inputs = List.map rename_var nd.node_inputs in
499 504
  let outputs = List.map rename_var nd.node_outputs in
500 505
  let locals = List.map rename_var nd.node_locals in
......
502 507
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
503 508
  let node_asserts = List.map 
504 509
    (fun a -> 
505
      { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
506
    ) nd.node_asserts
507
  in
508
  let eqs = List.map 
509
    (fun eq -> { eq with
510
      eq_lhs = List.map f_var eq.eq_lhs; 
511
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
512
    } ) nd.node_eqs
510
      {a with assert_expr = 
511
	  let expr = a.assert_expr in
512
	  rename_expr f_node f_var f_const expr})
513
    nd.node_asserts
513 514
  in
515
  let eqs = List.map rename_eq nd.node_eqs in
514 516
  let spec = 
515 517
    Utils.option_map 
516 518
      (fun s -> rename_node_annot f_node f_var f_const s) 
......
643 645
    Basic_library.internal_funs
644 646

  
645 647

  
648

  
649
(* Replace any occurence of a var in vars_to_replace by its associated
650
   expression in defs until e does not contain any such variables *)
651
let rec substitute_expr vars_to_replace defs e =
652
  let se = substitute_expr vars_to_replace defs in
653
  { e with expr_desc = 
654
      let ed = e.expr_desc in
655
      match ed with
656
      | Expr_const _ -> ed
657
      | Expr_array el -> Expr_array (List.map se el)
658
      | Expr_access (e1, d) -> Expr_access (se e1, d)
659
      | Expr_power (e1, d) -> Expr_power (se e1, d)
660
      | Expr_tuple el -> Expr_tuple (List.map se el)
661
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
662
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
663
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
664
      | Expr_pre e' -> Expr_pre (se e')
665
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
666
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
667
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
668
      | Expr_ident i -> 
669
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
670
	  let eq_i eq = eq.eq_lhs = [i] in
671
	  if List.exists eq_i defs then
672
	    let sub = List.find eq_i defs in
673
	    let sub' = se sub.eq_rhs in
674
	    sub'.expr_desc
675
	  else 
676
	    assert false
677
	)
678
	else
679
	  ed
680

  
681
  }
682
(* FAUT IL RETIRER ?
683
  
684
 let rec expr_to_eexpr  expr =
685
   { eexpr_tag = expr.expr_tag;
686
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
687
     eexpr_type = expr.expr_type;
688
     eexpr_clock = expr.expr_clock;
689
     eexpr_loc = expr.expr_loc
690
   }
691
 and expr_desc_to_eexpr_desc expr_desc =
692
   let conv = expr_to_eexpr in
693
   match expr_desc with
694
   | Expr_const c -> EExpr_const (match c with
695
     | Const_int x -> EConst_int x 
696
     | Const_real x -> EConst_real x 
697
     | Const_float x -> EConst_float x 
698
     | Const_tag x -> EConst_tag x 
699
     | _ -> assert false
700

  
701
   )
702
   | Expr_ident i -> EExpr_ident i
703
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
704

  
705
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
706
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
707
   | Expr_pre e' -> EExpr_pre (conv e')
708
   | Expr_appl (i, e', i') -> 
709
     EExpr_appl 
710
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
711

  
712
   | Expr_when _
713
   | Expr_merge _ -> assert false
714
   | Expr_array _ 
715
   | Expr_access _ 
716
   | Expr_power _  -> assert false
717
   | Expr_ite (c, t, e) -> assert false 
718
   | _ -> assert false
719

  
720
     *)
646 721
let rec get_expr_calls nodes e =
647 722
  get_calls_expr_desc nodes e.expr_desc
648 723
and get_calls_expr_desc nodes expr_desc =
src/corelang.mli
80 80
| Expr_phclock of expr * rat
81 81
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)
82 82

  
83
type assert_t = 
84
    {
85
      assert_expr: expr;
86
      assert_loc: Location.t
87
    } 
88

  
89 83
type eq =
90 84
    {eq_lhs: ident list;
91 85
     eq_rhs: expr;
92 86
     eq_loc: Location.t}
93 87

  
88
type assert_t = 
89
    {
90
      assert_expr: expr * eq list;
91
      assert_loc: Location.t
92
    } 
93

  
94 94
type node_desc =
95 95
    {node_id: ident;
96 96
     mutable node_type: Types.type_expr;
......
250 250

  
251 251
val update_expr_annot: expr -> LustreSpec.expr_annot -> expr
252 252

  
253
val substitute_expr: var_decl list -> eq list -> expr -> expr
253 254

  
254 255
(** Annotation expression related functions *)
255 256
val mkeexpr: Location.t ->  expr -> eexpr
src/horn_backend.ml
20 20
  | Types.Tarrow _
21 21
  | _                     -> Format.eprintf "internal error: pp_type %a@." 
22 22
                             Types.print_ty t; assert false
23
    
24 23

  
25 24
let pp_decl_var fmt id = 
26 25
  Format.fprintf fmt "(declare-var %s %a)"
......
30 29
let pp_var fmt id = Format.pp_print_string fmt id.var_id
31 30

  
32 31

  
32
let pp_conj pp fmt l = 
33
  match l with 
34
    [] -> assert false
35
  | [x] -> pp fmt x
36
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
37
    
38

  
39

  
33 40
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x 
34 41
let rename f = (fun v -> {v with var_id = f v.var_id } )
35 42
let rename_machine p = rename (fun n -> concat p n)
......
134 141
      let (n,_) = List.assoc i m.minstances in
135 142
      match node_name n, inputs, outputs with
136 143
      | "_arrow", [i1; i2], [o] -> begin
137
         if init then
138
           pp_assign
139
   	     m
140
   	     self
141
   	     (pp_horn_var m) 
142
	     (* (pp_horn_val self (pp_horn_var m) fmt o) *)
143
	     fmt
144
   	     o.var_type (LocalVar o) i1
145
         else
146
           pp_assign
147
   	     m self (pp_horn_var m) fmt
148
   	     o.var_type (LocalVar o) i2
149
	     
144
        if init then
145
          pp_assign
146
   	    m
147
   	    self
148
   	    (pp_horn_var m) 
149
	    fmt
150
   	    o.var_type (LocalVar o) i1
151
        else
152
          pp_assign
153
   	    m self (pp_horn_var m) fmt
154
   	    o.var_type (LocalVar o) i2
155
	    
150 156
      end
151 157
      | name, _, _ ->  
152 158
	begin
153 159
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
154 160
	  if init then
155
	  Format.fprintf fmt "(%a %a%t%a%t%a)"
156
	    pp_machine_init_name (node_name n) 
157
	    (* inputs *)
158
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
159
	    (Utils.pp_final_char_if_non_empty " " inputs) 
160
	    (* outputs *)
161
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
162
	    (Utils.pp_final_char_if_non_empty " " outputs)
163
	    (* memories (next) *)
164
	    (Utils.fprintf_list ~sep:" " pp_var) (
165
  	      rename_machine_list 
166
		(concat m.mname.node_id i) 
167
		(rename_next_list (* concat m.mname.node_id i *) 
168
		   (full_memory_vars machines target_machine)
169
		) 
170
	     )
161
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
162
	      pp_machine_init_name (node_name n) 
163
	      (* inputs *)
164
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
165
	      inputs
166
	      (Utils.pp_final_char_if_non_empty " " inputs) 
167
	      (* outputs *)
168
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
169
	      (List.map (fun v -> LocalVar v) outputs)
170
	      (Utils.pp_final_char_if_non_empty " " outputs)
171
	      (* memories (next) *)
172
	      (Utils.fprintf_list ~sep:" " pp_var) (
173
  		rename_machine_list 
174
		  (concat m.mname.node_id i) 
175
		  (rename_next_list (full_memory_vars machines target_machine)
176
		  ) 
177
	       )
171 178
	  else
172 179
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
173 180
	      pp_machine_step_name (node_name n) 
174 181
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
175 182
	      (Utils.pp_final_char_if_non_empty " " inputs) 
176
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
183
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
184
	      (List.map (fun v -> LocalVar v) outputs)
177 185
	      (Utils.pp_final_char_if_non_empty " " outputs)
178 186
	      (Utils.fprintf_list ~sep:" " pp_var) (
179 187
		(rename_machine_list 
180 188
		   (concat m.mname.node_id i) 
181
		   (rename_current_list (* concat m.mname.node_id i *) 
182
		      (full_memory_vars machines target_machine))
189
		   (rename_current_list (full_memory_vars machines target_machine))
183 190
		) @ 
184 191
		  (rename_machine_list 
185 192
		     (concat m.mname.node_id i) 
186
		     (rename_next_list (* concat m.mname.node_id i *) 
187
			(full_memory_vars machines target_machine))
193
		     (rename_next_list (full_memory_vars machines target_machine))
188 194
		  ) 
189 195
	       )
190 196
	    
......
194 200
      let (n,_) = List.assoc i m.mcalls in
195 201
      Format.fprintf fmt "(%s %a%t%a)"
196 202
	(node_name n)
197
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
203
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
204
	inputs
198 205
	(Utils.pp_final_char_if_non_empty " " inputs) 
199
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
200
	(* (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs  *)
206
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
207
	(List.map (fun v -> LocalVar v) outputs)
201 208
    )
202 209

  
203 210
let pp_machine_init (m: machine_t) self fmt inst =
......
229 236
    pp_assign
230 237
      m self (pp_horn_var m) fmt
231 238
      i.var_type (StateVar i) v
232
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> assert false (* This should not happen anymore *)
233
(*    pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl))) *)
239
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> 
240
    assert false (* This should not happen anymore *)
234 241
  | MStep (il, i, vl) ->
235 242
    pp_instance_call machines ~init:init m self fmt i vl il
236 243
  | MBranch (g,hl) ->
237 244
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
238 245
    then (* boolean case, needs special treatment in C because truth value is not unique *)
239
	 (* may disappear if we optimize code by replacing last branch test with default *)
246
      (* may disappear if we optimize code by replacing last branch test with default *)
240 247
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
241 248
      let el = try List.assoc tag_false hl with Not_found -> [] in
242 249
      pp_conditional machines ~init:init m self fmt g tl el
......
279 286
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
280 287
       
281 288
       (* Rule for single predicate *)
282
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
283
	 (Utils.fprintf_list ~sep:"@ " 
284
	    (pp_instr 
285
	       true (* In this case, the boolean init can be set to true or false. 
286
		       The node is stateless. *)
287
	       m.mname.node_id)
288
	 ) 
289
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
290
	 (pp_conj (pp_instr 
291
		     true (* In this case, the boolean init can be set to true or false. 
292
			     The node is stateless. *)
293
		     m.mname.node_id)
294
	 )
289 295
	 m.mstep.step_instrs
290 296
	 pp_machine_stateless_name m.mname.node_id
291 297
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
......
295 301
       (* Declaring predicate *)
296 302
       Format.fprintf fmt "(declare-rel %a (%a))@."
297 303
	 pp_machine_init_name m.mname.node_id
298
	 (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
304
	 (Utils.fprintf_list ~sep:" " pp_type) 
305
	 (List.map (fun v -> v.var_type) (init_vars machines m));
299 306
       
300 307
       Format.fprintf fmt "(declare-rel %a (%a))@."
301 308
	 pp_machine_step_name m.mname.node_id
302
	 (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m));
309
	 (Utils.fprintf_list ~sep:" " pp_type) 
310
	 (List.map (fun v -> v.var_type) (step_vars machines m));
311
       
303 312
       Format.pp_print_newline fmt ();
304 313

  
305
   (* Rule for init *)
306
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
307
	 (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
314
       (* Rule for init *)
315
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
316
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
308 317
	 pp_machine_init_name m.mname.node_id
309 318
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
310 319

  
311
   (* Rule for step *)
312
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
313
	 (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
320
       (* Rule for step *)
321
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
322
	 (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
314 323
	 pp_machine_step_name m.mname.node_id
315 324
	 (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
325

  
326
       (* Adding assertions *)
327
       (match m.mstep.step_asserts with
328
       | [] -> ()
329
       | assertsl -> begin
330
	 let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
331
	 
332
	 Format.fprintf fmt "; Asserts@.";
333
	 Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@."
334
	   (pp_conj pp_val) assertsl;
335
	 
336
	 (** TEME: the following code is the one we described. But it generates a segfault in z3 
337
	 Format.fprintf fmt "; Asserts for init@.";
338
	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@."
339
	   (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
340
	   pp_machine_init_name m.mname.node_id
341
	   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m)
342
	   (pp_conj pp_val) assertsl; 
343
	  
344
	 Format.fprintf fmt "; Asserts for step@.";
345
	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@."
346
	   (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
347

  
348
	   pp_machine_step_name m.mname.node_id
349
	   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m)
350
	   (pp_conj pp_val) assertsl
351
      	 *)
352
       end
353
       );
354
       
316 355
(*
317 356
       match m.mspec with
318 357
	 None -> () (* No node spec; we do nothing *)
......
329 368

  
330 369

  
331 370

  
332
let main_print machines fmt = 
333
if !Options.main_node <> "" then 
334
  begin
335
    let node = !Options.main_node in
336
    let machine = get_machine machines node in
337

  
371
let collecting_semantics machines fmt node machine =
338 372
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
339 373
    (* We print the types of the main node "memory tree" TODO: add the output *)
340 374
    let main_output =
......
359 393
      else
360 394
	pp_machine_init_name, pp_machine_step_name
361 395
    in
362
    
396

  
363 397
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
364 398
      (Utils.fprintf_list ~sep:" " pp_type) 
365 399
      (List.map (fun v -> v.var_type) main_memory_next);
......
379 413
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
380 414
      step_name node
381 415
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
382
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
416
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next 
383 417

  
384
    Format.fprintf fmt "; Property def@.";
385
    Format.fprintf fmt "(declare-rel ERR ())@.";
386
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (and %a))@ (MAIN %a)@])@ ERR))@."
387
      (Utils.fprintf_list ~sep:" " pp_var) main_output
388
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
418
let check_prop machines fmt node machine =
419
  let main_output =
420
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
421
  in
422
  let main_memory_next = 
423
    (rename_next_list (full_memory_vars machines machine)) @ main_output
424
  in
425
  Format.fprintf fmt "; Property def@.";
426
  Format.fprintf fmt "(declare-rel ERR ())@.";
427
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
428
    (pp_conj pp_var) main_output
429
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
389 430
    ;
390
    Format.fprintf fmt "(query ERR)@.";
431
  if !Options.horn_queries then
432
    Format.fprintf fmt "(query ERR)@."
391 433

  
392
    ()
434

  
435
let cex_computation machines fmt node machine =
436
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
437
    (* We print the types of the cex node "memory tree" TODO: add the output *)
438
    let cex_input =
439
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
440
    in
441
    let cex_input_dummy = 
442
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
443
    in
444
    let cex_output =
445
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
446
    in
447
    let cex_output_dummy = 
448
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
449
    in
450
    let cex_memory_next = 
451
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
452
    in
453
    let cex_memory_current = 
454
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
455
    in
456

  
457
    (* Special case when the cex node is stateless *)
458
    let init_name, step_name = 
459
      if is_stateless machine then
460
	pp_machine_stateless_name, pp_machine_stateless_name
461
      else
462
	pp_machine_init_name, pp_machine_step_name
463
    in
464

  
465
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
466
      (Utils.fprintf_list ~sep:" " pp_type) 
467
      (List.map (fun v -> v.var_type) cex_memory_next);
468
    
469
    Format.fprintf fmt "; Initial set@.";
470
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
471
      init_name node
472
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
473
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
474

  
475
    Format.fprintf fmt "; Inductive def@.";
476
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
477
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
478
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
479
    Format.fprintf fmt 
480
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
481
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
482
      step_name node
483
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
484
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next 
485

  
486
let get_cex machines fmt node machine =
487
    let cex_input =
488
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
489
    in
490
    let cex_output =
491
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
492
    in
493
  let cex_memory_next = 
494
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
495
  in
496
  Format.fprintf fmt "; Property def@.";
497
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
498
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
499
    (pp_conj pp_var) cex_output
500
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
501
    ;
502
  if !Options.horn_queries then
503
    Format.fprintf fmt "(query CEXTRACE)@."
504

  
505

  
506
let main_print machines fmt = 
507
if !Options.main_node <> "" then 
508
  begin
509
    let node = !Options.main_node in
510
    let machine = get_machine machines node in
511

  
512

  
513
    collecting_semantics machines fmt node machine;
514
    check_prop machines fmt node machine;
515

  
516
    cex_computation machines fmt node machine;
517
    get_cex machines fmt node machine 
393 518
end
394 519

  
395 520

  
......
399 524
  main_print machines fmt 
400 525

  
401 526

  
527
let traces_file fmt basename prog machines =
528
  Format.fprintf fmt 
529
    "; Horn code traceability generated by %s@.; SVN version number %s@.@."
530
    (Filename.basename Sys.executable_name) 
531
    Version.number;
532

  
533
  (* We extract the annotation dealing with traceability *)
534
  let machines_traces = List.map (fun m -> 
535
    let traces : (ident * expr) list= 
536
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
537
      let filtered = 
538
	List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots 
539
      in
540
      let content = List.map snd filtered in
541
      (* Elements are supposed to be a pair (tuple): variable, expression *)
542
      List.map (fun ee -> 
543
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with 
544
	| [], Expr_tuple [v;e] -> (
545
	  match v.expr_desc with 
546
	  | Expr_ident vid -> vid, e 
547
	  | _ -> assert false )
548
	| _ -> assert false)
549
	content
550
    in
551
    
552
    m, traces
553

  
554
  ) machines
555
  in
556

  
557
  (* Compute memories associated to each machine *)
558
  let compute_mems m =
559
    let rec aux fst prefix m =
560
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
561
	List.fold_left (fun accu (id, (n, _)) -> 
562
	  let name = node_name n in 
563
	  if name = "_arrow" then accu else
564
	    let machine_n = get_machine machines name in
565
	    ( aux false ((id,machine_n)::prefix) machine_n ) 
566
	    @ accu
567
	) [] m.minstances 
568
    in
569
    aux true [] m
570
  in
571

  
572
  List.iter (fun m ->
573
    Format.fprintf fmt "; Node %s@." m.mname.node_id;
574
    
575
    let memories_old = 
576
      List.map (fun (p, v) -> 
577
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
578
	let traces = List.assoc machine machines_traces in
579
	if List.mem_assoc v.var_id traces then
580
	  (* We take the expression associated to variable v in the trace info *)
581
	  p, List.assoc v.var_id traces
582
	else
583
	  (* We keep the variable as is: we create an expression v *)
584
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
585
	    
586
      ) (compute_mems m) 
587
    in
588
    let memories_next = (* We remove the topest pre in each expression *)
589
      List.map 
590
	(fun (prefix, ee) -> 
591
	  match ee.expr_desc with 
592
	  | Expr_pre e -> prefix, e 
593
	  | _ -> Format.eprintf 
594
	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?" 
595
	    (Utils.fprintf_list ~sep:"," 
596
	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) 
597
	    (List.rev prefix) 
598
	    Printers.pp_expr ee; 
599
	    assert false)
600
	memories_old
601
    in
602

  
603
    let pp_prefix_rev fmt prefix =
604
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
605
    in
606

  
607
    Format.fprintf fmt "; Init predicate@.";
608

  
609
    Format.fprintf fmt "; horn encoding@.";
610
    Format.fprintf fmt "(%a %a)@."
611
      pp_machine_init_name m.mname.node_id
612
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
613

  
614
    Format.fprintf fmt "; original expressions@.";
615
    Format.fprintf fmt "(%a %a%t%a)@."
616
      pp_machine_init_name m.mname.node_id
617
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
618
      (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
619
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
620

  
621
    Format.pp_print_newline fmt ();
622
    Format.fprintf fmt "; Step predicate@.";
623

  
624
    Format.fprintf fmt "; horn encoding@.";
625
    Format.fprintf fmt "(%a %a)@."
626
      pp_machine_step_name m.mname.node_id
627
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
628
    Format.fprintf fmt "; original expressions@.";
629
    Format.fprintf fmt "(%a %a%t%a)@."
630
      pp_machine_step_name m.mname.node_id
631
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
632
      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
633
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
634
    Format.pp_print_newline fmt ();    
635
  ) (List.rev machines);
636
  
637

  
402 638
(* Local Variables: *)
403 639
(* compile-command:"make -C .." *)
404 640
(* End: *)
src/inliner.ml
7 7
  | _ -> false) 
8 8

  
9 9

  
10
let rename_expr rename expr = expr_replace_var rename expr
11
let rename_eq rename eq = 
12
  { eq with
13
    eq_lhs = List.map rename eq.eq_lhs; 
14
    eq_rhs = rename_expr rename eq.eq_rhs
15
  }
16

  
10 17
(* 
11 18
    expr, locals', eqs = inline_call id args' reset locals nodes
12 19

  
......
27 34
      node.node_id uid v;
28 35
    Format.flush_str_formatter ()
29 36
  in
30
  let eqs' = List.map 
31
    (fun eq -> { eq with
32
      eq_lhs = List.map rename eq.eq_lhs; 
33
      eq_rhs = expr_replace_var rename eq.eq_rhs
34
    } ) node.node_eqs
37
  let eqs' = List.map (rename_eq rename) node.node_eqs
35 38
  in
36 39
  let rename_var v = { v with var_id = rename v.var_id } in
37 40
  let inputs' = List.map rename_var node.node_inputs in
......
51 54
    loc 
52 55
    (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
53 56
  in
54
  expr , inputs'@outputs'@locals'@locals, assign_inputs::eqs'
57
  let asserts' = (* We rename variables in assert expressions *)
58
    List.map 
59
      (fun a -> 
60
	{a with assert_expr = 
61
	    let expr = a.assert_expr in
62
	    rename_expr rename expr
63
      })
64
      node.node_asserts 
65
  in
66
  expr, 
67
  inputs'@outputs'@locals'@locals, 
68
  assign_inputs::eqs',
69
  asserts'
55 70

  
56 71

  
57 72

  
......
65 80
*)
66 81
let rec inline_expr expr locals nodes =
67 82
  let inline_tuple el = 
68
    List.fold_right (fun e (el_tail, locals, eqs) -> 
69
      let e', locals', eqs' = inline_expr e locals nodes in
70
      e'::el_tail, locals', eqs'@eqs
71
    ) el ([], locals, [])
83
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
84
      let e', locals', eqs', asserts' = inline_expr e locals nodes in
85
      e'::el_tail, locals', eqs'@eqs, asserts@asserts'
86
    ) el ([], locals, [], [])
72 87
  in
73 88
  let inline_pair e1 e2 = 
74
    let el', l', eqs' = inline_tuple [e1;e2] in
89
    let el', l', eqs', asserts' = inline_tuple [e1;e2] in
75 90
    match el' with
76
    | [e1'; e2'] -> e1', e2', l', eqs'
91
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'
77 92
    | _ -> assert false
78 93
  in
79 94
  let inline_triple e1 e2 e3 = 
80
    let el', l', eqs' = inline_tuple [e1;e2;e3] in
95
    let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
81 96
    match el' with
82
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs'
97
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
83 98
    | _ -> assert false
84 99
  in
85 100
    
86 101
  match expr.expr_desc with
87 102
  | Expr_appl (id, args, reset) ->
88
    let args', locals', eqs' = inline_expr args locals nodes in 
103
    let args', locals', eqs', asserts' = inline_expr args locals nodes in 
89 104
    if List.exists (check_node_name id) nodes then 
90 105
      (* The node should be inlined *)
91
(*      let _ =     Format.eprintf "Inlining call to %s@." id in
92
  *)    let node = try List.find (check_node_name id) nodes 
106
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
107
      let node = try List.find (check_node_name id) nodes 
93 108
	with Not_found -> (assert false) in
94
      let node = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
109
      let node = 
110
	match node.top_decl_desc with Node nd -> nd | _ -> assert false in
95 111
      let node = inline_node node nodes in
96
      let expr, locals', eqs'' = 
112
      let expr, locals', eqs'', asserts'' = 
97 113
	inline_call expr args' reset locals' node in
98
      expr, locals', eqs'@eqs''
114
      expr, locals', eqs'@eqs'', asserts'@asserts''
99 115
    else 
100 116
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
101
      { expr with expr_desc = Expr_appl(id, args', reset)}, locals', eqs'
117
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
118
      locals', 
119
      eqs', 
120
      asserts'
102 121

  
103 122
  (* For other cases, we just keep the structure, but convert sub-expressions *)
104 123
  | Expr_const _ 
105
  | Expr_ident _ -> expr, locals, []
124
  | Expr_ident _ -> expr, locals, [], []
106 125
  | Expr_tuple el -> 
107
    let el', l', eqs' = inline_tuple el in
108
    { expr with expr_desc = Expr_tuple el' }, l', eqs'
126
    let el', l', eqs', asserts' = inline_tuple el in
127
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
109 128
  | Expr_ite (g, t, e) ->
110
    let g', t', e', l', eqs' = inline_triple g t e in
111
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs'
129
    let g', t', e', l', eqs', asserts' = inline_triple g t e in
130
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
112 131
  | Expr_arrow (e1, e2) ->
113
    let e1', e2', l', eqs' = inline_pair e1 e2 in
114
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs'
132
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
133
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
115 134
  | Expr_fby (e1, e2) ->
116
    let e1', e2', l', eqs' = inline_pair e1 e2 in
117
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs'
135
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
136
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
118 137
  | Expr_array el ->
119
    let el', l', eqs' = inline_tuple el in
120
    { expr with expr_desc = Expr_array el' }, l', eqs'
138
    let el', l', eqs', asserts' = inline_tuple el in
139
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
121 140
  | Expr_access (e, dim) ->
122
    let e', l', eqs' = inline_expr e locals nodes in 
123
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs'
141
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
142
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
124 143
  | Expr_power (e, dim) ->
125
    let e', l', eqs' = inline_expr e locals nodes in 
126
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs'
144
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
145
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
127 146
  | Expr_pre e ->
128
    let e', l', eqs' = inline_expr e locals nodes in 
129
    { expr with expr_desc = Expr_pre e' }, l', eqs'
147
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
148
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
130 149
  | Expr_when (e, id, label) ->
131
    let e', l', eqs' = inline_expr e locals nodes in 
132
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs'
150
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
151
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
133 152
  | Expr_merge (id, branches) ->
134
    let el, l', eqs' = inline_tuple (List.map snd branches) in
153
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
135 154
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
136
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs'
155
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
137 156
and inline_node nd nodes = 
138
  let new_locals, eqs = 
139
    List.fold_left (fun (locals, eqs) eq ->
140
      let eq_rhs', locals', new_eqs' = 
157
  let new_locals, eqs, asserts = 
158
    List.fold_left (fun (locals, eqs, asserts) eq ->
159
      let eq_rhs', locals', new_eqs', asserts' = 
141 160
	inline_expr eq.eq_rhs locals nodes 
142 161
      in
143
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs 
144
    ) (nd.node_locals, []) nd.node_eqs
162
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
163
    ) (nd.node_locals, [], nd.node_asserts) nd.node_eqs
145 164
  in
146 165
  { nd with
147 166
    node_locals = new_locals;
148
    node_eqs = eqs
167
    node_eqs = eqs;
168
    node_asserts = asserts;
149 169
  }
150 170

  
151 171
let inline_all_calls node nodes =
src/lustreSpec.ml
1 1
open Format
2 2

  
3 3
type ident = Utils.ident
4
type label = Utils.ident
5 4
type rat = Utils.rat
6 5
type tag = Utils.tag
6
type label = Utils.ident
7 7

  
8 8
type type_dec =
9 9
    {ty_dec_desc: type_dec_desc;
......
117 117
type assert_t = 
118 118
    {
119 119
      assert_expr: expr;
120
      assert_loc: Location.t
120
      assert_loc: Location.t;
121 121
    } 
122 122

  
123 123
type node_desc =
......
177 177
  | Already_bound_symbol of ident
178 178

  
179 179

  
180

  
181 180
(* Local Variables: *)
182 181
(* compile-command:"make -C .." *)
183 182
(* End: *)
src/machine_code.ml
86 86
  step_outputs: var_decl list;
87 87
  step_locals: var_decl list;
88 88
  step_instrs: instr_t list;
89
  step_asserts: value_t list;
89 90
}
90 91

  
91 92
type static_call = top_decl * (Dimension.dim_expr list)
......
103 104
}
104 105

  
105 106
let pp_step fmt s =
106
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@]@ "
107
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
107 108
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
108 109
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
109 110
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
110 111
    (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks
111 112
    (Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs
113
    (Utils.fprintf_list ~sep:", " pp_val) s.step_asserts
114

  
112 115

  
113 116
let pp_static_call fmt (node, args) =
114 117
 Format.fprintf fmt "%s<%a>"
......
117 120

  
118 121
let pp_machine fmt m =
119 122
  Format.fprintf fmt 
120
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ step     :@   @[<v 2>%a@]@ @]@ "
123
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ step     :@   @[<v 2>%a@]@ @  spec : @[%t@]@  annot : @[%a@]@]@ "
121 124
    m.mname.node_id
122 125
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
123 126
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
124 127
    (Utils.fprintf_list ~sep:"@ " pp_instr) m.minit
125 128
    pp_step m.mstep
129
    (fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
130
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
126 131

  
127 132
(* Returns the declared stateless status and the computed one. *)
128 133
let get_stateless_status m =
......
199 204
      step_instrs = [conditional (StateVar var_state)
200 205
			         [MStateAssign(var_state, Cst (const_of_bool false));
201 206
                                  MLocalAssign(var_output, LocalVar var_input1)]
202
                                 [MLocalAssign(var_output, LocalVar var_input2)] ]
207
                                 [MLocalAssign(var_output, LocalVar var_input2)] ];
208
      step_asserts = [];
203 209
    };
204 210
    mspec = None;
205 211
    mannot = [];
......
457 463
  ;
458 464

  
459 465
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
466
  (* memories, init instructions, node calls, local variables (including memories), step instrs *)
460 467
  let m, init, j, locals, s = translate_eqs nd init_args (List.rev eqs_rev) in
461 468
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
462 469
  {
......
479 486
	| "horn" -> s
480 487
	| "C" | "java" | _ -> join_guards_list s
481 488
      );
489
      step_asserts = 
490
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
491
	List.map (translate_expr nd init_args) exprl
492
	;
482 493
    };
483 494
    mspec = nd.node_spec;
484 495
    mannot = nd.node_annot;
src/main_lustre_compiler.ml
356 356
	let source_file = destname ^ ".smt2" in (* Could be changed *)
357 357
	let source_out = open_out source_file in
358 358
	let fmt = formatter_of_out_channel source_out in
359
	Horn_backend.translate fmt basename prog machine_code
359
	Horn_backend.translate fmt basename prog machine_code;
360
	(* Tracability file if option is activated *)
361
	if !Options.horntraces then (
362
	let traces_file = destname ^ ".traces" in (* Could be changed *)
363
	let traces_out = open_out traces_file in
364
	let fmt = formatter_of_out_channel traces_out in
365
	Horn_backend.traces_file fmt basename prog machine_code	  
366
	)
360 367
      end
361 368
    | "lustre" -> 
362 369
      begin
src/normalization.ml
196 196
    let defvars, norm_elist =
197 197
      normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
198 198
    defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
199
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id && Types.is_array_type expr.expr_type ->
200
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
199
  | Expr_appl (id, args, None) 
200
      when Basic_library.is_internal_fun id 
201
	&& Types.is_array_type expr.expr_type ->
202
    let defvars, norm_args = 
203
      normalize_list 
204
	alias
205
	node
206
	offsets 
207
	(fun _ -> normalize_array_expr ~alias:true) 
208
	defvars 
209
	(expr_list_of_expr args) 
210
    in
201 211
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
202 212
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
203 213
    let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
......
341 351
    let norm_eq = { eq with eq_rhs = norm_rhs } in
342 352
    norm_eq::defs', vars'
343 353

  
354
(** normalize_node node returns a normalized node, 
355
    ie. 
356
    - updated locals
357
    - new equations
358
    - 
359
*)
344 360
let normalize_node node = 
345 361
  cpt_fresh := 0;
346 362
  let inputs_outputs = node.node_inputs@node.node_outputs in
347 363
  let is_local v =
348 364
    List.for_all ((!=) v) inputs_outputs in
365
  let orig_vars = inputs_outputs@node.node_locals in
349 366
  let defs, vars = 
350
    List.fold_left (normalize_eq node) ([], inputs_outputs@node.node_locals) node.node_eqs in
367
    List.fold_left (normalize_eq node) ([], orig_vars) node.node_eqs in
368
  (* Normalize the asserts *)
369
  let vars, assert_defs, asserts = 
370
    List.fold_left (
371
    fun (vars, def_accu, assert_accu) assert_ ->
372
      let assert_expr = assert_.assert_expr in
373
      let (defs, vars'), expr = 
374
	normalize_expr 
375
	  ~alias:false 
376
	  node 
377
	  [] (* empty offset for arrays *)
378
	  ([], vars) (* defvar only contains vars *)
379
	  assert_expr
380
      in
381
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
382
    ) (vars, [], []) node.node_asserts in
351 383
  let new_locals = List.filter is_local vars in
384
  (* Compute tracebaility info: 
385
     - gather newly bound variables
386
     - compute the associated expression without aliases     
387
  *)
388
  let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
389
  let norm_traceability = {
390
    annots = 
391
      List.map 
392
	(fun v -> 
393
	  let expr = substitute_expr diff_vars defs (
394
	    let eq = List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs in
395
	    eq.eq_rhs) in 
396
	  let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
397
	  ["horn_backend";"trace"], pair 
398
    ) 
399
    diff_vars ;
400
    annot_loc = Location.dummy_loc
401
  }
402

  
403
  in
352 404
  let node =
353
  { node with node_locals = new_locals; node_eqs = defs }
405
  { node with 
406
    node_locals = new_locals; 
407
    node_eqs = defs @ assert_defs;
408
    node_asserts = asserts;
409
    node_annot = norm_traceability::node.node_annot;
410
  }
354 411
  in ((*Printers.pp_node Format.err_formatter node;*) node)
355 412

  
356 413
let normalize_decl decl =
src/options.ml
36 36
let global_inline = ref false
37 37
let witnesses = ref false
38 38
let optimization = ref 2
39
let horntraces = ref false
40
let horn_queries = ref false
39 41

  
40 42
let options =
41 43
  [ "-d", Arg.Set_string dest_dir,
......
51 53
    "-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";
52 54
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
53 55
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
56
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
57
    "-horn-queries", Arg.Set horn_queries, "add the queries instructions at the end of the generated horn files";
54 58
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
55 59
    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
56 60
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
src/printers.ml
40 40

  
41 41
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
42 42

  
43
let pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type
44

  
45
let pp_node_var fmt id = fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock
46

  
47
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
48

  
49
let pp_quantifiers fmt (q, vars) =
50
  match q with
51
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
52
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
53

  
54
(*
55
let pp_econst fmt c = 
56
  match c with
57
    | EConst_int i -> pp_print_int fmt i
58
    | EConst_real r -> pp_print_string fmt r
59
    | EConst_float r -> pp_print_float fmt r
60
    | EConst_tag  t -> pp_print_string fmt t
61
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
62

  
63

  
64
let rec pp_eexpr fmt eexpr = 
65
  match eexpr.eexpr_desc with
66
    | EExpr_const c -> pp_econst fmt c
67
    | EExpr_ident id -> pp_print_string fmt id
68
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
69
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
70
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
71
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
72
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
73
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
74
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
75
    | EExpr_merge (id, e1, e2) -> 
76
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
77
    | EExpr_appl (id, e, r) -> pp_eapp fmt id e r
78
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
79
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
80

  
81

  
82
    (* | EExpr_whennot _ *)
83
    (* | EExpr_uclock _ *)
84
    (* | EExpr_dclock _ *)
85
    (* | EExpr_phclock _ -> assert false *)
86
and pp_eapp fmt id e r =
87
  match r with
88
  | None ->
89
    (match id, e.eexpr_desc with
90
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
91
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
92
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
93
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
94
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
95
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
96
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
97
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
98
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
99
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
100
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
101
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
102
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
103
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
104
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
105
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
106
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
107
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
108
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
109
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
110
*)
111

  
112

  
43 113
let rec pp_struct_const_field fmt (label, c) =
44 114
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
45 115
and pp_const fmt c = 
......
52 122
    | Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
53 123
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
54 124

  
55
and pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type
56

  
57
and pp_node_var fmt id = fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock
58 125

  
59
and pp_expr fmt expr =
60
  match expr.expr_desc with
126
let rec pp_expr fmt expr =
127
  (match expr.expr_annot with 
128
  | None -> fprintf fmt "%t" 
129
  | Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann)
130
    (fun fmt -> 
131
      match expr.expr_desc with
61 132
    | Expr_const c -> pp_const fmt c
62 133
    | Expr_ident id -> Format.fprintf fmt "%s" id
63 134
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
......
72 143
    | Expr_merge (id, hl) -> 
73 144
      fprintf fmt "merge %s %a" id pp_handlers hl
74 145
    | Expr_appl (id, e, r) -> pp_app fmt id e r
75

  
146
    )
76 147
and pp_tuple fmt el =
77 148
 fprintf_list ~sep:"," pp_expr fmt el
78 149

  
......
107 178
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
108 179
)
109 180
  | Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x 
181

  
182

  
183

  
184
and pp_eexpr fmt e =
185
  fprintf fmt "%a%t %a"
186
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
187
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
188
    pp_expr e.eexpr_qfexpr
189

  
190

  
191
and pp_expr_annot fmt expr_ann =
192
  let pp_annot fmt (kwds, ee) =
193
    Format.fprintf fmt "(*! %t: %a *)"
194
      (fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (fprintf_list ~sep:"/" Format.pp_print_string) kwds)
195
      pp_eexpr ee
196
  in
197
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
198
    
110 199
	
111 200
let pp_node_eq fmt eq = 
112 201
  fprintf fmt "%a = %a;" 
......
115 204

  
116 205
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq 
117 206

  
118
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
119 207

  
120 208
let pp_var_type_dec fmt ty =
121 209
  let rec pp_var_struct_type_field fmt (label, tdesc) =
......
146 234
(*   ) *)
147 235

  
148 236

  
149

  
150
let pp_quantifiers fmt (q, vars) =
151
  match q with
152
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
153
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
154

  
155
let pp_eexpr fmt e =
156
  fprintf fmt "%a%t %a"
157
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
158
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
159
    pp_expr e.eexpr_qfexpr
160

  
161 237
let pp_spec fmt spec =
162 238
  fprintf fmt "@[<hov 2>(*@@ ";
163 239
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
......
171 247
  fprintf fmt "@]*)";
172 248
  ()
173 249

  
250

  
251
let pp_asserts fmt asserts =
252
  match asserts with 
253
  | _::_ -> (
254
  fprintf fmt "(* Asserts definitions *)@ ";
255
  fprintf_list ~sep:"@ " (fun fmt assert_ -> 
256
    let expr = assert_.assert_expr in
257
    fprintf fmt "assert %a;" pp_expr expr 
258
  ) fmt asserts 
259
  )
260
  | _ -> ()
261
    
174 262
let pp_node fmt nd = 
175
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@]@ @]@.tel@]@."
263
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."
176 264
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
177 265
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")
178 266
  (if nd.node_dec_stateless then "function" else "node")
......
193 281
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
194 282
      checks
195 283
  ) nd.node_checks
284
  (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot
196 285
  pp_node_eqs nd.node_eqs
286
  pp_asserts nd.node_asserts
197 287
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
198 288

  
199 289
let pp_imported_node fmt ind = 
src/typing.ml
647 647
  let undefined_vars =
648 648
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
649 649
  in
650
  (* Typing asserts *)
651
  List.iter (fun assert_ ->
652
    let assert_expr =  assert_.assert_expr in
653
    type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool
654
  )  nd.node_asserts;
655
  
650 656
  (* check that table is empty *)
651 657
  if (not (IMap.is_empty undefined_vars)) then
652 658
    raise (Error (loc, Undefined_var undefined_vars));
test/test-compile.sh
151 151
    else
152 152
	$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus
153 153
    fi
154
    if [ $? -ne 0 ]; then
155
        rlustrec="INVALID";
156
    else
157
        rlustrec="VALID"
158
    fi
154 159
    # echo "z3 $build/$name".smt2 
155 160
    # TODO: This part of the script has to be optimized
156 161
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
......
160 165
        rhorn="VALID"
161 166
    fi
162 167
    if [ $verbose -gt 0 ]; then
163
	echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
168
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
164 169
    else
165
	echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
170
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
166 171
    fi
167 172
    popd > /dev/null
168 173
done < $file_list

Also available in: Unified diff