Skip to content

Commit b9914a8

Browse files
author
thk123
committed
Add some java testing utilities.
1 parent 2c175bd commit b9914a8

File tree

2 files changed

+287
-0
lines changed

2 files changed

+287
-0
lines changed

‎unit/testing-utils/java_testing_utils.cpp

+222
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,222 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test utilities
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
#include <goto-programs/goto_program.h>
10+
#include "java_testing_utils.h"
11+
12+
struct_component_assignment_locationt combine_locations(
13+
const struct_component_assignment_locationt &a,
14+
const struct_component_assignment_locationt &b)
15+
{
16+
struct_component_assignment_locationt new_locations;
17+
18+
new_locations.assignment_locations.insert(
19+
new_locations.assignment_locations.end(),
20+
a.assignment_locations.begin(),
21+
a.assignment_locations.end());
22+
23+
new_locations.assignment_locations.insert(
24+
new_locations.assignment_locations.end(),
25+
b.assignment_locations.begin(),
26+
b.assignment_locations.end());
27+
28+
return new_locations;
29+
}
30+
31+
struct_component_assignment_locationt find_struct_component_assignments(
32+
const exprt::operandst &entry_point_instructions,
33+
const irep_idt &structure_name,
34+
const irep_idt &component_name)
35+
{
36+
struct_component_assignment_locationt component_assignments;
37+
38+
for(const auto &instruction : entry_point_instructions)
39+
{
40+
const codet &assignment = to_code(instruction);
41+
INVARIANT(instruction.id() == ID_code, "All instructions must be code");
42+
if(assignment.get_statement() == ID_assign)
43+
{
44+
const code_assignt &code_assign = to_code_assign(assignment);
45+
46+
if(code_assign.lhs().id() == ID_member)
47+
{
48+
const auto &member_expr = to_member_expr(code_assign.lhs());
49+
const auto &symbol = member_expr.symbol();
50+
51+
if(
52+
symbol.get_identifier() == structure_name &&
53+
member_expr.get_component_name() == component_name)
54+
{
55+
component_assignments.assignment_locations.push_back(code_assign);
56+
}
57+
}
58+
}
59+
else if(assignment.get_statement() == ID_block)
60+
{
61+
const auto &assignments_in_block = find_struct_component_assignments(
62+
assignment.operands(), structure_name, component_name);
63+
component_assignments =
64+
combine_locations(component_assignments, assignments_in_block);
65+
}
66+
else if(assignment.get_statement() == ID_ifthenelse)
67+
{
68+
const code_ifthenelset &if_else_block =
69+
to_code_ifthenelse(to_code(assignment));
70+
const auto &assignments_in_block = find_struct_component_assignments(
71+
exprt::operandst{if_else_block.then_case()},
72+
structure_name,
73+
component_name);
74+
component_assignments =
75+
combine_locations(component_assignments, assignments_in_block);
76+
77+
if(if_else_block.has_else_case())
78+
{
79+
const auto &assignments_in_else = find_struct_component_assignments(
80+
exprt::operandst{if_else_block.else_case()},
81+
structure_name,
82+
component_name);
83+
component_assignments =
84+
combine_locations(component_assignments, assignments_in_else);
85+
}
86+
}
87+
else if(assignment.get_statement() == ID_label)
88+
{
89+
const code_labelt &label_statement = to_code_label(assignment);
90+
const auto &assignments_in_label = find_struct_component_assignments(
91+
exprt::operandst{label_statement.code()},
92+
structure_name,
93+
component_name);
94+
component_assignments =
95+
combine_locations(component_assignments, assignments_in_label);
96+
}
97+
}
98+
return component_assignments;
99+
}
100+
101+
/// Combine two pointer locations. Takes the null assignment if present in
102+
/// either (fails if present in both) and appends the non-null assignments
103+
/// \param a: The first set of assignments
104+
/// \param b: The second set of assignments
105+
/// \return The resulting assignment
106+
pointer_assignment_locationt combine_locations(
107+
const pointer_assignment_locationt &a,
108+
const pointer_assignment_locationt &b)
109+
{
110+
pointer_assignment_locationt new_locations;
111+
if(a.null_assignment.has_value())
112+
{
113+
INVARIANT(
114+
!b.null_assignment.has_value(), "Only expected one assignment to null");
115+
new_locations.null_assignment = a.null_assignment;
116+
}
117+
else if(b.null_assignment.has_value())
118+
{
119+
INVARIANT(
120+
!a.null_assignment.has_value(), "Only expected one assignment to null");
121+
new_locations.null_assignment = b.null_assignment;
122+
}
123+
124+
new_locations.non_null_assignments.insert(
125+
new_locations.non_null_assignments.end(),
126+
a.non_null_assignments.begin(),
127+
a.non_null_assignments.end());
128+
129+
new_locations.non_null_assignments.insert(
130+
new_locations.non_null_assignments.end(),
131+
b.non_null_assignments.begin(),
132+
b.non_null_assignments.end());
133+
134+
return new_locations;
135+
}
136+
137+
/// For a given variable name, gets the assignments to it in the functions
138+
/// \param pointer_name: The name of the variable
139+
/// \param instructions: The instructions to look through
140+
/// \return: A structure that contains the null assignment if found, and a
141+
/// vector of all other assignments
142+
pointer_assignment_locationt find_pointer_assignments(
143+
const irep_idt &pointer_name,
144+
const exprt::operandst &instructions)
145+
{
146+
pointer_assignment_locationt locations;
147+
for(const exprt &assignment : instructions)
148+
{
149+
const codet &statement = to_code(assignment);
150+
INVARIANT(assignment.id() == ID_code, "All instructions must be code");
151+
if(statement.get_statement() == ID_assign)
152+
{
153+
const code_assignt &code_assign = to_code_assign(to_code(assignment));
154+
if(
155+
code_assign.lhs().id() == ID_symbol &&
156+
to_symbol_expr(code_assign.lhs()).get_identifier() == pointer_name)
157+
{
158+
if(
159+
code_assign.rhs() ==
160+
null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
161+
{
162+
locations.null_assignment = code_assign;
163+
}
164+
else
165+
{
166+
locations.non_null_assignments.push_back(code_assign);
167+
}
168+
}
169+
}
170+
else if(statement.get_statement() == ID_block)
171+
{
172+
const auto &assignments_in_block =
173+
find_pointer_assignments(pointer_name, assignment.operands());
174+
locations = combine_locations(locations, assignments_in_block);
175+
}
176+
else if(statement.get_statement() == ID_ifthenelse)
177+
{
178+
const code_ifthenelset &if_else_block =
179+
to_code_ifthenelse(to_code(assignment));
180+
const auto &assignments_in_block = find_pointer_assignments(
181+
pointer_name, exprt::operandst{if_else_block.then_case()});
182+
locations = combine_locations(locations, assignments_in_block);
183+
184+
if(if_else_block.has_else_case())
185+
{
186+
const auto &assignments_in_else = find_pointer_assignments(
187+
pointer_name, exprt::operandst{if_else_block.else_case()});
188+
locations = combine_locations(locations, assignments_in_else);
189+
}
190+
}
191+
else if(statement.get_statement() == ID_label)
192+
{
193+
const code_labelt &label_statement = to_code_label(statement);
194+
const auto &assignments_in_label = find_pointer_assignments(
195+
pointer_name, exprt::operandst{label_statement.code()});
196+
locations = combine_locations(locations, assignments_in_label);
197+
}
198+
}
199+
200+
return locations;
201+
}
202+
203+
const exprt &find_declaration_by_name(
204+
const irep_idt &variable_name,
205+
const exprt::operandst &entry_point_instructions)
206+
{
207+
for(const auto &instruction : entry_point_instructions)
208+
{
209+
const codet &statement = to_code(instruction);
210+
INVARIANT(instruction.id() == ID_code, "All instructions must be code");
211+
if(statement.get_statement() == ID_decl)
212+
{
213+
const auto &decl_statement = to_code_decl(statement);
214+
215+
if(decl_statement.get_identifier() == variable_name)
216+
{
217+
return instruction;
218+
}
219+
}
220+
}
221+
throw no_decl_found_exception(variable_name.c_str());
222+
}

‎unit/testing-utils/java_testing_utils.h

+65
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test utilities
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Utilties for inspecting goto functions
11+
12+
#include <util/irep.h>
13+
#include <util/expr.h>
14+
#include <util/optional.h>
15+
#include <util/std_code.h>
16+
#include <util/std_types.h>
17+
#include <goto-programs/goto_program.h>
18+
19+
#ifndef CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H
20+
#define CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H
21+
22+
class no_decl_found_exception : public std::exception
23+
{
24+
public:
25+
explicit no_decl_found_exception(const std::string &varname)
26+
: _varname(varname)
27+
{
28+
}
29+
30+
virtual const char *what() const throw()
31+
{
32+
std::ostringstream stringStream;
33+
stringStream << "Failed to find declaration for: " << _varname;
34+
return stringStream.str().c_str();
35+
}
36+
37+
private:
38+
std::string _varname;
39+
};
40+
41+
struct struct_component_assignment_locationt
42+
{
43+
std::vector<code_assignt> assignment_locations;
44+
};
45+
46+
struct_component_assignment_locationt find_struct_component_assignments(
47+
const exprt::operandst &entry_point_instructions,
48+
const irep_idt &structure_name,
49+
const irep_idt &component_name);
50+
51+
struct pointer_assignment_locationt
52+
{
53+
optionalt<code_assignt> null_assignment;
54+
std::vector<code_assignt> non_null_assignments;
55+
};
56+
57+
pointer_assignment_locationt find_pointer_assignments(
58+
const irep_idt &pointer_name,
59+
const exprt::operandst &instructions);
60+
61+
const exprt &find_declaration_by_name(
62+
const irep_idt &variable_name,
63+
const exprt::operandst &entry_point_instructions);
64+
65+
#endif //TEST_GEN_SUPERBUILD_JAVA_TESTING_UTILS_H

0 commit comments

Comments
 (0)