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 <algorithm>
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/invariant.h>
22 #include <util/make_unique.h>
23 #include <util/suffix.h>
24 #include <util/version.h>
25 
26 #include <goto-instrument/dump_c.h>
30 
34 
35 std::unordered_set<irep_idt>
37 {
38  auto symbols = std::unordered_set<irep_idt>{};
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 
49 static void filter_goto_model(
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';
100  return CPROVER_EXIT_SUCCESS;
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).
109  config.set(cmdline);
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 
168  return CPROVER_EXIT_SUCCESS;
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 }
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
std::string get_value(char option) const
Definition: cmdline.cpp:47
virtual bool isset(char option) const
Definition: cmdline.cpp:29
argst args
Definition: cmdline.h:143
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
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1231
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().
void unload(const irep_idt &name)
Definition: goto_model.h:68
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:77
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 ...
mstreamt & status() const
Definition: message.h:414
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
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:2820
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
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:1579
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:49
#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
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.