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
std::vector< irep_idt > java_load_classes
The type of an expression, extends irept.
Definition: type.h:27
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
Symbol table entry.
Definition: symbol.h:27
java_string_library_preprocesst string_preprocess
void show_parse(std::ostream &out) override
java_object_factory_parameterst object_factory_parameters
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...
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...
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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:35
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 ('ci') analysis to determine which methods may be reachable from th...
Base class for all expressions.
Definition: expr.h:54
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...
The symbol table base class interface.
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.
Class responsible to load .class files.
Synthetic methods are particular methods internally generated by the Java frontend,...
Context-insensitive lazy methods container.
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
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
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
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.