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/suffix.h>
18 
20 
21 #include <langapi/mode.h>
22 
24 #include <util/file_util.h>
25 
37  const std::string &java_class_name,
38  const std::string &class_path,
39  const std::string &main)
40 {
42 
43  return load_java_class(
44  java_class_name, class_path, main, get_language_from_mode(ID_java));
45 }
46 
57  const std::string &java_class_name,
58  const std::string &class_path,
59  const std::string &main)
60 {
61  free_form_cmdlinet command_line;
62  command_line.add_flag("no-lazy-methods");
63  command_line.add_flag("no-refine-strings");
64 
66 
67  return load_java_class(
68  java_class_name,
69  class_path,
70  main,
71  get_language_from_mode(ID_java),
72  command_line);
73 }
74 
87  const std::string &java_class_name,
88  const std::string &class_path,
89  const std::string &main,
90  std::unique_ptr<languaget> &&java_lang,
91  const cmdlinet &command_line)
92 {
93  // We expect the name of the class without the .class suffix to allow us to
94  // check it
95  PRECONDITION(!has_suffix(java_class_name, ".class"));
96  std::string filename=java_class_name + ".class";
97 
98  // Construct a lazy_goto_modelt
99  lazy_goto_modelt lazy_goto_model(
100  [](goto_model_functiont &function, const abstract_goto_modelt &model) {},
101  [](goto_modelt &goto_model) { return false; },
102  [](const irep_idt &name) { return false; },
103  [](
104  const irep_idt &function_name,
105  symbol_table_baset &symbol_table,
106  goto_functiont &function,
107  bool body_available) { return false; },
109 
110  // Configure the path loading
111  config.java.classpath.clear();
112  config.java.classpath.push_back(class_path);
113  config.main = main;
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  // Configure the language, load the class files
124  language.get_language_options(command_line);
125  language.parse(java_code_stream, filename);
126  language.typecheck(lazy_goto_model.symbol_table, "");
127  language.generate_support_functions(lazy_goto_model.symbol_table);
128  language.final(lazy_goto_model.symbol_table);
129 
130  lazy_goto_model.load_all_functions();
131 
132  std::unique_ptr<goto_modelt> maybe_goto_model=
134  std::move(lazy_goto_model));
135  INVARIANT(maybe_goto_model, "Freezing lazy_goto_model failed");
136 
137  // Verify that the class was loaded
138  const std::string class_symbol_name="java::"+java_class_name;
139  REQUIRE(maybe_goto_model->symbol_table.has_symbol(class_symbol_name));
140  const symbolt &class_symbol=
141  *maybe_goto_model->symbol_table.lookup(class_symbol_name);
142  REQUIRE(class_symbol.is_type);
143  const typet &class_type=class_symbol.type;
144  REQUIRE(class_type.id()==ID_struct);
145 
146  // Log the working directory to help people identify the common error
147  // of wrong working directory (should be the `unit` directory when running
148  // the unit tests).
149  std::string path = get_current_working_directory();
150  INFO("Working directory: " << path);
151 
152  // if this fails it indicates the class was not loaded
153  // Check your working directory and the class path is correctly configured
154  // as this often indicates that one of these is wrong.
155  REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class));
156  return std::move(maybe_goto_model->symbol_table);
157 }
158 
160  const std::string &java_class_name,
161  const std::string &class_path,
162  const std::string &main,
163  std::unique_ptr<languaget> &&java_lang)
164 {
165  free_form_cmdlinet command_line;
166  command_line.add_flag("no-lazy-methods");
167  command_line.add_flag("no-refine-strings");
168  // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an
169  // TODO(tkiley): unknown argument. This could be changed by using the
170  // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail.
171  // TODO(tkiley): TG-2708 to investigate and fix
172  command_line.set("java-cp-include-files", class_path);
173  return load_java_class(
174  java_class_name, class_path, main, std::move(java_lang), command_line);
175 }
symbol_tablet load_java_class(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...
The type of an expression.
Definition: type.h:22
Abstract interface to eager or lazy GOTO models.
virtual void get_language_options(const cmdlinet &)
Definition: language.h:43
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
null_message_handlert null_message_handler
Definition: message.cpp:14
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
Model that holds partially loaded map of functions.
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
configt config
Definition: config.cpp:23
std::string get_current_working_directory()
Definition: file_util.cpp:45
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
std::unique_ptr< languaget > language
Definition: language_file.h:46
const irep_idt & id() const
Definition: irep.h:259
classpatht classpath
Definition: config.h:155
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:171
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&#39;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:242
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:148
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:33
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.
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.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:38
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 symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147