 Timestamp:
 Mar 14, 2013, 5:34:54 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/BackEndOps.ma
r2720 r2871 227 227 definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝ 228 228 λcarry,op,a1,a2. 229 match a1 with 230 [ BVByte b1 ⇒ 231 (* if match op with [ Or ⇒ true  _ ⇒ false ] ∧ eq_bv … (zero …) b1 then 232 return 〈a2, carry〉 233 else *) (* maybe it will be needed, need to see actual translations *) 234 match a2 with 235 [ BVByte b2 ⇒ 236 ! carry ← Bit_of_val UnsupportedOp carry ; 237 let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in 238 return 〈BVByte result, BBbit carry〉 239  BVptr _ _ ⇒ 240 match op with 241 [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1 242  Addc ⇒ be_add_sub_byte true carry a2 b1 243  _ ⇒ Error … [MSG UnsupportedOp] 244 ] 245  BVnonzero ⇒ 246 match op with 247 [ Or ⇒ return 〈BVnonzero, carry〉 248  _ ⇒ Error … [MSG UnsupportedOp] 249 ] 250  _ ⇒ Error … [MSG UnsupportedOp] 251 ] 252  BVptr ptr1 p1 ⇒ 253 match a2 with 254 [ BVByte b2 ⇒ 255 match op with 256 [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2 257  Addc ⇒ be_add_sub_byte true carry a1 b2 258  Sub ⇒ be_add_sub_byte false carry a1 b2 259  _ ⇒ Error … [MSG UnsupportedOp] 260 ] 261  BVptr ptr2 p2 ⇒ 262 match op with 263 [ Sub ⇒ 229 match op with 230 [ Add ⇒ 231 match a1 with 232 [ BVByte b1 ⇒ be_add_sub_byte true (BBbit false) a2 b1 233  BVptr ptr1 p1 ⇒ 234 match a2 with 235 [ BVByte b2 ⇒ be_add_sub_byte true (BBbit false) a1 b2 236  _ ⇒ Error … [MSG UnsupportedOp] 237 ] 238  _ ⇒ Error … [MSG UnsupportedOp] 239 ] 240  Addc ⇒ 241 match a1 with 242 [ BVByte b1 ⇒ be_add_sub_byte true carry a2 b1 243  BVptr ptr1 p1 ⇒ 244 match a2 with 245 [ BVByte b2 ⇒ be_add_sub_byte true carry a1 b2 246  _ ⇒ Error … [MSG UnsupportedOp] 247 ] 248  _ ⇒ Error … [MSG UnsupportedOp] 249 ] 250  Sub ⇒ 251 match a1 with 252 [ BVByte b1 ⇒ be_add_sub_byte false carry a2 b1 253  BVptr ptr1 p1 ⇒ 254 match a2 with 255 [ BVByte b2 ⇒ be_add_sub_byte false carry a1 b2 256  BVptr ptr2 p2 ⇒ 264 257 match ptype ptr1 with 265 258 [ Code ⇒ Error … [MSG UnsupportedOp] … … 275 268 else Error … [MSG UnsupportedOp] 276 269 ] 277  Xor ⇒ 278 if eqb p1 p2 then 279 return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉 280 else Error … [MSG UnsupportedOp] 281  _ ⇒ Error … [MSG UnsupportedOp] 282 ] 283  BVnull p2 ⇒ 284 match op with 285 [ Xor ⇒ 286 if eqb p1 p2 then 287 return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉 288 else 289 Error … [MSG UnsupportedOp] 290  _ ⇒ Error … [MSG UnsupportedOp] 291 ] 292  _ ⇒ Error … [MSG UnsupportedOp] 293 ] 294  BVnull p1 ⇒ 295 match a2 with 296 [ BVptr ptr2 p2 ⇒ 297 match op with 298 [ Xor ⇒ 299 if eqb p1 p2 then 300 return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉 301 else 302 Error … [MSG UnsupportedOp] 303  _ ⇒ Error … [MSG UnsupportedOp] 304 ] 305  BVnull p2 ⇒ 306 match op with 307 [ Xor ⇒ 308 if eqb p1 p2 then 309 return 〈BVXor (None ?) (None ?) p1, carry〉 310 else 311 Error … [MSG UnsupportedOp] 312  _ ⇒ Error … [MSG UnsupportedOp] 313 ] 314  _ ⇒ Error … [MSG UnsupportedOp] 315 ] 316  BVXor ptr1_opt ptr1_opt' p1 ⇒ 317 match a2 with 318 [ BVByte b2 ⇒ 319 match op with 320 [ Or ⇒ 321 if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉 322 else Error … [MSG UnsupportedOp] 323  _ ⇒ Error … [MSG UnsupportedOp] 324 ] 325  BVnonzero ⇒ 326 match op with 327 [ Or ⇒ 328 return 〈BVnonzero, carry〉 329  _ ⇒ Error … [MSG UnsupportedOp] 330 ] 331  BVXor ptr2_opt ptr2_opt' p2 ⇒ 332 match op with 333 [ Or ⇒ 270  _ ⇒ Error … [MSG UnsupportedOp] 271 ] 272  _ ⇒ Error … [MSG UnsupportedOp] 273 ] 274  Or ⇒ 275 match a1 with 276 [ BVByte b1 ⇒ 277 match a2 with 278 [ BVByte b2 ⇒ 279 let res ≝ \fst (op2 eval false Or b1 b2) in 280 return 〈BVByte res, carry〉 281  BVnonzero ⇒ return 〈BVnonzero, carry〉 282  _ ⇒ Error … [MSG UnsupportedOp] 283 ] 284  BVXor ptr1_opt ptr1_opt' p1 ⇒ 285 match a2 with 286 [ BVXor ptr2_opt ptr2_opt' p2 ⇒ 334 287 if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then 335 288 let eq_at ≝ λp,ptr1,ptr2. … … 342 295 else return 〈BVnonzero, carry〉 343 296 else Error … [MSG UnsupportedOp] 344  _ ⇒ Error … [MSG UnsupportedOp] 345 ] 346  _ ⇒ Error … [MSG UnsupportedOp] 347 ] 348  BVnonzero ⇒ 349 match a2 with 350 [ BVByte _ ⇒ 351 match op with 352 [ Or ⇒ return 〈BVnonzero, carry〉 297  BVnonzero ⇒ return 〈BVnonzero, carry〉 353 298  _ ⇒ Error … [MSG UnsupportedOp] 354 299 ] 355 300  BVnonzero ⇒ 356 match op with 357 [ Or ⇒ return 〈BVnonzero, carry〉 358  _ ⇒ Error … [MSG UnsupportedOp] 359 ] 360  BVXor _ _ _ ⇒ 361 match op with 362 [ Or ⇒ return 〈BVnonzero, carry〉 363  _ ⇒ Error … [MSG UnsupportedOp] 364 ] 365  _ ⇒ Error … [MSG UnsupportedOp] 366 ] 367  _ ⇒ Error … [MSG UnsupportedOp] 301 match a2 with 302 [ BVByte _ ⇒ return 〈BVnonzero, carry〉 303  BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉 304  BVnonzero ⇒ return 〈BVnonzero, carry〉 305  _ ⇒ Error … [MSG UnsupportedOp] 306 ] 307  _ ⇒ Error … [MSG UnsupportedOp] 308 ] 309  Xor ⇒ 310 match a1 with 311 [ BVByte b1 ⇒ 312 match a2 with 313 [ BVByte b2 ⇒ 314 let res ≝ \fst (op2 eval false Xor b1 b2) in 315 return 〈BVByte res, carry〉 316  _ ⇒ Error … [MSG UnsupportedOp] 317 ] 318  BVptr ptr1 p1 ⇒ 319 match a2 with 320 [ BVptr ptr2 p2 ⇒ 321 if eqb p1 p2 then 322 return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉 323 else Error … [MSG UnsupportedOp] 324  BVnull p2 ⇒ 325 if eqb p1 p2 then 326 return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉 327 else 328 Error … [MSG UnsupportedOp] 329  _ ⇒ Error … [MSG UnsupportedOp] 330 ] 331  BVnull p1 ⇒ 332 match a2 with 333 [ BVptr ptr2 p2 ⇒ 334 if eqb p1 p2 then 335 return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉 336 else 337 Error … [MSG UnsupportedOp] 338  BVnull p2 ⇒ 339 if eqb p1 p2 then 340 return 〈BVXor (None ?) (None ?) p1, carry〉 341 else 342 Error … [MSG UnsupportedOp] 343  _ ⇒ Error … [MSG UnsupportedOp] 344 ] 345  _ ⇒ Error … [MSG UnsupportedOp] 346 ] 347  And ⇒ 348 ! b1 ← Byte_of_val UnsupportedOp a1 ; 349 ! b2 ← Byte_of_val UnsupportedOp a2 ; 350 let res ≝ \fst (op2 eval false And b1 b2) in 351 return 〈BVByte res, carry〉 368 352 ].
Note: See TracChangeset
for help on using the changeset viewer.