Changeset 419 for Deliverables


Ignore:
Timestamp:
Dec 14, 2010, 2:13:07 PM (9 years ago)
Author:
mulligan
Message:

Type errors fixed, need to close additional proof obligations.

File:
1 edited

Legend:

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

    r418 r419  
    405405include "Status.ma".
    406406
    407 ndefinition assembly_jump
    408   λA, B: Type[0].
    409   λj.
    410   λaddr_of: A → B.
     407ndefinition assembly_jump: ? → (jump ?) → (? → [[relative]]) → instruction
     408  λA: Type[0].
     409  λj: jump A.
     410  λaddr_of: A → [[relative]].
    411411    match j with
    412       [ JC jmp ⇒ JC ? (addr_of jmp)
    413       | JNC jmp ⇒ JNC ? (addr_of jmp)
    414       | JZ jmp ⇒ JZ ? (addr_of jmp)
    415       | JNZ jmp ⇒ JNZ ? (addr_of jmp)
    416       | JB jmp jmp' ⇒ JB ? jmp (addr_of jmp')
    417       | JNB jmp jmp' ⇒ JNB ? jmp (addr_of jmp')
    418       | JBC jmp jmp' ⇒ JBC ? jmp (addr_of jmp')
    419       | CJNE jmp jmp' ⇒ CJNE ? jmp (addr_of jmp')
    420       | DJNZ jmp jmp' ⇒ DJNZ ? jmp (addr_of jmp')
     412      [ JC jmp ⇒ Jump [[relative]] (JC ? (addr_of jmp))
     413      | JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp))
     414      | JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp))
     415      | JNZ jmp ⇒ Jump ? (JNZ ? (addr_of jmp))
     416      | JB jmp jmp' ⇒ Jump ? (JB ? jmp (addr_of jmp'))
     417      | JNB jmp jmp' ⇒ Jump ? (JNB ? jmp (addr_of jmp'))
     418      | JBC jmp jmp' ⇒ Jump ? (JBC ? jmp (addr_of jmp'))
     419      | CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp'))
     420      | DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp'))
    421421      ].
    422422
    423 ndefinition address_of: BitVectorTrie ? ? → String → addressing_mode ≝
    424     λmap.
    425     λstring.
     423ndefinition address_of: BitVectorTrie (BitVector eight) eight → String → addressing_mode ≝
     424    λmap: BitVectorTrie (BitVector eight) eight.
     425    λstring: String.
    426426      let address ≝ lookup … (bitvector_of_string … string) map (zero ?) in
    427427      let address_bv ≝ nat_of_bitvector ? address in
     
    457457                  〈〈program_counter + program_counter_n', labels〉, costs〉
    458458              | Label label ⇒
    459                 let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
    460                   〈〈program_counter, (insert ? ? (bitvector_of_string ? label) program_counter_bv labels)〉, costs〉
     459                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
     460                  〈〈program_counter, (insert ? ? (bitvector_of_string eight label) program_counter_bv labels)〉, costs〉
    461461              | Cost cost ⇒
    462                 let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
     462                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    463463                  〈pc_labels, (insert ? ? program_counter_bv cost costs)〉
    464464              | Jmp jmp ⇒
     
    467467                  〈〈program_counter + three, labels〉, costs〉
    468468              | Mov dptr trgt ⇒ t
    469               | WithLabel jmp ⇒ ? (*
     469              | WithLabel jmp ⇒
    470470                let fake_addr ≝ RELATIVE (zero eight) in
    471                 let fake_jump ≝ assembly_jump ? ? jmp (λx. fake_addr) in
    472                 let code_memory ≝ load_code_memory (assembly1 (Jump relative fake_jump)) in
    473                 let 〈instr_pc', ignore〉  ≝ fetch code_memory (zero sixteen) in
     471                let fake_jump ≝ assembly_jump ? jmp (λx. fake_addr) in
     472                let code_memory ≝ load_code_memory (assembly1 fake_jump) in
     473                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
    474474                let 〈instr', program_counter'〉 ≝ instr_pc' in
    475475                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
    476                   〈〈program_counter + program_counter_n', labels〉, costs〉 *)
     476                  〈〈program_counter + program_counter_n', labels〉, costs〉
    477477              ]
    478478          ) 〈〈Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in
     
    491491                  | Call call ⇒
    492492                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
    493                     let address ≝ ADDR16 pc_offset in
     493                    let pc_offset_pad ≝ (zero eight) @@ pc_offset in
     494                    let address ≝ ADDR16 pc_offset_pad in
    494495                      assembly1 (LCALL ? address)
    495496                  | Mov d trgt ⇒
     
    500501                  | Jmp jmp ⇒
    501502                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in
    502                     let address ≝ ADDR16 pc_offset in
     503                    let pc_offset_pad ≝ (zero eight) @@ pc_offset in
     504                    let address ≝ ADDR16 pc_offset_pad in
    503505                      assembly1 (LJMP ? address)
    504                   | WithLabel jmp ⇒ ? (*
    505                     assembly1 (Jump ? (assembly_jump ? ? jmp (address_of labels))) *)
     506                  | WithLabel jmp ⇒
     507                    assembly1 (assembly_jump ? jmp (address_of labels))
    506508                  ]
    507509            ) instr_list
Note: See TracChangeset for help on using the changeset viewer.