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 
20 
22 #include <langapi/mode.h>
23 
24 #include <linking/linking.h>
25 
26 #include <util/config.h>
27 #include <util/exception_utils.h>
28 #include <util/exit_codes.h>
29 #include <util/version.h>
30 
33  argc,
34  argv,
35  std::string("SYMTAB2GB ") + CBMC_VERSION}
36 {
37 }
38 
39 static inline bool failed(bool error_indicator)
40 {
41  return error_indicator;
42 }
43 
44 static void run_symtab2gb(
45  const std::vector<std::string> &symtab_filenames,
46  const std::string &gb_filename)
47 {
48  // try opening all the files first to make sure we can
49  // even read/write what we want
50  std::ofstream out_file{gb_filename, std::ios::binary};
51  if(!out_file.is_open())
52  {
53  throw system_exceptiont{"couldn't open output file '" + gb_filename + "'"};
54  }
55  std::vector<std::ifstream> symtab_files;
56  for(auto const &symtab_filename : symtab_filenames)
57  {
58  std::ifstream symtab_file{symtab_filename};
59  if(!symtab_file.is_open())
60  {
61  throw system_exceptiont{"couldn't open input file '" + symtab_filename +
62  "'"};
63  }
64  symtab_files.emplace_back(std::move(symtab_file));
65  }
66 
67  stream_message_handlert message_handler{std::cerr};
68 
69  auto const symtab_language = new_json_symtab_language();
70  symtab_language->set_message_handler(message_handler);
71 
72  symbol_tablet linked_symbol_table;
73 
74  for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
75  {
76  auto const &symtab_filename = symtab_filenames[ix];
77  auto &symtab_file = symtab_files[ix];
78  if(failed(symtab_language->parse(symtab_file, symtab_filename)))
79  {
81  "failed to parse symbol table from file '" + symtab_filename + "'"};
82  }
83  symbol_tablet symtab{};
84  if(failed(symtab_language->typecheck(symtab, "<unused>")))
85  {
87  "failed to typecheck symbol table from file '" + symtab_filename + "'"};
88  }
90 
91  if(failed(linking(linked_symbol_table, symtab, message_handler)))
92  {
93  throw invalid_source_file_exceptiont{"failed to link `" +
94  symtab_filename + "'"};
95  }
96  }
97 
98  goto_modelt linked_goto_model;
99  linked_goto_model.symbol_table.swap(linked_symbol_table);
100  goto_convert(linked_goto_model, message_handler);
101 
102  if(failed(write_goto_binary(out_file, linked_goto_model)))
103  {
104  throw system_exceptiont{"failed to write goto binary to " + gb_filename};
105  }
106 }
107 
109 {
110  // As this is a converter and linker it only really needs to support
111  // the JSON symtab front-end.
113  // Workaround to allow external front-ends to use "C" mode
115 }
116 
118 {
119  if(cmdline.isset("version"))
120  {
121  log.status() << CBMC_VERSION << '\n';
122  return CPROVER_EXIT_SUCCESS;
123  }
124  if(cmdline.args.empty())
125  {
127  "expect at least one input file", "<json-symtab-file>"};
128  }
129  std::vector<std::string> symtab_filenames = cmdline.args;
130  std::string gb_filename = "a.out";
132  {
134  }
136  config.set(cmdline);
137  run_symtab2gb(symtab_filenames, gb_filename);
138  return CPROVER_EXIT_SUCCESS;
139 }
140 
142 {
143  log.status()
144  << '\n'
145  << banner_string("symtab2gb", CBMC_VERSION) << '\n'
146  << align_center_with_border("Copyright (C) 2019") << '\n'
147  << align_center_with_border("Diffblue Ltd.") << '\n'
148  << align_center_with_border("info@diffblue.com") << '\n'
149  << '\n'
150  << "Usage: Purpose:\n"
151  << '\n'
152  << "symtab2gb [-?] [-h] [--help] show help\n"
153  "symtab2gb compile .json_symtabs\n"
154  " <json-symtab-file>+ to a single goto-binary\n"
155  " [--out <outfile>]\n\n"
156  "<json-symtab-file> a CBMC symbol table in\n"
157  " JSON format\n"
158  "--out <outfile> specify the filename of\n"
159  " the resulting binary\n"
160  " (default: a.out)\n"
161  << messaget::eom;
162 }
std::unique_ptr< languaget > new_ansi_c_language()
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:145
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1254
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Thrown when we can't handle something in an input source file.
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
The symbol table.
Definition: symbol_table.h:14
void swap(symbol_tablet &other)
Swap symbol maps between two symbol tables.
Definition: symbol_table.h:74
symtab2gb_parse_optionst(int argc, const char *argv[])
Thrown when some external system fails unexpectedly.
configt config
Definition: config.cpp:25
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
Symbol Table + CFG.
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:206
std::unique_ptr< languaget > new_json_symtab_language()
bool linking(symbol_tablet &dest_symbol_table, const symbol_tablet &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
Definition: linking.cpp:1470
ANSI-C Linking.
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
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
static void run_symtab2gb(const std::vector< std::string > &symtab_filenames, const std::string &gb_filename)
static bool failed(bool error_indicator)
#define SYMTAB2GB_OPTIONS
#define SYMTAB2GB_OUT_FILE_OPT
const char * CBMC_VERSION
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.
Write GOTO binaries.