1structure armSyntax :> armSyntax = 2struct 3 4open Abbrev HolKernel arm_seq_monadTheory arm_decoderTheory; 5 6val ERR = Feedback.mk_HOL_ERR "armSyntax"; 7 8fun dest_strip t = 9let val (l,r) = strip_comb t in 10 (fst (dest_const l), r) 11end; 12 13local 14 val arm_state_type = ``:arm_state``; 15 val err = ERR "dest_monad_type" "not an instance of 'a M" 16in 17 fun dest_monad_type ty = 18 let val (tya,tyb) = dom_rng ty in 19 if tya = arm_state_type then 20 case total dest_thy_type tyb of 21 SOME {Tyop = "error_option", Thy = "arm_seq_monad", 22 Args = [tyc, tyd]} => 23 (if tyd = arm_state_type then tyc else raise err) 24 | _ => raise err 25 else 26 raise err 27 end handle HOL_ERR _ => raise err 28end; 29 30fun inst_word_alpha ty tm = 31 Term.inst [Type.alpha |-> 32 (if wordsSyntax.is_word_type (Term.type_of tm) then 33 ty 34 else 35 wordsSyntax.mk_word_type ty)] tm; 36 37fun mk_monad_const s = prim_mk_const{Name = s, Thy = "arm_seq_monad"} 38fun mk_core_const s = prim_mk_const{Name = s, Thy = "arm_coretypes"} 39fun mk_decode_const s = prim_mk_const{Name = s, Thy = "arm_decoder"}; 40 41val error_tm = mk_monad_const "Error" 42val valuestate_tm = mk_monad_const "ValueState" 43 44val constT_tm = mk_monad_const "constT" 45val seqT_tm = mk_monad_const "seqT" 46val parT_tm = mk_monad_const "parT" 47val forT_tm = mk_monad_const "forT" 48val readT_tm = mk_monad_const "readT" 49val writeT_tm = mk_monad_const "writeT" 50 51val read__reg_tm = mk_monad_const "read__reg" 52val write__reg_tm = mk_monad_const "write__reg" 53val read__psr_tm = mk_monad_const "read__psr" 54val write__psr_tm = mk_monad_const "write__psr" 55 56val read_reg_mode_tm = mk_monad_const "read_reg_mode" 57val write_reg_mode_tm = mk_monad_const "write_reg_mode" 58val read_reg_tm = mk_monad_const "read_reg" 59val write_reg_tm = mk_monad_const "write_reg" 60val read_cpsr_tm = mk_monad_const "read_cpsr" 61val write_cpsr_tm = mk_monad_const "write_cpsr" 62val read_spsr_tm = mk_monad_const "read_spsr" 63val write_spsr_tm = mk_monad_const "write_spsr" 64val read_memA_tm = mk_monad_const "read_memA" 65val write_memA_tm = mk_monad_const "write_memA" 66 67val clear_event_register_tm = mk_monad_const "clear_event_register" 68val send_event_tm = mk_monad_const "send_event" 69val wait_for_interrupt_tm = mk_monad_const "wait_for_interrupt" 70val clear_wait_for_interrupt_tm = mk_monad_const "clear_wait_for_interrupt" 71 72val decode_psr_tm = mk_core_const "decode_psr" 73val bytes_tm = mk_core_const "bytes" 74val align_tm = mk_core_const "align" 75val aligned_tm = mk_core_const "aligned" 76val Encoding_ARM_tm = mk_core_const "Encoding_ARM" 77val Encoding_Thumb_tm = mk_core_const "Encoding_Thumb" 78val Encoding_Thumb2_tm = mk_core_const "Encoding_Thumb2" 79val Encoding_ThumbEE_tm = mk_core_const "Encoding_ThumbEE" 80val ITAdvance_tm = mk_core_const "ITAdvance" 81val NoInterrupt_tm = mk_core_const "NoInterrupt" 82val HW_Reset_tm = mk_core_const "HW_Reset" 83val HW_Fiq_tm = mk_core_const "HW_Fiq" 84val HW_Irq_tm = mk_core_const "HW_Irq" 85 86val arm_decode_tm = mk_decode_const "arm_decode" 87val thumb_decode_tm = mk_decode_const "thumb_decode" 88val thumbee_decode_tm = mk_decode_const "thumbee_decode" 89val thumb2_decode_tm = mk_decode_const "thumb2_decode"; 90 91fun mk_error s = 92 HolKernel.mk_comb(error_tm, 93 Term.inst [Type.alpha |-> stringSyntax.string_ty] s) 94 handle HOL_ERR _ => raise ERR "mk_error" ""; 95 96fun mk_valuestate (v,s) = 97 HolKernel.list_mk_comb(Term.inst 98 [Type.alpha |-> Term.type_of v, 99 Type.beta |-> Term.type_of s] valuestate_tm, [v,s]) 100 handle HOL_ERR _ => raise ERR "mk_valuestate" ""; 101 102fun mk_constT t = 103 HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t) 104 handle HOL_ERR _ => raise ERR "mk_constT" ""; 105 106fun mk_seqT (f,g) = 107 HolKernel.list_mk_comb(Term.inst 108 [Type.alpha |-> dest_monad_type (Term.type_of f), 109 Type.beta |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g] 110 seqT_tm, [f,g]) 111 handle HOL_ERR _ => raise ERR "mk_seqT" ""; 112 113fun mk_parT (f,g) = 114 HolKernel.list_mk_comb(Term.inst 115 [Type.alpha |-> dest_monad_type (Term.type_of f), 116 Type.beta |-> dest_monad_type (Term.type_of g)] parT_tm,[f,g]) 117 handle HOL_ERR _ => raise ERR "mk_parT" ""; 118 119fun mk_forT (l,h,f) = 120 HolKernel.list_mk_comb(Term.inst 121 [Type.alpha |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) f] 122 forT_tm,[l,h,f]) 123 handle HOL_ERR _ => raise ERR "mk_forT" ""; 124 125fun mk_readT f = 126 HolKernel.mk_comb(Term.inst 127 [Type.alpha |-> snd (dom_rng (Term.type_of f))] readT_tm, f) 128 handle HOL_ERR _ => raise ERR "mk_readT" ""; 129 130fun mk_writeT f = 131 HolKernel.mk_comb(writeT_tm, f) 132 handle HOL_ERR _ => raise ERR "mk_writeT" ""; 133 134fun mk_read__reg (ii,r) = 135 HolKernel.list_mk_comb(read__reg_tm, 136 [Term.inst [Type.alpha |-> ``:iiid``] ii, 137 Term.inst [Type.alpha |-> ``:RName``] r]) 138 handle HOL_ERR _ => raise ERR "mk_read__reg" ""; 139 140fun mk_write__reg (ii,r,v) = 141 HolKernel.list_mk_comb(write__reg_tm, 142 [Term.inst [Type.alpha |-> ``:iiid``] ii, 143 Term.inst [Type.alpha |-> ``:RName``] r, 144 inst_word_alpha ``:32`` v]) 145 handle HOL_ERR _ => raise ERR "mk_write__reg" ""; 146 147fun mk_read__psr (ii,r) = 148 HolKernel.list_mk_comb(read__psr_tm, 149 [Term.inst [Type.alpha |-> ``:iiid``] ii, 150 Term.inst [Type.alpha |-> ``:PSRName``] r]) 151 handle HOL_ERR _ => raise ERR "mk_read__psr" ""; 152 153fun mk_write__psr (ii,r,v) = 154 HolKernel.list_mk_comb(write__psr_tm, 155 [Term.inst [Type.alpha |-> ``:iiid``] ii, 156 Term.inst [Type.alpha |-> ``:PSRName``] r, 157 Term.inst [Type.alpha |-> ``:ARMpsr``] v]) 158 handle HOL_ERR _ => raise ERR "mk_write__psr" ""; 159 160fun mk_read_reg (ii,n) = 161 HolKernel.list_mk_comb(read_reg_tm, 162 [Term.inst [Type.alpha |-> ``:iiid``] ii, 163 inst_word_alpha ``:4`` n]) 164 handle HOL_ERR _ => raise ERR "mk_read_reg" ""; 165 166fun mk_write_reg (ii,n,v) = 167 HolKernel.list_mk_comb(write_reg_tm, 168 [Term.inst [Type.alpha |-> ``:iiid``] ii, 169 inst_word_alpha ``:4`` n, 170 inst_word_alpha ``:32`` v]) 171 handle HOL_ERR _ => raise ERR "mk_write_reg" ""; 172 173fun mk_read_reg_mode (ii,n,m) = 174 HolKernel.list_mk_comb(read_reg_mode_tm, 175 [Term.inst [Type.alpha |-> ``:iiid``] ii, 176 pairSyntax.mk_pair 177 (inst_word_alpha ``:4`` n, inst_word_alpha ``:5`` m)]) 178 handle HOL_ERR _ => raise ERR "mk_read_reg_mode" ""; 179 180fun mk_write_reg_mode (ii,n,m,v) = 181 HolKernel.list_mk_comb(write_reg_mode_tm, 182 [Term.inst [Type.alpha |-> ``:iiid``] ii, 183 pairSyntax.mk_pair 184 (inst_word_alpha ``:4`` n, inst_word_alpha ``:5`` m), 185 inst_word_alpha ``:32`` v]) 186 handle HOL_ERR _ => raise ERR "mk_write_reg_mode" ""; 187 188fun mk_read_cpsr ii = 189 HolKernel.mk_comb(read_cpsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii) 190 handle HOL_ERR _ => raise ERR "mk_read_cpsr" ""; 191 192fun mk_write_cpsr (ii,v) = 193 HolKernel.list_mk_comb(write_cpsr_tm, 194 [Term.inst [Type.alpha |-> ``:iiid``] ii, 195 Term.inst [Type.alpha |-> ``:ARMpsr``] v]) 196 handle HOL_ERR _ => raise ERR "mk_write_cpsr" ""; 197 198fun mk_read_spsr ii = 199 HolKernel.mk_comb(read_spsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii) 200 handle HOL_ERR _ => raise ERR "mk_read_spsr" ""; 201 202fun mk_write_spsr (ii,v) = 203 HolKernel.list_mk_comb(write_spsr_tm, 204 [Term.inst [Type.alpha |-> ``:iiid``] ii, 205 Term.inst [Type.alpha |-> ``:ARMpsr``] v]) 206 handle HOL_ERR _ => raise ERR "mk_write_spsr" ""; 207 208fun mk_read_memA (ii,a,s) = 209 HolKernel.list_mk_comb(read_memA_tm, 210 [Term.inst [Type.alpha |-> ``:iiid``] ii, 211 pairSyntax.mk_pair 212 (inst_word_alpha ``:32`` a, 213 Term.inst [Type.alpha |-> ``:num``] s)]) 214 handle HOL_ERR _ => raise ERR "mk_read_memA" ""; 215 216fun mk_write_memA (ii,a,s,v) = 217 HolKernel.list_mk_comb(write_memA_tm, 218 [Term.inst [Type.alpha |-> ``:iiid``] ii, 219 pairSyntax.mk_pair 220 (inst_word_alpha ``:32`` a, 221 Term.inst [Type.alpha |-> ``:num``] s), 222 v]) 223 handle HOL_ERR _ => raise ERR "mk_write_memA" ""; 224 225fun mk_clear_event_register ii = 226 HolKernel.mk_comb(clear_event_register_tm, 227 Term.inst [Type.alpha |-> ``:iiid``] ii) 228 handle HOL_ERR _ => raise ERR "mk_clear_event_register" ""; 229 230fun mk_send_event ii = 231 HolKernel.mk_comb(send_event_tm, Term.inst [Type.alpha |-> ``:iiid``] ii) 232 handle HOL_ERR _ => raise ERR "mk_send_event" ""; 233 234fun mk_wait_for_interrupt ii = 235 HolKernel.mk_comb(wait_for_interrupt_tm, 236 Term.inst [Type.alpha |-> ``:iiid``] ii) 237 handle HOL_ERR _ => raise ERR "mk_wait_for_interrupt" ""; 238 239fun mk_clear_wait_for_interrupt ii = 240 HolKernel.mk_comb(clear_wait_for_interrupt_tm, 241 Term.inst [Type.alpha |-> ``:iiid``] ii) 242 handle HOL_ERR _ => raise ERR "mk_clear_wait_for_interrupt" ""; 243 244fun mk_decode_psr w = 245 HolKernel.mk_comb(decode_psr_tm, inst_word_alpha ``:32`` w) 246 handle HOL_ERR _ => raise ERR "mk_decode_psr" ""; 247 248fun mk_bytes (w,n) = 249 HolKernel.mk_comb(bytes_tm, pairSyntax.mk_pair(inst_word_alpha ``:32`` w, n)) 250 handle HOL_ERR _ => raise ERR "mk_bytes" ""; 251 252fun mk_align (w,n) = 253 HolKernel.mk_comb(Term.inst 254 [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] align_tm, 255 pairSyntax.mk_pair(w, n)) 256 handle HOL_ERR _ => raise ERR "mk_align" ""; 257 258fun mk_aligned (w,n) = 259 HolKernel.mk_comb(Term.inst 260 [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] aligned_tm, 261 pairSyntax.mk_pair(w, n)) 262 handle HOL_ERR _ => raise ERR "mk_aligned" ""; 263 264fun mk_ITAdvance w = 265 HolKernel.mk_comb(Term.inst 266 [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] ITAdvance_tm, w) 267 handle HOL_ERR _ => raise ERR "mk_ITAdvance" ""; 268 269fun mk_read_memA_1 (ii,a) = mk_read_memA (ii,a,``1n``); 270 271fun mk_write_memA_1 (ii,a,v) = 272 mk_write_memA (ii,a,``1n``,listSyntax.mk_list([v],``:word8``)); 273 274fun mk_read_memA_2 (ii,a) = mk_read_memA (ii,a,``2n``); 275fun mk_write_memA_2 (ii,a,v) = mk_write_memA (ii,a,``2n``,mk_bytes(v,``2n``)); 276fun mk_read_memA_4 (ii,a) = mk_read_memA (ii,a,``4n``); 277fun mk_write_memA_4 (ii,a,v) = mk_write_memA (ii,a,``4n``,mk_bytes(v,``4n``)); 278 279fun mk_arm_decode(b,w) = 280 HolKernel.list_mk_comb(arm_decode_tm, [b,inst_word_alpha ``:32`` w]) 281 handle HOL_ERR _ => raise ERR "mk_arm_decode" ""; 282 283fun mk_thumb_decode(a,itstate,w) = 284 HolKernel.list_mk_comb(thumb_decode_tm, 285 [a,inst_word_alpha ``:8`` itstate, inst_word_alpha ``:16`` w]) 286 handle HOL_ERR _ => raise ERR "mk_thumb_decode" ""; 287 288fun mk_thumbee_decode(a,itstate,w) = 289 HolKernel.list_mk_comb(thumbee_decode_tm, 290 [a,inst_word_alpha ``:8`` itstate, inst_word_alpha ``:16`` w]) 291 handle HOL_ERR _ => raise ERR "mk_thumbee_decode" ""; 292 293fun mk_thumb2_decode(a,itstate,w1,w2) = 294 HolKernel.list_mk_comb(thumb2_decode_tm, 295 [a,inst_word_alpha ``:8`` itstate, 296 pairSyntax.mk_pair 297 (inst_word_alpha ``:16`` w1, 298 inst_word_alpha ``:16`` w2)]) 299 handle HOL_ERR _ => raise ERR "mk_thumb2_decode" ""; 300 301val dest_error = HolKernel.dest_monop error_tm (ERR "dest_error" "") 302 303val dest_valuestate = 304 HolKernel.dest_binop valuestate_tm (ERR "dest_valuestate" "") 305 306val dest_constT = HolKernel.dest_monop constT_tm (ERR "dest_constT" "") 307val dest_seqT = HolKernel.dest_binop seqT_tm (ERR "dest_seqT" "") 308val dest_parT = HolKernel.dest_binop parT_tm (ERR "dest_parT" "") 309val dest_forT = HolKernel.dest_triop forT_tm (ERR "dest_forT" "") 310val dest_readT = HolKernel.dest_monop readT_tm (ERR "dest_readT" "") 311val dest_writeT = HolKernel.dest_monop writeT_tm (ERR "dest_writeT" "") 312 313val dest_read__reg = 314 HolKernel.dest_binop read__reg_tm (ERR "dest_read__reg" "") 315 316val dest_write__reg = 317 HolKernel.dest_triop write__reg_tm (ERR "dest_write__reg" "") 318 319val dest_read__psr = 320 HolKernel.dest_binop read__psr_tm (ERR "dest_read__psr" "") 321 322val dest_write__psr = 323 HolKernel.dest_triop write__psr_tm (ERR "dest_write__psr" "") 324 325val dest_read_reg_mode = 326 HolKernel.dest_binop read_reg_mode_tm (ERR "dest_read_reg_mode" "") 327 328val dest_write_reg_mode = 329 HolKernel.dest_triop write_reg_mode_tm (ERR "dest_write_reg_mode" "") 330 331val dest_read_reg = dest_binop read_reg_tm (ERR "dest_read_reg" "") 332val dest_write_reg = dest_triop write_reg_tm (ERR "dest_write_reg" "") 333val dest_read_cpsr = dest_monop read_cpsr_tm (ERR "dest_read_cpsr" "") 334val dest_write_cpsr = dest_binop write_cpsr_tm (ERR "dest_write_cpsr" "") 335val dest_read_spsr = dest_monop read_spsr_tm (ERR "dest_read_spsr" "") 336val dest_write_spsr = dest_binop write_spsr_tm (ERR "dest_write_spsr" "") 337val dest_read_memA = dest_binop read_memA_tm (ERR "dest_read_memA" "") 338val dest_write_memA = dest_triop write_memA_tm (ERR "dest_write_memA" "") 339val dest_decode_psr = dest_monop decode_psr_tm (ERR "dest_decode_psr" "") 340val dest_bytes = dest_monop bytes_tm (ERR "dest_bytes" ""); 341val dest_align = dest_monop align_tm (ERR "dest_align" ""); 342val dest_aligned = dest_monop aligned_tm (ERR "dest_align" ""); 343val dest_ITAdvance = dest_monop ITAdvance_tm (ERR "dest_ITAdvance" ""); 344 345val dest_clear_event_register = 346 HolKernel.dest_monop decode_psr_tm (ERR "dest_clear_event_register" ""); 347 348val dest_send_event = 349 HolKernel.dest_monop send_event_tm (ERR "dest_send_event" ""); 350 351val dest_wait_for_interrupt = 352 HolKernel.dest_monop wait_for_interrupt_tm 353 (ERR "dest_wait_for_interrupt" ""); 354 355val dest_clear_wait_for_interrupt = 356 HolKernel.dest_monop clear_wait_for_interrupt_tm 357 (ERR "dest_clear_wait_for_interrupt" ""); 358 359val dest_arm_decode = 360 HolKernel.dest_binop arm_decode_tm (ERR "dest_arm_decode" ""); 361 362val dest_thumb_decode = 363 HolKernel.dest_triop thumb_decode_tm (ERR "dest_thumb_decode" ""); 364 365val dest_thumbee_decode = 366 HolKernel.dest_triop thumbee_decode_tm (ERR "dest_thumbee_decode" ""); 367 368val dest_thumb2_decode = 369 HolKernel.dest_triop thumb2_decode_tm (ERR "dest_thumb2_decode" ""); 370 371val can = Lib.can 372 373val is_error = can dest_error 374val is_valuestate = can dest_valuestate 375 376val is_constT = can dest_constT 377val is_seqT = can dest_seqT 378val is_parT = can dest_parT 379val is_forT = can dest_forT 380val is_readT = can dest_readT 381val is_writeT = can dest_writeT 382 383val is_read__reg = can dest_read__reg 384val is_write__reg = can dest_write__reg 385val is_read__psr = can dest_read__psr 386val is_write__psr = can dest_write__psr 387val is_read_reg_mode = can dest_read_reg_mode 388val is_write_reg_mode = can dest_write_reg_mode 389val is_read_reg = can dest_read_reg 390val is_write_reg = can dest_write_reg 391val is_read_cpsr = can dest_read_cpsr 392val is_write_cpsr = can dest_write_cpsr 393val is_read_spsr = can dest_read_spsr 394val is_write_spsr = can dest_write_spsr 395val is_read_memA = can dest_read_memA 396val is_write_memA = can dest_write_memA 397val is_decode_psr = can dest_decode_psr 398val is_bytes = can dest_bytes 399val is_align = can dest_align 400val is_aligned = can dest_aligned 401val is_ITAdvance = can dest_ITAdvance 402 403val is_clear_event_register = can dest_clear_event_register 404val is_send_event = can dest_send_event 405val is_wait_for_interrupt = can dest_wait_for_interrupt 406val is_clear_wait_for_interrupt = can dest_clear_wait_for_interrupt; 407 408val is_arm_decode = can dest_arm_decode 409val is_thumb_decode = can dest_thumb_decode 410val is_thumbee_decode = can dest_thumbee_decode 411val is_thumb2_decode = can dest_thumb2_decode; 412 413end 414