1(* ========================================================================= *) 2(* FILE : instructionScript.sml *) 3(* DESCRIPTION : Datatype for ARM instructions, and an encoder -> word32 *) 4(* *) 5(* AUTHORS : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2006 - 2007 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["wordsTheory", "armTheory"]; 11*) 12 13open HolKernel boolLib Parse bossLib; 14open Q wordsTheory armTheory; 15 16val _ = new_theory "instruction"; 17 18(* ------------------------------------------------------------------------- *) 19 20val _ = Hol_datatype` 21 shift = 22 LSL of word4 23 | LSR of word4 24 | ASR of word4 25 | ROR of word4`; 26 27val _ = Hol_datatype 28 `addr_mode1 = 29 Dp_immediate of word4=>word8 30 | Dp_shift_immediate of shift=>word5 31 | Dp_shift_register of shift=>word4`; 32 33val _ = Hol_datatype 34 `addr_mode2 = 35 Dt_immediate of word12 36 | Dt_shift_immediate of shift=>word5`; 37 38val _ = Hol_datatype 39 `addr_mode3 = 40 Dth_immediate of word8 41 | Dth_register of word4`; 42 43val _ = Hol_datatype 44 `msr_mode = 45 Msr_immediate of word4=>word8 46 | Msr_register of word4`; 47 48val _ = Hol_datatype 49 `msr_psr = CPSR_c | CPSR_f | CPSR_a | SPSR_c | SPSR_f | SPSR_a`; 50 51val _ = Hol_datatype 52 `transfer_options = <| Pre : bool; Up : bool; Wb : bool |>`; 53 54val _ = Hol_datatype 55 `arm_instruction = 56 B of condition=>word24 57 | BL of condition=>word24 58 | SWI of condition 59 | AND of condition=>bool=>word4=>word4=>addr_mode1 60 | EOR of condition=>bool=>word4=>word4=>addr_mode1 61 | SUB of condition=>bool=>word4=>word4=>addr_mode1 62 | RSB of condition=>bool=>word4=>word4=>addr_mode1 63 | ADD of condition=>bool=>word4=>word4=>addr_mode1 64 | ADC of condition=>bool=>word4=>word4=>addr_mode1 65 | SBC of condition=>bool=>word4=>word4=>addr_mode1 66 | RSC of condition=>bool=>word4=>word4=>addr_mode1 67 | TST of condition=>word4=>addr_mode1 68 | TEQ of condition=>word4=>addr_mode1 69 | CMP of condition=>word4=>addr_mode1 70 | CMN of condition=>word4=>addr_mode1 71 | ORR of condition=>bool=>word4=>word4=>addr_mode1 72 | MOV of condition=>bool=>word4=>addr_mode1 73 | BIC of condition=>bool=>word4=>word4=>addr_mode1 74 | MVN of condition=>bool=>word4=>addr_mode1 75 | MUL of condition=>bool=>word4=>word4=>word4 76 | MLA of condition=>bool=>word4=>word4=>word4=>word4 77 | UMULL of condition=>bool=>word4=>word4=>word4=>word4 78 | UMLAL of condition=>bool=>word4=>word4=>word4=>word4 79 | SMULL of condition=>bool=>word4=>word4=>word4=>word4 80 | SMLAL of condition=>bool=>word4=>word4=>word4=>word4 81 | LDRH of condition=>bool=>bool=>transfer_options=>word4=>word4=>addr_mode3 82 | STRH of condition=>transfer_options=>word4=>word4=>addr_mode3 83 | LDR of condition=>bool=>transfer_options=>word4=>word4=>addr_mode2 84 | STR of condition=>bool=>transfer_options=>word4=>word4=>addr_mode2 85 | LDM of condition=>bool=>transfer_options=>word4=>word16 86 | STM of condition=>bool=>transfer_options=>word4=>word16 87 | SWP of condition=>bool=>word4=>word4=>word4 88 | MRS of condition=>bool=>word4 89 | MSR of condition=>msr_psr=>msr_mode 90 | CDP of condition=>word4=>word4=>word4=>word4=>word4=>word3 91 | LDC of condition=>bool=>transfer_options=>word4=>word4=>word4=>word8 92 | STC of condition=>bool=>transfer_options=>word4=>word4=>word4=>word8 93 | MRC of condition=>word4=>word3=>word4=>word4=>word4=>word3 94 | MCR of condition=>word4=>word3=>word4=>word4=>word4=>word3 95 | UND of condition`; 96 97(* ------------------------------------------------------------------------- *) 98 99val condition_encode_def = Define` 100 condition_encode cond = 101 (w2w (n2w (condition2num cond):word4 #<< 1) << 28):word32`; 102 103val shift_encode_def = Define` 104 (shift_encode (LSL Rm) = (w2w Rm):word32) /\ 105 (shift_encode (LSR Rm) = 0x20w || w2w Rm) /\ 106 (shift_encode (ASR Rm) = 0x40w || w2w Rm) /\ 107 (shift_encode (ROR Rm) = 0x60w || w2w Rm)`; 108 109val addr_mode1_encode_def = Define` 110 addr_mode1_encode op2 = 111 case op2 of 112 Dp_immediate rot imm => (0x2000000w || w2w rot << 8 || w2w imm):word32 113 | Dp_shift_immediate shift amount => w2w amount << 7 || shift_encode shift 114 | Dp_shift_register shift Rs => 0x10w || w2w Rs << 8 || shift_encode shift`; 115 116val addr_mode2_encode_def = Define` 117 addr_mode2_encode op2 = 118 case op2 of 119 Dt_immediate imm => (w2w imm):word32 120 | Dt_shift_immediate shift amount => 121 0x2000000w || w2w amount << 7 || shift_encode shift`; 122 123val addr_mode3_encode_def = Define` 124 addr_mode3_encode op2 = 125 case op2 of 126 Dth_immediate imm => 0x400000w || ((7 >< 4) imm) << 8 || ((3 >< 0) imm) 127 | Dth_register Rm => (w2w Rm):word32`; 128 129val msr_mode_encode_def = Define` 130 msr_mode_encode op = 131 case op of 132 Msr_immediate rot imm => (0x2000000w || w2w rot << 8 || w2w imm):word32 133 | Msr_register Rm => w2w Rm`; 134 135val msr_psr_encode_def = Define` 136 (msr_psr_encode CPSR_c = 0x10000w:word32) /\ 137 (msr_psr_encode CPSR_f = 0x80000w) /\ 138 (msr_psr_encode CPSR_a = 0x90000w) /\ 139 (msr_psr_encode SPSR_c = 0x410000w) /\ 140 (msr_psr_encode SPSR_f = 0x480000w) /\ 141 (msr_psr_encode SPSR_a = 0x490000w)`; 142 143val options_encode_def = Define` 144 options_encode x opt = 145 word_modify (\i b. (i = 24) /\ opt.Pre \/ (i = 23) /\ opt.Up \/ 146 (i = 22) /\ x \/ (i = 21) /\ opt.Wb) (0w:word32)`; 147 148val options_encode2_def = Define` 149 options_encode2 h opt = 150 word_modify (\i b. (i = 24) /\ opt.Pre \/ (i = 23) /\ opt.Up \/ 151 (i = 21) /\ opt.Wb \/ (i = 5) /\ h) (0w:word32)`; 152 153val data_proc_encode_def = Define` 154 data_proc_encode cond (op:word4) s (Rn:word4) (Rd:word4) Op2 = 155 condition_encode cond || w2w op << 21 || (if s then 0x100000w else 0w) || 156 w2w Rn << 16 || w2w Rd << 12 || addr_mode1_encode Op2`; 157 158val instruction_encode_def = with_flag (priming, SOME "") Define` 159 instruction_encode i = 160 case i of 161 B cond offset24 => condition_encode cond || 0xA000000w || w2w offset24 162 | BL cond offset24 => condition_encode cond || 0xB000000w || w2w offset24 163 | SWI cond => condition_encode cond || 0xF000000w 164 | AND cond s Rd Rn Op2 => data_proc_encode cond 0w s Rn Rd Op2 165 | EOR cond s Rd Rn Op2 => data_proc_encode cond 1w s Rn Rd Op2 166 | SUB cond s Rd Rn Op2 => data_proc_encode cond 2w s Rn Rd Op2 167 | RSB cond s Rd Rn Op2 => data_proc_encode cond 3w s Rn Rd Op2 168 | ADD cond s Rd Rn Op2 => data_proc_encode cond 4w s Rn Rd Op2 169 | ADC cond s Rd Rn Op2 => data_proc_encode cond 5w s Rn Rd Op2 170 | SBC cond s Rd Rn Op2 => data_proc_encode cond 6w s Rn Rd Op2 171 | RSC cond s Rd Rn Op2 => data_proc_encode cond 7w s Rn Rd Op2 172 | TST cond Rn Op2 => data_proc_encode cond 8w T Rn 0w Op2 173 | TEQ cond Rn Op2 => data_proc_encode cond 9w T Rn 0w Op2 174 | CMP cond Rn Op2 => data_proc_encode cond 10w T Rn 0w Op2 175 | CMN cond Rn Op2 => data_proc_encode cond 11w T Rn 0w Op2 176 | ORR cond s Rd Rn Op2 => data_proc_encode cond 12w s Rn Rd Op2 177 | MOV cond s Rd Op2 => data_proc_encode cond 13w s 0w Rd Op2 178 | BIC cond s Rd Rn Op2 => data_proc_encode cond 14w s Rn Rd Op2 179 | MVN cond s Rd Op2 => data_proc_encode cond 15w s 0w Rd Op2 180 | MUL cond s Rd Rm Rs => 181 condition_encode cond || (if s then 0x100090w else 0x90w) || 182 w2w Rd << 16 || w2w Rs << 8 || w2w Rm 183 | MLA cond s Rd Rm Rs Rn => 184 condition_encode cond || (if s then 0x300090w else 0x200090w) || 185 w2w Rd << 16 || w2w Rn << 12 || w2w Rs << 8 || w2w Rm 186 | UMULL cond s RdLo RdHi Rm Rs => 187 condition_encode cond || (if s then 0x900090w else 0x800090w) || 188 w2w RdHi << 16 || w2w RdLo << 12 || w2w Rs << 8 || w2w Rm 189 | UMLAL cond s RdLo RdHi Rm Rs => 190 condition_encode cond || (if s then 0xB00090w else 0xA00090w) || 191 w2w RdHi << 16 || w2w RdLo << 12 || w2w Rs << 8 || w2w Rm 192 | SMULL cond s RdLo RdHi Rm Rs => 193 condition_encode cond || (if s then 0xD00090w else 0xC00090w) || 194 w2w RdHi << 16 || w2w RdLo << 12 || w2w Rs << 8 || w2w Rm 195 | SMLAL cond s RdLo RdHi Rm Rs => 196 condition_encode cond || (if s then 0xF00090w else 0xE00090w) || 197 w2w RdHi << 16 || w2w RdLo << 12 || w2w Rs << 8 || w2w Rm 198 | LDRH cond s h options Rd Rn mode3 => 199 condition_encode cond || (if s then 0x1000D0w else 0x100090w) || 200 options_encode2 (h \/ (~h /\ ~s)) options || 201 w2w Rn << 16 || w2w Rd << 12 || addr_mode3_encode mode3 202 | STRH cond options Rd Rn mode3 => 203 condition_encode cond || 0x90w || options_encode2 T options || 204 w2w Rn << 16 || w2w Rd << 12 || addr_mode3_encode mode3 205 | LDR cond b options Rd Rn offset => 206 condition_encode cond || 0x4100000w || options_encode b options || 207 w2w Rn << 16 || w2w Rd << 12 || addr_mode2_encode offset 208 | STR cond b options Rd Rn offset => 209 condition_encode cond || 0x4000000w || options_encode b options || 210 w2w Rn << 16 || w2w Rd << 12 || addr_mode2_encode offset 211 | LDM cond s options Rn list => 212 condition_encode cond || 0x8100000w || options_encode s options || 213 w2w Rn << 16 || w2w list 214 | STM cond s options Rn list => 215 condition_encode cond || 0x8000000w || options_encode s options || 216 w2w Rn << 16 || w2w list 217 | SWP cond b Rd Rm Rn => 218 condition_encode cond || (if b then 0x1400090w else 0x1000090w) || 219 w2w Rn << 16 || w2w Rd << 12 || w2w Rm 220 | MRS cond R Rd => 221 condition_encode cond || (if R then 0x14F0000w else 0x10F0000w) || 222 w2w Rd << 12 223 | MSR cond psrd Op => 224 condition_encode cond || 0x120F000w || msr_psr_encode psrd || 225 (msr_mode_encode Op) 226 | CDP cond CPn Cop1 CRd CRn CRm Cop2 => 227 condition_encode cond || 0xE000000w || w2w Cop1 << 20 || 228 w2w CRn << 16 || w2w CRd << 12 || w2w CPn << 8 || 229 w2w Cop2 << 5 || w2w CRm 230 | LDC cond n options CPn CRd Rn offset8 => 231 condition_encode cond || 0xC100000w || options_encode n options || 232 w2w Rn << 16 || w2w CRd << 12 || w2w CPn << 8 || w2w offset8 233 | STC cond n options CPn CRd Rn offset8 => 234 condition_encode cond || 0xC000000w || options_encode n options || 235 w2w Rn << 16 || w2w CRd << 12 || w2w CPn << 8 || w2w offset8 236 | MRC cond CPn Cop1b Rd CRn CRm Cop2 => 237 condition_encode cond || 0xE100010w || w2w Cop1b << 21 || 238 w2w CRn << 16 || w2w Rd << 12 || w2w CPn << 8 || 239 w2w Cop2 << 5 || w2w CRm 240 | MCR cond CPn Cop1b Rd CRn CRm Cop2 => 241 condition_encode cond || 0xE000010w || w2w Cop1b << 21 || 242 w2w CRn << 16 || w2w Rd << 12 || w2w CPn << 8 || 243 w2w Cop2 << 5 || w2w CRm 244 | UND cond => condition_encode cond || 0x6000010w`; 245 246val _ = overload_on("enc", ``instruction_encode``); 247 248(* ------------------------------------------------------------------------- *) 249 250val _ = export_theory(); 251