Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / horn_backend.ml @ 4f3cc9f3

History | View | Annotate | Download (12.7 KB)

1 aa6b7d46 ploc
open Format
2
open LustreSpec
3
open Corelang
4
open Machine_code
5
6
7 40f8d0f9 ploc
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
8 04a7df69 ploc
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
9
10 aa6b7d46 ploc
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 04a7df69 ploc
  | _                     -> Format.eprintf "internal error: pp_type %a@." 
20
                             Types.print_ty t; assert false
21 aa6b7d46 ploc
    
22
23
let pp_decl_var fmt id = 
24 40f8d0f9 ploc
  Format.fprintf fmt "(declare-var %s %a)"
25 aa6b7d46 ploc
    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 4f3cc9f3 ploc
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x 
32
let rename f = (fun v -> {v with var_id = f v.var_id } )
33
let rename_machine p = rename (fun n -> concat p n)
34 c0003810 ploc
let rename_machine_list p = List.map (rename_machine p)
35
    
36
let rename_current =  rename (fun n -> n ^ "_c")
37
let rename_current_list = List.map rename_current
38
let rename_next = rename (fun n -> n ^ "_x")
39
let rename_next_list = List.map rename_next
40
41 faa5e5c5 ploc
42
let get_machine machines node_name = 
43
  List.find (fun m  -> m.mname.node_id = node_name) machines 
44
45 c0003810 ploc
let full_memory_vars machines machine =
46 4f3cc9f3 ploc
  let rec aux fst prefix m =
47
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
48 faa5e5c5 ploc
      List.fold_left (fun accu (id, (n, _)) -> 
49
	let name = node_name n in 
50
	if name = "_arrow" then accu else
51
	  let machine_n = get_machine machines name in
52 4f3cc9f3 ploc
	( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
53 faa5e5c5 ploc
      ) [] (m.minstances) 
54
  in
55 c0003810 ploc
  aux true machine.mname.node_id machine
56 faa5e5c5 ploc
57
let machine_vars machines m = 
58
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
59
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
60 c0003810 ploc
    (rename_current_list (full_memory_vars machines m)) @ 
61
    (rename_next_list (full_memory_vars machines m)) 
62 faa5e5c5 ploc
63
let step_vars machines m = 
64
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
65
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
66 c0003810 ploc
    (rename_current_list (full_memory_vars machines m)) @ 
67
    (rename_next_list (full_memory_vars machines m)) 
68 faa5e5c5 ploc
69
let init_vars machines m = 
70 04a7df69 ploc
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
71 23bdf881 ploc
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
72 c0003810 ploc
    (rename_next_list (full_memory_vars machines m)) 
73 23bdf881 ploc
  
74 04a7df69 ploc
(********************************************************************************************)
75
(*                    Instruction Printing functions                                        *)
76
(********************************************************************************************)
77
78
let pp_horn_var m fmt id =
79
  if Types.is_array_type id.var_type
80
  then
81
    assert false (* no arrays in Horn output *)
82
  else
83
    Format.fprintf fmt "%s" id.var_id
84
85
86
(* Used to print boolean constants *)
87
let pp_horn_tag fmt t =
88 4f3cc9f3 ploc
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
89 04a7df69 ploc
90
(* Prints a constant value *)
91
let rec pp_horn_const fmt c =
92
  match c with
93
    | Const_int i    -> pp_print_int fmt i
94
    | Const_real r   -> pp_print_string fmt r
95
    | Const_float r  -> pp_print_float fmt r
96
    | Const_tag t    -> pp_horn_tag fmt t
97
    | Const_array ca -> assert false
98
99
(* Prints a value expression [v], with internal function calls only.
100
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
101
   but an offset suffix may be added for array variables
102
*)
103
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
104
  match v with
105
    | Cst c         -> pp_horn_const fmt c
106
    | Array _      
107
    | Access _ -> assert false (* no arrays *)
108
    | Power (v, n)  -> assert false
109
    | LocalVar v    -> pp_var fmt (rename_machine self v)
110
    | StateVar v    ->
111
      if Types.is_array_type v.var_type
112
      then assert false 
113 4f3cc9f3 ploc
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
114 c0003810 ploc
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
115 04a7df69 ploc
116
(* Prints a [value] indexed by the suffix list [loop_vars] *)
117
let rec pp_value_suffix self pp_value fmt value =
118
 match value with
119
 | Fun (n, vl)  ->
120
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
121
 |  _            ->
122
   pp_horn_val self pp_value fmt value
123
124
(* type_directed assignment: array vs. statically sized type
125
   - [var_type]: type of variable to be assigned
126
   - [var_name]: name of variable to be assigned
127
   - [value]: assigned value
128
   - [pp_var]: printer for variables
129
*)
130
let pp_assign m self pp_var fmt var_type var_name value =
131 fc7a01ce ploc
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
132 04a7df69 ploc
  
133 23bdf881 ploc
let pp_instance_call 
134
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
135
  try (* stateful node instance *) 
136
    begin
137
      let (n,_) = List.assoc i m.minstances in
138
      match node_name n, inputs, outputs with
139
      | "_arrow", [i1; i2], [o] -> begin
140
         if init then
141
           pp_assign
142
   	     m
143
   	     self
144
   	     (pp_horn_var m)
145
	     (* (pp_horn_val self (pp_horn_var m) fmt o) *)  fmt
146
   	     o.var_type (LocalVar o) i1
147
         else
148
           pp_assign
149
   	     m self (pp_horn_var m) fmt
150
   	     o.var_type (LocalVar o) i2
151
	     
152
      end
153
      | name, _, _ ->  
154
	begin
155
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
156 faa5e5c5 ploc
	  if init then
157
	  Format.fprintf fmt "(%s_init %a%t%a%t%a)"
158 23bdf881 ploc
	    (node_name n) 
159
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
160
	    (Utils.pp_final_char_if_non_empty " " inputs) 
161
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
162 faa5e5c5 ploc
	    (Utils.pp_final_char_if_non_empty " " outputs)
163
	    (Utils.fprintf_list ~sep:" " pp_var) (
164 4f3cc9f3 ploc
  	      rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine)) 
165 faa5e5c5 ploc
	     )
166
	  else
167
	    Format.fprintf fmt "(%s_step %a%t%a%t%a)"
168
	    (node_name n) 
169
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
170
	      (Utils.pp_final_char_if_non_empty " " inputs) 
171
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
172
	      (Utils.pp_final_char_if_non_empty " " outputs)
173
	      (Utils.fprintf_list ~sep:" " pp_var) (
174
175 4f3cc9f3 ploc
	      (rename_machine_list (concat m.mname.node_id i) (rename_current_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) @ 
176
		(rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) 
177 faa5e5c5 ploc
	       )
178 23bdf881 ploc
	    
179
	     end
180
    end
181
    with Not_found -> ( (* stateless node instance *)
182
      let (n,_) = List.assoc i m.mcalls in
183 04a7df69 ploc
   Format.fprintf fmt "(%s %a%t%a)"
184
     (node_name n)
185
     (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
186
     (Utils.pp_final_char_if_non_empty " " inputs) 
187
     (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs 
188 23bdf881 ploc
    )
189 04a7df69 ploc
190 40f8d0f9 ploc
let pp_machine_init (m: machine_t) self fmt inst =
191 04a7df69 ploc
  let (node, static) = List.assoc inst m.minstances in
192
  fprintf fmt "(%a %a%t%s->%s)"
193 40f8d0f9 ploc
    pp_machine_init_name (node_name node)
194 04a7df69 ploc
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
195
    (Utils.pp_final_char_if_non_empty " " static)
196
    self inst
197
198
(* TODO *)
199
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
200
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
201
    (pp_horn_val self (pp_horn_var m)) c
202
    (Utils.pp_newline_if_non_empty tl)
203
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
204
    (Utils.pp_newline_if_non_empty el)
205
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
206
207
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
208
  match instr with 
209
  | MReset i ->
210 40f8d0f9 ploc
    pp_machine_init m self fmt i
211 04a7df69 ploc
  | MLocalAssign (i,v) ->
212
    pp_assign
213
      m self (pp_horn_var m) fmt
214
      i.var_type (LocalVar i) v
215
  | MStateAssign (i,v) ->
216
    pp_assign
217
      m self (pp_horn_var m) fmt
218
      i.var_type (StateVar i) v
219
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
220
    pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl)))
221
  | MStep (il, i, vl) ->
222
    pp_instance_call machines ~init:init m self fmt i vl il
223
  | MBranch (g,hl) ->
224
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
225
    then (* boolean case, needs special treatment in C because truth value is not unique *)
226
	 (* may disappear if we optimize code by replacing last branch test with default *)
227
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
228
      let el = try List.assoc tag_false hl with Not_found -> [] in
229
      pp_conditional machines ~init:init m self fmt g tl el
230
    else assert false (* enum type case *)
231
232
233
(**************************************************************)
234 aa6b7d46 ploc
    
235
(* Print the machine m: 
236
   two functions: m_init and m_step
237
   - m_init is a predicate over m memories
238
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
239
   We first declare all variables then the two /rules/.
240
*)
241 04a7df69 ploc
let print_machine machines fmt m = 
242
  let pp_instr init = pp_machine_instr machines ~init:init m in
243
  if m.mname.node_id = arrow_id then () 
244
  else 
245
    ( (* We don't print arrow function *)
246 aa6b7d46 ploc
   Format.fprintf fmt "; %s@." m.mname.node_id;
247
   (* Printing variables *)
248
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
249 faa5e5c5 ploc
     ((machine_vars machines m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
250 04a7df69 ploc
   Format.pp_print_newline fmt ();
251 aa6b7d46 ploc
   (* Declaring predicate *)
252 04a7df69 ploc
   Format.fprintf fmt "(declare-rel %a (%a))@."
253 40f8d0f9 ploc
     pp_machine_init_name m.mname.node_id
254 faa5e5c5 ploc
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
255 aa6b7d46 ploc
   
256 04a7df69 ploc
   Format.fprintf fmt "(declare-rel %a (%a))@."
257
     pp_machine_step_name m.mname.node_id
258 faa5e5c5 ploc
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m));
259 04a7df69 ploc
   Format.pp_print_newline fmt ();
260 aa6b7d46 ploc
261 04a7df69 ploc
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@."
262
     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
263 aa6b7d46 ploc
     m.mname.node_id
264 faa5e5c5 ploc
     (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
265
266 aa6b7d46 ploc
267 04a7df69 ploc
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@."
268
     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
269 aa6b7d46 ploc
     m.mname.node_id
270 faa5e5c5 ploc
     (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
271 aa6b7d46 ploc
   
272
()
273
  )
274
275 faa5e5c5 ploc
let main_print machines fmt = 
276
if !Options.main_node <> "" then 
277
  begin
278
    let node = !Options.main_node in
279
    let machine = get_machine machines node in
280
    Format.fprintf fmt "; Collecting semantics with main node %s@.@." node;
281
    (* We print the types of the main node "memory tree" TODO: add the output *)
282
    let main_memory_next = 
283 4f3cc9f3 ploc
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) 
284 faa5e5c5 ploc
    in
285
    let main_memory_current = 
286 4f3cc9f3 ploc
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) 
287 faa5e5c5 ploc
    in
288
    Format.fprintf fmt "(declare-rel MAIN (%a Bool))@."
289
      (Utils.fprintf_list ~sep:" " pp_type) 
290
      (List.map (fun v -> v.var_type) main_memory_next);
291
    
292
    Format.fprintf fmt "; Initial set@.";
293
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
294
    Format.fprintf fmt "(rule INIT_STATE)@.";
295
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%s_init %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
296
      node
297
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
298
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next;
299
300
    Format.fprintf fmt "; Inductive def@.";
301
    Format.fprintf fmt "(declare-var dummy Bool)@.";
302
    Format.fprintf fmt 
303
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
304
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
305
      node
306
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
307
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next;
308
309
    Format.fprintf fmt "; Property def@.";
310
    Format.fprintf fmt "(declare-rel ERR ())@.";
311
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (= top.OK true))@ (MAIN %a)@])@ ERR))@."
312
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current;
313
    Format.fprintf fmt "(query ERR)@.";
314
315
    ()
316
end
317
318 aa6b7d46 ploc
319
let translate fmt basename prog machines =
320 04a7df69 ploc
  List.iter (print_machine machines fmt) (List.rev machines);
321 faa5e5c5 ploc
  main_print machines fmt 
322 aa6b7d46 ploc
323
324
(* Local Variables: *)
325
(* compile-command:"make -C .." *)
326
(* End: *)