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 "assignments_from_json.h"
14 #include "ci_lazy_methods.h"
15 #include "ci_lazy_methods_needed.h"
16 #include "code_with_references.h"
17 #include "java_class_loader.h"
21 #include "select_pointer_type.h"
22 #include "synthetic_methods_map.h"
23 
24 #include <memory>
25 
26 #include <util/cmdline.h>
27 #include <util/make_unique.h>
28 #include <util/prefix_filter.h>
29 
30 #include <langapi/language.h>
31 
32 // clang-format off
33 #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
34  "(disable-uncaught-exception-check)" \
35  "(throw-assertion-error)" \
36  "(assert-no-exceptions-thrown)" \
37  "(java-assume-inputs-non-null)" \
38  "(java-assume-inputs-interval):" \
39  "(java-assume-inputs-integral)" \
40  "(throw-runtime-exceptions)" \
41  "(max-nondet-array-length):" \
42  "(max-nondet-tree-depth):" \
43  "(java-max-vla-length):" \
44  "(java-cp-include-files):" \
45  "(ignore-manifest-main-class)" \
46  "(context-include):" \
47  "(context-exclude):" \
48  "(no-lazy-methods)" \
49  "(lazy-methods-extra-entry-point):" \
50  "(java-load-class):" \
51  "(java-no-load-class):" \
52  "(static-values):" \
53  "(java-lift-clinit-calls)"
54 
55 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
56  " --disable-uncaught-exception-check\n" \
57  " ignore uncaught exceptions and errors\n" \
58  " --throw-assertion-error throw java.lang.AssertionError on violated\n" \
59  " assert statements instead of failing\n" \
60  " at the location of the assert statement\n" \
61  " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \
62  " --assert-no-exceptions-thrown\n"\
63  " transform `throw` instructions into `assert FALSE`\n"/* NOLINT(*) */ \
64  " followed by `assume FALSE`.\n" \
65  " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \
66  " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
67  " at level N references are set to null\n" /* NOLINT(*) */ \
68  " --java-assume-inputs-non-null\n" \
69  " never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
70  " entry point with null\n" /* NOLINT(*) */ \
71  " --java-assume-inputs-interval [L:U] or [L:] or [:U]\n" \
72  " force numerical primitive-typed inputs\n" /* NOLINT(*) */ \
73  " (byte, short, int, long, float, double) to be\n" /* NOLINT(*) */ \
74  " initialized within the given range; lower bound\n" /* NOLINT(*) */ \
75  " L and upper bound U must be integers;\n" /* NOLINT(*) */ \
76  " does not work for arrays;\n" /* NOLINT(*) */ \
77  " --java-assume-inputs-integral\n" \
78  " force float and double inputs to have integer values;\n" /* NOLINT(*) */ \
79  " does not work for arrays;\n" /* NOLINT(*) */ \
80  " --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
81  " --java-cp-include-files r regexp or JSON list of files to load\n" \
82  " (with '@' prefix)\n" \
83  " --ignore-manifest-main-class ignore Main-Class entries in JAR manifest files.\n" /* NOLINT(*) */ \
84  " If this option is specified and the options\n" /* NOLINT(*) */ \
85  " --function and --main-class are not, we can be\n" /* NOLINT(*) */ \
86  " certain that all classes in the JAR file are\n" /* NOLINT(*) */ \
87  " loaded.\n" \
88  " --context-include i only analyze code matching specification i that\n" /* NOLINT(*) */ \
89  " --context-exclude e does not match specification e.\n" \
90  " All other methods are excluded, i.e. we load their\n" /* NOLINT(*) */ \
91  " signatures and meta-information, but not their\n" /* NOLINT(*) */ \
92  " bodies.\n" \
93  " A specification is any prefix of a package, class\n" /* NOLINT(*) */ \
94  " or method name, e.g. \"org.cprover.\" or\n" /* NOLINT(*) */ \
95  " \"org.cprover.MyClass.\" or\n" \
96  " \"org.cprover.MyClass.methodToStub:(I)Z\".\n" \
97  " These options can be given multiple times.\n" \
98  " The default for context-include is 'all\n" \
99  " included'; default for context-exclude is\n" \
100  " 'nothing excluded'.\n" \
101  " --no-lazy-methods load and translate all methods given on\n" \
102  " the command line and in --classpath\n" \
103  " Default is to load methods that appear to be\n" /* NOLINT(*) */ \
104  " reachable from the --function entry point\n" \
105  " or main class\n" \
106  " Note that --show-symbol-table, --show-goto-functions\n" /* NOLINT(*) */ \
107  " and --show-properties output are restricted to\n" /* NOLINT(*) */ \
108  " loaded methods by default.\n" \
109  " --lazy-methods-extra-entry-point METHODNAME\n" \
110  " treat METHODNAME as a possible program entry\n" /* NOLINT(*) */ \
111  " point for the purpose of lazy method loading\n" /* NOLINT(*) */ \
112  " METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \
113  " against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \
114  " will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \
115  " overloads of a method will also be added.\n" \
116  " --static-values f Load initial values of static fields from the given\n"/* NOLINT(*) */ \
117  " JSON file. We assign static fields to these values\n"/* NOLINT(*) */ \
118  " instead of calling the normal static initializer\n"/* NOLINT(*) */ \
119  " (clinit) method.\n" \
120  " The argument can be a relative or absolute path to\n"/* NOLINT(*) */ \
121  " the file.\n" \
122  " --java-lift-clinit-calls Lifts clinit calls in function bodies to the top of the\n" /* NOLINT(*) */ \
123  " function. This may reduce the overall cost of static\n" /* NOLINT(*) */ \
124  " initialisation, but may be unsound if there are\n" /* NOLINT(*) */ \
125  " cyclic dependencies between static initializers due\n" /* NOLINT(*) */ \
126  " to potentially changing their order of execution,\n" /* NOLINT(*) */ \
127  " or if static initializers have side-effects such as\n" /* NOLINT(*) */ \
128  " updating another class' static field.\n" /* NOLINT(*) */
129 
130 #ifdef _WIN32
131  #define JAVA_CLASSPATH_SEPARATOR ";"
132 #else
133  #define JAVA_CLASSPATH_SEPARATOR ":"
134 #endif
135 
136 #define HELP_JAVA_CLASSPATH /* NOLINT(*) */ \
137  " -classpath dirs/jars\n" \
138  " -cp dirs/jars\n" \
139  " --classpath dirs/jars set class search path of directories and\n" \
140  " jar files\n" \
141  " A " JAVA_CLASSPATH_SEPARATOR \
142  " separated list of directories and JAR\n" \
143  " archives to search for class files.\n" \
144  " --main-class class-name set the name of the main class\n"
145 
146 #define HELP_JAVA_METHOD_NAME /* NOLINT(*) */ \
147  " method-name fully qualified name of method\n" \
148  " used as entry point, e.g.\n" \
149  " mypackage.Myclass.foo:(I)Z\n"
150 
151 #define HELP_JAVA_CLASS_NAME /* NOLINT(*) */ \
152  " class-name name of class\n" \
153  " The entry point is the method specified by\n" \
154  " --function, or otherwise, the\n" \
155  " public static void main(String[])\n" \
156  " method of the given class.\n"
157 
158 #define OPT_JAVA_JAR /* NOLINT(*) */ \
159  "(jar):"
160 
161 #define HELP_JAVA_JAR /* NOLINT(*) */ \
162  " -jar jarfile JAR file to be checked\n" \
163  " The entry point is the method specified by\n" \
164  " --function or otherwise, the\n" \
165  " public static void main(String[]) method\n" \
166  " of the class specified by --main-class or the main\n" /* NOLINT(*) */ \
167  " class specified in the JAR manifest\n" \
168  " (checked in this order).\n"
169 
170 #define OPT_JAVA_GOTO_BINARY /* NOLINT(*) */ \
171  "(gb):"
172 
173 #define HELP_JAVA_GOTO_BINARY /* NOLINT(*) */ \
174  " --gb goto-binary goto-binary file to be checked\n" \
175  " The entry point is the method specified by\n" \
176  " --function, or otherwise, the\n" \
177  " public static void main(String[])\n" \
178  " of the class specified by --main-class\n" \
179  " (checked in this order).\n"
180 // clang-format on
181 
182 class symbolt;
183 
185 {
189 };
190 
202 {
203 public:
205 
206  std::unordered_multimap<irep_idt, symbolt> &
207  get(const symbol_tablet &symbol_table);
208 
209  void reinitialize();
210 
211 private:
212  bool initialized = false;
213  std::unordered_multimap<irep_idt, symbolt> map;
214 };
215 
217 {
218  java_bytecode_language_optionst(const optionst &options, messaget &log);
219 
221 
227  bool throw_assertion_error = false;
228  bool threading_support = false;
229  bool nondet_static = false;
231 
235 
240 
242  std::vector<irep_idt> java_load_classes;
248 
250  std::unordered_set<std::string> no_load_classes;
251 
252  std::vector<load_extra_methodst> extra_methods;
253 
262 
267 
270 };
271 
272 #define JAVA_CLASS_MODEL_SUFFIX "@class_model"
273 
275 {
276 public:
277  void set_language_options(const optionst &) override;
278 
280 
281  virtual bool preprocess(
282  std::istream &instream,
283  const std::string &path,
284  std::ostream &outstream) override;
285 
286  // This is an extension to languaget
287  // required because parsing of Java programs can be initiated without
288  // opening a file first or providing a path to a file
289  // as dictated by \ref languaget.
290  virtual bool parse();
291 
292  bool parse(
293  std::istream &instream,
294  const std::string &path) override;
295 
297  symbol_tablet &symbol_table) override;
298 
299  bool typecheck(
300  symbol_tablet &context,
301  const std::string &module) override;
302 
303  virtual bool final(symbol_table_baset &context) override;
304 
305  void show_parse(std::ostream &out) override;
306 
307  virtual ~java_bytecode_languaget();
309  std::unique_ptr<select_pointer_typet> pointer_type_selector)
312  {
313  }
314 
317  std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
318  {
319  }
320 
321  bool from_expr(
322  const exprt &expr,
323  std::string &code,
324  const namespacet &ns) override;
325 
326  bool from_type(
327  const typet &type,
328  std::string &code,
329  const namespacet &ns) override;
330 
331  bool to_expr(
332  const std::string &code,
333  const std::string &module,
334  exprt &expr,
335  const namespacet &ns) override;
336 
337  std::unique_ptr<languaget> new_language() override
338  { return util_make_unique<java_bytecode_languaget>(); }
339 
340  std::string id() const override { return "java"; }
341  std::string description() const override { return "Java Bytecode"; }
342  std::set<std::string> extensions() const override;
343 
344  void modules_provided(std::set<std::string> &modules) override;
345  virtual void
346  methods_provided(std::unordered_set<irep_idt> &methods) const override;
347  virtual void convert_lazy_method(
348  const irep_idt &function_id,
349  symbol_table_baset &symbol_table) override;
350 
351 protected:
353  const irep_idt &function_id,
354  symbol_table_baset &symbol_table,
356  {
358  function_id,
359  symbol_table,
362  }
364  const irep_idt &function_id,
365  symbol_table_baset &symbol_table,
366  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
369  const irep_idt &function_id,
370  symbol_table_baset &symbol_table,
371  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
373 
376 
379  std::vector<irep_idt> main_jar_classes;
384 
385 private:
386  virtual std::vector<load_extra_methodst>
387  build_extra_entry_points(const optionst &) const;
388  const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
389 
396 
401  std::unordered_map<std::string, object_creation_referencet> references;
402 
403  void parse_from_main_class();
405 };
406 
407 std::unique_ptr<languaget> new_java_bytecode_language();
408 
409 void parse_java_language_options(const cmdlinet &cmd, optionst &options);
410 
411 prefix_filtert get_context(const optionst &options);
412 
413 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
Collect methods needed to be loaded using the lazy method.
Context-insensitive lazy methods container.
Non-graph-based representation of the class hierarchy.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
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...
void show_parse(std::ostream &out) override
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
std::vector< irep_idt > main_jar_classes
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
std::string id() const override
stub_global_initializer_factoryt stub_global_initializer_factory
std::set< std::string > extensions() const override
void set_message_handler(message_handlert &message_handler) override
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
std::unique_ptr< languaget > new_language() 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.
java_bytecode_languaget(std::unique_ptr< select_pointer_typet > pointer_type_selector)
std::string description() const override
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
bool do_ci_lazy_method_conversion(symbol_tablet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
java_object_factory_parameterst object_factory_parameters
optionalt< java_bytecode_language_optionst > language_options
java_string_library_preprocesst string_preprocess
void modules_provided(std::set< std::string > &modules) override
java_class_loadert java_class_loader
bool convert_single_method_code(const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typeche...
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.
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
const select_pointer_typet & get_pointer_type_selector() const
bool typecheck(symbol_tablet &context, const std::string &module) override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::unordered_map< std::string, object_creation_referencet > references
Map used in all calls to functions that deterministically create objects (currently only assign_from_...
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 convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
Class responsible to load .class files.
Map classes to the symbols they declare but is only computed once it is needed and the map is then ke...
std::unordered_multimap< irep_idt, symbolt > & get(const symbol_tablet &symbol_table)
std::unordered_multimap< irep_idt, symbolt > map
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
message_handlert * message_handler
Definition: message.h:439
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
Definition: prefix_filter.h:20
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
@ LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
prefix_filtert get_context(const optionst &options)
std::unique_ptr< languaget > new_java_bytecode_language()
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
Produce code for simple implementation of String Java libraries.
Abstract interface to support a programming language.
nonstd::optional< T > optionalt
Definition: optional.h:35
Prefix Filtering.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
bool assert_no_exceptions_thrown
Transform athrow bytecode instructions into assert FALSE followed by assume FALSE.
bool should_lift_clinit_calls
Should we lift clinit calls in function bodies to the top? For example, turning if(x) A....
optionalt< std::string > main_jar
If set then a JAR file has been given via the -jar option.
optionalt< prefix_filtert > method_context
If set, method bodies are only elaborated if they pass the filter.
optionalt< json_objectt > static_values_json
JSON which contains initial values of static fields (right after the static initializer of the class ...
bool assume_inputs_non_null
assume inputs variables to be non-null
size_t max_user_array_length
max size for user code created arrays
std::vector< irep_idt > java_load_classes
list of classes to force load even without reference from the entry point
std::unordered_set< std::string > no_load_classes
List of classes to never load.
std::vector< load_extra_methodst > extra_methods
Synthetic methods are particular methods internally generated by the Java frontend,...
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.