Changeset 1581 for src/ASM/Status.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1541 r1581  
    10201020qed.
    10211021     
    1022 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; carry ]] →
    1023                        Bit → PreStatus M ≝
    1024   λm, s, a, v.
    1025     match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
     1022(* XXX: Russell typing: Σs': PreStatus M. clock … s = clock M s', causes dangling de Bruijn
     1023        pointer assertion failure in nCicMetaSubst.ml, line 293.  *)
     1024definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝
     1025  λm: Type[0].
     1026  λs: PreStatus m.
     1027  λa: [[bit_addr; carry]].
     1028  λv: Bit.
     1029    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
    10261030      [ BIT_ADDR b ⇒ λbit_addr: True.
    1027           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    1028           let bit_1 ≝ get_index_v ?? nu 0 ? in
    1029           let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
    1030           match bit_1 with
    1031             [ true ⇒
    1032                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1033                 let d ≝ address ÷ 8 in
    1034                 let m ≝ address mod 8 in
    1035                 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1036                 let sfr ≝ get_bit_addressable_sfr ? s ? t true in
    1037                 let new_sfr ≝ set_index … sfr m v ? in
    1038                   set_bit_addressable_sfr ? s new_sfr t
    1039             | false ⇒
    1040                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1041                 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1042                 let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
    1043                 let n_bit ≝ set_index … t (modulus address 8) v ? in
    1044                 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
    1045                   set_low_internal_ram ? s memory
    1046             ]
     1031        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
     1032        let bit_1 ≝ get_index_v ?? nu 0 ? in
     1033        let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
     1034        match bit_1 return λ_. ? with
     1035          [ true ⇒
     1036            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     1037            let d ≝ address ÷ 8 in
     1038            let m ≝ address mod 8 in
     1039            let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     1040            let sfr ≝ get_bit_addressable_sfr ? s ? t true in
     1041            let new_sfr ≝ set_index … sfr m v ? in
     1042              set_bit_addressable_sfr ? s new_sfr t
     1043          | false ⇒
     1044            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     1045            let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1046            let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
     1047            let n_bit ≝ set_index … t (modulus address 8) v ? in
     1048            let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
     1049              set_low_internal_ram ? s memory
     1050          ]
    10471051      | CARRY ⇒
    10481052        λcarry: True.
    1049           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    1050           let bit_1 ≝ get_index_v… nu 1 ? in
    1051           let bit_2 ≝ get_index_v… nu 2 ? in
    1052           let bit_3 ≝ get_index_v… nu 3 ? in
    1053           let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
    1054             set_8051_sfr ? s SFR_PSW new_psw
     1053        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
     1054        let bit_1 ≝ get_index_v… nu 1 ? in
     1055        let bit_2 ≝ get_index_v… nu 2 ? in
     1056        let bit_3 ≝ get_index_v… nu 3 ? in
     1057        let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
     1058          set_8051_sfr ? s SFR_PSW new_psw
    10551059      | _ ⇒
    10561060        λother: False.
Note: See TracChangeset for help on using the changeset viewer.