Skip to content

Commit b90abb3

Browse files
NathanJPhillipsNathanJPhillips
committed
Change data storage for generic_parameter_specialization_mapt
This fixes the problem where we tried to unwind stacks in step that are not related, e.g. when a third generic class refers to two mutually recursive generic classes Instead stacks are created per scope (generic context) and unwound individually Also fixes problem where self-recursion isn't handled properly Add test that would have triggered invariant in get_recursively_instantiated_type
1 parent 909bab6 commit b90abb3

18 files changed

+319
-252
lines changed

‎jbmc/src/java_bytecode/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ SRC = assignments_from_json.cpp \
55
ci_lazy_methods_needed.cpp \
66
convert_java_nondet.cpp \
77
expr2java.cpp \
8+
generic_parameter_specialization_map.cpp \
89
generic_parameter_specialization_map_keys.cpp \
910
jar_file.cpp \
1011
jar_pool.cpp \

‎jbmc/src/java_bytecode/README.md

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -76,11 +76,7 @@ types so we keep a stack of types for each parameter.
7676

7777
We use the map in \ref select_pointer_typet::specialize_generics to
7878
retrieve the concrete type of generic parameters such as `MyGeneric::T` and of
79-
arrays of generic parameters such as `MyGeneric::T[]`. Special attention
80-
is paid to breaking infinite recursion when searching the map, e.g.,
81-
`MyGeneric::T` being specialized with `MyGeneric::U` and vice versa, for an
82-
example of such a recursion see
83-
\ref select_pointer_typet::get_recursively_instantiated_type. More complicated
79+
arrays of generic parameters such as `MyGeneric::T[]`. More complicated
8480
generic types such as `MyGeneric<T>` are specialized indirectly within \ref
8581
java_object_factoryt. Their concrete types are already stored in the map and are
8682
retrieved when needed, e.g., to initialize their fields.

‎jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
/// Author: Diffblue Ltd.
2+
3+
#include "generic_parameter_specialization_map.h"
4+
5+
std::size_t generic_parameter_specialization_mapt::insert(
6+
const std::vector<java_generic_parametert> &parameters,
7+
std::vector<reference_typet> types)
8+
{
9+
PRECONDITION(!parameters.empty());
10+
const auto first_param_it =
11+
param_to_container.find(parameters.front().get_name());
12+
std::size_t container_index;
13+
if(first_param_it == param_to_container.end())
14+
{
15+
container_index = container_to_specializations.size();
16+
container_to_specializations.emplace_back();
17+
std::size_t param_index = 0;
18+
for(const java_generic_parametert &parameter : parameters)
19+
{
20+
const auto result = param_to_container.emplace(
21+
parameter.get_name(), container_paramt{container_index, param_index++});
22+
INVARIANT(
23+
result.second, "Some but not all type parameters already mapped");
24+
}
25+
}
26+
else
27+
{
28+
container_index = first_param_it->second.container_index;
29+
std::size_t param_index = 0;
30+
for(const java_generic_parametert &parameter : parameters)
31+
{
32+
const auto param_it = param_to_container.find(parameter.get_name());
33+
INVARIANT(
34+
param_it != param_to_container.end(),
35+
"Some but not all type parameters already mapped");
36+
INVARIANT(
37+
param_it->second.container_index == container_index,
38+
"Not all type parameters assigned to same container");
39+
INVARIANT(
40+
param_it->second.param_index == param_index,
41+
"Type parameters found in different order");
42+
++param_index;
43+
}
44+
}
45+
container_to_specializations[container_index].push(std::move(types));
46+
return container_index;
47+
}
48+
49+
void generic_parameter_specialization_mapt::pop(std::size_t container_id)
50+
{
51+
container_to_specializations.at(container_id).pop();
52+
}
53+
54+
optionalt<reference_typet>
55+
generic_parameter_specialization_mapt::pop(const irep_idt &parameter_name)
56+
{
57+
const auto types_it = param_to_container.find(parameter_name);
58+
if(types_it == param_to_container.end())
59+
return {};
60+
std::stack<std::vector<reference_typet>> &stack =
61+
container_to_specializations.at(types_it->second.container_index);
62+
if(stack.empty())
63+
return {};
64+
reference_typet result = stack.top().at(types_it->second.param_index);
65+
stack.pop();
66+
return result;
67+
}

‎jbmc/src/java_bytecode/generic_parameter_specialization_map.h

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
/// Author: Diffblue Ltd.
2+
3+
#ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H
4+
#define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H
5+
6+
#include <stack>
7+
#include <vector>
8+
9+
#include <util/string_utils.h>
10+
11+
#include "expr2java.h"
12+
#include "java_types.h"
13+
14+
class generic_parameter_specialization_mapt
15+
{
16+
private:
17+
struct container_paramt
18+
{
19+
std::size_t container_index;
20+
std::size_t param_index;
21+
};
22+
std::unordered_map<irep_idt, container_paramt> param_to_container;
23+
std::vector<std::stack<std::vector<reference_typet>>>
24+
container_to_specializations;
25+
26+
public:
27+
std::size_t insert(
28+
const std::vector<java_generic_parametert> &parameters,
29+
std::vector<reference_typet> types);
30+
31+
void pop(std::size_t container_id);
32+
33+
optionalt<reference_typet> pop(const irep_idt &parameter_name);
34+
35+
struct printert
36+
{
37+
const generic_parameter_specialization_mapt &map;
38+
const namespacet &ns;
39+
40+
printert(
41+
const generic_parameter_specialization_mapt &map,
42+
const namespacet &ns)
43+
: map(map), ns(ns)
44+
{
45+
}
46+
};
47+
48+
template <typename ostream>
49+
friend ostream &operator<<(ostream &stm, const printert &map);
50+
};
51+
52+
template <typename ostream>
53+
ostream &operator<<(
54+
ostream &stm,
55+
const generic_parameter_specialization_mapt::printert &map)
56+
{
57+
if(map.map.container_to_specializations.empty())
58+
stm << "empty map";
59+
else
60+
stm << "map:\n";
61+
std::vector<std::vector<irep_idt>> container_to_params(
62+
map.map.container_to_specializations.size());
63+
for(const auto &elt : map.map.param_to_container)
64+
{
65+
std::vector<irep_idt> &params =
66+
container_to_params[elt.second.container_index];
67+
if(params.size() < elt.second.param_index + 1)
68+
params.resize(elt.second.param_index + 1);
69+
params[elt.second.param_index] = elt.first;
70+
}
71+
const namespacet &ns = map.ns;
72+
for(std::size_t index = 0; index < container_to_params.size(); ++index)
73+
{
74+
stm << "<";
75+
join_strings(
76+
stm,
77+
container_to_params.at(index).begin(),
78+
container_to_params.at(index).end(),
79+
", ");
80+
stm << ">: ";
81+
std::stack<std::vector<reference_typet>> stack =
82+
map.map.container_to_specializations.at(index);
83+
while(!stack.empty())
84+
{
85+
stm << "<";
86+
join_strings(
87+
stm,
88+
stack.top().begin(),
89+
stack.top().end(),
90+
", ",
91+
[&ns](const reference_typet &pointer_type) {
92+
if(is_java_generic_parameter(pointer_type))
93+
{
94+
return id2string(
95+
to_java_generic_parameter(pointer_type).get_name());
96+
}
97+
else
98+
return type2java(pointer_type, ns);
99+
});
100+
stm << ">, ";
101+
stack.pop();
102+
}
103+
stm << "\n";
104+
}
105+
return stm;
106+
}
107+
108+
#endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H

‎jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

Lines changed: 26 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -35,51 +35,18 @@ get_all_generic_parameters(const typet &type)
3535
return generic_parameters;
3636
}
3737

38-
/// Add pairs to the controlled map. Own the keys and pop from their stack
39-
/// on destruction; otherwise do nothing.
40-
/// \param parameters: generic parameters that are the keys of the pairs to add
41-
/// \param types: a type to add for each parameter
42-
void generic_parameter_specialization_map_keyst::insert_pairs(
43-
const std::vector<java_generic_parametert> &parameters,
44-
const std::vector<reference_typet> &types)
45-
{
46-
INVARIANT(erase_keys.empty(), "insert_pairs should only be called once");
47-
48-
for(const auto &pair : make_range(parameters).zip(types))
49-
{
50-
// Only add the pair if the type is not the parameter itself, e.g.,
51-
// pair.first = pair.second = java::A::T. This can happen for example
52-
// when initializing a pointer to an implicitly generic Java class type
53-
// in gen_nondet_init and would result in a loop when the map is used
54-
// to look up the type of the parameter.
55-
if(
56-
!(is_java_generic_parameter(pair.second) &&
57-
to_java_generic_parameter(pair.second).get_name() ==
58-
pair.first.get_name()))
59-
{
60-
const irep_idt &key = pair.first.get_name();
61-
const auto map_it = generic_parameter_specialization_map
62-
.emplace(key, std::vector<reference_typet>{})
63-
.first;
64-
map_it->second.push_back(pair.second);
65-
66-
// We added something; pop it when this
67-
// generic_parameter_specialization_map_keyst is destroyed
68-
erase_keys.push_back(key);
69-
}
70-
}
71-
}
72-
73-
/// Add a pair of a parameter and its types for each generic parameter of the
74-
/// given generic pointer type to the controlled map. Own the keys and pop
75-
/// from their stack on destruction; otherwise do nothing.
38+
/// Add the parameters and their types for each generic parameter of the
39+
/// given generic pointer type to the map.
40+
/// Own the keys and pop from their stack on destruction.
7641
/// \param pointer_type: pointer type to get the specialized generic types from
7742
/// \param pointer_subtype_struct: struct type to which the generic pointer
7843
/// points, must be generic if the pointer is generic
79-
void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
44+
void generic_parameter_specialization_map_keyst::insert(
8045
const pointer_typet &pointer_type,
8146
const typet &pointer_subtype_struct)
8247
{
48+
// Use a fresh generic_parameter_specialization_map_keyst for each scope
49+
PRECONDITION(!container_id);
8350
if(!is_java_generic_type(pointer_type))
8451
return;
8552
// The supplied type must be the full type of the pointer's subtype
@@ -91,7 +58,7 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
9158
// - an incomplete class or
9259
// - a class that is neither generic nor implicitly generic (this
9360
// may be due to unsupported class signature)
94-
// then ignore the generic types in the pointer and do not add any pairs.
61+
// then ignore the generic types in the pointer and do not add an entry.
9562
// TODO TG-1996 should decide how mocking and generics should work
9663
// together. Currently an incomplete class is never marked as generic. If
9764
// this changes in TG-1996 then the condition below should be updated.
@@ -115,34 +82,39 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
11582
type_args.size() == generic_parameters.size(),
11683
"All generic parameters of the pointer type need to be specified");
11784

118-
insert_pairs(generic_parameters, type_args);
85+
container_id =
86+
generic_parameter_specialization_map.insert(generic_parameters, type_args);
11987
}
12088

121-
/// Add a pair of a parameter and its types for each generic parameter of the
122-
/// given generic symbol type to the controlled map. This function is used
123-
/// for generic bases (superclass or interfaces) where the reference to it is
124-
/// in the form of a symbol rather than a pointer (as opposed to the function
125-
/// insert_pairs_for_pointer). Own the keys and pop from their stack
126-
/// on destruction; otherwise do nothing.
89+
/// Add the parameters and their types for each generic parameter of the
90+
/// given generic symbol type to the map.
91+
/// This function is used for generic bases (superclass or interfaces) where
92+
/// the reference to it is in the form of a symbol rather than a pointer.
93+
/// Own the keys and pop from their stack on destruction.
12794
/// \param struct_tag_type: symbol type to get the specialized generic types
12895
/// from
12996
/// \param symbol_struct: struct type of the symbol type, must be generic if
13097
/// the symbol is generic
131-
void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
98+
void generic_parameter_specialization_map_keyst::insert(
13299
const struct_tag_typet &struct_tag_type,
133100
const typet &symbol_struct)
134101
{
102+
// Use a fresh generic_parameter_specialization_map_keyst for each scope
103+
PRECONDITION(!container_id);
104+
if(!is_java_generic_struct_tag_type(struct_tag_type))
105+
return;
106+
// The supplied type must be the full type of the pointer's subtype
107+
PRECONDITION(
108+
struct_tag_type.get(ID_identifier) == symbol_struct.get(ID_name));
109+
135110
// If the struct is:
136111
// - an incomplete class or
137112
// - a class that is neither generic nor implicitly generic (this
138113
// may be due to unsupported class signature)
139-
// then ignore the generic types in the struct_tag_type and do not add any
140-
// pairs.
114+
// then ignore the generic types in the struct and do not add an entry.
141115
// TODO TG-1996 should decide how mocking and generics should work
142116
// together. Currently an incomplete class is never marked as generic. If
143117
// this changes in TG-1996 then the condition below should be updated.
144-
if(!is_java_generic_struct_tag_type(struct_tag_type))
145-
return;
146118
if(to_java_class_type(symbol_struct).get_is_stub())
147119
return;
148120
if(
@@ -163,5 +135,6 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
163135
type_args.size() == generic_parameters.size(),
164136
"All generic parameters of the superclass need to be concretized");
165137

166-
insert_pairs(generic_parameters, type_args);
138+
container_id =
139+
generic_parameter_specialization_map.insert(generic_parameters, type_args);
167140
}

‎jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

Lines changed: 10 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
21
/// Author: Diffblue Ltd.
32

43
#ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
@@ -15,6 +14,12 @@
1514
/// on leaving that scope.
1615
class generic_parameter_specialization_map_keyst
1716
{
17+
private:
18+
/// Generic parameter specialization map to modify
19+
generic_parameter_specialization_mapt &generic_parameter_specialization_map;
20+
/// Key of the container to pop on destruction
21+
optionalt<std::size_t> container_id;
22+
1823
public:
1924
/// Initialize a generic-parameter-specialization-map entry owner operating
2025
/// on a given map. Initially it does not own any map entry.
@@ -29,15 +34,8 @@ class generic_parameter_specialization_map_keyst
2934
/// controlled map.
3035
~generic_parameter_specialization_map_keyst()
3136
{
32-
for(const auto key : erase_keys)
33-
{
34-
const auto map_it = generic_parameter_specialization_map.find(key);
35-
PRECONDITION(map_it != generic_parameter_specialization_map.end());
36-
std::vector<reference_typet> &val = map_it->second;
37-
val.pop_back();
38-
if(val.empty())
39-
generic_parameter_specialization_map.erase(map_it);
40-
}
37+
if(container_id)
38+
generic_parameter_specialization_map.pop(*container_id);
4139
}
4240

4341
// Objects of these class cannot be copied in any way - delete the copy
@@ -47,21 +45,11 @@ class generic_parameter_specialization_map_keyst
4745
generic_parameter_specialization_map_keyst &
4846
operator=(const generic_parameter_specialization_map_keyst &) = delete;
4947

50-
void insert_pairs_for_pointer(
48+
void insert(
5149
const pointer_typet &pointer_type,
5250
const typet &pointer_subtype_struct);
53-
void
54-
insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct);
55-
56-
private:
57-
/// Generic parameter specialization map to modify
58-
generic_parameter_specialization_mapt &generic_parameter_specialization_map;
59-
/// Keys of the entries to pop on destruction
60-
std::vector<irep_idt> erase_keys;
6151

62-
void insert_pairs(
63-
const std::vector<java_generic_parametert> &parameters,
64-
const std::vector<reference_typet> &types);
52+
void insert(const struct_tag_typet &, const typet &symbol_struct);
6553
};
6654

6755
#endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H

0 commit comments

Comments
 (0)