(**************************************************************************)
(*     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 arm_coretypesTheory;


open HolDoc;
val _ = new_theory "arm_ast";


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

  This theory defines the abstract syntax tree (AST) for ARM instructions.

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

val _ = Hol_datatype
  `addressing_mode1 =
     mode1_immediate of word4=>word8
   | mode1_shift_immediate of word5=>word2=>word4
   | mode1_shift_register of word4=>word2=>word4`;

val _ = Hol_datatype
  `addressing_mode2 =
     mode2_immediate of word12
   | mode2_shift_immediate of word5=>word2=>word4`;

val _ = Hol_datatype
  `addressing_mode3 =
     mode3_immediate of word8
   | mode3_register of word4`;

val _ = Hol_datatype
 `ARMinstruction =
    Unpredictable
  | Undefined
  | Branch                of bool=>word24
  | Branch_Exchange       of word4
  | Branch_Link_Exchange1 of bool=>word24
  | Branch_Link_Exchange2 of word4
  | Count_Leading_Zeroes  of word4=>word4
  | Breakpoint            of word16
  | Supervisor_Call       of word24
  | Multiply              of bool=>bool=>word4=>word4=>word4=>word4
  | Multiply_Long         of bool=>bool=>bool=>word4=>word4=>word4=>word4
  | Status_to_Register    of bool=>word4
  | Register_to_Status    of bool=>word4=>word4
  | Immediate_to_Status   of bool=>word4=>word4=>word8
  | Data_Processing       of word4=>bool=>word4=>word4=>addressing_mode1
  | Swap                  of bool=>word4=>word4=>word4
  | Data_Memory_Barrier   of word4
  | Load_Store_Multiple   of bool=>bool=>bool=>bool=>bool=>word4=>word16
  | Load_Exclusive        of word4=>word4=>word8
  | Store_Exclusive       of word4=>word4=>word4=>word8
  | Load_Store            of bool=>bool=>bool=>bool=>bool=>word4=>word4=>
                             addressing_mode2
  | Load_Store_Halfword   of bool=>bool=>bool=>bool=>word4=>word4=>bool=>
                             addressing_mode3
  | Load_Store_Two_Words  of bool=>bool=>bool=>word4=>word4=>bool=>
                             addressing_mode3
  | CP_Load_Store         of bool=>bool=>bool=>bool=>bool=>word4=>word4=>
                             word4=>word8
  | CP_Load_Store2        of bool=>bool=>bool=>bool=>bool=>word4=>word4=>
                             word4=>word8
  | CP_Data_Processing    of word4=>word4=>word4=>word4=>word3=>word4
  | CP_Data_Processing2   of word4=>word4=>word4=>word4=>word3=>word4
  | CP_Transfer           of word3=>bool=>word4=>word4=>word4=>word3=>word4
  | CP_Transfer2          of word3=>bool=>word4=>word4=>word4=>word3=>word4
  | DSP_Add_Subtract      of word2=>word4=>word4=>word4
  | DSP_Multiply          of word4=>word4=>word4=>bool=>word4`;

val _ = export_theory ();