(**************************************************************************)
(*     ARM/Power Multiprocessor Machine Code Semantics: HOL sources       *)
(*                                                                        *)
(*                                                                        *)
(*  Jade Alglave (2), Anthony Fox (1), Samin Isthiaq (3),                 *)
(*  Magnus Myreen (1), Susmit Sarkar (1), Peter Sewell (1),               *)
(*  Francesco Zappa Nardelli (2)                                          *)
(*                                                                        *)
(*   (1) Computer Laboratory, University of Cambridge                     *)
(*   (2) Moscova project, INRIA Paris-Rocquencourt                        *)
(*   (3) Microsoft Research Cambridge                                     *)
(*                                                                        *)
(*     Copyright 2007-2008                                                *)
(*                                                                        *)
(*  Redistribution and use in source and binary forms, with or without    *)
(*  modification, are permitted provided that the following conditions    *)
(*  are met:                                                              *)
(*                                                                        *)
(*  1. Redistributions of source code must retain the above copyright     *)
(*     notice, this list of conditions and the following disclaimer.      *)
(*  2. Redistributions in binary form must reproduce the above copyright  *)
(*     notice, this list of conditions and the following disclaimer in    *)
(*     the documentation and/or other materials provided with the         *)
(*     distribution.                                                      *)
(*  3. The names of the authors may not be used to endorse or promote     *)
(*     products derived from this software without specific prior         *)
(*     written permission.                                                *)
(*                                                                        *)
(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,          *)
(*  WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING             *)
(*  NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS    *)
(*  SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.          *)
(*                                                                        *)
(**************************************************************************)

open HolKernel boolLib bossLib Parse;
open wordsLib;

(* NOTE: arm_event_opsemScript.sml IS AUTOGENERATED FROM arm_opsemScript.sml *)
(* DO NOT EDIT THE FORMER DIRECTLY *)

open arm_seq_monadTheory;

open HolDoc;
val _ = new_theory "arm_opsem";

(* ---------------------------------------------------------------------- *>

  We define the semantics of an instruction.

<* ---------------------------------------------------------------------- *)

val _ = set_fixity ">>-" (Infixr 660);
val _ = set_fixity ">>=" (Infixr 660);

val _ = overload_on(">>-", ``seqT``);
val _ = overload_on(">>=", ``bindT``);
val _ = overload_on("!!",  ``parT``);

val user_or_system_mode_def = Define`
  user_or_system_mode m = (m = usr) \/ (m = sys)`;

val word4_mode_to_reg_def = Define`
  word4_mode_to_reg (w:word4, m) =
  num2ARMreg (let n = w2n w in
    (if (n = 15) \/ user_or_system_mode m \/
        (m = fiq) /\ n < 8 \/
       ~(m = fiq) /\ n < 13
     then
       n
     else case m of
        fiq -> n + 8
     || irq -> n + 10
     || svc -> n + 12
     || abt -> n + 14
     || und -> n + 16
     || _ -> ARB))`;

val read_regm_def = Define`
  read_regm ii x = read_reg ii (word4_mode_to_reg x)`;

val write_regm_def = Define`
  write_regm ii x = write_reg ii (word4_mode_to_reg x)`;

val mode_to_psr_def = Define`
  mode_to_psr mode =
    case mode of
       usr -> CPSR
    || fiq -> SPSR_fiq
    || irq -> SPSR_irq
    || svc -> SPSR_svc
    || abt -> SPSR_abt
    || und -> SPSR_und
    || sys -> CPSR`;

val exception_to_mode_def = Define`
  exception_to_mode type =
    case type of
       Exception_reset          -> svc
    || Exception_undefined      -> und
    || Exception_supervisor     -> svc
    || Exception_address        -> svc
    || Exception_prefetch_abort -> abt
    || Exception_data_abort     -> abt
    || Exception_interrupt      -> irq
    || Exception_fast           -> fiq`;

val mode_to_word5_def = Define`
  mode_to_word5 mode : word5 =
    case mode of
       usr -> 16w
    || fiq -> 17w
    || irq -> 18w
    || svc -> 19w
    || abt -> 23w
    || und -> 27w
    || sys -> 31w`;

val exception_to_address_def = Define`
  exception_to_address high_vectors type : word32 =
    (if high_vectors then 0xFFFF0000w else 0w) +
    n2w (4 * ARMexception2num type)`;

val condition_passed_def = Define`
  condition_passed (N,Z,C,V) cond =
    case cond of
       EQ -> Z
    || NE -> ~Z
    || CS -> C
    || CC -> ~C
    || MI -> N
    || PL -> ~N
    || VS -> V
    || VC -> ~V
    || HI -> C /\ ~Z
    || LS -> ~C \/ Z
    || GE -> N = V
    || LT -> ~(N = V)
    || GT -> ~Z /\ (N = V)
    || LE -> Z \/ ~(N = V)
    || AL -> T
    || NV -> F`;

(* ------------------------------------------------------------------------ *)

val inc_pc_def = Define`
  inc_pc ii = read_reg ii r15 >>= (\x. write_reg ii r15 (x + 4w))`;

val branch_write_pc_def = Define`
  branch_write_pc ii (addr:word32) =
    (read_version ii !! read_instr_set ii) >>=
    (\(version,iset).
       if iset = InstrSet_ARM then
         if version < 6 /\ (( 1 >< 0) addr = 0w:word2)
         then
           failureT
         else
           write_reg ii r15 ((31 <> 2) addr)
       else
         write_reg ii r15 ((31 <> 1) addr))`;

(* ------------------------------------------------------------------------ *)

val LSL_def = Define`
  LSL (m:word32) (n:word8) c =
    if n = 0w then (c, m) else
      (n <=+ 32w /\ m ' (32 - w2n n), m << w2n n)`;

val LSR_def = Define`
  LSR (m:word32) (n:word8) c =
    if n = 0w then LSL m 0w c else
      (n <=+ 32w /\ m ' (w2n n - 1), m >>> w2n n)`;

val ASR_def = Define`
  ASR (m:word32) (n:word8) c =
    if n = 0w then LSL m 0w c else
      (m ' (MIN 31 (w2n n - 1)), m >> w2n n)`;

val ROR_def = Define`
  ROR (m:word32) (n:word8) c =
    if n = 0w then LSL m 0w c else
      (m ' (w2n ((w2w n):word5) - 1), m #>> w2n n)`;

val immediate_def = Define`
  immediate ii (rot:word4) (imm:word8) =
    (inc_pc ii !! read_flags ii) >>=
    (\(unit,(n,z,c,v)). constT (ROR (w2w imm) (2w * w2w rot) c))`;

val shift_immediate_def = Define`
  shift_immediate ii (shift:word5) (sh:word2) rm =
    (read_flags ii !! read_mode ii) >>=
    (\((n,z,c,v),m).
       read_regm ii (rm,m) >>=
       (\rm. inc_pc ii >>-
             constT
               case sh of
                  0w -> LSL rm (w2w shift) c
               || 1w -> LSR rm (if shift = 0w then 32w else w2w shift) c
               || 2w -> ASR rm (if shift = 0w then 32w else w2w shift) c
               || _  -> if shift = 0w then
                          word_rrx (c, rm)
                        else
                          ROR rm (w2w shift) c))`;

val shift_register_def = Define`
  shift_register ii rs (sh:word2) rm =
    (read_flags ii !! read_mode ii) >>=
    (\((n,z,c,v),m).
       read_regm ii (rs,m) >>=
       (\rs. inc_pc ii >>-
             read_regm ii (rm,m) >>=
             (\rm. constT
                case sh of
                   0w -> LSL rm (w2w rs) c
                || 1w -> LSR rm (w2w rs) c
                || 2w -> ASR rm (w2w rs) c
                || _  -> ROR rm (w2w rs) c)))`;

val addr_mode1_def = Define`
  (addr_mode1 ii (mode1_immediate rot imm) =
     immediate ii rot imm) /\
  (addr_mode1 ii (mode1_shift_immediate shift sh rm) =
     shift_immediate ii shift sh rm) /\
  (addr_mode1 ii (mode1_shift_register rs sh rm) =
     shift_register ii rs sh rm)`;

val addr_mode2_def = Define`
  (addr_mode2 ii u w rn (mode2_immediate offset) =
     read_mode ii >>=
     (\m.
        read_regm ii (rn,m) >>=
        (\rn. inc_pc ii >>-
              let address = if u then rn + w2w offset else rn - w2w offset in
                constT (if w then address else rn, address)))) /\
  (addr_mode2 ii u w rn (mode2_shift_immediate shift sh rm) =
     read_mode ii >>=
     (\m.
        read_regm ii (rn,m) >>=
        (\rn. shift_immediate ii shift sh rm >>=
           (\(c_shift,offset).
              let address = if u then rn + offset else rn - offset in
                constT (if w then address else rn, address)))))`;

(* ------------------------------------------------------------------------ *)

val ALU_arith_def = Define`
  ALU_arith op (rn:word32) (op2:word32) =
    let sign  = word_msb rn
    and (q,r) = DIVMOD_2EXP 32 (op (w2n rn) (w2n op2)) in
    let res   = (n2w r):word32 in
      ((word_msb res,r = 0,ODD q,
        (word_msb op2 = sign) /\ ~(word_msb res = sign)),res)`;

val ALU_logic_def = Define`
  ALU_logic (res:word32) = ((word_msb res,res = 0w,F,F),res)`;

val ALU_multiply_def = Define`
  ALU_multiply a rn rs rm =
    let res : word32 = rm * rs + (if a then rn else 0w) in
      (word_msb res,res = 0w,res)`;

val ALU_multiply_long_def = Define`
  ALU_multiply_long s a (rdhi:word32) (rdlo:word32) (rs:word32) (rm:word32) =
    let res : word64 =
           (if a then rdhi @@ rdlo else 0w:word64) +
           (if s then sw2sw rm * sw2sw rs else w2w rm * w2w rs)
    in
    let reshi = ( 63 >< 32 ) res : word32
    and reslo = ( 31 >< 0  ) res : word32
    in
      (word_msb res,res = 0w,reshi,reslo)`;

val ADD_def = Define`
  ADD a b c = ALU_arith (\x y.x+y+(if c then 1 else 0)) a b`;

val SUB_def = Define`SUB a b c = ADD a (~b) c`;
val AND_def = Define`AND a b   = ALU_logic (a && b)`;
val EOR_def = Define`EOR a b   = ALU_logic (a ?? b)`;
val ORR_def = Define`ORR a b   = ALU_logic (a !! b)`;

val ALU_def = Define`
  ALU (opc:word4) rn op2 c =
    case opc of
       0w  -> AND rn op2
    || 1w  -> EOR rn op2
    || 2w  -> SUB rn op2 T
    || 4w  -> ADD rn op2 F
    || 3w  -> SUB op2 rn T
    || 5w  -> ADD rn op2 c
    || 6w  -> SUB rn op2 c
    || 7w  -> SUB op2 rn c
    || 8w  -> AND rn op2
    || 9w  -> EOR rn op2
    || 10w -> SUB rn op2 T
    || 11w -> ADD rn op2 F
    || 12w -> ORR rn op2
    || 13w -> ALU_logic op2
    || 14w -> AND rn (~op2)
    || _   -> ALU_logic (~op2)`;

val arithmetic_def = Define`
  arithmetic (opcode:word4) =
    (opcode ' 2 \/ opcode ' 1) /\ (~(opcode ' 3) \/ ~(opcode ' 2))`;

val test_or_compare_def = Define`
  test_or_compare (opcode:word4) = ((3 -- 2 ) opcode = 2w)`;

val rotate_mem32_def = Define`
  rotate_mem32 (oareg:word2) (w:word32) = w #>> (8 * w2n oareg)`;

(* ------------------------------------------------------------------------ *)

val exception_exec_def = Define`
  exception_exec ii type =
    discardT
      ((read_reg ii r15 !! read_sctlr ii !! read_psr ii CPSR) >>=
       (\(pc,sctlr,cpsr).
          (let mode = exception_to_mode type in
             write_regm ii (14w,mode) (pc - 4w) !!
             branch_write_pc ii (exception_to_address sctlr.V type) !!
             write_psr ii (mode_to_psr mode) cpsr !!
             write_psr ii CPSR (cpsr with
               <| I := T;
                  F := (type IN {Exception_reset; Exception_fast} \/ cpsr.F);
                  A := ((type = Exception_reset) \/ cpsr.A); IT := 0w; J := F;
                  T := sctlr.TE; E := sctlr.EE;
                  M := mode_to_word5 mode |>))))`;

val branch_exec_def = Define`
  branch_exec ii (Branch l offset) =
    read_reg ii r15 >>=
    (\pc.
       let target = pc + sw2sw offset << 2 in
         if ~(word_msb target = word_msb (pc - 8w)) then
           failureT
         else
           if l then
             discardT (read_mode ii >>=
             (\m.
                write_regm ii (14w,m) (pc - 4w) !!
                branch_write_pc ii target))
           else
             branch_write_pc ii target)`;

val data_processing_exec_def = Define`
  data_processing_exec ii (Data_Processing opcode s rn rd op2) =
    (addr_mode1 ii op2 !! read_flags ii !! read_mode ii) >>=
    (\((c_shift, opnd2),(n,z,c,v),m).
       read_regm ii (rn,m) >>=
       (\rn.
          let ((n_alu,z_alu,c_alu,v_alu),res) = ALU opcode rn opnd2 c_shift in
            discardT
              (condT (~test_or_compare opcode)
                 (write_regm ii (rd,m) res) !!
               condT s
                 (if (rd = 15w) /\ ~(test_or_compare opcode) then
                    read_psr ii (mode_to_psr m) >>=
                    (\spsr. write_psr ii CPSR spsr)
                  else
                    write_flags ii
                      (if arithmetic opcode then
                         (n_alu,z_alu,c_alu,v_alu)
                       else
                         (n_alu,z_alu,c_shift,v))))))`;

val multiply_exec_def = Define`
  multiply_exec ii (Multiply a s rd rn rs rm) =
    if (rd = 15w) \/ (rm = 15w) \/ (rs = 15w) \/ (rd = rm) then
      failureT
    else
      discardT ((read_flags ii !! read_mode ii) >>=
      (\((n,z,c,v),m).
         (read_regm ii (rn,m) !!
          read_regm ii (rs,m) !!
          read_regm ii (rm,m)) >>=
          (\(rn,rs,rm).
             let (n_alu,z_alu,res) = ALU_multiply a rn rs rm in
               inc_pc ii !!
               write_regm ii (rd,m) res !!
               condT s (read_version ii >>=
               (\version.
                  let c_flag = if version = 4 then ARB else c in
                    write_flags ii (n_alu,z_alu,c_flag,v))))))`;

val multiply_long_exec_def = Define`
  multiply_long_exec ii (Multiply_Long u a s rdhi rdlo rs rm) =
    if (rdhi = 15w) \/ (rdlo = 15w) \/ (rm = 15w) \/ (rs = 15w) \/
       (rdhi = rm) \/ (rdlo = rm) \/ (rdhi = rdlo) then
      failureT
    else
      discardT ((read_flags ii !! read_mode ii) >>=
      (\((n,z,c,v),m).
         (read_regm ii (rdhi,m) !!
          read_regm ii (rdlo,m) !!
          read_regm ii (rs,m) !!
          read_regm ii (rm,m)) >>=
          (\(rdhi',rdlo',rs,rm).
             let (n_alu,z_alu,reshi,reslo) =
                    ALU_multiply_long u a rdhi' rdlo' rs rm
             in
               inc_pc ii !!
               write_regm ii (rdhi,m) reshi !!
               write_regm ii (rdlo,m) reslo !!
               condT s (read_version ii >>=
               (\version.
                  let c_flag = if version = 4 then ARB else c in
                    write_flags ii (n_alu,z_alu,c_flag,v))))))`;

val load_store_exec_def = Define`
  load_store_exec ii (Load_Store p u b w l rn rd op2) =
    let wb = p ==> w in
      if wb /\ (rn = rd) then
        failureT
      else
        discardT ((addr_mode2 ii u w rn op2 !! read_mode ii) >>=
        (\((address,wb_address),m).
          if l then
            condT wb (write_regm ii (rn,m) wb_address) !!
            (if b then
               read_mem8 ii address >>= (\d. constT (w2w d))
             else
               read_mem32 ii address >>=
               (\d. constT (rotate_mem32 (w2w address) d))) >>=
               (\data. write_regm ii (rd,m) data)
          else
            read_regm ii (rd,m) >>=
            (\rd.
               if b then
                 write_mem8 ii address (w2w rd)
               else
                 write_mem32 ii address rd) !!
            condT wb (write_regm ii (rn,m) wb_address)))`;

val load_exclusive_exec_def = Define`
  load_exclusive_exec ii (Load_Exclusive rn rt imm8) =
    read_version ii >>=
    (\version.
       if version < 6 then
         exception_exec ii Exception_undefined
       else
         if (rt = 15w) \/ (rn = 15w) then
           failureT
         else
           read_mode ii >>=
           (\m.
              read_regm ii (rn,m) >>=
              (\rn. let address = rn + w2w imm8 in
                 set_exclusive_monitorsT ii (address,4) >>-
                 read_mem32 ii address >>=
                 (\d. write_regm ii (rt,m) d))))`;

val store_exclusive_exec_def = Define`
  store_exclusive_exec ii (Store_Exclusive rn rd rt imm8) =
    read_version ii >>=
    (\version.
       if version < 6 then
         exception_exec ii Exception_undefined
       else
         if (rd = 15w) \/ (rt = 15w) \/ (rn = 15w) \/
            (rd = rt) \/ (rd = rt)
         then
           failureT
         else
           read_mode ii >>=
           (\m.
              read_regm ii (rn,m) >>=
              (\rn. let address = rn + w2w imm8 in
                 (exclusive_monitors_passT ii (address,4) >>=
                 (\pass.
                    if pass then
                      read_regm ii (rt,m) >>=
                      (\rt.
                        discardT
                          (write_mem32 ii address rt !!
                           write_regm ii (rd,m) 0w))
                    else
                      write_regm ii (rd,m) 1w)))))`;

val swap_exec_def = Define`
  swap_exec ii (Swap b rn rd rm) =
    if (rd = 15w) \/ (rn = 15w) \/ (rm = 15w) \/ (rn = rm) \/ (rn = rd) then
      failureT
    else
      lockT (read_mode ii >>=
      (\m.
         (read_regm ii (rn,m) !! read_regm ii (rm,m)) >>=
         (\(address,rm).
            (if b then
               read_mem8 ii address >>= (\d. constT (w2w d))
             else
               read_mem32 ii address >>=
               (\d. constT (rotate_mem32 (w2w address) d))) >>=
               (\data. discardT
                  (inc_pc ii !!
                   write_mem32 ii address rm !!
                   write_regm ii (rd,m) data)))))`;

val status_to_register_exec_def = Define`
  status_to_register_exec ii (Status_to_Register r rd) =
    read_psr ii CPSR >>=
    (\cpsr.
       let mode = word5_to_mode cpsr.M in let m = THE mode in
         if (rd = 15w) \/ IS_NONE mode \/ user_or_system_mode m /\ r then
           failureT
         else
           (if r then
              read_psr ii (mode_to_psr m) >>= (\spsr. constT (encode_psr spsr))
            else
              constT (encode_psr cpsr &&
                      0b11111000_11111111_00000011_11011111w)) >>=
           (\psr. discardT (inc_pc ii !! write_regm ii (rd,m) psr)))`;

val breakpoint_exec_def = Define`
  breakpoint_exec ii cond =
    if ~(cond = AL) then
      failureT
    else
      read_version ii >>=
      (\version.
         if version = 4 then
           exception_exec ii Exception_undefined
         else
           exception_exec ii Exception_prefetch_abort)`;

val data_memory_barrier_exec_def = Define`
  data_memory_barrier_exec ii (Data_Memory_Barrier option) =
    read_version ii >>=
    (\version.
       if version < 7 then
         exception_exec ii Exception_undefined
       else
         discardT (inc_pc ii !! dmbT ii
           (case option of
               0b0010w -> (MBReqDomain_OuterShareable, MBReqTypes_Writes)
            || 0b0011w -> (MBReqDomain_OuterShareable, MBReqTypes_All)
            || 0b0110w -> (MBReqDomain_Nonshareable, MBReqTypes_Writes)
            || 0b0111w -> (MBReqDomain_Nonshareable, MBReqTypes_All)
            || 0b1010w -> (MBReqDomain_InnerShareable, MBReqTypes_Writes)
            || 0b1011w -> (MBReqDomain_InnerShareable, MBReqTypes_All)
            || 0b1110w -> (MBReqDomain_FullSystem, MBReqTypes_Writes)
            || _       -> (MBReqDomain_FullSystem, MBReqTypes_All))))`;

(* ------------------------------------------------------------------------ *)

val arm_execute_def = with_flag (priming, SOME "_")Define`
  arm_execute ii (cond,inst) =
    read_flags ii >>=
    (\flags.
       if condition_passed flags cond then
         case inst of
            Branch l offset ->
              branch_exec ii inst
         || Swap b rn rd rm ->
              swap_exec ii inst
         || Data_Processing opcode s rn rd op2 ->
              data_processing_exec ii inst
         || Load_Store p u b w l rn rd op2_1 ->
              load_store_exec ii inst
         || Load_Exclusive rn rt imm8 ->
              load_exclusive_exec ii inst
         || Store_Exclusive rn rd rt imm8 ->
              store_exclusive_exec ii inst
         || Multiply_Long u a s rdhi rdlo rs rm ->
              multiply_long_exec ii inst
         || Multiply a s rd rn rs rm ->
              multiply_exec ii inst
         || Status_to_Register r rd ->
              status_to_register_exec ii inst
         || Breakpoint number16 ->
              breakpoint_exec ii cond
         || Data_Memory_Barrier option ->
              data_memory_barrier_exec ii inst
         || Supervisor_Call number24 ->
              exception_exec ii Exception_supervisor
         || Undefined ->
              exception_exec ii Exception_undefined
         || _ ->
              failureT
       else
         inc_pc ii)`;

(* ------------------------------------------------------------------------ *)

val _ = export_theory ();