CBMC
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 <util/config.h>
13#include <util/exit_codes.h>
14#include <util/help_formatter.h>
15#include <util/json.h>
16#include <util/version.h>
17
20
25#include <json/json_parser.h>
26#include <langapi/mode.h>
27#include <linking/linking.h>
28
29#include <fstream>
30#include <iostream>
31#include <string>
32
35 argc,
36 argv,
37 std::string("SYMTAB2GB ") + CBMC_VERSION}
38{
39}
40
41static inline bool failed(bool error_indicator)
42{
43 return error_indicator;
44}
45
46static void run_symtab2gb(
47 const std::vector<std::string> &symtab_filenames,
48 const std::string &gb_filename,
49 const std::string &goto_functions_filename_or_empty,
50 const std::string &cmdline_verbosity)
51{
52 // try opening all the files first to make sure we can
53 // even read/write what we want
54 std::ofstream out_file{gb_filename, std::ios::binary};
55 if(!out_file.is_open())
56 {
57 throw system_exceptiont{"couldn't open output file '" + gb_filename + "'"};
58 }
59 std::vector<std::ifstream> symtab_files;
60 for(auto const &symtab_filename : symtab_filenames)
61 {
62 std::ifstream symtab_file{symtab_filename};
63 if(!symtab_file.is_open())
64 {
65 throw system_exceptiont{"couldn't open input file '" + symtab_filename +
66 "'"};
67 }
68 symtab_files.emplace_back(std::move(symtab_file));
69 }
70
71 // Open goto functions file if specified
72 std::optional<std::ifstream> goto_functions_file;
74 {
76 if(!goto_functions_file->is_open())
77 {
79 "couldn't open goto functions file '" +
81 }
82 }
83
84 stream_message_handlert message_handler{std::cerr};
86 cmdline_verbosity, messaget::M_STATUS, message_handler);
87
89
91
92 for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
93 {
94 auto const &symtab_filename = symtab_filenames[ix];
96 if(failed(
97 symtab_language->parse(symtab_file, symtab_filename, message_handler)))
98 {
99 source_locationt source_location;
100 source_location.set_file(symtab_filename);
102 "failed to parse symbol table", source_location};
103 }
105 if(failed(symtab_language->typecheck(symtab, "<unused>", message_handler)))
106 {
107 source_locationt source_location;
108 source_location.set_file(symtab_filename);
110 "failed to typecheck symbol table", source_location};
111 }
113
114 if(failed(linking(linked_symbol_table, symtab, message_handler)))
115 {
117 "failed to link `" + symtab_filename + "'"};
118 }
119 }
120
122 linked_goto_model.symbol_table.swap(linked_symbol_table);
123
124 // If goto functions file is specified, parse it and use those functions
125 if(goto_functions_file.has_value())
126 {
127 jsont json;
131 message_handler,
132 json)))
133 {
134 source_locationt source_location;
137 "failed to parse JSON", source_location};
138 }
140 }
141
142 // Convert symbols to goto functions
143 goto_convert(linked_goto_model, message_handler);
144
146 {
147 throw system_exceptiont{"failed to write goto binary to " + gb_filename};
148 }
149}
150
152{
153 // As this is a converter and linker it only really needs to support
154 // the JSON symtab front-end.
156 // Workaround to allow external front-ends to use "C" mode
158}
159
161{
162 if(cmdline.isset("version"))
163 {
164 log.status() << CBMC_VERSION << '\n';
166 }
167 if(cmdline.args.empty())
168 {
170 "expect at least one input file", "<json-symtab-file>"};
171 }
172 std::vector<std::string> symtab_filenames = cmdline.args;
173 std::string gb_filename = "a.out";
175 {
177 }
178
181
188 cmdline.get_value("verbosity"));
190}
191
193{
194 log.status() << '\n'
195 << banner_string("symtab2gb", CBMC_VERSION) << '\n'
196 << align_center_with_border("Copyright (C) 2019") << '\n'
197 << align_center_with_border("Diffblue Ltd.") << '\n'
198 << align_center_with_border("info@diffblue.com") << '\n';
199
201 "\n"
202 "Usage: \tPurpose:\n"
203 "\n"
204 " {bsymtab2gb} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
205 " {bsymtab2gb} [options] {ujson-symtab-file...} \t compile CBMC symbol"
206 " table(s) in JSON format to a single goto-binary\n"
207 "\n"
208 "Options:\n"
209 " {y--out} {uoutfile} \t specify the filename of the resulting binary"
210 " (default: a.out)\n"
211 " {y--goto-functions} {ufile} \t specify a file containing JSON-encoded"
212 " goto functions\n"
213 " {y--verbosity} {u#} \t verbosity level\n");
215}
std::unique_ptr< languaget > new_ansi_c_language()
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:154
bool set(const cmdlinet &cmdline)
Definition config.cpp:863
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1363
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.
Definition json.h:27
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
@ M_STATUS
Definition message.h:169
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
void set_file(const irep_idt &file)
The symbol table.
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)
void goto_functions_from_json(const jsont &json, goto_functionst &goto_functions)
Deserialize goto_functionst from JSON.
JSON goto_functions deserialization.
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
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:1130
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 json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
static void run_symtab2gb(const std::vector< std::string > &symtab_filenames, const std::string &gb_filename, const std::string &goto_functions_filename_or_empty, const std::string &cmdline_verbosity)
static bool failed(bool error_indicator)
#define SYMTAB2GB_OPTIONS
#define SYMTAB2GB_OUT_FILE_OPT
#define SYMTAB2GB_GOTO_FUNCTIONS_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.