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)" \
35  "(java-max-input-array-length):" \
36  "(java-max-input-tree-depth):" \
37  "(java-max-vla-length):" \
38  "(java-cp-include-files):" \
39  "(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" \
46  " ignore uncaught exceptions and errors\n" \
47  " --throw-assertion-error throw java.lang.AssertionError on violated\n" /* NOLINT(*) */ \
48  " assert statements instead of failing\n" \
49  " at the location of the assert statement\n" /* NOLINT(*) */ \
50  " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
51  " entry point with null\n" /* NOLINT(*) */ \
52  " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \
53  " --java-max-input-array-length N limit input array size to <= N\n" /* NOLINT(*) */ \
54  " --java-max-input-tree-depth N object references are (deterministically) set to null in\n" /* NOLINT(*) */ \
55  " the object\n" /* NOLINT(*) */ \
56  " --java-max-vla-length limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
57  " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" /* NOLINT(*) */ \
58  " --lazy-methods only translate methods that appear to be reachable from\n" /* NOLINT(*) */ \
59  " the --function entry point or main class\n" /* NOLINT(*) */ \
60  " Note --show-symbol-table/goto-functions/properties output\n"/* NOLINT(*) */ \
61  " will be restricted to loaded methods in this case\n" /* NOLINT(*) */ \
62  " --lazy-methods-extra-entry-point METHODNAME\n" /* NOLINT(*) */ \
63  " treat METHODNAME as a possible program entry point for\n" /* NOLINT(*) */ \
64  " the purpose of lazy method loading\n" /* NOLINT(*) */ \
65  " A '.*' wildcard is allowed to specify all class members\n"
66 // clang-format on
67 
68 class symbolt;
69 
71 {
75 };
76 
77 #define JAVA_CLASS_MODEL_SUFFIX "@class_model"
78 
80 {
81 public:
82  virtual void get_language_options(const cmdlinet &) override;
83 
84  virtual bool preprocess(
85  std::istream &instream,
86  const std::string &path,
87  std::ostream &outstream) override;
88 
89  bool parse(
90  std::istream &instream,
91  const std::string &path) override;
92 
94  symbol_tablet &symbol_table) override;
95 
96  bool typecheck(
97  symbol_tablet &context,
98  const std::string &module) override;
99 
100  virtual bool final(symbol_table_baset &context) override;
101 
102  void show_parse(std::ostream &out) override;
103 
104  virtual ~java_bytecode_languaget();
106  std::unique_ptr<select_pointer_typet> pointer_type_selector):
107  assume_inputs_non_null(false),
113  {}
114 
117  std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
118  {}
119 
120 
121  bool from_expr(
122  const exprt &expr,
123  std::string &code,
124  const namespacet &ns) override;
125 
126  bool from_type(
127  const typet &type,
128  std::string &code,
129  const namespacet &ns) override;
130 
131  bool to_expr(
132  const std::string &code,
133  const std::string &module,
134  exprt &expr,
135  const namespacet &ns) override;
136 
137  std::unique_ptr<languaget> new_language() override
138  { return util_make_unique<java_bytecode_languaget>(); }
139 
140  std::string id() const override { return "java"; }
141  std::string description() const override { return "Java Bytecode"; }
142  std::set<std::string> extensions() const override;
143 
144  void modules_provided(std::set<std::string> &modules) override;
145  virtual void
146  methods_provided(std::unordered_set<irep_idt> &methods) const override;
147  virtual void convert_lazy_method(
148  const irep_idt &function_id,
149  symbol_table_baset &symbol_table) override;
150 
151 protected:
153  const irep_idt &function_id,
154  symbol_table_baset &symbol_table)
155  {
157  function_id, symbol_table, optionalt<ci_lazy_methods_neededt>());
158  }
160  const irep_idt &function_id,
161  symbol_table_baset &symbol_table,
162  optionalt<ci_lazy_methods_neededt> needed_lazy_methods);
163 
166 
168  std::vector<irep_idt> main_jar_classes;
171  bool assume_inputs_non_null; // assume inputs variables to be non-null
173  size_t max_user_array_length; // max size for user code created arrays
176  std::vector<irep_idt> lazy_methods_extra_entry_points;
183 
184  // list of classes to force load even without reference from the entry point
185  std::vector<irep_idt> java_load_classes;
186 
187 private:
188  const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
189 
196  // List of classes to never load
197  std::unordered_set<std::string> no_load_classes;
198 };
199 
200 std::unique_ptr<languaget> new_java_bytecode_language();
201 
202 #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
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
std::vector< irep_idt > lazy_methods_extra_entry_points
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
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
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.