49 std::ostringstream buf;
50 buf <<
"string_refinement#" << prefix <<
"#" << (
next_symbol_id++);
104 const exprt &unrefined_string)
108 if(unrefined_string.
id()==ID_function_application)
114 else if(unrefined_string.
id()==ID_symbol)
116 else if(unrefined_string.
id()==ID_address_of)
118 assert(unrefined_string.
op0().
id()==ID_symbol);
121 else if(unrefined_string.
id()==ID_if)
123 else if(unrefined_string.
id()==ID_nondet_symbol ||
124 unrefined_string.
id()==ID_struct)
128 else if(unrefined_string.
id()==ID_typecast)
136 throw "add_axioms_for_string_expr:\n"+unrefined_string.
pretty()+
137 "\nwhich is not a function application, "+
138 "a symbol or an if expression";
189 return entry.first->second;
201 assert(name.
id()==ID_symbol);
209 if(
id==ID_cprover_char_literal_func)
211 else if(
id==ID_cprover_string_length_func)
213 else if(
id==ID_cprover_string_equal_func)
215 else if(
id==ID_cprover_string_equals_ignore_case_func)
217 else if(
id==ID_cprover_string_is_empty_func)
219 else if(
id==ID_cprover_string_char_at_func)
221 else if(
id==ID_cprover_string_is_prefix_func)
223 else if(
id==ID_cprover_string_is_suffix_func)
225 else if(
id==ID_cprover_string_startswith_func)
227 else if(
id==ID_cprover_string_endswith_func)
229 else if(
id==ID_cprover_string_contains_func)
231 else if(
id==ID_cprover_string_hash_code_func)
233 else if(
id==ID_cprover_string_index_of_func)
235 else if(
id==ID_cprover_string_last_index_of_func)
237 else if(
id==ID_cprover_string_parse_int_func)
239 else if(
id==ID_cprover_string_to_char_array_func)
241 else if(
id==ID_cprover_string_code_point_at_func)
243 else if(
id==ID_cprover_string_code_point_before_func)
245 else if(
id==ID_cprover_string_code_point_count_func)
247 else if(
id==ID_cprover_string_offset_by_code_point_func)
249 else if(
id==ID_cprover_string_compare_to_func)
251 else if(
id==ID_cprover_string_literal_func)
253 else if(
id==ID_cprover_string_concat_func)
255 else if(
id==ID_cprover_string_concat_int_func)
257 else if(
id==ID_cprover_string_concat_long_func)
259 else if(
id==ID_cprover_string_concat_bool_func)
261 else if(
id==ID_cprover_string_concat_char_func)
263 else if(
id==ID_cprover_string_concat_double_func)
265 else if(
id==ID_cprover_string_concat_float_func)
267 else if(
id==ID_cprover_string_concat_code_point_func)
269 else if(
id==ID_cprover_string_insert_func)
271 else if(
id==ID_cprover_string_insert_int_func)
273 else if(
id==ID_cprover_string_insert_long_func)
275 else if(
id==ID_cprover_string_insert_bool_func)
277 else if(
id==ID_cprover_string_insert_char_func)
279 else if(
id==ID_cprover_string_insert_double_func)
281 else if(
id==ID_cprover_string_insert_float_func)
283 else if(
id==ID_cprover_string_insert_char_array_func)
285 else if(
id==ID_cprover_string_substring_func)
287 else if(
id==ID_cprover_string_trim_func)
289 else if(
id==ID_cprover_string_to_lower_case_func)
291 else if(
id==ID_cprover_string_to_upper_case_func)
293 else if(
id==ID_cprover_string_char_set_func)
295 else if(
id==ID_cprover_string_value_of_func)
297 else if(
id==ID_cprover_string_empty_string_func)
299 else if(
id==ID_cprover_string_copy_func)
301 else if(
id==ID_cprover_string_of_int_func)
303 else if(
id==ID_cprover_string_of_int_hex_func)
305 else if(
id==ID_cprover_string_of_float_func)
307 else if(
id==ID_cprover_string_of_double_func)
309 else if(
id==ID_cprover_string_of_long_func)
311 else if(
id==ID_cprover_string_of_bool_func)
313 else if(
id==ID_cprover_string_of_char_func)
315 else if(
id==ID_cprover_string_of_char_array_func)
317 else if(
id==ID_cprover_string_set_length_func)
319 else if(
id==ID_cprover_string_delete_func)
321 else if(
id==ID_cprover_string_delete_char_at_func)
323 else if(
id==ID_cprover_string_replace_func)
328 "string_constraint_generator::function_application: unknown symbol :");
349 axioms.push_back(res.axiom_for_has_same_length_as(s1));
362 const exprt &char_array)
407 exprt char_in_tab=data;
408 assert(char_in_tab.
id()==ID_index);
460 assert(args.size()==1);
462 const exprt &arg=args[0];
465 if(arg.operands().size()==1 &&
466 arg.op0().operands().size()==1 &&
467 arg.op0().op0().operands().size()==2 &&
468 arg.op0().op0().op0().id()==ID_string_constant)
472 assert(sval.size()==1);
477 throw "convert_char_literal unimplemented";
512 if(str.
id()==ID_symbol)
exprt add_axioms_for_compare_to(const function_application_exprt &f)
add axioms corresponding to the String.compareTo java function
The type of an expression.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
string_exprt add_axioms_for_insert_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(C) java function
string_exprt add_axioms_for_insert_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(I) java function
string_exprt add_axioms_from_literal(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the string literal ...
exprt add_axioms_for_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt &offset)
add axioms stating that the returned expression is true exactly when the first string is a prefix of ...
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
string_exprt add_axioms_for_java_char_array(const exprt &char_array)
add axioms corresponding to the String.valueOf([C) java function
Generates string constraints to link results from string functions with their arguments.
void assign_to_symbol(const symbol_exprt &sym, const string_exprt &expr)
exprt add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
string_exprt add_axioms_for_concat_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(D) java function
std::list< symbol_exprt > boolean_symbols
string_exprt add_axioms_for_delete(const string_exprt &str, const exprt &start, const exprt &end)
add axioms stating that the returned string corresponds to the input one where we removed characters ...
string_exprt add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
application of (mathematical) function
string_exprt add_axioms_from_bool(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(Z) java function
string_exprt & to_string_expr(exprt &expr)
string_exprt add_axioms_for_concat_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(I) java function
const typet & get_char_type() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
exprt add_axioms_for_equals(const function_application_exprt &f)
add axioms stating that the result is true exactly when the strings represented by the arguments are ...
exprt add_axioms_for_length(const function_application_exprt &f)
add axioms corresponding to the String.length java function
const irep_idt & get_identifier() const
string_exprt add_axioms_for_copy(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the argument of the function applic...
string_exprt add_axioms_for_insert_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(F) java function
string_exprt add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
static symbol_exprt fresh_symbol(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
exprt add_axioms_for_contains(const function_application_exprt &f)
add axioms corresponding to the String.contains java function
exprt add_axioms_for_code_point_count(const function_application_exprt &f)
add axioms giving approximate bounds on the result of the String.codePointCount java function ...
exprt add_axioms_for_offset_by_code_point(const function_application_exprt &f)
add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function...
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
string_exprt add_axioms_from_double(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(D) java function
string_exprt add_axioms_for_insert_long(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(J) java function
The trinary if-then-else operator.
equal_exprt axiom_for_has_same_length_as(const string_exprt &rhs) const
string_exprt add_axioms_from_long(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(J) java function
string_exprt add_axioms_for_trim(const function_application_exprt &expr)
add axioms corresponding to the String.trim java function
A constant literal expression.
exprt add_axioms_for_is_empty(const function_application_exprt &f)
add axioms stating that the returned value is true exactly when the argument string is empty ...
string_exprt add_axioms_for_empty_string(const function_application_exprt &f)
add axioms to say that the returned string expression is empty
string_exprt add_axioms_for_if(const if_exprt &expr)
add axioms for an if expression which should return a string
const array_typet & get_content_type() const
string_exprt add_axioms_for_concat_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(F) java function
exprt add_axioms_for_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
add axioms that the returned value is either -1 or greater than from_index and the character at that ...
exprt add_axioms_for_last_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
Extract member of struct or union.
exprt add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms...
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
string_exprt add_axioms_for_insert_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(D) java function
std::map< irep_idt, string_exprt > symbol_to_string
string_exprt fresh_string(const refined_string_typet &type)
construct a string expression whose length and content are new variables
string_exprt add_axioms_for_char_set(const function_application_exprt &expr)
add axioms corresponding stating that the result is similar to that of the StringBuilder.setCharAt java function Warning: this may be underspecified in the case wher the index exceed the length of the string
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
static bool is_unrefined_string_type(const typet &type)
string_exprt add_axioms_for_concat_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(Z) java function
const exprt & length() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
exprt add_axioms_for_hash_code(const function_application_exprt &f)
add axioms stating that if two strings are equal then their hash codes are equals ...
string_exprt add_axioms_from_float(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(F) java function
exprt::operandst argumentst
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
string_exprt add_axioms_for_value_of(const function_application_exprt &f)
add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) functions ...
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
string_exprt add_axioms_for_insert_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(Z) java function
string_exprt add_axioms_for_concat(const string_exprt &s1, const string_exprt &s2)
add axioms to say that the returned string expression is equal to the concatenation of the two string...
exprt add_axioms_for_parse_int(const function_application_exprt &f)
add axioms corresponding to the Integer.parseInt java function
exprt add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false)
add axioms corresponding to the String.isSuffix java function
string_exprt find_or_add_string_of_symbol(const symbol_exprt &sym)
if a symbol represent a string is present in the symbol_to_string table, returns the corresponding st...
std::list< exprt > axioms
exprt add_axioms_for_equals_ignore_case(const function_application_exprt &f)
add axioms corresponding to the String.equalsIgnoreCase java function
string_exprt add_axioms_for_insert(const string_exprt &s1, const string_exprt &s2, const exprt &offset)
add axioms stating that the result correspond to the first string where we inserted the second one at...
exprt add_axioms_for_char_literal(const function_application_exprt &f)
add axioms stating that the returned value is equal to the argument
const typet & get_index_type() const
bitvector_typet index_type()
Various predicates over pointers in programs.
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
string_exprt add_axioms_from_char(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(C) java function
exprt add_axioms_for_to_char_array(const function_application_exprt &f)
add axioms corresponding to the String.toCharArray java function
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
void set_string_symbol_equal_to_expr(const symbol_exprt &sym, const exprt &str)
add a correspondence to make sure the symbol points to the same string as the second argument ...
string_exprt add_axioms_for_to_lower_case(const function_application_exprt &expr)
add axioms corresponding to the String.toLowerCase java function
exprt add_axioms_for_char_at(const function_application_exprt &f)
add axioms stating that the character of the string at the given position is equal to the returned va...
const string_constantt & to_string_constant(const exprt &expr)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const exprt & content() const
string_exprt add_axioms_for_to_upper_case(const function_application_exprt &expr)
add axioms corresponding to the String.toUpperCase java function
irep_idt get_object_name() const
bool is_ssa_expr(const exprt &expr)
string_exprt add_axioms_for_set_length(const function_application_exprt &f)
add axioms to say that the returned string expression has length given by the second argument and who...
std::list< symbol_exprt > index_symbols
exprt add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
string_exprt add_axioms_from_int(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(I) java function
string_exprt add_axioms_for_replace(const function_application_exprt &f)
add axioms corresponding to the String.replace java function
Expression to hold a symbol (variable)
string_exprt add_axioms_from_int_hex(const exprt &i, const refined_string_typet &ref_type)
add axioms stating that the returned string corresponds to the integer argument written in hexadecima...
string_exprt add_axioms_for_concat_long(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.append(J) java function.
string_exprt add_axioms_for_concat_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(C) java function
static unsigned next_symbol_id
const irep_idt & get_value() const
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
bitvector_typet char_type()
string_exprt add_axioms_for_insert_char_array(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert:(I[CII) and StringBuilder.insert:(I[C) java func...
string_exprt add_axioms_from_char_array(const function_application_exprt &f)
add axioms corresponding to the String.
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive
string_exprt add_axioms_for_substring(const string_exprt &str, const exprt &start, const exprt &end)
add axioms stating that the returned string expression is equal to the input one starting at start an...