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 #include <util/exception_utils.h>
21 #include <util/exit_codes.h>
22 #include <util/invariant.h>
23 #include <util/optional.h>
24 #include <util/version.h>
25 
28  argc,
29  argv,
30  std::string("SYMTAB2GB ") + CBMC_VERSION}
31 {
32 }
33 
34 static inline bool failed(bool error_indicator)
35 {
36  return error_indicator;
37 }
38 
39 static void run_symtab2gb(
40  const std::vector<std::string> &symtab_filenames,
41  const std::string &gb_filename)
42 {
43  // try opening all the files first to make sure we can
44  // even read/write what we want
45  std::ofstream out_file{gb_filename, std::ios::binary};
46  if(!out_file.is_open())
47  {
48  throw system_exceptiont{"couldn't open output file '" + gb_filename + "'"};
49  }
50  std::vector<std::ifstream> symtab_files;
51  for(auto const &symtab_filename : symtab_filenames)
52  {
53  std::ifstream symtab_file{symtab_filename};
54  if(!symtab_file.is_open())
55  {
56  throw system_exceptiont{"couldn't open input file '" + symtab_filename +
57  "'"};
58  }
59  symtab_files.emplace_back(std::move(symtab_file));
60  }
61 
62  stream_message_handlert message_handler{std::cerr};
63 
64  auto const symtab_language = new_json_symtab_language();
65  symtab_language->set_message_handler(message_handler);
66 
67  goto_modelt linked_goto_model{};
68 
69  for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
70  {
71  auto const &symtab_filename = symtab_filenames[ix];
72  auto &symtab_file = symtab_files[ix];
73  if(failed(symtab_language->parse(symtab_file, symtab_filename)))
74  {
76  "failed to parse symbol table from file '" + symtab_filename + "'"};
77  }
78  symbol_tablet symtab{};
79  if(failed(symtab_language->typecheck(symtab, "<unused>")))
80  {
82  "failed to typecheck symbol table from file '" + symtab_filename + "'"};
83  }
84  goto_modelt goto_model{};
85  goto_model.symbol_table = symtab;
86  goto_convert(goto_model, message_handler);
87  link_goto_model(linked_goto_model, goto_model, message_handler);
88  }
89  if(failed(write_goto_binary(out_file, linked_goto_model)))
90  {
91  throw system_exceptiont{"failed to write goto binary to " + gb_filename};
92  }
93 }
94 
96 {
97  if(cmdline.isset("version"))
98  {
99  log.status() << CBMC_VERSION << '\n';
100  return CPROVER_EXIT_SUCCESS;
101  }
102  if(cmdline.args.empty())
103  {
105  "expect at least one input file", "<json-symtab-file>"};
106  }
107  std::vector<std::string> symtab_filenames = cmdline.args;
108  std::string gb_filename = "a.out";
110  {
112  }
113  run_symtab2gb(symtab_filenames, gb_filename);
114  return CPROVER_EXIT_SUCCESS;
115 }
116 
118 {
119  log.status()
120  << '\n'
121  << banner_string("symtab2gb", CBMC_VERSION) << '\n'
122  << align_center_with_border("Copyright (C) 2019") << '\n'
123  << align_center_with_border("Diffblue Ltd.") << '\n'
124  << align_center_with_border("info@diffblue.com") << '\n'
125  << '\n'
126  << "Usage: Purpose:\n"
127  << '\n'
128  << "symtab2gb [-?] [-h] [--help] show help\n"
129  "symtab2gb compile .json_symtabs\n"
130  " <json-symtab-file>+ to a single goto-binary\n"
131  " [--out <outfile>]\n\n"
132  "<json-symtab-file> a CBMC symbol table in\n"
133  " JSON format\n"
134  "--out <outfile> specify the filename of\n"
135  " the resulting binary\n"
136  " (default: a.out)\n"
137  << messaget::eom;
138 }
cmdlinet::args
argst args
Definition: cmdline.h:91
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:95
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:117
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:1846
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:26
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:34
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
parse_options_baset::log
messaget log
Definition: parse_options.h:43
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:204
run_symtab2gb
static void run_symtab2gb(const std::vector< std::string > &symtab_filenames, const std::string &gb_filename)
Definition: symtab2gb_parse_options.cpp:39
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