1(* ------------------------------------------------------------------------ 2 Support for defining the context (antecedent) of an ARM step evaluation 3 For example: the architecture version, Thumb or ARM encoding, ... 4 ------------------------------------------------------------------------ *) 5 6structure arm_configLib :> arm_configLib = 7struct 8 9open HolKernel boolLib bossLib 10open armTheory utilsLib 11 12structure Parse = 13struct 14 open Parse 15 val (Type, Term) = parse_from_grammars armTheory.arm_grammars 16end 17 18open Parse 19 20val ERR = Feedback.mk_HOL_ERR "arm_configLib" 21 22(* ----------------------------------------------------------------------- *) 23 24val st = Term.mk_var ("s", Type.mk_type ("arm_state", [])) 25 26fun mk_arm_const n = Term.prim_mk_const {Thy = "arm", Name = n} 27fun mk_arm_type n = Type.mk_thy_type {Thy = "arm", Tyop = n, Args = []} 28 29(* ----------------------------------------------------------------------- *) 30 31val lower = List.map (List.map utilsLib.lowercase) 32 33val endian_options = lower 34 [["le", "little-endian", "LittleEndian"], 35 ["be", "big-endian", "BigEndian"]] 36 37val arch_options = lower 38 [["v4", "ARMv4"], 39 ["v4T", "ARMv4T"], 40 ["v5", "v5T", "ARMv5", "ARMv5T"], 41 ["v5TE", "ARMv5TE"], 42 ["v6", "ARMv6"], 43 ["v6K", "ARMv6K"], 44 ["v6T2", "ARMv6T2"], 45 ["v7", "v7_A", "v7-A", "ARMv7", "ARMv7_A", "ARMv7-A"], 46 ["v7_R", "v7-R", "ARMv7_R", "ARMv7-R"]] 47 48val thumb_options = 49 [["thumb","thumb2","16-bit","16"], 50 ["arm","32-bit","32"]] 51 52val vfp_options = lower 53 [["VFPv4"], 54 ["VFPv3"], 55 ["fp", "vfp", "VFPv2"], 56 ["nofp", "novfp"]] 57 58val default_options = 59 {arch = mk_arm_const "ARMv7_A", 60 bigendian = false, 61 thumb = false, 62 vfp = 3, 63 itblock = wordsSyntax.mk_wordii (0, 8)} 64 65fun isDelim c = 66 Char.isPunct c andalso (c <> #"-") andalso (c <> #":") orelse Char.isSpace c 67 68val print_options = utilsLib.print_options (SOME 34) 69 70fun process_options s = 71 let 72 val l = String.tokens isDelim s 73 val l = List.map utilsLib.lowercase l 74 val (bigendian, l) = process_opt endian_options "Endian" 75 (#bigendian default_options) l (fn i => i <> 0) 76 val (vfp, l) = 77 process_opt vfp_options "VFP" (#vfp default_options) l Lib.I 78 val (arch, l) = 79 process_opt arch_options "Arch" (#arch default_options) l 80 (fn i => 81 mk_arm_const 82 (case i of 83 0 => "ARMv4" | 1 => "ARMv4T" 84 | 2 => "ARMv5T" | 3 => "ARMv5TE" 85 | 4 => "ARMv6" | 5 => "ARMv6K" | 6 => "ARMv6T2" 86 | 7 => "ARMv7_A" | 8 => "ARMv7_R" 87 | _ => raise ERR "process_options" "Bad Arch option.")) 88 val (thumb, l) = process_opt thumb_options "Thumb" 89 (#thumb default_options) l (fn i => i = 0) 90 val (itblock, l) = 91 process_option (String.isPrefix "it:") 92 (fn s => 93 Option.valOf (Int.fromString (String.extract (s, 3, NONE)))) 94 "IT block" (#itblock default_options) l 95 (fn i => if i < 256 96 then wordsSyntax.mk_wordii (i, 8) 97 else raise ERR "process_options" "Bad IT value.") 98 in 99 if List.null l 100 then {arch = arch, 101 bigendian = bigendian, 102 thumb = thumb, 103 vfp = vfp, 104 itblock = itblock} 105 else ( print_options "Endianness" endian_options 106 ; print_options "Architecture version" arch_options 107 ; print_options "Thumb mode" thumb_options 108 ; print_options "Floating-point" vfp_options 109 ; raise ERR "process_options" 110 ("Unrecognized option" ^ 111 (if List.length l > 1 then "s" else "") ^ 112 ": " ^ String.concat (commafy l)) 113 ) 114 end 115 116(* ----------------------------------------------------------------------- *) 117 118local 119 val neg = boolSyntax.mk_neg 120 val architecture = ``^st.Architecture`` 121 val no_vfp = ``^st.VFPExtension = NoVFP`` 122 val extension_vfp2 = ``^st.VFPExtension = VFPv2`` 123 val extension_vfp3 = ``^st.VFPExtension = VFPv3`` 124 val extension_vfp4 = ``^st.VFPExtension = VFPv4`` 125 val cpsr_it = ``^st.CPSR.IT`` 126 val cpsr_e = ``^st.CPSR.E`` 127 val cpsr_t = ``^st.CPSR.T`` 128in 129 fun mk_config_terms s = 130 let 131 val c = process_options s 132 fun prop f t = if f c then t else neg t 133 fun eq t f = boolSyntax.mk_eq (t, f c) 134 in 135 (if #thumb c then [eq cpsr_it (#itblock)] else []) @ 136 (case #vfp c of 137 0 => [extension_vfp4] 138 | 1 => [extension_vfp3] 139 | 2 => [extension_vfp2] 140 | _ => [no_vfp]) @ 141 [eq architecture (#arch), 142 prop #bigendian cpsr_e, 143 prop #thumb cpsr_t] 144 end 145end 146 147(* ----------------------------------------------------------------------- *) 148 149end 150