Changeset 2730 for extracted/liveness.ml


Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (8 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/liveness.ml

    r2719 r2730  
    114114
    115115(** val register_lattice : Fixpoints.property_lattice **)
    116 let register_lattice () =
     116let register_lattice =
    117117  { Fixpoints.l_bottom =
    118     (Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd =
    119       Set_adt.set_empty () }); Fixpoints.l_equal = (fun left right ->
     118    (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
     119      Set_adt.set_empty }); Fixpoints.l_equal = (fun left right ->
    120120    Bool.andb
    121121      (Set_adt.set_equal
     
    134134
    135135(** val rl_bottom : __ **)
    136 let rl_bottom () =
    137   (register_lattice ()).Fixpoints.l_bottom
     136let rl_bottom =
     137  register_lattice.Fixpoints.l_bottom
    138138
    139139(** val rl_psingleton : Registers.register -> __ **)
    140140let rl_psingleton r =
    141141  Obj.magic { Types.fst = (Set_adt.set_singleton r); Types.snd =
    142     Set_adt.set_empty () }
     142    Set_adt.set_empty }
    143143
    144144(** val rl_hsingleton : I8051.register -> __ **)
    145145let rl_hsingleton r =
    146   Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd =
     146  Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
    147147    (Set_adt.set_singleton r) }
    148148
     
    165165| Joint.Sequential (seq, l) ->
    166166  (match seq with
    167    | Joint.COST_LABEL clabel -> rl_bottom ()
     167   | Joint.COST_LABEL clabel -> rl_bottom
    168168   | Joint.CALL (x, x0, x1) ->
    169      Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd =
     169     Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
    170170       (Set_adt.set_from_list I8051.registerCallerSaved) }
    171    | Joint.COND (r, lbl_true) -> rl_bottom ()
     171   | Joint.COND (r, lbl_true) -> rl_bottom
    172172   | Joint.Step_seq s0 ->
    173173     (match s0 with
    174       | Joint.COMMENT c -> rl_bottom ()
     174      | Joint.COMMENT c -> rl_bottom
    175175      | Joint.MOVE pair_reg ->
    176176        (match (Obj.magic pair_reg).Types.fst with
     
    178178         | ERTL.HDW h -> rl_hsingleton h)
    179179      | Joint.POP r -> rl_psingleton (Obj.magic r)
    180       | Joint.PUSH r -> rl_bottom ()
     180      | Joint.PUSH r -> rl_bottom
    181181      | Joint.ADDRESS (x, r5, r6) ->
    182182        rl_join (rl_psingleton (Obj.magic r5)) (rl_psingleton (Obj.magic r6))
     
    204204      | Joint.SET_CARRY -> rl_hsingleton I8051.RegisterCarry
    205205      | Joint.LOAD (r, x, x0) -> rl_psingleton (Obj.magic r)
    206       | Joint.STORE (acc_a, dpl, dph) -> rl_bottom ()
     206      | Joint.STORE (acc_a, dpl, dph) -> rl_bottom
    207207      | Joint.Extension_seq ext ->
    208208        (match Obj.magic ext with
     
    218218         | ERTLptr.LOW_ADDRESS (r5, l0) -> rl_psingleton r5
    219219         | ERTLptr.HIGH_ADDRESS (r5, l0) -> rl_psingleton r5)))
    220 | Joint.Final x -> rl_bottom ()
     220| Joint.Final x -> rl_bottom
    221221| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
    222222
    223223(** val ret_regs : I8051.register Set_adt.set0 **)
    224 let ret_regs () =
     224let ret_regs =
    225225  Set_adt.set_from_list I8051.registerRets
    226226
     
    228228let rl_arg = function
    229229| Joint.Reg r -> rl_psingleton r
    230 | Joint.Imm x -> rl_bottom ()
     230| Joint.Imm x -> rl_bottom
    231231
    232232(** val used :
     
    236236| Joint.Sequential (seq, l) ->
    237237  (match seq with
    238    | Joint.COST_LABEL clabel -> Obj.magic (rl_bottom ())
     238   | Joint.COST_LABEL clabel -> Obj.magic rl_bottom
    239239   | Joint.CALL (x, nparams, x0) ->
    240      { Types.fst = Set_adt.set_empty (); Types.snd =
     240     { Types.fst = Set_adt.set_empty; Types.snd =
    241241       (Set_adt.set_from_list
    242242         (Util.prefix (Obj.magic nparams) I8051.registerParams)) }
     
    244244   | Joint.Step_seq s0 ->
    245245     (match s0 with
    246       | Joint.COMMENT x -> Obj.magic (rl_bottom ())
     246      | Joint.COMMENT x -> Obj.magic rl_bottom
    247247      | Joint.MOVE pair_reg ->
    248248        let r5 = (Obj.magic pair_reg).Types.snd in
     
    252252            | ERTL.PSD r -> Obj.magic (rl_psingleton r)
    253253            | ERTL.HDW r -> Obj.magic (rl_hsingleton r))
    254          | Joint.Imm x -> Obj.magic (rl_bottom ()))
    255       | Joint.POP x -> Obj.magic (rl_bottom ())
     254         | Joint.Imm x -> Obj.magic rl_bottom)
     255      | Joint.POP x -> Obj.magic rl_bottom
    256256      | Joint.PUSH r -> Obj.magic (rl_arg (Obj.magic r))
    257       | Joint.ADDRESS (x, x1, x2) -> Obj.magic (rl_bottom ())
     257      | Joint.ADDRESS (x, x1, x2) -> Obj.magic rl_bottom
    258258      | Joint.OPACCS (opaccs0, dr1, dr2, sr1, sr2) ->
    259259        Obj.magic (rl_join (rl_arg (Obj.magic sr1)) (rl_arg (Obj.magic sr2)))
     
    263263          (rl_join (rl_join (rl_arg (Obj.magic r5)) (rl_arg (Obj.magic r6)))
    264264            (match op4 with
    265              | BackEndOps.Add -> (rl_bottom ())
     265             | BackEndOps.Add -> rl_bottom
    266266             | BackEndOps.Addc -> rl_hsingleton I8051.RegisterCarry
    267267             | BackEndOps.Sub -> rl_hsingleton I8051.RegisterCarry
    268              | BackEndOps.And -> (rl_bottom ())
    269              | BackEndOps.Or -> (rl_bottom ())
    270              | BackEndOps.Xor -> (rl_bottom ())))
    271       | Joint.CLEAR_CARRY -> Obj.magic (rl_bottom ())
    272       | Joint.SET_CARRY -> Obj.magic (rl_bottom ())
     268             | BackEndOps.And -> rl_bottom
     269             | BackEndOps.Or -> rl_bottom
     270             | BackEndOps.Xor -> rl_bottom))
     271      | Joint.CLEAR_CARRY -> Obj.magic rl_bottom
     272      | Joint.SET_CARRY -> Obj.magic rl_bottom
    273273      | Joint.LOAD (acc_a, dpl, dph) ->
    274274        Obj.magic (rl_join (rl_arg (Obj.magic dpl)) (rl_arg (Obj.magic dph)))
     
    290290                (rl_join (rl_hsingleton I8051.registerSPL)
    291291                  (rl_hsingleton I8051.registerSPH))
    292             | ERTL.Ertl_frame_size r -> Obj.magic (rl_bottom ()))
    293          | ERTLptr.LOW_ADDRESS (r5, l0) -> Obj.magic (rl_bottom ())
    294          | ERTLptr.HIGH_ADDRESS (r5, l0) -> Obj.magic (rl_bottom ()))))
     292            | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)
     293         | ERTLptr.LOW_ADDRESS (r5, l0) -> Obj.magic rl_bottom
     294         | ERTLptr.HIGH_ADDRESS (r5, l0) -> Obj.magic rl_bottom)))
    295295| Joint.Final fin ->
    296296  (match fin with
    297    | Joint.GOTO l -> Obj.magic (rl_bottom ())
     297   | Joint.GOTO l -> Obj.magic rl_bottom
    298298   | Joint.RETURN ->
    299      { Types.fst = Set_adt.set_empty (); Types.snd =
     299     { Types.fst = Set_adt.set_empty; Types.snd =
    300300       (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved)
    301          (ret_regs ())) }
     301         ret_regs) }
    302302   | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
    303303| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
     
    431431  match Identifiers.lookup0 PreIdentifiers.LabelTag
    432432          (Obj.magic int_fun.Joint.joint_if_code) label0 with
    433   | Types.None -> (rl_bottom ())
     433  | Types.None -> rl_bottom
    434434  | Types.Some stmt -> statement_semantics globals stmt (liveafter label0)
    435435
     
    440440  match Identifiers.lookup0 PreIdentifiers.LabelTag
    441441          (Obj.magic int_fun.Joint.joint_if_code) label0 with
    442   | Types.None -> (rl_bottom ())
     442  | Types.None -> rl_bottom
    443443  | Types.Some stmt ->
    444     List.fold rl_join (rl_bottom ()) (fun successor -> Bool.True)
     444    List.fold rl_join rl_bottom (fun successor -> Bool.True)
    445445      (fun successor -> livebefore globals int_fun successor liveafter0)
    446446      (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTLptr.eRTLptr);
     
    452452    Joint.joint_internal_function -> Fixpoints.valuation **)
    453453let analyse_liveness the_fixpoint globals int_fun =
    454   Fixpoints.fix_lfp (register_lattice ()) (the_fixpoint (register_lattice ()))
     454  Fixpoints.fix_lfp register_lattice (the_fixpoint register_lattice)
    455455    (liveafter globals int_fun)
    456456
Note: See TracChangeset for help on using the changeset viewer.