Project

General

Profile

« Previous | Next » 

Revision 75c459f4

Added by LĂ©lio Brun 9 months ago

start with Spec AST generation

View differences:

src/machine_code.ml
12 12
open Lustre_types
13 13
open Machine_code_types
14 14
open Machine_code_common
15
open Spec_types
16
open Spec_common
15 17
open Corelang
16 18
open Clocks
17 19
open Causality
20
open Utils
18 21

  
19 22
exception NormalizationError
20 23

  
......
58 61

  
59 62
let translate_ident env id =
60 63
  (* Format.eprintf "trnaslating ident: %s@." id; *)
61
  try (* id is a var that shall be visible here , ie. in vars *)
64
  (* id is a var that shall be visible here , ie. in vars *)
65
  try
62 66
    let var_id = env.get_var id in
63 67
    mk_val (Var var_id) var_id.var_type
64 68
  with Not_found ->
65
  try (* id is a constant *)
69

  
70
 (* id is a constant *)
71
  try
66 72
    let vdecl = (Corelang.var_decl_of_const
67 73
                   (const_of_top (Hashtbl.find Corelang.consts_table id)))
68 74
    in
69 75
    mk_val (Var vdecl) vdecl.var_type
70 76
  with Not_found ->
71
  (* id is a tag, getting its type in the list of declared enums *)
77

  
78
   (* id is a tag, getting its type in the list of declared enums *)
72 79
  try
73 80
    let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
74 81
    mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
......
76 83
    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
77 84
    assert false
78 85

  
79
let rec control_on_clock env ck inst =
80
  match (Clocks.repr ck).cdesc with
81
  | Con (ck1, cr, l) ->
82
    let id = Clocks.const_of_carrier cr in
83
    control_on_clock env ck1
84
      (mkinstr (MBranch (translate_ident env id, [l, [inst]])))
85
  | _ -> inst
86

  
87 86

  
88 87
(* specialize predefined (polymorphic) operators wrt their instances,
89 88
   so that the C semantics is preserved *)
......
158 157
      [translate_act (y, t)]
159 158
      [translate_act (y, e)]
160 159
  | Expr_merge (x, hl) ->
161
    mkinstr ~lustre_eq
162
      (MBranch (translate_ident x,
163
                List.map (fun (t,  h) -> t, [translate_act (y, h)]) hl))
164
  | _ -> mkinstr ~lustre_eq (MLocalAssign (y, translate_expr expr))
165

  
166
let reset_instance env i r c =
167
  match r with
168
  | Some r ->
169
    [control_on_clock env c
170
       (mk_conditional
171
          (translate_guard env r)
172
          [mkinstr (MReset i)]
173
          [mkinstr (MNoReset i)])]
174
  | None -> []
175

  
160
    mk_branch ~lustre_eq
161
      (translate_ident x)
162
      (List.map (fun (t, h) -> t, [translate_act (y, h)]) hl)
163
  | _ ->
164
    mk_assign ~lustre_eq y (translate_expr expr)
176 165

  
177 166
(* Datastructure updated while visiting equations *)
178 167
type machine_ctx = {
179
  m: VSet.t; (* Memories *)
168
  (* Memories *)
169
  m: VSet.t;
170
  (* Reset instructions *)
180 171
  si: instr_t list;
181
  j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
172
  (* Instances *)
173
  j: (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;
174
  (* Step instructions *)
182 175
  s: instr_t list;
176
  (* Memory pack spec *)
177
  mp: mc_formula_t list;
178
  (* Clocked spec *)
179
  c: mc_formula_t IMap.t;
180
  (* Transition spec *)
181
  t: mc_formula_t list;
183 182
}
184 183

  
185
let ctx_init = { m = VSet.empty; (* memories *)
186
                 si = []; (* init instr *)
187
                 j = Utils.IMap.empty;
188
                 s = [] }
184
let ctx_init = {
185
  m = VSet.empty;
186
  si = [];
187
  j = IMap.empty;
188
  s = [];
189
  mp = [];
190
  c = IMap.empty;
191
  t = []
192
}
189 193

  
190 194
(****************************************************************)
191 195
(* Main function to translate equations into this machine context we
192 196
   are building *) 
193 197
(****************************************************************)
194 198

  
199
let mk_control id vs v l inst =
200
  mkinstr
201
    (Imply (mk_clocked_on id vs, inst.instr_spec))
202
    (MBranch (v, [l, [inst]]))
203

  
204
let control_on_clock env ctx ck inst =
205
  let rec aux (ck_ids, vs, ctx, inst as acc) ck =
206
    match (Clocks.repr ck).cdesc with
207
    | Con (ck, cr, l) ->
208
      let id = Clocks.const_of_carrier cr in
209
      let v = translate_ident env id in
210
      let ck_ids' = String.concat "_" ck_ids in
211
      let id' = id ^ "_" ^ ck_ids' in
212
      let ck_spec = mk_condition v l in
213
      aux (id :: ck_ids,
214
           v :: vs,
215
           { ctx
216
             with c = IMap.add id ck_spec
217
                      (IMap.add id'
218
                         (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
219
           },
220
           mk_control id' (v :: vs) v l inst) ck
221
    | _ -> acc
222
  in
223
  let _, _, ctx, inst = aux ([], [], ctx, inst) ck in
224
  ctx, inst
225

  
226
let reset_instance env i r c =
227
  match r with
228
  | Some r ->
229
    [snd (control_on_clock env ctx_init c
230
            (mk_conditional
231
               (translate_guard env r)
232
               [mkinstr True (MReset i)]
233
               [mkinstr True (MNoReset i)]))]
234
  | None -> []
195 235

  
196 236

  
197 237
let translate_eq env ctx eq =
198 238
  let translate_expr = translate_expr env in
199 239
  let translate_act = translate_act env in
200
  let control_on_clock = control_on_clock env in
240
  let control_on_clock ck inst =
241
    let ctx, ins = control_on_clock env ctx ck inst in
242
    { ctx with s = ins :: ctx.s }
243
  in
201 244
  let reset_instance = reset_instance env in
202
  let mkinstr' = mkinstr ~lustre_eq:eq in
245
  let mkinstr' = mkinstr ~lustre_eq:eq True in
203 246
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
204 247
    control_on_clock ck (mkinstr' instr) in
205 248

  
......
211 254
    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
212 255
    let c1 = translate_expr e1 in
213 256
    let c2 = translate_expr e2 in
257
    let ctx = ctl (MStep ([var_x], o, [c1;c2])) in
214 258
    { ctx with
215
      si = mkinstr (MReset o) :: ctx.si;
216
      j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
217
      s = ctl (MStep ([var_x], o, [c1;c2])) :: ctx.s
259
      si = mkinstr True (MReset o) :: ctx.si;
260
      j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
218 261
    }
219 262
  | [x], Expr_pre e1 when env.is_local x    ->
220 263
    let var_x = env.get_var x in
264
    let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in
221 265
    { ctx with
222 266
      m = VSet.add var_x ctx.m;
223
      s = ctl (MStateAssign (var_x, translate_expr e1)) :: ctx.s
224 267
    }
225 268
  | [x], Expr_fby (e1, e2) when env.is_local x ->
226 269
    let var_x = env.get_var x in
270
    let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in
227 271
    { ctx with
228 272
      m = VSet.add var_x ctx.m;
229 273
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
230
      s = ctl (MStateAssign (var_x, translate_expr e2)) :: ctx.s
231 274
    }
232 275
  | p, Expr_appl (f, arg, r)
233 276
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
......
241 284
        el [eq.eq_rhs.expr_clock] in
242 285
    let call_ck = Clock_calculus.compute_root_clock
243 286
        (Clock_predef.ck_tuple env_cks) in
287
    let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in
244 288
    (*Clocks.new_var true in
245 289
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
246 290
      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;*)
247 291
    { ctx with
248 292
      si = if Stateless.check_node node_f
249
        then ctx.si else mkinstr (MReset o) :: ctx.si;
250
      j = Utils.IMap.add o call_f ctx.j;
293
        then ctx.si else mkinstr True (MReset o) :: ctx.si;
294
      j = IMap.add o call_f ctx.j;
251 295
      s = (if Stateless.check_node node_f
252
           then [] else reset_instance o r call_ck)
253
          @ ctl ~ck:call_ck (MStep (var_p, o, vl))
254
          :: ctx.s
296
           then []
297
           else reset_instance o r call_ck)
298
          @ ctx.s
255 299
    }
256 300
  | [x], _ ->
257 301
    let var_x = env.get_var x in
258
    { ctx with
259
      s = control_on_clock eq.eq_rhs.expr_clock
260
          (translate_act (var_x, eq.eq_rhs))
261
          :: ctx.s
262
      }
302
    control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs))
263 303
  | _ ->
264 304
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
265 305
      Printers.pp_node_eq eq;
......
270 310
      if vdecl.var_dec_const
271 311
      then
272 312
        { eq_lhs = [vdecl.var_id];
273
          eq_rhs = Utils.desome vdecl.var_dec_value;
313
          eq_rhs = desome vdecl.var_dec_value;
274 314
          eq_loc = vdecl.var_loc
275 315
        } :: eqs
276 316
      else eqs)
......
326 366
  let ctx0 = translate_eqs env ctx_init constant_eqs in
327 367
  assert (VSet.is_empty ctx0.m);
328 368
  assert (ctx0.si = []);
329
  assert (Utils.IMap.is_empty ctx0.j);
369
  assert (IMap.is_empty ctx0.j);
330 370

  
331 371
  (* Compute ctx for all eqs *)
332 372
  let ctx = translate_eqs env ctx_init sorted_eqs in
......
371 411
    let l = VSet.elements (VSet.diff locals ctx.m) in
372 412
    List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
373 413
  in
374
  let mmap = Utils.IMap.bindings ctx.j in
414
  let mmap = IMap.bindings ctx.j in
375 415
  {
376 416
    mname = nd;
377 417
    mmemory = VSet.elements ctx.m;
......
417 457
    List.map
418 458
      (fun decl ->
419 459
         let node = node_of_top decl in
420
         let sch = Utils.IMap.find node.node_id node_schs in
460
         let sch = IMap.find node.node_id node_schs in
421 461
         translate_decl node sch
422 462
      ) nodes
423 463
  in

Also available in: Unified diff