Project

General

Profile

Revision 7a19992d

View differences:

src/basic_library.ml
169 169
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
170 170
    | _ -> assert false
171 171

  
172
let pp_horn i pp_val fmt vl = 
173
  match i, vl with
174
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 
175
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
176
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v 
177
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 
178
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 
179
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 
180
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 
181
  | _ -> assert false
182
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
183
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
184
  | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
185
*)
172 186

  
173 187
(* Local Variables: *)
174 188
(* compile-command:"make -C .." *)
src/horn_backend.ml
4 4
open Machine_code
5 5

  
6 6

  
7
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
8
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
9

  
7 10
let pp_type fmt t =
8 11
  match (Types.repr t).Types.tdesc with
9 12
  | Types.Tbool           -> Format.fprintf fmt "Bool"
......
13 16
  | Types.Tstatic _
14 17
  | Types.Tconst _
15 18
  | Types.Tarrow _
16
  | _                     -> Format.eprintf "internal error: pp_type %a@." Types.print_ty t; assert false
19
  | _                     -> Format.eprintf "internal error: pp_type %a@." 
20
                             Types.print_ty t; assert false
17 21
    
18 22

  
19 23
let pp_decl_var fmt id = 
......
26 30
let pp_instr machine_name fmt i =
27 31
  Format.fprintf fmt "(xxx)"
28 32

  
29
let rename f = List.map (fun v -> {v with var_id = f v.var_id } )
30
let rename_current machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_c")
33
let rename f = (fun v -> {v with var_id = f v.var_id } )
34
let rename_current machine_name =  rename (fun n -> machine_name ^ "." ^ n ^ "_c")
35
let rename_current_list machine_name = List.map (rename_current machine_name)
31 36
let rename_next machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_x")
37
let rename_next_list machine_name = List.map (rename_next machine_name)
32 38
let rename_machine machine_name = rename (fun n -> machine_name ^ "." ^ n)
39
let rename_machine_list machine_name = List.map (rename_machine machine_name)
33 40

  
34 41
let machine_vars m = 
35
  (rename_current m.mname.node_id m.mstatic)@
36
    (rename_next m.mname.node_id m.mstatic)@
37
    (rename_machine m.mname.node_id m.mstep.step_inputs)@
38
    (rename_machine m.mname.node_id m.mstep.step_outputs)
42
  (rename_current_list m.mname.node_id m.mmemory)@
43
    (rename_next_list m.mname.node_id m.mmemory)@
44
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
45
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
46

  
47

  
48
(********************************************************************************************)
49
(*                    Instruction Printing functions                                        *)
50
(********************************************************************************************)
51

  
52
let pp_horn_var m fmt id =
53
  if Types.is_array_type id.var_type
54
  then
55
    assert false (* no arrays in Horn output *)
56
  else
57
    Format.fprintf fmt "%s" id.var_id
58

  
59

  
60
(* Used to print boolean constants *)
61
let pp_horn_tag fmt t =
62
  pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
63

  
64
(* Prints a constant value *)
65
let rec pp_horn_const fmt c =
66
  match c with
67
    | Const_int i    -> pp_print_int fmt i
68
    | Const_real r   -> pp_print_string fmt r
69
    | Const_float r  -> pp_print_float fmt r
70
    | Const_tag t    -> pp_horn_tag fmt t
71
    | Const_array ca -> assert false
72

  
73
(* Prints a value expression [v], with internal function calls only.
74
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
75
   but an offset suffix may be added for array variables
76
*)
77
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
78
  match v with
79
    | Cst c         -> pp_horn_const fmt c
80
    | Array _      
81
    | Access _ -> assert false (* no arrays *)
82
    | Power (v, n)  -> assert false
83
    | LocalVar v    -> pp_var fmt (rename_machine self v)
84
    | StateVar v    ->
85
      if Types.is_array_type v.var_type
86
      then assert false 
87
      else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)
88
    | Fun (n, vl)   -> Format.fprintf fmt "(%a)" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
89

  
90
(* Prints a [value] indexed by the suffix list [loop_vars] *)
91
let rec pp_value_suffix self pp_value fmt value =
92
 match value with
93
 | Fun (n, vl)  ->
94
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
95
 |  _            ->
96
   pp_horn_val self pp_value fmt value
97

  
98
(* type_directed assignment: array vs. statically sized type
99
   - [var_type]: type of variable to be assigned
100
   - [var_name]: name of variable to be assigned
101
   - [value]: assigned value
102
   - [pp_var]: printer for variables
103
*)
104
let pp_assign m self pp_var fmt var_type var_name value =
105
  fprintf fmt "(%a = %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
106
  
107
let pp_instance_call machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
108
 try (* stateful node instance *) (
109
   let (n,_) = List.assoc i m.minstances in
110
   match node_name n, inputs, outputs with
111
   | "_arrow", [i1; i2], [o] -> (
112
     if init then
113
       pp_assign
114
	 m self (pp_horn_val self (pp_horn_var m) fmt o) fmt
115
	 o.var_type (LocalVar o) i1
116
     else
117
       pp_assign
118
	 m self (pp_horn_val self (pp_horn_var m) fmt o) fmt
119
	 o.var_type (LocalVar o) i2
120
       
121
   )
122
   | name, _, _ ->  (
123
     let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
124
     Format.fprintf fmt "(%s_%s %a%txxx%axxx%t%a)"
125
       (node_name n) (if init then "init" else "step")
126
       (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
127
       (Utils.pp_final_char_if_non_empty " " inputs) 
128
       (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) outputs
129
       (Utils.pp_final_char_if_non_empty " " outputs)
130
       
131
       (Utils.fprintf_list ~sep:" " pp_var) (machine_vars target_machine)
132
       
133
   )
134
 )
135
 with Not_found -> (* stateless node instance *)
136
   let (n,_) = List.assoc i m.mcalls in
137
   Format.fprintf fmt "(%s %a%t%a)"
138
     (node_name n)
139
     (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
140
     (Utils.pp_final_char_if_non_empty " " inputs) 
141
     (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs 
142

  
143
let pp_machine_reset (m: machine_t) self fmt inst =
144
  let (node, static) = List.assoc inst m.minstances in
145
  fprintf fmt "(%a %a%t%s->%s)"
146
    pp_machine_reset_name (node_name node)
147
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
148
    (Utils.pp_final_char_if_non_empty " " static)
149
    self inst
150

  
151
(* TODO *)
152
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
153
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
154
    (pp_horn_val self (pp_horn_var m)) c
155
    (Utils.pp_newline_if_non_empty tl)
156
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
157
    (Utils.pp_newline_if_non_empty el)
158
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
159

  
160
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
161
  match instr with 
162
  | MReset i ->
163
    pp_machine_reset m self fmt i
164
  | MLocalAssign (i,v) ->
165
    pp_assign
166
      m self (pp_horn_var m) fmt
167
      i.var_type (LocalVar i) v
168
  | MStateAssign (i,v) ->
169
    pp_assign
170
      m self (pp_horn_var m) fmt
171
      i.var_type (StateVar i) v
172
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
173
    pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl)))
174
  | MStep (il, i, vl) ->
175
    pp_instance_call machines ~init:init m self fmt i vl il
176
  | MBranch (g,hl) ->
177
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
178
    then (* boolean case, needs special treatment in C because truth value is not unique *)
179
	 (* may disappear if we optimize code by replacing last branch test with default *)
180
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
181
      let el = try List.assoc tag_false hl with Not_found -> [] in
182
      pp_conditional machines ~init:init m self fmt g tl el
183
    else assert false (* enum type case *)
184

  
185

  
186
(**************************************************************)
39 187
    
40 188
(* Print the machine m: 
41 189
   two functions: m_init and m_step
......
43 191
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
44 192
   We first declare all variables then the two /rules/.
45 193
*)
46
let print_machine fmt m = 
47
 if m.mname.node_id = arrow_id then () else ( (* We don't print arrow function *)
194
let print_machine machines fmt m = 
195
  let pp_instr init = pp_machine_instr machines ~init:init m in
196
  if m.mname.node_id = arrow_id then () 
197
  else 
198
    ( (* We don't print arrow function *)
48 199
   Format.fprintf fmt "; %s@." m.mname.node_id;
49 200
   (* Printing variables *)
50 201
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
51
     ((machine_vars m)@(rename_machine m.mname.node_id m.mstep.step_locals));
52

  
202
     ((machine_vars m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
203
   Format.pp_print_newline fmt ();
53 204
   (* Declaring predicate *)
54
   Format.fprintf fmt "(declare-rel %s_init (%a))@."
55
     m.mname.node_id
56
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mstatic);
205
   Format.fprintf fmt "(declare-rel %a (%a))@."
206
     pp_machine_reset_name m.mname.node_id
207
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mmemory);
57 208
   
58
   Format.fprintf fmt "(declare-rel %s_step (%a))@."
59
     m.mname.node_id
209
   Format.fprintf fmt "(declare-rel %a (%a))@."
210
     pp_machine_step_name m.mname.node_id
60 211
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (machine_vars m));
212
   Format.pp_print_newline fmt ();
61 213

  
62
   Format.fprintf fmt "(rule (=> (and %a) (%s_init %a)))"
63
     (Utils.fprintf_list ~sep:"@." (pp_instr m.mname.node_id)) m.minit
214
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@."
215
     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
64 216
     m.mname.node_id
65
     (Utils.fprintf_list ~sep:" " pp_var) (rename_machine m.mname.node_id m.mstatic);
217
     (Utils.fprintf_list ~sep:" " pp_var) (rename_next_list m.mname.node_id m.mmemory);
66 218

  
67
   Format.fprintf fmt "(rule (=> (and %a) (%s_step %a)))"
68
     (Utils.fprintf_list ~sep:"@." (pp_instr m.mname.node_id)) m.mstep.step_instrs
219
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@."
220
     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
69 221
     m.mname.node_id
70 222
     (Utils.fprintf_list ~sep:" " pp_var) (machine_vars m);
71 223
   
......
75 227
let main_print fmt = ()
76 228

  
77 229
let translate fmt basename prog machines =
78
  List.iter (print_machine fmt) machines;
230
  List.iter (print_machine machines fmt) (List.rev machines);
79 231
  main_print fmt 
80 232

  
81 233

  
src/machine_code.ml
291 291
 | Expr_access (t, i)               -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
292 292
 | Expr_power  (e, n)               -> Power  (translate_expr node args e, translate_expr node args (expr_of_dimension n))
293 293
 | Expr_tuple _
294
 | Expr_ite _
295 294
 | Expr_arrow _ 
296 295
 | Expr_fby _
297 296
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
......
302 301
   (match e.expr_desc with
303 302
   | Expr_tuple el -> Fun (node_name nd, List.map (translate_expr node args) el)
304 303
   | _             -> Fun (node_name nd, [translate_expr node args e]))
304
 | Expr_ite (g,t,e) -> Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
305

  
305 306
 | _                   -> raise NormalizationError
306 307

  
307 308
let translate_guard node args expr =
......
367 368
     d,
368 369
     reset_instance node args o r eq.eq_rhs.expr_clock @
369 370
       (control_on_clock node args eq.eq_rhs.expr_clock (MStep (var_p, o, vl))) :: s)
371
  | [x], Expr_ite   (c, t, e) -> 
372
    let var_x = node_var x node in
373
    (m, 
374
     si, 
375
     j, 
376
     d, 
377
     (control_on_clock node args eq.eq_rhs.expr_clock 
378
       (MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
379
    )
370 380
  | [x], _                                       ->
371 381
    let var_x = node_var x node in
372 382
    (m, si, j, d, 
......
425 435
      step_outputs = nd.node_outputs;
426 436
      step_locals = ISet.elements (ISet.diff locals m);
427 437
      step_checks = List.map (fun d -> d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks;
428
      step_instrs = join_guards_list s;
438
      step_instrs = (* join_guards_list *) s;
429 439
    };
430 440
    mspec = nd.node_spec;
431 441
    mannot = nd.node_annot;

Also available in: Unified diff