cprover
Loading...
Searching...
No Matches
goto_harness_parse_options.cpp
Go to the documentation of this file.
1/******************************************************************\
2
3Module: goto_harness_parse_options
4
5Author: Diffblue Ltd.
6
7\******************************************************************/
8
10
11#include <util/config.h>
13#include <util/exit_codes.h>
14#include <util/help_formatter.h>
15#include <util/invariant.h>
16#include <util/make_unique.h>
17#include <util/suffix.h>
18#include <util/version.h>
19
23
25
29
30#include <algorithm>
31#include <fstream>
32#include <iostream>
33#include <set>
34#include <string>
35#include <unordered_set>
36#include <utility>
37
38std::unordered_set<irep_idt>
40{
41 auto symbols = std::unordered_set<irep_idt>{};
42 std::transform(
43 goto_model.get_symbol_table().begin(),
44 goto_model.get_symbol_table().end(),
45 std::inserter(symbols, symbols.end()),
46 [](const std::pair<const irep_idt, symbolt> &key_value_pair) {
47 return key_value_pair.first;
48 });
49 return symbols;
50}
51
53 goto_modelt &goto_model_with_harness,
54 const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
55{
56 for(auto const &symbol_id : goto_model_without_harness_symbols)
57 {
58 auto &symbol =
59 goto_model_with_harness.symbol_table.get_writeable_ref(symbol_id);
60 if(symbol.is_function())
61 {
62 // We don’t want bodies of functions that already existed in the
63 // symbol table (i.e. not generated by us)
64 goto_model_with_harness.unload(symbol_id);
65 if(symbol.is_file_local)
66 {
67 goto_model_with_harness.symbol_table.remove(symbol_id);
68 }
69 }
70 else if(!symbol.is_type && symbol.is_file_local)
71 {
72 // We don’t want file local symbols from an existing goto model
73 // except types / typedefs, which also apparently get marked
74 // file local sometimes.
75 goto_model_with_harness.symbol_table.remove(symbol_id);
76 }
77 else if(!symbol.is_type && symbol.is_static_lifetime)
78 {
79 // if it has static lifetime and is *not* a type it is a global variable
80 // We keep around other global variables in case we want to initialise
81 // them, but mark them as extern so we don't duplicate their definitions
82 symbol.value = nil_exprt{};
83 symbol.is_extern = true;
84 }
85 }
86}
87
88// The basic idea is that this module is handling the following
89// sequence of events:
90// 1. Initialise a goto-model by parsing an input (goto) binary
91// 2. Initialise the harness generator (with some config) that will handle
92// the mutation of the goto-model. The generator should create a new
93// function that can be called by `cbmc --function`. The generated function
94// should implement the behaviour of the harness (What exactly this means
95// depends on the configuration)
96// 3. Write the end result of that process to the output binary
97
99{
100 if(cmdline.isset("version"))
101 {
102 std::cout << CBMC_VERSION << '\n';
104 }
105
106 auto got_harness_config = handle_common_options();
107 auto factory = make_factory();
108
109 auto factory_options = collect_generate_factory_options();
110
111 // This just sets up the defaults (and would interpret options such as --32).
113
114 // Normally we would register language front-ends here but as goto-harness
115 // only works on goto binaries, we don't need to
116
117 // Read goto binary into goto-model
118 auto read_goto_binary_result =
119 read_goto_binary(got_harness_config.in_file, ui_message_handler);
120 if(!read_goto_binary_result.has_value())
121 {
122 throw deserialization_exceptiont{"failed to read goto program from file '" +
123 got_harness_config.in_file + "'"};
124 }
125 auto goto_model = std::move(read_goto_binary_result.value());
126 auto const goto_model_without_harness_symbols =
128
129 // This has to be called after the defaults are set up (as per the
130 // config.set(cmdline) above) otherwise, e.g. the architecture specification
131 // will be unknown.
132 config.set_from_symbol_table(goto_model.symbol_table);
133
134 if(goto_model.symbol_table.has_symbol(
135 got_harness_config.harness_function_name))
136 {
138 "harness function `" +
139 id2string(got_harness_config.harness_function_name) +
140 "` already in "
141 "the symbol table",
143 }
144
145 // Initialise harness generator
146 auto harness_generator = factory.factory(
147 got_harness_config.harness_type, factory_options, goto_model);
148 CHECK_RETURN(harness_generator != nullptr);
149
150 harness_generator->generate(
151 goto_model, got_harness_config.harness_function_name);
152
153 if(has_suffix(got_harness_config.out_file, ".c"))
154 {
155 filter_goto_model(goto_model, goto_model_without_harness_symbols);
156 auto harness_out = std::ofstream{got_harness_config.out_file};
157 dump_c(
158 goto_model.goto_functions,
159 true,
160 true,
161 false,
162 namespacet{goto_model.get_symbol_table()},
163 harness_out);
164 }
165 else
166 {
168 got_harness_config.out_file, goto_model, log.get_message_handler());
169 }
170
172}
173
175{
176 std::cout << '\n'
177 << banner_string("Goto-Harness", CBMC_VERSION) << '\n'
178 << align_center_with_border("Copyright (C) 2019") << '\n'
179 << align_center_with_border("Diffblue Ltd.") << '\n'
180 << align_center_with_border("info@diffblue.com") << '\n';
181
182 // clang-format off
183 std::cout << help_formatter(
184 "\n"
185 "Usage: \tPurpose:\n"
186 "\n"
187 " {bgoto-harness} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
188 " {bgoto-harness} {y--version} \t show version and exit\n"
189 " {bgoto-harness} {uin} {uout} {y--harness-function-name} {uname}"
190 " {y--harness-type} {uharness-type} [harness options]\n"
191 "\n"
192 " {uin} \t goto binary to read from\n"
193 " {uout} \t file to write the harness to; the harness is printed as C"
194 " code, if {uout} has a .c suffix, else a goto binary including the harness"
195 " is generated\n"
196 " {y--harness-function-name} {uname} \t the name of the harness function to"
197 " generate\n"
198 " {y--harness-type} {utype} \t one of the harness types listed below\n"
199 "\n"
201 "\n"
203 "\n");
204 // clang-format on
205}
206
208 int argc,
209 const char *argv[])
211 argc,
212 argv,
213 std::string("GOTO-HARNESS ") + CBMC_VERSION}
214{
215}
216
219{
220 goto_harness_configt goto_harness_config{};
221
222 // This just checks the positional arguments to be 2.
223 // Options are not in .args
224 if(cmdline.args.size() != 2)
225 {
226 help();
228 "need to specify both input and output file names (may be "
229 "the same)",
230 "<in goto binary> <output C file or goto binary>"};
231 }
232
233 goto_harness_config.in_file = cmdline.args[0];
234 goto_harness_config.out_file = cmdline.args[1];
235
237 {
239 "required option not set", "--" GOTO_HARNESS_GENERATOR_TYPE_OPT};
240 }
241 goto_harness_config.harness_type =
243
244 // Read the name of the harness function to generate
246 {
248 "required option not set",
250 }
251 goto_harness_config.harness_function_name = {
253
254 return goto_harness_config;
255}
256
258{
259 auto factory = goto_harness_generator_factoryt{};
260 factory.register_generator("call-function", [this]() {
263 });
264
265 factory.register_generator("initialize-with-memory-snapshot", [this]() {
268 });
269
270 return factory;
271}
272
275{
276 auto const common_options =
277 std::set<std::string>{"version",
280
282
283 for(auto const &option : cmdline.option_names())
284 {
285 if(common_options.find(option) == common_options.end())
286 {
287 factory_options.insert({option, cmdline.get_values(option.c_str())});
288 }
289 }
290
291 return factory_options;
292}
configt config
Definition config.cpp:25
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
option_namest option_names() const
Pseudo-object that can be used to iterate over options in this cmdlinet (should not outlive this)
Definition cmdline.cpp:161
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
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
helper to select harness type by name.
std::map< std::string, std::list< std::string > > generator_optionst
void register_generator(std::string generator_name, build_generatort build_generator)
register a new goto-harness generator with the given name.
goto_harness_configt handle_common_options()
Handle command line arguments that are common to all harness generators.
goto_harness_parse_optionst(int argc, const char *argv[])
goto_harness_generator_factoryt make_factory()
Setup the generator factory.
goto_harness_generator_factoryt::generator_optionst collect_generate_factory_options()
Gather all the options that are not handled by handle_common_options().
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition goto_model.h:84
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
std::size_t unload(const irep_idt &name)
Remove the function named name from the function map, if it exists.
Definition goto_model.h:72
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
message_handlert & get_message_handler()
Definition message.h:184
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3026
ui_message_handlert ui_message_handler
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
virtual iteratort begin() override
virtual iteratort end() override
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition dump_c.cpp:1645
Dump C from Goto Program.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition exit_codes.h:16
#define FUNCTION_HARNESS_GENERATOR_HELP
#define GOTO_HARNESS_GENERATOR_TYPE_OPT
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
std::unordered_set< irep_idt > get_symbol_names_from_goto_model(const goto_modelt &goto_model)
static void filter_goto_model(goto_modelt &goto_model_with_harness, const std::unordered_set< irep_idt > &goto_model_without_harness_symbols)
#define GOTO_HARNESS_OPTIONS
Symbol Table + CFG.
Help Formatter.
static help_formattert help_formatter(const std::string &s)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
STL namespace.
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.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
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.