Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 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/eRTLptrToLTL.ml

    r2890 r2951  
    11open Preamble
     2
     3open Extra_bool
     4
     5open Coqlib
     6
     7open Values
     8
     9open FrontEndVal
     10
     11open GenMem
     12
     13open FrontEndMem
     14
     15open Globalenvs
    216
    317open String
     
    167181    arg_decision -> 'a1 **)
    168182let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    169 | Arg_decision_colour x_22106 -> h_arg_decision_colour x_22106
    170 | Arg_decision_spill x_22107 -> h_arg_decision_spill x_22107
    171 | Arg_decision_imm x_22108 -> h_arg_decision_imm x_22108
     183| Arg_decision_colour x_19209 -> h_arg_decision_colour x_19209
     184| Arg_decision_spill x_19210 -> h_arg_decision_spill x_19210
     185| Arg_decision_imm x_19211 -> h_arg_decision_imm x_19211
    172186
    173187(** val arg_decision_rect_Type5 :
     
    175189    arg_decision -> 'a1 **)
    176190let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    177 | Arg_decision_colour x_22113 -> h_arg_decision_colour x_22113
    178 | Arg_decision_spill x_22114 -> h_arg_decision_spill x_22114
    179 | Arg_decision_imm x_22115 -> h_arg_decision_imm x_22115
     191| Arg_decision_colour x_19216 -> h_arg_decision_colour x_19216
     192| Arg_decision_spill x_19217 -> h_arg_decision_spill x_19217
     193| Arg_decision_imm x_19218 -> h_arg_decision_imm x_19218
    180194
    181195(** val arg_decision_rect_Type3 :
     
    183197    arg_decision -> 'a1 **)
    184198let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    185 | Arg_decision_colour x_22120 -> h_arg_decision_colour x_22120
    186 | Arg_decision_spill x_22121 -> h_arg_decision_spill x_22121
    187 | Arg_decision_imm x_22122 -> h_arg_decision_imm x_22122
     199| Arg_decision_colour x_19223 -> h_arg_decision_colour x_19223
     200| Arg_decision_spill x_19224 -> h_arg_decision_spill x_19224
     201| Arg_decision_imm x_19225 -> h_arg_decision_imm x_19225
    188202
    189203(** val arg_decision_rect_Type2 :
     
    191205    arg_decision -> 'a1 **)
    192206let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    193 | Arg_decision_colour x_22127 -> h_arg_decision_colour x_22127
    194 | Arg_decision_spill x_22128 -> h_arg_decision_spill x_22128
    195 | Arg_decision_imm x_22129 -> h_arg_decision_imm x_22129
     207| Arg_decision_colour x_19230 -> h_arg_decision_colour x_19230
     208| Arg_decision_spill x_19231 -> h_arg_decision_spill x_19231
     209| Arg_decision_imm x_19232 -> h_arg_decision_imm x_19232
    196210
    197211(** val arg_decision_rect_Type1 :
     
    199213    arg_decision -> 'a1 **)
    200214let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    201 | Arg_decision_colour x_22134 -> h_arg_decision_colour x_22134
    202 | Arg_decision_spill x_22135 -> h_arg_decision_spill x_22135
    203 | Arg_decision_imm x_22136 -> h_arg_decision_imm x_22136
     215| Arg_decision_colour x_19237 -> h_arg_decision_colour x_19237
     216| Arg_decision_spill x_19238 -> h_arg_decision_spill x_19238
     217| Arg_decision_imm x_19239 -> h_arg_decision_imm x_19239
    204218
    205219(** val arg_decision_rect_Type0 :
     
    207221    arg_decision -> 'a1 **)
    208222let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    209 | Arg_decision_colour x_22141 -> h_arg_decision_colour x_22141
    210 | Arg_decision_spill x_22142 -> h_arg_decision_spill x_22142
    211 | Arg_decision_imm x_22143 -> h_arg_decision_imm x_22143
     223| Arg_decision_colour x_19244 -> h_arg_decision_colour x_19244
     224| Arg_decision_spill x_19245 -> h_arg_decision_spill x_19245
     225| Arg_decision_imm x_19246 -> h_arg_decision_imm x_19246
    212226
    213227(** val arg_decision_inv_rect_Type4 :
     
    799813
    800814(** val translate_step :
    801     AST.ident List.list -> Nat.nat -> Fixpoints.valuation ->
    802     Interference.coloured_graph -> Nat.nat -> Graphs.label ->
    803     Joint.joint_step -> Blocks.bind_step_block **)
    804 let translate_step globals localss after grph stack_sz lbl s =
     815    AST.ident List.list -> Joint.joint_internal_function -> Nat.nat ->
     816    Fixpoints.valuation -> Interference.coloured_graph -> Nat.nat ->
     817    Graphs.label -> Joint.joint_step -> Blocks.bind_step_block **)
     818let translate_step globals fn localss after grph stack_sz lbl s =
    805819  Bind_new.Bret
    806820    (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
     
    956970    Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
    957971  in
    958   let coloured_graph = build globals (Types.pi1 int_fun) after in
     972  let coloured_graph =
     973    build globals (Types.pi1 int_fun)
     974      (Fixpoints.fix_lfp Liveness.register_lattice
     975        (Liveness.liveafter globals (Types.pi1 int_fun)) after)
     976  in
    959977  let stack_sz =
    960978    Nat.plus coloured_graph.Interference.spilled_no
     
    965983  TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
    966984  List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step =
    967   (translate_step globals (Types.pi1 int_fun).Joint.joint_if_local_stacksize
    968     after coloured_graph stack_sz); TranslateUtils.f_fin =
    969   (translate_fin_step globals) }
     985  (translate_step globals (Types.pi1 int_fun)
     986    (Types.pi1 int_fun).Joint.joint_if_local_stacksize
     987    (Fixpoints.fix_lfp Liveness.register_lattice
     988      (Liveness.liveafter globals (Types.pi1 int_fun)) after) coloured_graph
     989    stack_sz); TranslateUtils.f_fin = (translate_fin_step globals) }
    970990
    971991(** val ertlptr_to_ltl :
Note: See TracChangeset for help on using the changeset viewer.