Changeset 2719


Ignore:
Timestamp:
Feb 23, 2013, 1:29:21 AM (6 years ago)
Author:
sacerdot
Message:

More values manually abstracted to functions to avoid failwiths at
initialization time.

Location:
extracted
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/liveness.ml

    r2718 r2719  
    114114
    115115(** val register_lattice : Fixpoints.property_lattice **)
    116 let register_lattice =
     116let register_lattice () =
    117117  { Fixpoints.l_bottom =
    118118    (Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd =
     
    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 -> __ **)
     
    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) ->
    169169     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) ->
    240240     { Types.fst = Set_adt.set_empty (); Types.snd =
     
    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 ->
    299299     { 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
  • extracted/liveness.mli

    r2717 r2719  
    113113open Fixpoints
    114114
    115 val register_lattice : Fixpoints.property_lattice
     115val register_lattice : unit -> Fixpoints.property_lattice
    116116
    117 val rl_bottom : __
     117val rl_bottom : unit -> __
    118118
    119119val rl_psingleton : Registers.register -> __
     
    127127val defined : AST.ident List.list -> Joint.joint_statement -> __
    128128
    129 val ret_regs : I8051.register Set_adt.set0
     129val ret_regs : unit -> I8051.register Set_adt.set0
    130130
    131131val rl_arg : Joint.psd_argument -> __
Note: See TracChangeset for help on using the changeset viewer.