1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
|
(**************************************************************************)
(* *)
(* The Why platform for program certification *)
(* Copyright (C) 2002-2008 *)
(* Romain BARDOU *)
(* Jean-Franois COUCHOT *)
(* Mehdi DOGGUY *)
(* Jean-Christophe FILLITRE *)
(* Thierry HUBERT *)
(* Claude MARCH *)
(* Yannick MOY *)
(* Christine PAULIN *)
(* Yann RGIS-GIANAS *)
(* Nicolas ROUSSET *)
(* Xavier URBAIN *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU General Public *)
(* License version 2, as published by the Free Software Foundation. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(* See the GNU General Public License version 2 for more details *)
(* (enclosed in the file GPL). *)
(* *)
(**************************************************************************)
(*i $Id: calldp.ml,v 1.46 2008/02/12 13:41:29 marche Exp $ i*)
open Printf
open Options
type prover_result =
| Valid of float
| Invalid of float * string option
| CannotDecide of float * string option
| Timeout of float
| ProverFailure of float * string
let remove_file ?(debug=false) f =
if not debug then try Sys.remove f with _ -> ()
let file_contents f =
let buf = Buffer.create 1024 in
try
let c = open_in f in
begin try
while true do
let s = input_line c in Buffer.add_string buf s;
Buffer.add_char buf '\n'
done;
assert false
with End_of_file ->
close_in c;
Buffer.contents buf
end
with _ ->
sprintf "(cannot open %s)" f
let timed_sys_command ~debug timeout cmd =
let t0 = Unix.times () in
if debug then Format.eprintf "command line: %s@." cmd;
let out = Filename.temp_file "out" "" in
let cmd = sprintf "cpulimit %d %s > %s 2>&1" timeout cmd out in
let ret = Sys.command cmd in
let t1 = Unix.times () in
let cpu_time = t1.Unix.tms_cutime -. t0.Unix.tms_cutime in
if debug then Format.eprintf "Output file %s:@.%s@." out (file_contents out);
(cpu_time,ret,out)
let error c t cmd =
if c = 152 then Timeout t
else ProverFailure (t,"command failed: " ^ cmd)
let cvcl ?(debug=false) ?(timeout=10) ~filename:f () =
let cmd = sprintf "cvcl < %s" f in
let t,c,out = timed_sys_command debug timeout cmd in
if c <> 0 then error c t cmd
else if Sys.command (sprintf "grep -q -w -i Error %s" out) = 0 then
ProverFailure(t,"command failed: " ^ cmd ^ "\n" ^ file_contents out)
else
let r=
let c = Sys.command (sprintf "grep -q -w Valid %s" out) in
if c = 0 then Valid t
else
let c = Sys.command (sprintf "grep -q -w Unknown %s" out) in
if c = 0 then
CannotDecide(t,Some (file_contents out))
else
Invalid (t, Some (file_contents out))
in
remove_file ~debug out;
r
let simplify ?(debug=false) ?(timeout=10) ~filename:f () =
let cmd = sprintf "Simplify %s" f in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then error c t cmd
else
let r =
if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then
Valid t
else
if Sys.command (sprintf "grep -q -w Invalid %s" out) = 0 then
CannotDecide (t,Some (file_contents out))
else
ProverFailure(t,"command failed: " ^ cmd ^ "\n" ^ file_contents out)
in
remove_file ~debug out;
r
(**
Graph is an interface which aims at recursively calling
the hypotheses_filtering module if needed.
@param timeout is the global timeout for the proof
@param f : is the name of the input file which contains the proof obligation
For the moment, the proof obligation is stored as a why file.
The first part try to check whether the formula f is valid by
discharging it into simplify in a timeout set to timeout/4.
The function exits when the result is valid, unknown or not valid.
Otherwise, the function enters in a second step.
The hypotheses_filtering module is
called with with a depth that increases, provided
the result returned by the prover is not_valid or unknown.
Face to a timeout result, the prover is called again with the same PO but
with a longer timeout.
**)
let graph ?(debug=false) ?(timeout=10) ~filename:f () =
let pruning_hyp = 3 in
let last_dot_index = String.rindex f '.' in
let f_for_simplify = (String.sub f 0 last_dot_index) ^ "_why.sx" in
let cmd = sprintf "why --simplify --no-prelude %s " f in
let t'=
(float_of_int timeout) /. (float_of_int (pruning_hyp +1)) in
let t'',c,out = timed_sys_command ~debug (int_of_float t') cmd in
let cmd = sprintf "Simplify %s" f_for_simplify in
let t'',c,out = timed_sys_command ~debug (int_of_float (t' -. t'')) cmd in
let result_sort t'' out =
if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then
Valid t''
else
if Sys.command (sprintf "grep -q -w Invalid %s" out) = 0 then
CannotDecide (t'',Some (file_contents out))
else
ProverFailure
(t'',"command failed: " ^ cmd ^ "\n" ^ file_contents out) in
if c == 0 then
let r = result_sort t'' out in
remove_file ~debug out;
r
else
let t = ref 0.0 in
let c = ref 0 in
let vb = ref 0 in
let pb = ref 1 in
let explicitRes = ref true in
let r = ref (Valid 0.0) in
while ( !c == 0 && !explicitRes && !t < float_of_int timeout)
(**** UPDATE THIS WITH A LOOP OVER PB AS DONE IN THE ARTICLE CouchotHubert07**)
do
(* compute the new proof obligation *)
let cmd = sprintf "why --simplify --no-prelude --prune-hyp %d %d %s " !pb !vb f in
let t'',c',out = timed_sys_command ~debug (int_of_float t') cmd in
let cmd = sprintf "Simplify %s" f_for_simplify in
let t'',c',out = timed_sys_command ~debug (int_of_float (t' -. t'')) cmd in
t := !t +. t'';
c := c';
r := result_sort t'' out ;
vb := !vb+1 ;
explicitRes := match !r with
Valid _ | Timeout _ | ProverFailure _ -> false
| Invalid _ | CannotDecide _ -> true ;
done;
let res =
if !t >= float_of_int timeout then
error !c (float_of_int timeout) cmd
else
if !c != 0 then
error !c (float_of_int timeout) cmd
else
!r in
res
let rvsat ?(debug=false) ?(timeout=10) ~filename:f () =
(*let cmd = sprintf "rv-sat %s" f in*)
let cmd = sprintf "rv-sat %s" f in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then error c t cmd
else
let r =
if Sys.command (sprintf "grep -q -w unsat %s" out) = 0 then
Valid t
else
if Sys.command (sprintf "grep -q -w sat %s" out) = 0 then
Invalid (t, None)
else
ProverFailure(t,"command failed: " ^ cmd)
in
(*remove_file ~debug out;*)
r
let yices ?(debug=false) ?(timeout=30) ~filename:f () =
let cmd = sprintf "yices -pc 0 -smt < %s" f in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then
if c==1 &&
Sys.command (sprintf "grep -q -w 'feature not supported' %s" out) = 0 then
ProverFailure(t,"command failed: " ^ cmd)
else
error c t cmd
else
let r =
if Sys.command (sprintf "grep -q -w unsat %s" out) = 0 then
Valid t
else
if Sys.command (sprintf "grep -q -w unknown %s" out) = 0 then
CannotDecide (t, None)
else
ProverFailure(t,"command failed: " ^ cmd)
in
remove_file ~debug out;
r
let cvc3 ?(debug=false) ?(timeout=30) ~filename:f () =
let cmd =
sprintf "cvc3 +arith-new +quant-polarity -quant-new -lang smt < %s" f
in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then
if c==1 &&
Sys.command (sprintf "grep -q -w 'feature not supported' %s" out) = 0 then
ProverFailure(t,"command failed: " ^ cmd)
else
error c t cmd
else
let r =
if Sys.command (sprintf "grep -q -w unsat %s" out) = 0 then
Valid t
else if Sys.command (sprintf "grep -q -w sat %s" out) = 0 then
CannotDecide (t, None)
else if Sys.command (sprintf "grep -q -w unknown %s" out) = 0 then
CannotDecide (t, None)
else
ProverFailure(t,"command failed: " ^ cmd)
in
remove_file ~debug out;
r
let z3 ?(debug=false) ?(timeout=30) ~filename:f () =
let cmd = sprintf "z3 -smt %s" f in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then
if c==1 &&
Sys.command (sprintf "grep -q -w 'feature not supported' %s" out) = 0 then
ProverFailure(t,"command failed: " ^ cmd)
else
error c t cmd
else
let r =
if Sys.command (sprintf "grep -q -w unsat %s" out) = 0 then
Valid t
else
if Sys.command (sprintf "grep -q -w unknown %s" out) = 0 then
CannotDecide (t, None)
else
ProverFailure(t,"command failed: " ^ cmd)
in
remove_file ~debug out;
r
let harvey ?(debug=false) ?(timeout=10) ~filename:f () =
let cmd = sprintf "rvc %s" f in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then (error c t cmd)
else begin
let f = Filename.chop_suffix f ".rv" in
let fi = f ^ "-0" ^ ".baf" in
let cmd = sprintf "rv %s" fi in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then (error c t cmd)
else
let r =
if Sys.command
(sprintf "grep -q -w \"is valid\" %s " out) = 0 then
Valid t
else
if Sys.command
(sprintf "grep -q -w \"cannot be decided\" %s " out) = 0
then
CannotDecide (t, None)
else
ProverFailure(t,"command failed: " ^ cmd)
in
remove_file ~debug out;
r
end
let ergo ?(debug=false) ?(timeout=10) ~filename:f () =
let cmd = sprintf "ergo %s" f in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then error c t cmd
else
let r =
if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then
Valid t
else if Sys.command (sprintf "grep -q -w \"I don't know\" %s" out) = 0
then
CannotDecide (t, None)
else if Sys.command (sprintf "grep -q -w \"Invalid\" %s" out) = 0
then
(* ergo 0.6 never really say 'invalid' *)
CannotDecide (t,None)
else
ProverFailure(t,"command failed: " ^ cmd)
in
remove_file ~debug out;
r
let zenon ?(debug=false) ?(timeout=10) ~filename:f () =
let cmd = sprintf "zenon %s" f in
let t,c,out = timed_sys_command ~debug timeout cmd in
if c <> 0 then error c t cmd
else
let r =
if Sys.command (sprintf "grep -q PROOF-FOUND %s" out) = 0 then
Valid t
else
ProverFailure(t,"command failed: " ^ cmd)
in
remove_file ~debug out;
r
|
