Skip to content

Commit ed34a73

Browse files
author
Matthias Güdemann
committed
support class load configuration via JSON file
e.g. ``` { "jar": [ "A.jar", "B.jar" ], "classFiles": [ "jarfile3$A.class", "jarfile3.class" ] } ```
1 parent b236ee4 commit ed34a73

File tree

10 files changed

+60
-17
lines changed

10 files changed

+60
-17
lines changed

‎src/cbmc/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
2828
../assembler/assembler$(LIBEXT) \
2929
../solvers/solvers$(LIBEXT) \
3030
../util/util$(LIBEXT) \
31-
../miniz/miniz$(OBJEXT)
31+
../miniz/miniz$(OBJEXT) \
32+
../json/json$(LIBEXT)
3233

3334
INCLUDES= -I ..
3435

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1155,7 +1155,7 @@ void cbmc_parse_optionst::help()
11551155
// NOLINTNEXTLINE(whitespace/line_length)
11561156
" --java-max-vla-length limit the length of user-code-created arrays\n"
11571157
// NOLINTNEXTLINE(whitespace/line_length)
1158-
" --java-cp-include-files regexp of class files to load\n"
1158+
" --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n"
11591159
" --java-unwind-enum-static try to unwind loops in static initialization of enums\n"
11601160
"\n"
11611161
"Semantic transformations:\n"

‎src/cegis/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
116116
../cbmc/cbmc_dimacs$(OBJEXT) ../cbmc/all_properties$(OBJEXT) \
117117
../cbmc/fault_localization$(OBJEXT) \
118118
../cbmc/symex_coverage$(OBJEXT) \
119-
../miniz/miniz$(OBJEXT)
119+
../miniz/miniz$(OBJEXT) \
120+
../json/json$(LIBEXT)
120121

121122
INCLUDES= -I ..
122123

‎src/goto-cc/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,8 @@ OBJ += ../big-int/big-int$(LIBEXT) \
1414
../xmllang/xmllang$(LIBEXT) \
1515
../assembler/assembler$(LIBEXT) \
1616
../langapi/langapi$(LIBEXT) \
17-
../miniz/miniz$(OBJEXT)
17+
../miniz/miniz$(OBJEXT) \
18+
../json/json$(LIBEXT)
1819

1920
INCLUDES= -I ..
2021

‎src/goto-diff/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1414
../xmllang/xmllang$(LIBEXT) \
1515
../util/util$(LIBEXT) \
1616
../solvers/solvers$(LIBEXT) \
17-
../miniz/miniz$(OBJEXT)
17+
../miniz/miniz$(OBJEXT) \
18+
../json/json$(LIBEXT)
1819

1920
INCLUDES= -I ..
2021

‎src/goto-instrument/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
3838
../xmllang/xmllang$(LIBEXT) \
3939
../util/util$(LIBEXT) \
4040
../solvers/solvers$(LIBEXT) \
41-
../miniz/miniz$(OBJEXT)
41+
../miniz/miniz$(OBJEXT) \
42+
../json/json$(LIBEXT)
4243

4344
INCLUDES= -I ..
4445

‎src/java_bytecode/jar_file.cpp

Lines changed: 42 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,11 @@ Author: Daniel Kroening, [email protected]
88

99
#include <cstring>
1010
#include <cassert>
11-
#include <sstream>
11+
#include <json/json_parser.h>
12+
#include <unordered_set>
1213
#include "jar_file.h"
1314
#include <util/suffix.h>
14-
15+
#include <iostream>
1516
/*******************************************************************\
1617
1718
Function: jar_filet::open
@@ -24,7 +25,9 @@ Function: jar_filet::open
2425
2526
\*******************************************************************/
2627

27-
void jar_filet::open(std::string &java_cp_include_files, const std::string &filename)
28+
void jar_filet::open(
29+
std::string &java_cp_include_files,
30+
const std::string &filename)
2831
{
2932
if(!mz_ok)
3033
{
@@ -35,6 +38,32 @@ void jar_filet::open(std::string &java_cp_include_files, const std::string &file
3538

3639
if(mz_ok)
3740
{
41+
// '@' signals file reading with list of class files to load
42+
bool regex_match=java_cp_include_files[0]!='@';
43+
std::regex regex_matcher;
44+
std::smatch string_matcher;
45+
std::unordered_set<std::string> set_matcher;
46+
jsont json_cp_config;
47+
if(regex_match)
48+
regex_matcher=std::regex(java_cp_include_files);
49+
else
50+
{
51+
assert(java_cp_include_files.length()>1);
52+
if(parse_json(
53+
java_cp_include_files.substr(1),
54+
get_message_handler(),
55+
json_cp_config))
56+
throw "cannot read JSON input configuration for JAR loading";
57+
assert(json_cp_config.is_object() && "JSON has wrong format");
58+
jsont include_files=json_cp_config["classFiles"];
59+
assert(include_files.is_array() && "JSON has wrong format");
60+
for(const jsont &file_entry : include_files.array)
61+
{
62+
assert(file_entry.is_string());
63+
set_matcher.insert(file_entry.value);
64+
}
65+
}
66+
3867
std::size_t number_of_files=
3968
mz_zip_reader_get_num_files(&zip);
4069

@@ -47,11 +76,16 @@ void jar_filet::open(std::string &java_cp_include_files, const std::string &file
4776
mz_zip_reader_get_filename(&zip, i, filename_char, filename_length);
4877
assert(filename_length==filename_len);
4978
std::string file_name(filename_char);
50-
std::smatch string_matcher;
51-
std::regex matcher(java_cp_include_files);
52-
// load .class files only if they match regex
53-
if(std::regex_match(file_name, string_matcher, matcher) ||
54-
!has_suffix(file_name, ".class"))
79+
80+
// non-class files are loaded in any case
81+
bool add_file=!has_suffix(file_name, ".class");
82+
// load .class file only if they match regex
83+
if(regex_match)
84+
add_file|=std::regex_match(file_name, string_matcher, regex_matcher);
85+
// load .class file only if it is in the match set
86+
else
87+
add_file|=set_matcher.count(file_name)>0;
88+
if(add_file)
5589
{
5690
index.push_back(file_name);
5791
filtered_jar[filtered_index]=i;

‎src/java_bytecode/jar_file.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,9 @@ Author: Daniel Kroening, [email protected]
1616
#include <vector>
1717
#include <map>
1818
#include <regex>
19+
#include <util/message.h>
1920

20-
class jar_filet
21+
class jar_filet:public messaget
2122
{
2223
public:
2324
jar_filet():mz_ok(false) { }
@@ -48,7 +49,7 @@ class jar_filet
4849
std::map<int, int> index_map;
4950
};
5051

51-
class jar_poolt
52+
class jar_poolt:public messaget
5253
{
5354
public:
5455
void set_java_cp_include_files(std::string &_java_cp_include_files)
@@ -62,6 +63,7 @@ class jar_poolt
6263
if(it==file_map.end())
6364
{
6465
jar_filet &jar_file=file_map[file_name];
66+
jar_file.set_message_handler(get_message_handler());
6567
jar_file.open(java_cp_include_files, file_name);
6668
return jar_file;
6769
}

‎src/java_bytecode/java_class_loader.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ class java_class_loadert:public messaget
2323
void set_java_cp_include_files(std::string &java_cp_include_files)
2424
{
2525
jar_pool.set_java_cp_include_files(java_cp_include_files);
26+
jar_pool.set_message_handler(get_message_handler());
2627
}
2728

2829
// maps class names to the parse trees

‎src/symex/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1717
../pointer-analysis/dereference$(OBJEXT) \
1818
../goto-instrument/cover$(OBJEXT) \
1919
../path-symex/path-symex$(LIBEXT) \
20-
../miniz/miniz$(OBJEXT)
20+
../miniz/miniz$(OBJEXT) \
21+
../json/json$(LIBEXT)
2122

2223
INCLUDES= -I ..
2324

0 commit comments

Comments
 (0)