src/HOL/Boogie/Tools/boogie_vcs.ML
author boehmes
Sun Aug 08 04:28:51 2010 +0200 (2010-08-08)
changeset 38245 27da291ee202
parent 35863 d4218a55cf20
child 38246 130d89f79ac1
permissions -rw-r--r--
added scanning of if-then-else expressions
boehmes@33419
     1
(*  Title:      HOL/Boogie/Tools/boogie_vcs.ML
boehmes@33419
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@33419
     3
boehmes@33419
     4
Store for Boogie's verification conditions.
boehmes@33419
     5
*)
boehmes@33419
     6
boehmes@33419
     7
signature BOOGIE_VCS =
boehmes@33419
     8
sig
boehmes@34181
     9
  type vc
boehmes@34181
    10
  val prop_of_vc: vc -> term
boehmes@34181
    11
  val size_of: vc -> int
boehmes@34181
    12
  val names_of: vc -> string list * string list
boehmes@34181
    13
  val path_names_of: vc -> (string * bool) list list
boehmes@34181
    14
  val paths_of: vc -> vc list
boehmes@34181
    15
  val split_path: int -> vc -> (vc * vc) option
boehmes@34181
    16
  val extract: vc -> string -> vc option
boehmes@34181
    17
  val only: string list -> vc -> vc
boehmes@34181
    18
  val without: string list -> vc -> vc
boehmes@34181
    19
  val paths_and: int list -> string list -> vc -> vc
boehmes@34181
    20
  val paths_without: int list -> string list -> vc -> vc
boehmes@34068
    21
boehmes@34181
    22
  datatype state = Proved | NotProved | PartiallyProved
boehmes@33419
    23
  val set: (string * term) list -> theory -> theory
boehmes@34181
    24
  val lookup: theory -> string -> vc option
boehmes@34181
    25
  val discharge: string * (vc * thm) -> theory -> theory
boehmes@34181
    26
  val state_of: theory -> (string * state) list
boehmes@34181
    27
  val state_of_vc: theory -> string -> string list * string list
boehmes@33419
    28
  val close: theory -> theory
boehmes@33419
    29
  val is_closed: theory -> bool
boehmes@35863
    30
boehmes@35863
    31
  val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) ->
boehmes@35863
    32
    theory -> theory
boehmes@33419
    33
end
boehmes@33419
    34
boehmes@33419
    35
structure Boogie_VCs: BOOGIE_VCS =
boehmes@33419
    36
struct
boehmes@33419
    37
boehmes@34181
    38
fun app_both f g (x, y) = (f x, g y)
boehmes@34181
    39
fun app_hd_tl f g = (fn [] => [] | x :: xs => f x :: map g xs)
boehmes@34068
    40
boehmes@34068
    41
boehmes@34181
    42
(* abstract representation of verification conditions *)
boehmes@34068
    43
boehmes@34181
    44
datatype vc =
boehmes@34181
    45
  Assume of term * vc |
boehmes@34181
    46
  Assert of (string * term) * vc |
boehmes@34181
    47
  Ignore of vc |
boehmes@34181
    48
  Proved of string * vc |
boehmes@34181
    49
  Choice of vc * vc |
boehmes@34181
    50
  True
boehmes@34068
    51
boehmes@34181
    52
val assume = curry Assume and assert = curry Assert
boehmes@34181
    53
and proved = curry Proved and choice = curry Choice
boehmes@34181
    54
and choice' = curry (Choice o swap)
boehmes@34181
    55
boehmes@34181
    56
val vc_of_term =
boehmes@34068
    57
  let
boehmes@34181
    58
    fun vc_of @{term True} = NONE
boehmes@34181
    59
      | vc_of (@{term assert_at} $ Free (n, _) $ t) =
boehmes@34181
    60
          SOME (Assert ((n, t), True))
boehmes@34181
    61
      | vc_of (@{term "op -->"} $ @{term True} $ u) = vc_of u
boehmes@34181
    62
      | vc_of (@{term "op -->"} $ t $ u) =
boehmes@34181
    63
          vc_of u |> Option.map (assume t)
boehmes@34181
    64
      | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
boehmes@34181
    65
          SOME (vc_of u |> the_default True |> assert (n, t))
boehmes@34181
    66
      | vc_of (@{term "op &"} $ t $ u) =
boehmes@34181
    67
          (case (vc_of t, vc_of u) of
boehmes@34181
    68
            (NONE, r) => r
boehmes@34181
    69
          | (l, NONE) => l
boehmes@34181
    70
          | (SOME lv, SOME rv) => SOME (Choice (lv, rv)))
boehmes@34181
    71
      | vc_of t = raise TERM ("vc_of_term", [t])
boehmes@34181
    72
  in the_default True o vc_of end
boehmes@34068
    73
boehmes@34181
    74
val prop_of_vc =
boehmes@34181
    75
  let
boehmes@34181
    76
    fun mk_conj t u = @{term "op &"} $ t $ u
boehmes@34068
    77
boehmes@34181
    78
    fun term_of (Assume (t, v)) = @{term "op -->"} $ t $ term_of v
boehmes@34181
    79
      | term_of (Assert ((n, t), v)) =
boehmes@34181
    80
          mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v)
boehmes@34181
    81
      | term_of (Ignore v) = term_of v
boehmes@34181
    82
      | term_of (Proved (_, v)) = term_of v
boehmes@34181
    83
      | term_of (Choice (lv, rv)) = mk_conj (term_of lv) (term_of rv)
boehmes@34181
    84
      | term_of True = @{term True}
boehmes@34181
    85
  in HOLogic.mk_Trueprop o term_of end
boehmes@34068
    86
boehmes@34068
    87
boehmes@34181
    88
(* properties of verification conditions *)
boehmes@34068
    89
boehmes@34181
    90
fun size_of (Assume (_, v)) = size_of v
boehmes@34181
    91
  | size_of (Assert (_, v)) = size_of v + 1
boehmes@34181
    92
  | size_of (Ignore v) = size_of v
boehmes@34181
    93
  | size_of (Proved (_, v)) = size_of v
boehmes@34181
    94
  | size_of (Choice (lv, rv)) = size_of lv + size_of rv
boehmes@34181
    95
  | size_of True = 0
boehmes@34068
    96
boehmes@34181
    97
val names_of =
boehmes@34181
    98
  let
boehmes@34181
    99
    fun add (Assume (_, v)) = add v
boehmes@34181
   100
      | add (Assert ((n, _), v)) = apfst (cons n) #> add v
boehmes@34181
   101
      | add (Ignore v) = add v
boehmes@34181
   102
      | add (Proved (n, v)) = apsnd (cons n) #> add v
boehmes@34181
   103
      | add (Choice (lv, rv)) = add lv #> add rv
boehmes@34181
   104
      | add True = I
boehmes@34181
   105
  in (fn vc => pairself rev (add vc ([], []))) end
boehmes@34068
   106
boehmes@34181
   107
fun path_names_of (Assume (_, v)) = path_names_of v
boehmes@34181
   108
  | path_names_of (Assert ((n, _), v)) =
boehmes@34181
   109
      path_names_of v
boehmes@34181
   110
      |> app_hd_tl (cons (n, true)) (cons (n, false))
boehmes@34181
   111
  | path_names_of (Ignore v) = path_names_of v
boehmes@34181
   112
  | path_names_of (Proved (n, v)) = map (cons (n, false)) (path_names_of v)
boehmes@34181
   113
  | path_names_of (Choice (lv, rv)) = path_names_of lv @ path_names_of rv
boehmes@34181
   114
  | path_names_of True = [[]]
boehmes@34181
   115
boehmes@34181
   116
fun count_paths (Assume (_, v)) = count_paths v
boehmes@34181
   117
  | count_paths (Assert (_, v)) = count_paths v
boehmes@34181
   118
  | count_paths (Ignore v) = count_paths v
boehmes@34181
   119
  | count_paths (Proved (_, v)) = count_paths v
boehmes@34181
   120
  | count_paths (Choice (lv, rv)) = count_paths lv + count_paths rv
boehmes@34181
   121
  | count_paths True = 1
boehmes@34068
   122
boehmes@34068
   123
boehmes@34181
   124
(* extract parts of a verification condition *)
boehmes@34068
   125
boehmes@34181
   126
fun paths_of (Assume (t, v)) = paths_of v |> map (assume t)
boehmes@34181
   127
  | paths_of (Assert (a, v)) = paths_of v |> app_hd_tl (assert a) Ignore
boehmes@34181
   128
  | paths_of (Ignore v) = paths_of v |> map Ignore
boehmes@34181
   129
  | paths_of (Proved (n, v)) = paths_of v |> app_hd_tl (proved n) Ignore
boehmes@34181
   130
  | paths_of (Choice (lv, rv)) =
boehmes@34181
   131
      map (choice' True) (paths_of lv) @ map (choice True) (paths_of rv)
boehmes@34181
   132
  | paths_of True = [True]
boehmes@34068
   133
boehmes@34181
   134
fun prune f (Assume (t, v)) = Option.map (assume t) (prune f v)
boehmes@34181
   135
  | prune f (Assert (a, v)) = f a v
boehmes@34181
   136
  | prune f (Ignore v) = Option.map Ignore (prune f v)
boehmes@34181
   137
  | prune f (Proved (n, v)) = Option.map (proved n) (prune f v)
boehmes@34181
   138
  | prune f (Choice (lv, rv)) =
boehmes@34181
   139
      (case (prune f lv, prune f rv) of
boehmes@34181
   140
        (NONE, r) => r |> Option.map (choice True)
boehmes@34181
   141
      | (l, NONE) => l |> Option.map (choice' True)
boehmes@34181
   142
      | (SOME lv', SOME rv') => SOME (Choice (lv', rv')))
boehmes@34181
   143
  | prune _ True = NONE
boehmes@34068
   144
boehmes@34181
   145
val split_path =
boehmes@34068
   146
  let
boehmes@34181
   147
    fun app f = Option.map (pairself f)
boehmes@34181
   148
boehmes@34181
   149
    fun split i (Assume (t, v)) = app (assume t) (split i v)
boehmes@34181
   150
      | split i (Assert (a, v)) =
boehmes@34068
   151
          if i > 1
boehmes@34181
   152
          then Option.map (app_both (assert a) Ignore) (split (i-1) v)
boehmes@34181
   153
          else Option.map (pair (Assert (a, True)))
boehmes@34181
   154
            (prune (SOME o Assert oo pair) (Ignore v))
boehmes@34181
   155
      | split i (Ignore v) = app Ignore (split i v)
boehmes@34181
   156
      | split i (Proved (n, v)) = app (proved n) (split i v)
boehmes@34181
   157
      | split i (Choice (v, True)) = app (choice' True) (split i v)
boehmes@34181
   158
      | split i (Choice (True, v)) = app (choice True) (split i v)
boehmes@34181
   159
      | split _ _ = NONE
boehmes@34181
   160
  in split end
boehmes@34068
   161
boehmes@34181
   162
fun select_labels P =
boehmes@34068
   163
  let
boehmes@34181
   164
    fun assert (a as (n, _)) v =
boehmes@34181
   165
      if P n then SOME (Assert (a, the_default True v))
boehmes@34181
   166
      else Option.map Ignore v
boehmes@34181
   167
    fun sel vc = prune (fn a => assert a o sel) vc
boehmes@34181
   168
  in sel end
boehmes@34181
   169
boehmes@34181
   170
fun extract vc l = select_labels (equal l) vc
boehmes@34181
   171
fun only ls = the_default True o select_labels (member (op =) ls)
boehmes@34181
   172
fun without ls = the_default True o select_labels (not o member (op =) ls)
boehmes@34181
   173
boehmes@34181
   174
fun select_paths ps sub_select =
boehmes@34181
   175
  let
boehmes@34181
   176
    fun disjoint pp = null (inter (op =) ps pp)
boehmes@34068
   177
boehmes@34181
   178
    fun sel pp (Assume (t, v)) = Assume (t, sel pp v)
boehmes@34181
   179
      | sel pp (Assert (a, v)) =
boehmes@34181
   180
          if member (op =) ps (hd pp)
boehmes@34181
   181
          then Assert (a, sel pp v)
boehmes@34181
   182
          else Ignore (sel pp v)
boehmes@34181
   183
      | sel pp (Ignore v) = Ignore (sel pp v)
boehmes@34181
   184
      | sel pp (Proved (n, v)) = Proved (n, sel pp v)
boehmes@34181
   185
      | sel pp (Choice (lv, rv)) =
boehmes@34181
   186
          let val (lpp, rpp) = chop (count_paths lv) pp
boehmes@34181
   187
          in
boehmes@34181
   188
            if disjoint lpp then Choice (sub_select lv, sel rpp rv)
boehmes@34181
   189
            else if disjoint rpp then Choice (sel lpp lv, sub_select rv)
boehmes@34181
   190
            else Choice (sel lpp lv, sel rpp rv)
boehmes@34181
   191
          end
boehmes@34181
   192
      | sel _ True = True
boehmes@34181
   193
boehmes@34181
   194
    fun sel0 vc =
boehmes@34181
   195
      let val pp = 1 upto count_paths vc
boehmes@34181
   196
      in if disjoint pp then True else sel pp vc end
boehmes@34181
   197
  in sel0 end
boehmes@34181
   198
boehmes@34181
   199
fun paths_and ps ls = select_paths ps (only ls)
boehmes@34181
   200
fun paths_without ps ls = without ls o select_paths ps (K True)
boehmes@34068
   201
boehmes@34068
   202
boehmes@34181
   203
(* discharge parts of a verification condition *)
boehmes@34068
   204
boehmes@34068
   205
local
boehmes@34181
   206
  fun cprop_of thy t = Thm.cterm_of thy (HOLogic.mk_Trueprop t)
boehmes@34181
   207
  fun imp_intr ct thm = Thm.implies_intr ct thm COMP_INCR @{thm impI}
boehmes@34181
   208
  fun imp_elim th thm = @{thm mp} OF [thm, th]
boehmes@34068
   209
  fun conj1 thm = @{thm conjunct1} OF [thm]
boehmes@34068
   210
  fun conj2 thm = @{thm conjunct2} OF [thm]
boehmes@34181
   211
  fun conj_intr lth rth = @{thm conjI} OF [lth, rth]
boehmes@34068
   212
in
boehmes@34181
   213
fun thm_of thy (Assume (t, v)) = imp_intr (cprop_of thy t) (thm_of thy v)
boehmes@34181
   214
  | thm_of thy (Assert (_, v)) = thm_of thy v
boehmes@34181
   215
  | thm_of thy (Ignore v) = thm_of thy v
boehmes@34181
   216
  | thm_of thy (Proved (_, v)) = thm_of thy v
boehmes@34181
   217
  | thm_of thy (Choice (lv, rv)) = conj_intr (thm_of thy lv) (thm_of thy rv)
boehmes@34181
   218
  | thm_of _ True = @{thm TrueI}
boehmes@34068
   219
boehmes@34181
   220
fun join (Assume (_, pv), pthm) (Assume (t, v), thm) =
boehmes@34068
   221
      let
boehmes@34181
   222
        val mk_prop = Thm.capply @{cterm Trueprop}
boehmes@34181
   223
        val ct = Thm.cprop_of thm |> Thm.dest_arg |> Thm.dest_arg1 |> mk_prop
boehmes@34181
   224
        val th = Thm.assume ct
boehmes@34181
   225
        val (v', thm') = join (pv, imp_elim th pthm) (v, imp_elim th thm)
boehmes@34181
   226
      in (Assume (t, v'), imp_intr ct thm') end
boehmes@34181
   227
  | join (Assert ((pn, pt), pv), pthm) (Assert ((n, t), v), thm) =
boehmes@34181
   228
      let val pthm1 = conj1 pthm
boehmes@34181
   229
      in
boehmes@34181
   230
        if pn = n andalso pt aconv t
boehmes@34181
   231
        then
boehmes@34181
   232
          let val (v', thm') = join (pv, conj2 pthm) (v, thm)
boehmes@34181
   233
          in (Proved (n, v'), conj_intr pthm1 thm') end
boehmes@34181
   234
        else raise THM ("join: not matching", 1, [thm, pthm])
boehmes@34181
   235
      end
boehmes@34181
   236
  | join (Ignore pv, pthm) (Assert (a, v), thm) =
boehmes@34181
   237
      join (pv, pthm) (v, thm) |>> assert a
boehmes@34181
   238
  | join (Proved (_, pv), pthm) (Proved (n, v), thm) =
boehmes@34181
   239
      let val (v', thm') = join (pv, pthm) (v, conj2 thm)
boehmes@34181
   240
      in (Proved (n, v'), conj_intr (conj1 thm) thm') end
boehmes@34181
   241
  | join (Ignore pv, pthm) (Proved (n, v), thm) =
boehmes@34181
   242
      let val (v', thm') = join (pv, pthm) (v, conj2 thm)
boehmes@34181
   243
      in (Proved (n, v'), conj_intr (conj1 thm) thm') end
boehmes@34181
   244
  | join (Choice (plv, prv), pthm) (Choice (lv, rv), thm) =
boehmes@34181
   245
      let
boehmes@34181
   246
        val (lv', lthm) = join (plv, conj1 pthm) (lv, conj1 thm)
boehmes@34181
   247
        val (rv', rthm) = join (prv, conj2 pthm) (rv, conj2 thm)
boehmes@34181
   248
      in (Choice (lv', rv'), conj_intr lthm rthm) end
boehmes@34181
   249
  | join (True, pthm) (v, thm) =
boehmes@34181
   250
      if Thm.prop_of pthm aconv @{prop True} then (v, thm)
boehmes@34181
   251
      else raise THM ("join: not True", 1, [pthm])
boehmes@34181
   252
  | join (_, pthm) (_, thm) = raise THM ("join: not matching", 1, [thm, pthm])
boehmes@34068
   253
end
boehmes@34068
   254
boehmes@34068
   255
boehmes@34068
   256
(* the VC store *)
boehmes@34068
   257
boehmes@35863
   258
fun err_unfinished () = error "An unfinished Boogie environment is still open."
boehmes@35863
   259
boehmes@35863
   260
fun err_vcs names = error (Pretty.string_of
boehmes@35863
   261
  (Pretty.big_list "Undischarged Boogie verification conditions found:"
boehmes@35863
   262
    (map Pretty.str names)))
boehmes@33419
   263
wenzelm@33522
   264
structure VCs = Theory_Data
boehmes@33419
   265
(
boehmes@35863
   266
  type T = ((vc * (term * thm)) Symtab.table * (theory -> thm -> thm)) option
boehmes@33419
   267
  val empty = NONE
boehmes@33419
   268
  val extend = I
wenzelm@33522
   269
  fun merge (NONE, NONE) = NONE
boehmes@35863
   270
    | merge _ = err_unfinished ()
boehmes@33419
   271
)
boehmes@33419
   272
boehmes@35863
   273
fun prep thy = vc_of_term #> (fn vc => (vc, (prop_of_vc vc, thm_of thy vc)))
boehmes@34068
   274
boehmes@34068
   275
fun set vcs thy = VCs.map (fn
boehmes@35863
   276
    NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I)
boehmes@35863
   277
  | SOME _ => err_unfinished ()) thy
boehmes@33419
   278
boehmes@34068
   279
fun lookup thy name =
boehmes@33419
   280
  (case VCs.get thy of
boehmes@35863
   281
    SOME (vcs, _) => Option.map fst (Symtab.lookup vcs name)
boehmes@33419
   282
  | NONE => NONE)
boehmes@33419
   283
boehmes@34181
   284
fun discharge (name, prf) =
boehmes@35863
   285
  let fun jn (vc, (t, thm)) = join prf (vc, thm) |> apsnd (pair t)
boehmes@35863
   286
  in VCs.map (Option.map (apfst (Symtab.map_entry name jn))) end
boehmes@34181
   287
boehmes@34181
   288
datatype state = Proved | NotProved | PartiallyProved
boehmes@34181
   289
boehmes@34181
   290
fun state_of_vc thy name =
boehmes@34181
   291
  (case lookup thy name of
boehmes@34181
   292
    SOME vc => names_of vc
boehmes@34181
   293
  | NONE => ([], []))
boehmes@33419
   294
boehmes@35863
   295
fun state_of_vc' (vc, _) =
boehmes@35863
   296
  (case names_of vc of
boehmes@35863
   297
    ([], _) => Proved
boehmes@35863
   298
  | (_, []) => NotProved
boehmes@35863
   299
  | (_, _) => PartiallyProved)
boehmes@35863
   300
boehmes@34181
   301
fun state_of thy =
boehmes@34181
   302
  (case VCs.get thy of
boehmes@35863
   303
    SOME (vcs, _) => map (apsnd state_of_vc') (Symtab.dest vcs)
boehmes@34181
   304
  | NONE => [])
boehmes@34181
   305
boehmes@35863
   306
fun finished g (_, (t, thm)) = Thm.prop_of (g thm) aconv t
boehmes@35863
   307
boehmes@34181
   308
fun close thy = thy |> VCs.map (fn
boehmes@35863
   309
    SOME (vcs, g) =>
boehmes@35863
   310
      let fun check vc = state_of_vc' vc = Proved andalso finished (g thy) vc
boehmes@35863
   311
      in
boehmes@35863
   312
        Symtab.dest vcs
boehmes@35863
   313
        |> map_filter (fn (n, vc) => if check vc then NONE else SOME n)
boehmes@35863
   314
        |> (fn names => if null names then NONE else err_vcs names)
boehmes@35863
   315
      end
boehmes@33419
   316
  | NONE => NONE)
boehmes@33419
   317
boehmes@33419
   318
val is_closed = is_none o VCs.get
boehmes@33419
   319
boehmes@35863
   320
fun rewrite_vcs f g thy =
boehmes@35863
   321
  let
boehmes@35863
   322
    fun rewr (_, (t, _)) = vc_of_term (f thy t)
boehmes@35863
   323
      |> (fn vc => (vc, (t, thm_of thy vc)))
boehmes@35863
   324
  in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end
boehmes@35863
   325
boehmes@33419
   326
end