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