Changeset 1515 for src/ASM


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
Location:
src/ASM
Files:
7 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASM.ma

    r1493 r1515  
    11include "ASM/BitVector.ma".
    2 
    3 definition Identifier ≝ Word.
     2include "common/Identifiers.ma".
     3include "common/CostLabel.ma".
     4
     5axiom ASMTag : String.
     6definition Identifier ≝ identifier ASMTag.
     7definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].
    48
    59inductive addressing_mode: Type[0] ≝
    … …  
    194198  | Instruction: preinstruction Identifier → pseudo_instruction
    195199  | Comment: String → pseudo_instruction
    196   | Cost: Identifier → pseudo_instruction
     200  | Cost: costlabel → pseudo_instruction
    197201  | Jmp: Identifier → pseudo_instruction
    198202  | Call: Identifier → pseudo_instruction

  • src/ASM/Erase.ma

    r1463 r1515  
    11include "ASM/ASM.ma".
    2 include "ASM/BitVectorTrie.ma".
    3      
     2
    43let rec pre_erase
    54  (the_program: list labelled_instruction) (labels: list Identifier)
    6     on the_program: ((BitVectorTrie Identifier 16) × (list labelled_instruction)) ≝
     5    on the_program: ((identifier_map ASMTag Identifier) × (list labelled_instruction)) ≝
    76  match the_program with
    87  [ nil        ⇒
    98    match labels with
    10     [ nil ⇒ 〈Stub Identifier 16, [ ]〉 (* XXX: labels should be empty *)
     9    [ nil ⇒ 〈empty_map ??, [ ]〉 (* XXX: labels should be empty *)
    1110    | _   ⇒ ⊥
    1211    ]
    … …  
    2524        | _ ⇒
    2625          let 〈maps, the_program〉 ≝ pre_erase tl [ ] in
    27           let maps ≝ foldr … (λl. λmap. insert … l label map) maps (label::labels) in
     26          let maps ≝ foldr ?? (λl. λmap. add … map l label) maps (label::labels) in
    2827            〈maps, the_program〉
    2928        ]
    … …  
    3332qed.
    3433
    35 definition relabel_instruction: preinstruction Identifier → BitVectorTrie Identifier 16 → preinstruction Identifier ≝
     34definition relabel_instruction: preinstruction Identifier → identifier_map ASMTag Identifier → preinstruction Identifier ≝
    3635  λpre.
    3736  λmap.
    3837  match pre with
    3938  [ JC ident ⇒
    40     let located ≝ lookup … ident map ident in
     39    let located ≝ lookup_def … map ident ident in
    4140      JC … located
    4241  | JNC ident ⇒
    43     let located ≝ lookup … ident map ident in
     42    let located ≝ lookup_def … map ident ident in
    4443      JNC … located
    4544  | JB bit ident ⇒
    46     let located ≝ lookup … ident map ident in
     45    let located ≝ lookup_def … map ident ident in
    4746      JB … bit located
    4847  | JNB bit ident ⇒
    49     let located ≝ lookup … ident map ident in
     48    let located ≝ lookup_def … map ident ident in
    5049      JNB … bit located
    5150  | JBC bit ident ⇒
    52     let located ≝ lookup … ident map ident in
     51    let located ≝ lookup_def … map ident ident in
    5352      JBC … bit located
    5453  | JZ ident ⇒
    55     let located ≝ lookup … ident map ident in
     54    let located ≝ lookup_def … map ident ident in
    5655      JZ … located
    5756  | JNZ ident ⇒
    58     let located ≝ lookup … ident map ident in
     57    let located ≝ lookup_def … map ident ident in
    5958      JNZ … located
    6059  | CJNE src ident ⇒
    61     let located ≝ lookup … ident map ident in
     60    let located ≝ lookup_def … map ident ident in
    6261      CJNE … src located
    6362  | DJNZ src ident ⇒
    64     let located ≝ lookup … ident map ident in
     63    let located ≝ lookup_def … map ident ident in
    6564      DJNZ … src located
    6665  (* XXX: no identifiers in rest of instructions *)
    … …  
    6867  ].
    6968
    70 definition relabel_pseudo_instruction: pseudo_instruction → BitVectorTrie Identifier 16 → pseudo_instruction ≝
     69definition relabel_pseudo_instruction: pseudo_instruction → identifier_map ASMTag Identifier → pseudo_instruction ≝
    7170  λpseudo.
    7271  λmap.
    … …  
    7675  | Comment comment ⇒ Comment comment
    7776  | Jmp ident ⇒
    78     let located ≝ lookup … ident map ident in
     77    let located ≝ lookup_def … map ident ident in
    7978      Jmp located
    8079  | Call ident ⇒
    81     let located ≝ lookup … ident map ident in
     80    let located ≝ lookup_def … map ident ident in
    8281      Call located
    8382  | Mov dptr ident ⇒
    84     let located ≝ lookup … ident map ident in
     83    let located ≝ lookup_def … map ident ident in
    8584      Mov dptr located
    8685  ].
    8786     
    8887let rec relabel
    89   (the_program: list labelled_instruction) (map: BitVectorTrie Identifier 16)
     88  (the_program: list labelled_instruction) (map: identifier_map ASMTag Identifier)
    9089    on the_program: list labelled_instruction ≝
    9190  match the_program with
    … …  
    9796      match label with
    9897      [ None ⇒ None …
    99       | Some label ⇒ Some … (lookup … ident map ident)
     98      | Some label ⇒ Some … (lookup_def … map ident ident)
    10099      ]
    101100    in

  • src/ASM/I8051.ma

    r1416 r1515  
    77include "utilities/Compare.ma".
    88include "joint/BEValues.ma".
     9include "ASM/BitVectorTrie.ma".
    910
    1011definition int_size ≝ bitvector_of_nat 8 1.

  • src/ASM/Interpret.ma

    r1514 r1515  
    686686      let preamble ≝ \fst (code_memory ? s) in
    687687      let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
    688         set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup ? ? ident data_labels (zero ?)))) dptr
     688        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
    689689    ]
    690690  in

  • src/ASM/Interpret2.ma

    r1478 r1515  
    2323 let s ≝ execute_1_pseudo_instruction ticks_of s in
    2424 match instr with
    25  [ Cost cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉
     25 [ Cost cst ⇒ ret … 〈Echarge cst, s〉
    2626 | _ ⇒ ret ? 〈E0, s〉 ].
    2727
    … …  
    3737
    3838(*CSC: move this definition elsewhere *)
    39 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie Identifier 16).
     39definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
    4040
    41 definition make_global: object_code → BitVectorTrie Identifier 16 ≝ \snd.
     41definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
    4242
    4343definition execute_1_instruction:
    44  BitVectorTrie Identifier 16 → Status → IO io_out io_in (trace × Status) ≝
     44 BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
    4545λcosts,s.
    4646 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
    … …  
    4949 match lookup_opt … pc costs with
    5050 [ None ⇒ ret … 〈E0, s〉
    51  | Some cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉 ].
     51 | Some cst ⇒ ret … 〈Echarge cst, s〉 ].
    5252
    53 axiom is_final: BitVectorTrie Identifier 16 → Status → option int.
     53axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
    5454
    5555definition exec: trans_system io_out io_in ≝

  • src/ASM/Status.ma

    r1459 r1515  
    702702  λr: BitVector 3.
    703703    let address ≝ bit_address_of_register ? s r in
    704       lookup … address (low_internal_ram ? s) (zero 8).
     704      lookup ?? address (low_internal_ram ? s) (zero 8).
    705705     
    706706definition set_register ≝
    … …  
    717717  λM: Type[0].
    718718  λs: PreStatus M.
    719     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
     719    let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_SP) in
    720720    let m ≝ get_index_v … nu O ? in
    721721    let r1 ≝ get_index_v … nu 1 ? in
    … …  
    804804        λext_indirect_dptr: True.
    805805          let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    806             lookup … 16 address (external_ram ? s) (zero 8)
     806            lookup ? 16 address (external_ram ? s) (zero 8)
    807807      | EXT_INDIRECT e ⇒
    808808        λext_indirect: True.
    809809          let address ≝ get_register ? s [[ false; false; e ]]  in
    810810          let padded_address ≝ pad 8 8 address in
    811             lookup … 16 padded_address (external_ram ? s) (zero 8)
     811            lookup ? 16 padded_address (external_ram ? s) (zero 8)
    812812      | ACC_DPTR ⇒
    813813        λacc_dptr: True.
    … …  
    815815          let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
    816816          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
    817             lookup … 16 address (external_ram ? s) (zero 8)
     817            lookup ? 16 address (external_ram ? s) (zero 8)
    818818      | ACC_PC ⇒
    819819        λacc_pc: True.
    820820          let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
    821821          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in
    822             lookup … 16 address (external_ram ? s) (zero 8)
     822            lookup ? 16 address (external_ram ? s) (zero 8)
    823823      | DIRECT d ⇒
    824824        λdirect: True.
    825           let 〈 nu, nl 〉 ≝ split … 4 4 d in
     825          let 〈 nu, nl 〉 ≝ split ? 4 4 d in
    826826          let bit_one ≝ get_index_v ? ? nu 0 ? in
    827827          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
    … …  
    836836          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in
    837837          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    838           let bit_1 ≝ get_index_v … bit_one_v O ? in
     838          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
    839839          match  bit_1 with
    840840            [ false ⇒
    … …  
    10021002                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10031003                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1004                 let trans ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in
     1004                let trans ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
    10051005                  ¬(get_index_v … trans (modulus address 8) ?)
    10061006              ]
    … …  
    10381038                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10391039                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1040                 let t ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in
     1040                let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
    10411041                let n_bit ≝ set_index … t (modulus address 8) v ? in
    10421042                let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
    … …  
    10961096    match \fst x with
    10971097    [ None ⇒ false
    1098     | Some x ⇒ eq_bv ? x y
     1098    | Some x ⇒ eq_identifier ? x y
    10991099    ].
    11001100
    … …  
    11141114lemma does_not_occur_Some:
    11151115 ∀id,id',i,list_instr.
    1116   eq_bv ? id' id = false →
     1116  eq_identifier ? id' id = false →
    11171117   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
    11181118    does_not_occur id list_instr.
    … …  
    11261126  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
    11271127 #id #i #list_instr elim list_instr
    1128   [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
    1129     >eq_bv_refl %
     1128  [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
     1129    >eq_identifier_refl %
    11301130  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
    11311131qed.
    … …  
    11511151lemma occurs_exactly_once_Some:
    11521152 ∀id,id',i,prefix.
    1153   occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
     1153  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
    11541154 #id #id' #i #prefix elim prefix
    1155   [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    1156     change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
     1155  [ whd in ⊢ (?% → ?)
     1156    change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) with (eq_identifier ? id' id)
     1157    @eq_identifier_elim normalize nodelta; /2/
    11571158  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    11581159    cases he; normalize nodelta
    11591160     [ #H @ (IH H)
    1160      | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    1161        change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
    1162        [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
    1163         /2/ #H >does_not_occur_Some //
     1161     | #x whd in ⊢ (? → ?(??%)) change in match (instruction_matches_identifier ??) with (eq_identifier ? x id)
     1162       @eq_identifier_elim #E normalize nodelta
     1163       [ destruct @eq_identifier_elim normalize nodelta;
     1164        /2/ #H >does_not_occur_Some /2/
    11641165       | #H @IH @H]]]
    11651166qed.
    … …  
    11681169  ∀id,id',i,prefix.
    11691170    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
    1170     (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
    1171     (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
     1171    (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨
     1172    (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
    11721173 #id #id' #i #prefix elim prefix
    1173  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
    1174   change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
     1174 [ whd in ⊢ (?% → ?) change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?) with (eq_identifier ???)
     1175   @eq_identifier_elim #E
    11751176  [ normalize //
    11761177  | normalize #H @⊥ @H 
    … …  
    11791180   cases he; normalize nodelta
    11801181   [ #H @ (IH H)
    1181    | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    1182      generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
    1183      cases (eq_bv ???) in ⊢ (???% → %) #Heq
    1184      [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
    1185        [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
     1182   | #x @eq_identifier_elim #Heq
     1183     [ @eq_identifier_elim normalize nodelta
     1184       [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
    11861185       | #H >(does_not_occur_Some)
    1187          [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
    1188            change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
    1189            @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
    1190            change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 
    1191          | @(sym_eq … H)
     1186         [ #H2 whd in match (does_not_occur ??)
     1187           change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1188           >Heq >eq_identifier_refl normalize nodelta
     1189           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??)
     1190           change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1191           >eq_identifier_refl
     1192           normalize nodelta @H2 
     1193         | /2/
    11921194         ]
    11931195       ]
    1194      | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
    1195        generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)
    1196        #Heq2
    1197        [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
    1198          whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
    1199          change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
    1200          cases (does_not_occur id tl) in Hor; normalize nodelta //
     1196     | normalize nodelta #H lapply (IH H) -IH -H;
     1197       @eq_identifier_elim #Heq2
     1198       #Hor @orb_elim
     1199       [ <Heq2 in Hor; #Hor normalize in Hor;
     1200         whd in match (does_not_occur ??) change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1201         >eq_identifier_false // normalize nodelta
     1202         cases (does_not_occur id' tl) in Hor; normalize nodelta //
    12011203       | normalize nodelta whd in match (occurs_exactly_once ??)
    1202          whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
    1203          >Heq normalize nodelta <Heq2 in Hor; normalize //
     1204         change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1205         >eq_identifier_false //
    12041206       ]
    12051207     ] 
    … …  
    12411243
    12421244lemma index_of_internal_Some_miss: ∀i,id,id'.
    1243  eq_bv ? id' id = false →
     1245 eq_identifier ? id' id = false →
    12441246 ∀instr_list,n.
    12451247 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    … …  
    12591261  = |instr_list| + n.
    12601262 #i #id #instr_list elim instr_list
    1261   [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
     1263  [ #n #_ whd in ⊢ (??%%) change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
    12621264  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
    1263     [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
     1265    [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
    12641266qed.
    12651267
    … …  
    12781280
    12791281lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    1280  eq_bv ? id' id = false →
     1282 eq_identifier ? id' id = false →
    12811283  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    12821284   address_of_word_labels_code_mem instr_list id =
    12831285   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    12841286 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    1285  >(index_of_internal_Some_miss … H) //
     1287 >(index_of_internal_Some_miss … H) [ @refl | // ]
    12861288qed.
    12871289
    … …  
    12911293   = bitvector_of_nat … (|instr_list|).
    12921294 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
    1293  >(index_of_internal_Some_hit … H) //
     1295 >(index_of_internal_Some_hit … H) <plus_n_O @refl
    12941296qed.
    12951297
    … …  
    13011303definition construct_datalabels ≝
    13021304  λpreamble.
    1303     \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
     1305    \fst (foldl ((identifier_map ASMTag Word) × nat) ? (
    13041306    λt. λpreamble.
    13051307      let 〈datalabels, addr〉 ≝ t in
    13061308      let 〈name, size〉 ≝ preamble in
    13071309      let addr_16 ≝ bitvector_of_nat 16 addr in
    1308         〈insert ? ? name addr_16 datalabels, addr + size〉)
    1309           〈(Stub ? ?), 0〉 preamble).
     1310        〈add ? ? datalabels name addr_16, addr + size〉)
     1311          〈empty_map …, 0〉 preamble).

  • src/ASM/StatusProofs.ma

    r1014 r1515  
    182182lemma get_8051_sfr_write_at_stack_pointer:
    183183 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
    184  #T #s #x #y whd in ⊢ (??%%) //
     184 #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl
    185185qed.
    186186
Note: See TracChangeset for help on using the changeset viewer.