Changeset 2435 for src/common


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

new back end operations

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/BackEndOps.ma

    r2286 r2435  
    6666    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
    6767    return 〈BVByte rslt, BBbit carry''〉
    68   | BVptr b p o ⇒
    69     match p with
    70     [ O ⇒ λ_:0<size_pointer.λo : Vector Byte 1.
    71       if eq_bebit carry (BBbit false) then
    72         let o' ≝ from_singl … o in
    73         let 〈rslt,carry〉 ≝ op2 eval false op b2 o' in
    74         let p' : part ≝ mk_part 0 ? in
    75         return 〈BVptr b p' [[rslt]], BBptrcarry is_add b p' o [[b2]]〉
    76       else
    77         Error … [MSG UnsupportedOp]
    78     | S k ⇒ λSk_ok:S k<size_pointer.λo : Vector Byte (S (S k)).
    79       match carry with
    80       [ BBptrcarry is_add' b' p' o' by' ⇒
    81         if eq_b is_add is_add' ∧ eq_block b b' ∧ vsuffix … (eq_bv 8) o' o then
    82           If eqb k p' then with prf do
    83             let by' ≝ by' ⌈Vector ?? ↦ Vector Byte (S k)⌉ in
    84             let 〈rslt,ignore〉 ≝ op2_bytes op … false o (b2 ::: by') in
    85             let Sk_part ≝ mk_part (S k) Sk_ok in
    86             OK … 〈BVptr b Sk_part rslt,
    87                      BBptrcarry is_add b Sk_part o (b2 ::: by')〉
     68  | BVptr ptr p ⇒
     69    match ptype ptr with
     70    [ Code ⇒ Error … [MSG UnsupportedOp]
     71    | XData ⇒
     72      match p with
     73      [ O ⇒
     74        ! carry' ← Bit_of_val UnsupportedOp carry ;
     75        if carry' then Error … [MSG UnsupportedOp]
     76        else
     77          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
     78          let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in
     79          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
     80          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
     81          return 〈BVptr ptr' p, BBptrcarry is_add ptr p0 b2〉
     82      | _ ⇒ (* it is 1. To generalize, many casts ⌈…⌉ needs to be added *)
     83        match carry with
     84        [ BBptrcarry is_add' ptr' p' by' ⇒
     85          if eq_b is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
     86            eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr'))
     87          then If eqb p' 0 then with prf do
     88            let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in
     89            let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in
     90            let o1o0 ≝ [[\fst o1o0 ; \snd o1o0]] in
     91            let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in
     92            let part1 ≝ mk_part 1 (le_n …) in
     93            let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in
     94            OK … 〈BVptr ptr' part1,
     95                  BBptrcarry is_add ptr' part1 (b2 @@ by')〉
    8896          else Error … [MSG UnsupportedOp]
    89         else Error … [MSG UnsupportedOp]
    90       | _ ⇒ Error … [MSG UnsupportedOp]
    91       ]
    92     ] (part_no_ok p) o
     97          else Error … [MSG UnsupportedOp]
     98        | _ ⇒ Error … [MSG UnsupportedOp]
     99        ]
     100      ]
     101    ]
    93102  | _ ⇒ Error … [MSG UnsupportedOp]
    94103  ].
    95 @hide_prf [//]
    96 lapply prf @(eqb_elim k) #H * >H %
     104@hide_prf
     105lapply prf @(eqb_elim p') #H * >H %
    97106qed.
     107
     108definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝
     109λn,v,p,H.
     110let suffix : BitVector (8 + 8*p) ≝
     111  \snd (vsplit … (v⌈BitVector ?↦BitVector (8*(n - S p) + (8 + 8*p))⌉)) in
     112\fst (vsplit … suffix).
     113>(commutative_times_fast ? p)
     114change with (? = BitVector (? + S p*8))
     115>(commutative_times_fast (S p))
     116<distributive_times_plus_fast
     117<(plus_minus_m_m … H) %
     118qed.
     119
     120definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝
     121λA,eq,m,n.
     122match m with
     123[ Some a ⇒
     124  match n with
     125  [ Some b ⇒ eq a b
     126  | _ ⇒ false
     127  ]
     128| _ ⇒
     129  match m with
     130  [ None ⇒ true
     131  | _ ⇒ false
     132  ]
     133].
    98134
    99135(* This tables shows what binary ops may be defined on bevals depending on
    100136   the arguments (columns marked by 1st argument, rows by 2nd). Further
    101137   checks for definedness are done for pointer parts taking into account
    102    blocks, parts and the carry value.
    103             | BVByte    | BVptr          | BVnull | BVnonzero | BVundef |
    104   ----------+-----------+----------------+--------+-----------+---------|
    105   BVByte    | all       | Add, Addc, Sub | none   | Or        | none    |
    106   ----------+-----------+----------------+--------+-----------+---------|
    107   BVptr     | Add, Addc | Sub, Xor       | Xor    | none      | none    |
    108   ----------+-----------+----------------+--------+-----------+---------|
    109   BVnull    | none      | Xor            | Xor    | none      | none    |
    110   ----------+-----------+----------------+--------+-----------+---------|
    111   BVnonzero | Or        | none           | none   | Or        | none    |
    112   ----------+-----------+----------------+--------+-----------+---------|
    113   BVundef   | none      | none           | none   | none      | none    |
    114   ----------------------------------------------------------------------+
     138   blocks, parts and the carry value. TODO update table
     139  arg2\arg1 | BVByte    | BVptr (D)      | BVptr (C) | BVnull | BVXor | BVnonzero |
     140  ----------+-----------+----------------+-----------+--------+-------+-----------+
     141  BVByte    | all       | Add, Addc, Sub | --        | --     | --    | Or        |
     142  ----------+-----------+----------------+-----------+--------+-------+-----------+
     143  BVptr (D) | Add, Addc | Sub, Xor       | Xor       | Xor    | --    | --        |
     144  ----------+-----------+----------------+-----------+--------+-------+-----------+
     145  BVptr (C) | --        | Xor            | Xor       | Xor    | --    | --        |
     146  ----------+-----------+----------------+-----------+--------+-------+-----------+
     147  BVnull    | --        | Xor            | Xor       | Xor    | --    | --        |
     148  ----------+-----------+----------------+-----------+--------+-------+-----------+
     149  BVXor     | --        | --             | --        | --     | Or    | Or        |
     150  ----------+-----------+----------------+-----------+--------+-------+-----------+
     151  BVnonzero | Or        | --             | --        | --     | Or    | --        |
     152  ----------+-----------+----------------+-----------+--------+-------+-----------+
    115153*)
    116154definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
     
    118156  match a1 with
    119157  [ BVByte b1 ⇒
    120     match a2 with
    121     [ BVByte b2 ⇒
    122       ! carry ← Bit_of_val UnsupportedOp carry ;
    123       let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
    124       return 〈BVByte result, BBbit carry〉
    125     | BVptr bl2 p2 o2 ⇒
    126       match op with
    127       [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
    128       | Addc ⇒ be_add_sub_byte true carry a2 b1
    129       | _ ⇒ Error … [MSG UnsupportedOp]
    130       ]
    131     | BVnonzero ⇒
    132       match op with
    133       [ Or ⇒ return 〈BVnonzero, carry〉
    134       | _ ⇒ Error … [MSG UnsupportedOp]
    135       ]
    136     | _ ⇒ Error … [MSG UnsupportedOp]
    137     ]
    138   | BVptr bl1 p1 o1 ⇒
     158(*    if match op with [ Or ⇒ true | _ ⇒ false ] ∧ eq_bv … (zero …) b1 then
     159      return 〈a2, carry〉
     160    else *) (* maybe it will be needed, need to see actual translations *)
     161      match a2 with
     162      [ BVByte b2 ⇒
     163        ! carry ← Bit_of_val UnsupportedOp carry ;
     164        let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
     165        return 〈BVByte result, BBbit carry〉
     166      | BVptr _ _ ⇒
     167        match op with
     168        [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
     169        | Addc ⇒ be_add_sub_byte true carry a2 b1
     170        | _ ⇒ Error … [MSG UnsupportedOp]
     171        ]
     172      | BVnonzero ⇒
     173        match op with
     174        [ Or ⇒ return 〈BVnonzero, carry〉
     175        | _ ⇒ Error … [MSG UnsupportedOp]
     176        ]
     177      | _ ⇒ Error … [MSG UnsupportedOp]
     178      ]
     179  | BVptr ptr1 p1 ⇒
    139180    match a2 with
    140181    [ BVByte b2 ⇒
     
    145186      | _ ⇒ Error … [MSG UnsupportedOp]
    146187      ]
    147     | BVptr bl2 p2 o2 ⇒
     188    | BVptr ptr2 p2 ⇒
    148189      match op with
    149190      [ Sub ⇒
    150         if eq_block bl1 bl2 ∧ eqb p1 p2 then
     191        match ptype ptr1 with
     192        [ Code ⇒ Error … [MSG UnsupportedOp]
     193        | XData ⇒
     194          if eq_block (pblock ptr1) (pblock ptr2) ∧
     195             eqb p1 p2
     196          then
    151197          ! carry ← Bit_of_val UnsupportedOp carry ;
    152           let by1 ≝ head' … o1 in
    153           let by2 ≝ head' … o2 in
    154           let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
    155           return 〈BVByte result, BBbit carry〉
    156         else Error … [MSG UnsupportedOp]
     198            let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in
     199            let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in
     200            let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
     201            return 〈BVByte result, BBbit carry〉
     202          else Error … [MSG UnsupportedOp]
     203        ]
    157204      | Xor ⇒
    158         if eq_block bl1 bl2 ∧ eqb p1 p2 then
    159           if vprefix … (eq_bv 8) o1 o2 (* equivalent to equality *) then
    160             return 〈BVByte (bv_zero …), carry〉
    161           else
    162             return 〈BVnonzero, carry〉
     205        if eqb p1 p2 then
     206          return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
    163207        else Error … [MSG UnsupportedOp]
    164208      | _ ⇒ Error … [MSG UnsupportedOp]
     
    168212      [ Xor ⇒
    169213        if eqb p1 p2 then
    170           return 〈BVnonzero, carry〉
     214          return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
    171215        else
    172216          Error … [MSG UnsupportedOp]
     217      | _ ⇒ Error … [MSG UnsupportedOp]
     218      ]
     219    | _ ⇒ Error … [MSG UnsupportedOp]
     220    ]
     221  | BVnull p1 ⇒
     222    match op with
     223    [ Xor ⇒
     224      match a2 with
     225      [ BVptr ptr2 p2 ⇒
     226        if eqb p1 p2 then
     227          return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
     228        else
     229          Error … [MSG UnsupportedOp]
     230      | BVnull p2 ⇒
     231        if eqb p1 p2 then
     232          return 〈BVXor (None ?) (None ?) p1, carry〉
     233        else
     234          Error … [MSG UnsupportedOp]
     235      | _ ⇒ Error … [MSG UnsupportedOp]
     236      ]
     237    | _ ⇒ Error … [MSG UnsupportedOp]
     238    ]
     239  | BVXor ptr1_opt ptr1_opt' p1 ⇒
     240    match op with
     241    [ Or ⇒
     242      match a2 with
     243      [ BVByte b2 ⇒
     244        if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉
     245        else Error … [MSG UnsupportedOp]
     246      | BVnonzero ⇒ return 〈BVnonzero, carry〉
     247      | BVXor ptr2_opt ptr2_opt' p2 ⇒
     248        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
     249          let eq_at ≝ λp,ptr1,ptr2.
     250            eq_block (pblock ptr1) (pblock ptr2) ∧
     251            eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p))
     252                    (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in
     253          if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧
     254             eq_opt ? (eq_at p2) ptr2_opt ptr2_opt'
     255          then return 〈BVByte (bv_zero …), carry〉
     256          else return 〈BVnonzero, carry〉
     257        else Error … [MSG UnsupportedOp]
    173258      | _ ⇒ Error … [MSG UnsupportedOp]
    174259      ]
     
    181266      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
    182267      | BVnonzero ⇒ return 〈BVnonzero, carry〉
    183       | _ ⇒ Error … [MSG UnsupportedOp]
    184       ]
    185     | _ ⇒ Error … [MSG UnsupportedOp]
    186     ]
    187   | BVnull p1 ⇒
    188     match op with
    189     [ Xor ⇒
    190       match a2 with
    191       [ BVptr _ p2 _ ⇒
    192         if eqb p1 p2 then
    193           return 〈BVnonzero, carry〉
    194         else
    195           Error … [MSG UnsupportedOp]
    196       | BVnull p2 ⇒
    197         if eqb p1 p2 then
    198           return 〈BVByte (bv_zero …), carry〉
    199         else
    200           Error … [MSG UnsupportedOp]
     268      | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
    201269      | _ ⇒ Error … [MSG UnsupportedOp]
    202270      ]
     
    205273  | _ ⇒ Error … [MSG UnsupportedOp]
    206274  ].
    207 
  • 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 *)
  • src/common/FrontEndVal.ma

    r2286 r2435  
    66   resolve the sizes; they are not strictly checked. *)
    77
    8 let rec make_parts_aux (*r:region*) (n:nat) (H:lt n (size_pointer (*r*))) (tl:list (part (*r*))) on n : list (part (*r*)) ≝
    9 match n return λn.lt n ? → ? with
    10 [ O ⇒ λH'. (mk_part (*r*) O H')::tl
    11 | S m ⇒ λH'. make_parts_aux (*r*) m ? ((mk_part (*r*) n H)::tl)
    12 ] H.
    13 /2/
    14 qed.
    15 
    16 definition make_parts : (*∀r:region.*) list (part (*r*)) ≝
    17 (*λr.*) make_parts_aux (*r*) (pred (size_pointer (*r*))) ? [ ].
    18 //
    19 qed.
     8definition make_parts : list part ≝
     9  map ?? part_from_sig (range_strong size_pointer).
    2010
    2111definition make_be_null : (*region →*) list beval ≝
     
    8676| cons h t ⇒
    8777    match h with
    88     [ BVundef ⇒ Vundef
    89     | BVnonzero ⇒ Vundef
    90     | BVByte b ⇒ build_integer_val ty l
    91     | BVptr _ _ _ ⇒
     78    [ BVByte b ⇒ build_integer_val ty l
     79    | BVptr _ _ ⇒
    9280      match pointer_of_bevals l with
    9381      [ OK ptr ⇒ Vptr ptr
     
    9583      ]
    9684    | BVnull  pt ⇒ if eqb (part_no  pt) O ∧ check_be_null  (S O) t then Vnull  else Vundef
     85    | _ ⇒ Vundef
    9786    ]
    9887].
Note: See TracChangeset for help on using the changeset viewer.