cprover
Loading...
Searching...
No Matches
java_string_library_preprocess.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Produce code for simple implementation of String Java libraries
4
5Author: Romain Brenguier
6
7Date: March 2017
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
15#define CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
16
17#include <util/std_code.h>
18#include <util/symbol_table.h>
20#include <util/string_expr.h>
21
22#include <util/ieee_float.h> // should get rid of this
23#include <util/optional.h>
24
25#include <array>
26#include <unordered_set>
27#include <functional>
29#include "java_types.h"
30
32
33// Arbitrary limit of 10 arguments for the number of arguments to String.format
34#define MAX_FORMAT_ARGS 10
35
37{
38public:
43 {
44 }
45
48
49 bool implements_function(const irep_idt &function_id) const;
50 void get_all_function_names(std::unordered_set<irep_idt> &methods) const;
51
53 const symbolt &symbol,
54 symbol_table_baset &symbol_table,
55 message_handlert &message_handler);
56
58 {
60 }
61 std::vector<irep_idt> get_string_type_base_classes(
62 const irep_idt &class_name);
63 void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table);
64 bool is_known_string_type(irep_idt class_name);
65
67 {
72 }
73 static bool implements_java_char_sequence(const typet &type)
74 {
78 || is_java_string_type(type);
79 }
80
81private:
82 // We forbid copies of the object
84 const java_string_library_preprocesst &)=delete;
85
86 static bool java_type_matches_tag(const typet &type, const std::string &tag);
87 static bool is_java_string_pointer_type(const typet &type);
88 static bool is_java_string_type(const typet &type);
89 static bool is_java_string_builder_type(const typet &type);
90 static bool is_java_string_builder_pointer_type(const typet &type);
91 static bool is_java_string_buffer_type(const typet &type);
92 static bool is_java_string_buffer_pointer_type(const typet &type);
93 static bool is_java_char_sequence_type(const typet &type);
94 static bool is_java_char_sequence_pointer_type(const typet &type);
95 static bool is_java_char_array_type(const typet &type);
96 static bool is_java_char_array_pointer_type(const typet &type);
97
99
103
104 typedef std::function<codet(
105 const java_method_typet &,
106 const source_locationt &,
107 const irep_idt &,
111
112 typedef std::unordered_map<irep_idt, irep_idt> id_mapt;
113
114 // Table mapping each java method signature to the code generating function
115 std::unordered_map<irep_idt, conversion_functiont> conversion_table;
116
117 // Some Java functions have an equivalent in the solver that we will
118 // call with the same argument and will return the same result
120
121 // Some Java functions have an equivalent except that they should
122 // return Java Strings instead of string_exprt
124
125 // Some Java initialization function initialize strings with the
126 // same result as some function of the solver
128
129 // Some Java functions have an equivalent in the solver except that
130 // in addition they assign the result to the object on which it is called
132
133 // Some Java functions have an equivalent in the solver except that
134 // they assign the result to the object on which it is called instead
135 // of returning it
137
138 const std::array<id_mapt *, 5> id_maps = std::array<id_mapt *, 5>
139 {
140 {
146 }
147 };
148
149 // A set tells us what java types should be considered as string objects
150 std::unordered_set<irep_idt> string_types;
151
153 const java_method_typet &type,
154 const source_locationt &loc,
155 const irep_idt &function_id,
156 symbol_table_baset &symbol_table,
157 message_handlert &message_handler);
158
160 const java_method_typet &type,
161 const source_locationt &loc,
162 const irep_idt &function_id,
163 symbol_table_baset &symbol_table,
164 message_handlert &message_handler);
165
167 const java_method_typet &type,
168 const source_locationt &loc,
169 const irep_idt &function_id,
170 symbol_table_baset &symbol_table,
171 message_handlert &message_handler);
172
174 const java_method_typet &type,
175 const source_locationt &loc,
176 const irep_idt &function_id,
177 symbol_table_baset &symbol_table,
178 message_handlert &message_handler);
179
181 const java_method_typet &type,
182 const source_locationt &loc,
183 const irep_idt &function_id,
184 symbol_table_baset &symbol_table,
185 message_handlert &message_handler);
186
187 // Helper functions
189 const java_method_typet::parameterst &params,
190 const source_locationt &loc,
191 const irep_idt &function_name,
192 symbol_table_baset &symbol_table,
193 code_blockt &init_code);
194
195 // Friending this function for unit testing convert_exprt_to_string_exprt
198 const exprt &deref,
199 const source_locationt &loc,
200 const irep_idt &function_id,
201 symbol_tablet &symbol_table,
202 code_blockt &init_code);
203
205 const exprt &deref,
206 const source_locationt &loc,
207 symbol_table_baset &symbol_table,
208 const irep_idt &function_name,
209 code_blockt &init_code);
210
212 const exprt::operandst &operands,
213 const source_locationt &loc,
214 const irep_idt &function_name,
215 symbol_table_baset &symbol_table,
216 code_blockt &init_code);
217
219 const exprt &array_pointer,
220 const source_locationt &loc,
221 const irep_idt &function_name,
222 symbol_table_baset &symbol_table,
223 code_blockt &code);
224
226 const typet &type,
227 const source_locationt &loc,
228 const irep_idt &function_id,
229 symbol_table_baset &symbol_table);
230
232 const source_locationt &loc,
233 const irep_idt &function_id,
234 symbol_table_baset &symbol_table,
235 code_blockt &code);
236
238 const source_locationt &loc,
239 const irep_idt &function_id,
240 symbol_table_baset &symbol_table,
241 code_blockt &code);
242
244 const typet &type,
245 const source_locationt &loc,
246 const irep_idt &function_id,
247 symbol_table_baset &symbol_table,
248 code_blockt &code);
249
251 const irep_idt &function_id,
252 const exprt::operandst &arguments,
253 const typet &type,
254 symbol_table_baset &symbol_table);
255
257 const irep_idt &function_id,
258 const exprt::operandst &arguments,
259 const source_locationt &loc,
260 symbol_table_baset &symbol_table,
261 code_blockt &code);
262
264 const exprt &lhs,
265 const exprt &rhs_array,
266 const exprt &rhs_length,
267 const symbol_table_baset &symbol_table,
268 bool is_constructor);
269
271 const exprt &lhs,
272 const refined_string_exprt &rhs,
273 const symbol_table_baset &symbol_table,
274 bool is_constructor);
275
277 const refined_string_exprt &lhs,
278 const exprt &rhs,
279 const source_locationt &loc,
280 const symbol_table_baset &symbol_table,
281 code_blockt &code);
282
284 const std::string &s,
285 const source_locationt &loc,
286 symbol_table_baset &symbol_table,
287 code_blockt &code);
288
290 const irep_idt &function_id,
291 const java_method_typet &type,
292 const source_locationt &loc,
293 symbol_table_baset &symbol_table);
294
296 const irep_idt &function_id,
297 const java_method_typet &type,
298 const source_locationt &loc,
299 symbol_table_baset &symbol_table,
300 bool is_constructor = true);
301
303 const irep_idt &function_id,
304 const java_method_typet &type,
305 const source_locationt &loc,
306 symbol_table_baset &symbol_table);
307
309 const irep_idt &function_id,
310 const java_method_typet &type,
311 const source_locationt &loc,
312 symbol_table_baset &symbol_table);
313
315 const irep_idt &function_id,
316 const java_method_typet &type,
317 const source_locationt &loc,
318 symbol_table_baset &symbol_table);
319};
320
322 symbol_table_baset &symbol_table,
323 const source_locationt &loc,
324 const irep_idt &function_id,
325 code_blockt &code);
326
328 const exprt &pointer,
329 const exprt &array,
330 symbol_table_baset &symbol_table,
331 const source_locationt &loc,
332 const irep_idt &function_id,
333 code_blockt &code);
334
336 const exprt &array,
337 const exprt &length,
338 symbol_table_baset &symbol_table,
339 const source_locationt &loc,
340 const irep_idt &function_id,
341 code_blockt &code);
342
344 const exprt &pointer,
345 const exprt &length,
346 const irep_idt &char_range,
347 symbol_table_baset &symbol_table,
348 const source_locationt &loc,
349 const irep_idt &function_id,
350 code_blockt &code);
351
352#endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
static std::string preprocess(const std::string &source_file, const c_wranglert &c_wrangler)
Definition: c_wrangler.cpp:321
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible,...
A codet representing sequential composition of program statements.
Definition: std_code.h:130
codet representation of a function call statement.
codet representation of a "return from a function" statement.
std::vector< parametert > parameterst
Definition: std_types.h:542
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
code_blockt make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Provide code for the String.valueOf(F) function.
std::unordered_map< irep_idt, irep_idt > id_mapt
friend refined_string_exprt convert_exprt_to_string_exprt_unit_test(java_string_library_preprocesst &preprocess, const exprt &deref, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &init_code)
code_blockt make_string_returning_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Provide code for a function that calls a function from the solver and return the string_expr result a...
code_returnt make_string_length_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Generates code for the String.length method.
refined_string_exprt string_literal_to_string_expr(const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Create a string expression whose value is given by a literal.
codet code_assign_components_to_java_string(const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table, bool is_constructor)
Produce code for an assignment of a string expr to a Java string.
refined_string_exprt convert_exprt_to_string_exprt(const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, const irep_idt &function_name, code_blockt &init_code)
Creates a string_exprt from the input exprt representing a char sequence.
java_string_library_preprocesst(const java_string_library_preprocesst &)=delete
void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Add to the symbol table type declaration for a String-like Java class.
code_blockt make_assign_and_return_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function, assign the result to object this and return it.
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
static bool implements_java_char_sequence_pointer(const typet &type)
std::function< codet(const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &, message_handlert &)> conversion_functiont
std::unordered_map< irep_idt, conversion_functiont > conversion_table
refined_string_exprt string_expr_of_function(const irep_idt &function_id, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primit...
code_blockt make_class_identifier_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Used to provide our own implementation of the CProver.classIdentifier() function.
static bool is_java_char_sequence_type(const typet &type)
static bool is_java_string_buffer_type(const typet &type)
bool implements_function(const irep_idt &function_id) const
code_blockt make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Generates code for a function which copies a string object to a new string object.
std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)
Gets the base classes for known String and String-related types, or returns an empty list for other t...
static bool is_java_char_array_pointer_type(const typet &type)
refined_string_exprt make_nondet_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr fro...
code_blockt make_assign_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function and assign the result to object this.
exprt allocate_fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
declare a new String and allocate it
static bool is_java_string_pointer_type(const typet &type)
refined_string_exprt replace_char_array(const exprt &array_pointer, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &code)
we declare a new cprover_string whose contents is deduced from the char array.
static bool is_java_string_builder_pointer_type(const typet &type)
exprt::operandst process_parameters(const java_method_typet::parameterst &params, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)
calls string_refine_preprocesst::process_operands with a list of parameters.
static bool is_java_char_sequence_pointer_type(const typet &type)
static bool is_java_char_array_type(const typet &type)
code_blockt make_init_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool is_constructor=true)
Generate the goto code for string initialization.
codet replace_character_call(code_function_callt call)
character_refine_preprocesst character_preprocess
static bool is_java_string_builder_type(const typet &type)
code_blockt make_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Provide code for a function that calls a function from the solver and simply returns it.
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
std::unordered_set< irep_idt > string_types
codet code_assign_string_expr_to_java_string(const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table, bool is_constructor)
Produce code for an assignemnt of a string expr to a Java string.
static bool is_java_string_buffer_pointer_type(const typet &type)
codet code_return_function_application(const irep_idt &function_id, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
return the result of a function call
symbol_exprt fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
add a symbol with static lifetime and name containing cprover_string and given type
code_blockt make_copy_constructor_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Generates code for a constructor of a string object from another string object.
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
static bool implements_java_char_sequence(const typet &type)
exprt::operandst process_operands(const exprt::operandst &operands, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)
for each expression that is of a type implementing strings, we declare a new cprover_string whose con...
static bool is_java_string_type(const typet &type)
const std::array< id_mapt *, 5 > id_maps
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler)
Should be called to provide code for string functions that are used in the code but for which no impl...
static bool java_type_matches_tag(const typet &type, const std::string &tag)
refined_string_exprt decl_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
Add declaration of a refined string expr whose content and length are fresh symbols.
void code_assign_java_string_to_string_expr(const refined_string_exprt &lhs, const exprt &rhs, const source_locationt &loc, const symbol_table_baset &symbol_table, code_blockt &code)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
static bool is_constructor(const irep_idt &method_name)
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_range, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
signedbv_typet java_int_type()
Definition: java_types.cpp:31
unsignedbv_typet java_char_type()
Definition: java_types.cpp:61
Type for string expressions used by the string solver.
String expressions for the string solver.
Author: Diffblue Ltd.