Changeset 2256 for src/ASM


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

MOV and MOVX cases complete

Location:
src/ASM
Files:
2 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
  • src/ASM/AssemblyProofSplit.ma

    r2247 r2256  
    123123lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
    124124  ∀M', cm, status, status', sigma.
    125   ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *)
     125  ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
    126126    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    127127    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
     
    129129  #M' #cm #status #status' #sigma #addr1 #sfr_refl
    130130  @(subaddressing_mode_elim … addr1) try (#w #_ @I)
    131   [1: #_ @I ]
    132   #w whd in ⊢ (??%? → %);
     131  [1,4: #_ @I ] #w
     132  whd in ⊢ (??%? → %);
    133133  inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
    134   [1:
     134  [1,3:
    135135    #absurd destruct(absurd)
    136   |2:
     136  |2,4:
    137137    #_
    138138    @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
     
    221221  ∀M', cm.
    222222  ∀sigma, status, status', b, b'.
    223   ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr]]. (* XXX: expand as needed *)
     223  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
    224224    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    225225    low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
     
    275275      ]
    276276    ]
    277   |5,6:
    278     #w #_ %
     277  |5,6,7,8:
     278    #w try #w' %
    279279  ]
    280280qed.
     
    19351935      ]     
    19361936    ]
    1937   |*)43: (* MOV *)
     1937  |43: (* MOV *)
    19381938    >EQP -P normalize nodelta
    19391939    inversion addr
     
    21212121      change with (set_arg_1 ????? = ?)
    21222122      @set_arg_1_status_of_pseudo_status
    2123       >EQs >EQticks <instr_refl >addr_refl try %
    2124       [1:
     2123      [1:
     2124        >EQs >EQticks <instr_refl >addr_refl
    21252125        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
    21262126        @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    21272127        @(subaddressing_mode_elim … carry) @I
    21282128      |2:
    2129         @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps)
    2130         [1:
    2131           normalize nodelta
     2129        >EQs >EQticks <instr_refl >addr_refl %
     2130      |3,4: (* XXX: following two cases same proof but Matita is too slow if merged *)
     2131        @(pose … (set_clock ????)) #status #status_refl
     2132        [1:
     2133          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
    21322134        |2:
    2133           assumption
    2134         ]
    2135       ]
    2136     ]
    2137   |44: (* MOVX *)
     2135          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
     2136        ]
     2137        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
     2138        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
     2139        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
     2140      ]
     2141    ]
     2142  |*)44: (* MOVX *)
     2143    >EQP -P normalize nodelta
     2144    inversion addr
     2145    [1:
     2146      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
     2147      #addr_refl
     2148      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2149      whd in maps_assm:(??%%);
     2150      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2151      [2: normalize nodelta #absurd destruct(absurd) ]
     2152      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2153      [2: normalize nodelta #absurd destruct(absurd) ]
     2154      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     2155      whd in ⊢ (??%?);
     2156      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2157      change with (set_arg_8 ????? = ?)
     2158      @set_arg_8_status_of_pseudo_status try %
     2159      >EQs >EQticks <instr_refl >addr_refl
     2160      [1:
     2161        @sym_eq @set_clock_status_of_pseudo_status %
     2162      |2:
     2163        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     2164        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2165      |3:
     2166        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
     2167        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] try %
     2168        @(pose … (set_clock ????)) #status #status_refl
     2169        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     2170        [1:
     2171          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     2172          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2173        |2:
     2174          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     2175          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2176        ]
     2177      ]
     2178    |2:
     2179      #others_acc_a cases others_acc_a #others #acc_a
     2180      #addr_refl
     2181      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2182      whd in maps_assm:(??%%);
     2183      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2184      [2: normalize nodelta #absurd destruct(absurd) ]
     2185      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2186      [2: normalize nodelta #absurd destruct(absurd) ]
     2187      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     2188      whd in ⊢ (??%?);
     2189      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2190      change with (set_arg_8 ????? = ?)
     2191      @set_arg_8_status_of_pseudo_status
     2192      >EQs >EQticks <instr_refl >addr_refl try %
     2193      [1:
     2194        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
     2195        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2196      |2:
     2197        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
     2198        [1:
     2199          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2200        |2,3:
     2201          %
     2202        |4:
     2203          @(pose … (set_clock ????)) #status #status_refl
     2204          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     2205          [1:
     2206            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2)
     2207            [1: @(subaddressing_mode_elim … acc_a) % ] %
     2208          |2:
     2209            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
     2210            [1: @(subaddressing_mode_elim … acc_a) % ] %
     2211          ]
     2212        ]
     2213      ]
     2214    ]
    21382215  |45: (* SETB *)
    21392216    >EQP -P normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.