(**************************************************************************)
(*     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 wordsTheory common_coretypesTheory;
open wordsLib;

open HolDoc;
val _ = new_theory "arm_coretypes";


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

  This theory defines the types and operations over these types for the
  ARM model.

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

(* used by the AST *)

(* type of address values and of values stored in registers *)
val _ = type_abbrev("Aimm",    ``:word32``);

val _ = Hol_datatype `ARMreg =
 r0     | r1     | r2      | r3      | r4      | r5      | r6      | r7  |
 r8     | r9     | r10     | r11     | r12     | r13     | r14     | r15 |
 r8_fiq | r9_fiq | r10_fiq | r11_fiq | r12_fiq | r13_fiq | r14_fiq |
                                                 r13_irq | r14_irq |
                                                 r13_svc | r14_svc |
                                                 r13_abt | r14_abt |
                                                 r13_und | r14_und`;

val _ = Hol_datatype `ARMpsr =
  CPSR | SPSR_fiq | SPSR_irq | SPSR_svc | SPSR_abt | SPSR_und`;

val _ = Hol_datatype `ARMmode = usr | fiq | irq | svc | abt | und | sys`;

val _ = Hol_datatype `ARMstatus =
  <| N : bool; Z : bool; C : bool; V : bool;
     Q : bool; IT : word8; J : bool; Reserved : word4; GE : word4;
     E : bool; A : bool;
     I : bool; F : bool; T : bool; M : word5 |>`;

val _ = Hol_datatype `ARMsctlr =
  <| TE   : bool; AFE  : bool; TRE  : bool; NMFI : bool; EE   : bool;
     VE   : bool; U    : bool; FI   : bool; HA   : bool; RR   : bool;
     V    : bool; I    : bool; Z    : bool; SW   : bool; B    : bool;
     C    : bool; A    : bool; M    : bool |>`;

val _ = Hol_datatype `ARMcp_registers = <| SCTLR : ARMsctlr |>`;

val _ = Hol_datatype `ARMcondition =
  EQ | CS | MI | VS | HI | GE | GT | AL |
  NE | CC | PL | VC | LS | LT | LE | NV`;

val _ = Hol_datatype `ARMexception =
  Exception_reset |
  Exception_undefined |
  Exception_supervisor |
  Exception_prefetch_abort |
  Exception_data_abort |
  Exception_address |
  Exception_interrupt |
  Exception_fast`;

val _ = Hol_datatype `ARMversion =
  ARMv4 | ARMv4T |
  ARMv5T | ARMv5TE |
  ARMv6 | ARMv6K | ARMv6T2 |
  ARMv7_A | ARMv7_R | ARMv7_M`;

val _ = Hol_datatype `ARMextensions =
  Extension_ThumbEE | Extension_VFP | Extension_AdvanvedSIMD |
  Extension_Security | Extension_Jazelle | Extension_Multiprocessing`;

val _ = Hol_datatype `ARMinfo =
  <| version : ARMversion;
     extensions : ARMextensions set |>`;

val _ = Hol_datatype `InstrSet =
  InstrSet_ARM | InstrSet_Thumb | InstrSet_Jazelle | InstrSet_ThumbEE`;

val _ = Hol_datatype `MemType =
  MemType_Normal | MemType_Device | MemType_StringlyOrdered`;

val _ = Hol_datatype `MemoryAttributes =
  <| type           : MemType;
     innerattrs     : word2;
     outerattrs     : word2;
     shareable      : bool;
     outershareable : bool |>`;

val _ = Hol_datatype `FullAddress =
  <| physicaladdress    : word32;
     physicaladdressext : word8;
     NS                 : bool  (* F = Secure; T = Non-secure *) |>`;

val _ = Hol_datatype `AddressDescriptor =
  <| memattrs : MemoryAttributes;
     paddress : FullAddress |>`;

val _ = type_abbrev("ExclusiveMonitor", ``: FullAddress # iiid # num -> bool``);

val _ = Hol_datatype `ExclusiveMonitors =
  <| TranslateAddress :
        word32 # bool # bool -> AddressDescriptor;
      (* TranslateAddress(VA,ispriv,iswrite) converts a virtual address to
         an address descriptor.  Implementation depends on the memory
         architecture. *)
     MarkExclusiveGlobal :
       (FullAddress # iiid # num) -> ExclusiveMonitor -> ExclusiveMonitor;
     MarkExclusiveLocal :
       (FullAddress # iiid # num) -> ExclusiveMonitor -> ExclusiveMonitor;
     ClearExclusiveLocal : iiid -> ExclusiveMonitor # ExclusiveMonitor ->
                                   ExclusiveMonitor # ExclusiveMonitor;
     IsExclusiveLocal  : ExclusiveMonitor;
     IsExclusiveGlobal : ExclusiveMonitor |>`;

val _ = Hol_datatype `MBReqDomain =
  MBReqDomain_FullSystem |
  MBReqDomain_OuterShareable |
  MBReqDomain_InnerShareable |
  MBReqDomain_Nonshareable`;

val _ = Hol_datatype `MBReqTypes = MBReqTypes_All | MBReqTypes_Writes`;

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

val word5_to_mode_def = Define`
  word5_to_mode (m:word5) =
    case m of
       16w -> SOME usr
    || 17w -> SOME fiq
    || 18w -> SOME irq
    || 19w -> SOME svc
    || 23w -> SOME abt
    || 27w -> SOME und
    || 31w -> SOME sys
    || _   -> NONE`;

val align_def = Define`
  align (w : 'a word, n : num) : 'a word =
    n2w (n * (w2n w DIV n))`;

val decode_psr_def = Define`
  decode_psr (psr:word32) =
    <| N := psr ' 31;
       Z := psr ' 30;
       C := psr ' 29;
       V := psr ' 28;
       Q := psr ' 27;
       IT := (( 15 >< 10 ) psr : word6) @@ (( 26 >< 25 ) psr : word2);
       J := psr ' 24;
       Reserved := ( 23 >< 20 ) psr;
       GE := ( 19 >< 16 ) psr;
       E := psr ' 9;
       A := psr ' 8;
       I := psr ' 7;
       F := psr ' 6;
       T := psr ' 5;
       M := ( 4 >< 0 ) psr |>`;

val encode_psr_def = Define`
  encode_psr (psr:ARMstatus) : word32 =
    word_modify (\x b.
      if x < 5 then psr.M ' x else
      if x = 5 then psr.T else
      if x = 6 then psr.F else
      if x = 7 then psr.I else
      if x = 8 then psr.A else
      if x = 9 then psr.E else
      if x < 16 then psr.IT ' (x - 8) else
      if x < 20 then psr.GE ' (x - 16) else
      if x < 24 then psr.Reserved ' (x - 20) else
      if x = 24 then psr.J else
      if x < 27 then psr.IT ' (x - 25) else
      if x = 27 then psr.Q else
      if x = 28 then psr.V else
      if x = 29 then psr.C else
      if x = 30 then psr.Z else
      (* x = 31 *)   psr.N) 0w`;

val version_number_def = Define`
  (version_number ARMv4   = 4) /\
  (version_number ARMv4T  = 4) /\
  (version_number ARMv5T  = 5) /\
  (version_number ARMv5TE = 5) /\
  (version_number ARMv6   = 6) /\
  (version_number ARMv6K  = 6) /\
  (version_number ARMv6T2 = 6) /\
  (version_number ARMv7_A = 7) /\
  (version_number ARMv7_R = 7) /\
  (version_number ARMv7_M = 7)`;

val _ = export_theory ();