cprover
java_string_library_preprocess.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Produce code for simple implementation of String Java libraries
4 
5 Author: Romain Brenguier
6 
7 Date: 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/ui_message.h>
18 #include <util/std_code.h>
19 #include <util/symbol_table.h>
21 #include <util/string_expr.h>
22 
23 #include <util/ieee_float.h> // should get rid of this
24 
25 #include <array>
26 #include <unordered_set>
27 #include <functional>
29 #include "java_types.h"
30 
31 // Arbitrary limit of 10 arguments for the number of arguments to String.format
32 #define MAX_FORMAT_ARGS 10
33 
35 {
36 public:
41  {
42  }
43 
47 
48  bool implements_function(const irep_idt &function_id) const;
49  void get_all_function_names(std::unordered_set<irep_idt> &methods) const;
50 
51  exprt
52  code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table);
53 
55  {
57  }
58  std::vector<irep_idt> get_string_type_base_classes(
59  const irep_idt &class_name);
60  void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table);
61  bool is_known_string_type(irep_idt class_name);
62 
64  {
69  }
70  static bool implements_java_char_sequence(const typet &type)
71  {
72  return is_java_char_sequence_type(type)
75  || is_java_string_type(type);
76  }
77 
78 private:
79  // We forbid copies of the object
81  const java_string_library_preprocesst &)=delete;
82 
83  static bool java_type_matches_tag(const typet &type, const std::string &tag);
84  static bool is_java_string_pointer_type(const typet &type);
85  static bool is_java_string_type(const typet &type);
86  static bool is_java_string_builder_type(const typet &type);
87  static bool is_java_string_builder_pointer_type(const typet &type);
88  static bool is_java_string_buffer_type(const typet &type);
89  static bool is_java_string_buffer_pointer_type(const typet &type);
90  static bool is_java_char_sequence_type(const typet &type);
91  static bool is_java_char_sequence_pointer_type(const typet &type);
92  static bool is_java_char_array_type(const typet &type);
93  static bool is_java_char_array_pointer_type(const typet &type);
94 
96 
100 
101  typedef std::function<codet(
102  const java_method_typet &,
103  const source_locationt &,
104  const irep_idt &,
107 
108  typedef std::unordered_map<irep_idt, irep_idt> id_mapt;
109 
110  // Table mapping each java method signature to the code generating function
111  std::unordered_map<irep_idt, conversion_functiont> conversion_table;
112 
113  // Some Java functions have an equivalent in the solver that we will
114  // call with the same argument and will return the same result
116 
117  // Some Java functions have an equivalent except that they should
118  // return Java Strings instead of string_exprt
120 
121  // Some Java initialization function initialize strings with the
122  // same result as some function of the solver
124 
125  // Some Java functions have an equivalent in the solver except that
126  // in addition they assign the result to the object on which it is called
128 
129  // Some Java functions have an equivalent in the solver except that
130  // they assign the result to the object on which it is called instead
131  // of returning it
133 
134  const std::array<id_mapt *, 5> id_maps = std::array<id_mapt *, 5>
135  {
136  {
142  }
143  };
144 
145  // A set tells us what java types should be considered as string objects
146  std::unordered_set<irep_idt> string_types;
147 
149  const java_method_typet &type,
150  const source_locationt &loc,
151  const irep_idt &function_id,
152  symbol_table_baset &symbol_table);
153 
155  const java_method_typet &type,
156  const source_locationt &loc,
157  const irep_idt &function_id,
158  symbol_table_baset &symbol_table);
159 
161  const java_method_typet &type,
162  const source_locationt &loc,
163  const irep_idt &function_id,
164  symbol_tablet &symbol_table);
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 
173  const java_method_typet &type,
174  const source_locationt &loc,
175  const irep_idt &function_id,
176  symbol_table_baset &symbol_table);
177 
179  const java_method_typet &type,
180  const source_locationt &loc,
181  const irep_idt &function_id,
182  symbol_table_baset &symbol_table);
183 
185  const java_method_typet &type,
186  const source_locationt &loc,
187  const irep_idt &function_id,
188  symbol_table_baset &symbol_table);
189 
191  const java_method_typet &type,
192  const source_locationt &loc,
193  const irep_idt &function_id,
194  symbol_table_baset &symbol_table);
195 
196  // Helper functions
198  const java_method_typet::parameterst &params,
199  const source_locationt &loc,
200  symbol_table_baset &symbol_table,
201  code_blockt &init_code);
202 
203  // Friending this function for unit testing convert_exprt_to_string_exprt
206  const exprt &deref,
207  const source_locationt &loc,
208  symbol_tablet &symbol_table,
209  code_blockt &init_code);
210 
212  const exprt &deref,
213  const source_locationt &loc,
214  symbol_table_baset &symbol_table,
215  code_blockt &init_code);
216 
218  const exprt::operandst &operands,
219  const source_locationt &loc,
220  symbol_table_baset &symbol_table,
221  code_blockt &init_code);
222 
224  const exprt::operandst &operands,
225  const source_locationt &loc,
226  symbol_table_baset &symbol_table,
227  code_blockt &init_code);
228 
230  const exprt &array_pointer,
231  const source_locationt &loc,
232  symbol_table_baset &symbol_table,
233  code_blockt &code);
234 
236  const typet &type,
237  const source_locationt &loc,
238  symbol_table_baset &symbol_table);
239 
241  const typet &type,
242  const source_locationt &loc,
243  symbol_tablet &symbol_table);
244 
246  const source_locationt &loc,
247  symbol_table_baset &symbol_table,
248  code_blockt &code);
249 
251  const source_locationt &loc,
252  const irep_idt &function_id,
253  symbol_table_baset &symbol_table,
254  code_blockt &code);
255 
257  const typet &type,
258  const source_locationt &loc,
259  const irep_idt &function_id,
260  symbol_table_baset &symbol_table,
261  code_blockt &code);
262 
264  const typet &type,
265  const source_locationt &loc,
266  const irep_idt &function_id,
267  symbol_tablet &symbol_table,
268  code_blockt &code);
269 
271  const irep_idt &function_name,
272  const exprt::operandst &arguments,
273  const typet &type,
274  symbol_table_baset &symbol_table);
275 
277  const irep_idt &function_name,
278  const exprt::operandst &arguments,
279  const source_locationt &loc,
280  symbol_table_baset &symbol_table,
281  code_blockt &code);
282 
284  const exprt &lhs,
285  const exprt &rhs_array,
286  const exprt &rhs_length,
287  const symbol_table_baset &symbol_table);
288 
290  const exprt &lhs,
291  const refined_string_exprt &rhs,
292  const symbol_table_baset &symbol_table);
293 
295  const refined_string_exprt &lhs,
296  const exprt &rhs,
297  const source_locationt &loc,
298  const symbol_table_baset &symbol_table,
299  code_blockt &code);
300 
302  const std::string &s,
303  const source_locationt &loc,
304  symbol_table_baset &symbol_table,
305  code_blockt &code);
306 
308  const irep_idt &function_name,
309  const java_method_typet &type,
310  const source_locationt &loc,
311  symbol_table_baset &symbol_table);
312 
314  const irep_idt &function_name,
315  const java_method_typet &type,
316  const source_locationt &loc,
317  symbol_table_baset &symbol_table,
318  bool ignore_first_arg = true);
319 
321  const irep_idt &function_name,
322  const java_method_typet &type,
323  const source_locationt &loc,
324  symbol_table_baset &symbol_table);
325 
327  const irep_idt &function_name,
328  const java_method_typet &type,
329  const source_locationt &loc,
330  symbol_table_baset &symbol_table);
331 
333  const irep_idt &function_name,
334  const java_method_typet &type,
335  const source_locationt &loc,
336  symbol_table_baset &symbol_table);
337 
339  const exprt &argv,
340  std::size_t index,
341  const struct_typet &structured_type,
342  const source_locationt &loc,
343  const irep_idt &function_id,
344  symbol_table_baset &symbol_table,
345  code_blockt &code);
346 
348  const exprt &object,
349  irep_idt type_name,
350  const source_locationt &loc,
351  symbol_table_baset &symbol_table,
352  code_blockt &code);
353 
354  exprt get_object_at_index(const exprt &argv, std::size_t index);
355 
357  const java_method_typet &type,
358  const source_locationt &loc,
359  const irep_idt &function_id,
360  symbol_table_baset &symbol_table);
361 };
362 
364  symbol_table_baset &symbol_table,
365  const source_locationt &loc,
366  const irep_idt &function_id,
367  code_blockt &code);
368 
370  const exprt &pointer,
371  const exprt &array,
372  symbol_table_baset &symbol_table,
373  const source_locationt &loc,
374  code_blockt &code);
375 
377  const exprt &array,
378  const exprt &length,
379  symbol_table_baset &symbol_table,
380  const source_locationt &loc,
381  code_blockt &code);
382 
384  const exprt &pointer,
385  const exprt &length,
386  const irep_idt &char_set,
387  symbol_table_baset &symbol_table,
388  const source_locationt &loc,
389  code_blockt &code);
390 
391 #endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
#define loc()
The type of an expression.
Definition: type.h:22
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.
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.
static bool is_java_string_type(const typet &type)
codet make_equals_function_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide code for the Java String.equals(Object) function.
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...
static bool is_java_string_pointer_type(const typet &type)
symbol_exprt fresh_array(const typet &type, const source_locationt &loc, symbol_tablet &symbol_table)
add a symbol in the table with static lifetime and name containing cprover_string_array and given typ...
typet java_int_type()
Definition: java_types.cpp:32
Type for string expressions used by the string solver.
const refined_string_typet refined_string_type
codet code_return_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
return the result of a function call
codet make_string_format_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide code for the Java String.format function.
std::vector< parametert > parameterst
Definition: std_types.h:767
refined_string_exprt decl_string_expr(const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Add declaration of a refined string expr whose content and length are fresh symbols.
static bool is_java_char_sequence_pointer_type(const typet &type)
std::unordered_set< irep_idt > string_types
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
Structure type.
Definition: std_types.h:297
refined_string_exprt string_expr_of_function(const irep_idt &function_name, 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...
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
std::function< codet(const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &)> conversion_functiont
static bool is_java_string_buffer_pointer_type(const typet &type)
static bool is_java_string_builder_type(const typet &type)
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
symbol_exprt fresh_string(const typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
add a symbol with static lifetime and name containing cprover_string and given type ...
codet replace_character_call(code_function_callt call)
const std::array< id_mapt *, 5 > id_maps
std::unordered_map< irep_idt, irep_idt > id_mapt
The symbol table.
Definition: symbol_table.h:19
codet make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Provide code for the String.valueOf(F) function.
exprt get_object_at_index(const exprt &argv, std::size_t index)
Helper for format function.
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible, returns the same code otherwise.
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
A function call.
Definition: std_code.h:858
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_set, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
exprt::operandst process_parameters(const java_method_typet::parameterst &params, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
calls string_refine_preprocesst::process_operands with a list of parameters.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
static bool is_java_char_array_pointer_type(const typet &type)
exprt::operandst process_operands(const exprt::operandst &operands, const source_locationt &loc, 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...
codet make_object_get_class_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide our own implementation of the java.lang.Object.getClass() function.
codet make_init_from_array_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide code for constructor from a char array.
codet code_assign_string_expr_to_java_string(const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table)
Produce code for an assignemnt of a string expr to a Java string.
bool implements_function(const irep_idt &function_id) const
std::vector< exprt > operandst
Definition: expr.h:45
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
codet make_string_to_char_array_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table)
codet make_string_length_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for the String.length method.
String expressions for the string solver.
static bool is_java_char_array_type(const typet &type)
exprt make_argument_for_format(const exprt &argv, std::size_t index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
Helper for format function.
exprt code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
Base class for all expressions.
Definition: expr.h:42
The symbol table base class interface.
refined_string_exprt replace_char_array(const exprt &array_pointer, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
we declare a new cprover_string whose contents is deduced from the char array.
codet make_assign_function_from_call(const irep_idt &function_name, 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.
codet make_function_from_call(const irep_idt &function_name, 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...
codet make_copy_constructor_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for a constructor of a string object from another string object.
character_refine_preprocesst character_preprocess
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.
static bool java_type_matches_tag(const typet &type, const std::string &tag)
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Sequential composition.
Definition: std_code.h:89
static bool implements_java_char_sequence_pointer(const typet &type)
exprt allocate_fresh_array(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &code)
declare a new character array and allocate it
static bool is_java_string_buffer_type(const typet &type)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
codet make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for a function which copies a string object to a new string object.
A statement in a programming language.
Definition: std_code.h:21
typet java_char_type()
Definition: java_types.cpp:57
static bool implements_java_char_sequence(const typet &type)
codet make_string_returning_function_from_call(const irep_idt &function_name, 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...
codet make_assign_and_return_function_from_call(const irep_idt &function_name, 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. ...
static bool is_java_string_builder_pointer_type(const typet &type)
codet make_init_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool ignore_first_arg=true)
Generate the goto code for string initialization.
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)
friend refined_string_exprt convert_exprt_to_string_exprt_unit_test(java_string_library_preprocesst &preprocess, const exprt &deref, const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &init_code)
codet code_assign_components_to_java_string(const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table)
Produce code for an assignment of a string expr to a Java string.
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...
exprt::operandst process_equals_function_operands(const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
Converts the operands of the equals function to string expressions and outputs these conversions...
refined_string_exprt convert_exprt_to_string_exprt(const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
Creates a string_exprt from the input exprt representing a char sequence.
static bool is_java_char_sequence_type(const typet &type)
exprt get_primitive_value_of_object(const exprt &object, irep_idt type_name, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Adds to the code an assignment of the form type_name tmp_type_name tmp_type_name = ((Classname*)arg_i...