Go to the documentation of this file.
51 "java-assume-inputs-non-null", cmd.
isset(
"java-assume-inputs-non-null"));
53 "throw-runtime-exceptions", cmd.
isset(
"throw-runtime-exceptions"));
55 "uncaught-exception-check", !cmd.
isset(
"disable-uncaught-exception-check"));
57 "throw-assertion-error", cmd.
isset(
"throw-assertion-error"));
60 if(cmd.
isset(
"java-max-vla-length"))
63 "java-max-vla-length", cmd.
get_value(
"java-max-vla-length"));
67 "symex-driven-lazy-loading", cmd.
isset(
"symex-driven-lazy-loading"));
69 if(cmd.
isset(
"java-load-class"))
72 if(cmd.
isset(
"java-no-load-class"))
75 "java-no-load-class", cmd.
get_values(
"java-no-load-class"));
77 if(cmd.
isset(
"lazy-methods-extra-entry-point"))
80 "lazy-methods-extra-entry-point",
81 cmd.
get_values(
"lazy-methods-extra-entry-point"));
83 if(cmd.
isset(
"java-cp-include-files"))
86 "java-cp-include-files", cmd.
get_value(
"java-cp-include-files"));
122 if(options.
is_set(
"java-load-class"))
128 if(options.
is_set(
"java-no-load-class"))
130 const auto &no_load_values = options.
get_list_option(
"java-no-load-class");
133 const std::list<std::string> &extra_entry_points =
136 extra_entry_points.begin(),
137 extra_entry_points.end(),
150 jsont json_cp_config;
155 throw "cannot read JSON input configuration for JAR loading";
158 throw "the JSON file has a wrong format";
159 jsont include_files=json_cp_config[
"jar"];
161 throw "the JSON file has a wrong format";
164 for(
const jsont &file_entry : include_files.
array)
168 "classpath entry must be jar filename, but '" + file_entry.
value +
184 return {
"class",
"jar" };
213 const std::string &path)
229 auto get_string_base_classes = [
this](
const irep_idt &
id) {
250 const std::string &entry_method =
config.
main;
252 if(!entry_method.empty())
254 const auto last_dot_position = entry_method.find_last_of(
'.');
255 main_class = entry_method.substr(0, last_dot_position);
260 std::string manifest_main_class = manifest[
"Main-Class"];
263 if(!manifest_main_class.empty())
273 status() <<
"JAR file without entry point: loading class files" <<
eom;
275 for(
const auto &c : classes)
311 if(instruction.
statement ==
"getfield" ||
314 const exprt &fieldref = instruction.
args[0];
316 const symbolt *class_symbol = symbol_table.
lookup(class_symbol_id);
318 class_symbol !=
nullptr,
319 "all types containing fields should have been loaded");
323 const irep_idt &component_name = fieldref.
get(ID_component_name);
329 symbolt &writable_class_symbol =
333 components.emplace_back(component_name, fieldref.
type());
334 components.back().set_base_name(component_name);
335 components.back().set_pretty_name(component_name);
342 !class_type->
bases().empty(),
344 +
"' (which was missing a field '" +
id2string(component_name)
345 +
"' referenced from method '" +
id2string(method.name)
346 +
"') should have an opaque superclass");
347 const auto &superclass_type = class_type->
bases().front().type();
348 class_symbol_id = superclass_type.get_identifier();
373 new_class_symbol.
type = symbol_expr.
type();
376 "class identifier should have 'java::' prefix");
379 new_class_symbol.
mode = ID_java;
383 new_class_symbol.
type.
set(ID_C_no_nondet_initialization,
true);
384 symbol_table.
add(new_class_symbol);
405 const exprt &ldc_arg0,
407 bool string_refinement_enabled)
409 if(ldc_arg0.
id() == ID_type)
416 else if(ldc_arg0.
id() == ID_java_string_literal)
421 ldc_arg0, symbol_table, string_refinement_enabled));
426 ldc_arg0.
id() == ID_constant,
427 "ldc argument should be constant, string literal or class literal");
444 bool string_refinement_enabled)
459 instruction.
args.size() != 0,
460 "ldc instructions should have an argument");
461 instruction.
args[0] =
465 string_refinement_enabled);
486 const typet &symbol_type,
488 bool force_nondet_init)
494 new_symbol.
name = symbol_id;
496 new_symbol.
type = symbol_type;
497 new_symbol.
type.
set(ID_C_class, class_id);
501 new_symbol.
type.
set(ID_C_access, ID_public);
503 new_symbol.
mode = ID_java;
508 if(symbol_type.
id() == ID_pointer && !force_nondet_init)
512 bool add_failed = symbol_table.
add(new_symbol);
514 !add_failed,
"caller should have checked symbol not already in table");
532 std::vector<irep_idt> classes_to_check;
533 classes_to_check.push_back(start_class_id);
535 while(!classes_to_check.empty())
537 irep_idt to_check = classes_to_check.back();
538 classes_to_check.pop_back();
544 to_check !=
"java::java.lang.Object")
550 class_hierarchy.
class_map.at(to_check).parents;
551 classes_to_check.insert(
552 classes_to_check.end(), parents.begin(), parents.end());
579 if(instruction.
statement ==
"getstatic" ||
583 instruction.
args.size() > 0,
584 "get/putstatic should have at least one argument");
587 !
component.empty(),
"get/putstatic should specify a component");
588 irep_idt class_id = instruction.
args[0].get_string(ID_class);
590 !class_id.empty(),
"get/putstatic should specify a class");
601 if(!referred_component.is_valid())
608 class_id, symbol_table, class_hierarchy);
620 bool no_incomplete_ancestors = add_to_class_id.
empty();
621 if(no_incomplete_ancestors)
623 add_to_class_id = class_id;
628 <<
"non-stub type " << class_id <<
". In future this "
639 instruction.
args[0].type(),
641 no_incomplete_ancestors);
662 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
684 if(class_trees.second.front().parsed_class.name.empty())
709 if(c.second.front().parsed_class.name.empty())
714 c.second.front().parsed_class.name, symbol_table);
719 <<
"Not marking class " << c.first
720 <<
" implicitly generic due to missing outer class symbols"
738 const std::size_t before_constant_globals_size = symbol_table.
symbols.size();
747 status() <<
"Java: added "
748 << (symbol_table.
symbols.size() - before_constant_globals_size)
749 <<
" String or Class constant symbols"
804 function_id_and_type.first, journalling_symbol_table);
812 for(
const auto &fn_name : journalling_symbol_table.
get_inserted())
863 symbol_table_builder,
894 [
this, &symbol_table_builder](
898 function_id, symbol_table_builder, std::move(lazy_methods_needed));
928 std::unordered_set<irep_idt> &methods)
const
930 const std::string cprover_class_prefix =
"java::org.cprover.CProver.";
937 const std::string &method_id =
id2string(kv.first);
942 if(
has_prefix(method_id, cprover_class_prefix))
944 std::size_t method_name_end_offset =
945 method_id.find(
':', cprover_class_prefix.length());
947 method_name_end_offset != std::string::npos,
948 "org.cprover.CProver method should have a postfix type descriptor");
950 const std::string method_name =
952 cprover_class_prefix.length(),
953 method_name_end_offset - cprover_class_prefix.length());
958 methods.insert(kv.first);
962 methods.insert(kv.first);
1008 const codet &function_body,
1011 if(needed_lazy_methods)
1017 if(it->id() == ID_code)
1019 const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1027 expr_dynamic_cast<symbol_exprt>(fn_call->function());
1057 synthetic_methods_mapt::iterator synthetic_method_it;
1067 symbol, cmb->get().method.local_variable_table, symbol_table);
1070 const codet generated_code =
1075 symbol.
value = std::move(generated_code);
1085 switch(synthetic_method_it->second)
1123 symbol_table.
lookup_ref(cmb->get().class_id),
1129 std::move(needed_lazy_methods),
1141 type_try_dynamic_cast<pointer_typet>(function_type.
return_type()))
1153 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1169 parse_trees.front().output(out);
1170 if(parse_trees.size() > 1)
1172 out <<
"\n\nClass has the following overlays:\n\n";
1173 for(
auto parse_tree_it = std::next(parse_trees.begin());
1174 parse_tree_it != parse_trees.end();
1177 parse_tree_it->output(out);
1179 out <<
"End of class overlays.\n";
1185 return util_make_unique<java_bytecode_languaget>();
1207 const std::string &code,
1208 const std::string &module,
1217 std::istringstream i_preprocessed(code);
1221 java_bytecode_parser.clear();
1222 java_bytecode_parser.filename=
"";
1223 java_bytecode_parser.in=&i_preprocessed;
1225 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1226 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1227 java_bytecode_scanner_init();
1229 bool result=java_bytecode_parser.parse();
1231 if(java_bytecode_parser.parse_tree.items.empty())
1235 expr=java_bytecode_parser.parse_tree.items.front().value();
1245 java_bytecode_parser.clear();
1266 std::vector<load_extra_methodst>
Class that provides messages with a built-in verbosity 'level'.
jar_poolt jar_pool
a cache for jar_filet, by path name
const componentst & components() const
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
method_bytecodet method_bytecode
#define JAVA_CLASS_MODEL_SUFFIX
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
std::set< std::string > extensions() const override
#define PRECONDITION(CONDITION)
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
const_depth_iteratort depth_cbegin() const
void create_static_initializer_wrappers(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Create static initializer wrappers for all classes that need them.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
struct configt::javat java
code_ifthenelset get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Produces the static initializer wrapper body for the given function.
Non-graph-based representation of the class hierarchy.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
virtual bool isset(char option) const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
The type of an expression, extends irept.
const std::string get_option(const std::string &option) const
bool language_options_initialized
mstreamt & status() const
std::vector< load_extra_methodst > extra_methods
main_function_resultt get_main_symbol(const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler)
Figures out the entry point of the code to verify.
typet type
Type of symbol.
bool do_ci_lazy_method_conversion(symbol_tablet &, method_bytecodet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
std::vector< irep_idt > load_entire_jar(const std::string &jar_path)
Load all class files from a .jar file.
std::unique_ptr< languaget > new_java_bytecode_language()
opt_reft get(const irep_idt &method_id)
static void notify_static_method_calls(const codet &function_body, optionalt< ci_lazy_methods_neededt > needed_lazy_methods)
Notify ci_lazy_methods, if present, of any static function calls made by the given function body.
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Base class for all expressions.
bool implements_function(const irep_idt &function_id) const
static void infer_opaque_type_fields(const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table)
Infer fields that must exist on opaque types from field accesses against them.
irep_idt base_name
Base (non-scoped) name.
A struct tag type, i.e., struct_typet with an identifier.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
void initialize_known_type_table()
void set_option(const std::string &option, const bool value)
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
Expression to hold a symbol (variable)
bool has_suffix(const std::string &s, const std::string &suffix)
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
bool parse(std::istream &instream, const std::string &path) override
We set the main class (i.e. class to start the class loading analysis from, see java_class_loadert) d...
#define UNREACHABLE
This should be used to mark dead code.
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)
Gets the base classes for known String and String-related types, or returns an empty list for other t...
bool throw_runtime_exceptions
stub_global_initializer_factoryt stub_global_initializer_factory
irep_idt pretty_name
Language-specific display name.
const codet & to_code(const exprt &expr)
static irep_idt get_any_incomplete_ancestor_for_stub_static_field(const irep_idt &start_class_id, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy)
Find any incomplete ancestor of a given class that can have a stub static field attached to it.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)
static void create_stub_global_symbol(symbol_table_baset &symbol_table, const irep_idt &symbol_id, const irep_idt &symbol_basename, const typet &symbol_type, const irep_idt &class_id, bool force_nondet_init)
Add a stub global symbol to the symbol table, initialising pointer-typed symbols with null and primit...
typet & type()
Return the type of the expression.
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
virtual std::vector< load_extra_methodst > build_extra_entry_points(const optionst &) const
This method should be overloaded to provide alternative approaches for specifying extra entry points.
irep_idt mode
Language mode.
mstreamt & result() const
bool string_refinement_enabled
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
std::vector< irep_idt > main_jar_classes
void set_java_cp_include_files(const std::string &java_cp_include_files)
Set the argument of the class loader limit java_class_loader_limitt.
The null pointer constant.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const std::string & id2string(const irep_idt &d)
virtual ~java_bytecode_languaget()
static exprt get_ldc_result(const exprt &ldc_arg0, symbol_tablet &symbol_table, bool string_refinement_enabled)
Get result of a Java load-constant (ldc) instruction.
java_class_loadert java_class_loader
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
void mark_java_implicitly_generic_class_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
const irep_idt & get_identifier() const
The symbol table base class interface.
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
void show_parse(std::ostream &out) override
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
lazy_methods_modet lazy_methods_mode
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::string get_value(char option) const
virtual void set_message_handler(message_handlert &_message_handler)
bool assert_uncaught_exceptions
const basest & bases() const
Get the collection of base classes/structs.
static void create_stub_global_symbols(const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, messaget &log)
Search for getstatic and putstatic instructions in a class' bytecode and create stub symbols for any ...
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
void add_classpath_entry(const std::string &)
Appends an entry to the class path, used for loading classes.
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
bool has_component(const irep_idt &component_name) const
const irep_idt & id() const
bool throw_assertion_error
std::vector< irep_idt > idst
void modules_provided(std::set< std::string > &modules) override
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
java_string_library_preprocesst string_preprocess
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
nonstd::optional< T > optionalt
void set_extra_class_refs_function(get_extra_class_refs_functiont func)
Sets a function that provides extra dependencies for a particular class.
unsigned int get_unsigned_int_option(const std::string &option) const
std::function< std::vector< irep_idt >const symbol_tablet &symbol_table)> build_load_method_by_regex(const std::string &pattern)
Create a lambda that returns the symbols that the given pattern should be loaded.If the pattern doesn...
void set(const optionst &)
Assigns the parameters from given options.
void java_bytecode_instrument(symbol_tablet &symbol_table, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions.
Class representing a filter for class file loading.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
bool assume_inputs_non_null
exprt value
Initial value of symbol.
message_handlert & get_message_handler()
const select_pointer_typet & get_pointer_type_selector() const
class_hierarchyt class_hierarchy
void java_internal_additions(symbol_table_baset &dest)
A generated (synthetic) static initializer function for a stub type.
bool java_entry_point(symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
message_handlert * message_handler
bool typecheck(symbol_tablet &context, const std::string &module) override
code_blockt get_stub_initializer_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
std::string java_cp_include_files
void add_load_classes(const std::vector< irep_idt > &classes)
Adds the list of classes to the load queue, forcing them to be loaded even without explicit reference...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void create_stub_global_initializer_symbols(symbol_tablet &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, synthetic_methods_mapt &synthetic_methods)
Create static initializer symbols for each distinct class that has stub globals.
const irep_idt & get(const irep_namet &name) const
const_depth_iteratort depth_cend() const
code_blockt get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Thread safe version of the static initializer.
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
std::vector< irep_idt > java_load_classes
const std::vector< std::string > exception_needed_classes
void set(const irep_namet &name, const irep_idt &value)
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
std::string id() const override
static symbol_exprt get_or_create_class_literal_symbol(const irep_idt &class_id, symbol_tablet &symbol_table)
Create if necessary, then return the constant global java.lang.Class symbol for a given class id.
bool get_bool_option(const std::string &option) const
static void generate_constant_global_variables(java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, bool string_refinement_enabled)
Creates global variables for constants mentioned in a given method.
size_t max_user_array_length
std::string type2java(const typet &type, const namespacet &ns)
java_object_factory_parameterst object_factory_parameters
std::string expr2java(const exprt &expr, const namespacet &ns)
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
bool has_prefix(const std::string &s, const std::string &prefix)
void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
symbol_exprt get_or_create_string_literal_symbol(const exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
const java_class_typet & to_java_class_type(const typet &type)
const changesett & get_inserted() const
void clear_classpath()
Clear all classpath entries.
Operator to return the address of an object.
const java_method_typet & to_java_method_type(const typet &type)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
mstreamt & warning() const
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
const std::list< std::string > & get_values(const std::string &option) const
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
A symbol table wrapper that records which entries have been updated/removed.
const value_listt & get_list_option(const std::string &option) const
irep_idt name
The unique identifier.
bool java_bytecode_convert_class(const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &string_preprocess, const std::unordered_set< std::string > &no_load_classes)
See class java_bytecode_convert_classt.
void java_bytecode_initialize_parameter_names(symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize sym...
Data structure for representing an arbitrary statement in a program.
std::unordered_set< std::string > no_load_classes