cprover
Loading...
Searching...
No Matches
goto_synthesizer_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2Module: Parse Options Module
3Author: Qinheping Hu
4\*******************************************************************/
5
8
10
11#include <util/exit_codes.h>
12#include <util/help_formatter.h>
13#include <util/unicode.h>
14#include <util/version.h>
15
21
22#include <ansi-c/gcc_version.h>
27
29
30#include <fstream>
31#include <iostream>
32
34 int argc,
35 const char **argv)
38 argc,
39 argv,
40 "goto-synthesizer")
41{
42}
43
46{
47 if(cmdline.isset("version"))
48 {
49 std::cout << CBMC_VERSION << '\n';
51 }
52
53 if(cmdline.args.size() != 1 && cmdline.args.size() != 2)
54 {
55 help();
57 }
58
61
63
67
68 // configure gcc, if required -- get_goto_program will have set the config
70 {
71 gcc_versiont gcc_version;
72 gcc_version.get("gcc");
73 configure_gcc(gcc_version);
74 }
75
76 // Get options for the backend verifier and preprocess `goto_model`.
77 const auto &options = get_options();
78
79 // Synthesize loop invariants and annotate them into `goto_model`
81 const auto &invariant_map = synthesizer.synthesize_all();
82 const auto &assigns_map = synthesizer.get_assigns_map();
83
84 if(cmdline.isset("dump-loop-contracts"))
85 {
86 // Default output destination is stdout.
87 // Crangler will print the result to screen when the output destination
88 // is "stdout".
89 std::string json_output_str = "stdout";
90 if(cmdline.isset("json-output"))
91 {
92 json_output_str = cmdline.get_value("json-output");
93 }
94
96 // Output file specified
97 if(cmdline.args.size() == 2)
98 {
99 std::ofstream out(widen_if_needed(cmdline.args[1]));
100
101 if(!out)
102 {
103 log.error() << "failed to write to '" << cmdline.args[1] << "'";
105 }
107 goto_model, invariant_map, assigns_map, json_output_str, out);
108 }
109 // No output file specified. Print synthesized contracts with std::cout
110 else
111 {
113 goto_model, invariant_map, assigns_map, json_output_str, std::cout);
114 }
115
117 }
118 else if(cmdline.isset("json-output"))
119 {
121 "Incompatible option detected",
122 "--json-output must be used with --dump-loop-contracts");
123 }
124
125 // Annotate loop contracts.
127 annotate_assigns(assigns_map, goto_model);
128
129 // Apply loop contracts.
130 std::set<std::string> to_exclude_from_nondet_static(
131 cmdline.get_values("nondet-static-exclude").begin(),
132 cmdline.get_values("nondet-static-exclude").end());
134 contracts.unwind_transformed_loops =
136 contracts.apply_loop_contracts(to_exclude_from_nondet_static);
137
138 // recalculate numbers, etc.
140
141 // add loop ids
143
144 // label the assertions
146
147 // recalculate numbers, etc.
149
150 // write new binary?
151 if(cmdline.args.size() == 2)
152 {
153 log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
154 << messaget::eom;
155
158 else
160 }
161 else if(cmdline.args.size() < 2)
162 {
164 "Invalid number of positional arguments passed",
165 "[in] [out]",
166 "goto-instrument needs one input and one output file, aside from other "
167 "flags");
168 }
169
170 help();
172}
173
175{
176 log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
177 << messaget::eom;
178
180
182
183 if(!result.has_value())
185
186 goto_model = std::move(result.value());
187
190}
191
193{
194 optionst options;
195
196 // Default options
197 // These options are the same as we run CBMC without any set flag.
198 options.set_option("built-in-assertions", true);
199 options.set_option("propagation", true);
200 options.set_option("simple-slice", true);
201 options.set_option("simplify", true);
202 options.set_option("show-goto-symex-steps", false);
203 options.set_option("show-points-to-sets", false);
204 options.set_option("show-array-constraints", false);
205 options.set_option("built-in-assertions", true);
206 options.set_option("assertions", true);
207 options.set_option("assumptions", true);
208 options.set_option("depth", UINT32_MAX);
209 options.set_option("exploration-strategy", "lifo");
210 options.set_option("symex-cache-dereferences", false);
211 options.set_option("rewrite-rw-ok", true);
212 options.set_option("rewrite-union", true);
213 options.set_option("self-loops-to-assumptions", true);
214
215 options.set_option("arrays-uf", "auto");
216 if(cmdline.isset("arrays-uf-always"))
217 options.set_option("arrays-uf", "always");
218 else if(cmdline.isset("arrays-uf-never"))
219 options.set_option("arrays-uf", "never");
220
221 // Generating trace for counterexamples.
222 options.set_option("trace", true);
223
225
226 return options;
227}
228
231{
232 std::cout << '\n'
233 << banner_string("Goto-synthesizer", CBMC_VERSION) << '\n'
234 << align_center_with_border("Copyright (C) 2022") << '\n'
235 << align_center_with_border("Qinheping Hu") << '\n'
236 << align_center_with_border("qinhh@amazon.com") << '\n';
237
238 std::cout << help_formatter(
239 "\n"
240 "Usage: \tPurpose:\n"
241 "\n"
242 " {bgoto-synthesizer} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
243 " {bgoto-synthesizer} {y--version} \t show version and exit\n"
244 " {bgoto-synthesizer} {uin} {uout} \t synthesize and apply loop"
245 " invariants.\n"
246 "\n"
248 "\n"
249 "Accepts all of cbmc's options plus the following backend "
251 "\n"
252 " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
253 " {y--arrays-uf-always} \t always turn arrays into uninterpreted"
254 " functions\n"
255 "\n"
256 "Other options:\n"
257 " {y--xml-ui} \t use XML-formatted output\n"
258 " {y--json-ui} \t use JSON-formatted output\n"
259 " {y--verbosity} {u#} \t verbosity level\n"
260 "\n");
261}
configt config
Definition config.cpp:25
CBMC Command Line Option Processing.
#define CBMC_OPTIONS
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:145
const std::list< std::string > & get_values(const std::string &option) const
Definition cmdline.cpp:109
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1258
struct configt::ansi_ct ansi_c
void get(const std::string &executable)
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
void help() override
display command line help
goto_synthesizer_parse_optionst(int argc, const char **argv)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition message.cpp:105
mstreamt & error() const
Definition message.h:399
@ M_STATISTICS
Definition message.h:171
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
void set_option(const std::string &option, const bool value)
Definition options.cpp:28
ui_message_handlert ui_message_handler
#define HELP_CONFIG_BACKEND
Definition config.h:123
Verify and use annotated invariants and pre/post-conditions.
#define HELP_LOOP_CONTRACTS_NO_UNWIND
Definition contracts.h:37
#define FLAG_LOOP_CONTRACTS_NO_UNWIND
Definition contracts.h:36
void dump_loop_contracts(goto_modelt &goto_model, const std::map< loop_idt, exprt > &invariant_map, const std::map< loop_idt, std::set< exprt > > &assigns_map, const std::string &json_output_str, std::ostream &out)
#define HELP_DUMP_LOOP_CONTRACTS
Enumerative Loop Contracts Synthesizer.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
Definition exit_codes.h:62
#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_SUCCESS
Success indicates the required analysis has been performed without error.
Definition exit_codes.h:16
void configure_gcc(const gcc_versiont &gcc_version)
#define GOTO_SYNTHESIZER_OPTIONS
Help Formatter.
static help_formattert help_formatter(const std::string &s)
Volatile Variables.
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)
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
Read Goto Programs.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
Show the goto functions.
Show the properties.
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
#define HELP_SOLVER
#define widen_if_needed(s)
Definition unicode.h:28
void annotate_assigns(const std::map< loop_idt, std::set< exprt > > &assigns_map, goto_modelt &goto_model)
Annotate the assigns in assigns_map to their corresponding loops.
Definition utils.cpp:720
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
Definition utils.cpp:700
const char * CBMC_VERSION
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.