working/0.2/CFLScript.sml

202   (!dst src.mdecode st (MLDR dst src) =
203       write st (toREG dst) (read st (toMEM src))) /\
204   (!dst src.mdecode st (MSTR dst src) =
205       write st (toMEM dst) (read st (toREG src))) /\
206   (mdecode st (MMOV dst src) =
207       write st (toREG dst) (read st (toEXP src))) /\
208   (mdecode st (MADD dst src1 src2) =
209       write st (toREG dst) (read st (toREG src1) + read st (toEXP src2))) /\
210   (mdecode st (MSUB dst src1 src2) =
211       write st (toREG dst) (read st (toREG src1) - read st (toEXP src2))) /\
212   (mdecode st (MRSB dst src1 src2) =
213       write st (toREG dst) (read st (toEXP src2) - read st (toREG src1))) /\
214   (mdecode st (MMUL dst src1 src2) =
215       write st (toREG dst) (read st (toREG src1) * read st (toEXP src2))) /\
216   (mdecode st (MAND dst src1 src2) =
217       write st (toREG dst) (read st (toREG src1) && read st (toEXP src2))) /\
218   (mdecode st (MORR dst src1 src2) =
219       write st (toREG dst) (read st (toREG src1) !! read st (toEXP src2))) /\
220   (mdecode st (MEOR dst src1 src2) =
221       write st (toREG dst) (read st (toREG src1) ?? read st (toEXP src2))) /\
222   (mdecode st (MLSL dst src2_reg src2_num) =
223       write st (toREG dst) (read st (toREG src2_reg) << w2n src2_num)) /\
224   (mdecode st (MLSR dst src2_reg src2_num) =
225       write st (toREG dst) (read st (toREG src2_reg) >>> w2n src2_num)) /\
226   (mdecode st (MASR dst src2_reg src2_num) =
227       write st (toREG dst) (read st (toREG src2_reg) >> w2n src2_num)) /\
228   (mdecode st (MROR dst src2_reg src2_num) =
229       write st (toREG dst) (read st (toREG src2_reg) #>> w2n src2_num)) /\
230   (mdecode st (MPUSH dst' srcL) =
231       pushL st dst' srcL) /\
232   (mdecode st (MPOP dst' srcL) =
233       popL st dst' srcL)
237     (translate_assignment (MMOV dst src) = ((MOV,NONE,F),SOME (toREG dst), [toEXP src], NONE):INST) /\
238     (translate_assignment (MADD dst src1 src2) = ((ADD,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
239     (translate_assignment (MSUB dst src1 src2) = ((SUB,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
240     (translate_assignment (MRSB dst src1 src2) = ((RSB,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
241     (translate_assignment (MMUL dst src1 src2) = ((MUL,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
242     (translate_assignment (MAND dst src1 src2) = ((AND,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
243     (translate_assignment (MORR dst src1 src2) = ((ORR,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
244     (translate_assignment (MEOR dst src1 src2) = ((EOR,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\
245     (translate_assignment (MLSL dst src2_reg src2_num) = ((LSL,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\
246     (translate_assignment (MLSR dst src2_reg src2_num) = ((LSR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\
247     (translate_assignment (MASR dst src2_reg src2_num) = ((ASR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\
248     (translate_assignment (MROR dst src2_reg src2_num) = ((ROR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\
249     (!dst src.translate_assignment (MLDR dst src) = ((LDR,NONE,F),SOME (toREG dst), [toMEM src], NONE):INST) /\
250     (!dst src.translate_assignment (MSTR dst src) = ((STR,NONE,F),SOME (toREG src), [toMEM dst], NONE):INST) /\
251     (!dst srcL.translate_assignment (MPUSH dst srcL) = ((STMFD,NONE,F),SOME (WREG dst), MAP REG srcL, NONE):INST) /\
252     (!dst srcL.translate_assignment (MPOP dst srcL) = ((LDMFD,NONE,F),SOME (WREG dst), MAP REG srcL, NONE):INST)