Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by LĂ©lio Brun 7 months ago

work on spec generation almost done

View differences:

src/machine_code.ml
42 42
}
43 43

  
44 44

  
45
let build_env locals non_locals =
46
  let all = VSet.union locals non_locals in
47
  {
48
    is_local = (fun id -> VSet.exists (fun v -> v.var_id = id) locals);
49
    get_var = (fun id -> try VSet.get id all with Not_found ->
45
let build_env inputs locals outputs =
46
  let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in
47
  { is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals);
48
    get_var = (fun id -> try List.find (fun v -> v.var_id = id) all with Not_found ->
50 49
        (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
51 50
         *   id
52 51
         *   VSet.pp all; *)
......
64 63
  (* id is a var that shall be visible here , ie. in vars *)
65 64
  try
66 65
    let var_id = env.get_var id in
67
    mk_val (Var var_id) var_id.var_type
66
    vdecl_to_val var_id
68 67
  with Not_found ->
69 68

  
70 69
 (* id is a constant *)
......
72 71
    let vdecl = (Corelang.var_decl_of_const
73 72
                   (const_of_top (Hashtbl.find Corelang.consts_table id)))
74 73
    in
75
    mk_val (Var vdecl) vdecl.var_type
74
    vdecl_to_val vdecl
76 75
  with Not_found ->
77 76

  
78 77
   (* id is a tag, getting its type in the list of declared enums *)
79 78
  try
80
    let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
81
    mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
79
    id_to_tag id
82 80
  with Not_found ->
83 81
    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
84 82
    assert false
......
147 145
let rec translate_act env (y, expr) =
148 146
  let translate_act = translate_act env in
149 147
  let translate_guard = translate_guard env in
150
  let translate_ident = translate_ident env in
148
  (* let translate_ident = translate_ident env in *)
151 149
  let translate_expr = translate_expr env in
152 150
  let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
153 151
  match expr.expr_desc with
154 152
  | Expr_ite (c, t, e) ->
155
    mk_conditional ~lustre_eq
156
      (translate_guard c)
157
      [translate_act (y, t)]
158
      [translate_act (y, e)]
153
    let c = translate_guard c in
154
    let t, spec_t = translate_act (y, t) in
155
    let e, spec_e = translate_act (y, e) in
156
    mk_conditional ~lustre_eq c [t] [e],
157
    mk_conditional_tr c spec_t spec_e
159 158
  | Expr_merge (x, hl) ->
160
    mk_branch ~lustre_eq
161
      (translate_ident x)
162
      (List.map (fun (t, h) -> t, [translate_act (y, h)]) hl)
159
    let var_x = env.get_var x in
160
    let hl, spec_hl = List.(split (map (fun (t, h) ->
161
        let h, spec_h = translate_act (y, h) in
162
        (t, [h]), (t, spec_h))
163
        hl)) in
164
    mk_branch ~lustre_eq var_x hl,
165
    mk_branch_tr var_x spec_hl
163 166
  | _ ->
164
    mk_assign ~lustre_eq y (translate_expr expr)
167
    let e = translate_expr expr in
168
    mk_assign ~lustre_eq y e,
169
    mk_assign_tr y e
170

  
171
let get_memory env mems eq = match eq.eq_lhs, eq.eq_rhs.expr_desc with
172
  | ([x], Expr_pre _ | [x], Expr_fby _) when env.is_local x ->
173
    let var_x = env.get_var x in
174
    VSet.add var_x mems
175
  | _ -> mems
176

  
177
let get_memories env =
178
  List.fold_left (get_memory env) VSet.empty
165 179

  
166 180
(* Datastructure updated while visiting equations *)
167 181
type machine_ctx = {
168
  (* machine name *)
169
  id: ident;
170
  (* Memories *)
171
  m: VSet.t;
172 182
  (* Reset instructions *)
173 183
  si: instr_t list;
174 184
  (* Instances *)
......
177 187
  s: instr_t list;
178 188
  (* Memory pack spec *)
179 189
  mp: mc_formula_t list;
180
  (* Clocked spec *)
181
  c: mc_formula_t IMap.t;
182 190
  (* Transition spec *)
183
  t: mc_formula_t list;
191
  t: (var_decl list * var_decl list * var_decl list * mc_formula_t) list;
184 192
}
185 193

  
186
let ctx_init id = {
187
  id;
188
  m = VSet.empty;
194
let ctx_init = {
189 195
  si = [];
190 196
  j = IMap.empty;
191 197
  s = [];
192 198
  mp = [];
193
  c = IMap.empty;
194 199
  t = []
195 200
}
196 201

  
197
let ctx_dummy = ctx_init ""
198

  
199 202
(****************************************************************)
200 203
(* Main function to translate equations into this machine context we
201 204
   are building *) 
......
203 206

  
204 207
let mk_control v l inst =
205 208
  mkinstr
206
    True
207
    (* (Imply (mk_clocked_on id vs, inst.instr_spec)) *)
208
    (MBranch (v, [l, [inst]]))
209
    (MBranch (vdecl_to_val v, [l, [inst]]))
209 210

  
210
let control_on_clock env ctx ck spec inst =
211
  let rec aux (ck_ids, vs, ctx, spec, inst as acc) ck =
211
let control_on_clock env ck inst =
212
  let rec aux (fspec, inst as acc) ck =
212 213
    match (Clocks.repr ck).cdesc with
213 214
    | Con (ck, cr, l) ->
214 215
      let id = Clocks.const_of_carrier cr in
215
      let v = translate_ident env id in
216
      let ck_ids' = String.concat "_" ck_ids in
217
      let id' = id ^ "_" ^ ck_ids' in
218
      let ck_spec = mk_condition v l in
219
      aux (id :: ck_ids,
220
           v :: vs,
221
           { ctx with
222
             c = IMap.add id ck_spec
223
                 (IMap.add id' (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
224
           },
225
           Imply (mk_clocked_on id' (v :: vs), spec),
226
           mk_control v l inst) ck
216
      let v = env.get_var id in
217
      aux ((fun spec -> Imply (Equal (Var v, Tag l), fspec spec)),
218
           mk_control v l inst)
219
        ck
227 220
    | _ -> acc
228 221
  in
229
  let _, _, ctx, spec, inst = aux ([], [], ctx, spec, inst) ck in
230
  ctx, spec, inst
222
  let fspec, inst = aux ((fun spec -> spec), inst) ck in
223
  fspec, inst
231 224

  
232 225
let reset_instance env i r c =
233 226
  match r with
234 227
  | Some r ->
235
    let _, _, inst = control_on_clock env ctx_dummy c True
228
    let _, inst = control_on_clock env c
236 229
        (mk_conditional
237 230
           (translate_guard env r)
238
           [mkinstr True (MReset i)]
239
           [mkinstr True (MNoReset i)]) in
231
           [mkinstr (MSetReset i)]
232
           [mkinstr (MNoReset i)]) in
240 233
    [ inst ]
241 234
  | None -> []
242 235

  
243

  
244
let translate_eq env ctx i eq =
236
let translate_eq env ctx id inputs locals outputs i eq =
245 237
  let translate_expr = translate_expr env in
246 238
  let translate_act = translate_act env in
247
  let control_on_clock ck spec inst =
248
    let ctx, _spec, inst = control_on_clock env ctx ck spec inst in
239
  let locals_pi = Lustre_live.inter_live_i_with id (i-1) locals in
240
  let outputs_pi = Lustre_live.inter_live_i_with id (i-1) outputs in
241
  let locals_i = Lustre_live.inter_live_i_with id i locals in
242
  let outputs_i = Lustre_live.inter_live_i_with id i outputs in
243
  let pred_mp ctx a =
244
    And [mk_memory_pack ~i:(i-1) id; a] :: ctx.mp in
245
  let pred_t ctx a =
246
    (inputs, locals_i, outputs_i,
247
     Exists
248
       (Lustre_live.existential_vars id i eq (locals @ outputs),
249
        And [
250
          mk_transition ~i:(i-1) id
251
            (vdecls_to_vals inputs)
252
            (vdecls_to_vals locals_pi)
253
            (vdecls_to_vals outputs_pi);
254
          a
255
        ]))
256
    :: ctx.t in
257
  let control_on_clock ck inst spec_mp spec_t =
258
    let fspec, inst = control_on_clock env ck inst in
249 259
    { ctx with
250 260
      s = { inst with
251
            instr_spec = mk_transition ~i ctx.id [] } :: ctx.s }
261
            instr_spec = [
262
              mk_memory_pack ~i id;
263
              mk_transition ~i id
264
                (vdecls_to_vals inputs)
265
                (vdecls_to_vals locals_i)
266
                (vdecls_to_vals outputs_i)
267
            ] }
268
          :: ctx.s;
269
      mp = pred_mp ctx spec_mp;
270
      t = pred_t ctx (fspec spec_t);
271
    }
252 272
  in
253 273
  let reset_instance = reset_instance env in
254
  let mkinstr' = mkinstr ~lustre_eq:eq True in
255
  let ctl ?(ck=eq.eq_rhs.expr_clock) spec instr =
256
    control_on_clock ck spec (mkinstr' instr) in
274
  let mkinstr' = mkinstr ~lustre_eq:eq in
275
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr spec_mp spec_t =
276
    control_on_clock ck (mkinstr' instr) spec_mp spec_t in
257 277

  
258 278
  (* Format.eprintf "translate_eq %a with clock %a@." 
259 279
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
......
261 281
  | [x], Expr_arrow (e1, e2)                     ->
262 282
    let var_x = env.get_var x in
263 283
    let td = Arrow.arrow_top_decl () in
264
    let o = new_instance td eq.eq_rhs.expr_tag in
284
    let inst = new_instance td eq.eq_rhs.expr_tag in
265 285
    let c1 = translate_expr e1 in
266 286
    let c2 = translate_expr e2 in
287
    assert (c1.value_desc = Cst (Const_tag "true"));
288
    assert (c2.value_desc = Cst (Const_tag "false"));
267 289
    let ctx = ctl
268
        (mk_transition (node_name td) [])
269
        (MStep ([var_x], o, [c1;c2])) in
290
        (MStep ([var_x], inst, [c1; c2]))
291
        (mk_memory_pack ~inst (node_name td))
292
        (mk_transition ~inst (node_name td) [] [] [vdecl_to_val var_x])
293
    in
270 294
    { ctx with
271
      si = mkinstr True (MReset o) :: ctx.si;
272
      j = IMap.add o (td, []) ctx.j;
295
      si = mkinstr (MSetReset inst) :: ctx.si;
296
      j = IMap.add inst (td, []) ctx.j;
273 297
    }
274 298

  
275
  | [x], Expr_pre e1 when env.is_local x    ->
299
  | [x], Expr_pre e when env.is_local x    ->
276 300
    let var_x = env.get_var x in
277
    let ctx = ctl
278
        True
279
        (MStateAssign (var_x, translate_expr e1)) in
280
    { ctx with
281
      m = VSet.add var_x ctx.m;
282
    }
301
    let e = translate_expr e in
302
    ctl
303
      (MStateAssign (var_x, e))
304
      (mk_state_variable_pack var_x)
305
      (mk_state_assign_tr var_x e)
283 306

  
284 307
  | [x], Expr_fby (e1, e2) when env.is_local x ->
285 308
    let var_x = env.get_var x in
309
    let e2 = translate_expr e2 in
286 310
    let ctx = ctl
287
        True
288
        (MStateAssign (var_x, translate_expr e2)) in
311
        (MStateAssign (var_x, e2))
312
        (mk_state_variable_pack var_x)
313
        (mk_state_assign_tr var_x e2)
314
    in
289 315
    { ctx with
290
      m = VSet.add var_x ctx.m;
291 316
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
292 317
    }
293 318

  
......
298 323
    let vl = List.map translate_expr el in
299 324
    let node_f = node_from_name f in
300 325
    let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
301
    let o = new_instance node_f eq.eq_rhs.expr_tag in
326
    let inst = new_instance node_f eq.eq_rhs.expr_tag in
302 327
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks)
303 328
        el [eq.eq_rhs.expr_clock] in
304 329
    let call_ck = Clock_calculus.compute_root_clock
305 330
        (Clock_predef.ck_tuple env_cks) in
306 331
    let ctx = ctl
307 332
        ~ck:call_ck
308
        True
309
        (MStep (var_p, o, vl)) in
333
        (MStep (var_p, inst, vl))
334
        (mk_memory_pack ~inst (node_name node_f))
335
        (mk_transition ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
336
    in
310 337
    (*Clocks.new_var true in
311 338
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
312 339
      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;*)
313 340
    { ctx with
314 341
      si = if Stateless.check_node node_f
315
        then ctx.si else mkinstr True (MReset o) :: ctx.si;
316
      j = IMap.add o call_f ctx.j;
342
        then ctx.si else mkinstr (MSetReset inst) :: ctx.si;
343
      j = IMap.add inst call_f ctx.j;
317 344
      s = (if Stateless.check_node node_f
318 345
           then []
319
           else reset_instance o r call_ck)
320
          @ ctx.s
346
           else reset_instance inst r call_ck)
347
          @ ctx.s;
321 348
    }
322 349

  
323 350
  | [x], _ ->
324 351
    let var_x = env.get_var x in
325
    control_on_clock eq.eq_rhs.expr_clock True (translate_act (var_x, eq.eq_rhs))
352
    let instr, spec = translate_act (var_x, eq.eq_rhs) in
353
    control_on_clock eq.eq_rhs.expr_clock instr True spec
326 354

  
327 355
  | _ ->
328 356
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
......
330 358
    assert false
331 359

  
332 360
let constant_equations locals =
333
  VSet.fold (fun vdecl eqs ->
361
  List.fold_left (fun eqs vdecl ->
334 362
      if vdecl.var_dec_const
335 363
      then
336 364
        { eq_lhs = [vdecl.var_id];
......
338 366
          eq_loc = vdecl.var_loc
339 367
        } :: eqs
340 368
      else eqs)
341
    locals []
369
    [] locals
342 370

  
343
let translate_eqs env ctx eqs =
371
let translate_eqs env ctx id inputs locals outputs eqs =
344 372
  List.fold_right (fun eq (ctx, i) ->
345
      let ctx = translate_eq env ctx i eq in
373
      let ctx = translate_eq env ctx id inputs locals outputs i eq in
346 374
      ctx, i - 1)
347 375
    eqs (ctx, List.length eqs)
348 376
  |> fst
......
385 413
    in
386 414
    vars, eql, assertl
387 415

  
388
let translate_core nid sorted_eqs locals other_vars =
416
let translate_core env nid sorted_eqs inputs locals outputs =
389 417
  let constant_eqs = constant_equations locals in
390 418

  
391
  let env = build_env locals other_vars  in
392

  
393 419
  (* Compute constants' instructions  *)
394
  let ctx0 = translate_eqs env (ctx_init nid) constant_eqs in
395
  assert (VSet.is_empty ctx0.m);
420
  let ctx0 = translate_eqs env ctx_init nid inputs locals outputs constant_eqs in
396 421
  assert (ctx0.si = []);
397 422
  assert (IMap.is_empty ctx0.j);
398 423

  
399 424
  (* Compute ctx for all eqs *)
400
  let ctx = translate_eqs env (ctx_init nid) sorted_eqs in
425
  let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in
401 426

  
402 427
  ctx, ctx0.s
403 428

  
429
let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int
430

  
431
let memory_pack_0 nd =
432
  {
433
    mpname = nd;
434
    mpindex = Some 0;
435
    mpformula = And [StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero)]
436
  }
437

  
438
let memory_pack_toplevel nd i =
439
  {
440
    mpname = nd;
441
    mpindex = None;
442
    mpformula = Ternary (Memory ResetFlag,
443
                         StateVarPack ResetFlag,
444
                         mk_memory_pack ~i nd.node_id)
445
  }
446

  
447
let transition_0 nd =
448
  {
449
    tname = nd;
450
    tindex = Some 0;
451
    tinputs = nd.node_inputs;
452
    tlocals = [];
453
    toutputs = [];
454
    tformula = True;
455
  }
456

  
457
let transition_toplevel nd i =
458
  {
459
    tname = nd;
460
    tindex = None;
461
    tinputs = nd.node_inputs;
462
    tlocals = [];
463
    toutputs = nd.node_outputs;
464
    tformula = ExistsMem (Predicate (ResetCleared nd.node_id),
465
                          mk_transition nd.node_id ~i
466
                            (vdecls_to_vals (nd.node_inputs))
467
                            []
468
                            (vdecls_to_vals nd.node_outputs));
469
  }
404 470

  
405 471
let translate_decl nd sch =
406 472
  (* Format.eprintf "Translating node %s@." nd.node_id; *)
......
413 479
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
414 480

  
415 481
  (* Build the env: variables visible in the current scope *)
416
  let locals_list = nd.node_locals @ new_locals in
417
  let locals = VSet.of_list locals_list in
418
  let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in
419
  let env = build_env locals inout_vars  in 
482
  let locals = nd.node_locals @ new_locals in
483
  (* let locals = VSet.of_list locals_list in *)
484
  (* let inout_vars = nd.node_inputs @ nd.node_outputs in *)
485
  let env = build_env nd.node_inputs locals nd.node_outputs in
420 486

  
421 487
  (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
422 488

  
......
430 496
   *   VSet.pp inout_vars
431 497
   * ; *)
432 498

  
433
  let ctx, ctx0_s = translate_core
434
      nd.node_id (assert_instrs@sorted_eqs) locals inout_vars in
499
  let equations = assert_instrs @ sorted_eqs in
500
  let mems = get_memories env equations in
501
  (* Removing computed memories from locals. We also removed unused variables. *)
502
  let locals = List.filter
503
      (fun v -> not (VSet.mem v mems) && not (List.mem v.var_id unused)) locals in
504
  (* Compute live sets for spec *)
505
  Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations;
506

  
507
  (* Translate equations *)
508
  let ctx, ctx0_s = translate_core env nd.node_id equations
509
     nd.node_inputs locals nd.node_outputs in
435 510

  
436 511
  (* Format.eprintf "ok4@.@?"; *)
437 512

  
438
  (* Removing computed memories from locals. We also removed unused variables. *)
439
  let updated_locals =
440
    let l = VSet.elements (VSet.diff locals ctx.m) in
441
    List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
442
  in
513
  (* Build the machine *)
443 514
  let mmap = IMap.bindings ctx.j in
515
  let mmemory_packs =
516
    memory_pack_0 nd
517
    :: List.mapi (fun i f ->
518
      {
519
        mpname = nd;
520
        mpindex = Some (i + 1);
521
        mpformula = red f
522
      }) ctx.mp
523
    @ [memory_pack_toplevel nd (List.length ctx.mp)]
524
  in
525
  let mtransitions =
526
    transition_0 nd
527
    :: List.mapi (fun i (tinputs, tlocals, toutputs, f) ->
528
        {
529
          tname = nd;
530
          tindex = Some (i + 1);
531
          tinputs;
532
          tlocals;
533
          toutputs;
534
          tformula = red f;
535
        }) ctx.t
536
    @ [transition_toplevel nd (List.length ctx.t)]
537
  in
538
  let clear_reset = mkinstr ~instr_spec:[
539
      mk_memory_pack ~i:0 nd.node_id;
540
      mk_transition ~i:0 nd.node_id
541
        (vdecls_to_vals nd.node_inputs)
542
        []
543
        []] MClearReset in
444 544
  {
445 545
    mname = nd;
446
    mmemory = VSet.elements ctx.m;
546
    mmemory = VSet.elements mems;
447 547
    mcalls = mmap;
448 548
    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
449 549
    minit = ctx.si;
......
452 552
    mstep = {
453 553
      step_inputs = nd.node_inputs;
454 554
      step_outputs = nd.node_outputs;
455
      step_locals = updated_locals;
555
      step_locals = locals;
456 556
      step_checks = List.map (fun d -> d.Dimension.dim_loc,
457 557
                                       translate_expr env
458 558
                                         (expr_of_dimension d))
459 559
          nd.node_checks;
460
      step_instrs = (
461
        (* special treatment depending on the active backend. For horn backend,
462
           common branches are not merged while they are in C or Java
463
           backends. *)
464
        if !Backends.join_guards then
465
          join_guards_list ctx.s
466
        else
467
          ctx.s
468
      );
560
      step_instrs = clear_reset ::
561
                    (* special treatment depending on the active backend. For horn backend,
562
                       common branches are not merged while they are in C or Java
563
                       backends. *)
564
                    (if !Backends.join_guards then
565
                       join_guards_list ctx.s
566
                     else
567
                       ctx.s);
469 568
      step_asserts = List.map (translate_expr env) nd_node_asserts;
470 569
    };
471 570

  
......
474 573
       cocospec node, or the current one is a cocospec node. Contract do
475 574
       not contain any statement or import. *)
476 575

  
477
    mspec = { mnode_spec = nd.node_spec; mtransitions = [] };
576
    mspec = { mnode_spec = nd.node_spec; mtransitions; mmemory_packs };
478 577
    mannot = nd.node_annot;
479 578
    msch = Some sch;
480 579
  }

Also available in: Unified diff