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