CBMC
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 <util/config.h>
12 #include <util/exception_utils.h>
13 #include <util/exit_codes.h>
14 #include <util/help_formatter.h>
15 #include <util/version.h>
16 
20 
21 #include <ansi-c/ansi_c_language.h>
23 #include <langapi/mode.h>
24 #include <linking/linking.h>
25 
26 #include <fstream>
27 #include <iostream>
28 #include <string>
29 
32  argc,
33  argv,
34  std::string("SYMTAB2GB ") + CBMC_VERSION}
35 {
36 }
37 
38 static inline bool failed(bool error_indicator)
39 {
40  return error_indicator;
41 }
42 
43 static void run_symtab2gb(
44  const std::vector<std::string> &symtab_filenames,
45  const std::string &gb_filename,
46  const std::string &cmdline_verbosity)
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};
69  cmdline_verbosity, messaget::M_STATISTICS, message_handler);
70 
71  auto const symtab_language = new_json_symtab_language();
72 
73  symbol_tablet linked_symbol_table;
74 
75  for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
76  {
77  auto const &symtab_filename = symtab_filenames[ix];
78  auto &symtab_file = symtab_files[ix];
79  if(failed(
80  symtab_language->parse(symtab_file, symtab_filename, message_handler)))
81  {
82  source_locationt source_location;
83  source_location.set_file(symtab_filename);
85  "failed to parse symbol table", source_location};
86  }
87  symbol_tablet symtab{};
88  if(failed(symtab_language->typecheck(symtab, "<unused>", message_handler)))
89  {
90  source_locationt source_location;
91  source_location.set_file(symtab_filename);
93  "failed to typecheck symbol table", source_location};
94  }
96 
97  if(failed(linking(linked_symbol_table, symtab, message_handler)))
98  {
100  "failed to link `" + symtab_filename + "'"};
101  }
102  }
103 
104  goto_modelt linked_goto_model;
105  linked_goto_model.symbol_table.swap(linked_symbol_table);
106  goto_convert(linked_goto_model, message_handler);
107 
108  if(failed(write_goto_binary(out_file, linked_goto_model)))
109  {
110  throw system_exceptiont{"failed to write goto binary to " + gb_filename};
111  }
112 }
113 
115 {
116  // As this is a converter and linker it only really needs to support
117  // the JSON symtab front-end.
119  // Workaround to allow external front-ends to use "C" mode
121 }
122 
124 {
125  if(cmdline.isset("version"))
126  {
127  log.status() << CBMC_VERSION << '\n';
128  return CPROVER_EXIT_SUCCESS;
129  }
130  if(cmdline.args.empty())
131  {
133  "expect at least one input file", "<json-symtab-file>"};
134  }
135  std::vector<std::string> symtab_filenames = cmdline.args;
136  std::string gb_filename = "a.out";
138  {
140  }
142  config.set(cmdline);
143  run_symtab2gb(symtab_filenames, gb_filename, cmdline.get_value("verbosity"));
144  return CPROVER_EXIT_SUCCESS;
145 }
146 
148 {
149  log.status() << '\n'
150  << banner_string("symtab2gb", CBMC_VERSION) << '\n'
151  << align_center_with_border("Copyright (C) 2019") << '\n'
152  << align_center_with_border("Diffblue Ltd.") << '\n'
153  << align_center_with_border("info@diffblue.com") << '\n';
154 
156  "\n"
157  "Usage: \tPurpose:\n"
158  "\n"
159  " {bsymtab2gb} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
160  " {bsymtab2gb} [options] {ujson-symtab-file...} \t compile CBMC symbol"
161  " table(s) in JSON format to a single goto-binary\n"
162  "\n"
163  "Options:\n"
164  " {y--out} {uoutfile} \t specify the filename of the resulting binary"
165  " (default: a.out)\n"
166  " {y--verbosity} {u#} \t verbosity level\n");
167  log.status() << messaget::eom;
168 }
std::unique_ptr< languaget > new_ansi_c_language()
configt config
Definition: config.cpp:25
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:151
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
void set_from_symbol_table(const symbol_table_baset &)
Definition: config.cpp:1266
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Thrown when user-provided input cannot be processed.
Thrown when we can't handle something in an input source file.
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:105
mstreamt & status() const
Definition: message.h:414
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
void set_file(const irep_idt &file)
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.
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.
Help Formatter.
static help_formattert help_formatter(const std::string &s)
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:187
std::unique_ptr< languaget > new_json_symtab_language()
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &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:1618
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, const std::string &cmdline_verbosity)
static bool failed(bool error_indicator)
#define SYMTAB2GB_OPTIONS
#define SYMTAB2GB_OUT_FILE_OPT
const char * CBMC_VERSION
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.