working/0.1/ILTheory.sig

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)