cprover
Loading...
Searching...
No Matches
symtab2gb_parse_options.cpp
Go to the documentation of this file.
1/******************************************************************\
2
3Module: symtab2gb_parse_options
4
5Author: Diffblue Ltd.
6
7\******************************************************************/
8
10
11#include <fstream>
12#include <iostream>
13#include <string>
14
16
20
22#include <langapi/mode.h>
23
24#include <linking/linking.h>
25
26#include <util/config.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
39static inline bool failed(bool error_indicator)
40{
41 return error_indicator;
42}
43
44static 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';
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 }
137 run_symtab2gb(symtab_filenames, gb_filename);
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.
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
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.
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
STL namespace.
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.