Ignore:
Timestamp:
Dec 13, 2010, 6:03:05 PM (9 years ago)
Author:
mulligan
Message:

Got a few more cases working.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Assembly.ma

    r410 r414  
    430430          let 〈name, size〉 ≝ preamble in
    431431          let addr_sixteen ≝ bitvector_of_nat sixteen addr in
    432             〈insert ? ? addr_sixteen name datalabels, addr + size〉)
     432            〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉)
    433433              〈(Stub ? ?), Z〉 preamble in
    434434    let 〈pc_labels, costs〉 ≝
     
    440440              [ Instruction instr ⇒
    441441                let code_memory ≝ load_code_memory (assembly1 instr) in
    442                 let 〈instr_pc', ignore〉  ≝ fetch code_memory (zero sixteen) in
     442                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
    443443                let 〈instr', program_counter'〉 ≝ instr_pc' in
    444444                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
     
    446446              | Label label ⇒
    447447                let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
    448                   〈〈program_counter, (insert ? ? program_counter_bv label labels)〉, costs〉
     448                  〈〈program_counter, (insert ? ? (bitvector_of_string ? label) program_counter_bv labels)〉, costs〉
    449449              | Cost cost ⇒
    450450                let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
     
    479479                  | Call call ⇒
    480480                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
    481                     let address ≝ ADDR16 (bitvector_of_nat sixteen pc_offset) in
    482                       assembly1 (LCALL address)
    483                   | _ ⇒ ?
     481                    let address ≝ ADDR16 pc_offset in
     482                      assembly1 (LCALL ? address)
     483                  | Mov d trgt ⇒
     484                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in
     485                    let address ≝ DATA16 pc_offset in
     486                      assembly1 (MOV ? (Right ? ?(Right ? ? (Right ? ? (Right ? ? (Right ? ? 〈DPTR, address〉))))))
     487                  | Instruction instr ⇒ ?
     488                  | Jmp jmp ⇒
     489                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in
     490                    let address ≝ ADDR16 pc_offset in
     491                      assembly1 (LJMP ? address)
     492                  | WithLabel jmp ⇒ ?
    484493                  ]
    485494            ) instr_list
Note: See TracChangeset for help on using the changeset viewer.