Changeset 3066


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
Files:
4 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).

  • 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.