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