Changeset 2435 for src/common/BackEndOps.ma
 Timestamp:
 Nov 6, 2012, 4:12:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/BackEndOps.ma
r2286 r2435 66 66 let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in 67 67 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')〉 88 96 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 ] 93 102  _ ⇒ Error … [MSG UnsupportedOp] 94 103 ]. 95 @hide_prf [//]96 lapply prf @(eqb_elim k) #H * >H %104 @hide_prf 105 lapply prf @(eqb_elim p') #H * >H % 97 106 qed. 107 108 definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝ 109 λn,v,p,H. 110 let 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) 114 change with (? = BitVector (? + S p*8)) 115 >(commutative_times_fast (S p)) 116 <distributive_times_plus_fast 117 <(plus_minus_m_m … H) % 118 qed. 119 120 definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝ 121 λA,eq,m,n. 122 match 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 ]. 98 134 99 135 (* This tables shows what binary ops may be defined on bevals depending on 100 136 the arguments (columns marked by 1st argument, rows by 2nd). Further 101 137 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 +++++++ 115 153 *) 116 154 definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝ … … 118 156 match a1 with 119 157 [ 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 ⇒ 139 180 match a2 with 140 181 [ BVByte b2 ⇒ … … 145 186  _ ⇒ Error … [MSG UnsupportedOp] 146 187 ] 147  BVptr bl2 p2 o2 ⇒188  BVptr ptr2 p2 ⇒ 148 189 match op with 149 190 [ 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 151 197 ! 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 ] 157 204  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〉 163 207 else Error … [MSG UnsupportedOp] 164 208  _ ⇒ Error … [MSG UnsupportedOp] … … 168 212 [ Xor ⇒ 169 213 if eqb p1 p2 then 170 return 〈BV nonzero, carry〉214 return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉 171 215 else 172 216 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] 173 258  _ ⇒ Error … [MSG UnsupportedOp] 174 259 ] … … 181 266 [ BVByte _ ⇒ return 〈BVnonzero, carry〉 182 267  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〉 201 269  _ ⇒ Error … [MSG UnsupportedOp] 202 270 ] … … 205 273  _ ⇒ Error … [MSG UnsupportedOp] 206 274 ]. 207
Note: See TracChangeset
for help on using the changeset viewer.