Changeset 2963


Ignore:
Timestamp:
Mar 26, 2013, 6:32:38 PM (4 years ago)
Author:
sacerdot
Message:

Bug fixed: the pre-main for the final code is now

COST k1
initialization code
CALL main

l: COST k2

Jmp l

with l the label of the final state. In this way the static analysis on the
object code does not diverge.

Files:
3 edited

Legend:

Unmodified
Added
Removed
  • extracted/lINToASM.ml

    r2960 r2963  
    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 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_250 =
     143    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     144    -> 'a1 **)
     145let 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_250
     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 **)
    155 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_252 =
     157    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     158    -> 'a1 **)
     159let 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_252
     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 **)
    167 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_254 =
     171    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     172    -> 'a1 **)
     173let 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_254
     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 **)
    179 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_256 =
     185    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     186    -> 'a1 **)
     187let 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_256
     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 **)
    191 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_258 =
     199    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     200    -> 'a1 **)
     201let 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_258
     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 **)
    203 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_260 =
     213    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
     214    -> 'a1 **)
     215let 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_260
     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 **)
     
    288320  let globals_addr_internal = fun res_offset x_size ->
    289321    let { Types.fst = res; Types.snd = offset } = res_offset in
    290     let { Types.fst = eta17; Types.snd = data } = x_size in
    291     let { Types.fst = x; Types.snd = region } = eta17 in
     322    let { Types.fst = eta6; Types.snd = data } = x_size in
     323    let { Types.fst = x; Types.snd = region } = eta6 in
    292324    { Types.fst =
    293325    (Identifiers.add PreIdentifiers.SymbolTag res x
     
    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 :
     
    320352        (Identifiers.empty_map PreIdentifiers.LabelTag)
    321353    in
    322     let { Types.fst = eta18; Types.snd = lmap0 } =
     354    let { Types.fst = eta7; Types.snd = lmap0 } =
    323355      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    324356      | Types.None ->
     
    332364          lmap }
    333365    in
    334     let { Types.fst = id; Types.snd = univ } = eta18 in
     366    let { Types.fst = id; Types.snd = univ } = eta7 in
    335367    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    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 :
     
    344377  Obj.magic (fun u ->
    345378    let imap = u.ident_map in
    346     let { Types.fst = eta19; Types.snd = imap0 } =
     379    let { Types.fst = eta8; Types.snd = imap0 } =
    347380      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    348381      | Types.None ->
     
    356389          imap }
    357390    in
    358     let { Types.fst = id; Types.snd = univ } = eta19 in
     391    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
     
    12401276            Monad.m_bind0 (Monad.smax_def State.state_monad)
    12411277              (translate_initialization p) (fun init ->
    1242               Monad.m_return0 (Monad.smax_def State.state_monad)
    1243                 (let code0 =
    1244                    List.append init (List.Cons ({ Types.fst = Types.None;
    1245                      Types.snd = (ASM.Call main) }, (List.Cons ({ Types.fst =
    1246                      (Types.Some exit_label); Types.snd = (ASM.Jmp
    1247                      exit_label) }, code))))
    1248                  in
    1249                 Monad.m_bind0 (Monad.max_def Option.option)
    1250                   (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
    1251                   Monad.m_return0 (Monad.max_def Option.option)
    1252                     { ASM.preamble = List.Nil; ASM.code = code0;
    1253                     ASM.renamed_symbols = symboltable; ASM.final_label =
    1254                     exit_label }))))))))
    1255 
     1278              Monad.m_bind0 (Monad.smax_def State.state_monad)
     1279                State.state_get (fun u ->
     1280                Monad.m_return0 (Monad.smax_def State.state_monad)
     1281                  (let code0 =
     1282                     List.append init (List.Cons ({ Types.fst = Types.None;
     1283                       Types.snd = (ASM.Call main) }, (List.Cons
     1284                       ({ Types.fst = (Types.Some exit_label); Types.snd =
     1285                       (ASM.Cost u.fresh_cost_label) }, (List.Cons
     1286                       ({ Types.fst = Types.None; Types.snd = (ASM.Jmp
     1287                       exit_label) }, code))))))
     1288                   in
     1289                  Monad.m_bind0 (Monad.max_def Option.option)
     1290                    (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
     1291                    Monad.m_return0 (Monad.max_def Option.option)
     1292                      { ASM.preamble = List.Nil; ASM.code = code0;
     1293                      ASM.renamed_symbols = symboltable; ASM.final_label =
     1294                      exit_label })))))))))
     1295
  • extracted/lINToASM.mli

    r2951 r2963  
    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
  • src/LIN/LINToASM.ma

    r2946 r2963  
    66
    77include "LIN/LIN.ma".
    8 
    9 
    108
    119(* utilities to provide Identifier's and addresses  *)
     
    1715; address_map : identifier_map SymbolTag Word
    1816; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
     17; fresh_cost_label: Pos
    1918}.
     19
     20definition report_cost:
     21 ∀globals. costlabel → state_monad (ASM_universe globals) unit ≝
     22 λglobals,cl,u.
     23  let clw ≝ word_of_identifier … cl in
     24  if leb (fresh_cost_label … u) clw then
     25   〈mk_ASM_universe … (id_univ … u) (current_funct … u) (ident_map … u)
     26    (label_map … u) (address_map … u) (globals_are_in … u) (succ clw), it〉 
     27  else
     28   〈u,it〉.
    2029
    2130definition new_ASM_universe :
     
    3241  (an_identifier … one (* dummy *))
    3342  (empty_map …) (empty_map …)
    34   (\fst addresses) ?.
     43  (\fst addresses) ? one.
    3544@hide_prf
    3645normalize nodelta
     
    6675  ] in
    6776〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
    68   (address_map … u) (globals_are_in … u), id〉.
     77  (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
    6978
    7079definition Identifier_of_ident :
     
    8089  ] in
    8190〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
    82   (address_map … u) (globals_are_in … u), id〉.
     91  (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
    8392
    8493definition start_funct_translation :
     
    8796  λg,id_f,u.
    8897    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
    89       (address_map … u) (globals_are_in … u), it〉.
     98      (address_map … u) (globals_are_in … u) (fresh_cost_label … u), it〉.
    9099
    91100definition address_of_ident :
     
    98107λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
    99108〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
    100   (address_map … u) (globals_are_in … u), id〉.
     109  (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
    101110
    102111definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    304313          return Instruction (JMP … INDIRECT_DPTR)
    305314        ]
    306       | COST_LABEL lbl ⇒ return Cost lbl
     315      | COST_LABEL lbl ⇒
     316         !_ report_cost … lbl ;
     317         return Cost lbl
    307318      | COND _ lbl ⇒
    308319        ! l ← Identifier_of_label … lbl;
     
    455466     ! symboltable ← get_symboltable … ;
    456467     ! init ← translate_initialization p ;
     468     ! u ← state_get … ;
    457469     return
    458        (let code ≝
    459         init @ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     470       (
     471        let code ≝
     472        init @
     473         〈None ?, Call main〉 ::
     474         〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ::
     475         〈None ?, Jmp exit_label〉 :: code in
    460476        ! code_ok ← code_size_opt code ; 
    461477        (* atm no data identifier is used in the code, so preamble must be empty *)
Note: See TracChangeset for help on using the changeset viewer.