Project

General

Profile

Download (9.15 KB) Statistics
| Branch: | Tag: | Revision:
1
open Format
2
open LustreSpec
3
open Corelang
4
open Machine_code
5

    
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

    
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
let pp_instr machine_name fmt i =
31
  Format.fprintf fmt "(xxx)"
32

    
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)
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)
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)
40

    
41
let full_memory_vars machine instance =
42
  (rename_current_list machine.mname.node_id machine.mmemory) @
43
    (rename_next_list machine.mname.node_id machine.mmemory)
44

    
45
let machine_vars m = 
46
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
47
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
48
  full_memory_vars m ()
49

    
50
  
51
(********************************************************************************************)
52
(*                    Instruction Printing functions                                        *)
53
(********************************************************************************************)
54

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

    
62

    
63
(* Used to print boolean constants *)
64
let pp_horn_tag fmt t =
65
  pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
66

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

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

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

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

    
153
let pp_machine_reset (m: machine_t) self fmt inst =
154
  let (node, static) = List.assoc inst m.minstances in
155
  fprintf fmt "(%a %a%t%s->%s)"
156
    pp_machine_reset_name (node_name node)
157
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
158
    (Utils.pp_final_char_if_non_empty " " static)
159
    self inst
160

    
161
(* TODO *)
162
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
163
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
164
    (pp_horn_val self (pp_horn_var m)) c
165
    (Utils.pp_newline_if_non_empty tl)
166
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
167
    (Utils.pp_newline_if_non_empty el)
168
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
169

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

    
195

    
196
(**************************************************************)
197
    
198
(* Print the machine m: 
199
   two functions: m_init and m_step
200
   - m_init is a predicate over m memories
201
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
202
   We first declare all variables then the two /rules/.
203
*)
204
let print_machine machines fmt m = 
205
  let pp_instr init = pp_machine_instr machines ~init:init m in
206
  if m.mname.node_id = arrow_id then () 
207
  else 
208
    ( (* We don't print arrow function *)
209
   Format.fprintf fmt "; %s@." m.mname.node_id;
210
   (* Printing variables *)
211
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
212
     ((machine_vars m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
213
   Format.pp_print_newline fmt ();
214
   (* Declaring predicate *)
215
   Format.fprintf fmt "(declare-rel %a (%a))@."
216
     pp_machine_reset_name m.mname.node_id
217
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mmemory);
218
   
219
   Format.fprintf fmt "(declare-rel %a (%a))@."
220
     pp_machine_step_name m.mname.node_id
221
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (machine_vars m));
222
   Format.pp_print_newline fmt ();
223

    
224
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@."
225
     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
226
     m.mname.node_id
227
     (Utils.fprintf_list ~sep:" " pp_var) (rename_next_list m.mname.node_id m.mmemory);
228

    
229
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@."
230
     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
231
     m.mname.node_id
232
     (Utils.fprintf_list ~sep:" " pp_var) (machine_vars m);
233
   
234
()
235
  )
236

    
237
let main_print fmt = ()
238

    
239
let translate fmt basename prog machines =
240
  List.iter (print_machine machines fmt) (List.rev machines);
241
  main_print fmt 
242

    
243

    
244
(* Local Variables: *)
245
(* compile-command:"make -C .." *)
246
(* End: *)
(20-20/45)