Project

General

Profile

« Previous | Next » 

Revision 5de4dde4

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

Major refreshing of machine generation

View differences:

src/machine_code.ml
18 18
  
19 19
exception NormalizationError
20 20

  
21
(* Questions:
22

  
23
   - where are used the mconst. They contain initialization of
24
   constant in nodes. But they do not seem to be used by c_backend *)
21 25

  
22 26
       
23 27
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
......
26 30
(*                       j : node aka machine instances  *)
27 31
(*                       d : local variables             *)
28 32
(*                       s : step instructions           *)
29
let translate_ident vars _ (* (m, si, j, d, s) *) id =
33

  
34
(* Machine processing requires knowledge about variables and local
35
   variables. Local could be memories while other could not.  *)
36
type machine_env = {
37
    is_local: string -> bool;
38
    get_var: string -> var_decl
39
  }
40

  
41
                 
42
let build_env locals non_locals =
43
  let all = VSet.union locals non_locals in
44
  {
45
    is_local = (fun id -> VSet.exists (fun v -> v.var_id = id) locals);
46
    get_var = (fun id -> try
47
                  VSet.get id all
48
                with Not_found -> (
49
                  Format.eprintf "Impossible to find variable %s in set %a@.@?"
50
                    id
51
                    VSet.pp all;
52
                  raise Not_found
53
                )
54
              )  
55
  }
56

  
57
  
58

  
59
(****************************************************************)
60
(* Basic functions to translate to machine values, instructions *) 
61
(****************************************************************)
62

  
63
let translate_ident env id =
30 64
  (* Format.eprintf "trnaslating ident: %s@." id; *)
31 65
  try (* id is a var that shall be visible here , ie. in vars *)
32
    let var_id = get_var id vars in
66
    let var_id = env.get_var id in
33 67
    mk_val (Var var_id) var_id.var_type
34 68
  with Not_found ->
35 69
    try (* id is a constant *)
......
38 72
      in
39 73
      mk_val (Var vdecl) vdecl.var_type
40 74
    with Not_found ->
41
      (* id is a tag *)
42
      (* DONE construire une liste des enum declarés et alors chercher
43
         dedans la liste qui contient id *)
75
      (* id is a tag, getting its type in the list of declared enums *)
44 76
      try
45 77
        let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
46 78
        mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
......
49 81
                           id;
50 82
                         assert false)
51 83

  
52
let rec control_on_clock vars ((m, si, j, d, s) as args) ck inst =
84
let rec control_on_clock env ck inst =
53 85
 match (Clocks.repr ck).cdesc with
54 86
 | Con    (ck1, cr, l) ->
55 87
   let id  = Clocks.const_of_carrier cr in
56
   control_on_clock vars args ck1 (mkinstr
57
				     (* TODO il faudrait prendre le lustre
58
					associé à instr et rajouter print_ck_suffix
59
					ck) de clocks.ml *)
60
				     (MBranch (translate_ident vars args id,
61
					       [l, [inst]] )))
88
   control_on_clock env ck1
89
     (mkinstr
90
	(MBranch (translate_ident env id,
91
		  [l, [inst]] )))
62 92
 | _                   -> inst
63 93

  
64 94

  
65
(* specialize predefined (polymorphic) operators
66
   wrt their instances, so that the C semantics
67
   is preserved *)
95
(* specialize predefined (polymorphic) operators wrt their instances,
96
   so that the C semantics is preserved *)
68 97
let specialize_to_c expr =
69 98
 match expr.expr_desc with
70 99
 | Expr_appl (id, e, r) ->
......
83 112
  | "C" -> specialize_to_c expr
84 113
  | _   -> expr
85 114

  
86
let rec translate_expr vars ((m, si, j, d, s) as args) expr =
115
let rec translate_expr env expr =
87 116
  let expr = specialize_op expr in
88
  (* all calls are using the same arguments (vars for the variable
89
     enviroment and args for computed memories). No fold constructs
90
     here. We can do partial evaluation of translate_expr *)
91
  let translate_expr = translate_expr vars args in 
117
  let translate_expr = translate_expr env in
92 118
  let value_desc = 
93 119
    match expr.expr_desc with
94 120
    | Expr_const v                     -> Cst v
95
    | Expr_ident x                     -> (translate_ident vars args x).value_desc
121
    | Expr_ident x                     -> (translate_ident env x).value_desc
96 122
    | Expr_array el                    -> Array (List.map translate_expr el)
97 123
    | Expr_access (t, i)               -> Access (translate_expr t,
98 124
                                                  translate_expr 
......
115 141
       let nd = node_from_name id in
116 142
       Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
117 143
    | Expr_ite (g,t,e) -> (
118
      (* special treatment depending on the active backend. For horn backend, ite
119
	 are preserved in expression. While they are removed for C or Java
120
	 backends. *)
121
      match !Options.output with
122
      | "horn" -> 
123
	 Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
124
      | "C" | "java" | _ -> 
125
	 (Format.eprintf "Normalization error for backend %s: %a@."
126
	    !Options.output
127
	    Printers.pp_expr expr;
128
	  raise NormalizationError)
144
      (* special treatment depending on the active backend. For
145
         functional ones, like horn backend, ite are preserved in
146
         expression. While they are removed for C or Java backends. *)
147
      if Backends.is_functional () then
148
	Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
149
      else 
150
	(Format.eprintf "Normalization error for backend %s: %a@."
151
	   !Options.output
152
	   Printers.pp_expr expr;
153
	 raise NormalizationError)
129 154
    )
130 155
    | _                   -> raise NormalizationError
131 156
  in
132 157
  mk_val value_desc expr.expr_type
133 158

  
134
let translate_guard vars args expr =
159
let translate_guard env expr =
135 160
  match expr.expr_desc with
136
  | Expr_ident x  -> translate_ident vars args x
161
  | Expr_ident x  -> translate_ident env x
137 162
  | _ -> (Format.eprintf "internal error: translate_guard %a@."
138 163
            Printers.pp_expr expr;
139 164
          assert false)
140 165

  
141
let rec translate_act vars ((m, si, j, d, s) as args) (y, expr) =
142
  let translate_act = translate_act vars args in
143
  let translate_guard = translate_guard vars args in
144
  let translate_ident = translate_ident vars args in
145
  let translate_expr = translate_expr vars args in
166
let rec translate_act env (y, expr) =
167
  let translate_act = translate_act env in
168
  let translate_guard = translate_guard env in
169
  let translate_ident = translate_ident env in
170
  let translate_expr = translate_expr env in
146 171
  let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
147 172
  match expr.expr_desc with
148 173
  | Expr_ite   (c, t, e) -> let g = translate_guard c in
......
157 182
  | _                    -> mkinstr ?lustre_eq:(Some eq)
158 183
                              (MLocalAssign (y, translate_expr expr))
159 184

  
160
let reset_instance vars args i r c =
185
let reset_instance env i r c =
161 186
  match r with
162 187
  | None        -> []
163
  | Some r      -> let g = translate_guard vars args r in
188
  | Some r      -> let g = translate_guard env r in
164 189
                   [control_on_clock
165
                      vars
166
                      args
190
                      env
167 191
                      c
168 192
                      (mk_conditional
169 193
                         g
......
171 195
                         [mkinstr (MNoReset i)])
172 196
                   ]
173 197

  
174
let translate_eq vars ((m, si, j, d, s) as args) eq =
175
  let translate_expr = translate_expr vars args in
176
  let translate_act = translate_act vars args in
177
  let control_on_clock = control_on_clock vars args in
178
  let reset_instance = reset_instance vars args in
198

  
199
(* Datastructure updated while visiting equations *)
200
type machine_ctx = {
201
    m: VSet.t; (* Memories *)
202
    si: instr_t list;
203
    j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
204
    s: instr_t list;
205
  }
206

  
207
let ctx_init = { m = VSet.empty; (* memories *)
208
                 si = []; (* init instr *)
209
                 j = Utils.IMap.empty;
210
                 s = [] }
211
             
212
(****************************************************************)
213
(* Main function to translate equations into this machine context we
214
   are building *) 
215
(****************************************************************)
216

  
217
                   
218

  
219
let translate_eq env ctx eq =
220
  let translate_expr = translate_expr env in
221
  let translate_act = translate_act env in
222
  let control_on_clock = control_on_clock env in
223
  let reset_instance = reset_instance env in
179 224

  
180 225
  (* Format.eprintf "translate_eq %a with clock %a@." 
181 226
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
182 227
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
183 228
  | [x], Expr_arrow (e1, e2)                     ->
184
     let var_x = get_var x vars in
229
     let var_x = env.get_var x in
185 230
     let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
186 231
     let c1 = translate_expr e1 in
187 232
     let c2 = translate_expr e2 in
188
     (m,
189
      mkinstr (MReset o) :: si,
190
      Utils.IMap.add o (Arrow.arrow_top_decl, []) j,
191
      d,
192
      (control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)
193
  | [x], Expr_pre e1 when VSet.mem (get_var x vars) d     ->
194
     let var_x = get_var x vars in
195
     (VSet.add var_x m,
196
      si,
197
      j,
198
      d,
199
      control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1))) :: s)
200
  | [x], Expr_fby (e1, e2) when VSet.mem (get_var x vars) d ->
201
     let var_x = get_var x vars in
202
     (VSet.add var_x m,
203
      mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1)) :: si,
204
      j,
205
      d,
206
      control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e2))) :: s)
233
     { ctx with
234
       si = mkinstr (MReset o) :: ctx.si;
235
       j = Utils.IMap.add o (Arrow.arrow_top_decl, []) ctx.j;
236
       s = (control_on_clock
237
              eq.eq_rhs.expr_clock
238
              (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))
239
           ) :: ctx.s
240
     }
241
  | [x], Expr_pre e1 when env.is_local x    ->
242
     let var_x = env.get_var x in
243
     
244
      { ctx with
245
        m = VSet.add var_x ctx.m;
246
        s = control_on_clock
247
              eq.eq_rhs.expr_clock
248
              (mkinstr ?lustre_eq:(Some eq)
249
                 (MStateAssign (var_x, translate_expr e1)))
250
            :: ctx.s
251
      }
252
  | [x], Expr_fby (e1, e2) when env.is_local x ->
253
     let var_x = env.get_var x in
254
     { ctx with
255
       m = VSet.add var_x ctx.m;
256
       si = mkinstr ?lustre_eq:(Some eq)
257
              (MStateAssign (var_x, translate_expr e1))
258
            :: ctx.si;
259
       s = control_on_clock
260
             eq.eq_rhs.expr_clock
261
             (mkinstr ?lustre_eq:(Some eq)
262
                (MStateAssign (var_x, translate_expr e2)))
263
           :: ctx.s
264
     }
207 265

  
208 266
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
209
     let var_p = List.map (fun v -> get_var v vars) p in
267
     let var_p = List.map (fun v -> env.get_var v) p in
210 268
     let el = expr_list_of_expr arg in
211 269
     let vl = List.map translate_expr el in
212 270
     let node_f = node_from_name f in
......
219 277
     (*Clocks.new_var true in
220 278
       Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
221 279
       Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
222
     (m,
223
      (if Stateless.check_node node_f then si else mkinstr (MReset o) :: si),
224
      Utils.IMap.add o call_f j,
225
      d,
226
      (if Stateless.check_node node_f
227
       then []
228
       else reset_instance o r call_ck) @
229
	(control_on_clock call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s)
230
  (*
231
    (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
232
    are preserved. While they are replaced as if g then x = t else x = e in  C or Java
233
    backends. *)
234
    | [x], Expr_ite   (c, t, e)
235
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
236
    ->
237
    let var_x = get_node_var x node in
238
    (m,
239
    si,
240
    j,
241
    d,
242
    (control_on_clock node args eq.eq_rhs.expr_clock
243
    (MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
244
    )
280
     { ctx with
281
       si = 
282
         (if Stateless.check_node node_f then ctx.si else mkinstr (MReset o) :: ctx.si);
283
      j = Utils.IMap.add o call_f ctx.j;
284
      s = (if Stateless.check_node node_f
285
           then []
286
           else reset_instance o r call_ck) @
287
	    (control_on_clock call_ck
288
               (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl))))
289
            :: ctx.s
290
     }
245 291

  
246
  *)
247 292
  | [x], _                                       -> (
248
    let var_x = get_var x vars in
249
    (m, si, j, d,
250
     control_on_clock
293
    let var_x = env.get_var x in
294
    { ctx with
295
      s = 
296
     control_on_clock 
251 297
       eq.eq_rhs.expr_clock
252
       (translate_act (var_x, eq.eq_rhs)) :: s
253
    )
298
       (translate_act (var_x, eq.eq_rhs)) :: ctx.s
299
    }
254 300
  )
255 301
  | _                                            ->
256 302
     begin
257
       Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;
303
       Format.eprintf "internal error: Machine_code.translate_eq %a@?"
304
         Printers.pp_node_eq eq;
258 305
       assert false
259 306
     end
260 307

  
261 308

  
262 309

  
263
let constant_equations nd =
264
 List.fold_right (fun vdecl eqs ->
310
let constant_equations locals =
311
 VSet.fold (fun vdecl eqs ->
265 312
   if vdecl.var_dec_const
266 313
   then
267 314
     { eq_lhs = [vdecl.var_id];
......
269 316
       eq_loc = vdecl.var_loc
270 317
     } :: eqs
271 318
   else eqs)
272
   nd.node_locals []
319
   locals []
273 320

  
274
let translate_eqs node args eqs =
275
  List.fold_right (fun eq args -> translate_eq node args eq) eqs args;;
321
let translate_eqs env ctx eqs =
322
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx;;
323

  
324

  
325
(****************************************************************)
326
(* Processing nodes *) 
327
(****************************************************************)
276 328

  
277 329
let process_asserts nd =
278 330
  
......
299 351
	  in
300 352
	  assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); 
301 353
	  let eq = mkeq loc ([var_id], expr) in
302
          (i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)
354
          (i+1,
355
           assert_var::vars,
356
           eq::eqlist,
357
           {expr with expr_desc = Expr_ident var_id}::assertlist)
303 358
	) (1, [], [], []) exprl
304 359
      in
305 360
      vars, eql, assertl
361

  
362
let translate_core sorted_eqs locals other_vars =
363
  let constant_eqs = constant_equations locals in
306 364
  
307
let translate_decl nd sch =
308
  (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
309
  let schedule = sch.Scheduling_type.schedule in
310
  let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in
311
  let constant_eqs = constant_equations nd in
365
  let env = build_env locals other_vars  in
366
  
367
  (* Compute constants' instructions  *)
368
  let ctx0 = translate_eqs env ctx_init constant_eqs in
369
  assert (VSet.is_empty ctx0.m);
370
  assert (ctx0.si = []);
371
  assert (Utils.IMap.is_empty ctx0.j);
372
  
373
  (* Compute ctx for all eqs *)
374
  let ctx = translate_eqs env ctx_init sorted_eqs in
375
  
376
  ctx, ctx0.s
312 377

  
378
let translate_decl nd sch =
379
  (* Extracting eqs, variables ..  *)
380
  let eqs, auts = get_node_eqs nd in
381
  assert (auts = []); (* Automata should be expanded by now *)
382
  
313 383
  (* In case of non functional backend (eg. C), additional local variables have
314 384
     to be declared for each assert *)
315 385
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
386

  
387
  (* Build the env: variables visible in the current scope *)
316 388
  let locals_list = nd.node_locals @ new_locals in
317
  let nd = { nd with node_locals = locals_list } in
318
  let vars = get_node_vars nd in
389
  let locals = VSet.of_list locals_list in
390
  let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in
391
  let env = build_env locals inout_vars  in 
392
  
393
  (* Computing main content *)
394
  let schedule = sch.Scheduling_type.schedule in
395
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
396

  
397
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
398
(* CODE QUI MARCHE
399
  let constant_eqs = constant_equations locals in
319 400
  
320
  let init_args = VSet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> VSet.add l) locals_list VSet.empty, [] in
321
  (* memories, init instructions, node calls, local variables (including memories), step instrs *)
401
  (* Compute constants' instructions  *)
402
  let ctx0 = translate_eqs env ctx_init constant_eqs in
403
  assert (VSet.is_empty ctx0.m);
404
  assert (ctx0.si = []);
405
  assert (Utils.IMap.is_empty ctx0.j);
322 406

  
323
  let m0, init0, j0, locals0, s0 =
324
    translate_eqs vars init_args constant_eqs
407
  (* Compute ctx for all eqs *)
408
  let ctx = translate_eqs env ctx_init (assert_instrs@sorted_eqs) in
409
 *)
410
  
411
  (*
412
  (* Processing spec: locals would be actual locals of the spec while
413
     non locals would be inputs/ouptpus of the node. Locals of the
414
     node are not visible. *)
415
  let spec =
416
    match nd.node_spec with
417
    | None -> None
418
    | Some spec -> translate_spec inout_vars spec
325 419
  in
326 420

  
327
  assert (VSet.is_empty m0);
328
  assert (init0 = []);
329
  assert (Utils.IMap.is_empty j0);
330 421

  
331
  let m, init, j, locals, s as context_with_asserts =
332
    translate_eqs
333
      vars
334
      (m0, init0, j0, locals0, [])
335
      (assert_instrs@sorted_eqs)
336
  in
337
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
422
        inout_vars spec =
423
    let locals = VSet.of_list spec.locals in
424
    let spec_consts = VSet.of_list spec.consts in
425
    let other_spec_vars = VSet.union inout_vars spec_consts in
426
    let spec_env = build_env spec_locals other_spec_vars in
427
   *)             
428
  let mmap = Utils.IMap.elements ctx.j in
338 429
  {
339 430
    mname = nd;
340
    mmemory = VSet.elements m;
431
    mmemory = VSet.elements ctx.m;
341 432
    mcalls = mmap;
342 433
    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
343
    minit = init;
344
    mconst = s0;
434
    minit = ctx.si;
435
    mconst = ctx0_s;
345 436
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
346 437
    mstep = {
347
      step_inputs = nd.node_inputs;
348
      step_outputs = nd.node_outputs;
349
      step_locals = VSet.elements (VSet.diff locals m);
350
      step_checks = List.map (fun d -> d.Dimension.dim_loc,
351
                                       translate_expr vars init_args
352
                                         (expr_of_dimension d))
353
                      nd.node_checks;
354
      step_instrs = (
355
	(* special treatment depending on the active backend. For horn backend,
438
        step_inputs = nd.node_inputs;
439
        step_outputs = nd.node_outputs;
440
        step_locals = (* Removing computed memories from locals *)
441
          VSet.elements (VSet.diff locals ctx.m);
442
        step_checks = List.map (fun d -> d.Dimension.dim_loc,
443
                                         translate_expr env 
444
                                           (expr_of_dimension d))
445
                        nd.node_checks;
446
        step_instrs = (
447
	  (* special treatment depending on the active backend. For horn backend,
356 448
	   common branches are not merged while they are in C or Java
357 449
	   backends. *)
358
	(*match !Options.output with
359
	| "horn" -> s
360
	  | "C" | "java" | _ ->*)
361
	if !Backends.join_guards then
362
	  join_guards_list s
363
	else
364
	  s
365
      );
366
      step_asserts = List.map (translate_expr vars context_with_asserts) nd_node_asserts;
367
    };
450
	  if !Backends.join_guards then
451
	    join_guards_list ctx.s
452
	  else
453
	    ctx.s
454
        );
455
        step_asserts = List.map (translate_expr env) nd_node_asserts;
456
      };
368 457
    mspec = nd.node_spec;
369 458
    mannot = nd.node_annot;
370 459
    msch = Some sch;

Also available in: Unified diff