Changeset 410 for Deliverables


Ignore:
Timestamp:
Dec 13, 2010, 5:00:02 PM (9 years ago)
Author:
mulligan
Message:

Using bitvectortries for a dictionary doesn't work even if we hypothesise conversion functions from bitvectors to string, and back again. Many changes, including most of the assembly function implemented.

Location:
Deliverables/D4.1/Matita
Files:
2 added
5 edited

Legend:

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

    r374 r410  
    195195 | Call: String → labelled_instruction
    196196 | Mov: [[dptr]] → String → labelled_instruction
    197  | WithLabel: preinstruction String → labelled_instruction.
     197 | Label: String → labelled_instruction
     198 | WithLabel: jump String → labelled_instruction.
    198199
    199200ndefinition preamble ≝ List (String × Nat).
  • Deliverables/D4.1/Matita/Assembly.ma

    r341 r410  
    11include "ASM.ma".
     2include "BitVectorTrie.ma".
    23
    34ndefinition assembly1 ≝
     
    400401          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].
    401402
     403include "Arithmetic.ma".
     404include "Fetch.ma".
     405include "Status.ma".
     406
     407ndefinition 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
     423ndefinition 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
    402489(*
    403490let 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  
    77
    88include "Vector.ma".
     9include "String.ma".
    910
    1011(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    217218        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    218219    ].
     220   
     221naxiom bitvector_of_string:
     222  ∀n: Nat.
     223  ∀s: String.
     224    BitVector n.
     225   
     226naxiom string_of_bitvector:
     227  ∀n: Nat.
     228  ∀b: BitVector n.
     229    String.
  • Deliverables/D4.1/Matita/Nat.ma

    r363 r410  
    719719ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
    720720ndefinition 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.
     722ndefinition 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  
    1515Connectives.ma Plogic/equality.ma
    1616Bool.ma Universes.ma
    17 Assembly.ma ASM.ma
     17Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
    1818List.ma Maybe.ma Util.ma
    1919Interpret.ma Fetch.ma Status.ma
    2020Util.ma Nat.ma
    21 BitVector.ma Vector.ma
     21BitVector.ma String.ma Vector.ma
    2222String.ma Char.ma List.ma
    2323Plogic/equality.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.