Lines Matching refs:dst
1267 |- (!st dst src.
1268 mdecode st (MLDR dst src) =
1269 write st (toREG dst) (read st (toMEM src))) /\
1270 (!st dst src.
1271 mdecode st (MSTR dst src) =
1272 write st (toMEM dst) (read st (toREG src))) /\
1273 (!st dst src.
1274 mdecode st (MMOV dst src) =
1275 write st (toREG dst) (read st (toEXP src))) /\
1276 (!st dst src1 src2.
1277 mdecode st (MADD dst src1 src2) =
1278 write st (toREG dst) (read st (toREG src1) + read st (toEXP src2))) /\
1279 (!st dst src1 src2.
1280 mdecode st (MSUB dst src1 src2) =
1281 write st (toREG dst) (read st (toREG src1) - read st (toEXP src2))) /\
1282 (!st dst src1 src2.
1283 mdecode st (MRSB dst src1 src2) =
1284 write st (toREG dst) (read st (toEXP src2) - read st (toREG src1))) /\
1285 (!st dst src1 src2_reg.
1286 mdecode st (MMUL dst src1 src2_reg) =
1287 write st (toREG dst)
1289 (!st dst src1 src2.
1290 mdecode st (MAND dst src1 src2) =
1291 write st (toREG dst) (read st (toREG src1) && read st (toEXP src2))) /\
1292 (!st dst src1 src2.
1293 mdecode st (MORR dst src1 src2) =
1294 write st (toREG dst) (read st (toREG src1) !! read st (toEXP src2))) /\
1295 (!st dst src1 src2.
1296 mdecode st (MEOR dst src1 src2) =
1297 write st (toREG dst) (read st (toREG src1) ?? read st (toEXP src2))) /\
1298 (!st dst src2_reg src2_num.
1299 mdecode st (MLSL dst src2_reg src2_num) =
1300 write st (toREG dst) (read st (toREG src2_reg) << w2n src2_num)) /\
1301 (!st dst src2_reg src2_num.
1302 mdecode st (MLSR dst src2_reg src2_num) =
1303 write st (toREG dst) (read st (toREG src2_reg) >>> w2n src2_num)) /\
1304 (!st dst src2_reg src2_num.
1305 mdecode st (MASR dst src2_reg src2_num) =
1306 write st (toREG dst) (read st (toREG src2_reg) >> w2n src2_num)) /\
1307 (!st dst src2_reg src2_num.
1308 mdecode st (MROR dst src2_reg src2_num) =
1309 write st (toREG dst) (read st (toREG src2_reg) #>> w2n src2_num)) /\
1310 (!st dst' srcL. mdecode st (MPUSH dst' srcL) = pushL st dst' srcL) /\
1311 !st dst' srcL. mdecode st (MPOP dst' srcL) = popL st dst' srcL
1362 |- (!dst src.
1363 translate_assignment (MMOV dst src) =
1364 ((MOV,NONE,F),SOME (toREG dst),[toEXP src],NONE)) /\
1365 (!dst src1 src2.
1366 translate_assignment (MADD dst src1 src2) =
1367 ((ADD,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\
1368 (!dst src1 src2.
1369 translate_assignment (MSUB dst src1 src2) =
1370 ((SUB,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\
1371 (!dst src1 src2.
1372 translate_assignment (MRSB dst src1 src2) =
1373 ((RSB,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\
1374 (!dst src1 src2_reg.
1375 translate_assignment (MMUL dst src1 src2_reg) =
1376 ((MUL,NONE,F),SOME (toREG dst),[toREG src1; toREG src2_reg],NONE)) /\
1377 (!dst src1 src2.
1378 translate_assignment (MAND dst src1 src2) =
1379 ((AND,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\
1380 (!dst src1 src2.
1381 translate_assignment (MORR dst src1 src2) =
1382 ((ORR,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\
1383 (!dst src1 src2.
1384 translate_assignment (MEOR dst src1 src2) =
1385 ((EOR,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\
1386 (!dst src2_reg src2_num.
1387 translate_assignment (MLSL dst src2_reg src2_num) =
1388 ((LSL,NONE,F),SOME (toREG dst),[toREG src2_reg; WCONST (w2w src2_num)],
1390 (!dst src2_reg src2_num.
1391 translate_assignment (MLSR dst src2_reg src2_num) =
1392 ((LSR,NONE,F),SOME (toREG dst),[toREG src2_reg; WCONST (w2w src2_num)],
1394 (!dst src2_reg src2_num.
1395 translate_assignment (MASR dst src2_reg src2_num) =
1396 ((ASR,NONE,F),SOME (toREG dst),[toREG src2_reg; WCONST (w2w src2_num)],
1398 (!dst src2_reg src2_num.
1399 translate_assignment (MROR dst src2_reg src2_num) =
1400 ((ROR,NONE,F),SOME (toREG dst),[toREG src2_reg; WCONST (w2w src2_num)],
1402 (!dst src.
1403 translate_assignment (MLDR dst src) =
1404 ((LDR,NONE,F),SOME (toREG dst),[toMEM src],NONE)) /\
1405 (!dst src.
1406 translate_assignment (MSTR dst src) =
1407 ((STR,NONE,F),SOME (toREG src),[toMEM dst],NONE)) /\
1408 (!dst srcL.
1409 translate_assignment (MPUSH dst srcL) =
1410 ((STMFD,NONE,F),SOME (WREG dst),MAP REG srcL,NONE)) /\
1411 !dst srcL.
1412 translate_assignment (MPOP dst srcL) =
1413 ((LDMFD,NONE,F),SOME (WREG dst),MAP REG srcL,NONE)