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 }
cmdlinet::args
argst args
Definition: cmdline.h:91
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
messaget::status
mstreamt & status() const
Definition: message.h:414
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:187
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:50
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
mode.h
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:37
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:254
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:44
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:1462
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
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:1205
goto_harness_parse_optionst::help
void help() override
Definition: goto_harness_parse_options.cpp:161
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:249
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:237
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:198
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
goto_harness_parse_optionst::doit
int doit() override
Definition: goto_harness_parse_options.cpp:96
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
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