Skip to content

Commit 4280d03

Browse files
author
owen-jones-diffblue
authored
Merge pull request diffblue#416 from diffblue/bugfix/lvsa-casts
Bugfix/lvsa casts
2 parents 7e57194 + 5f70d13 commit 4280d03

File tree

5 files changed

+205
-33
lines changed

5 files changed

+205
-33
lines changed

regression/LVSA/TestCasts/Test.java

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
package LVSA.TestCasts;
2+
3+
public class Test {
4+
public static TestInterface interfaceFromChild;
5+
public static TestInterface interfaceFromParent;
6+
public static TestParent parentFromChild;
7+
public static TestParent parentFromInterface;
8+
public static TestChild childFromInterface;
9+
public static TestChild childFromParent;
10+
11+
public void cast_from_child() {
12+
TestChild testChild = new TestChild();
13+
14+
interfaceFromChild = (TestInterface)testChild;
15+
parentFromChild = (TestParent)testChild;
16+
}
17+
18+
public void cast_from_parent() {
19+
TestParent testParent = new TestChild();
20+
21+
interfaceFromParent = (TestInterface)testParent;
22+
childFromParent = (TestChild)testParent;
23+
}
24+
25+
public void cast_from_interface() {
26+
TestInterface testInterface = (TestInterface)new TestChild();
27+
28+
parentFromInterface = (TestParent)testInterface;
29+
childFromInterface = (TestChild)testInterface;
30+
}
31+
}
32+
33+
interface TestInterface {
34+
}
35+
36+
class TestParent {
37+
}
38+
39+
class TestChild extends TestParent implements TestInterface {
40+
}
Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
import fasteners
2+
import regression.LVSA.lvsa_driver as driver
3+
import os
4+
import regression.utils as utils
5+
6+
7+
def _get_this_file_dir():
8+
return os.path.dirname(os.path.abspath(__file__))
9+
10+
11+
def _get_folder_name():
12+
return os.path.basename(_get_this_file_dir())
13+
14+
15+
@fasteners.interprocess_locked(os.path.join(os.path.dirname(__file__), ".build_lock"))
16+
def test_cast_from_child(tmpdir):
17+
""" Test addition and removal of casts to DO's """
18+
with utils.working_dir(_get_this_file_dir()):
19+
os.system("javac Test.java")
20+
lvsa_driver = driver.LvsaDriver(tmpdir, _get_folder_name()).with_test_function('cast_from_child')
21+
lvsa_expectation = lvsa_driver.run()
22+
23+
value_set_expectation = lvsa_expectation.get_value_set_for_public_static('interfaceFromChild')
24+
value_set_expectation.check_number_of_values(1)
25+
value_set_expectation.check_contains_typecast_dynamic_object(1, True, 'LVSA.TestCasts.TestInterface')
26+
27+
value_set_expectation = lvsa_expectation.get_value_set_for_public_static('parentFromChild')
28+
value_set_expectation.check_number_of_values(1)
29+
value_set_expectation.check_contains_soft_cast_dynamic_object(1, True, 'LVSA.TestCasts.TestParent')
30+
31+
32+
@fasteners.interprocess_locked(os.path.join(os.path.dirname(__file__), ".build_lock"))
33+
def test_cast_from_parent(tmpdir):
34+
""" Test addition and removal of casts to DO's """
35+
with utils.working_dir(_get_this_file_dir()):
36+
os.system("javac Test.java")
37+
lvsa_driver = driver.LvsaDriver(tmpdir, _get_folder_name()).with_test_function('cast_from_parent')
38+
lvsa_expectation = lvsa_driver.run()
39+
40+
value_set_expectation = lvsa_expectation.get_value_set_for_public_static('interfaceFromParent')
41+
value_set_expectation.check_number_of_values(1)
42+
value_set_expectation.check_contains_typecast_dynamic_object(1, True, 'LVSA.TestCasts.TestInterface')
43+
44+
value_set_expectation = lvsa_expectation.get_value_set_for_public_static('childFromParent')
45+
value_set_expectation.check_number_of_values(1)
46+
value_set_expectation.check_contains_dynamic_object(1, True)
47+
48+
49+
@fasteners.interprocess_locked(os.path.join(os.path.dirname(__file__), ".build_lock"))
50+
def test_cast_from_interface(tmpdir):
51+
""" Test addition and removal of casts to DO's """
52+
with utils.working_dir(_get_this_file_dir()):
53+
os.system("javac Test.java")
54+
lvsa_driver = driver.LvsaDriver(tmpdir, _get_folder_name()).with_test_function('cast_from_interface')
55+
lvsa_expectation = lvsa_driver.run()
56+
57+
value_set_expectation = lvsa_expectation.get_value_set_for_public_static('parentFromInterface')
58+
value_set_expectation.check_number_of_values(1)
59+
value_set_expectation.check_contains_soft_cast_dynamic_object(1, True, 'LVSA.TestCasts.TestParent')
60+
61+
value_set_expectation = lvsa_expectation.get_value_set_for_public_static('childFromInterface')
62+
value_set_expectation.check_number_of_values(1)
63+
value_set_expectation.check_contains_dynamic_object(1, True)
64+

regression/LVSA/lvsa_driver.py

Lines changed: 50 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,9 @@ class Expr:
1010

1111
def __init__(self, expr):
1212
if expr['namedSub']['type']['id'] == 'symbol':
13-
self.type_identifier = expr['namedSub']['type']['namedSub']['identifier']['id']
13+
self.type_identifier = expr['namedSub']['type']['namedSub']['identifier']['id'].replace('java::', '')
14+
elif expr['namedSub']['type']['id'] == 'struct':
15+
self.type_identifier = expr['namedSub']['type']['namedSub']['base_name']['id']
1416
else:
1517
self.type_identifier = None
1618

@@ -27,6 +29,28 @@ def __init__(self, dynamic_object_expr):
2729
dynamic_object_expr['namedSub']['is_most_recent_allocation']['id'] == 'most_recent_allocation'
2830

2931

32+
class TypecastDynamicObject(Expr):
33+
"""Turn the json for a typecast dynamic object expr into a python object"""
34+
35+
def __init__(self, typecast_dynamic_object_expr):
36+
assert typecast_dynamic_object_expr['id'] == 'typecast'
37+
assert typecast_dynamic_object_expr['sub'][0]['id'] == 'dynamic_object'
38+
Expr.__init__(self, typecast_dynamic_object_expr)
39+
self.dynamic_object = DynamicObject(typecast_dynamic_object_expr['sub'][0])
40+
41+
42+
class SoftCastDynamicObject(Expr):
43+
"""Turn the json for a soft-cast dynamic object expr into a python object"""
44+
45+
def __init__(self, soft_cast_dynamic_object_expr):
46+
assert soft_cast_dynamic_object_expr['id'] == 'member'
47+
assert soft_cast_dynamic_object_expr['namedSub']['component_name']['id'].startswith('@')
48+
assert soft_cast_dynamic_object_expr['sub'][0]['id'] == 'dynamic_object'
49+
Expr.__init__(self, soft_cast_dynamic_object_expr)
50+
assert soft_cast_dynamic_object_expr['namedSub']['component_name']['id'] == '@' + self.type_identifier
51+
self.dynamic_object = DynamicObject(soft_cast_dynamic_object_expr['sub'][0])
52+
53+
3054
class EvsType(Enum):
3155
root_object = '0'
3256
per_field = '1'
@@ -72,13 +96,19 @@ def __init__(self, evs_expr):
7296
else:
7397
assert False
7498

99+
75100
class ValueSetExpectation:
76101
"""Encapsulate the states that a particular variable can take"""
77102

78103
def __init__(self, var_state):
79104
self.var_state = var_state['values']
80105
self.null_objects = [x for x in self.var_state if x['id'] == 'NULL-object']
81106
self.dynamic_objects = [DynamicObject(x) for x in self.var_state if x['id'] == 'dynamic_object']
107+
self.typecast_dynamic_objects = [TypecastDynamicObject(x) for x in self.var_state if x['id'] ==
108+
'typecast' and x['sub'][0]['id'] == 'dynamic_object']
109+
self.soft_cast_dynamic_objects = [SoftCastDynamicObject(x) for x in self.var_state if
110+
x['id'] == 'member' and x['namedSub']['component_name']['id'].startswith(
111+
'@') and x['sub'][0]['id'] == 'dynamic_object']
82112
self.external_value_sets = [ExternalValueSet(x) for x in self.var_state if x['id'] == 'external_value_set']
83113
self.unknown = [x for x in self.var_state if x['id'] == 'unknown']
84114

@@ -100,6 +130,23 @@ def check_contains_dynamic_object(self, expected_number=1, is_most_recent_alloca
100130
matches = [x for x in matches if x.is_most_recent_allocation == is_most_recent_allocation]
101131
assert expected_number == len(matches)
102132

133+
def check_contains_typecast_dynamic_object(self, expected_number=1, is_most_recent_allocation=None, type=None):
134+
matches = self.typecast_dynamic_objects
135+
if is_most_recent_allocation is not None:
136+
# Expect True or False
137+
matches = [x for x in matches if x.dynamic_object.is_most_recent_allocation == is_most_recent_allocation]
138+
if type is not None:
139+
# Expect string
140+
matches = [x for x in matches if x.type_identifier == type]
141+
assert expected_number == len(matches)
142+
143+
def check_contains_soft_cast_dynamic_object(self, expected_number=1, is_most_recent_allocation=None, type=None):
144+
matches = self.soft_cast_dynamic_objects
145+
if is_most_recent_allocation is not None:
146+
# Expect string
147+
matches = [x for x in matches if x.type_identifier == type]
148+
assert expected_number == len(matches)
149+
103150
def check_contains_root_object_evs(self, expected_number=1, label_suffix=None):
104151
matches = [x for x in self.external_value_sets if x.evs_type == EvsType.root_object]
105152
if label_suffix is not None:
@@ -267,7 +314,8 @@ def run(self):
267314
class_path = os.path.join('LVSA', self.folder_name, self.class_filename)
268315
cmd = [executable_path, '--local-value-set-analysis', '--lvsa-summary-directory', self.temp_dir_path,
269316
'--function', fq_function_name, '--show-value-sets', '--json-ui']
270-
if "SECURITY_REGRESSION_TESTS_USE_CSVSA" in os.environ and os.environ["SECURITY_REGRESSION_TESTS_USE_CSVSA"] != 0:
317+
if "SECURITY_REGRESSION_TESTS_USE_CSVSA" in os.environ and os.environ[
318+
"SECURITY_REGRESSION_TESTS_USE_CSVSA"] != 0:
271319
cmd.append("--lazy-methods-context-sensitive")
272320
if self.max_input_tree_depth is not None:
273321
cmd += ['--java-max-input-tree-depth', str(self.max_input_tree_depth)]

src/driver/sec_driver_parse_options.cpp

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -109,10 +109,13 @@ void sec_driver_parse_optionst::get_command_line_options(optionst &options)
109109

110110
static irep_idt get_cprover_start_main_callee(const goto_modelt &goto_model)
111111
{
112-
const goto_programt &start_body =
113-
goto_model.get_goto_functions().function_map.at(
114-
goto_functionst::entry_point()).body;
112+
const goto_functionst::function_mapt &function_map =
113+
goto_model.get_goto_functions().function_map;
114+
auto entry_it = function_map.find(goto_functionst::entry_point());
115+
if(entry_it == function_map.end())
116+
return {};
115117

118+
const goto_programt &start_body = entry_it->second.body;
116119
auto last_call_it =
117120
std::find_if(
118121
start_body.instructions.rbegin(),
@@ -242,12 +245,15 @@ int sec_driver_parse_optionst::doit()
242245
local_value_set_analysist::dbt summarydb(serializer, 30);
243246
namespacet ns(goto_model.symbol_table);
244247

245-
const std::string function_name = cmdline.get_value("function");
246248
const bool print_function_summary = cmdline.isset("show-value-sets");
247249
const bool print_all_summaries = cmdline.isset("show-value-sets-all");
248250

249-
irep_idt fully_qualified_name =
250-
get_cprover_start_main_callee(goto_model);
251+
irep_idt fully_qualified_name = get_cprover_start_main_callee(goto_model);
252+
if(fully_qualified_name.empty())
253+
{
254+
error() << "You must specify an entry point with --function" << eom;
255+
return CPROVER_EXIT_USAGE_ERROR;
256+
}
251257

252258
call_grapht const call_graph(goto_model.goto_functions);
253259
std::vector<irep_idt> process_order =

src/pointer-analysis/local_value_set.cpp

Lines changed: 39 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -67,13 +67,13 @@ upcast_to_type(exprt expr, const typet &intended_type, const namespacet &ns)
6767
while(type_of_expr != intended_type)
6868
{
6969
const optionalt<typet> base_type = get_base_type(type_of_expr, ns);
70+
// Whether type_of_expr is object or an incomplete type class_hierarchy
71+
// can not have found intended_type in the direct parents but did find it as
72+
// an ancestor so intended_type must be an interface. Return nothing and
73+
// do a hard cast
7074
if(!base_type)
7175
return {};
7276

73-
// If the base class is a stub class return unknown to remain sound
74-
if(base_type->get_bool(ID_incomplete_class))
75-
return exprt(ID_unknown, intended_type);
76-
7777
update_expr_with_soft_cast_to_base_type(expr, ns);
7878

7979
type_of_expr = ns.follow(expr.type());
@@ -86,18 +86,26 @@ upcast_to_type(exprt expr, const typet &intended_type, const namespacet &ns)
8686
}
8787

8888
/// Remove all superclass accesses from `expr` and return the result
89-
static exprt remove_all_superclass_accesses(exprt expr)
89+
static exprt remove_all_typecasts_and_superclass_accesses(exprt expr)
9090
{
91-
while(expr.id() == ID_member)
91+
while(expr.id() == ID_member || expr.id() == ID_typecast)
9292
{
93-
const member_exprt &member = to_member_expr(expr);
94-
const std::string &component_name = id2string(member.get_component_name());
95-
const bool is_superclass_access = has_prefix(component_name, "@") &&
96-
component_name != "@lock" &&
97-
component_name != "@class_identifier";
98-
if(!is_superclass_access)
99-
break;
100-
expr = member.compound();
93+
if(expr.id() == ID_typecast)
94+
{
95+
expr = expr.op0();
96+
}
97+
else
98+
{
99+
const member_exprt &member = to_member_expr(expr);
100+
const std::string &component_name =
101+
id2string(member.get_component_name());
102+
const bool is_superclass_access = has_prefix(component_name, "@") &&
103+
component_name != "@lock" &&
104+
component_name != "@class_identifier";
105+
if(!is_superclass_access)
106+
break;
107+
expr = member.compound();
108+
}
101109
}
102110
return expr;
103111
}
@@ -110,15 +118,17 @@ void local_value_sett::make_union_adjusting_types(
110118
{
111119
for(const auto &num : src.read())
112120
{
121+
// Remove soft-casts (and hard casts?) from the rhs value
113122
const exprt underlying_object =
114-
remove_all_superclass_accesses(object_numbering[num.first]);
123+
remove_all_typecasts_and_superclass_accesses(object_numbering[num.first]);
115124

116125
if(underlying_object.id() == ID_external_value_set)
117126
{
118127
external_value_set_exprt evse_copy =
119128
to_external_value_set(underlying_object);
129+
// Adjust the type of the EVS and return it
120130
evse_copy.type() = input_type;
121-
insert(dest, evse_copy, num.second);
131+
insert(dest, evse_copy);
122132
}
123133
else
124134
{
@@ -143,7 +153,7 @@ void local_value_sett::make_union_adjusting_types(
143153

144154
if(no_cast_required || intended_type_eventually_void)
145155
{
146-
insert(dest, num.first, num.second);
156+
insert(dest, underlying_object);
147157
}
148158
else if(
149159
is_ancestor(
@@ -153,7 +163,8 @@ void local_value_sett::make_union_adjusting_types(
153163
{
154164
optionalt<exprt> cast_expr =
155165
upcast_to_type(underlying_object, intended_type, ns);
156-
CHECK_RETURN(cast_expr);
166+
if(!cast_expr)
167+
cast_expr = typecast_exprt(underlying_object, intended_type);
157168

158169
insert(dest, *cast_expr);
159170
}
@@ -203,10 +214,10 @@ static const typet &type_from_suffix(
203214
suffix_without_supertypes = suffix;
204215
const typet *ret = &original_type;
205216
size_t next_member = 1; // Skip initial '.'
206-
if(suffix.size() != 0)
207-
assert(suffix[0] == '.');
217+
INVARIANT(suffix.size() != 1, "Suffix length is single character");
208218
while(next_member < suffix.size())
209219
{
220+
INVARIANT(suffix[next_member - 1] == '.', "Suffix separator not found");
210221
ret = &ns.follow(*ret);
211222
assert(ret->id() == ID_struct || ret->id() == ID_union);
212223
// TODO: replace this silly string-chewing with a vector
@@ -266,12 +277,14 @@ static const typet &type_from_suffix(
266277
/// cast" means dereferencing a pointer to a class, accessing the field
267278
/// corresponding to its base class, and taking the address of that field -
268279
/// `&input->parent_class`
269-
static exprt remove_soft_casts(const exprt &input)
280+
static exprt remove_casts(exprt input)
270281
{
282+
while(input.id() == ID_typecast)
283+
input = input.op0();
271284
if(input.id() == ID_address_of)
272285
{
273286
const exprt &input_target = to_address_of_expr(input).object();
274-
exprt expr = remove_all_superclass_accesses(input_target);
287+
exprt expr = remove_all_typecasts_and_superclass_accesses(input_target);
275288
if(expr != input_target && expr.id() == ID_dereference)
276289
return to_dereference_expr(expr).pointer();
277290
}
@@ -293,11 +306,12 @@ void local_value_sett::get_value_set_rec(
293306
const typet &op_type = ns.follow(typecast_expr.op().type());
294307
if(op_type.id() == ID_pointer)
295308
{
296-
// pointer-to-pointer -- we just ignore these
309+
// Adjust the types of each rhs value to match the expected type
297310
object_mapt tmp;
298-
exprt expr_to_cast = remove_soft_casts(typecast_expr.op());
311+
// Hard casts have been removed by the simplifier but soft casts need
312+
// to be removed too (maybe?)
313+
exprt expr_to_cast = remove_casts(typecast_expr.op());
299314
get_value_set_rec(expr_to_cast, tmp, suffix, original_type, ns);
300-
// ...except to fix up the types of external objects as they pass through:
301315
make_union_adjusting_types(dest, tmp, typecast_expr.type().subtype(), ns);
302316
}
303317
}

0 commit comments

Comments
 (0)