Changeset 421 for Deliverables


Ignore:
Timestamp:
Dec 14, 2010, 4:13:55 PM (9 years ago)
Author:
mulligan
Message:

Removed duplicate "assembly1" function. Removed Ocaml code from file.

File:
1 edited

Legend:

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

    r420 r421  
    528528
    529529(*
    530 let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty
    531 
    532 let load_mem mem status = { status with code_memory = mem }
    533 let load l = load_mem (load_code_memory l)
    534 
    535 module StringMap = Map.Make(String);;
    536 module IntMap = Map.Make(struct type t = int let compare = compare end);;
    537 
    538 
    539 let assembly_jump addr_of =
    540  function
    541     `JC a1 -> `JC (addr_of a1)
    542   | `JNC a1 -> `JNC (addr_of a1)
    543   | `JB (a1,a2) -> `JB (a1,addr_of a2)
    544   | `JNB (a1,a2) -> `JNB (a1,addr_of a2)
    545   | `JBC (a1,a2) -> `JBC (a1,addr_of a2)
    546   | `JZ a1 -> `JZ (addr_of a1)
    547   | `JNZ a1 -> `JNZ (addr_of a1)
    548   | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2)
    549   | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2)
    550 ;;
    551 
    552 let assembly (preamble,l) =
    553  let datalabels,_ =
    554   List.fold_left
    555    (fun (datalabels,addr) (name,size) ->
    556      let addr16 = vect_of_int addr `Sixteen in
    557       StringMap.add name addr16 datalabels, addr+size
    558    ) (StringMap.empty,0) preamble
    559  in
    560  let pc,labels,costs =
    561   List.fold_left
    562    (fun (pc,labels,costs) i ->
    563      match i with
    564         `Label s -> pc, StringMap.add s pc labels, costs
    565       | `Cost s -> pc, labels, IntMap.add pc s costs
    566       | `Mov (_,_) -> pc, labels, costs
    567       | `Jmp _
    568       | `Call _ -> pc + 3, labels, costs  (*CSC: very stupid: always expand to worst opcode *)
    569       | `WithLabel i ->
    570           let fake_addr _ = `REL (zero `Eight) in
    571           let fake_jump = assembly_jump fake_addr i in
    572           let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
    573            assert (fake_jump = i');
    574            (pc + int_of_vect pc',labels, costs)
    575       | #instruction as i ->
    576         let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
    577          assert (i = i');
    578          (pc + int_of_vect pc',labels, costs)
    579    ) (0,StringMap.empty,IntMap.empty) l
    580  in
    581   if pc >= 65536 then
    582    raise CodeTooLarge
    583   else
    584       List.flatten (List.map
    585          (function
    586             `Label _
    587           | `Cost _ -> []
    588           | `WithLabel i ->
    589               let addr_of (`Label s) =
    590                let addr = StringMap.find s labels in
    591                (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
    592                 assert (addr < 256);
    593                 `REL (vect_of_int addr `Eight)
    594               in
    595                assembly1 (assembly_jump addr_of i)
    596           | `Mov (`DPTR,s) ->
    597               let addrr16 = StringMap.find s datalabels in
    598                assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
    599           | `Jmp s ->
    600               let pc_offset = StringMap.find s labels in
    601                 assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen)))
    602           | `Call s ->
    603               let pc_offset = StringMap.find s labels in
    604                 assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen)))
    605           | #instruction as i -> assembly1 i) l), costs
    606 ;;
    607 *)
    608 
    609530ndefinition assembly: List instruction → List Byte ≝
    610531 fold_right … (λi,l. assembly1 i @ l) [].
     532*)
Note: See TracChangeset for help on using the changeset viewer.