Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / horn_backend.ml @ 12af4908

History | View | Annotate | Download (13.4 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.Treal           -> Format.fprintf fmt "Real"
15
  | Types.Tclock _
16
  | Types.Tarray _
17
  | Types.Tstatic _
18
  | Types.Tconst _
19
  | Types.Tarrow _
20
  | _                     -> Format.eprintf "internal error: pp_type %a@." 
21
                             Types.print_ty t; assert false
22
    
23

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

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

    
31

    
32
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x 
33
let rename f = (fun v -> {v with var_id = f v.var_id } )
34
let rename_machine p = rename (fun n -> concat p n)
35
let rename_machine_list p = List.map (rename_machine p)
36
    
37
let rename_current =  rename (fun n -> n ^ "_c")
38
let rename_current_list = List.map rename_current
39
let rename_next = rename (fun n -> n ^ "_x")
40
let rename_next_list = List.map rename_next
41

    
42

    
43
let get_machine machines node_name = 
44
  List.find (fun m  -> m.mname.node_id = node_name) machines 
45

    
46
let full_memory_vars machines machine =
47
  let rec aux fst prefix m =
48
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
49
      List.fold_left (fun accu (id, (n, _)) -> 
50
	let name = node_name n in 
51
	if name = "_arrow" then accu else
52
	  let machine_n = get_machine machines name in
53
	( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
54
      ) [] (m.minstances) 
55
  in
56
  aux true machine.mname.node_id machine
57

    
58
let machine_vars machines m = 
59
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
60
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
61
    (rename_current_list (full_memory_vars machines m)) @ 
62
    (rename_next_list (full_memory_vars machines m)) 
63

    
64
let step_vars machines m = 
65
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
66
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
67
    (rename_current_list (full_memory_vars machines m)) @ 
68
    (rename_next_list (full_memory_vars machines m)) 
69

    
70
let init_vars machines m = 
71
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
72
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
73
    (rename_next_list (full_memory_vars machines m)) 
74
  
75
(********************************************************************************************)
76
(*                    Instruction Printing functions                                        *)
77
(********************************************************************************************)
78

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

    
86

    
87
(* Used to print boolean constants *)
88
let pp_horn_tag fmt t =
89
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
90

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

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

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

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

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

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

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

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

    
233

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

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

    
267

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

    
273
   match m.mspec with
274
     None -> () (* No node spec; we do nothing *)
275
   | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> 
276
     ( 
277
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
278
       ()
279
	 
280
     )
281
   | _ -> () (* Other cases give nothing *)
282
    )
283

    
284

    
285

    
286
let main_print machines fmt = 
287
if !Options.main_node <> "" then 
288
  begin
289
    let node = !Options.main_node in
290
    let machine = get_machine machines node in
291

    
292
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
293
    (* We print the types of the main node "memory tree" TODO: add the output *)
294
    let main_output =
295
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
296
    in
297
    let main_output_dummy = 
298
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
299
    in
300
    let main_memory_next = 
301
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
302
      main_output
303
    in
304
    let main_memory_current = 
305
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
306
      main_output_dummy
307
    in
308
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
309
      (Utils.fprintf_list ~sep:" " pp_type) 
310
      (List.map (fun v -> v.var_type) main_memory_next);
311
    
312
    Format.fprintf fmt "; Initial set@.";
313
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
314
    Format.fprintf fmt "(rule INIT_STATE)@.";
315
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%s_init %a@])@]@ )@ (MAIN %a)@]@.))@.@."
316
      node
317
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
318
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
319

    
320
    Format.fprintf fmt "; Inductive def@.";
321
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
322
    Format.fprintf fmt 
323
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@."
324
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
325
      node
326
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
327
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
328

    
329
    Format.fprintf fmt "; Property def@.";
330
    Format.fprintf fmt "(declare-rel ERR ())@.";
331
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (and %a))@ (MAIN %a)@])@ ERR))@."
332
      (Utils.fprintf_list ~sep:" " pp_var) main_output
333
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
334
    ;
335
    Format.fprintf fmt "(query ERR)@.";
336

    
337
    ()
338
end
339

    
340

    
341
let translate fmt basename prog machines =
342
  List.iter (print_machine machines fmt) (List.rev machines);
343
  
344
  main_print machines fmt 
345

    
346

    
347
(* Local Variables: *)
348
(* compile-command:"make -C .." *)
349
(* End: *)