Changeset 2871 for src/common/BackEndOps.ma
- Timestamp:
- Mar 14, 2013, 5:34:54 PM (8 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.