Changeset 821 for src/ASM/Interpret.ma
 Timestamp:
 May 23, 2011, 3:23:17 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r820 r821 158 158 include alias "ASM/BitVectorTrie.ma". 159 159 160 definition execute_1_preinstruction: ∀A : Type[0]. (A → Byte) → preinstruction A → Status → Status≝161 λA : Type[0].160 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → Byte) → preinstruction A → PreStatus M → PreStatus M ≝ 161 λA, M: Type[0]. 162 162 λaddr_of: A → Byte. 163 163 λinstr: preinstruction A. 164 λs: Status.164 λs: PreStatus M. 165 165 match instr with 166 166 [ ADD addr1 addr2 ⇒ 167 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)168 (get_arg_8 s false addr2) false in167 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1) 168 (get_arg_8 ? s false addr2) false in 169 169 let cy_flag ≝ get_index' ? O ? flags in 170 170 let ac_flag ≝ get_index' ? 1 ? flags in 171 171 let ov_flag ≝ get_index' ? 2 ? flags in 172 let s ≝ set_arg_8 s ACC_A result in173 set_flags s cy_flag (Some Bit ac_flag) ov_flag172 let s ≝ set_arg_8 ? s ACC_A result in 173 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 174 174  ADDC addr1 addr2 ⇒ 175 let old_cy_flag ≝ get_cy_flag s in176 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)177 (get_arg_8 s false addr2) old_cy_flag in175 let old_cy_flag ≝ get_cy_flag ? s in 176 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1) 177 (get_arg_8 ? s false addr2) old_cy_flag in 178 178 let cy_flag ≝ get_index' ? O ? flags in 179 179 let ac_flag ≝ get_index' ? 1 ? flags in 180 180 let ov_flag ≝ get_index' ? 2 ? flags in 181 let s ≝ set_arg_8 s ACC_A result in182 set_flags s cy_flag (Some Bit ac_flag) ov_flag181 let s ≝ set_arg_8 ? s ACC_A result in 182 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 183 183  SUBB addr1 addr2 ⇒ 184 let old_cy_flag ≝ get_cy_flag s in185 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)186 (get_arg_8 s false addr2) old_cy_flag in184 let old_cy_flag ≝ get_cy_flag ? s in 185 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1) 186 (get_arg_8 ? s false addr2) old_cy_flag in 187 187 let cy_flag ≝ get_index' ? O ? flags in 188 188 let ac_flag ≝ get_index' ? 1 ? flags in 189 189 let ov_flag ≝ get_index' ? 2 ? flags in 190 let s ≝ set_arg_8 s ACC_A result in191 set_flags s cy_flag (Some Bit ac_flag) ov_flag190 let s ≝ set_arg_8 ? s ACC_A result in 191 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 192 192  ANL addr ⇒ 193 193 match addr with … … 196 196 [ inl l' ⇒ 197 197 let 〈addr1, addr2〉 ≝ l' in 198 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in199 set_arg_8 s addr1 and_val198 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 199 set_arg_8 ? s addr1 and_val 200 200  inr r ⇒ 201 201 let 〈addr1, addr2〉 ≝ r in 202 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in203 set_arg_8 s addr1 and_val202 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 203 set_arg_8 ? s addr1 and_val 204 204 ] 205 205  inr r ⇒ 206 206 let 〈addr1, addr2〉 ≝ r in 207 let and_val ≝ (get_cy_flag s) ∧ (get_arg_1s addr2 true) in208 set_flags s and_val (None ?) (get_ov_flags)207 let and_val ≝ (get_cy_flag ? s) ∧ (get_arg_1 ? s addr2 true) in 208 set_flags ? s and_val (None ?) (get_ov_flag ? s) 209 209 ] 210 210  ORL addr ⇒ … … 214 214 [ inl l' ⇒ 215 215 let 〈addr1, addr2〉 ≝ l' in 216 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in217 set_arg_8 s addr1 or_val216 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 217 set_arg_8 ? s addr1 or_val 218 218  inr r ⇒ 219 219 let 〈addr1, addr2〉 ≝ r in 220 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in221 set_arg_8 s addr1 or_val220 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 221 set_arg_8 ? s addr1 or_val 222 222 ] 223 223  inr r ⇒ 224 224 let 〈addr1, addr2〉 ≝ r in 225 let or_val ≝ (get_cy_flag s) ∨ (get_arg_1s addr2 true) in226 set_flags s or_val (None ?) (get_ov_flags)225 let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in 226 set_flags ? s or_val (None ?) (get_ov_flag ? s) 227 227 ] 228 228  XRL addr ⇒ … … 230 230 [ inl l' ⇒ 231 231 let 〈addr1, addr2〉 ≝ l' in 232 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in233 set_arg_8 s addr1 xor_val232 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 233 set_arg_8 ? s addr1 xor_val 234 234  inr r ⇒ 235 235 let 〈addr1, addr2〉 ≝ r in 236 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in237 set_arg_8 s addr1 xor_val236 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 237 set_arg_8 ? s addr1 xor_val 238 238 ] 239 239  INC addr ⇒ … … 244 244 dptr ]] x) → ? with 245 245 [ ACC_A ⇒ λacc_a: True. 246 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat 8 1) in247 set_arg_8 s ACC_A result246 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in 247 set_arg_8 ? s ACC_A result 248 248  REGISTER r ⇒ λregister: True. 249 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat 8 1) in250 set_arg_8 s (REGISTER r) result249 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in 250 set_arg_8 ? s (REGISTER r) result 251 251  DIRECT d ⇒ λdirect: True. 252 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat 8 1) in253 set_arg_8 s (DIRECT d) result252 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in 253 set_arg_8 ? s (DIRECT d) result 254 254  INDIRECT i ⇒ λindirect: True. 255 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat 8 1) in256 set_arg_8 s (INDIRECT i) result255 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in 256 set_arg_8 ? s (INDIRECT i) result 257 257  DPTR ⇒ λdptr: True. 258 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat 8 1) in259 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero 8) carry in260 let s ≝ set_8051_sfr s SFR_DPL bl in261 set_8051_sfr s SFR_DPH bu258 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in 259 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in 260 let s ≝ set_8051_sfr ? s SFR_DPL bl in 261 set_8051_sfr ? s SFR_DPH bu 262 262  _ ⇒ λother: False. ⊥ 263 263 ] (subaddressing_modein … addr) 264 264  DEC addr ⇒ 265 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in266 set_arg_8 s addr result265 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in 266 set_arg_8 ? s addr result 267 267  MUL addr1 addr2 ⇒ 268 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in269 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in268 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in 269 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in 270 270 let product ≝ acc_a_nat * acc_b_nat in 271 271 let ov_flag ≝ product ≥ 256 in 272 272 let low ≝ bitvector_of_nat 8 (product mod 256) in 273 273 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 274 let s ≝ set_8051_sfr s SFR_ACC_A low in275 set_8051_sfr s SFR_ACC_B high274 let s ≝ set_8051_sfr ? s SFR_ACC_A low in 275 set_8051_sfr ? s SFR_ACC_B high 276 276  DIV addr1 addr2 ⇒ 277 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in278 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in277 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in 278 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in 279 279 match acc_b_nat with 280 [ O ⇒ set_flags s false (None Bit) true280 [ O ⇒ set_flags ? s false (None Bit) true 281 281  S o ⇒ 282 282 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 283 283 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 284 let s ≝ set_8051_sfr s SFR_ACC_A q in285 let s ≝ set_8051_sfr s SFR_ACC_B r in286 set_flags s false (None Bit) false284 let s ≝ set_8051_sfr ? s SFR_ACC_A q in 285 let s ≝ set_8051_sfr ? s SFR_ACC_B r in 286 set_flags ? s false (None Bit) false 287 287 ] 288 288  DA addr ⇒ 289 let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in290 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then291 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in289 let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in 290 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then 291 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in 292 292 let cy_flag ≝ get_index' ? O ? flags in 293 293 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in … … 295 295 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 296 296 let new_acc ≝ nu @@ acc_nl' in 297 let s ≝ set_8051_sfr s SFR_ACC_A new_acc in298 set_flags s cy_flag (Some ? (get_ac_flag s)) (get_ov_flags)297 let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in 298 set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s) 299 299 else 300 300 s … … 303 303  CLR addr ⇒ 304 304 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 305 [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero 8)306  CARRY ⇒ λcarry: True. set_arg_1 s CARRY false307  BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false305 [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8) 306  CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false 307  BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false 308 308  _ ⇒ λother: False. ⊥ 309 309 ] (subaddressing_modein … addr) … … 311 311 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 312 312 [ ACC_A ⇒ λacc_a: True. 313 let old_acc ≝ get_8051_sfr s SFR_ACC_A in313 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 314 314 let new_acc ≝ negation_bv ? old_acc in 315 set_8051_sfr s SFR_ACC_A new_acc315 set_8051_sfr ? s SFR_ACC_A new_acc 316 316  CARRY ⇒ λcarry: True. 317 let old_cy_flag ≝ get_arg_1 s CARRY true in317 let old_cy_flag ≝ get_arg_1 ? s CARRY true in 318 318 let new_cy_flag ≝ ¬old_cy_flag in 319 set_arg_1 s CARRY new_cy_flag319 set_arg_1 ? s CARRY new_cy_flag 320 320  BIT_ADDR b ⇒ λbit_addr: True. 321 let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in321 let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in 322 322 let new_bit ≝ ¬old_bit in 323 set_arg_1 s (BIT_ADDR b) new_bit323 set_arg_1 ? s (BIT_ADDR b) new_bit 324 324  _ ⇒ λother: False. ? 325 325 ] (subaddressing_modein … addr) 326  SETB b ⇒ set_arg_1 s b false326  SETB b ⇒ set_arg_1 ? s b false 327 327  RL _ ⇒ (* DPM: always ACC_A *) 328 let old_acc ≝ get_8051_sfr s SFR_ACC_A in328 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 329 329 let new_acc ≝ rotate_left … 1 old_acc in 330 set_8051_sfr s SFR_ACC_A new_acc330 set_8051_sfr ? s SFR_ACC_A new_acc 331 331  RR _ ⇒ (* DPM: always ACC_A *) 332 let old_acc ≝ get_8051_sfr s SFR_ACC_A in332 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 333 333 let new_acc ≝ rotate_right … 1 old_acc in 334 set_8051_sfr s SFR_ACC_A new_acc334 set_8051_sfr ? s SFR_ACC_A new_acc 335 335  RLC _ ⇒ (* DPM: always ACC_A *) 336 let old_cy_flag ≝ get_cy_flag s in337 let old_acc ≝ get_8051_sfr s SFR_ACC_A in336 let old_cy_flag ≝ get_cy_flag ? s in 337 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 338 338 let new_cy_flag ≝ get_index' ? O ? old_acc in 339 339 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 340 let s ≝ set_arg_1 s CARRY new_cy_flag in341 set_8051_sfr s SFR_ACC_A new_acc340 let s ≝ set_arg_1 ? s CARRY new_cy_flag in 341 set_8051_sfr ? s SFR_ACC_A new_acc 342 342  RRC _ ⇒ (* DPM: always ACC_A *) 343 let old_cy_flag ≝ get_cy_flag s in344 let old_acc ≝ get_8051_sfr s SFR_ACC_A in343 let old_cy_flag ≝ get_cy_flag ? s in 344 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 345 345 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 346 346 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 347 let s ≝ set_arg_1 s CARRY new_cy_flag in348 set_8051_sfr s SFR_ACC_A new_acc347 let s ≝ set_arg_1 ? s CARRY new_cy_flag in 348 set_8051_sfr ? s SFR_ACC_A new_acc 349 349  SWAP _ ⇒ (* DPM: always ACC_A *) 350 let old_acc ≝ get_8051_sfr s SFR_ACC_A in350 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 351 351 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 352 352 let new_acc ≝ nl @@ nu in 353 set_8051_sfr s SFR_ACC_A new_acc353 set_8051_sfr ? s SFR_ACC_A new_acc 354 354  PUSH addr ⇒ 355 355 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with 356 356 [ DIRECT d ⇒ λdirect: True. 357 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in358 let s ≝ set_8051_sfr s SFR_SP new_sp in359 write_at_stack_pointer s d357 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 358 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 359 write_at_stack_pointer ? s d 360 360  _ ⇒ λother: False. ⊥ 361 361 ] (subaddressing_modein … addr) 362 362  POP addr ⇒ 363 let contents ≝ read_at_stack_pointer s in364 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in365 let s ≝ set_8051_sfr s SFR_SP new_sp in366 set_arg_8 s addr contents363 let contents ≝ read_at_stack_pointer ? s in 364 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 365 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 366 set_arg_8 ? s addr contents 367 367  XCH addr1 addr2 ⇒ 368 let old_addr ≝ get_arg_8 s false addr2 in369 let old_acc ≝ get_8051_sfr s SFR_ACC_A in370 let s ≝ set_8051_sfr s SFR_ACC_A old_addr in371 set_arg_8 s addr2 old_acc368 let old_addr ≝ get_arg_8 ? s false addr2 in 369 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 370 let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in 371 set_arg_8 ? s addr2 old_acc 372 372  XCHD addr1 addr2 ⇒ 373 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in374 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in373 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in 374 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in 375 375 let new_acc ≝ acc_nu @@ arg_nl in 376 376 let new_arg ≝ arg_nu @@ acc_nl in 377 let s ≝ set_8051_sfr s SFR_ACC_A new_acc in378 set_arg_8 s addr2 new_arg377 let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in 378 set_arg_8 ? s addr2 new_arg 379 379  RET ⇒ 380 let high_bits ≝ read_at_stack_pointer s in381 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in382 let s ≝ set_8051_sfr s SFR_SP new_sp in383 let low_bits ≝ read_at_stack_pointer s in384 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in385 let s ≝ set_8051_sfr s SFR_SP new_sp in380 let high_bits ≝ read_at_stack_pointer ? s in 381 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 382 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 383 let low_bits ≝ read_at_stack_pointer ? s in 384 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 385 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 386 386 let new_pc ≝ high_bits @@ low_bits in 387 set_program_counter s new_pc387 set_program_counter ? s new_pc 388 388  RETI ⇒ 389 let high_bits ≝ read_at_stack_pointer s in390 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in391 let s ≝ set_8051_sfr s SFR_SP new_sp in392 let low_bits ≝ read_at_stack_pointer s in393 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in394 let s ≝ set_8051_sfr s SFR_SP new_sp in389 let high_bits ≝ read_at_stack_pointer ? s in 390 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 391 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 392 let low_bits ≝ read_at_stack_pointer ? s in 393 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 394 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 395 395 let new_pc ≝ high_bits @@ low_bits in 396 set_program_counter s new_pc396 set_program_counter ? s new_pc 397 397  MOVX addr ⇒ 398 398 (* DPM: only copies  doesn't affect I/O *) … … 400 400 [ inl l ⇒ 401 401 let 〈addr1, addr2〉 ≝ l in 402 set_arg_8 s addr1 (get_arg_8s false addr2)402 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 403 403  inr r ⇒ 404 404 let 〈addr1, addr2〉 ≝ r in 405 set_arg_8 s addr1 (get_arg_8s false addr2)405 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 406 406 ] 407 407  MOV addr ⇒ … … 417 417 [ inl l'''' ⇒ 418 418 let 〈addr1, addr2〉 ≝ l'''' in 419 set_arg_8 s addr1 (get_arg_8s false addr2)419 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 420 420  inr r'''' ⇒ 421 421 let 〈addr1, addr2〉 ≝ r'''' in 422 set_arg_8 s addr1 (get_arg_8s false addr2)422 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 423 423 ] 424 424  inr r''' ⇒ 425 425 let 〈addr1, addr2〉 ≝ r''' in 426 set_arg_8 s addr1 (get_arg_8s false addr2)426 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 427 427 ] 428 428  inr r'' ⇒ 429 429 let 〈addr1, addr2〉 ≝ r'' in 430 set_arg_16 s (get_arg_16s addr2) addr1430 set_arg_16 ? s (get_arg_16 ? s addr2) addr1 431 431 ] 432 432  inr r ⇒ 433 433 let 〈addr1, addr2〉 ≝ r in 434 set_arg_1 s addr1 (get_arg_1s addr2 false)434 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false) 435 435 ] 436 436  inr r ⇒ 437 437 let 〈addr1, addr2〉 ≝ r in 438 set_arg_1 s addr1 (get_arg_1s addr2 false)438 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false) 439 439 ] 440 440  JC addr ⇒ 441 441 let r ≝ addr_of addr in 442 if get_cy_flag s then443 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in444 set_program_counter s new_pc442 if get_cy_flag ? s then 443 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 444 set_program_counter ? s new_pc 445 445 else 446 446 s 447 447  JNC addr ⇒ 448 448 let r ≝ addr_of addr in 449 if ¬(get_cy_flag s) then450 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in451 set_program_counter s new_pc449 if ¬(get_cy_flag ? s) then 450 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 451 set_program_counter ? s new_pc 452 452 else 453 453 s 454 454  JB addr1 addr2 ⇒ 455 455 let r ≝ addr_of addr2 in 456 if get_arg_1 s addr1 false then457 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in458 set_program_counter s new_pc456 if get_arg_1 ? s addr1 false then 457 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 458 set_program_counter ? s new_pc 459 459 else 460 460 s 461 461  JNB addr1 addr2 ⇒ 462 462 let r ≝ addr_of addr2 in 463 if ¬(get_arg_1 s addr1 false) then464 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in465 set_program_counter s new_pc463 if ¬(get_arg_1 ? s addr1 false) then 464 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 465 set_program_counter ? s new_pc 466 466 else 467 467 s 468 468  JBC addr1 addr2 ⇒ 469 469 let r ≝ addr_of addr2 in 470 let s ≝ set_arg_1 s addr1 false in471 if get_arg_1 s addr1 false then472 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in473 set_program_counter s new_pc470 let s ≝ set_arg_1 ? s addr1 false in 471 if get_arg_1 ? s addr1 false then 472 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 473 set_program_counter ? s new_pc 474 474 else 475 475 s 476 476  JZ addr ⇒ 477 477 let r ≝ addr_of addr in 478 if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then479 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in480 set_program_counter s new_pc478 if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then 479 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 480 set_program_counter ? s new_pc 481 481 else 482 482 s 483 483  JNZ addr ⇒ 484 484 let r ≝ addr_of addr in 485 if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then486 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in487 set_program_counter s new_pc485 if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then 486 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 487 set_program_counter ? s new_pc 488 488 else 489 489 s … … 493 493 [ inl l ⇒ 494 494 let 〈addr1, addr2〉 ≝ l in 495 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))496 (nat_of_bitvector ? (get_arg_8 s false addr2)) in497 if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8s false addr2)) then498 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in499 let s ≝ set_program_counter s new_pc in500 set_flags s new_cy (None ?) (get_ov_flags)495 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1)) 496 (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in 497 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then 498 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 499 let s ≝ set_program_counter ? s new_pc in 500 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 501 501 else 502 (set_flags s new_cy (None ?) (get_ov_flags))502 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 503 503  inr r' ⇒ 504 504 let 〈addr1, addr2〉 ≝ r' in 505 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))506 (nat_of_bitvector ? (get_arg_8 s false addr2)) in507 if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8s false addr2)) then508 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in509 let s ≝ set_program_counter s new_pc in510 set_flags s new_cy (None ?) (get_ov_flags)505 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1)) 506 (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in 507 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then 508 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 509 let s ≝ set_program_counter ? s new_pc in 510 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 511 511 else 512 (set_flags s new_cy (None ?) (get_ov_flags))512 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 513 513 ] 514 514  DJNZ addr1 addr2 ⇒ 515 515 let r ≝ addr_of addr2 in 516 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in517 let s ≝ set_arg_8 s addr1 result in516 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in 517 let s ≝ set_arg_8 ? s addr1 result in 518 518 if ¬(eq_bv ? result (zero 8)) then 519 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in520 set_program_counter s new_pc519 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 520 set_program_counter ? s new_pc 521 521 else 522 522 s … … 541 541 definition execute_1: Status → Status ≝ 542 542 λs: Status. 543 let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counters) in543 let 〈instr_pc, ticks〉 ≝ fetch (code_memory ? s) (program_counter ? s) in 544 544 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 545 let s ≝ set_clock s (clocks + ticks) in546 let s ≝ set_program_counter s pc in545 let s ≝ set_clock ? s (clock ? s + ticks) in 546 let s ≝ set_program_counter ? s pc in 547 547 let s ≝ 548 548 match instr with 549 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] 549 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ? 550 550 (λx. 551 551 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with … … 556 556 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 557 557 [ ADDR11 a ⇒ λaddr11: True. 558 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in559 let s ≝ set_8051_sfr s SFR_SP new_sp in560 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in561 let s ≝ write_at_stack_pointer s pc_bl in562 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in563 let s ≝ set_8051_sfr s SFR_SP new_sp in564 let s ≝ write_at_stack_pointer s pc_bu in558 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 559 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 560 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 561 let s ≝ write_at_stack_pointer ? s pc_bl in 562 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 563 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 564 let s ≝ write_at_stack_pointer ? s pc_bu in 565 565 let 〈thr, eig〉 ≝ split ? 3 8 a in 566 566 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 567 567 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 568 set_program_counter s new_addr568 set_program_counter ? s new_addr 569 569  _ ⇒ λother: False. ⊥ 570 570 ] (subaddressing_modein … addr) … … 572 572 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 573 573 [ ADDR16 a ⇒ λaddr16: True. 574 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in575 let s ≝ set_8051_sfr s SFR_SP new_sp in576 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in577 let s ≝ write_at_stack_pointer s pc_bl in578 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in579 let s ≝ set_8051_sfr s SFR_SP new_sp in580 let s ≝ write_at_stack_pointer s pc_bu in581 set_program_counter s a574 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 575 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 576 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 577 let s ≝ write_at_stack_pointer ? s pc_bl in 578 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 579 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 580 let s ≝ write_at_stack_pointer ? s pc_bu in 581 set_program_counter ? s a 582 582  _ ⇒ λother: False. ⊥ 583 583 ] (subaddressing_modein … addr) … … 585 585 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with 586 586 [ ACC_DPTR ⇒ λacc_dptr: True. 587 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in588 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfrs SFR_DPL) in587 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 588 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 589 589 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in 590 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in591 set_8051_sfr s SFR_ACC_A result590 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 591 set_8051_sfr ? s SFR_ACC_A result 592 592  ACC_PC ⇒ λacc_pc: True. 593 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in594 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in593 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 594 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in 595 595 (* DPM: Under specified: does the carry from PC incrementation affect the *) 596 596 (* addition of the PC with the DPTR? At the moment, no. *) 597 let s ≝ set_program_counter s inc_pc in597 let s ≝ set_program_counter ? s inc_pc in 598 598 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 599 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in600 set_8051_sfr s SFR_ACC_A result599 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 600 set_8051_sfr ? s SFR_ACC_A result 601 601  _ ⇒ λother: False. ⊥ 602 602 ] (subaddressing_modein … addr2) 603 603  JMP _ ⇒ (* DPM: always indirect_dptr *) 604 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfrs SFR_DPL) in605 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in604 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 605 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 606 606 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 607 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in608 set_program_counter s new_pc607 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in 608 set_program_counter ? s new_pc 609 609  LJMP addr ⇒ 610 610 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 611 611 [ ADDR16 a ⇒ λaddr16: True. 612 set_program_counter s a612 set_program_counter ? s a 613 613  _ ⇒ λother: False. ⊥ 614 614 ] (subaddressing_modein … addr) … … 616 616 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 617 617 [ RELATIVE r ⇒ λrelative: True. 618 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in619 set_program_counter s new_pc618 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 619 set_program_counter ? s new_pc 620 620  _ ⇒ λother: False. ⊥ 621 621 ] (subaddressing_modein … addr) … … 623 623 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 624 624 [ ADDR11 a ⇒ λaddr11: True. 625 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in625 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 626 626 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 627 627 let bit ≝ get_index' ? O ? nl in 628 628 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 629 629 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 630 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in631 set_program_counter s new_pc630 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in 631 set_program_counter ? s new_pc 632 632  _ ⇒ λother: False. ⊥ 633 633 ] (subaddressing_modein … addr) … … 652 652 653 653 axiom fetch_pseudo_instruction: 654 ∀p : list labelled_instruction.654 ∀ps: PseudoStatus. 655 655 ∀pc: Word. 656 656 (pseudo_instruction × Word) × nat. … … 659 659 axiom address_of_word_labels: Identifier → Word. 660 660 661 definition execute_1_pseudo_instruction: pseudo_assembly_program → Status → Status ≝ 662 λp. 661 definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus ≝ 663 662 λs. 664 let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction (\snd p) (program_counters) in663 let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) in 665 664 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 666 let s ≝ set_clock s (clocks + ticks) in667 let s ≝ set_program_counter s pc in665 let s ≝ set_clock ? s (clock ? s + ticks) in 666 let s ≝ set_program_counter ? s pc in 668 667 let s ≝ 669 668 match instr with 670 [ Instruction instr ⇒ execute_1_preinstruction ?address_of_labels instr s669 [ Instruction instr ⇒ execute_1_preinstruction … address_of_labels instr s 671 670  Comment cmt ⇒ s 672 671  Cost cst ⇒ s 673  Jmp jmp ⇒ set_program_counter s (address_of_word_labels jmp)672  Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels jmp) 674 673  Call call ⇒ 675 674 let a ≝ address_of_word_labels call in 676 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in677 let s ≝ set_8051_sfr s SFR_SP new_sp in678 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in679 let s ≝ write_at_stack_pointer s pc_bl in680 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in681 let s ≝ set_8051_sfr s SFR_SP new_sp in682 let s ≝ write_at_stack_pointer s pc_bu in683 set_program_counter s a684  Mov dptr ident ⇒ set_arg_16 s (get_arg_16s (DATA16 (address_of_word_labels ident))) dptr675 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 676 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 677 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 678 let s ≝ write_at_stack_pointer ? s pc_bl in 679 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 680 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 681 let s ≝ write_at_stack_pointer ? s pc_bu in 682 set_program_counter ? s a 683  Mov dptr ident ⇒ set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels ident))) dptr 685 684 ] 686 685 in … … 696 695 ]. 697 696 698 let rec execute_pseudo_instruction (n: nat) ( p: pseudo_assembly_program) (s: Status) on n:Status ≝697 let rec execute_pseudo_instruction (n: nat) (s: PseudoStatus) on n: PseudoStatus ≝ 699 698 match n with 700 699 [ O ⇒ s 701  S o ⇒ execute_pseudo_instruction o p (execute_1_pseudo_instruction ps)700  S o ⇒ execute_pseudo_instruction o (execute_1_pseudo_instruction s) 702 701 ].
Note: See TracChangeset
for help on using the changeset viewer.