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