Ignore:
Timestamp:
Jul 25, 2012, 12:12:57 PM (8 years ago)
Author:
mulligan
Message:

MOV and MOVX cases complete

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2247 r2256  
    480480          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧
    481481            ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
    482     | EXT_INDIRECT _ ⇒ true
     482    | EXT_INDIRECT e ⇒
     483        let address ≝ bit_address_of_register … s [[false;false;e]] in
     484          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
    483485    | REGISTER r ⇒
    484486        let address ≝ bit_address_of_register … s r in
     
    679681            None ?
    680682      | NOP ⇒ Some … M
    681       | MOVX addr1 ⇒ Some … M
     683      | MOVX addr1 ⇒
     684        match addr1 with
     685        [ inl l ⇒
     686          let 〈acc_a, others〉 ≝ l in
     687          let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
     688          let others_ok ≝ addressing_mode_ok T M … s others in
     689            if acc_a_ok ∧ others_ok then
     690              Some ? M
     691            else
     692              None ?
     693        | inr r ⇒
     694          let 〈others, acc_a〉 ≝ r in
     695          let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
     696          let others_ok ≝ addressing_mode_ok T M … s others in
     697            if others_ok ∧ acc_a_ok then
     698              Some ? M
     699            else
     700              None ?
     701        ]
    682702      | XRL addr1 ⇒
    683703        match addr1 with
Note: See TracChangeset for help on using the changeset viewer.