-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcheckquery.ml
170 lines (163 loc) · 6.82 KB
/
checkquery.ml
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
open Tuple
open Query
open Printer
open Settings
open Sourcepos
open Report
open Name
open Formula
open Intfdesc
open Stability
open AskZ3
open Z3
(* This file is part of Arsenic, a proofchecker for New Lace logic.
Copyright (c) 2015 Richard Bornat.
Licensed under the MIT license (sic): see LICENCE.txt or
https://opensource.org/licenses/MIT
*)
exception Error of string
let parse_queries_from_channel in_channel =
let lexbuf = Lexing.from_channel in_channel in
try
let result = temp_setting Settings.allow_special_formulas true (fun () -> Parser.queries Lexer.make_token lexbuf) in
result
with
| Parsing.Parse_error ->
(let curr = lexbuf.Lexing.lex_curr_p in
raise (Error ("**Parse error at line "^string_of_int (curr.Lexing.pos_lnum)^
" character "^string_of_int (curr.Lexing.pos_cnum-curr.Lexing.pos_bol)^
" (just before \""^Lexing.lexeme lexbuf^"\")")))
| Program.ParseError(spos,s) ->
raise (Error ("\n**SYNTAX ERROR at "^string_of_sourcepos spos ^ " " ^ s))
| Lexer.LexError(spos,s) ->
raise (Error ("\n**LEXING ERROR at "^string_of_sourcepos spos ^ ": " ^ s))
let parse_queries_from_file filename =
let in_channel = open_in filename in
try
let result = parse_queries_from_channel in_channel in
close_in in_channel;
result
with
| exn -> (close_in in_channel; raise exn)
let check_query prefix query =
let tidyup s =
(* if !keep_log then Z3.close_log (); *)
print_string s;
flush stdout;
flush stderr
in
try
if !keep_log then
(let logname = prefix ^ ".log" in
print_newline (print_string ("opening log file " ^ logname ^ "; " ^ string_of_bool (Z3.open_log logname)))
);
Printf.printf "\nQuery is: %s\n" (string_of_query query);
let tautZ3 f fs =
match z3check_query Tautology (fun () -> "") !verbose (List.rev fs) f with
| Valid _ ->
print_string ("\nValid\n")
| Invalid (assertions, f, m) ->
if !verbose || !verbose_z3report || !z3track<>Z3trackOff then
print_string ("\nInvalid with counter-example\n" ^ m ^ "\n")
else
Printf.printf "\nInvalid\n"
| Undecided (assertions, f, m) ->
print_string ("\n**Unknown with remark " ^ m ^ "\n")
| BadQuery (f, s) ->
print_string ("\n**BadQuery " ^ s ^ "\n")
in
let show_sat = function
| Valid _ -> "Sat"
| Invalid (assertions, f, m) -> "Unsat"
| Undecided (assertions, f, m) -> "Unknown with remark " ^ m
| BadQuery (f, s) -> "BadQuery " ^ s
in
let satZ3 f fs =
z3check_query Satisfiable (fun () -> "") !verbose (List.rev fs) f
in
let rec show_query fs query =
match fs with
| [] -> explain_string_of_formula query
| f::fs -> "_assert " ^ string_of_formula f ^ ";\n" ^ show_query fs query
in
let rec do_query assertions query =
match query with
| Qassert (f,q) -> do_query (f::assertions) q
| Qtaut f -> tautZ3 f assertions
| Qsat f -> Printf.printf "\n%s\n" (show_sat (satZ3 f assertions))
| Qstableformula (p,i) ->
let scq = Stability.sc_stable_query_intfdesc p i in
Printf.printf "\nSC/INT stability\n%s\n" (show_query assertions scq);
tautZ3 scq assertions;
let extq = Stability.ext_stable_query_intfdesc p i in
Printf.printf "\nEXT stability\n%s\n" (show_query assertions extq);
tautZ3 extq assertions;
let uextq = Stability.uext_stable_query_intfdesc p i in
Printf.printf "\nUEXT stability\n%s\n" (show_query assertions uextq);
tautZ3 uextq assertions
| Qstableintf (i1,i2) ->
let boq = Stability.bo_stable_query_intfdescs i1 i2 in
Printf.printf "\nBO stability 1 against 2\n%s\n" (show_query assertions boq);
tautZ3 boq assertions;
let boq = Stability.bo_stable_query_intfdescs i2 i1 in
Printf.printf "\nBO stability 2 against 1\n%s\n" (show_query assertions boq);
tautZ3 boq assertions;
let uoq = Stability.uo_stable_query_intfdescs i1 i2 in
Printf.printf "\nUO stability 1 against 2\n%s\n" (show_query assertions uoq);
tautZ3 uoq assertions;
let uoq = Stability.uo_stable_query_intfdescs i2 i1 in
Printf.printf "\nUO stability 2 against 1\n%s\n" (show_query assertions uoq);
tautZ3 uoq assertions
| Qspimplies (p,assign,q) ->
let sp = Strongestpost.strongest_post true p assign in
let spq = _recImplies sp q in
Printf.printf "\nsp-implies assertion\n%s\n" (show_query assertions spq);
tautZ3 spq assertions
in
let start = Time.start_timer() in
do_query [] query;
Time.show_interval "total time" (Time.interval start (Time.now()));
tidyup "";
with
| Sys_error s -> tidyup ("\n\n** FATAL Sys_error \""^s^"\"")
| Error s | Formula.Error s -> tidyup ("\n\n" ^ s)
| AskZ3.Crash s -> tidyup ("\n\n** CRASH: " ^ s)
| Z3.Error(_,code) -> tidyup ("\n\n** Z3 error: " ^ Z3utils.string_of_Z3error_code code)
| Report.Exit -> tidyup ("")
| Invalid_argument s -> tidyup ("\n\n** Invalid argument: " ^s)
| exn -> tidyup ("\n\n** Unexpected exception " ^ Printexc.to_string exn)
let checkfile filename =
AskZ3.z3_querycount:=0;
AskZ3.triv_querycount:=0;
AskZ3.invalid_querycount:=0;
AskZ3.unsat_querycount:=0;
AskZ3.undef_querycount:=0;
errorcount:=0;
undecidedcount:=0;
warningcount:=0;
print_newline (print_string ("\nprocessing " ^ filename));
let basename = Filename.basename filename in
let prefix =
try Filename.chop_extension basename with _ -> basename
in
List.iter (check_query prefix) (parse_queries_from_file filename);
let showvar name vref =
if !vref=0 then ""
else
Printf.sprintf "%s %d"
name !vref
in
let results = [showvar "Z3 queries" AskZ3.z3_querycount;
showvar "trivial queries" AskZ3.triv_querycount;
showvar "invalid queries" AskZ3.invalid_querycount;
showvar "unsats" AskZ3.unsat_querycount;
showvar "undefs" AskZ3.undef_querycount;
showvar "errors" errorcount;
showvar "undecided" undecidedcount;
showvar "warnings" warningcount
]
in
Printf.printf "\n%s\n" (String.concat ", " (List.filter (fun s -> String.length s <> 0) results))
let _ = match !Usage.files with
| [] -> List.iter (check_query "stdin") (parse_queries_from_channel stdin)
| fs -> List.iter checkfile (List.rev fs)