diff --git a/lib/Etanercept.thy b/lib/Etanercept.thy index 8e18e5ece..105775078 100644 --- a/lib/Etanercept.thy +++ b/lib/Etanercept.thy @@ -13,14 +13,23 @@ theory Etanercept imports NICTACompat SignedWords WordBitwiseSigned + "ml-helpers/TermPatternAntiquote" keywords - "etanercept" :: diag + "word_refute" :: diag begin text {* This theory implements a tool for refuting word propositions. It works by constructing a C program that exhaustively explores the state space of your proposition. + Usage: + Run the "word_refute" command in a proof. The proof goal should involve only word + and boolean expressions. + Options: + These are config options which can be set using "declare" or "using". + - word_refute_debug enable verbose debugging output + - word_refute_timeout timeout, in seconds + It is currently a work in progress and has the following known issues: - Temporary files are just left for Isabelle to clean up when it exits. Should we be attempting to remove these ourselves? @@ -30,8 +39,6 @@ text {* with GNU statement expressions, but I'm unsure if it's worth it. - We currently only support 8-, 16-, 32-, and 64-bit words. It would be straightforward to support other non-standard widths if required. - - Much of the pattern matching in this theory was generated by a script and is quite verbose. It - could probably be simplified. The tool is named after etanercept, an ill-advised treatment for primary progressive aphasia, a condition who's symptoms include an inability to find the right words for things. Amusingly the @@ -47,7 +54,28 @@ ML {* struct (* Toggle this to enable debugging output. *) - val debug = false + val config_debug = let + val (config, setup) = Attrib.config_bool (Binding.name "word_refute_debug") (K false) + in + Context.>>(Context.map_theory setup); + config + end + + (* Timeout, in seconds. *) + val config_timeout = let + val (config, setup) = Attrib.config_real (Binding.name "word_refute_timeout") (K 60.0) + in + Context.>>(Context.map_theory setup); + config + end + + (* C compiler options. Rationale: + * -O3: search for counterexamples faster + * -fwrapv: match HOL-Word semantics for signed overflow + *) + val config_cflags = "-O3 -fwrapv" + + fun debug_log ctxt str = if Config.get ctxt config_debug then tracing str else () (* XXX: Clagged from metis *) fun dropWhile p = @@ -59,7 +87,8 @@ ML {* end (* Exponentiation. *) - fun exp base n = Real.floor (Math.pow (Real.fromInt base, Real.fromInt n)) + fun exp _ 0 = 1 + | exp base n = if n mod 2 = 0 then exp (base*base) (n div 2) else base * exp base (n - 1) (* Strip whitespace from the end of a string. *) fun rstrip s = @@ -85,7 +114,7 @@ ML {* |> String.concat (* Find a C compiler. Prefer Clang. *) - val cc = + fun cc () = let val (clang, r1) = Isabelle_System.bash_output "which clang"; val (gcc, r2) = Isabelle_System.bash_output "which gcc" @@ -96,281 +125,159 @@ ML {* end (* Compile a C program. *) - fun compile file = - case cc of + fun compile ctxt file = + case cc () of SOME compiler => let val serial = serial_string (); val tmp = File.shell_path (File.tmp_path (Path.explode ("etanercept" ^ serial ^ ".exe"))); - val (_, ret) = Isabelle_System.bash_output (compiler ^ " -O3 -o " ^ tmp ^ " " ^ file) + val cmd = compiler ^ " " ^ config_cflags ^ " -o " ^ tmp ^ " " ^ file + val _ = debug_log ctxt ("Compiling: " ^ cmd) + val (_, ret) = Isabelle_System.bash_output cmd in if ret = 0 then tmp - else error "failed to compile generated program (BUG)" + else error "Etanercept: failed to compile generated program (BUG)" end - | NONE => error "no available C compiler" + | NONE => error "Etanercept: no available C compiler" - (* Find index of x in xs *) - fun indexOf xs x = - let - fun indexOf' i xs x = - case xs of - [] => NONE - | (y::ys) => if x = y then SOME i else indexOf' (i + 1) ys x - in - indexOf' 0 xs x - end - - (* FIXME: ugh *) - fun type_supported [typ] = - (case typ of - @{typ 8} => true - | @{typ "8 signed"} => true - | @{typ 16} => true - | @{typ "16 signed"} => true - | @{typ 32} => true - | @{typ "32 signed"} => true - | @{typ 64} => true - | @{typ "64 signed"} => true - | _ => false) - | type_supported _ = false - - (* Find a previously seen variable's index or register a newly discovered variable. *) - fun var_index vs v = - case indexOf vs v of - NONE => (vs @ [v], length vs) - | SOME n => (vs, n) + (* Mapping between Isabelle and C variables. *) + fun var_index (vs, sz) v = + case Termtab.lookup vs v of + NONE => ((Termtab.update_new (v, sz) vs, sz+1), sz) + | SOME n => ((vs, sz), n) + val empty_var_index = (Termtab.empty, 0) (* The C symbol for the nth variable. *) fun to_var n = "v" ^ Int.toString n + (* Create variable list from mapping *) + val var_index_list = + fst #> Termtab.dest + #> sort (int_ord o apply2 snd) + #> map (apsnd to_var) - fun min_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "INT8_MIN" - | min_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "INT16_MIN" - | min_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "INT32_MIN" - | min_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "INT64_MIN" - | min_of (Var (_, Type (@{type_name "Word.word"}, _))) = "0" - | min_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "INT8_MIN" - | min_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "INT16_MIN" - | min_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "INT32_MIN" - | min_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "INT64_MIN" - | min_of (Var (_, Type (@{type_name nat}, _))) = "0" - | min_of (Var (_, Type (@{type_name int}, _))) = "INTMAX_MIN" - | min_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "INT8_MIN" - | min_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "INT16_MIN" - | min_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "INT32_MIN" - | min_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "INT64_MIN" - | min_of (Free (_, Type (@{type_name "Word.word"}, _))) = "0" - | min_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "INT8_MIN" - | min_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "INT16_MIN" - | min_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "INT32_MIN" - | min_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "INT64_MIN" - | min_of (Free (_, Type (@{type_name nat}, _))) = "0" - | min_of (Free (_, Type (@{type_name int}, _))) = "INTMAX_MIN" - | min_of _ = error "unsupported type (BUG)" + fun name_of (Free (name, _)) = safe_name name + | name_of t = raise TERM ("Etanercept: unexpected variable (BUG)", [t]) - fun max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "UINT8_MAX" - | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "INT8_MAX" - | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "UINT16_MAX" - | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "INT16_MAX" - | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "UINT32_MAX" - | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "INT32_MAX" - | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "UINT64_MAX" - | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "INT64_MAX" - | max_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "INT8_MAX" - | max_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "INT16_MAX" - | max_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "INT32_MAX" - | max_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "INT64_MAX" - | max_of (Var (_, Type (@{type_name nat}, _))) = "UINTMAX_MAX" - | max_of (Var (_, Type (@{type_name int}, _))) = "INTMAX_MAX" - | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "UINT8_MAX" - | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "INT8_MAX" - | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "UINT16_MAX" - | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "INT16_MAX" - | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "UINT32_MAX" - | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "INT32_MAX" - | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "UINT64_MAX" - | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "INT64_MAX" - | max_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "INT8_MAX" - | max_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "INT16_MAX" - | max_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "INT32_MAX" - | max_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "INT64_MAX" - | max_of (Free (_, Type (@{type_name nat}, _))) = "UINTMAX_MAX" - | max_of (Free (_, Type (@{type_name int}, _))) = "INTMAX_MAX" - | max_of _ = error "unsupported type (BUG)" - fun type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "uint8_t" - | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "int8_t" - | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "uint16_t" - | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "int16_t" - | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "uint32_t" - | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "int32_t" - | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "uint64_t" - | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "int64_t" - | type_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "int8_t" - | type_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "int16_t" - | type_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "int32_t" - | type_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "int64_t" - | type_of (Var (_, Type (@{type_name nat}, _))) = "uintmax_t" - | type_of (Var (_, Type (@{type_name int}, _))) = "intmax_t" - | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "uint8_t" - | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "int8_t" - | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "uint16_t" - | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "int16_t" - | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "uint32_t" - | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "int32_t" - | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "uint64_t" - | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "int64_t" - | type_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "int8_t" - | type_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "int16_t" - | type_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "int32_t" - | type_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "int64_t" - | type_of (Free (_, Type (@{type_name nat}, _))) = "uintmax_t" - | type_of (Free (_, Type (@{type_name int}, _))) = "intmax_t" - | type_of _ = error "unsupported type (BUG)" + (* Types that we know about. *) + type IntInfo = { isa_type: typ, + c_type: string, + c_min: string, + c_max: string, + c_printf: string + } + val type_info : IntInfo Typtab.table = + [ + { isa_type = @{typ "8 word"}, + c_type = "uint8_t", + c_min = "((uint8_t)0)", + c_max = "UINT8_MAX", + c_printf = "PRIu8" + }, + { isa_type = @{typ "16 word"}, + c_type = "uint16_t", + c_min = "((uint16_t)0)", + c_max = "UINT16_MAX", + c_printf = "PRIu16" + }, + { isa_type = @{typ "32 word"}, + c_type = "uint32_t", + c_min = "((uint32_t)0)", + c_max = "UINT32_MAX", + c_printf = "PRIu32" + }, + { isa_type = @{typ "64 word"}, + c_type = "uint64_t", + c_min = "((uint64_t)0)", + c_max = "UINT64_MAX", + c_printf = "PRIu64" + }, + { isa_type = @{typ "nat"}, + c_type = "uintmax_t", + c_min = "((uintmax_t)0)", + c_max = "UINTMAX_MAX", + c_printf = "PRIuMAX" + }, - fun name_of (Var ((name, _), _)) = safe_name name - | name_of (Free (name, _)) = safe_name name - | name_of _ = error "unexpected variable (BUG)" + { isa_type = @{typ "8 signed word"}, + c_type = "int8_t", + c_min = "INT8_MIN", + c_max = "INT8_MAX", + c_printf = "PRId8" + }, + { isa_type = @{typ "16 signed word"}, + c_type = "int16_t", + c_min = "INT16_MIN", + c_max = "INT16_MAX", + c_printf = "PRId16" + }, + { isa_type = @{typ "32 signed word"}, + c_type = "int32_t", + c_min = "INT32_MIN", + c_max = "INT32_MAX", + c_printf = "PRId32" + }, + { isa_type = @{typ "64 signed word"}, + c_type = "int64_t", + c_min = "INT64_MIN", + c_max = "INT64_MAX", + c_printf = "PRId64" + }, + { isa_type = @{typ "int"}, + c_type = "intmax_t", + c_min = "INTMAX_MIN", + c_max = "INTMAX_MAX", + c_printf = "PRIdMAX" + } + ] |> (fn infos => Typtab.make (map (fn info => (#isa_type info, info)) infos)) - fun format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "PRIu8" - | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "PRId8" - | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "PRIu16" - | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "PRId16" - | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "PRIu32" - | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "PRId32" - | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "PRIu64" - | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "PRId64" - | format_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "PRId8" - | format_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "PRId16" - | format_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "PRId32" - | format_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "PRId64" - | format_of (Var (_, Type (@{type_name nat}, _))) = "PRIuMAX" - | format_of (Var (_, Type (@{type_name int}, _))) = "PRIdMAX" - | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "PRIu8" - | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "PRId8" - | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "PRIu16" - | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "PRId16" - | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "PRIu32" - | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "PRId32" - | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "PRIu64" - | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "PRId64" - | format_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "PRId8" - | format_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "PRId16" - | format_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "PRId32" - | format_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "PRId64" - | format_of (Free (_, Type (@{type_name nat}, _))) = "PRIuMAX" - | format_of (Free (_, Type (@{type_name int}, _))) = "PRIdMAX" - | format_of _ = error "unsupported type (BUG)" + fun lookup_info f expect_success t = + let val severity = if expect_success then " (BUG)" else "" + in case t of + Free (_, ty) => (case Typtab.lookup type_info ty of + SOME info => f info + | NONE => raise TYPE ("etanercept: unsupported type" ^ severity, [ty], [t])) + | _ => raise TERM ("Etanercept: unsupported term" ^ severity, [t]) end - fun cast_to _ @{typ "8 signed word \ 8 signed word"} = "int8_t" - | cast_to _ @{typ "8 signed word \ 8 word"} = "uint8_t" - | cast_to _ @{typ "8 signed word \ 16 signed word"} = "int16_t" - | cast_to _ @{typ "8 signed word \ 16 word"} = "uint16_t" - | cast_to _ @{typ "8 signed word \ 32 signed word"} = "int32_t" - | cast_to _ @{typ "8 signed word \ 32 word"} = "uint32_t" - | cast_to _ @{typ "8 signed word \ 64 signed word"} = "int64_t" - | cast_to _ @{typ "8 signed word \ 64 word"} = "uint64_t" - | cast_to _ @{typ "8 word \ 8 signed word"} = "int8_t" - | cast_to _ @{typ "8 word \ 8 word"} = "uint8_t" - | cast_to _ @{typ "8 word \ 16 signed word"} = "int16_t" - | cast_to _ @{typ "8 word \ 16 word"} = "uint16_t" - | cast_to _ @{typ "8 word \ 32 signed word"} = "int32_t" - | cast_to _ @{typ "8 word \ 32 word"} = "uint32_t" - | cast_to _ @{typ "8 word \ 64 signed word"} = "int64_t" - | cast_to _ @{typ "8 word \ 64 word"} = "uint64_t" - | cast_to _ @{typ "16 signed word \ 8 signed word"} = "int8_t" - | cast_to _ @{typ "16 signed word \ 8 word"} = "uint8_t" - | cast_to _ @{typ "16 signed word \ 16 signed word"} = "int16_t" - | cast_to _ @{typ "16 signed word \ 16 word"} = "uint16_t" - | cast_to _ @{typ "16 signed word \ 32 signed word"} = "int32_t" - | cast_to _ @{typ "16 signed word \ 32 word"} = "uint32_t" - | cast_to _ @{typ "16 signed word \ 64 signed word"} = "int64_t" - | cast_to _ @{typ "16 signed word \ 64 word"} = "uint64_t" - | cast_to _ @{typ "16 word \ 8 signed word"} = "int8_t" - | cast_to _ @{typ "16 word \ 8 word"} = "uint8_t" - | cast_to _ @{typ "16 word \ 16 signed word"} = "int16_t" - | cast_to _ @{typ "16 word \ 16 word"} = "uint16_t" - | cast_to _ @{typ "16 word \ 32 signed word"} = "int32_t" - | cast_to _ @{typ "16 word \ 32 word"} = "uint32_t" - | cast_to _ @{typ "16 word \ 64 signed word"} = "int64_t" - | cast_to _ @{typ "16 word \ 64 word"} = "uint64_t" - | cast_to _ @{typ "32 signed word \ 8 signed word"} = "int8_t" - | cast_to _ @{typ "32 signed word \ 8 word"} = "uint8_t" - | cast_to _ @{typ "32 signed word \ 16 signed word"} = "int16_t" - | cast_to _ @{typ "32 signed word \ 16 word"} = "uint16_t" - | cast_to _ @{typ "32 signed word \ 32 signed word"} = "int32_t" - | cast_to _ @{typ "32 signed word \ 32 word"} = "uint32_t" - | cast_to _ @{typ "32 signed word \ 64 signed word"} = "int64_t" - | cast_to _ @{typ "32 signed word \ 64 word"} = "uint64_t" - | cast_to _ @{typ "32 word \ 8 signed word"} = "int8_t" - | cast_to _ @{typ "32 word \ 8 word"} = "uint8_t" - | cast_to _ @{typ "32 word \ 16 signed word"} = "int16_t" - | cast_to _ @{typ "32 word \ 16 word"} = "uint16_t" - | cast_to _ @{typ "32 word \ 32 signed word"} = "int32_t" - | cast_to _ @{typ "32 word \ 32 word"} = "uint32_t" - | cast_to _ @{typ "32 word \ 64 signed word"} = "int64_t" - | cast_to _ @{typ "32 word \ 64 word"} = "uint64_t" - | cast_to _ @{typ "64 signed word \ 8 signed word"} = "int8_t" - | cast_to _ @{typ "64 signed word \ 8 word"} = "uint8_t" - | cast_to _ @{typ "64 signed word \ 16 signed word"} = "int16_t" - | cast_to _ @{typ "64 signed word \ 16 word"} = "uint16_t" - | cast_to _ @{typ "64 signed word \ 32 signed word"} = "int32_t" - | cast_to _ @{typ "64 signed word \ 32 word"} = "uint32_t" - | cast_to _ @{typ "64 signed word \ 64 signed word"} = "int64_t" - | cast_to _ @{typ "64 signed word \ 64 word"} = "uint64_t" - | cast_to _ @{typ "64 word \ 8 signed word"} = "int8_t" - | cast_to _ @{typ "64 word \ 8 word"} = "uint8_t" - | cast_to _ @{typ "64 word \ 16 signed word"} = "int16_t" - | cast_to _ @{typ "64 word \ 16 word"} = "uint16_t" - | cast_to _ @{typ "64 word \ 32 signed word"} = "int32_t" - | cast_to _ @{typ "64 word \ 32 word"} = "uint32_t" - | cast_to _ @{typ "64 word \ 64 signed word"} = "int64_t" - | cast_to _ @{typ "64 word \ 64 word"} = "uint64_t" - | cast_to st t = error ("unsupported ucast/scast result type: " ^ - Pretty.string_of (Syntax.pretty_typ (Proof.context_of st) t)) + val min_of = lookup_info #c_min true + val max_of = lookup_info #c_max true + val type_of = lookup_info #c_type true + val format_of = lookup_info #c_printf true + + fun cast_to _ (Type ("fun", [from, to])) = + (case try (lookup_info #c_type false) (Free ("_", to)) of + SOME c_type => c_type + | NONE => raise TYPE ("Etanercept: unsupported ucast/scast result type", [to], [])) + | cast_to _ T = raise TYPE ("Etanercept: strange ucast/scast type (BUG)", [T], []) (* A printf format string for printing the variables. *) fun format_string vs = - case vs of - [] => "" - | (y::ys) => "\" " ^ name_of y ^ " = %\" " ^ format_of y ^ " \"\\n\" " ^ format_string ys + var_index_list vs + |> map (fn (var, c_var) => "\" " ^ name_of var ^ " = %\" " ^ format_of var ^ " \"\\n\" ") + |> String.concat (* The variables as a list of arguments to be passed to a C function. *) fun as_args vs = - let - fun as_args' n vs = - case vs of - [] => "" - | (_::ys) => ", " ^ to_var n ^ as_args' (n + 1) ys - in - as_args' 0 vs - end + var_index_list vs + |> map (fn (var, c_var) => ", " ^ c_var) + |> String.concat (* Initialisation for the variables. *) fun loop_header vs = - let - fun loop_header' i vs = - case vs of - [] => "" - | (y::ys) => type_of y ^ " " ^ to_var i ^ ";\n" ^ - "for (" ^ to_var i ^ " = " ^ min_of y ^ "; ; " ^ to_var i ^ "++) {\n" ^ - loop_header' (i + 1) ys - in - loop_header' 0 vs - end + var_index_list vs + |> map (fn (var, c_var) => + type_of var ^ " " ^ c_var ^ ";\n" ^ + "for (" ^ c_var ^ " = " ^ min_of var ^ "; ; " ^ c_var ^ "++) {\n") + |> String.concat (* Per-variable loop termination. *) fun loop_footer vs = - let - fun loop_footer' i vs = - case vs of - [] => "" - | (y::ys) => loop_footer' (i + 1) ys ^ - "if (" ^ to_var i ^ " == " ^ max_of y ^ ") { break; }\n" ^ - "}\n" - in - loop_footer' 0 vs - end + var_index_list vs + |> rev + |> map (fn (var, c_var) => + "if (" ^ c_var ^ " == " ^ max_of var ^ ") { break; }\n}\n") + |> String.concat (* Translate an Isabelle term into the equivalent C expression, collecting discovered variables * along the way. @@ -388,79 +295,79 @@ ML {* @{term "Trueprop"} $ t' => tr vs t' | @{term "True"} => (vs, "true") | @{term "False"} => (vs, "false") - | Const (@{const_name HOL.eq}, _) $ a $ b => + | @{term_pat "?a = ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " == " ^ s2 ^ ")") end - | Const (@{const_name HOL.Not}, _) $ a => + | @{term_pat "\ ?a"} => let val (vs', s) = tr vs a in (vs', "(!" ^ s ^ ")") end - | Const (@{const_name less}, _) $ a $ b => + | @{term_pat "?a < ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " < " ^ s2 ^ ")") end - | Const (@{const_name less_eq}, _) $ a $ b => + | @{term_pat "?a \ ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " <= " ^ s2 ^ ")") end - | Const (@{const_name plus}, _) $ a $ b => + | @{term_pat "?a + ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " + " ^ s2 ^ ")") end - | Const (@{const_name minus}, _) $ a $ b => + | @{term_pat "?a - ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " - " ^ s2 ^ ")") end - | Const (@{const_name times}, _) $ a $ b => + | @{term_pat "?a * ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " * " ^ s2 ^ ")") end - | Const (@{const_name uminus}, _) $ a => + | @{term_pat "- ?a"} => let val (vs', s) = tr vs a in (vs', "(-" ^ s ^ ")") end - | Const (@{const_name div}, _) $ a $ b => + | @{term_pat "?a div ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s2 ^ " == 0 ? 0 : (" ^ s1 ^ " / " ^ s2 ^ "))") end - | Const (@{const_name mod}, _) $ a $ b => + | @{term_pat "?a mod ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s2 ^ " == 0 ? " ^ s1 ^ " : (" ^ s1 ^ " % " ^ s2 ^ "))") end - | Const (@{const_name HOL.implies}, _) $ a $ b => + | @{term_pat "?a \ ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "((!" ^ s1 ^ ") || (" ^ s2 ^ "))") end - | Const (@{const_name Bits.shiftl}, _) $ a $ b => + | @{term_pat "shiftl ?a ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " << " ^ s2 ^ ")") end - | Const (@{const_name Bits.shiftr}, _) $ a $ b => + | @{term_pat "shiftr ?a ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " >> " ^ s2 ^ ")") end - | Const (@{const_name Bits.bitAND}, _) $ a $ b => + | @{term_pat "?a && ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " & " ^ s2 ^ ")") end - | Const (@{const_name Bits.bitOR}, _) $ a $ b => + | @{term_pat "?a || ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " | " ^ s2 ^ ")") end - | Const (@{const_name Bits.bitXOR}, _) $ a $ b => + | @{term_pat "?a xor ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " ^ " ^ s2 ^ ")") end - | Const (@{const_name Bits.bitNOT}, _) $ a => + | @{term_pat "NOT ?a"} => let val (vs', s) = tr vs a in (vs', "(~" ^ s ^ ")") end - | Const (@{const_name Bits.test_bit}, _) $ a $ b => + | @{term_pat "test_bit ?a ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " ^ & (1ULL << " ^ s2 ^ "))") end - | Const (@{const_name Bits.lsb}, _) $ a => + | @{term_pat "lsb ?a"} => let val (vs', s) = tr vs a in (vs', "(" ^ s ^ " & 1)") end @@ -472,60 +379,34 @@ ML {* let val (vs', s) = tr vs a in (vs', "((" ^ cast_to state typ ^ ")" ^ s ^ ")") end - | Free (name, Type (@{type_name "Word.word"}, typs)) => - if type_supported typs + | Free (name, T) => + if Typtab.defined type_info T then let val (vs', n) = var_index vs t in (vs', to_var n) end - else error ("unsupported word width of variable " ^ name) - | Var ((name, _), Type (@{type_name "Word.word"}, typs)) => - if type_supported typs - then let val (vs', n) = var_index vs t - in (vs', to_var n) - end - else error ("unsupported word width of variable " ^ name) - | Free (_, Type (@{type_name nat}, _)) => - let val (vs', n) = var_index vs t - in (vs', to_var n) - end - | Var (_, Type (@{type_name nat}, _)) => - let val (vs', n) = var_index vs t - in (vs', to_var n) - end - | Free (_, Type (@{type_name int}, _)) => - let val (vs', n) = var_index vs t - in (vs', to_var n) - end - | Var (_, Type (@{type_name int}, _)) => - let val (vs', n) = var_index vs t - in (vs', to_var n) - end - | @{const HOL.conj} $ a $ b => + else (case T of Type ("Word.word", _) => + raise TYPE ("unsupported word width of variable " ^ name, [T], []) + | _ => raise TYPE ("unsupported type of variable " ^ name, [T], [])) + | @{term_pat "?a \ ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " && " ^ s2 ^ ")") end - | @{const HOL.disj} $ a $ b => + | @{term_pat "?a \ ?b"} => let val (vs', s1, s2) = bin_op a b in (vs', "(" ^ s1 ^ " || " ^ s2 ^ ")") end - | Const (@{const_name Groups.zero}, _) => (vs, "(0)") - | Const (@{const_name Groups.one}, _) => (vs, "(1)") - | Const (@{const_name Suc}, _) $ a => + | @{term_pat "0"} => (vs, "(0)") + | @{term_pat "1"} => (vs, "(1)") + | @{term_pat "Suc ?a"} => let val (vs', s) = tr vs a in (vs', "(1 + " ^ s ^ ")") end - | Const (@{const_name numeral}, _) $ a => - (* XXX: Clagged from c-parser *) - let fun calc acc base t = case t of - Const (@{const_name "Num.num.Bit0"}, _) $ t' => calc acc (base * 2) t' - | Const (@{const_name "Num.num.Bit1"}, _) $ t' => calc (acc + base) (base * 2) t' - | Const (@{const_name "Num.num.One"}, _) => acc + base - | _ => error "unexpected numeric literal case (BUG)"; - val v = calc 0 1 a; - val suffix = if v > exp 2 32 - 1 then "ull" else "" - in (vs, "(" ^ string_of_int (calc 0 1 a) ^ suffix ^ ")") + | @{term_pat "numeral ?a"} => + let val a' = HOLogic.dest_num a + val suffix = if a' > exp 2 32 - 1 then "ull" else "" + in (vs, "(" ^ string_of_int a' ^ suffix ^ ")") end - | _ => error ("unsupported subterm " ^ Pretty.string_of (Syntax.pretty_term (Proof.context_of state) t)) + | _ => raise TERM ("unsupported subterm ", [t]) end (* Construct a C program to match the current goal state. *) @@ -535,7 +416,7 @@ ML {* val {goal = g, ...} = Proof.raw_goal state; val (_, g') = Subgoal.focus (Proof.context_of state) 1 g val (gi, _) = Logic.goal_params (Thm.prop_of g') 1 - val (vars, expr) = translate state [] gi + val (vars, expr) = translate state empty_var_index gi in "#include \n" ^ "#include \n" ^ @@ -555,63 +436,74 @@ ML {* (* Try to refute the current goal by using a C program to find a counter example. *) fun refute st = - case cc of - SOME _ => - let - val program = make_program st; - val serial = serial_string (); - val tmp = File.tmp_path (Path.explode ("etanercept" ^ serial ^ ".c")); - val _ = File.write tmp program; - val aout = compile (File.shell_path tmp); - val (msg, ret) = Isabelle_System.bash_output aout - in - if debug - then writeln ("Program:\n" ^ program ^ "\nWritten to: " ^ File.shell_path tmp ^ "\nCompiled to: " ^ aout) - else (); - (if ret = 0 - then msg - else "Etanercept found no counter example") - |> writeln - end - | NONE => writeln "no available C compiler" + let + val ctxt = Proof.context_of (Toplevel.proof_of st); + val program = make_program st; + val serial = serial_string (); + val tmp = File.tmp_path (Path.explode ("etanercept" ^ serial ^ ".c")); + val _ = File.write tmp program; + val aout = compile ctxt (File.shell_path tmp); + val _ = debug_log ctxt + ("Program:\n" ^ program ^ "\nWritten to: " ^ File.shell_path tmp ^ "\nCompiled to: " ^ aout) + val (msg, ret) = TimeLimit.timeLimit (Config.get ctxt config_timeout |> Time.fromReal) + Isabelle_System.bash_output aout + in + (if ret = 0 + then msg + else "Etanercept found no counter example") + |> writeln + end + handle TimeLimit.TimeOut => + warning "Etanercept: timed out" (* Install the command itself. *) - val _ = Outer_Syntax.command @{command_keyword etanercept} + val _ = Outer_Syntax.command @{command_keyword word_refute} "Construct a C program to find counter-examples to word propositions" (Scan.succeed [] >> (fn _ => Toplevel.keep_proof refute)) end *} + +text {* Basic examples *} lemma "True \ False" - etanercept + word_refute oops lemma "(x::32 word) = 0" - etanercept + word_refute + + using [[word_refute_debug]] + word_refute oops -etanercept +word_refute -- "requires a proof state" +text {* Can deal with top-level quantified vars *} lemma "\x. (x::32 word) \ y\<^sub>1 \ y \ x" - etanercept + word_refute oops lemma "(x::8 word) = y" - etanercept + word_refute oops lemma "(x::64 word) < y" - etanercept + word_refute oops lemma "\(x::32 word) y. x = y" - etanercept + word_refute oops text {* Previously, this example would give us a tautological comparison warning from Clang. *} lemma "y = y \ (x::32 word) << y = x" - etanercept + word_refute + oops + +text {* Also works for nats (approximated with uint64) *} +lemma "(x :: nat) = 0" + word_refute oops text {* Example that partially demonstrates Etanercept's utility. *} @@ -621,7 +513,7 @@ lemma "(x::8 word) > y \ x < y + y + y + y" (* quickcheck[random] takes a little while *) quickcheck[random] (* Etanercept immediately finds the trivial counterexample *) - etanercept + word_refute oops text {* Example that demonstrates one of Etanercept's weaknesses. *} @@ -629,7 +521,7 @@ lemma "(x::32 word) div y = x" (* The naive exploration strategy means we wait for Etanercept to try every value of y before * moving x beyond 0. *) - etanercept + word_refute oops text {* @@ -638,74 +530,91 @@ text {* discovery of a counter-example. *} lemma "(x::64 word) \ y \ x \ y + y" - etanercept + word_refute oops text {* Various cases that test our handling of numeric literals. *} lemma "(x::32 word) && 45 = 0" - etanercept + word_refute oops lemma "(x::32 word) < 45" - etanercept + word_refute oops lemma "(x::32 word) < 0" - etanercept + word_refute oops lemma "(x::32 word) < 1" - etanercept + word_refute oops lemma "(x::32 word) < 0x45" - etanercept + word_refute oops text {* Test something non-trivial that we shouldn't be able to refute. *} lemma "(x::32 word) && 1 = 1 \ x && (~~ 1) = 0 \ x = 1" - etanercept + word_refute apply word_bitwise done lemma "(x::32 signed word) && 1 = 1 \ x && (~~ 1) = 0 \ x = 1" - etanercept + word_refute apply word_bitwise_signed done text {* Test that division by zero is correctly modelled with Isabelle's semantics. *} lemma "(x::64 word) div 0 = 0" - etanercept + word_refute by (simp add: word_arith_nat_defs(6)) text {* Test we can handle large literals. *} -lemma "(x::64 word) > 0xcafebeefcafebeef" - etanercept +lemma "0xdeadbeeffacecafe > 0xdeadbeeffacade00 + (x::64 word)" + word_refute oops text {* Test some casting operations. *} lemma "(ucast::32 signed word \ 32 word) (x::32 signed word) = (y::32 word)" - etanercept + word_refute oops lemma "ucast (x::32 word) = (y:: 8 word)" - etanercept + word_refute oops lemma "ucast (x::32 word) = (y::32 word)" - etanercept + word_refute oops lemma "scast (x::32 signed word) = (y::8 word)" - etanercept + word_refute oops text {* Try some things we shouldn't be able to refute. *} lemma "(x::64 word) >> 0 = x" - etanercept + word_refute by simp lemma "(x::64 word) >> 1 = x div 2" - etanercept + word_refute apply simp apply (rule shiftr_div_2n_w[where n=1, simplified]) apply (simp add:word_size) done lemma "(x::64 word) << 1 = x * 2" - etanercept + word_refute apply (subst shiftl_t2n) apply simp done +text {* Test that our compiler setup permits signed overflow *} +lemma "(x :: 32 signed word) < x + 1" + word_refute -- "should find INT_MAX" + oops + +text {* C translation pitfalls *} +lemma "(ucast (x * y :: 16 word) :: 32 signed word) \ 0" + text {* A naive translation fails due to semantic mismatch *} + word_refute + by simp + + +text {* Unsupported constructs *} +lemma "(x :: 1 word) = 0" -- "bad word size" + (* word_refute *) + oops + end