Changeset 2951 for extracted/liveness.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (8 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/liveness.ml

    r2890 r2951  
    2727open Util
    2828
     29open Extra_bool
     30
     31open Coqlib
     32
     33open Values
     34
     35open FrontEndVal
     36
     37open GenMem
     38
     39open FrontEndMem
     40
     41open Globalenvs
     42
    2943open String
    3044
     
    112126
    113127open Fixpoints
     128
     129(** val rl_included :
     130    (PreIdentifiers.identifier Set_adt.set, I8051.register Set_adt.set)
     131    Types.prod -> (PreIdentifiers.identifier Set_adt.set, I8051.register
     132    Set_adt.set) Types.prod -> Bool.bool **)
     133let rl_included left right =
     134  Bool.andb
     135    (Set_adt.set_subset
     136      (Identifiers.eq_identifier PreIdentifiers.RegisterTag) left.Types.fst
     137      right.Types.fst)
     138    (Set_adt.set_subset I8051.eq_Register left.Types.snd right.Types.snd)
    114139
    115140(** val register_lattice : Fixpoints.property_lattice **)
     
    124149      (Set_adt.set_equal I8051.eq_Register (Obj.magic left).Types.snd
    125150        (Obj.magic right).Types.snd)); Fixpoints.l_included =
    126     (fun left right ->
    127     Bool.andb
    128       (Set_adt.set_subset
    129         (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    130         (Obj.magic left).Types.fst (Obj.magic right).Types.fst)
    131       (Set_adt.set_subset I8051.eq_Register (Obj.magic left).Types.snd
    132         (Obj.magic right).Types.snd)); Fixpoints.l_is_maximal = (fun x ->
    133     Bool.False) }
     151    (Obj.magic rl_included); Fixpoints.l_is_maximal = (fun x -> Bool.False) }
    134152
    135153(** val rl_bottom : __ **)
     
    423441(** val livebefore :
    424442    AST.ident List.list -> Joint.joint_internal_function ->
    425     PreIdentifiers.identifier -> Fixpoints.valuation -> __ **)
    426 let livebefore globals int_fun label liveafter =
     443    Fixpoints.valuation -> Fixpoints.valuation **)
     444let livebefore globals int_fun liveafter label =
    427445  match Identifiers.lookup PreIdentifiers.LabelTag
    428446          (Obj.magic int_fun.Joint.joint_if_code) label with
     
    439457  | Types.Some stmt ->
    440458    List.fold rl_join rl_bottom (fun successor -> Bool.True)
    441       (fun successor -> livebefore globals int_fun successor liveafter0)
     459      (fun successor -> livebefore globals int_fun liveafter0 successor)
    442460      (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTLptr.eRTLptr);
    443461        Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
     
    446464(** val analyse_liveness :
    447465    Fixpoints.fixpoint_computer -> AST.ident List.list ->
    448     Joint.joint_internal_function -> Fixpoints.valuation **)
     466    Joint.joint_internal_function -> Fixpoints.fixpoint **)
    449467let analyse_liveness the_fixpoint globals int_fun =
    450   Fixpoints.fix_lfp register_lattice (the_fixpoint register_lattice)
    451     (liveafter globals int_fun)
     468  the_fixpoint register_lattice (liveafter globals int_fun)
    452469
    453470type vertex = (Registers.register, I8051.register) Types.sum
Note: See TracChangeset for help on using the changeset viewer.