Project

General

Profile

« Previous | Next » 

Revision bd3ef34a

Added by Pierre-Loïc Garoche over 7 years ago

Solved local var name bugs for stateless nodes as outlined by Teme

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@276 041b043f-8d7c-46b2-b46e-ef0dd855326e

View differences:

src/horn_backend.ml
6 6

  
7 7
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
8 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
9 10

  
10 11
let pp_type fmt t =
11 12
  match (Types.repr t).Types.tdesc with
......
55 56
  in
56 57
  aux true machine.mname.node_id machine
57 58

  
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

  
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
    
64 63
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)@
64
  (stateless_vars machines m)@
67 65
    (rename_current_list (full_memory_vars machines m)) @ 
68 66
    (rename_next_list (full_memory_vars machines m)) 
69

  
67
    
70 68
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
  
69
  (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m)) 
70
    
75 71
(********************************************************************************************)
76 72
(*                    Instruction Printing functions                                        *)
77 73
(********************************************************************************************)
......
142 138
           pp_assign
143 139
   	     m
144 140
   	     self
145
   	     (pp_horn_var m)
146
	     (* (pp_horn_val self (pp_horn_var m) fmt o) *)  fmt
141
   	     (pp_horn_var m) 
142
	     (* (pp_horn_val self (pp_horn_var m) fmt o) *)
143
	     fmt
147 144
   	     o.var_type (LocalVar o) i1
148 145
         else
149 146
           pp_assign
......
155 152
	begin
156 153
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
157 154
	  if init then
158
	  Format.fprintf fmt "(%s_init %a%t%a%t%a)"
159
	    (node_name n) 
155
	  Format.fprintf fmt "(%a %a%t%a%t%a)"
156
	    pp_machine_init_name (node_name n) 
157
	    (* inputs *)
160 158
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
161 159
	    (Utils.pp_final_char_if_non_empty " " inputs) 
160
	    (* outputs *)
162 161
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
163 162
	    (Utils.pp_final_char_if_non_empty " " outputs)
163
	    (* memories (next) *)
164 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)) 
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
		) 
166 170
	     )
167 171
	  else
168
	    Format.fprintf fmt "(%s_step %a%t%a%t%a)"
169
	    (node_name n) 
172
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
173
	      pp_machine_step_name (node_name n) 
170 174
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
171 175
	      (Utils.pp_final_char_if_non_empty " " inputs) 
172 176
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
173 177
	      (Utils.pp_final_char_if_non_empty " " outputs)
174 178
	      (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))) 
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
		  ) 
178 189
	       )
179 190
	    
180
	     end
191
	end
181 192
    end
182 193
    with Not_found -> ( (* stateless node instance *)
183 194
      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 
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  *)
189 201
    )
190 202

  
191 203
let pp_machine_init (m: machine_t) self fmt inst =
......
217 229
    pp_assign
218 230
      m self (pp_horn_var m) fmt
219 231
      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)))
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))) *)
222 234
  | MStep (il, i, vl) ->
223 235
    pp_instance_call machines ~init:init m self fmt i vl il
224 236
  | MBranch (g,hl) ->
......
241 253
*)
242 254
let print_machine machines fmt m = 
243 255
  let pp_instr init = pp_machine_instr machines ~init:init m in
244
  if m.mname.node_id = arrow_id then () 
256
  if m.mname.node_id = arrow_id then 
257
    (* We don't print arrow function *)
258
    ()
245 259
  else 
246
    ( (* We don't print arrow function *)
247
   Format.fprintf fmt "; %s@." m.mname.node_id;
260
    begin 
261
      Format.fprintf fmt "; %s@." m.mname.node_id;
262

  
248 263
   (* Printing variables *)
249 264
   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));
265
     ((step_vars machines m)@
266
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
260 267
   Format.pp_print_newline fmt ();
261 268

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

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

  
309
   (* Rule for step *)
310
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
311
	 (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
312
	 pp_machine_step_name m.mname.node_id
313
	 (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
314

  
315
       match m.mspec with
316
	 None -> () (* No node spec; we do nothing *)
317
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> 
318
	 ( 
277 319
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
278
       ()
279
	 
280
     )
281
   | _ -> () (* Other cases give nothing *)
282
    )
320
	   ()
321
	     
322
	 )
323
       | _ -> () (* Other cases give nothing *)
324
     end
325
    end
283 326

  
284 327

  
285 328

  
......
312 355
    Format.fprintf fmt "; Initial set@.";
313 356
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
314 357
    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
358
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
359
      pp_machine_init_name node
317 360
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
318 361
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
319 362

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

  

Also available in: Unified diff