cprover
java_bytecode_language.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
12 
13 #include "ci_lazy_methods.h"
14 #include "ci_lazy_methods_needed.h"
15 #include "java_class_loader.h"
19 #include "select_pointer_type.h"
20 #include "synthetic_methods_map.h"
21 
22 #include <memory>
23 
24 #include <util/cmdline.h>
25 #include <util/make_unique.h>
26 
27 #include <langapi/language.h>
28 
29 // clang-format off
30 #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
31  "(disable-uncaught-exception-check)" \
32  "(throw-assertion-error)" \
33  "(java-assume-inputs-non-null)" \
34  "(throw-runtime-exceptions)" \
35  "(max-nondet-array-length):" \
36  "(max-nondet-tree-depth):" \
37  "(java-max-vla-length):" \
38  "(java-cp-include-files):" \
39  "(no-lazy-methods)" \
40  "(lazy-methods-extra-entry-point):" \
41  "(java-load-class):" \
42  "(java-no-load-class):"
43 
44 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
45  " --disable-uncaught-exception-check\n" \
46  " ignore uncaught exceptions and errors\n" \
47  " --throw-assertion-error throw java.lang.AssertionError on violated\n" \
48  " assert statements instead of failing\n" \
49  " at the location of the assert statement\n" \
50  " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \
51  " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \
52  " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
53  " at level N references are set to null\n" /* NOLINT(*) */ \
54  " --java-assume-inputs-non-null\n" \
55  " never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
56  " entry point with null\n" /* NOLINT(*) */ \
57  " --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
58  " --java-cp-include-files r regexp or JSON list of files to load\n" \
59  " (with '@' prefix)\n" \
60  " --no-lazy-methods load and translate all methods given on\n" \
61  " the command line and in --classpath\n" \
62  " Default is to load methods that appear to be\n" /* NOLINT(*) */ \
63  " reachable from the --function entry point\n" \
64  " or main class\n" \
65  " Note that --show-symbol-table, --show-goto-functions\n" /* NOLINT(*) */ \
66  " and --show-properties output are restricted to\n" /* NOLINT(*) */ \
67  " loaded methods by default.\n" \
68  " --lazy-methods-extra-entry-point METHODNAME\n" \
69  " treat METHODNAME as a possible program entry\n" /* NOLINT(*) */ \
70  " point for the purpose of lazy method loading\n" /* NOLINT(*) */ \
71  " METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \
72  " against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \
73  " will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \
74  " overloads of a method will also be added.\n"
75 // clang-format on
76 
77 class symbolt;
78 
80 {
84 };
85 
86 #define JAVA_CLASS_MODEL_SUFFIX "@class_model"
87 
89 {
90 public:
91  void set_language_options(const optionst &) override;
92 
93  virtual bool preprocess(
94  std::istream &instream,
95  const std::string &path,
96  std::ostream &outstream) override;
97 
98  bool parse(
99  std::istream &instream,
100  const std::string &path) override;
101 
103  symbol_tablet &symbol_table) override;
104 
105  bool typecheck(
106  symbol_tablet &context,
107  const std::string &module) override;
108 
109  virtual bool final(symbol_table_baset &context) override;
110 
111  void show_parse(std::ostream &out) override;
112 
113  virtual ~java_bytecode_languaget();
115  std::unique_ptr<select_pointer_typet> pointer_type_selector):
116  assume_inputs_non_null(false),
122  {
123  }
124 
127  std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
128  {
129  }
130 
131  bool from_expr(
132  const exprt &expr,
133  std::string &code,
134  const namespacet &ns) override;
135 
136  bool from_type(
137  const typet &type,
138  std::string &code,
139  const namespacet &ns) override;
140 
141  bool to_expr(
142  const std::string &code,
143  const std::string &module,
144  exprt &expr,
145  const namespacet &ns) override;
146 
147  std::unique_ptr<languaget> new_language() override
148  { return util_make_unique<java_bytecode_languaget>(); }
149 
150  std::string id() const override { return "java"; }
151  std::string description() const override { return "Java Bytecode"; }
152  std::set<std::string> extensions() const override;
153 
154  void modules_provided(std::set<std::string> &modules) override;
155  virtual void
156  methods_provided(std::unordered_set<irep_idt> &methods) const override;
157  virtual void convert_lazy_method(
158  const irep_idt &function_id,
159  symbol_table_baset &symbol_table) override;
160 
161 protected:
163  const irep_idt &function_id,
164  symbol_table_baset &symbol_table)
165  {
167  function_id, symbol_table, optionalt<ci_lazy_methods_neededt>());
168  }
170  const irep_idt &function_id,
171  symbol_table_baset &symbol_table,
172  optionalt<ci_lazy_methods_neededt> needed_lazy_methods);
173 
176 
178  std::vector<irep_idt> main_jar_classes;
181  bool assume_inputs_non_null; // assume inputs variables to be non-null
183  size_t max_user_array_length; // max size for user code created arrays
193 
194  // list of classes to force load even without reference from the entry point
195  std::vector<irep_idt> java_load_classes;
196 
197 private:
198  virtual std::vector<load_extra_methodst>
199  build_extra_entry_points(const optionst &) const;
200  const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
201 
208  // List of classes to never load
209  std::unordered_set<std::string> no_load_classes;
210 
211  std::vector<load_extra_methodst> extra_methods;
212 };
213 
214 std::unique_ptr<languaget> new_java_bytecode_language();
215 
216 void parse_java_language_options(const cmdlinet &cmd, optionst &options);
217 
218 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
java_static_initializers.h
method_bytecodet
Definition: ci_lazy_methods.h:33
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
java_bytecode_languaget::method_bytecode
method_bytecodet method_bytecode
Definition: java_bytecode_language.h:184
java_bytecode_languaget::extensions
std::set< std::string > extensions() const override
Definition: java_bytecode_language.cpp:182
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EAGER
Definition: java_bytecode_language.h:81
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:42
select_pointer_type.h
java_bytecode_languaget::pointer_type_selector
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
Definition: java_bytecode_language.h:200
optionst
Definition: options.h:22
java_bytecode_languaget::synthetic_methods
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
Definition: java_bytecode_language.h:205
java_bytecode_languaget::to_expr
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
Definition: java_bytecode_language.cpp:1206
typet
The type of an expression, extends irept.
Definition: type.h:27
java_bytecode_languaget::extra_methods
std::vector< load_extra_methodst > extra_methods
Definition: java_bytecode_language.h:211
java_bytecode_languaget::do_ci_lazy_method_conversion
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...
Definition: java_bytecode_language.cpp:886
java_bytecode_languaget::methods_provided
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...
Definition: java_bytecode_language.cpp:927
parse_java_language_options
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
Definition: java_bytecode_language.cpp:48
java_bytecode_languaget::main_class
irep_idt main_class
Definition: java_bytecode_language.h:177
java_bytecode_languaget::convert_single_method
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Definition: java_bytecode_language.h:162
exprt
Base class for all expressions.
Definition: expr.h:54
java_string_library_preprocess.h
java_object_factory_parameters.h
java_bytecode_languaget::from_type
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
Definition: java_bytecode_language.cpp:1197
java_bytecode_languaget::java_bytecode_languaget
java_bytecode_languaget()
Definition: java_bytecode_language.h:125
synthetic_methods_mapt
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Definition: synthetic_methods_map.h:38
stub_global_initializer_factoryt
Definition: java_static_initializers.h:44
java_bytecode_languaget::parse
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...
Definition: java_bytecode_language.cpp:211
java_bytecode_languaget::throw_runtime_exceptions
bool throw_runtime_exceptions
Definition: java_bytecode_language.h:187
java_bytecode_languaget::stub_global_initializer_factory
stub_global_initializer_factoryt stub_global_initializer_factory
Definition: java_bytecode_language.h:206
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
java_bytecode_languaget::set_language_options
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
Definition: java_bytecode_language.cpp:91
cmdlinet
Definition: cmdline.h:19
java_bytecode_languaget::build_extra_entry_points
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.
Definition: java_bytecode_language.cpp:1267
make_unique.h
java_bytecode_languaget::string_refinement_enabled
bool string_refinement_enabled
Definition: java_bytecode_language.h:186
java_bytecode_languaget::main_jar_classes
std::vector< irep_idt > main_jar_classes
Definition: java_bytecode_language.h:178
java_bytecode_languaget::~java_bytecode_languaget
virtual ~java_bytecode_languaget()
Definition: java_bytecode_language.cpp:1259
java_bytecode_languaget::java_class_loader
java_class_loadert java_class_loader
Definition: java_bytecode_language.h:179
java_bytecode_languaget::threading_support
bool threading_support
Definition: java_bytecode_language.h:180
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
ci_lazy_methods_needed.h
java_bytecode_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: java_bytecode_language.cpp:1165
java_class_loader.h
java_bytecode_languaget::lazy_methods_mode
lazy_methods_modet lazy_methods_mode
Definition: java_bytecode_language.h:185
java_bytecode_languaget::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
Definition: java_bytecode_language.cpp:844
java_bytecode_languaget::nondet_static
bool nondet_static
Definition: java_bytecode_language.h:192
java_bytecode_languaget::new_language
std::unique_ptr< languaget > new_language() override
Definition: java_bytecode_language.h:147
select_pointer_typet
Definition: select_pointer_type.h:28
language.h
java_bytecode_languaget::assert_uncaught_exceptions
bool assert_uncaught_exceptions
Definition: java_bytecode_language.h:188
java_bytecode_languaget::convert_lazy_method
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...
Definition: java_bytecode_language.cpp:973
java_bytecode_languaget::throw_assertion_error
bool throw_assertion_error
Definition: java_bytecode_language.h:189
java_bytecode_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: java_bytecode_language.cpp:187
java_bytecode_languaget::string_preprocess
java_string_library_preprocesst string_preprocess
Definition: java_bytecode_language.h:190
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
ci_lazy_methods.h
java_class_loadert
Class responsible to load .class files.
Definition: java_class_loader.h:26
java_bytecode_languaget::from_expr
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
Definition: java_bytecode_language.cpp:1188
java_bytecode_languaget::assume_inputs_non_null
bool assume_inputs_non_null
Definition: java_bytecode_language.h:181
java_bytecode_languaget::class_hierarchy
class_hierarchyt class_hierarchy
Definition: java_bytecode_language.h:207
java_bytecode_languaget::get_pointer_type_selector
const select_pointer_typet & get_pointer_type_selector() const
Definition: java_bytecode_language.cpp:916
java_bytecode_languaget::typecheck
bool typecheck(symbol_tablet &context, const std::string &module) override
Definition: java_bytecode_language.cpp:648
java_bytecode_languaget::java_cp_include_files
std::string java_cp_include_files
Definition: java_bytecode_language.h:191
lazy_methods_modet
lazy_methods_modet
Definition: java_bytecode_language.h:79
cmdline.h
java_bytecode_languaget::java_load_classes
std::vector< irep_idt > java_load_classes
Definition: java_bytecode_language.h:195
symbolt
Symbol table entry.
Definition: symbol.h:27
java_bytecode_languaget::id
std::string id() const override
Definition: java_bytecode_language.h:150
java_string_library_preprocesst
Definition: java_string_library_preprocess.h:35
java_bytecode_languaget::max_user_array_length
size_t max_user_array_length
Definition: java_bytecode_language.h:183
languaget
Definition: language.h:39
LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
Definition: java_bytecode_language.h:82
java_bytecode_languaget::object_factory_parameters
java_object_factory_parameterst object_factory_parameters
Definition: java_bytecode_language.h:182
java_bytecode_languaget::java_bytecode_languaget
java_bytecode_languaget(std::unique_ptr< select_pointer_typet > pointer_type_selector)
Definition: java_bytecode_language.h:114
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1183
java_bytecode_languaget
Definition: java_bytecode_language.h:88
LAZY_METHODS_MODE_EXTERNAL_DRIVER
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
Definition: java_bytecode_language.h:83
java_bytecode_languaget::preprocess
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Definition: java_bytecode_language.cpp:193
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:14
synthetic_methods_map.h
java_bytecode_languaget::no_load_classes
std::unordered_set< std::string > no_load_classes
Definition: java_bytecode_language.h:209
java_bytecode_languaget::description
std::string description() const override
Definition: java_bytecode_language.h:151