src/HOL/Boogie/Tools/boogie_commands.ML
author boehmes
Sun Aug 08 04:28:51 2010 +0200 (2010-08-08)
changeset 38245 27da291ee202
parent 37944 4b7afae88c57
child 38756 d07959fabde6
permissions -rw-r--r--
added scanning of if-then-else expressions
     1 (*  Title:      HOL/Boogie/Tools/boogie_commands.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Isar commands to create a Boogie environment simulation.
     5 *)
     6 
     7 signature BOOGIE_COMMANDS =
     8 sig
     9   val setup: theory -> theory
    10 end
    11 
    12 structure Boogie_Commands: BOOGIE_COMMANDS =
    13 struct
    14 
    15 (* commands *)
    16 
    17 fun boogie_open ((quiet, base_name), offsets) thy =
    18   let
    19     val path = Path.explode (base_name ^ ".b2i")
    20     val _ = File.exists path orelse
    21       error ("Unable to find file " ^ quote (Path.implode path))
    22     val _ = Boogie_VCs.is_closed thy orelse
    23       error ("Found the beginning of a new Boogie environment, " ^
    24         "but another Boogie environment is still open.")
    25   in Boogie_Loader.load_b2i (not quiet) offsets path thy end
    26 
    27 
    28 datatype vc_opts =
    29   VC_Complete |
    30   VC_Take of int list * (bool * string list) option |
    31   VC_Only of string list |
    32   VC_Without of string list |
    33   VC_Examine of string list |
    34   VC_Single of string
    35 
    36 fun get_vc thy vc_name =
    37   (case Boogie_VCs.lookup thy vc_name of
    38     SOME vc => vc
    39   | NONE => 
    40       (case AList.lookup (op =) (Boogie_VCs.state_of thy) vc_name of
    41         SOME Boogie_VCs.Proved => error ("The verification condition " ^
    42           quote vc_name ^ " has already been proved.")
    43       | _ => error ("There is no verification condition " ^
    44           quote vc_name ^ ".")))
    45 
    46 local
    47   fun split_goal t =
    48     (case Boogie_Tactics.split t of
    49       [tp] => tp
    50     | _ => error "Multiple goals.")
    51 
    52   fun single_prep t =
    53     let
    54       val (us, u) = split_goal t
    55       val assms = [((@{binding vc_trace}, []), map (rpair []) us)]
    56     in
    57       pair [u] o snd o ProofContext.add_assms_i Assumption.assume_export assms
    58     end
    59 
    60   fun single_prove goal ctxt thm =
    61     Goal.prove ctxt [] [] goal (fn {context, ...} => HEADGOAL (
    62       Boogie_Tactics.split_tac
    63       THEN' Boogie_Tactics.drop_assert_at_tac
    64       THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context))
    65 in
    66 fun boogie_vc (vc_name, vc_opts) thy =
    67   let
    68     val vc = get_vc thy vc_name
    69 
    70     fun extract vc l =
    71       (case Boogie_VCs.extract vc l of
    72         SOME vc' => vc'
    73       | NONE => error ("There is no assertion to be proved with label " ^
    74           quote l ^ "."))
    75 
    76     val vcs =
    77       (case vc_opts of
    78         VC_Complete => [vc]
    79       | VC_Take (ps, NONE) => [Boogie_VCs.paths_and ps [] vc]
    80       | VC_Take (ps, SOME (true, ls)) => [Boogie_VCs.paths_and ps ls vc]
    81       | VC_Take (ps, SOME (false, ls)) => [Boogie_VCs.paths_without ps ls vc]
    82       | VC_Only ls => [Boogie_VCs.only ls vc]
    83       | VC_Without ls => [Boogie_VCs.without ls vc]
    84       | VC_Examine ls => map (extract vc) ls
    85       | VC_Single l => [extract vc l])
    86     val ts = map Boogie_VCs.prop_of_vc vcs
    87 
    88     val (prepare, finish) =
    89       (case vc_opts of
    90          VC_Single _ => (single_prep (hd ts), single_prove (hd ts))
    91       | _ => (pair ts, K I))
    92 
    93     val discharge = fold (Boogie_VCs.discharge o pair vc_name)
    94     fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
    95       | after_qed _ = I
    96   in
    97     ProofContext.init_global thy
    98     |> fold Variable.auto_fixes ts
    99     |> (fn ctxt1 => ctxt1
   100     |> prepare
   101     |-> (fn us => fn ctxt2 => ctxt2
   102     |> Proof.theorem NONE (fn thmss => fn ctxt =>
   103          let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
   104          in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
   105   end
   106 end
   107 
   108 fun write_list head =
   109   map Pretty.str o sort (dict_ord string_ord o pairself explode) #>
   110   Pretty.writeln o Pretty.big_list head
   111 
   112 fun parens s = "(" ^ s ^ ")"
   113 
   114 fun boogie_status thy =
   115   let
   116     fun string_of_state Boogie_VCs.Proved = "proved"
   117       | string_of_state Boogie_VCs.NotProved = "not proved"
   118       | string_of_state Boogie_VCs.PartiallyProved = "partially proved"
   119   in
   120     Boogie_VCs.state_of thy
   121     |> map (fn (name, proved) => name ^ " " ^ parens (string_of_state proved))
   122     |> write_list "Boogie verification conditions:"
   123   end
   124 
   125 fun boogie_status_vc full vc_name thy =
   126   let
   127     fun pretty tag s = s ^ " " ^ parens tag
   128 
   129     val (not_proved, proved) = Boogie_VCs.state_of_vc thy vc_name
   130   in
   131     if full
   132     then write_list ("Assertions of Boogie verification condition " ^
   133       quote vc_name ^ ":")
   134       (map (pretty "proved") proved @ map (pretty "not proved") not_proved)
   135     else write_list ("Unproved assertions of Boogie verification condition " ^
   136       quote vc_name ^ ":") not_proved
   137   end
   138 
   139 fun boogie_status_vc_paths full vc_name thy =
   140   let
   141     fun labels ls = Pretty.blk (0, Pretty.breaks (map Pretty.str ls))
   142 
   143     fun pp (i, ns) =
   144       if full
   145       then
   146         [Pretty.big_list ("Path " ^ string_of_int (i+1) ^ ":")
   147           [labels (map (fn (n, true) => n | (n, _) => parens n) ns)]]
   148       else
   149         let val ns' = map_filter (fn (n, true) => SOME n | _ => NONE) ns
   150         in
   151           if null ns' then []
   152           else
   153             [Pretty.big_list ("Unproved assertions of path " ^
   154               string_of_int (i+1) ^ ":") [labels ns']]
   155         end
   156   in
   157     Pretty.writeln
   158       (Pretty.big_list
   159         ("Paths of Boogie verification condition " ^ quote vc_name ^ ":")
   160         (flat (map_index pp (Boogie_VCs.path_names_of (get_vc thy vc_name)))))
   161   end
   162 
   163 
   164 local
   165   fun trying s = tracing ("Trying " ^ s ^ " ...")
   166   fun success_on s = tracing ("Succeeded on " ^ s ^ ".")
   167   fun failure_on s c = tracing ("Failed on " ^ s ^ c)
   168 
   169   fun string_of_asserts vc = space_implode ", " (fst (Boogie_VCs.names_of vc))
   170 
   171   fun string_of_path (i, n) =
   172     "path " ^ string_of_int i ^ " of " ^ string_of_int n
   173 
   174   fun itemize_paths ps =
   175     let val n = length ps
   176     in fst (fold_map (fn p => fn i => (((i, n), p), i+1)) ps 1) end
   177 
   178   fun par_map f = flat o Par_List.map f
   179 
   180   fun divide f vc =
   181     let val n = Boogie_VCs.size_of vc
   182     in
   183       if n <= 1 then fst (Boogie_VCs.names_of vc)
   184       else
   185         let val (vc1, vc2) = the (Boogie_VCs.split_path (n div 2) vc)
   186         in par_map f [vc1, vc2] end
   187     end
   188 
   189   fun prove thy meth vc =
   190     ProofContext.init_global thy
   191     |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
   192     |> Proof.apply meth
   193     |> Seq.hd
   194     |> Proof.global_done_proof
   195 in
   196 fun boogie_narrow_vc (quick, timeout) vc_name meth thy =
   197   let
   198     fun tp t = TimeLimit.timeLimit (Time.fromSeconds t) (prove thy meth)
   199 
   200     fun try_vc t (tag, split_tag) split vc = (trying tag;
   201       (case try (tp t) vc of
   202         SOME _ => (success_on tag; [])
   203       | NONE => (failure_on tag split_tag; split vc)))
   204 
   205     fun some_asserts vc =
   206       let
   207         val (t, sep) = if Boogie_VCs.size_of vc = 1 then (timeout, ".")
   208           else (quick, ", further splitting ...")
   209       in try_vc t (string_of_asserts vc, sep) (divide some_asserts) vc end
   210 
   211     fun single_path p =
   212       try_vc quick (string_of_path p, ", splitting into assertions ...")
   213         (divide some_asserts)
   214 
   215     val complete_vc =
   216       try_vc quick ("full goal", ", splitting into paths ...")
   217         (par_map (uncurry single_path) o itemize_paths o Boogie_VCs.paths_of)
   218 
   219     val unsolved = complete_vc (get_vc thy vc_name)
   220   in
   221     if null unsolved
   222     then writeln ("Completely solved Boogie verification condition " ^
   223       quote vc_name ^ ".")
   224     else write_list ("Unsolved assertions of Boogie verification condition " ^
   225       quote vc_name ^ ":") unsolved
   226   end
   227 
   228 fun boogie_scan_vc timeout vc_name meth thy =
   229   let
   230     val tp = TimeLimit.timeLimit (Time.fromSeconds timeout) (prove thy meth)
   231 
   232     val vc = get_vc thy vc_name
   233     fun prove_assert name =
   234       (trying name; tp (the (Boogie_VCs.extract vc name)))
   235     val find_first_failure = find_first (is_none o try prove_assert)
   236   in
   237     (case find_first_failure (fst (Boogie_VCs.names_of vc)) of
   238       SOME name => writeln ("failed on " ^ quote name)
   239     | NONE => writeln "succeeded")
   240   end
   241 end
   242 
   243 
   244 
   245 fun boogie_end thy =
   246   let
   247     fun not_proved (_, Boogie_VCs.Proved) = NONE
   248       | not_proved (name, _) = SOME name
   249 
   250     val unproved = map_filter not_proved (Boogie_VCs.state_of thy)
   251   in
   252     if null unproved then Boogie_VCs.close thy
   253     else error (Pretty.string_of (Pretty.big_list 
   254       "The following verification conditions have not been proved:"
   255       (map Pretty.str unproved)))
   256   end
   257 
   258 
   259 
   260 (* syntax and setup *)
   261 
   262 fun scan_val n f = Args.$$$ n -- Args.colon |-- f
   263 fun scan_arg f = Args.parens f
   264 fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n >> K true)) false
   265 
   266 val vc_offsets = Scan.optional (Args.bracks (Parse.list1
   267   (Parse.string --| Args.colon -- Parse.nat))) []
   268 
   269 val _ =
   270   Outer_Syntax.command "boogie_open"
   271     "open a new Boogie environment and load a Boogie-generated .b2i file"
   272     Keyword.thy_decl
   273     (scan_opt "quiet" -- Parse.name -- vc_offsets >> 
   274       (Toplevel.theory o boogie_open))
   275 
   276 
   277 val vc_name = Parse.name
   278 
   279 val vc_label = Parse.name
   280 val vc_labels = Scan.repeat1 vc_label
   281 
   282 val vc_paths =
   283   Parse.nat -- (Args.$$$ "-" |-- Parse.nat) >> (op upto) ||
   284   Parse.nat >> single
   285 
   286 val vc_opts =
   287   scan_arg
   288    (scan_val "assertion" vc_label >> VC_Single ||
   289     scan_val "examine" vc_labels >> VC_Examine ||
   290     scan_val "take" ((Parse.list vc_paths >> flat) -- Scan.option (
   291       scan_val "without" vc_labels >> pair false ||
   292       scan_val "and_also" vc_labels >> pair true) >> VC_Take) ||
   293     scan_val "only" vc_labels >> VC_Only ||
   294     scan_val "without" vc_labels >> VC_Without) ||
   295   Scan.succeed VC_Complete
   296 
   297 val _ =
   298   Outer_Syntax.command "boogie_vc"
   299     "enter into proof mode for a specific verification condition"
   300     Keyword.thy_goal
   301     (vc_name -- vc_opts >> (fn args =>
   302       (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
   303 
   304 
   305 val quick_timeout = 5
   306 val default_timeout = 20
   307 
   308 fun timeout name = Scan.optional (scan_val name Parse.nat)
   309 
   310 val status_test =
   311   scan_arg (
   312     Args.$$$ "scan" |-- timeout "timeout" quick_timeout >> boogie_scan_vc ||
   313     Args.$$$ "narrow" |-- timeout "step_timeout" quick_timeout --
   314       timeout "final_timeout" default_timeout >> boogie_narrow_vc) --
   315   vc_name -- Method.parse >>
   316   (fn ((f, vc_name), meth) => f vc_name meth)
   317 
   318 val status_vc =
   319   (scan_arg
   320     (Args.$$$ "full" |--
   321       (Args.$$$ "paths" >> K (boogie_status_vc_paths true) ||
   322        Scan.succeed (boogie_status_vc true)) ||
   323      Args.$$$ "paths" >> K (boogie_status_vc_paths false)) ||
   324    Scan.succeed (boogie_status_vc false)) --
   325   vc_name >> (fn (f, vc_name) => f vc_name)
   326 
   327 fun status_cmd f = Toplevel.no_timing o Toplevel.keep (fn state =>
   328   f (Toplevel.theory_of state))
   329 
   330 val _ =
   331   Outer_Syntax.improper_command "boogie_status"
   332     "show the name and state of all loaded verification conditions"
   333     Keyword.diag
   334     (status_test >> status_cmd ||
   335      status_vc >> status_cmd ||
   336      Scan.succeed (status_cmd boogie_status))
   337 
   338 
   339 val _ =
   340   Outer_Syntax.command "boogie_end"
   341     "close the current Boogie environment"
   342     Keyword.thy_decl
   343     (Scan.succeed (Toplevel.theory boogie_end))
   344 
   345 
   346 val setup = Theory.at_end (fn thy =>
   347   let
   348     val _ = Boogie_VCs.is_closed thy
   349       orelse error ("Found the end of the theory, " ^ 
   350         "but the last Boogie environment is still open.")
   351   in NONE end)
   352 
   353 end