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/fresh_symbol.h>
25 #include <util/std_code.h>
26 #include <util/std_expr.h>
27 #include <util/string_expr.h>
28 
29 #include "java_types.h"
30 #include "java_utils.h"
31 
33 #include "java_root_class.h"
34 
37 static irep_idt get_tag(const typet &type)
38 {
40  if(type.id() == ID_struct_tag)
41  return to_struct_tag_type(type).get_identifier();
42  else if(type.id() == ID_struct)
43  return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
44  else
45  return irep_idt();
46 }
47 
53  const typet &type, const std::string &tag)
54 {
55  return irep_idt("java::" + tag) == get_tag(type);
56 }
57 
61  const typet &type)
62 {
63  if(type.id()==ID_pointer)
64  {
65  const pointer_typet &pt=to_pointer_type(type);
66  const typet &subtype=pt.subtype();
67  return is_java_string_type(subtype);
68  }
69  return false;
70 }
71 
75  const typet &type)
76 {
77  return java_type_matches_tag(type, "java.lang.String");
78 }
79 
83  const typet &type)
84 {
85  return java_type_matches_tag(type, "java.lang.StringBuilder");
86 }
87 
92  const typet &type)
93 {
94  if(type.id()==ID_pointer)
95  {
96  const pointer_typet &pt=to_pointer_type(type);
97  const typet &subtype=pt.subtype();
98  return is_java_string_builder_type(subtype);
99  }
100  return false;
101 }
102 
106  const typet &type)
107 {
108  return java_type_matches_tag(type, "java.lang.StringBuffer");
109 }
110 
115  const typet &type)
116 {
117  if(type.id()==ID_pointer)
118  {
119  const pointer_typet &pt=to_pointer_type(type);
120  const typet &subtype=pt.subtype();
121  return is_java_string_buffer_type(subtype);
122  }
123  return false;
124 }
125 
129  const typet &type)
130 {
131  return java_type_matches_tag(type, "java.lang.CharSequence");
132 }
133 
138  const typet &type)
139 {
140  if(type.id()==ID_pointer)
141  {
142  const pointer_typet &pt=to_pointer_type(type);
143  const typet &subtype=pt.subtype();
144  return is_java_char_sequence_type(subtype);
145  }
146  return false;
147 }
148 
152  const typet &type)
153 {
154  return java_type_matches_tag(type, "array[char]");
155 }
156 
161  const typet &type)
162 {
163  if(type.id()==ID_pointer)
164  {
165  const pointer_typet &pt=to_pointer_type(type);
166  const typet &subtype=pt.subtype();
167  return is_java_char_array_type(subtype);
168  }
169  return false;
170 }
171 
174 {
175  return java_int_type();
176 }
177 
182 std::vector<irep_idt>
184  const irep_idt &class_name)
185 {
186  if(!is_known_string_type(class_name))
187  return {};
188 
189  std::vector<irep_idt> bases;
190  bases.reserve(3);
191  if(class_name != "java.lang.CharSequence")
192  {
193  bases.push_back("java.io.Serializable");
194  bases.push_back("java.lang.CharSequence");
195  }
196  if(class_name == "java.lang.String")
197  bases.push_back("java.lang.Comparable");
198 
199  if(class_name == "java.lang.StringBuilder" ||
200  class_name == "java.lang.StringBuffer")
201  bases.push_back("java.lang.AbstractStringBuilder");
202 
203  return bases;
204 }
205 
210  const irep_idt &class_name, symbol_tablet &symbol_table)
211 {
212  java_class_typet string_type;
213  string_type.set_tag(class_name);
214  string_type.set_name("java::" + id2string(class_name));
215  string_type.components().resize(3);
216  string_type.components()[0].set_name("@java.lang.Object");
217  string_type.components()[0].set_pretty_name("@java.lang.Object");
218  string_type.components()[0].type() =
219  struct_tag_typet("java::java.lang.Object");
220  string_type.components()[1].set_name("length");
221  string_type.components()[1].set_pretty_name("length");
222  string_type.components()[1].type()=string_length_type();
223  string_type.components()[2].set_name("data");
224  string_type.components()[2].set_pretty_name("data");
225  string_type.components()[2].type() = pointer_type(java_char_type());
226  string_type.set_access(ID_public);
227  string_type.add_base(struct_tag_typet("java::java.lang.Object"));
228 
229  std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
230  for(const irep_idt &base_name : bases)
231  string_type.add_base(struct_tag_typet("java::" + id2string(base_name)));
232 
233  symbolt tmp_string_symbol;
234  tmp_string_symbol.name="java::"+id2string(class_name);
235  symbolt *string_symbol=nullptr;
236  symbol_table.move(tmp_string_symbol, string_symbol);
237  string_symbol->base_name=id2string(class_name);
238  string_symbol->pretty_name=id2string(class_name);
239  string_symbol->type=string_type;
240  string_symbol->is_type=true;
241  string_symbol->mode = ID_java;
242 }
243 
253  const java_method_typet::parameterst &params,
254  const source_locationt &loc,
255  const irep_idt &function_id,
256  symbol_table_baset &symbol_table,
257  code_blockt &init_code)
258 {
259  exprt::operandst ops;
260  for(const auto &p : params)
261  ops.emplace_back(symbol_exprt(p.get_identifier(), p.type()));
262  return process_operands(ops, loc, function_id, symbol_table, init_code);
263 }
264 
282  const exprt &expr_to_process,
283  const source_locationt &loc,
284  symbol_table_baset &symbol_table,
285  const irep_idt &function_id,
286  code_blockt &init_code)
287 {
289  const refined_string_exprt string_expr =
290  decl_string_expr(loc, function_id, symbol_table, init_code);
292  string_expr, expr_to_process, loc, symbol_table, init_code);
293  return string_expr;
294 }
295 
310  const exprt::operandst &operands,
311  const source_locationt &loc,
312  const irep_idt &function_id,
313  symbol_table_baset &symbol_table,
314  code_blockt &init_code)
315 {
316  exprt::operandst ops;
317  for(const auto &p : operands)
318  {
320  {
321  init_code.add(code_assumet(
323  ops.push_back(convert_exprt_to_string_exprt(
324  p, loc, symbol_table, function_id, init_code));
325  }
326  else if(is_java_char_array_pointer_type(p.type()))
327  ops.push_back(
328  replace_char_array(p, loc, function_id, symbol_table, init_code));
329  else
330  ops.push_back(p);
331  }
332  return ops;
333 }
334 
339 static const typet &
340 get_data_type(const typet &type, const symbol_tablet &symbol_table)
341 {
342  PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
343  if(type.id() == ID_struct_tag)
344  {
345  const symbolt &sym =
346  symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
347  CHECK_RETURN(sym.type.id() != ID_struct_tag);
348  return get_data_type(sym.type, symbol_table);
349  }
350  // else type id is ID_struct
351  const struct_typet &struct_type=to_struct_type(type);
352  return struct_type.component_type("data");
353 }
354 
359 static const typet &
360 get_length_type(const typet &type, const symbol_tablet &symbol_table)
361 {
362  PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
363  if(type.id() == ID_struct_tag)
364  {
365  const symbolt &sym =
366  symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
367  CHECK_RETURN(sym.type.id() != ID_struct_tag);
368  return get_length_type(sym.type, symbol_table);
369  }
370  // else type id is ID_struct
371  const struct_typet &struct_type=to_struct_type(type);
372  return struct_type.component_type("length");
373 }
374 
379 static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
380 {
381  return member_exprt(
382  expr, "length", get_length_type(expr.type(), symbol_table));
383 }
384 
389 static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
390 {
391  return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
392 }
393 
403  const exprt &array_pointer,
404  const source_locationt &loc,
405  const irep_idt &function_id,
406  symbol_table_baset &symbol_table,
407  code_blockt &code)
408 {
409  // array is *array_pointer
410  const dereference_exprt array = checked_dereference(array_pointer);
411  // array_data is array_pointer-> data
412  const exprt array_data = get_data(array, symbol_table);
413  const symbolt &sym_char_array = fresh_java_symbol(
414  array_data.type(), "char_array", loc, function_id, symbol_table);
415  const symbol_exprt char_array = sym_char_array.symbol_expr();
416  // char_array = array_pointer->data
417  code.add(code_assignt(char_array, array_data), loc);
418 
419  // string_expr is `{ rhs->length; string_array }`
420  const refined_string_exprt string_expr(
421  get_length(array, symbol_table), char_array, refined_string_type);
422 
423  const dereference_exprt inf_array(
425 
427  string_expr.content(), inf_array, symbol_table, loc, function_id, code);
428 
429  return string_expr;
430 }
431 
440  const typet &type,
441  const source_locationt &loc,
442  const irep_idt &function_id,
443  symbol_table_baset &symbol_table)
444 {
445  symbolt string_symbol =
446  fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
447  string_symbol.is_static_lifetime=true;
448  return string_symbol.symbol_expr();
449 }
450 
459  const source_locationt &loc,
460  const irep_idt &function_id,
461  symbol_table_baset &symbol_table,
462  code_blockt &code)
463 {
464  const symbolt &sym_length = fresh_java_symbol(
465  index_type, "cprover_string_length", loc, function_id, symbol_table);
466  const symbol_exprt length_field = sym_length.symbol_expr();
467  const pointer_typet array_type = pointer_type(java_char_type());
468  const symbolt &sym_content = fresh_java_symbol(
469  array_type, "cprover_string_content", loc, function_id, symbol_table);
470  const symbol_exprt content_field = sym_content.symbol_expr();
471  code.add(code_declt(content_field), loc);
472  code.add(code_declt{length_field}, loc);
473  return refined_string_exprt{length_field, content_field, refined_string_type};
474 }
475 
484  const source_locationt &loc,
485  const irep_idt &function_id,
486  symbol_table_baset &symbol_table,
487  code_blockt &code)
488 {
490  const refined_string_exprt str =
491  decl_string_expr(loc, function_id, symbol_table, code);
492 
493  const side_effect_expr_nondett nondet_length(str.length().type(), loc);
494  code.add(code_assignt(str.length(), nondet_length), loc);
495 
496  const exprt nondet_array_expr =
497  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
498 
499  const address_of_exprt array_pointer(
500  index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
501 
503  array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
504 
506  nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
507 
508  code.add(code_assignt(str.content(), array_pointer), loc);
509 
510  return refined_string_exprt(str.length(), str.content());
511 }
512 
521  const typet &type,
522  const source_locationt &loc,
523  const irep_idt &function_id,
524  symbol_table_baset &symbol_table,
525  code_blockt &code)
526 {
527  const exprt str = fresh_string(type, loc, function_id, symbol_table);
528 
529  allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
530 
531  code_blockt tmp;
532  allocate_objects.allocate_dynamic_object(tmp, str, str.type().subtype());
533  allocate_objects.declare_created_symbols(code);
534  code.append(tmp);
535 
536  return str;
537 }
538 
549  const exprt &lhs,
550  const irep_idt &function_id,
551  const exprt::operandst &arguments,
552  symbol_table_baset &symbol_table)
553 {
554  return code_assignt(
555  lhs,
557  function_id, arguments, lhs.type(), symbol_table));
558 }
559 
570  const irep_idt &function_id,
571  const exprt::operandst &arguments,
572  const typet &type,
573  symbol_table_baset &symbol_table)
574 {
575  return code_returnt(
576  make_function_application(function_id, arguments, type, symbol_table));
577 }
578 
586  symbol_table_baset &symbol_table,
587  const source_locationt &loc,
588  const irep_idt &function_id,
589  code_blockt &code)
590 {
591  const array_typet array_type(
593  const symbolt data_sym = fresh_java_symbol(
594  pointer_type(array_type),
595  "nondet_infinite_array_pointer",
596  loc,
597  function_id,
598  symbol_table);
599 
600  const symbol_exprt data_pointer = data_sym.symbol_expr();
601  code.add(code_declt(data_pointer));
602  code.add(make_allocate_code(data_pointer, array_type.size()));
603  side_effect_expr_nondett nondet_data{array_type, loc};
604  dereference_exprt data{data_pointer};
605  code.add(code_assignt{data, std::move(nondet_data)}, loc);
606  return std::move(data);
607 }
608 
618  const exprt &pointer,
619  const exprt &array,
620  symbol_table_baset &symbol_table,
621  const source_locationt &loc,
622  const irep_idt &function_id,
623  code_blockt &code)
624 {
625  PRECONDITION(array.type().id() == ID_array);
626  PRECONDITION(pointer.type().id() == ID_pointer);
627  const symbolt &return_sym = fresh_java_symbol(
628  java_int_type(), "return_array", loc, function_id, symbol_table);
629  const auto return_expr = return_sym.symbol_expr();
630  code.add(code_declt(return_expr), loc);
631  code.add(
633  return_expr,
634  ID_cprover_associate_array_to_pointer_func,
635  {array, pointer},
636  symbol_table),
637  loc);
638 }
639 
649  const exprt &array,
650  const exprt &length,
651  symbol_table_baset &symbol_table,
652  const source_locationt &loc,
653  const irep_idt &function_id,
654  code_blockt &code)
655 {
656  const symbolt &return_sym = fresh_java_symbol(
657  java_int_type(), "return_array", loc, function_id, symbol_table);
658  const auto return_expr = return_sym.symbol_expr();
659  code.add(code_declt(return_expr), loc);
660  code.add(
662  return_expr,
663  ID_cprover_associate_length_to_array_func,
664  {array, length},
665  symbol_table),
666  loc);
667 }
668 
681  const exprt &pointer,
682  const exprt &length,
683  const irep_idt &char_range,
684  symbol_table_baset &symbol_table,
685  const source_locationt &loc,
686  const irep_idt &function_id,
687  code_blockt &code)
688 {
689  PRECONDITION(pointer.type().id() == ID_pointer);
690  const symbolt &return_sym = fresh_java_symbol(
691  java_int_type(), "cnstr_added", loc, function_id, symbol_table);
692  const auto return_expr = return_sym.symbol_expr();
693  code.add(code_declt(return_expr), loc);
694  const constant_exprt char_set_expr(char_range, string_typet());
695  code.add(
697  return_expr,
698  ID_cprover_string_constrain_characters_func,
699  {length, pointer, char_set_expr},
700  symbol_table),
701  loc);
702 }
703 
721  const irep_idt &function_id,
722  const exprt::operandst &arguments,
723  const source_locationt &loc,
724  symbol_table_baset &symbol_table,
725  code_blockt &code)
726 {
727  // int return_code;
728  const symbolt return_code_sym = fresh_java_symbol(
729  java_int_type(),
730  std::string("return_code_") + function_id.c_str(),
731  loc,
732  function_id,
733  symbol_table);
734  const auto return_code = return_code_sym.symbol_expr();
735  code.add(code_declt(return_code), loc);
736 
737  const refined_string_exprt string_expr =
738  make_nondet_string_expr(loc, function_id, symbol_table, code);
739 
740  // args is { str.length, str.content, arguments... }
741  exprt::operandst args;
742  args.push_back(string_expr.length());
743  args.push_back(string_expr.content());
744  args.insert(args.end(), arguments.begin(), arguments.end());
745 
746  // return_code = <function_id>_data(args)
747  code.add(
749  return_code, function_id, args, symbol_table),
750  loc);
751 
752  return string_expr;
753 }
754 
768  const exprt &lhs,
769  const exprt &rhs_array,
770  const exprt &rhs_length,
771  const symbol_table_baset &symbol_table,
772  bool is_constructor)
773 {
776 
777  if(is_constructor)
778  {
779  // A String has a field Object with @clsid = String
780  struct_tag_typet jlo_tag("java::java.lang.Object");
781  struct_exprt jlo_init({}, jlo_tag);
782  irep_idt clsid = get_tag(lhs.type().subtype());
783  namespacet ns(symbol_table);
784  java_root_class_init(jlo_init, ns.follow_tag(jlo_tag), clsid);
785 
786  struct_exprt struct_rhs({jlo_init, rhs_length, rhs_array}, deref.type());
787  return code_assignt(checked_dereference(lhs), struct_rhs);
788  }
789  else
790  {
791  return code_blockt(
792  {code_assignt(get_length(deref, symbol_table), rhs_length),
793  code_assignt(get_data(deref, symbol_table), rhs_array)});
794  }
795 }
796 
809  const exprt &lhs,
810  const refined_string_exprt &rhs,
811  const symbol_table_baset &symbol_table,
812  bool is_constructor)
813 {
815  lhs, rhs.content(), rhs.length(), symbol_table, is_constructor);
816 }
817 
828  const refined_string_exprt &lhs,
829  const exprt &rhs,
830  const source_locationt &loc,
831  const symbol_table_baset &symbol_table,
832  code_blockt &code)
833 {
835 
836  const dereference_exprt deref = checked_dereference(rhs);
837 
838  // Although we should not reach this code if rhs is null, the association
839  // `pointer -> length` is added to the solver anyway, so we have to make sure
840  // the length is set to something reasonable.
841  auto rhs_length = if_exprt(
843  from_integer(0, lhs.length().type()),
844  get_length(deref, symbol_table));
845  rhs_length.set(ID_mode, ID_java);
846 
847  // Assignments
848  code.add(code_assignt(lhs.length(), rhs_length), loc);
849  exprt data_as_array = get_data(deref, symbol_table);
850  code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc);
851 }
852 
865  const std::string &s,
866  const source_locationt &loc,
867  symbol_table_baset &symbol_table,
868  code_blockt &code)
869 {
871  ID_cprover_string_literal_func,
873  loc,
874  symbol_table,
875  code);
876 }
877 
885  const java_method_typet &type,
886  const source_locationt &loc,
887  const irep_idt &function_id,
888  symbol_table_baset &symbol_table)
889 {
890  // Getting the argument
892  PRECONDITION(params.size()==1);
893  PRECONDITION(!params[0].get_identifier().empty());
894  const symbol_exprt arg(params[0].get_identifier(), params[0].type());
895 
896  // Holder for output code
897  code_blockt code;
898 
899  // Declaring and allocating String * str
900  const exprt str = allocate_fresh_string(
901  type.return_type(), loc, function_id, symbol_table, code);
902 
903  // Expression representing 0.0
904  const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
905  ieee_floatt zero_float(float_spec);
906  zero_float.from_float(0.0);
907  const constant_exprt zero = zero_float.to_expr();
908 
909  // For each possible case with have a condition and a string_exprt
910  std::vector<exprt> condition_list;
911  std::vector<refined_string_exprt> string_expr_list;
912 
913  // Case of computerized scientific notation
914  condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
915  const refined_string_exprt sci_notation = string_expr_of_function(
916  ID_cprover_string_of_float_scientific_notation_func,
917  {arg},
918  loc,
919  symbol_table,
920  code);
921  string_expr_list.push_back(sci_notation);
922 
923  // Subcase of negative scientific notation
924  condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
925  const refined_string_exprt minus_sign =
926  string_literal_to_string_expr("-", loc, symbol_table, code);
927  const refined_string_exprt neg_sci_notation = string_expr_of_function(
928  ID_cprover_string_concat_func,
929  {minus_sign, sci_notation},
930  loc,
931  symbol_table,
932  code);
933  string_expr_list.push_back(neg_sci_notation);
934 
935  // Case of NaN
936  condition_list.push_back(isnan_exprt(arg));
937  const refined_string_exprt nan =
938  string_literal_to_string_expr("NaN", loc, symbol_table, code);
939  string_expr_list.push_back(nan);
940 
941  // Case of Infinity
942  extractbit_exprt is_neg(arg, float_spec.width()-1);
943  condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
944  const refined_string_exprt infinity =
945  string_literal_to_string_expr("Infinity", loc, symbol_table, code);
946  string_expr_list.push_back(infinity);
947 
948  // Case -Infinity
949  condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
950  const refined_string_exprt minus_infinity =
951  string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
952  string_expr_list.push_back(minus_infinity);
953 
954  // Case of 0.0
955  // Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt,
956  // the latter disregards the sign
957  condition_list.push_back(equal_exprt(arg, zero));
958  const refined_string_exprt zero_string =
959  string_literal_to_string_expr("0.0", loc, symbol_table, code);
960  string_expr_list.push_back(zero_string);
961 
962  // Case of -0.0
963  ieee_floatt minus_zero_float(float_spec);
964  minus_zero_float.from_float(-0.0f);
965  condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
966  const refined_string_exprt minus_zero_string =
967  string_literal_to_string_expr("-0.0", loc, symbol_table, code);
968  string_expr_list.push_back(minus_zero_string);
969 
970  // Case of simple notation
971  ieee_floatt bound_inf_float(float_spec);
972  ieee_floatt bound_sup_float(float_spec);
973  bound_inf_float.from_float(1e-3f);
974  bound_sup_float.from_float(1e7f);
975  bound_inf_float.change_spec(float_spec);
976  bound_sup_float.change_spec(float_spec);
977  const constant_exprt bound_inf = bound_inf_float.to_expr();
978  const constant_exprt bound_sup = bound_sup_float.to_expr();
979 
980  const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf),
981  binary_relation_exprt(arg, ID_lt, bound_sup)};
982  condition_list.push_back(is_simple_float);
983 
984  const refined_string_exprt simple_notation = string_expr_of_function(
985  ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
986  string_expr_list.push_back(simple_notation);
987 
988  // Case of a negative number in simple notation
989  const and_exprt is_neg_simple_float{
990  binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
991  binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))};
992  condition_list.push_back(is_neg_simple_float);
993 
994  const refined_string_exprt neg_simple_notation = string_expr_of_function(
995  ID_cprover_string_concat_func,
996  {minus_sign, simple_notation},
997  loc,
998  symbol_table,
999  code);
1000  string_expr_list.push_back(neg_simple_notation);
1001 
1002  // Combining all cases
1003  INVARIANT(
1004  string_expr_list.size()==condition_list.size(),
1005  "number of created strings should correspond to number of conditions");
1006 
1007  // We do not check the condition of the first element in the list as it
1008  // will be reached only if all other conditions are not satisfied.
1010  str, string_expr_list[0], symbol_table, true);
1011  for(std::size_t i=1; i<condition_list.size(); i++)
1012  {
1013  tmp_code = code_ifthenelset(
1014  condition_list[i],
1016  str, string_expr_list[i], symbol_table, true),
1017  tmp_code);
1018  }
1019  code.add(tmp_code, loc);
1020 
1021  // Return str
1022  code.add(code_returnt(str), loc);
1023  return code;
1024 }
1025 
1042  const irep_idt &function_id,
1043  const java_method_typet &type,
1044  const source_locationt &loc,
1045  symbol_table_baset &symbol_table,
1046  bool is_constructor)
1047 {
1049 
1050  // The first parameter is the object to be initialized
1051  PRECONDITION(!params.empty());
1052  PRECONDITION(!params[0].get_identifier().empty());
1053  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1054  if(is_constructor)
1055  params.erase(params.begin());
1056 
1057  // Holder for output code
1058  code_blockt code;
1059 
1060  // Processing parameters
1061  const exprt::operandst args =
1062  process_parameters(params, loc, function_id, symbol_table, code);
1063 
1064  // string_expr <- function(arg1)
1065  const refined_string_exprt string_expr =
1066  string_expr_of_function(function_id, args, loc, symbol_table, code);
1067 
1068  // arg_this <- string_expr
1069  code.add(
1071  arg_this, string_expr, symbol_table, is_constructor),
1072  loc);
1073 
1074  return code;
1075 }
1076 
1086  const irep_idt &function_id,
1087  const java_method_typet &type,
1088  const source_locationt &loc,
1089  symbol_table_baset &symbol_table)
1090 {
1091  // This is similar to assign functions except we return a pointer to `this`
1092  const java_method_typet::parameterst &params = type.parameters();
1093  PRECONDITION(!params.empty());
1094  PRECONDITION(!params[0].get_identifier().empty());
1095  code_blockt code;
1096  code.add(
1097  make_assign_function_from_call(function_id, type, loc, symbol_table), loc);
1098  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1099  code.add(code_returnt(arg_this), loc);
1100  return code;
1101 }
1102 
1111  const irep_idt &function_id,
1112  const java_method_typet &type,
1113  const source_locationt &loc,
1114  symbol_table_baset &symbol_table)
1115 {
1116  // This is similar to initialization function except we do not ignore
1117  // the first argument
1119  function_id, type, loc, symbol_table, false);
1120 }
1121 
1134  const java_method_typet &type,
1135  const source_locationt &loc,
1136  const irep_idt &function_id,
1137  symbol_table_baset &symbol_table)
1138 {
1140  PRECONDITION(!params.empty());
1141  PRECONDITION(!params[0].get_identifier().empty());
1142  const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1143 
1144  // Code to be returned
1145  code_blockt code;
1146 
1147  // class_identifier is obj->@class_identifier
1148  const member_exprt class_identifier{
1150 
1151  // string_expr = cprover_string_literal(this->@class_identifier)
1152  const refined_string_exprt string_expr = string_expr_of_function(
1153  ID_cprover_string_literal_func,
1154  {class_identifier},
1155  loc,
1156  symbol_table,
1157  code);
1158 
1159  // string_expr1 = substr(string_expr, 6)
1160  // We do this to remove the "java::" prefix
1161  const refined_string_exprt string_expr1 = string_expr_of_function(
1162  ID_cprover_string_substring_func,
1163  {string_expr, from_integer(6, java_int_type())},
1164  loc,
1165  symbol_table,
1166  code);
1167 
1168  // string1 = (String*) string_expr
1169  const typet &string_ptr_type = type.return_type();
1170  const exprt string1 = allocate_fresh_string(
1171  string_ptr_type, loc, function_id, symbol_table, code);
1172  code.add(
1174  string1, string_expr1, symbol_table, true),
1175  loc);
1176 
1177  // > return string1;
1178  code.add(code_returnt{string1}, loc);
1179  return code;
1180 }
1181 
1193  const irep_idt &function_id,
1194  const java_method_typet &type,
1195  const source_locationt &loc,
1196  symbol_table_baset &symbol_table)
1197 {
1198  code_blockt code;
1199  const exprt::operandst args =
1200  process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1201  code.add(
1203  function_id, args, type.return_type(), symbol_table),
1204  loc);
1205  return code;
1206 }
1207 
1223  const irep_idt &function_id,
1224  const java_method_typet &type,
1225  const source_locationt &loc,
1226  symbol_table_baset &symbol_table)
1227 {
1228  // Code for the output
1229  code_blockt code;
1230 
1231  // Calling the function
1232  const exprt::operandst arguments =
1233  process_parameters(type.parameters(), loc, function_id, symbol_table, code);
1234 
1235  // String expression that will hold the result
1236  const refined_string_exprt string_expr =
1237  string_expr_of_function(function_id, arguments, loc, symbol_table, code);
1238 
1239  // Assign to string
1240  const exprt str = allocate_fresh_string(
1241  type.return_type(), loc, function_id, symbol_table, code);
1242  code.add(
1244  str, string_expr, symbol_table, true),
1245  loc);
1246 
1247  // Return value
1248  code.add(code_returnt(str), loc);
1249  return code;
1250 }
1251 
1267  const java_method_typet &type,
1268  const source_locationt &loc,
1269  const irep_idt &function_id,
1270  symbol_table_baset &symbol_table)
1271 {
1272  // Code for the output
1273  code_blockt code;
1274 
1275  // String expression that will hold the result
1276  const refined_string_exprt string_expr =
1277  decl_string_expr(loc, function_id, symbol_table, code);
1278 
1279  // Assign the argument to string_expr
1280  const java_method_typet::parametert &op = type.parameters()[0];
1282  const symbol_exprt arg0{op.get_identifier(), op.type()};
1284  string_expr, arg0, loc, symbol_table, code);
1285 
1286  // Allocate and assign the string
1287  const exprt str = allocate_fresh_string(
1288  type.return_type(), loc, function_id, symbol_table, code);
1289  code.add(
1291  str, string_expr, symbol_table, true),
1292  loc);
1293 
1294  // Return value
1295  code.add(code_returnt(str), loc);
1296  return code;
1297 }
1298 
1312  const java_method_typet &type,
1313  const source_locationt &loc,
1314  const irep_idt &function_id,
1315  symbol_table_baset &symbol_table)
1316 {
1317  (void)function_id;
1318 
1319  // Code for the output
1320  code_blockt code;
1321 
1322  // String expression that will hold the result
1323  const refined_string_exprt string_expr =
1324  decl_string_expr(loc, function_id, symbol_table, code);
1325 
1326  // Assign argument to a string_expr
1327  const java_method_typet::parameterst &params = type.parameters();
1328  PRECONDITION(!params[0].get_identifier().empty());
1329  PRECONDITION(!params[1].get_identifier().empty());
1330  const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
1332  string_expr, arg1, loc, symbol_table, code);
1333 
1334  // Assign string_expr to `this` object
1335  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1336  code.add(
1338  arg_this, string_expr, symbol_table, true),
1339  loc);
1340 
1341  return code;
1342 }
1343 
1356  const java_method_typet &type,
1357  const source_locationt &loc,
1358  const irep_idt &function_id,
1359  symbol_table_baset &symbol_table)
1360 {
1361  (void)function_id;
1362 
1363  const java_method_typet::parameterst &params = type.parameters();
1364  PRECONDITION(!params[0].get_identifier().empty());
1365  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1366  const dereference_exprt deref = checked_dereference(arg_this);
1367 
1368  code_returnt ret(get_length(deref, symbol_table));
1369  ret.add_source_location() = loc;
1370 
1371  return ret;
1372 }
1373 
1375  const irep_idt &function_id) const
1376 {
1377  for(const id_mapt *map : id_maps)
1378  if(map->count(function_id) != 0)
1379  return true;
1380 
1381  return conversion_table.count(function_id) != 0;
1382 }
1383 
1384 template <typename TMap, typename TContainer>
1385 void add_keys_to_container(const TMap &map, TContainer &container)
1386 {
1387  static_assert(
1388  std::is_same<typename TMap::key_type,
1389  typename TContainer::value_type>::value,
1390  "TContainer value_type doesn't match TMap key_type");
1391  std::transform(
1392  map.begin(),
1393  map.end(),
1394  std::inserter(container, container.begin()),
1395  [](const typename TMap::value_type &pair) { return pair.first; });
1396 }
1397 
1399  std::unordered_set<irep_idt> &methods) const
1400 {
1401  for(const id_mapt *map : id_maps)
1402  add_keys_to_container(*map, methods);
1403 
1405 }
1406 
1414  const symbolt &symbol,
1415  symbol_table_baset &symbol_table)
1416 {
1417  const irep_idt &function_id = symbol.name;
1418  const java_method_typet &type = to_java_method_type(symbol.type);
1419  const source_locationt &loc = symbol.location;
1420  auto it_id=cprover_equivalent_to_java_function.find(function_id);
1421  if(it_id!=cprover_equivalent_to_java_function.end())
1422  return make_function_from_call(it_id->second, type, loc, symbol_table);
1423 
1427  it_id->second, type, loc, symbol_table);
1428 
1429  it_id=cprover_equivalent_to_java_constructor.find(function_id);
1432  it_id->second, type, loc, symbol_table);
1433 
1437  it_id->second, type, loc, symbol_table);
1438 
1439  it_id=cprover_equivalent_to_java_assign_function.find(function_id);
1442  it_id->second, type, loc, symbol_table);
1443 
1444  auto it=conversion_table.find(function_id);
1445  INVARIANT(
1446  it != conversion_table.end(), "Couldn't retrieve code for string method");
1447 
1448  return it->second(type, loc, function_id, symbol_table);
1449 }
1450 
1456  irep_idt class_name)
1457 {
1458  return string_types.find(class_name)!=string_types.end();
1459 }
1460 
1462 {
1463  string_types = std::unordered_set<irep_idt>{"java.lang.String",
1464  "java.lang.StringBuilder",
1465  "java.lang.CharSequence",
1466  "java.lang.StringBuffer"};
1467 }
1468 
1471 {
1473 
1474  // The following list of function is organized by libraries, with
1475  // constructors first and then methods in alphabetic order.
1476  // Methods that are not supported here should ultimately have Java models
1477  // provided for them in the class-path.
1478 
1479  // CProverString library
1481  ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1482  "lang/CharSequence;II)"
1483  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1484  // CProverString.charAt differs from the Java String.charAt in that no
1485  // exception is raised for the out of bounds case.
1487  ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1488  ID_cprover_string_char_at_func;
1490  ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1491  ID_cprover_string_char_at_func;
1493  ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1494  ID_cprover_string_code_point_at_func;
1496  ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1497  ID_cprover_string_code_point_before_func;
1499  ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1500  ID_cprover_string_code_point_count_func;
1502  ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1503  "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1505  ["java::org.cprover.CProverString.delete:(Ljava/lang/"
1506  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1507  ID_cprover_string_delete_func;
1509  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1510  "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1511  ID_cprover_string_delete_char_at_func;
1513  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1514  "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1515  ID_cprover_string_delete_char_at_func;
1516 
1517  std::string format_signature = "java::org.cprover.CProverString.format:(";
1518  for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1519  format_signature += "Ljava/lang/String;";
1520  format_signature += ")Ljava/lang/String;";
1522  ID_cprover_string_format_func;
1523 
1525  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1526  "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1528  ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1529  "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1531  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1532  "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1534  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1535  "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1537  ["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1538  ID_cprover_string_set_length_func;
1540  ["java::org.cprover.CProverString.setLength:(Ljava/lang/"
1541  "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1543  ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1544  "lang/CharSequence;"] = ID_cprover_string_substring_func;
1545  // CProverString.substring differs from the Java String.substring in that no
1546  // exception is raised for the out of bounds case.
1548  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1549  "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1551  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1552  "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1554  ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
1555  "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1557  ["java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1558  ID_cprover_string_of_int_func;
1560  ["java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1561  ID_cprover_string_of_int_func;
1563  ["java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1564  ID_cprover_string_of_long_func;
1566  ["java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1567  ID_cprover_string_of_long_func;
1569  ["java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1570  std::bind(
1572  this,
1573  std::placeholders::_1,
1574  std::placeholders::_2,
1575  std::placeholders::_3,
1576  std::placeholders::_4);
1578  ["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1579  ID_cprover_string_parse_int_func;
1581  ["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1582  ID_cprover_string_parse_int_func;
1583 
1584  // String library
1585  conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1586  std::bind(
1588  this,
1589  std::placeholders::_1,
1590  std::placeholders::_2,
1591  std::placeholders::_3,
1592  std::placeholders::_4);
1594  ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1596  this,
1597  std::placeholders::_1,
1598  std::placeholders::_2,
1599  std::placeholders::_3,
1600  std::placeholders::_4);
1602  ["java::java.lang.String.<init>:()V"]=
1603  ID_cprover_string_empty_string_func;
1604 
1606  ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1607  ID_cprover_string_compare_to_func;
1609  ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1610  ID_cprover_string_concat_func;
1612  ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1613  ID_cprover_string_contains_func;
1615  ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1616  ID_cprover_string_endswith_func;
1618  ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1619  ID_cprover_string_equals_ignore_case_func;
1620 
1622  ["java::java.lang.String.indexOf:(I)I"]=
1623  ID_cprover_string_index_of_func;
1625  ["java::java.lang.String.indexOf:(II)I"]=
1626  ID_cprover_string_index_of_func;
1628  ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1629  ID_cprover_string_index_of_func;
1631  ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1632  ID_cprover_string_index_of_func;
1634  ["java::java.lang.String.isEmpty:()Z"]=
1635  ID_cprover_string_is_empty_func;
1637  ["java::java.lang.String.lastIndexOf:(I)I"]=
1638  ID_cprover_string_last_index_of_func;
1640  ["java::java.lang.String.lastIndexOf:(II)I"]=
1641  ID_cprover_string_last_index_of_func;
1643  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1644  ID_cprover_string_last_index_of_func;
1646  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1647  ID_cprover_string_last_index_of_func;
1648  conversion_table["java::java.lang.String.length:()I"] = std::bind(
1650  this,
1651  std::placeholders::_1,
1652  std::placeholders::_2,
1653  std::placeholders::_3,
1654  std::placeholders::_4);
1656  ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1657  ID_cprover_string_replace_func;
1659  ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
1660  ID_cprover_string_replace_func;
1662  ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1663  ID_cprover_string_startswith_func;
1665  ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1666  ID_cprover_string_startswith_func;
1668  ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1669  ID_cprover_string_to_lower_case_func;
1670  conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
1671  std::bind(
1673  this,
1674  std::placeholders::_1,
1675  std::placeholders::_2,
1676  std::placeholders::_3,
1677  std::placeholders::_4);
1679  ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1680  ID_cprover_string_to_upper_case_func;
1682  ["java::java.lang.String.trim:()Ljava/lang/String;"]=
1683  ID_cprover_string_trim_func;
1684 
1685  // StringBuilder library
1687  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1689  this,
1690  std::placeholders::_1,
1691  std::placeholders::_2,
1692  std::placeholders::_3,
1693  std::placeholders::_4);
1695  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1696  std::bind(
1698  this,
1699  std::placeholders::_1,
1700  std::placeholders::_2,
1701  std::placeholders::_3,
1702  std::placeholders::_4);
1704  ["java::java.lang.StringBuilder.<init>:()V"]=
1705  ID_cprover_string_empty_string_func;
1707  ["java::java.lang.StringBuilder.<init>:(I)V"] =
1708  ID_cprover_string_empty_string_func;
1709 
1711  ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1712  ID_cprover_string_concat_char_func;
1714  ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1715  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1717  ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1718  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1720  ["java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1721  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1723  ["java::java.lang.StringBuilder.appendCodePoint:(I)"
1724  "Ljava/lang/StringBuilder;"]=
1725  ID_cprover_string_concat_code_point_func;
1727  ["java::java.lang.StringBuilder.charAt:(I)C"]=
1728  ID_cprover_string_char_at_func;
1730  ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
1731  ID_cprover_string_code_point_at_func;
1733  ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1734  ID_cprover_string_code_point_before_func;
1736  ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
1737  ID_cprover_string_code_point_count_func;
1738  conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
1740  this,
1741  std::placeholders::_1,
1742  std::placeholders::_2,
1743  std::placeholders::_3,
1744  std::placeholders::_4);
1746  ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1747  ID_cprover_string_substring_func;
1749  ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1750  ID_cprover_string_substring_func;
1752  ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1754  this,
1755  std::placeholders::_1,
1756  std::placeholders::_2,
1757  std::placeholders::_3,
1758  std::placeholders::_4);
1759 
1760  // StringBuffer library
1762  ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1764  this,
1765  std::placeholders::_1,
1766  std::placeholders::_2,
1767  std::placeholders::_3,
1768  std::placeholders::_4);
1770  ["java::java.lang.StringBuffer.<init>:()V"]=
1771  ID_cprover_string_empty_string_func;
1772 
1774  ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1775  ID_cprover_string_concat_char_func;
1777  ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1778  "Ljava/lang/StringBuffer;"]=
1779  ID_cprover_string_concat_func;
1781  ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1782  "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1784  ["java::java.lang.StringBuffer.appendCodePoint:(I)"
1785  "Ljava/lang/StringBuffer;"]=
1786  ID_cprover_string_concat_code_point_func;
1788  ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
1789  ID_cprover_string_code_point_at_func;
1791  ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1792  ID_cprover_string_code_point_before_func;
1794  ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
1795  ID_cprover_string_code_point_count_func;
1797  ["java::java.lang.StringBuffer.length:()I"]=
1798  conversion_table["java::java.lang.String.length:()I"];
1800  ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1801  ID_cprover_string_substring_func;
1803  ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1805  this,
1806  std::placeholders::_1,
1807  std::placeholders::_2,
1808  std::placeholders::_3,
1809  std::placeholders::_4);
1810 
1811  // CharSequence library
1813  ["java::java.lang.CharSequence.charAt:(I)C"]=
1814  ID_cprover_string_char_at_func;
1816  ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1818  this,
1819  std::placeholders::_1,
1820  std::placeholders::_2,
1821  std::placeholders::_3,
1822  std::placeholders::_4);
1824  ["java::java.lang.CharSequence.length:()I"]=
1825  conversion_table["java::java.lang.String.length:()I"];
1826 
1827  // Other libraries
1829  ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1830  ID_cprover_string_of_int_hex_func;
1831  conversion_table["java::org.cprover.CProver.classIdentifier:("
1832  "Ljava/lang/Object;)Ljava/lang/String;"] =
1833  std::bind(
1835  this,
1836  std::placeholders::_1,
1837  std::placeholders::_2,
1838  std::placeholders::_3,
1839  std::placeholders::_4);
1840 }
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:281
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:402
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:252
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:617
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:1266
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:1355
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:173
java_root_class_init
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
Definition: java_root_class.cpp:43
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:648
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:1222
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
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2917
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:720
checked_dereference
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:212
data
Definition: kdev_t.h:24
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2993
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:315
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:405
and_exprt
Boolean AND.
Definition: std_expr.h:2166
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:1085
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:458
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:1374
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:1110
java_string_library_preprocess.h
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:1041
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
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:1133
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1461
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:309
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:137
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:585
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:827
equal_exprt
Equality.
Definition: std_expr.h:1196
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:82
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:173
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:749
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4140
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:183
notequal_exprt
Disequality.
Definition: std_expr.h:1254
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:864
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1645
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:209
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
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:4018
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:1311
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:1192
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:538
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:1398
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:151
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:483
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:1413
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:128
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:211
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:487
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:360
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:52
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:1955
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:160
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2658
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3434
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:884
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:105
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:318
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:1313
refined_string_type.h
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:767
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:114
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:3583
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:105
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:1455
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:509
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:548
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
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:520
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
loc
#define loc()
Definition: ansi_c_lex.yy.cpp:4684
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:1470
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:439
index_exprt
Array index operator.
Definition: std_expr.h:1299
get_length
static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
access length member
Definition: java_string_library_preprocess.cpp:379
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2815
java_types.h
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:257
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:298
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:60
java_utils.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:3935
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:808
java_string_library_preprocesst::string_types
std::unordered_set< irep_idt > string_types
Definition: java_string_library_preprocess.h:146
std_expr.h
string_expr.h
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:389
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:1385
java_string_library_preprocesst::is_java_string_type
static bool is_java_string_type(const typet &type)
Definition: java_string_library_preprocess.cpp:74
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:680
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:91
validation_modet::INVARIANT
@ INVARIANT
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3538
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:340
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:2872
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:37
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:569