CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
java_class_loader_limit.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: limit class path loading
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <json/json_parser.h>
15
16#include <util/invariant.h>
17
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] != '@';
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);
67 if(parse_json(
68 java_cp_include_files.substr(1),
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
89bool java_class_loader_limitt::load_class_file(const std::string &file_name)
90{
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"
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void setup_class_load_limit(const std::string &)
Initializes class with either regex matcher or match set.
bool use_regex_match
Whether to use regex_matcher instead of set_matcher.
std::set< std::string > set_matcher
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 json.h:27
bool is_array() const
Definition json.h:61
bool is_null() const
Definition json.h:81
mstreamt & debug() const
Definition message.h:421
message_handlert & get_message_handler()
Definition message.h:183
static eomt eom
Definition message.h:289
limit class path loading
json_arrayt & to_json_array(jsont &json)
Definition json.h:424
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
#define PRECONDITION(CONDITION)
Definition invariant.h:463