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
33
35
36#include "java_types.h"
37#include "java_utils.h"
38
41static irep_idt get_tag(const typet &type)
42{
44 if(type.id() == ID_struct_tag)
46 else if(type.id() == ID_struct)
47 return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
48 else
49 return irep_idt();
50}
51
57 const typet &type, const std::string &tag)
58{
59 return irep_idt("java::" + tag) == get_tag(type);
60}
61
65 const typet &type)
66{
67 if(type.id()==ID_pointer)
68 {
69 const pointer_typet &pt=to_pointer_type(type);
70 const typet &base_type = pt.base_type();
71 return is_java_string_type(base_type);
72 }
73 return false;
74}
75
79 const typet &type)
80{
81 return java_type_matches_tag(type, "java.lang.String");
82}
83
87 const typet &type)
88{
89 return java_type_matches_tag(type, "java.lang.StringBuilder");
90}
91
96 const typet &type)
97{
98 if(type.id()==ID_pointer)
99 {
100 const pointer_typet &pt=to_pointer_type(type);
101 const typet &base_type = pt.base_type();
102 return is_java_string_builder_type(base_type);
103 }
104 return false;
105}
106
110 const typet &type)
111{
112 return java_type_matches_tag(type, "java.lang.StringBuffer");
113}
114
119 const typet &type)
120{
121 if(type.id()==ID_pointer)
122 {
123 const pointer_typet &pt=to_pointer_type(type);
124 const typet &base_type = pt.base_type();
125 return is_java_string_buffer_type(base_type);
126 }
127 return false;
128}
129
133 const typet &type)
134{
135 return java_type_matches_tag(type, "java.lang.CharSequence");
136}
137
142 const typet &type)
143{
144 if(type.id()==ID_pointer)
145 {
146 const pointer_typet &pt=to_pointer_type(type);
147 const typet &base_type = pt.base_type();
148 return is_java_char_sequence_type(base_type);
149 }
150 return false;
151}
152
156 const typet &type)
157{
158 return java_type_matches_tag(type, "array[char]");
159}
160
165 const typet &type)
166{
167 if(type.id()==ID_pointer)
168 {
169 const pointer_typet &pt=to_pointer_type(type);
170 const typet &base_type = pt.base_type();
171 return is_java_char_array_type(base_type);
172 }
173 return false;
174}
175
178{
179 return java_int_type();
180}
181
186std::vector<irep_idt>
188 const irep_idt &class_name)
189{
190 if(!is_known_string_type(class_name))
191 return {};
192
193 std::vector<irep_idt> bases;
194 bases.reserve(3);
195
196 // StringBuilder and StringBuffer derive from AbstractStringBuilder;
197 // other String types (String and CharSequence) derive directly from Object.
198 if(
199 class_name == "java.lang.StringBuilder" ||
200 class_name == "java.lang.StringBuffer")
201 bases.push_back("java.lang.AbstractStringBuilder");
202 else
203 bases.push_back("java.lang.Object");
204
205 // Interfaces:
206 if(class_name != "java.lang.CharSequence")
207 {
208 bases.push_back("java.io.Serializable");
209 bases.push_back("java.lang.CharSequence");
210 }
211 if(class_name == "java.lang.String")
212 bases.push_back("java.lang.Comparable");
213
214 return bases;
215}
216
221 const irep_idt &class_name,
222 symbol_table_baset &symbol_table)
223{
224 irep_idt class_symbol_name = "java::" + id2string(class_name);
225 type_symbolt tmp_string_symbol{class_symbol_name, typet{}, ID_java};
226 symbolt *string_symbol = nullptr;
227 bool already_exists = symbol_table.move(tmp_string_symbol, string_symbol);
228
229 if(already_exists)
230 {
231 // A library has already defined this type -- we'll replace its
232 // components with those required for internal string modelling, but
233 // otherwise leave it alone.
234 to_java_class_type(string_symbol->type).components().clear();
235 }
236 else
237 {
238 // No definition of this type exists -- define it as it usually occurs in
239 // the JDK:
240 java_class_typet new_string_type;
241 new_string_type.set_tag(class_name);
242 new_string_type.set_name(class_symbol_name);
243 new_string_type.set_access(ID_public);
244
245 std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
246 for(const irep_idt &base_name : bases)
247 new_string_type.add_base(
248 struct_tag_typet("java::" + id2string(base_name)));
249
250 string_symbol->base_name = id2string(class_name);
251 string_symbol->pretty_name = id2string(class_name);
252 string_symbol->type = new_string_type;
253 }
254
255 auto &string_type = to_java_class_type(string_symbol->type);
256
257 string_type.components().resize(3);
258 const struct_tag_typet &supertype = string_type.bases().front().type();
259 irep_idt supertype_component_name =
260 "@" + id2string(supertype.get_identifier()).substr(6);
261 string_type.components()[0].set_name(supertype_component_name);
262 string_type.components()[0].set_pretty_name(supertype_component_name);
263 string_type.components()[0].type() = supertype;
264 string_type.components()[1].set_name("length");
265 string_type.components()[1].set_pretty_name("length");
266 string_type.components()[1].type()=string_length_type();
267 string_type.components()[2].set_name("data");
268 string_type.components()[2].set_pretty_name("data");
269 string_type.components()[2].type() = pointer_type(java_char_type());
270}
271
281 const java_method_typet::parameterst &params,
282 const source_locationt &loc,
283 const irep_idt &function_id,
284 symbol_table_baset &symbol_table,
285 code_blockt &init_code)
286{
288 for(const auto &p : params)
289 ops.emplace_back(symbol_exprt(p.get_identifier(), p.type()));
290 return process_operands(ops, loc, function_id, symbol_table, init_code);
291}
292
310 const exprt &expr_to_process,
311 const source_locationt &loc,
312 symbol_table_baset &symbol_table,
313 const irep_idt &function_id,
314 code_blockt &init_code)
315{
317 const refined_string_exprt string_expr =
318 decl_string_expr(loc, function_id, symbol_table, init_code);
320 string_expr, expr_to_process, loc, symbol_table, init_code);
321 return string_expr;
322}
323
338 const exprt::operandst &operands,
339 const source_locationt &loc,
340 const irep_idt &function_id,
341 symbol_table_baset &symbol_table,
342 code_blockt &init_code)
343{
345 for(const auto &p : operands)
346 {
348 {
349 init_code.add(code_assumet(
351 ops.push_back(convert_exprt_to_string_exprt(
352 p, loc, symbol_table, function_id, init_code));
353 }
354 else if(is_java_char_array_pointer_type(p.type()))
355 ops.push_back(
356 replace_char_array(p, loc, function_id, symbol_table, init_code));
357 else
358 ops.push_back(p);
359 }
360 return ops;
361}
362
367static const typet &
368get_data_type(const typet &type, const symbol_table_baset &symbol_table)
369{
370 PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
371 if(type.id() == ID_struct_tag)
372 {
373 const symbolt &sym =
374 symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
375 CHECK_RETURN(sym.type.id() != ID_struct_tag);
376 return get_data_type(sym.type, symbol_table);
377 }
378 // else type id is ID_struct
379 const struct_typet &struct_type=to_struct_type(type);
380 return struct_type.component_type("data");
381}
382
387static const typet &
388get_length_type(const typet &type, const symbol_table_baset &symbol_table)
389{
390 PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
391 if(type.id() == ID_struct_tag)
392 {
393 const symbolt &sym =
394 symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
395 CHECK_RETURN(sym.type.id() != ID_struct_tag);
396 return get_length_type(sym.type, symbol_table);
397 }
398 // else type id is ID_struct
399 const struct_typet &struct_type=to_struct_type(type);
400 return struct_type.component_type("length");
401}
402
407static exprt
408get_length(const exprt &expr, const symbol_table_baset &symbol_table)
409{
410 return member_exprt(
411 expr, "length", get_length_type(expr.type(), symbol_table));
412}
413
418static exprt get_data(const exprt &expr, const symbol_table_baset &symbol_table)
419{
420 return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
421}
422
432 const exprt &array_pointer,
433 const source_locationt &loc,
434 const irep_idt &function_id,
435 symbol_table_baset &symbol_table,
436 code_blockt &code)
437{
438 // array is *array_pointer
439 const dereference_exprt array = checked_dereference(array_pointer);
440 // array_data is array_pointer-> data
441 const exprt array_data = get_data(array, symbol_table);
442 const symbolt &sym_char_array = fresh_java_symbol(
443 array_data.type(), "char_array", loc, function_id, symbol_table);
444 const symbol_exprt char_array = sym_char_array.symbol_expr();
445 // char_array = array_pointer->data
446 code.add(code_assignt(char_array, array_data), loc);
447
448 // string_expr is `{ rhs->length; string_array }`
449 const refined_string_exprt string_expr(
450 get_length(array, symbol_table), char_array, refined_string_type);
451
452 const dereference_exprt inf_array(
454
456 string_expr.content(), inf_array, symbol_table, loc, function_id, code);
457
458 return string_expr;
459}
460
469 const typet &type,
470 const source_locationt &loc,
471 const irep_idt &function_id,
472 symbol_table_baset &symbol_table)
473{
474 symbolt string_symbol =
475 fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
476 string_symbol.is_static_lifetime=true;
477 return string_symbol.symbol_expr();
478}
479
488 const source_locationt &loc,
489 const irep_idt &function_id,
490 symbol_table_baset &symbol_table,
491 code_blockt &code)
492{
493 const symbolt &sym_length = fresh_java_symbol(
494 index_type, "cprover_string_length", loc, function_id, symbol_table);
495 const symbol_exprt length_field = sym_length.symbol_expr();
496 const pointer_typet array_type = pointer_type(java_char_type());
497 const symbolt &sym_content = fresh_java_symbol(
498 array_type, "cprover_string_content", loc, function_id, symbol_table);
499 const symbol_exprt content_field = sym_content.symbol_expr();
500 code.add(code_declt(content_field), loc);
501 code.add(code_declt{length_field}, loc);
502 return refined_string_exprt{length_field, content_field, refined_string_type};
503}
504
513 const source_locationt &loc,
514 const irep_idt &function_id,
515 symbol_table_baset &symbol_table,
516 code_blockt &code)
517{
519 const refined_string_exprt str =
520 decl_string_expr(loc, function_id, symbol_table, code);
521
523 code.add(code_assignt(str.length(), nondet_length), loc);
524
525 const exprt nondet_array_expr =
526 make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
527
528 const address_of_exprt array_pointer(
529 index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
530
532 array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
533
535 nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
536
537 code.add(code_assignt(str.content(), array_pointer), loc);
538
539 return refined_string_exprt(str.length(), str.content());
540}
541
550 const typet &type,
551 const source_locationt &loc,
552 const irep_idt &function_id,
553 symbol_table_baset &symbol_table,
554 code_blockt &code)
555{
556 const exprt str = fresh_string(type, loc, function_id, symbol_table);
557
558 allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
559
560 code_blockt tmp;
561 allocate_objects.allocate_dynamic_object(
562 tmp, str, to_reference_type(str.type()).base_type());
563 allocate_objects.declare_created_symbols(code);
564 code.append(tmp);
565
566 return str;
567}
568
579 const exprt &lhs,
580 const irep_idt &function_id,
581 const exprt::operandst &arguments,
582 symbol_table_baset &symbol_table)
583{
584 return code_assignt(
585 lhs,
587 function_id, arguments, lhs.type(), symbol_table));
588}
589
600 const irep_idt &function_id,
601 const exprt::operandst &arguments,
602 const typet &type,
603 symbol_table_baset &symbol_table)
604{
605 return code_returnt(
606 make_function_application(function_id, arguments, type, symbol_table));
607}
608
616 symbol_table_baset &symbol_table,
617 const source_locationt &loc,
618 const irep_idt &function_id,
619 code_blockt &code)
620{
621 const array_typet array_type(
623 const symbolt data_sym = fresh_java_symbol(
624 pointer_type(array_type),
625 "nondet_infinite_array_pointer",
626 loc,
627 function_id,
628 symbol_table);
629
630 const symbol_exprt data_pointer = data_sym.symbol_expr();
631 code.add(code_declt(data_pointer));
632 code.add(make_allocate_code(data_pointer, array_type.size()));
633 side_effect_expr_nondett nondet_data{array_type, loc};
634 dereference_exprt data{data_pointer};
635 code.add(code_assignt{data, std::move(nondet_data)}, loc);
636 return std::move(data);
637}
638
648 const exprt &pointer,
649 const exprt &array,
650 symbol_table_baset &symbol_table,
651 const source_locationt &loc,
652 const irep_idt &function_id,
653 code_blockt &code)
654{
655 PRECONDITION(array.type().id() == ID_array);
656 PRECONDITION(pointer.type().id() == ID_pointer);
657 const symbolt &return_sym = fresh_java_symbol(
658 java_int_type(), "return_array", loc, function_id, symbol_table);
659 const auto return_expr = return_sym.symbol_expr();
660 code.add(code_declt(return_expr), loc);
661 code.add(
663 return_expr,
664 ID_cprover_associate_array_to_pointer_func,
665 {array, pointer},
666 symbol_table),
667 loc);
668}
669
679 const exprt &array,
680 const exprt &length,
681 symbol_table_baset &symbol_table,
682 const source_locationt &loc,
683 const irep_idt &function_id,
684 code_blockt &code)
685{
686 const symbolt &return_sym = fresh_java_symbol(
687 java_int_type(), "return_array", loc, function_id, symbol_table);
688 const auto return_expr = return_sym.symbol_expr();
689 code.add(code_declt(return_expr), loc);
690 code.add(
692 return_expr,
693 ID_cprover_associate_length_to_array_func,
694 {array, length},
695 symbol_table),
696 loc);
697}
698
711 const exprt &pointer,
712 const exprt &length,
713 const irep_idt &char_range,
714 symbol_table_baset &symbol_table,
715 const source_locationt &loc,
716 const irep_idt &function_id,
717 code_blockt &code)
718{
719 PRECONDITION(pointer.type().id() == ID_pointer);
720 const symbolt &return_sym = fresh_java_symbol(
721 java_int_type(), "cnstr_added", loc, function_id, symbol_table);
722 const auto return_expr = return_sym.symbol_expr();
723 code.add(code_declt(return_expr), loc);
724 const constant_exprt char_set_expr(char_range, string_typet());
725 code.add(
727 return_expr,
728 ID_cprover_string_constrain_characters_func,
729 {length, pointer, char_set_expr},
730 symbol_table),
731 loc);
732}
733
751 const irep_idt &function_id,
752 const exprt::operandst &arguments,
753 const source_locationt &loc,
754 symbol_table_baset &symbol_table,
755 code_blockt &code)
756{
757 // int return_code;
758 const symbolt return_code_sym = fresh_java_symbol(
760 std::string("return_code_") + function_id.c_str(),
761 loc,
762 function_id,
763 symbol_table);
764 const auto return_code = return_code_sym.symbol_expr();
765 code.add(code_declt(return_code), loc);
766
767 const refined_string_exprt string_expr =
768 make_nondet_string_expr(loc, function_id, symbol_table, code);
769
770 // args is { str.length, str.content, arguments... }
771 exprt::operandst args;
772 args.push_back(string_expr.length());
773 args.push_back(string_expr.content());
774 args.insert(args.end(), arguments.begin(), arguments.end());
775
776 // return_code = <function_id>_data(args)
777 code.add(
779 return_code, function_id, args, symbol_table),
780 loc);
781
782 return string_expr;
783}
784
798 const exprt &lhs,
799 const exprt &rhs_array,
800 const exprt &rhs_length,
801 const symbol_table_baset &symbol_table,
802 bool is_constructor)
803{
806
808 {
809 // Initialise the supertype with the appropriate classid:
810 namespacet ns(symbol_table);
811 const struct_typet &lhs_type =
812 ns.follow_tag(to_struct_tag_type(deref.type()));
813 auto zero_base_object = *zero_initializer(
814 lhs_type.components().front().type(), source_locationt{}, ns);
816 to_struct_expr(zero_base_object), ns, to_struct_tag_type(deref.type()));
817 struct_exprt struct_rhs(
818 {zero_base_object, rhs_length, rhs_array}, deref.type());
819 return code_assignt(checked_dereference(lhs), struct_rhs);
820 }
821 else
822 {
823 return code_blockt(
824 {code_assignt(get_length(deref, symbol_table), rhs_length),
825 code_assignt(get_data(deref, symbol_table), rhs_array)});
826 }
827}
828
841 const exprt &lhs,
842 const refined_string_exprt &rhs,
843 const symbol_table_baset &symbol_table,
844 bool is_constructor)
845{
847 lhs, rhs.content(), rhs.length(), symbol_table, is_constructor);
848}
849
860 const refined_string_exprt &lhs,
861 const exprt &rhs,
862 const source_locationt &loc,
863 const symbol_table_baset &symbol_table,
864 code_blockt &code)
865{
867
868 const dereference_exprt deref = checked_dereference(rhs);
869
870 // Although we should not reach this code if rhs is null, the association
871 // `pointer -> length` is added to the solver anyway, so we have to make sure
872 // the length is set to something reasonable.
873 auto rhs_length = if_exprt(
875 from_integer(0, lhs.length().type()),
876 get_length(deref, symbol_table));
877 rhs_length.set(ID_mode, ID_java);
878
879 // Assignments
880 code.add(code_assignt(lhs.length(), rhs_length), loc);
881 exprt data_as_array = get_data(deref, symbol_table);
882 code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc);
883}
884
897 const std::string &s,
898 const source_locationt &loc,
899 symbol_table_baset &symbol_table,
900 code_blockt &code)
901{
903 ID_cprover_string_literal_func,
905 loc,
906 symbol_table,
907 code);
908}
909
918 const java_method_typet &type,
919 const source_locationt &loc,
920 const irep_idt &function_id,
921 symbol_table_baset &symbol_table,
922 message_handlert &message_handler)
923{
924 (void)message_handler;
925
926 // Getting the argument
928 PRECONDITION(params.size()==1);
929 PRECONDITION(!params[0].get_identifier().empty());
930 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
931
932 // Holder for output code
933 code_blockt code;
934
935 // Declaring and allocating String * str
936 const exprt str = allocate_fresh_string(
937 type.return_type(), loc, function_id, symbol_table, code);
938
939 // Expression representing 0.0
940 const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
941 ieee_floatt zero_float(float_spec);
942 zero_float.from_float(0.0);
943 const constant_exprt zero = zero_float.to_expr();
944
945 // For each possible case with have a condition and a string_exprt
946 std::vector<exprt> condition_list;
947 std::vector<refined_string_exprt> string_expr_list;
948
949 // Case of computerized scientific notation
950 condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
952 ID_cprover_string_of_float_scientific_notation_func,
953 {arg},
954 loc,
955 symbol_table,
956 code);
957 string_expr_list.push_back(sci_notation);
958
959 // Subcase of negative scientific notation
960 condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
961 const refined_string_exprt minus_sign =
962 string_literal_to_string_expr("-", loc, symbol_table, code);
963 const refined_string_exprt neg_sci_notation = string_expr_of_function(
964 ID_cprover_string_concat_func,
965 {minus_sign, sci_notation},
966 loc,
967 symbol_table,
968 code);
969 string_expr_list.push_back(neg_sci_notation);
970
971 // Case of NaN
972 condition_list.push_back(isnan_exprt(arg));
973 const refined_string_exprt nan =
974 string_literal_to_string_expr("NaN", loc, symbol_table, code);
975 string_expr_list.push_back(nan);
976
977 // Case of Infinity
978 extractbit_exprt is_neg(arg, float_spec.width()-1);
979 condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
980 const refined_string_exprt infinity =
981 string_literal_to_string_expr("Infinity", loc, symbol_table, code);
982 string_expr_list.push_back(infinity);
983
984 // Case -Infinity
985 condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
986 const refined_string_exprt minus_infinity =
987 string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
988 string_expr_list.push_back(minus_infinity);
989
990 // Case of 0.0
991 // Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt,
992 // the latter disregards the sign
993 condition_list.push_back(equal_exprt(arg, zero));
994 const refined_string_exprt zero_string =
995 string_literal_to_string_expr("0.0", loc, symbol_table, code);
996 string_expr_list.push_back(zero_string);
997
998 // Case of -0.0
999 ieee_floatt minus_zero_float(float_spec);
1000 minus_zero_float.from_float(-0.0f);
1001 condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
1002 const refined_string_exprt minus_zero_string =
1003 string_literal_to_string_expr("-0.0", loc, symbol_table, code);
1004 string_expr_list.push_back(minus_zero_string);
1005
1006 // Case of simple notation
1007 ieee_floatt bound_inf_float(float_spec);
1008 ieee_floatt bound_sup_float(float_spec);
1009 bound_inf_float.from_float(1e-3f);
1010 bound_sup_float.from_float(1e7f);
1011 bound_inf_float.change_spec(float_spec);
1012 bound_sup_float.change_spec(float_spec);
1013 const constant_exprt bound_inf = bound_inf_float.to_expr();
1014 const constant_exprt bound_sup = bound_sup_float.to_expr();
1015
1016 const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf),
1017 binary_relation_exprt(arg, ID_lt, bound_sup)};
1018 condition_list.push_back(is_simple_float);
1019
1020 const refined_string_exprt simple_notation = string_expr_of_function(
1021 ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1022 string_expr_list.push_back(simple_notation);
1023
1024 // Case of a negative number in simple notation
1025 const and_exprt is_neg_simple_float{
1026 binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
1027 binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))};
1028 condition_list.push_back(is_neg_simple_float);
1029
1030 const refined_string_exprt neg_simple_notation = string_expr_of_function(
1031 ID_cprover_string_concat_func,
1032 {minus_sign, simple_notation},
1033 loc,
1034 symbol_table,
1035 code);
1036 string_expr_list.push_back(neg_simple_notation);
1037
1038 // Combining all cases
1039 INVARIANT(
1040 string_expr_list.size()==condition_list.size(),
1041 "number of created strings should correspond to number of conditions");
1042
1043 // We do not check the condition of the first element in the list as it
1044 // will be reached only if all other conditions are not satisfied.
1046 str, string_expr_list[0], symbol_table, true);
1047 for(std::size_t i=1; i<condition_list.size(); i++)
1048 {
1049 tmp_code = code_ifthenelset(
1050 condition_list[i],
1052 str, string_expr_list[i], symbol_table, true),
1053 tmp_code);
1054 }
1055 code.add(tmp_code, loc);
1056
1057 // Return str
1058 code.add(code_returnt(str), loc);
1059 return code;
1060}
1061
1078 const irep_idt &function_id,
1079 const java_method_typet &type,
1080 const source_locationt &loc,
1081 symbol_table_baset &symbol_table,
1082 bool is_constructor)
1083{
1085
1086 // The first parameter is the object to be initialized
1087 PRECONDITION(!params.empty());
1088 PRECONDITION(!params[0].get_identifier().empty());
1089 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1090 if(is_constructor)
1091 params.erase(params.begin());
1092
1093 // Holder for output code
1094 code_blockt code;
1095
1096 // Processing parameters
1097 const exprt::operandst args =
1098 process_parameters(params, loc, function_id, symbol_table, code);
1099
1100 // string_expr <- function(arg1)
1101 const refined_string_exprt string_expr =
1102 string_expr_of_function(function_id, args, loc, symbol_table, code);
1103
1104 // arg_this <- string_expr
1105 code.add(
1107 arg_this, string_expr, symbol_table, is_constructor),
1108 loc);
1109
1110 return code;
1111}
1112
1122 const irep_idt &function_id,
1123 const java_method_typet &type,
1124 const source_locationt &loc,
1125 symbol_table_baset &symbol_table)
1126{
1127 // This is similar to assign functions except we return a pointer to `this`
1128 const java_method_typet::parameterst &params = type.parameters();
1129 PRECONDITION(!params.empty());
1130 PRECONDITION(!params[0].get_identifier().empty());
1131 code_blockt code;
1132 code.add(
1133 make_assign_function_from_call(function_id, type, loc, symbol_table), loc);
1134 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1135 code.add(code_returnt(arg_this), loc);
1136 return code;
1137}
1138
1147 const irep_idt &function_id,
1148 const java_method_typet &type,
1149 const source_locationt &loc,
1150 symbol_table_baset &symbol_table)
1151{
1152 // This is similar to initialization function except we do not ignore
1153 // the first argument
1155 function_id, type, loc, symbol_table, false);
1156}
1157
1171 const java_method_typet &type,
1172 const source_locationt &loc,
1173 const irep_idt &function_id,
1174 symbol_table_baset &symbol_table,
1175 message_handlert &message_handler)
1176{
1178 PRECONDITION(!params.empty());
1179 PRECONDITION(!params[0].get_identifier().empty());
1180 const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1181
1182 // Code to be returned
1183 code_blockt code;
1184
1185 // class_identifier is obj->@class_identifier
1186 const member_exprt class_identifier{
1188
1189 // string_expr = cprover_string_literal(this->@class_identifier)
1191 ID_cprover_string_literal_func,
1192 {class_identifier},
1193 loc,
1194 symbol_table,
1195 code);
1196
1197 // string_expr1 = substr(string_expr, 6)
1198 // We do this to remove the "java::" prefix
1199 const refined_string_exprt string_expr1 = string_expr_of_function(
1200 ID_cprover_string_substring_func,
1201 {string_expr, from_integer(6, java_int_type())},
1202 loc,
1203 symbol_table,
1204 code);
1205
1206 // string1 = (String*) string_expr
1207 const typet &string_ptr_type = type.return_type();
1208 const exprt string1 = allocate_fresh_string(
1209 string_ptr_type, loc, function_id, symbol_table, code);
1210 code.add(
1212 string1, string_expr1, symbol_table, true),
1213 loc);
1214
1215 // > return string1;
1216 code.add(code_returnt{string1}, loc);
1217 return code;
1218}
1219
1231 const irep_idt &function_id,
1232 const java_method_typet &type,
1233 const source_locationt &loc,
1234 symbol_table_baset &symbol_table)
1235{
1236 code_blockt code;
1237 const exprt::operandst args =
1238 process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1239 code.add(
1241 function_id, args, type.return_type(), symbol_table),
1242 loc);
1243 return code;
1244}
1245
1261 const irep_idt &function_id,
1262 const java_method_typet &type,
1263 const source_locationt &loc,
1264 symbol_table_baset &symbol_table)
1265{
1266 // Code for the output
1267 code_blockt code;
1268
1269 // Calling the function
1270 const exprt::operandst arguments =
1271 process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1272
1273 // String expression that will hold the result
1274 const refined_string_exprt string_expr =
1275 string_expr_of_function(function_id, arguments, loc, symbol_table, code);
1276
1277 // Assign to string
1278 const exprt str = allocate_fresh_string(
1279 type.return_type(), loc, function_id, symbol_table, code);
1280 code.add(
1282 str, string_expr, symbol_table, true),
1283 loc);
1284
1285 // Return value
1286 code.add(code_returnt(str), loc);
1287 return code;
1288}
1289
1306 const java_method_typet &type,
1307 const source_locationt &loc,
1308 const irep_idt &function_id,
1309 symbol_table_baset &symbol_table,
1310 message_handlert &message_handler)
1311{
1312 (void)message_handler;
1313
1314 // Code for the output
1315 code_blockt code;
1316
1317 // String expression that will hold the result
1318 const refined_string_exprt string_expr =
1319 decl_string_expr(loc, function_id, symbol_table, code);
1320
1321 // Assign the argument to string_expr
1322 const java_method_typet::parametert &op = type.parameters()[0];
1324 const symbol_exprt arg0{op.get_identifier(), op.type()};
1326 string_expr, arg0, loc, symbol_table, code);
1327
1328 // Allocate and assign the string
1329 const exprt str = allocate_fresh_string(
1330 type.return_type(), loc, function_id, symbol_table, code);
1331 code.add(
1333 str, string_expr, symbol_table, true),
1334 loc);
1335
1336 // Return value
1337 code.add(code_returnt(str), loc);
1338 return code;
1339}
1340
1356 const java_method_typet &type,
1357 const source_locationt &loc,
1358 const irep_idt &function_id,
1359 symbol_table_baset &symbol_table,
1360 message_handlert &message_handler)
1361{
1362 (void)message_handler;
1363
1365
1366 // String expression that will hold the result
1367 const refined_string_exprt string_expr =
1368 decl_string_expr(loc, function_id, symbol_table, copy_constructor_body);
1369
1370 // Assign argument to a string_expr
1371 const java_method_typet::parameterst &params = type.parameters();
1372 PRECONDITION(!params[0].get_identifier().empty());
1373 PRECONDITION(!params[1].get_identifier().empty());
1374 const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
1376 string_expr, arg1, loc, symbol_table, copy_constructor_body);
1377
1378 // Assign string_expr to `this` object
1379 const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1382 arg_this, string_expr, symbol_table, true),
1383 loc);
1384
1386}
1387
1401 const java_method_typet &type,
1402 const source_locationt &loc,
1403 const irep_idt &function_id,
1404 symbol_table_baset &symbol_table,
1405 message_handlert &message_handler)
1406{
1407 (void)function_id;
1408 (void)message_handler;
1409
1410 const java_method_typet::parameterst &params = type.parameters();
1411 PRECONDITION(!params[0].get_identifier().empty());
1412 const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1414
1415 code_returnt ret(get_length(deref, symbol_table));
1416 ret.add_source_location() = loc;
1417
1418 return ret;
1419}
1420
1422 const irep_idt &function_id) const
1423{
1424 for(const id_mapt *map : id_maps)
1425 if(map->count(function_id) != 0)
1426 return true;
1427
1428 return conversion_table.count(function_id) != 0;
1429}
1430
1431template <typename TMap, typename TContainer>
1432void add_keys_to_container(const TMap &map, TContainer &container)
1433{
1434 static_assert(
1435 std::is_same<typename TMap::key_type,
1436 typename TContainer::value_type>::value,
1437 "TContainer value_type doesn't match TMap key_type");
1438 std::transform(
1439 map.begin(),
1440 map.end(),
1441 std::inserter(container, container.begin()),
1442 [](const typename TMap::value_type &pair) { return pair.first; });
1443}
1444
1446 std::unordered_set<irep_idt> &methods) const
1447{
1448 for(const id_mapt *map : id_maps)
1449 add_keys_to_container(*map, methods);
1450
1452}
1453
1462 const symbolt &symbol,
1463 symbol_table_baset &symbol_table,
1464 message_handlert &message_handler)
1465{
1466 const irep_idt &function_id = symbol.name;
1467 const java_method_typet &type = to_java_method_type(symbol.type);
1468 const source_locationt &loc = symbol.location;
1469 auto it_id=cprover_equivalent_to_java_function.find(function_id);
1471 return make_function_from_call(it_id->second, type, loc, symbol_table);
1472
1476 it_id->second, type, loc, symbol_table);
1477
1478 it_id=cprover_equivalent_to_java_constructor.find(function_id);
1481 it_id->second, type, loc, symbol_table);
1482
1486 it_id->second, type, loc, symbol_table);
1487
1488 it_id=cprover_equivalent_to_java_assign_function.find(function_id);
1491 it_id->second, type, loc, symbol_table);
1492
1493 auto it=conversion_table.find(function_id);
1494 INVARIANT(
1495 it != conversion_table.end(), "Couldn't retrieve code for string method");
1496
1497 return it->second(type, loc, function_id, symbol_table, message_handler);
1498}
1499
1505 irep_idt class_name)
1506{
1507 return string_types.find(class_name)!=string_types.end();
1508}
1509
1511{
1512 string_types = std::unordered_set<irep_idt>{"java.lang.String",
1513 "java.lang.StringBuilder",
1514 "java.lang.CharSequence",
1515 "java.lang.StringBuffer"};
1516}
1517
1520{
1522
1523 // The following list of function is organized by libraries, with
1524 // constructors first and then methods in alphabetic order.
1525 // Methods that are not supported here should ultimately have Java models
1526 // provided for them in the class-path.
1527
1528 // CProverString library
1530 ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1531 "lang/CharSequence;II)"
1532 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1533 // CProverString.charAt differs from the Java String.charAt in that no
1534 // exception is raised for the out of bounds case.
1536 ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1537 ID_cprover_string_char_at_func;
1539 ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1540 ID_cprover_string_char_at_func;
1542 ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1543 ID_cprover_string_code_point_at_func;
1545 ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1546 ID_cprover_string_code_point_before_func;
1548 ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1549 ID_cprover_string_code_point_count_func;
1551 ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1552 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1554 ["java::org.cprover.CProverString.delete:(Ljava/lang/"
1555 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1556 ID_cprover_string_delete_func;
1558 ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1559 "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1560 ID_cprover_string_delete_char_at_func;
1562 ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1563 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1564 ID_cprover_string_delete_char_at_func;
1565
1566 std::string format_signature = "java::org.cprover.CProverString.format:(";
1567 for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1568 format_signature += "Ljava/lang/String;";
1569 format_signature += ")Ljava/lang/String;";
1571 ID_cprover_string_format_func;
1572
1574 ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1575 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1577 ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1578 "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1580 ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1581 "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1583 ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1584 "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1586 ["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1587 ID_cprover_string_set_length_func;
1589 ["java::org.cprover.CProverString.setLength:(Ljava/lang/"
1590 "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1592 ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1593 "lang/CharSequence;"] = ID_cprover_string_substring_func;
1594 // CProverString.substring differs from the Java String.substring in that no
1595 // exception is raised for the out of bounds case.
1597 ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1598 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1600 ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1601 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1603 ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
1604 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1606 ["java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1607 ID_cprover_string_of_int_func;
1609 ["java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1610 ID_cprover_string_of_int_func;
1612 ["java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1613 ID_cprover_string_of_long_func;
1615 ["java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1616 ID_cprover_string_of_long_func;
1618 ["java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1619 std::bind(
1621 this,
1622 std::placeholders::_1,
1623 std::placeholders::_2,
1624 std::placeholders::_3,
1625 std::placeholders::_4,
1626 std::placeholders::_5);
1628 ["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1629 ID_cprover_string_parse_int_func;
1631 ["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1632 ID_cprover_string_parse_int_func;
1634 ["java::org.cprover.CProverString.isValidInt:(Ljava/lang/String;I)Z"] =
1635 ID_cprover_string_is_valid_int_func;
1637 ["java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z"] =
1638 ID_cprover_string_is_valid_long_func;
1639
1640 // String library
1641 conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1642 std::bind(
1644 this,
1645 std::placeholders::_1,
1646 std::placeholders::_2,
1647 std::placeholders::_3,
1648 std::placeholders::_4,
1649 std::placeholders::_5);
1651 ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1653 this,
1654 std::placeholders::_1,
1655 std::placeholders::_2,
1656 std::placeholders::_3,
1657 std::placeholders::_4,
1658 std::placeholders::_5);
1660 ["java::java.lang.String.<init>:()V"]=
1661 ID_cprover_string_empty_string_func;
1662
1664 ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1665 ID_cprover_string_compare_to_func;
1667 ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1668 ID_cprover_string_concat_func;
1670 ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1671 ID_cprover_string_contains_func;
1673 ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1674 ID_cprover_string_endswith_func;
1676 ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1677 ID_cprover_string_equals_ignore_case_func;
1678
1680 ["java::java.lang.String.indexOf:(I)I"]=
1681 ID_cprover_string_index_of_func;
1683 ["java::java.lang.String.indexOf:(II)I"]=
1684 ID_cprover_string_index_of_func;
1686 ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1687 ID_cprover_string_index_of_func;
1689 ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1690 ID_cprover_string_index_of_func;
1692 ["java::java.lang.String.isEmpty:()Z"]=
1693 ID_cprover_string_is_empty_func;
1695 ["java::java.lang.String.lastIndexOf:(I)I"]=
1696 ID_cprover_string_last_index_of_func;
1698 ["java::java.lang.String.lastIndexOf:(II)I"]=
1699 ID_cprover_string_last_index_of_func;
1701 ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1702 ID_cprover_string_last_index_of_func;
1704 ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1705 ID_cprover_string_last_index_of_func;
1706 conversion_table["java::java.lang.String.length:()I"] = std::bind(
1708 this,
1709 std::placeholders::_1,
1710 std::placeholders::_2,
1711 std::placeholders::_3,
1712 std::placeholders::_4,
1713 std::placeholders::_5);
1715 ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1716 ID_cprover_string_replace_func;
1718 ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
1719 ID_cprover_string_replace_func;
1721 ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1722 ID_cprover_string_startswith_func;
1724 ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1725 ID_cprover_string_startswith_func;
1727 ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1728 ID_cprover_string_to_lower_case_func;
1729 conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
1730 std::bind(
1732 this,
1733 std::placeholders::_1,
1734 std::placeholders::_2,
1735 std::placeholders::_3,
1736 std::placeholders::_4,
1737 std::placeholders::_5);
1739 ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1740 ID_cprover_string_to_upper_case_func;
1742 ["java::java.lang.String.trim:()Ljava/lang/String;"]=
1743 ID_cprover_string_trim_func;
1744
1745 // StringBuilder library
1747 ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1749 this,
1750 std::placeholders::_1,
1751 std::placeholders::_2,
1752 std::placeholders::_3,
1753 std::placeholders::_4,
1754 std::placeholders::_5);
1756 ["java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1757 std::bind(
1759 this,
1760 std::placeholders::_1,
1761 std::placeholders::_2,
1762 std::placeholders::_3,
1763 std::placeholders::_4,
1764 std::placeholders::_5);
1766 ["java::java.lang.StringBuilder.<init>:()V"]=
1767 ID_cprover_string_empty_string_func;
1769 ["java::java.lang.StringBuilder.<init>:(I)V"] =
1770 ID_cprover_string_empty_string_func;
1771
1773 ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1774 ID_cprover_string_concat_char_func;
1776 ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1777 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1779 ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1780 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1782 ["java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1783 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1785 ["java::java.lang.StringBuilder.appendCodePoint:(I)"
1786 "Ljava/lang/StringBuilder;"]=
1787 ID_cprover_string_concat_code_point_func;
1789 ["java::java.lang.StringBuilder.charAt:(I)C"]=
1790 ID_cprover_string_char_at_func;
1792 ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
1793 ID_cprover_string_code_point_at_func;
1795 ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1796 ID_cprover_string_code_point_before_func;
1798 ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
1799 ID_cprover_string_code_point_count_func;
1800 conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
1802 this,
1803 std::placeholders::_1,
1804 std::placeholders::_2,
1805 std::placeholders::_3,
1806 std::placeholders::_4,
1807 std::placeholders::_5);
1809 ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1810 ID_cprover_string_substring_func;
1812 ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1813 ID_cprover_string_substring_func;
1815 ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1817 this,
1818 std::placeholders::_1,
1819 std::placeholders::_2,
1820 std::placeholders::_3,
1821 std::placeholders::_4,
1822 std::placeholders::_5);
1823
1824 // StringBuffer library
1826 ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1828 this,
1829 std::placeholders::_1,
1830 std::placeholders::_2,
1831 std::placeholders::_3,
1832 std::placeholders::_4,
1833 std::placeholders::_5);
1835 ["java::java.lang.StringBuffer.<init>:()V"]=
1836 ID_cprover_string_empty_string_func;
1837
1839 ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1840 ID_cprover_string_concat_char_func;
1842 ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1843 "Ljava/lang/StringBuffer;"]=
1844 ID_cprover_string_concat_func;
1846 ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1847 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1849 ["java::java.lang.StringBuffer.appendCodePoint:(I)"
1850 "Ljava/lang/StringBuffer;"]=
1851 ID_cprover_string_concat_code_point_func;
1853 ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
1854 ID_cprover_string_code_point_at_func;
1856 ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1857 ID_cprover_string_code_point_before_func;
1859 ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
1860 ID_cprover_string_code_point_count_func;
1862 ["java::java.lang.StringBuffer.length:()I"]=
1863 conversion_table["java::java.lang.String.length:()I"];
1865 ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1866 ID_cprover_string_substring_func;
1868 ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1870 this,
1871 std::placeholders::_1,
1872 std::placeholders::_2,
1873 std::placeholders::_3,
1874 std::placeholders::_4,
1875 std::placeholders::_5);
1876
1877 // CharSequence library
1879 ["java::java.lang.CharSequence.charAt:(I)C"]=
1880 ID_cprover_string_char_at_func;
1882 ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1884 this,
1885 std::placeholders::_1,
1886 std::placeholders::_2,
1887 std::placeholders::_3,
1888 std::placeholders::_4,
1889 std::placeholders::_5);
1891 ["java::java.lang.CharSequence.length:()I"]=
1892 conversion_table["java::java.lang.String.length:()I"];
1893
1894 // Other libraries
1896 ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1897 ID_cprover_string_of_int_hex_func;
1899 ["java::org.cprover.CProver.classIdentifier:("
1900 "Ljava/lang/Object;)Ljava/lang/String;"] =
1901 std::bind(
1903 this,
1904 std::placeholders::_1,
1905 std::placeholders::_2,
1906 std::placeholders::_3,
1907 std::placeholders::_4,
1908 std::placeholders::_5);
1909}
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:235
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.
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:2125
Arrays with given size.
Definition std_types.h:807
const exprt & size() const
Definition std_types.h:840
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
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 afunction" statement.
const irep_idt & get_identifier() const
Definition std_types.h:634
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
std::vector< parametert > parameterst
Definition std_types.h:586
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Definition std_expr.h:2995
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:38
bool empty() const
Definition dstring.h:89
const char * c_str() const
Definition dstring.h:116
Equality.
Definition std_expr.h:1366
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
source_locationt & add_source_location()
Definition expr.h:236
Extracts a single bit of a bit-vector operand.
The trinary if-then-else operator.
Definition std_expr.h:2375
Array index operator.
Definition std_expr.h:1470
An expression denoting infinity.
Definition std_expr.h:3102
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
const componentst & components() const
Definition java_types.h:223
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
Definition java_types.h:563
void set_access(const irep_idt &access)
Definition java_types.h:327
std::vector< parametert > parameterst
Definition std_types.h:586
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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:2849
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
Boolean negation.
Definition std_expr.h:2332
Disequality.
Definition std_expr.h:1425
The null pointer constant.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
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:966
Struct constructor from list of elements.
Definition std_expr.h:1877
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition std_types.cpp:99
const typet & component_type(const irep_idt &component_name) const
Definition std_types.cpp:77
void set_tag(const irep_idt &tag)
Definition std_types.h:169
const componentst & components() const
Definition std_types.h:147
Expression to hold a symbol (variable)
Definition std_expr.h:131
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
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
bool is_static_lifetime
Definition symbol.h:70
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
const irep_idt & get_identifier() const
Definition std_types.h:410
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:484
std::optional< 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:44
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.
const symbol_exprt arg_this
Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primit...
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:183
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:581
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:1900
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:518
String expressions for the string solver.
Definition kdev_t.h:24
Author: Diffblue Ltd.
dstringt irep_idt