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