Go to the documentation of this file.
40 if(type.
id() == ID_struct_tag)
42 else if(type.
id() == ID_struct)
53 const typet &type,
const std::string &tag)
63 if(type.
id()==ID_pointer)
94 if(type.
id()==ID_pointer)
117 if(type.
id()==ID_pointer)
140 if(type.
id()==ID_pointer)
163 if(type.
id()==ID_pointer)
182 std::vector<irep_idt>
189 std::vector<irep_idt> bases;
191 if(class_name !=
"java.lang.CharSequence")
193 bases.push_back(
"java.io.Serializable");
194 bases.push_back(
"java.lang.CharSequence");
196 if(class_name ==
"java.lang.String")
197 bases.push_back(
"java.lang.Comparable");
199 if(class_name ==
"java.lang.StringBuilder" ||
200 class_name ==
"java.lang.StringBuffer")
201 bases.push_back(
"java.lang.AbstractStringBuilder");
213 string_type.
set_tag(class_name);
216 string_type.
components()[0].set_name(
"@java.lang.Object");
217 string_type.
components()[0].set_pretty_name(
"@java.lang.Object");
220 string_type.
components()[1].set_name(
"length");
221 string_type.
components()[1].set_pretty_name(
"length");
224 string_type.
components()[2].set_pretty_name(
"data");
230 for(
const irep_idt &base_name : bases)
235 symbolt *string_symbol=
nullptr;
236 symbol_table.
move(tmp_string_symbol, string_symbol);
239 string_symbol->
type=string_type;
241 string_symbol->
mode = ID_java;
260 for(
const auto &p : params)
261 ops.emplace_back(
symbol_exprt(p.get_identifier(), p.type()));
282 const exprt &expr_to_process,
292 string_expr, expr_to_process,
loc, symbol_table, init_code);
317 for(
const auto &p : operands)
324 p,
loc, symbol_table, function_id, init_code));
343 if(type.
id() == ID_struct_tag)
363 if(type.
id() == ID_struct_tag)
403 const exprt &array_pointer,
414 array_data.
type(),
"char_array",
loc, function_id, symbol_table);
427 string_expr.
content(), inf_array, symbol_table,
loc, function_id, code);
465 index_type,
"cprover_string_length",
loc, function_id, symbol_table);
469 array_type,
"cprover_string_content",
loc, function_id, symbol_table);
496 const exprt nondet_array_expr =
503 array_pointer, nondet_array_expr, symbol_table,
loc, function_id, code);
506 nondet_array_expr, str.
length(), symbol_table,
loc, function_id, code);
557 function_id, arguments, lhs.
type(), symbol_table));
595 "nondet_infinite_array_pointer",
606 return std::move(
data);
618 const exprt &pointer,
634 ID_cprover_associate_array_to_pointer_func,
663 ID_cprover_associate_length_to_array_func,
681 const exprt &pointer,
698 ID_cprover_string_constrain_characters_func,
699 {length, pointer, char_set_expr},
730 std::string(
"return_code_") + function_id.
c_str(),
734 const auto return_code = return_code_sym.
symbol_expr();
742 args.push_back(string_expr.
length());
743 args.push_back(string_expr.
content());
744 args.insert(args.end(), arguments.begin(), arguments.end());
749 return_code, function_id, args, symbol_table),
769 const exprt &rhs_array,
770 const exprt &rhs_length,
845 rhs_length.set(ID_mode, ID_java);
865 const std::string &s,
871 ID_cprover_string_literal_func,
894 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
910 std::vector<exprt> condition_list;
911 std::vector<refined_string_exprt> string_expr_list;
916 ID_cprover_string_of_float_scientific_notation_func,
921 string_expr_list.push_back(sci_notation);
928 ID_cprover_string_concat_func,
929 {minus_sign, sci_notation},
933 string_expr_list.push_back(neg_sci_notation);
939 string_expr_list.push_back(nan);
946 string_expr_list.push_back(infinity);
952 string_expr_list.push_back(minus_infinity);
960 string_expr_list.push_back(zero_string);
968 string_expr_list.push_back(minus_zero_string);
982 condition_list.push_back(is_simple_float);
985 ID_cprover_string_of_float_func, {arg},
loc, symbol_table, code);
986 string_expr_list.push_back(simple_notation);
992 condition_list.push_back(is_neg_simple_float);
995 ID_cprover_string_concat_func,
996 {minus_sign, simple_notation},
1000 string_expr_list.push_back(neg_simple_notation);
1004 string_expr_list.size()==condition_list.size(),
1005 "number of created strings should correspond to number of conditions");
1010 str, string_expr_list[0], symbol_table,
true);
1011 for(std::size_t i=1; i<condition_list.size(); i++)
1016 str, string_expr_list[i], symbol_table,
true),
1053 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1055 params.erase(params.begin());
1098 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1119 function_id, type,
loc, symbol_table,
false);
1142 const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1153 ID_cprover_string_literal_func,
1162 ID_cprover_string_substring_func,
1171 string_ptr_type,
loc, function_id, symbol_table, code);
1174 string1, string_expr1, symbol_table,
true),
1203 function_id, args, type.
return_type(), symbol_table),
1244 str, string_expr, symbol_table,
true),
1284 string_expr, arg0,
loc, symbol_table, code);
1291 str, string_expr, symbol_table,
true),
1332 string_expr, arg1,
loc, symbol_table, code);
1338 arg_this, string_expr, symbol_table,
true),
1378 if(map->count(function_id) != 0)
1384 template <
typename TMap,
typename TContainer>
1388 std::is_same<
typename TMap::key_type,
1389 typename TContainer::value_type>::value,
1390 "TContainer value_type doesn't match TMap key_type");
1394 std::inserter(container, container.begin()),
1395 [](
const typename TMap::value_type &pair) { return pair.first; });
1399 std::unordered_set<irep_idt> &methods)
const
1427 it_id->second, type,
loc, symbol_table);
1432 it_id->second, type,
loc, symbol_table);
1437 it_id->second, type,
loc, symbol_table);
1442 it_id->second, type,
loc, symbol_table);
1448 return it->second(type,
loc, function_id, symbol_table);
1463 string_types = std::unordered_set<irep_idt>{
"java.lang.String",
1464 "java.lang.StringBuilder",
1465 "java.lang.CharSequence",
1466 "java.lang.StringBuffer"};
1481 [
"java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1482 "lang/CharSequence;II)"
1483 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1487 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1488 ID_cprover_string_char_at_func;
1490 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1491 ID_cprover_string_char_at_func;
1493 [
"java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1494 ID_cprover_string_code_point_at_func;
1496 [
"java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1497 ID_cprover_string_code_point_before_func;
1499 [
"java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1500 ID_cprover_string_code_point_count_func;
1502 [
"java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1503 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1505 [
"java::org.cprover.CProverString.delete:(Ljava/lang/"
1506 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1507 ID_cprover_string_delete_func;
1509 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1510 "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1511 ID_cprover_string_delete_char_at_func;
1513 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1514 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1515 ID_cprover_string_delete_char_at_func;
1517 std::string format_signature =
"java::org.cprover.CProverString.format:(";
1519 format_signature +=
"Ljava/lang/String;";
1520 format_signature +=
")Ljava/lang/String;";
1522 ID_cprover_string_format_func;
1525 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1526 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1528 [
"java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1529 "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1531 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1532 "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1534 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1535 "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1537 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1538 ID_cprover_string_set_length_func;
1540 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/"
1541 "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1543 [
"java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1544 "lang/CharSequence;"] = ID_cprover_string_substring_func;
1548 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1549 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1551 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1552 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1554 [
"java::org.cprover.CProverString.substring:(Ljava/Lang/"
1555 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1557 [
"java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1558 ID_cprover_string_of_int_func;
1560 [
"java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1561 ID_cprover_string_of_int_func;
1563 [
"java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1564 ID_cprover_string_of_long_func;
1566 [
"java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1567 ID_cprover_string_of_long_func;
1569 [
"java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1573 std::placeholders::_1,
1574 std::placeholders::_2,
1575 std::placeholders::_3,
1576 std::placeholders::_4);
1578 [
"java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1579 ID_cprover_string_parse_int_func;
1581 [
"java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1582 ID_cprover_string_parse_int_func;
1589 std::placeholders::_1,
1590 std::placeholders::_2,
1591 std::placeholders::_3,
1592 std::placeholders::_4);
1594 [
"java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1597 std::placeholders::_1,
1598 std::placeholders::_2,
1599 std::placeholders::_3,
1600 std::placeholders::_4);
1602 [
"java::java.lang.String.<init>:()V"]=
1603 ID_cprover_string_empty_string_func;
1606 [
"java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1607 ID_cprover_string_compare_to_func;
1609 [
"java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1610 ID_cprover_string_concat_func;
1612 [
"java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1613 ID_cprover_string_contains_func;
1615 [
"java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1616 ID_cprover_string_endswith_func;
1618 [
"java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1619 ID_cprover_string_equals_ignore_case_func;
1622 [
"java::java.lang.String.indexOf:(I)I"]=
1623 ID_cprover_string_index_of_func;
1625 [
"java::java.lang.String.indexOf:(II)I"]=
1626 ID_cprover_string_index_of_func;
1628 [
"java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1629 ID_cprover_string_index_of_func;
1631 [
"java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1632 ID_cprover_string_index_of_func;
1634 [
"java::java.lang.String.isEmpty:()Z"]=
1635 ID_cprover_string_is_empty_func;
1637 [
"java::java.lang.String.lastIndexOf:(I)I"]=
1638 ID_cprover_string_last_index_of_func;
1640 [
"java::java.lang.String.lastIndexOf:(II)I"]=
1641 ID_cprover_string_last_index_of_func;
1643 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1644 ID_cprover_string_last_index_of_func;
1646 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1647 ID_cprover_string_last_index_of_func;
1651 std::placeholders::_1,
1652 std::placeholders::_2,
1653 std::placeholders::_3,
1654 std::placeholders::_4);
1656 [
"java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1657 ID_cprover_string_replace_func;
1659 [
"java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]=
1660 ID_cprover_string_replace_func;
1662 [
"java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1663 ID_cprover_string_startswith_func;
1665 [
"java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1666 ID_cprover_string_startswith_func;
1668 [
"java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1669 ID_cprover_string_to_lower_case_func;
1674 std::placeholders::_1,
1675 std::placeholders::_2,
1676 std::placeholders::_3,
1677 std::placeholders::_4);
1679 [
"java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1680 ID_cprover_string_to_upper_case_func;
1682 [
"java::java.lang.String.trim:()Ljava/lang/String;"]=
1683 ID_cprover_string_trim_func;
1687 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1690 std::placeholders::_1,
1691 std::placeholders::_2,
1692 std::placeholders::_3,
1693 std::placeholders::_4);
1695 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1699 std::placeholders::_1,
1700 std::placeholders::_2,
1701 std::placeholders::_3,
1702 std::placeholders::_4);
1704 [
"java::java.lang.StringBuilder.<init>:()V"]=
1705 ID_cprover_string_empty_string_func;
1707 [
"java::java.lang.StringBuilder.<init>:(I)V"] =
1708 ID_cprover_string_empty_string_func;
1711 [
"java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1712 ID_cprover_string_concat_char_func;
1714 [
"java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1715 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1717 [
"java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1718 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1720 [
"java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1721 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1723 [
"java::java.lang.StringBuilder.appendCodePoint:(I)"
1724 "Ljava/lang/StringBuilder;"]=
1725 ID_cprover_string_concat_code_point_func;
1727 [
"java::java.lang.StringBuilder.charAt:(I)C"]=
1728 ID_cprover_string_char_at_func;
1730 [
"java::java.lang.StringBuilder.codePointAt:(I)I"]=
1731 ID_cprover_string_code_point_at_func;
1733 [
"java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1734 ID_cprover_string_code_point_before_func;
1736 [
"java::java.lang.StringBuilder.codePointCount:(II)I"]=
1737 ID_cprover_string_code_point_count_func;
1741 std::placeholders::_1,
1742 std::placeholders::_2,
1743 std::placeholders::_3,
1744 std::placeholders::_4);
1746 [
"java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1747 ID_cprover_string_substring_func;
1749 [
"java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1750 ID_cprover_string_substring_func;
1752 [
"java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1755 std::placeholders::_1,
1756 std::placeholders::_2,
1757 std::placeholders::_3,
1758 std::placeholders::_4);
1762 [
"java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1765 std::placeholders::_1,
1766 std::placeholders::_2,
1767 std::placeholders::_3,
1768 std::placeholders::_4);
1770 [
"java::java.lang.StringBuffer.<init>:()V"]=
1771 ID_cprover_string_empty_string_func;
1774 [
"java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1775 ID_cprover_string_concat_char_func;
1777 [
"java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1778 "Ljava/lang/StringBuffer;"]=
1779 ID_cprover_string_concat_func;
1781 [
"java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1782 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1784 [
"java::java.lang.StringBuffer.appendCodePoint:(I)"
1785 "Ljava/lang/StringBuffer;"]=
1786 ID_cprover_string_concat_code_point_func;
1788 [
"java::java.lang.StringBuffer.codePointAt:(I)I"]=
1789 ID_cprover_string_code_point_at_func;
1791 [
"java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1792 ID_cprover_string_code_point_before_func;
1794 [
"java::java.lang.StringBuffer.codePointCount:(II)I"]=
1795 ID_cprover_string_code_point_count_func;
1797 [
"java::java.lang.StringBuffer.length:()I"]=
1800 [
"java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1801 ID_cprover_string_substring_func;
1803 [
"java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1806 std::placeholders::_1,
1807 std::placeholders::_2,
1808 std::placeholders::_3,
1809 std::placeholders::_4);
1813 [
"java::java.lang.CharSequence.charAt:(I)C"]=
1814 ID_cprover_string_char_at_func;
1816 [
"java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1819 std::placeholders::_1,
1820 std::placeholders::_2,
1821 std::placeholders::_3,
1822 std::placeholders::_4);
1824 [
"java::java.lang.CharSequence.length:()I"]=
1829 [
"java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1830 ID_cprover_string_of_int_hex_func;
1832 "Ljava/lang/Object;)Ljava/lang/String;"] =
1836 std::placeholders::_1,
1837 std::placeholders::_2,
1838 std::placeholders::_3,
1839 std::placeholders::_4);
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.
const irep_idt & get_identifier() const
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.
exprt::operandst process_parameters(const java_method_typet::parameterst ¶ms, 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.
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
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.
std::unordered_map< irep_idt, irep_idt > id_mapt
id_mapt cprover_equivalent_to_java_assign_and_return_function
A codet representing sequential composition of program statements.
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
const char * c_str() const
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & subtype() const
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
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...
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
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...
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< parametert > parameterst
typet type
Type of symbol.
Operator to dereference a pointer.
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...
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
The trinary if-then-else operator.
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &range, symbol_table_baset &symbol_table)
Create a (mathematical) function application expression.
void add_base(const struct_tag_typet &base)
Add a base class/struct.
A codet representing the declaration of a local variable.
id_mapt cprover_equivalent_to_java_function
id_mapt cprover_equivalent_to_java_string_returning_function
void change_spec(const ieee_float_spect &dest_spec)
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.
id_mapt cprover_equivalent_to_java_constructor
const typet & component_type(const irep_idt &component_name) const
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.
Base class for all expressions.
bool implements_function(const irep_idt &function_id) const
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.
irep_idt base_name
Base (non-scoped) name.
A struct tag type, i.e., struct_typet with an identifier.
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.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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)
Used to provide our own implementation of the CProver.classIdentifier() function.
void initialize_known_type_table()
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_char_sequence_pointer_type(const typet &type)
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.
Expression to hold a symbol (variable)
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)
static bool is_java_string_builder_type(const typet &type)
void from_float(const float f)
static typet string_length_type()
codet representation of an if-then-else statement.
An expression denoting infinity.
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...
const exprt & length() const
irep_idt pretty_name
Language-specific display name.
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.
Struct constructor from list of elements.
const exprt & size() const
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
irep_idt mode
Language mode.
std::unordered_map< irep_idt, conversion_functiont > conversion_table
The null pointer constant.
const std::string & id2string(const irep_idt &d)
void set_tag(const irep_idt &tag)
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.
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.
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
The symbol table base class interface.
An assumption, which must hold in subsequent code.
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
static bool is_java_char_array_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...
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
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...
pointer_typet pointer_type(const typet &subtype)
id_mapt cprover_equivalent_to_java_assign_function
The unary minus expression.
static bool is_java_char_sequence_type(const typet &type)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< exprt > operandst
void add(const codet &code)
signedbv_typet java_int_type()
const parameterst & parameters() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
static const typet & get_length_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the length component.
static bool java_type_matches_tag(const typet &type, const std::string &tag)
character_refine_preprocesst character_preprocess
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
A side_effect_exprt that returns a non-deterministically chosen value.
static bool is_java_char_array_pointer_type(const typet &type)
Extract member of struct or union.
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.
static bool is_java_string_buffer_type(const typet &type)
const componentst & components() const
const exprt & content() const
void set_access(const irep_idt &access)
Structure type, corresponds to C style structs.
codet representation of a "return from a function" statement.
const refined_string_typet refined_string_type
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.
static bool is_java_string_buffer_pointer_type(const typet &type)
const std::array< id_mapt *, 5 > id_maps
Evaluates to true if the operand is infinite.
source_locationt location
Source code location of definition of symbol.
static bool implements_java_char_sequence_pointer(const typet &type)
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
unsignedbv_typet java_char_type()
A base class for relations, i.e., binary predicates whose two operands have the same type.
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
const irep_idt & get_identifier() const
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
static codet code_assign_function_application(const exprt &lhs, const irep_idt &function_id, const exprt::operandst &arguments, symbol_table_baset &symbol_table)
assign the result of a function call
code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
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
const typet & return_type() const
exprt allocate_dynamic_object(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generate the same code as allocate_dynamic_object_symbol, but return a dereference_exprt that derefer...
constant_exprt to_expr() const
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
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
static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
access length member
Operator to return the address of an object.
source_locationt & add_source_location()
const java_method_typet & to_java_method_type(const typet &type)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
static bool is_constructor(const irep_idt &method_name)
A codet representing an assignment in the program.
static bool is_java_string_pointer_type(const typet &type)
A constant literal expression.
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.
std::unordered_set< irep_idt > string_types
static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
access data member
irep_idt name
The unique identifier.
void add_keys_to_container(const TMap &map, TContainer &container)
static bool is_java_string_type(const typet &type)
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...
static bool is_java_string_builder_pointer_type(const typet &type)
Evaluates to true if the operand is NaN.
static const typet & get_data_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the data component.
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
Data structure for representing an arbitrary statement in a program.
static irep_idt get_tag(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