Skip to content

Commit a7d8bb9

Browse files
committed
Add new jbmc option --static-values
The option expects the path to a JSON file as an argument, and the file is expected to contain a map of maps: the first map uses class names as keys, the inner maps use field names, and the values of the inner maps are initial values of static fields. This path is then stored in a new field of java_bytecode_languaget. From here, we will be able to look for the file if it was specified, parse it, and construct assignments that are equivalent to and replace the clinit function.
1 parent 85c8fe0 commit a7d8bb9

File tree

2 files changed

+18
-2
lines changed

2 files changed

+18
-2
lines changed

jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,10 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
8787
options.set_option(
8888
"java-cp-include-files", cmd.get_value("java-cp-include-files"));
8989
}
90+
if(cmd.isset("static-values"))
91+
{
92+
options.set_option("static-values", cmd.get_value("static-values"));
93+
}
9094
}
9195

9296
/// Consume options that are java bytecode specific.
@@ -177,6 +181,7 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
177181
java_cp_include_files=".*";
178182

179183
nondet_static = options.get_bool_option("nondet-static");
184+
static_values_file = options.get_option("static-values");
180185

181186
language_options_initialized=true;
182187
}

jbmc/src/java_bytecode/java_bytecode_language.h

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,8 @@ Author: Daniel Kroening, [email protected]
3939
"(no-lazy-methods)" \
4040
"(lazy-methods-extra-entry-point):" \
4141
"(java-load-class):" \
42-
"(java-no-load-class):"
42+
"(java-no-load-class):" \
43+
"(static-values):"
4344

4445
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
4546
" --disable-uncaught-exception-check\n" \
@@ -71,7 +72,13 @@ Author: Daniel Kroening, [email protected]
7172
" METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \
7273
" against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \
7374
" will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \
74-
" overloads of a method will also be added.\n"
75+
" overloads of a method will also be added.\n" \
76+
" --static-values f Load initial values of static fields from the given\n"/* NOLINT(*) */ \
77+
" JSON file. We assign static fields to these values\n"/* NOLINT(*) */ \
78+
" instead of calling the normal static initializer\n"/* NOLINT(*) */ \
79+
" (clinit) method.\n" \
80+
" The argument can be a relative or absolute path to\n"/* NOLINT(*) */ \
81+
" the file.\n"
7582
// clang-format on
7683

7784
class symbolt;
@@ -197,6 +204,10 @@ class java_bytecode_languaget:public languaget
197204
java_string_library_preprocesst string_preprocess;
198205
std::string java_cp_include_files;
199206
bool nondet_static;
207+
/// Path to a JSON file which contains initial values of static fields (right
208+
/// after the static initializer of the class was run). This is read from the
209+
/// --static-values command-line option.
210+
std::string static_values_file;
200211

201212
// list of classes to force load even without reference from the entry point
202213
std::vector<irep_idt> java_load_classes;

0 commit comments

Comments
 (0)