cprover
symtab2gb_parse_options.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: symtab2gb_parse_options
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
10 
11 #include <fstream>
12 #include <iostream>
13 #include <string>
14 
20 
21 #include <util/config.h>
22 #include <util/exception_utils.h>
23 #include <util/exit_codes.h>
24 #include <util/invariant.h>
25 #include <util/optional.h>
26 #include <util/version.h>
27 
30  argc,
31  argv,
32  std::string("SYMTAB2GB ") + CBMC_VERSION}
33 {
34 }
35 
36 static inline bool failed(bool error_indicator)
37 {
38  return error_indicator;
39 }
40 
41 static void run_symtab2gb(
42  const std::vector<std::string> &symtab_filenames,
43  const std::string &gb_filename)
44 {
45  // try opening all the files first to make sure we can
46  // even read/write what we want
47  std::ofstream out_file{gb_filename, std::ios::binary};
48  if(!out_file.is_open())
49  {
50  throw system_exceptiont{"couldn't open output file '" + gb_filename + "'"};
51  }
52  std::vector<std::ifstream> symtab_files;
53  for(auto const &symtab_filename : symtab_filenames)
54  {
55  std::ifstream symtab_file{symtab_filename};
56  if(!symtab_file.is_open())
57  {
58  throw system_exceptiont{"couldn't open input file '" + symtab_filename +
59  "'"};
60  }
61  symtab_files.emplace_back(std::move(symtab_file));
62  }
63 
64  stream_message_handlert message_handler{std::cerr};
65 
66  auto const symtab_language = new_json_symtab_language();
67  symtab_language->set_message_handler(message_handler);
68 
69  goto_modelt linked_goto_model{};
70 
71  for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
72  {
73  auto const &symtab_filename = symtab_filenames[ix];
74  auto &symtab_file = symtab_files[ix];
75  if(failed(symtab_language->parse(symtab_file, symtab_filename)))
76  {
78  "failed to parse symbol table from file '" + symtab_filename + "'"};
79  }
80  symbol_tablet symtab{};
81  if(failed(symtab_language->typecheck(symtab, "<unused>")))
82  {
84  "failed to typecheck symbol table from file '" + symtab_filename + "'"};
85  }
87  goto_modelt goto_model{};
88  goto_model.symbol_table = symtab;
89  goto_convert(goto_model, message_handler);
90  link_goto_model(linked_goto_model, goto_model, message_handler);
91  }
92  if(failed(write_goto_binary(out_file, linked_goto_model)))
93  {
94  throw system_exceptiont{"failed to write goto binary to " + gb_filename};
95  }
96 }
97 
99 {
100  if(cmdline.isset("version"))
101  {
102  log.status() << CBMC_VERSION << '\n';
103  return CPROVER_EXIT_SUCCESS;
104  }
105  if(cmdline.args.empty())
106  {
108  "expect at least one input file", "<json-symtab-file>"};
109  }
110  std::vector<std::string> symtab_filenames = cmdline.args;
111  std::string gb_filename = "a.out";
113  {
115  }
116  config.set(cmdline);
117  run_symtab2gb(symtab_filenames, gb_filename);
118  return CPROVER_EXIT_SUCCESS;
119 }
120 
122 {
123  log.status()
124  << '\n'
125  << banner_string("symtab2gb", CBMC_VERSION) << '\n'
126  << align_center_with_border("Copyright (C) 2019") << '\n'
127  << align_center_with_border("Diffblue Ltd.") << '\n'
128  << align_center_with_border("info@diffblue.com") << '\n'
129  << '\n'
130  << "Usage: Purpose:\n"
131  << '\n'
132  << "symtab2gb [-?] [-h] [--help] show help\n"
133  "symtab2gb compile .json_symtabs\n"
134  " <json-symtab-file>+ to a single goto-binary\n"
135  " [--out <outfile>]\n\n"
136  "<json-symtab-file> a CBMC symbol table in\n"
137  " JSON format\n"
138  "--out <outfile> specify the filename of\n"
139  " the resulting binary\n"
140  " (default: a.out)\n"
141  << messaget::eom;
142 }
cmdlinet::args
argst args
Definition: cmdline.h:143
exception_utils.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
parse_options_baset
Definition: parse_options.h:20
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
messaget::status
mstreamt & status() const
Definition: message.h:414
optional.h
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
symtab2gb_parse_optionst::doit
int doit() override
Definition: symtab2gb_parse_options.cpp:98
invariant.h
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
messaget::eom
static eomt eom
Definition: message.h:297
symtab2gb_parse_optionst::help
void help() override
Definition: symtab2gb_parse_options.cpp:121
version.h
write_goto_binary.h
Write GOTO binaries.
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1863
CBMC_VERSION
const char * CBMC_VERSION
new_json_symtab_language
std::unique_ptr< languaget > new_json_symtab_language()
Definition: json_symtab_language.h:73
symtab2gb_parse_options.h
symtab2gb_parse_optionst::symtab2gb_parse_optionst
symtab2gb_parse_optionst(int argc, const char *argv[])
Definition: symtab2gb_parse_options.cpp:28
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
failed
static bool failed(bool error_indicator)
Definition: symtab2gb_parse_options.cpp:36
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
system_exceptiont
Thrown when some external system fails unexpectedly.
Definition: exception_utils.h:61
SYMTAB2GB_OPTIONS
#define SYMTAB2GB_OPTIONS
Definition: symtab2gb_parse_options.h:18
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1229
config
configt config
Definition: config.cpp:24
parse_options_baset::log
messaget log
Definition: parse_options.h:43
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.
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:206
config.h
run_symtab2gb
static void run_symtab2gb(const std::vector< std::string > &symtab_filenames, const std::string &gb_filename)
Definition: symtab2gb_parse_options.cpp:41
goto_convert_functions.h
Goto Programs with Functions.
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
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
json_symtab_language.h
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
SYMTAB2GB_OUT_FILE_OPT
#define SYMTAB2GB_OUT_FILE_OPT
Definition: symtab2gb_parse_options.h:14
stream_message_handlert
Definition: message.h:111