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 #include <util/optional.h>
25 
26 #include <array>
27 #include <unordered_set>
28 #include <functional>
30 #include "java_types.h"
31 
32 // Arbitrary limit of 10 arguments for the number of arguments to String.format
33 #define MAX_FORMAT_ARGS 10
34 
36 {
37 public:
42  {
43  }
44 
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  codet
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_table_baset &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 
184  // Helper functions
186  const java_method_typet::parameterst &params,
187  const source_locationt &loc,
188  symbol_table_baset &symbol_table,
189  code_blockt &init_code);
190 
191  // Friending this function for unit testing convert_exprt_to_string_exprt
194  const exprt &deref,
195  const source_locationt &loc,
196  symbol_tablet &symbol_table,
197  code_blockt &init_code);
198 
200  const exprt &deref,
201  const source_locationt &loc,
202  symbol_table_baset &symbol_table,
203  code_blockt &init_code);
204 
206  const exprt::operandst &operands,
207  const source_locationt &loc,
208  symbol_table_baset &symbol_table,
209  code_blockt &init_code);
210 
212  const exprt::operandst &operands,
213  const source_locationt &loc,
214  symbol_table_baset &symbol_table,
215  code_blockt &init_code);
216 
218  const exprt &array_pointer,
219  const source_locationt &loc,
220  symbol_table_baset &symbol_table,
221  code_blockt &code);
222 
224  const typet &type,
225  const source_locationt &loc,
226  symbol_table_baset &symbol_table);
227 
229  const typet &type,
230  const source_locationt &loc,
231  symbol_tablet &symbol_table);
232 
234  const source_locationt &loc,
235  symbol_table_baset &symbol_table,
236  code_blockt &code);
237 
239  const source_locationt &loc,
240  const irep_idt &function_id,
241  symbol_table_baset &symbol_table,
242  code_blockt &code);
243 
245  const typet &type,
246  const source_locationt &loc,
247  const irep_idt &function_id,
248  symbol_table_baset &symbol_table,
249  code_blockt &code);
250 
252  const irep_idt &function_name,
253  const exprt::operandst &arguments,
254  const typet &type,
255  symbol_table_baset &symbol_table);
256 
258  const irep_idt &function_name,
259  const exprt::operandst &arguments,
260  const source_locationt &loc,
261  symbol_table_baset &symbol_table,
262  code_blockt &code);
263 
265  const exprt &lhs,
266  const exprt &rhs_array,
267  const exprt &rhs_length,
268  const symbol_table_baset &symbol_table,
269  bool is_constructor);
270 
272  const exprt &lhs,
273  const refined_string_exprt &rhs,
274  const symbol_table_baset &symbol_table,
275  bool is_constructor);
276 
278  const refined_string_exprt &lhs,
279  const exprt &rhs,
280  const source_locationt &loc,
281  const symbol_table_baset &symbol_table,
282  code_blockt &code);
283 
285  const std::string &s,
286  const source_locationt &loc,
287  symbol_table_baset &symbol_table,
288  code_blockt &code);
289 
291  const irep_idt &function_name,
292  const java_method_typet &type,
293  const source_locationt &loc,
294  symbol_table_baset &symbol_table);
295 
297  const irep_idt &function_name,
298  const java_method_typet &type,
299  const source_locationt &loc,
300  symbol_table_baset &symbol_table,
301  bool is_constructor = true);
302 
304  const irep_idt &function_name,
305  const java_method_typet &type,
306  const source_locationt &loc,
307  symbol_table_baset &symbol_table);
308 
310  const irep_idt &function_name,
311  const java_method_typet &type,
312  const source_locationt &loc,
313  symbol_table_baset &symbol_table);
314 
316  const irep_idt &function_name,
317  const java_method_typet &type,
318  const source_locationt &loc,
319  symbol_table_baset &symbol_table);
320 
322  const exprt &argv,
323  std::size_t index,
324  const struct_typet &structured_type,
325  const source_locationt &loc,
326  const irep_idt &function_id,
327  symbol_table_baset &symbol_table,
328  code_blockt &code);
329 
331  const exprt &object,
332  irep_idt type_name,
333  const source_locationt &loc,
334  symbol_table_baset &symbol_table,
335  code_blockt &code);
336 
337  dereference_exprt get_object_at_index(const exprt &argv, std::size_t index);
338 };
339 
341  symbol_table_baset &symbol_table,
342  const source_locationt &loc,
343  const irep_idt &function_id,
344  code_blockt &code);
345 
347  const exprt &pointer,
348  const exprt &array,
349  symbol_table_baset &symbol_table,
350  const source_locationt &loc,
351  code_blockt &code);
352 
354  const exprt &array,
355  const exprt &length,
356  symbol_table_baset &symbol_table,
357  const source_locationt &loc,
358  code_blockt &code);
359 
361  const exprt &pointer,
362  const exprt &length,
363  const irep_idt &char_set,
364  symbol_table_baset &symbol_table,
365  const source_locationt &loc,
366  code_blockt &code);
367 
368 #endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
java_string_library_preprocesst::char_type
const typet char_type
Definition: java_string_library_preprocess.h:97
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
java_string_library_preprocesst::make_copy_string_code
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)
Generates code for a function which copies a string object to a new string object.
Definition: java_string_library_preprocess.cpp:1658
java_string_library_preprocesst::make_string_length_code
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)
Generates code for the String.length method.
Definition: java_string_library_preprocess.cpp:1742
java_string_library_preprocesst::id_mapt
std::unordered_map< irep_idt, irep_idt > id_mapt
Definition: java_string_library_preprocess.h:108
java_string_library_preprocesst::cprover_equivalent_to_java_assign_and_return_function
id_mapt cprover_equivalent_to_java_assign_and_return_function
Definition: java_string_library_preprocess.h:127
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
java_string_library_preprocesst::java_string_library_preprocesst
java_string_library_preprocesst()
Definition: java_string_library_preprocess.h:38
java_string_library_preprocesst::index_type
const typet index_type
Definition: java_string_library_preprocess.h:98
java_int_type
typet java_int_type()
Definition: java_types.cpp:32
java_string_library_preprocesst::fresh_array
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...
Definition: java_string_library_preprocess.cpp:248
character_refine_preprocess.h
typet
The type of an expression, extends irept.
Definition: type.h:27
make_nondet_infinite_char_array
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.
Definition: java_string_library_preprocess.cpp:640
java_string_library_preprocesst::convert_exprt_to_string_exprt_unit_test
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)
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
optional.h
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:3355
character_refine_preprocesst
Definition: character_refine_preprocess.h:29
refined_string_typet
Definition: refined_string_type.h:26
add_pointer_to_array_association
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...
Definition: java_string_library_preprocess.cpp:672
java_string_library_preprocesst::cprover_equivalent_to_java_function
id_mapt cprover_equivalent_to_java_function
Definition: java_string_library_preprocess.h:115
java_string_library_preprocesst::cprover_equivalent_to_java_string_returning_function
id_mapt cprover_equivalent_to_java_string_returning_function
Definition: java_string_library_preprocess.h:119
java_string_library_preprocesst::make_function_from_call
code_blockt 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.
Definition: java_string_library_preprocess.cpp:1584
java_string_library_preprocesst::make_string_returning_function_from_call
code_blockt 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...
Definition: java_string_library_preprocess.cpp:1614
java_string_library_preprocesst::cprover_equivalent_to_java_constructor
id_mapt cprover_equivalent_to_java_constructor
Definition: java_string_library_preprocess.h:123
exprt
Base class for all expressions.
Definition: expr.h:54
java_string_library_preprocesst::implements_function
bool implements_function(const irep_idt &function_id) const
Definition: java_string_library_preprocess.cpp:1761
java_string_library_preprocesst::make_assign_and_return_function_from_call
code_blockt 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.
Definition: java_string_library_preprocess.cpp:1138
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1848
java_string_library_preprocesst::is_java_char_sequence_pointer_type
static bool is_java_char_sequence_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:136
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
java_string_library_preprocesst::code_assign_java_string_to_string_expr
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)
Definition: java_string_library_preprocess.cpp:892
java_string_library_preprocesst::is_java_string_builder_type
static bool is_java_string_builder_type(const typet &type)
Definition: java_string_library_preprocess.cpp:81
java_string_library_preprocesst::make_argument_for_format
struct_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.
Definition: java_string_library_preprocess.cpp:1338
java_string_library_preprocesst::get_string_type_base_classes
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...
Definition: java_string_library_preprocess.cpp:182
refined_string_exprt
Definition: string_expr.h:114
java_string_library_preprocesst::string_literal_to_string_expr
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.
Definition: java_string_library_preprocess.cpp:938
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1920
java_string_library_preprocesst::add_string_type
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.
Definition: java_string_library_preprocess.cpp:208
java_string_library_preprocesst::make_object_get_class_code
code_blockt 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.
Definition: java_string_library_preprocess.cpp:1504
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
java_string_library_preprocesst::process_parameters
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.
Definition: java_string_library_preprocess.cpp:271
java_string_library_preprocesst::conversion_functiont
std::function< codet(const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &)> conversion_functiont
Definition: java_string_library_preprocess.h:106
java_string_library_preprocesst::process_equals_function_operands
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.
Definition: java_string_library_preprocess.cpp:356
java_string_library_preprocesst::conversion_table
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Definition: java_string_library_preprocess.h:111
java_string_library_preprocesst::convert_exprt_to_string_exprt
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.
Definition: java_string_library_preprocess.cpp:301
java_string_library_preprocesst::decl_string_expr
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.
Definition: java_string_library_preprocess.cpp:499
java_string_library_preprocesst::make_copy_constructor_code
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)
Generates code for a constructor of a string object from another string object.
Definition: java_string_library_preprocess.cpp:1701
java_string_library_preprocesst::string_expr_of_function
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...
Definition: java_string_library_preprocess.cpp:780
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
java_string_library_preprocesst::get_all_function_names
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
Definition: java_string_library_preprocess.cpp:1785
java_string_library_preprocesst::is_java_char_array_type
static bool is_java_char_array_type(const typet &type)
Definition: java_string_library_preprocess.cpp:150
java_string_library_preprocesst::replace_character_call
codet replace_character_call(code_function_callt call)
Definition: java_string_library_preprocess.h:54
java_string_library_preprocesst::make_nondet_string_expr
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...
Definition: java_string_library_preprocess.cpp:534
java_string_library_preprocesst::code_for_function
codet 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...
Definition: java_string_library_preprocess.cpp:1800
java_string_library_preprocesst::get_primitive_value_of_object
optionalt< symbol_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.
Definition: java_string_library_preprocess.cpp:1195
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
java_string_library_preprocesst::cprover_equivalent_to_java_assign_function
id_mapt cprover_equivalent_to_java_assign_function
Definition: java_string_library_preprocess.h:132
java_string_library_preprocesst::implements_java_char_sequence
static bool implements_java_char_sequence(const typet &type)
Definition: java_string_library_preprocess.h:70
java_string_library_preprocesst::is_java_char_sequence_type
static bool is_java_char_sequence_type(const typet &type)
Definition: java_string_library_preprocess.cpp:127
java_string_library_preprocesst::process_operands
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...
Definition: java_string_library_preprocess.cpp:326
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
java_string_library_preprocesst::code_return_function_application
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
Definition: java_string_library_preprocess.cpp:611
java_string_library_preprocesst::fresh_string
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
Definition: java_string_library_preprocess.cpp:482
java_string_library_preprocesst::make_init_function_from_call
code_blockt 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 is_constructor=true)
Generate the goto code for string initialization.
Definition: java_string_library_preprocess.cpp:1096
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_string_library_preprocesst::java_type_matches_tag
static bool java_type_matches_tag(const typet &type, const std::string &tag)
Definition: java_string_library_preprocess.cpp:51
java_string_library_preprocesst::character_preprocess
character_refine_preprocesst character_preprocess
Definition: java_string_library_preprocess.h:95
java_string_library_preprocesst::make_string_format_code
code_blockt 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.
Definition: java_string_library_preprocess.cpp:1444
source_locationt
Definition: source_location.h:20
java_string_library_preprocesst::is_java_char_array_pointer_type
static bool is_java_char_array_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:159
java_string_library_preprocesst::make_float_to_string_code
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)
Provide code for the String.valueOf(F) function.
Definition: java_string_library_preprocess.cpp:955
java_string_library_preprocesst::is_java_string_buffer_type
static bool is_java_string_buffer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:104
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
add_array_to_length_association
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...
Definition: java_string_library_preprocess.cpp:706
refined_string_type.h
java_string_library_preprocesst::refined_string_type
const refined_string_typet refined_string_type
Definition: java_string_library_preprocess.h:99
java_string_library_preprocesst::code_assign_components_to_java_string
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.
Definition: java_string_library_preprocess.cpp:828
java_string_library_preprocesst::is_java_string_buffer_pointer_type
static bool is_java_string_buffer_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:113
java_string_library_preprocesst::id_maps
const std::array< id_mapt *, 5 > id_maps
Definition: java_string_library_preprocess.h:134
java_string_library_preprocesst::implements_java_char_sequence_pointer
static bool implements_java_char_sequence_pointer(const typet &type)
Definition: java_string_library_preprocess.h:63
symbolt
Symbol table entry.
Definition: symbol.h:27
ieee_float.h
java_string_library_preprocesst
Definition: java_string_library_preprocess.h:35
add_character_set_constraint
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...
Definition: java_string_library_preprocess.cpp:741
java_string_library_preprocesst::is_known_string_type
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
Definition: java_string_library_preprocess.cpp:1842
java_string_library_preprocesst::allocate_fresh_string
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
Definition: java_string_library_preprocess.cpp:570
java_char_type
typet java_char_type()
Definition: java_types.cpp:57
loc
#define loc()
Definition: ansi_c_lex.yy.cpp:4256
java_string_library_preprocesst::initialize_conversion_table
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
Definition: java_string_library_preprocess.cpp:1857
java_string_library_preprocesst::get_object_at_index
dereference_exprt get_object_at_index(const exprt &argv, std::size_t index)
Helper for format function.
Definition: java_string_library_preprocess.cpp:1293
java_string_library_preprocesst::make_assign_function_from_call
code_blockt 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.
Definition: java_string_library_preprocess.cpp:1163
java_types.h
symbol_table.h
Author: Diffblue Ltd.
is_constructor
static bool is_constructor(const irep_idt &method_name)
Definition: java_bytecode_convert_method.cpp:126
java_string_library_preprocesst::is_java_string_pointer_type
static bool is_java_string_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:59
java_string_library_preprocesst::code_assign_string_expr_to_java_string
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.
Definition: java_string_library_preprocess.cpp:873
character_refine_preprocesst::replace_character_call
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible,...
Definition: character_refine_preprocess.cpp:1374
java_string_library_preprocesst::string_types
std::unordered_set< irep_idt > string_types
Definition: java_string_library_preprocess.h:146
string_expr.h
java_method_typet
Definition: java_types.h:264
java_string_library_preprocesst::is_java_string_type
static bool is_java_string_type(const typet &type)
Definition: java_string_library_preprocess.cpp:73
java_string_library_preprocesst::is_java_string_builder_pointer_type
static bool is_java_string_builder_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:90
java_string_library_preprocesst::replace_char_array
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.
Definition: java_string_library_preprocess.cpp:446
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
ui_message.h