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
21
22#include <util/arith_tools.h>
23#include <util/bitvector_expr.h>
24#include <util/c_types.h>
26#include <util/floatbv_expr.h>
28#include <util/std_code.h>
29#include <util/string_expr.h>
30
31#include "java_types.h"
32#include "java_utils.h"
33
35
38static irep_idt get_tag(const typet &type)
39{
41 if(type.id() == ID_struct_tag)
43 else if(type.id() == ID_struct)
44 return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
45 else
46 return irep_idt();
47}
48
54 const typet &type, const std::string &tag)
55{
56 return irep_idt("java::" + tag) == get_tag(type);
57}
58
62 const typet &type)
63{
64 if(type.id()==ID_pointer)
65 {
66 const pointer_typet &pt=to_pointer_type(type);
67 const typet &base_type = pt.base_type();
69 }
70 return false;
71}
72
76 const typet &type)
77{
78 return java_type_matches_tag(type, "java.lang.String");
79}
80
84 const typet &type)
85{
86 return java_type_matches_tag(type, "java.lang.StringBuilder");
87}
88
93 const typet &type)
94{
95 if(type.id()==ID_pointer)
96 {
97 const pointer_typet &pt=to_pointer_type(type);
98 const typet &base_type = pt.base_type();
100 }
101 return false;
102}
103
107 const typet &type)
108{
109 return java_type_matches_tag(type, "java.lang.StringBuffer");
110}
111
116 const typet &type)
117{
118 if(type.id()==ID_pointer)
119 {
120 const pointer_typet &pt=to_pointer_type(type);
121 const typet &base_type = pt.base_type();
123 }
124 return false;
125}
126
130 const typet &type)
131{
132 return java_type_matches_tag(type, "java.lang.CharSequence");
133}
134
139 const typet &type)
140{
141 if(type.id()==ID_pointer)
142 {
143 const pointer_typet &pt=to_pointer_type(type);
144 const typet &base_type = pt.base_type();
146 }
147 return false;
148}
149
153 const typet &type)
154{
155 return java_type_matches_tag(type, "array[char]");
156}
157
162 const typet &type)
163{
164 if(type.id()==ID_pointer)
165 {
166 const pointer_typet &pt=to_pointer_type(type);
167 const typet &base_type = pt.base_type();
169 }
170 return false;
171}
172
175{
176 return java_int_type();
177}
178
183std::vector<irep_idt>
185 const irep_idt &class_name)
186{
187 if(!is_known_string_type(class_name))
188 return {};
189
190 std::vector<irep_idt> bases;
191 bases.reserve(3);
192
193 // StringBuilder and StringBuffer derive from AbstractStringBuilder;
194 // other String types (String and CharSequence) derive directly from Object.
195 if(
196 class_name == "java.lang.StringBuilder" ||
197 class_name == "java.lang.StringBuffer")
198 bases.push_back("java.lang.AbstractStringBuilder");
199 else
200 bases.push_back("java.lang.Object");
201
202 // Interfaces:
203 if(class_name != "java.lang.CharSequence")
204 {
205 bases.push_back("java.io.Serializable");
206 bases.push_back("java.lang.CharSequence");
207 }
208 if(class_name == "java.lang.String")
209 bases.push_back("java.lang.Comparable");
210
211 return bases;
212}
213
218 const irep_idt &class_name, symbol_tablet &symbol_table)
219{
220 irep_idt class_symbol_name = "java::" + id2string(class_name);
223 symbolt *string_symbol = nullptr;
225
227 {
228 // A library has already defined this type -- we'll replace its
229 // components with those required for internal string modelling, but
230 // otherwise leave it alone.
232 }
233 else
234 {
235 // No definition of this type exists -- define it as it usually occurs in
236 // the JDK:
238 new_string_type.set_tag(class_name);
240 new_string_type.set_access(ID_public);
241
242 std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
243 for(const irep_idt &base_name : bases)
244 new_string_type.add_base(
245 struct_tag_typet("java::" + id2string(base_name)));
246
247 string_symbol->base_name = id2string(class_name);
248 string_symbol->pretty_name = id2string(class_name);
250 string_symbol->is_type = true;
251 string_symbol->mode = ID_java;
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_tablet &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_tablet &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 get_length(const exprt &expr, const symbol_tablet &symbol_table)
407{
408 return member_exprt(
409 expr, "length", get_length_type(expr.type(), symbol_table));
410}
411
416static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
417{
418 return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
419}
420
430 const exprt &array_pointer,
431 const source_locationt &loc,
432 const irep_idt &function_id,
433 symbol_table_baset &symbol_table,
434 code_blockt &code)
435{
436 // array is *array_pointer
438 // array_data is array_pointer-> data
439 const exprt array_data = get_data(array, symbol_table);
441 array_data.type(), "char_array", loc, function_id, symbol_table);
442 const symbol_exprt char_array = sym_char_array.symbol_expr();
443 // char_array = array_pointer->data
445
446 // string_expr is `{ rhs->length; string_array }`
448 get_length(array, symbol_table), char_array, refined_string_type);
449
452
454 string_expr.content(), inf_array, symbol_table, loc, function_id, code);
455
456 return string_expr;
457}
458
467 const typet &type,
468 const source_locationt &loc,
469 const irep_idt &function_id,
470 symbol_table_baset &symbol_table)
471{
473 fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
474 string_symbol.is_static_lifetime=true;
475 return string_symbol.symbol_expr();
476}
477
486 const source_locationt &loc,
487 const irep_idt &function_id,
488 symbol_table_baset &symbol_table,
489 code_blockt &code)
490{
492 index_type, "cprover_string_length", loc, function_id, symbol_table);
493 const symbol_exprt length_field = sym_length.symbol_expr();
496 array_type, "cprover_string_content", loc, function_id, symbol_table);
497 const symbol_exprt content_field = sym_content.symbol_expr();
498 code.add(code_declt(content_field), loc);
499 code.add(code_declt{length_field}, loc);
501}
502
511 const source_locationt &loc,
512 const irep_idt &function_id,
513 symbol_table_baset &symbol_table,
514 code_blockt &code)
515{
517 const refined_string_exprt str =
518 decl_string_expr(loc, function_id, symbol_table, code);
519
521 code.add(code_assignt(str.length(), nondet_length), loc);
522
524 make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
525
528
530 array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
531
533 nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
534
535 code.add(code_assignt(str.content(), array_pointer), loc);
536
537 return refined_string_exprt(str.length(), str.content());
538}
539
548 const typet &type,
549 const source_locationt &loc,
550 const irep_idt &function_id,
551 symbol_table_baset &symbol_table,
552 code_blockt &code)
553{
554 const exprt str = fresh_string(type, loc, function_id, symbol_table);
555
556 allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
557
559 allocate_objects.allocate_dynamic_object(tmp, str, str.type().subtype());
560 allocate_objects.declare_created_symbols(code);
561 code.append(tmp);
562
563 return str;
564}
565
576 const exprt &lhs,
577 const irep_idt &function_id,
578 const exprt::operandst &arguments,
579 symbol_table_baset &symbol_table)
580{
581 return code_assignt(
582 lhs,
584 function_id, arguments, lhs.type(), symbol_table));
585}
586
597 const irep_idt &function_id,
598 const exprt::operandst &arguments,
599 const typet &type,
600 symbol_table_baset &symbol_table)
601{
602 return code_returnt(
603 make_function_application(function_id, arguments, type, symbol_table));
604}
605
613 symbol_table_baset &symbol_table,
614 const source_locationt &loc,
615 const irep_idt &function_id,
616 code_blockt &code)
617{
622 "nondet_infinite_array_pointer",
623 loc,
624 function_id,
625 symbol_table);
626
627 const symbol_exprt data_pointer = data_sym.symbol_expr();
632 code.add(code_assignt{data, std::move(nondet_data)}, loc);
633 return std::move(data);
634}
635
645 const exprt &pointer,
646 const exprt &array,
647 symbol_table_baset &symbol_table,
648 const source_locationt &loc,
649 const irep_idt &function_id,
650 code_blockt &code)
651{
652 PRECONDITION(array.type().id() == ID_array);
653 PRECONDITION(pointer.type().id() == ID_pointer);
655 java_int_type(), "return_array", loc, function_id, symbol_table);
656 const auto return_expr = return_sym.symbol_expr();
657 code.add(code_declt(return_expr), loc);
658 code.add(
662 {array, pointer},
663 symbol_table),
664 loc);
665}
666
676 const exprt &array,
677 const exprt &length,
678 symbol_table_baset &symbol_table,
679 const source_locationt &loc,
680 const irep_idt &function_id,
681 code_blockt &code)
682{
684 java_int_type(), "return_array", loc, function_id, symbol_table);
685 const auto return_expr = return_sym.symbol_expr();
686 code.add(code_declt(return_expr), loc);
687 code.add(
691 {array, length},
692 symbol_table),
693 loc);
694}
695
708 const exprt &pointer,
709 const exprt &length,
710 const irep_idt &char_range,
711 symbol_table_baset &symbol_table,
712 const source_locationt &loc,
713 const irep_idt &function_id,
714 code_blockt &code)
715{
716 PRECONDITION(pointer.type().id() == ID_pointer);
718 java_int_type(), "cnstr_added", loc, function_id, symbol_table);
719 const auto return_expr = return_sym.symbol_expr();
720 code.add(code_declt(return_expr), loc);
722 code.add(
726 {length, pointer, char_set_expr},
727 symbol_table),
728 loc);
729}
730
748 const irep_idt &function_id,
749 const exprt::operandst &arguments,
750 const source_locationt &loc,
751 symbol_table_baset &symbol_table,
752 code_blockt &code)
753{
754 // int return_code;
757 std::string("return_code_") + function_id.c_str(),
758 loc,
759 function_id,
760 symbol_table);
761 const auto return_code = return_code_sym.symbol_expr();
762 code.add(code_declt(return_code), loc);
763
765 make_nondet_string_expr(loc, function_id, symbol_table, code);
766
767 // args is { str.length, str.content, arguments... }
768 exprt::operandst args;
769 args.push_back(string_expr.length());
770 args.push_back(string_expr.content());
771 args.insert(args.end(), arguments.begin(), arguments.end());
772
773 // return_code = <function_id>_data(args)
774 code.add(
776 return_code, function_id, args, symbol_table),
777 loc);
778
779 return string_expr;
780}
781
795 const exprt &lhs,
796 const exprt &rhs_array,
797 const exprt &rhs_length,
798 const symbol_table_baset &symbol_table,
799 bool is_constructor)
800{
803
805 {
806 // Initialise the supertype with the appropriate classid:
807 namespacet ns(symbol_table);
808 const struct_typet &lhs_type = to_struct_type(ns.follow(deref.type()));
810 lhs_type.components().front().type(), source_locationt{}, ns);
816 }
817 else
818 {
819 return code_blockt(
820 {code_assignt(get_length(deref, symbol_table), rhs_length),
821 code_assignt(get_data(deref, symbol_table), rhs_array)});
822 }
823}
824
837 const exprt &lhs,
838 const refined_string_exprt &rhs,
839 const symbol_table_baset &symbol_table,
840 bool is_constructor)
841{
843 lhs, rhs.content(), rhs.length(), symbol_table, is_constructor);
844}
845
856 const refined_string_exprt &lhs,
857 const exprt &rhs,
858 const source_locationt &loc,
859 const symbol_table_baset &symbol_table,
860 code_blockt &code)
861{
863
865
866 // Although we should not reach this code if rhs is null, the association
867 // `pointer -> length` is added to the solver anyway, so we have to make sure
868 // the length is set to something reasonable.
869 auto rhs_length = if_exprt(
871 from_integer(0, lhs.length().type()),
872 get_length(deref, symbol_table));
874
875 // Assignments
876 code.add(code_assignt(lhs.length(), rhs_length), loc);
877 exprt data_as_array = get_data(deref, symbol_table);
878 code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc);
879}
880
893 const std::string &s,
894 const source_locationt &loc,
895 symbol_table_baset &symbol_table,
896 code_blockt &code)
897{
901 loc,
902 symbol_table,
903 code);
904}
905
914 const java_method_typet &type,
915 const source_locationt &loc,
916 const irep_idt &function_id,
917 symbol_table_baset &symbol_table,
918 message_handlert &message_handler)
919{
920 (void)message_handler;
921
922 // Getting the argument
924 PRECONDITION(params.size()==1);
925 PRECONDITION(!params[0].get_identifier().empty());
926 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
927
928 // Holder for output code
929 code_blockt code;
930
931 // Declaring and allocating String * str
932 const exprt str = allocate_fresh_string(
933 type.return_type(), loc, function_id, symbol_table, code);
934
935 // Expression representing 0.0
936 const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
938 zero_float.from_float(0.0);
939 const constant_exprt zero = zero_float.to_expr();
940
941 // For each possible case with have a condition and a string_exprt
942 std::vector<exprt> condition_list;
943 std::vector<refined_string_exprt> string_expr_list;
944
945 // Case of computerized scientific notation
946 condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
949 {arg},
950 loc,
951 symbol_table,
952 code);
954
955 // Subcase of negative scientific notation
956 condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
958 string_literal_to_string_expr("-", loc, symbol_table, code);
962 loc,
963 symbol_table,
964 code);
966
967 // Case of NaN
968 condition_list.push_back(isnan_exprt(arg));
970 string_literal_to_string_expr("NaN", loc, symbol_table, code);
971 string_expr_list.push_back(nan);
972
973 // Case of Infinity
974 extractbit_exprt is_neg(arg, float_spec.width()-1);
976 const refined_string_exprt infinity =
977 string_literal_to_string_expr("Infinity", loc, symbol_table, code);
978 string_expr_list.push_back(infinity);
979
980 // Case -Infinity
981 condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
982 const refined_string_exprt minus_infinity =
983 string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
984 string_expr_list.push_back(minus_infinity);
985
986 // Case of 0.0
987 // Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt,
988 // the latter disregards the sign
989 condition_list.push_back(equal_exprt(arg, zero));
991 string_literal_to_string_expr("0.0", loc, symbol_table, code);
992 string_expr_list.push_back(zero_string);
993
994 // Case of -0.0
996 minus_zero_float.from_float(-0.0f);
997 condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
999 string_literal_to_string_expr("-0.0", loc, symbol_table, code);
1001
1002 // Case of simple notation
1005 bound_inf_float.from_float(1e-3f);
1006 bound_sup_float.from_float(1e7f);
1007 bound_inf_float.change_spec(float_spec);
1008 bound_sup_float.change_spec(float_spec);
1009 const constant_exprt bound_inf = bound_inf_float.to_expr();
1010 const constant_exprt bound_sup = bound_sup_float.to_expr();
1011
1015
1017 ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1019
1020 // Case of a negative number in simple notation
1025
1029 loc,
1030 symbol_table,
1031 code);
1033
1034 // Combining all cases
1035 INVARIANT(
1036 string_expr_list.size()==condition_list.size(),
1037 "number of created strings should correspond to number of conditions");
1038
1039 // We do not check the condition of the first element in the list as it
1040 // will be reached only if all other conditions are not satisfied.
1042 str, string_expr_list[0], symbol_table, true);
1043 for(std::size_t i=1; i<condition_list.size(); i++)
1044 {
1048 str, string_expr_list[i], symbol_table, true),
1049 tmp_code);
1050 }
1051 code.add(tmp_code, loc);
1052
1053 // Return str
1054 code.add(code_returnt(str), loc);
1055 return code;
1056}
1057
1074 const irep_idt &function_id,
1075 const java_method_typet &type,
1076 const source_locationt &loc,
1077 symbol_table_baset &symbol_table,
1078 bool is_constructor)
1079{
1081
1082 // The first parameter is the object to be initialized
1083 PRECONDITION(!params.empty());
1084 PRECONDITION(!params[0].get_identifier().empty());
1085 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1086 if(is_constructor)
1087 params.erase(params.begin());
1088
1089 // Holder for output code
1090 code_blockt code;
1091
1092 // Processing parameters
1093 const exprt::operandst args =
1094 process_parameters(params, loc, function_id, symbol_table, code);
1095
1096 // string_expr <- function(arg1)
1098 string_expr_of_function(function_id, args, loc, symbol_table, code);
1099
1100 // arg_this <- string_expr
1101 code.add(
1103 arg_this, string_expr, symbol_table, is_constructor),
1104 loc);
1105
1106 return code;
1107}
1108
1118 const irep_idt &function_id,
1119 const java_method_typet &type,
1120 const source_locationt &loc,
1121 symbol_table_baset &symbol_table)
1122{
1123 // This is similar to assign functions except we return a pointer to `this`
1124 const java_method_typet::parameterst &params = type.parameters();
1125 PRECONDITION(!params.empty());
1126 PRECONDITION(!params[0].get_identifier().empty());
1127 code_blockt code;
1128 code.add(
1129 make_assign_function_from_call(function_id, type, loc, symbol_table), loc);
1130 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1131 code.add(code_returnt(arg_this), loc);
1132 return code;
1133}
1134
1143 const irep_idt &function_id,
1144 const java_method_typet &type,
1145 const source_locationt &loc,
1146 symbol_table_baset &symbol_table)
1147{
1148 // This is similar to initialization function except we do not ignore
1149 // the first argument
1151 function_id, type, loc, symbol_table, false);
1152}
1153
1167 const java_method_typet &type,
1168 const source_locationt &loc,
1169 const irep_idt &function_id,
1170 symbol_table_baset &symbol_table,
1171 message_handlert &message_handler)
1172{
1174 PRECONDITION(!params.empty());
1175 PRECONDITION(!params[0].get_identifier().empty());
1176 const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1177
1178 // Code to be returned
1179 code_blockt code;
1180
1181 // class_identifier is obj->@class_identifier
1182 const member_exprt class_identifier{
1184
1185 // string_expr = cprover_string_literal(this->@class_identifier)
1188 {class_identifier},
1189 loc,
1190 symbol_table,
1191 code);
1192
1193 // string_expr1 = substr(string_expr, 6)
1194 // We do this to remove the "java::" prefix
1198 loc,
1199 symbol_table,
1200 code);
1201
1202 // string1 = (String*) string_expr
1203 const typet &string_ptr_type = type.return_type();
1205 string_ptr_type, loc, function_id, symbol_table, code);
1206 code.add(
1208 string1, string_expr1, symbol_table, true),
1209 loc);
1210
1211 // > return string1;
1212 code.add(code_returnt{string1}, loc);
1213 return code;
1214}
1215
1227 const irep_idt &function_id,
1228 const java_method_typet &type,
1229 const source_locationt &loc,
1230 symbol_table_baset &symbol_table)
1231{
1232 code_blockt code;
1233 const exprt::operandst args =
1234 process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1235 code.add(
1237 function_id, args, type.return_type(), symbol_table),
1238 loc);
1239 return code;
1240}
1241
1257 const irep_idt &function_id,
1258 const java_method_typet &type,
1259 const source_locationt &loc,
1260 symbol_table_baset &symbol_table)
1261{
1262 // Code for the output
1263 code_blockt code;
1264
1265 // Calling the function
1266 const exprt::operandst arguments =
1267 process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1268
1269 // String expression that will hold the result
1271 string_expr_of_function(function_id, arguments, loc, symbol_table, code);
1272
1273 // Assign to string
1274 const exprt str = allocate_fresh_string(
1275 type.return_type(), loc, function_id, symbol_table, code);
1276 code.add(
1278 str, string_expr, symbol_table, true),
1279 loc);
1280
1281 // Return value
1282 code.add(code_returnt(str), loc);
1283 return code;
1284}
1285
1302 const java_method_typet &type,
1303 const source_locationt &loc,
1304 const irep_idt &function_id,
1305 symbol_table_baset &symbol_table,
1306 message_handlert &message_handler)
1307{
1308 (void)message_handler;
1309
1310 // Code for the output
1311 code_blockt code;
1312
1313 // String expression that will hold the result
1315 decl_string_expr(loc, function_id, symbol_table, code);
1316
1317 // Assign the argument to string_expr
1318 const java_method_typet::parametert &op = type.parameters()[0];
1320 const symbol_exprt arg0{op.get_identifier(), op.type()};
1322 string_expr, arg0, loc, symbol_table, code);
1323
1324 // Allocate and assign the string
1325 const exprt str = allocate_fresh_string(
1326 type.return_type(), loc, function_id, symbol_table, code);
1327 code.add(
1329 str, string_expr, symbol_table, true),
1330 loc);
1331
1332 // Return value
1333 code.add(code_returnt(str), loc);
1334 return code;
1335}
1336
1352 const java_method_typet &type,
1353 const source_locationt &loc,
1354 const irep_idt &function_id,
1355 symbol_table_baset &symbol_table,
1356 message_handlert &message_handler)
1357{
1358 (void)message_handler;
1359
1361
1362 // String expression that will hold the result
1364 decl_string_expr(loc, function_id, symbol_table, copy_constructor_body);
1365
1366 // Assign argument to a string_expr
1367 const java_method_typet::parameterst &params = type.parameters();
1368 PRECONDITION(!params[0].get_identifier().empty());
1369 PRECONDITION(!params[1].get_identifier().empty());
1370 const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
1372 string_expr, arg1, loc, symbol_table, copy_constructor_body);
1373
1374 // Assign string_expr to `this` object
1375 const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1378 arg_this, string_expr, symbol_table, true),
1379 loc);
1380
1381 return copy_constructor_body;
1382}
1383
1397 const java_method_typet &type,
1398 const source_locationt &loc,
1399 const irep_idt &function_id,
1400 symbol_table_baset &symbol_table,
1401 message_handlert &message_handler)
1402{
1403 (void)function_id;
1404 (void)message_handler;
1405
1406 const java_method_typet::parameterst &params = type.parameters();
1407 PRECONDITION(!params[0].get_identifier().empty());
1408 const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1410
1411 code_returnt ret(get_length(deref, symbol_table));
1412 ret.add_source_location() = loc;
1413
1414 return ret;
1415}
1416
1418 const irep_idt &function_id) const
1419{
1420 for(const id_mapt *map : id_maps)
1421 if(map->count(function_id) != 0)
1422 return true;
1423
1424 return conversion_table.count(function_id) != 0;
1425}
1426
1427template <typename TMap, typename TContainer>
1428void add_keys_to_container(const TMap &map, TContainer &container)
1429{
1430 static_assert(
1431 std::is_same<typename TMap::key_type,
1432 typename TContainer::value_type>::value,
1433 "TContainer value_type doesn't match TMap key_type");
1434 std::transform(
1435 map.begin(),
1436 map.end(),
1437 std::inserter(container, container.begin()),
1438 [](const typename TMap::value_type &pair) { return pair.first; });
1439}
1440
1442 std::unordered_set<irep_idt> &methods) const
1443{
1444 for(const id_mapt *map : id_maps)
1445 add_keys_to_container(*map, methods);
1446
1448}
1449
1458 const symbolt &symbol,
1459 symbol_table_baset &symbol_table,
1460 message_handlert &message_handler)
1461{
1462 const irep_idt &function_id = symbol.name;
1463 const java_method_typet &type = to_java_method_type(symbol.type);
1464 const source_locationt &loc = symbol.location;
1465 auto it_id=cprover_equivalent_to_java_function.find(function_id);
1467 return make_function_from_call(it_id->second, type, loc, symbol_table);
1468
1472 it_id->second, type, loc, symbol_table);
1473
1477 it_id->second, type, loc, symbol_table);
1478
1482 it_id->second, type, loc, symbol_table);
1483
1487 it_id->second, type, loc, symbol_table);
1488
1489 auto it=conversion_table.find(function_id);
1490 INVARIANT(
1491 it != conversion_table.end(), "Couldn't retrieve code for string method");
1492
1493 return it->second(type, loc, function_id, symbol_table, message_handler);
1494}
1495
1501 irep_idt class_name)
1502{
1503 return string_types.find(class_name)!=string_types.end();
1504}
1505
1507{
1508 string_types = std::unordered_set<irep_idt>{"java.lang.String",
1509 "java.lang.StringBuilder",
1510 "java.lang.CharSequence",
1511 "java.lang.StringBuffer"};
1512}
1513
1516{
1518
1519 // The following list of function is organized by libraries, with
1520 // constructors first and then methods in alphabetic order.
1521 // Methods that are not supported here should ultimately have Java models
1522 // provided for them in the class-path.
1523
1524 // CProverString library
1526 ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1527 "lang/CharSequence;II)"
1528 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1529 // CProverString.charAt differs from the Java String.charAt in that no
1530 // exception is raised for the out of bounds case.
1532 ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1535 ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1538 ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1541 ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1544 ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1547 ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1548 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1550 ["java::org.cprover.CProverString.delete:(Ljava/lang/"
1551 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1554 ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1555 "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1558 ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1559 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1561
1562 std::string format_signature = "java::org.cprover.CProverString.format:(";
1563 for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1564 format_signature += "Ljava/lang/String;";
1565 format_signature += ")Ljava/lang/String;";
1568
1570 ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1571 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1573 ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1576 ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1577 "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1579 ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1580 "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1582 ["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1585 ["java::org.cprover.CProverString.setLength:(Ljava/lang/"
1586 "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1588 ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1589 "lang/CharSequence;"] = ID_cprover_string_substring_func;
1590 // CProverString.substring differs from the Java String.substring in that no
1591 // exception is raised for the out of bounds case.
1593 ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1594 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1596 ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1597 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1599 ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
1600 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1602 ["java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1605 ["java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1608 ["java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1611 ["java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1614 ["java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1615 std::bind(
1617 this,
1618 std::placeholders::_1,
1619 std::placeholders::_2,
1620 std::placeholders::_3,
1621 std::placeholders::_4,
1622 std::placeholders::_5);
1624 ["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1627 ["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1630 ["java::org.cprover.CProverString.isValidInt:(Ljava/lang/String;I)Z"] =
1633 ["java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z"] =
1635
1636 // String library
1637 conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1638 std::bind(
1640 this,
1641 std::placeholders::_1,
1642 std::placeholders::_2,
1643 std::placeholders::_3,
1644 std::placeholders::_4,
1645 std::placeholders::_5);
1647 ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1649 this,
1650 std::placeholders::_1,
1651 std::placeholders::_2,
1652 std::placeholders::_3,
1653 std::placeholders::_4,
1654 std::placeholders::_5);
1656 ["java::java.lang.String.<init>:()V"]=
1658
1660 ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1663 ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1666 ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1669 ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1672 ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1674
1676 ["java::java.lang.String.indexOf:(I)I"]=
1679 ["java::java.lang.String.indexOf:(II)I"]=
1682 ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1685 ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1688 ["java::java.lang.String.isEmpty:()Z"]=
1691 ["java::java.lang.String.lastIndexOf:(I)I"]=
1694 ["java::java.lang.String.lastIndexOf:(II)I"]=
1697 ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1700 ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1702 conversion_table["java::java.lang.String.length:()I"] = std::bind(
1704 this,
1705 std::placeholders::_1,
1706 std::placeholders::_2,
1707 std::placeholders::_3,
1708 std::placeholders::_4,
1709 std::placeholders::_5);
1711 ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1714 ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
1717 ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1720 ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1723 ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1725 conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
1726 std::bind(
1728 this,
1729 std::placeholders::_1,
1730 std::placeholders::_2,
1731 std::placeholders::_3,
1732 std::placeholders::_4,
1733 std::placeholders::_5);
1735 ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1738 ["java::java.lang.String.trim:()Ljava/lang/String;"]=
1740
1741 // StringBuilder library
1743 ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1745 this,
1746 std::placeholders::_1,
1747 std::placeholders::_2,
1748 std::placeholders::_3,
1749 std::placeholders::_4,
1750 std::placeholders::_5);
1752 ["java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1753 std::bind(
1755 this,
1756 std::placeholders::_1,
1757 std::placeholders::_2,
1758 std::placeholders::_3,
1759 std::placeholders::_4,
1760 std::placeholders::_5);
1762 ["java::java.lang.StringBuilder.<init>:()V"]=
1765 ["java::java.lang.StringBuilder.<init>:(I)V"] =
1767
1769 ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1772 ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1773 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1775 ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1776 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1778 ["java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1779 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1781 ["java::java.lang.StringBuilder.appendCodePoint:(I)"
1782 "Ljava/lang/StringBuilder;"]=
1785 ["java::java.lang.StringBuilder.charAt:(I)C"]=
1788 ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
1791 ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1794 ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
1796 conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
1798 this,
1799 std::placeholders::_1,
1800 std::placeholders::_2,
1801 std::placeholders::_3,
1802 std::placeholders::_4,
1803 std::placeholders::_5);
1805 ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1808 ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1811 ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1813 this,
1814 std::placeholders::_1,
1815 std::placeholders::_2,
1816 std::placeholders::_3,
1817 std::placeholders::_4,
1818 std::placeholders::_5);
1819
1820 // StringBuffer library
1822 ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1824 this,
1825 std::placeholders::_1,
1826 std::placeholders::_2,
1827 std::placeholders::_3,
1828 std::placeholders::_4,
1829 std::placeholders::_5);
1831 ["java::java.lang.StringBuffer.<init>:()V"]=
1833
1835 ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1838 ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1839 "Ljava/lang/StringBuffer;"]=
1842 ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1843 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1845 ["java::java.lang.StringBuffer.appendCodePoint:(I)"
1846 "Ljava/lang/StringBuffer;"]=
1849 ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
1852 ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1855 ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
1858 ["java::java.lang.StringBuffer.length:()I"]=
1859 conversion_table["java::java.lang.String.length:()I"];
1861 ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1864 ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1866 this,
1867 std::placeholders::_1,
1868 std::placeholders::_2,
1869 std::placeholders::_3,
1870 std::placeholders::_4,
1871 std::placeholders::_5);
1872
1873 // CharSequence library
1875 ["java::java.lang.CharSequence.charAt:(I)C"]=
1878 ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1880 this,
1881 std::placeholders::_1,
1882 std::placeholders::_2,
1883 std::placeholders::_3,
1884 std::placeholders::_4,
1885 std::placeholders::_5);
1887 ["java::java.lang.CharSequence.length:()I"]=
1888 conversion_table["java::java.lang.String.length:()I"];
1889
1890 // Other libraries
1892 ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1895 ["java::org.cprover.CProver.classIdentifier:("
1896 "Ljava/lang/Object;)Ljava/lang/String;"] =
1897 std::bind(
1899 this,
1900 std::placeholders::_1,
1901 std::placeholders::_2,
1902 std::placeholders::_3,
1903 std::placeholders::_4,
1904 std::placeholders::_5);
1905}
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.
void base_type(typet &type, const namespacet &ns)
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:253
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:1974
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:674
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
A 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:89
void add(const codet &code)
Definition std_code.h:168
A codet representing the declaration of a local variable.
codet representation of an if-then-else statement.
Definition std_code.h:460
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:2807
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:37
bool empty() const
Definition dstring.h:88
const char * c_str() const
Definition dstring.h:99
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
Extracts a single bit of a bit-vector operand.
The trinary if-then-else operator.
Definition std_expr.h:2226
Array index operator.
Definition std_expr.h:1328
An expression denoting infinity.
Definition std_expr.h:2890
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.
const componentst & components() const
Definition java_types.h:224
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.
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.
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.
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:2667
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:2181
Disequality.
Definition std_expr.h:1283
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:901
Struct constructor from list of elements.
Definition std_expr.h:1722
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:80
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
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
const irep_idt & get_identifier() const
Definition std_types.h:410
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
The unary minus expression.
Definition std_expr.h:390
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.
dstringt irep_idt
Definition irep.h:37
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 const typet & get_length_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the length component.
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
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.
static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
access length member
static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
access data member
static const typet & get_data_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the data component.
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...
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 pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Type for string expressions used by the string solver.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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:1745
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