Changeset 307 for Deliverables
 Timestamp:
 Nov 26, 2010, 12:25:19 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Assembly.ma
r306 r307 400 400  DATA b2 ⇒ λ_. 401 401 [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ] 402  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 403 404  _ ⇒ [ ]]. 405 402  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]]. 406 403 407 404 (* 408 nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ { 409 elem:> A; 410 witness: T elem 411 }. 412 413 interpretation "Sigma" 'sigma T = (Sigma ? T). 414 415 naxiom daemon: False. 416 417 naxiom decode_register: Vector Bool (S (S (S Z))) → [reg]. 418 naxiom decode_direct: Vector Bool (S (S (S Z))) → [direct]. 419 420 ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction)) 421 ≝ 422 [mk_Cartesian ?? 423 (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true]) 424 (λl. 425 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 426 (mk_subaddressing_mode ? ? (decode_register l) ?)); 427 mk_Cartesian ?? 428 (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true]) 429 (λl. 430 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 431 (mk_subaddressing_mode ? ? (decode_direct l) ?)) ]. 432 ncases daemon. 433 nqed. 434 435 436 naxiom decode_register: List Bool → [reg]. 437 naxiom decode_direct: List Bool → [direct]. 438 439 ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction)) 440 ≝ 441 [mk_Cartesian ?? 442 [ false; false; true; false; true] 443 (λl. 444 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 445 (mk_subaddressing_mode ? ? (decode_register l) ?)); 446 mk_Cartesian ?? 447 [ false; false; true; false; true] 448 (λl. 449 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 450 (mk_subaddressing_mode ? ? (decode_direct l) ?)) ]. 451 ncases daemon. 452 nqed. 453 454 455 ndefinition decode_tbl1: 456 List (List Bool × Σaddr:all_types. [addr] → Instruction) 457 ≝ 458 [mk_Cartesian ?? 459 [ false; false; true; false; true] 460 (mk_Sigma ? (λaddr:all_types. [addr] → Instruction) 461 reg 462 (λa. 463 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 464 (mk_subaddressing_mode ? ? a ?))) ]. 465 ncases daemon. 466 nqed. 467 468 ndefinition decode_tbl2: 469 List (List Bool × Σaddr:all_types. [addr] → Instruction) 470 ≝ 471 [mk_Cartesian ?? 472 [ false; false; true; false; false; true; false; true] 473 (mk_Sigma ? (λaddr:all_types. [addr] → Instruction) 474 direct 475 (λa. 476 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 477 (mk_subaddressing_mode ? ? a ?))) ]. 478 ncases daemon. 479 nqed. 480 481 ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2. 482 483 decode_addr_mode; ∀addr:all_types. List Bool → [addr]. 484 485 decode ≝ 486 λl:List Bit. 487 List.iter 488 (fun l0 addr mk_f → 489 match split_prefix l l0 with 490 [ None ⇒ ... 491  Some r ⇒ mk_f (decode_addr_mode r) ] 492 493 ) decode_tbl 494 495 encode ≝ 496 497 ndefinition decode_tbl: 498 List (List Bool × Σaddr:all_types. [addr] → Instruction) 499 ≝ 500 [mk_Cartesian ?? 501 [ False; False; True; False; True] 502 (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction) 503 reg 504 (λa:subaddressing_mode ? [reg]. 505 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 506 (mk_subaddressing_mode ? ? a ?))); 507 mk_Cartesian ?? 508 [ False; False; True; False; False; True; False; True] 509 (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction) 510 direct 511 (λa:subaddressing_mode ? [direct]. 512 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 513 (mk_subaddressing_mode ? ? a ?))) 514 ]. 515 nnormalize; 516 517 ]. 405 let load_code_memory = fold_lefti (fun i mem v > WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty 406 407 let load_mem mem status = { status with code_memory = mem } 408 let load l = load_mem (load_code_memory l) 409 410 module StringMap = Map.Make(String);; 411 module IntMap = Map.Make(struct type t = int let compare = compare end);; 412 413 414 let assembly_jump addr_of = 415 function 416 `JC a1 > `JC (addr_of a1) 417  `JNC a1 > `JNC (addr_of a1) 418  `JB (a1,a2) > `JB (a1,addr_of a2) 419  `JNB (a1,a2) > `JNB (a1,addr_of a2) 420  `JBC (a1,a2) > `JBC (a1,addr_of a2) 421  `JZ a1 > `JZ (addr_of a1) 422  `JNZ a1 > `JNZ (addr_of a1) 423  `CJNE (a1,a2) > `CJNE (a1,addr_of a2) 424  `DJNZ (a1,a2) > `DJNZ (a1,addr_of a2) 425 ;; 426 427 let assembly (preamble,l) = 428 let datalabels,_ = 429 List.fold_left 430 (fun (datalabels,addr) (name,size) > 431 let addr16 = vect_of_int addr `Sixteen in 432 StringMap.add name addr16 datalabels, addr+size 433 ) (StringMap.empty,0) preamble 434 in 435 let pc,labels,costs = 436 List.fold_left 437 (fun (pc,labels,costs) i > 438 match i with 439 `Label s > pc, StringMap.add s pc labels, costs 440  `Cost s > pc, labels, IntMap.add pc s costs 441  `Mov (_,_) > pc, labels, costs 442  `Jmp _ 443  `Call _ > pc + 3, labels, costs (*CSC: very stupid: always expand to worst opcode *) 444  `WithLabel i > 445 let fake_addr _ = `REL (zero `Eight) in 446 let fake_jump = assembly_jump fake_addr i in 447 let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in 448 assert (fake_jump = i'); 449 (pc + int_of_vect pc',labels, costs) 450  #instruction as i > 451 let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in 452 assert (i = i'); 453 (pc + int_of_vect pc',labels, costs) 454 ) (0,StringMap.empty,IntMap.empty) l 455 in 456 if pc >= 65536 then 457 raise CodeTooLarge 458 else 459 List.flatten (List.map 460 (function 461 `Label _ 462  `Cost _ > [] 463  `WithLabel i > 464 let addr_of (`Label s) = 465 let addr = StringMap.find s labels in 466 (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *) 467 assert (addr < 256); 468 `REL (vect_of_int addr `Eight) 469 in 470 assembly1 (assembly_jump addr_of i) 471  `Mov (`DPTR,s) > 472 let addrr16 = StringMap.find s datalabels in 473 assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16))) 474  `Jmp s > 475 let pc_offset = StringMap.find s labels in 476 assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen))) 477  `Call s > 478 let pc_offset = StringMap.find s labels in 479 assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen))) 480  #instruction as i > assembly1 i) l), costs 481 ;; 518 482 *)
Note: See TracChangeset
for help on using the changeset viewer.