Skip to content

Commit c7bb936

Browse files
danpoedanpoe
authored
Merge pull request #5265 from danpoe/refactor/get-goto-model
Function to get a goto model from a C program for use in unit tests
2 parents 2e0a7f0 + 174f8f3 commit c7bb936

File tree

7 files changed

+172
-60
lines changed

7 files changed

+172
-60
lines changed

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \
1616
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
1717
big-int/big-int.cpp \
1818
compound_block_locations.cpp \
19+
get_goto_model_from_c_test.cpp \
1920
goto-checker/report_util/is_property_less_than.cpp \
2021
goto-instrument/cover_instrument.cpp \
2122
goto-instrument/cover/cover_only.cpp \

‎unit/get_goto_model_from_c_test.cpp

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
/*******************************************************************\
2+
3+
Module: Get goto model test
4+
5+
Author: Daniel Poetzl
6+
7+
\*******************************************************************/
8+
9+
#include <testing-utils/get_goto_model_from_c.h>
10+
#include <testing-utils/use_catch.h>
11+
12+
TEST_CASE("Get goto model from C test", "[core]")
13+
{
14+
const std::string code =
15+
"int g;"
16+
"void f(int a) { int b; }"
17+
"void main() {}";
18+
19+
const auto goto_model = get_goto_model_from_c(code);
20+
21+
const auto &function_map = goto_model.goto_functions.function_map;
22+
23+
REQUIRE(function_map.find("main") != function_map.end());
24+
REQUIRE(function_map.find(CPROVER_PREFIX "_start") != function_map.end());
25+
REQUIRE(function_map.find("f") != function_map.end());
26+
27+
const auto &main_instructions = function_map.at("main").body.instructions;
28+
REQUIRE(!main_instructions.empty());
29+
30+
const auto &f_instructions = function_map.at("f").body.instructions;
31+
REQUIRE(f_instructions.size() >= 2);
32+
33+
const auto &symbol_table = goto_model.symbol_table;
34+
35+
REQUIRE(symbol_table.has_symbol("main"));
36+
REQUIRE(symbol_table.has_symbol(CPROVER_PREFIX "_start"));
37+
REQUIRE(symbol_table.has_symbol("g"));
38+
REQUIRE(symbol_table.has_symbol("f::a"));
39+
REQUIRE(symbol_table.has_symbol("f::1::b"));
40+
}

‎unit/json_symbol_table.cpp

Lines changed: 3 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@
2323
#include <util/options.h>
2424
#include <util/symbol_table.h>
2525

26+
#include <testing-utils/get_goto_model_from_c.h>
2627
#include <testing-utils/message.h>
2728
#include <testing-utils/use_catch.h>
2829

@@ -49,67 +50,11 @@ class test_ui_message_handlert : public ui_message_handlert
4950
json_stream_arrayt json_stream_array;
5051
};
5152

52-
void get_goto_model(std::istream &in, goto_modelt &goto_model)
53-
{
54-
optionst options;
55-
cbmc_parse_optionst::set_default_options(options);
56-
57-
messaget null_message(null_message_handler);
58-
59-
language_filest language_files;
60-
language_files.set_message_handler(null_message_handler);
61-
62-
std::string filename;
63-
64-
language_filet &language_file = language_files.add_file(filename);
65-
66-
language_file.language = get_default_language();
67-
68-
languaget &language = *language_file.language;
69-
language.set_message_handler(null_message_handler);
70-
language.set_language_options(options);
71-
72-
{
73-
bool r = language.parse(in, filename);
74-
REQUIRE(!r);
75-
}
76-
77-
language_file.get_modules();
78-
79-
{
80-
bool r = language_files.typecheck(goto_model.symbol_table);
81-
REQUIRE(!r);
82-
}
83-
84-
REQUIRE(!goto_model.symbol_table.has_symbol(goto_functionst::entry_point()));
85-
86-
{
87-
bool r = language_files.generate_support_functions(goto_model.symbol_table);
88-
REQUIRE(!r);
89-
}
90-
91-
goto_convert(
92-
goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
93-
}
94-
9553
TEST_CASE("json symbol table read/write consistency")
9654
{
97-
register_language(new_ansi_c_language);
98-
99-
cmdlinet cmdline;
100-
config.main = std::string("main");
101-
config.set(cmdline);
102-
103-
goto_modelt goto_model;
104-
10555
// Get symbol table associated with goto program
106-
107-
{
108-
std::string program = "int main() { return 0; }\n";
109-
110-
std::istringstream in(program);
111-
get_goto_model(in, goto_model);
112-
}
56+
const std::string program = "int main() { return 0; }\n";
57+
const auto goto_model = get_goto_model_from_c(program);
11358

11459
const symbol_tablet &symbol_table1 = goto_model.symbol_table;
11560

‎unit/testing-utils/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
SRC = \
22
call_graph_test_utils.cpp \
33
free_form_cmdline.cpp \
4+
get_goto_model_from_c.cpp \
45
invariant.cpp \
56
message.cpp \
67
require_expr.cpp \

‎unit/testing-utils/get_goto_model_from_c.cpp

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
/*******************************************************************\
2+
3+
Module: Get goto model
4+
5+
Author: Daniel Poetzl
6+
7+
\*******************************************************************/
8+
9+
#include "get_goto_model_from_c.h"
10+
11+
#include <ansi-c/ansi_c_language.h>
12+
13+
#include <goto-programs/goto_convert_functions.h>
14+
15+
#include <langapi/language_file.h>
16+
#include <langapi/mode.h>
17+
18+
#include <util/cmdline.h>
19+
#include <util/config.h>
20+
#include <util/exception_utils.h>
21+
#include <util/invariant.h>
22+
#include <util/message.h>
23+
#include <util/options.h>
24+
#include <util/symbol_table.h>
25+
26+
#include <testing-utils/message.h>
27+
28+
goto_modelt get_goto_model_from_c(std::istream &in)
29+
{
30+
{
31+
const bool has_language = get_language_from_mode(ID_C) != nullptr;
32+
33+
if(!has_language)
34+
{
35+
register_language(new_ansi_c_language);
36+
}
37+
}
38+
39+
{
40+
cmdlinet cmdline;
41+
42+
config = configt{};
43+
config.main = std::string("main");
44+
config.set(cmdline);
45+
}
46+
47+
language_filest language_files;
48+
language_files.set_message_handler(null_message_handler);
49+
50+
language_filet &language_file = language_files.add_file("");
51+
52+
language_file.language = get_language_from_mode(ID_C);
53+
CHECK_RETURN(language_file.language);
54+
55+
languaget &language = *language_file.language;
56+
language.set_message_handler(null_message_handler);
57+
58+
{
59+
const bool error = language.parse(in, "");
60+
61+
if(error)
62+
throw invalid_source_file_exceptiont("parsing failed");
63+
}
64+
65+
language_file.get_modules();
66+
67+
goto_modelt goto_model;
68+
69+
{
70+
const bool error = language_files.typecheck(goto_model.symbol_table);
71+
72+
if(error)
73+
throw invalid_source_file_exceptiont("typechecking failed");
74+
}
75+
76+
{
77+
const bool error =
78+
language_files.generate_support_functions(goto_model.symbol_table);
79+
80+
if(error)
81+
throw invalid_source_file_exceptiont(
82+
"support function generation failed");
83+
}
84+
85+
goto_convert(
86+
goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
87+
88+
return goto_model;
89+
}
90+
91+
goto_modelt get_goto_model_from_c(const std::string &code)
92+
{
93+
std::istringstream in(code);
94+
return get_goto_model_from_c(in);
95+
}

‎unit/testing-utils/get_goto_model_from_c.h

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/*******************************************************************\
2+
3+
Module: Get goto model
4+
5+
Author: Daniel Poetzl
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H
10+
#define CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H
11+
12+
#include <goto-programs/goto_model.h>
13+
14+
#include <iosfwd>
15+
16+
/// Convert C program to a goto model
17+
///
18+
/// \param code: string giving the C program
19+
/// \return goto model
20+
goto_modelt get_goto_model_from_c(const std::string &code);
21+
22+
/// Convert C program to a goto model
23+
///
24+
/// \param in: input stream to read a C program from
25+
/// \return goto model
26+
goto_modelt get_goto_model_from_c(const std::istream &in);
27+
28+
#endif /* CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H_ */

‎unit/testing-utils/module_dependencies.txt

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
1+
analyses
12
ansi-c
23
catch
4+
goto-programs
5+
langapi
36
testing-utils
4-
util
5-
analyses
7+
util

0 commit comments

Comments
 (0)