Changeset 2979


Ignore:
Timestamp:
Mar 27, 2013, 4:34:35 PM (7 years ago)
Author:
sacerdot
Message:
  1. LINToASM: new extraction (fix deletion backtracked)
  2. translateUtils: hand-made patch waiting for the new extraction
Location:
extracted
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • extracted/lINToASM.ml

    r2977 r2979  
    134134                      label_map : ASM.identifier Identifiers.identifier_map
    135135                                  Identifiers.identifier_map;
    136                       address_map : BitVector.word Identifiers.identifier_map }
     136                      address_map : BitVector.word Identifiers.identifier_map;
     137                      fresh_cost_label : Positive.pos }
    137138
    138139(** val aSM_universe_rect_Type4 :
    … …  
    140141    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    141142    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    142     Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
     143    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     144    -> 'a1 **)
    143145let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_3 =
    144146  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    145     ident_map0; label_map = label_map0; address_map = address_map0 } = x_3
     147    ident_map0; label_map = label_map0; address_map = address_map0;
     148    fresh_cost_label = fresh_cost_label0 } = x_3
    146149  in
    147150  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    148     address_map0 __
     151    address_map0 __ fresh_cost_label0
    149152
    150153(** val aSM_universe_rect_Type5 :
    … …  
    152155    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    153156    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    154     Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
     157    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     158    -> 'a1 **)
    155159let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5 =
    156160  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    157     ident_map0; label_map = label_map0; address_map = address_map0 } = x_5
     161    ident_map0; label_map = label_map0; address_map = address_map0;
     162    fresh_cost_label = fresh_cost_label0 } = x_5
    158163  in
    159164  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    160     address_map0 __
     165    address_map0 __ fresh_cost_label0
    161166
    162167(** val aSM_universe_rect_Type3 :
    … …  
    164169    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    165170    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    166     Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
     171    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     172    -> 'a1 **)
    167173let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_7 =
    168174  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    169     ident_map0; label_map = label_map0; address_map = address_map0 } = x_7
     175    ident_map0; label_map = label_map0; address_map = address_map0;
     176    fresh_cost_label = fresh_cost_label0 } = x_7
    170177  in
    171178  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    172     address_map0 __
     179    address_map0 __ fresh_cost_label0
    173180
    174181(** val aSM_universe_rect_Type2 :
    … …  
    176183    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    177184    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    178     Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
     185    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     186    -> 'a1 **)
    179187let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_9 =
    180188  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    181     ident_map0; label_map = label_map0; address_map = address_map0 } = x_9
     189    ident_map0; label_map = label_map0; address_map = address_map0;
     190    fresh_cost_label = fresh_cost_label0 } = x_9
    182191  in
    183192  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    184     address_map0 __
     193    address_map0 __ fresh_cost_label0
    185194
    186195(** val aSM_universe_rect_Type1 :
    … …  
    188197    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    189198    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    190     Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
     199    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     200    -> 'a1 **)
    191201let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_11 =
    192202  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    193     ident_map0; label_map = label_map0; address_map = address_map0 } = x_11
     203    ident_map0; label_map = label_map0; address_map = address_map0;
     204    fresh_cost_label = fresh_cost_label0 } = x_11
    194205  in
    195206  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    196     address_map0 __
     207    address_map0 __ fresh_cost_label0
    197208
    198209(** val aSM_universe_rect_Type0 :
    … …  
    200211    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    201212    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    202     Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
     213    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     214    -> 'a1 **)
    203215let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_13 =
    204216  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    205     ident_map0; label_map = label_map0; address_map = address_map0 } = x_13
     217    ident_map0; label_map = label_map0; address_map = address_map0;
     218    fresh_cost_label = fresh_cost_label0 } = x_13
    206219  in
    207220  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    208     address_map0 __
     221    address_map0 __ fresh_cost_label0
    209222
    210223(** val id_univ :
    … …  
    235248  xxx.address_map
    236249
     250(** val fresh_cost_label :
     251    AST.ident List.list -> aSM_universe -> Positive.pos **)
     252let rec fresh_cost_label globals xxx =
     253  xxx.fresh_cost_label
     254
    237255(** val aSM_universe_inv_rect_Type4 :
    238256    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    239257    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    240258    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    241     Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     259    Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
    242260let aSM_universe_inv_rect_Type4 x1 hterm h1 =
    243261  let hcut = aSM_universe_rect_Type4 x1 h1 hterm in hcut __
    … …  
    247265    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    248266    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    249     Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     267    Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
    250268let aSM_universe_inv_rect_Type3 x1 hterm h1 =
    251269  let hcut = aSM_universe_rect_Type3 x1 h1 hterm in hcut __
    … …  
    255273    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    256274    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    257     Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     275    Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
    258276let aSM_universe_inv_rect_Type2 x1 hterm h1 =
    259277  let hcut = aSM_universe_rect_Type2 x1 h1 hterm in hcut __
    … …  
    263281    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    264282    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    265     Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     283    Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
    266284let aSM_universe_inv_rect_Type1 x1 hterm h1 =
    267285  let hcut = aSM_universe_rect_Type1 x1 h1 hterm in hcut __
    … …  
    271289    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    272290    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    273     Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     291    Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
    274292let aSM_universe_inv_rect_Type0 x1 hterm h1 =
    275293  let hcut = aSM_universe_rect_Type0 x1 h1 hterm in hcut __
    … …  
    280298  Logic.eq_rect_Type2 x
    281299    (let { id_univ = a0; current_funct = a10; ident_map = a2; label_map = a3;
    282        address_map = a4 } = x
     300       address_map = a4; fresh_cost_label = a6 } = x
    283301     in
    284     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
     302    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
     303
     304(** val report_cost :
     305    AST.ident List.list -> CostLabel.costlabel -> Types.unit0
     306    Monad.smax_def__o__monad **)
     307let report_cost globals cl =
     308  Obj.magic (fun u ->
     309    let clw = Identifiers.word_of_identifier PreIdentifiers.CostTag cl in
     310    (match Positive.leb u.fresh_cost_label clw with
     311     | Bool.True ->
     312       { Types.fst = { id_univ = u.id_univ; current_funct = u.current_funct;
     313         ident_map = u.ident_map; label_map = u.label_map; address_map =
     314         u.address_map; fresh_cost_label = (Positive.succ clw) }; Types.snd =
     315         Types.It }
     316     | Bool.False -> { Types.fst = u; Types.snd = Types.It }))
    285317
    286318(** val new_ASM_universe : Joint.joint_program -> aSM_universe **)
    … …  
    308340  (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map =
    309341  (Identifiers.empty_map PreIdentifiers.SymbolTag); address_map =
    310   addresses.Types.fst }
     342  addresses.Types.fst; fresh_cost_label = Positive.One }
    311343
    312344(** val identifier_of_label :
    … …  
    336368    u.ident_map; label_map =
    337369    (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0);
    338     address_map = u.address_map }; Types.snd = id })
     370    address_map = u.address_map; fresh_cost_label = u.fresh_cost_label };
     371    Types.snd = id })
    339372
    340373(** val identifier_of_ident :
    … …  
    358391    let { Types.fst = id; Types.snd = univ } = eta8 in
    359392    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    360     ident_map = imap0; label_map = u.label_map; address_map =
    361     u.address_map }; Types.snd = id })
     393    ident_map = imap0; label_map = u.label_map; address_map = u.address_map;
     394    fresh_cost_label = u.fresh_cost_label }; Types.snd = id })
    362395
    363396(** val start_funct_translation :
    … …  
    367400  Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct =
    368401    id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map;
    369     address_map = u.address_map }; Types.snd = Types.It })
     402    address_map = u.address_map; fresh_cost_label = u.fresh_cost_label };
     403    Types.snd = Types.It })
    370404
    371405(** val address_of_ident :
    … …  
    385419    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    386420    ident_map = u.ident_map; label_map = u.label_map; address_map =
    387     u.address_map }; Types.snd = id })
     421    u.address_map; fresh_cost_label = u.fresh_cost_label }; Types.snd = id })
    388422
    389423(** val register_address : I8051.register -> ASM.subaddressing_mode **)
    … …  
    659693  (match instr with
    660694   | Joint.COST_LABEL lbl ->
    661      Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl)
     695     Monad.m_bind0 (Monad.smax_def State.state_monad)
     696       (report_cost globals lbl) (fun x0 ->
     697       Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl))
    662698   | Joint.CALL (f, x0, x1) ->
    663699     (match f with
    … …  
    12461282            Monad.m_bind0 (Monad.smax_def State.state_monad)
    12471283              (translate_initialization p) (fun init ->
    1248               Monad.m_return0 (Monad.smax_def State.state_monad)
    1249                 (let code0 =
    1250                    List.append init (List.Cons ({ Types.fst = Types.None;
    1251                      Types.snd = (ASM.Call main) }, (List.Cons ({ Types.fst =
    1252                      (Types.Some exit_label); Types.snd = (ASM.Jmp
    1253                      exit_label) }, code))))
    1254                  in
    1255                 Monad.m_bind0 (Monad.max_def Option.option)
    1256                   (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
    1257                   Monad.m_return0 (Monad.max_def Option.option)
    1258                     { ASM.preamble = List.Nil; ASM.code = code0;
    1259                     ASM.renamed_symbols = symboltable; ASM.final_label =
    1260                     exit_label }))))))))
    1261 
     1284              Monad.m_bind0 (Monad.smax_def State.state_monad)
     1285                State.state_get (fun u ->
     1286                Monad.m_return0 (Monad.smax_def State.state_monad)
     1287                  (let code0 =
     1288                     List.append init (List.Cons ({ Types.fst = Types.None;
     1289                       Types.snd = (ASM.Call main) }, (List.Cons
     1290                       ({ Types.fst = (Types.Some exit_label); Types.snd =
     1291                       (ASM.Cost u.fresh_cost_label) }, (List.Cons
     1292                       ({ Types.fst = Types.None; Types.snd = (ASM.Jmp
     1293                       exit_label) }, code))))))
     1294                   in
     1295                  Monad.m_bind0 (Monad.max_def Option.option)
     1296                    (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
     1297                    Monad.m_return0 (Monad.max_def Option.option)
     1298                      { ASM.preamble = List.Nil; ASM.code = code0;
     1299                      ASM.renamed_symbols = symboltable; ASM.final_label =
     1300                      exit_label })))))))))
     1301

  • extracted/lINToASM.mli

    r2977 r2979  
    134134                      label_map : ASM.identifier Identifiers.identifier_map
    135135                                  Identifiers.identifier_map;
    136                       address_map : BitVector.word Identifiers.identifier_map }
     136                      address_map : BitVector.word Identifiers.identifier_map;
     137                      fresh_cost_label : Positive.pos }
    137138
    138139val aSM_universe_rect_Type4 :
    … …  
    140141  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    141142  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    142   __ -> 'a1) -> aSM_universe -> 'a1
     143  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    143144
    144145val aSM_universe_rect_Type5 :
    … …  
    146147  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    147148  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    148   __ -> 'a1) -> aSM_universe -> 'a1
     149  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    149150
    150151val aSM_universe_rect_Type3 :
    … …  
    152153  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    153154  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    154   __ -> 'a1) -> aSM_universe -> 'a1
     155  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    155156
    156157val aSM_universe_rect_Type2 :
    … …  
    158159  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    159160  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    160   __ -> 'a1) -> aSM_universe -> 'a1
     161  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    161162
    162163val aSM_universe_rect_Type1 :
    … …  
    164165  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    165166  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    166   __ -> 'a1) -> aSM_universe -> 'a1
     167  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    167168
    168169val aSM_universe_rect_Type0 :
    … …  
    170171  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    171172  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    172   __ -> 'a1) -> aSM_universe -> 'a1
     173  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    173174
    174175val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe
    … …  
    188189  Identifiers.identifier_map
    189190
     191val fresh_cost_label : AST.ident List.list -> aSM_universe -> Positive.pos
     192
    190193val aSM_universe_inv_rect_Type4 :
    191194  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    192195  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    193196  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    194   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     197  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    195198
    196199val aSM_universe_inv_rect_Type3 :
    … …  
    198201  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    199202  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    200   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     203  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    201204
    202205val aSM_universe_inv_rect_Type2 :
    … …  
    204207  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    205208  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    206   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     209  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    207210
    208211val aSM_universe_inv_rect_Type1 :
    … …  
    210213  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    211214  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    212   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     215  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    213216
    214217val aSM_universe_inv_rect_Type0 :
    … …  
    216219  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    217220  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    218   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     221  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    219222
    220223val aSM_universe_jmdiscr :
    221224  AST.ident List.list -> aSM_universe -> aSM_universe -> __
     225
     226val report_cost :
     227  AST.ident List.list -> CostLabel.costlabel -> Types.unit0
     228  Monad.smax_def__o__monad
    222229
    223230val new_ASM_universe : Joint.joint_program -> aSM_universe

  • extracted/translateUtils.ml

    r2974 r2979  
    640640  let prologue = data0.added_prologue in
    641641  let { Types.fst = init0; Types.snd = entry' } =
    642     Obj.magic adds_graph_pre dst_g_pars globals (fun x i -> i) prologue
     642    Obj.magic adds_graph_post dst_g_pars globals prologue
    643643      (Obj.magic entry) init
    644644  in
Note: See TracChangeset for help on using the changeset viewer.