Changeset 2963 for src/LIN


Ignore:
Timestamp:
Mar 26, 2013, 6:32:38 PM (8 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.