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