1(*  Title:      HOL/Word/Tools/smt_word.ML
2    Author:     Sascha Boehme, TU Muenchen
3
4SMT setup for words.
5*)
6
7structure SMT_Word: sig end =
8struct
9
10open Word_Lib
11
12
13(* SMT-LIB logic *)
14
15(* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers.
16   Better set the logic to "" and make at least Z3 happy. *)
17fun smtlib_logic ts =
18  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
19
20
21(* SMT-LIB builtins *)
22
23local
24  val smtlibC = SMTLIB_Interface.smtlibC
25
26  val wordT = \<^typ>\<open>'a::len word\<close>
27
28  fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
29  fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
30
31  fun word_typ (Type (\<^type_name>\<open>word\<close>, [T])) =
32      Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
33    | word_typ _ = NONE
34
35  fun word_num (Type (\<^type_name>\<open>word\<close>, [T])) k =
36        Option.map (index1 ("bv" ^ string_of_int k)) (try dest_binT T)
37    | word_num _ _ = NONE
38
39  fun if_fixed pred m n T ts =
40    let val (Us, U) = Term.strip_type T
41    in
42      if pred (U, Us) then SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T))) else NONE
43    end
44
45  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
46  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
47
48  fun add_word_fun f (t, n) =
49    let val (m, _) = Term.dest_Const t
50    in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
51
52  val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
53
54  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
55    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
56
57  fun shift m n T ts =
58    let val U = Term.domain_type T
59    in
60      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
61        (true, SOME i) =>
62          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
63      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
64    end
65
66  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
67
68  fun extract m n T ts =
69    let val U = Term.range_type (Term.range_type T)
70    in
71      (case (try (snd o HOLogic.dest_number o hd) ts, try dest_wordT U) of
72        (SOME lb, SOME i) =>
73          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
74      | _ => NONE)
75    end
76
77  fun mk_extend c ts = Term.list_comb (Const c, ts)
78
79  fun extend m n T ts =
80    let val (U1, U2) = Term.dest_funT T
81    in
82      (case (try dest_wordT U1, try dest_wordT U2) of
83        (SOME i, SOME j) =>
84          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
85          else NONE
86      | _ => NONE)
87    end
88
89  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
90
91  fun rotate m n T ts =
92    let val U = Term.domain_type (Term.range_type T)
93    in
94      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
95        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
96      | _ => NONE)
97    end
98in
99
100val setup_builtins =
101  SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
102  fold (add_word_fun if_fixed_all) [
103    (\<^term>\<open>uminus :: 'a::len word \<Rightarrow> _\<close>, "bvneg"),
104    (\<^term>\<open>plus :: 'a::len word \<Rightarrow> _\<close>, "bvadd"),
105    (\<^term>\<open>minus :: 'a::len word \<Rightarrow> _\<close>, "bvsub"),
106    (\<^term>\<open>times :: 'a::len word \<Rightarrow> _\<close>, "bvmul"),
107    (\<^term>\<open>bitNOT :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
108    (\<^term>\<open>bitAND :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
109    (\<^term>\<open>bitOR :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
110    (\<^term>\<open>bitXOR :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
111    (\<^term>\<open>word_cat :: 'a::len word \<Rightarrow> _\<close>, "concat") ] #>
112  fold (add_word_fun shift) [
113    (\<^term>\<open>shiftl :: 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
114    (\<^term>\<open>shiftr :: 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
115    (\<^term>\<open>sshiftr :: 'a::len word \<Rightarrow> _\<close>, "bvashr") ] #>
116  add_word_fun extract
117    (\<^term>\<open>slice :: _ \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "extract") #>
118  fold (add_word_fun extend) [
119    (\<^term>\<open>ucast :: 'a::len word \<Rightarrow> _\<close>, "zero_extend"),
120    (\<^term>\<open>scast :: 'a::len word \<Rightarrow> _\<close>, "sign_extend") ] #>
121  fold (add_word_fun rotate) [
122    (\<^term>\<open>word_rotl\<close>, "rotate_left"),
123    (\<^term>\<open>word_rotr\<close>, "rotate_right") ] #>
124  fold (add_word_fun if_fixed_args) [
125    (\<^term>\<open>less :: 'a::len word \<Rightarrow> _\<close>, "bvult"),
126    (\<^term>\<open>less_eq :: 'a::len word \<Rightarrow> _\<close>, "bvule"),
127    (\<^term>\<open>word_sless\<close>, "bvslt"),
128    (\<^term>\<open>word_sle\<close>, "bvsle") ]
129
130end
131
132
133(* setup *)
134
135val _ = Theory.setup (Context.theory_map (
136  SMTLIB_Interface.add_logic (20, smtlib_logic) #>
137  setup_builtins))
138
139end;
140