Project

General

Profile

Revision 86ae18b7 src/backends/Horn/horn_backend_printers.ml

View differences:

src/backends/Horn/horn_backend_printers.ml
21 21
open Machine_code
22 22

  
23 23
open Horn_backend_common
24

  
24
open Types
25 25

  
26 26
(********************************************************************************************)
27 27
(*                    Instruction Printing functions                                        *)
28 28
(********************************************************************************************)
29 29

  
30 30
let pp_horn_var m fmt id =
31
  if Types.is_array_type id.var_type
31
  (*if Types.is_array_type id.var_type
32 32
  then
33 33
    assert false (* no arrays in Horn output *)
34
  else
34
  else*)
35 35
    fprintf fmt "%s" id.var_id
36 36

  
37 37
(* Used to print boolean constants *)
......
46 46
    | Const_tag t    -> pp_horn_tag fmt t
47 47
    | _              -> assert false
48 48

  
49
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *)
50
(* let rec get_type_cst c = *)
51
(*   match c with *)
52
(*   | Const_int(n) -> new_ty Tint *)
53
(*   | Const_real _ -> new_ty Treal *)
54
(*   (\* | Const_float _ -> new_ty Treal *\) *)
55
(*   | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *)
56
(* 				     get_type_cst (List.hd l))) *)
57
(*   | Const_tag(tag) -> new_ty Tbool *)
58
(*   | Const_string(str) ->  assert false(\* used only for annotations *\) *)
59
(*   | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *)
60

  
61
(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *)
62

  
63
(*
64
let rec get_type v =
65
  match v with
66
  | Cst c -> Typing.type_const Location.dummy_loc c (* get_type_cst c*)
67
  | Access(tab, index) -> begin
68
      let rec remove_link ltype =
69
        match (dynamic_type ltype).tdesc with
70
        | Tlink t -> t
71
        | _ -> ltype
72
      in
73
      match (dynamic_type (remove_link (get_type tab))).tdesc with
74
      | Tarray(size, t) -> remove_link t
75
      | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
76
      | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
77
      | _ -> Format.eprintf "Type of access is not an array "; assert false
78
                          end
79
  | Power(v, n) -> assert false
80
  | LocalVar v -> v.var_type
81
  | StateVar v -> v.var_type
82
  | Fun(n, vl) -> begin match n with
83
                  | "+"
84
                  | "-"
85
                  | "*" -> get_type (List.hd vl)
86
                  | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
87
                  end
88
  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int
89
                                 (Location.dummy_loc)
90
                                 (List.length l),
91
                               get_type (List.hd l)))
92
  | _ -> assert false
93
*)
94

  
95
(* Default value for each type, used when building arrays. Eg integer array
96
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
97
   for the type integer (arrays).
98
*)
99
let rec pp_default_val fmt t =
100
  match (dynamic_type t).tdesc with
101
  | Tint -> fprintf fmt "0"
102
  | Treal -> fprintf fmt "0"
103
  | Tbool -> fprintf fmt "true"
104
  | Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
105
     let valt = array_element_type t in
106
     fprintf fmt "((as const (Array Int %a)) %a)"
107
       pp_type valt 
108
       pp_default_val valt
109
  | Tstruct(l) -> assert false
110
  | Ttuple(l) -> assert false
111
  |_ -> assert false
112

  
113

  
49 114
(* Prints a value expression [v], with internal function calls only.
50 115
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
51 116
   but an offset suffix may be added for array variables
52 117
*)
53 118
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
54 119
  match v.value_desc with
55
    | Cst c         -> pp_horn_const fmt c
56
    | Array _
57
    | Access _ -> assert false (* no arrays *)
58
    | Power (v, n)  -> assert false
59
    | LocalVar v    -> pp_var fmt (rename_machine self v)
60
    | StateVar v    ->
61
      if Types.is_array_type v.var_type
62
      then assert false
63
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
64
    | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
120
  | Cst c       -> pp_horn_const fmt c
121

  
122
  (* Code specific for arrays *)
123
  | Array il    ->
124
     (* An array definition: 
125
	(store (
126
	  ...
127
 	    (store (
128
	       store (
129
	          default_val
130
	       ) 
131
	       idx_n val_n
132
	    ) 
133
	    idx_n-1 val_n-1)
134
	  ... 
135
	  idx_1 val_1
136
	) *)
137
     let rec print fmt (tab, x) =
138
       match tab with
139
       | [] -> pp_default_val fmt v.value_type(* (get_type v) *)
140
       | h::t ->
141
	  fprintf fmt "(store %a %i %a)"
142
	    print (t, (x+1))
143
	    x
144
	    (pp_horn_val ~is_lhs:is_lhs self pp_var) h
145
     in
146
     print fmt (il, 0)
147
       
148
  | Access(tab,index) ->
149
     fprintf fmt "(select %a %a)"
150
       (pp_horn_val ~is_lhs:is_lhs self pp_var) tab
151
       (pp_horn_val ~is_lhs:is_lhs self pp_var) index
152

  
153
  (* Code specific for arrays *)
154
    
155
  | Power (v, n)  -> assert false
156
  | LocalVar v    -> pp_var fmt (rename_machine self v)
157
  | StateVar v    ->
158
     if Types.is_array_type v.var_type
159
     then assert false
160
     else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
161
  | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
65 162

  
66 163
(* Prints a [value] indexed by the suffix list [loop_vars] *)
67 164
let rec pp_value_suffix self pp_value fmt value =
......
79 176
*)
80 177
let pp_assign m pp_var fmt var_name value =
81 178
  let self = m.mname.node_id in
82
  fprintf fmt "(= %a %a)" 
179
  fprintf fmt "(= %a %a)"
83 180
    (pp_horn_val ~is_lhs:true self pp_var) var_name
84 181
    (pp_value_suffix self pp_var) value
85
    
182

  
86 183

  
87 184
(* In case of no reset call, we define mid_mem = current_mem *)
88 185
let pp_no_reset machines m fmt i =
89 186
  let (n,_) = List.assoc i m.minstances in
90 187
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
91 188

  
92
  let m_list = 
189
  let m_list =
93 190
    rename_machine_list
94 191
      (concat m.mname.node_id i)
95 192
      (rename_mid_list (full_memory_vars machines target_machine))
......
104 201
    fprintf fmt "(= %a %a)"
105 202
      (pp_horn_var m) mhd
106 203
      (pp_horn_var m) chd
107
  
204

  
108 205
  | _ -> (
109 206
    fprintf fmt "@[<v 0>(and @[<v 0>";
110
    List.iter2 (fun mhd chd -> 
207
    List.iter2 (fun mhd chd ->
111 208
      fprintf fmt "(= %a %a)@ "
112 209
      (pp_horn_var m) mhd
113 210
      (pp_horn_var m) chd
......
120 217
let pp_instance_reset machines m fmt i =
121 218
  let (n,_) = List.assoc i m.minstances in
122 219
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
123
  
220

  
124 221
  fprintf fmt "(%a @[<v 0>%a)@]"
125 222
    pp_machine_reset_name (node_name n)
126
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
223
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
127 224
    (
128 225
      (rename_machine_list
129 226
	 (concat m.mname.node_id i)
130 227
	 (rename_current_list (full_memory_vars machines target_machine))
131
      ) 
228
      )
132 229
      @
133 230
	(rename_machine_list
134 231
	   (concat m.mname.node_id i)
......
146 243
      if not (List.mem i reset_instances) then
147 244
	(* If not, declare mem_m = mem_c *)
148 245
	pp_no_reset machines m fmt i;
149
      
246

  
150 247
      let mems = full_memory_vars machines target_machine in
151 248
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
152 249
      let mid_mems = rename_mems rename_mid_list in
......
157 254
	fprintf fmt "@[<v 5>(and ";
158 255
	fprintf fmt "(= %a (ite %a %a %a))"
159 256
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
160
	  (pp_horn_var m) mem_m 
257
	  (pp_horn_var m) mem_m
161 258
	  (pp_horn_val self (pp_horn_var m)) i1
162 259
	  (pp_horn_val self (pp_horn_var m)) i2
163 260
	;
......
175 272
	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
176 273
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
177 274
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
178
	
275

  
179 276
      end
180 277
    end
181 278
  with Not_found -> ( (* stateless node instance *)
......
188 285
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
189 286
      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
190 287
  )
191
    
192
    
288

  
289

  
193 290
(* Print the instruction and update the set of reset instances *)
194 291
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
195 292
  match instr with
......
230 327
       statement. *)
231 328
    let self = m.mname.node_id in
232 329
    let pp_branch fmt (tag, instrs) =
233
      fprintf fmt 
234
	"@[<v 3>(or (not (= %a %s))@ " 
330
      fprintf fmt
331
	"@[<v 3>(or (not (= %a %s))@ "
235 332
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
236 333
					  seems that => within Horn predicate
237 334
					  may cause trouble. I have hard time
......
244 341
      () (* rs *)
245 342
    in
246 343
    pp_conj pp_branch fmt hl;
247
    reset_instances 
344
    reset_instances
248 345

  
249
and pp_machine_instrs machines reset_instances m fmt instrs = 
346
and pp_machine_instrs machines reset_instances m fmt instrs =
250 347
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
251 348
  match instrs with
252
  | [x] -> ppi reset_instances fmt x 
349
  | [x] -> ppi reset_instances fmt x
253 350
  | _::_ ->
254 351
    fprintf fmt "(and @[<v 0>";
255
    let rs = List.fold_left (fun rs i -> 
352
    let rs = List.fold_left (fun rs i ->
256 353
      let rs = ppi rs fmt i in
257 354
      fprintf fmt "@ ";
258 355
      rs
259 356
    )
260
      reset_instances instrs 
357
      reset_instances instrs
261 358
    in
262 359
    fprintf fmt "@])";
263 360
    rs
......
269 366
  fprintf fmt "@[<v 5>(and @ ";
270 367

  
271 368
  (* print "x_m = x_c" for each local memory *)
272
  (Utils.fprintf_list ~sep:"@ " (fun fmt v -> 
369
  (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
273 370
    fprintf fmt "(= %a %a)"
274 371
      (pp_horn_var m) (rename_mid v)
275 372
      (pp_horn_var m) (rename_current v)
......
281 378
  *)
282 379
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
283 380
    let name = node_name n in
284
    if name = "_arrow" then ( 
381
    if name = "_arrow" then (
285 382
      fprintf fmt "(= %s._arrow._first_m true)"
286
	(concat m.mname.node_id id)  
383
	(concat m.mname.node_id id)
287 384
    ) else (
288
      let machine_n = get_machine machines name in 
289
      fprintf fmt "(%s_reset @[<hov 0>%a@])" 
385
      let machine_n = get_machine machines name in
386
      fprintf fmt "(%s_reset @[<hov 0>%a@])"
290 387
	name
291
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
388
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
292 389
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
293 390
    )
294 391
   )) fmt m.minstances;
......
314 411
  else
315 412
    begin
316 413
      fprintf fmt "; %s@." m.mname.node_id;
317
      
414

  
318 415
      (* Printing variables *)
319 416
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
320 417
	(
......
358 455

  
359 456
	  (* Rule for reset *)
360 457
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
361
	    (pp_machine_reset machines) m 
458
	    (pp_machine_reset machines) m
362 459
	    pp_machine_reset_name m.mname.node_id
363 460
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
364 461

  
......
373 470
		pp_machine_step_name m.mname.node_id
374 471
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
375 472
	    end
376
	  | assertsl -> 
473
	  | assertsl ->
377 474
	    begin
378 475
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
379 476
	      (* print_string pp_val; *)
380 477
	      fprintf fmt "; with Assertions @.";
381
	      
478

  
382 479
	      (*Rule for step*)
383 480
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
384 481
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
......
386 483
		pp_machine_step_name m.mname.node_id
387 484
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
388 485
	    end
389
	      
390
	      
486

  
487

  
391 488
	end
392 489
    end
393 490

  
394 491

  
492
let mk_flags arity =
493
  let b_range =
494
   let rec range i j =
495
     if i > arity then [] else i :: (range (i+1) j) in
496
   range 2 arity;
497
 in
498
 List.fold_left (fun acc x -> acc ^ " false") "true" b_range
499

  
500

  
501
  (*Get sfunction infos from command line*)
502
let get_sf_info() =
503
  let splitted = Str.split (Str.regexp "@") !Options.sfunction in
504
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
505
  let sf_name, flags, arity = match splitted with
506
      [h;flg;par] -> h, flg, par
507
    | _ -> failwith "Wrong Sfunction info"
508

  
509
  in
510
  Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
511
  sf_name, flags, arity
512

  
513

  
514
    (*a function to print the rules in case we have an s-function*)
515
  let print_sfunction machines fmt m =
516
      if m.mname.node_id = arrow_id then
517
        (* We don't print arrow function *)
518
        ()
519
      else
520
        begin
521
          Format.fprintf fmt "; SFUNCTION@.";
522
          Format.fprintf fmt "; %s@." m.mname.node_id;
523
          Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
524

  
525
          (* Check if there is annotation for s-function *)
526
          if m.mannot != [] then(
527
              Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
528
            );
529

  
530
       (* Printing variables *)
531
          Utils.fprintf_list ~sep:"@." pp_decl_var fmt
532
                             ((step_vars machines m)@
533
    	                        (rename_machine_list m.mname.node_id m.mstep.step_locals));
534
          Format.pp_print_newline fmt ();
535
          let sf_name, flags, arity = get_sf_info() in
536

  
537
       if is_stateless m then
538
         begin
539
           (* Declaring single predicate *)
540
           Format.fprintf fmt "(declare-rel %a (%a))@."
541
    	                  pp_machine_stateless_name m.mname.node_id
542
    	                  (Utils.fprintf_list ~sep:" " pp_type)
543
    	                  (List.map (fun v -> v.var_type) (reset_vars machines m));
544
           Format.pp_print_newline fmt ();
545
           (* Rule for single predicate *)
546
           let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
547
           Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
548
                          str_flags
549
                          (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m)
550
	                  pp_machine_stateless_name m.mname.node_id
551
	                  (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m);
552
         end
553
      else
554
         begin
555
           (* Declaring predicate *)
556
           Format.fprintf fmt "(declare-rel %a (%a))@."
557
    	                  pp_machine_reset_name m.mname.node_id
558
    	                  (Utils.fprintf_list ~sep:" " pp_type)
559
    	                  (List.map (fun v -> v.var_type) (inout_vars machines m));
560

  
561
           Format.fprintf fmt "(declare-rel %a (%a))@."
562
    	                  pp_machine_step_name m.mname.node_id
563
    	                  (Utils.fprintf_list ~sep:" " pp_type)
564
    	                  (List.map (fun v -> v.var_type) (step_vars machines m));
565

  
566
           Format.pp_print_newline fmt ();
567
          (* Adding assertions *)
568
           match m.mstep.step_asserts with
569
	  | [] ->
570
	    begin
571

  
572
	      (* Rule for step*)
573
	      fprintf fmt "@[<v 2>(rule (=> @ ";
574
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
575
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
576
		pp_machine_step_name m.mname.node_id
577
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
578
	    end
579
	  | assertsl ->
580
	    begin
581
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
582
	      (* print_string pp_val; *)
583
	      fprintf fmt "; with Assertions @.";
584

  
585
	      (*Rule for step*)
586
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
587
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
588
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
589
		pp_machine_step_name m.mname.node_id
590
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
591
	    end
592

  
593
         end
594

  
595
        end
395 596
(* Local Variables: *)
396 597
(* compile-command:"make -C ../../.." *)
397 598
(* End: *)

Also available in: Unified diff