dev/sw/preARMScript.sml

182     read (regs,mem) (exp:EXP) =
196   ` (read (regs,mem) (MEM (r,POS k)) = mem ' (MEM_ADDR (regs ' (n2w r)) + (n2w k))) /\
197     (read (regs,mem) (MEM (r,NEG k)) = mem ' (MEM_ADDR (regs ' (n2w r)) - (n2w k))) /\
198     (read (regs,mem) (NCONST i) = n2w i) /\
199     (read (regs,mem) (WCONST w) = w) /\
200     (read (regs,mem) (REG r) = regs ' (n2w r)) /\
201     (read (regs,mem) (MEM (r,INR)) = ARB)`,
254           MOV => (cpsr, write s (THE dst) (read s (HD src)))
262                              (* We must read values from the original state instead of the updated state *)
263                             (cpsr, FST (FOLDL (\(s1,i) reg. (write s1 reg (read s (MEM(r,POS(i+1)))), i+1)) (s,0) src))
266                             (cpsr, write (FST (FOLDL (\(s1,i) reg. (write s1 reg (read s (MEM(r,POS(i+1)))), i+1)) (s,0) src))
267                                                  (REG r) (read s (REG r) + n2w (4*LENGTH src)))
277                                  (* We must read values from the original state instead of the updated state *)
278                                  FST (FOLDL (\(s1,i) reg. (write s1 (MEM(r,NEG i)) (read s reg), i+1)) (s,0) (REVERSE src))) |
281                                  write (FST (FOLDL (\(s1,i) reg. (write s1 (MEM(r,NEG i)) (read s reg), i+1)) (s,0) (REVERSE src)))
282                                         (REG r) (read s (REG r) - n2w (4*LENGTH src)))
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))) +
294                                                   read s (HD (TL (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))))))
304                                 (read s (HD src) << w2n (read s (HD (TL (src)))))))
307                                 (read s (HD src) >>> w2n (read s (HD (TL (src)))))))
310                                 (read s (HD src) >> w2n (read s (HD (TL (src)))))))
313                                 (read s (HD src) #>> w2n (read s (HD (TL (src)))))))
316           CMP => (let a = read s (HD src) in
317                  let b = read s (HD (TL (src))) in
327           TST => (let a = read s (HD src) in
328                  let b = read s (HD (TL (src))) in
336           LDR => (cpsr, (write s (THE dst) (read s (HD src))))
340           STR => (cpsr, (write s (HD src) (read s (THE dst))))
344           MSR => (read s (HD src), s)
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))))) /\
367       let a = read s (HD src) in
368       let b = read s (HD (TL (src))) in
374       (let a = read s (HD src) in
375                      let b = read s (HD (TL (src))) in
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))) /\
389                              (write s1 reg (read s (MEM (r,POS (i + 1)))),
396                                    (read s (MEM (r,POS (i + 1)))),i + 1))
398                              (read s (REG r) + n2w (4*LENGTH src)))) /\
402                              (write s1 (MEM (r,NEG i)) (read s reg),i + 1))
408                                 (write s1 (MEM (r,NEG i)) (read s reg),
410                        (read s (REG r) - n2w (4*LENGTH src)))) /\
412   (decode_op (pc,cpsr,s) (MSR,NONE,src,jump) = (read s (HD src),s)) /\