cprover
load_java_class.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Unit test utilities
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include "load_java_class.h"
10 
11 #include <iostream>
12 #include <testing-utils/catch.hpp>
14 #include <testing-utils/message.h>
15 
16 #include <util/config.h>
17 #include <util/options.h>
18 #include <util/suffix.h>
19 
21 
23 #include <util/file_util.h>
24 
36  const std::string &java_class_name,
37  const std::string &class_path,
38  const std::string &main)
39 {
40  std::unique_ptr<languaget> lang = new_java_bytecode_language();
41 
42  return load_java_class(java_class_name, class_path, main, std::move(lang));
43 }
44 
48  const std::string &java_class_name,
49  const std::string &class_path,
50  const std::string &main)
51 {
52  return load_goto_model_from_java_class(java_class_name, class_path, main)
54 }
55 
58  const std::string &java_class_name,
59  const std::string &class_path,
60  const std::string &main,
61  std::unique_ptr<languaget> &&java_lang,
62  const cmdlinet &command_line)
63 {
65  java_class_name,
66  class_path,
67  main,
68  std::move(java_lang),
69  command_line)
71 }
72 
88  const std::string &java_class_name,
89  const std::string &class_path,
90  const std::string &main,
91  std::unique_ptr<languaget> &&java_lang,
92  const cmdlinet &command_line)
93 {
94  // We expect the name of the class without the .class suffix to allow us to
95  // check it
96  PRECONDITION(!has_suffix(java_class_name, ".class"));
97  std::string filename=java_class_name + ".class";
98 
99  // Construct a lazy_goto_modelt
100  lazy_goto_modelt lazy_goto_model(
101  [](goto_model_functiont &, const abstract_goto_modelt &) {},
102  [](goto_modelt &) { return false; },
103  [](const irep_idt &) { return false; },
104  [](const irep_idt &, symbol_table_baset &, goto_functiont &, bool) {
105  return false;
106  },
108 
109  // Configure the path loading
110  config.java.classpath.clear();
111  config.java.classpath.push_back(class_path);
112  config.main = main;
113 
114  // Add the language to the model
115  language_filet &lf=lazy_goto_model.add_language_file(filename);
116  lf.language=std::move(java_lang);
117  languaget &language=*lf.language;
118 
119  std::istringstream java_code_stream("ignored");
120 
121  optionst options;
122  parse_java_language_options(command_line, options);
123 
124  // Configure the language, load the class files
126  language.set_language_options(options);
127  language.parse(java_code_stream, filename);
128  language.typecheck(lazy_goto_model.symbol_table, "");
129  language.generate_support_functions(lazy_goto_model.symbol_table);
130  language.final(lazy_goto_model.symbol_table);
131 
132  lazy_goto_model.load_all_functions();
133 
134  std::unique_ptr<goto_modelt> maybe_goto_model=
136  std::move(lazy_goto_model));
137  INVARIANT(maybe_goto_model, "Freezing lazy_goto_model failed");
138 
139  // Verify that the class was loaded
140  const std::string class_symbol_name="java::"+java_class_name;
141  REQUIRE(maybe_goto_model->symbol_table.has_symbol(class_symbol_name));
142  const symbolt &class_symbol=
143  *maybe_goto_model->symbol_table.lookup(class_symbol_name);
144  REQUIRE(class_symbol.is_type);
145  const typet &class_type=class_symbol.type;
146  REQUIRE(class_type.id()==ID_struct);
147 
148  // Log the working directory to help people identify the common error
149  // of wrong working directory (should be the `unit` directory when running
150  // the unit tests).
151  std::string path = get_current_working_directory();
152  INFO("Working directory: " << path);
153 
154  // if this fails it indicates the class was not loaded
155  // Check your working directory and the class path is correctly configured
156  // as this often indicates that one of these is wrong.
157  REQUIRE_FALSE(to_java_class_type(class_type).get_is_stub());
158  return std::move(*maybe_goto_model);
159 }
160 
165  const std::string &java_class_name,
166  const std::string &class_path,
167  const std::string &main,
168  std::unique_ptr<languaget> &&java_lang)
169 {
170  free_form_cmdlinet command_line;
171  command_line.add_flag("no-lazy-methods");
172  command_line.add_flag("no-refine-strings");
173  // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an
174  // TODO(tkiley): unknown argument. This could be changed by using the
175  // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail.
176  // TODO(tkiley): TG-2708 to investigate and fix
177  command_line.set("java-cp-include-files", class_path);
178  return load_java_class(
179  java_class_name, class_path, main, std::move(java_lang), command_line);
180 }
181 
186  const std::string &java_class_name,
187  const std::string &class_path,
188  const std::string &main)
189 {
190  free_form_cmdlinet command_line;
191  command_line.add_flag("no-lazy-methods");
192  command_line.add_flag("no-refine-strings");
193 
194  std::unique_ptr<languaget> lang = new_java_bytecode_language();
195 
197  java_class_name, class_path, main, std::move(lang), command_line);
198 }
symbol_tablet load_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main)
Returns the symbol table from load_goto_model_from_java_class(const std::string &java_class_name,...
The type of an expression, extends irept.
Definition: type.h:27
Abstract interface to eager or lazy GOTO models.
null_message_handlert null_message_handler
Definition: message.cpp:14
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
A GOTO model that produces function bodies on demand.
configt config
Definition: config.cpp:24
std::string get_current_working_directory()
Definition: file_util.cpp:48
goto_modelt load_goto_model_from_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main, std::unique_ptr< languaget > &&java_lang, const cmdlinet &command_line)
Go through the process of loading, type-checking and finalising a specific class file to build a goto...
std::unique_ptr< languaget > language
Definition: language_file.h:46
const irep_idt & id() const
Definition: irep.h:259
classpatht classpath
Definition: config.h:156
virtual bool final(symbol_table_baset &symbol_table)
Final adjustments, e.g.
Definition: language.cpp:21
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
std::string main
Definition: config.h:172
The symbol table.
Definition: symbol_table.h:19
virtual void set(const std::string &option)
Definition: cmdline.cpp:60
static std::unique_ptr< goto_modelt > process_whole_model_and_freeze(lazy_goto_modelt &&model)
The model returned here has access to the functions we've already loaded but is frozen in the sense t...
void add_flag(std::string flag)
Equivalent to specifying –flag for the command line.
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
std::unique_ptr< languaget > new_java_bytecode_language()
int main()
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
An implementation of cmdlinet to be used in tests.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
Author: Diffblue Ltd.
Utility for loading and parsing a specified java class file, returning the symbol table generated by ...
The symbol table base class interface.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
Options.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
symbol_tablet load_java_class_lazy(const std::string &java_class_name, const std::string &class_path, const std::string &main)
Go through the process of loading, type-checking and finalising loading a specific class file to buil...
virtual bool parse(std::istream &instream, const std::string &path)=0
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:76
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153