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 {
41  free_form_cmdlinet lazy_command_line;
42  lazy_command_line.add_flag("lazy-methods");
43 
45 
46  return load_java_class(
47  java_class_name,
48  class_path,
49  main,
50  get_language_from_mode(ID_java),
51  lazy_command_line);
52 }
53 
64  const std::string &java_class_name,
65  const std::string &class_path,
66  const std::string &main)
67 {
69 
70  return load_java_class(
71  java_class_name, class_path, main, get_language_from_mode(ID_java));
72 }
73 
86  const std::string &java_class_name,
87  const std::string &class_path,
88  const std::string &main,
89  std::unique_ptr<languaget> &&java_lang,
90  const cmdlinet &command_line)
91 {
92  // We expect the name of the class without the .class suffix to allow us to
93  // check it
94  PRECONDITION(!has_suffix(java_class_name, ".class"));
95  std::string filename=java_class_name + ".class";
96 
97  // Construct a lazy_goto_modelt
98  lazy_goto_modelt lazy_goto_model(
99  [](goto_model_functiont &function, const abstract_goto_modelt &model) {},
100  [](goto_modelt &goto_model) { return false; },
101  [](const irep_idt &name) { return false; },
102  [](
103  const irep_idt &function_name,
104  symbol_table_baset &symbol_table,
105  goto_functiont &function,
106  bool body_available) { return false; },
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  // Configure the language, load the class files
123  language.get_language_options(command_line);
124  language.parse(java_code_stream, filename);
125  language.typecheck(lazy_goto_model.symbol_table, "");
126  language.generate_support_functions(lazy_goto_model.symbol_table);
127  language.final(lazy_goto_model.symbol_table);
128 
129  lazy_goto_model.load_all_functions();
130 
131  std::unique_ptr<goto_modelt> maybe_goto_model=
133  std::move(lazy_goto_model));
134  INVARIANT(maybe_goto_model, "Freezing lazy_goto_model failed");
135 
136  // Verify that the class was loaded
137  const std::string class_symbol_name="java::"+java_class_name;
138  REQUIRE(maybe_goto_model->symbol_table.has_symbol(class_symbol_name));
139  const symbolt &class_symbol=
140  *maybe_goto_model->symbol_table.lookup(class_symbol_name);
141  REQUIRE(class_symbol.is_type);
142  const typet &class_type=class_symbol.type;
143  REQUIRE(class_type.id()==ID_struct);
144 
145  // Log the working directory to help people identify the common error
146  // of wrong working directory (should be the `unit` directory when running
147  // the unit tests).
148  std::string path = get_current_working_directory();
149  INFO("Working directory: " << path);
150 
151  // if this fails it indicates the class was not loaded
152  // Check your working directory and the class path is correctly configured
153  // as this often indicates that one of these is wrong.
154  REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class));
155  return std::move(maybe_goto_model->symbol_table);
156 }
157 
159  const std::string &java_class_name,
160  const std::string &class_path,
161  const std::string &main,
162  std::unique_ptr<languaget> &&java_lang)
163 {
164  cmdlinet command_line;
165  // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an
166  // TODO(tkiley): unknown argument. This could be changed by using the
167  // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail.
168  // TODO(tkiley): TG-2708 to investigate and fix
169  command_line.set("java-cp-include-files", class_path);
170  return load_java_class(
171  java_class_name, class_path, main, std::move(java_lang), command_line);
172 }
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:205
std::unique_ptr< languaget > language
Definition: language_file.h:46
const irep_idt & id() const
Definition: irep.h:189
classpatht classpath
Definition: config.h:147
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:163
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:230
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
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