Changeset 2247 for src/ASM/AssemblyProof.ma

Timestamp:

Jul 24, 2012, 6:00:48 PM (8 years ago)

Author:

mulligan

Message:

Work on the MOV instruction from today and bug fixes in set_arg_1.

File:

• src/ASM/AssemblyProof.ma (modified) (6 diffs)

src/ASM/AssemblyProof.ma

@@ -464 +464 @@
 
 definition addressing_mode_ok ≝
- λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
-  λaddr:addressing_mode.
-   match addr with
+  λT.
+  λM: internal_pseudo_address_map.
+  λcm.
+  λs: PreStatus T cm.
+  λaddr: addressing_mode.
+  match addr with
     [ DIRECT d ⇒
         if eq_bv … d (bitvector_of_nat … 224) then
@@ -481 +484 @@
         let address ≝ bit_address_of_register … s r in
           ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
-    | ACC_A ⇒ match \snd M with [ data ⇒ true | _ ⇒ false ]
+    | ACC_A ⇒
+      match \snd M with
+      [ data ⇒ true
+      | _ ⇒ false
+      ]
     | ACC_B ⇒ true
     | DPTR ⇒ true
@@ -491 +498 @@
     | INDIRECT_DPTR ⇒ true
     | CARRY ⇒ true
-    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
-    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
+    | BIT_ADDR b ⇒
+      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
+        if head' bool 0 bit_one then
+          eq_accumulator_address_map_entry (\snd M) data
+        else
+          let address ≝ nat_of_bitvector 7 seven_bits in 
+          let address' ≝ bitvector_of_nat 7 ((address÷8)+32) in
+            ¬assoc_list_exists ?? (false:::address') (eq_bv 8) (\fst M)
+    | N_BIT_ADDR b ⇒ ¬true (* TO BE COMPLETED *)
     | RELATIVE _ ⇒ true
     | ADDR11 _ ⇒ true
@@ -650 +664 @@
       | RET ⇒
         let 〈callM, accM〉 ≝ M in
-        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
-        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
+        let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
+        let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
           if sp_plus_1 ∧ sp_plus_2 then
             Some … M
@@ -658 +672 @@
       | RETI ⇒
         let 〈callM, accM〉 ≝ M in
-        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
-        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
+        let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
+        let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
           if sp_plus_1 ∧ sp_plus_2 then
             Some … M
@@ -745 +759 @@
             None ?
         ]
-      | MOV addr1 ⇒ Some … M
+      | MOV addr1 ⇒
+        match addr1 with
+        [ inl l ⇒
+          match l with
+          [ inl l' ⇒
+            match l' with
+            [ inl l'' ⇒
+              match l'' with
+              [ inl l''' ⇒
+                match l''' with
+                [ inl l'''' ⇒
+                  let 〈acc_a, others〉 ≝ l'''' in
+                  if addressing_mode_ok T M … s acc_a ∧ addressing_mode_ok T M … s others then
+                    Some ? M
+                  else
+                    None ?
+                | inr r ⇒
+                  let 〈others, others'〉 ≝ r in
+                  if addressing_mode_ok T M … s others ∧ addressing_mode_ok T M … s others' then
+                    Some ? M
+                  else
+                    None ?
+                ]
+              | inr r ⇒
+                let 〈direct, others〉 ≝ r in
+                if addressing_mode_ok T M … s direct ∧ addressing_mode_ok T M … s others then
+                  Some ? M
+                else
+                  None ?
+              ]
+            | inr r ⇒
+              let 〈dptr, data_16〉 ≝ r in
+              if addressing_mode_ok T M … s dptr ∧ addressing_mode_ok T M … s data_16 then
+                Some ? M
+              else
+                None ?
+            ]
+          | inr r ⇒
+            let 〈carry, bit_addr〉 ≝ r in
+            if addressing_mode_ok T M … s carry ∧ addressing_mode_ok T M … s bit_addr then
+              Some ? M
+            else
+              None ?
+          ]
+        | inr r ⇒
+          let 〈bit_addr, carry〉 ≝ r in
+          if addressing_mode_ok T M … s bit_addr ∧ addressing_mode_ok T M … s carry then
+            Some ? M
+          else
+            None ?
+        ]
       ]
     ].