Changeset 307


Ignore:
Timestamp:
Nov 26, 2010, 12:25:19 AM (9 years ago)
Author:
sacerdot
Message:

assembly1 completed, but two cases commented out since they require infinite
time (why??)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Assembly.ma

    r306 r307  
    400400          | DATA b2 ⇒ λ_.
    401401             [ ([[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)]].
    406403
    407404(*
    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  ].
     405let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty
     406
     407let load_mem mem status = { status with code_memory = mem }
     408let load l = load_mem (load_code_memory l)
     409
     410module StringMap = Map.Make(String);;
     411module IntMap = Map.Make(struct type t = int let compare = compare end);;
     412
     413
     414let 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
     427let 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;;
    518482*)
Note: See TracChangeset for help on using the changeset viewer.