Changeset 2984


Ignore:
Timestamp:
Mar 27, 2013, 6:17:23 PM (4 years ago)
Author:
tranquil
Message:

better LINToASM initialization of globals (to be tested!)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2978 r2984  
    367367    ].
    368368
    369 definition store_bytes : list Byte → list labelled_instruction ≝
    370 λbytes.
    371 \fold[(append ?), (nil ?)]_{by ∈ bytes}
    372     [ 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA by〉))))))〉 ;
    373       〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ;
    374       〈None ?, Instruction (INC ? DPTR)〉 ]. @I qed.
     369record init_mutable : Type[0] ≝
     370{ virtual_dptr : Z
     371; actual_dptr : Z
     372; built : list labelled_instruction
     373}.
     374
     375definition store_byte : Byte → init_mutable → init_mutable ≝
     376λby,mut.
     377match mut with
     378[ mk_init_mutable virt act acc ⇒
     379  let off ≝ virt - act in
     380  let pre ≝
     381    if eqZb off OZ then [ ]
     382    else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ]
     383    else [ 〈None ?, Instruction (MOV ? (inl … (inl … (inr …
     384        〈DPTR, DATA16 (bitvector_of_Z … virt)〉))))〉 ] in
     385  mk_init_mutable (Zsucc virt) virt
     386    (pre @
     387     [ 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ?
     388                             〈ACC_A, DATA by〉))))))〉 ;
     389       〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ])
     390]. @I qed.
    375391
    376392definition do_store_init_data :
    377   ∀globals.ASM_universe globals → Z → init_data → list labelled_instruction
    378 λglobals,u,nxt_dptr,data.
     393  ∀globals.ASM_universe globals → init_data → init_mutable → init_mutable
     394λglobals,u,data.
    379395match data with
    380396[ Init_int8 n ⇒
    381   store_bytes [ n ]
     397  store_byte n
    382398| Init_int16 n ⇒
    383   let 〈by0, by1〉 ≝ vsplit ? 8 8 n in store_bytes [ by0 ; by1 ]
     399  let 〈by0, by1〉 ≝ vsplit ? 8 8 n in
     400  store_byte by1 ∘ store_byte by0
    384401| Init_int32 n ⇒
    385402  let 〈by0, n〉 ≝ vsplit ? 8 24 n in
    386403  let 〈by1, n〉 ≝ vsplit ? 8 16 n in
    387404  let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
    388   store_bytes [ by0 ; by1 ; by2 ; by3 ]
     405  store_byte by3 ∘ store_byte by2 ∘ store_byte by1 ∘ store_byte by0
    389406| Init_addrof symb ofs ⇒
    390407  let addr : Word ≝
     
    394411    ] in
    395412  let 〈by1, by0〉 ≝ vsplit ? 8 8 addr in
    396   store_bytes [by0 ; by1] 
     413  store_byte by1 ∘ store_byte by0
    397414| Init_space n ⇒
    398   (* if n = 1 it is better to use INC, ow we can set the DPTR with MOV *)
    399   match n with
    400   [ O ⇒ [ ]
    401   | S k ⇒
    402     match k with
    403     [ O ⇒ [ 〈None ?, Instruction (INC ? DPTR)〉 ]
    404     | _ ⇒ [ 〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … nxt_dptr)〉))))〉 ]
    405     ]
    406   ]
    407 | Init_null ⇒ store_bytes [ bv_zero ? ; bv_zero ? ]
    408 ]. @I qed.
     415  λmut.mk_init_mutable (n + virtual_dptr mut) (actual_dptr mut) (built mut)
     416| Init_null ⇒
     417  let z ≝ bv_zero ? in
     418  store_byte z ∘ store_byte z
     419].
    409420
    410421definition do_store_init_data_list :
    411422  ∀globals.ASM_universe globals → Z → list init_data → list labelled_instruction ≝
    412 λglobals,u,start_dptr,data.
    413 let f ≝ λdata,dptr_acc.
    414   let 〈dptr, acc〉 ≝ dptr_acc in
    415   let nxt_dptr ≝ dptr + size_init_data data in
    416   〈nxt_dptr, do_store_init_data … u nxt_dptr data @ acc〉 in
    417 〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … start_dptr)〉))))〉 ::
    418 \snd (foldr ?? f 〈start_dptr, [ ]〉 data).
    419 @I qed.
    420 
    421 definition translate_initialization : ∀p : lin_program.
    422   state_monad (ASM_universe (prog_var_names … p)) (list labelled_instruction) ≝
    423   λp : lin_program.λu.
     423  λglobals,u,start_dptr,data.
     424  let init ≝ mk_init_mutable start_dptr OZ [ ] in
     425  built (foldr … (do_store_init_data … u) init data).
     426
     427definition translate_premain : ∀p : lin_program.
     428  Identifier → state_monad (ASM_universe (prog_var_names … p)) (list labelled_instruction) ≝
     429  λp : lin_program.λexit_label.
     430  ! main ← Identifier_of_ident … (prog_main … p) ;
     431  ! u ← state_get … ;
    424432  let start_sp : Z ≝ -(globals_stacksize … p) in
    425433  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
     
    433441  let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
    434442  let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
    435   〈u, [
     443  return ([
    436444    〈None ?, Cost (init_cost_label … p)〉 ;
    437445    (* initialize the internal stack pointer past the addressable bits *)
     
    446454    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
    447455      〈reg_sph, DATA sph〉))))))〉 ] @
    448   do_store_init_data_list ? u start_sp data〉. @I qed.
     456  do_store_init_data_list ? u start_sp data @
     457  [ 〈None ?, Call main〉 ;
     458    〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ;
     459    〈None ?, Jmp exit_label〉]). @I qed.
    449460
    450461definition get_symboltable :
     
    463474      ! acc ← acc ;
    464475      return (code @ acc) in
     476     ! exit_label ← ASM_fresh … ;
    465477     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
    466      ! exit_label ← ASM_fresh … ;
    467      ! main ← Identifier_of_ident … (prog_main … p) ;
    468478     ! symboltable ← get_symboltable … ;
    469      ! init ← translate_initialization p ;
    470      ! u ← state_get … ;
     479     ! init ← translate_premain p exit_label;
    471480     return
    472481       (
    473482        let code ≝
    474         init @
    475          〈None ?, Call main〉 ::
    476          〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ::
    477          〈None ?, Jmp exit_label〉 :: code in
     483        init @ code in
    478484        ! code_ok ← code_size_opt code ; 
    479485        (* atm no data identifier is used in the code, so preamble must be empty *)
Note: See TracChangeset for help on using the changeset viewer.