cprover
java_string_library_preprocess.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: 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 
8 Author: Romain Brenguier
9 
10 Date: April 2017
11 
12 \*******************************************************************/
13 
18 
20 
21 #include <util/allocate_objects.h>
22 #include <util/arith_tools.h>
23 #include <util/bitvector_expr.h>
24 #include <util/c_types.h>
25 #include <util/expr_initializer.h>
26 #include <util/floatbv_expr.h>
27 #include <util/fresh_symbol.h>
29 #include <util/std_code.h>
30 #include <util/std_expr.h>
31 #include <util/string_expr.h>
32 
33 #include "java_types.h"
34 #include "java_utils.h"
35 
37 #include "java_root_class.h"
38 
41 static irep_idt get_tag(const typet &type)
42 {
44  if(type.id() == ID_struct_tag)
45  return to_struct_tag_type(type).get_identifier();
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 &subtype=pt.subtype();
71  return is_java_string_type(subtype);
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 &subtype=pt.subtype();
102  return is_java_string_builder_type(subtype);
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 &subtype=pt.subtype();
125  return is_java_string_buffer_type(subtype);
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 &subtype=pt.subtype();
148  return is_java_char_sequence_type(subtype);
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 &subtype=pt.subtype();
171  return is_java_char_array_type(subtype);
172  }
173  return false;
174 }
175 
178 {
179  return java_int_type();
180 }
181 
186 std::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, symbol_tablet &symbol_table)
222 {
223  irep_idt class_symbol_name = "java::" + id2string(class_name);
224  symbolt tmp_string_symbol;
225  tmp_string_symbol.name = class_symbol_name;
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  string_symbol->is_type = true;
254  string_symbol->mode = ID_java;
255  }
256 
257  auto &string_type = to_java_class_type(string_symbol->type);
258 
259  string_type.components().resize(3);
260  const struct_tag_typet &supertype = string_type.bases().front().type();
261  irep_idt supertype_component_name =
262  "@" + id2string(supertype.get_identifier()).substr(6);
263  string_type.components()[0].set_name(supertype_component_name);
264  string_type.components()[0].set_pretty_name(supertype_component_name);
265  string_type.components()[0].type() = supertype;
266  string_type.components()[1].set_name("length");
267  string_type.components()[1].set_pretty_name("length");
268  string_type.components()[1].type()=string_length_type();
269  string_type.components()[2].set_name("data");
270  string_type.components()[2].set_pretty_name("data");
271  string_type.components()[2].type() = pointer_type(java_char_type());
272 }
273 
283  const java_method_typet::parameterst &params,
284  const source_locationt &loc,
285  const irep_idt &function_id,
286  symbol_table_baset &symbol_table,
287  code_blockt &init_code)
288 {
289  exprt::operandst ops;
290  for(const auto &p : params)
291  ops.emplace_back(symbol_exprt(p.get_identifier(), p.type()));
292  return process_operands(ops, loc, function_id, symbol_table, init_code);
293 }
294 
312  const exprt &expr_to_process,
313  const source_locationt &loc,
314  symbol_table_baset &symbol_table,
315  const irep_idt &function_id,
316  code_blockt &init_code)
317 {
319  const refined_string_exprt string_expr =
320  decl_string_expr(loc, function_id, symbol_table, init_code);
322  string_expr, expr_to_process, loc, symbol_table, init_code);
323  return string_expr;
324 }
325 
340  const exprt::operandst &operands,
341  const source_locationt &loc,
342  const irep_idt &function_id,
343  symbol_table_baset &symbol_table,
344  code_blockt &init_code)
345 {
346  exprt::operandst ops;
347  for(const auto &p : operands)
348  {
350  {
351  init_code.add(code_assumet(
353  ops.push_back(convert_exprt_to_string_exprt(
354  p, loc, symbol_table, function_id, init_code));
355  }
356  else if(is_java_char_array_pointer_type(p.type()))
357  ops.push_back(
358  replace_char_array(p, loc, function_id, symbol_table, init_code));
359  else
360  ops.push_back(p);
361  }
362  return ops;
363 }
364 
369 static const typet &
370 get_data_type(const typet &type, const symbol_tablet &symbol_table)
371 {
372  PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
373  if(type.id() == ID_struct_tag)
374  {
375  const symbolt &sym =
376  symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
377  CHECK_RETURN(sym.type.id() != ID_struct_tag);
378  return get_data_type(sym.type, symbol_table);
379  }
380  // else type id is ID_struct
381  const struct_typet &struct_type=to_struct_type(type);
382  return struct_type.component_type("data");
383 }
384 
389 static const typet &
390 get_length_type(const typet &type, const symbol_tablet &symbol_table)
391 {
392  PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
393  if(type.id() == ID_struct_tag)
394  {
395  const symbolt &sym =
396  symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
397  CHECK_RETURN(sym.type.id() != ID_struct_tag);
398  return get_length_type(sym.type, symbol_table);
399  }
400  // else type id is ID_struct
401  const struct_typet &struct_type=to_struct_type(type);
402  return struct_type.component_type("length");
403 }
404 
409 static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
410 {
411  return member_exprt(
412  expr, "length", get_length_type(expr.type(), symbol_table));
413 }
414 
419 static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
420 {
421  return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
422 }
423 
433  const exprt &array_pointer,
434  const source_locationt &loc,
435  const irep_idt &function_id,
436  symbol_table_baset &symbol_table,
437  code_blockt &code)
438 {
439  // array is *array_pointer
440  const dereference_exprt array = checked_dereference(array_pointer);
441  // array_data is array_pointer-> data
442  const exprt array_data = get_data(array, symbol_table);
443  const symbolt &sym_char_array = fresh_java_symbol(
444  array_data.type(), "char_array", loc, function_id, symbol_table);
445  const symbol_exprt char_array = sym_char_array.symbol_expr();
446  // char_array = array_pointer->data
447  code.add(code_assignt(char_array, array_data), loc);
448 
449  // string_expr is `{ rhs->length; string_array }`
450  const refined_string_exprt string_expr(
451  get_length(array, symbol_table), char_array, refined_string_type);
452 
453  const dereference_exprt inf_array(
455 
457  string_expr.content(), inf_array, symbol_table, loc, function_id, code);
458 
459  return string_expr;
460 }
461 
470  const typet &type,
471  const source_locationt &loc,
472  const irep_idt &function_id,
473  symbol_table_baset &symbol_table)
474 {
475  symbolt string_symbol =
476  fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
477  string_symbol.is_static_lifetime=true;
478  return string_symbol.symbol_expr();
479 }
480 
489  const source_locationt &loc,
490  const irep_idt &function_id,
491  symbol_table_baset &symbol_table,
492  code_blockt &code)
493 {
494  const symbolt &sym_length = fresh_java_symbol(
495  index_type, "cprover_string_length", loc, function_id, symbol_table);
496  const symbol_exprt length_field = sym_length.symbol_expr();
497  const pointer_typet array_type = pointer_type(java_char_type());
498  const symbolt &sym_content = fresh_java_symbol(
499  array_type, "cprover_string_content", loc, function_id, symbol_table);
500  const symbol_exprt content_field = sym_content.symbol_expr();
501  code.add(code_declt(content_field), loc);
502  code.add(code_declt{length_field}, loc);
503  return refined_string_exprt{length_field, content_field, refined_string_type};
504 }
505 
514  const source_locationt &loc,
515  const irep_idt &function_id,
516  symbol_table_baset &symbol_table,
517  code_blockt &code)
518 {
520  const refined_string_exprt str =
521  decl_string_expr(loc, function_id, symbol_table, code);
522 
523  const side_effect_expr_nondett nondet_length(str.length().type(), loc);
524  code.add(code_assignt(str.length(), nondet_length), loc);
525 
526  const exprt nondet_array_expr =
527  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
528 
529  const address_of_exprt array_pointer(
530  index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
531 
533  array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
534 
536  nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
537 
538  code.add(code_assignt(str.content(), array_pointer), loc);
539 
540  return refined_string_exprt(str.length(), str.content());
541 }
542 
551  const typet &type,
552  const source_locationt &loc,
553  const irep_idt &function_id,
554  symbol_table_baset &symbol_table,
555  code_blockt &code)
556 {
557  const exprt str = fresh_string(type, loc, function_id, symbol_table);
558 
559  allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
560 
561  code_blockt tmp;
562  allocate_objects.allocate_dynamic_object(tmp, str, str.type().subtype());
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(
759  java_int_type(),
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 
807  if(is_constructor)
808  {
809  // Initialise the supertype with the appropriate classid:
810  namespacet ns(symbol_table);
811  const struct_typet &lhs_type = to_struct_type(ns.follow(deref.type()));
812  auto zero_base_object = *zero_initializer(
813  lhs_type.components().front().type(), source_locationt{}, ns);
815  to_struct_expr(zero_base_object), ns, to_struct_tag_type(deref.type()));
816  struct_exprt struct_rhs(
817  {zero_base_object, rhs_length, rhs_array}, deref.type());
818  return code_assignt(checked_dereference(lhs), struct_rhs);
819  }
820  else
821  {
822  return code_blockt(
823  {code_assignt(get_length(deref, symbol_table), rhs_length),
824  code_assignt(get_data(deref, symbol_table), rhs_array)});
825  }
826 }
827 
840  const exprt &lhs,
841  const refined_string_exprt &rhs,
842  const symbol_table_baset &symbol_table,
843  bool is_constructor)
844 {
846  lhs, rhs.content(), rhs.length(), symbol_table, is_constructor);
847 }
848 
859  const refined_string_exprt &lhs,
860  const exprt &rhs,
861  const source_locationt &loc,
862  const symbol_table_baset &symbol_table,
863  code_blockt &code)
864 {
866 
867  const dereference_exprt deref = checked_dereference(rhs);
868 
869  // Although we should not reach this code if rhs is null, the association
870  // `pointer -> length` is added to the solver anyway, so we have to make sure
871  // the length is set to something reasonable.
872  auto rhs_length = if_exprt(
874  from_integer(0, lhs.length().type()),
875  get_length(deref, symbol_table));
876  rhs_length.set(ID_mode, ID_java);
877 
878  // Assignments
879  code.add(code_assignt(lhs.length(), rhs_length), loc);
880  exprt data_as_array = get_data(deref, symbol_table);
881  code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc);
882 }
883 
896  const std::string &s,
897  const source_locationt &loc,
898  symbol_table_baset &symbol_table,
899  code_blockt &code)
900 {
902  ID_cprover_string_literal_func,
904  loc,
905  symbol_table,
906  code);
907 }
908 
917  const java_method_typet &type,
918  const source_locationt &loc,
919  const irep_idt &function_id,
920  symbol_table_baset &symbol_table,
921  message_handlert &message_handler)
922 {
923  (void)message_handler;
924 
925  // Getting the argument
927  PRECONDITION(params.size()==1);
928  PRECONDITION(!params[0].get_identifier().empty());
929  const symbol_exprt arg(params[0].get_identifier(), params[0].type());
930 
931  // Holder for output code
932  code_blockt code;
933 
934  // Declaring and allocating String * str
935  const exprt str = allocate_fresh_string(
936  type.return_type(), loc, function_id, symbol_table, code);
937 
938  // Expression representing 0.0
939  const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
940  ieee_floatt zero_float(float_spec);
941  zero_float.from_float(0.0);
942  const constant_exprt zero = zero_float.to_expr();
943 
944  // For each possible case with have a condition and a string_exprt
945  std::vector<exprt> condition_list;
946  std::vector<refined_string_exprt> string_expr_list;
947 
948  // Case of computerized scientific notation
949  condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
950  const refined_string_exprt sci_notation = string_expr_of_function(
951  ID_cprover_string_of_float_scientific_notation_func,
952  {arg},
953  loc,
954  symbol_table,
955  code);
956  string_expr_list.push_back(sci_notation);
957 
958  // Subcase of negative scientific notation
959  condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
960  const refined_string_exprt minus_sign =
961  string_literal_to_string_expr("-", loc, symbol_table, code);
962  const refined_string_exprt neg_sci_notation = string_expr_of_function(
963  ID_cprover_string_concat_func,
964  {minus_sign, sci_notation},
965  loc,
966  symbol_table,
967  code);
968  string_expr_list.push_back(neg_sci_notation);
969 
970  // Case of NaN
971  condition_list.push_back(isnan_exprt(arg));
972  const refined_string_exprt nan =
973  string_literal_to_string_expr("NaN", loc, symbol_table, code);
974  string_expr_list.push_back(nan);
975 
976  // Case of Infinity
977  extractbit_exprt is_neg(arg, float_spec.width()-1);
978  condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
979  const refined_string_exprt infinity =
980  string_literal_to_string_expr("Infinity", loc, symbol_table, code);
981  string_expr_list.push_back(infinity);
982 
983  // Case -Infinity
984  condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
985  const refined_string_exprt minus_infinity =
986  string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
987  string_expr_list.push_back(minus_infinity);
988 
989  // Case of 0.0
990  // Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt,
991  // the latter disregards the sign
992  condition_list.push_back(equal_exprt(arg, zero));
993  const refined_string_exprt zero_string =
994  string_literal_to_string_expr("0.0", loc, symbol_table, code);
995  string_expr_list.push_back(zero_string);
996 
997  // Case of -0.0
998  ieee_floatt minus_zero_float(float_spec);
999  minus_zero_float.from_float(-0.0f);
1000  condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
1001  const refined_string_exprt minus_zero_string =
1002  string_literal_to_string_expr("-0.0", loc, symbol_table, code);
1003  string_expr_list.push_back(minus_zero_string);
1004 
1005  // Case of simple notation
1006  ieee_floatt bound_inf_float(float_spec);
1007  ieee_floatt bound_sup_float(float_spec);
1008  bound_inf_float.from_float(1e-3f);
1009  bound_sup_float.from_float(1e7f);
1010  bound_inf_float.change_spec(float_spec);
1011  bound_sup_float.change_spec(float_spec);
1012  const constant_exprt bound_inf = bound_inf_float.to_expr();
1013  const constant_exprt bound_sup = bound_sup_float.to_expr();
1014 
1015  const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf),
1016  binary_relation_exprt(arg, ID_lt, bound_sup)};
1017  condition_list.push_back(is_simple_float);
1018 
1019  const refined_string_exprt simple_notation = string_expr_of_function(
1020  ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1021  string_expr_list.push_back(simple_notation);
1022 
1023  // Case of a negative number in simple notation
1024  const and_exprt is_neg_simple_float{
1025  binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
1026  binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))};
1027  condition_list.push_back(is_neg_simple_float);
1028 
1029  const refined_string_exprt neg_simple_notation = string_expr_of_function(
1030  ID_cprover_string_concat_func,
1031  {minus_sign, simple_notation},
1032  loc,
1033  symbol_table,
1034  code);
1035  string_expr_list.push_back(neg_simple_notation);
1036 
1037  // Combining all cases
1038  INVARIANT(
1039  string_expr_list.size()==condition_list.size(),
1040  "number of created strings should correspond to number of conditions");
1041 
1042  // We do not check the condition of the first element in the list as it
1043  // will be reached only if all other conditions are not satisfied.
1045  str, string_expr_list[0], symbol_table, true);
1046  for(std::size_t i=1; i<condition_list.size(); i++)
1047  {
1048  tmp_code = code_ifthenelset(
1049  condition_list[i],
1051  str, string_expr_list[i], symbol_table, true),
1052  tmp_code);
1053  }
1054  code.add(tmp_code, loc);
1055 
1056  // Return str
1057  code.add(code_returnt(str), loc);
1058  return code;
1059 }
1060 
1077  const irep_idt &function_id,
1078  const java_method_typet &type,
1079  const source_locationt &loc,
1080  symbol_table_baset &symbol_table,
1081  bool is_constructor)
1082 {
1084 
1085  // The first parameter is the object to be initialized
1086  PRECONDITION(!params.empty());
1087  PRECONDITION(!params[0].get_identifier().empty());
1088  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1089  if(is_constructor)
1090  params.erase(params.begin());
1091 
1092  // Holder for output code
1093  code_blockt code;
1094 
1095  // Processing parameters
1096  const exprt::operandst args =
1097  process_parameters(params, loc, function_id, symbol_table, code);
1098 
1099  // string_expr <- function(arg1)
1100  const refined_string_exprt string_expr =
1101  string_expr_of_function(function_id, args, loc, symbol_table, code);
1102 
1103  // arg_this <- string_expr
1104  code.add(
1106  arg_this, string_expr, symbol_table, is_constructor),
1107  loc);
1108 
1109  return code;
1110 }
1111 
1121  const irep_idt &function_id,
1122  const java_method_typet &type,
1123  const source_locationt &loc,
1124  symbol_table_baset &symbol_table)
1125 {
1126  // This is similar to assign functions except we return a pointer to `this`
1127  const java_method_typet::parameterst &params = type.parameters();
1128  PRECONDITION(!params.empty());
1129  PRECONDITION(!params[0].get_identifier().empty());
1130  code_blockt code;
1131  code.add(
1132  make_assign_function_from_call(function_id, type, loc, symbol_table), loc);
1133  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1134  code.add(code_returnt(arg_this), loc);
1135  return code;
1136 }
1137 
1146  const irep_idt &function_id,
1147  const java_method_typet &type,
1148  const source_locationt &loc,
1149  symbol_table_baset &symbol_table)
1150 {
1151  // This is similar to initialization function except we do not ignore
1152  // the first argument
1154  function_id, type, loc, symbol_table, false);
1155 }
1156 
1170  const java_method_typet &type,
1171  const source_locationt &loc,
1172  const irep_idt &function_id,
1173  symbol_table_baset &symbol_table,
1174  message_handlert &message_handler)
1175 {
1177  PRECONDITION(!params.empty());
1178  PRECONDITION(!params[0].get_identifier().empty());
1179  const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1180 
1181  // Code to be returned
1182  code_blockt code;
1183 
1184  // class_identifier is obj->@class_identifier
1185  const member_exprt class_identifier{
1187 
1188  // string_expr = cprover_string_literal(this->@class_identifier)
1189  const refined_string_exprt string_expr = string_expr_of_function(
1190  ID_cprover_string_literal_func,
1191  {class_identifier},
1192  loc,
1193  symbol_table,
1194  code);
1195 
1196  // string_expr1 = substr(string_expr, 6)
1197  // We do this to remove the "java::" prefix
1198  const refined_string_exprt string_expr1 = string_expr_of_function(
1199  ID_cprover_string_substring_func,
1200  {string_expr, from_integer(6, java_int_type())},
1201  loc,
1202  symbol_table,
1203  code);
1204 
1205  // string1 = (String*) string_expr
1206  const typet &string_ptr_type = type.return_type();
1207  const exprt string1 = allocate_fresh_string(
1208  string_ptr_type, loc, function_id, symbol_table, code);
1209  code.add(
1211  string1, string_expr1, symbol_table, true),
1212  loc);
1213 
1214  // > return string1;
1215  code.add(code_returnt{string1}, loc);
1216  return code;
1217 }
1218 
1230  const irep_idt &function_id,
1231  const java_method_typet &type,
1232  const source_locationt &loc,
1233  symbol_table_baset &symbol_table)
1234 {
1235  code_blockt code;
1236  const exprt::operandst args =
1237  process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1238  code.add(
1240  function_id, args, type.return_type(), symbol_table),
1241  loc);
1242  return code;
1243 }
1244 
1260  const irep_idt &function_id,
1261  const java_method_typet &type,
1262  const source_locationt &loc,
1263  symbol_table_baset &symbol_table)
1264 {
1265  // Code for the output
1266  code_blockt code;
1267 
1268  // Calling the function
1269  const exprt::operandst arguments =
1270  process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1271 
1272  // String expression that will hold the result
1273  const refined_string_exprt string_expr =
1274  string_expr_of_function(function_id, arguments, loc, symbol_table, code);
1275 
1276  // Assign to string
1277  const exprt str = allocate_fresh_string(
1278  type.return_type(), loc, function_id, symbol_table, code);
1279  code.add(
1281  str, string_expr, symbol_table, true),
1282  loc);
1283 
1284  // Return value
1285  code.add(code_returnt(str), loc);
1286  return code;
1287 }
1288 
1305  const java_method_typet &type,
1306  const source_locationt &loc,
1307  const irep_idt &function_id,
1308  symbol_table_baset &symbol_table,
1309  message_handlert &message_handler)
1310 {
1311  (void)message_handler;
1312 
1313  // Code for the output
1314  code_blockt code;
1315 
1316  // String expression that will hold the result
1317  const refined_string_exprt string_expr =
1318  decl_string_expr(loc, function_id, symbol_table, code);
1319 
1320  // Assign the argument to string_expr
1321  const java_method_typet::parametert &op = type.parameters()[0];
1323  const symbol_exprt arg0{op.get_identifier(), op.type()};
1325  string_expr, arg0, loc, symbol_table, code);
1326 
1327  // Allocate and assign the string
1328  const exprt str = allocate_fresh_string(
1329  type.return_type(), loc, function_id, symbol_table, code);
1330  code.add(
1332  str, string_expr, symbol_table, true),
1333  loc);
1334 
1335  // Return value
1336  code.add(code_returnt(str), loc);
1337  return code;
1338 }
1339 
1355  const java_method_typet &type,
1356  const source_locationt &loc,
1357  const irep_idt &function_id,
1358  symbol_table_baset &symbol_table,
1359  message_handlert &message_handler)
1360 {
1361  (void)message_handler;
1362 
1363  code_blockt copy_constructor_body;
1364 
1365  // String expression that will hold the result
1366  const refined_string_exprt string_expr =
1367  decl_string_expr(loc, function_id, symbol_table, copy_constructor_body);
1368 
1369  // Assign argument to a string_expr
1370  const java_method_typet::parameterst &params = type.parameters();
1371  PRECONDITION(!params[0].get_identifier().empty());
1372  PRECONDITION(!params[1].get_identifier().empty());
1373  const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
1375  string_expr, arg1, loc, symbol_table, copy_constructor_body);
1376 
1377  // Assign string_expr to `this` object
1378  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1379  copy_constructor_body.add(
1381  arg_this, string_expr, symbol_table, true),
1382  loc);
1383 
1384  return copy_constructor_body;
1385 }
1386 
1400  const java_method_typet &type,
1401  const source_locationt &loc,
1402  const irep_idt &function_id,
1403  symbol_table_baset &symbol_table,
1404  message_handlert &message_handler)
1405 {
1406  (void)function_id;
1407  (void)message_handler;
1408 
1409  const java_method_typet::parameterst &params = type.parameters();
1410  PRECONDITION(!params[0].get_identifier().empty());
1411  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1412  const dereference_exprt deref = checked_dereference(arg_this);
1413 
1414  code_returnt ret(get_length(deref, symbol_table));
1415  ret.add_source_location() = loc;
1416 
1417  return ret;
1418 }
1419 
1421  const irep_idt &function_id) const
1422 {
1423  for(const id_mapt *map : id_maps)
1424  if(map->count(function_id) != 0)
1425  return true;
1426 
1427  return conversion_table.count(function_id) != 0;
1428 }
1429 
1430 template <typename TMap, typename TContainer>
1431 void add_keys_to_container(const TMap &map, TContainer &container)
1432 {
1433  static_assert(
1434  std::is_same<typename TMap::key_type,
1435  typename TContainer::value_type>::value,
1436  "TContainer value_type doesn't match TMap key_type");
1437  std::transform(
1438  map.begin(),
1439  map.end(),
1440  std::inserter(container, container.begin()),
1441  [](const typename TMap::value_type &pair) { return pair.first; });
1442 }
1443 
1445  std::unordered_set<irep_idt> &methods) const
1446 {
1447  for(const id_mapt *map : id_maps)
1448  add_keys_to_container(*map, methods);
1449 
1451 }
1452 
1461  const symbolt &symbol,
1462  symbol_table_baset &symbol_table,
1463  message_handlert &message_handler)
1464 {
1465  const irep_idt &function_id = symbol.name;
1466  const java_method_typet &type = to_java_method_type(symbol.type);
1467  const source_locationt &loc = symbol.location;
1468  auto it_id=cprover_equivalent_to_java_function.find(function_id);
1469  if(it_id!=cprover_equivalent_to_java_function.end())
1470  return make_function_from_call(it_id->second, type, loc, symbol_table);
1471 
1475  it_id->second, type, loc, symbol_table);
1476 
1477  it_id=cprover_equivalent_to_java_constructor.find(function_id);
1480  it_id->second, type, loc, symbol_table);
1481 
1485  it_id->second, type, loc, symbol_table);
1486 
1487  it_id=cprover_equivalent_to_java_assign_function.find(function_id);
1490  it_id->second, type, loc, symbol_table);
1491 
1492  auto it=conversion_table.find(function_id);
1493  INVARIANT(
1494  it != conversion_table.end(), "Couldn't retrieve code for string method");
1495 
1496  return it->second(type, loc, function_id, symbol_table, message_handler);
1497 }
1498 
1504  irep_idt class_name)
1505 {
1506  return string_types.find(class_name)!=string_types.end();
1507 }
1508 
1510 {
1511  string_types = std::unordered_set<irep_idt>{"java.lang.String",
1512  "java.lang.StringBuilder",
1513  "java.lang.CharSequence",
1514  "java.lang.StringBuffer"};
1515 }
1516 
1519 {
1521 
1522  // The following list of function is organized by libraries, with
1523  // constructors first and then methods in alphabetic order.
1524  // Methods that are not supported here should ultimately have Java models
1525  // provided for them in the class-path.
1526 
1527  // CProverString library
1529  ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1530  "lang/CharSequence;II)"
1531  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1532  // CProverString.charAt differs from the Java String.charAt in that no
1533  // exception is raised for the out of bounds case.
1535  ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1536  ID_cprover_string_char_at_func;
1538  ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1539  ID_cprover_string_char_at_func;
1541  ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1542  ID_cprover_string_code_point_at_func;
1544  ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1545  ID_cprover_string_code_point_before_func;
1547  ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1548  ID_cprover_string_code_point_count_func;
1550  ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1551  "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1553  ["java::org.cprover.CProverString.delete:(Ljava/lang/"
1554  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1555  ID_cprover_string_delete_func;
1557  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1558  "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1559  ID_cprover_string_delete_char_at_func;
1561  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1562  "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1563  ID_cprover_string_delete_char_at_func;
1564 
1565  std::string format_signature = "java::org.cprover.CProverString.format:(";
1566  for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1567  format_signature += "Ljava/lang/String;";
1568  format_signature += ")Ljava/lang/String;";
1570  ID_cprover_string_format_func;
1571 
1573  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1574  "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1576  ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1577  "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1579  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1580  "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1582  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1583  "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1585  ["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1586  ID_cprover_string_set_length_func;
1588  ["java::org.cprover.CProverString.setLength:(Ljava/lang/"
1589  "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1591  ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1592  "lang/CharSequence;"] = ID_cprover_string_substring_func;
1593  // CProverString.substring differs from the Java String.substring in that no
1594  // exception is raised for the out of bounds case.
1596  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1597  "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1599  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1600  "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1602  ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
1603  "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1605  ["java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1606  ID_cprover_string_of_int_func;
1608  ["java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1609  ID_cprover_string_of_int_func;
1611  ["java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1612  ID_cprover_string_of_long_func;
1614  ["java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1615  ID_cprover_string_of_long_func;
1617  ["java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1618  std::bind(
1620  this,
1621  std::placeholders::_1,
1622  std::placeholders::_2,
1623  std::placeholders::_3,
1624  std::placeholders::_4,
1625  std::placeholders::_5);
1627  ["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1628  ID_cprover_string_parse_int_func;
1630  ["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1631  ID_cprover_string_parse_int_func;
1633  ["java::org.cprover.CProverString.isValidInt:(Ljava/lang/String;I)Z"] =
1634  ID_cprover_string_is_valid_int_func;
1636  ["java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z"] =
1637  ID_cprover_string_is_valid_long_func;
1638 
1639  // String library
1640  conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1641  std::bind(
1643  this,
1644  std::placeholders::_1,
1645  std::placeholders::_2,
1646  std::placeholders::_3,
1647  std::placeholders::_4,
1648  std::placeholders::_5);
1650  ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1652  this,
1653  std::placeholders::_1,
1654  std::placeholders::_2,
1655  std::placeholders::_3,
1656  std::placeholders::_4,
1657  std::placeholders::_5);
1659  ["java::java.lang.String.<init>:()V"]=
1660  ID_cprover_string_empty_string_func;
1661 
1663  ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1664  ID_cprover_string_compare_to_func;
1666  ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1667  ID_cprover_string_concat_func;
1669  ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1670  ID_cprover_string_contains_func;
1672  ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1673  ID_cprover_string_endswith_func;
1675  ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1676  ID_cprover_string_equals_ignore_case_func;
1677 
1679  ["java::java.lang.String.indexOf:(I)I"]=
1680  ID_cprover_string_index_of_func;
1682  ["java::java.lang.String.indexOf:(II)I"]=
1683  ID_cprover_string_index_of_func;
1685  ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1686  ID_cprover_string_index_of_func;
1688  ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1689  ID_cprover_string_index_of_func;
1691  ["java::java.lang.String.isEmpty:()Z"]=
1692  ID_cprover_string_is_empty_func;
1694  ["java::java.lang.String.lastIndexOf:(I)I"]=
1695  ID_cprover_string_last_index_of_func;
1697  ["java::java.lang.String.lastIndexOf:(II)I"]=
1698  ID_cprover_string_last_index_of_func;
1700  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1701  ID_cprover_string_last_index_of_func;
1703  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1704  ID_cprover_string_last_index_of_func;
1705  conversion_table["java::java.lang.String.length:()I"] = std::bind(
1707  this,
1708  std::placeholders::_1,
1709  std::placeholders::_2,
1710  std::placeholders::_3,
1711  std::placeholders::_4,
1712  std::placeholders::_5);
1714  ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1715  ID_cprover_string_replace_func;
1717  ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
1718  ID_cprover_string_replace_func;
1720  ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1721  ID_cprover_string_startswith_func;
1723  ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1724  ID_cprover_string_startswith_func;
1726  ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1727  ID_cprover_string_to_lower_case_func;
1728  conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
1729  std::bind(
1731  this,
1732  std::placeholders::_1,
1733  std::placeholders::_2,
1734  std::placeholders::_3,
1735  std::placeholders::_4,
1736  std::placeholders::_5);
1738  ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1739  ID_cprover_string_to_upper_case_func;
1741  ["java::java.lang.String.trim:()Ljava/lang/String;"]=
1742  ID_cprover_string_trim_func;
1743 
1744  // StringBuilder library
1746  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1748  this,
1749  std::placeholders::_1,
1750  std::placeholders::_2,
1751  std::placeholders::_3,
1752  std::placeholders::_4,
1753  std::placeholders::_5);
1755  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1756  std::bind(
1758  this,
1759  std::placeholders::_1,
1760  std::placeholders::_2,
1761  std::placeholders::_3,
1762  std::placeholders::_4,
1763  std::placeholders::_5);
1765  ["java::java.lang.StringBuilder.<init>:()V"]=
1766  ID_cprover_string_empty_string_func;
1768  ["java::java.lang.StringBuilder.<init>:(I)V"] =
1769  ID_cprover_string_empty_string_func;
1770 
1772  ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1773  ID_cprover_string_concat_char_func;
1775  ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1776  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1778  ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1779  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1781  ["java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1782  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1784  ["java::java.lang.StringBuilder.appendCodePoint:(I)"
1785  "Ljava/lang/StringBuilder;"]=
1786  ID_cprover_string_concat_code_point_func;
1788  ["java::java.lang.StringBuilder.charAt:(I)C"]=
1789  ID_cprover_string_char_at_func;
1791  ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
1792  ID_cprover_string_code_point_at_func;
1794  ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1795  ID_cprover_string_code_point_before_func;
1797  ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
1798  ID_cprover_string_code_point_count_func;
1799  conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
1801  this,
1802  std::placeholders::_1,
1803  std::placeholders::_2,
1804  std::placeholders::_3,
1805  std::placeholders::_4,
1806  std::placeholders::_5);
1808  ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1809  ID_cprover_string_substring_func;
1811  ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1812  ID_cprover_string_substring_func;
1814  ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1816  this,
1817  std::placeholders::_1,
1818  std::placeholders::_2,
1819  std::placeholders::_3,
1820  std::placeholders::_4,
1821  std::placeholders::_5);
1822 
1823  // StringBuffer library
1825  ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1827  this,
1828  std::placeholders::_1,
1829  std::placeholders::_2,
1830  std::placeholders::_3,
1831  std::placeholders::_4,
1832  std::placeholders::_5);
1834  ["java::java.lang.StringBuffer.<init>:()V"]=
1835  ID_cprover_string_empty_string_func;
1836 
1838  ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1839  ID_cprover_string_concat_char_func;
1841  ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1842  "Ljava/lang/StringBuffer;"]=
1843  ID_cprover_string_concat_func;
1845  ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1846  "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1848  ["java::java.lang.StringBuffer.appendCodePoint:(I)"
1849  "Ljava/lang/StringBuffer;"]=
1850  ID_cprover_string_concat_code_point_func;
1852  ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
1853  ID_cprover_string_code_point_at_func;
1855  ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1856  ID_cprover_string_code_point_before_func;
1858  ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
1859  ID_cprover_string_code_point_count_func;
1861  ["java::java.lang.StringBuffer.length:()I"]=
1862  conversion_table["java::java.lang.String.length:()I"];
1864  ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1865  ID_cprover_string_substring_func;
1867  ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1869  this,
1870  std::placeholders::_1,
1871  std::placeholders::_2,
1872  std::placeholders::_3,
1873  std::placeholders::_4,
1874  std::placeholders::_5);
1875 
1876  // CharSequence library
1878  ["java::java.lang.CharSequence.charAt:(I)C"]=
1879  ID_cprover_string_char_at_func;
1881  ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1883  this,
1884  std::placeholders::_1,
1885  std::placeholders::_2,
1886  std::placeholders::_3,
1887  std::placeholders::_4,
1888  std::placeholders::_5);
1890  ["java::java.lang.CharSequence.length:()I"]=
1891  conversion_table["java::java.lang.String.length:()I"];
1892 
1893  // Other libraries
1895  ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1896  ID_cprover_string_of_int_hex_func;
1898  ["java::org.cprover.CProver.classIdentifier:("
1899  "Ljava/lang/Object;)Ljava/lang/String;"] =
1900  std::bind(
1902  this,
1903  std::placeholders::_1,
1904  std::placeholders::_2,
1905  std::placeholders::_3,
1906  std::placeholders::_4,
1907  std::placeholders::_5);
1908 }
code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
API to expression classes for bitvectors.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
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.
Definition: pointer_expr.h:200
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:1835
Arrays with given size.
Definition: std_types.h:968
const exprt & size() const
Definition: std_types.h:976
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
A codet representing an assignment in the program.
Definition: std_code.h:295
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
A codet representing sequential composition of program statements.
Definition: std_code.h:170
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:88
void add(const codet &code)
Definition: std_code.h:208
A codet representing the declaration of a local variable.
Definition: std_code.h:402
codet representation of an if-then-else statement.
Definition: std_code.h:778
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
const irep_idt & get_identifier() const
Definition: std_types.h:795
std::vector< parametert > parameterst
Definition: std_types.h:746
const typet & return_type() const
Definition: std_types.h:850
const parameterst & parameters() const
Definition: std_types.h:860
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
A constant literal expression.
Definition: std_expr.h:2668
Operator to dereference a pointer.
Definition: pointer_expr.h:256
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:1140
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:239
typet & type()
Return the type of the expression.
Definition: expr.h:82
Extracts a single bit of a bit-vector operand.
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
void from_float(const float f)
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition: std_expr.h:2087
Array index operator.
Definition: std_expr.h:1243
An expression denoting infinity.
Definition: std_expr.h:2762
const irep_idt & id() const
Definition: irep.h:407
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
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:566
void set_access(const irep_idt &access)
Definition: java_types.h:330
const componentst & components() const
Definition: java_types.h:226
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:2528
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Boolean negation.
Definition: std_expr.h:2042
Disequality.
Definition: std_expr.h:1198
The null pointer constant.
Definition: std_expr.h:2751
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
const exprt & length() const
Definition: string_expr.h:128
const exprt & content() const
Definition: string_expr.h:138
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
String type.
Definition: std_types.h:1669
Struct constructor from list of elements.
Definition: std_expr.h:1583
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:498
Structure type, corresponds to C style structs.
Definition: std_types.h:226
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:102
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:80
void set_tag(const irep_idt &tag)
Definition: std_types.h:164
const componentst & components() const
Definition: std_types.h:142
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
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.
Definition: symbol_table.h:20
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
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:65
bool is_type
Definition: symbol.h:61
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:122
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
irep_idt mode
Language mode.
Definition: symbol.h:49
const irep_idt & get_identifier() const
Definition: std_types.h:459
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
The unary minus expression.
Definition: std_expr.h:391
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.
Fresh auxiliary symbol creation.
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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 const typet & get_data_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the data 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
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.
#define MAX_FORMAT_ARGS
signedbv_typet java_int_type()
Definition: java_types.cpp:32
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
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)
Definition: java_utils.cpp:558
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:284
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.
Definition: java_utils.cpp:387
Type for string expressions used by the string solver.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1606
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
String expressions for the string solver.
Definition: kdev_t.h:24