Project

General

Profile

Revision cf9cc6f9 src/backends/Horn/horn_backend_printers.ml

View differences:

src/backends/Horn/horn_backend_printers.ml
78 78
   - [value]: assigned value
79 79
   - [pp_var]: printer for variables
80 80
*)
81
let pp_assign m self pp_var fmt var_type var_name value =
81
let pp_assign m pp_var fmt var_type var_name value =
82
  let self = m.mname.node_id in
82 83
  fprintf fmt "(= %a %a)" 
83 84
    (pp_horn_val ~is_lhs:true self pp_var) var_name
84 85
    (pp_value_suffix self pp_var) value
85 86
    
86 87

  
87 88
(* In case of no reset call, we define mid_mem = current_mem *)
88
let pp_no_reset machines m target_machine i fmt =
89
let pp_no_reset machines m fmt i =
90
  let (n,_) = List.assoc i m.minstances in
91
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
92

  
89 93
  let m_list = 
90 94
    rename_machine_list
91 95
      (concat m.mname.node_id i)
......
114 118
    fprintf fmt ")@]@ @]"
115 119
  )
116 120

  
117
let pp_instance_reset machines m self fmt i =
121
let pp_instance_reset machines m fmt i =
118 122
  let (n,_) = List.assoc i m.minstances in
119 123
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
120 124
  
......
133 137
	)
134 138
    )
135 139

  
136
let pp_instance_call machines reset_instances m self fmt i inputs outputs =
140
let pp_instance_call machines reset_instances m fmt i inputs outputs =
141
  let self = m.mname.node_id in
137 142
  try (* stateful node instance *)
138 143
    begin
139 144
      let (n,_) = List.assoc i m.minstances in
......
141 146
      (* Checking whether this specific instances has been reset yet *)
142 147
      if not (List.mem i reset_instances) then
143 148
	(* If not, declare mem_m = mem_c *)
144
	pp_no_reset machines m target_machine i fmt;
149
	pp_no_reset machines m fmt i;
145 150
      
146 151
      let mems = full_memory_vars machines target_machine in
147 152
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
......
208 213
(*     pp_print_newline fmt; *)
209 214
    
210 215
    
211

  
212
let rec pp_machine_instr machines reset_instances (m: machine_t) self fmt instr =
216
(* Print the instruction and update the set of reset instances *)
217
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
213 218
  match instr with
219
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
220
    pp_no_reset machines m fmt i;
221
    i::reset_instances
214 222
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
215
    pp_instance_reset machines m self fmt i;
223
    pp_instance_reset machines m fmt i;
216 224
    i::reset_instances
217 225
  | MLocalAssign (i,v) ->
218 226
    pp_assign
219
      m self (pp_horn_var m) fmt
227
      m (pp_horn_var m) fmt
220 228
      i.var_type (LocalVar i) v;
221 229
    reset_instances
222 230
  | MStateAssign (i,v) ->
223 231
    pp_assign
224
      m self (pp_horn_var m) fmt
232
      m (pp_horn_var m) fmt
225 233
      i.var_type (StateVar i) v;
226 234
    reset_instances
227 235
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
228 236
    assert false (* This should not happen anymore *)
229 237
  | MStep (il, i, vl) ->
230
      (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
231
	 mem_c and print the call to mem_m *)
232
    pp_instance_call machines reset_instances m self fmt i vl il;
238
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
239
       mem_c and print the call to mem_m *)
240
    pp_instance_call machines reset_instances m fmt i vl il;
233 241
    reset_instances (* Since this instance call will only happen once, we
234 242
		       don't have to update reset_instances *)
235
  | MBranch (g,hl) -> (* should not be produced yet. Later, we will have to
243

  
244
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
245
			 should not be produced yet. Later, we will have to
236 246
			 compare the reset_instances of each branch and
237 247
			 introduced the mem_m = mem_c for branches to do not
238 248
			 address it while other did. Am I clear ? *)
239
    assert false
240
      
241
  (* if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false *)
242
  (* then (\* boolean case, needs special treatment in C because truth value is not unique *\) *)
243
  (*   (\* may disappear if we optimize code by replacing last branch test with default *\) *)
244
  (*   let tl = try List.assoc tag_true  hl with Not_found -> [] in *)
245
  (*   let el = try List.assoc tag_false hl with Not_found -> [] in *)
246
  (*   pp_bool_conditional machines ~init:init m self fmt g tl el *)
247
  (* else (\* enum type case *\) *)
248

  
249
  (*   pp_enum_conditional machines ~init:init m self fmt g hl  *)
249
    (* For each branch we obtain the logical encoding, and the information
250
       whether a sub node has been reset or not. If a node has been reset in one
251
       of the branch, then all others have to have the mem_m = mem_c
252
       statement. *)
253
    let self = m.mname.node_id in
254
    let pp_branch fmt (tag, instrs) =
255
      fprintf fmt "@[<v 3>(=> (= %a %s)@ "
256
	(pp_horn_val self (pp_horn_var m)) g
257
	tag;
258
      let rs = pp_machine_instrs machines reset_instances m fmt instrs in
259
      fprintf fmt "@])";
260
      () (* rs *)
261
    in
262
    pp_conj pp_branch fmt hl;
263
    reset_instances (* TODO: le code est faux en ce qui concerne les resets. Il
264
		       faut calculer ce qui se passe sur chaque branche et rajouter les instructions
265
		       adequates *)
266
	     
267
(* if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false *)
268
(* then (\* boolean case, needs special treatment in C because truth value is not unique *\) *)
269
(*   (\* may disappear if we optimize code by replacing last branch test with default *\) *)
270
(*   let tl = try List.assoc tag_true  hl with Not_found -> [] in *)
271
(*   let el = try List.assoc tag_false hl with Not_found -> [] in *)
272
(*   pp_bool_conditional machines ~init:init m self fmt g tl el *)
273
(* else (\* enum type case *\) *)
274

  
275
(*   pp_enum_conditional machines ~init:init m self fmt g hl  *)
250 276
and pp_machine_instrs machines reset_instances m fmt instrs = 
251
  let ppi rs fmt i = pp_machine_instr machines rs m m.mname.node_id fmt i in
277
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
252 278
  match instrs with
253
  | [] -> assert false
254 279
  | [x] -> ppi reset_instances fmt x 
255 280
  | _::_ ->
256 281
    fprintf fmt "(and @[<v 0>";
......
261 286
    )
262 287
      reset_instances instrs 
263 288
    in
264
    fprintf fmt "@]@ )";
289
    fprintf fmt "@])";
265 290
    rs
266 291

  
292
  | [] -> fprintf fmt "true"; reset_instances
293

  
267 294
let pp_machine_reset machines fmt m =
268 295
  let locals = local_memory_vars machines m in
269 296
  fprintf fmt "@[<v 5>(and @ ";

Also available in: Unified diff