(**************************************************************************) (* 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_opsemTheory; open HolDoc; val _ = new_theory "arm_decoder"; val condition_decode_def = Define` condition_decode (cond : word4) = let n = w2n ((3 -- 1) cond) in num2ARMcondition (if cond ' 0 then n + 8 else n)`; val arm_decode_def = with_flag (priming, SOME "_") Define` arm_decode version (ireg : word32) = let b n = ireg ' n and i2 n = ( n + 1 >< n ) ireg : word2 and i3 n = ( n + 2 >< n ) ireg : word3 and i4 n = ( n + 3 >< n ) ireg : word4 and i5 n = ( n + 4 >< n ) ireg : word5 and i8 n = ( n + 7 >< n ) ireg : word8 and i12 n = ( n + 11 >< n ) ireg : word12 and i16 n = ( n + 15 >< n ) ireg : word16 and i24 n = ( 23 >< 0 ) ireg : word24 in let cond = i4 28 and r = i4 in if cond = 15w then if version < 5 then (AL,Unpredictable) else case (b 27,b 26,b 25,b 24,b 23,b 22,b 21,b 20,b 7,b 6,b 5,b 4) of (F, T , F , T , F , T , T , T, F, T, F, T) -> (AL, Data_Memory_Barrier (i4 0)) || (F,_26,_25,_24,_23,_22,_21,_20,_7,_6,_5,_4) -> (AL,Undefined) || (T, F , F ,_24,_23,_22,_21,_20,_7,_6,_5,_4) -> (AL,Undefined) || (T, F , T ,b24,_23,_22,_21,_20,_7,_6,_5,_4) -> (AL,Branch_Link_Exchange1 b24 (i24 0)) || (T, T , F ,b24,_23,_22,_21,_20,_7,_6,_5,_4) -> (AL, CP_Load_Store2 b24 (b 23) (b 22) (b 21) (b 20) (r 16) (r 12) (i4 8) (i8 0)) || (T, T , T , F ,_23,_22,_21,_20,_7,_6,_5, F) -> (AL,CP_Data_Processing2 (i4 20) (r 16) (r 12) (i4 8) (i3 5) (r 0)) || (T, T , T , F ,_23,_22,_21,_20,_7,_6,_5, T) -> (AL,CP_Transfer2 (i3 21) (b 20) (r 16) (r 12) (i4 8) (i3 5) (r 0)) || (T,T,T,T,_23,_22,_21,_20,_7,_6,_5,_4) -> (AL,Undefined) else (condition_decode cond, case (b 27,b 26,b 25,b 24,b 23,b 22,b 21,b 20,b 7,b 6,b 5,b 4) of (* v --- "Miscellaneous instructions" -------------------------------------v *) (F,F,F, T , F ,b22, F , F , F, F, F, F) -> Status_to_Register b22 (r 12) || (F,F,F, T , F ,b22, T , F , F, F, F, F) -> Register_to_Status b22 (i4 16) (r 0) || (F,F,F, T , F , F , T , F , F, F, F, T) -> Branch_Exchange (r 0) || (F,F,F, T , F , T , T , F , F, F, F, T) -> Count_Leading_Zeroes (r 12) (r 0) || (F,F,F, T , F , F , T , F , F, F, T, T) -> Branch_Link_Exchange2 (r 0) || (F,F,F, T , F ,_22,_21, F , F, T, F, T) -> DSP_Add_Subtract (i2 21) (r 16) (r 12) (r 0) || (F,F,F, T , F , F , T , F , F, T, T, T) -> Breakpoint (i12 8 @@ i4 0) || (F,F,F, T , F ,_22,_21, F , T,b6,_5, F) -> DSP_Multiply (r 16) (r 12) (r 8) b6 (r 0) (* ^-----------------------------------------------------------------------^ *) || (F,F,F,_24,_23,_22,_21,b20,_7,_6,_5, F) -> Data_Processing (i4 21) b20 (r 16) (r 12) (mode1_shift_immediate (i5 7) (i2 5) (r 0)) || (F,F,F,_24,_23,_22,_21,b20, F,_6,_5, T) -> Data_Processing (i4 21) b20 (r 16) (r 12) (mode1_shift_register (r 8) (i2 5) (r 0)) (* v --- "Multiplies and extra load/store instruction" --------------------v *) || (F,F,F, F , F , F ,b21,b20, T, F, F, T) -> Multiply b21 b20 (r 16) (r 12) (r 8) (r 0) || (F,F,F, F , T ,b22,b21,b20, T, F, F, T) -> Multiply_Long b22 b21 b20 (r 16) (r 12) (r 8) (r 0) || (F,F,F, T , F ,b22, F , F , T, F, F, T) -> Swap b22 (r 16) (r 12) (r 0) || (F,F,F, T , T , F , F , F , T, F, F, T) -> Store_Exclusive (r 16) (r 12) (r 0) 0w || (F,F,F, T , T , F , F , T , T, F, F, T) -> Load_Exclusive (r 16) (r 12) 0w || (F,F,F,b24,b23, F ,b21,b20, T, F, T, T) -> Load_Store_Halfword b24 b23 b21 b20 (r 16) (r 12) ARB (mode3_register (r 0)) || (F,F,F,b24,b23, T ,b21,b20, T, F, T, T) -> Load_Store_Halfword b24 b23 b21 b20 (r 16) (r 12) ARB (mode3_immediate (i4 8 @@ i4 0)) || (F,F,F,b24,b23, F ,b21, F , T, T,b5, T) -> Load_Store_Two_Words b24 b23 b21 (r 16) (r 12) b5 (mode3_register (r 0)) || (F,F,F,b24,b23, F ,b21, T , T, T,b5, T) -> Load_Store_Halfword b24 b23 b21 T (r 16) (r 12) b5 (mode3_register (r 0)) || (F,F,F,b24,b23, T ,b21, F , T, T,b5, T) -> Load_Store_Two_Words b24 b23 b21 (r 16) (r 12) b5 (mode3_immediate (i4 8 @@ i4 0)) || (F,F,F,b24,b23, T ,b21, T , T, T,b5, T) -> Load_Store_Halfword b24 b23 b21 T (r 16) (r 12) b5 (mode3_immediate (i4 8 @@ i4 0)) (* ^-----------------------------------------------------------------------^ *) || (F,F,T, T , F ,_22, F , F ,_7,_6,_5,_4) -> if version < 4 then Unpredictable else Undefined || (F,F,T, T , F ,b22, T , F ,_7,_6,_5,_4) -> Immediate_to_Status b22 (i4 16) (i4 8) (i8 0) || (F,F,T,_24,_23,_22,_21,b20,_7,_6,_5,_4) -> Data_Processing (i4 21) b20 (r 16) (r 12) (mode1_immediate (i4 8) (i8 0)) || (F,T,F,b24,b23,b22,b21,b20,_7,_6,_5,_4) -> Load_Store b24 b23 b22 b21 b20 (r 16) (r 12) (mode2_immediate (i12 0)) || (F,T,T,b24,b23,b22,b21,b20,_7,_6,_5, F) -> Load_Store b24 b23 b22 b21 b20 (r 16) (r 12) (mode2_shift_immediate (i5 7) (i2 5) (r 0)) || (F,T,T,_24,_23,_22,_21,_20,_7,_6,_5, T) -> Undefined || (T,F,F,b24,b23,b22,b21,b20,_7,_6,_5,_4) -> Load_Store_Multiple b24 b23 b22 b21 b20 (r 16) (i16 0) || (T,F,T,b24,_23,_22,_21,_20,_7,_6,_5,_4) -> Branch b24 (i24 0) || (T,T,F,b24,b23,b22,b21,b20,_7,_6,_5,_4) -> CP_Load_Store b24 b23 b22 b21 b20 (r 16) (r 12) (i4 8) (i8 0) || (T,T,T, F ,_23,_22,_21,_20,_7,_6,_5, F) -> CP_Data_Processing (i4 20) (r 16) (r 12) (i4 8) (i3 5) (r 0) || (T,T,T, F ,_23,_22,_21,b20,_7,_6,_5, T) -> CP_Transfer (i3 21) b20 (r 16) (r 12) (i4 8) (i3 5) (r 0) || (T,T,T, T ,_23,_22,_21,_20,_7,_6,_5,_4) -> Supervisor_Call (i24 0) || __ -> if version < 4 then Unpredictable else Undefined)`; val _ = export_theory();