Project

General

Profile

Revision 3b2bd83d src/machine_code.ml

View differences:

src/machine_code.ml
21 21

  
22 22
module ISet = Set.Make(OrdVarDecl)
23 23

  
24
type value_t =
25
  | Cst of constant
26
  | LocalVar of var_decl
27
  | StateVar of var_decl
28
  | Fun of ident * value_t list
29
  | Array of value_t list
30
  | Access of value_t * value_t
31
  | Power of value_t * value_t
32

  
33
type instr_t =
34
  | MLocalAssign of var_decl * value_t
35
  | MStateAssign of var_decl * value_t
36
  | MReset of ident
37
  | MStep of var_decl list * ident * value_t list
38
  | MBranch of value_t * (label * instr_t list) list
39

  
40 24
let rec pp_val fmt v =
41
  match v with
42
    | Cst c         -> Printers.pp_const fmt c
25
  match v.value_desc with
26
    | Cst c         -> Printers.pp_const fmt c 
43 27
    | LocalVar v    -> Format.pp_print_string fmt v.var_id
44 28
    | StateVar v    -> Format.pp_print_string fmt v.var_id
45 29
    | Array vl      -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val)  vl
......
52 36
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
53 37
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
54 38
    | MReset i           -> Format.fprintf fmt "reset %s" i
39
    | MNoReset i         -> Format.fprintf fmt "noreset %s" i
55 40
    | MStep (il, i, vl)  ->
56 41
      Format.fprintf fmt "%a = %s (%a)"
57 42
	(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
......
61 46
      Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
62 47
	pp_val g
63 48
	(Utils.fprintf_list ~sep:"@," pp_branch) hl
49
    | MComment s -> Format.pp_print_string fmt s
64 50

  
65 51
and pp_branch fmt (t, h) =
66 52
  Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h
......
119 105
    (fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
120 106
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
121 107

  
108
let rec is_const_value v =
109
  match v.value_desc with
110
  | Cst _          -> true
111
  | Fun (id, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
112
  | _              -> false
113

  
122 114
(* Returns the declared stateless status and the computed one. *)
123 115
let get_stateless_status m =
124 116
 (m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless)
......
144 136
    var_dec_const = false;
145 137
    var_dec_value = None;
146 138
    var_type =  typ;
147
    var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
139
    var_clock = Clocks.new_ck Clocks.Cvar true;
148 140
    var_loc = Location.dummy_loc
149 141
  }
150 142

  
......
177 169
    top_decl_loc = Location.dummy_loc
178 170
  }
179 171

  
172
let mk_val v t = { value_desc = v; 
173
		   value_type = t; 
174
		   value_annot = None }
175

  
180 176
let arrow_machine =
181 177
  let state = "_first" in
182 178
  let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in
183 179
  let var_input1 = List.nth arrow_desc.node_inputs 0 in
184 180
  let var_input2 = List.nth arrow_desc.node_inputs 1 in
185 181
  let var_output = List.nth arrow_desc.node_outputs 0 in
182
  let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
183
  let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *)
186 184
  {
187 185
    mname = arrow_desc;
188 186
    mmemory = [var_state];
189 187
    mcalls = [];
190 188
    minstances = [];
191
    minit = [MStateAssign(var_state, Cst (const_of_bool true))];
192
    mconst = [];
189
    minit = [MStateAssign(var_state, cst true)];
193 190
    mstatic = [];
191
    mconst = [];
194 192
    mstep = {
195 193
      step_inputs = arrow_desc.node_inputs;
196 194
      step_outputs = arrow_desc.node_outputs;
197 195
      step_locals = [];
198 196
      step_checks = [];
199
      step_instrs = [conditional (StateVar var_state)
200
			         [MStateAssign(var_state, Cst (const_of_bool false));
201
                                  MLocalAssign(var_output, LocalVar var_input1)]
202
                                 [MLocalAssign(var_output, LocalVar var_input2)] ];
197
      step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool)
198
			         [MStateAssign(var_state, cst false);
199
                                  MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)]
200
                                 [MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)] ];
201
      step_asserts = [];
202
    };
203
    mspec = None;
204
    mannot = [];
205
  }
206

  
207
let empty_desc =
208
  {
209
    node_id = arrow_id;
210
    node_type = Types.bottom;
211
    node_clock = Clocks.bottom;
212
    node_inputs= [];
213
    node_outputs= [];
214
    node_locals= [];
215
    node_gencalls = [];
216
    node_checks = [];
217
    node_asserts = [];
218
    node_stmts= [];
219
    node_dec_stateless = true;
220
    node_stateless = Some true;
221
    node_spec = None;
222
    node_annot = [];  }
223

  
224
let empty_machine =
225
  {
226
    mname = empty_desc;
227
    mmemory = [];
228
    mcalls = [];
229
    minstances = [];
230
    minit = [];
231
    mstatic = [];
232
    mconst = [];
233
    mstep = {
234
      step_inputs = [];
235
      step_outputs = [];
236
      step_locals = [];
237
      step_checks = [];
238
      step_instrs = [];
203 239
      step_asserts = [];
204 240
    };
205 241
    mspec = None;
......
233 269
  try (* id is a node var *)
234 270
    let var_id = get_node_var id node in
235 271
    if ISet.exists (fun v -> v.var_id = id) m
236
    then StateVar var_id
237
    else LocalVar var_id
272
    then mk_val (StateVar var_id) var_id.var_type
273
    else mk_val (LocalVar var_id) var_id.var_type
238 274
  with Not_found ->
239 275
    try (* id is a constant *)
240
      LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)))
276
      let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in
277
      mk_val (LocalVar vdecl) vdecl.var_type
241 278
    with Not_found ->
242 279
      (* id is a tag *)
243
      Cst (Const_tag id)
280
      (* DONE construire une liste des enum declar├ęs et alors chercher dedans la liste
281
	 qui contient id *)
282
      try
283
        let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
284
        mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
285
      with Not_found -> (Format.eprintf "internal error: Machine_code.translate_ident %s" id;
286
                         assert false)
244 287

  
245 288
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =
246 289
 match (Clocks.repr ck).cdesc with
......
292 335
  | "C" -> specialize_to_c expr
293 336
  | _   -> expr
294 337

  
295
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =
338
let rec translate_expr node ((m, si, j, d, s) as args) expr =
296 339
  let expr = specialize_op expr in
297
 match expr.expr_desc with
298
 | Expr_const v                     -> Cst v
299
 | Expr_ident x                     -> translate_ident node args x
300
 | Expr_array el                    -> Array (List.map (translate_expr node args) el)
301
 | Expr_access (t, i)               -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
302
 | Expr_power  (e, n)               -> Power  (translate_expr node args e, translate_expr node args (expr_of_dimension n))
303
 | Expr_tuple _
304
 | Expr_arrow _
305
 | Expr_fby _
306
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
307
 | Expr_when    (e1, _, _)          -> translate_expr node args e1
308
 | Expr_merge   (x, _)              -> raise NormalizationError
309
 | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
310
   let nd = node_from_name id in
311
   Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
312
 | Expr_ite (g,t,e) -> (
313
   (* special treatment depending on the active backend. For horn backend, ite
314
      are preserved in expression. While they are removed for C or Java
315
      backends. *)
316
   match !Options.output with
317
   | "horn" ->
318
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
319
   | ("C" | "java") when ite ->
320
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
321
   | _ ->
322
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
323
 )
324
 | _                   -> raise NormalizationError
340
  let value_desc = 
341
    match expr.expr_desc with
342
    | Expr_const v                     -> Cst v
343
    | Expr_ident x                     -> (translate_ident node args x).value_desc
344
    | Expr_array el                    -> Array (List.map (translate_expr node args) el)
345
    | Expr_access (t, i)               -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
346
    | Expr_power  (e, n)               -> Power  (translate_expr node args e, translate_expr node args (expr_of_dimension n))
347
    | Expr_tuple _
348
    | Expr_arrow _ 
349
    | Expr_fby _
350
    | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
351
    | Expr_when    (e1, _, _)          -> (translate_expr node args e1).value_desc
352
    | Expr_merge   (x, _)              -> raise NormalizationError
353
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
354
      let nd = node_from_name id in
355
      Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
356
    (*| Expr_ite (g,t,e) -> (
357
      (* special treatment depending on the active backend. For horn backend, ite
358
	 are preserved in expression. While they are removed for C or Java
359
	 backends. *)
360
      match !Options.output with | "horn" -> 
361
	Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
362
      | "C" | "java" | _ -> 
363
	(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
364
    )*)
365
    | _                   -> raise NormalizationError
366
  in
367
  mk_val value_desc expr.expr_type
325 368

  
326 369
let translate_guard node args expr =
327 370
  match expr.expr_desc with
......
331 374
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
332 375
  match expr.expr_desc with
333 376
  | Expr_ite   (c, t, e) -> let g = translate_guard node args c in
334
			    conditional g [translate_act node args (y, t)]
377
			    conditional g
378
                              [translate_act node args (y, t)]
335 379
                              [translate_act node args (y, e)]
336
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x, List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
337
  | _                    ->
338
    MLocalAssign (y, translate_expr node args expr)
380
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x,
381
                                     List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
382
  | _                    -> MLocalAssign (y, translate_expr node args expr)
339 383

  
340 384
let reset_instance node args i r c =
341 385
  match r with
342 386
  | None        -> []
343 387
  | Some r      -> let g = translate_guard node args r in
344
                   [control_on_clock node args c (conditional g [MReset i] [])]
388
                   [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
345 389

  
346 390
let translate_eq node ((m, si, j, d, s) as args) eq =
347 391
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
......
371 415
     d,
372 416
     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
373 417

  
374
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) ->
418
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
375 419
    let var_p = List.map (fun v -> get_node_var v node) p in
376 420
    let el = expr_list_of_expr arg in
377 421
    let vl = List.map (translate_expr node args) el in
......
393 437
      then []
394 438
      else reset_instance node args o r call_ck) @
395 439
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
396

  
440
(*
397 441
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
398 442
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
399 443
      backends. *)
......
409 453
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
410 454
    )
411 455

  
456
*)
412 457
  | [x], _                                       -> (
413 458
    let var_x = get_node_var x node in
414 459
    (m, si, j, d,
......
421 466
  )
422 467
  | _                                            ->
423 468
    begin
424
      Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq;
469
      Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;
425 470
      assert false
426 471
    end
427 472

  
......
444 489
   to the computed schedule [sch]
445 490
*)
446 491
let sort_equations_from_schedule nd sch =
447
(*Format.eprintf "%s schedule: %a@."
448
		 nd.node_id
449
		 (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)
492
  (* Format.eprintf "%s schedule: %a@." *)
493
  (* 		 nd.node_id *)
494
  (* 		 (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *)
450 495
  let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
451 496
  let eqs_rev, remainder =
452 497
    List.fold_left
......
515 560
	(* special treatment depending on the active backend. For horn backend,
516 561
	   common branches are not merged while they are in C or Java
517 562
	   backends. *)
518
	match !Options.output with
563
	(*match !Options.output with
519 564
	| "horn" -> s
520
	| "C" | "java" | _ -> join_guards_list s
565
	| "C" | "java" | _ ->*) join_guards_list s
521 566
      );
522 567
      step_asserts =
523 568
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
......
554 599
  with Not_found -> assert false
555 600

  
556 601

  
557
let value_of_ident m id =
602
let value_of_ident loc m id =
558 603
  (* is is a state var *)
559 604
  try
560
    StateVar (List.find (fun v -> v.var_id = id) m.mmemory)
605
    let v = List.find (fun v -> v.var_id = id) m.mmemory
606
    in mk_val (StateVar v) v.var_type 
561 607
  with Not_found ->
562
  try (* id is a node var *)
563
    LocalVar (get_node_var id m.mname)
608
    try (* id is a node var *)
609
      let v = get_node_var id m.mname
610
      in mk_val (LocalVar v) v.var_type
564 611
  with Not_found ->
565 612
    try (* id is a constant *)
566
      LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)))
613
      let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))
614
      in mk_val (LocalVar c) c.var_type
567 615
    with Not_found ->
568 616
      (* id is a tag *)
569
      Cst (Const_tag id)
617
      let t = Const_tag id
618
      in mk_val (Cst t) (Typing.type_const loc t)
619

  
620
(* type of internal fun used in dimension expression *)
621
let type_of_value_appl f args =
622
  if List.mem f Basic_library.arith_funs
623
  then (List.hd args).value_type
624
  else Type_predef.type_bool
570 625

  
571 626
let rec value_of_dimension m dim =
572 627
  match dim.Dimension.dim_desc with
573
  | Dimension.Dbool b         -> Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))
574
  | Dimension.Dint i          -> Cst (Const_int i)
575
  | Dimension.Dident v        -> value_of_ident m v
576
  | Dimension.Dappl (f, args) -> Fun (f, List.map (value_of_dimension m) args)
577
  | Dimension.Dite (i, t, e)  -> Fun ("ite", List.map (value_of_dimension m) [i; t; e])
628
  | Dimension.Dbool b         ->
629
     mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool
630
  | Dimension.Dint i          ->
631
     mk_val (Cst (Const_int i)) Type_predef.type_int
632
  | Dimension.Dident v        -> value_of_ident dim.Dimension.dim_loc m v
633
  | Dimension.Dappl (f, args) ->
634
     let vargs = List.map (value_of_dimension m) args
635
     in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) 
636
  | Dimension.Dite (i, t, e)  ->
637
     (match List.map (value_of_dimension m) [i; t; e] with
638
     | [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
639
     | _            -> assert false)
578 640
  | Dimension.Dlink dim'      -> value_of_dimension m dim'
579 641
  | _                         -> assert false
580 642

  
581 643
let rec dimension_of_value value =
582
  match value with
644
  match value.value_desc with
583 645
  | Cst (Const_tag t) when t = Corelang.tag_true  -> Dimension.mkdim_bool  Location.dummy_loc true
584 646
  | Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool  Location.dummy_loc false
585 647
  | Cst (Const_int i)                             -> Dimension.mkdim_int   Location.dummy_loc i

Also available in: Unified diff