Changeset 3051


Ignore:
Timestamp:
Apr 1, 2013, 6:28:59 PM (4 years ago)
Author:
tranquil
Message:

fixed order of global initialization in LINToASM. For the moment assembly preamble now holds a map of identifiers to addresses rather than reserved sizes. To be discussed.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r3045 r3051  
    10281028qed.
    10291029
     1030(* probably to be changed *)
    10301031definition construct_datalabels: list (Identifier × Word) → ? ≝
    1031   λthe_preamble.
     1032foldl (identifier_map ASMTag Word) ? (λdatalabels,preamble.
     1033      let 〈name, addr〉 ≝ preamble in
     1034      add ? ? datalabels name addr) (empty_map …).
     1035(*  λthe_preamble.
    10321036    foldl ((identifier_map ASMTag Word)) ? (
    10331037    λpreamble,t. add … preamble (\fst t) (\snd t)) (empty_map ??) the_preamble.
  • src/LIN/LINToASM.ma

    r3045 r3051  
    394394
    395395definition do_store_init_data :
    396   init_data → state_monad ASM_universe init_mutable
     396  state_monad ASM_universe init_mutable → init_data
    397397  state_monad ASM_universe init_mutable ≝
    398 λdata,m_mut.
     398λm_mut,data.
    399399! mut ← m_mut ;
    400400let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in
     
    423423
    424424definition do_store_global :
     425    state_monad ASM_universe init_mutable →
    425426  (ident × region × (list init_data)) →
    426     state_monad ASM_universe init_mutable →
    427427    state_monad ASM_universe init_mutable ≝
    428   λid_reg_data,m_mut.! mut ← m_mut ;
     428  λm_mut,id_reg_data.! mut ← m_mut ;
    429429  let 〈id, reg, data〉 ≝ id_reg_data in
    430430  ! Id ← Identifier_of_ident … id ;
     
    435435  for now, I'll change lookup_datalabels... *)
    436436      (〈Id, bitvector_of_Z … (virtual_dptr mut)〉 :: built_preamble mut) in
    437   foldr … do_store_init_data (return mut) data.
     437  foldl … do_store_init_data (return mut) data.
    438438
    439439let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝
     
    451451  let start_sp : Z ≝ -(S (globals_stacksize … p)) in
    452452  let mut ≝ mk_init_mutable start_sp OZ [ ] [ ] in
    453   ! globals_init ← foldr … do_store_global (return mut) (prog_vars … p) ;
     453  ! globals_init ← foldl … do_store_global (return mut) (prog_vars … p) ;
    454454  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
    455455  let init_isp ≝
Note: See TracChangeset for help on using the changeset viewer.