src/HOL/SMT_Examples/boogie.ML
author wenzelm
Sat Nov 16 16:57:09 2013 +0100 (2013-11-16)
changeset 54447 019394de2b41
parent 52734 077149654ab4
child 55788 67699e08e969
permissions -rw-r--r--
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
     1 (*  Title:      HOL/SMT_Examples/boogie.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Proving Boogie-generated verification conditions.
     5 *)
     6 
     7 signature BOOGIE =
     8 sig
     9   val boogie_prove: theory -> string -> unit
    10 end
    11 
    12 structure Boogie: BOOGIE =
    13 struct
    14 
    15 (* utility functions *)
    16 
    17 val as_int = fst o read_int o raw_explode
    18 
    19 
    20 val isabelle_name =
    21   let
    22     fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else
    23       (case s of
    24         "." => "_o_"
    25       | "_" => "_n_"
    26       | "$" => "_S_"
    27       | "@" => "_G_"
    28       | "#" => "_H_"
    29       | "^" => "_T_"
    30       | _   => ("_" ^ string_of_int (ord s) ^ "_"))
    31   in prefix "b_" o translate_string purge end
    32 
    33 
    34 
    35 (* context *)
    36 
    37 type context =
    38   typ Symtab.table * (term * bool) Symtab.table * term list * term list
    39 
    40 val empty_context: context = (Symtab.empty, Symtab.empty, [], [])
    41 
    42 
    43 fun add_type name (tds, fds, axs, vcs) =
    44   let
    45     val T = TFree (isabelle_name name, @{sort type})
    46     val tds' = Symtab.update (name, T) tds
    47   in (tds', fds, axs, vcs) end
    48 
    49 
    50 fun add_func name Ts T unique (tds, fds, axs, vcs) =
    51   let
    52     val t = Free (isabelle_name name, Ts ---> T)
    53     val fds' = Symtab.update (name, (t, unique)) fds
    54   in (tds, fds', axs, vcs) end
    55 
    56 
    57 fun add_axiom t (tds, fds, axs, vcs) = (tds, fds, t :: axs, vcs)
    58 
    59 fun add_vc t (tds, fds, axs, vcs) = (tds, fds, axs, t :: vcs)
    60 
    61 
    62 fun lookup_type (tds, _, _, _) name =
    63   (case Symtab.lookup tds name of
    64     SOME T => T
    65   | NONE => error "Undeclared type")
    66 
    67 
    68 fun lookup_func (_, fds, _, _) name =
    69   (case Symtab.lookup fds name of
    70     SOME t_unique => t_unique
    71   | NONE => error "Undeclared function")
    72 
    73 
    74 
    75 (* constructors *)
    76 
    77 fun mk_var name T = Free ("V_" ^ isabelle_name name, T)
    78 
    79 
    80 fun mk_arrayT (Ts, T) = Type (@{type_name "fun"}, [HOLogic.mk_tupleT Ts, T])
    81 
    82 
    83 fun mk_binary t (t1, t2) = t $ t1 $ t2
    84 
    85 
    86 fun mk_nary _ t [] = t
    87   | mk_nary f _ ts = uncurry (fold_rev f) (split_last ts)
    88 
    89 
    90 fun mk_distinct [] = @{const HOL.True}
    91   | mk_distinct [_] = @{const HOL.True}
    92   | mk_distinct (t :: ts) =
    93       let
    94         fun mk_noteq u u' =
    95           HOLogic.mk_conj (HOLogic.mk_not (HOLogic.mk_eq (t, u)), u')
    96       in fold_rev mk_noteq ts (mk_distinct ts) end
    97 
    98 
    99 fun mk_store m k v =
   100   let
   101     val mT = Term.fastype_of m and kT = Term.fastype_of k
   102     val vT = Term.fastype_of v
   103   in Const (@{const_name fun_upd}, mT --> kT --> vT --> mT) $ m $ k $ v end
   104 
   105 
   106 fun mk_quant q (Free (x, T)) t = q T $ absfree (x, T) t
   107   | mk_quant _ t _ = raise TERM ("bad variable", [t])
   108 
   109 
   110 fun mk_list T = HOLogic.mk_list T
   111 
   112 
   113 val patternT = @{typ "SMT.pattern"}
   114 
   115 fun mk_pat t =
   116   Const (@{const_name "SMT.pat"}, Term.fastype_of t --> patternT) $ t
   117 
   118 fun mk_pattern [] = raise TERM ("mk_pattern", [])
   119   | mk_pattern ts = mk_list patternT (map mk_pat ts)
   120 
   121 
   122 fun mk_trigger [] t = t
   123   | mk_trigger pss t =
   124       @{term "SMT.trigger"} $
   125         mk_list @{typ "SMT.pattern list"} (map mk_pattern pss) $ t
   126 
   127 
   128 (* parser *)
   129 
   130 fun repeat f n ls =
   131   let fun apply (xs, ls) = f ls |>> (fn x => x :: xs)
   132   in funpow (as_int n) apply ([], ls) |>> rev end
   133 
   134 
   135 fun parse_type _ (["bool"] :: ls) = (@{typ bool}, ls)
   136   | parse_type _ (["int"] :: ls) = (@{typ int}, ls)
   137   | parse_type cx (["array", arity] :: ls) =
   138       repeat (parse_type cx) arity ls |>> mk_arrayT o split_last
   139   | parse_type cx (("type-con" :: name :: _) :: ls) = (lookup_type cx name, ls)
   140   | parse_type _ _ = error "Bad type"
   141 
   142 
   143 fun parse_expr _ (["true"] :: ls) = (@{term True}, ls)
   144   | parse_expr _ (["false"] :: ls) = (@{term False}, ls)
   145   | parse_expr cx (["not"] :: ls) = parse_expr cx ls |>> HOLogic.mk_not
   146   | parse_expr cx (["and", n] :: ls) =
   147       parse_nary_expr cx n HOLogic.mk_conj @{term True} ls
   148   | parse_expr cx (["or", n] :: ls) =
   149       parse_nary_expr cx n HOLogic.mk_disj @{term False} ls
   150   | parse_expr cx (["implies"] :: ls) =
   151       parse_bin_expr cx (mk_binary @{term HOL.implies}) ls
   152   | parse_expr cx (["="] :: ls) = parse_bin_expr cx HOLogic.mk_eq ls
   153   | parse_expr cx (["var", name] :: ls) = parse_type cx ls |>> mk_var name
   154   | parse_expr cx (["fun", name, n] :: ls) =
   155       let val (t, _) = lookup_func cx name
   156       in repeat (parse_expr cx) n ls |>> curry Term.list_comb t end
   157   | parse_expr cx (("label" :: _) :: ls) = parse_expr cx ls
   158   | parse_expr _ (["int-num", n] :: ls) =
   159       (HOLogic.mk_number @{typ int} (as_int n), ls)
   160   | parse_expr cx (["<"] :: ls) =
   161       parse_bin_expr cx (mk_binary @{term "op < :: int => _"}) ls
   162   | parse_expr cx (["<="] :: ls) =
   163       parse_bin_expr cx (mk_binary @{term "op <= :: int => _"}) ls
   164   | parse_expr cx ([">"] :: ls) =
   165       parse_bin_expr cx (mk_binary @{term "op < :: int => _"}o swap) ls
   166   | parse_expr cx ([">="] :: ls) =
   167       parse_bin_expr cx (mk_binary @{term "op <= :: int => _"} o swap) ls
   168   | parse_expr cx (["+"] :: ls) =
   169       parse_bin_expr cx (mk_binary @{term "op + :: int => _"}) ls
   170   | parse_expr cx (["-"] :: ls) =
   171       parse_bin_expr cx (mk_binary @{term "op - :: int => _"}) ls
   172   | parse_expr cx (["*"] :: ls) =
   173       parse_bin_expr cx (mk_binary @{term "op * :: int => _"}) ls
   174   | parse_expr cx (["/"] :: ls) =
   175       parse_bin_expr cx (mk_binary @{term boogie_div}) ls
   176   | parse_expr cx (["%"] :: ls) =
   177       parse_bin_expr cx (mk_binary @{term boogie_mod}) ls
   178   | parse_expr cx (["select", n] :: ls) =
   179       repeat (parse_expr cx) n ls
   180       |>> (fn ts => hd ts $ HOLogic.mk_tuple (tl ts))
   181   | parse_expr cx (["store", n] :: ls) =
   182       repeat (parse_expr cx) n ls
   183       |>> split_last
   184       |>> (fn (ts, t) => mk_store (hd ts) (HOLogic.mk_tuple (tl ts)) t)
   185   | parse_expr cx (["forall", vars, pats, atts] :: ls) =
   186       parse_quant cx HOLogic.all_const vars pats atts ls
   187   | parse_expr cx (["exists", vars, pats, atts] :: ls) =
   188       parse_quant cx HOLogic.exists_const vars pats atts ls
   189   | parse_expr _ _ = error "Bad expression"
   190 
   191 
   192 and parse_bin_expr cx f ls = ls |> parse_expr cx ||>> parse_expr cx |>> f
   193 
   194 
   195 and parse_nary_expr cx n f c ls =
   196   repeat (parse_expr cx) n ls |>> mk_nary (curry f) c
   197 
   198 
   199 and parse_quant cx q vars pats atts ls =
   200   let
   201     val ((((vs, pss), _), t), ls') =
   202       ls
   203       |> repeat (parse_var cx) vars
   204       ||>> repeat (parse_pat cx) pats
   205       ||>> repeat (parse_attr cx) atts
   206       ||>> parse_expr cx
   207   in (fold_rev (mk_quant q) vs (mk_trigger pss t), ls') end
   208 
   209 
   210 and parse_var cx (["var", name] :: ls) = parse_type cx ls |>> mk_var name
   211   | parse_var _ _ = error "Bad variable"
   212 
   213 
   214 and parse_pat cx (["pat", n] :: ls) = repeat (parse_expr cx) n ls
   215   | parse_pat _ _ = error "Bad pattern"
   216 
   217 
   218 and parse_attr cx (["attribute", name, n] :: ls) =
   219       let
   220         fun attr (["expr-attr"] :: ls) = parse_expr cx ls |>> K ()
   221           | attr (("string-attr" :: _) :: ls) = ((), ls)
   222           | attr _ = error "Bad attribute value"
   223       in repeat attr n ls |>> K name end
   224   | parse_attr _ _ = error "Bad attribute"
   225 
   226 
   227 fun parse_func cx arity n ls =
   228   let
   229     val ((Ts, atts), ls') =
   230       ls |> repeat (parse_type cx) arity ||>> repeat (parse_attr cx) n
   231     val unique = member (op =) atts "unique"
   232   in ((split_last Ts, unique), ls') end
   233 
   234 
   235 fun parse_decl (("type-decl" :: name :: _) :: ls) cx = (ls, add_type name cx)
   236   | parse_decl (["fun-decl", name, arity, n] :: ls) cx =
   237       let val (((Ts, T), unique), ls') = parse_func cx arity n ls
   238       in (ls', add_func name Ts T unique cx) end
   239   | parse_decl (("axiom" :: _) :: ls) cx =
   240       let val (t, ls') = parse_expr cx ls
   241       in (ls', add_axiom t cx) end
   242   | parse_decl (("var-decl" :: _) :: ls) cx =
   243       parse_type cx ls |> snd |> rpair cx
   244   | parse_decl (("vc" :: _) :: ls) cx =
   245       let val (t, ls') = parse_expr cx ls
   246       in (ls', add_vc t cx) end
   247   | parse_decl _ _ = error "Bad declaration"
   248 
   249 
   250 fun parse_lines [] cx = cx
   251   | parse_lines ls cx = parse_decl ls cx |-> parse_lines
   252 
   253 
   254 
   255 (* splitting of text into a lists of lists of tokens *)
   256 
   257 fun is_blank c = (c = " " orelse c = "\t" orelse c = "\r" orelse c = "\n")
   258 
   259 fun explode_lines text =
   260   text
   261   |> split_lines
   262   |> map (String.tokens (is_blank o str))
   263   |> filter (fn [] => false | _ => true)
   264 
   265 
   266 
   267 (* proving verification conditions *)
   268 
   269 fun add_unique_axioms (tds, fds, axs, vcs) =
   270   Symtab.fold (fn (_, (t, true)) => cons t | _ => I) fds []
   271   |> map (swap o Term.dest_Free)
   272   |> AList.group (op =)
   273   |> map (fn (T, ns) => mk_distinct (map (Free o rpair T) ns))
   274   |> (fn axs' => (tds, fds, axs' @ axs, vcs))
   275 
   276 
   277 fun build_proof_context thy (tds, fds, axs, vcs) =
   278   let
   279     val vc =
   280       (case vcs of
   281         [vc] => vc
   282       | _ => error "Bad number of verification conditions")
   283   in
   284     Proof_Context.init_global thy
   285     |> Symtab.fold (fn (_, T) => Variable.declare_typ T) tds
   286     |> Symtab.fold (fn (_, (t, _)) => Variable.declare_term t) fds
   287     |> fold Variable.declare_term axs
   288     |> fold Variable.declare_term vcs
   289     |> pair (map HOLogic.mk_Trueprop axs, HOLogic.mk_Trueprop vc)
   290   end
   291 
   292 
   293 val boogie_rules =
   294   [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @
   295   [@{thm fun_upd_same}, @{thm fun_upd_apply}]
   296 
   297 
   298 fun boogie_tac ctxt axioms =
   299   ALLGOALS (SMT_Solver.smt_tac ctxt (boogie_rules @ axioms))
   300 
   301 
   302 fun boogie_prove thy text =
   303   let
   304     val lines = explode_lines text
   305 
   306     val ((axioms, vc), ctxt) =
   307       empty_context
   308       |> parse_lines lines
   309       |> add_unique_axioms
   310       |> build_proof_context thy
   311 
   312     val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
   313       boogie_tac context prems)
   314     val _ = writeln "Verification condition proved successfully"
   315 
   316   in () end
   317 
   318 
   319 (* Isar command *)
   320 
   321 val _ =
   322   Outer_Syntax.command @{command_spec "boogie_file"}
   323     "prove verification condition from .b2i file"
   324     (Thy_Load.provide_parse_files "boogie_file" >> (fn files =>
   325       Toplevel.theory (fn thy =>
   326         let
   327           val ([{text, ...}], thy') = files thy;
   328           val _ = boogie_prove thy' text;
   329         in thy' end)))
   330 
   331 end