Project

General

Profile

Revision 5500edb8 src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
22 22
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
23 23
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
24 24

  
25
let pp_type fmt t =
25
let empty_array_var m dim = m.mname.node_id  ^ "_empty_array_" ^ string_of_int dim
26

  
27
(* Common function to build array both for expressions and constants *)
28
let build_array_string element_builder empty_array_var_name vl =
29
  match vl with 
30
  | [] -> assert false 
31
  | vl_hd::vl_tl ->
32
    begin
33
      (* Array assigned. We declare it as var = (store  (store var 1 e1) 2 e2) *)
34
      let rec build_array element_builder list idx accu = 
35
	match list with
36
	| [] -> accu
37
	| hd::tl -> (
38
	  fprintf str_formatter "(store %s %i %a)"
39
	    accu
40
	    idx
41
	    element_builder hd;
42
	  build_array element_builder tl (idx+1) (flush_str_formatter ())
43
	)
44
      in
45
      build_array element_builder
46
	vl_tl 
47
	2 
48
	( (* store 1 vl_hd var_name *)
49
	  fprintf str_formatter "(store %s 1 %a)"
50
	    empty_array_var_name
51
	    element_builder vl_hd;
52
	  flush_str_formatter ()
53
	)
54
    end
55

  
56

  
57
let pp_horn_basic_type fmt t =
26 58
  match (Types.repr t).Types.tdesc with
27
  | Types.Tbool           -> Format.fprintf fmt "Bool"
28
  | Types.Tint            -> Format.fprintf fmt "Int"
29
  | Types.Treal           -> Format.fprintf fmt "Real"
30
  | Types.Tclock _
31
  | Types.Tarray _
32
  | Types.Tstatic _
33
  | Types.Tconst _
34
  | Types.Tarrow _
35
  | _                     -> Format.eprintf "internal error: pp_type %a@."
36
    Types.print_ty t; assert false
59
  | Types.Tbool           -> fprintf fmt "Bool"
60
  | Types.Tint            -> fprintf fmt "Int"
61
  | Types.Treal           -> fprintf fmt "Real"
62
  | _ -> assert false (* Not a basic type *)
37 63

  
64
let rec pp_horn_type fmt t =
65
  match (Types.repr t).Types.tdesc with
66
  | Types.Tclock t' -> pp_horn_type fmt t' 
67
  | Types.Tbool  | Types.Tint | Types.Treal -> pp_horn_basic_type fmt t
68
  | Types.Tarray (_, t') ->     (* Arrays should be indexed by int *)
69
    fprintf fmt "(Array Int %a)" pp_horn_type t'
70
  | Types.Tstatic (_, t') -> (* Static types are declared as regular types *)
71
    pp_horn_type fmt t'
72
  | Types.Tconst _ (* ty -> fprintf fmt "%s %s" ty var -- from C backend *)
73
  | _ (* (Trat|Tarrow (_, _)|Ttuple _|Tenum _|Tstruct _|Tlink _|Tvar|Tunivar) *)
74
    -> Format.eprintf "internal error: pp_type const %a@." Types.print_ty t; assert false
75
      
38 76
let pp_decl_var fmt id =
39 77
  Format.fprintf fmt "(declare-var %s %a)"
40 78
    id.var_id
41
    pp_type id.var_type
79
    pp_horn_type id.var_type
42 80

  
43 81
let pp_var fmt id = Format.pp_print_string fmt id.var_id
44 82

  
......
96 134
(********************************************************************************************)
97 135

  
98 136
let pp_horn_var m fmt id =
99
  if Types.is_array_type id.var_type
137
(* PLOC TODO: array are printed as other variable 
138
   if Types.is_array_type id.var_type
100 139
  then
101 140
    assert false (* no arrays in Horn output *)
102 141
  else
103
    Format.fprintf fmt "%s" id.var_id
142
*)   Format.fprintf fmt "%s" id.var_id
104 143

  
105 144

  
106 145
(* Used to print boolean constants *)
......
110 149
(* Prints a constant value *)
111 150
let rec pp_horn_const fmt c =
112 151
  match c with
113
    | Const_int i    -> pp_print_int fmt i
114
    | Const_real r   -> pp_print_string fmt r
115
    | Const_float r  -> pp_print_float fmt r
116
    | Const_tag t    -> pp_horn_tag fmt t
117
    | _              -> assert false
152
  | Const_int i    -> pp_print_int fmt i
153
  | Const_real r   -> pp_print_string fmt r
154
  | Const_float r  -> pp_print_float fmt r
155
  | Const_tag t    -> pp_horn_tag fmt t
156
  | Const_array ca -> assert false (* No constant arrays yet. We have to
157
				      introduce a dedicated constant array
158
				      builder *)
159
  | Const_string _ -> assert false (* String occurs in annotations *)
160
  | Const_struct _ ->assert false (* No struct yet in Horn *)
118 161

  
119 162
(* Prints a value expression [v], with internal function calls only.
120 163
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
121 164
   but an offset suffix may be added for array variables
122 165
*)
123
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
166
let rec pp_horn_val ?(is_lhs=false) m self pp_var fmt v =
124 167
  match v with
125 168
    | Cst c         -> pp_horn_const fmt c
126
    | Array _
127
    | Access _ -> assert false (* no arrays *)
169
    | Array vl      -> 
170
      begin
171
	let array_multidim = get_array_instr_multidim v in
172
	fprintf fmt "%s" 
173
	  (build_array_string (pp_horn_val m self pp_var) (empty_array_var m array_multidim) vl)
174
      end
175
    | Access (t, i) -> 
176
      let pp = pp_horn_val ~is_lhs:is_lhs m self pp_var in
177
      fprintf fmt "(select %a %a)" pp t pp i 
128 178
    | Power (v, n)  -> assert false
129 179
    | LocalVar v    -> pp_var fmt (rename_machine self v)
130 180
    | StateVar v    ->
131 181
      if Types.is_array_type v.var_type
132 182
      then assert false
133 183
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
134
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
184
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val m self pp_var)) vl
135 185

  
136 186
(* Prints a [value] indexed by the suffix list [loop_vars] *)
137
let rec pp_value_suffix self pp_value fmt value =
187
let rec pp_value_suffix m self pp_value fmt value =
138 188
 match value with
139 189
 | Fun (n, vl)  ->
140
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
190
   Basic_library.pp_horn n (pp_value_suffix m self pp_value) fmt vl
141 191
 |  _            ->
142
   pp_horn_val self pp_value fmt value
192
   pp_horn_val m self pp_value fmt value
193

  
143 194

  
195
      
144 196
(* type_directed assignment: array vs. statically sized type
145 197
   - [var_type]: type of variable to be assigned
146 198
   - [var_name]: name of variable to be assigned
......
148 200
   - [pp_var]: printer for variables
149 201
*)
150 202
let pp_assign m self pp_var fmt var_type var_name value =
151
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
203
    fprintf fmt "(= %a %a)" 
204
      (pp_horn_val ~is_lhs:true m self pp_var) var_name 
205
      (pp_value_suffix m self pp_var) value
152 206

  
153 207
let pp_instance_call
154 208
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
......
177 231
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
178 232
	      pp_machine_init_name (node_name n)
179 233
	      (* inputs *)
180
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
234
	      (Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
181 235
	      inputs
182 236
	      (Utils.pp_final_char_if_non_empty " " inputs)
183 237
	      (* outputs *)
184
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
238
	      (Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
185 239
	      (List.map (fun v -> LocalVar v) outputs)
186 240
	      (Utils.pp_final_char_if_non_empty " " outputs)
187 241
	      (* memories (next) *)
......
194 248
	  else
195 249
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
196 250
	      pp_machine_step_name (node_name n)
197
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
251
	      (Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m))) inputs
198 252
	      (Utils.pp_final_char_if_non_empty " " inputs)
199
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
253
	      (Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
200 254
	      (List.map (fun v -> LocalVar v) outputs)
201 255
	      (Utils.pp_final_char_if_non_empty " " outputs)
202 256
	      (Utils.fprintf_list ~sep:" " pp_var) (
......
216 270
      let (n,_) = List.assoc i m.mcalls in
217 271
      Format.fprintf fmt "(%s %a%t%a)"
218 272
	(node_name n)
219
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
273
	(Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
220 274
	inputs
221 275
	(Utils.pp_final_char_if_non_empty " " inputs)
222
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
276
	(Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
223 277
	(List.map (fun v -> LocalVar v) outputs)
224 278
    )
225 279

  
......
234 288
(* TODO *)
235 289
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
236 290
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
237
    (pp_horn_val self (pp_horn_var m)) c
291
    (pp_horn_val m self (pp_horn_var m)) c
238 292
    (Utils.pp_newline_if_non_empty tl)
239 293
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
240 294
    (Utils.pp_newline_if_non_empty el)
......
275 329
   - m_init is a predicate over m memories
276 330
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
277 331
   We first declare all variables then the two /rules/.
332

  
333
   For all arrays type, either inputs, outputs, state vars or local ones, we
334
   introduce an empty array variable: {machine_name}_array_x with x the dimension.
278 335
*)
279 336
let print_machine machines fmt m =
280 337
  let pp_instr init = pp_machine_instr machines ~init:init m in
......
291 348
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
292 349
   Format.pp_print_newline fmt ();
293 350

  
294

  
295

  
351
   (* Printing array empty val *)
352
   (* We gather required dimension and print the empty vars *)
353
   let required_empty_vars, _ = 
354
     List.fold_left (
355
       fun ((accu_var, accu_dim) as accu) vd ->
356
      (* If vd is an array, we may have to add an element to accu *)
357
	 if Types.is_array_type vd.var_type then
358
	   (* We compute the dimension width (???) of the array, ie. array is 1 vs
359
	      matrix is 2 vs 3D matrix is 3 , etc *)
360
	   let dim_size = Types.multidim vd.var_type in
361
	   if List.mem dim_size accu_dim then
362
	     (* this dimension was already computed. Do nothing *)
363
	     accu
364
	   else (* We create a new empty var, copying vd and changing its
365
		   name. We do not care for actual dimension, ie. size of
366
		   arrays *)
367
	     let new_var = {vd with var_id = empty_array_var m dim_size } in
368
	     new_var::accu_var, dim_size::accu_dim
369
	 else (* other wise do nothing *)
370
	   accu
371
     ) ([], []) (m.mstep.step_locals@m.mstep.step_inputs@m.mstep.step_outputs)
372
   in
373
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
374
     required_empty_vars;
375
   Format.pp_print_newline fmt ();
376
 
296 377
   if is_stateless m then
297 378
     begin
298 379
       (* Declaring single predicate *)
299 380
       Format.fprintf fmt "(declare-rel %a (%a))@."
300 381
	 pp_machine_stateless_name m.mname.node_id
301
	 (Utils.fprintf_list ~sep:" " pp_type)
382
	 (Utils.fprintf_list ~sep:" " pp_horn_type)
302 383
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
303 384

  
304 385
       (* Rule for single predicate *)
......
317 398
       (* Declaring predicate *)
318 399
       Format.fprintf fmt "(declare-rel %a (%a))@."
319 400
	 pp_machine_init_name m.mname.node_id
320
	 (Utils.fprintf_list ~sep:" " pp_type)
401
	 (Utils.fprintf_list ~sep:" " pp_horn_type)
321 402
	 (List.map (fun v -> v.var_type) (init_vars machines m));
322 403

  
323 404
       Format.fprintf fmt "(declare-rel %a (%a))@."
324 405
	 pp_machine_step_name m.mname.node_id
325
	 (Utils.fprintf_list ~sep:" " pp_type)
406
	 (Utils.fprintf_list ~sep:" " pp_horn_type)
326 407
	 (List.map (fun v -> v.var_type) (step_vars machines m));
327 408

  
328 409
       Format.pp_print_newline fmt ();
......
350 431
          end
351 432
       | assertsl ->
352 433
          begin
353
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
434
	    let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id pp_var in
354 435
            (* print_string pp_val; *)
355 436
            let instrs_concat = m.mstep.step_instrs in
356 437
            Format.fprintf fmt "; with Assertions @.";
......
400 481
    in
401 482

  
402 483
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
403
      (Utils.fprintf_list ~sep:" " pp_type)
484
      (Utils.fprintf_list ~sep:" " pp_horn_type)
404 485
      (List.map (fun v -> v.var_type) main_memory_next);
405 486

  
406 487
    Format.fprintf fmt "; Initial set@.";
......
467 548
    in
468 549

  
469 550
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
470
      (Utils.fprintf_list ~sep:" " pp_type)
551
      (Utils.fprintf_list ~sep:" " pp_horn_type)
471 552
      (List.map (fun v -> v.var_type) cex_memory_next);
472 553

  
473 554
    Format.fprintf fmt "; Initial set@.";
......
520 601
      get_cex machines fmt node machine)
521 602
end
522 603

  
604
let print_const_def fmt cdecl =
605
  (* Declare var with appropriate type *)
606
  fprintf fmt "(declare-const %s %a);@."
607
    cdecl.const_id 
608
    pp_horn_type cdecl.const_type;
609
  (* Assert its value. Special treatment for array constants *)
610
  match cdecl.const_value, (Types.repr cdecl.const_type).Types.tdesc with
611
  | Const_array cl, Types.Tstatic _  -> 
612
    fprintf fmt "(assert (= %s %s));@."
613
      cdecl.const_id
614
      (build_array_string pp_horn_const cdecl.const_id cl)
615

  
616
  | _ -> 
617
    fprintf fmt "(assert (= %s %a));@." 
618
      cdecl.const_id
619
      pp_horn_const cdecl.const_value 
620
      
523 621

  
524 622
let translate fmt basename prog machines =
623
  (* Print consts *)
624
  fprintf fmt "; Global constants (definitions) @.";
625
  fprintf fmt "@[<v>";
626
  List.iter (fun c -> print_const_def fmt (const_of_top c)) (get_consts prog);
627
  fprintf fmt "@]@.";
628

  
629
  (* Print machines *)
525 630
  List.iter (print_machine machines fmt) (List.rev machines);
631

  
632
  (* Print main *)
526 633
  main_print machines fmt
527 634

  
528 635

  
......
618 725
    let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
619 726
     Format.fprintf fmt "     <input name=\"%a\" type=\"%a\">%a</input> @."
620 727
                   (Utils.fprintf_list ~sep:" | " pp_var) input_vars
621
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) input_vars
728
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_horn_type fmt id.var_type)) input_vars
622 729
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs);
623 730

  
624 731
    Format.fprintf fmt "      <output name=\"%a\" type=\"%a\">%a</output> @."
625 732
                   (Utils.fprintf_list ~sep:" | " pp_var)  output_vars
626
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
733
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_horn_type fmt id.var_type)) output_vars
627 734
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
628 735

  
629 736
    let init_local_vars = (rename_next_list (full_memory_vars machines m)) in
......
631 738

  
632 739
    Format.fprintf fmt "      <localInit name=\"%a\" type=\"%a\">%t%a</localInit> @."
633 740
                   (Utils.fprintf_list ~sep:" | " pp_var) init_local_vars
634
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
741
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_horn_type fmt id.var_type)) init_local_vars
635 742
                   (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "")
636 743
                   (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next;
637 744

  
638 745
    Format.fprintf fmt "      <localStep name=\"%a\" type=\"%a\">%t%a</localStep> @."
639 746
                   (Utils.fprintf_list ~sep:" | " pp_var) step_local_vars
640
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
747
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_horn_type fmt id.var_type)) step_local_vars
641 748
                   (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
642 749
                     (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)"
643 750
                                    Printers.pp_expr ee)) (memories_old);

Also available in: Unified diff