Skip to content

Commit 7150660

Browse files
smowtonsmowton
authored
Merge pull request #1221 from smowton/smowton/feature/force_load_method
Allow extra entry-points to be specified for CI lazy loading
2 parents e6f02bc + 51f088a commit 7150660

32 files changed

+347
-89
lines changed

‎regression/cbmc-java/lazyloading10/test.class

444 Bytes
Binary file not shown.

‎regression/cbmc-java/lazyloading10/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.class
3+
--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
entry point 'test\.sety' is ambiguous between:
7+
test\.sety:\(I\)V
8+
test\.sety:\(F\)V

‎regression/cbmc-java/lazyloading10/test.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
public class test {
2+
3+
int x;
4+
int y;
5+
6+
public test() { x = 1; y = 2; }
7+
public void setx(int _x) { x = _x; }
8+
public void sety(int _y) { y = _y; }
9+
public void sety(float _y) { y = (int)_y; }
10+
public void f() { }
11+
12+
}
13+
14+

‎regression/cbmc-java/lazyloading11/test.class

444 Bytes
Binary file not shown.

‎regression/cbmc-java/lazyloading11/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.class
3+
--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(I)V" --lazy-methods-extra-entry-point "test.sety:(F)V"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
CI lazy methods: elaborate java::test\.sety:\(I\)V
8+
CI lazy methods: elaborate java::test\.sety:\(F\)V
9+
--
10+
CI lazy methods: elaborate java::test\.setx:\(I\)V

‎regression/cbmc-java/lazyloading11/test.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
public class test {
2+
3+
int x;
4+
int y;
5+
6+
public test() { x = 1; y = 2; }
7+
public void setx(int _x) { x = _x; }
8+
public void sety(int _y) { y = _y; }
9+
public void sety(float _y) { y = (int)_y; }
10+
public void f() { }
11+
12+
}
13+
14+

‎regression/cbmc-java/lazyloading6/test.class

444 Bytes
Binary file not shown.

‎regression/cbmc-java/lazyloading6/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.class
3+
--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.setx
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
CI lazy methods: elaborate java::test\.setx:\(I\)V
8+
--
9+
CI lazy methods: elaborate java::test\.sety:\(I\)V
10+
CI lazy methods: elaborate java::test\.sety:\(F\)V

‎regression/cbmc-java/lazyloading6/test.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
public class test {
2+
3+
int x;
4+
int y;
5+
6+
public test() { x = 1; y = 2; }
7+
public void setx(int _x) { x = _x; }
8+
public void sety(int _y) { y = _y; }
9+
public void sety(float _y) { y = (int)_y; }
10+
public void f() { }
11+
12+
}
13+
14+

‎regression/cbmc-java/lazyloading7/test.class

444 Bytes
Binary file not shown.

‎regression/cbmc-java/lazyloading7/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.class
3+
--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(I)V"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
CI lazy methods: elaborate java::test\.sety:\(I\)V
8+
--
9+
CI lazy methods: elaborate java::test\.setx:\(I\)V
10+
CI lazy methods: elaborate java::test\.sety:\(F\)V

‎regression/cbmc-java/lazyloading7/test.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
public class test {
2+
3+
int x;
4+
int y;
5+
6+
public test() { x = 1; y = 2; }
7+
public void setx(int _x) { x = _x; }
8+
public void sety(int _y) { y = _y; }
9+
public void sety(float _y) { y = (int)_y; }
10+
public void f() { }
11+
12+
}
13+
14+

‎regression/cbmc-java/lazyloading8/test.class

444 Bytes
Binary file not shown.

‎regression/cbmc-java/lazyloading8/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.class
3+
--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(F)V"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
CI lazy methods: elaborate java::test\.sety:\(F\)V
8+
--
9+
CI lazy methods: elaborate java::test\.sety:\(I\)V
10+
CI lazy methods: elaborate java::test\.setx:\(I\)V

‎regression/cbmc-java/lazyloading8/test.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
public class test {
2+
3+
int x;
4+
int y;
5+
6+
public test() { x = 1; y = 2; }
7+
public void setx(int _x) { x = _x; }
8+
public void sety(int _y) { y = _y; }
9+
public void sety(float _y) { y = (int)_y; }
10+
public void f() { }
11+
12+
}
13+
14+

‎regression/cbmc-java/lazyloading9/test.class

444 Bytes
Binary file not shown.

‎regression/cbmc-java/lazyloading9/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
test.class
3+
--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.*"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
CI lazy methods: elaborate java::test\.setx:\(I\)V
8+
CI lazy methods: elaborate java::test\.sety:\(I\)V
9+
CI lazy methods: elaborate java::test\.sety:\(F\)V

‎regression/cbmc-java/lazyloading9/test.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
public class test {
2+
3+
int x;
4+
int y;
5+
6+
public test() { x = 1; y = 2; }
7+
public void setx(int _x) { x = _x; }
8+
public void sety(int _y) { y = _y; }
9+
public void sety(float _y) { y = (int)_y; }
10+
public void f() { }
11+
12+
}
13+
14+

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1073,22 +1073,9 @@ void cbmc_parse_optionst::help()
10731073
"Java Bytecode frontend options:\n"
10741074
" --classpath dir/jar set the classpath\n"
10751075
" --main-class class-name set the name of the main class\n"
1076-
// NOLINTNEXTLINE(whitespace/line_length)
1077-
" --java-assume-inputs-non-null test harness makes input arguments not null\n"
1078-
// NOLINTNEXTLINE(whitespace/line_length)
1079-
" --java-max-input-array-length N maximum allowed length for an array passed as input\n"
1080-
// NOLINTNEXTLINE(whitespace/line_length)
1081-
" --java-max-input-tree-depth N object references are (deterministically) set to null in the object\n"
1082-
// NOLINTNEXTLINE(whitespace/line_length)
1083-
" hierarchy of input parameters when their depth is >= N and the object\n"
1084-
" type happens twice in the tree branch\n"
1085-
// NOLINTNEXTLINE(whitespace/line_length)
1086-
" --java-max-vla-length limit the length of user-code-created arrays\n"
1087-
// NOLINTNEXTLINE(whitespace/line_length)
1088-
" --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n"
1089-
// NOLINTNEXTLINE(whitespace/line_length)
1090-
" --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n"
1091-
// NOLINTNEXTLINE(whitespace/line_length)
1076+
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
1077+
// This one is handled by cbmc_parse_options not by the Java frontend,
1078+
// hence its presence here:
10921079
" --java-unwind-enum-static try to unwind loops in static initialization of enums\n"
10931080
"\n"
10941081
"Semantic transformations:\n"

‎src/cbmc/cbmc_parse_options.h

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
1919

2020
#include <analyses/goto_check.h>
2121

22+
#include <java_bytecode/java_bytecode_language.h>
23+
2224
#include "xml_interface.h"
2325

2426
class bmct;
@@ -64,14 +66,9 @@ class optionst;
6466
"(string-abstraction)(no-arch)(arch):" \
6567
"(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
6668
"(graphml-witness):" \
67-
"(java-max-vla-length):" \
69+
JAVA_BYTECODE_LANGUAGE_OPTIONS \
6870
"(java-unwind-enum-static)" \
69-
"(java-cp-include-files):" \
70-
"(java-throw-runtime-exceptions)" \
71-
"(java-max-input-array-length):" \
72-
"(java-max-input-tree-depth):" \
7371
"(localize-faults)(localize-faults-method):" \
74-
"(lazy-methods)" \
7572
"(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
7673

7774
class cbmc_parse_optionst:

‎src/clobber/clobber_parse_options.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -536,6 +536,8 @@ void clobber_parse_optionst::help()
536536
" --round-to-minus-inf IEEE floating point rounding mode\n"
537537
" --round-to-zero IEEE floating point rounding mode\n"
538538
"\n"
539+
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
540+
"\n"
539541
"Program instrumentation options:\n"
540542
HELP_GOTO_CHECK
541543
" --show-properties show the properties\n"

‎src/clobber/clobber_parse_options.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
2020
#include <analyses/goto_check.h>
2121
#include <goto-programs/show_goto_functions.h>
2222

23+
#include <java_bytecode/java_bytecode_language.h>
24+
2325
class goto_functionst;
2426
class optionst;
2527

@@ -32,7 +34,8 @@ class optionst;
3234
"(version)" \
3335
"(string-abstraction)" \
3436
"(show-locs)(show-vcc)(show-properties)(show-trace)" \
35-
"(property):"
37+
"(property):" \
38+
JAVA_BYTECODE_LANGUAGE_OPTIONS
3639

3740
class clobber_parse_optionst:
3841
public parse_options_baset,

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -493,6 +493,7 @@ void goto_analyzer_parse_optionst::help()
493493
"Java Bytecode frontend options:\n"
494494
" --classpath dir/jar set the classpath\n"
495495
" --main-class class-name set the name of the main class\n"
496+
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
496497
"\n"
497498
"Program representations:\n"
498499
" --show-parse-tree show parse tree\n"

‎src/goto-analyzer/goto_analyzer_parse_options.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
2222

2323
#include <analyses/goto_check.h>
2424

25+
#include <java_bytecode/java_bytecode_language.h>
26+
2527
class bmct;
2628
class goto_functionst;
2729
class optionst;
@@ -45,7 +47,8 @@ class optionst;
4547
"(unreachable-instructions)(unreachable-functions)" \
4648
"(reachable-functions)" \
4749
"(intervals)(show-intervals)" \
48-
"(non-null)(show-non-null)"
50+
"(non-null)(show-non-null)" \
51+
JAVA_BYTECODE_LANGUAGE_OPTIONS
4952

5053
class goto_analyzer_parse_optionst:
5154
public parse_options_baset,

‎src/java_bytecode/java_bytecode_language.cpp

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com
2828
#include "java_entry_point.h"
2929
#include "java_bytecode_parser.h"
3030
#include "java_class_loader.h"
31+
#include "java_utils.h"
3132

3233
#include "expr2java.h"
3334

@@ -54,6 +55,13 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
5455
else
5556
lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
5657

58+
const std::list<std::string> &extra_entry_points=
59+
cmd.get_values("lazy-methods-extra-entry-point");
60+
lazy_methods_extra_entry_points.insert(
61+
lazy_methods_extra_entry_points.end(),
62+
extra_entry_points.begin(),
63+
extra_entry_points.end());
64+
5765
if(cmd.isset("java-cp-include-files"))
5866
{
5967
java_cp_include_files=cmd.get_value("java-cp-include-files");
@@ -463,6 +471,54 @@ bool java_bytecode_languaget::typecheck(
463471
return false;
464472
}
465473

474+
/// Translates the given list of method names from human-readable to
475+
/// internal syntax.
476+
/// Expands any wildcards (entries ending in '.*') in the given method
477+
/// list to include all non-static methods defined on the given class.
478+
/// \param [in, out] methods: List of methods to expand. Any wildcard entries
479+
/// will be deleted and the expanded entries appended to the end.
480+
/// \param symbol_table: global symbol table
481+
static void resolve_method_names(
482+
std::vector<irep_idt> &methods,
483+
const symbol_tablet &symbol_table)
484+
{
485+
std::vector<irep_idt> new_methods;
486+
for(const irep_idt &method : methods)
487+
{
488+
const std::string &method_str=id2string(method);
489+
if(!has_suffix(method_str, ".*"))
490+
{
491+
std::string error_message;
492+
irep_idt internal_name=
493+
resolve_friendly_method_name(
494+
method_str,
495+
symbol_table,
496+
error_message);
497+
if(internal_name==irep_idt())
498+
throw "entry point "+error_message;
499+
new_methods.push_back(internal_name);
500+
}
501+
else
502+
{
503+
irep_idt classname="java::"+method_str.substr(0, method_str.length()-2);
504+
if(!symbol_table.has_symbol(classname))
505+
throw "wildcard entry point '"+method_str+"': unknown class";
506+
507+
for(const auto &name_symbol : symbol_table.symbols)
508+
{
509+
if(name_symbol.second.type.id()!=ID_code)
510+
continue;
511+
if(!to_code_type(name_symbol.second.type).has_this())
512+
continue;
513+
if(has_prefix(id2string(name_symbol.first), id2string(classname)))
514+
new_methods.push_back(name_symbol.first);
515+
}
516+
}
517+
}
518+
519+
methods=std::move(new_methods);
520+
}
521+
466522
/// Uses a simple context-insensitive ('ci') analysis to determine which methods
467523
/// may be reachable from the main entry point. In brief, static methods are
468524
/// reachable if we find a callsite in another reachable site, while virtual
@@ -512,6 +568,15 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
512568
else
513569
method_worklist2.push_back(main_function.main_function.name);
514570

571+
// Add any extra entry points specified; we should elaborate these in the
572+
// same way as the main function.
573+
std::vector<irep_idt> extra_entry_points=lazy_methods_extra_entry_points;
574+
resolve_method_names(extra_entry_points, symbol_table);
575+
method_worklist2.insert(
576+
method_worklist2.begin(),
577+
extra_entry_points.begin(),
578+
extra_entry_points.end());
579+
515580
std::set<irep_idt> needed_classes;
516581

517582
{

‎src/java_bytecode/java_bytecode_language.h

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,32 @@ Author: Daniel Kroening, kroening@kroening.com
1616
#include "java_class_loader.h"
1717
#include "java_string_library_preprocess.h"
1818

19+
#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
20+
"(java-assume-inputs-non-null)" \
21+
"(java-throw-runtime-exceptions)" \
22+
"(java-max-input-array-length):" \
23+
"(java-max-input-tree-depth):" \
24+
"(java-max-vla-length):" \
25+
"(java-cp-include-files):" \
26+
"(lazy-methods)" \
27+
"(lazy-methods-extra-entry-point):"
28+
29+
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
30+
" --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" \
31+
" entry point with null\n" \
32+
" --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" \
33+
" --java-max-input-array-length N limit input array size to <= N\n" \
34+
" --java-max-input-tree-depth N object references are (deterministically) set to null in\n"\
35+
" the object\n" \
36+
" --java-max-vla-length limit the length of user-code-created arrays\n" \
37+
" --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" \
38+
" --lazy-methods only translate methods that appear to be reachable from\n" \
39+
" the --function entry point or main class\n" \
40+
" --lazy-methods-extra-entry-point METHODNAME\n" \
41+
" treat METHODNAME as a possible program entry point for\n" \
42+
" the purpose of lazy method loading\n" \
43+
" A '.*' wildcard is allowed to specify all class members\n"
44+
1945
#define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
2046
#define MAX_NONDET_TREE_DEPTH 5
2147

@@ -107,6 +133,7 @@ class java_bytecode_languaget:public languaget
107133
size_t max_user_array_length; // max size for user code created arrays
108134
lazy_methodst lazy_methods;
109135
lazy_methods_modet lazy_methods_mode;
136+
std::vector<irep_idt> lazy_methods_extra_entry_points;
110137
bool string_refinement_enabled;
111138
bool throw_runtime_exceptions;
112139
java_string_library_preprocesst string_preprocess;

0 commit comments

Comments
 (0)