Changeset 2470 for src/common/ByteValues.ma
 Timestamp:
 Nov 15, 2012, 7:06:45 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/ByteValues.ma
r2462 r2470 10 10 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code). 11 11 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData). 12 13 (* this is like a code pointer, but with unbounded offset. 14 used only in the backend, they become code pointers in LIN → ASM *) 15 record program_counter : Type[0] ≝ 16 { pc_block : Σb : block.block_region b = Code 17 ; pc_offset : Pos 18 }. 19 20 definition eq_program_counter : program_counter → program_counter → bool ≝ 21 λpc1,pc2.eq_block (pc_block pc1) (pc_block pc2) ∧ 22 eqb (pc_offset pc1) (pc_offset pc2). 23 24 lemma eq_program_counter_elim : ∀P:bool→Prop. 25 ∀pc1,pc2.(pc1=pc2→P true)→(pc1≠pc2→P false)→P (eq_program_counter pc1 pc2). 26 #P ** #bl1 #H1 #o1 ** #bl2 #H2 #o2 27 #Heq #Hneq whd in ⊢ (?%); 28 @eq_block_elim #EQ1 29 [ @eqb_elim #EQ2 ] 30 [ @Heq destruct % 31 *: @Hneq % #ABS destruct 32 [ @(absurd ?? EQ2)  @(absurd ?? EQ1) ] % 33 ] qed. 34 35 lemma reflexive_eq_program_counter : ∀pc.eq_program_counter pc pc = true. 36 ** #bl1 #H1 #o1 whd in ⊢ (??%?); >eq_block_b_b >eqb_n_n % qed. 37 38 definition bitvector_from_pos : 39 ∀n.Pos → BitVector n ≝ 40 λn,p.bitvector_of_Z n (Zpred (pos p)). 41 42 definition pos_from_bitvector : 43 ∀n.BitVector n → Pos ≝ 44 λn,v. 45 match Zsucc (Z_of_unsigned_bitvector n v) 46 return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ? 47 with 48 [ OZ ⇒ λprf.⊥ 49  pos x ⇒ λ_. x 50  neg x ⇒ λprf.⊥ 51 ] (refl …). 52 @hide_prf 53 elim v in prf; 54 [2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed. 55 56 definition cpointer_of_pc : program_counter → option cpointer ≝ 57 λpc. 58 let pc_off ≝ pc_offset pc in 59 if leb pc_off (two_power_nat offset_size) then 60 return «mk_pointer (pc_block pc) (mk_offset (bitvector_from_pos … pc_off)),?» 61 else 62 None ?. 63 elim (pc_block pc) #bl #H @H qed. 12 64 13 65 record part (*r: region*): Type[0] ≝ … … 43 95  BVnull: (*∀r:region.*) part → beval 44 96  BVptr: pointer → part → beval 45  BVpc: cpointer → part → beval. (* only used in back end, needed to separate97  BVpc: program_counter → part → beval. (* only used in back end, needed to separate 46 98 program counters that go in the stack from 47 99 function pointers, as they are linked with … … 89 141 ]. 90 142 91 definition pc_of_bevals: list beval → res cpointer ≝143 definition pc_of_bevals: list beval → res program_counter ≝ 92 144 λl. 93 145 match l with … … 104 156 match bv2 with 105 157 [ BVpc ptr2 p2 ⇒ 106 if eqb p1 0 ∧ eqb p2 1 ∧ eq_p ointer ptr1 ptr2 then158 if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then 107 159 return ptr2 108 160 else Error … [MSG CorruptedPointer] … … 120 172 121 173 definition bevals_of_pc ≝ 122 λp: cpointer.174 λp:program_counter. 123 175 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer). 124 176 … … 138 190 whd in match (bevals_of_pc ?); 139 191 whd in ⊢ (??%?); 140 >reflexive_eq_p ointer192 >reflexive_eq_program_counter 141 193 % 142 194 qed. … … 162 214  _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*) 163 215 164 definition beval_pair_of_pc: cpointer → beval × beval ≝216 definition beval_pair_of_pc: program_counter → beval × beval ≝ 165 217 λp. list_to_pair ? (bevals_of_pc p) (refl …). 166 218
Note: See TracChangeset
for help on using the changeset viewer.