dev/sw/preARMScript.sml

252   decode_op (pc,cpsr,s) (op,dst,src,jump) =
254           MOV => (cpsr, write s (THE dst) (read s (HD src)))
260           LDMFD => (case THE dst of
274           STMFD => (case THE dst of
285           ADD => (cpsr, (write s (THE dst) (read s (HD src) + read s (HD (TL (src))))))
287           SUB => (cpsr, (write s (THE dst) (read s (HD src) - read s (HD (TL (src))))))
289           RSB => (cpsr, (write s (THE dst) (read s (HD (TL (src))) - read s (HD src))))
291           MUL => (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))))))
293           MLA => (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))) +
296           AND => (cpsr, (write s (THE dst) (read s (HD src) && read s (HD (TL (src))))))
298           ORR => (cpsr, (write s (THE dst) (read s (HD src) !! read s (HD (TL (src))))))
300           EOR => (cpsr, (write s (THE dst) (read s (HD src) ?? read s (HD (TL (src))))))
303           LSL => (cpsr, (write s (THE dst)
306           LSR => (cpsr, (write s (THE dst)
309           ASR => (cpsr, (write s (THE dst)
312           ROR => (cpsr, (write s (THE dst)
336           LDR => (cpsr, (write s (THE dst) (read s (HD src))))
337                 (* write the value in src (i.e. the memory) to the dst (i.e. the register)*)
340           STR => (cpsr, (write s (HD src) (read s (THE dst))))
341                 (* write the value in src (i.e. the register) to the dst (i.e. the memory)*)
346           MRS => (cpsr, (write s (THE dst) cpsr))
356   `!pc cpsr s dst src jump.
357   (decode_op (pc,cpsr,s) (MOV,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src)))) /\
358   (decode_op (pc,cpsr,s) (ADD,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) + read s (HD (TL src))))) /\
359   (decode_op (pc,cpsr,s) (SUB,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) - read s (HD (TL src))))) /\
360   (decode_op (pc,cpsr,s) (RSB,SOME dst,src,jump) = (cpsr, write s dst (read s (HD (TL src)) - read s (HD src)))) /\
361   (decode_op (pc,cpsr,s) (MUL,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) * read s (HD (TL src))))) /\
362   (decode_op (pc,cpsr,s) (MLA,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) * read s (HD (TL src)) + read s (HD (TL (TL src)))))) /\
363   (decode_op (pc,cpsr,s) (AND,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) && read s (HD (TL src))))) /\
364   (decode_op (pc,cpsr,s) (ORR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) !! read s (HD (TL src))))) /\
365   (decode_op (pc,cpsr,s) (EOR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) ?? read s (HD (TL src))))) /\
380   (decode_op (pc,cpsr,s) (LSL,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) << w2n (read s (HD (TL src)))))) /\
381   (decode_op (pc,cpsr,s) (LSR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) >>> w2n (read s (HD (TL src)))))) /\
382   (decode_op (pc,cpsr,s) (ASR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) >> w2n (read s (HD (TL src)))))) /\
383   (decode_op (pc,cpsr,s) (ROR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) #>> w2n (read s (HD (TL src)))))) /\
384   (decode_op (pc,cpsr,s) (LDR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src)))) /\
385   (decode_op (pc,cpsr,s) (STR,SOME dst,src,jump) = (cpsr, write s (HD src) (read s dst))) /\
411   (decode_op (pc,cpsr,s) (MRS,SOME dst,src,jump) = (cpsr,write s dst cpsr)) /\
439     (decode_cond ((pc,cpsr,s):STATE) (((op,cond,sflag), dst, src, jump):INST)) =
441             NONE => (pc+1, decode_op (pc,cpsr,s) (op,dst,src,jump))
444                           if (decode_cond_cpsr cpsr c) then (goto(pc,jump), decode_op (pc,cpsr,s) (op,dst,src,jump))
450   `!pc cpsr s op sflag dst src jump.
451           (decode_cond (pc,cpsr,s) ((op,NONE,sflag),dst,src,jump) = (pc+1, decode_op (pc,cpsr,s) (op,dst,src,jump))) /\
452      (decode_cond (pc,cpsr,s) ((op,SOME AL,sflag),dst,src,jump) = (goto(pc,jump), decode_op (pc,cpsr,s) (op,dst,src,jump))) /\
453           (decode_cond (pc,cpsr,s) ((op,SOME NV,sflag),dst,src,jump) = (pc+1, cpsr, s))`,