cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
java_class_loader_limit.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: limit class path loading
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
java_class_loader_limit.h
"
13
14
#include <
json/json_parser.h
>
15
16
#include <
util/invariant.h
>
17
50
void
java_class_loader_limitt::setup_class_load_limit
(
51
const
std::string &java_cp_include_files)
52
{
53
PRECONDITION
(!java_cp_include_files.empty());
54
55
// '@' signals file reading with list of class files to load
56
use_regex_match
= java_cp_include_files[0] !=
'@'
;
57
if
(
use_regex_match
)
58
{
59
regex_matcher
=std::regex(java_cp_include_files);
60
log
.debug() <<
"Limit loading to classes matching '"
61
<< java_cp_include_files <<
"'"
<<
messaget::eom
;
62
}
63
else
64
{
65
PRECONDITION
(java_cp_include_files.length() > 1);
66
jsont
json_cp_config;
67
if
(
parse_json
(
68
java_cp_include_files.substr(1),
69
log
.get_message_handler(),
70
json_cp_config))
71
throw
"cannot read JSON input configuration for JAR loading"
;
72
if
(!json_cp_config.
is_object
())
73
throw
"the JSON file has a wrong format"
;
74
jsont
include_files=json_cp_config[
"classFiles"
];
75
if
(!include_files.
is_null
() && !include_files.
is_array
())
76
throw
"the JSON file has a wrong format"
;
77
for
(
const
jsont
&file_entry :
to_json_array
(include_files))
78
{
79
PRECONDITION
(file_entry.is_string());
80
set_matcher
.insert(file_entry.value);
81
}
82
}
83
}
84
89
bool
java_class_loader_limitt::load_class_file
(
const
std::string &file_name)
90
{
91
if
(
use_regex_match
)
92
{
93
std::smatch string_matches;
94
if
(std::regex_match(file_name, string_matches,
regex_matcher
))
95
return
true
;
96
log
.debug() << file_name +
" discarded since not matching loader regexp"
97
<<
messaget::eom
;
98
return
false
;
99
}
100
else
101
// load .class file only if it is in the match set
102
return
set_matcher
.find(file_name) !=
set_matcher
.end();
103
}
java_class_loader_limitt::setup_class_load_limit
void setup_class_load_limit(const std::string &)
Initializes class with either regex matcher or match set.
Definition
java_class_loader_limit.cpp:50
java_class_loader_limitt::use_regex_match
bool use_regex_match
Whether to use regex_matcher instead of set_matcher.
Definition
java_class_loader_limit.h:26
java_class_loader_limitt::log
messaget log
Definition
java_class_loader_limit.h:23
java_class_loader_limitt::set_matcher
std::set< std::string > set_matcher
Definition
java_class_loader_limit.h:28
java_class_loader_limitt::load_class_file
bool load_class_file(const std::string &class_file_name)
Use the class load limiter to decide whether a class file should be loaded or not.
Definition
java_class_loader_limit.cpp:89
java_class_loader_limitt::regex_matcher
std::regex regex_matcher
Definition
java_class_loader_limit.h:27
jsont
Definition
json.h:27
jsont::is_array
bool is_array() const
Definition
json.h:61
jsont::is_null
bool is_null() const
Definition
json.h:81
jsont::is_object
bool is_object() const
Definition
json.h:56
messaget::eom
static eomt eom
Definition
message.h:289
java_class_loader_limit.h
limit class path loading
to_json_array
json_arrayt & to_json_array(jsont &json)
Definition
json.h:424
parse_json
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition
json_parser.cpp:27
json_parser.h
invariant.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
jbmc
src
java_bytecode
java_class_loader_limit.cpp
Generated by
1.17.0