cprover
Loading...
Searching...
No Matches
java_string_library_preprocess.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java_string_libraries_preprocess, gives code for methods on
4 strings of the java standard library. In particular methods
5 from java.lang.String, java.lang.StringBuilder,
6 java.lang.StringBuffer.
7
8Author: Romain Brenguier
9
10Date: April 2017
11
12\*******************************************************************/
13
18
20
21#include <util/arith_tools.h>
22#include <util/bitvector_expr.h>
23#include <util/c_types.h>
25#include <util/floatbv_expr.h>
26#include <util/ieee_float.h>
28#include <util/std_code.h>
29#include <util/string_expr.h>
31
34
35#include "java_types.h"
36#include "java_utils.h"
37
40static irep_idt get_tag(const typet &type)
41{
43 if(type.id() == ID_struct_tag)
44 return to_struct_tag_type(type).get_identifier();
45 else if(type.id() == ID_struct)
46 return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
47 else
48 return irep_idt();
49}
50
56 const typet &type, const std::string &tag)
57{
58 return irep_idt("java::" + tag) == get_tag(type);
59}
60
64 const typet &type)
65{
66 if(type.id()==ID_pointer)
67 {
68 const pointer_typet &pt=to_pointer_type(type);
69 const typet &base_type = pt.base_type();
70 return is_java_string_type(base_type);
71 }
72 return false;
73}
74
78 const typet &type)
79{
80 return java_type_matches_tag(type, "java.lang.String");
81}
82
86 const typet &type)
87{
88 return java_type_matches_tag(type, "java.lang.StringBuilder");
89}
90
95 const typet &type)
96{
97 if(type.id()==ID_pointer)
98 {
99 const pointer_typet &pt=to_pointer_type(type);
100 const typet &base_type = pt.base_type();
101 return is_java_string_builder_type(base_type);
102 }
103 return false;
104}
105
109 const typet &type)
110{
111 return java_type_matches_tag(type, "java.lang.StringBuffer");
112}
113
118 const typet &type)
119{
120 if(type.id()==ID_pointer)
121 {
122 const pointer_typet &pt=to_pointer_type(type);
123 const typet &base_type = pt.base_type();
124 return is_java_string_buffer_type(base_type);
125 }
126 return false;
127}
128
132 const typet &type)
133{
134 return java_type_matches_tag(type, "java.lang.CharSequence");
135}
136
141 const typet &type)
142{
143 if(type.id()==ID_pointer)
144 {
145 const pointer_typet &pt=to_pointer_type(type);
146 const typet &base_type = pt.base_type();
147 return is_java_char_sequence_type(base_type);
148 }
149 return false;
150}
151
155 const typet &type)
156{
157 return java_type_matches_tag(type, "array[char]");
158}
159
164 const typet &type)
165{
166 if(type.id()==ID_pointer)
167 {
168 const pointer_typet &pt=to_pointer_type(type);
169 const typet &base_type = pt.base_type();
170 return is_java_char_array_type(base_type);
171 }
172 return false;
173}
174
177{
178 return java_int_type();
179}
180
185std::vector<irep_idt>
187 const irep_idt &class_name)
188{
189 if(!is_known_string_type(class_name))
190 return {};
191
192 std::vector<irep_idt> bases;
193 bases.reserve(3);
194
195 // StringBuilder and StringBuffer derive from AbstractStringBuilder;
196 // other String types (String and CharSequence) derive directly from Object.
197 if(
198 class_name == "java.lang.StringBuilder" ||
199 class_name == "java.lang.StringBuffer")
200 bases.push_back("java.lang.AbstractStringBuilder");
201 else
202 bases.push_back("java.lang.Object");
203
204 // Interfaces:
205 if(class_name != "java.lang.CharSequence")
206 {
207 bases.push_back("java.io.Serializable");
208 bases.push_back("java.lang.CharSequence");
209 }
210 if(class_name == "java.lang.String")
211 bases.push_back("java.lang.Comparable");
212
213 return bases;
214}
215
220 const irep_idt &class_name,
221 symbol_table_baset &symbol_table)
222{
223 irep_idt class_symbol_name = "java::" + id2string(class_name);
225 symbolt *string_symbol = nullptr;
227
229 {
230 // A library has already defined this type -- we'll replace its
231 // components with those required for internal string modelling, but
232 // otherwise leave it alone.
233 to_java_class_type(string_symbol->type).components().clear();
234 }
235 else
236 {
237 // No definition of this type exists -- define it as it usually occurs in
238 // the JDK:
240 new_string_type.set_tag(class_name);
242 new_string_type.set_access(ID_public);
243
244 std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
245 for(const irep_idt &base_name : bases)
246 new_string_type.add_base(
247 struct_tag_typet("java::" + id2string(base_name)));
248
249 string_symbol->base_name = id2string(class_name);
250 string_symbol->pretty_name = id2string(class_name);
252 }
253
255
256 string_type.components().resize(3);
257 const struct_tag_typet &supertype = string_type.bases().front().type();
259 "@" + id2string(supertype.get_identifier()).substr(6);
260 string_type.components()[0].set_name(supertype_component_name);
261 string_type.components()[0].set_pretty_name(supertype_component_name);
262 string_type.components()[0].type() = supertype;
263 string_type.components()[1].set_name("length");
264 string_type.components()[1].set_pretty_name("length");
265 string_type.components()[1].type()=string_length_type();
266 string_type.components()[2].set_name("data");
267 string_type.components()[2].set_pretty_name("data");
268 string_type.components()[2].type() = pointer_type(java_char_type());
269}
270
280 const java_method_typet::parameterst &params,
281 const source_locationt &loc,
282 const irep_idt &function_id,
283 symbol_table_baset &symbol_table,
285{
287 for(const auto &p : params)
288 ops.emplace_back(symbol_exprt(p.get_identifier(), p.type()));
289 return process_operands(ops, loc, function_id, symbol_table, init_code);
290}
291
322
337 const exprt::operandst &operands,
338 const source_locationt &loc,
339 const irep_idt &function_id,
340 symbol_table_baset &symbol_table,
342{
344 for(const auto &p : operands)
345 {
347 {
351 p, loc, symbol_table, function_id, init_code));
352 }
353 else if(is_java_char_array_pointer_type(p.type()))
354 ops.push_back(
355 replace_char_array(p, loc, function_id, symbol_table, init_code));
356 else
357 ops.push_back(p);
358 }
359 return ops;
360}
361
366static const typet &
367get_data_type(const typet &type, const symbol_table_baset &symbol_table)
368{
369 PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
370 if(type.id() == ID_struct_tag)
371 {
372 const symbolt &sym =
373 symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
374 CHECK_RETURN(sym.type.id() != ID_struct_tag);
375 return get_data_type(sym.type, symbol_table);
376 }
377 // else type id is ID_struct
379 return struct_type.component_type("data");
380}
381
386static const typet &
387get_length_type(const typet &type, const symbol_table_baset &symbol_table)
388{
389 PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
390 if(type.id() == ID_struct_tag)
391 {
392 const symbolt &sym =
393 symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
394 CHECK_RETURN(sym.type.id() != ID_struct_tag);
395 return get_length_type(sym.type, symbol_table);
396 }
397 // else type id is ID_struct
399 return struct_type.component_type("length");
400}
401
406static exprt
407get_length(const exprt &expr, const symbol_table_baset &symbol_table)
408{
409 return member_exprt(
410 expr, "length", get_length_type(expr.type(), symbol_table));
411}
412
417static exprt get_data(const exprt &expr, const symbol_table_baset &symbol_table)
418{
419 return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
420}
421
431 const exprt &array_pointer,
432 const source_locationt &loc,
433 const irep_idt &function_id,
434 symbol_table_baset &symbol_table,
435 code_blockt &code)
436{
437 // array is *array_pointer
439 // array_data is array_pointer-> data
440 const exprt array_data = get_data(array, symbol_table);
442 array_data.type(), "char_array", loc, function_id, symbol_table);
443 const symbol_exprt char_array = sym_char_array.symbol_expr();
444 // char_array = array_pointer->data
446
447 // string_expr is `{ rhs->length; string_array }`
449 get_length(array, symbol_table), char_array, refined_string_type);
450
453
455 string_expr.content(), inf_array, symbol_table, loc, function_id, code);
456
457 return string_expr;
458}
459
468 const typet &type,
469 const source_locationt &loc,
470 const irep_idt &function_id,
471 symbol_table_baset &symbol_table)
472{
474 fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
475 string_symbol.is_static_lifetime=true;
476 return string_symbol.symbol_expr();
477}
478
487 const source_locationt &loc,
488 const irep_idt &function_id,
489 symbol_table_baset &symbol_table,
490 code_blockt &code)
491{
493 index_type, "cprover_string_length", loc, function_id, symbol_table);
494 const symbol_exprt length_field = sym_length.symbol_expr();
497 array_type, "cprover_string_content", loc, function_id, symbol_table);
498 const symbol_exprt content_field = sym_content.symbol_expr();
499 code.add(code_declt(content_field), loc);
500 code.add(code_declt{length_field}, loc);
502}
503
512 const source_locationt &loc,
513 const irep_idt &function_id,
514 symbol_table_baset &symbol_table,
515 code_blockt &code)
516{
518 const refined_string_exprt str =
519 decl_string_expr(loc, function_id, symbol_table, code);
520
521 const side_effect_expr_nondett nondet_length(str.length().type(), loc);
522 code.add(code_assignt(str.length(), nondet_length), loc);
523
525 make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
526
529
531 array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
532
534 nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
535
536 code.add(code_assignt(str.content(), array_pointer), loc);
537
538 return refined_string_exprt(str.length(), str.content());
539}
540
549 const typet &type,
550 const source_locationt &loc,
551 const irep_idt &function_id,
552 symbol_table_baset &symbol_table,
553 code_blockt &code)
554{
555 const exprt str = fresh_string(type, loc, function_id, symbol_table);
556
557 allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
558
560 allocate_objects.allocate_dynamic_object(
561 tmp, str, to_reference_type(str.type()).base_type());
562 allocate_objects.declare_created_symbols(code);
563 code.append(tmp);
564
565 return str;
566}
567
578 const exprt &lhs,
579 const irep_idt &function_id,
580 const exprt::operandst &arguments,
581 symbol_table_baset &symbol_table)
582{
583 return code_assignt(
584 lhs,
586 function_id, arguments, lhs.type(), symbol_table));
587}
588
599 const irep_idt &function_id,
600 const exprt::operandst &arguments,
601 const typet &type,
602 symbol_table_baset &symbol_table)
603{
604 return code_returnt(
605 make_function_application(function_id, arguments, type, symbol_table));
606}
607
615 symbol_table_baset &symbol_table,
616 const source_locationt &loc,
617 const irep_idt &function_id,
618 code_blockt &code)
619{
624 "nondet_infinite_array_pointer",
625 loc,
626 function_id,
627 symbol_table);
628
629 const symbol_exprt data_pointer = data_sym.symbol_expr();
634 code.add(code_assignt{data, std::move(nondet_data)}, loc);
635 return std::move(data);
636}
637
647 const exprt &pointer,
648 const exprt &array,
649 symbol_table_baset &symbol_table,
650 const source_locationt &loc,
651 const irep_idt &function_id,
652 code_blockt &code)
653{
654 PRECONDITION(array.type().id() == ID_array);
655 PRECONDITION(pointer.type().id() == ID_pointer);
657 java_int_type(), "return_array", loc, function_id, symbol_table);
658 const auto return_expr = return_sym.symbol_expr();
659 code.add(code_declt(return_expr), loc);
660 code.add(
664 {array, pointer},
665 symbol_table),
666 loc);
667}
668
678 const exprt &array,
679 const exprt &length,
680 symbol_table_baset &symbol_table,
681 const source_locationt &loc,
682 const irep_idt &function_id,
683 code_blockt &code)
684{
686 java_int_type(), "return_array", loc, function_id, symbol_table);
687 const auto return_expr = return_sym.symbol_expr();
688 code.add(code_declt(return_expr), loc);
689 code.add(
693 {array, length},
694 symbol_table),
695 loc);
696}
697
710 const exprt &pointer,
711 const exprt &length,
712 const irep_idt &char_range,
713 symbol_table_baset &symbol_table,
714 const source_locationt &loc,
715 const irep_idt &function_id,
716 code_blockt &code)
717{
718 PRECONDITION(pointer.type().id() == ID_pointer);
720 java_int_type(), "cnstr_added", loc, function_id, symbol_table);
721 const auto return_expr = return_sym.symbol_expr();
722 code.add(code_declt(return_expr), loc);
724 code.add(
728 {length, pointer, char_set_expr},
729 symbol_table),
730 loc);
731}
732
750 const irep_idt &function_id,
751 const exprt::operandst &arguments,
752 const source_locationt &loc,
753 symbol_table_baset &symbol_table,
754 code_blockt &code)
755{
756 // int return_code;
759 std::string("return_code_") + function_id.c_str(),
760 loc,
761 function_id,
762 symbol_table);
763 const auto return_code = return_code_sym.symbol_expr();
764 code.add(code_declt(return_code), loc);
765
767 make_nondet_string_expr(loc, function_id, symbol_table, code);
768
769 // args is { str.length, str.content, arguments... }
770 exprt::operandst args;
771 args.push_back(string_expr.length());
772 args.push_back(string_expr.content());
773 args.insert(args.end(), arguments.begin(), arguments.end());
774
775 // return_code = <function_id>_data(args)
776 code.add(
778 return_code, function_id, args, symbol_table),
779 loc);
780
781 return string_expr;
782}
783
797 const exprt &lhs,
798 const exprt &rhs_array,
799 const exprt &rhs_length,
800 const symbol_table_baset &symbol_table,
801 bool is_constructor)
802{
805
807 {
808 // Initialise the supertype with the appropriate classid:
809 namespacet ns(symbol_table);
810 const struct_typet &lhs_type = to_struct_type(ns.follow(deref.type()));
812 lhs_type.components().front().type(), source_locationt{}, ns);
818 }
819 else
820 {
821 return code_blockt(
822 {code_assignt(get_length(deref, symbol_table), rhs_length),
823 code_assignt(get_data(deref, symbol_table), rhs_array)});
824 }
825}
826
839 const exprt &lhs,
840 const refined_string_exprt &rhs,
841 const symbol_table_baset &symbol_table,
842 bool is_constructor)
843{
845 lhs, rhs.content(), rhs.length(), symbol_table, is_constructor);
846}
847
858 const refined_string_exprt &lhs,
859 const exprt &rhs,
860 const source_locationt &loc,
861 const symbol_table_baset &symbol_table,
862 code_blockt &code)
863{
865
867
868 // Although we should not reach this code if rhs is null, the association
869 // `pointer -> length` is added to the solver anyway, so we have to make sure
870 // the length is set to something reasonable.
871 auto rhs_length = if_exprt(
873 from_integer(0, lhs.length().type()),
874 get_length(deref, symbol_table));
876
877 // Assignments
878 code.add(code_assignt(lhs.length(), rhs_length), loc);
879 exprt data_as_array = get_data(deref, symbol_table);
880 code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc);
881}
882
895 const std::string &s,
896 const source_locationt &loc,
897 symbol_table_baset &symbol_table,
898 code_blockt &code)
899{
903 loc,
904 symbol_table,
905 code);
906}
907
916 const java_method_typet &type,
917 const source_locationt &loc,
918 const irep_idt &function_id,
919 symbol_table_baset &symbol_table,
920 message_handlert &message_handler)
921{
922 (void)message_handler;
923
924 // Getting the argument
926 PRECONDITION(params.size()==1);
927 PRECONDITION(!params[0].get_identifier().empty());
928 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
929
930 // Holder for output code
931 code_blockt code;
932
933 // Declaring and allocating String * str
934 const exprt str = allocate_fresh_string(
935 type.return_type(), loc, function_id, symbol_table, code);
936
937 // Expression representing 0.0
938 const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
940 zero_float.from_float(0.0);
941 const constant_exprt zero = zero_float.to_expr();
942
943 // For each possible case with have a condition and a string_exprt
944 std::vector<exprt> condition_list;
945 std::vector<refined_string_exprt> string_expr_list;
946
947 // Case of computerized scientific notation
948 condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
951 {arg},
952 loc,
953 symbol_table,
954 code);
956
957 // Subcase of negative scientific notation
958 condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
960 string_literal_to_string_expr("-", loc, symbol_table, code);
964 loc,
965 symbol_table,
966 code);
968
969 // Case of NaN
970 condition_list.push_back(isnan_exprt(arg));
972 string_literal_to_string_expr("NaN", loc, symbol_table, code);
973 string_expr_list.push_back(nan);
974
975 // Case of Infinity
976 extractbit_exprt is_neg(arg, float_spec.width()-1);
978 const refined_string_exprt infinity =
979 string_literal_to_string_expr("Infinity", loc, symbol_table, code);
980 string_expr_list.push_back(infinity);
981
982 // Case -Infinity
983 condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
984 const refined_string_exprt minus_infinity =
985 string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
986 string_expr_list.push_back(minus_infinity);
987
988 // Case of 0.0
989 // Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt,
990 // the latter disregards the sign
991 condition_list.push_back(equal_exprt(arg, zero));
993 string_literal_to_string_expr("0.0", loc, symbol_table, code);
994 string_expr_list.push_back(zero_string);
995
996 // Case of -0.0
998 minus_zero_float.from_float(-0.0f);
999 condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
1001 string_literal_to_string_expr("-0.0", loc, symbol_table, code);
1003
1004 // Case of simple notation
1007 bound_inf_float.from_float(1e-3f);
1008 bound_sup_float.from_float(1e7f);
1009 bound_inf_float.change_spec(float_spec);
1010 bound_sup_float.change_spec(float_spec);
1011 const constant_exprt bound_inf = bound_inf_float.to_expr();
1012 const constant_exprt bound_sup = bound_sup_float.to_expr();
1013
1017
1019 ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1021
1022 // Case of a negative number in simple notation
1027
1031 loc,
1032 symbol_table,
1033 code);
1035
1036 // Combining all cases
1037 INVARIANT(
1038 string_expr_list.size()==condition_list.size(),
1039 "number of created strings should correspond to number of conditions");
1040
1041 // We do not check the condition of the first element in the list as it
1042 // will be reached only if all other conditions are not satisfied.
1044 str, string_expr_list[0], symbol_table, true);
1045 for(std::size_t i=1; i<condition_list.size(); i++)
1046 {
1048 condition_list[i],
1050 str, string_expr_list[i], symbol_table, true),
1051 tmp_code);
1052 }
1053 code.add(tmp_code, loc);
1054
1055 // Return str
1056 code.add(code_returnt(str), loc);
1057 return code;
1058}
1059
1076 const irep_idt &function_id,
1077 const java_method_typet &type,
1078 const source_locationt &loc,
1079 symbol_table_baset &symbol_table,
1080 bool is_constructor)
1081{
1083
1084 // The first parameter is the object to be initialized
1085 PRECONDITION(!params.empty());
1086 PRECONDITION(!params[0].get_identifier().empty());
1087 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1088 if(is_constructor)
1089 params.erase(params.begin());
1090
1091 // Holder for output code
1092 code_blockt code;
1093
1094 // Processing parameters
1095 const exprt::operandst args =
1096 process_parameters(params, loc, function_id, symbol_table, code);
1097
1098 // string_expr <- function(arg1)
1100 string_expr_of_function(function_id, args, loc, symbol_table, code);
1101
1102 // arg_this <- string_expr
1103 code.add(
1105 arg_this, string_expr, symbol_table, is_constructor),
1106 loc);
1107
1108 return code;
1109}
1110
1120 const irep_idt &function_id,
1121 const java_method_typet &type,
1122 const source_locationt &loc,
1123 symbol_table_baset &symbol_table)
1124{
1125 // This is similar to assign functions except we return a pointer to `this`
1126 const java_method_typet::parameterst &params = type.parameters();
1127 PRECONDITION(!params.empty());
1128 PRECONDITION(!params[0].get_identifier().empty());
1129 code_blockt code;
1130 code.add(
1131 make_assign_function_from_call(function_id, type, loc, symbol_table), loc);
1132 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1133 code.add(code_returnt(arg_this), loc);
1134 return code;
1135}
1136
1145 const irep_idt &function_id,
1146 const java_method_typet &type,
1147 const source_locationt &loc,
1148 symbol_table_baset &symbol_table)
1149{
1150 // This is similar to initialization function except we do not ignore
1151 // the first argument
1153 function_id, type, loc, symbol_table, false);
1154}
1155
1169 const java_method_typet &type,
1170 const source_locationt &loc,
1171 const irep_idt &function_id,
1172 symbol_table_baset &symbol_table,
1173 message_handlert &message_handler)
1174{
1176 PRECONDITION(!params.empty());
1177 PRECONDITION(!params[0].get_identifier().empty());
1178 const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1179
1180 // Code to be returned
1181 code_blockt code;
1182
1183 // class_identifier is obj->@class_identifier
1184 const member_exprt class_identifier{
1186
1187 // string_expr = cprover_string_literal(this->@class_identifier)
1190 {class_identifier},
1191 loc,
1192 symbol_table,
1193 code);
1194
1195 // string_expr1 = substr(string_expr, 6)
1196 // We do this to remove the "java::" prefix
1200 loc,
1201 symbol_table,
1202 code);
1203
1204 // string1 = (String*) string_expr
1205 const typet &string_ptr_type = type.return_type();
1207 string_ptr_type, loc, function_id, symbol_table, code);
1208 code.add(
1210 string1, string_expr1, symbol_table, true),
1211 loc);
1212
1213 // > return string1;
1214 code.add(code_returnt{string1}, loc);
1215 return code;
1216}
1217
1229 const irep_idt &function_id,
1230 const java_method_typet &type,
1231 const source_locationt &loc,
1232 symbol_table_baset &symbol_table)
1233{
1234 code_blockt code;
1235 const exprt::operandst args =
1236 process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1237 code.add(
1239 function_id, args, type.return_type(), symbol_table),
1240 loc);
1241 return code;
1242}
1243
1259 const irep_idt &function_id,
1260 const java_method_typet &type,
1261 const source_locationt &loc,
1262 symbol_table_baset &symbol_table)
1263{
1264 // Code for the output
1265 code_blockt code;
1266
1267 // Calling the function
1268 const exprt::operandst arguments =
1269 process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1270
1271 // String expression that will hold the result
1273 string_expr_of_function(function_id, arguments, loc, symbol_table, code);
1274
1275 // Assign to string
1276 const exprt str = allocate_fresh_string(
1277 type.return_type(), loc, function_id, symbol_table, code);
1278 code.add(
1280 str, string_expr, symbol_table, true),
1281 loc);
1282
1283 // Return value
1284 code.add(code_returnt(str), loc);
1285 return code;
1286}
1287
1304 const java_method_typet &type,
1305 const source_locationt &loc,
1306 const irep_idt &function_id,
1307 symbol_table_baset &symbol_table,
1308 message_handlert &message_handler)
1309{
1310 (void)message_handler;
1311
1312 // Code for the output
1313 code_blockt code;
1314
1315 // String expression that will hold the result
1317 decl_string_expr(loc, function_id, symbol_table, code);
1318
1319 // Assign the argument to string_expr
1320 const java_method_typet::parametert &op = type.parameters()[0];
1321 PRECONDITION(!op.get_identifier().empty());
1322 const symbol_exprt arg0{op.get_identifier(), op.type()};
1324 string_expr, arg0, loc, symbol_table, code);
1325
1326 // Allocate and assign the string
1327 const exprt str = allocate_fresh_string(
1328 type.return_type(), loc, function_id, symbol_table, code);
1329 code.add(
1331 str, string_expr, symbol_table, true),
1332 loc);
1333
1334 // Return value
1335 code.add(code_returnt(str), loc);
1336 return code;
1337}
1338
1354 const java_method_typet &type,
1355 const source_locationt &loc,
1356 const irep_idt &function_id,
1357 symbol_table_baset &symbol_table,
1358 message_handlert &message_handler)
1359{
1360 (void)message_handler;
1361
1363
1364 // String expression that will hold the result
1366 decl_string_expr(loc, function_id, symbol_table, copy_constructor_body);
1367
1368 // Assign argument to a string_expr
1369 const java_method_typet::parameterst &params = type.parameters();
1370 PRECONDITION(!params[0].get_identifier().empty());
1371 PRECONDITION(!params[1].get_identifier().empty());
1372 const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
1374 string_expr, arg1, loc, symbol_table, copy_constructor_body);
1375
1376 // Assign string_expr to `this` object
1377 const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1380 arg_this, string_expr, symbol_table, true),
1381 loc);
1382
1383 return copy_constructor_body;
1384}
1385
1399 const java_method_typet &type,
1400 const source_locationt &loc,
1401 const irep_idt &function_id,
1402 symbol_table_baset &symbol_table,
1403 message_handlert &message_handler)
1404{
1405 (void)function_id;
1406 (void)message_handler;
1407
1408 const java_method_typet::parameterst &params = type.parameters();
1409 PRECONDITION(!params[0].get_identifier().empty());
1410 const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1412
1413 code_returnt ret(get_length(deref, symbol_table));
1414 ret.add_source_location() = loc;
1415
1416 return ret;
1417}
1418
1420 const irep_idt &function_id) const
1421{
1422 for(const id_mapt *map : id_maps)
1423 if(map->count(function_id) != 0)
1424 return true;
1425
1426 return conversion_table.count(function_id) != 0;
1427}
1428
1429template <typename TMap, typename TContainer>
1430void add_keys_to_container(const TMap &map, TContainer &container)
1431{
1432 static_assert(
1433 std::is_same<typename TMap::key_type,
1434 typename TContainer::value_type>::value,
1435 "TContainer value_type doesn't match TMap key_type");
1436 std::transform(
1437 map.begin(),
1438 map.end(),
1439 std::inserter(container, container.begin()),
1440 [](const typename TMap::value_type &pair) { return pair.first; });
1441}
1442
1444 std::unordered_set<irep_idt> &methods) const
1445{
1446 for(const id_mapt *map : id_maps)
1447 add_keys_to_container(*map, methods);
1448
1450}
1451
1460 const symbolt &symbol,
1461 symbol_table_baset &symbol_table,
1462 message_handlert &message_handler)
1463{
1464 const irep_idt &function_id = symbol.name;
1465 const java_method_typet &type = to_java_method_type(symbol.type);
1466 const source_locationt &loc = symbol.location;
1467 auto it_id=cprover_equivalent_to_java_function.find(function_id);
1469 return make_function_from_call(it_id->second, type, loc, symbol_table);
1470
1474 it_id->second, type, loc, symbol_table);
1475
1479 it_id->second, type, loc, symbol_table);
1480
1484 it_id->second, type, loc, symbol_table);
1485
1489 it_id->second, type, loc, symbol_table);
1490
1491 auto it=conversion_table.find(function_id);
1492 INVARIANT(
1493 it != conversion_table.end(), "Couldn't retrieve code for string method");
1494
1495 return it->second(type, loc, function_id, symbol_table, message_handler);
1496}
1497
1503 irep_idt class_name)
1504{
1505 return string_types.find(class_name)!=string_types.end();
1506}
1507
1509{
1510 string_types = std::unordered_set<irep_idt>{"java.lang.String",
1511 "java.lang.StringBuilder",
1512 "java.lang.CharSequence",
1513 "java.lang.StringBuffer"};
1514}
1515
1518{
1520
1521 // The following list of function is organized by libraries, with
1522 // constructors first and then methods in alphabetic order.
1523 // Methods that are not supported here should ultimately have Java models
1524 // provided for them in the class-path.
1525
1526 // CProverString library
1528 ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1529 "lang/CharSequence;II)"
1530 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1531 // CProverString.charAt differs from the Java String.charAt in that no
1532 // exception is raised for the out of bounds case.
1534 ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1537 ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1540 ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1543 ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1546 ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1549 ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1550 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1552 ["java::org.cprover.CProverString.delete:(Ljava/lang/"
1553 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1556 ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1557 "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1560 ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1561 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1563
1564 std::string format_signature = "java::org.cprover.CProverString.format:(";
1565 for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1566 format_signature += "Ljava/lang/String;";
1567 format_signature += ")Ljava/lang/String;";
1570
1572 ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1573 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1575 ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1578 ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1579 "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1581 ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1582 "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1584 ["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1587 ["java::org.cprover.CProverString.setLength:(Ljava/lang/"
1588 "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1590 ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1591 "lang/CharSequence;"] = ID_cprover_string_substring_func;
1592 // CProverString.substring differs from the Java String.substring in that no
1593 // exception is raised for the out of bounds case.
1595 ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1596 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1598 ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1599 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1601 ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
1602 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1604 ["java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1607 ["java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1610 ["java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1613 ["java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1616 ["java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1617 std::bind(
1619 this,
1620 std::placeholders::_1,
1621 std::placeholders::_2,
1622 std::placeholders::_3,
1623 std::placeholders::_4,
1624 std::placeholders::_5);
1626 ["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1629 ["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1632 ["java::org.cprover.CProverString.isValidInt:(Ljava/lang/String;I)Z"] =
1635 ["java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z"] =
1637
1638 // String library
1639 conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1640 std::bind(
1642 this,
1643 std::placeholders::_1,
1644 std::placeholders::_2,
1645 std::placeholders::_3,
1646 std::placeholders::_4,
1647 std::placeholders::_5);
1649 ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1651 this,
1652 std::placeholders::_1,
1653 std::placeholders::_2,
1654 std::placeholders::_3,
1655 std::placeholders::_4,
1656 std::placeholders::_5);
1658 ["java::java.lang.String.<init>:()V"]=
1660
1662 ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1665 ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1668 ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1671 ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1674 ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1676
1678 ["java::java.lang.String.indexOf:(I)I"]=
1681 ["java::java.lang.String.indexOf:(II)I"]=
1684 ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1687 ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1690 ["java::java.lang.String.isEmpty:()Z"]=
1693 ["java::java.lang.String.lastIndexOf:(I)I"]=
1696 ["java::java.lang.String.lastIndexOf:(II)I"]=
1699 ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1702 ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1704 conversion_table["java::java.lang.String.length:()I"] = std::bind(
1706 this,
1707 std::placeholders::_1,
1708 std::placeholders::_2,
1709 std::placeholders::_3,
1710 std::placeholders::_4,
1711 std::placeholders::_5);
1713 ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1716 ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
1719 ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1722 ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1725 ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1727 conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
1728 std::bind(
1730 this,
1731 std::placeholders::_1,
1732 std::placeholders::_2,
1733 std::placeholders::_3,
1734 std::placeholders::_4,
1735 std::placeholders::_5);
1737 ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1740 ["java::java.lang.String.trim:()Ljava/lang/String;"]=
1742
1743 // StringBuilder library
1745 ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1747 this,
1748 std::placeholders::_1,
1749 std::placeholders::_2,
1750 std::placeholders::_3,
1751 std::placeholders::_4,
1752 std::placeholders::_5);
1754 ["java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1755 std::bind(
1757 this,
1758 std::placeholders::_1,
1759 std::placeholders::_2,
1760 std::placeholders::_3,
1761 std::placeholders::_4,
1762 std::placeholders::_5);
1764 ["java::java.lang.StringBuilder.<init>:()V"]=
1767 ["java::java.lang.StringBuilder.<init>:(I)V"] =
1769
1771 ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1774 ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1775 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1777 ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1778 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1780 ["java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1781 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1783 ["java::java.lang.StringBuilder.appendCodePoint:(I)"
1784 "Ljava/lang/StringBuilder;"]=
1787 ["java::java.lang.StringBuilder.charAt:(I)C"]=
1790 ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
1793 ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1796 ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
1798 conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
1800 this,
1801 std::placeholders::_1,
1802 std::placeholders::_2,
1803 std::placeholders::_3,
1804 std::placeholders::_4,
1805 std::placeholders::_5);
1807 ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1810 ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1813 ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1815 this,
1816 std::placeholders::_1,
1817 std::placeholders::_2,
1818 std::placeholders::_3,
1819 std::placeholders::_4,
1820 std::placeholders::_5);
1821
1822 // StringBuffer library
1824 ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1826 this,
1827 std::placeholders::_1,
1828 std::placeholders::_2,
1829 std::placeholders::_3,
1830 std::placeholders::_4,
1831 std::placeholders::_5);
1833 ["java::java.lang.StringBuffer.<init>:()V"]=
1835
1837 ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1840 ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1841 "Ljava/lang/StringBuffer;"]=
1844 ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1845 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1847 ["java::java.lang.StringBuffer.appendCodePoint:(I)"
1848 "Ljava/lang/StringBuffer;"]=
1851 ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
1854 ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1857 ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
1860 ["java::java.lang.StringBuffer.length:()I"]=
1861 conversion_table["java::java.lang.String.length:()I"];
1863 ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1866 ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1868 this,
1869 std::placeholders::_1,
1870 std::placeholders::_2,
1871 std::placeholders::_3,
1872 std::placeholders::_4,
1873 std::placeholders::_5);
1874
1875 // CharSequence library
1877 ["java::java.lang.CharSequence.charAt:(I)C"]=
1880 ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1882 this,
1883 std::placeholders::_1,
1884 std::placeholders::_2,
1885 std::placeholders::_3,
1886 std::placeholders::_4,
1887 std::placeholders::_5);
1889 ["java::java.lang.CharSequence.length:()I"]=
1890 conversion_table["java::java.lang.String.length:()I"];
1891
1892 // Other libraries
1894 ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1897 ["java::org.cprover.CProver.classIdentifier:("
1898 "Ljava/lang/Object;)Ljava/lang/String;"] =
1899 std::bind(
1901 this,
1902 std::placeholders::_1,
1903 std::placeholders::_2,
1904 std::placeholders::_3,
1905 std::placeholders::_4,
1906 std::placeholders::_5);
1907}
code_frontend_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static std::pair< symbol_exprt, code_with_references_listt > nondet_length(allocate_objectst &allocate, source_locationt loc)
Declare a non-deterministic length expression.
API to expression classes for bitvectors.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Extract class identifier.
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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...
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Boolean AND.
Definition std_expr.h:2071
Arrays with given size.
Definition std_types.h:763
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
A goto_instruction_codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition std_code.h:217
A codet representing sequential composition of program statements.
Definition std_code.h:130
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition std_code.cpp:86
void add(const codet &code)
Definition std_code.h:168
A goto_instruction_codet representing the declaration of a local variable.
codet representation of an if-then-else statement.
Definition std_code.h:460
goto_instruction_codet representation of a "return from a function" statement.
const irep_idt & get_identifier() const
Definition std_types.h:590
std::vector< parametert > parameterst
Definition std_types.h:542
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Definition std_expr.h:2942
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
const char * c_str() const
Definition dstring.h:117
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
Extracts a single bit of a bit-vector operand.
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
An expression denoting infinity.
Definition std_expr.h:3042
const irep_idt & id() const
Definition irep.h:396
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
code_blockt make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Provide code for the String.valueOf(F) function.
std::unordered_map< irep_idt, irep_idt > id_mapt
code_blockt make_string_returning_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Provide code for a function that calls a function from the solver and return the string_expr result a...
code_returnt make_string_length_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Generates code for the String.length method.
refined_string_exprt string_literal_to_string_expr(const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Create a string expression whose value is given by a literal.
codet code_assign_components_to_java_string(const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table, bool is_constructor)
Produce code for an assignment of a string expr to a Java string.
refined_string_exprt convert_exprt_to_string_exprt(const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, const irep_idt &function_name, code_blockt &init_code)
Creates a string_exprt from the input exprt representing a char sequence.
code_blockt make_assign_and_return_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function, assign the result to object this and return it.
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
static bool implements_java_char_sequence_pointer(const typet &type)
std::unordered_map< irep_idt, conversion_functiont > conversion_table
refined_string_exprt string_expr_of_function(const irep_idt &function_id, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primit...
code_blockt make_class_identifier_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Used to provide our own implementation of the CProver.classIdentifier() function.
static bool is_java_char_sequence_type(const typet &type)
static bool is_java_string_buffer_type(const typet &type)
bool implements_function(const irep_idt &function_id) const
code_blockt make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Generates code for a function which copies a string object to a new string object.
std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)
Gets the base classes for known String and String-related types, or returns an empty list for other t...
static bool is_java_char_array_pointer_type(const typet &type)
refined_string_exprt make_nondet_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr fro...
code_blockt make_assign_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function and assign the result to object this.
void add_string_type(const irep_idt &class_name, symbol_table_baset &symbol_table)
Add to the symbol table type declaration for a String-like Java class.
exprt allocate_fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
declare a new String and allocate it
static bool is_java_string_pointer_type(const typet &type)
refined_string_exprt replace_char_array(const exprt &array_pointer, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &code)
we declare a new cprover_string whose contents is deduced from the char array.
static bool is_java_string_builder_pointer_type(const typet &type)
exprt::operandst process_parameters(const java_method_typet::parameterst &params, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)
calls string_refine_preprocesst::process_operands with a list of parameters.
static bool is_java_char_sequence_pointer_type(const typet &type)
static bool is_java_char_array_type(const typet &type)
code_blockt make_init_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool is_constructor=true)
Generate the goto code for string initialization.
character_refine_preprocesst character_preprocess
static bool is_java_string_builder_type(const typet &type)
code_blockt make_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Provide code for a function that calls a function from the solver and simply returns it.
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
std::unordered_set< irep_idt > string_types
codet code_assign_string_expr_to_java_string(const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table, bool is_constructor)
Produce code for an assignemnt of a string expr to a Java string.
static bool is_java_string_buffer_pointer_type(const typet &type)
codet code_return_function_application(const irep_idt &function_id, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
return the result of a function call
symbol_exprt fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
add a symbol with static lifetime and name containing cprover_string and given type
code_blockt make_copy_constructor_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Generates code for a constructor of a string object from another string object.
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
exprt::operandst process_operands(const exprt::operandst &operands, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)
for each expression that is of a type implementing strings, we declare a new cprover_string whose con...
static bool is_java_string_type(const typet &type)
const std::array< id_mapt *, 5 > id_maps
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler)
Should be called to provide code for string functions that are used in the code but for which no impl...
static bool java_type_matches_tag(const typet &type, const std::string &tag)
refined_string_exprt decl_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
Add declaration of a refined string expr whose content and length are fresh symbols.
void code_assign_java_string_to_string_expr(const refined_string_exprt &lhs, const exprt &rhs, const source_locationt &loc, const symbol_table_baset &symbol_table, code_blockt &code)
Extract member of struct or union.
Definition std_expr.h:2794
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean negation.
Definition std_expr.h:2278
Disequality.
Definition std_expr.h:1365
The null pointer constant.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const exprt & length() const
const exprt & content() const
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
String type.
Definition std_types.h:913
Struct constructor from list of elements.
Definition std_expr.h:1819
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
Structure type, corresponds to C style structs.
Definition std_types.h:231
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition symbol.h:139
The type of an expression, extends irept.
Definition type.h:29
The unary minus expression.
Definition std_expr.h:423
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
API to expression classes for floating-point arithmetic.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static bool is_constructor(const irep_idt &method_name)
static irep_idt get_tag(const typet &type)
static typet string_length_type()
void add_keys_to_container(const TMap &map, TContainer &container)
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 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
static const typet & get_data_type(const typet &type, const symbol_table_baset &symbol_table)
Finds the type of the data component.
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...
static exprt get_data(const exprt &expr, const symbol_table_baset &symbol_table)
access data member
static exprt get_length(const exprt &expr, const symbol_table_baset &symbol_table)
access length member
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
static const typet & get_length_type(const typet &type, const symbol_table_baset &symbol_table)
Finds the type of the length component.
Produce code for simple implementation of String Java libraries.
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
#define MAX_FORMAT_ARGS
signedbv_typet java_int_type()
unsignedbv_typet java_char_type()
const java_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:184
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:582
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)
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
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.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Type for string expressions used by the string solver.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1842
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
String expressions for the string solver.
Definition kdev_t.h:24
Author: Diffblue Ltd.
dstringt irep_idt