working/0.2/preARMScript.sml

240   decode_op (pc,cpsr,s) (op,dst,src,jump) =
242           MOV -> (cpsr, write s (THE dst) (read s (HD src)))
248           LDMFD -> (case THE dst of
262           STMFD -> (case THE dst of
273           ADD -> (cpsr, (write s (THE dst) (read s (HD src) + read s (HD (TL (src))))))
275           SUB -> (cpsr, (write s (THE dst) (read s (HD src) - read s (HD (TL (src))))))
277           RSB -> (cpsr, (write s (THE dst) (read s (HD (TL (src))) - read s (HD src))))
279           MUL -> (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))))))
281           MLA -> (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))) +
284           AND -> (cpsr, (write s (THE dst) (read s (HD src) && read s (HD (TL (src))))))
286           ORR -> (cpsr, (write s (THE dst) (read s (HD src) !! read s (HD (TL (src))))))
288           EOR -> (cpsr, (write s (THE dst) (read s (HD src) ?? read s (HD (TL (src))))))
291           LSL -> (cpsr, (write s (THE dst)
294           LSR -> (cpsr, (write s (THE dst)
297           ASR -> (cpsr, (write s (THE dst)
300           ROR -> (cpsr, (write s (THE dst)
324           LDR -> (cpsr, (write s (THE dst) (read s (HD src))))
325                 (* write the value in src (i.e. the memory) to the dst (i.e. the register)*)
328           STR -> (cpsr, (write s (HD src) (read s (THE dst))))
329                 (* write the value in src (i.e. the register) to the dst (i.e. the memory)*)
334           MRS -> (cpsr, (write s (THE dst) cpsr))
344   `!pc cpsr s dst src jump.
345   (decode_op (pc,cpsr,s) (MOV,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src)))) /\
346   (decode_op (pc,cpsr,s) (ADD,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) + read s (HD (TL src))))) /\
347   (decode_op (pc,cpsr,s) (SUB,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) - read s (HD (TL src))))) /\
348   (decode_op (pc,cpsr,s) (RSB,SOME dst,src,jump) = (cpsr, write s dst (read s (HD (TL src)) - read s (HD src)))) /\
349   (decode_op (pc,cpsr,s) (MUL,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) * read s (HD (TL src))))) /\
350   (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)))))) /\
351   (decode_op (pc,cpsr,s) (AND,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) && read s (HD (TL src))))) /\
352   (decode_op (pc,cpsr,s) (ORR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) !! read s (HD (TL src))))) /\
353   (decode_op (pc,cpsr,s) (EOR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) ?? read s (HD (TL src))))) /\
368   (decode_op (pc,cpsr,s) (LSL,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) << w2n (read s (HD (TL src)))))) /\
369   (decode_op (pc,cpsr,s) (LSR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) >>> w2n (read s (HD (TL src)))))) /\
370   (decode_op (pc,cpsr,s) (ASR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) >> w2n (read s (HD (TL src)))))) /\
371   (decode_op (pc,cpsr,s) (ROR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) #>> w2n (read s (HD (TL src)))))) /\
372   (decode_op (pc,cpsr,s) (LDR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src)))) /\
373   (decode_op (pc,cpsr,s) (STR,SOME dst,src,jump) = (cpsr, write s (HD src) (read s dst))) /\
399   (decode_op (pc,cpsr,s) (MRS,SOME dst,src,jump) = (cpsr,write s dst cpsr)) /\
427     (decode_cond ((pc,cpsr,s):STATE) (((op,cond,sflag), dst, src, jump):INST)) =
429             NONE -> (pc+1, decode_op (pc,cpsr,s) (op,dst,src,jump))
432                           if (decode_cond_cpsr cpsr c) then (goto(pc,jump), decode_op (pc,cpsr,s) (op,dst,src,jump))
438   `!pc cpsr s op sflag dst src jump.
439           (decode_cond (pc,cpsr,s) ((op,NONE,sflag),dst,src,jump) = (pc+1, decode_op (pc,cpsr,s) (op,dst,src,jump))) /\
440      (decode_cond (pc,cpsr,s) ((op,SOME AL,sflag),dst,src,jump) = (goto(pc,jump), decode_op (pc,cpsr,s) (op,dst,src,jump))) /\
441           (decode_cond (pc,cpsr,s) ((op,SOME NV,sflag),dst,src,jump) = (pc+1, cpsr, s))`,