Ignore:
Timestamp:
Nov 6, 2012, 4:12:21 PM (8 years ago)
Author:
tranquil
Message:

new back end operations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2286 r2435  
    1111 }.
    1212
     13definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝
     14λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig).
     15
     16coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝
     17part_from_sig on _n_sig:Σn.n<size_pointer to part.
     18
    1319(* Byte-sized values used in the back-end.
    1420   Values larger than a single Byte are represented via their parts.
     
    2127  - the [BVundef] value denoting an arbitrary bit pattern, such as the
    2228    value of an uninitialized variable
    23   - the [BVnonzero] value denoting an arbitrary but non-zero bit pattern,
    24     which arise in the RTLabs → RTL pass when translating equality comparisons
    25     between pointers (which get translated to multiple XORs between pointer
    26     parts).   
     29  - [BVXor] is a formal XOR between (possibly null) pointer parts
     30  - [BVnonzero] is any nonzero value
    2731*)
    2832
     
    3034  | BVundef: beval
    3135  | BVnonzero: beval
     36  | BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *)
    3237  | BVByte: Byte → beval
    3338  | BVnull: (*∀r:region.*) part  → beval
    34   | BVptr: block → ∀p:part.Vector Byte (S p) → beval.
     39  | BVptr: pointer → part → beval.
    3540
    36 definition eq_beval: beval → beval → bool ≝
    37  λv1,v2.
    38   match v1 with
    39    [ BVundef      ⇒ match v2 with [ BVundef      ⇒ true                           | _ ⇒ false ]
    40    | BVnonzero    ⇒ match v2 with [ BVnonzero    ⇒ true                           | _ ⇒ false ]
    41    | BVByte b1    ⇒ match v2 with [ BVByte b2    ⇒ eq_bv … b1 b2                  | _ ⇒ false ]
    42    | BVnull p1    ⇒ match v2 with [ BVnull p2    ⇒ eqb p1 p2                      | _ ⇒ false ]
    43    | BVptr b1 p1 o1  ⇒
    44       match v2 with
    45       [ BVptr b2 p2 o2  ⇒
    46         eq_block … b1 b2 ∧ eqb p1 p2 ∧
    47           (* equivalent to equality if p1 = p2 *)
    48           vprefix … (eq_bv 8) o1 o2
    49       | _ ⇒ false
    50       ]
    51    ].
     41definition eq_bv_suffix : ∀n,m,p.
     42  BitVector (n + p) → BitVector (m + p) → bool ≝
     43λn,m,p,v1,v2.
     44let b1 ≝ \snd (vsplit … v1) in
     45let b2 ≝ \snd (vsplit … v2) in
     46eq_bv … b1 b2.
    5247
    5348include alias "arithmetics/nat.ma".
    5449
    5550axiom CorruptedPointer: String.
    56 
    57 let rec pointer_of_bevals_aux (b:block) (part: nat) (acc : BitVector (part*8))
    58   (l: list beval) on l : res pointer ≝
    59  match l with
    60   [ nil ⇒
    61      If eqb part (size_pointer (*ptype p*)) then with prf do
    62       return mk_pointer b (mk_offset (acc⌈BitVector (part*8)↦?⌉))
    63      else
    64       Error … [MSG CorruptedPointer]
    65   | cons v tl ⇒
    66      match v with
    67       [ BVptr b' part' o' ⇒
    68         let acc' ≝ vflatten … o' in
    69         if eq_block b b' ∧
    70            eqb part part' ∧
    71            vsuffix … eq_b acc acc' then
    72            pointer_of_bevals_aux b (S part') acc' tl
    73          else
    74           Error … [MSG CorruptedPointer]
    75       | _ ⇒ Error … [MSG CorruptedPointer]
    76       ]
    77   ].
    78   @hide_prf
    79   >commutative_times_fast
    80   lapply prf @(eqb_elim part) #H * >H % qed.
    8151
    8252(* CSC: use vectors in place of lists? Or even better products of tuples
     
    8656 match l with
    8757  [ nil ⇒ Error … [MSG CorruptedPointer]
    88   | cons he tl ⇒
    89      match he with
    90       [ BVptr b part o ⇒
    91          if eqb part 0 then
    92            pointer_of_bevals_aux b (S part) (vflatten … o) tl
    93          else Error … [MSG CorruptedPointer]
    94       | _ ⇒ Error … [MSG CorruptedPointer]
     58  | cons bv1 tl ⇒
     59    match tl with
     60    [ nil ⇒ Error … [MSG CorruptedPointer]
     61    | cons bv2 tl' ⇒
     62      match tl' with
     63      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
     64      | nil ⇒
     65        match bv1 with
     66        [ BVptr ptr1 p1 ⇒
     67          match bv2 with
     68          [ BVptr ptr2 p2 ⇒
     69            if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧
     70               eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2))
     71            then
     72              return ptr2
     73            else Error … [MSG CorruptedPointer]
     74          | _ ⇒ Error … [MSG CorruptedPointer]
     75          ]
     76        | _ ⇒ Error … [MSG CorruptedPointer]
     77        ]
    9578      ]
     79    ]
    9680  ].
    9781
    98 (* CSC: use vectors in place of lists? Or even better products of tuples
    99    (more easily pattern matchable in the finite case)? *)
    100 let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) on n: n + part = size_pointer (*ptype p*) → list beval ≝
    101  match n with
    102   [ O ⇒ λ_.[]
    103   | S m ⇒ λpr': S m + part = ?.
    104     let postfix ≝ rvsplit … (\snd (vsplit bool (m*8) (S part*8) (offv (poff p) ⌈BitVector ?↦?⌉))) in
    105     (BVptr (pblock p) (mk_part … part …) postfix)::bevals_of_pointer_aux p (S part) m ?
    106   ].
    107 @hide_prf
    108 [3: change with (?*?) in match offset_size;
    109   <pr' >(commutative_times_fast ? 8) >(commutative_times_fast ? 8)
    110   <distributive_times_plus_fast <plus_n_Sm_fast %
    111 ] -postfix
    112 /3 by lt_plus_to_minus_r, lt_plus_to_lt_l/ qed.
    113 
    114 definition bevals_of_pointer: pointer → list beval ≝
    115  λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) ….
    116 @hide_prf @plus_n_O qed.
     82definition bevals_of_pointer ≝
     83 λp:pointer.
     84 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer).
    11785
    11886lemma pointer_of_bevals_bevals_of_pointer:
    11987 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
    120 * #pbl * #voff
     88#ptr
    12189whd in match (bevals_of_pointer ?);
    122 @vsplit_elim #pre #post
    123 normalize nodelta
    124 #EQ >EQ
    125 whd in match (bevals_of_pointer_aux ????);
    126 @vsplit_elim #pre' #post'
    127 normalize nodelta
    128 >(Vector_O … pre') #EQ' normalize in EQ'; <EQ' -pre' -post'
    12990whd in ⊢ (??%?);
    130 >eq_block_b_b >eqb_n_n
    131 >vflatten_rvsplit >vflatten_rvsplit
    132 >vsuffix_true
    133 [2: change with (bool_to_Prop (eq_bv ???)) >eq_bv_refl % ]
    134 normalize nodelta %
     91>eq_block_b_b
     92change with (eq_bv ???) in match (eq_bv_suffix ?????);
     93>eq_bv_refl %
    13594qed.
    13695
     
    146105(* Fails if the address is not representable as a pair *)
    147106definition beval_pair_of_pointer: pointer → res (beval × beval) ≝
    148  λp. OK … (list_to_pair … (bevals_of_pointer p) ?).
     107 λp. OK … (list_to_pair … (bevals_of_pointer p) (refl …)).
    149108(*
    150109 λp. match p with [ mk_pointer pty pbl pok poff ⇒
     
    153112   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
    154113   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
    155 % qed.
    156114
    157115definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
    158  λp. list_to_pair ? (bevals_of_pointer p) ?.
     116 λp. list_to_pair ? (bevals_of_pointer p) (refl …).
    159117(*
    160118 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
     
    162120   [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
    163121   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
    164 [@(pi2 … p) |7: // |8: %] destruct (abs)*) %
    165 qed.
    166 
     122[@(pi2 … p) |7: // |8: %] destruct (abs)*)
    167123
    168124axiom NotACodePointer: String.
     
    172128  do p ← pointer_of_bevals [v1;v2] ;
    173129  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
    174   [ Code ⇒ λE.OK ? (mk_Sig … p ?)
    175   | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
    176 // qed.
     130  [ Code ⇒ λE.OK ? (mk_Sig … p E)
     131  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …).
    177132
    178133axiom ValueNotABoolean: String.
     
    181136 λv.match v with
    182137  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
    183   | BVnonzero ⇒ OK … true
     138  | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can
     139                                                   tell the value, we will always
     140                                                   call bool_of_beval after a
     141                                                   series of XORs has been
     142                                                   completed *)
    184143  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
    185   | BVnull y ⇒  OK … false
    186   | BVptr p q o ⇒ OK ? true ].
     144  | BVnull _ ⇒  OK … false
     145  | _ ⇒ OK ? true
     146  ].
    187147
    188148definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
     
    210170| BBundef : bebit
    211171| BBptrcarry :
    212   (* is add *) bool → block → ∀p : part.Vector Byte (S p) → Vector Byte (S p) → bebit.
    213 
    214 definition eq_bebit: bebit → bebit → bool ≝
    215  λv1,v2.
    216   match v1 with
    217    [ BBundef      ⇒ match v2 with [ BBundef      ⇒ true                           | _ ⇒ false ]
    218    | BBbit b1    ⇒ match v2 with [ BBbit b2    ⇒ eq_b b1 b2                  | _ ⇒ false ]
    219    | BBptrcarry is_add1 b1 p1 o1 by1  ⇒
    220       match v2 with
    221       [ BBptrcarry is_add2 b2 p2 o2 by2  ⇒
    222         eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧
    223           (* equivalent to equality if p1 = p2 *)
    224           vprefix … (eq_bv 8) o1 o2 ∧
    225           vprefix … (eq_bv 8) by1 by2
    226       | _ ⇒ false
    227       ]
    228    ].
     172  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
    229173
    230174definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
Note: See TracChangeset for help on using the changeset viewer.