working/0.1/preARMScript.sml

248   decode_op (pc,cpsr,s) (op,dst,src,jump) =
250           MOV -> (cpsr, write s (THE dst) (read s (HD src)))
256           LDMFD -> (case THE dst of
270           STMFD -> (case THE dst of
281           ADD -> (cpsr, (write s (THE dst) (read s (HD src) + read s (HD (TL (src))))))
283           SUB -> (cpsr, (write s (THE dst) (read s (HD src) - read s (HD (TL (src))))))
285           RSB -> (cpsr, (write s (THE dst) (read s (HD (TL (src))) - read s (HD src))))
287           MUL -> (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))))))
289           MLA -> (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))) +
292           AND -> (cpsr, (write s (THE dst) (read s (HD src) && read s (HD (TL (src))))))
294           ORR -> (cpsr, (write s (THE dst) (read s (HD src) !! read s (HD (TL (src))))))
296           EOR -> (cpsr, (write s (THE dst) (read s (HD src) ?? read s (HD (TL (src))))))
299           LSL -> (cpsr, (write s (THE dst)
302           LSR -> (cpsr, (write s (THE dst)
305           ASR -> (cpsr, (write s (THE dst)
308           ROR -> (cpsr, (write s (THE dst)
332           LDR -> (cpsr, (write s (THE dst) (read s (HD src))))
333                 (* write the value in src (i.e. the memory) to the dst (i.e. the register)*)
336           STR -> (cpsr, (write s (HD src) (read s (THE dst))))
337                 (* write the value in src (i.e. the register) to the dst (i.e. the memory)*)
342           MRS -> (cpsr, (write s (THE dst) cpsr))
352   `!pc cpsr s dst src jump.
353   (decode_op (pc,cpsr,s) (MOV,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src)))) /\
354   (decode_op (pc,cpsr,s) (ADD,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) + read s (HD (TL src))))) /\
355   (decode_op (pc,cpsr,s) (SUB,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) - read s (HD (TL src))))) /\
356   (decode_op (pc,cpsr,s) (RSB,SOME dst,src,jump) = (cpsr, write s dst (read s (HD (TL src)) - read s (HD src)))) /\
357   (decode_op (pc,cpsr,s) (MUL,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) * read s (HD (TL src))))) /\
358   (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)))))) /\
359   (decode_op (pc,cpsr,s) (AND,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) && read s (HD (TL src))))) /\
360   (decode_op (pc,cpsr,s) (ORR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) !! read s (HD (TL src))))) /\
361   (decode_op (pc,cpsr,s) (EOR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) ?? read s (HD (TL src))))) /\
376   (decode_op (pc,cpsr,s) (LSL,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) << w2n (read s (HD (TL src)))))) /\
377   (decode_op (pc,cpsr,s) (LSR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) >>> w2n (read s (HD (TL src)))))) /\
378   (decode_op (pc,cpsr,s) (ASR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) >> w2n (read s (HD (TL src)))))) /\
379   (decode_op (pc,cpsr,s) (ROR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) #>> w2n (read s (HD (TL src)))))) /\
380   (decode_op (pc,cpsr,s) (LDR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src)))) /\
381   (decode_op (pc,cpsr,s) (STR,SOME dst,src,jump) = (cpsr, write s (HD src) (read s dst))) /\
407   (decode_op (pc,cpsr,s) (MRS,SOME dst,src,jump) = (cpsr,write s dst cpsr)) /\
435     (decode_cond ((pc,cpsr,s):STATE) (((op,cond,sflag), dst, src, jump):INST)) =
437             NONE -> (pc+1, decode_op (pc,cpsr,s) (op,dst,src,jump))
440                           if (decode_cond_cpsr cpsr c) then (goto(pc,jump), decode_op (pc,cpsr,s) (op,dst,src,jump))
446   `!pc cpsr s op sflag dst src jump.
447           (decode_cond (pc,cpsr,s) ((op,NONE,sflag),dst,src,jump) = (pc+1, decode_op (pc,cpsr,s) (op,dst,src,jump))) /\
448      (decode_cond (pc,cpsr,s) ((op,SOME AL,sflag),dst,src,jump) = (goto(pc,jump), decode_op (pc,cpsr,s) (op,dst,src,jump))) /\
449           (decode_cond (pc,cpsr,s) ((op,SOME NV,sflag),dst,src,jump) = (pc+1, cpsr, s))`,