cprover
goto_harness_parse_options.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: goto_harness_parse_options
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
10 
11 #include <cstddef>
12 #include <fstream>
13 #include <set>
14 #include <string>
15 #include <unordered_set>
16 #include <utility>
17 
18 #include <util/config.h>
19 #include <util/exception_utils.h>
20 #include <util/exit_codes.h>
21 #include <util/expr_iterator.h>
22 #include <util/invariant.h>
23 #include <util/suffix.h>
24 #include <util/version.h>
25 
26 #include <goto-instrument/dump_c.h>
32 
36 
37 std::unordered_set<irep_idt>
39 {
40  auto symbols = std::unordered_set<irep_idt>{};
42  goto_model.get_symbol_table().begin(),
43  goto_model.get_symbol_table().end(),
44  std::inserter(symbols, symbols.end()),
45  [](const std::pair<const irep_idt, symbolt> &key_value_pair) {
46  return key_value_pair.first;
47  });
48  return symbols;
49 }
50 
51 static void filter_goto_model(
52  goto_modelt &goto_model_with_harness,
53  const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
54 {
55  for(auto const &symbol_id : goto_model_without_harness_symbols)
56  {
57  auto &symbol =
58  goto_model_with_harness.symbol_table.get_writeable_ref(symbol_id);
59  if(symbol.is_function())
60  {
61  // We don’t want bodies of functions that already existed in the
62  // symbol table (i.e. not generated by us)
63  goto_model_with_harness.unload(symbol_id);
64  if(symbol.is_file_local)
65  {
66  goto_model_with_harness.symbol_table.remove(symbol_id);
67  }
68  }
69  else if(!symbol.is_type && symbol.is_file_local)
70  {
71  // We don’t want file local symbols from an existing goto model
72  // except types / typedefs, which also apparently get marked
73  // file local sometimes.
74  goto_model_with_harness.symbol_table.remove(symbol_id);
75  }
76  else if(!symbol.is_type && symbol.is_static_lifetime)
77  {
78  // if it has static lifetime and is *not* a type it is a global variable
79  // We keep around other global variables in case we want to initialise
80  // them, but mark them as extern so we don't duplicate their definitions
81  symbol.value = nil_exprt{};
82  symbol.is_extern = true;
83  }
84  }
85 }
86 
87 // The basic idea is that this module is handling the following
88 // sequence of events:
89 // 1. Initialise a goto-model by parsing an input (goto) binary
90 // 2. Initialise the harness generator (with some config) that will handle
91 // the mutation of the goto-model. The generator should create a new
92 // function that can be called by `cbmc --function`. The generated function
93 // should implement the behaviour of the harness (What exactly this means
94 // depends on the configuration)
95 // 3. Write the end result of that process to the output binary
96 
98 {
99  if(cmdline.isset("version"))
100  {
101  log.status() << CBMC_VERSION << '\n';
102  return CPROVER_EXIT_SUCCESS;
103  }
104 
105  auto got_harness_config = handle_common_options();
106  auto factory = make_factory();
107 
108  auto factory_options = collect_generate_factory_options();
109 
110  // This just sets up the defaults (and would interpret options such as --32).
111  config.set(cmdline);
112 
113  // Read goto binary into goto-model
114  auto read_goto_binary_result =
115  read_goto_binary(got_harness_config.in_file, ui_message_handler);
116  if(!read_goto_binary_result.has_value())
117  {
118  throw deserialization_exceptiont{"failed to read goto program from file '" +
119  got_harness_config.in_file + "'"};
120  }
121  auto goto_model = std::move(read_goto_binary_result.value());
122  auto const goto_model_without_harness_symbols =
124 
125  // This has to be called after the defaults are set up (as per the
126  // config.set(cmdline) above) otherwise, e.g. the architecture specification
127  // will be unknown.
128  config.set_from_symbol_table(goto_model.symbol_table);
129 
130  if(goto_model.symbol_table.has_symbol(
131  got_harness_config.harness_function_name))
132  {
134  "harness function `" +
135  id2string(got_harness_config.harness_function_name) +
136  "` already in "
137  "the symbol table",
139  }
140 
141  // Initialise harness generator
142  auto harness_generator = factory.factory(
143  got_harness_config.harness_type, factory_options, goto_model);
144  CHECK_RETURN(harness_generator != nullptr);
145 
146  harness_generator->generate(
147  goto_model, got_harness_config.harness_function_name);
148 
149  if(has_suffix(got_harness_config.out_file, ".c"))
150  {
151  filter_goto_model(goto_model, goto_model_without_harness_symbols);
152  auto harness_out = std::ofstream{got_harness_config.out_file};
153  dump_c(
154  goto_model.goto_functions,
155  true,
156  true,
157  false,
158  namespacet{goto_model.get_symbol_table()},
159  harness_out);
160  }
161  else
162  {
164  got_harness_config.out_file, goto_model, log.get_message_handler());
165  }
166 
167  return CPROVER_EXIT_SUCCESS;
168 }
169 
171 {
172  log.status()
173  << '\n'
174  << banner_string("Goto-Harness", CBMC_VERSION) << '\n'
175  << align_center_with_border("Copyright (C) 2019") << '\n'
176  << align_center_with_border("Diffblue Ltd.") << '\n'
177  << align_center_with_border("info@diffblue.com") << '\n'
178  << '\n'
179  << "Usage: Purpose:\n"
180  << '\n'
181  << " goto-harness [-?] [-h] [--help] show help\n"
182  << " goto-harness --version show version\n"
183  << " goto-harness <in> <out> --harness-function-name <name> --harness-type "
184  "<harness-type> [harness options]\n"
185  << "\n"
186  << "<in> goto binary to read from\n"
187  << "<out> file to write the harness to\n"
188  << " the harness is printed as C code, if <out> "
189  "has a .c suffix,\n"
190  " else a goto binary including the harness is "
191  "generated\n"
192  << "--harness-function-name the name of the harness function to "
193  "generate\n"
194  << "--harness-type one of the harness types listed below\n"
195  << "\n\n"
198 }
199 
201  int argc,
202  const char *argv[])
204  argc,
205  argv,
206  std::string("GOTO-HARNESS ") + CBMC_VERSION}
207 {
208 }
209 
212 {
213  goto_harness_configt goto_harness_config{};
214 
215  // This just checks the positional arguments to be 2.
216  // Options are not in .args
217  if(cmdline.args.size() != 2)
218  {
219  help();
221  "need to specify both input and output file names (may be "
222  "the same)",
223  "<in goto binary> <output C file or goto binary>"};
224  }
225 
226  goto_harness_config.in_file = cmdline.args[0];
227  goto_harness_config.out_file = cmdline.args[1];
228 
230  {
232  "required option not set", "--" GOTO_HARNESS_GENERATOR_TYPE_OPT};
233  }
234  goto_harness_config.harness_type =
236 
237  // Read the name of the harness function to generate
239  {
241  "required option not set",
243  }
244  goto_harness_config.harness_function_name = {
246 
247  return goto_harness_config;
248 }
249 
251 {
252  auto factory = goto_harness_generator_factoryt{};
253  factory.register_generator("call-function", [this]() {
254  return util_make_unique<function_call_harness_generatort>(
256  });
257 
258  factory.register_generator("initialise-with-memory-snapshot", [this]() {
259  return util_make_unique<memory_snapshot_harness_generatort>(
261  });
262 
263  return factory;
264 }
265 
268 {
269  auto const common_options =
270  std::set<std::string>{"version",
273 
275 
276  for(auto const &option : cmdline.option_names())
277  {
278  if(common_options.find(option) == common_options.end())
279  {
280  factory_options.insert({option, cmdline.get_values(option.c_str())});
281  }
282  }
283 
284  return factory_options;
285 }
cmdlinet::args
argst args
Definition: cmdline.h:143
exception_utils.h
GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
Definition: goto_harness_generator_factory.h:20
goto_modelt::unload
void unload(const irep_idt &name)
Definition: goto_model.h:68
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
parse_options_baset
Definition: parse_options.h:20
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
GOTO_HARNESS_GENERATOR_TYPE_OPT
#define GOTO_HARNESS_GENERATOR_TYPE_OPT
Definition: goto_harness_generator_factory.h:19
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
transform
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.cpp:157
messaget::status
mstreamt & status() const
Definition: message.h:414
write_goto_binary
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.
Definition: write_goto_binary.cpp:25
MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
Definition: memory_snapshot_harness_generator_options.h:34
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:73
goto_harness_parse_optionst::goto_harness_parse_optionst
goto_harness_parse_optionst(int argc, const char *argv[])
Definition: goto_harness_parse_options.cpp:200
function_call_harness_generator.h
goto_harness_generator_factory.h
invariant.h
filter_goto_model
static void filter_goto_model(goto_modelt &goto_model_with_harness, const std::unordered_set< irep_idt > &goto_model_without_harness_symbols)
Definition: goto_harness_parse_options.cpp:51
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
goto_harness_generator_factoryt::register_generator
void register_generator(std::string generator_name, build_generatort build_generator)
register a new goto-harness generator with the given name.
Definition: goto_harness_generator_factory.cpp:22
get_symbol_names_from_goto_model
std::unordered_set< irep_idt > get_symbol_names_from_goto_model(const goto_modelt &goto_model)
Definition: goto_harness_parse_options.cpp:38
messaget::eom
static eomt eom
Definition: message.h:297
goto_convert.h
Program Transformation.
version.h
goto_harness_parse_optionst::collect_generate_factory_options
goto_harness_generator_factoryt::generator_optionst collect_generate_factory_options()
Gather all the options that are not handled by handle_common_options().
Definition: goto_harness_parse_options.cpp:267
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
write_goto_binary.h
Write GOTO binaries.
symbol_tablet::begin
virtual iteratort begin() override
Definition: symbol_table.h:114
goto_harness_generator_factoryt::generator_optionst
std::map< std::string, std::list< std::string > > generator_optionst
Definition: goto_harness_generator_factory.h:38
goto_harness_parse_options.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
CBMC_VERSION
const char * CBMC_VERSION
GOTO_HARNESS_OPTIONS
#define GOTO_HARNESS_OPTIONS
Definition: goto_harness_parse_options.h:23
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
symbol_tablet::end
virtual iteratort end() override
Definition: symbol_table.h:118
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
dump_c
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:1577
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
show_symbol_table.h
Show the symbol table.
goto_harness_generator_factoryt
helper to select harness type by name.
Definition: goto_harness_generator_factory.h:32
goto_harness_parse_optionst::goto_harness_configt
Definition: goto_harness_parse_options.h:43
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1229
goto_harness_parse_optionst::help
void help() override
Definition: goto_harness_parse_options.cpp:170
read_goto_binary.h
Read Goto Programs.
symbol_table_baset::remove
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Definition: symbol_table_base.cpp:27
cmdlinet::option_names
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:162
memory_snapshot_harness_generator.h
config
configt config
Definition: config.cpp:24
goto_harness_parse_optionst::make_factory
goto_harness_generator_factoryt make_factory()
Setup the generator factory.
Definition: goto_harness_parse_options.cpp:250
parse_options_baset::log
messaget log
Definition: parse_options.h:43
goto_harness_parse_optionst::handle_common_options
goto_harness_configt handle_common_options()
Handle command line arguments that are common to all harness generators.
Definition: goto_harness_parse_options.cpp:211
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
suffix.h
goto_harness_parse_optionst::doit
int doit() override
Definition: goto_harness_parse_options.cpp:97
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:797
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
goto_modelt::get_symbol_table
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:77
config.h
read_goto_binary
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.
Definition: read_goto_binary.cpp:59
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
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
dump_c.h
Dump C from Goto Program.
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
FUNCTION_HARNESS_GENERATOR_HELP
#define FUNCTION_HARNESS_GENERATOR_HELP
Definition: function_harness_generator_options.h:41
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