Project

General

Profile

Revision 7d77632f src/tools/zustre/zustre_common.ml

View differences:

src/tools/zustre/zustre_common.ml
90 90
  | _                     -> Format.eprintf "internal error: pp_type %a@."
91 91
                               Types.print_ty t; assert false
92 92

  
93

  
94
(* let idx_var = *)
95
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort  *)
96
    
97
(* let uid_var = *)
98
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort  *)
99

  
93 100
(** Func decls
94 101

  
95 102
    Similarly fun_decls are registerd, by their name, into a hashtbl. The
......
116 123
  register_fdecl id.var_id fdecl;
117 124
  fdecl
118 125

  
119
let decl_rel name args_sorts =
120
  (*verifier ce qui est construit. On veut un declare-rel *)
126
let idx_sort = int_sort
127
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
128
let uid_conc = 
129
  let fd = Z3.Z3List.get_cons_decl uid_sort in
130
  fun head tail -> Z3.FuncDecl.apply fd [head;tail]
131

  
132
let get_instance_uid =
133
  let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in
134
  let cpt = ref 0 in
135
  fun i ->
136
    let id =
137
      if Hashtbl.mem hash i then
138
	Hashtbl.find hash i
139
      else (
140
	incr cpt;
141
	Hashtbl.add hash i !cpt;
142
	!cpt
143
      )
144
    in
145
    Z3.Arithmetic.Integer.mk_numeral_i !ctx id
146
  
147

  
148
  
149
let decl_rel ?(no_additional_vars=false) name args_sorts =
150
  (* Enriching arg_sorts with two new variables: a counting index and an
151
     uid *)
152
  let args_sorts =
153
    if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in
121 154
  
122 155
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
123 156
  if !debug then
......
133 166
  fdecl
134 167
  
135 168

  
169

  
170
(* Shared variables to describe counter and uid *)
171

  
172
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int
173
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) 
174
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
175
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort 
176
let _ = register_fdecl "__uid__"  uid_fd  
177
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 
178

  
136 179
(** Conversion functions
137 180

  
138 181
    The following is similar to the Horn backend. Each printing function is
......
412 455
  let (n,_) = List.assoc i m.minstances in
413 456
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
414 457
  let vars =
415
    (
416
      (rename_machine_list
417
	 (concat m.mname.node_id i)
418
	 (rename_current_list (full_memory_vars machines target_machine))
419
      ) 
420
      @
421
	(rename_machine_list
422
	   (concat m.mname.node_id i)
423
	   (rename_mid_list (full_memory_vars machines target_machine))
424
	)
458
    (rename_machine_list
459
       (concat m.mname.node_id i)
460
       (rename_current_list (full_memory_vars machines target_machine))@  (rename_mid_list (full_memory_vars machines target_machine))
425 461
    )
462
    
426 463
  in
427 464
  let expr =
428 465
    Z3.Expr.mk_app
429 466
      !ctx
430 467
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
431
      (List.map (horn_var_to_expr) vars)
468
      (List.map (horn_var_to_expr) (idx::uid::vars))
432 469
  in
433 470
  [expr]
434 471

  
435 472
let instance_call_to_exprs machines reset_instances m i inputs outputs =
436 473
  let self = m.mname.node_id in
474

  
475
  (* Building call args *)
476
  let idx_uid_inout =
477
    (* Additional input to register step counters, and uid *)
478
    let idx = horn_var_to_expr idx in
479
    let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
480
    let inout = 
481
      List.map (horn_val_to_expr self)
482
	(inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs))
483
    in
484
    idx::uid::inout
485
  in
486
    
437 487
  try (* stateful node instance *)
438 488
    begin
439 489
      let (n,_) = List.assoc i m.minstances in
......
454 504
      let next_mems = rename_mems rename_next_list in
455 505

  
456 506
      let call_expr = 
457
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
458
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
507
	match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
508
	| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
459 509
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
460 510
            Z3.Boolean.mk_eq !ctx
461 511
              ( (* output var *)
......
477 527
              (Z3.Boolean.mk_false !ctx)
478 528
          in
479 529
          [stmt1; stmt2]
480
      end
481

  
482
      | node_name_n ->
483
         let expr = 
484
           Z3.Expr.mk_app
485
             !ctx
486
             (get_fdecl (machine_step_name (node_name n)))
487
             ( (* Arguments are input, output, mid_mems, next_mems *)
488
               (
489
                 List.map (horn_val_to_expr self) (
490
                     inputs @
491
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
492
                   )
493
               ) @ (
494
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
495
	       )
496
             )
497
         in
498
         [expr]
530
	end
531

  
532
	| node_name_n ->
533
           let expr = 
534
             Z3.Expr.mk_app
535
               !ctx
536
               (get_fdecl (machine_step_name (node_name n)))
537
               ( (* Arguments are input, output, mid_mems, next_mems *)
538
		 idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems)
539
		    
540
               )
541
           in
542
           [expr]
499 543
      in
500 544

  
501 545
      reset_exprs@call_expr
......
506 550
      Z3.Expr.mk_app
507 551
        !ctx
508 552
        (get_fdecl (machine_stateless_name (node_name n)))
509
        ((* Arguments are inputs, outputs *)
510
         List.map (horn_val_to_expr self)
511
           (
512
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
513
           )
514
        )
553
        idx_uid_inout 	  (* Arguments are inputs, outputs *)
515 554
    in
516 555
    [expr]
517 556
  )
......
747 786
	  !ctx
748 787
	  (get_fdecl (name ^ "_reset"))
749 788
	  (List.map (horn_var_to_expr)
750
	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
751
	  )
789
	     (idx::uid:: (* Additional vars: counters, uid *)
790
	      	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
791
	  ))
752 792
	  
753 793
      )
754 794
    ) m.minstances
......
798 838
	    Z3.Expr.mk_app
799 839
	      !ctx
800 840
	      (get_fdecl (machine_stateless_name m.mname.node_id))
801
	      (List.map (horn_var_to_expr) vars)
841
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
802 842
	  in
803 843
	  (* this line seems useless *)
804
	  let vars = vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
844
	  let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
805 845
	  (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
806 846
	  match m.mstep.step_asserts with
807 847
	  | [] ->
......
836 876
	    Z3.Expr.mk_app
837 877
	      !ctx
838 878
	      (get_fdecl (machine_reset_name m.mname.node_id))
839
	      (List.map (horn_var_to_expr) vars)
879
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
840 880
	  in
841 881

  
842 882
	  
843 883
	  let _ =
844
	    add_rule vars (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
884
	    add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
845 885
	      
846 886
	  in
847 887

  
......
860 900
	    Z3.Expr.mk_app
861 901
	      !ctx
862 902
	      (get_fdecl (machine_step_name m.mname.node_id))
863
	      (List.map (horn_var_to_expr) vars)
903
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
864 904
	  in
865 905
	  match m.mstep.step_asserts with
866 906
	  | [] ->
867 907
	     begin
868 908
	       (* Rule for single predicate *) 
869 909
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
870
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
910
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
871 911
		 
872 912
	     end
873 913
	  | assertsl ->
......
878 918
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
879 919
	       in
880 920
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
881
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
921
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
882 922
		 
883 923
	     end
884 924
     	       

Also available in: Unified diff