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 
15 #include <ansi-c/ansi_c_language.h>
16 
22 #include <langapi/mode.h>
23 
24 #include <util/config.h>
25 #include <util/exception_utils.h>
26 #include <util/exit_codes.h>
27 #include <util/version.h>
28 
31  argc,
32  argv,
33  std::string("SYMTAB2GB ") + CBMC_VERSION}
34 {
35 }
36 
37 static inline bool failed(bool error_indicator)
38 {
39  return error_indicator;
40 }
41 
42 static void run_symtab2gb(
43  const std::vector<std::string> &symtab_filenames,
44  const std::string &gb_filename)
45 {
46  // try opening all the files first to make sure we can
47  // even read/write what we want
48  std::ofstream out_file{gb_filename, std::ios::binary};
49  if(!out_file.is_open())
50  {
51  throw system_exceptiont{"couldn't open output file '" + gb_filename + "'"};
52  }
53  std::vector<std::ifstream> symtab_files;
54  for(auto const &symtab_filename : symtab_filenames)
55  {
56  std::ifstream symtab_file{symtab_filename};
57  if(!symtab_file.is_open())
58  {
59  throw system_exceptiont{"couldn't open input file '" + symtab_filename +
60  "'"};
61  }
62  symtab_files.emplace_back(std::move(symtab_file));
63  }
64 
65  stream_message_handlert message_handler{std::cerr};
66 
67  auto const symtab_language = new_json_symtab_language();
68  symtab_language->set_message_handler(message_handler);
69 
70  goto_modelt linked_goto_model{};
71 
72  for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
73  {
74  auto const &symtab_filename = symtab_filenames[ix];
75  auto &symtab_file = symtab_files[ix];
76  if(failed(symtab_language->parse(symtab_file, symtab_filename)))
77  {
79  "failed to parse symbol table from file '" + symtab_filename + "'"};
80  }
81  symbol_tablet symtab{};
82  if(failed(symtab_language->typecheck(symtab, "<unused>")))
83  {
85  "failed to typecheck symbol table from file '" + symtab_filename + "'"};
86  }
88  goto_modelt goto_model{};
89  goto_model.symbol_table = symtab;
90  goto_convert(goto_model, message_handler);
91  link_goto_model(linked_goto_model, goto_model, message_handler);
92  }
93  if(failed(write_goto_binary(out_file, linked_goto_model)))
94  {
95  throw system_exceptiont{"failed to write goto binary to " + gb_filename};
96  }
97 }
98 
100 {
101  // As this is a converter and linker it only really needs to support
102  // the JSON symtab front-end.
104  // Workaround to allow external front-ends to use "C" mode
106 }
107 
109 {
110  if(cmdline.isset("version"))
111  {
112  log.status() << CBMC_VERSION << '\n';
113  return CPROVER_EXIT_SUCCESS;
114  }
115  if(cmdline.args.empty())
116  {
118  "expect at least one input file", "<json-symtab-file>"};
119  }
120  std::vector<std::string> symtab_filenames = cmdline.args;
121  std::string gb_filename = "a.out";
123  {
125  }
127  config.set(cmdline);
128  run_symtab2gb(symtab_filenames, gb_filename);
129  return CPROVER_EXIT_SUCCESS;
130 }
131 
133 {
134  log.status()
135  << '\n'
136  << banner_string("symtab2gb", CBMC_VERSION) << '\n'
137  << align_center_with_border("Copyright (C) 2019") << '\n'
138  << align_center_with_border("Diffblue Ltd.") << '\n'
139  << align_center_with_border("info@diffblue.com") << '\n'
140  << '\n'
141  << "Usage: Purpose:\n"
142  << '\n'
143  << "symtab2gb [-?] [-h] [--help] show help\n"
144  "symtab2gb compile .json_symtabs\n"
145  " <json-symtab-file>+ to a single goto-binary\n"
146  " [--out <outfile>]\n\n"
147  "<json-symtab-file> a CBMC symbol table in\n"
148  " JSON format\n"
149  "--out <outfile> specify the filename of\n"
150  " the resulting binary\n"
151  " (default: a.out)\n"
152  << messaget::eom;
153 }
cmdlinet::args
argst args
Definition: cmdline.h:143
exception_utils.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
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
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:24
symtab2gb_parse_optionst::doit
int doit() override
Definition: symtab2gb_parse_options.cpp:108
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
mode.h
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:132
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:1876
CBMC_VERSION
const char * CBMC_VERSION
new_json_symtab_language
std::unique_ptr< languaget > new_json_symtab_language()
Definition: json_symtab_language.h:75
symtab2gb_parse_options.h
symtab2gb_parse_optionst::symtab2gb_parse_optionst
symtab2gb_parse_optionst(int argc, const char *argv[])
Definition: symtab2gb_parse_options.cpp:29
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:174
failed
static bool failed(bool error_indicator)
Definition: symtab2gb_parse_options.cpp:37
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:1231
config
configt config
Definition: config.cpp:25
parse_options_baset::log
messaget log
Definition: parse_options.h:46
symtab2gb_parse_optionst::register_languages
void register_languages() override
Definition: symtab2gb_parse_options.cpp:99
register_language
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:39
ansi_c_language.h
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.
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:141
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:205
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:42
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:161
SYMTAB2GB_OUT_FILE_OPT
#define SYMTAB2GB_OUT_FILE_OPT
Definition: symtab2gb_parse_options.h:14
stream_message_handlert
Definition: message.h:111