Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / horn_backend.ml @ 0038002e

History | View | Annotate | Download (14.6 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
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
10

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

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

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

    
32

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

    
43

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

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

    
59
let stateless_vars machines m = 
60
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
61
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
62
    
63
let step_vars machines m = 
64
  (stateless_vars machines m)@
65
    (rename_current_list (full_memory_vars machines m)) @ 
66
    (rename_next_list (full_memory_vars machines m)) 
67
    
68
let init_vars machines m = 
69
  (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m)) 
70
    
71
(********************************************************************************************)
72
(*                    Instruction Printing functions                                        *)
73
(********************************************************************************************)
74

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

    
82

    
83
(* Used to print boolean constants *)
84
let pp_horn_tag fmt t =
85
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
86

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

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

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

    
121
(* type_directed assignment: array vs. statically sized type
122
   - [var_type]: type of variable to be assigned
123
   - [var_name]: name of variable to be assigned
124
   - [value]: assigned value
125
   - [pp_var]: printer for variables
126
*)
127
let pp_assign m self pp_var fmt var_type var_name value =
128
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
129
  
130
let pp_instance_call 
131
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
132
  try (* stateful node instance *) 
133
    begin
134
      let (n,_) = List.assoc i m.minstances in
135
      match node_name n, inputs, outputs with
136
      | "_arrow", [i1; i2], [o] -> begin
137
         if init then
138
           pp_assign
139
   	     m
140
   	     self
141
   	     (pp_horn_var m) 
142
	     (* (pp_horn_val self (pp_horn_var m) fmt o) *)
143
	     fmt
144
   	     o.var_type (LocalVar o) i1
145
         else
146
           pp_assign
147
   	     m self (pp_horn_var m) fmt
148
   	     o.var_type (LocalVar o) i2
149
	     
150
      end
151
      | name, _, _ ->  
152
	begin
153
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
154
	  if init then
155
	  Format.fprintf fmt "(%a %a%t%a%t%a)"
156
	    pp_machine_init_name (node_name n) 
157
	    (* inputs *)
158
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
159
	    (Utils.pp_final_char_if_non_empty " " inputs) 
160
	    (* outputs *)
161
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
162
	    (Utils.pp_final_char_if_non_empty " " outputs)
163
	    (* memories (next) *)
164
	    (Utils.fprintf_list ~sep:" " pp_var) (
165
  	      rename_machine_list 
166
		(concat m.mname.node_id i) 
167
		(rename_next_list (* concat m.mname.node_id i *) 
168
		   (full_memory_vars machines target_machine)
169
		) 
170
	     )
171
	  else
172
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
173
	      pp_machine_step_name (node_name n) 
174
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
175
	      (Utils.pp_final_char_if_non_empty " " inputs) 
176
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
177
	      (Utils.pp_final_char_if_non_empty " " outputs)
178
	      (Utils.fprintf_list ~sep:" " pp_var) (
179
		(rename_machine_list 
180
		   (concat m.mname.node_id i) 
181
		   (rename_current_list (* concat m.mname.node_id i *) 
182
		      (full_memory_vars machines target_machine))
183
		) @ 
184
		  (rename_machine_list 
185
		     (concat m.mname.node_id i) 
186
		     (rename_next_list (* concat m.mname.node_id i *) 
187
			(full_memory_vars machines target_machine))
188
		  ) 
189
	       )
190
	    
191
	end
192
    end
193
    with Not_found -> ( (* stateless node instance *)
194
      let (n,_) = List.assoc i m.mcalls in
195
      Format.fprintf fmt "(%s %a%t%a)"
196
	(node_name n)
197
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
198
	(Utils.pp_final_char_if_non_empty " " inputs) 
199
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
200
	(* (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs  *)
201
    )
202

    
203
let pp_machine_init (m: machine_t) self fmt inst =
204
  let (node, static) = List.assoc inst m.minstances in
205
  fprintf fmt "(%a %a%t%s->%s)"
206
    pp_machine_init_name (node_name node)
207
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
208
    (Utils.pp_final_char_if_non_empty " " static)
209
    self inst
210

    
211
(* TODO *)
212
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
213
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
214
    (pp_horn_val self (pp_horn_var m)) c
215
    (Utils.pp_newline_if_non_empty tl)
216
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
217
    (Utils.pp_newline_if_non_empty el)
218
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
219

    
220
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
221
  match instr with 
222
  | MReset i ->
223
    pp_machine_init m self fmt i
224
  | MLocalAssign (i,v) ->
225
    pp_assign
226
      m self (pp_horn_var m) fmt
227
      i.var_type (LocalVar i) v
228
  | MStateAssign (i,v) ->
229
    pp_assign
230
      m self (pp_horn_var m) fmt
231
      i.var_type (StateVar i) v
232
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> assert false (* This should not happen anymore *)
233
(*    pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl))) *)
234
  | MStep (il, i, vl) ->
235
    pp_instance_call machines ~init:init m self fmt i vl il
236
  | MBranch (g,hl) ->
237
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
238
    then (* boolean case, needs special treatment in C because truth value is not unique *)
239
	 (* may disappear if we optimize code by replacing last branch test with default *)
240
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
241
      let el = try List.assoc tag_false hl with Not_found -> [] in
242
      pp_conditional machines ~init:init m self fmt g tl el
243
    else assert false (* enum type case *)
244

    
245

    
246
(**************************************************************)
247
   
248
let is_stateless m = m.minstances = [] && m.mmemory = [] 
249

    
250
(* Print the machine m: 
251
   two functions: m_init and m_step
252
   - m_init is a predicate over m memories
253
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
254
   We first declare all variables then the two /rules/.
255
*)
256
let print_machine machines fmt m = 
257
  let pp_instr init = pp_machine_instr machines ~init:init m in
258
  if m.mname.node_id = arrow_id then 
259
    (* We don't print arrow function *)
260
    ()
261
  else 
262
    begin 
263
      Format.fprintf fmt "; %s@." m.mname.node_id;
264

    
265
   (* Printing variables *)
266
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
267
     ((step_vars machines m)@
268
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
269
   Format.pp_print_newline fmt ();
270

    
271
   
272
   
273
   if is_stateless m then
274
     begin
275
       (* Declaring single predicate *)
276
       Format.fprintf fmt "(declare-rel %a (%a))@."
277
	 pp_machine_stateless_name m.mname.node_id
278
	 (Utils.fprintf_list ~sep:" " pp_type) 
279
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
280
       
281
       (* Rule for single predicate *)
282
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
283
	 (Utils.fprintf_list ~sep:"@ " 
284
	    (pp_instr 
285
	       true (* In this case, the boolean init can be set to true or false. 
286
		       The node is stateless. *)
287
	       m.mname.node_id)
288
	 ) 
289
	 m.mstep.step_instrs
290
	 pp_machine_stateless_name m.mname.node_id
291
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
292
     end
293
   else 
294
     begin
295
       (* Declaring predicate *)
296
       Format.fprintf fmt "(declare-rel %a (%a))@."
297
	 pp_machine_init_name m.mname.node_id
298
	 (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
299
       
300
       Format.fprintf fmt "(declare-rel %a (%a))@."
301
	 pp_machine_step_name m.mname.node_id
302
	 (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m));
303
       Format.pp_print_newline fmt ();
304

    
305
   (* Rule for init *)
306
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
307
	 (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
308
	 pp_machine_init_name m.mname.node_id
309
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
310

    
311
   (* Rule for step *)
312
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
313
	 (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
314
	 pp_machine_step_name m.mname.node_id
315
	 (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
316
(*
317
       match m.mspec with
318
	 None -> () (* No node spec; we do nothing *)
319
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> 
320
	 ( 
321
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
322
	   ()
323
	     
324
	 )
325
       | _ -> () (* Other cases give nothing *)
326
*)      
327
     end
328
    end
329

    
330

    
331

    
332
let main_print machines fmt = 
333
if !Options.main_node <> "" then 
334
  begin
335
    let node = !Options.main_node in
336
    let machine = get_machine machines node in
337

    
338
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
339
    (* We print the types of the main node "memory tree" TODO: add the output *)
340
    let main_output =
341
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
342
    in
343
    let main_output_dummy = 
344
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
345
    in
346
    let main_memory_next = 
347
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
348
      main_output
349
    in
350
    let main_memory_current = 
351
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
352
      main_output_dummy
353
    in
354

    
355
    (* Special case when the main node is stateless *)
356
    let init_name, step_name = 
357
      if is_stateless machine then
358
	pp_machine_stateless_name, pp_machine_stateless_name
359
      else
360
	pp_machine_init_name, pp_machine_step_name
361
    in
362
    
363
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
364
      (Utils.fprintf_list ~sep:" " pp_type) 
365
      (List.map (fun v -> v.var_type) main_memory_next);
366
    
367
    Format.fprintf fmt "; Initial set@.";
368
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
369
    Format.fprintf fmt "(rule INIT_STATE)@.";
370
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
371
      init_name node
372
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
373
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
374

    
375
    Format.fprintf fmt "; Inductive def@.";
376
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
377
    Format.fprintf fmt 
378
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
379
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
380
      step_name node
381
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
382
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
383

    
384
    Format.fprintf fmt "; Property def@.";
385
    Format.fprintf fmt "(declare-rel ERR ())@.";
386
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (and %a))@ (MAIN %a)@])@ ERR))@."
387
      (Utils.fprintf_list ~sep:" " pp_var) main_output
388
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
389
    ;
390
    Format.fprintf fmt "(query ERR)@.";
391

    
392
    ()
393
end
394

    
395

    
396
let translate fmt basename prog machines =
397
  List.iter (print_machine machines fmt) (List.rev machines);
398
  
399
  main_print machines fmt 
400

    
401

    
402
(* Local Variables: *)
403
(* compile-command:"make -C .." *)
404
(* End: *)