Merge pull request #1 in SEL4/l4v from ~JALIM/l4v:etanercept-reloaded to master
* commit '28e6511148e7daeec3803465ca50294e2840ed4d': etanercept: remove user config for CFLAGS; it could inject shell commands. Added -fwrapv to default CFLAGS. etanercept: tweak header documentation. etanercept: revert accidental change to int and nat translation. etanercept: use term_pat antiquote, just for fun. etanercept: search for C compiler at run time, not at init time. etanercept: use HOLogic. etanercept: improve exception throwing and messages. etanercept: refactor variable handling. Uses Termtab for simplicity. etanercept: add a couple more examples. etanercept: refactor type lookup code. etanercept: avoid unnecessary floating point code. etanercept: add options: debug, timeout, and CFLAGS. etanercept: rename user command to "word_refute".
This commit is contained in:
Japheth Lim
commit
a918b41163
|
|
@ -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 \<Rightarrow> 8 signed word"} = "int8_t"
|
||||
| cast_to _ @{typ "8 signed word \<Rightarrow> 8 word"} = "uint8_t"
|
||||
| cast_to _ @{typ "8 signed word \<Rightarrow> 16 signed word"} = "int16_t"
|
||||
| cast_to _ @{typ "8 signed word \<Rightarrow> 16 word"} = "uint16_t"
|
||||
| cast_to _ @{typ "8 signed word \<Rightarrow> 32 signed word"} = "int32_t"
|
||||
| cast_to _ @{typ "8 signed word \<Rightarrow> 32 word"} = "uint32_t"
|
||||
| cast_to _ @{typ "8 signed word \<Rightarrow> 64 signed word"} = "int64_t"
|
||||
| cast_to _ @{typ "8 signed word \<Rightarrow> 64 word"} = "uint64_t"
|
||||
| cast_to _ @{typ "8 word \<Rightarrow> 8 signed word"} = "int8_t"
|
||||
| cast_to _ @{typ "8 word \<Rightarrow> 8 word"} = "uint8_t"
|
||||
| cast_to _ @{typ "8 word \<Rightarrow> 16 signed word"} = "int16_t"
|
||||
| cast_to _ @{typ "8 word \<Rightarrow> 16 word"} = "uint16_t"
|
||||
| cast_to _ @{typ "8 word \<Rightarrow> 32 signed word"} = "int32_t"
|
||||
| cast_to _ @{typ "8 word \<Rightarrow> 32 word"} = "uint32_t"
|
||||
| cast_to _ @{typ "8 word \<Rightarrow> 64 signed word"} = "int64_t"
|
||||
| cast_to _ @{typ "8 word \<Rightarrow> 64 word"} = "uint64_t"
|
||||
| cast_to _ @{typ "16 signed word \<Rightarrow> 8 signed word"} = "int8_t"
|
||||
| cast_to _ @{typ "16 signed word \<Rightarrow> 8 word"} = "uint8_t"
|
||||
| cast_to _ @{typ "16 signed word \<Rightarrow> 16 signed word"} = "int16_t"
|
||||
| cast_to _ @{typ "16 signed word \<Rightarrow> 16 word"} = "uint16_t"
|
||||
| cast_to _ @{typ "16 signed word \<Rightarrow> 32 signed word"} = "int32_t"
|
||||
| cast_to _ @{typ "16 signed word \<Rightarrow> 32 word"} = "uint32_t"
|
||||
| cast_to _ @{typ "16 signed word \<Rightarrow> 64 signed word"} = "int64_t"
|
||||
| cast_to _ @{typ "16 signed word \<Rightarrow> 64 word"} = "uint64_t"
|
||||
| cast_to _ @{typ "16 word \<Rightarrow> 8 signed word"} = "int8_t"
|
||||
| cast_to _ @{typ "16 word \<Rightarrow> 8 word"} = "uint8_t"
|
||||
| cast_to _ @{typ "16 word \<Rightarrow> 16 signed word"} = "int16_t"
|
||||
| cast_to _ @{typ "16 word \<Rightarrow> 16 word"} = "uint16_t"
|
||||
| cast_to _ @{typ "16 word \<Rightarrow> 32 signed word"} = "int32_t"
|
||||
| cast_to _ @{typ "16 word \<Rightarrow> 32 word"} = "uint32_t"
|
||||
| cast_to _ @{typ "16 word \<Rightarrow> 64 signed word"} = "int64_t"
|
||||
| cast_to _ @{typ "16 word \<Rightarrow> 64 word"} = "uint64_t"
|
||||
| cast_to _ @{typ "32 signed word \<Rightarrow> 8 signed word"} = "int8_t"
|
||||
| cast_to _ @{typ "32 signed word \<Rightarrow> 8 word"} = "uint8_t"
|
||||
| cast_to _ @{typ "32 signed word \<Rightarrow> 16 signed word"} = "int16_t"
|
||||
| cast_to _ @{typ "32 signed word \<Rightarrow> 16 word"} = "uint16_t"
|
||||
| cast_to _ @{typ "32 signed word \<Rightarrow> 32 signed word"} = "int32_t"
|
||||
| cast_to _ @{typ "32 signed word \<Rightarrow> 32 word"} = "uint32_t"
|
||||
| cast_to _ @{typ "32 signed word \<Rightarrow> 64 signed word"} = "int64_t"
|
||||
| cast_to _ @{typ "32 signed word \<Rightarrow> 64 word"} = "uint64_t"
|
||||
| cast_to _ @{typ "32 word \<Rightarrow> 8 signed word"} = "int8_t"
|
||||
| cast_to _ @{typ "32 word \<Rightarrow> 8 word"} = "uint8_t"
|
||||
| cast_to _ @{typ "32 word \<Rightarrow> 16 signed word"} = "int16_t"
|
||||
| cast_to _ @{typ "32 word \<Rightarrow> 16 word"} = "uint16_t"
|
||||
| cast_to _ @{typ "32 word \<Rightarrow> 32 signed word"} = "int32_t"
|
||||
| cast_to _ @{typ "32 word \<Rightarrow> 32 word"} = "uint32_t"
|
||||
| cast_to _ @{typ "32 word \<Rightarrow> 64 signed word"} = "int64_t"
|
||||
| cast_to _ @{typ "32 word \<Rightarrow> 64 word"} = "uint64_t"
|
||||
| cast_to _ @{typ "64 signed word \<Rightarrow> 8 signed word"} = "int8_t"
|
||||
| cast_to _ @{typ "64 signed word \<Rightarrow> 8 word"} = "uint8_t"
|
||||
| cast_to _ @{typ "64 signed word \<Rightarrow> 16 signed word"} = "int16_t"
|
||||
| cast_to _ @{typ "64 signed word \<Rightarrow> 16 word"} = "uint16_t"
|
||||
| cast_to _ @{typ "64 signed word \<Rightarrow> 32 signed word"} = "int32_t"
|
||||
| cast_to _ @{typ "64 signed word \<Rightarrow> 32 word"} = "uint32_t"
|
||||
| cast_to _ @{typ "64 signed word \<Rightarrow> 64 signed word"} = "int64_t"
|
||||
| cast_to _ @{typ "64 signed word \<Rightarrow> 64 word"} = "uint64_t"
|
||||
| cast_to _ @{typ "64 word \<Rightarrow> 8 signed word"} = "int8_t"
|
||||
| cast_to _ @{typ "64 word \<Rightarrow> 8 word"} = "uint8_t"
|
||||
| cast_to _ @{typ "64 word \<Rightarrow> 16 signed word"} = "int16_t"
|
||||
| cast_to _ @{typ "64 word \<Rightarrow> 16 word"} = "uint16_t"
|
||||
| cast_to _ @{typ "64 word \<Rightarrow> 32 signed word"} = "int32_t"
|
||||
| cast_to _ @{typ "64 word \<Rightarrow> 32 word"} = "uint32_t"
|
||||
| cast_to _ @{typ "64 word \<Rightarrow> 64 signed word"} = "int64_t"
|
||||
| cast_to _ @{typ "64 word \<Rightarrow> 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 "\<not> ?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 \<le> ?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 \<longrightarrow> ?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 \<and> ?b"} =>
|
||||
let val (vs', s1, s2) = bin_op a b
|
||||
in (vs', "(" ^ s1 ^ " && " ^ s2 ^ ")")
|
||||
end
|
||||
| @{const HOL.disj} $ a $ b =>
|
||||
| @{term_pat "?a \<or> ?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 <inttypes.h>\n" ^
|
||||
"#include <limits.h>\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 \<and> 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 "\<And>x. (x::32 word) \<noteq> y\<^sub>1 \<and> y \<ge> x"
|
||||
etanercept
|
||||
word_refute
|
||||
oops
|
||||
|
||||
lemma "(x::8 word) = y"
|
||||
etanercept
|
||||
word_refute
|
||||
oops
|
||||
|
||||
lemma "(x::64 word) < y"
|
||||
etanercept
|
||||
word_refute
|
||||
oops
|
||||
|
||||
lemma "\<And>(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 \<and> (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 \<or> 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) \<ge> y \<and> x \<ge> 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 \<and> x && (~~ 1) = 0 \<longrightarrow> x = 1"
|
||||
etanercept
|
||||
word_refute
|
||||
apply word_bitwise
|
||||
done
|
||||
lemma "(x::32 signed word) && 1 = 1 \<and> x && (~~ 1) = 0 \<longrightarrow> 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 \<Rightarrow> 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) \<ge> 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
|
||||
|
|
|
|||
Loading…
Reference in New Issue