Changeset 3066 for src/ASM


Ignore:
Timestamp:
Apr 2, 2013, 1:48:08 PM (7 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
Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r3065 r3066  
    513513  ].
    514514
     515definition is_code : region → bool ≝ λr.match r with [ Code ⇒ true | _ ⇒ false ].
     516
    515517definition expand_pseudo_instruction:
    516518    ∀lookup_labels.
     
    522524  λpolicy: Word → bool.
    523525  λppc.
    524   λlookup_datalabels:Identifier → Word.
     526  λlookup_datalabels:Identifier → region × Word.
    525527  λi.
    526528  match i with
     
    539541        [ LCALL address ]
    540542  | Mov d trgt off ⇒
    541     let addr ≝ \fst (add_16_with_carry … (lookup_datalabels trgt) off false) in
     543    let 〈r, addr〉 ≝ lookup_datalabels trgt in
     544    let addr ≝ \fst (add_16_with_carry … addr off false) in
     545    let addr ≝ if is_code r then sigma addr else addr in
    542546    match d with
    543547    [ inl _ ⇒
     
    664668    let labels ≝ \fst (create_label_cost_map instr_list) in
    665669    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    666     let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (sigma (lookup_labels x)) in
     670    let lookup_datalabels ≝ λx.
     671      match lookup ASMTag … (construct_datalabels preamble) x with
     672      [ Some addr ⇒ 〈XData, addr〉
     673      | None ⇒ 〈Code, lookup_labels x〉
     674      ] in
    667675    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    668676    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
     
    684692   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi).
    685693#lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2
    686 cases pi // * [ #addr #Id #off % ] * #addr * @(subaddressing_mode_elim … addr) //
     694cases pi // *
     695[ #addr  @(subaddressing_mode_elim … addr)
     696| * #addr @(subaddressing_mode_elim … addr) [2,3: #arg ] *
     697] #Id #off whd in ⊢ (??(???%)(???%));
     698whd in match (expand_pseudo_instruction ??????) in ⊢ (??%%);
     699normalize nodelta
     700@pair_elim * #a #_ @pair_elim * #b #_ %
    687701qed.
    688702
     
    812826  normalize in ⊢ (?%?); //
    813827|5: #acc #dst1 #dst2 normalize in ⊢ (?%?); //
    814 |7: * [ #dptr #id #offset normalize in ⊢ (?%?); //]
    815     * #dst @(subaddressing_mode_elim … dst) [2,3: #w] * #lbl #off
    816     whd in match (assembly_1_pseudoinstruction ??????);
    817     whd in match (expand_pseudo_instruction ??????);
    818     lapply (vsplit bool 8 8 ?) * #high #low
    819     normalize in ⊢ (?%?); //
     828|7: *
     829  [ #dst @(subaddressing_mode_elim … dst)
     830  | * #dst @(subaddressing_mode_elim … dst) [2,3: #w] *
     831  ] #lbl #off
     832  whd in match (assembly_1_pseudoinstruction ??????);
     833  whd in match (expand_pseudo_instruction ??????);
     834  normalize nodelta @pair_elim #a #b #_
     835  [|*: lapply (vsplit bool 8 8 ?) * #high #low ]
     836  normalize in ⊢ (?%?); //
    820837]
    821838qed.
     
    837854       let datalabels ≝ construct_datalabels preamble in
    838855       let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    839        let lookup_datalabels ≝ λx.lookup_def … datalabels x (sigma (lookup_labels x)) in
     856       let lookup_datalabels ≝ λx.
     857         match lookup ASMTag … (construct_datalabels preamble) x with
     858         [ Some addr ⇒ 〈XData, addr〉
     859         | None ⇒ 〈Code, lookup_labels x〉
     860         ] in
    840861       ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|.
    841862         let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in
     
    856877  let datalabels ≝ construct_datalabels preamble in
    857878  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    858   let lookup_datalabels ≝ λx.lookup_def … datalabels x (sigma (lookup_labels x)) in
     879  let lookup_datalabels ≝ λx.
     880    match lookup ASMTag … (construct_datalabels preamble) x with
     881    [ Some addr ⇒ 〈XData, addr〉
     882    | None ⇒ 〈Code, lookup_labels x〉
     883    ] in
    859884  let 〈next_pc,revcode〉 ≝ pi1 … (
    860885     foldl_strong
  • src/ASM/Interpret.ma

    r3064 r3066  
    186186              | _ ⇒ λother: False. ⊥
    187187              ] (subaddressing_modein … addr)
    188         | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
     188        | JMP acc_dptr ⇒ λinstr_refl.
    189189          let s ≝ add_ticks1 s in
    190           let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    191           let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    192           let jmp_addr : Word ≝ add … big_acc dptr in
     190          let jmp_addr ≝ get_arg_16 … s acc_dptr in
    193191            set_program_counter … s jmp_addr
    194192        | NOP ⇒ λinstr_refl.
     
    612610              | _ ⇒ λother: False. ⊥
    613611              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
    614         | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
     612        | JMP acc_dptr ⇒ λinstr_refl.
    615613          let s ≝ add_ticks1 s in
    616           let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    617           let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    618           let jmp_addr ≝ add … big_acc dptr in
    619           let new_pc : Word ≝ add … (program_counter … s) jmp_addr in (* JHM: type annotation *)
    620             set_program_counter … s new_pc
     614          let jmp_addr ≝ get_arg_16 … s acc_dptr in
     615            set_program_counter … s jmp_addr
    621616        | NOP ⇒ λinstr_refl.
    622617           let s ≝ add_ticks2 s in
     
    960955                         program_counter_set_8051_sfr,program_counter_set_arg_1/
    961956    try (% @I) try (@or_introl % @I) try (@or_intror % @I) //
     957    normalize nodelta
     958    @(subaddressing_mode_elim … arg2) #w whd in match (get_arg_16 ????);
     959    %1 -arg2
     960    @(subaddressing_mode_elim … arg1)
     961    whd in match (set_arg_16 ?????);
     962    whd in match (set_arg_16' ?????);
     963    @vsplit_elim #vh #vl #_ normalize nodelta %
    962964qed.
    963965
  • src/ASM/Status.ma

    r3056 r3066  
    756756qed.
    757757
    758    
    759 definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝
     758definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory →
     759  [[ data16 ; acc_dptr ]] → Word ≝
    760760  λm, cm, s, a.
    761     match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
     761    match a return λx. bool_to_Prop (is_in ? [[ data16 ; acc_dptr ]] x) → ? with
    762762      [ DATA16 d ⇒ λ_:True. d
    763       | _ ⇒ λK.
    764         match K in False with
    765         [
    766         ]
     763      | ACC_DPTR ⇒ λ_:True.
     764        let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
     765        let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
     766        add … big_acc dptr
     767      | _ ⇒ Ⓧ
    767768      ] (subaddressing_modein … a).
    768769     
     
    10281029qed.
    10291030
    1030 (* probably to be changed *)
    1031 definition construct_datalabels: list (Identifier × Word) → ? ≝
    1032 foldl (identifier_map ASMTag Word) ? (λdatalabels,preamble.
    1033       let 〈name, addr〉 ≝ preamble in
    1034       add ? ? datalabels name addr) (empty_map …).
    1035 (*
     1031definition construct_datalabels: list (Identifier × Word) →
     1032  identifier_map ASMTag Word ≝
     1033  λthe_preamble.
     1034  \fst (foldl ((identifier_map ASMTag Word) × Word) ? (λt,preamble.
    10361035      let 〈datalabels, addr〉 ≝ t in
    10371036      let 〈name, size〉 ≝ preamble in
    1038       let 〈carry, sum〉 ≝ half_add … addr size in
    1039         〈add ? ? datalabels name addr, sum〉)
    1040           〈empty_map …, zero 16〉 (the_preamble)).
    1041 *)
     1037      let 〈addr, carry〉 ≝ sub_16_with_carry addr size false in
     1038      〈add ?? datalabels name addr, addr〉)
     1039    (* mcu8051ide disallows XDATA access at -1, bug or feature? *)
     1040    〈empty_map …, maximum …〉 the_preamble).
Note: See TracChangeset for help on using the changeset viewer.