Changeset 1363


Ignore:
Timestamp:
Oct 12, 2011, 9:11:07 PM (8 years ago)
Author:
boender
Message:
  • done stuff with create_label_trie
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1309 r1363  
    556556  let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (|bv|)) false in
    557557  new_pc.
     558
     559definition is_label ≝
     560  λx:labelled_instruction.λl:Identifier.
     561  let 〈lbl,instr〉 ≝ x in
     562  match lbl with
     563  [ Some l' ⇒ l' = l
     564  | _       ⇒ False
     565  ].
    558566 
     567lemma oeo_Some_Stronger:
     568  ∀id,id',i,prefix.
     569    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
     570    (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
     571    (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
     572 #id #id' #i #prefix elim prefix
     573 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
     574  change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
     575  [ normalize //
     576  | normalize #H @⊥ @H 
     577  ]
     578 | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     579   cases he; normalize nodelta
     580   [ #H @ (IH H)
     581   | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
     582     generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
     583     cases (eq_bv ???) in ⊢ (???% → %) #Heq
     584     [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
     585       [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
     586       | #H >(does_not_occur_Some)
     587         [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
     588           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
     589           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
     590           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 
     591         | @(sym_eq … H)
     592         ]
     593       ]
     594     | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
     595       generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)
     596       #Heq2
     597       [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
     598         whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
     599         change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
     600         cases (does_not_occur id tl) in Hor; normalize nodelta //
     601       | normalize nodelta whd in match (occurs_exactly_once ??)
     602         whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
     603         >Heq normalize nodelta <Heq2 in Hor; normalize //
     604       ]
     605     ] 
     606   ]
     607 ]
     608qed.   
     609
     610lemma bla:
     611  ∀i,p,l.
     612  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
     613 #i #p #l generalize in match i; elim p
     614 [ #i >nth_nil #H @⊥ @H
     615 | #h #t #IH #i cases i -i
     616   [ cases h #hi #hp cases hi normalize
     617     [ #H @⊥ @H
     618     | #l' #Heq change in match (eq_v ??? l' l) with (eq_bv ? l' l)
     619       >(eq_eq_bv … Heq) //
     620     ]
     621   | #i #H whd in match (does_not_occur ??)
     622     whd in match (instruction_matches_identifier ??)
     623     cases h #hi #hp cases hi normalize
     624     [ @(IH i) @H
     625     | #l' cases (eq_v ??? l' l)
     626       [ normalize //
     627       | normalize @(IH i) @H
     628       ]
     629     ]
     630   ]
     631 ]
     632qed. 
     633     
    559634definition create_label_trie: list labelled_instruction → jump_expansion_policy →
    560635  label_trie ≝
    561636  λprogram.λpolicy.
    562   let 〈final_n, final_pc, final_labels〉 ≝
     637  let 〈final_pc, final_labels〉 ≝
    563638    foldl_strong (option Identifier × pseudo_instruction)
    564     (λprefix.Σres.True)
     639    (λprefix.Σres.
     640      let 〈pc,labels〉 ≝ res in
     641      ∀i:ℕ.i < |prefix| →
     642      ∀l.occurs_exactly_once l prefix ->
     643      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
     644      ∃a.lookup_opt … l labels = Some ? 〈i,a〉
     645    )
    565646    program
    566647    (λprefix.λx.λtl.λprf.λacc.
    567      let 〈n,pc,labels〉 ≝ acc in
     648     let 〈pc,labels〉 ≝ acc in
    568649     let 〈label,instr〉 ≝ x in
    569650     let new_labels ≝
    570651       match label with
    571652       [ None   ⇒ labels
    572        | Some l ⇒ insert … l 〈n, pc〉 labels
     653       | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
    573654       ] in
    574      let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, long_jump〉 in
     655     let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉 in
    575656     let new_pc ≝ add_instruction_size pc jmp_len instr in
    576      〈S n, new_pc, new_labels〉
    577     ) 〈0, zero ?, Stub ? ?〉 in
     657     〈new_pc, new_labels〉
     658    ) 〈zero ?, Stub ? ?〉 in
    578659    final_labels.
    579  @I
     660[ lapply (sig2 … acc) >p >p1 normalize nodelta #Hacc #i >append_length
     661  <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     662  [ #Hi #l cases label
     663    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
     664      lapply (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #Ha elim Ha; -Ha; #addr #Haddr
     665      % [ @addr | @Haddr ]
     666    | #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) -Hocc; #Hocc
     667      lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq
     668      [ >Heq in Hocc; #Hocc normalize in Hocc;
     669        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
     670        @⊥ @(absurd … Hocc)
     671      | >Heq in Hocc; normalize nodelta #Hocc lapply (Hacc i (le_S_S_to_le … Hi) l ? ?)
     672        [ >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
     673        | @Hocc
     674        | #H elim H #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]   
     675        ]
     676      ]
     677      >(bla i … Hl) normalize nodelta @nmk //
     678    ]
     679  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
     680    [ <minus_n_n #Hl normalize in Hl; cases label in Hl;
     681      [ normalize nodelta #H @⊥ @H
     682      | #l' normalize nodelta #Heq % [ @pc | <Heq @lookup_opt_insert_hit ]
     683      ]
     684    | @le_n
     685    ]
     686  ]
     687| #i #Hi #l #Hl @⊥ @Hl
     688]
    580689qed.
    581690
     
    10251134   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
    10261135   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
    1027    | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
     1136   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
    10281137   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
    10291138   | #id normalize nodelta; -labels1; cases label; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.