cprover
Loading...
Searching...
No Matches
load_java_class.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unit test utilities
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
9#include "load_java_class.h"
10
11#include <iostream>
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
43}
44
48 const std::string &java_class_name,
49 const std::string &class_path,
50 const std::string &main)
51{
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{
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
97 std::string filename=java_class_name + ".class";
98
99 // Construct a lazy_goto_modelt
102 [](goto_modelt &) { return false; },
103 [](const irep_idt &) { return false; },
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 config.java.main_class = java_class_name;
114
115 // Add the language to the model
116 language_filet &lf=lazy_goto_model.add_language_file(filename);
117 lf.language=std::move(java_lang);
118 languaget &language=*lf.language;
119
120 std::istringstream java_code_stream("ignored");
121
122 optionst options;
123 parse_java_language_options(command_line, options);
124
125 // Configure the language, load the class files
127 language.set_language_options(options);
128 language.parse(java_code_stream, filename);
129 language.typecheck(lazy_goto_model.symbol_table, "");
130 language.generate_support_functions(lazy_goto_model.symbol_table);
131 language.final(lazy_goto_model.symbol_table);
132
133 lazy_goto_model.load_all_functions();
134
135 std::unique_ptr<goto_modelt> maybe_goto_model=
137 std::move(lazy_goto_model));
138 INVARIANT(maybe_goto_model, "Freezing lazy_goto_model failed");
139
140 // Verify that the class was loaded
141 const std::string class_symbol_name="java::"+java_class_name;
142 REQUIRE(maybe_goto_model->symbol_table.has_symbol(class_symbol_name));
143 const symbolt &class_symbol=
144 *maybe_goto_model->symbol_table.lookup(class_symbol_name);
145 REQUIRE(class_symbol.is_type);
146 const typet &class_type=class_symbol.type;
148
149 // Log the working directory to help people identify the common error
150 // of wrong working directory (should be the `unit` directory when running
151 // the unit tests).
152 std::string path = get_current_working_directory();
153 INFO("Working directory: " << path);
154
155 // if this fails it indicates the class was not loaded
156 // Check your working directory and the class path is correctly configured
157 // as this often indicates that one of these is wrong.
159 return std::move(*maybe_goto_model);
160}
161
166 const std::string &java_class_name,
167 const std::string &class_path,
168 const std::string &main,
169 std::unique_ptr<languaget> &&java_lang)
170{
171 free_form_cmdlinet command_line;
172 command_line.add_flag("no-lazy-methods");
173 return load_java_class(
174 java_class_name, class_path, main, std::move(java_lang), command_line);
175}
176
178 const std::string &java_class_name,
179 const std::string &class_path,
180 const std::vector<std::string> &command_line_flags,
181 const std::unordered_map<std::string, std::string> &command_line_options,
182 const std::string &main)
183{
184 free_form_cmdlinet command_line;
185 for(const auto &flag : command_line_flags)
186 command_line.add_flag(flag);
187 for(const auto &option : command_line_options)
188 command_line.add_option(option.first, option.second);
189
190 std::unique_ptr<languaget> lang = new_java_bytecode_language();
191
193 java_class_name, class_path, main, std::move(lang), command_line);
194}
195
200 const std::string &java_class_name,
201 const std::string &class_path,
202 const std::string &main)
203{
205 java_class_name, class_path, {"no-lazy-methods"}, {}, main);
206}
configt config
Definition config.cpp:25
Abstract interface to eager or lazy GOTO models.
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
optionalt< std::string > main
Definition config.h:353
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:39
An implementation of cmdlinet to be used in tests.
void add_flag(std::string flag)
Equivalent to specifying –flag for the command line.
void add_option(std::string flag, std::string value)
Equivalent to specifying –flag value.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:190
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition goto_model.h:84
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition language.h:39
virtual bool final(symbol_table_baset &symbol_table)
Final adjustments, e.g.
Definition language.cpp:16
virtual bool parse(std::istream &instream, const std::string &path)=0
virtual bool typecheck(symbol_table_baset &symbol_table, const std::string &module)=0
virtual bool generate_support_functions(symbol_table_baset &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
A GOTO model that produces function bodies on demand.
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...
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
The symbol table base class interface.
The symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
int main()
Definition example.cpp:18
std::string get_current_working_directory()
Definition file_util.cpp:51
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
std::unique_ptr< languaget > new_java_bytecode_language()
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:582
Author: Diffblue Ltd.
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,...
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...
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...
Utility for loading and parsing a specified java class file, returning the symbol table generated by ...
Options.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
null_message_handlert null_message_handler
Definition message.cpp:14