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 <set>
13 #include <string>
14 #include <utility>
15 
20 #include <util/config.h>
21 #include <util/exception_utils.h>
22 #include <util/exit_codes.h>
23 #include <util/invariant.h>
24 #include <util/version.h>
25 
29 
30 // The basic idea is that this module is handling the following
31 // sequence of events:
32 // 1. Initialise a goto-model by parsing an input (goto) binary
33 // 2. Initialise the harness generator (with some config) that will handle
34 // the mutation of the goto-model. The generator should create a new
35 // function that can be called by `cbmc --function`. The generated function
36 // should implement the behaviour of the harness (What exactly this means
37 // depends on the configuration)
38 // 3. Write the end result of that process to the output binary
39 
41 {
42  if(cmdline.isset("version"))
43  {
44  log.status() << CBMC_VERSION << '\n';
45  return CPROVER_EXIT_SUCCESS;
46  }
47 
48  auto got_harness_config = handle_common_options();
49  auto factory = make_factory();
50 
51  auto factory_options = collect_generate_factory_options();
52 
53  // This just sets up the defaults (and would interpret options such as --32).
55 
56  // Read goto binary into goto-model
57  auto read_goto_binary_result =
58  read_goto_binary(got_harness_config.in_file, ui_message_handler);
59  if(!read_goto_binary_result.has_value())
60  {
61  throw deserialization_exceptiont{"failed to read goto program from file '" +
62  got_harness_config.in_file + "'"};
63  }
64  auto goto_model = std::move(read_goto_binary_result.value());
65 
66  // This has to be called after the defaults are set up (as per the
67  // config.set(cmdline) above) otherwise, e.g. the architecture specification
68  // will be unknown.
69  config.set_from_symbol_table(goto_model.symbol_table);
70 
71  if(goto_model.symbol_table.has_symbol(
72  got_harness_config.harness_function_name))
73  {
75  "harness function `" +
76  id2string(got_harness_config.harness_function_name) +
77  "` already in "
78  "the symbol table",
80  }
81 
82  // Initialise harness generator
83  auto harness_generator = factory.factory(
84  got_harness_config.harness_type, factory_options, goto_model);
85  CHECK_RETURN(harness_generator != nullptr);
86 
87  harness_generator->generate(
88  goto_model, got_harness_config.harness_function_name);
89 
90  // Write end result to new goto-binary
92  got_harness_config.out_file, goto_model, ui_message_handler))
93  {
94  throw system_exceptiont{"failed to write goto program from file '" +
95  got_harness_config.out_file + "'"};
96  }
97 
98  return CPROVER_EXIT_SUCCESS;
99 }
100 
102 {
103  log.status()
104  << '\n'
105  << banner_string("Goto-Harness", CBMC_VERSION) << '\n'
106  << align_center_with_border("Copyright (C) 2019") << '\n'
107  << align_center_with_border("Diffblue Ltd.") << '\n'
108  << align_center_with_border("info@diffblue.com") << '\n'
109  << '\n'
110  << "Usage: Purpose:\n"
111  << '\n'
112  << " goto-harness [-?] [-h] [--help] show help\n"
113  << " goto-harness --version show version\n"
114  << " goto-harness <in> <out> --harness-function-name <name> --harness-type "
115  "<harness-type> [harness options]\n"
116  << "\n"
117  << "<in> <out> goto binaries to read from / write to\n"
118  << "--harness-function-name the name of the harness function to "
119  "generate\n"
120  << "--harness-type one of the harness types listed below\n"
121  << "\n\n"
124 }
125 
127  int argc,
128  const char *argv[])
130  argc,
131  argv,
132  std::string("GOTO-HARNESS ") + CBMC_VERSION}
133 {
134 }
135 
138 {
139  goto_harness_configt goto_harness_config{};
140 
141  // This just checks the positional arguments to be 2.
142  // Options are not in .args
143  if(cmdline.args.size() != 2)
144  {
145  help();
147  "need to specify both input and output goto binary file names (may be "
148  "the same)",
149  "<in goto binary> <out goto binary>"};
150  }
151 
152  goto_harness_config.in_file = cmdline.args[0];
153  goto_harness_config.out_file = cmdline.args[1];
154 
156  {
158  "required option not set", "--" GOTO_HARNESS_GENERATOR_TYPE_OPT};
159  }
160  goto_harness_config.harness_type =
162 
163  // Read the name of the harness function to generate
165  {
167  "required option not set",
169  }
170  goto_harness_config.harness_function_name = {
172 
173  return goto_harness_config;
174 }
175 
177 {
178  auto factory = goto_harness_generator_factoryt{};
179  factory.register_generator("call-function", [this]() {
180  return util_make_unique<function_call_harness_generatort>(
182  });
183 
184  factory.register_generator("initialise-with-memory-snapshot", [this]() {
185  return util_make_unique<memory_snapshot_harness_generatort>(
187  });
188 
189  return factory;
190 }
191 
194 {
195  auto const common_options =
196  std::set<std::string>{"version",
199 
201 
202  for(auto const &option : cmdline.option_names())
203  {
204  if(common_options.find(option) == common_options.end())
205  {
206  factory_options.insert({option, cmdline.get_values(option.c_str())});
207  }
208  }
209 
210  return factory_options;
211 }
cmdlinet::args
argst args
Definition: cmdline.h:85
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
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
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:28
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:400
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:126
function_call_harness_generator.h
goto_harness_generator_factory.h
invariant.h
goto_model.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
messaget::eom
static eomt eom
Definition: message.h:283
goto_convert.h
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:193
write_goto_binary.h
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
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:146
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:46
system_exceptiont
Thrown when some external system fails unexpectedly.
Definition: exception_utils.h:61
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:1178
goto_harness_parse_optionst::help
void help() override
Definition: goto_harness_parse_options.cpp:101
read_goto_binary.h
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:248
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:176
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:137
goto_harness_parse_optionst::doit
int doit() override
Definition: goto_harness_parse_options.cpp:40
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:768
exit_codes.h
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
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:107
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
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:133