1structure arm_astSyntax :> arm_astSyntax = 2struct 3 4(* interactive use: 5 app load ["arm_astTheory", "wordsSyntax"]; 6*) 7 8open Abbrev HolKernel arm_astTheory; 9 10(* ------------------------------------------------------------------------- *) 11 12val ERR = Feedback.mk_HOL_ERR "arm_astSyntax"; 13 14fun inst_word_alpha ty tm = 15 Term.inst [Type.alpha |-> 16 (if wordsSyntax.is_word_type (Term.type_of tm) then 17 ty 18 else 19 wordsSyntax.mk_word_type ty)] tm; 20 21fun in_numeral_type ty = 22 case Lib.total Type.dest_thy_type ty 23 of NONE => false 24 | SOME {Tyop,...} => Lib.mem Tyop ["one","bit0","bit1"]; 25 26fun inst_list x y = 27 List.map (fn (ty,v) => 28 (if in_numeral_type ty then 29 inst_word_alpha ty 30 else 31 Term.inst [Type.alpha |-> ty]) v) (Lib.zip x y); 32 33(* ------------------------------------------------------------------------- *) 34 35fun mk_ast_const s = Term.prim_mk_const {Name = s, Thy = "arm_ast"} 36 37val Mode1_register_shifted_register_tm = 38 mk_ast_const "Mode1_register_shifted_register" 39 40val Mode1_immediate_tm = mk_ast_const "Mode1_immediate" 41val Mode1_register_tm = mk_ast_const "Mode1_register" 42val Mode2_immediate_tm = mk_ast_const "Mode2_immediate" 43val Mode2_register_tm = mk_ast_const "Mode2_register" 44val Mode3_immediate_tm = mk_ast_const "Mode3_immediate" 45val Mode3_register_tm = mk_ast_const "Mode3_register" 46 47val Parallel_normal_tm = mk_ast_const "Parallel_normal" 48val Parallel_saturating_tm = mk_ast_const "Parallel_saturating" 49val Parallel_halving_tm = mk_ast_const "Parallel_halving" 50val Parallel_add_16_tm = mk_ast_const "Parallel_add_16" 51val Parallel_add_sub_exchange_tm = mk_ast_const "Parallel_add_sub_exchange" 52val Parallel_sub_add_exchange_tm = mk_ast_const "Parallel_sub_add_exchange" 53val Parallel_sub_16_tm = mk_ast_const "Parallel_sub_16" 54val Parallel_add_8_tm = mk_ast_const "Parallel_add_8" 55val Parallel_sub_8_tm = mk_ast_const "Parallel_sub_8" 56 57val Hint_nop_tm = mk_ast_const "Hint_nop" 58val Hint_yield_tm = mk_ast_const "Hint_yield" 59val Hint_wait_for_event_tm = mk_ast_const "Hint_wait_for_event" 60val Hint_wait_for_interrupt_tm = mk_ast_const "Hint_wait_for_interrupt" 61val Hint_send_event_tm = mk_ast_const "Hint_send_event" 62val Hint_debug_tm = mk_ast_const "Hint_debug" 63 64val Branch_Target_tm = mk_ast_const "Branch_Target" 65val Branch_Exchange_tm = mk_ast_const "Branch_Exchange" 66val Compare_Branch_tm = mk_ast_const "Compare_Branch" 67val Table_Branch_Byte_tm = mk_ast_const "Table_Branch_Byte" 68val Check_Array_tm = mk_ast_const "Check_Array" 69val Handler_Branch_Link_tm = mk_ast_const "Handler_Branch_Link" 70val Handler_Branch_Parameter_tm = mk_ast_const "Handler_Branch_Parameter" 71 72val Handler_Branch_Link_Parameter_tm = 73 mk_ast_const "Handler_Branch_Link_Parameter" 74 75val Branch_Link_Exchange_Immediate_tm = 76 mk_ast_const "Branch_Link_Exchange_Immediate" 77 78val Branch_Link_Exchange_Register_tm = 79 mk_ast_const "Branch_Link_Exchange_Register" 80 81val Data_Processing_tm = mk_ast_const "Data_Processing" 82val Add_Sub_tm = mk_ast_const "Add_Sub" 83val Move_Halfword_tm = mk_ast_const "Move_Halfword" 84val Multiply_tm = mk_ast_const "Multiply" 85val Multiply_Subtract_tm = mk_ast_const "Multiply_Subtract" 86val Signed_Halfword_Multiply_tm = mk_ast_const "Signed_Halfword_Multiply" 87val Signed_Multiply_Dual_tm = mk_ast_const "Signed_Multiply_Dual" 88val Signed_Multiply_Long_Dual_tm = mk_ast_const "Signed_Multiply_Long_Dual" 89val Multiply_Long_tm = mk_ast_const "Multiply_Long" 90val Saturate_tm = mk_ast_const "Saturate" 91val Saturate_16_tm = mk_ast_const "Saturate_16" 92val Saturating_Add_Subtract_tm = mk_ast_const "Saturating_Add_Subtract" 93val Pack_Halfword_tm = mk_ast_const "Pack_Halfword" 94val Extend_Byte_tm = mk_ast_const "Extend_Byte" 95val Extend_Byte_16_tm = mk_ast_const "Extend_Byte_16" 96val Extend_Halfword_tm = mk_ast_const "Extend_Halfword" 97val Bit_Field_Clear_Insert_tm = mk_ast_const "Bit_Field_Clear_Insert" 98val Count_Leading_Zeroes_tm = mk_ast_const "Count_Leading_Zeroes" 99val Reverse_Bits_tm = mk_ast_const "Reverse_Bits" 100val Byte_Reverse_Word_tm = mk_ast_const "Byte_Reverse_Word" 101val Bit_Field_Extract_tm = mk_ast_const "Bit_Field_Extract" 102val Select_Bytes_tm = mk_ast_const "Select_Bytes" 103val Parallel_Add_Subtract_tm = mk_ast_const "Parallel_Add_Subtract" 104val Divide_tm = mk_ast_const "Divide" 105 106val Signed_Most_Significant_Multiply_tm = 107 mk_ast_const "Signed_Most_Significant_Multiply" 108 109val Signed_Most_Significant_Multiply_Subtract_tm = 110 mk_ast_const "Signed_Most_Significant_Multiply_Subtract" 111 112val Multiply_Accumulate_Accumulate_tm = 113 mk_ast_const "Multiply_Accumulate_Accumulate" 114 115val Byte_Reverse_Packed_Halfword_tm = 116 mk_ast_const "Byte_Reverse_Packed_Halfword" 117 118val Byte_Reverse_Signed_Halfword_tm = 119 mk_ast_const "Byte_Reverse_Signed_Halfword" 120 121val Unsigned_Sum_Absolute_Differences_tm = 122 mk_ast_const "Unsigned_Sum_Absolute_Differences" 123 124val Status_to_Register_tm = mk_ast_const "Status_to_Register" 125val Register_to_Status_tm = mk_ast_const "Register_to_Status" 126val Immediate_to_Status_tm = mk_ast_const "Immediate_to_Status" 127val Change_Processor_State_tm = mk_ast_const "Change_Processor_State" 128val Set_Endianness_tm = mk_ast_const "Set_Endianness" 129 130val Load_tm = mk_ast_const "Load" 131val Store_tm = mk_ast_const "Store" 132val Load_Halfword_tm = mk_ast_const "Load_Halfword" 133val Store_Halfword_tm = mk_ast_const "Store_Halfword" 134val Load_Dual_tm = mk_ast_const "Load_Dual" 135val Store_Dual_tm = mk_ast_const "Store_Dual" 136val Load_Multiple_tm = mk_ast_const "Load_Multiple" 137val Store_Multiple_tm = mk_ast_const "Store_Multiple" 138val Load_Exclusive_tm = mk_ast_const "Load_Exclusive" 139val Store_Exclusive_tm = mk_ast_const "Store_Exclusive" 140val Load_Exclusive_Doubleword_tm = mk_ast_const "Load_Exclusive_Doubleword" 141val Store_Exclusive_Doubleword_tm = mk_ast_const "Store_Exclusive_Doubleword" 142val Load_Exclusive_Halfword_tm = mk_ast_const "Load_Exclusive_Halfword" 143val Store_Exclusive_Halfword_tm = mk_ast_const "Store_Exclusive_Halfword" 144val Load_Exclusive_Byte_tm = mk_ast_const "Load_Exclusive_Byte" 145val Store_Exclusive_Byte_tm = mk_ast_const "Store_Exclusive_Byte" 146val Store_Return_State_tm = mk_ast_const "Store_Return_State" 147val Return_From_Exception_tm = mk_ast_const "Return_From_Exception" 148 149val Hint_tm = mk_ast_const "Hint" 150val Breakpoint_tm = mk_ast_const "Breakpoint" 151val Data_Memory_Barrier_tm = mk_ast_const "Data_Memory_Barrier" 152val Swap_tm = mk_ast_const "Swap" 153val Preload_Data_tm = mk_ast_const "Preload_Data" 154val Preload_Instruction_tm = mk_ast_const "Preload_Instruction" 155val Supervisor_Call_tm = mk_ast_const "Supervisor_Call" 156val Secure_Monitor_Call_tm = mk_ast_const "Secure_Monitor_Call" 157val Enterx_Leavex_tm = mk_ast_const "Enterx_Leavex" 158val Clear_Exclusive_tm = mk_ast_const "Clear_Exclusive" 159val If_Then_tm = mk_ast_const "If_Then" 160 161val Data_Synchronization_Barrier_tm = 162 mk_ast_const "Data_Synchronization_Barrier" 163 164val Instruction_Synchronization_Barrier_tm = 165 mk_ast_const "Instruction_Synchronization_Barrier" 166 167val Coprocessor_Load_tm = mk_ast_const "Coprocessor_Load" 168val Coprocessor_Store_tm = mk_ast_const "Coprocessor_Store" 169val Coprocessor_Data_Processing_tm = mk_ast_const "Coprocessor_Data_Processing" 170val Coprocessor_Transfer_tm = mk_ast_const "Coprocessor_Transfer" 171val Coprocessor_Transfer_Two_tm = mk_ast_const "Coprocessor_Transfer_Two" 172 173val Unpredictable_tm = mk_ast_const "Unpredictable" 174val Undefined_tm = mk_ast_const "Undefined" 175val Branch_tm = mk_ast_const "Branch" 176val DataProcessing_tm = mk_ast_const "DataProcessing" 177val StatusAccess_tm = mk_ast_const "StatusAccess" 178val LoadStore_tm = mk_ast_const "LoadStore" 179val Miscellaneous_tm = mk_ast_const "Miscellaneous" 180val Coprocessor_tm = mk_ast_const "Coprocessor" 181 182(* ------------------------------------------------------------------------- *) 183 184fun mk_Mode1_immediate t = 185 Term.mk_comb(Mode1_immediate_tm, inst_word_alpha ``:12`` t) 186 handle HOL_ERR _ => raise ERR "mk_Mode1_immediate" ""; 187 188fun mk_Mode1_register(r,s,t) = 189 Term.list_mk_comb(Mode1_register_tm, inst_list [``:5``,``:2``,``:4``] [r,s,t]) 190 handle HOL_ERR _ => raise ERR "mk_Mode1_register" ""; 191 192fun mk_Mode1_register_shifted_register(r,s,t) = 193 Term.list_mk_comb(Mode1_register_shifted_register_tm, 194 inst_list [``:4``,``:2``,``:4``] [r,s,t]) 195 handle HOL_ERR _ => raise ERR "mk_Mode1_register_shifted_register" ""; 196 197fun mk_Mode2_immediate t = 198 Term.mk_comb(Mode2_immediate_tm, inst_word_alpha ``:12`` t) 199 handle HOL_ERR _ => raise ERR "mk_Mode2_immediate" ""; 200 201fun mk_Mode2_register(r,s,t) = 202 Term.list_mk_comb(Mode2_register_tm, inst_list [``:5``,``:2``,``:3``] [r,s,t]) 203 handle HOL_ERR _ => raise ERR "mk_Mode2_register" ""; 204 205fun mk_Mode3_immediate t = 206 Term.mk_comb(Mode3_immediate_tm, inst_word_alpha ``:12`` t) 207 handle HOL_ERR _ => raise ERR "mk_Mode3_immediate" ""; 208 209fun mk_Mode3_register(r,s) = 210 Term.list_mk_comb(Mode3_register_tm, inst_list [``:2``,``:4``] [r,s]) 211 handle HOL_ERR _ => raise ERR "mk_Mode3_register" ""; 212 213fun mk_Hint_debug t = 214 Term.mk_comb(Hint_debug_tm, inst_word_alpha ``:4`` t) 215 handle HOL_ERR _ => raise ERR "mk_Hint_debug" ""; 216 217(* .. *) 218 219fun mk_Branch t = 220 Term.mk_comb(Branch_tm, inst [alpha |-> ``:branch_instruction``] t) 221 handle HOL_ERR _ => raise ERR "mk_Branch" ""; 222 223fun mk_Branch_Target t = 224 Term.mk_comb(Branch_Target_tm, inst_word_alpha ``:24`` t) |> mk_Branch 225 handle HOL_ERR _ => raise ERR "mk_Branch_Target" ""; 226 227fun mk_Branch_Exchange t = 228 Term.mk_comb(Branch_Exchange_tm, inst_word_alpha ``:4`` t) |> mk_Branch 229 handle HOL_ERR _ => raise ERR "mk_Branch_Exchange" ""; 230 231fun mk_Branch_Link_Exchange_Immediate(r,s,t) = 232 Term.list_mk_comb(Branch_Link_Exchange_Immediate_tm, 233 inst_list [bool,bool,``:24``] [r,s,t]) |> mk_Branch 234 handle HOL_ERR _ => raise ERR "mk_Branch_Link_Exchange_Immediate" ""; 235 236fun mk_Branch_Link_Exchange_Register t = 237 Term.mk_comb(Branch_Link_Exchange_Register_tm, inst_word_alpha ``:4`` t) 238 |> mk_Branch 239 handle HOL_ERR _ => raise ERR "mk_Branch_Link_Exchange_Register" ""; 240 241fun mk_Compare_Branch(r,s,t) = 242 Term.list_mk_comb(Compare_Branch_tm, inst_list [bool,``:6``,``:3``] [r,s,t]) 243 |> mk_Branch 244 handle HOL_ERR _ => raise ERR "mk_Compare_Branch" ""; 245 246fun mk_Table_Branch_Byte(r,s,t) = 247 Term.list_mk_comb 248 (Table_Branch_Byte_tm, inst_list [``:4``,bool,``:4``] [r,s,t]) 249 |> mk_Branch 250 handle HOL_ERR _ => raise ERR "mk_Table_Branch_Byte" ""; 251 252fun mk_Check_Array(r,s) = 253 Term.list_mk_comb(Check_Array_tm, inst_list [``:4``,``:4``] [r,s]) 254 |> mk_Branch 255 handle HOL_ERR _ => raise ERR "mk_Check_Array" ""; 256 257fun mk_Handler_Branch_Link(r,s) = 258 Term.list_mk_comb(Handler_Branch_Link_tm, inst_list [bool,``:8``] [r,s]) 259 |> mk_Branch 260 handle HOL_ERR _ => raise ERR "mk_Handler_Branch_Link" ""; 261 262fun mk_Handler_Branch_Link_Parameter(r,s) = 263 Term.list_mk_comb 264 (Handler_Branch_Link_Parameter_tm, inst_list [``:5``,``:5``] [r,s]) 265 |> mk_Branch 266 handle HOL_ERR _ => raise ERR "mk_Handler_Branch_Link_Parameter" ""; 267 268fun mk_Handler_Branch_Parameter(r,s) = 269 Term.list_mk_comb 270 (Handler_Branch_Parameter_tm, inst_list [``:3``,``:5``] [r,s]) 271 |> mk_Branch 272 handle HOL_ERR _ => raise ERR "mk_Handler_Branch_Parameter" ""; 273 274(* .. *) 275 276fun mk_DataProcessing t = 277 Term.mk_comb(DataProcessing_tm, 278 inst [alpha |-> ``:data_processing_instruction``] t) 279 handle HOL_ERR _ => raise ERR "mk_DataProcessing" ""; 280 281fun mk_Data_Processing(r,s,t,u,v) = 282 Term.list_mk_comb(Data_Processing_tm, 283 inst_list [``:4``,bool,``:4``,``:4``,``:addressing_mode1``] [r,s,t,u,v]) 284 |> mk_DataProcessing 285 handle HOL_ERR _ => raise ERR "mk_Data_Processing" ""; 286 287fun mk_Add_Sub(r,s,t,u) = 288 Term.list_mk_comb 289 (Add_Sub_tm, inst_list [bool,``:4``,``:4``,``:12``] [r,s,t,u]) 290 |> mk_DataProcessing 291 handle HOL_ERR _ => raise ERR "mk_Add_Sub" ""; 292 293fun mk_Move_Halfword(r,s,t) = 294 Term.list_mk_comb(Move_Halfword_tm, inst_list [bool,``:4``,``:16``] [r,s,t]) 295 |> mk_DataProcessing 296 handle HOL_ERR _ => raise ERR "mk_Move_Halfword" ""; 297 298fun mk_Multiply(r,s,t,u,v,w) = 299 Term.list_mk_comb(Multiply_tm, 300 inst_list [bool,bool,``:4``,``:4``,``:4``,``:4``] [r,s,t,u,v,w]) 301 |> mk_DataProcessing 302 handle HOL_ERR _ => raise ERR "mk_Multiply" ""; 303 304fun mk_Multiply_Subtract(r,s,t,u) = 305 Term.list_mk_comb(Multiply_Subtract_tm, 306 inst_list [``:4``,``:4``,``:4``,``:4``] [r,s,t,u]) 307 |> mk_DataProcessing 308 handle HOL_ERR _ => raise ERR "mk_Multiply_Subtract" ""; 309 310fun mk_Signed_Halfword_Multiply(r,s,t,u,v,w,x) = 311 Term.list_mk_comb(Signed_Halfword_Multiply_tm, 312 inst_list [``:2``,bool,bool,``:4``,``:4``,``:4``,``:4``] [r,s,t,u,v,w,x]) 313 |> mk_DataProcessing 314 handle HOL_ERR _ => raise ERR "mk_Signed_Halfword_Multiply" ""; 315 316fun mk_Signed_Multiply_Dual(r,s,t,u,v,w) = 317 Term.list_mk_comb(Signed_Multiply_Dual_tm, 318 inst_list [``:4``,``:4``,``:4``,bool,bool,``:4``] [r,s,t,u,v,w]) 319 |> mk_DataProcessing 320 handle HOL_ERR _ => raise ERR "mk_Signed_Multiply_Dual" ""; 321 322fun mk_Signed_Multiply_Long_Dual(r,s,t,u,v,w) = 323 Term.list_mk_comb(Signed_Multiply_Long_Dual_tm, 324 inst_list [``:4``,``:4``,``:4``,bool,bool,``:4``] [r,s,t,u,v,w]) 325 |> mk_DataProcessing 326 handle HOL_ERR _ => raise ERR "mk_Signed_Multiply_Long_Dual" ""; 327 328fun mk_Multiply_Long(r,s,t,u,v,w,x) = 329 Term.list_mk_comb(Multiply_Long_tm, 330 inst_list [bool,bool,bool,``:4``,``:4``,``:4``,``:4``] [r,s,t,u,v,w,x]) 331 |> mk_DataProcessing 332 handle HOL_ERR _ => raise ERR "mk_Multiply_Long" ""; 333 334fun mk_Saturate(r,s,t,u,v,w) = 335 Term.list_mk_comb(Saturate_tm, 336 inst_list [bool,``:5``,``:4``,``:5``,bool,``:4``] [r,s,t,u,v,w]) 337 |> mk_DataProcessing 338 handle HOL_ERR _ => raise ERR "mk_Saturate" ""; 339 340fun mk_Saturate_16(r,s,t,u) = 341 Term.list_mk_comb(Saturate_16_tm, 342 inst_list [bool,``:4``,``:4``,``:4``] [r,s,t,u]) 343 |> mk_DataProcessing 344 handle HOL_ERR _ => raise ERR "mk_Saturate_16" ""; 345 346fun mk_Saturating_Add_Subtract(r,s,t,u) = 347 Term.list_mk_comb(Saturating_Add_Subtract_tm, 348 inst_list [``:2``,``:4``,``:4``,``:4``] [r,s,t,u]) 349 |> mk_DataProcessing 350 handle HOL_ERR _ => raise ERR "mk_Saturating_Add_Subtract" ""; 351 352fun mk_Pack_Halfword(r,s,t,u,v) = 353 Term.list_mk_comb(Pack_Halfword_tm, 354 inst_list [``:4``,``:4``,``:5``,bool,``:4``] [r,s,t,u,v]) 355 |> mk_DataProcessing 356 handle HOL_ERR _ => raise ERR "mk_Pack_Halfword" ""; 357 358fun mk_Extend_Byte(r,s,t,u,v) = 359 Term.list_mk_comb(Extend_Byte_tm, 360 inst_list [bool,``:4``,``:4``,``:2``,``:4``] [r,s,t,u,v]) 361 |> mk_DataProcessing 362 handle HOL_ERR _ => raise ERR "mk_Extend_Byte" ""; 363 364fun mk_Extend_Byte_16(r,s,t,u,v) = 365 Term.list_mk_comb(Extend_Byte_16_tm, 366 inst_list [bool,``:4``,``:4``,``:2``,``:4``] [r,s,t,u,v]) 367 |> mk_DataProcessing 368 handle HOL_ERR _ => raise ERR "mk_Extend_Byte_16" ""; 369 370fun mk_Extend_Halfword(r,s,t,u,v) = 371 Term.list_mk_comb(Extend_Halfword_tm, 372 inst_list [bool,``:4``,``:4``,``:2``,``:4``] [r,s,t,u,v]) 373 |> mk_DataProcessing 374 handle HOL_ERR _ => raise ERR "mk_Extend_Halfword" ""; 375 376fun mk_Bit_Field_Clear_Insert(r,s,t,u) = 377 Term.list_mk_comb(Bit_Field_Clear_Insert_tm, 378 inst_list [``:5``,``:4``,``:5``,``:4``] [r,s,t,u]) 379 |> mk_DataProcessing 380 handle HOL_ERR _ => raise ERR "mk_Bit_Field_Clear_Insert" ""; 381 382fun mk_Count_Leading_Zeroes(r,s) = 383 Term.list_mk_comb(Count_Leading_Zeroes_tm, inst_list [``:4``,``:4``] [r,s]) 384 |> mk_DataProcessing 385 handle HOL_ERR _ => raise ERR "mk_Count_Leading_Zeroes" ""; 386 387fun mk_Reverse_Bits(r,s) = 388 Term.list_mk_comb(Reverse_Bits_tm, inst_list [``:4``,``:4``] [r,s]) 389 |> mk_DataProcessing 390 handle HOL_ERR _ => raise ERR "mk_Reverse_Bits" ""; 391 392fun mk_Byte_Reverse_Word(r,s) = 393 Term.list_mk_comb(Byte_Reverse_Word_tm, inst_list [``:4``,``:4``] [r,s]) 394 |> mk_DataProcessing 395 handle HOL_ERR _ => raise ERR "mk_Byte_Reverse_Word" ""; 396 397fun mk_Bit_Field_Extract(r,s,t,u,v) = 398 Term.list_mk_comb(Bit_Field_Extract_tm, 399 inst_list [bool,``:5``,``:4``,``:5``,``:4``] [r,s,t,u,v]) 400 |> mk_DataProcessing 401 handle HOL_ERR _ => raise ERR "mk_Bit_Field_Extract" ""; 402 403fun mk_Select_Bytes(r,s,t) = 404 Term.list_mk_comb(Select_Bytes_tm, inst_list [``:4``,``:4``,``:4``] [r,s,t]) 405 |> mk_DataProcessing 406 handle HOL_ERR _ => raise ERR "mk_Select_Bytes" ""; 407 408fun mk_Parallel_Add_Subtract(r,s,t,u,v) = 409 Term.list_mk_comb(Parallel_Add_Subtract_tm, 410 inst_list [bool,``:parallel_add_sub_op1 # parallel_add_sub_op2``, 411 ``:4``,``:4``,``:4``] [r,s,t,u,v]) 412 |> mk_DataProcessing 413 handle HOL_ERR _ => raise ERR "mk_Parallel_Add_Subtract" ""; 414 415fun mk_Divide(r,s,t,u) = 416 Term.list_mk_comb(Divide_tm, inst_list [bool,``:4``,``:4``,``:4``] [r,s,t,u]) 417 |> mk_DataProcessing 418 handle HOL_ERR _ => raise ERR "mk_Divide" ""; 419 420fun mk_Signed_Most_Significant_Multiply(r,s,t,u,v) = 421 Term.list_mk_comb(Signed_Most_Significant_Multiply_tm, 422 inst_list [``:4``,``:4``,``:4``,bool,``:4``] [r,s,t,u,v]) 423 |> mk_DataProcessing 424 handle HOL_ERR _ => raise ERR "mk_Signed_Most_Significant_Multiply" ""; 425 426fun mk_Signed_Most_Significant_Multiply_Subtract(r,s,t,u,v) = 427 Term.list_mk_comb(Signed_Most_Significant_Multiply_Subtract_tm, 428 inst_list [``:4``,``:4``,``:4``,bool,``:4``] [r,s,t,u,v]) 429 |> mk_DataProcessing 430 handle HOL_ERR _ => 431 raise ERR "mk_Signed_Most_Significant_Multiply_Subtract" ""; 432 433fun mk_Multiply_Accumulate_Accumulate(r,s,t,u) = 434 Term.list_mk_comb(Multiply_Accumulate_Accumulate_tm, 435 inst_list [``:4``,``:4``,``:4``,``:4``] [r,s,t,u]) 436 |> mk_DataProcessing 437 handle HOL_ERR _ => raise ERR "mk_Multiply_Accumulate_Accumulate" ""; 438 439fun mk_Byte_Reverse_Packed_Halfword(r,s) = 440 Term.list_mk_comb(Byte_Reverse_Packed_Halfword_tm, 441 inst_list [``:4``,``:4``] [r,s]) 442 |> mk_DataProcessing 443 handle HOL_ERR _ => raise ERR "mk_Byte_Reverse_Packed_Halfword" ""; 444 445fun mk_Byte_Reverse_Signed_Halfword(r,s) = 446 Term.list_mk_comb(Byte_Reverse_Signed_Halfword_tm, 447 inst_list [``:4``,``:4``] [r,s]) 448 |> mk_DataProcessing 449 handle HOL_ERR _ => raise ERR "mk_Byte_Reverse_Signed_Halfword" ""; 450 451fun mk_Unsigned_Sum_Absolute_Differences(r,s,t,u) = 452 Term.list_mk_comb(Unsigned_Sum_Absolute_Differences_tm, 453 inst_list [``:4``,``:4``,``:4``,``:4``] [r,s,t,u]) 454 |> mk_DataProcessing 455 handle HOL_ERR _ => raise ERR "mk_Unsigned_Sum_Absolute_Differences" ""; 456 457(* .. *) 458 459fun mk_StatusAccess t = 460 Term.mk_comb(StatusAccess_tm, inst [alpha |-> ``:status_access_instruction``] t) 461 handle HOL_ERR _ => raise ERR "mk_StatusAccess" ""; 462 463fun mk_Status_to_Register(r,s) = 464 Term.list_mk_comb(Status_to_Register_tm, inst_list [bool,``:4``] [r,s]) 465 |> mk_StatusAccess 466 handle HOL_ERR _ => raise ERR "mk_Status_to_Register" ""; 467 468fun mk_Register_to_Status(r,s,t) = 469 Term.list_mk_comb 470 (Register_to_Status_tm, inst_list [bool,``:4``,``:4``] [r,s,t]) 471 |> mk_StatusAccess 472 handle HOL_ERR _ => raise ERR "mk_Register_to_Status" ""; 473 474fun mk_Immediate_to_Status(r,s,t) = 475 Term.list_mk_comb 476 (Immediate_to_Status_tm, inst_list [bool,``:4``,``:12``] [r,s,t]) 477 |> mk_StatusAccess 478 handle HOL_ERR _ => raise ERR "mk_Immediate_to_Status" ""; 479 480fun mk_Change_Processor_State(r,s,t,u,v) = 481 Term.list_mk_comb(Change_Processor_State_tm, 482 inst_list [``:2``,bool,bool,bool,``:word5 option``] [r,s,t,u,v]) 483 |> mk_StatusAccess 484 handle HOL_ERR _ => raise ERR "mk_Change_Processor_State" ""; 485 486fun mk_Set_Endianness t = 487 Term.mk_comb(Set_Endianness_tm, inst [alpha |-> bool] t) 488 |> mk_StatusAccess 489 handle HOL_ERR _ => raise ERR "mk_Set_Endianness" ""; 490 491(* .. *) 492 493fun mk_LoadStore t = 494 Term.mk_comb(LoadStore_tm, inst [alpha |-> ``:load_store_instruction``] t) 495 handle HOL_ERR _ => raise ERR "mk_LoadStore" ""; 496 497fun mk_Load(r,s,t,u,v,w,x,y) = 498 Term.list_mk_comb(Load_tm, 499 inst_list [bool,bool,bool,bool,bool,``:4``,``:4``,``:addressing_mode2``] 500 [r,s,t,u,v,w,x,y]) |> mk_LoadStore 501 handle HOL_ERR _ => raise ERR "mk_Load" ""; 502 503fun mk_Store(r,s,t,u,v,w,x,y) = 504 Term.list_mk_comb(Store_tm, 505 inst_list [bool,bool,bool,bool,bool,``:4``,``:4``,``:addressing_mode2``] 506 [r,s,t,u,v,w,x,y]) |> mk_LoadStore 507 handle HOL_ERR _ => raise ERR "mk_Store" ""; 508 509fun mk_Load_Halfword(r,s,t,u,v,w,x,y,z) = 510 Term.list_mk_comb(Load_Halfword_tm, 511 inst_list [bool,bool,bool,bool,bool,bool,``:4``,``:4``, 512 ``:addressing_mode3``] 513 [r,s,t,u,v,w,x,y,z]) |> mk_LoadStore 514 handle HOL_ERR _ => raise ERR "mk_Load_Halfword" ""; 515 516fun mk_Store_Halfword(r,s,t,u,v,w,x) = 517 Term.list_mk_comb(Store_Halfword_tm, 518 inst_list [bool,bool,bool,bool,``:4``,``:4``,``:addressing_mode3``] 519 [r,s,t,u,v,w,x]) |> mk_LoadStore 520 handle HOL_ERR _ => raise ERR "mk_Store_Halfword" ""; 521 522fun mk_Load_Dual(r,s,t,u,v,w,x) = 523 Term.list_mk_comb(Load_Dual_tm, 524 inst_list [bool,bool,bool,``:4``,``:4``,``:4``,``:addressing_mode3``] 525 [r,s,t,u,v,w,x]) |> mk_LoadStore 526 handle HOL_ERR _ => raise ERR "mk_Load_Dual" ""; 527 528fun mk_Store_Dual(r,s,t,u,v,w,x) = 529 Term.list_mk_comb(Store_Dual_tm, 530 inst_list [bool,bool,bool,``:4``,``:4``,``:4``,``:addressing_mode3``] 531 [r,s,t,u,v,w,x]) |> mk_LoadStore 532 handle HOL_ERR _ => raise ERR "mk_Store_Dual" ""; 533 534fun mk_Load_Multiple(r,s,t,u,v,w) = 535 Term.list_mk_comb(Load_Multiple_tm, 536 inst_list [bool,bool,bool,bool,``:4``,``:16``] [r,s,t,u,v,w]) 537 |> mk_LoadStore 538 handle HOL_ERR _ => raise ERR "mk_Load_Multiple" ""; 539 540fun mk_Store_Multiple(r,s,t,u,v,w) = 541 Term.list_mk_comb(Store_Multiple_tm, 542 inst_list [bool,bool,bool,bool,``:4``,``:16``] [r,s,t,u,v,w]) 543 |> mk_LoadStore 544 handle HOL_ERR _ => raise ERR "mk_Store_Multiple" ""; 545 546fun mk_Load_Exclusive(r,s,t) = 547 Term.list_mk_comb 548 (Load_Exclusive_tm, inst_list [``:4``,``:4``,``:8``] [r,s,t]) 549 |> mk_LoadStore 550 handle HOL_ERR _ => raise ERR "mk_Load_Exclusive" ""; 551 552fun mk_Store_Exclusive(r,s,t,u) = 553 Term.list_mk_comb(Store_Exclusive_tm, 554 inst_list [``:4``,``:4``,``:4``,``:8``] [r,s,t,u]) 555 |> mk_LoadStore 556 handle HOL_ERR _ => raise ERR "mk_Store_Exclusive" ""; 557 558fun mk_Load_Exclusive_Doubleword(r,s,t) = 559 Term.list_mk_comb(Load_Exclusive_Doubleword_tm, 560 inst_list [``:4``,``:4``,``:4``] [r,s,t]) 561 |> mk_LoadStore 562 handle HOL_ERR _ => raise ERR "mk_Load_Exclusive_Doubleword" ""; 563 564fun mk_Store_Exclusive_Doubleword(r,s,t,u) = 565 Term.list_mk_comb(Store_Exclusive_Doubleword_tm, 566 inst_list [``:4``,``:4``,``:4``,``:4``] [r,s,t,u]) 567 |> mk_LoadStore 568 handle HOL_ERR _ => raise ERR "mk_Store_Exclusive_Doubleword" ""; 569 570fun mk_Load_Exclusive_Halfword(r,s) = 571 Term.list_mk_comb 572 (Load_Exclusive_Halfword_tm, inst_list [``:4``,``:4``] [r,s]) 573 |> mk_LoadStore 574 handle HOL_ERR _ => raise ERR "mk_Load_Exclusive_Halfword" ""; 575 576fun mk_Store_Exclusive_Halfword(r,s,t) = 577 Term.list_mk_comb(Store_Exclusive_Halfword_tm, 578 inst_list [``:4``,``:4``,``:4``] [r,s,t]) 579 |> mk_LoadStore 580 handle HOL_ERR _ => raise ERR "mk_Store_Exclusive_Halfword" ""; 581 582fun mk_Load_Exclusive_Byte(r,s) = 583 Term.list_mk_comb 584 (Load_Exclusive_Byte_tm, inst_list [``:4``,``:4``] [r,s]) 585 |> mk_LoadStore 586 handle HOL_ERR _ => raise ERR "mk_Load_Exclusive_Byte" ""; 587 588fun mk_Store_Exclusive_Byte(r,s,t) = 589 Term.list_mk_comb(Store_Exclusive_Byte_tm, 590 inst_list [``:4``,``:4``,``:4``] [r,s,t]) 591 |> mk_LoadStore 592 handle HOL_ERR _ => raise ERR "mk_Store_Exclusive_Byte" ""; 593 594fun mk_Store_Return_State(r,s,t,u) = 595 Term.list_mk_comb(Store_Return_State_tm, 596 inst_list [bool,bool,bool,``:5``] [r,s,t,u]) 597 |> mk_LoadStore 598 handle HOL_ERR _ => raise ERR "mk_Store_Return_State" ""; 599 600fun mk_Return_From_Exception(r,s,t,u) = 601 Term.list_mk_comb(Return_From_Exception_tm, 602 inst_list [bool,bool,bool,``:5``] [r,s,t,u]) 603 |> mk_LoadStore 604 handle HOL_ERR _ => raise ERR "mk_Return_From_Exception" ""; 605 606(* .. *) 607 608fun mk_Miscellaneous t = 609 Term.mk_comb 610 (Miscellaneous_tm, inst [alpha |-> ``:load_store_instruction``] t) 611 handle HOL_ERR _ => raise ERR "mk_Miscellaneous" ""; 612 613fun mk_Hint t = 614 Term.mk_comb(Hint_tm, inst [alpha |-> ``:hint``] t) 615 |> mk_Miscellaneous 616 handle HOL_ERR _ => raise ERR "mk_Hint" ""; 617 618fun mk_Breakpoint t = 619 Term.mk_comb(Breakpoint_tm, inst_word_alpha ``:16`` t) |> mk_Miscellaneous 620 handle HOL_ERR _ => raise ERR "mk_Breakpoint" ""; 621 622fun mk_Data_Memory_Barrier t = 623 Term.mk_comb 624 (Data_Memory_Barrier_tm, inst_word_alpha ``:4`` t) |> mk_Miscellaneous 625 handle HOL_ERR _ => raise ERR "mk_Data_Memory_Barrier" ""; 626 627fun mk_Swap(r,s,t,u) = 628 Term.list_mk_comb 629 (Swap_tm, inst_list [bool,``:4``,``:4``,``:4``] [r,s,t,u]) 630 |> mk_Miscellaneous 631 handle HOL_ERR _ => raise ERR "mk_Swap" ""; 632 633fun mk_Preload_Data(r,s,t,u) = 634 Term.list_mk_comb(Preload_Data_tm, 635 inst_list [bool,bool,``:4``,``:addressing_mode2``] [r,s,t,u]) 636 |> mk_Miscellaneous 637 handle HOL_ERR _ => raise ERR "mk_Preload_Data" ""; 638 639fun mk_Preload_Instruction(r,s,t) = 640 Term.list_mk_comb(Preload_Instruction_tm, 641 inst_list [bool,``:4``,``:addressing_mode2``] [r,s,t]) 642 |> mk_Miscellaneous 643 handle HOL_ERR _ => raise ERR "mk_Preload_Instruction" ""; 644 645fun mk_Supervisor_Call t = 646 Term.mk_comb(Supervisor_Call_tm, inst_word_alpha ``:24`` t) 647 |> mk_Miscellaneous 648 handle HOL_ERR _ => raise ERR "mk_Supervisor_Call" ""; 649 650fun mk_Secure_Monitor_Call t = 651 Term.mk_comb(Secure_Monitor_Call_tm, inst_word_alpha ``:4`` t) 652 |> mk_Miscellaneous 653 handle HOL_ERR _ => raise ERR "mk_Secure_Monitor_Call" ""; 654 655fun mk_Enterx_Leavex t = 656 Term.mk_comb(Enterx_Leavex_tm, t) 657 |> mk_Miscellaneous 658 handle HOL_ERR _ => raise ERR "mk_Enterx_Leavex" ""; 659 660fun mk_If_Then(r,s) = 661 Term.list_mk_comb(If_Then_tm, inst_list [``:4``,``:4``] [r,s]) 662 |> mk_Miscellaneous 663 handle HOL_ERR _ => raise ERR "mk_If_Then" ""; 664 665fun mk_Data_Synchronization_Barrier t = 666 Term.mk_comb(Data_Synchronization_Barrier_tm, inst_word_alpha ``:4`` t) 667 |> mk_Miscellaneous 668 handle HOL_ERR _ => raise ERR "mk_Data_Synchronization_Barrier" ""; 669 670fun mk_Instruction_Synchronization_Barrier t = 671 Term.mk_comb(Instruction_Synchronization_Barrier_tm, inst_word_alpha ``:4`` t) 672 |> mk_Miscellaneous 673 handle HOL_ERR _ => raise ERR "mk_Instruction_Synchronization_Barrier" ""; 674 675(* .. *) 676 677fun mk_Coprocessor t = 678 Term.mk_comb(Coprocessor_tm, inst [alpha |-> ``:coprocessor_instruction``] t) 679 handle HOL_ERR _ => raise ERR "mk_Coprocessor" ""; 680 681fun mk_Coprocessor_Load (r,s,t,u,v,w,x,y) = 682 Term.list_mk_comb(Coprocessor_Load_tm, 683 inst_list [bool,bool,bool,bool,``:4``,``:4``,``:4``,``:8``] 684 [r,s,t,u,v,w,x,y]) |> mk_Coprocessor 685 handle HOL_ERR _ => raise ERR "mk_Coprocessor_Load" ""; 686 687fun mk_Coprocessor_Store (r,s,t,u,v,w,x,y) = 688 Term.list_mk_comb(Coprocessor_Store_tm, 689 inst_list [bool,bool,bool,bool,``:4``,``:4``,``:4``,``:8``] 690 [r,s,t,u,v,w,x,y]) |> mk_Coprocessor 691 handle HOL_ERR _ => raise ERR "mk_Coprocessor_Store" ""; 692 693fun mk_Coprocessor_Data_Processing (r,s,t,u,v,w) = 694 Term.list_mk_comb(Coprocessor_Data_Processing_tm, 695 inst_list [``:4``,``:4``,``:4``,``:4``,``:3``,``:4``] 696 [r,s,t,u,v,w]) |> mk_Coprocessor 697 handle HOL_ERR _ => raise ERR "mk_Coprocessor_Data_Processing" ""; 698 699fun mk_Coprocessor_Transfer (r,s,t,u,v,w,x) = 700 Term.list_mk_comb(Coprocessor_Transfer_tm, 701 inst_list [``:3``,bool,``:4``,``:4``,``:4``,``:3``,``:4``] 702 [r,s,t,u,v,w,x]) |> mk_Coprocessor 703 handle HOL_ERR _ => raise ERR "mk_Coprocessor_Transfer" ""; 704 705fun mk_Coprocessor_Transfer_Two (r,s,t,u,v,w) = 706 Term.list_mk_comb(Coprocessor_Transfer_Two_tm, 707 inst_list [bool,``:4``,``:4``,``:4``,``:4``,``:4``] 708 [r,s,t,u,v,w]) |> mk_Coprocessor 709 handle HOL_ERR _ => raise ERR "mk_Coprocessor_Transfer_Two" ""; 710 711(* ------------------------------------------------------------------------- *) 712 713fun dest_op4 c e tm = 714 case Lib.with_exn boolSyntax.strip_comb tm e of 715 (t,[t1,t2,t3,t4]) => if Term.same_const t c then (t1,t2,t3,t4) else raise e 716 | _ => raise e; 717 718fun dest_op5 c e tm = 719 case Lib.with_exn boolSyntax.strip_comb tm e of 720 (t,[t1,t2,t3,t4,t5]) => 721 if Term.same_const t c then (t1,t2,t3,t4,t5) else raise e 722 | _ => raise e; 723 724fun dest_op6 c e tm = 725 case Lib.with_exn boolSyntax.strip_comb tm e of 726 (t,[t1,t2,t3,t4,t5,t6]) => 727 if Term.same_const t c then (t1,t2,t3,t4,t5,t6) else raise e 728 | _ => raise e; 729 730fun dest_op7 c e tm = 731 case Lib.with_exn boolSyntax.strip_comb tm e of 732 (t,[t1,t2,t3,t4,t5,t6,t7]) => 733 if Term.same_const t c then (t1,t2,t3,t4,t5,t6,t7) else raise e 734 | _ => raise e; 735 736fun dest_op8 c e tm = 737 case Lib.with_exn boolSyntax.strip_comb tm e of 738 (t,[t1,t2,t3,t4,t5,t6,t7,t8]) => 739 if Term.same_const t c then (t1,t2,t3,t4,t5,t6,t7,t8) else raise e 740 | _ => raise e; 741 742fun dest_op9 c e tm = 743 case Lib.with_exn boolSyntax.strip_comb tm e of 744 (t,[t1,t2,t3,t4,t5,t6,t7,t8,t9]) => 745 if Term.same_const t c then (t1,t2,t3,t4,t5,t6,t7,t8,t9) else raise e 746 | _ => raise e; 747 748(* .. *) 749 750val dest_Mode1_immediate = 751 HolKernel.dest_monop Mode1_immediate_tm (ERR "dest_Mode1_immediate" ""); 752 753val dest_Mode1_register = 754 HolKernel.dest_triop Mode1_register_tm (ERR "dest_Mode1_register" ""); 755 756val dest_Mode1_register_shifted_register = 757 HolKernel.dest_triop Mode1_register_shifted_register_tm 758 (ERR "dest_Mode1_register_shifted_register" ""); 759 760val dest_Mode2_immediate = 761 HolKernel.dest_monop Mode2_immediate_tm (ERR "dest_Mode2_immediate" ""); 762 763val dest_Mode2_register = 764 HolKernel.dest_triop Mode2_register_tm (ERR "dest_Mode2_register" ""); 765 766val dest_Mode3_immediate = 767 HolKernel.dest_monop Mode3_immediate_tm (ERR "dest_Mode3_immediate" ""); 768 769val dest_Mode3_register = 770 HolKernel.dest_binop Mode3_register_tm (ERR "dest_Mode3_register" ""); 771 772val dest_Hint_debug = 773 HolKernel.dest_monop Hint_debug_tm (ERR "dest_Hint_debug" ""); 774 775(* .. *) 776 777val dest_Branch = HolKernel.dest_monop Branch_tm (ERR "dest_Branch" ""); 778 779val dest_Branch_Target = 780 HolKernel.dest_monop Branch_Target_tm (ERR "dest_Branch_Target" "") o 781 dest_Branch; 782 783val dest_Branch_Exchange = 784 HolKernel.dest_monop Branch_Exchange_tm (ERR "dest_Branch_Exchange" "") o 785 dest_Branch; 786 787val dest_Branch_Link_Exchange_Immediate = 788 HolKernel.dest_triop Branch_Link_Exchange_Immediate_tm 789 (ERR "dest_Branch_Link_Exchange_Immediate" "") o dest_Branch; 790 791val dest_Branch_Link_Exchange_Register = 792 HolKernel.dest_monop Branch_Link_Exchange_Register_tm 793 (ERR "dest_Branch_Link_Exchange_Register" "") o dest_Branch; 794 795val dest_Compare_Branch = 796 HolKernel.dest_triop Compare_Branch_tm (ERR "dest_Compare_Branch" "") o 797 dest_Branch; 798 799val dest_Table_Branch_Byte = 800 HolKernel.dest_triop Table_Branch_Byte_tm (ERR "dest_Table_Branch_Byte" "") o 801 dest_Branch; 802 803val dest_Check_Array = 804 HolKernel.dest_binop Check_Array_tm (ERR "dest_Check_Array" "") o 805 dest_Branch; 806 807val dest_Handler_Branch_Link = 808 HolKernel.dest_binop Handler_Branch_Link_tm 809 (ERR "dest_Handler_Branch_Link" "") o dest_Branch; 810 811val dest_Handler_Branch_Link_Parameter = 812 HolKernel.dest_binop Handler_Branch_Link_Parameter_tm 813 (ERR "dest_Handler_Branch_Link_Parameter" "") o dest_Branch; 814 815val dest_Handler_Branch_Parameter = 816 HolKernel.dest_binop Handler_Branch_Parameter_tm 817 (ERR "dest_Handler_Branch_Parameter" "") o dest_Branch; 818 819(* .. *) 820 821val dest_DataProcessing = 822 HolKernel.dest_monop DataProcessing_tm (ERR "dest_DataProcessing" ""); 823 824val dest_Data_Processing = 825 dest_op5 Data_Processing_tm (ERR "dest_Data_Processing" "") o 826 dest_DataProcessing; 827 828val dest_Add_Sub = 829 dest_op4 Add_Sub_tm (ERR "dest_Add_Sub" "") o dest_DataProcessing; 830 831val dest_Move_Halfword = 832 HolKernel.dest_triop Move_Halfword_tm (ERR "dest_Move_Halfword" "") o 833 dest_DataProcessing; 834 835val dest_Multiply = 836 dest_op6 Multiply_tm (ERR "dest_Multiply" "") o dest_DataProcessing; 837 838val dest_Multiply_Subtract = 839 dest_op4 Multiply_Subtract_tm (ERR "dest_Multiply_Subtract" "") o 840 dest_DataProcessing; 841 842val dest_Signed_Halfword_Multiply = 843 dest_op7 Signed_Halfword_Multiply_tm 844 (ERR "dest_Signed_Halfword_Multiply" "") o dest_DataProcessing; 845 846val dest_Signed_Multiply_Dual = 847 dest_op6 Signed_Multiply_Dual_tm (ERR "dest_Signed_Multiply_Dual" "") o 848 dest_DataProcessing; 849 850val dest_Signed_Multiply_Long_Dual = 851 dest_op6 Signed_Multiply_Dual_tm (ERR "dest_Signed_Multiply_Dual" "") o 852 dest_DataProcessing; 853 854val dest_Multiply_Long = 855 dest_op7 Multiply_Long_tm (ERR "dest_Multiply_Long" "") o 856 dest_DataProcessing; 857 858val dest_Saturate = 859 dest_op6 Saturate_tm (ERR "dest_Saturate" "") o 860 dest_DataProcessing; 861 862val dest_Saturate_16 = 863 dest_op4 Saturate_16_tm (ERR "dest_Saturate_16" "") o 864 dest_DataProcessing; 865 866val dest_Saturating_Add_Subtract = 867 dest_op4 Saturating_Add_Subtract_tm (ERR "dest_Saturating_Add_Subtract" "") o 868 dest_DataProcessing; 869 870val dest_Pack_Halfword = 871 dest_op5 Pack_Halfword_tm (ERR "dest_Pack_Halfword" "") o 872 dest_DataProcessing; 873 874val dest_Extend_Byte = 875 dest_op5 Extend_Byte_tm (ERR "dest_Extend_Byte" "") o 876 dest_DataProcessing; 877 878val dest_Extend_Byte_16 = 879 dest_op5 Extend_Byte_16_tm (ERR "dest_Extend_Byte_16" "") o 880 dest_DataProcessing; 881 882val dest_Extend_Halfword = 883 dest_op5 Extend_Halfword_tm (ERR "dest_Extend_Halfword" "") o 884 dest_DataProcessing; 885 886val dest_Bit_Field_Clear_Insert = 887 dest_op4 Bit_Field_Clear_Insert_tm (ERR "dest_Bit_Field_Clear_Insert" "") o 888 dest_DataProcessing; 889 890val dest_Count_Leading_Zeroes = 891 HolKernel.dest_binop 892 Count_Leading_Zeroes_tm (ERR "dest_Count_Leading_Zeroes" "") o 893 dest_DataProcessing; 894 895val dest_Reverse_Bits = 896 HolKernel.dest_binop Reverse_Bits_tm (ERR "dest_Reverse_Bits" "") o 897 dest_DataProcessing; 898 899val dest_Byte_Reverse_Word = 900 HolKernel.dest_binop Byte_Reverse_Word_tm (ERR "dest_Byte_Reverse_Word" "") o 901 dest_DataProcessing; 902 903val dest_Bit_Field_Extract = 904 dest_op5 Bit_Field_Extract_tm (ERR "dest_Bit_Field_Extract" "") o 905 dest_DataProcessing; 906 907val dest_Select_Bytes = 908 HolKernel.dest_triop Select_Bytes_tm (ERR "dest_Select_Bytes" "") o 909 dest_DataProcessing; 910 911val dest_Parallel_Add_Subtract = 912 dest_op5 Parallel_Add_Subtract_tm (ERR "dest_Parallel_Add_Subtract" "") o 913 dest_DataProcessing; 914 915val dest_Divide = 916 dest_op4 Divide_tm (ERR "dest_Divide" "") o 917 dest_DataProcessing; 918 919val dest_Signed_Most_Significant_Multiply = 920 dest_op5 Signed_Most_Significant_Multiply_tm 921 (ERR "dest_Signed_Most_Significant_Multiply" "") o 922 dest_DataProcessing; 923 924val dest_Signed_Most_Significant_Multiply_Subtract = 925 dest_op5 Signed_Most_Significant_Multiply_Subtract_tm 926 (ERR "dest_Signed_Most_Significant_Multiply_Subtract" "") o 927 dest_DataProcessing; 928 929val dest_Multiply_Accumulate_Accumulate = 930 dest_op4 Multiply_Accumulate_Accumulate_tm 931 (ERR "dest_Multiply_Accumulate_Accumulate" "") o 932 dest_DataProcessing; 933 934val dest_Byte_Reverse_Packed_Halfword = 935 HolKernel.dest_binop Byte_Reverse_Packed_Halfword_tm 936 (ERR "dest_Byte_Reverse_Packed_Halfword" "") o 937 dest_DataProcessing; 938 939val dest_Byte_Reverse_Signed_Halfword = 940 HolKernel.dest_binop Byte_Reverse_Signed_Halfword_tm 941 (ERR "dest_Byte_Reverse_Signed_Halfword" "") o 942 dest_DataProcessing; 943 944val dest_Unsigned_Sum_Absolute_Differences = 945 dest_op4 Unsigned_Sum_Absolute_Differences_tm 946 (ERR "dest_Unsigned_Sum_Absolute_Differences" "") o 947 dest_DataProcessing; 948 949(* .. *) 950 951val dest_StatusAccess = 952 HolKernel.dest_monop StatusAccess_tm (ERR "dest_StatusAccess" ""); 953 954val dest_Status_to_Register = 955 HolKernel.dest_binop 956 Status_to_Register_tm (ERR "dest_Status_to_Register" "") o 957 dest_StatusAccess; 958 959val dest_Register_to_Status = 960 HolKernel.dest_triop 961 Register_to_Status_tm (ERR "dest_Register_to_Status" "") o 962 dest_StatusAccess; 963 964val dest_Immediate_to_Status = 965 HolKernel.dest_triop 966 Immediate_to_Status_tm (ERR "dest_Immediate_to_Status" "") o 967 dest_StatusAccess; 968 969val dest_Change_Processor_State = 970 dest_op5 Change_Processor_State_tm (ERR "dest_Change_Processor_State" "") o 971 dest_StatusAccess; 972 973val dest_Set_Endianness = 974 HolKernel.dest_monop Set_Endianness_tm (ERR "dest_Set_Endianness" "") o 975 dest_StatusAccess; 976 977(* .. *) 978 979val dest_LoadStore = 980 HolKernel.dest_monop LoadStore_tm (ERR "dest_LoadStore" ""); 981 982val dest_Load = 983 dest_op8 Load_tm (ERR "dest_Load" "") o 984 dest_LoadStore; 985 986val dest_Store = 987 dest_op8 Store_tm (ERR "dest_Store" "") o 988 dest_LoadStore; 989 990val dest_Load_Halfword = 991 dest_op9 Load_Halfword_tm (ERR "dest_Load_Halfword" "") o 992 dest_LoadStore; 993 994val dest_Store_Halfword = 995 dest_op7 Store_Halfword_tm (ERR "dest_Store_Halfword" "") o 996 dest_LoadStore; 997 998val dest_Load_Dual = 999 dest_op7 Load_Dual_tm (ERR "dest_Load_Dual" "") o 1000 dest_LoadStore; 1001 1002val dest_Store_Dual = 1003 dest_op7 Store_Dual_tm (ERR "dest_Store_Dual" "") o 1004 dest_LoadStore; 1005 1006val dest_Load_Multiple = 1007 dest_op6 Load_Multiple_tm (ERR "dest_Load_Multiple" "") o 1008 dest_LoadStore; 1009 1010val dest_Store_Multiple = 1011 dest_op6 Store_Multiple_tm (ERR "dest_Store_Multiple" "") o 1012 dest_LoadStore; 1013 1014val dest_Load_Exclusive = 1015 HolKernel.dest_triop Load_Exclusive_tm (ERR "dest_Load_Exclusive" "") o 1016 dest_LoadStore; 1017 1018val dest_Store_Exclusive = 1019 dest_op4 Store_Exclusive_tm (ERR "dest_Store_Exclusive" "") o 1020 dest_LoadStore; 1021 1022val dest_Load_Exclusive_Doubleword = 1023 HolKernel.dest_triop Load_Exclusive_Doubleword_tm 1024 (ERR "dest_Load_Exclusive_Doubleword" "") o 1025 dest_LoadStore; 1026 1027val dest_Store_Exclusive_Doubleword = 1028 dest_op4 Store_Exclusive_Doubleword_tm 1029 (ERR "dest_Store_Exclusive_Doubleword" "") o 1030 dest_LoadStore; 1031 1032val dest_Load_Exclusive_Halfword = 1033 HolKernel.dest_binop Load_Exclusive_Halfword_tm 1034 (ERR "dest_Load_Exclusive_Halfword" "") o 1035 dest_LoadStore; 1036 1037val dest_Store_Exclusive_Halfword = 1038 HolKernel.dest_triop Store_Exclusive_Halfword_tm 1039 (ERR "dest_Store_Exclusive_Halfword" "") o 1040 dest_LoadStore; 1041 1042val dest_Load_Exclusive_Byte = 1043 HolKernel.dest_binop 1044 Load_Exclusive_Byte_tm (ERR "dest_Load_Exclusive_Byte" "") o 1045 dest_LoadStore; 1046 1047val dest_Store_Exclusive_Byte = 1048 HolKernel.dest_triop 1049 Store_Exclusive_Byte_tm (ERR "dest_Store_Exclusive_Byte" "") o 1050 dest_LoadStore; 1051 1052val dest_Store_Return_State = 1053 dest_op4 Store_Return_State_tm (ERR "dest_Store_Return_State" "") o 1054 dest_LoadStore; 1055 1056val dest_Return_From_Exception = 1057 dest_op4 Return_From_Exception_tm (ERR "dest_Return_From_Exception" "") o 1058 dest_LoadStore; 1059 1060(* .. *) 1061 1062val dest_Miscellaneous = 1063 HolKernel.dest_monop Miscellaneous_tm (ERR "dest_Miscellaneous" ""); 1064 1065val dest_Hint = 1066 HolKernel.dest_monop Hint_tm (ERR "dest_Hint" "") o 1067 dest_Miscellaneous; 1068 1069val dest_Breakpoint = 1070 HolKernel.dest_monop Breakpoint_tm (ERR "dest_Breakpoint" "") o 1071 dest_Miscellaneous; 1072 1073val dest_Data_Memory_Barrier = 1074 HolKernel.dest_monop 1075 Data_Memory_Barrier_tm (ERR "dest_Data_Memory_Barrier" "") o 1076 dest_Miscellaneous; 1077 1078val dest_Swap = 1079 dest_op4 Swap_tm (ERR "dest_Swap" "") o 1080 dest_Miscellaneous; 1081 1082val dest_Preload_Data = 1083 dest_op4 Preload_Data_tm (ERR "dest_Preload_Data" "") o 1084 dest_Miscellaneous; 1085 1086val dest_Preload_Instruction = 1087 HolKernel.dest_triop 1088 Preload_Instruction_tm (ERR "dest_Preload_Instruction" "") o 1089 dest_Miscellaneous; 1090 1091val dest_Supervisor_Call = 1092 HolKernel.dest_monop Supervisor_Call_tm (ERR "dest_Supervisor_Call" "") o 1093 dest_Miscellaneous; 1094 1095val dest_Secure_Monitor_Call = 1096 HolKernel.dest_monop 1097 Secure_Monitor_Call_tm (ERR "dest_Secure_Monitor_Call" "") o 1098 dest_Miscellaneous; 1099 1100val dest_Enterx_Leavex = 1101 HolKernel.dest_monop Enterx_Leavex_tm (ERR "dest_Enterx_Leavex" "") o 1102 dest_Miscellaneous; 1103 1104val dest_If_Then = 1105 HolKernel.dest_binop If_Then_tm (ERR "dest_If_Then" "") o 1106 dest_Miscellaneous; 1107 1108val dest_Data_Synchronization_Barrier = 1109 HolKernel.dest_monop Data_Synchronization_Barrier_tm 1110 (ERR "dest_Data_Synchronization_Barrier" "") o 1111 dest_Miscellaneous; 1112 1113val dest_Instruction_Synchronization_Barrier = 1114 HolKernel.dest_monop Instruction_Synchronization_Barrier_tm 1115 (ERR "dest_Instruction_Synchronization_Barrier" "") o 1116 dest_Miscellaneous; 1117 1118(* .. *) 1119 1120val dest_Coprocessor = 1121 HolKernel.dest_monop Coprocessor_tm (ERR "dest_Coprocessor" ""); 1122 1123val dest_Coprocessor_Load = 1124 dest_op8 Coprocessor_Load_tm (ERR "dest_Coprocessor_Load" "") o 1125 dest_Coprocessor; 1126 1127val dest_Coprocessor_Store = 1128 dest_op8 Coprocessor_Store_tm (ERR "dest_Coprocessor_Store" "") o 1129 dest_Coprocessor; 1130 1131val dest_Coprocessor_Data_Processing = 1132 dest_op6 Coprocessor_Data_Processing_tm 1133 (ERR "dest_Coprocessor_Data_Processing" "") o 1134 dest_Coprocessor; 1135 1136val dest_Coprocessor_Transfer = 1137 dest_op7 Coprocessor_Transfer_tm (ERR "dest_Coprocessor_Transfer" "") o 1138 dest_Coprocessor; 1139 1140val dest_Coprocessor_Transfer_Two = 1141 dest_op6 Coprocessor_Transfer_Two_tm 1142 (ERR "dest_Coprocessor_Transfer_Two" "") o 1143 dest_Coprocessor; 1144 1145(* ------------------------------------------------------------------------- *) 1146 1147val can = Lib.can 1148 1149val is_Mode1_immediate = can dest_Mode1_immediate 1150val is_Mode1_register = can dest_Mode1_register 1151 1152val is_Mode1_register_shifted_register = 1153 can dest_Mode1_register_shifted_register 1154 1155val is_Mode2_immediate = can dest_Mode2_immediate 1156val is_Mode2_register = can dest_Mode2_register 1157val is_Mode3_immediate = can dest_Mode3_immediate 1158val is_Mode3_register = can dest_Mode3_register 1159val is_Hint_debug = can dest_Hint_debug 1160val is_Branch = can dest_Branch 1161val is_Branch_Target = can dest_Branch_Target 1162val is_Branch_Exchange = can dest_Branch_Exchange 1163val is_Branch_Link_Exchange_Immediate = can dest_Branch_Link_Exchange_Immediate 1164val is_Branch_Link_Exchange_Register = can dest_Branch_Link_Exchange_Register 1165val is_Compare_Branch = can dest_Compare_Branch 1166val is_Table_Branch_Byte = can dest_Table_Branch_Byte 1167val is_Check_Array = can dest_Check_Array 1168val is_Handler_Branch_Link = can dest_Handler_Branch_Link 1169val is_Handler_Branch_Link_Parameter = can dest_Handler_Branch_Link_Parameter 1170val is_Handler_Branch_Parameter = can dest_Handler_Branch_Parameter 1171val is_DataProcessing = can dest_DataProcessing 1172val is_Data_Processing = can dest_Data_Processing 1173val is_Add_Sub = can dest_Add_Sub 1174val is_Move_Halfword = can dest_Move_Halfword 1175val is_Multiply = can dest_Multiply 1176val is_Multiply_Subtract = can dest_Multiply_Subtract 1177val is_Signed_Halfword_Multiply = can dest_Signed_Halfword_Multiply 1178val is_Signed_Multiply_Dual = can dest_Signed_Multiply_Dual 1179val is_Signed_Multiply_Long_Dual = can dest_Signed_Multiply_Long_Dual 1180val is_Multiply_Long = can dest_Multiply_Long 1181val is_Saturate = can dest_Saturate 1182val is_Saturate_16 = can dest_Saturate_16 1183val is_Saturating_Add_Subtract = can dest_Saturating_Add_Subtract 1184val is_Pack_Halfword = can dest_Pack_Halfword 1185val is_Extend_Byte = can dest_Extend_Byte 1186val is_Extend_Byte_16 = can dest_Extend_Byte_16 1187val is_Extend_Halfword = can dest_Extend_Halfword 1188val is_Bit_Field_Clear_Insert = can dest_Bit_Field_Clear_Insert 1189val is_Count_Leading_Zeroes = can dest_Count_Leading_Zeroes 1190val is_Reverse_Bits = can dest_Reverse_Bits 1191val is_Byte_Reverse_Word = can dest_Byte_Reverse_Word 1192val is_Bit_Field_Extract = can dest_Bit_Field_Extract 1193val is_Select_Bytes = can dest_Select_Bytes 1194val is_Parallel_Add_Subtract = can dest_Parallel_Add_Subtract 1195val is_Divide = can dest_Divide 1196val is_Multiply_Accumulate_Accumulate = can dest_Multiply_Accumulate_Accumulate 1197val is_Byte_Reverse_Packed_Halfword = can dest_Byte_Reverse_Packed_Halfword 1198val is_Byte_Reverse_Signed_Halfword = can dest_Byte_Reverse_Signed_Halfword 1199 1200val is_Signed_Most_Significant_Multiply = 1201 can dest_Signed_Most_Significant_Multiply 1202 1203val is_Signed_Most_Significant_Multiply_Subtract = 1204 can dest_Signed_Most_Significant_Multiply_Subtract 1205 1206val is_Unsigned_Sum_Absolute_Differences = 1207 can dest_Unsigned_Sum_Absolute_Differences 1208 1209val is_StatusAccess = can dest_StatusAccess 1210val is_Status_to_Register = can dest_Status_to_Register 1211val is_Register_to_Status = can dest_Register_to_Status 1212val is_Immediate_to_Status = can dest_Immediate_to_Status 1213val is_Change_Processor_State = can dest_Change_Processor_State 1214val is_Set_Endianness = can dest_Set_Endianness 1215val is_LoadStore = can dest_LoadStore 1216val is_Load = can dest_Load 1217val is_Store = can dest_Store 1218val is_Load_Halfword = can dest_Load_Halfword 1219val is_Store_Halfword = can dest_Store_Halfword 1220val is_Load_Dual = can dest_Load_Dual 1221val is_Store_Dual = can dest_Store_Dual 1222val is_Load_Multiple = can dest_Load_Multiple 1223val is_Store_Multiple = can dest_Store_Multiple 1224val is_Load_Exclusive = can dest_Load_Exclusive 1225val is_Store_Exclusive = can dest_Store_Exclusive 1226val is_Load_Exclusive_Doubleword = can dest_Load_Exclusive_Doubleword 1227val is_Store_Exclusive_Doubleword = can dest_Store_Exclusive_Doubleword 1228val is_Load_Exclusive_Halfword = can dest_Load_Exclusive_Halfword 1229val is_Store_Exclusive_Halfword = can dest_Store_Exclusive_Halfword 1230val is_Load_Exclusive_Byte = can dest_Load_Exclusive_Byte 1231val is_Store_Exclusive_Byte = can dest_Store_Exclusive_Byte 1232val is_Store_Return_State = can dest_Store_Return_State 1233val is_Return_From_Exception = can dest_Return_From_Exception 1234val is_Miscellaneous = can dest_Miscellaneous 1235val is_Hint = can dest_Hint 1236val is_Breakpoint = can dest_Breakpoint 1237val is_Data_Memory_Barrier = can dest_Data_Memory_Barrier 1238val is_Swap = can dest_Swap 1239val is_Preload_Data = can dest_Preload_Data 1240val is_Preload_Instruction = can dest_Preload_Instruction 1241val is_Supervisor_Call = can dest_Supervisor_Call 1242val is_Secure_Monitor_Call = can dest_Secure_Monitor_Call 1243val is_Enterx_Leavex = can dest_Enterx_Leavex 1244val is_If_Then = can dest_If_Then 1245val is_Data_Synchronization_Barrier = can dest_Data_Synchronization_Barrier 1246 1247val is_Instruction_Synchronization_Barrier = 1248 can dest_Instruction_Synchronization_Barrier 1249 1250val is_Coprocessor = can dest_Coprocessor 1251val is_Coprocessor_Load = can dest_Coprocessor_Load 1252val is_Coprocessor_Store = can dest_Coprocessor_Store 1253val is_Coprocessor_Data_Processing = can dest_Coprocessor_Data_Processing 1254val is_Coprocessor_Transfer = can dest_Coprocessor_Transfer 1255val is_Coprocessor_Transfer_Two = can dest_Coprocessor_Transfer_Two 1256 1257end 1258