Skip to content

Commit 5eefd82

Browse files
author
thk123
committed
Chang the structure to use a lambda rather than a class
This reduces overall boilerplate.
1 parent d9dd1e0 commit 5eefd82

7 files changed

+56
-83
lines changed

jbmc/src/java_bytecode/ci_lazy_methods.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,7 @@ ci_lazy_methodst::ci_lazy_methodst(
3434
const symbol_tablet &symbol_table,
3535
const irep_idt &main_class,
3636
const std::vector<irep_idt> &main_jar_classes,
37-
const std::vector<std::unique_ptr<load_extra_methodst>>
38-
&lazy_methods_extra_entry_points,
37+
const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
3938
java_class_loadert &java_class_loader,
4039
const std::vector<irep_idt> &extra_instantiated_classes,
4140
const select_pointer_typet &pointer_type_selector,
@@ -107,8 +106,7 @@ bool ci_lazy_methodst::operator()(
107106
std::vector<irep_idt> extra_entry_points;
108107
for(const auto &extra_function_generator : lazy_methods_extra_entry_points)
109108
{
110-
const auto &extra_methods =
111-
extra_function_generator->extra_methods(symbol_table);
109+
const auto &extra_methods = extra_function_generator(symbol_table);
112110
extra_entry_points.insert(
113111
extra_entry_points.end(), extra_methods.begin(), extra_methods.end());
114112
}

jbmc/src/java_bytecode/ci_lazy_methods.h

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -91,12 +91,8 @@ typedef std::function<
9191
bool(const irep_idt &function_id, ci_lazy_methods_neededt)>
9292
method_convertert;
9393

94-
class load_extra_methodst
95-
{
96-
public:
97-
virtual std::vector<irep_idt>
98-
extra_methods(const symbol_tablet &symbol_table) const = 0;
99-
};
94+
typedef std::function<std::vector<irep_idt>(const symbol_tablet &)>
95+
load_extra_methodst;
10096

10197
class ci_lazy_methodst:public messaget
10298
{
@@ -105,8 +101,7 @@ class ci_lazy_methodst:public messaget
105101
const symbol_tablet &symbol_table,
106102
const irep_idt &main_class,
107103
const std::vector<irep_idt> &main_jar_classes,
108-
const std::vector<std::unique_ptr<load_extra_methodst>>
109-
&lazy_methods_extra_entry_points,
104+
const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
110105
java_class_loadert &java_class_loader,
111106
const std::vector<irep_idt> &extra_instantiated_classes,
112107
const select_pointer_typet &pointer_type_selector,
@@ -153,8 +148,7 @@ class ci_lazy_methodst:public messaget
153148
class_hierarchyt class_hierarchy;
154149
irep_idt main_class;
155150
std::vector<irep_idt> main_jar_classes;
156-
const std::vector<std::unique_ptr<load_extra_methodst>>
157-
&lazy_methods_extra_entry_points;
151+
const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points;
158152
java_class_loadert &java_class_loader;
159153
const std::vector<irep_idt> &extra_instantiated_classes;
160154
const select_pointer_typet &pointer_type_selector;

jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
100100
extra_entry_points.end(),
101101
std::back_inserter(extra_methods),
102102
[](const std::string &pattern) {
103-
return util_make_unique<load_method_by_regext>(pattern);
103+
return build_load_method_by_regex(pattern);
104104
});
105105

106106
if(cmd.isset("java-cp-include-files"))

jbmc/src/java_bytecode/java_bytecode_language.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -198,7 +198,7 @@ class java_bytecode_languaget:public languaget
198198
// List of classes to never load
199199
std::unordered_set<std::string> no_load_classes;
200200

201-
std::vector<std::unique_ptr<load_extra_methodst>> extra_methods;
201+
std::vector<load_extra_methodst> extra_methods;
202202
};
203203

204204
std::unique_ptr<languaget> new_java_bytecode_language();

jbmc/src/java_bytecode/load_method_by_regex.cpp

Lines changed: 37 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,12 @@ Author: Diffblue Ltd.
1313

1414
#include <util/symbol_table.h>
1515

16-
/// Create a load_method_by_regext matching the pattern. If the pattern doesn't
17-
/// include a colon for matching the descriptor, append a `:\(.*\).*` to the
18-
/// regex. Note this will mean all overloaded methods will be marked as extra
19-
/// entry points for CI lazy loading.
20-
/// If the pattern doesn't include the java:: prefix, prefix that
16+
/// For a given user provided pattern, return a regex, having dealt with the
17+
/// cases where the user has not prefixed with java:: or suffixed with the
18+
/// descriptor
2119
/// \param pattern: The user provided pattern
22-
load_method_by_regext::load_method_by_regext(const std::string &pattern)
20+
/// \return The regex to match with
21+
static std::regex build_regex_from_pattern(const std::string &pattern)
2322
{
2423
std::string modified_pattern = pattern;
2524
if(does_pattern_miss_descriptor(pattern))
@@ -28,43 +27,51 @@ load_method_by_regext::load_method_by_regext(const std::string &pattern)
2827
if(!has_prefix(pattern, "java::"))
2928
modified_pattern = "java::" + modified_pattern;
3029

31-
regex = std::regex{modified_pattern};
30+
return std::regex{modified_pattern};
3231
}
3332

34-
/// Get the methods that match the regex
35-
/// \param symbol_table: The symbol table to look through
36-
/// \return: The method identifiers that should be loaded
37-
std::vector<irep_idt>
38-
load_method_by_regext::extra_methods(const symbol_tablet &symbol_table) const
39-
{
40-
std::vector<irep_idt> matched_methods;
41-
for(const auto &symbol : symbol_table.symbols)
42-
{
43-
if(symbol.second.is_function())
44-
{
45-
const std::string symbol_name = id2string(symbol.first);
46-
if(std::regex_match(symbol_name, regex))
47-
{
48-
matched_methods.push_back(symbol_name);
49-
}
50-
}
51-
}
52-
return matched_methods;
53-
}
5433

5534
/// Identify if a parameter includes a part that will match a descriptor. That
5635
/// is, does it have a colon separtor.
5736
/// \param pattern: The user provided pattern
5837
/// \return True if no descriptor is found (that is, the only : relates to the
5938
/// java:: prefix.
60-
bool load_method_by_regext::does_pattern_miss_descriptor(
61-
const std::string &pattern)
39+
bool does_pattern_miss_descriptor(const std::string &pattern)
6240
{
6341
const size_t descriptor_index = pattern.rfind(':');
6442
if(descriptor_index == std::string::npos)
6543
return true;
6644

6745
static const std::string java_prefix = "java::";
6846
return descriptor_index == java_prefix.length() - 1 &&
69-
has_prefix(pattern, "java::");
47+
has_prefix(pattern, java_prefix);
48+
}
49+
50+
/// Create a lambda that returns the symbols that the given pattern should be
51+
/// loaded.If the pattern doesn't include a colon for matching the descriptor,
52+
/// append a `:\(.*\).*` to the regex. Note this will mean all overloaded
53+
/// methods will be marked as extra entry points for CI lazy loading.
54+
/// If the pattern doesn't include the java:: prefix, prefix that
55+
/// \param pattern: The user provided pattern
56+
/// \return The lambda to execute.
57+
std::function<std::vector<irep_idt>(const symbol_tablet &symbol_table)>
58+
build_load_method_by_regex(const std::string &pattern)
59+
{
60+
std::regex regex = build_regex_from_pattern(pattern);
61+
62+
return [=](const symbol_tablet &symbol_table) {
63+
std::vector<irep_idt> matched_methods;
64+
for(const auto &symbol : symbol_table.symbols)
65+
{
66+
if(symbol.second.is_function())
67+
{
68+
const std::string symbol_name = id2string(symbol.first);
69+
if(std::regex_match(symbol_name, regex))
70+
{
71+
matched_methods.push_back(symbol_name);
72+
}
73+
}
74+
}
75+
return matched_methods;
76+
};
7077
}

jbmc/src/java_bytecode/load_method_by_regex.h

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -17,20 +17,9 @@ Author: Diffblue Ltd.
1717

1818
class symbol_tablet;
1919

20-
class load_method_by_regext : public load_extra_methodst
21-
{
22-
public:
23-
explicit load_method_by_regext(const std::string &pattern);
20+
std::function<std::vector<irep_idt>(const symbol_tablet &symbol_table)>
21+
build_load_method_by_regex(const std::string &pattern);
2422

25-
std::vector<irep_idt>
26-
extra_methods(const symbol_tablet &symbol_table) const override;
27-
private:
28-
29-
std::regex regex;
30-
31-
static bool does_pattern_miss_descriptor(const std::string &pattern);
32-
33-
friend class load_method_by_regex_testt;
34-
};
23+
bool does_pattern_miss_descriptor(const std::string &pattern);
3524

3625
#endif // CPROVER_JAVA_BYTECODE_LOAD_METHOD_BY_REGEX_H

jbmc/unit/java_bytecode/load_method_by_regex.cpp

Lines changed: 8 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -10,15 +10,6 @@
1010
#include <testing-utils/catch.hpp>
1111
#include <testing-utils/require_vectors_equal_unordered.h>
1212

13-
class load_method_by_regex_testt
14-
{
15-
public:
16-
static bool does_pattern_miss_descriptor(const std::string &pattern)
17-
{
18-
return load_method_by_regext::does_pattern_miss_descriptor(pattern);
19-
}
20-
};
21-
2213
SCENARIO(
2314
"load_method_by_regex::does_pattern_miss_descriptor",
2415
"[core][java_bytecode][load_method_by_regex]")
@@ -28,8 +19,7 @@ SCENARIO(
2819
const std::string pattern = "java::com.diffblue.ClassName.methodName";
2920
WHEN("When calling does_pattern_miss_descriptor")
3021
{
31-
bool result =
32-
load_method_by_regex_testt::does_pattern_miss_descriptor(pattern);
22+
bool result = does_pattern_miss_descriptor(pattern);
3323
THEN("It should miss discriptor")
3424
{
3525
REQUIRE(result);
@@ -41,8 +31,7 @@ SCENARIO(
4131
const std::string pattern = "java::com.diffblue.ClassName.methodName:()V";
4232
WHEN("When calling does_pattern_miss_descriptor")
4333
{
44-
bool result =
45-
load_method_by_regex_testt::does_pattern_miss_descriptor(pattern);
34+
bool result = does_pattern_miss_descriptor(pattern);
4635
THEN("It should have the discriptor")
4736
{
4837
REQUIRE_FALSE(result);
@@ -54,8 +43,7 @@ SCENARIO(
5443
const std::string pattern = "com.diffblue.ClassName.methodName";
5544
WHEN("When calling does_pattern_miss_descriptor")
5645
{
57-
bool result =
58-
load_method_by_regex_testt::does_pattern_miss_descriptor(pattern);
46+
bool result = does_pattern_miss_descriptor(pattern);
5947
THEN("It should miss discriptor")
6048
{
6149
REQUIRE(result);
@@ -67,8 +55,7 @@ SCENARIO(
6755
const std::string pattern = "com.diffblue.ClassName.methodName:()V";
6856
WHEN("When calling does_pattern_miss_descriptor")
6957
{
70-
bool result =
71-
load_method_by_regex_testt::does_pattern_miss_descriptor(pattern);
58+
bool result = does_pattern_miss_descriptor(pattern);
7259
THEN("It should have the discriptor")
7360
{
7461
REQUIRE_FALSE(result);
@@ -80,8 +67,7 @@ SCENARIO(
8067
const std::string pattern = "java:com.diffblue.ClassName.methodName";
8168
WHEN("When calling does_pattern_miss_descriptor")
8269
{
83-
bool result =
84-
load_method_by_regex_testt::does_pattern_miss_descriptor(pattern);
70+
bool result = does_pattern_miss_descriptor(pattern);
8571
THEN("It should classify the last : as a descriptor")
8672
{
8773
REQUIRE_FALSE(result);
@@ -93,8 +79,7 @@ SCENARIO(
9379
const std::string pattern = "java:com.diffblue.ClassName.methodName:()V";
9480
WHEN("When calling does_pattern_miss_descriptor")
9581
{
96-
bool result =
97-
load_method_by_regex_testt::does_pattern_miss_descriptor(pattern);
82+
bool result = does_pattern_miss_descriptor(pattern);
9883
THEN("It should have the discriptor")
9984
{
10085
REQUIRE_FALSE(result);
@@ -118,8 +103,8 @@ static void require_result_for_pattern(
118103
{
119104
WHEN("Constructing a load_method_by_regex")
120105
{
121-
load_method_by_regext matcher{pattern};
122-
const auto &results = matcher.extra_methods(symbol_table);
106+
const auto matcher = build_load_method_by_regex(pattern);
107+
const auto &results = matcher(symbol_table);
123108
if(expected.size() == 1)
124109
{
125110
THEN("Expect " + id2string(expected[0]))

0 commit comments

Comments
 (0)