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_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:78
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
configt::java
struct configt::javat java
java_bytecode_language.h
parse_java_language_options
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
Definition: java_bytecode_language.cpp:48
file_util.h
optionst
Definition: options.h:22
typet
The type of an expression, extends irept.
Definition: type.h:27
load_java_class
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,...
Definition: load_java_class.cpp:47
cmdlinet::set
virtual void set(const std::string &option)
Definition: cmdline.cpp:60
lazy_goto_modelt::process_whole_model_and_freeze
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...
Definition: lazy_goto_model.h:200
configt::main
std::string main
Definition: config.h:172
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1183
language_filet
Definition: language_file.h:40
load_goto_model_from_java_class
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...
Definition: load_java_class.cpp:87
languaget::final
virtual bool final(symbol_table_baset &symbol_table)
Final adjustments, e.g.
Definition: language.cpp:21
goto_modelt
Definition: goto_model.h:24
options.h
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
lazy_goto_model.h
Author: Diffblue Ltd.
configt::javat::classpath
classpatht classpath
Definition: config.h:156
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
message.h
cmdlinet
Definition: cmdline.h:19
languaget::generate_support_functions
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
lazy_goto_modelt
A GOTO model that produces function bodies on demand.
Definition: lazy_goto_model.h:41
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
free_form_cmdlinet
An implementation of cmdlinet to be used in tests.
Definition: free_form_cmdline.h:17
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
irept::id
const irep_idt & id() const
Definition: irep.h:259
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:46
config
configt config
Definition: config.cpp:24
free_form_cmdline.h
load_java_class_lazy
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...
Definition: load_java_class.cpp:35
suffix.h
symbolt
Symbol table entry.
Definition: symbol.h:27
goto_modelt::get_symbol_table
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:76
languaget
Definition: language.h:39
languaget::typecheck
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
config.h
free_form_cmdlinet::add_flag
void add_flag(std::string flag)
Equivalent to specifying –flag for the command line.
Definition: free_form_cmdline.cpp:22
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
get_current_working_directory
std::string get_current_working_directory()
Definition: file_util.cpp:48
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:19
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
main
int main()
Definition: file_converter.cpp:15
null_message_handler
null_message_handlert null_message_handler
Definition: message.cpp:14
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
validation_modet::INVARIANT
load_java_class.h