cprover
parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "parse_options.h"
10 
11 #include <algorithm>
12 #include <cctype>
13 #include <climits>
14 #include <iostream>
15 
16 #if defined (_WIN32)
17 #define EX_OK 0
18 #define EX_USAGE 1
19 #else
20 #include <sysexits.h>
21 #endif
22 
23 #include "cmdline.h"
24 #include "exception_utils.h"
25 #include "exit_codes.h"
26 #include "signal_catcher.h"
27 #include "string_utils.h"
28 
30  const std::string &_optstring,
31  int argc,
32  const char **argv,
33  const std::string &program)
34  : parse_result(cmdline.parse(
35  argc,
36  argv,
37  (std::string("?h(help)") + _optstring).c_str())),
38  ui_message_handler(cmdline, program),
39  log(ui_message_handler)
40 {
41 }
42 
44 {
45 }
46 
48 {
49  log.error() << "Usage error!\n" << messaget::eom;
50  help();
51 }
52 
56 {
57  if(!cmdline.unknown_arg.empty())
58  {
59  log.error() << "Unknown option: " << cmdline.unknown_arg;
60  auto const suggestions =
62  if(!suggestions.empty())
63  {
64  log.error() << ", did you mean ";
65  if(suggestions.size() > 1)
66  {
67  log.error() << "one of ";
68  }
69  join_strings(log.error(), suggestions.begin(), suggestions.end(), ", ");
70  log.error() << "?";
71  }
72  log.error() << messaget::eom;
73  }
74 }
75 
77 {
78  // catch all exceptions here so that this code is not duplicated
79  // for each tool
80  try
81  {
82  if(parse_result)
83  {
84  usage_error();
86  return EX_USAGE;
87  }
88 
89  if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help"))
90  {
91  help();
92  return EX_OK;
93  }
94 
95  // install signal catcher
97 
98  return doit();
99  }
100 
101  // CPROVER style exceptions in order of decreasing happiness
103  {
104  log.error() << e.what() << messaget::eom;
106  }
107  catch(const cprover_exception_baset &e)
108  {
109  log.error() << e.what() << messaget::eom;
110  return CPROVER_EXIT_EXCEPTION;
111  }
112  catch(const std::string &e)
113  {
114  log.error() << "C++ string exception : " << e << messaget::eom;
115  return CPROVER_EXIT_EXCEPTION;
116  }
117  catch(const char *e)
118  {
119  log.error() << "C string exception : " << e << messaget::eom;
120  return CPROVER_EXIT_EXCEPTION;
121  }
122  catch(int e)
123  {
124  log.error() << "Numeric exception : " << e << messaget::eom;
125  return CPROVER_EXIT_EXCEPTION;
126  }
127  // C++ style exceptions
128  catch(const std::bad_alloc &)
129  {
130  log.error() << "Out of memory" << messaget::eom;
132  }
133  catch(const std::exception &e)
134  {
135  log.error() << e.what() << messaget::eom;
136  return CPROVER_EXIT_EXCEPTION;
137  }
138  catch(const invariant_failedt &e)
139  {
140  log.error() << e.what() << messaget::eom;
141  return CPROVER_EXIT_EXCEPTION;
142  }
143  catch(...)
144  {
145  log.error() << "Unknown exception type!" << messaget::eom;
146  return CPROVER_EXIT_EXCEPTION;
147  }
148 }
149 
150 std::string align_center_with_border(const std::string &text)
151 {
152  auto const total_length = std::size_t{63};
153  auto const border = std::string{"* *"};
154  auto const fill =
155  total_length - std::min(total_length, 2 * border.size() + text.size());
156  auto const fill_right = fill / 2;
157  auto const fill_left = fill - fill_right;
158  return border + std::string(fill_left, ' ') + text +
159  std::string(fill_right, ' ') + border;
160 }
161 
162 std::string
163 banner_string(const std::string &front_end, const std::string &version)
164 {
165  const std::string version_str = front_end + " " + version + " " +
166  std::to_string(sizeof(void *) * CHAR_BIT) +
167  "-bit";
168 
169  return align_center_with_border(version_str);
170 }
171 
172 std::string help_entry(
173  const std::string &option,
174  const std::string &description,
175  const std::size_t left_margin,
176  const std::size_t width)
177 {
178  PRECONDITION(!option.empty());
179  PRECONDITION(!std::isspace(option.front()));
180  PRECONDITION(!std::isspace(option.back()));
181  PRECONDITION(option.length() <= width);
182 
183  PRECONDITION(!description.empty());
184  PRECONDITION(!std::isspace(description.front()));
185  PRECONDITION(!std::isspace(description.back()));
186 
187  PRECONDITION(left_margin < width);
188 
189  std::string result;
190 
191  if(option.length() >= left_margin - 1)
192  {
193  result = " " + option + "\n";
194  result += wrap_line(description, left_margin, width) + "\n";
195 
196  return result;
197  }
198 
199  std::string padding(left_margin - option.length() - 1, ' ');
200  result = " " + option + padding;
201 
202  if(description.length() <= (width - left_margin))
203  {
204  return result + description + "\n";
205  }
206 
207  auto it = description.cbegin() + (width - left_margin);
208  auto rit = std::reverse_iterator<decltype(it)>(it) - 1;
209 
210  auto rit_space = std::find(rit, description.crend(), ' ');
211  auto it_space = rit_space.base() - 1;
212  CHECK_RETURN(*it_space == ' ');
213 
214  result.append(description.cbegin(), it_space);
215  result.append("\n");
216 
217  result +=
218  wrap_line(it_space + 1, description.cend(), left_margin, width) + "\n";
219 
220  return result;
221 }
exception_utils.h
wrap_line
std::string wrap_line(const std::string &line, const std::size_t left_margin, const std::size_t width)
Wrap line at spaces to not extend past the right margin, and include given padding with spaces to the...
Definition: string_utils.cpp:185
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
parse_options_baset::unknown_option_msg
void unknown_option_msg()
Print an error message mentioning the option that was not recognized when parsing the command line.
Definition: parse_options.cpp:55
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:52
invariant_failedt
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:111
CPROVER_EXIT_EXCEPTION
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:41
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:47
invalid_command_line_argument_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: exception_utils.cpp:12
messaget::error
mstreamt & error() const
Definition: message.h:399
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
join_strings
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:64
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
cprover_exception_baset::what
virtual std::string what() const =0
A human readable description of what went wrong.
cmdlinet::unknown_arg
std::string unknown_arg
Definition: cmdline.h:92
parse_options.h
help_entry
std::string help_entry(const std::string &option, const std::string &description, const std::size_t left_margin, const std::size_t width)
Definition: parse_options.cpp:172
parse_options_baset::main
virtual int main()
Definition: parse_options.cpp:76
parse_options_baset::parse_options_baset
parse_options_baset(const std::string &optstring, int argc, const char **argv, const std::string &program)
Definition: parse_options.cpp:29
parse_options_baset::log
messaget log
Definition: parse_options.h:43
install_signal_catcher
void install_signal_catcher()
Definition: signal_catcher.cpp:40
cmdline.h
parse_options_baset::doit
virtual int doit()=0
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
invariant_failedt::what
virtual std::string what() const noexcept
Definition: invariant.cpp:156
signal_catcher.h
parse_options_baset::help
virtual void help()
Definition: parse_options.cpp:43
cmdlinet::get_argument_suggestions
std::vector< std::string > get_argument_suggestions(const std::string &unknown_argument)
Definition: cmdline.cpp:255
parse_options_baset::parse_result
bool parse_result
Definition: parse_options.h:39
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:150
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition: exception_utils.h:25