Skip to content

Commit 9c0e0d3

Browse files
owen-mc-diffblueowen-mc-diffblue
authored
Merge pull request #5115 from antlechner/antonia/context-include
[TG-9294][UFC] Fix context-include/exclude jbmc options
2 parents c7e449b + ceb297d commit 9c0e0d3

33 files changed

+366
-77
lines changed

‎jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.class

1.01 KB
Binary file not shown.

‎jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.java

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
import org.cprover.other.MyOther;
2+
import org.cprover.other.Parent;
3+
import org.cprover.other.Child;
4+
5+
public class ExcludedProperties {
6+
7+
public static void parameters() {
8+
int i = MyOther.identity(21);
9+
assert (i == 21);
10+
}
11+
12+
public static void compileTimeReturnType() {
13+
Parent p = MyOther.subclass();
14+
assert (p == null || p instanceof Parent);
15+
if (p == null) {
16+
assert false; // reachable with "return nondet" body
17+
} else {
18+
if (p.num() == 1) {
19+
assert false; // reachable with "return nondet" body
20+
} else {
21+
assert false; // reachable with "return nondet" body
22+
}
23+
}
24+
}
25+
26+
public static void runtimeReturnType() {
27+
Parent p = MyOther.subclass();
28+
assert (p == null || p instanceof Child);
29+
}
30+
}

‎jbmc/regression/jbmc/context-include-exclude/Main.class

-106 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/context-include-exclude/Main.java

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import org.cprover.MyClass;
2+
import org.cprover.other.MyOther;
23

34
public class Main {
45
public static void main(String[] args) {
@@ -7,9 +8,11 @@ public static void main(String[] args) {
78
MyClass m = new MyClass(y);
89
int z = m.get();
910
int w = MyClass.Inner.doIt(z);
11+
int u = MyOther.identity(w);
1012
assert(x == y);
1113
assert(y == z);
1214
assert(z == w);
15+
assert (w == u);
1316
}
1417

1518
public static int myMethod(int x) {

‎jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.class

262 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
package org.cprover.other;
2+
3+
public class Child extends Parent {
4+
5+
public int num() { return 2; }
6+
}

‎jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.class

386 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package org.cprover.other;
2+
3+
public class MyOther {
4+
5+
public static int identity(int x) { return x; }
6+
7+
public static Parent subclass() { return new Child(); }
8+
}

‎jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.class

298 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.java

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package org.cprover.other;
2+
3+
public class Parent {
4+
5+
int field = 1;
6+
7+
public int num() { return field; }
8+
}

‎jbmc/regression/jbmc/context-include-exclude/test_exclude_absent.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
Main.class
3+
--context-exclude org.cprover.oh
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: SUCCESS
9+
.* line 15 assertion at file Main.java line 15 .*: SUCCESS
10+
--
11+
WARNING: no body for function .*
12+
--
13+
Tests that when --context-exclude is given a package prefix that does not occur
14+
anywhere on the classpath, it has no effect.

‎jbmc/regression/jbmc/context-include-exclude/test_exclude_from_all.desc

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,11 @@ Main.class
33
--context-exclude 'org.cprover.MyClass$Inner.'
44
^EXIT=10$
55
^SIGNAL=0$
6-
.* line 10 assertion at file Main.java line 10 .*: SUCCESS
7-
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
8-
.* line 12 assertion at file Main.java line 12 .*: FAILURE
9-
WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
6+
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: FAILURE
9+
.* line 15 assertion at file Main.java line 15 .*: SUCCESS
1010
--
11-
WARNING: no body for function .*clinit_wrapper
12-
WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
13-
WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
14-
WARNING: no body for function java::Main\.myMethod:\(I\)I
11+
WARNING: no body for function .*
1512
--
1613
Tests that no methods except those in the specified class are excluded.

‎jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,12 @@ Main.class
33
--context-include Main.main --context-include 'Main.<clinit' --context-include org.cprover.MyClass --context-exclude 'org.cprover.MyClass$Inner.'
44
^EXIT=10$
55
^SIGNAL=0$
6-
.* line 10 assertion at file Main.java line 10 .*: FAILURE
7-
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
86
.* line 12 assertion at file Main.java line 12 .*: FAILURE
9-
WARNING: no body for function java::Main\.myMethod:\(I\)I
10-
WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: FAILURE
9+
.* line 15 assertion at file Main.java line 15 .*: FAILURE
1110
--
12-
WARNING: no body for function .*clinit_wrapper
13-
WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
14-
WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
11+
WARNING: no body for function .*
1512
--
1613
Tests that only the specified methods and classes are included, while
1714
the inner class from MyClass is excluded.

‎jbmc/regression/jbmc/context-include-exclude/test_exclude_package_prefix.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
Main.class
3+
--context-include Main --context-include org.cprover --context-exclude org.cprover.ot
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: SUCCESS
9+
.* line 15 assertion at file Main.java line 15 .*: FAILURE
10+
--
11+
WARNING: no body for function .*
12+
--
13+
Tests that --context-exclude works with an argument that is the prefix of a
14+
package name.

‎jbmc/regression/jbmc/context-include-exclude/test_excluded_deleted_original_body.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
ExcludedProperties.class
3+
--context-exclude org.cprover.other --function ExcludedProperties.runtimeReturnType
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
.* line 28 assertion at file ExcludedProperties.java line 28.*: FAILURE
7+
--
8+
--
9+
Test that for an excluded method, we do not convert its "real" body from the
10+
bytecode.
11+
We instead assign it a "return nondet" body as for stubbed methods, which is
12+
tested by test_excluded_has_nondet_body.desc.

‎jbmc/regression/jbmc/context-include-exclude/test_excluded_has_nondet_body.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
ExcludedProperties.class
3+
--context-exclude org.cprover.other --function ExcludedProperties.compileTimeReturnType
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
.* line 14 assertion at file ExcludedProperties.java line 14 .*: SUCCESS
7+
.* line 16 assertion at file ExcludedProperties.java line 16 .*: FAILURE
8+
.* line 19 assertion at file ExcludedProperties.java line 19 .*: FAILURE
9+
.* line 21 assertion at file ExcludedProperties.java line 21 .*: FAILURE
10+
--
11+
--
12+
Test that for an excluded method, we keep the information about the
13+
(compile-time) return type of the method and return a nondet object of that
14+
type, or null.
15+
Note that we do this in the same way as for stubbed methods.

‎jbmc/regression/jbmc/context-include-exclude/test_excluded_has_parameter_info.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
ExcludedProperties.class
3+
--context-exclude org.cprover.other --show-symbol-table --function ExcludedProperties.parameters
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
java::org\.cprover\.other\.MyOther\.identity:\(I\)I::arg0i
7+
--
8+
java::org\.cprover\.other\.MyOther\.identity:\(I\)I::stub
9+
--
10+
Test that for an excluded method, we still create a symbol for its parameter(s)
11+
just like for non-excluded methods.
12+
Only the body of excluded methods should be missing, not their signature or
13+
other "meta-information".

‎jbmc/regression/jbmc/context-include-exclude/test_include.desc

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,11 @@ Main.class
33
--context-include Main.
44
^EXIT=10$
55
^SIGNAL=0$
6-
.* line 10 assertion at file Main.java line 10 .*: SUCCESS
7-
.* line 11 assertion at file Main.java line 11 .*: FAILURE
8-
.* line 12 assertion at file Main.java line 12 .*: FAILURE
9-
WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
10-
WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
11-
WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
6+
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: FAILURE
8+
.* line 14 assertion at file Main.java line 14 .*: FAILURE
9+
.* line 15 assertion at file Main.java line 15 .*: FAILURE
1210
--
13-
WARNING: no body for function .*clinit_wrapper
14-
WARNING: no body for function java::Main\.myMethod:\(I\)I
11+
WARNING: no body for function .*
1512
--
1613
Tests that only methods from the specified class are included.

‎jbmc/regression/jbmc/context-include-exclude/test_include_all.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ Main.class
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
.* line 10 assertion at file Main.java line 10 .*: SUCCESS
7-
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
86
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: SUCCESS
9+
.* line 15 assertion at file Main.java line 15 .*: SUCCESS
910
--
1011
WARNING: no body for function .*
1112
--

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -425,7 +425,8 @@ static irep_idt get_method_identifier(
425425

426426
void java_bytecode_convert_methodt::convert(
427427
const symbolt &class_symbol,
428-
const methodt &m)
428+
const methodt &m,
429+
const optionalt<prefix_filtert> &method_context)
429430
{
430431
// Construct the fully qualified method name
431432
// (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
@@ -605,8 +606,12 @@ void java_bytecode_convert_methodt::convert(
605606
if((!m.is_abstract) && (!m.is_native))
606607
{
607608
code_blockt code(convert_parameter_annotations(m, method_type));
608-
code.append(convert_instructions(m));
609-
method_symbol.value = std::move(code);
609+
// Do not convert if method is not in context
610+
if(!method_context || (*method_context)(id2string(method_identifier)))
611+
{
612+
code.append(convert_instructions(m));
613+
method_symbol.value = std::move(code);
614+
}
610615
}
611616
}
612617

@@ -3184,7 +3189,8 @@ void java_bytecode_convert_method(
31843189
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
31853190
java_string_library_preprocesst &string_preprocess,
31863191
const class_hierarchyt &class_hierarchy,
3187-
bool threading_support)
3192+
bool threading_support,
3193+
const optionalt<prefix_filtert> &method_context)
31883194

31893195
{
31903196
java_bytecode_convert_methodt java_bytecode_convert_method(
@@ -3197,7 +3203,7 @@ void java_bytecode_convert_method(
31973203
class_hierarchy,
31983204
threading_support);
31993205

3200-
java_bytecode_convert_method(class_symbol, method);
3206+
java_bytecode_convert_method(class_symbol, method, method_context);
32013207
}
32023208

32033209
/// Returns true iff method \p methodid from class \p classname is

‎jbmc/src/java_bytecode/java_bytecode_convert_method.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/symbol_table.h>
2121

2222
class class_hierarchyt;
23+
class prefix_filtert;
2324

2425
void java_bytecode_initialize_parameter_names(
2526
symbolt &method_symbol,
@@ -37,7 +38,8 @@ void java_bytecode_convert_method(
3738
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
3839
java_string_library_preprocesst &string_preprocess,
3940
const class_hierarchyt &class_hierarchy,
40-
bool threading_support);
41+
bool threading_support,
42+
const optionalt<prefix_filtert> &method_context);
4143

4244
void create_method_stub_symbol(
4345
const irep_idt &identifier,

‎jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -61,9 +61,12 @@ class java_bytecode_convert_methodt:public messaget
6161
typedef methodt::local_variable_tablet local_variable_tablet;
6262
typedef methodt::local_variablet local_variablet;
6363

64-
void operator()(const symbolt &class_symbol, const methodt &method)
64+
void operator()(
65+
const symbolt &class_symbol,
66+
const methodt &method,
67+
const optionalt<prefix_filtert> &method_context)
6568
{
66-
convert(class_symbol, method);
69+
convert(class_symbol, method, method_context);
6770
}
6871

6972
typedef uint16_t method_offsett;
@@ -290,7 +293,10 @@ class java_bytecode_convert_methodt:public messaget
290293
bool allow_merge = true);
291294

292295
// conversion
293-
void convert(const symbolt &class_symbol, const methodt &);
296+
void convert(
297+
const symbolt &class_symbol,
298+
const methodt &,
299+
const optionalt<prefix_filtert> &method_context);
294300

295301
code_blockt convert_parameter_annotations(
296302
const methodt &method,

‎jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 24 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
104104
}
105105
}
106106

107-
static prefix_filtert get_context(const optionst &options)
107+
prefix_filtert get_context(const optionst &options)
108108
{
109109
std::vector<std::string> context_include;
110110
std::vector<std::string> context_exclude;
@@ -245,7 +245,7 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
245245
options.get_bool_option("ignore-manifest-main-class");
246246

247247
if(options.is_set("context-include") || options.is_set("context-exclude"))
248-
method_in_context = get_context(options);
248+
method_context = get_context(options);
249249

250250
language_options_initialized=true;
251251
}
@@ -1173,12 +1173,6 @@ bool java_bytecode_languaget::convert_single_method(
11731173
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
11741174
lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
11751175
{
1176-
// Do not convert if method is not in context
1177-
if(method_in_context && !(*method_in_context)(id2string(function_id)))
1178-
{
1179-
return false;
1180-
}
1181-
11821176
const symbolt &symbol = symbol_table.lookup_ref(function_id);
11831177

11841178
// Nothing to do if body is already loaded
@@ -1312,29 +1306,33 @@ bool java_bytecode_languaget::convert_single_method(
13121306
std::move(needed_lazy_methods),
13131307
string_preprocess,
13141308
class_hierarchy,
1315-
threading_support);
1309+
threading_support,
1310+
method_context);
13161311
INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
13171312
return false;
13181313
}
13191314

1320-
// The return of an opaque function is a source of an otherwise invisible
1321-
// instantiation, so here we ensure we've loaded the appropriate classes.
1322-
const java_method_typet function_type = to_java_method_type(symbol.type);
1323-
if(
1324-
const pointer_typet *pointer_return_type =
1325-
type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1315+
if(needed_lazy_methods)
13261316
{
1327-
// If the return type is abstract, we won't forcibly instantiate it here
1328-
// otherwise this can cause abstract methods to be explictly called
1329-
// TODO(tkiley): Arguably no abstract class should ever be added to
1330-
// TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1331-
// TODO(tkiley): investigation
1332-
namespacet ns{symbol_table};
1333-
const java_class_typet &underlying_type =
1334-
to_java_class_type(ns.follow(pointer_return_type->subtype()));
1335-
1336-
if(!underlying_type.is_abstract())
1337-
needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1317+
// The return of an opaque function is a source of an otherwise invisible
1318+
// instantiation, so here we ensure we've loaded the appropriate classes.
1319+
const java_method_typet function_type = to_java_method_type(symbol.type);
1320+
if(
1321+
const pointer_typet *pointer_return_type =
1322+
type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1323+
{
1324+
// If the return type is abstract, we won't forcibly instantiate it here
1325+
// otherwise this can cause abstract methods to be explictly called
1326+
// TODO(tkiley): Arguably no abstract class should ever be added to
1327+
// TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1328+
// TODO(tkiley): investigation
1329+
namespacet ns{symbol_table};
1330+
const java_class_typet &underlying_type =
1331+
to_java_class_type(ns.follow(pointer_return_type->subtype()));
1332+
1333+
if(!underlying_type.is_abstract())
1334+
needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1335+
}
13381336
}
13391337

13401338
INVARIANT(declaring_class(symbol), "Method must have a declaring class.");

0 commit comments

Comments
 (0)