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 <algorithm>
12#include <fstream>
13#include <set>
14#include <string>
15#include <unordered_set>
16#include <utility>
17
18#include <util/config.h>
20#include <util/exit_codes.h>
21#include <util/invariant.h>
22#include <util/make_unique.h>
23#include <util/suffix.h>
24#include <util/version.h>
25
30
34
35std::unordered_set<irep_idt>
37{
38 auto symbols = std::unordered_set<irep_idt>{};
39 std::transform(
40 goto_model.get_symbol_table().begin(),
41 goto_model.get_symbol_table().end(),
42 std::inserter(symbols, symbols.end()),
43 [](const std::pair<const irep_idt, symbolt> &key_value_pair) {
44 return key_value_pair.first;
45 });
46 return symbols;
47}
48
50 goto_modelt &goto_model_with_harness,
51 const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
52{
53 for(auto const &symbol_id : goto_model_without_harness_symbols)
54 {
55 auto &symbol =
56 goto_model_with_harness.symbol_table.get_writeable_ref(symbol_id);
57 if(symbol.is_function())
58 {
59 // We don’t want bodies of functions that already existed in the
60 // symbol table (i.e. not generated by us)
61 goto_model_with_harness.unload(symbol_id);
62 if(symbol.is_file_local)
63 {
64 goto_model_with_harness.symbol_table.remove(symbol_id);
65 }
66 }
67 else if(!symbol.is_type && symbol.is_file_local)
68 {
69 // We don’t want file local symbols from an existing goto model
70 // except types / typedefs, which also apparently get marked
71 // file local sometimes.
72 goto_model_with_harness.symbol_table.remove(symbol_id);
73 }
74 else if(!symbol.is_type && symbol.is_static_lifetime)
75 {
76 // if it has static lifetime and is *not* a type it is a global variable
77 // We keep around other global variables in case we want to initialise
78 // them, but mark them as extern so we don't duplicate their definitions
79 symbol.value = nil_exprt{};
80 symbol.is_extern = true;
81 }
82 }
83}
84
85// The basic idea is that this module is handling the following
86// sequence of events:
87// 1. Initialise a goto-model by parsing an input (goto) binary
88// 2. Initialise the harness generator (with some config) that will handle
89// the mutation of the goto-model. The generator should create a new
90// function that can be called by `cbmc --function`. The generated function
91// should implement the behaviour of the harness (What exactly this means
92// depends on the configuration)
93// 3. Write the end result of that process to the output binary
94
96{
97 if(cmdline.isset("version"))
98 {
99 log.status() << CBMC_VERSION << '\n';
101 }
102
103 auto got_harness_config = handle_common_options();
104 auto factory = make_factory();
105
106 auto factory_options = collect_generate_factory_options();
107
108 // This just sets up the defaults (and would interpret options such as --32).
110
111 // Normally we would register language front-ends here but as goto-harness
112 // only works on goto binaries, we don't need to
113
114 // Read goto binary into goto-model
115 auto read_goto_binary_result =
116 read_goto_binary(got_harness_config.in_file, ui_message_handler);
117 if(!read_goto_binary_result.has_value())
118 {
119 throw deserialization_exceptiont{"failed to read goto program from file '" +
120 got_harness_config.in_file + "'"};
121 }
122 auto goto_model = std::move(read_goto_binary_result.value());
123 auto const goto_model_without_harness_symbols =
125
126 // This has to be called after the defaults are set up (as per the
127 // config.set(cmdline) above) otherwise, e.g. the architecture specification
128 // will be unknown.
129 config.set_from_symbol_table(goto_model.symbol_table);
130
131 if(goto_model.symbol_table.has_symbol(
132 got_harness_config.harness_function_name))
133 {
135 "harness function `" +
136 id2string(got_harness_config.harness_function_name) +
137 "` already in "
138 "the symbol table",
140 }
141
142 // Initialise harness generator
143 auto harness_generator = factory.factory(
144 got_harness_config.harness_type, factory_options, goto_model);
145 CHECK_RETURN(harness_generator != nullptr);
146
147 harness_generator->generate(
148 goto_model, got_harness_config.harness_function_name);
149
150 if(has_suffix(got_harness_config.out_file, ".c"))
151 {
152 filter_goto_model(goto_model, goto_model_without_harness_symbols);
153 auto harness_out = std::ofstream{got_harness_config.out_file};
154 dump_c(
155 goto_model.goto_functions,
156 true,
157 true,
158 false,
159 namespacet{goto_model.get_symbol_table()},
160 harness_out);
161 }
162 else
163 {
165 got_harness_config.out_file, goto_model, log.get_message_handler());
166 }
167
169}
170
172{
173 log.status()
174 << '\n'
175 << banner_string("Goto-Harness", CBMC_VERSION) << '\n'
176 << align_center_with_border("Copyright (C) 2019") << '\n'
177 << align_center_with_border("Diffblue Ltd.") << '\n'
178 << align_center_with_border("info@diffblue.com") << '\n'
179 << '\n'
180 << "Usage: Purpose:\n"
181 << '\n'
182 << " goto-harness [-?] [-h] [--help] show help\n"
183 << " goto-harness --version show version\n"
184 << " goto-harness <in> <out> --harness-function-name <name> --harness-type "
185 "<harness-type> [harness options]\n"
186 << "\n"
187 << "<in> goto binary to read from\n"
188 << "<out> file to write the harness to\n"
189 << " the harness is printed as C code, if <out> "
190 "has a .c suffix,\n"
191 " else a goto binary including the harness is "
192 "generated\n"
193 << "--harness-function-name the name of the harness function to "
194 "generate\n"
195 << "--harness-type one of the harness types listed below\n"
196 << "\n\n"
199}
200
202 int argc,
203 const char *argv[])
205 argc,
206 argv,
207 std::string("GOTO-HARNESS ") + CBMC_VERSION}
208{
209}
210
213{
214 goto_harness_configt goto_harness_config{};
215
216 // This just checks the positional arguments to be 2.
217 // Options are not in .args
218 if(cmdline.args.size() != 2)
219 {
220 help();
222 "need to specify both input and output file names (may be "
223 "the same)",
224 "<in goto binary> <output C file or goto binary>"};
225 }
226
227 goto_harness_config.in_file = cmdline.args[0];
228 goto_harness_config.out_file = cmdline.args[1];
229
231 {
233 "required option not set", "--" GOTO_HARNESS_GENERATOR_TYPE_OPT};
234 }
235 goto_harness_config.harness_type =
237
238 // Read the name of the harness function to generate
240 {
242 "required option not set",
244 }
245 goto_harness_config.harness_function_name = {
247
248 return goto_harness_config;
249}
250
252{
253 auto factory = goto_harness_generator_factoryt{};
254 factory.register_generator("call-function", [this]() {
255 return util_make_unique<function_call_harness_generatort>(
257 });
258
259 factory.register_generator("initialise-with-memory-snapshot", [this]() {
260 return util_make_unique<memory_snapshot_harness_generatort>(
262 });
263
264 return factory;
265}
266
269{
270 auto const common_options =
271 std::set<std::string>{"version",
274
276
277 for(auto const &option : cmdline.option_names())
278 {
279 if(common_options.find(option) == common_options.end())
280 {
281 factory_options.insert({option, cmdline.get_values(option.c_str())});
282 }
283 }
284
285 return factory_options;
286}
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
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1254
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
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:77
void unload(const irep_idt &name)
Definition: goto_model.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
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
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
The NIL expression.
Definition: std_expr.h:2874
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
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
Definition: symbol_table.h:108
virtual iteratort end() override
Definition: symbol_table.h:112
configt config
Definition: config.cpp:25
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:1584
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.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
#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
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.