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 <goto-instrument/dump_c.h>
24 #include <langapi/mode.h>
25 #include <util/config.h>
26 #include <util/exception_utils.h>
27 #include <util/exit_codes.h>
28 #include <util/expr_iterator.h>
29 #include <util/invariant.h>
30 #include <util/version.h>
31 
35 
36 std::unordered_set<irep_idt>
38 {
39  auto symbols = std::unordered_set<irep_idt>{};
40  std::transform(
41  goto_model.get_symbol_table().begin(),
42  goto_model.get_symbol_table().end(),
43  std::inserter(symbols, symbols.end()),
44  [](const std::pair<const irep_idt, symbolt> &key_value_pair) {
45  return key_value_pair.first;
46  });
47  return symbols;
48 }
49 
50 static void filter_goto_model(
51  goto_modelt &goto_model_with_harness,
52  const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
53 {
54  for(auto const &symbol_id : goto_model_without_harness_symbols)
55  {
56  auto &symbol =
57  goto_model_with_harness.symbol_table.get_writeable_ref(symbol_id);
58  if(symbol.is_function())
59  {
60  // We don’t want bodies of functions that already existed in the
61  // symbol table (i.e. not generated by us)
62  goto_model_with_harness.unload(symbol_id);
63  if(symbol.is_file_local)
64  {
65  goto_model_with_harness.symbol_table.remove(symbol_id);
66  }
67  }
68  else if(!symbol.is_type && symbol.is_file_local)
69  {
70  // We don’t want file local symbols from an existing goto model
71  // except types / typedefs, which also apparently get marked
72  // file local sometimes.
73  goto_model_with_harness.symbol_table.remove(symbol_id);
74  }
75  else if(!symbol.is_type && symbol.is_static_lifetime)
76  {
77  // if it has static lifetime and is *not* a type it is a global variable
78  // We keep around other global variables in case we want to initialise
79  // them, but mark them as extern so we don't duplicate their definitions
80  symbol.value = nil_exprt{};
81  symbol.is_extern = true;
82  }
83  }
84 }
85 
86 // The basic idea is that this module is handling the following
87 // sequence of events:
88 // 1. Initialise a goto-model by parsing an input (goto) binary
89 // 2. Initialise the harness generator (with some config) that will handle
90 // the mutation of the goto-model. The generator should create a new
91 // function that can be called by `cbmc --function`. The generated function
92 // should implement the behaviour of the harness (What exactly this means
93 // depends on the configuration)
94 // 3. Write the end result of that process to the output binary
95 
97 {
98  if(cmdline.isset("version"))
99  {
100  log.status() << CBMC_VERSION << '\n';
101  return CPROVER_EXIT_SUCCESS;
102  }
103 
104  auto got_harness_config = handle_common_options();
105  auto factory = make_factory();
106 
107  auto factory_options = collect_generate_factory_options();
108 
109  // This just sets up the defaults (and would interpret options such as --32).
110  config.set(cmdline);
111 
112  // Read goto binary into goto-model
113  auto read_goto_binary_result =
114  read_goto_binary(got_harness_config.in_file, ui_message_handler);
115  if(!read_goto_binary_result.has_value())
116  {
117  throw deserialization_exceptiont{"failed to read goto program from file '" +
118  got_harness_config.in_file + "'"};
119  }
120  auto goto_model = std::move(read_goto_binary_result.value());
121  auto const goto_model_without_harness_symbols =
123 
124  // This has to be called after the defaults are set up (as per the
125  // config.set(cmdline) above) otherwise, e.g. the architecture specification
126  // will be unknown.
127  config.set_from_symbol_table(goto_model.symbol_table);
128 
129  if(goto_model.symbol_table.has_symbol(
130  got_harness_config.harness_function_name))
131  {
133  "harness function `" +
134  id2string(got_harness_config.harness_function_name) +
135  "` already in "
136  "the symbol table",
138  }
139 
140  // Initialise harness generator
141  auto harness_generator = factory.factory(
142  got_harness_config.harness_type, factory_options, goto_model);
143  CHECK_RETURN(harness_generator != nullptr);
144 
145  harness_generator->generate(
146  goto_model, got_harness_config.harness_function_name);
147 
148  filter_goto_model(goto_model, goto_model_without_harness_symbols);
149  auto harness_out = std::ofstream{got_harness_config.out_file};
150  dump_c(
151  goto_model.goto_functions,
152  true,
153  true,
154  false,
155  namespacet{goto_model.get_symbol_table()},
156  harness_out);
157 
158  return CPROVER_EXIT_SUCCESS;
159 }
160 
162 {
163  log.status()
164  << '\n'
165  << banner_string("Goto-Harness", CBMC_VERSION) << '\n'
166  << align_center_with_border("Copyright (C) 2019") << '\n'
167  << align_center_with_border("Diffblue Ltd.") << '\n'
168  << align_center_with_border("info@diffblue.com") << '\n'
169  << '\n'
170  << "Usage: Purpose:\n"
171  << '\n'
172  << " goto-harness [-?] [-h] [--help] show help\n"
173  << " goto-harness --version show version\n"
174  << " goto-harness <in> <out> --harness-function-name <name> --harness-type "
175  "<harness-type> [harness options]\n"
176  << "\n"
177  << "<in> goto binaries to read from\n"
178  << "<out> C file to write the harness to\n"
179  << "--harness-function-name the name of the harness function to "
180  "generate\n"
181  << "--harness-type one of the harness types listed below\n"
182  << "\n\n"
185 }
186 
188  int argc,
189  const char *argv[])
191  argc,
192  argv,
193  std::string("GOTO-HARNESS ") + CBMC_VERSION}
194 {
195 }
196 
199 {
200  goto_harness_configt goto_harness_config{};
201 
202  // This just checks the positional arguments to be 2.
203  // Options are not in .args
204  if(cmdline.args.size() != 2)
205  {
206  help();
208  "need to specify both input and output goto binary file names (may be "
209  "the same)",
210  "<in goto binary> <out goto binary>"};
211  }
212 
213  goto_harness_config.in_file = cmdline.args[0];
214  goto_harness_config.out_file = cmdline.args[1];
215 
217  {
219  "required option not set", "--" GOTO_HARNESS_GENERATOR_TYPE_OPT};
220  }
221  goto_harness_config.harness_type =
223 
224  // Read the name of the harness function to generate
226  {
228  "required option not set",
230  }
231  goto_harness_config.harness_function_name = {
233 
234  return goto_harness_config;
235 }
236 
238 {
239  auto factory = goto_harness_generator_factoryt{};
240  factory.register_generator("call-function", [this]() {
241  return util_make_unique<function_call_harness_generatort>(
243  });
244 
245  factory.register_generator("initialise-with-memory-snapshot", [this]() {
246  return util_make_unique<memory_snapshot_harness_generatort>(
248  });
249 
250  return factory;
251 }
252 
255 {
256  auto const common_options =
257  std::set<std::string>{"version",
260 
262 
263  for(auto const &option : cmdline.option_names())
264  {
265  if(common_options.find(option) == common_options.end())
266  {
267  factory_options.insert({option, cmdline.get_values(option.c_str())});
268  }
269  }
270 
271  return factory_options;
272 }
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:1230
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
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:92
The NIL expression.
Definition: std_expr.h:2735
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
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:114
virtual iteratort end() override
Definition: symbol_table.h:118
configt config
Definition: config.cpp:24
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:1576
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
Forward depth-first search iterators These iterators' copy operations are expensive,...
#define FUNCTION_HARNESS_GENERATOR_HELP
Program Transformation.
#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.
Show the symbol table.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
const char * CBMC_VERSION
Write GOTO binaries.