Skip to content

Commit 1039255

Browse files
kroeningkroening
committed
new help formatter and console API
This commit adds a new help formatter, which supports a limited form of markup to visually distinguish different syntactic elements of the command line arguments. Rendering of the syntax highlighting is done via a new console API.
1 parent b08632a commit 1039255

10 files changed

+344
-10
lines changed

Diff for: ‎src/cprover/Makefile

-2
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@ SRC = address_taken.cpp \
22
axioms.cpp \
33
bv_pointers_wide.cpp \
44
c_safety_checks.cpp \
5-
console.cpp \
65
cprover_main.cpp \
76
cprover_parse_options.cpp \
87
counterexample_found.cpp \
@@ -13,7 +12,6 @@ SRC = address_taken.cpp \
1312
format_hooks.cpp \
1413
free_symbols.cpp \
1514
generalization.cpp \
16-
help_formatter.cpp \
1715
inductiveness.cpp \
1816
instrument_contracts.cpp \
1917
instrument_given_invariants.cpp \

Diff for: ‎src/cprover/cprover_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/config.h>
1515
#include <util/cout_message.h>
1616
#include <util/exit_codes.h>
17+
#include <util/help_formatter.h>
1718
#include <util/options.h>
1819
#include <util/signal_catcher.h>
1920
#include <util/ui_message.h>
@@ -35,7 +36,6 @@ Author: Daniel Kroening, [email protected]
3536

3637
#include "c_safety_checks.h"
3738
#include "format_hooks.h"
38-
#include "help_formatter.h"
3939
#include "instrument_contracts.h"
4040
#include "instrument_given_invariants.h"
4141
#include "state_encoding.h"

Diff for: ‎src/cprover/report_properties.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "report_properties.h"
1313

1414
#include <util/cout_message.h>
15-
16-
#include "console.h"
15+
#include <util/console.h>
1716

1817
#include <iomanip>
1918

Diff for: ‎src/cprover/report_traces.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ Author: Daniel Kroening, [email protected]
1212
#include "report_traces.h"
1313

1414
#include <util/format_expr.h>
15+
#include <util/console.h>
1516

16-
#include "console.h"
1717
#include "state.h"
1818

1919
#include <iomanip>

Diff for: ‎src/cprover/solver.cpp

+3-1
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,14 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "solver.h"
1313

14+
#include <util/console.h>
1415
#include <util/cout_message.h>
1516
#include <util/format_expr.h>
1617
#include <util/std_expr.h>
1718

1819
#include "address_taken.h"
19-
#include "console.h"
20+
#include "axioms.h"
21+
#include "bv_pointers_wide.h"
2022
#include "counterexample_found.h"
2123
#include "generalization.h"
2224
#include "inductiveness.h"

Diff for: ‎src/util/Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ SRC = arith_tools.cpp \
88
c_types.cpp \
99
cmdline.cpp \
1010
config.cpp \
11+
console.cpp \
1112
cout_message.cpp \
1213
dstring.cpp \
1314
endianness_map.cpp \
@@ -28,6 +29,7 @@ SRC = arith_tools.cpp \
2829
fresh_symbol.cpp \
2930
get_base_name.cpp \
3031
get_module.cpp \
32+
help_formatter.cpp \
3133
identifier.cpp \
3234
ieee_float.cpp \
3335
interval_union.cpp \

Diff for: ‎src/util/console.cpp

+242
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,242 @@
1+
/*******************************************************************\
2+
3+
Module: Console
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "console.h"
10+
11+
#include <cctype>
12+
#include <iostream>
13+
#include <sstream>
14+
15+
#ifdef _WIN32
16+
# include <io.h>
17+
# include <windows.h>
18+
# define isatty _isatty
19+
#else
20+
# include <unistd.h>
21+
#endif
22+
23+
#include <util/run.h>
24+
#include <util/string_utils.h>
25+
#include <util/unicode.h>
26+
27+
#ifdef _WIN32
28+
class windows_coutt : public std::streambuf
29+
{
30+
public:
31+
// this turns UTF8 into Windows UTF16
32+
std::streamsize xsputn(const char_type *s, std::streamsize n) override
33+
{
34+
if(consolet::is_terminal())
35+
{
36+
auto wide_string = widen(std::string(s, n));
37+
DWORD number_written;
38+
HANDLE h = GetStdHandle(STD_OUTPUT_HANDLE);
39+
WriteConsoleW(
40+
h,
41+
wide_string.c_str(),
42+
(DWORD)wide_string.size(),
43+
&number_written,
44+
nullptr);
45+
}
46+
else
47+
{
48+
std::cout.write(s, n);
49+
}
50+
51+
return n;
52+
}
53+
54+
int_type overflow(int_type c) override
55+
{
56+
if(consolet::is_terminal())
57+
std::wcout << wchar_t(c);
58+
else
59+
std::cout << char(c);
60+
return wchar_t(c);
61+
}
62+
} windows_cout;
63+
#endif
64+
65+
bool consolet::_is_terminal = false;
66+
bool consolet::_use_SGR = false;
67+
bool consolet::_init_done = false;
68+
bool consolet::_width_is_set = false;
69+
std::size_t consolet::_width;
70+
std::ostream *consolet::_out = nullptr;
71+
std::ostream *consolet::_err = nullptr;
72+
73+
void consolet::init()
74+
{
75+
if(_init_done)
76+
return;
77+
78+
_init_done = true;
79+
_is_terminal = isatty(1);
80+
81+
_out = &std::cout;
82+
_err = &std::cerr;
83+
84+
#ifdef _WIN32
85+
if(_is_terminal)
86+
{
87+
HANDLE out_handle = GetStdHandle(STD_OUTPUT_HANDLE);
88+
89+
DWORD consoleMode;
90+
if(GetConsoleMode(out_handle, &consoleMode))
91+
{
92+
consoleMode |= ENABLE_VIRTUAL_TERMINAL_PROCESSING;
93+
if(SetConsoleMode(out_handle, consoleMode))
94+
_use_SGR = true;
95+
}
96+
97+
std::cout.rdbuf(&windows_cout);
98+
}
99+
#else
100+
_use_SGR = true;
101+
#endif
102+
}
103+
104+
std::ostream &consolet::blue(std::ostream &str)
105+
{
106+
if(is_terminal() && use_SGR())
107+
return str << "\x1b[34m";
108+
else
109+
return str;
110+
}
111+
112+
std::ostream &consolet::cyan(std::ostream &str)
113+
{
114+
if(is_terminal() && use_SGR())
115+
return str << "\x1b[36m";
116+
else
117+
return str;
118+
}
119+
120+
std::ostream &consolet::green(std::ostream &str)
121+
{
122+
if(is_terminal() && use_SGR())
123+
return str << "\x1b[32m";
124+
else
125+
return str;
126+
}
127+
128+
std::ostream &consolet::red(std::ostream &str)
129+
{
130+
if(is_terminal() && use_SGR())
131+
return str << "\x1b[31m";
132+
else
133+
return str;
134+
}
135+
136+
std::ostream &consolet::yellow(std::ostream &str)
137+
{
138+
if(is_terminal() && use_SGR())
139+
return str << "\x1b[33m";
140+
else
141+
return str;
142+
}
143+
144+
std::ostream &consolet::orange(std::ostream &str)
145+
{
146+
if(is_terminal() && use_SGR())
147+
return str << "\x1b[38;5;214m";
148+
else
149+
return str;
150+
}
151+
152+
std::ostream &consolet::bold(std::ostream &str)
153+
{
154+
if(is_terminal() && use_SGR())
155+
return str << "\x1b[1m";
156+
else
157+
return str;
158+
}
159+
160+
std::ostream &consolet::faint(std::ostream &str)
161+
{
162+
if(is_terminal() && use_SGR())
163+
return str << "\x1b[2m";
164+
else
165+
return str;
166+
}
167+
168+
std::ostream &consolet::underline(std::ostream &str)
169+
{
170+
if(is_terminal() && use_SGR())
171+
return str << "\x1b[4m";
172+
else
173+
return str;
174+
}
175+
176+
std::ostream &consolet::reset(std::ostream &str)
177+
{
178+
if(is_terminal() && use_SGR())
179+
return str << "\x1b[m";
180+
else
181+
return str;
182+
}
183+
184+
std::size_t consolet::width()
185+
{
186+
if(_width_is_set)
187+
return _width;
188+
189+
_width_is_set = true;
190+
_width = 80; // default
191+
192+
if(is_terminal())
193+
{
194+
#ifdef _WIN32
195+
HANDLE h = GetStdHandle(STD_OUTPUT_HANDLE);
196+
CONSOLE_SCREEN_BUFFER_INFO info;
197+
GetConsoleScreenBufferInfo(h, &info);
198+
_width = info.srWindow.Right - info.srWindow.Left + 1;
199+
#else
200+
std::ostringstream width_stream;
201+
run("stty", {"stty", "size"}, "", width_stream, "");
202+
auto stty_output = split_string(width_stream.str(), ' ');
203+
if(
204+
stty_output.size() >= 1 && !stty_output[1].empty() &&
205+
isdigit(stty_output[1][0]))
206+
{
207+
auto width_l = atol(stty_output[1].c_str());
208+
if(width_l >= 10 && width_l <= 400)
209+
_width = width_l;
210+
}
211+
#endif
212+
}
213+
214+
return _width;
215+
}
216+
217+
extern "C" int mk_wcwidth(wchar_t ucs);
218+
219+
int consolet::wcwidth(wchar_t ucs)
220+
{
221+
return mk_wcwidth(ucs);
222+
}
223+
224+
consolet::redirectt::redirectt(
225+
std::ostream &__console_out,
226+
std::ostream &__console_err)
227+
{
228+
consolet::init();
229+
old_out = consolet::_out;
230+
old_err = consolet::_err;
231+
old_is_terminal = consolet::_is_terminal;
232+
consolet::_out = &__console_out;
233+
consolet::_err = &__console_err;
234+
consolet::_is_terminal = false;
235+
}
236+
237+
consolet::redirectt::~redirectt()
238+
{
239+
consolet::_out = old_out;
240+
consolet::_err = old_err;
241+
consolet::_is_terminal = old_is_terminal;
242+
}

0 commit comments

Comments
 (0)