working/0.1/ILScript.sml

163   (!dst src.mdecode st (MLDR dst src) =
164       write st (toREG dst) (read st (toMEM src))) /\
165   (!dst src.mdecode st (MSTR dst src) =
166       write st (toMEM dst) (read st (toREG src))) /\
167   (mdecode st (MMOV dst src) =
168       write st (toREG dst) (read st (toEXP src))) /\
169   (mdecode st (MADD dst src1 src2) =
170       write st (toREG dst) (read st (toREG src1) + read st (toEXP src2))) /\
171   (mdecode st (MSUB dst src1 src2) =
172       write st (toREG dst) (read st (toREG src1) - read st (toEXP src2))) /\
173   (mdecode st (MRSB dst src1 src2) =
174       write st (toREG dst) (read st (toEXP src2) - read st (toREG src1))) /\
175   (mdecode st (MMUL dst src1 src2_reg) =
176       write st (toREG dst) (read st (toREG src1) * read st (toREG src2_reg))) /\
177   (mdecode st (MAND dst src1 src2) =
178       write st (toREG dst) (read st (toREG src1) && read st (toEXP src2))) /\
179   (mdecode st (MORR dst src1 src2) =
180       write st (toREG dst) (read st (toREG src1) !! read st (toEXP src2))) /\
181   (mdecode st (MEOR dst src1 src2) =
182       write st (toREG dst) (read st (toREG src1) ?? read st (toEXP src2))) /\
183   (mdecode st (MLSL dst src2_reg src2_num) =
184       write st (toREG dst) (read st (toREG src2_reg) << w2n src2_num)) /\
185   (mdecode st (MLSR dst src2_reg src2_num) =
186       write st (toREG dst) (read st (toREG src2_reg) >>> w2n src2_num)) /\
187   (mdecode st (MASR dst src2_reg src2_num) =
188       write st (toREG dst) (read st (toREG src2_reg) >> w2n src2_num)) /\
189   (mdecode st (MROR dst src2_reg src2_num) =
190       write st (toREG dst) (read st (toREG src2_reg) #>> w2n src2_num)) /\
191   (mdecode st (MPUSH dst' srcL) =
192       pushL st dst' srcL) /\
193   (mdecode st (MPOP dst' srcL) =
194       popL st dst' srcL)
198     (translate_assignment (MMOV dst src) = ((MOV,NONE,F),SOME (toREG dst), [toEXP src], NONE):INST) /\
199     (translate_assignment (MADD dst src1 src2) = ((ADD,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
200     (translate_assignment (MSUB dst src1 src2) = ((SUB,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
201     (translate_assignment (MRSB dst src1 src2) = ((RSB,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
202     (translate_assignment (MMUL dst src1 src2_reg) = ((MUL,NONE,F),SOME (toREG dst), [toREG src1; toREG src2_reg], NONE):INST) /\
203     (translate_assignment (MAND dst src1 src2) = ((AND,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
204     (translate_assignment (MORR dst src1 src2) = ((ORR,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
205     (translate_assignment (MEOR dst src1 src2) = ((EOR,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
206     (translate_assignment (MLSL dst src2_reg src2_num) = ((LSL,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\
207     (translate_assignment (MLSR dst src2_reg src2_num) = ((LSR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\
208     (translate_assignment (MASR dst src2_reg src2_num) = ((ASR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\
209     (translate_assignment (MROR dst src2_reg src2_num) = ((ROR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\
210     (!dst src.translate_assignment (MLDR dst src) = ((LDR,NONE,F),SOME (toREG dst), [toMEM src], NONE):INST) /\
211     (!dst src.translate_assignment (MSTR dst src) = ((STR,NONE,F),SOME (toREG src), [toMEM dst], NONE):INST) /\
212     (!dst srcL.translate_assignment (MPUSH dst srcL) = ((STMFD,NONE,F),SOME (WREG dst), MAP REG srcL, NONE):INST) /\
213     (!dst srcL.translate_assignment (MPOP dst srcL) = ((LDMFD,NONE,F),SOME (WREG dst), MAP REG srcL, NONE):INST)