blob: 85c3ef6a12dc432c7017c1b925bdf9902a78bde7 (
plain)
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
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
open Ast
open Format
open Builtin
open VeritPrinter
let _ = Printexc.record_backtrace true
(* Captures the output and exit status of a unix command : aux func *)
let syscall cmd =
let ic, oc = Unix.open_process cmd in
let buf = Buffer.create 16 in
(try
while true do
Buffer.add_channel buf ic 1
done
with End_of_file -> ());
ignore(Unix.close_process (ic, oc));
Buffer.contents buf
(* Set width of pretty printing boxes to number of columns *)
let vt_width =
try
let scol = syscall "tput cols" in
let w = int_of_string (String.trim scol) in
set_margin w;
w
with Not_found | Failure _ -> 80
let _ =
pp_set_margin std_formatter vt_width;
pp_set_margin err_formatter vt_width;
set_max_indent (get_margin () / 3)
module C = Converter.Make (VeritPrinter)
(* Hard coded signatures *)
let signatures =
let sigdir = try Sys.getenv "LFSCSIGS" with Not_found -> Sys.getcwd () in
["sat.plf";
"smt.plf";
"th_base.plf";
"th_int.plf";
"th_bv.plf";
"th_bv_bitblast.plf";
"th_bv_rewrites.plf";
"th_arrays.plf" ]
|> List.map (Filename.concat sigdir)
let process_signatures () =
try
List.iter (fun f ->
let chan = open_in f in
let lexbuf = Lexing.from_channel chan in
LfscParser.ignore_commands LfscLexer.main lexbuf;
close_in chan
) signatures
with
| Ast.TypingError (t1, t2) ->
eprintf "@[<hov>LFSC typing error: expected %a, got %a@]@."
Ast.print_term t1
Ast.print_term t2
(** Translate to veriT proof format and print pretty LFSC proof with colors *)
let pretty_to_verit () =
process_signatures ();
let chan =
try
let filename = Sys.argv.(1) in
open_in filename
with Invalid_argument _ -> stdin
in
let buf = Lexing.from_channel chan in
try
let proof = LfscParser.proof LfscLexer.main buf in
printf "LFSC proof:\n\n%a\n\n@." print_proof proof;
printf "Verit proof:\n@.";
match List.rev proof with
| Check p :: _ ->
flatten_term p;
C.convert_pt p |> ignore
| _ -> eprintf "No proof@."; exit 1
with Ast.TypingError (t1, t2) ->
eprintf "@[<hov>Typing error: expected %a, got %a@]@."
Ast.print_term t1
Ast.print_term t2
(** Translate to veriT proof format *)
let to_verit () =
process_signatures ();
let chan =
try
let filename = Sys.argv.(1) in
open_in filename
with Invalid_argument _ -> stdin
in
let buf = Lexing.from_channel chan in
eprintf "Type-checking LFSC proof.@.";
try
match LfscParser.last_command LfscLexer.main buf with
| Some (Check p) ->
(* eprintf "Flattening pointer structures...@."; *)
(* flatten_term p; *)
(* eprintf "Done (flatten)@."; *)
C.convert_pt p |> ignore
| _ -> eprintf "No proof@."; exit 1
with
| Ast.TypingError (t1, t2) as e ->
let backtrace = Printexc.get_backtrace () in
eprintf "Fatal error: %s@." (Printexc.to_string e);
eprintf "Backtrace:@\n%s@." backtrace;
eprintf "@[<hov>Typing error: expected %a, got %a@]@."
Ast.print_term t1
Ast.print_term t2
| Ast.CVC4Sat ->
eprintf "CVC4 returned SAT@."; exit 1
let _ = to_verit ()
(*
Local Variables:
compile-command: "make"
indent-tabs-mode: nil
End:
*)
|
