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  "(java-throw-runtime-exceptions)" /* will go away */ \
35  "(throw-runtime-exceptions)" \
36  "(java-max-input-array-length):" /* will go away */ \
37  "(max-nondet-array-length):" \
38  "(java-max-input-tree-depth):" /* will go away */ \
39  "(max-nondet-tree-depth):" \
40  "(java-max-vla-length):" \
41  "(java-cp-include-files):" \
42  "(lazy-methods)" /* will go away */ \
43  "(no-lazy-methods)" \
44  "(lazy-methods-extra-entry-point):" \
45  "(java-load-class):" \
46  "(java-no-load-class):"
47 
48 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
49  " --disable-uncaught-exception-check\n" \
50  " ignore uncaught exceptions and errors\n" \
51  " --throw-assertion-error throw java.lang.AssertionError on violated\n" \
52  " assert statements instead of failing\n" \
53  " at the location of the assert statement\n" \
54  " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \
55  " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \
56  " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
57  " at level N references are set to null\n" /* NOLINT(*) */ \
58  " --java-assume-inputs-non-null\n" \
59  " never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
60  " entry point with null\n" /* NOLINT(*) */ \
61  " --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
62  " --java-cp-include-files r regexp or JSON list of files to load\n" \
63  " (with '@' prefix)\n" \
64  " --no-lazy-methods load and translate all methods given on\n" \
65  " the command line and in --classpath\n" \
66  " Default is to load methods that appear to be\n" /* NOLINT(*) */ \
67  " reachable from the --function entry point\n" \
68  " or main class\n" \
69  " Note that --show-symbol-table, --show-goto-functions\n" /* NOLINT(*) */ \
70  " and --show-properties output are restricted to\n" /* NOLINT(*) */ \
71  " loaded methods by default.\n" \
72  " --lazy-methods-extra-entry-point METHODNAME\n" \
73  " treat METHODNAME as a possible program entry\n" /* NOLINT(*) */ \
74  " point for the purpose of lazy method loading\n" /* NOLINT(*) */ \
75  " METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \
76  " against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \
77  " will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \
78  " overloads of a method will also be added.\n"
79 // clang-format on
80 
81 class symbolt;
82 
84 {
88 };
89 
90 #define JAVA_CLASS_MODEL_SUFFIX "@class_model"
91 
93 {
94 public:
95  virtual void get_language_options(const cmdlinet &) override;
96 
97  virtual bool preprocess(
98  std::istream &instream,
99  const std::string &path,
100  std::ostream &outstream) override;
101 
102  bool parse(
103  std::istream &instream,
104  const std::string &path) override;
105 
107  symbol_tablet &symbol_table) override;
108 
109  bool typecheck(
110  symbol_tablet &context,
111  const std::string &module) override;
112 
113  virtual bool final(symbol_table_baset &context) override;
114 
115  void show_parse(std::ostream &out) override;
116 
117  virtual ~java_bytecode_languaget();
119  std::unique_ptr<select_pointer_typet> pointer_type_selector):
120  assume_inputs_non_null(false),
126  {}
127 
130  std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
131  {}
132 
133 
134  bool from_expr(
135  const exprt &expr,
136  std::string &code,
137  const namespacet &ns) override;
138 
139  bool from_type(
140  const typet &type,
141  std::string &code,
142  const namespacet &ns) override;
143 
144  bool to_expr(
145  const std::string &code,
146  const std::string &module,
147  exprt &expr,
148  const namespacet &ns) override;
149 
150  std::unique_ptr<languaget> new_language() override
151  { return util_make_unique<java_bytecode_languaget>(); }
152 
153  std::string id() const override { return "java"; }
154  std::string description() const override { return "Java Bytecode"; }
155  std::set<std::string> extensions() const override;
156 
157  void modules_provided(std::set<std::string> &modules) override;
158  virtual void
159  methods_provided(std::unordered_set<irep_idt> &methods) const override;
160  virtual void convert_lazy_method(
161  const irep_idt &function_id,
162  symbol_table_baset &symbol_table) override;
163 
164 protected:
166  const irep_idt &function_id,
167  symbol_table_baset &symbol_table)
168  {
170  function_id, symbol_table, optionalt<ci_lazy_methods_neededt>());
171  }
173  const irep_idt &function_id,
174  symbol_table_baset &symbol_table,
175  optionalt<ci_lazy_methods_neededt> needed_lazy_methods);
176 
179 
181  std::vector<irep_idt> main_jar_classes;
184  bool assume_inputs_non_null; // assume inputs variables to be non-null
186  size_t max_user_array_length; // max size for user code created arrays
195 
196  // list of classes to force load even without reference from the entry point
197  std::vector<irep_idt> java_load_classes;
198 
199 private:
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 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
std::vector< irep_idt > java_load_classes
The type of an expression.
Definition: type.h:22
std::unique_ptr< languaget > new_language() override
Non-graph-based representation of the class hierarchy.
java_class_loadert java_class_loader
void modules_provided(std::set< std::string > &modules) override
std::unique_ptr< languaget > new_java_bytecode_language()
const select_pointer_typet & get_pointer_type_selector() const
STL namespace.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
java_string_library_preprocesst string_preprocess
void show_parse(std::ostream &out) override
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&#39;t been converted) into a...
object_factory_parameterst object_factory_parameters
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::set< std::string > extensions() const override
lazy_methods_modet
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...
virtual void get_language_options(const cmdlinet &) override
Consume options that are java bytecode specific.
bool typecheck(symbol_tablet &context, const std::string &module) override
nonstd::optional< T > optionalt
Definition: optional.h:35
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
The symbol table.
Definition: symbol_table.h:19
Collect methods needed to be loaded using the lazy method.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::vector< load_extra_methodst > extra_methods
Abstract interface to support a programming language.
std::string id() const override
java_bytecode_languaget(std::unique_ptr< 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...
std::string description() const override
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
std::unordered_set< std::string > no_load_classes
bool do_ci_lazy_method_conversion(symbol_tablet &, method_bytecodet &)
Uses a simple context-insensitive (&#39;ci&#39;) analysis to determine which methods may be reachable from th...
Base class for all expressions.
Definition: expr.h:42
bool parse(std::istream &instream, const std::string &path) override
The symbol table base class interface.
Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types.
Context-insensitive lazy methods container.
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
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...
stub_global_initializer_factoryt stub_global_initializer_factory
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
std::vector< irep_idt > main_jar_classes
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Produce code for simple implementation of String Java libraries.