CBMC
Loading...
Searching...
No Matches
cprover_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: CPROVER Command Line Option Processing
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
13
14#include <util/config.h>
15#include <util/cout_message.h>
16#include <util/exit_codes.h>
17#include <util/help_formatter.h>
18#include <util/options.h>
19#include <util/parse_options.h>
20#include <util/signal_catcher.h>
21#include <util/ui_message.h>
22#include <util/unicode.h>
23#include <util/version.h>
24
32
34#include <ansi-c/gcc_version.h>
35#include <langapi/mode.h>
36
37#include "c_safety_checks.h"
38#include "format_hooks.h"
41#include "state_encoding.h"
42
43#include <fstream> // IWYU pragma: keep
44#include <iostream>
45
46static void show_goto_functions(const goto_modelt &goto_model)
47{
48 // sort alphabetically
49 const auto sorted = goto_model.goto_functions.sorted();
50
51 const namespacet ns(goto_model.symbol_table);
52 for(const auto &fun : sorted)
53 {
54 const symbolt &symbol = ns.lookup(fun->first);
55 const bool has_body = fun->second.body_available();
56
57 if(has_body)
58 {
59 std::cout << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
60
61 std::cout << symbol.display_name() << " /* " << symbol.name << " */\n";
62 fun->second.body.output(std::cout);
63 }
64 }
65}
66
67static void show_functions_with_loops(const goto_modelt &goto_model)
68{
69 // sort alphabetically
70 const auto sorted = goto_model.goto_functions.sorted();
71
72 const namespacet ns(goto_model.symbol_table);
73 for(const auto &fun : sorted)
74 {
75 const symbolt &symbol = ns.lookup(fun->first);
76
77 if(symbol.is_file_local)
78 continue;
79
80 bool has_loop = false;
81 for(auto &instruction : fun->second.body.instructions)
82 if(instruction.is_backwards_goto())
83 has_loop = true;
84
85 if(has_loop)
86 std::cout << symbol.display_name() << '\n';
87 }
88}
89
91{
92 try
93 {
95
96 cmdlinet cmdline;
97
98 if(cmdline.parse(argc, argv, CPROVER_OPTIONS))
99 {
100 std::cerr << "Usage error!" << '\n';
102 }
103
104 if(cmdline.isset("version"))
105 {
106 std::cout << CBMC_VERSION << '\n';
108 }
109
110 if(cmdline.isset('?') || cmdline.isset("help") || cmdline.isset('h'))
111 {
112 help();
114 }
115
117 format_hooks();
118
119 if(cmdline.args.empty())
120 {
121 std::cerr << "Please provide a program to verify\n";
123 }
124
125 config.set(cmdline);
126
127 // configure gcc, if required
129 {
130 gcc_versiont gcc_version;
131 gcc_version.get("gcc");
132 configure_gcc(gcc_version);
133 }
134
135 console_message_handlert message_handler;
137
138 if(cmdline.isset("verbose"))
139 message_handler.set_verbosity(messaget::M_PROGRESS);
140 else
141 message_handler.set_verbosity(messaget::M_STATUS);
142
143 optionst options;
144 auto goto_model =
145 initialize_goto_model(cmdline.args, message_handler, options);
146
148 cmdline.isset("verbose")
149 ? static_cast<message_handlert &>(message_handler)
150 : static_cast<message_handlert &>(null_message_handler);
151
154
155 adjust_float_expressions(goto_model);
156 instrument_given_invariants(goto_model);
157
158 bool perform_inlining;
159
160 if(cmdline.isset("smt2"))
161 {
162 perform_inlining = !cmdline.isset("no-inline");
163 }
164 else
165 {
166 perform_inlining = cmdline.isset("inline");
167 }
168
170 instrument_contracts(goto_model);
171
172 if(!cmdline.isset("no-safety"))
173 c_safety_checks(goto_model);
174
175 if(cmdline.isset("no-assertions"))
176 no_assertions(goto_model);
177
178 label_properties(goto_model);
179
180 // bool perform_inlining = false;
181 bool variable_encoding = cmdline.isset("variables");
182
184 {
185 std::cout << "Performing inlining\n";
186 goto_inline(goto_model, message_handler, false);
187 }
188
189 goto_model.goto_functions.compute_target_numbers();
190 goto_model.goto_functions.compute_location_numbers();
191
192 if(cmdline.isset("show-goto-functions"))
193 {
194 show_goto_functions(goto_model);
196 }
197
198 // show loop ids?
199 if(cmdline.isset("show-loops"))
200 {
203 }
204
205 if(cmdline.isset("show-functions-with-loops"))
206 {
207 show_functions_with_loops(goto_model);
209 }
210
211 if(cmdline.isset("validate-goto-model"))
212 {
213 goto_model.validate();
214 }
215
216 if(cmdline.isset("show-properties"))
217 {
218 ui_message_handlert ui_message_handler(cmdline, "cprover");
219 show_properties(goto_model, ui_message_handler);
221 }
222
223 // gcc produces a spurious warning for std::optional<irep_idt> if
224 // initialised with ternary operator. Initialising with an immediately
225 // invoked lambda avoids this.
226 const auto contract = [&]() -> std::optional<irep_idt> {
227 if(cmdline.isset("contract"))
228 return {cmdline.get_value("contract")};
229 else
230 return {};
231 }();
232
233 if(cmdline.isset("smt2") || cmdline.isset("text") || variable_encoding)
234 {
235 auto format = cmdline.isset("smt2") ? state_encoding_formatt::SMT2
237
238 if(cmdline.isset("outfile"))
239 {
240 auto file_name = cmdline.get_value("outfile");
241 std::ofstream out(widen_if_needed(file_name));
242
243 if(!out)
244 {
245 std::cerr << "failed to open " << file_name << '\n';
247 }
248
250 ::variable_encoding(goto_model, format, out);
251 else
253
254 std::cout << "formula written to " << file_name << '\n';
255 }
256 else
257 {
259 ::variable_encoding(goto_model, format, std::cout);
260 else
262 goto_model, format, perform_inlining, contract, std::cout);
263 }
264
265 if(!cmdline.isset("solve"))
267 }
268
270
271 if(cmdline.isset("unwind"))
272 {
273 solver_options.loop_limit = std::stoull(cmdline.get_value("unwind"));
274 }
275 else
276 solver_options.loop_limit = 1;
277
278 solver_options.trace = cmdline.isset("trace");
279 solver_options.verbose = cmdline.isset("verbose");
280
281 // solve
282 auto result = state_encoding_solver(
284
285 switch(result)
286 {
289
292
295 }
296 }
297 catch(const cprover_exception_baset &e)
298 {
299 std::cerr << "error: " << e.what() << '\n';
301 }
302
303 UNREACHABLE; // to silence a gcc warning
304}
305
308{
309 std::cout << '\n';
310
311 std::cout << '\n'
312 << banner_string("CPROVER", CBMC_VERSION) << '\n'
313 << align_center_with_border("Copyright 2022") << '\n';
314
315 std::cout << help_formatter(
316 "\n"
317 "Usage: \tPurpose:\n"
318 "\n"
319 " {bcprover} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
320 " {bcprover} {usource-file.c} \t convert a given C program\n"
321 "\n"
322 "Other options:\n"
323 " {y--inline} \t perform function call inlining before"
324 " generating the formula\n"
325 " {y--no-safety} \t disable safety checks\n"
326 " {y--contract} {ufunction} \t check contract of given function\n"
327 " {y--outfile} {ufile-name} \t set output file for formula\n"
328 " {y--smt2} \t output formula in SMT-LIB2 format\n"
329 " {y--text} \t output formula in text format\n"
330 "\n");
331}
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
std::unique_ptr< languaget > new_ansi_c_language()
configt config
Definition config.cpp:25
void c_safety_checks(goto_functionst::function_mapt::value_type &f, const exprt &expr, access_typet access_type, const namespacet &ns, goto_programt &dest)
void no_assertions(goto_functionst::function_mapt::value_type &f)
Checks for Errors in C/C++ Programs.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
argst args
Definition cmdline.h:154
virtual bool parse(int argc, const char **argv, const char *optstring)
Parses a commandline according to a specification given in optstring.
Definition cmdline.cpp:163
bool set(const cmdlinet &cmdline)
Definition config.cpp:863
struct configt::ansi_ct ansi_c
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
virtual std::string what() const
A human readable description of what went wrong.
void help()
display command line help
void get(const std::string &executable)
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
void set_verbosity(unsigned _verbosity)
Definition message.h:52
@ M_STATUS
Definition message.h:169
@ M_PROGRESS
Definition message.h:170
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Symbol table entry.
Definition symbol.h:28
bool is_file_local
Definition symbol.h:73
irep_idt name
The unique identifier.
Definition symbol.h:40
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
static void show_functions_with_loops(const goto_modelt &goto_model)
static void show_goto_functions(const goto_modelt &goto_model)
Command Line Parsing.
#define CPROVER_OPTIONS
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition exit_codes.h:45
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition exit_codes.h:49
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.
Definition exit_codes.h:37
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
Definition exit_codes.h:25
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition exit_codes.h:33
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition exit_codes.h:41
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition exit_codes.h:16
static format_containert< T > format(const T &o)
Definition format.h:37
void format_hooks()
void configure_gcc(const gcc_versiont &gcc_version)
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Inline every function call into the entry_point() function.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Help Formatter.
static help_formattert help_formatter(const std::string &s)
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
void instrument_contracts(goto_modelt &goto_model)
Instrument Given Invariants.
void instrument_given_invariants(goto_functionst::function_mapt::value_type &f)
Instrument Given Invariants.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition loop_ids.cpp:21
Loop IDs.
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition mode.cpp:39
Options.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)
Remove Indirect Function Calls.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
void install_signal_catcher()
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
solver_resultt state_encoding_solver(const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, const solver_optionst &solver_options)
void state_encoding(const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, encoding_targett &dest)
void variable_encoding(const goto_modelt &goto_model, state_encoding_formatt state_encoding_format, std::ostream &out)
State Encoding.
#define widen_if_needed(s)
Definition unicode.h:28
null_message_handlert null_message_handler
Definition message.cpp:14
const char * CBMC_VERSION