Changeset 1581 for src/ASM/Status.ma

Timestamp:

Dec 1, 2011, 3:15:15 PM (9 years ago)

Author:

mulligan

Message:

Dangling de Bruijn pointer when trying to propagate russell to set_arg_1

File:

• src/ASM/Status.ma (modified) (1 diff)

src/ASM/Status.ma

@@ -1020 +1020 @@
 qed.
       
-definition set_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; carry ]] →
-                       Bit → PreStatus M ≝
-  λm, s, a, v.
-    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
+(* XXX: Russell typing: Σs': PreStatus M. clock … s = clock M s', causes dangling de Bruijn
+        pointer assertion failure in nCicMetaSubst.ml, line 293.  *)
+definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝
+  λm: Type[0].
+  λs: PreStatus m.
+  λa: [[bit_addr; carry]].
+  λv: Bit.
+    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
       [ BIT_ADDR b ⇒ λbit_addr: True.
-          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
-          let bit_1 ≝ get_index_v ?? nu 0 ? in
-          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
-          match bit_1 with
-            [ true ⇒
-                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
-                let d ≝ address ÷ 8 in
-                let m ≝ address mod 8 in
-                let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
-                let sfr ≝ get_bit_addressable_sfr ? s ? t true in
-                let new_sfr ≝ set_index … sfr m v ? in
-                  set_bit_addressable_sfr ? s new_sfr t
-            | false ⇒
-                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
-                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
-                let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
-                let n_bit ≝ set_index … t (modulus address 8) v ? in
-                let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
-                  set_low_internal_ram ? s memory
-            ]
+        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
+        let bit_1 ≝ get_index_v ?? nu 0 ? in
+        let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
+        match bit_1 return λ_. ? with
+          [ true ⇒
+            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
+            let d ≝ address ÷ 8 in
+            let m ≝ address mod 8 in
+            let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+            let sfr ≝ get_bit_addressable_sfr ? s ? t true in
+            let new_sfr ≝ set_index … sfr m v ? in
+              set_bit_addressable_sfr ? s new_sfr t
+          | false ⇒
+            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
+            let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+            let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
+            let n_bit ≝ set_index … t (modulus address 8) v ? in
+            let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
+              set_low_internal_ram ? s memory
+          ]
       | CARRY ⇒
         λcarry: True.
-          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
-          let bit_1 ≝ get_index_v… nu 1 ? in
-          let bit_2 ≝ get_index_v… nu 2 ? in
-          let bit_3 ≝ get_index_v… nu 3 ? in
-          let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
-            set_8051_sfr ? s SFR_PSW new_psw
+        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
+        let bit_1 ≝ get_index_v… nu 1 ? in
+        let bit_2 ≝ get_index_v… nu 2 ? in
+        let bit_3 ≝ get_index_v… nu 3 ? in
+        let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
+          set_8051_sfr ? s SFR_PSW new_psw
       | _ ⇒
         λother: False.