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 #include <util/allocate_objects.h>
21 #include <util/arith_tools.h>
22 #include <util/c_types.h>
23 #include <util/expr_initializer.h>
24 #include <util/fresh_symbol.h>
26 #include <util/std_code.h>
27 #include <util/std_expr.h>
28 #include <util/string_expr.h>
29 
30 #include "java_types.h"
31 #include "java_utils.h"
32 
34 #include "java_root_class.h"
35 
38 static irep_idt get_tag(const typet &type)
39 {
41  if(type.id() == ID_struct_tag)
42  return to_struct_tag_type(type).get_identifier();
43  else if(type.id() == ID_struct)
44  return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
45  else
46  return irep_idt();
47 }
48 
54  const typet &type, const std::string &tag)
55 {
56  return irep_idt("java::" + tag) == get_tag(type);
57 }
58 
62  const typet &type)
63 {
64  if(type.id()==ID_pointer)
65  {
66  const pointer_typet &pt=to_pointer_type(type);
67  const typet &subtype=pt.subtype();
68  return is_java_string_type(subtype);
69  }
70  return false;
71 }
72 
76  const typet &type)
77 {
78  return java_type_matches_tag(type, "java.lang.String");
79 }
80 
84  const typet &type)
85 {
86  return java_type_matches_tag(type, "java.lang.StringBuilder");
87 }
88 
93  const typet &type)
94 {
95  if(type.id()==ID_pointer)
96  {
97  const pointer_typet &pt=to_pointer_type(type);
98  const typet &subtype=pt.subtype();
99  return is_java_string_builder_type(subtype);
100  }
101  return false;
102 }
103 
107  const typet &type)
108 {
109  return java_type_matches_tag(type, "java.lang.StringBuffer");
110 }
111 
116  const typet &type)
117 {
118  if(type.id()==ID_pointer)
119  {
120  const pointer_typet &pt=to_pointer_type(type);
121  const typet &subtype=pt.subtype();
122  return is_java_string_buffer_type(subtype);
123  }
124  return false;
125 }
126 
130  const typet &type)
131 {
132  return java_type_matches_tag(type, "java.lang.CharSequence");
133 }
134 
139  const typet &type)
140 {
141  if(type.id()==ID_pointer)
142  {
143  const pointer_typet &pt=to_pointer_type(type);
144  const typet &subtype=pt.subtype();
145  return is_java_char_sequence_type(subtype);
146  }
147  return false;
148 }
149 
153  const typet &type)
154 {
155  return java_type_matches_tag(type, "array[char]");
156 }
157 
162  const typet &type)
163 {
164  if(type.id()==ID_pointer)
165  {
166  const pointer_typet &pt=to_pointer_type(type);
167  const typet &subtype=pt.subtype();
168  return is_java_char_array_type(subtype);
169  }
170  return false;
171 }
172 
175 {
176  return java_int_type();
177 }
178 
183 std::vector<irep_idt>
185  const irep_idt &class_name)
186 {
187  if(!is_known_string_type(class_name))
188  return {};
189 
190  std::vector<irep_idt> bases;
191  bases.reserve(3);
192 
193  // StringBuilder and StringBuffer derive from AbstractStringBuilder;
194  // other String types (String and CharSequence) derive directly from Object.
195  if(
196  class_name == "java.lang.StringBuilder" ||
197  class_name == "java.lang.StringBuffer")
198  bases.push_back("java.lang.AbstractStringBuilder");
199  else
200  bases.push_back("java.lang.Object");
201 
202  // Interfaces:
203  if(class_name != "java.lang.CharSequence")
204  {
205  bases.push_back("java.io.Serializable");
206  bases.push_back("java.lang.CharSequence");
207  }
208  if(class_name == "java.lang.String")
209  bases.push_back("java.lang.Comparable");
210 
211  return bases;
212 }
213 
218  const irep_idt &class_name, symbol_tablet &symbol_table)
219 {
220  irep_idt class_symbol_name = "java::" + id2string(class_name);
221  symbolt tmp_string_symbol;
222  tmp_string_symbol.name = class_symbol_name;
223  symbolt *string_symbol = nullptr;
224  bool already_exists = symbol_table.move(tmp_string_symbol, string_symbol);
225 
226  if(already_exists)
227  {
228  // A library has already defined this type -- we'll replace its
229  // components with those required for internal string modelling, but
230  // otherwise leave it alone.
231  to_java_class_type(string_symbol->type).components().clear();
232  }
233  else
234  {
235  // No definition of this type exists -- define it as it usually occurs in
236  // the JDK:
237  java_class_typet new_string_type;
238  new_string_type.set_tag(class_name);
239  new_string_type.set_name(class_symbol_name);
240  new_string_type.set_access(ID_public);
241 
242  std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
243  for(const irep_idt &base_name : bases)
244  new_string_type.add_base(
245  struct_tag_typet("java::" + id2string(base_name)));
246 
247  string_symbol->base_name = id2string(class_name);
248  string_symbol->pretty_name = id2string(class_name);
249  string_symbol->type = new_string_type;
250  string_symbol->is_type = true;
251  string_symbol->mode = ID_java;
252  }
253 
254  auto &string_type = to_java_class_type(string_symbol->type);
255 
256  string_type.components().resize(3);
257  const struct_tag_typet &supertype = string_type.bases().front().type();
258  irep_idt supertype_component_name =
259  "@" + id2string(supertype.get_identifier()).substr(6);
260  string_type.components()[0].set_name(supertype_component_name);
261  string_type.components()[0].set_pretty_name(supertype_component_name);
262  string_type.components()[0].type() = supertype;
263  string_type.components()[1].set_name("length");
264  string_type.components()[1].set_pretty_name("length");
265  string_type.components()[1].type()=string_length_type();
266  string_type.components()[2].set_name("data");
267  string_type.components()[2].set_pretty_name("data");
268  string_type.components()[2].type() = pointer_type(java_char_type());
269 }
270 
280  const java_method_typet::parameterst &params,
281  const source_locationt &loc,
282  const irep_idt &function_id,
283  symbol_table_baset &symbol_table,
284  code_blockt &init_code)
285 {
286  exprt::operandst ops;
287  for(const auto &p : params)
288  ops.emplace_back(symbol_exprt(p.get_identifier(), p.type()));
289  return process_operands(ops, loc, function_id, symbol_table, init_code);
290 }
291 
309  const exprt &expr_to_process,
310  const source_locationt &loc,
311  symbol_table_baset &symbol_table,
312  const irep_idt &function_id,
313  code_blockt &init_code)
314 {
316  const refined_string_exprt string_expr =
317  decl_string_expr(loc, function_id, symbol_table, init_code);
319  string_expr, expr_to_process, loc, symbol_table, init_code);
320  return string_expr;
321 }
322 
337  const exprt::operandst &operands,
338  const source_locationt &loc,
339  const irep_idt &function_id,
340  symbol_table_baset &symbol_table,
341  code_blockt &init_code)
342 {
343  exprt::operandst ops;
344  for(const auto &p : operands)
345  {
347  {
348  init_code.add(code_assumet(
350  ops.push_back(convert_exprt_to_string_exprt(
351  p, loc, symbol_table, function_id, init_code));
352  }
353  else if(is_java_char_array_pointer_type(p.type()))
354  ops.push_back(
355  replace_char_array(p, loc, function_id, symbol_table, init_code));
356  else
357  ops.push_back(p);
358  }
359  return ops;
360 }
361 
366 static const typet &
367 get_data_type(const typet &type, const symbol_tablet &symbol_table)
368 {
369  PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
370  if(type.id() == ID_struct_tag)
371  {
372  const symbolt &sym =
373  symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
374  CHECK_RETURN(sym.type.id() != ID_struct_tag);
375  return get_data_type(sym.type, symbol_table);
376  }
377  // else type id is ID_struct
378  const struct_typet &struct_type=to_struct_type(type);
379  return struct_type.component_type("data");
380 }
381 
386 static const typet &
387 get_length_type(const typet &type, const symbol_tablet &symbol_table)
388 {
389  PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
390  if(type.id() == ID_struct_tag)
391  {
392  const symbolt &sym =
393  symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
394  CHECK_RETURN(sym.type.id() != ID_struct_tag);
395  return get_length_type(sym.type, symbol_table);
396  }
397  // else type id is ID_struct
398  const struct_typet &struct_type=to_struct_type(type);
399  return struct_type.component_type("length");
400 }
401 
406 static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
407 {
408  return member_exprt(
409  expr, "length", get_length_type(expr.type(), symbol_table));
410 }
411 
416 static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
417 {
418  return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
419 }
420 
430  const exprt &array_pointer,
431  const source_locationt &loc,
432  const irep_idt &function_id,
433  symbol_table_baset &symbol_table,
434  code_blockt &code)
435 {
436  // array is *array_pointer
437  const dereference_exprt array = checked_dereference(array_pointer);
438  // array_data is array_pointer-> data
439  const exprt array_data = get_data(array, symbol_table);
440  const symbolt &sym_char_array = fresh_java_symbol(
441  array_data.type(), "char_array", loc, function_id, symbol_table);
442  const symbol_exprt char_array = sym_char_array.symbol_expr();
443  // char_array = array_pointer->data
444  code.add(code_assignt(char_array, array_data), loc);
445 
446  // string_expr is `{ rhs->length; string_array }`
447  const refined_string_exprt string_expr(
448  get_length(array, symbol_table), char_array, refined_string_type);
449 
450  const dereference_exprt inf_array(
452 
454  string_expr.content(), inf_array, symbol_table, loc, function_id, code);
455 
456  return string_expr;
457 }
458 
467  const typet &type,
468  const source_locationt &loc,
469  const irep_idt &function_id,
470  symbol_table_baset &symbol_table)
471 {
472  symbolt string_symbol =
473  fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
474  string_symbol.is_static_lifetime=true;
475  return string_symbol.symbol_expr();
476 }
477 
486  const source_locationt &loc,
487  const irep_idt &function_id,
488  symbol_table_baset &symbol_table,
489  code_blockt &code)
490 {
491  const symbolt &sym_length = fresh_java_symbol(
492  index_type, "cprover_string_length", loc, function_id, symbol_table);
493  const symbol_exprt length_field = sym_length.symbol_expr();
494  const pointer_typet array_type = pointer_type(java_char_type());
495  const symbolt &sym_content = fresh_java_symbol(
496  array_type, "cprover_string_content", loc, function_id, symbol_table);
497  const symbol_exprt content_field = sym_content.symbol_expr();
498  code.add(code_declt(content_field), loc);
499  code.add(code_declt{length_field}, loc);
500  return refined_string_exprt{length_field, content_field, refined_string_type};
501 }
502 
511  const source_locationt &loc,
512  const irep_idt &function_id,
513  symbol_table_baset &symbol_table,
514  code_blockt &code)
515 {
517  const refined_string_exprt str =
518  decl_string_expr(loc, function_id, symbol_table, code);
519 
520  const side_effect_expr_nondett nondet_length(str.length().type(), loc);
521  code.add(code_assignt(str.length(), nondet_length), loc);
522 
523  const exprt nondet_array_expr =
524  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
525 
526  const address_of_exprt array_pointer(
527  index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
528 
530  array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
531 
533  nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
534 
535  code.add(code_assignt(str.content(), array_pointer), loc);
536 
537  return refined_string_exprt(str.length(), str.content());
538 }
539 
548  const typet &type,
549  const source_locationt &loc,
550  const irep_idt &function_id,
551  symbol_table_baset &symbol_table,
552  code_blockt &code)
553 {
554  const exprt str = fresh_string(type, loc, function_id, symbol_table);
555 
556  allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
557 
558  code_blockt tmp;
559  allocate_objects.allocate_dynamic_object(tmp, str, str.type().subtype());
560  allocate_objects.declare_created_symbols(code);
561  code.append(tmp);
562 
563  return str;
564 }
565 
576  const exprt &lhs,
577  const irep_idt &function_id,
578  const exprt::operandst &arguments,
579  symbol_table_baset &symbol_table)
580 {
581  return code_assignt(
582  lhs,
584  function_id, arguments, lhs.type(), symbol_table));
585 }
586 
597  const irep_idt &function_id,
598  const exprt::operandst &arguments,
599  const typet &type,
600  symbol_table_baset &symbol_table)
601 {
602  return code_returnt(
603  make_function_application(function_id, arguments, type, symbol_table));
604 }
605 
613  symbol_table_baset &symbol_table,
614  const source_locationt &loc,
615  const irep_idt &function_id,
616  code_blockt &code)
617 {
618  const array_typet array_type(
620  const symbolt data_sym = fresh_java_symbol(
621  pointer_type(array_type),
622  "nondet_infinite_array_pointer",
623  loc,
624  function_id,
625  symbol_table);
626 
627  const symbol_exprt data_pointer = data_sym.symbol_expr();
628  code.add(code_declt(data_pointer));
629  code.add(make_allocate_code(data_pointer, array_type.size()));
630  side_effect_expr_nondett nondet_data{array_type, loc};
631  dereference_exprt data{data_pointer};
632  code.add(code_assignt{data, std::move(nondet_data)}, loc);
633  return std::move(data);
634 }
635 
645  const exprt &pointer,
646  const exprt &array,
647  symbol_table_baset &symbol_table,
648  const source_locationt &loc,
649  const irep_idt &function_id,
650  code_blockt &code)
651 {
652  PRECONDITION(array.type().id() == ID_array);
653  PRECONDITION(pointer.type().id() == ID_pointer);
654  const symbolt &return_sym = fresh_java_symbol(
655  java_int_type(), "return_array", loc, function_id, symbol_table);
656  const auto return_expr = return_sym.symbol_expr();
657  code.add(code_declt(return_expr), loc);
658  code.add(
660  return_expr,
661  ID_cprover_associate_array_to_pointer_func,
662  {array, pointer},
663  symbol_table),
664  loc);
665 }
666 
676  const exprt &array,
677  const exprt &length,
678  symbol_table_baset &symbol_table,
679  const source_locationt &loc,
680  const irep_idt &function_id,
681  code_blockt &code)
682 {
683  const symbolt &return_sym = fresh_java_symbol(
684  java_int_type(), "return_array", loc, function_id, symbol_table);
685  const auto return_expr = return_sym.symbol_expr();
686  code.add(code_declt(return_expr), loc);
687  code.add(
689  return_expr,
690  ID_cprover_associate_length_to_array_func,
691  {array, length},
692  symbol_table),
693  loc);
694 }
695 
708  const exprt &pointer,
709  const exprt &length,
710  const irep_idt &char_range,
711  symbol_table_baset &symbol_table,
712  const source_locationt &loc,
713  const irep_idt &function_id,
714  code_blockt &code)
715 {
716  PRECONDITION(pointer.type().id() == ID_pointer);
717  const symbolt &return_sym = fresh_java_symbol(
718  java_int_type(), "cnstr_added", loc, function_id, symbol_table);
719  const auto return_expr = return_sym.symbol_expr();
720  code.add(code_declt(return_expr), loc);
721  const constant_exprt char_set_expr(char_range, string_typet());
722  code.add(
724  return_expr,
725  ID_cprover_string_constrain_characters_func,
726  {length, pointer, char_set_expr},
727  symbol_table),
728  loc);
729 }
730 
748  const irep_idt &function_id,
749  const exprt::operandst &arguments,
750  const source_locationt &loc,
751  symbol_table_baset &symbol_table,
752  code_blockt &code)
753 {
754  // int return_code;
755  const symbolt return_code_sym = fresh_java_symbol(
756  java_int_type(),
757  std::string("return_code_") + function_id.c_str(),
758  loc,
759  function_id,
760  symbol_table);
761  const auto return_code = return_code_sym.symbol_expr();
762  code.add(code_declt(return_code), loc);
763 
764  const refined_string_exprt string_expr =
765  make_nondet_string_expr(loc, function_id, symbol_table, code);
766 
767  // args is { str.length, str.content, arguments... }
768  exprt::operandst args;
769  args.push_back(string_expr.length());
770  args.push_back(string_expr.content());
771  args.insert(args.end(), arguments.begin(), arguments.end());
772 
773  // return_code = <function_id>_data(args)
774  code.add(
776  return_code, function_id, args, symbol_table),
777  loc);
778 
779  return string_expr;
780 }
781 
795  const exprt &lhs,
796  const exprt &rhs_array,
797  const exprt &rhs_length,
798  const symbol_table_baset &symbol_table,
799  bool is_constructor)
800 {
803 
804  if(is_constructor)
805  {
806  // Initialise the supertype with the appropriate classid:
807  namespacet ns(symbol_table);
808  const struct_typet &lhs_type = to_struct_type(ns.follow(deref.type()));
809  auto zero_base_object = *zero_initializer(
810  lhs_type.components().front().type(), source_locationt{}, ns);
812  to_struct_expr(zero_base_object), ns, to_struct_tag_type(deref.type()));
813  struct_exprt struct_rhs(
814  {zero_base_object, rhs_length, rhs_array}, deref.type());
815  return code_assignt(checked_dereference(lhs), struct_rhs);
816  }
817  else
818  {
819  return code_blockt(
820  {code_assignt(get_length(deref, symbol_table), rhs_length),
821  code_assignt(get_data(deref, symbol_table), rhs_array)});
822  }
823 }
824 
837  const exprt &lhs,
838  const refined_string_exprt &rhs,
839  const symbol_table_baset &symbol_table,
840  bool is_constructor)
841 {
843  lhs, rhs.content(), rhs.length(), symbol_table, is_constructor);
844 }
845 
856  const refined_string_exprt &lhs,
857  const exprt &rhs,
858  const source_locationt &loc,
859  const symbol_table_baset &symbol_table,
860  code_blockt &code)
861 {
863 
864  const dereference_exprt deref = checked_dereference(rhs);
865 
866  // Although we should not reach this code if rhs is null, the association
867  // `pointer -> length` is added to the solver anyway, so we have to make sure
868  // the length is set to something reasonable.
869  auto rhs_length = if_exprt(
871  from_integer(0, lhs.length().type()),
872  get_length(deref, symbol_table));
873  rhs_length.set(ID_mode, ID_java);
874 
875  // Assignments
876  code.add(code_assignt(lhs.length(), rhs_length), loc);
877  exprt data_as_array = get_data(deref, symbol_table);
878  code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc);
879 }
880 
893  const std::string &s,
894  const source_locationt &loc,
895  symbol_table_baset &symbol_table,
896  code_blockt &code)
897 {
899  ID_cprover_string_literal_func,
901  loc,
902  symbol_table,
903  code);
904 }
905 
913  const java_method_typet &type,
914  const source_locationt &loc,
915  const irep_idt &function_id,
916  symbol_table_baset &symbol_table)
917 {
918  // Getting the argument
920  PRECONDITION(params.size()==1);
921  PRECONDITION(!params[0].get_identifier().empty());
922  const symbol_exprt arg(params[0].get_identifier(), params[0].type());
923 
924  // Holder for output code
925  code_blockt code;
926 
927  // Declaring and allocating String * str
928  const exprt str = allocate_fresh_string(
929  type.return_type(), loc, function_id, symbol_table, code);
930 
931  // Expression representing 0.0
932  const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
933  ieee_floatt zero_float(float_spec);
934  zero_float.from_float(0.0);
935  const constant_exprt zero = zero_float.to_expr();
936 
937  // For each possible case with have a condition and a string_exprt
938  std::vector<exprt> condition_list;
939  std::vector<refined_string_exprt> string_expr_list;
940 
941  // Case of computerized scientific notation
942  condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
943  const refined_string_exprt sci_notation = string_expr_of_function(
944  ID_cprover_string_of_float_scientific_notation_func,
945  {arg},
946  loc,
947  symbol_table,
948  code);
949  string_expr_list.push_back(sci_notation);
950 
951  // Subcase of negative scientific notation
952  condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
953  const refined_string_exprt minus_sign =
954  string_literal_to_string_expr("-", loc, symbol_table, code);
955  const refined_string_exprt neg_sci_notation = string_expr_of_function(
956  ID_cprover_string_concat_func,
957  {minus_sign, sci_notation},
958  loc,
959  symbol_table,
960  code);
961  string_expr_list.push_back(neg_sci_notation);
962 
963  // Case of NaN
964  condition_list.push_back(isnan_exprt(arg));
965  const refined_string_exprt nan =
966  string_literal_to_string_expr("NaN", loc, symbol_table, code);
967  string_expr_list.push_back(nan);
968 
969  // Case of Infinity
970  extractbit_exprt is_neg(arg, float_spec.width()-1);
971  condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
972  const refined_string_exprt infinity =
973  string_literal_to_string_expr("Infinity", loc, symbol_table, code);
974  string_expr_list.push_back(infinity);
975 
976  // Case -Infinity
977  condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
978  const refined_string_exprt minus_infinity =
979  string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
980  string_expr_list.push_back(minus_infinity);
981 
982  // Case of 0.0
983  // Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt,
984  // the latter disregards the sign
985  condition_list.push_back(equal_exprt(arg, zero));
986  const refined_string_exprt zero_string =
987  string_literal_to_string_expr("0.0", loc, symbol_table, code);
988  string_expr_list.push_back(zero_string);
989 
990  // Case of -0.0
991  ieee_floatt minus_zero_float(float_spec);
992  minus_zero_float.from_float(-0.0f);
993  condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
994  const refined_string_exprt minus_zero_string =
995  string_literal_to_string_expr("-0.0", loc, symbol_table, code);
996  string_expr_list.push_back(minus_zero_string);
997 
998  // Case of simple notation
999  ieee_floatt bound_inf_float(float_spec);
1000  ieee_floatt bound_sup_float(float_spec);
1001  bound_inf_float.from_float(1e-3f);
1002  bound_sup_float.from_float(1e7f);
1003  bound_inf_float.change_spec(float_spec);
1004  bound_sup_float.change_spec(float_spec);
1005  const constant_exprt bound_inf = bound_inf_float.to_expr();
1006  const constant_exprt bound_sup = bound_sup_float.to_expr();
1007 
1008  const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf),
1009  binary_relation_exprt(arg, ID_lt, bound_sup)};
1010  condition_list.push_back(is_simple_float);
1011 
1012  const refined_string_exprt simple_notation = string_expr_of_function(
1013  ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1014  string_expr_list.push_back(simple_notation);
1015 
1016  // Case of a negative number in simple notation
1017  const and_exprt is_neg_simple_float{
1018  binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
1019  binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))};
1020  condition_list.push_back(is_neg_simple_float);
1021 
1022  const refined_string_exprt neg_simple_notation = string_expr_of_function(
1023  ID_cprover_string_concat_func,
1024  {minus_sign, simple_notation},
1025  loc,
1026  symbol_table,
1027  code);
1028  string_expr_list.push_back(neg_simple_notation);
1029 
1030  // Combining all cases
1031  INVARIANT(
1032  string_expr_list.size()==condition_list.size(),
1033  "number of created strings should correspond to number of conditions");
1034 
1035  // We do not check the condition of the first element in the list as it
1036  // will be reached only if all other conditions are not satisfied.
1038  str, string_expr_list[0], symbol_table, true);
1039  for(std::size_t i=1; i<condition_list.size(); i++)
1040  {
1041  tmp_code = code_ifthenelset(
1042  condition_list[i],
1044  str, string_expr_list[i], symbol_table, true),
1045  tmp_code);
1046  }
1047  code.add(tmp_code, loc);
1048 
1049  // Return str
1050  code.add(code_returnt(str), loc);
1051  return code;
1052 }
1053 
1070  const irep_idt &function_id,
1071  const java_method_typet &type,
1072  const source_locationt &loc,
1073  symbol_table_baset &symbol_table,
1074  bool is_constructor)
1075 {
1077 
1078  // The first parameter is the object to be initialized
1079  PRECONDITION(!params.empty());
1080  PRECONDITION(!params[0].get_identifier().empty());
1081  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1082  if(is_constructor)
1083  params.erase(params.begin());
1084 
1085  // Holder for output code
1086  code_blockt code;
1087 
1088  // Processing parameters
1089  const exprt::operandst args =
1090  process_parameters(params, loc, function_id, symbol_table, code);
1091 
1092  // string_expr <- function(arg1)
1093  const refined_string_exprt string_expr =
1094  string_expr_of_function(function_id, args, loc, symbol_table, code);
1095 
1096  // arg_this <- string_expr
1097  code.add(
1099  arg_this, string_expr, symbol_table, is_constructor),
1100  loc);
1101 
1102  return code;
1103 }
1104 
1114  const irep_idt &function_id,
1115  const java_method_typet &type,
1116  const source_locationt &loc,
1117  symbol_table_baset &symbol_table)
1118 {
1119  // This is similar to assign functions except we return a pointer to `this`
1120  const java_method_typet::parameterst &params = type.parameters();
1121  PRECONDITION(!params.empty());
1122  PRECONDITION(!params[0].get_identifier().empty());
1123  code_blockt code;
1124  code.add(
1125  make_assign_function_from_call(function_id, type, loc, symbol_table), loc);
1126  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1127  code.add(code_returnt(arg_this), loc);
1128  return code;
1129 }
1130 
1139  const irep_idt &function_id,
1140  const java_method_typet &type,
1141  const source_locationt &loc,
1142  symbol_table_baset &symbol_table)
1143 {
1144  // This is similar to initialization function except we do not ignore
1145  // the first argument
1147  function_id, type, loc, symbol_table, false);
1148 }
1149 
1162  const java_method_typet &type,
1163  const source_locationt &loc,
1164  const irep_idt &function_id,
1165  symbol_table_baset &symbol_table)
1166 {
1168  PRECONDITION(!params.empty());
1169  PRECONDITION(!params[0].get_identifier().empty());
1170  const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1171 
1172  // Code to be returned
1173  code_blockt code;
1174 
1175  // class_identifier is obj->@class_identifier
1176  const member_exprt class_identifier{
1178 
1179  // string_expr = cprover_string_literal(this->@class_identifier)
1180  const refined_string_exprt string_expr = string_expr_of_function(
1181  ID_cprover_string_literal_func,
1182  {class_identifier},
1183  loc,
1184  symbol_table,
1185  code);
1186 
1187  // string_expr1 = substr(string_expr, 6)
1188  // We do this to remove the "java::" prefix
1189  const refined_string_exprt string_expr1 = string_expr_of_function(
1190  ID_cprover_string_substring_func,
1191  {string_expr, from_integer(6, java_int_type())},
1192  loc,
1193  symbol_table,
1194  code);
1195 
1196  // string1 = (String*) string_expr
1197  const typet &string_ptr_type = type.return_type();
1198  const exprt string1 = allocate_fresh_string(
1199  string_ptr_type, loc, function_id, symbol_table, code);
1200  code.add(
1202  string1, string_expr1, symbol_table, true),
1203  loc);
1204 
1205  // > return string1;
1206  code.add(code_returnt{string1}, loc);
1207  return code;
1208 }
1209 
1221  const irep_idt &function_id,
1222  const java_method_typet &type,
1223  const source_locationt &loc,
1224  symbol_table_baset &symbol_table)
1225 {
1226  code_blockt code;
1227  const exprt::operandst args =
1228  process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1229  code.add(
1231  function_id, args, type.return_type(), symbol_table),
1232  loc);
1233  return code;
1234 }
1235 
1251  const irep_idt &function_id,
1252  const java_method_typet &type,
1253  const source_locationt &loc,
1254  symbol_table_baset &symbol_table)
1255 {
1256  // Code for the output
1257  code_blockt code;
1258 
1259  // Calling the function
1260  const exprt::operandst arguments =
1261  process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1262 
1263  // String expression that will hold the result
1264  const refined_string_exprt string_expr =
1265  string_expr_of_function(function_id, arguments, loc, symbol_table, code);
1266 
1267  // Assign to string
1268  const exprt str = allocate_fresh_string(
1269  type.return_type(), loc, function_id, symbol_table, code);
1270  code.add(
1272  str, string_expr, symbol_table, true),
1273  loc);
1274 
1275  // Return value
1276  code.add(code_returnt(str), loc);
1277  return code;
1278 }
1279 
1295  const java_method_typet &type,
1296  const source_locationt &loc,
1297  const irep_idt &function_id,
1298  symbol_table_baset &symbol_table)
1299 {
1300  // Code for the output
1301  code_blockt code;
1302 
1303  // String expression that will hold the result
1304  const refined_string_exprt string_expr =
1305  decl_string_expr(loc, function_id, symbol_table, code);
1306 
1307  // Assign the argument to string_expr
1308  const java_method_typet::parametert &op = type.parameters()[0];
1310  const symbol_exprt arg0{op.get_identifier(), op.type()};
1312  string_expr, arg0, loc, symbol_table, code);
1313 
1314  // Allocate and assign the string
1315  const exprt str = allocate_fresh_string(
1316  type.return_type(), loc, function_id, symbol_table, code);
1317  code.add(
1319  str, string_expr, symbol_table, true),
1320  loc);
1321 
1322  // Return value
1323  code.add(code_returnt(str), loc);
1324  return code;
1325 }
1326 
1341  const java_method_typet &type,
1342  const source_locationt &loc,
1343  const irep_idt &function_id,
1344  symbol_table_baset &symbol_table)
1345 {
1346  code_blockt copy_constructor_body;
1347 
1348  // String expression that will hold the result
1349  const refined_string_exprt string_expr =
1350  decl_string_expr(loc, function_id, symbol_table, copy_constructor_body);
1351 
1352  // Assign argument to a string_expr
1353  const java_method_typet::parameterst &params = type.parameters();
1354  PRECONDITION(!params[0].get_identifier().empty());
1355  PRECONDITION(!params[1].get_identifier().empty());
1356  const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
1358  string_expr, arg1, loc, symbol_table, copy_constructor_body);
1359 
1360  // Assign string_expr to `this` object
1361  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1362  copy_constructor_body.add(
1364  arg_this, string_expr, symbol_table, true),
1365  loc);
1366 
1367  return copy_constructor_body;
1368 }
1369 
1382  const java_method_typet &type,
1383  const source_locationt &loc,
1384  const irep_idt &function_id,
1385  symbol_table_baset &symbol_table)
1386 {
1387  (void)function_id;
1388 
1389  const java_method_typet::parameterst &params = type.parameters();
1390  PRECONDITION(!params[0].get_identifier().empty());
1391  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1392  const dereference_exprt deref = checked_dereference(arg_this);
1393 
1394  code_returnt ret(get_length(deref, symbol_table));
1395  ret.add_source_location() = loc;
1396 
1397  return ret;
1398 }
1399 
1401  const irep_idt &function_id) const
1402 {
1403  for(const id_mapt *map : id_maps)
1404  if(map->count(function_id) != 0)
1405  return true;
1406 
1407  return conversion_table.count(function_id) != 0;
1408 }
1409 
1410 template <typename TMap, typename TContainer>
1411 void add_keys_to_container(const TMap &map, TContainer &container)
1412 {
1413  static_assert(
1414  std::is_same<typename TMap::key_type,
1415  typename TContainer::value_type>::value,
1416  "TContainer value_type doesn't match TMap key_type");
1417  std::transform(
1418  map.begin(),
1419  map.end(),
1420  std::inserter(container, container.begin()),
1421  [](const typename TMap::value_type &pair) { return pair.first; });
1422 }
1423 
1425  std::unordered_set<irep_idt> &methods) const
1426 {
1427  for(const id_mapt *map : id_maps)
1428  add_keys_to_container(*map, methods);
1429 
1431 }
1432 
1440  const symbolt &symbol,
1441  symbol_table_baset &symbol_table)
1442 {
1443  const irep_idt &function_id = symbol.name;
1444  const java_method_typet &type = to_java_method_type(symbol.type);
1445  const source_locationt &loc = symbol.location;
1446  auto it_id=cprover_equivalent_to_java_function.find(function_id);
1447  if(it_id!=cprover_equivalent_to_java_function.end())
1448  return make_function_from_call(it_id->second, type, loc, symbol_table);
1449 
1453  it_id->second, type, loc, symbol_table);
1454 
1455  it_id=cprover_equivalent_to_java_constructor.find(function_id);
1458  it_id->second, type, loc, symbol_table);
1459 
1463  it_id->second, type, loc, symbol_table);
1464 
1465  it_id=cprover_equivalent_to_java_assign_function.find(function_id);
1468  it_id->second, type, loc, symbol_table);
1469 
1470  auto it=conversion_table.find(function_id);
1471  INVARIANT(
1472  it != conversion_table.end(), "Couldn't retrieve code for string method");
1473 
1474  return it->second(type, loc, function_id, symbol_table);
1475 }
1476 
1482  irep_idt class_name)
1483 {
1484  return string_types.find(class_name)!=string_types.end();
1485 }
1486 
1488 {
1489  string_types = std::unordered_set<irep_idt>{"java.lang.String",
1490  "java.lang.StringBuilder",
1491  "java.lang.CharSequence",
1492  "java.lang.StringBuffer"};
1493 }
1494 
1497 {
1499 
1500  // The following list of function is organized by libraries, with
1501  // constructors first and then methods in alphabetic order.
1502  // Methods that are not supported here should ultimately have Java models
1503  // provided for them in the class-path.
1504 
1505  // CProverString library
1507  ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1508  "lang/CharSequence;II)"
1509  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1510  // CProverString.charAt differs from the Java String.charAt in that no
1511  // exception is raised for the out of bounds case.
1513  ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1514  ID_cprover_string_char_at_func;
1516  ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1517  ID_cprover_string_char_at_func;
1519  ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1520  ID_cprover_string_code_point_at_func;
1522  ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1523  ID_cprover_string_code_point_before_func;
1525  ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1526  ID_cprover_string_code_point_count_func;
1528  ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1529  "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1531  ["java::org.cprover.CProverString.delete:(Ljava/lang/"
1532  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1533  ID_cprover_string_delete_func;
1535  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1536  "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1537  ID_cprover_string_delete_char_at_func;
1539  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1540  "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1541  ID_cprover_string_delete_char_at_func;
1542 
1543  std::string format_signature = "java::org.cprover.CProverString.format:(";
1544  for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1545  format_signature += "Ljava/lang/String;";
1546  format_signature += ")Ljava/lang/String;";
1548  ID_cprover_string_format_func;
1549 
1551  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1552  "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1554  ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1555  "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1557  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1558  "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1560  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1561  "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1563  ["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1564  ID_cprover_string_set_length_func;
1566  ["java::org.cprover.CProverString.setLength:(Ljava/lang/"
1567  "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1569  ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1570  "lang/CharSequence;"] = ID_cprover_string_substring_func;
1571  // CProverString.substring differs from the Java String.substring in that no
1572  // exception is raised for the out of bounds case.
1574  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1575  "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1577  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1578  "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1580  ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
1581  "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1583  ["java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1584  ID_cprover_string_of_int_func;
1586  ["java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1587  ID_cprover_string_of_int_func;
1589  ["java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1590  ID_cprover_string_of_long_func;
1592  ["java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1593  ID_cprover_string_of_long_func;
1595  ["java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1596  std::bind(
1598  this,
1599  std::placeholders::_1,
1600  std::placeholders::_2,
1601  std::placeholders::_3,
1602  std::placeholders::_4);
1604  ["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1605  ID_cprover_string_parse_int_func;
1607  ["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1608  ID_cprover_string_parse_int_func;
1610  ["java::org.cprover.CProverString.isValidInt:(Ljava/lang/String;I)Z"] =
1611  ID_cprover_string_is_valid_int_func;
1613  ["java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z"] =
1614  ID_cprover_string_is_valid_long_func;
1615 
1616  // String library
1617  conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1618  std::bind(
1620  this,
1621  std::placeholders::_1,
1622  std::placeholders::_2,
1623  std::placeholders::_3,
1624  std::placeholders::_4);
1626  ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1628  this,
1629  std::placeholders::_1,
1630  std::placeholders::_2,
1631  std::placeholders::_3,
1632  std::placeholders::_4);
1634  ["java::java.lang.String.<init>:()V"]=
1635  ID_cprover_string_empty_string_func;
1636 
1638  ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1639  ID_cprover_string_compare_to_func;
1641  ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1642  ID_cprover_string_concat_func;
1644  ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1645  ID_cprover_string_contains_func;
1647  ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1648  ID_cprover_string_endswith_func;
1650  ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1651  ID_cprover_string_equals_ignore_case_func;
1652 
1654  ["java::java.lang.String.indexOf:(I)I"]=
1655  ID_cprover_string_index_of_func;
1657  ["java::java.lang.String.indexOf:(II)I"]=
1658  ID_cprover_string_index_of_func;
1660  ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1661  ID_cprover_string_index_of_func;
1663  ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1664  ID_cprover_string_index_of_func;
1666  ["java::java.lang.String.isEmpty:()Z"]=
1667  ID_cprover_string_is_empty_func;
1669  ["java::java.lang.String.lastIndexOf:(I)I"]=
1670  ID_cprover_string_last_index_of_func;
1672  ["java::java.lang.String.lastIndexOf:(II)I"]=
1673  ID_cprover_string_last_index_of_func;
1675  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1676  ID_cprover_string_last_index_of_func;
1678  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1679  ID_cprover_string_last_index_of_func;
1680  conversion_table["java::java.lang.String.length:()I"] = std::bind(
1682  this,
1683  std::placeholders::_1,
1684  std::placeholders::_2,
1685  std::placeholders::_3,
1686  std::placeholders::_4);
1688  ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1689  ID_cprover_string_replace_func;
1691  ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
1692  ID_cprover_string_replace_func;
1694  ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1695  ID_cprover_string_startswith_func;
1697  ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1698  ID_cprover_string_startswith_func;
1700  ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1701  ID_cprover_string_to_lower_case_func;
1702  conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
1703  std::bind(
1705  this,
1706  std::placeholders::_1,
1707  std::placeholders::_2,
1708  std::placeholders::_3,
1709  std::placeholders::_4);
1711  ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1712  ID_cprover_string_to_upper_case_func;
1714  ["java::java.lang.String.trim:()Ljava/lang/String;"]=
1715  ID_cprover_string_trim_func;
1716 
1717  // StringBuilder library
1719  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1721  this,
1722  std::placeholders::_1,
1723  std::placeholders::_2,
1724  std::placeholders::_3,
1725  std::placeholders::_4);
1727  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1728  std::bind(
1730  this,
1731  std::placeholders::_1,
1732  std::placeholders::_2,
1733  std::placeholders::_3,
1734  std::placeholders::_4);
1736  ["java::java.lang.StringBuilder.<init>:()V"]=
1737  ID_cprover_string_empty_string_func;
1739  ["java::java.lang.StringBuilder.<init>:(I)V"] =
1740  ID_cprover_string_empty_string_func;
1741 
1743  ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1744  ID_cprover_string_concat_char_func;
1746  ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1747  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1749  ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1750  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1752  ["java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1753  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1755  ["java::java.lang.StringBuilder.appendCodePoint:(I)"
1756  "Ljava/lang/StringBuilder;"]=
1757  ID_cprover_string_concat_code_point_func;
1759  ["java::java.lang.StringBuilder.charAt:(I)C"]=
1760  ID_cprover_string_char_at_func;
1762  ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
1763  ID_cprover_string_code_point_at_func;
1765  ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1766  ID_cprover_string_code_point_before_func;
1768  ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
1769  ID_cprover_string_code_point_count_func;
1770  conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
1772  this,
1773  std::placeholders::_1,
1774  std::placeholders::_2,
1775  std::placeholders::_3,
1776  std::placeholders::_4);
1778  ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1779  ID_cprover_string_substring_func;
1781  ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1782  ID_cprover_string_substring_func;
1784  ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1786  this,
1787  std::placeholders::_1,
1788  std::placeholders::_2,
1789  std::placeholders::_3,
1790  std::placeholders::_4);
1791 
1792  // StringBuffer library
1794  ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1796  this,
1797  std::placeholders::_1,
1798  std::placeholders::_2,
1799  std::placeholders::_3,
1800  std::placeholders::_4);
1802  ["java::java.lang.StringBuffer.<init>:()V"]=
1803  ID_cprover_string_empty_string_func;
1804 
1806  ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1807  ID_cprover_string_concat_char_func;
1809  ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1810  "Ljava/lang/StringBuffer;"]=
1811  ID_cprover_string_concat_func;
1813  ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1814  "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1816  ["java::java.lang.StringBuffer.appendCodePoint:(I)"
1817  "Ljava/lang/StringBuffer;"]=
1818  ID_cprover_string_concat_code_point_func;
1820  ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
1821  ID_cprover_string_code_point_at_func;
1823  ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1824  ID_cprover_string_code_point_before_func;
1826  ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
1827  ID_cprover_string_code_point_count_func;
1829  ["java::java.lang.StringBuffer.length:()I"]=
1830  conversion_table["java::java.lang.String.length:()I"];
1832  ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1833  ID_cprover_string_substring_func;
1835  ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1837  this,
1838  std::placeholders::_1,
1839  std::placeholders::_2,
1840  std::placeholders::_3,
1841  std::placeholders::_4);
1842 
1843  // CharSequence library
1845  ["java::java.lang.CharSequence.charAt:(I)C"]=
1846  ID_cprover_string_char_at_func;
1848  ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1850  this,
1851  std::placeholders::_1,
1852  std::placeholders::_2,
1853  std::placeholders::_3,
1854  std::placeholders::_4);
1856  ["java::java.lang.CharSequence.length:()I"]=
1857  conversion_table["java::java.lang.String.length:()I"];
1858 
1859  // Other libraries
1861  ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1862  ID_cprover_string_of_int_hex_func;
1863  conversion_table["java::org.cprover.CProver.classIdentifier:("
1864  "Ljava/lang/Object;)Ljava/lang/String;"] =
1865  std::bind(
1867  this,
1868  std::placeholders::_1,
1869  std::placeholders::_2,
1870  std::placeholders::_3,
1871  std::placeholders::_4);
1872 }
java_string_library_preprocesst::convert_exprt_to_string_exprt
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.
Definition: java_string_library_preprocess.cpp:308
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
java_string_library_preprocesst::replace_char_array
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.
Definition: java_string_library_preprocess.cpp:429
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
java_string_library_preprocesst::process_parameters
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.
Definition: java_string_library_preprocess.cpp:279
add_pointer_to_array_association
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...
Definition: java_string_library_preprocess.cpp:644
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_string_library_preprocesst::make_copy_string_code
code_blockt make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for a function which copies a string object to a new string object.
Definition: java_string_library_preprocess.cpp:1294
java_string_library_preprocesst::make_string_length_code
code_returnt make_string_length_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for the String.length method.
Definition: java_string_library_preprocess.cpp:1381
java_string_library_preprocesst::id_mapt
std::unordered_map< irep_idt, irep_idt > id_mapt
Definition: java_string_library_preprocess.h:108
java_string_library_preprocesst::cprover_equivalent_to_java_assign_and_return_function
id_mapt cprover_equivalent_to_java_assign_and_return_function
Definition: java_string_library_preprocess.h:127
ieee_floatt
Definition: ieee_float.h:120
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
dstringt::c_str
const char * c_str() const
Definition: dstring.h:99
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_root_class.h
JAVA_CLASS_IDENTIFIER_FIELD_NAME
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
Definition: class_identifier.h:20
arith_tools.h
add_array_to_length_association
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...
Definition: java_string_library_preprocess.cpp:675
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
java_string_library_preprocesst::index_type
const typet index_type
Definition: java_string_library_preprocess.h:98
java_string_library_preprocesst::make_string_returning_function_from_call
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...
Definition: java_string_library_preprocess.cpp:1250
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
fresh_symbol.h
Fresh auxiliary symbol creation.
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
java_string_library_preprocesst::string_expr_of_function
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...
Definition: java_string_library_preprocess.cpp:747
checked_dereference
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:291
data
Definition: kdev_t.h:24
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
make_function_application
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:394
struct_typet::add_base
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:88
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
and_exprt
Boolean AND.
Definition: std_expr.h:2137
java_string_library_preprocesst::cprover_equivalent_to_java_function
id_mapt cprover_equivalent_to_java_function
Definition: java_string_library_preprocess.h:115
java_string_library_preprocesst::cprover_equivalent_to_java_string_returning_function
id_mapt cprover_equivalent_to_java_string_returning_function
Definition: java_string_library_preprocess.h:119
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1044
java_string_library_preprocesst::make_assign_and_return_function_from_call
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.
Definition: java_string_library_preprocess.cpp:1113
java_string_library_preprocesst::cprover_equivalent_to_java_constructor
id_mapt cprover_equivalent_to_java_constructor
Definition: java_string_library_preprocess.h:123
struct_union_typet::component_type
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:66
java_string_library_preprocesst::decl_string_expr
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.
Definition: java_string_library_preprocess.cpp:485
exprt
Base class for all expressions.
Definition: expr.h:53
java_string_library_preprocesst::implements_function
bool implements_function(const irep_idt &function_id) const
Definition: java_string_library_preprocess.cpp:1400
java_string_library_preprocesst::make_assign_function_from_call
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.
Definition: java_string_library_preprocess.cpp:1138
java_string_library_preprocess.h
Produce code for simple implementation of String Java libraries.
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
java_string_library_preprocesst::make_init_function_from_call
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.
Definition: java_string_library_preprocess.cpp:1069
java_string_library_preprocesst::make_class_identifier_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)
Used to provide our own implementation of the CProver.classIdentifier() function.
Definition: java_string_library_preprocess.cpp:1161
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1487
java_string_library_preprocesst::process_operands
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...
Definition: java_string_library_preprocess.cpp:336
irep_idt
dstringt irep_idt
Definition: irep.h:32
java_string_library_preprocesst::is_java_char_sequence_pointer_type
static bool is_java_char_sequence_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:138
make_nondet_infinite_char_array
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.
Definition: java_string_library_preprocess.cpp:612
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
java_string_library_preprocesst::code_assign_java_string_to_string_expr
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)
Definition: java_string_library_preprocess.cpp:855
equal_exprt
Equality.
Definition: std_expr.h:1190
java_string_library_preprocesst::is_java_string_builder_type
static bool is_java_string_builder_type(const typet &type)
Definition: java_string_library_preprocess.cpp:83
ieee_floatt::from_float
void from_float(const float f)
Definition: ieee_float.cpp:1114
string_length_type
static typet string_length_type()
Definition: java_string_library_preprocess.cpp:174
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4111
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
java_string_library_preprocesst::get_string_type_base_classes
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...
Definition: java_string_library_preprocess.cpp:184
notequal_exprt
Disequality.
Definition: std_expr.h:1248
refined_string_exprt
Definition: string_expr.h:109
refined_string_exprt::length
const exprt & length() const
Definition: string_expr.h:128
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
ieee_float_spect
Definition: ieee_float.h:26
java_class_typet
Definition: java_types.h:199
java_string_library_preprocesst::string_literal_to_string_expr
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.
Definition: java_string_library_preprocess.cpp:892
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
array_typet::size
const exprt & size() const
Definition: std_types.h:973
java_string_library_preprocesst::add_string_type
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.
Definition: java_string_library_preprocess.cpp:217
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
MAX_FORMAT_ARGS
#define MAX_FORMAT_ARGS
Definition: java_string_library_preprocess.h:33
set_class_identifier
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.
Definition: class_identifier.cpp:82
expr_initializer.h
Expression Initialization.
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_string_library_preprocesst::conversion_table
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Definition: java_string_library_preprocess.h:111
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition: std_types.h:164
java_string_library_preprocesst::make_copy_constructor_code
code_blockt make_copy_constructor_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for a constructor of a string object from another string object.
Definition: java_string_library_preprocess.cpp:1340
java_string_library_preprocesst::make_function_from_call
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.
Definition: java_string_library_preprocess.cpp:1220
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
java_string_library_preprocesst::get_all_function_names
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
Definition: java_string_library_preprocess.cpp:1424
java_string_library_preprocesst::is_java_char_array_type
static bool is_java_char_array_type(const typet &type)
Definition: java_string_library_preprocess.cpp:152
java_string_library_preprocesst::make_nondet_string_expr
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...
Definition: java_string_library_preprocess.cpp:510
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
java_string_library_preprocesst::code_for_function
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
Definition: java_string_library_preprocess.cpp:1439
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
java_string_library_preprocesst::cprover_equivalent_to_java_assign_function
id_mapt cprover_equivalent_to_java_assign_function
Definition: java_string_library_preprocess.h:132
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
java_string_library_preprocesst::is_java_char_sequence_type
static bool is_java_char_sequence_type(const typet &type)
Definition: java_string_library_preprocess.cpp:129
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
std_code.h
fresh_java_symbol
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:566
get_length_type
static const typet & get_length_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the length component.
Definition: java_string_library_preprocess.cpp:387
java_string_library_preprocesst::java_type_matches_tag
static bool java_type_matches_tag(const typet &type, const std::string &tag)
Definition: java_string_library_preprocess.cpp:53
java_string_library_preprocesst::character_preprocess
character_refine_preprocesst character_preprocess
Definition: java_string_library_preprocess.h:95
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:69
allocate_objectst::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Definition: allocate_objects.cpp:226
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
java_string_library_preprocesst::is_java_char_array_pointer_type
static bool is_java_char_array_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:161
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2629
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
java_string_library_preprocesst::make_float_to_string_code
code_blockt make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Provide code for the String.valueOf(F) function.
Definition: java_string_library_preprocess.cpp:912
java_string_library_preprocesst::is_java_string_buffer_type
static bool is_java_string_buffer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:106
java_class_typet::components
const componentst & components() const
Definition: java_types.h:226
refined_string_exprt::content
const exprt & content() const
Definition: string_expr.h:138
java_class_typet::set_access
void set_access(const irep_idt &access)
Definition: java_types.h:330
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
array_typet
Arrays with given size.
Definition: std_types.h:965
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
refined_string_type.h
Type for string expressions used by the string solver.
java_string_library_preprocesst::refined_string_type
const refined_string_typet refined_string_type
Definition: java_string_library_preprocess.h:99
java_string_library_preprocesst::code_assign_components_to_java_string
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.
Definition: java_string_library_preprocess.cpp:794
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
java_string_library_preprocesst::is_java_string_buffer_pointer_type
static bool is_java_string_buffer_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:115
java_string_library_preprocesst::id_maps
const std::array< id_mapt *, 5 > id_maps
Definition: java_string_library_preprocess.h:134
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3554
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
java_string_library_preprocesst::implements_java_char_sequence_pointer
static bool implements_java_char_sequence_pointer(const typet &type)
Definition: java_string_library_preprocess.h:63
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
code_blockt::append
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:87
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
symbolt::is_type
bool is_type
Definition: symbol.h:61
string_typet
String type.
Definition: std_types.h:1655
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
java_string_library_preprocesst::is_known_string_type
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
Definition: java_string_library_preprocess.cpp:1481
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:792
code_typet::parametert
Definition: std_types.h:753
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
java_class_typet::set_name
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
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
code_assign_function_application
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
Definition: java_string_library_preprocess.cpp:575
make_allocate_code
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
Definition: allocate_objects.cpp:255
class_identifier.h
Extract class identifier.
java_string_library_preprocesst::allocate_fresh_string
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
Definition: java_string_library_preprocess.cpp:547
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
allocate_objectst
Definition: allocate_objects.h:31
allocate_objectst::allocate_dynamic_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...
Definition: allocate_objects.cpp:171
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
java_string_library_preprocesst::initialize_conversion_table
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
Definition: java_string_library_preprocess.cpp:1496
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
java_string_library_preprocesst::fresh_string
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
Definition: java_string_library_preprocess.cpp:466
index_exprt
Array index operator.
Definition: std_expr.h:1293
get_length
static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
access length member
Definition: java_string_library_preprocess.cpp:406
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
java_types.h
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
is_constructor
static bool is_constructor(const irep_idt &method_name)
Definition: java_bytecode_convert_method.cpp:128
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
java_string_library_preprocesst::is_java_string_pointer_type
static bool is_java_string_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:61
java_utils.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
java_string_library_preprocesst::code_assign_string_expr_to_java_string
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.
Definition: java_string_library_preprocess.cpp:836
java_string_library_preprocesst::string_types
std::unordered_set< irep_idt > string_types
Definition: java_string_library_preprocess.h:146
std_expr.h
API to expression classes.
string_expr.h
String expressions for the string solver.
java_method_typet
Definition: java_types.h:103
get_data
static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
access data member
Definition: java_string_library_preprocess.cpp:416
allocate_objects.h
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
add_keys_to_container
void add_keys_to_container(const TMap &map, TContainer &container)
Definition: java_string_library_preprocess.cpp:1411
java_string_library_preprocesst::is_java_string_type
static bool is_java_string_type(const typet &type)
Definition: java_string_library_preprocess.cpp:75
add_character_set_constraint
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...
Definition: java_string_library_preprocess.cpp:707
java_string_library_preprocesst::is_java_string_builder_pointer_type
static bool is_java_string_builder_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:92
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1656
validation_modet::INVARIANT
@ INVARIANT
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3509
get_data_type
static const typet & get_data_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the data component.
Definition: java_string_library_preprocess.cpp:367
character_refine_preprocesst::initialize_conversion_table
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
Definition: character_refine_preprocess.cpp:1303
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
not_exprt
Boolean negation.
Definition: std_expr.h:2843
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:38
java_string_library_preprocesst::code_return_function_application
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
Definition: java_string_library_preprocess.cpp:596