Changeset 410
- Timestamp:
- Dec 13, 2010, 5:00:02 PM (9 years ago)
- Location:
- Deliverables/D4.1/Matita
- Files:
-
- 2 added
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/ASM.ma
r374 r410 195 195 | Call: String → labelled_instruction 196 196 | Mov: [[dptr]] → String → labelled_instruction 197 | WithLabel: preinstruction String → labelled_instruction. 197 | Label: String → labelled_instruction 198 | WithLabel: jump String → labelled_instruction. 198 199 199 200 ndefinition preamble ≝ List (String × Nat). -
Deliverables/D4.1/Matita/Assembly.ma
r341 r410 1 1 include "ASM.ma". 2 include "BitVectorTrie.ma". 2 3 3 4 ndefinition assembly1 ≝ … … 400 401 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]]. 401 402 403 include "Arithmetic.ma". 404 include "Fetch.ma". 405 include "Status.ma". 406 407 ndefinition assembly_jump ≝ 408 λA, B: Type[0]. 409 λj. 410 λaddr_of: A → B. 411 match j with 412 [ JC jmp ⇒ JC ? (addr_of jmp) 413 | JNC jmp ⇒ JNC ? (addr_of jmp) 414 | JZ jmp ⇒ JZ ? (addr_of jmp) 415 | JNZ jmp ⇒ JNZ ? (addr_of jmp) 416 | JB jmp jmp' ⇒ JB ? jmp (addr_of jmp') 417 | JNB jmp jmp' ⇒ JNB ? jmp (addr_of jmp') 418 | JBC jmp jmp' ⇒ JBC ? jmp (addr_of jmp') 419 | CJNE jmp jmp' ⇒ CJNE ? jmp (addr_of jmp') 420 | DJNZ jmp jmp' ⇒ DJNZ ? jmp (addr_of jmp') 421 ]. 422 423 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie ? sixteen)) ≝ 424 λp. 425 let 〈preamble, instr_list〉 ≝ p in 426 let 〈datalabels, ignore〉 ≝ 427 fold_left ? ? ( 428 λt. λpreamble. 429 let 〈datalabels, addr〉 ≝ t in 430 let 〈name, size〉 ≝ preamble in 431 let addr_sixteen ≝ bitvector_of_nat sixteen addr in 432 〈insert ? ? addr_sixteen name datalabels, addr + size〉) 433 〈(Stub ? ?), Z〉 preamble in 434 let 〈pc_labels, costs〉 ≝ 435 fold_left ? ? ( 436 λt. λi. 437 let 〈pc_labels, costs〉 ≝ t in 438 let 〈program_counter, labels〉 ≝ pc_labels in 439 match i with 440 [ Instruction instr ⇒ 441 let code_memory ≝ load_code_memory (assembly1 instr) in 442 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in 443 let 〈instr', program_counter'〉 ≝ instr_pc' in 444 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in 445 〈〈program_counter + program_counter_n', labels〉, costs〉 446 | Label label ⇒ 447 let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in 448 〈〈program_counter, (insert ? ? program_counter_bv label labels)〉, costs〉 449 | Cost cost ⇒ 450 let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in 451 〈pc_labels, (insert ? ? program_counter_bv cost costs)〉 452 | Jmp jmp ⇒ 453 〈〈program_counter + three, labels〉, costs〉 454 | Call call ⇒ 455 〈〈program_counter + three, labels〉, costs〉 456 | Mov dptr trgt ⇒ t 457 | WithLabel jmp ⇒ ? (* 458 let fake_addr ≝ RELATIVE (zero eight) in 459 let fake_jump ≝ assembly_jump ? ? jmp (λx. fake_addr) in 460 let code_memory ≝ load_code_memory (assembly1 (Jump relative fake_jump)) in 461 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in 462 let 〈instr', program_counter'〉 ≝ instr_pc' in 463 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in 464 〈〈program_counter + program_counter_n', labels〉, costs〉 *) 465 ] 466 ) 〈〈Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in 467 let 〈program_counter, labels〉 ≝ pc_labels in 468 if greater_than_b program_counter 469 sixty_five_thousand_five_hundred_and_thirty_six then 470 Nothing ? 471 else 472 let flat_list ≝ 473 flatten ? ( 474 map ? ? ( 475 λi: labelled_instruction. 476 match i with 477 [ Cost cost ⇒ [ ] 478 | Label label ⇒ [ ] 479 | Call call ⇒ 480 let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in 481 let address ≝ ADDR16 (bitvector_of_nat sixteen pc_offset) in 482 assembly1 (LCALL address) 483 | _ ⇒ ? 484 ] 485 ) instr_list 486 ) in 487 Just ? 〈flat_list, costs〉. 488 402 489 (* 403 490 let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty -
Deliverables/D4.1/Matita/BitVector.ma
r374 r410 7 7 8 8 include "Vector.ma". 9 include "String.ma". 9 10 10 11 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 217 218 ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl 218 219 ]. 220 221 naxiom bitvector_of_string: 222 ∀n: Nat. 223 ∀s: String. 224 BitVector n. 225 226 naxiom string_of_bitvector: 227 ∀n: Nat. 228 ∀b: BitVector n. 229 String. -
Deliverables/D4.1/Matita/Nat.ma
r363 r410 719 719 ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen. 720 720 ndefinition two_hundred_and_fifty_six ≝ 721 one_hundred_and_twenty_eight + one_hundred_and_twenty_eight. 721 one_hundred_and_twenty_eight + one_hundred_and_twenty_eight. 722 ndefinition sixty_five_thousand_five_hundred_and_thirty_six ≝ 723 two_hundred_and_fifty_six * two_hundred_and_fifty_six. -
Deliverables/D4.1/Matita/depends
r364 r410 15 15 Connectives.ma Plogic/equality.ma 16 16 Bool.ma Universes.ma 17 Assembly.ma ASM.ma 17 Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma 18 18 List.ma Maybe.ma Util.ma 19 19 Interpret.ma Fetch.ma Status.ma 20 20 Util.ma Nat.ma 21 BitVector.ma Vector.ma21 BitVector.ma String.ma Vector.ma 22 22 String.ma Char.ma List.ma 23 23 Plogic/equality.ma Universes.ma
Note: See TracChangeset
for help on using the changeset viewer.