Changeset 832


Ignore:
Timestamp:
May 24, 2011, 6:40:13 PM (8 years ago)
Author:
mulligan
Message:

work from today

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r820 r832  
    111111  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
    112112 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
    113 
     113 
    114114inductive preinstruction (A: Type[0]) : Type[0] ≝
    115115  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
  • src/ASM/Assembly.ma

    r825 r832  
    410410qed.
    411411
    412 definition assembly_expansion ≝
     412inductive jump_length: Type[0] ≝
     413  | short_jump: jump_length
     414  | medium_jump: jump_length
     415  | long_jump: jump_length.
     416
     417axiom jump_expansion_policy:
     418  ∀program: pseudo_assembly_program.
     419  ∀pc: Word.
     420    jump_length.
     421
     422definition expand_relative_jump_internal ≝
     423  λjmp_len.
    413424  λi.
    414   λcosts: BitVectorTrie Identifier 16.
    415   λprogram_counter: nat.
    416             match i with
    417               [ Instruction instr ⇒
    418                 let code_memory ≝ load_code_memory (assembly_preinstruction Identifier (λx. zero 8) instr) in
    419                 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
    420                 let 〈instr', program_counter'〉 ≝ instr_pc' in
    421                 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
    422                   〈program_counter + program_counter_n', costs〉
    423               | Comment comment ⇒ 〈program_counter, costs〉
    424               | Cost cost ⇒
    425                 let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    426                   〈program_counter, (insert ? ? program_counter_bv cost costs)〉
    427               | Jmp jmp ⇒
    428                   〈program_counter + 3, costs〉
    429               | Call call ⇒
    430                   〈program_counter + 3, costs〉
    431               | Mov dptr trgt ⇒ 〈program_counter, costs〉
    432               ].
    433 
    434 definition assembly_1_pseudoinstruction ≝
     425  match jmp_len with
     426  [ short_jump ⇒ Some ? [ i ]
     427  | medium_jump ⇒ None ?
     428  | long_jump ⇒
     429    Some ? [ RealInstruction i;
     430      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
     431      LJMP (ADDR16 (bitvector_of_nat ? 0)) (* fill in *)
     432    ]
     433  ].
     434  @ I
     435qed.
     436
     437definition expand_relative_jump: jump_length → preinstruction Identifier → option (list instruction) ≝
     438  λjmp_len: jump_length.
     439  λi: preinstruction Identifier.
     440  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
     441  match i with
     442  [ JC jmp ⇒ expand_relative_jump_internal jmp_len (JC ? rel_jmp)
     443  | JNC jmp ⇒ expand_relative_jump_internal jmp_len (JNC ? rel_jmp)
     444  | JB baddr jmp ⇒ expand_relative_jump_internal jmp_len (JB ? baddr rel_jmp)
     445  | JZ jmp ⇒ expand_relative_jump_internal jmp_len (JZ ? rel_jmp)
     446  | JNZ jmp ⇒ expand_relative_jump_internal jmp_len (JNZ ? rel_jmp)
     447  | JBC baddr jmp ⇒ expand_relative_jump_internal jmp_len (JBC ? baddr rel_jmp)
     448  | JNB baddr jmp ⇒ expand_relative_jump_internal jmp_len (JNB ? baddr rel_jmp)
     449  | CJNE addr jmp ⇒ expand_relative_jump_internal jmp_len (CJNE ? addr rel_jmp)
     450  | DJNZ addr jmp ⇒ expand_relative_jump_internal jmp_len (DJNZ ? addr rel_jmp)
     451  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
     452  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
     453  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
     454  | INC arg ⇒ Some ? [ INC ? arg ]
     455  | DEC arg ⇒ Some ? [ DEC ? arg ]
     456  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
     457  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
     458  | DA arg ⇒ Some ? [ DA ? arg ]
     459  | ANL arg ⇒ Some ? [ ANL ? arg ]
     460  | ORL arg ⇒ Some ? [ ORL ? arg ]
     461  | XRL arg ⇒ Some ? [ XRL ? arg ]
     462  | CLR arg ⇒ Some ? [ CLR ? arg ]
     463  | CPL arg ⇒ Some ? [ CPL ? arg ]
     464  | RL arg ⇒ Some ? [ RL ? arg ]
     465  | RR arg ⇒ Some ? [ RR ? arg ]
     466  | RLC arg ⇒ Some ? [ RLC ? arg ]
     467  | RRC arg ⇒ Some ? [ RRC ? arg ]
     468  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
     469  | MOV arg ⇒ Some ? [ MOV ? arg ]
     470  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
     471  | SETB arg ⇒ Some ? [ SETB ? arg ]
     472  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
     473  | POP arg ⇒ Some ? [ POP ? arg ]
     474  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
     475  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
     476  | RET ⇒ Some ? [ RET ? ]
     477  | RETI ⇒ Some ? [ RETI ? ]
     478  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
     479  ].
     480  @ I
     481qed.
     482
     483definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
    435484  λlookup_labels.
    436485  λlookup_datalabels.
    437   λaddress_of.
    438   λi: labelled_instruction.
    439                 match \snd i with
    440                   [ Cost cost ⇒ [ ]
    441                   | Comment comment ⇒ [ ]
    442                   | Call call ⇒
    443                     let address ≝ ADDR16 (lookup_labels call) in
    444                       assembly1 (LCALL address)
    445                   | Mov d trgt ⇒
    446                     let address ≝ DATA16 (lookup_datalabels trgt) in
    447                       assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
    448                   | Instruction instr ⇒ assembly_preinstruction ? address_of instr
    449                   | Jmp jmp ⇒
    450                     let address ≝ ADDR16 (lookup_labels jmp) in
    451                       assembly1 (LJMP address)
    452 (*                  | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels))
    453 *)
    454                   ].
     486  λpc.
     487  λjmp_len.
     488  λi.
     489  match i with
     490  [ Cost cost ⇒ Some ? [ ]
     491  | Comment comment ⇒ Some ? [ ]
     492  | Call call ⇒
     493    match jmp_len with
     494    [ short_jump ⇒ None ?
     495    | medium_jump ⇒
     496      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
     497      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
     498      if eq_bv ? ignore fst_5 then
     499        let address ≝ ADDR11 address in
     500          Some ? ([ ACALL address ])
     501      else
     502        None ?
     503    | long_jump ⇒
     504      let address ≝ ADDR16 (lookup_labels call) in
     505        Some ? [ LCALL address ]
     506    ]
     507  | Mov d trgt ⇒
     508    let address ≝ DATA16 (lookup_datalabels trgt) in
     509      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
     510  | Instruction instr ⇒ expand_relative_jump jmp_len instr
     511  | Jmp jmp ⇒
     512    match jmp_len with
     513    [ short_jump ⇒
     514      let lookup_address ≝ lookup_labels jmp in
     515      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
     516      let 〈upper, lower〉 ≝ split ? 8 8 result in
     517      if eq_bv ? upper (zero 8) then
     518        let address ≝ RELATIVE lower in
     519          Some ? [ SJMP address ]
     520      else
     521        None ?
     522    | medium_jump ⇒
     523      let address ≝ lookup_labels jmp in
     524      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
     525      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
     526      if eq_bv ? fst_5_addr fst_5_pc then
     527        let address ≝ ADDR11 rest_addr in
     528          Some ? ([ AJMP address ])
     529      else
     530        None ?
     531    | long_jump ⇒
     532      let address ≝ ADDR16 (lookup_labels jmp) in
     533        Some ? [ LJMP address ]
     534    ]
     535  ].
    455536  @ I
    456537qed.
     538
     539definition assembly_1_pseudoinstruction ≝
     540  λprogram.
     541  λpc.
     542  λlookup_labels.
     543  λlookup_datalabels.
     544  λi.
     545  let expansion ≝ jump_expansion_policy program pc in
     546    match (expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i) with
     547    [ None ⇒ None ?
     548    | Some pseudos ⇒ Some ? (flatten ? (map ? ? assembly1 pseudos))
     549    ].
    457550
    458551definition construct_datalabels ≝
     
    466559          〈(Stub ? ?), 0〉 preamble).
    467560
    468 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    469   λp.
    470     let 〈preamble, instr_list〉 ≝ p in
    471     let datalabels ≝ construct_datalabels preamble in
    472     let 〈labels,pc_costs〉 ≝
    473       foldl ((BitVectorTrie ? ?) × (nat  × (BitVectorTrie ? ?))) ? (
    474         λt. λi.
    475           let 〈label, i〉 ≝ i in
    476           let 〈labels, pc_costs〉 ≝ t in
    477           let 〈program_counter, costs〉 ≝ pc_costs in
    478           let labels ≝ match label with
    479           [ None ⇒ labels
    480           | Some label ⇒
    481             let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    482               insert ? ? label program_counter_bv labels
    483           ] in
    484           〈labels, assembly_expansion i costs program_counter〉
    485           ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in
    486     let 〈program_counter, costs〉 ≝ pc_costs in
    487       if gtb program_counter (2^16) then (* 65536 *)
     561definition is_jump ≝
     562  λi: preinstruction Identifier.
     563  match i with
     564  [ JC _ ⇒ true
     565  | JNC _ ⇒ true
     566  | JB _ _ ⇒ true
     567  | JNB _ _ ⇒ true
     568  | JBC _ _ ⇒ true
     569  | JZ _ ⇒ true
     570  | JNZ _ ⇒ true
     571  | CJNE _ _ ⇒ true
     572  | DJNZ _ _ ⇒ true
     573  | _ ⇒ false
     574  ].
     575
     576definition construct_costs ≝
     577  λprogram.
     578  λprogram_counter: nat.
     579  λlookup_labels.
     580  λlookup_datalabels.
     581  λcosts: BitVectorTrie Word 16.
     582  λi.
     583  match i with
     584  [ Comment comment ⇒ Some ? 〈program_counter, costs〉
     585  | Cost cost ⇒
     586    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
     587      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
     588  | _ ⇒
     589    let pc_bv ≝ bitvector_of_nat ? program_counter in
     590    let assembled ≝ assembly_1_pseudoinstruction program pc_bv
     591                     lookup_labels lookup_datalabels i in
     592    match assembled with
     593    [ None ⇒ None ?
     594    | Some assembled ⇒
     595      let code_memory ≝ load_code_memory assembled in
     596      let pc ≝ foldr ? ? (λy. λpc.
     597          let 〈instr_pc', ignore〉 ≝ fetch code_memory pc in
     598          let 〈instr', program_counter'〉 ≝ instr_pc' in
     599            program_counter') (zero ?) assembled in
     600      Some ? 〈(nat_of_bitvector 16 pc) + program_counter, costs〉       
     601    ]
     602  ].
     603
     604definition build_maps ≝
     605  λinstr_list.
     606  let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))) ?
     607    (λt. λi.
     608       let 〈label, i〉 ≝ i in
     609       match t with
     610       [ None ⇒ None ?
     611       | Some t ⇒
     612         let 〈labels, pc_costs〉 ≝ t in
     613         let 〈program_counter, costs〉 ≝ pc_costs in
     614         let labels ≝
     615           match label with
     616           [ None ⇒ labels
     617           | Some label ⇒
     618             let program_counter_bv ≝ bitvector_of_nat ? program_counter in
     619               insert ? ? label program_counter_bv labels
     620           ]
     621         in
     622           match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) costs i with
     623           [ None ⇒ None ?
     624           | Some construct ⇒ Some ? 〈labels, construct〉
     625           ]
     626       ]) (Some ? 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉) (\snd instr_list) in
     627  match result with
     628  [ None ⇒ None ?
     629  | Some result ⇒
     630    let 〈labels, pc_costs〉 ≝ result in
     631    let 〈pc, costs〉 ≝ pc_costs in
     632      if gtb pc (2^16) then
    488633        None ?
    489634      else
    490         let flat_list ≝ flatten ? (
    491           map ? ? (
    492             assembly_1_pseudoinstruction (
    493               λx. lookup ? ? x labels (zero ?))
    494                 (λx. lookup ? ? x datalabels (zero ?))
    495                 (address_of labels)) instr_list) in
    496         Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
     635        Some ? 〈labels, costs〉
     636  ].
     637
     638check lookup.
     639
     640definition assembly ≝
     641  λp.
     642  λpc.
     643    let 〈preamble, instr_list〉 ≝ p in
     644    match build_maps p with
     645    [ None ⇒ None ?
     646    | Some maps ⇒
     647      let labels ≝ \fst maps in
     648      let datalabels ≝ construct_datalabels preamble in
     649      match build_maps p with
     650      [ None ⇒ None ?
     651      | Some labels_costs ⇒
     652        let 〈labels,costs〉 ≝ labels_costs in
     653        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
     654        let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
     655        let to_flatten ≝ map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels x) instr_list in
     656        (*
     657          foldr ? ? (λx. λy.
     658            match y with
     659            [ None ⇒ None ?
     660            | Some lst ⇒
     661              match x with
     662              [ None ⇒ None ?
     663              | Some x ⇒ Some ? (x @ lst)
     664              ]
     665            ]) (Some ? [ ]) to_flatten *) ?
     666      ]
     667    ].
     668   
     669(*
     670        if  then (* 65536 *)
     671          None ?
     672        else
     673          let flat_list ≝ flatten ? (
     674            map ? ? (
     675              assembly_1_pseudoinstruction (
     676                λx. lookup ? ? x labels (zero ?))
     677                  (λx. lookup ? ? x datalabels (zero ?))
     678                  (address_of labels)) instr_list) in
     679          Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉
     680*)
     681
    497682(*
    498683  [2,3,4,5,6:
     
    511696qed. *)
    512697
     698
     699
    513700definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    514701 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
  • src/ASM/AssemblyProof.ma

    r831 r832  
    5050      # H
    5151      whd
    52       normalize
     52      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    5353    ]
    5454  | cases not_implemented
Note: See TracChangeset for help on using the changeset viewer.