Changeset 1528 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Nov 22, 2011, 11:58:43 AM (8 years ago)
Author:
campbell
Message:

Update most of Assembly.ma with new syntax and identifier maps.
Change positive.ma a little to reduce name clashes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1493 r1528  
    55include "ASM/Status.ma".
    66include alias "basics/logic.ma".
     7include alias "arithmetics/nat.ma".
    78
    89definition assembly_preinstruction ≝
     
    545546qed.
    546547
    547 (* label_trie: identifier ↦ 〈instruction number, address〉 *)
    548 definition label_trie ≝ BitVectorTrie (nat × nat) 16.
     548(* label_map: identifier ↦ 〈instruction number, address〉 *)
     549definition label_map ≝ identifier_map ASMTag (nat × nat).
    549550
    550551definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
     
    572573 [ #i >nth_nil #H @⊥ @H
    573574 | #h #t #IH #i cases i -i
    574    [ cases h #hi #hp cases hi normalize
    575      [ #H @⊥ @H
    576      | #l' #Heq change in match (eq_v ??? l' l) with (eq_bv ? l' l)
    577        >(eq_eq_bv … Heq) //
     575   [ cases h #hi #hp cases hi
     576     [ normalize #H @⊥ @H
     577     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
     578       whd in Heq; >Heq
     579       >eq_identifier_refl //
    578580     ]
    579    | #i #H whd in match (does_not_occur ??)
    580      whd in match (instruction_matches_identifier ??)
    581      cases h #hi #hp cases hi normalize
     581   | #i #H whd in match (does_not_occur ??);
     582     whd in match (instruction_matches_identifier ??);
     583     cases h #hi #hp cases hi normalize nodelta
    582584     [ @(IH i) @H
    583      | #l' cases (eq_v ??? l' l)
     585     | #l' @eq_identifier_elim
    584586       [ normalize //
    585        | normalize @(IH i) @H
     587       | normalize #_ @(IH i) @H
    586588       ]
    587589     ]
     
    603605coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
    604606≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
    605      
    606 let rec create_label_trie (program: list labelled_instruction)
     607
     608let rec create_label_map (program: list labelled_instruction)
    607609  (policy: jump_expansion_policy):
    608   (Σlabels:label_trie.
    609     ∀i:ℕ.i < |program|
     610  (Σlabels:label_map.
     611    ∀i:ℕ.lt i (|program|) (* XXX using < causes (false?) ambiguity *)
    610612    ∀l.occurs_exactly_once l program →
    611613    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    612     ∃a.lookup_opt … l labels = Some ? 〈i,a〉
     614    ∃a.lookup … labels l = Some ? 〈i,a〉
    613615  ) ≝
    614616  let 〈final_pc, final_labels〉 ≝
     
    618620      ∀l.occurs_exactly_once l prefix →
    619621      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    620       ∃a.lookup_opt … l labels = Some ? 〈i,a〉)
     622      ∃a.lookup … labels l = Some ? 〈i,a〉)
    621623    )
    622624    program
     
    627629          match label with
    628630          [ None   ⇒ labels
    629           | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
     631          | Some l ⇒ add … labels l 〈|prefix|, pc〉
    630632          ] in
    631           let jmp_len ≝ \snd (lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
     633          let jmp_len ≝ \snd (bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
    632634          〈add_instruction_size pc jmp_len instr, new_labels〉
    633     ) 〈0, Stub ? ?〉 in
     635    ) 〈0, empty_map …〉 in
    634636    final_labels.
    635 [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     637[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    636638  [ #Hi #l normalize nodelta; cases label normalize nodelta
    637639    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
    638640      lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
    639641      % [ @addr | @Haddr ]
    640     | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc; #Hocc
    641       lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq
    642       [ >Heq in Hocc; #Hocc normalize in Hocc;
     642    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
     643      @eq_identifier_elim #Heq #Hocc
     644      [ normalize in Hocc;
    643645        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
    644646        @⊥ @(absurd … Hocc)
    645       | >Heq in Hocc; normalize nodelta #Hocc lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
    646         [ #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]
     647      | normalize nodelta lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
     648        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
    647649        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
    648650        ]
     
    653655    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
    654656      [ normalize nodelta #H @⊥ @H
    655       | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_opt_insert_hit ]
     657      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
    656658      ]
    657659    | @le_n
     
    662664qed.
    663665
    664 definition select_reljump_length: label_trie → ℕ → Identifier → jump_length ≝
     666definition select_reljump_length: label_map → ℕ → Identifier → jump_length ≝
    665667  λlabels.λpc.λlbl.
    666   let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
     668  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
    667669  if leb pc addr (* forward jump *)
    668670  then if leb (addr - pc) 126
     
    673675       else long_jump.
    674676
    675 definition select_call_length: label_trie → ℕ → Identifier → jump_length ≝
     677definition select_call_length: label_map → ℕ → Identifier → jump_length ≝
    676678  λlabels.λpc_nat.λlbl.
    677679  let pc ≝ bitvector_of_nat 16 pc_nat in
    678   let addr ≝ bitvector_of_nat 16 (\snd (lookup ? ? lbl labels 〈0, pc_nat〉)) in
     680  let addr ≝ bitvector_of_nat 16 (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
    679681  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
    680682  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
     
    683685  else long_jump.
    684686 
    685 definition select_jump_length: label_trie → ℕ → Identifier → jump_length ≝
     687definition select_jump_length: label_map → ℕ → Identifier → jump_length ≝
    686688  λlabels.λpc.λlbl.
    687   let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
     689  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
    688690  if leb pc addr
    689691  then if leb (addr - pc) 126
     
    694696       else select_call_length labels pc lbl.
    695697 
    696 definition jump_expansion_step_instruction: label_trie → ℕ →
     698definition jump_expansion_step_instruction: label_map → ℕ →
    697699  preinstruction Identifier → option jump_length ≝
    698700  λlabels.λpc.λi.
     
    830832  (old_policy: Σpolicy.jump_in_policy program policy):
    831833  (Σpolicy.
    832     jump_in_policy program policy ∧
     834    And (jump_in_policy program policy) (* XXX ∧ causes ambiguity *)
    833835    (jump_in_policy program policy →
    834      (∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
     836     (∀i.lt i (|program|) (* XXX < causes ambiguity *) → is_jump (nth i ? program 〈None ?, Comment []〉) →
    835837     jmpleq
    836838       (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
     
    838840    )
    839841   ) ≝
    840   let labels ≝ create_label_trie program old_policy in
     842  let labels ≝ create_label_map program old_policy in
    841843  let 〈final_pc, final_policy〉 ≝
    842844    foldl_strong (option Identifier × pseudo_instruction)
     
    902904            % [1,3,5,7: @pc
    903905              |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
    904                 cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %)
     906                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %);
    905907                #x #y #Hl normalize nodelta
    906             % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
     908            % [1,3,5,7: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j))
    907909              |2,4,6,8: @lookup_opt_insert_hit
    908910              ] ]
     
    910912            % [1,3,5,7,9: @pc
    911913              |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
    912                 cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %)         
     914                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %);
    913915                #x #y #Hl normalize nodelta
    914             % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
     916            % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j))
    915917              |2,4,6,8,10: @lookup_opt_insert_hit
    916918              ] ]
     
    920922            |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    921923                #x #y normalize nodelta
    922             % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
    923               |3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j))
     924            % [1: @(max_length y (select_jump_length (create_label_map program old_policy) pc j))
     925              |3: @(max_length y (select_call_length (create_label_map program old_policy) pc j))
    924926              |2,4: @lookup_opt_insert_hit
    925927              ]
     
    940942        [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    941943        | #z normalize nodelta
    942           whd in match (snd ℕ jump_expansion_policy ?) >lookup_insert_miss
     944          whd in match (snd ℕ jump_expansion_policy ?); >lookup_insert_miss
    943945          [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    944946          | @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     
    961963          |9,10,14,15: #j normalize nodelta #_
    962964            cases (lookup ???? 〈0,short_jump〉) #x #y
    963             whd in match (snd ℕ jump_expansion_policy ?) 
     965            whd in match (snd ℕ jump_expansion_policy ?);
    964966            >lookup_insert_hit normalize @jmpleq_max_length
    965967          |11,12,13,16,17: #z #j normalize nodelta #_
    966968            cases (lookup ???? 〈0,short_jump〉) #x #y           
    967             whd in match (snd ℕ jump_expansion_policy ?)
     969            whd in match (snd ℕ jump_expansion_policy ?);
    968970            >lookup_insert_hit normalize @jmpleq_max_length
    969971          ]
    970972        |4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y
    971               whd in match (snd ℕ jump_expansion_policy ?)
     973              whd in match (snd ℕ jump_expansion_policy ?);
    972974              >lookup_insert_hit normalize @jmpleq_max_length
    973975        ]
     
    10271029  λpseudo_program_counter: nat.
    10281030  λprogram_counter: nat.
    1029   λcosts: BitVectorTrie Word 16.
     1031  λcosts: BitVectorTrie costlabel 16.
    10301032  λi.
    10311033  match i with
     
    11481150   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
    11491151 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
    1150  generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
    1151  whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
     1152 generalize in match (sig2 ?? pol); whd in prf:(???%); <prf in pol; #pol
     1153 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
    11521154 normalize nodelta >sigma00_append
    11531155 cases (sigma00 ?? prefix ?)
     
    11661168 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
    11671169 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
    1168   (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
     1170  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
    11691171 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
    11701172 @pair_elim' #pc #map #EQ4 normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.