Skip to content

Commit 11c4c40

Browse files
hannes-steffenhagen-diffbluehannes-steffenhagen-diffblue
committed
FIX: use parse_options_baset to parse command line options
1 parent bd8edb1 commit 11c4c40

File tree

4 files changed

+171
-111
lines changed

4 files changed

+171
-111
lines changed

‎src/symtab2gb/CMakeLists.txt

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,8 @@
1-
add_executable(symtab2gb symtab2gb_main.cpp)
1+
add_executable(symtab2gb
2+
symtab2gb_main.cpp
3+
symtab2gb_parse_options.cpp
4+
symtab2gb_parse_options.h)
5+
26
generic_includes(symtab2gb)
37

48
target_link_libraries(symtab2gb

‎src/symtab2gb/symtab2gb_main.cpp

Lines changed: 4 additions & 110 deletions
Original file line numberDiff line numberDiff line change
@@ -9,116 +9,10 @@ Author: Diffblue Ltd.
99
/// \file
1010
/// symtab2gb Main Module
1111

12-
#include <fstream>
13-
#include <goto-programs/goto_convert_functions.h>
14-
#include <goto-programs/goto_model.h>
15-
#include <goto-programs/link_goto_model.h>
16-
#include <goto-programs/write_goto_binary.h>
17-
#include <iostream>
18-
#include <json-symtab-language/json_symtab_language.h>
19-
#include <string>
20-
#include <util/exception_utils.h>
21-
#include <util/invariant.h>
22-
#include <util/optional.h>
12+
#include "symtab2gb_parse_options.h"
2313

24-
static inline bool failed(bool error_indicator)
14+
int main(int argc, const char *argv[])
2515
{
26-
return error_indicator;
27-
}
28-
29-
static void run_symtab2gb(
30-
const std::vector<std::string> &symtab_filenames,
31-
const std::string &gb_filename)
32-
{
33-
// try opening all the files first to make sure we can
34-
// even read/write what we want
35-
auto out_file = std::ofstream{gb_filename};
36-
if(!out_file.is_open())
37-
{
38-
throw system_exceptiont{"couldn't open output file `" + gb_filename + "'"};
39-
}
40-
std::vector<std::ifstream> symtab_files;
41-
for(auto const &symtab_filename : symtab_filenames)
42-
{
43-
auto symtab_file = std::ifstream{symtab_filename};
44-
if(!symtab_file.is_open())
45-
{
46-
throw system_exceptiont{"couldn't open input file `" + symtab_filename +
47-
"'"};
48-
}
49-
symtab_files.emplace_back(std::move(symtab_file));
50-
}
51-
52-
auto message_handler = stream_message_handlert{std::cerr};
53-
54-
auto const symtab_language = new_json_symtab_language();
55-
symtab_language->set_message_handler(message_handler);
56-
57-
auto linked_goto_model = goto_modelt{};
58-
59-
for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
60-
{
61-
auto const &symtab_filename = symtab_filenames[ix];
62-
auto &symtab_file = symtab_files[ix];
63-
if(failed(symtab_language->parse(symtab_file, symtab_filename)))
64-
{
65-
throw invalid_source_file_exceptiont{
66-
"failed to parse symbol table from file `" + symtab_filename + "'"};
67-
}
68-
auto symtab = symbol_tablet{};
69-
if(failed(symtab_language->typecheck(symtab, "<unused>")))
70-
{
71-
throw invalid_source_file_exceptiont{
72-
"failed to typecheck symbol table from file `" + symtab_filename + "'"};
73-
}
74-
auto goto_model = goto_modelt{};
75-
goto_model.symbol_table = symtab;
76-
goto_convert(goto_model, message_handler);
77-
link_goto_model(linked_goto_model, goto_model, message_handler);
78-
}
79-
if(failed(write_goto_binary(out_file, linked_goto_model)))
80-
{
81-
throw system_exceptiont{"failed to write goto binary to " + gb_filename};
82-
}
83-
}
84-
85-
int main(int argc, char *argv[])
86-
{
87-
PRECONDITION(argc > 0);
88-
auto const executable_name = argv[0];
89-
try
90-
{
91-
if(argc < 2)
92-
{
93-
throw invalid_command_line_argument_exceptiont{
94-
"expect input file as first argument", "<positional>"};
95-
}
96-
std::vector<std::string> symtab_filenames;
97-
optionalt<std::string> gb_file;
98-
for(int i = 1; i < argc; ++i)
99-
{
100-
if(argv[i] == std::string("--out"))
101-
{
102-
if(i + 1 >= argc)
103-
{
104-
throw invalid_command_line_argument_exceptiont{
105-
"expected output file name", "--out"};
106-
}
107-
gb_file = std::string(argv[i + 1]);
108-
++i;
109-
}
110-
else
111-
{
112-
symtab_filenames.emplace_back(argv[i]);
113-
}
114-
}
115-
auto const gb_filename = gb_file.has_value() ? gb_file.value() : "a.out";
116-
run_symtab2gb(symtab_filenames, gb_filename);
117-
}
118-
catch(const cprover_exception_baset &exception)
119-
{
120-
std::cerr << executable_name << ":\n" << exception.what() << std::endl;
121-
return EXIT_FAILURE;
122-
}
123-
return EXIT_SUCCESS;
16+
symtab2gb_parse_optionst parse_options{argc, argv};
17+
return parse_options.main();
12418
}

‎src/symtab2gb/symtab2gb_parse_options.cpp

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
/******************************************************************\
2+
3+
Module: symtab2gb_parse_options
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#include "symtab2gb_parse_options.h"
10+
11+
#include <fstream>
12+
#include <iostream>
13+
#include <string>
14+
15+
#include <goto-programs/goto_convert_functions.h>
16+
#include <goto-programs/goto_model.h>
17+
#include <goto-programs/link_goto_model.h>
18+
#include <goto-programs/write_goto_binary.h>
19+
#include <json-symtab-language/json_symtab_language.h>
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+
26+
symtab2gb_parse_optionst::symtab2gb_parse_optionst(int argc, const char *argv[])
27+
: parse_options_baset{SYMTAB2GB_OPTIONS,
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};
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+
{
75+
throw invalid_source_file_exceptiont{
76+
"failed to parse symbol table from file `" + symtab_filename + "'"};
77+
}
78+
symbol_tablet symtab{};
79+
if(failed(symtab_language->typecheck(symtab, "<unused>")))
80+
{
81+
throw invalid_source_file_exceptiont{
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+
95+
int symtab2gb_parse_optionst::doit()
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+
{
104+
throw invalid_command_line_argument_exceptiont{
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";
109+
if(cmdline.isset(SYMTAB2GB_OUT_FILE_OPT))
110+
{
111+
gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT);
112+
}
113+
run_symtab2gb(symtab_filenames, gb_filename);
114+
return CPROVER_EXIT_SUCCESS;
115+
}
116+
117+
void symtab2gb_parse_optionst::help()
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("[email protected]") << '\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+
}

‎src/symtab2gb/symtab2gb_parse_options.h

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#ifndef CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H
2+
#define CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H
3+
4+
#include <util/parse_options.h>
5+
6+
#define SYMTAB2GB_OUT_FILE_OPT "out"
7+
8+
// clang-format off
9+
10+
#define SYMTAB2GB_OPTIONS \
11+
"(" SYMTAB2GB_OUT_FILE_OPT "):" \
12+
// end options
13+
14+
// clang-format on
15+
16+
class symtab2gb_parse_optionst : public parse_options_baset
17+
{
18+
public:
19+
symtab2gb_parse_optionst(int argc, const char *argv[]);
20+
void help() override;
21+
int doit() override;
22+
};
23+
24+
#endif // CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H

0 commit comments

Comments
 (0)