Changeset 2470 for src/common


Ignore:
Timestamp:
Nov 15, 2012, 7:06:45 PM (7 years ago)
Author:
tranquil
Message:

completely separated program counters from code pointers in joint languages: the advantage is program counters with an unbounded offset in Pos

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2462 r2470  
    1010unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
    1111unification 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 back-end, they become code pointers in LIN → ASM *)
     15record program_counter : Type[0] ≝
     16  { pc_block : Σb : block.block_region b = Code
     17  ; pc_offset : Pos
     18  }.
     19
     20definition 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
     24lemma 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
     35lemma 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
     38definition bitvector_from_pos :
     39  ∀n.Pos → BitVector n ≝
     40  λn,p.bitvector_of_Z n (Zpred (pos p)).
     41
     42definition 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
     53elim v in prf;
     54[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
     55
     56definition 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 ?.
     63elim (pc_block pc) #bl #H @H qed.
    1264
    1365record part (*r: region*): Type[0] ≝
     
    4395  | BVnull: (*∀r:region.*) part  → beval
    4496  | BVptr: pointer → part → beval
    45   | BVpc: cpointer → part → beval. (* only used in back end, needed to separate
     97  | BVpc: program_counter → part → beval. (* only used in back end, needed to separate
    4698                                      program counters that go in the stack from
    4799                                      function pointers, as they are linked with
     
    89141  ].
    90142
    91 definition pc_of_bevals: list beval → res cpointer ≝
     143definition pc_of_bevals: list beval → res program_counter ≝
    92144 λl.
    93145 match l with
     
    104156          match bv2 with
    105157          [ BVpc ptr2 p2 ⇒
    106             if eqb p1 0 ∧ eqb p2 1 ∧ eq_pointer ptr1 ptr2 then
     158            if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then
    107159              return ptr2
    108160            else Error … [MSG CorruptedPointer]
     
    120172
    121173definition bevals_of_pc ≝
    122  λp:cpointer.
     174 λp:program_counter.
    123175 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).
    124176
     
    138190whd in match (bevals_of_pc ?);
    139191whd in ⊢ (??%?);
    140 >reflexive_eq_pointer
     192>reflexive_eq_program_counter
    141193%
    142194qed.
     
    162214   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
    163215
    164 definition beval_pair_of_pc: cpointer → beval × beval ≝
     216definition beval_pair_of_pc: program_counter → beval × beval ≝
    165217 λp. list_to_pair ? (bevals_of_pc p) (refl …).
    166218
Note: See TracChangeset for help on using the changeset viewer.