Changeset 3066 for src/LIN


Ignore:
Timestamp:
Apr 2, 2013, 1:48:08 PM (8 years ago)
Author:
tranquil
Message:
  • implemented get_arg_16 for ACC_DPTR
  • LINToASM is now agnostic as to where single global variables end up, as long as all global variables end up at the bottom of XData
  • consequently, ASM preamble is back indicating sizes rather than addresses
  • Assembly now correctly maps identifiers with offsets in case of code points
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r3051 r3066  
    360360
    361361record init_mutable : Type[0] ≝
    362 { virtual_dptr : Z
    363 ; actual_dptr : Z
     362{ virtual_dptr : Identifier × Z
     363; actual_dptr : Identifier × Z
    364364; built_code : list (list labelled_instruction)
    365365; built_preamble : list (Identifier × Word)
     
    371371match mut with
    372372[ mk_init_mutable virt act acc1 acc2 ⇒
    373   let off ≝ virt - act in
    374373  let pre ≝
    375     if eqZb off OZ then [ ]
    376     else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ]
    377     else [ 〈None ?, Instruction (MOV ? (inl … (inl … (inr …
    378         〈DPTR, DATA16 (bitvector_of_Z … virt)〉))))〉 ] in
     374    if eq_identifier … (\fst virt) (\fst act) then
     375      let off ≝ \snd virt - \snd act in
     376      if eqZb off OZ then [ ]
     377      else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ]
     378      else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ]
     379    else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ] in
    379380  let post ≝ match by with
    380381    [ inl by ⇒
     
    384385      〈None ?, Mov (inr ?? 〈ACC_A, \fst si_id〉) (\snd si_id) (bv_zero ?)〉
    385386    ] in
    386   mk_init_mutable (Zsucc virt) virt
     387  mk_init_mutable 〈\fst virt, Zsucc (\snd virt)〉 virt
    387388    ((pre @
    388389      [ post ;
     
    415416  return store_Identifier HIGH id (store_Identifier LOW id mut)
    416417| Init_space n ⇒
    417   return mk_init_mutable (n + virtual_dptr mut) (actual_dptr mut)
     418  let 〈virt_id, virt_off〉 ≝ virtual_dptr mut in
     419  return mk_init_mutable 〈virt_id, n + virt_off〉 (actual_dptr mut)
    418420    (built_code mut) (built_preamble mut)
    419421| Init_null ⇒
     
    429431  let 〈id, reg, data〉 ≝ id_reg_data in
    430432  ! Id ← Identifier_of_ident … id ;
    431   let mut ≝ mk_init_mutable (virtual_dptr mut) (actual_dptr mut) (built_code mut)
    432   (* Paolo: this is what you intended Claudio:
    433       (〈Id, bitvector_of_nat … (size_init_data_list … data)〉 :: built_preamble mut) in
    434   however, if we do initialization here, we need to actually fix the addresses!
    435   for now, I'll change lookup_datalabels... *)
    436       (〈Id, bitvector_of_Z … (virtual_dptr mut)〉 :: built_preamble mut) in
     433  let mut ≝ mk_init_mutable 〈Id, OZ〉 (actual_dptr … mut) (built_code mut)
     434    (〈Id, bitvector_of_nat … (size_init_data_list … data)〉 :: built_preamble mut) in
    437435  foldl … do_store_init_data (return mut) data.
    438436
     
    448446  ! main ← Identifier_of_ident … (prog_main … p) ;
    449447  ! u ← state_get … ;
    450   (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
    451   let start_sp : Z ≝ -(S (globals_stacksize … p)) in
    452   let mut ≝ mk_init_mutable start_sp OZ [ ] [ ] in
     448  (* setting this as actual_dptr will force loading of the correct dptr *)
     449  let dummy_dptr : Identifier × Z ≝ 〈an_identifier … one, -1〉 in
     450  let mut ≝ mk_init_mutable dummy_dptr dummy_dptr [ ] [ ] in
    453451  ! globals_init ← foldl … do_store_global (return mut) (prog_vars … p) ;
    454   let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
     452  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … (-(S (globals_stacksize … p)))) in
    455453  let init_isp ≝
    456454    (* initial stack pointer set to 2Fh in order to use addressable bits *)
Note: See TracChangeset for help on using the changeset viewer.