Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / horn_backend.ml @ f19eb2fd

History | View | Annotate | Download (12.5 KB)

1
open Format
2
open LustreSpec
3
open Corelang
4
open Machine_code
5

    
6

    
7
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
8
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
9

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

    
23
let pp_decl_var fmt id = 
24
  Format.fprintf fmt "(declare-var %s %a)"
25
    id.var_id
26
    pp_type id.var_type
27

    
28
let pp_var fmt id = Format.pp_print_string fmt id.var_id
29

    
30

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

    
39
let get_machine machines node_name = 
40
  List.find (fun m  -> m.mname.node_id = node_name) machines 
41

    
42
let full_memory_vars machines prefix machine =
43
  let rec aux prefix m =
44
    let pref x = if prefix = "" then x else prefix ^ "." ^ x in 
45
    (rename_machine_list (pref m.mname.node_id) m.mmemory) @
46
      List.fold_left (fun accu (id, (n, _)) -> 
47
	let name = node_name n in 
48
	if name = "_arrow" then accu else
49
	  let machine_n = get_machine machines name in
50
	( aux (pref id) machine_n ) @ accu
51
      ) [] (m.minstances) 
52
  in
53
  aux prefix machine
54

    
55
let machine_vars machines m = 
56
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
57
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
58
    (rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @ 
59
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
60

    
61
let step_vars machines m = 
62
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
63
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
64
    (rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @ 
65
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
66

    
67
let init_vars machines m = 
68
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
69
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
70
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
71

    
72
  
73
(********************************************************************************************)
74
(*                    Instruction Printing functions                                        *)
75
(********************************************************************************************)
76

    
77
let pp_horn_var m fmt id =
78
  if Types.is_array_type id.var_type
79
  then
80
    assert false (* no arrays in Horn output *)
81
  else
82
    Format.fprintf fmt "%s" id.var_id
83

    
84

    
85
(* Used to print boolean constants *)
86
let pp_horn_tag fmt t =
87
  pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
88

    
89
(* Prints a constant value *)
90
let rec pp_horn_const fmt c =
91
  match c with
92
    | Const_int i    -> pp_print_int fmt i
93
    | Const_real r   -> pp_print_string fmt r
94
    | Const_float r  -> pp_print_float fmt r
95
    | Const_tag t    -> pp_horn_tag fmt t
96
    | Const_array ca -> assert false
97

    
98
(* Prints a value expression [v], with internal function calls only.
99
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
100
   but an offset suffix may be added for array variables
101
*)
102
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
103
  match v with
104
    | Cst c         -> pp_horn_const fmt c
105
    | Array _      
106
    | Access _ -> assert false (* no arrays *)
107
    | Power (v, n)  -> assert false
108
    | LocalVar v    -> pp_var fmt (rename_machine self v)
109
    | StateVar v    ->
110
      if Types.is_array_type v.var_type
111
      then assert false 
112
      else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)
113
    | Fun (n, vl)   -> Format.fprintf fmt "(%a)" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
114

    
115
(* Prints a [value] indexed by the suffix list [loop_vars] *)
116
let rec pp_value_suffix self pp_value fmt value =
117
 match value with
118
 | Fun (n, vl)  ->
119
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
120
 |  _            ->
121
   pp_horn_val self pp_value fmt value
122

    
123
(* type_directed assignment: array vs. statically sized type
124
   - [var_type]: type of variable to be assigned
125
   - [var_name]: name of variable to be assigned
126
   - [value]: assigned value
127
   - [pp_var]: printer for variables
128
*)
129
let pp_assign m self pp_var fmt var_type var_name value =
130
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
131
  
132
let pp_instance_call 
133
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
134
  try (* stateful node instance *) 
135
    begin
136
      let (n,_) = List.assoc i m.minstances in
137
      match node_name n, inputs, outputs with
138
      | "_arrow", [i1; i2], [o] -> begin
139
         if init then
140
           pp_assign
141
   	     m
142
   	     self
143
   	     (pp_horn_var m)
144
	     (* (pp_horn_val self (pp_horn_var m) fmt o) *)  fmt
145
   	     o.var_type (LocalVar o) i1
146
         else
147
           pp_assign
148
   	     m self (pp_horn_var m) fmt
149
   	     o.var_type (LocalVar o) i2
150
	     
151
      end
152
      | name, _, _ ->  
153
	begin
154
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
155
	  if init then
156
	  Format.fprintf fmt "(%s_init %a%t%a%t%a)"
157
	    (node_name n) 
158
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
159
	    (Utils.pp_final_char_if_non_empty " " inputs) 
160
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
161
	    (Utils.pp_final_char_if_non_empty " " outputs)
162
	    (Utils.fprintf_list ~sep:" " pp_var) (
163
  	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
164
	     )
165
	  else
166
	    Format.fprintf fmt "(%s_step %a%t%a%t%a)"
167
	    (node_name n) 
168
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
169
	      (Utils.pp_final_char_if_non_empty " " inputs) 
170
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
171
	      (Utils.pp_final_char_if_non_empty " " outputs)
172
	      (Utils.fprintf_list ~sep:" " pp_var) (
173

    
174
	      (rename_current_list m.mname.node_id (full_memory_vars machines i target_machine)) @ 
175
	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
176
	       )
177
	    
178
	     end
179
    end
180
    with Not_found -> ( (* stateless node instance *)
181
      let (n,_) = List.assoc i m.mcalls in
182
   Format.fprintf fmt "(%s %a%t%a)"
183
     (node_name n)
184
     (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
185
     (Utils.pp_final_char_if_non_empty " " inputs) 
186
     (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs 
187
    )
188

    
189
let pp_machine_init (m: machine_t) self fmt inst =
190
  let (node, static) = List.assoc inst m.minstances in
191
  fprintf fmt "(%a %a%t%s->%s)"
192
    pp_machine_init_name (node_name node)
193
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
194
    (Utils.pp_final_char_if_non_empty " " static)
195
    self inst
196

    
197
(* TODO *)
198
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
199
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
200
    (pp_horn_val self (pp_horn_var m)) c
201
    (Utils.pp_newline_if_non_empty tl)
202
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
203
    (Utils.pp_newline_if_non_empty el)
204
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
205

    
206
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
207
  match instr with 
208
  | MReset i ->
209
    pp_machine_init m self fmt i
210
  | MLocalAssign (i,v) ->
211
    pp_assign
212
      m self (pp_horn_var m) fmt
213
      i.var_type (LocalVar i) v
214
  | MStateAssign (i,v) ->
215
    pp_assign
216
      m self (pp_horn_var m) fmt
217
      i.var_type (StateVar i) v
218
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
219
    pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl)))
220
  | MStep (il, i, vl) ->
221
    pp_instance_call machines ~init:init m self fmt i vl il
222
  | MBranch (g,hl) ->
223
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
224
    then (* boolean case, needs special treatment in C because truth value is not unique *)
225
	 (* may disappear if we optimize code by replacing last branch test with default *)
226
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
227
      let el = try List.assoc tag_false hl with Not_found -> [] in
228
      pp_conditional machines ~init:init m self fmt g tl el
229
    else assert false (* enum type case *)
230

    
231

    
232
(**************************************************************)
233
    
234
(* Print the machine m: 
235
   two functions: m_init and m_step
236
   - m_init is a predicate over m memories
237
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
238
   We first declare all variables then the two /rules/.
239
*)
240
let print_machine machines fmt m = 
241
  let pp_instr init = pp_machine_instr machines ~init:init m in
242
  if m.mname.node_id = arrow_id then () 
243
  else 
244
    ( (* We don't print arrow function *)
245
   Format.fprintf fmt "; %s@." m.mname.node_id;
246
   (* Printing variables *)
247
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
248
     ((machine_vars machines m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
249
   Format.pp_print_newline fmt ();
250
   (* Declaring predicate *)
251
   Format.fprintf fmt "(declare-rel %a (%a))@."
252
     pp_machine_init_name m.mname.node_id
253
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
254
   
255
   Format.fprintf fmt "(declare-rel %a (%a))@."
256
     pp_machine_step_name m.mname.node_id
257
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m));
258
   Format.pp_print_newline fmt ();
259

    
260
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@."
261
     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
262
     m.mname.node_id
263
     (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
264

    
265

    
266
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@."
267
     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
268
     m.mname.node_id
269
     (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
270
   
271
()
272
  )
273

    
274
let main_print machines fmt = 
275
if !Options.main_node <> "" then 
276
  begin
277
    let node = !Options.main_node in
278
    let machine = get_machine machines node in
279
    Format.fprintf fmt "; Collecting semantics with main node %s@.@." node;
280
    (* We print the types of the main node "memory tree" TODO: add the output *)
281
    let main_memory_next = 
282
      (rename_next_list machine.mname.node_id (full_memory_vars machines "" machine)) 
283
    in
284
    let main_memory_current = 
285
      (rename_current_list machine.mname.node_id (full_memory_vars machines "" machine)) 
286
    in
287
    Format.fprintf fmt "(declare-rel MAIN (%a Bool))@."
288
      (Utils.fprintf_list ~sep:" " pp_type) 
289
      (List.map (fun v -> v.var_type) main_memory_next);
290
    
291
    Format.fprintf fmt "; Initial set@.";
292
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
293
    Format.fprintf fmt "(rule INIT_STATE)@.";
294
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%s_init %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
295
      node
296
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
297
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next;
298

    
299
    Format.fprintf fmt "; Inductive def@.";
300
    Format.fprintf fmt "(declare-var dummy Bool)@.";
301
    Format.fprintf fmt 
302
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
303
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
304
      node
305
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
306
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next;
307

    
308
    Format.fprintf fmt "; Property def@.";
309
    Format.fprintf fmt "(declare-rel ERR ())@.";
310
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (= top.OK true))@ (MAIN %a)@])@ ERR))@."
311
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current;
312
    Format.fprintf fmt "(query ERR)@.";
313

    
314
    ()
315
end
316

    
317

    
318
let translate fmt basename prog machines =
319
  List.iter (print_machine machines fmt) (List.rev machines);
320
  main_print machines fmt 
321

    
322

    
323
(* Local Variables: *)
324
(* compile-command:"make -C .." *)
325
(* End: *)