Changeset 3039 for src/LIN


Ignore:
Timestamp:
Mar 29, 2013, 5:45:14 PM (7 years ago)
Author:
tranquil
Message:
  • merged and extended MovSuccessor? and Mov in one instruction (Mov dst

ident offset)

  • JMP now correctly uses ACCDPTR argument
  • LINToASM: ADDRESS now translate to a symbolical Mov (now a preamble

is generated), and globals initialization is fixed accordingly

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r3028 r3039  
    88
    99(* utilities to provide Identifier's and addresses  *)
    10 record ASM_universe (globals : list ident) : Type[0] :=
     10record ASM_universe : Type[0] :=
    1111{ id_univ : universe ASMTag
    1212; current_funct : ident
    1313; ident_map : identifier_map SymbolTag Identifier
    1414; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
    15 ; address_map : identifier_map SymbolTag Word
    16 ; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
    1715; fresh_cost_label: Pos
    1816}.
    1917
    2018definition report_cost:
    21  ∀globals. costlabel → state_monad (ASM_universe globals) unit ≝
    22  λglobals,cl,u.
     19 costlabel → state_monad ASM_universe unit ≝
     20 λcl,u.
    2321  let clw ≝ word_of_identifier … cl in
    2422  if leb (fresh_cost_label … u) clw then
    2523   〈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〉 
     24    (label_map … u) (succ clw), it〉 
    2725  else
    2826   〈u,it〉.
    2927
    30 definition new_ASM_universe :
    31 ∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝
    32 λp.
    33   let globals_addr_internal ≝
    34    λres_offset : identifier_map SymbolTag Word × Z.
    35    λx_size: ident × region × (list init_data).
    36     let 〈res, offset〉 ≝ res_offset in
    37     let 〈x, region, data〉 ≝ x_size in
    38       〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat (size_init_data_list data)〉 in
    39       (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
    40   let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, -(S (globals_stacksize … p))〉 (prog_vars ?? p) in
    41 mk_ASM_universe ? (mk_universe … one)
    42   (an_identifier … one (* dummy *))
    43   (empty_map …) (empty_map …)
    44   (\fst addresses) ? one.
    45 @hide_prf
    46 normalize nodelta
    47 cases p -p * #vars #functs #main #cost_init
    48 #i #H
    49 letin init_val ≝ (〈empty_map ? Word, -(S (globals_stacksize ??))〉)
    50 cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
    51 [ %2{H} ] -H
    52 lapply i -i lapply init_val -init_val elim vars -vars
    53 [2: ** #id #r #v #tl #IH ] #init_val #i
    54 [2: * [2: * ] #H @H ]
    55 * [2: #H cases (orb_Prop_true … H) -H ] #H
    56 @IH
    57 [ %1 cases init_val normalize nodelta #init_map #off
    58   >(proj1 ?? (eqb_true ???) H) @mem_set_add_id
    59 | %2{H}
    60 | %1 cases init_val in H; normalize nodelta #init_map #off #H
    61   >mem_set_add @orb_Prop_r @H
    62 ]
    63 qed.
    64 
    6528definition Identifier_of_label :
    66   ∀globals.label → state_monad (ASM_universe globals) Identifier ≝
    67 λg,l,u.
     29  label → state_monad ASM_universe Identifier ≝
     30λl,u.
    6831let current ≝ current_funct … u in
    6932let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
     
    7639  ] in
    7740〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
    78   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     41  (fresh_cost_label … u), id〉.
    7942
    8043definition Identifier_of_ident :
    81   ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝
    82 λg,i,u.
     44  ident → state_monad ASM_universe Identifier ≝
     45λi,u.
    8346let imap ≝ ident_map … u in
    84 let 〈id, univ, imap〉 ≝
    85   match lookup … imap i with
     47let res ≝ match lookup … imap i with
    8648  [ Some id ⇒ 〈id, id_univ … u, imap〉
    8749  | None ⇒
     
    8951    〈id, univ, add … imap i id〉
    9052  ] in
     53let id ≝ \fst (\fst res) in
     54let univ ≝ \snd (\fst res) in
     55let imap ≝ \snd res in
    9156〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
    92   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     57  (fresh_cost_label … u), id〉.
     58
     59definition new_ASM_universe :
     60∀p : joint_program LIN.ASM_universe ≝
     61λp.
     62mk_ASM_universe (mk_universe … one)
     63  (an_identifier … one (* dummy *))
     64  (empty_map …) (empty_map …) one.
     65(*@hide_prf normalize nodelta
     66cases p -p * #vars #functs #main #cost_init
     67#i #H
     68normalize nodelta
     69letin init_val ≝ (〈empty_map SymbolTag Identifier, mk_universe ASMTag one〉)
     70cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
     71[ %2{H} ] -H
     72lapply i -i lapply init_val -init_val
     73whd in match prog_var_names; normalize nodelta
     74elim vars -vars
     75[2: ** #id #r #v #tl #IH ] #init_val #i
     76[2: * [2: * ] #H @H ]
     77* [2: #H cases (orb_Prop_true … H) -H ] #H
     78@IH
     79[ %1 cases init_val normalize nodelta #init_map #off
     80  >(proj1 ?? (eqb_true ???) H) @pair_elim #lft #rgt #_ @mem_set_add_id
     81| %2{H}
     82| %1 cases init_val in H; normalize nodelta #init_map #off #H
     83  @pair_elim #lft #rgt #_
     84  >mem_set_add @orb_Prop_r @H
     85]
     86qed.
     87*)
    9388
    9489definition start_funct_translation :
    9590  ∀globals.(ident × (joint_function LIN globals)) →
    96     state_monad (ASM_universe globals) unit ≝
     91    state_monad ASM_universe unit ≝
    9792  λg,id_f,u.
    9893    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
    99       (address_map … u) (globals_are_in … u) (fresh_cost_label … u), it〉.
    100 
    101 definition address_of_ident :
    102   ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝
    103 λglobals,i,prf,u.
    104 〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed.
     94      (fresh_cost_label … u), it〉.
    10595
    10696definition ASM_fresh :
    107   ∀globals.state_monad (ASM_universe globals) Identifier ≝
    108 λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
     97  state_monad ASM_universe Identifier ≝
     98λu.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
    10999〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
    110   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     100  (fresh_cost_label … u), id〉.
    111101
    112102definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    161151(* TODO: check and change to free bit *)
    162152definition asm_other_bit ≝ BIT_ADDR (zero_byte).
     153definition one_word : Word ≝ bv_zero 15 @@ [[ true ]].
    163154
    164155definition translate_statements :
    165156  ∀globals.
    166157  joint_statement LIN globals →
    167   state_monad (ASM_universe globals) pseudo_instruction ≝
     158  state_monad ASM_universe pseudo_instruction ≝
    168159  λglobals,statement.
    169160  match statement with
     
    188179          | LOW_ADDRESS lbl ⇒
    189180            ! lbl' ← Identifier_of_label … lbl ;
    190             return MovSuccessor (register_address RegisterA) LOW lbl'
     181            return Mov (inr ?? 〈register_address RegisterA, LOW〉) lbl' one_word
    191182          | HIGH_ADDRESS lbl ⇒
    192183            ! lbl' ← Identifier_of_label … lbl ;
    193             return MovSuccessor (register_address RegisterA) HIGH lbl'
     184            return Mov (inr ?? 〈register_address RegisterA, HIGH〉) lbl' one_word
    194185          ]
    195186        | COMMENT comment ⇒ return Comment comment
     
    253244        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    254245        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    255         | ADDRESS addr proof _ _ ⇒
    256           ! addr' ← address_of_ident … proof ;
    257           return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉)))))
     246        | ADDRESS id proof _ _ ⇒
     247          ! Id ← Identifier_of_ident … id ;
     248          return (Mov (inl ?? DPTR) Id (bv_zero ?))
    258249        | SET_CARRY ⇒
    259250          return Instruction (SETB ? CARRY)
     
    312303          return Call (toASM_ident ? id')
    313304        | inr _ ⇒
    314           return Instruction (JMP … INDIRECT_DPTR)
     305          return Instruction (JMP … ACC_DPTR)
    315306        ]
    316307      | COST_LABEL lbl ⇒
     
    336327  match \fst statement with
    337328  [ Some lbl ⇒
    338     ! lbl' ← Identifier_of_label globals lbl ;
     329    ! lbl' ← Identifier_of_label lbl ;
    339330    return 〈Some ? lbl', stmt〉
    340331  | None ⇒
     
    371362{ virtual_dptr : Z
    372363; actual_dptr : Z
    373 ; built : list labelled_instruction
     364; built_code : list (list labelled_instruction)
     365; built_preamble : list (Identifier × Word)
    374366}.
    375367
    376 definition store_byte : Byte → init_mutable → init_mutable ≝
     368definition store_byte_or_Identifier :
     369  (Byte ⊎ (word_side × Identifier)) → init_mutable → init_mutable ≝
    377370λby,mut.
    378371match mut with
    379 [ mk_init_mutable virt act acc
     372[ mk_init_mutable virt act acc1 acc2
    380373  let off ≝ virt - act in
    381374  let pre ≝
     
    384377    else [ 〈None ?, Instruction (MOV ? (inl … (inl … (inr …
    385378        〈DPTR, DATA16 (bitvector_of_Z … virt)〉))))〉 ] in
     379  let post ≝ match by with
     380    [ inl by ⇒
     381      〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ?
     382                               〈ACC_A, DATA by〉))))))〉
     383    | inr si_id ⇒
     384      〈None ?, Mov (inr ?? 〈ACC_A, \fst si_id〉) (\snd si_id) (bv_zero ?)〉
     385    ] in
    386386  mk_init_mutable (Zsucc virt) virt
    387     (pre @
    388      [ 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ?
    389                              〈ACC_A, DATA by〉))))))〉 ;
    390        〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ])
     387    ((pre @
     388      [ post ;
     389       〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ]) ::
     390     acc1)
     391    acc2 
    391392]. @I qed.
    392393
     394
    393395definition do_store_init_data :
    394   ∀globals.ASM_universe globals → init_data → init_mutable → init_mutable ≝
    395 λglobals,u,data.
     396  init_data → state_monad ASM_universe init_mutable →
     397  state_monad ASM_universe init_mutable ≝
     398λdata,m_mut.
     399! mut ← m_mut ;
     400let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in
     401let store_Identifier ≝ λside,id.store_byte_or_Identifier (inr … 〈side, id〉) in
    396402match data with
    397403[ Init_int8 n ⇒
    398   store_byte n
     404  return store_byte n mut
    399405| Init_int16 n ⇒
    400406  let 〈by0, by1〉 ≝ vsplit ? 8 8 n in
    401   store_byte by1 ∘ store_byte by0
     407  return store_byte by1 (store_byte by0 mut)
    402408| Init_int32 n ⇒
    403409  let 〈by0, n〉 ≝ vsplit ? 8 24 n in
    404410  let 〈by1, n〉 ≝ vsplit ? 8 16 n in
    405411  let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
    406   store_byte by3 ∘ store_byte by2 ∘ store_byte by1 ∘ store_byte by0
     412  return store_byte by3 (store_byte by2 (store_byte by1 (store_byte by0 mut)))
    407413| Init_addrof symb ofs ⇒
    408   let addr : Word ≝
    409     match lookup … (address_map … u) symb with
    410     [ Some x ⇒ bitvector_of_Z ? (Z_of_unsigned_bitvector … x + ofs)
    411     | None ⇒ bv_zero ?
    412     ] in
    413   let 〈by1, by0〉 ≝ vsplit ? 8 8 addr in
    414   store_byte by1 ∘ store_byte by0
     414  ! id ← Identifier_of_ident … symb ;
     415  return store_Identifier HIGH id (store_Identifier LOW id mut)
    415416| Init_space n ⇒
    416   λmut.mk_init_mutable (n + virtual_dptr mut) (actual_dptr mut) (built mut)
     417  return mk_init_mutable (n + virtual_dptr mut) (actual_dptr mut)
     418    (built_code mut) (built_preamble mut)
    417419| Init_null ⇒
    418420  let z ≝ bv_zero ? in
    419   store_byte z ∘ store_byte z
     421  return store_byte z (store_byte z mut)
    420422].
    421423
    422 definition do_store_init_data_list :
    423   ∀globals.ASM_universe globals → Z → list init_data → list labelled_instruction ≝
    424   λglobals,u,start_dptr,data.
    425   let init ≝ mk_init_mutable start_dptr OZ [ ] in
    426   built (foldr … (do_store_init_data … u) init data).
    427 
    428 definition translate_premain : ∀p : lin_program.
    429   Identifier → state_monad (ASM_universe (prog_var_names … p)) (list labelled_instruction) ≝
     424definition do_store_global :
     425  (ident × region × (list init_data)) →
     426    state_monad ASM_universe init_mutable →
     427    state_monad ASM_universe init_mutable ≝
     428  λid_reg_data,m_mut.! mut ← m_mut ;
     429  let 〈id, reg, data〉 ≝ id_reg_data in
     430  ! Id ← Identifier_of_ident … id ;
     431  let mut ≝ mk_init_mutable (virtual_dptr mut) (actual_dptr mut) (built_code mut)
     432      (〈Id, bitvector_of_Z … (virtual_dptr mut)〉 :: built_preamble mut) in
     433  foldr … do_store_init_data (return mut) data.
     434
     435let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝
     436match l with
     437[ nil ⇒ acc
     438| cons hd tl ⇒ reversed_flatten_aux … (hd @ acc) tl
     439].
     440
     441definition translate_premain : ∀p : lin_program.Identifier →
     442  state_monad ASM_universe (list labelled_instruction × (list (Identifier × Word))) ≝
    430443  λp : lin_program.λexit_label.
    431444  ! main ← Identifier_of_ident … (prog_main … p) ;
     
    433446  (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
    434447  let start_sp : Z ≝ -(S (globals_stacksize … p)) in
     448  let mut ≝ mk_init_mutable start_sp OZ [ ] [ ] in
     449  ! globals_init ← foldr … do_store_global (return mut) (prog_vars … p) ;
    435450  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
    436   let data ≝ flatten ? (map ?? (λx.\snd x) (prog_vars … p)) in
    437451  let init_isp ≝
    438452    (* initial stack pointer set to 2Fh in order to use addressable bits *)
     
    443457  let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
    444458  let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
    445   return ([
     459  return [
    446460    〈None ?, Cost (init_cost_label … p)〉 ;
    447461    (* initialize the internal stack pointer past the addressable bits *)
     
    456470    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
    457471      〈reg_sph, DATA sph〉))))))〉 ] @
    458   do_store_init_data_list ? u start_sp data @
     472  reversed_flatten_aux … [ ] (built_code globals_init) @
    459473  [ 〈None ?, Call main〉 ;
    460474    〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ;
    461     〈None ?, Jmp exit_label〉]). @I qed.
     475    〈None ?, Jmp exit_label〉], built_preamble globals_init〉. @I qed.
    462476
    463477definition get_symboltable :
    464   ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
    465   λglobals,u.
     478  state_monad ASM_universe (list (Identifier × ident)) ≝
     479  λu.
    466480  let imap ≝ ident_map … u in
    467481  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
     
    479493     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
    480494     ! symboltable ← get_symboltable … ;
    481      ! init ← translate_premain p exit_label;
     495     ! 〈init, preamble〉 ← translate_premain p exit_label;
    482496     return
    483497       (
     
    487501        (* atm no data identifier is used in the code, so preamble must be empty *)
    488502        return
    489           (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
     503          (mk_pseudo_assembly_program preamble code code_ok symboltable exit_label ? ?))).
    490504cases daemon
    491505qed.
Note: See TracChangeset for help on using the changeset viewer.