Project

General

Profile

« Previous | Next » 

Revision 0406ab94

Added by LĂ©lio Brun 7 months ago

implement optimization on spec: IT WORKS

View differences:

src/optimize_machine.ml
11 11

  
12 12
open Utils
13 13
open Lustre_types
14
open Spec_types
14 15
open Machine_code_types
15 16
open Corelang
16 17
open Causality
......
597 598
  | Power (v, n) ->
598 599
    { value with value_desc = Power (value_replace_var fvar v, n) }
599 600

  
600
let rec instr_replace_var fvar instr cont =
601
  match get_instr_desc instr with
602
  | MLocalAssign (i, v) ->
603
    instr_cons
604
      (update_instr_desc instr
605
         (MLocalAssign (fvar i, value_replace_var fvar v)))
606
      cont
607
  | MStateAssign (i, v) ->
608
    instr_cons
609
      (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v)))
610
      cont
611
  | MSetReset _
612
  | MNoReset _
613
  | MClearReset
614
  | MResetAssign _
615
  | MSpec _
616
  | MComment _ ->
617
    instr_cons instr cont
618
  | MStep (il, i, vl) ->
619
    instr_cons
620
      (update_instr_desc instr
621
         (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)))
622
      cont
623
  | MBranch (g, hl) ->
624
    instr_cons
625
      (update_instr_desc instr
626
         (MBranch
627
            ( value_replace_var fvar g,
628
              List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )))
629
      cont
601
let expr_spec_replace :
602
    type a.
603
    (var_decl -> var_decl) ->
604
    (value_t, a) expression_t ->
605
    (value_t, a) expression_t =
606
 fun fvar -> function
607
  | Val v ->
608
    Val (value_replace_var fvar v)
609
  | Var v ->
610
    Var (fvar v)
611
  | e ->
612
    e
613

  
614
let predicate_spec_replace fvar = function
615
  | Transition (f, inst, i, vars, r, mems, insts) ->
616
    Transition
617
      (f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)
618
  | p ->
619
    p
620

  
621
let rec instr_spec_replace fvar =
622
  let aux instr = instr_spec_replace fvar instr in
623
  function
624
  | Equal (e1, e2) ->
625
    Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
626
  | And f ->
627
    And (List.map aux f)
628
  | Or f ->
629
    Or (List.map aux f)
630
  | Imply (a, b) ->
631
    Imply (aux a, aux b)
632
  | Exists (xs, a) ->
633
    let fvar v = if List.mem v xs then v else fvar v in
634
    Exists (xs, instr_spec_replace fvar a)
635
  | Forall (xs, a) ->
636
    let fvar v = if List.mem v xs then v else fvar v in
637
    Forall (xs, instr_spec_replace fvar a)
638
  | Ternary (e, a, b) ->
639
    Ternary (expr_spec_replace fvar e, aux a, aux b)
640
  | Predicate p ->
641
    Predicate (predicate_spec_replace fvar p)
642
  | ExistsMem (f, a, b) ->
643
    ExistsMem (f, aux a, aux b)
644
  | f ->
645
    f
646

  
647
let rec instr_replace_var fvar instr =
648
  let instr_desc =
649
    match instr.instr_desc with
650
    | MLocalAssign (i, v) ->
651
      MLocalAssign (fvar i, value_replace_var fvar v)
652
    | MStateAssign (i, v) ->
653
      MStateAssign (i, value_replace_var fvar v)
654
    | MStep (il, i, vl) ->
655
      MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)
656
    | MBranch (g, hl) ->
657
      MBranch
658
        ( value_replace_var fvar g,
659
          List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )
660
    | MSetReset _
661
    | MNoReset _
662
    | MClearReset
663
    | MResetAssign _
664
    | MSpec _
665
    | MComment _ ->
666
      instr.instr_desc
667
  in
668
  let instr_spec = List.map (instr_spec_replace fvar) instr.instr_spec in
669
  instr_cons { instr with instr_desc; instr_spec }
630 670

  
631 671
and instrs_replace_var fvar instrs cont =
632 672
  List.fold_right (instr_replace_var fvar) instrs cont
......
657 697
let machine_replace_variables fvar m =
658 698
  { m with mstep = step_replace_var fvar m.mstep }
659 699

  
660
let machine_reuse_variables m reuse =
700
let machine_reuse_variables reuse m =
661 701
  let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
662 702
  machine_replace_variables fvar m
663 703

  
664
let machines_reuse_variables prog reuse_tables =
665
  List.map
666
    (fun m ->
667
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables))
668
    prog
704
let machines_reuse_variables reuse_tables =
705
  List.map (fun m ->
706
      machine_reuse_variables (Utils.IMap.find m.mname.node_id reuse_tables) m)
669 707

  
670 708
let rec instr_assign res instr =
671 709
  match get_instr_desc instr with
......
723 761
    i1 :: instrs_reduce branches (i2 :: q) cont
724 762

  
725 763
let rec instrs_fusion instrs =
726
  match instrs, List.map get_instr_desc instrs with
727
  | [], [] | [ _ ], [ _ ] ->
764
  match instrs with
765
  | [] | [ _ ] ->
728 766
    instrs
729
  | i1 :: _ :: q, _ :: MBranch ({ value_desc = Var v; _ }, hl) :: _
730
    when instr_constant_assign v i1 ->
731
    instr_reduce
732
      (List.map (fun (h, b) -> h, instrs_fusion b) hl)
733
      i1 (instrs_fusion q)
734
  | i1 :: i2 :: q, _ ->
735
    i1 :: instrs_fusion (i2 :: q)
736
  | _ ->
737
    assert false
738
(* Other cases should not happen since both lists are of same size *)
767
  | i1 :: i2 :: q -> (
768
    match i2.instr_desc with
769
    | MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 ->
770
      instr_reduce
771
        (List.map (fun (h, b) -> h, instrs_fusion b) hl)
772
        { i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
773
        (instrs_fusion q)
774
    | _ ->
775
      i1 :: instrs_fusion (i2 :: q))
739 776

  
740 777
let step_fusion step =
741 778
  { step with step_instrs = instrs_fusion step.step_instrs }
......
897 934
        Scheduling.remove_prog_inlined_locals removed_table node_schs
898 935
      in
899 936
      let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
900
      machines_fusion (machines_reuse_variables machine_code reuse_tables))
937
      machines_fusion (machines_reuse_variables reuse_tables machine_code))
901 938
    else machine_code
902 939
  in
903 940

  

Also available in: Unified diff