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 
19 #include <util/arith_tools.h>
20 #include <util/std_expr.h>
21 #include <util/std_code.h>
22 #include <util/fresh_symbol.h>
24 #include <util/string_expr.h>
25 #include <util/c_types.h>
26 
27 #include "java_types.h"
28 #include "java_object_factory.h"
29 #include "java_utils.h"
30 
32 #include "java_root_class.h"
33 
36 static irep_idt get_tag(const typet &type)
37 {
39  if(type.id() == ID_struct_tag)
40  return to_struct_tag_type(type).get_identifier();
41  else if(type.id() == ID_struct)
42  return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
43  else
44  return "";
45 }
46 
52  const typet &type, const std::string &tag)
53 {
54  return irep_idt("java::" + tag) == get_tag(type);
55 }
56 
60  const typet &type)
61 {
62  if(type.id()==ID_pointer)
63  {
64  const pointer_typet &pt=to_pointer_type(type);
65  const typet &subtype=pt.subtype();
66  return is_java_string_type(subtype);
67  }
68  return false;
69 }
70 
74  const typet &type)
75 {
76  return java_type_matches_tag(type, "java.lang.String");
77 }
78 
82  const typet &type)
83 {
84  return java_type_matches_tag(type, "java.lang.StringBuilder");
85 }
86 
91  const typet &type)
92 {
93  if(type.id()==ID_pointer)
94  {
95  const pointer_typet &pt=to_pointer_type(type);
96  const typet &subtype=pt.subtype();
97  return is_java_string_builder_type(subtype);
98  }
99  return false;
100 }
101 
105  const typet &type)
106 {
107  return java_type_matches_tag(type, "java.lang.StringBuffer");
108 }
109 
114  const typet &type)
115 {
116  if(type.id()==ID_pointer)
117  {
118  const pointer_typet &pt=to_pointer_type(type);
119  const typet &subtype=pt.subtype();
120  return is_java_string_buffer_type(subtype);
121  }
122  return false;
123 }
124 
128  const typet &type)
129 {
130  return java_type_matches_tag(type, "java.lang.CharSequence");
131 }
132 
137  const typet &type)
138 {
139  if(type.id()==ID_pointer)
140  {
141  const pointer_typet &pt=to_pointer_type(type);
142  const typet &subtype=pt.subtype();
143  return is_java_char_sequence_type(subtype);
144  }
145  return false;
146 }
147 
151  const typet &type)
152 {
153  return java_type_matches_tag(type, "array[char]");
154 }
155 
160  const typet &type)
161 {
162  if(type.id()==ID_pointer)
163  {
164  const pointer_typet &pt=to_pointer_type(type);
165  const typet &subtype=pt.subtype();
166  return is_java_char_array_type(subtype);
167  }
168  return false;
169 }
170 
173 {
174  return java_int_type();
175 }
176 
181 std::vector<irep_idt>
183  const irep_idt &class_name)
184 {
185  if(!is_known_string_type(class_name))
186  return {};
187 
188  std::vector<irep_idt> bases;
189  bases.reserve(3);
190  if(class_name != "java.lang.CharSequence")
191  {
192  bases.push_back("java.io.Serializable");
193  bases.push_back("java.lang.CharSequence");
194  }
195  if(class_name == "java.lang.String")
196  bases.push_back("java.lang.Comparable");
197 
198  if(class_name == "java.lang.StringBuilder" ||
199  class_name == "java.lang.StringBuffer")
200  bases.push_back("java.lang.AbstractStringBuilder");
201 
202  return bases;
203 }
204 
209  const irep_idt &class_name, symbol_tablet &symbol_table)
210 {
211  java_class_typet string_type;
212  string_type.set_tag(class_name);
213  string_type.set_name("java::" + id2string(class_name));
214  string_type.components().resize(3);
215  string_type.components()[0].set_name("@java.lang.Object");
216  string_type.components()[0].set_pretty_name("@java.lang.Object");
217  string_type.components()[0].type() =
218  struct_tag_typet("java::java.lang.Object");
219  string_type.components()[1].set_name("length");
220  string_type.components()[1].set_pretty_name("length");
221  string_type.components()[1].type()=string_length_type();
222  string_type.components()[2].set_name("data");
223  string_type.components()[2].set_pretty_name("data");
224  string_type.components()[2].type() = pointer_type(java_char_type());
225  string_type.set_access(ID_public);
226  string_type.add_base(struct_tag_typet("java::java.lang.Object"));
227 
228  std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
229  for(const irep_idt &base_name : bases)
230  string_type.add_base(struct_tag_typet("java::" + id2string(base_name)));
231 
232  symbolt tmp_string_symbol;
233  tmp_string_symbol.name="java::"+id2string(class_name);
234  symbolt *string_symbol=nullptr;
235  symbol_table.move(tmp_string_symbol, string_symbol);
236  string_symbol->base_name=id2string(class_name);
237  string_symbol->pretty_name=id2string(class_name);
238  string_symbol->type=string_type;
239  string_symbol->is_type=true;
240  string_symbol->mode = ID_java;
241 }
242 
249  const typet &type,
250  const source_locationt &location,
251  symbol_tablet &symbol_table)
252 {
253  symbolt array_symbol=get_fresh_aux_symbol(
254  type,
255  "cprover_string_array",
256  "cprover_string_array",
257  location,
258  ID_java,
259  symbol_table);
260  array_symbol.is_static_lifetime=true;
261  return array_symbol.symbol_expr();
262 }
263 
272  const java_method_typet::parameterst &params,
273  const source_locationt &loc,
274  symbol_table_baset &symbol_table,
275  code_blockt &init_code)
276 {
277  exprt::operandst ops;
278  for(const auto &p : params)
279  {
280  symbol_exprt sym(p.get_identifier(), p.type());
281  ops.push_back(sym);
282  }
283  return process_operands(ops, loc, symbol_table, init_code);
284 }
285 
302  const exprt &expr_to_process,
303  const source_locationt &loc,
304  symbol_table_baset &symbol_table,
305  code_blockt &init_code)
306 {
308  const refined_string_exprt string_expr =
309  decl_string_expr(loc, symbol_table, init_code);
311  string_expr, expr_to_process, loc, symbol_table, init_code);
312  return string_expr;
313 }
314 
327  const exprt::operandst &operands,
328  const source_locationt &loc,
329  symbol_table_baset &symbol_table,
330  code_blockt &init_code)
331 {
332  exprt::operandst ops;
333  for(const auto &p : operands)
334  {
336  ops.push_back(
337  convert_exprt_to_string_exprt(p, loc, symbol_table, init_code));
338  else if(is_java_char_array_pointer_type(p.type()))
339  ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
340  else
341  ops.push_back(p);
342  }
343  return ops;
344 }
345 
357  const exprt::operandst &operands,
358  const source_locationt &loc,
359  symbol_table_baset &symbol_table,
360  code_blockt &init_code)
361 {
362  PRECONDITION(operands.size()==2);
363  exprt::operandst ops;
364  const exprt &op0=operands[0];
365  const exprt &op1 = operands[1];
367 
368  ops.push_back(
369  convert_exprt_to_string_exprt(op0, loc, symbol_table, init_code));
370 
371  // TODO: Manage the case where we have a non-String Object (this should
372  // probably be handled upstream. At any rate, the following code should be
373  // protected with assertions on the type of op1.
374  typecast_exprt tcast(op1, to_pointer_type(op0.type()));
375  ops.push_back(
376  convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code));
377  return ops;
378 }
379 
384 static const typet &
385 get_data_type(const typet &type, const symbol_tablet &symbol_table)
386 {
387  PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
388  if(type.id() == ID_struct_tag)
389  {
390  const symbolt &sym =
391  symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
392  CHECK_RETURN(sym.type.id() != ID_struct_tag);
393  return get_data_type(sym.type, symbol_table);
394  }
395  // else type id is ID_struct
396  const struct_typet &struct_type=to_struct_type(type);
397  return struct_type.component_type("data");
398 }
399 
404 static const typet &
405 get_length_type(const typet &type, const symbol_tablet &symbol_table)
406 {
407  PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag);
408  if(type.id() == ID_struct_tag)
409  {
410  const symbolt &sym =
411  symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier());
412  CHECK_RETURN(sym.type.id() != ID_struct_tag);
413  return get_length_type(sym.type, symbol_table);
414  }
415  // else type id is ID_struct
416  const struct_typet &struct_type=to_struct_type(type);
417  return struct_type.component_type("length");
418 }
419 
424 static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
425 {
426  return member_exprt(
427  expr, "length", get_length_type(expr.type(), symbol_table));
428 }
429 
434 static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
435 {
436  return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
437 }
438 
447  const exprt &array_pointer,
448  const source_locationt &loc,
449  symbol_table_baset &symbol_table,
450  code_blockt &code)
451 {
452  // array is *array_pointer
453  dereference_exprt array=
454  checked_dereference(array_pointer, array_pointer.type().subtype());
455  // array_data is array_pointer-> data
456  const exprt array_data = get_data(array, symbol_table);
457  symbolt sym_char_array = get_fresh_aux_symbol(
458  array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
459  symbol_exprt char_array=sym_char_array.symbol_expr();
460  // char_array = array_pointer->data
461  code.add(code_assignt(char_array, array_data), loc);
462 
463  // string_expr is `{ rhs->length; string_array }`
464  refined_string_exprt string_expr(
465  get_length(array, symbol_table), char_array, refined_string_type);
466 
467  dereference_exprt inf_array(
469 
471  string_expr.content(), inf_array, symbol_table, loc, code);
472 
473  return string_expr;
474 }
475 
483  const typet &type,
484  const source_locationt &loc,
485  symbol_table_baset &symbol_table)
486 {
487  symbolt string_symbol=get_fresh_aux_symbol(
488  type, "cprover_string", "cprover_string", loc, ID_java, symbol_table);
489  string_symbol.is_static_lifetime=true;
490  return string_symbol.symbol_expr();
491 }
492 
500  const source_locationt &loc,
501  symbol_table_baset &symbol_table,
502  code_blockt &code)
503 {
504  symbolt sym_length = get_fresh_aux_symbol(
505  index_type,
506  "cprover_string_length",
507  "cprover_string_length",
508  loc,
509  ID_java,
510  symbol_table);
511  symbol_exprt length_field=sym_length.symbol_expr();
512  pointer_typet array_type = pointer_type(java_char_type());
513  symbolt sym_content = get_fresh_aux_symbol(
514  array_type,
515  "cprover_string_content",
516  "cprover_string_content",
517  loc,
518  ID_java,
519  symbol_table);
520  symbol_exprt content_field = sym_content.symbol_expr();
521  code.add(code_declt(content_field), loc);
522  refined_string_exprt str(length_field, content_field, refined_string_type);
523  code.add(code_declt(length_field), loc);
524  return str;
525 }
526 
535  const source_locationt &loc,
536  const irep_idt &function_id,
537  symbol_table_baset &symbol_table,
538  code_blockt &code)
539 {
541  const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
542 
543  const side_effect_expr_nondett nondet_length(str.length().type(), loc);
544  code.add(code_assignt(str.length(), nondet_length), loc);
545 
546  exprt nondet_array_expr =
547  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
548 
549  address_of_exprt array_pointer(
550  index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
551 
553  array_pointer, nondet_array_expr, symbol_table, loc, code);
554 
556  nondet_array_expr, str.length(), symbol_table, loc, code);
557 
558  code.add(code_assignt(str.content(), array_pointer), loc);
559 
560  return refined_string_exprt(str.length(), str.content());
561 }
562 
571  const typet &type,
572  const source_locationt &loc,
573  const irep_idt &function_id,
574  symbol_table_baset &symbol_table,
575  code_blockt &code)
576 {
577  exprt str=fresh_string(type, loc, symbol_table);
578  allocate_dynamic_object_with_decl(str, symbol_table, loc, function_id, code);
579  return str;
580 }
581 
592  const exprt &lhs,
593  const irep_idt &function_name,
594  const exprt::operandst &arguments,
595  symbol_table_baset &symbol_table)
596 {
598  function_name, arguments, lhs.type(), symbol_table);
599  return code_assignt(lhs, fun_app);
600 }
601 
612  const irep_idt &function_name,
613  const exprt::operandst &arguments,
614  const typet &type,
615  symbol_table_baset &symbol_table)
616 {
618  function_name, arguments, type, symbol_table);
619  return code_returnt(fun_app);
620 }
621 
626 static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
627 {
628  side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
629  alloc.add_to_operands(size);
630  alloc.add_to_operands(false_exprt());
631  return code_assignt(lhs, alloc);
632 }
633 
641  symbol_table_baset &symbol_table,
642  const source_locationt &loc,
643  const irep_idt &function_id,
644  code_blockt &code)
645 {
646  const array_typet array_type(
648  const symbolt data_sym = get_fresh_aux_symbol(
649  pointer_type(array_type),
650  id2string(function_id),
651  "nondet_infinite_array_pointer",
652  loc,
653  ID_java,
654  symbol_table);
655 
656  const symbol_exprt data_pointer = data_sym.symbol_expr();
657  code.add(code_declt(data_pointer));
658  code.add(make_allocate_code(data_pointer, array_type.size()));
659  const exprt nondet_data = side_effect_expr_nondett(array_type, loc);
660  const exprt data = dereference_exprt(data_pointer, array_type);
661  code.add(code_assignt(data, nondet_data), loc);
662  return data;
663 }
664 
673  const exprt &pointer,
674  const exprt &array,
675  symbol_table_baset &symbol_table,
676  const source_locationt &loc,
677  code_blockt &code)
678 {
679  PRECONDITION(array.type().id() == ID_array);
680  PRECONDITION(pointer.type().id() == ID_pointer);
681  symbolt &return_sym = get_fresh_aux_symbol(
682  java_int_type(),
683  "return_array",
684  "return_array",
685  loc,
686  ID_java,
687  symbol_table);
688  auto return_expr = return_sym.symbol_expr();
689  code.add(code_declt(return_expr), loc);
690  code.add(
692  return_expr,
693  ID_cprover_associate_array_to_pointer_func,
694  {array, pointer},
695  symbol_table),
696  loc);
697 }
698 
707  const exprt &array,
708  const exprt &length,
709  symbol_table_baset &symbol_table,
710  const source_locationt &loc,
711  code_blockt &code)
712 {
713  symbolt &return_sym = get_fresh_aux_symbol(
714  java_int_type(),
715  "return_array",
716  "return_array",
717  loc,
718  ID_java,
719  symbol_table);
720  const auto return_expr = return_sym.symbol_expr();
721  code.add(code_declt(return_expr), loc);
722  code.add(
724  return_expr,
725  ID_cprover_associate_length_to_array_func,
726  {array, length},
727  symbol_table),
728  loc);
729 }
730 
742  const exprt &pointer,
743  const exprt &length,
744  const irep_idt &char_set,
745  symbol_table_baset &symbol_table,
746  const source_locationt &loc,
747  code_blockt &code)
748 {
749  PRECONDITION(pointer.type().id() == ID_pointer);
750  symbolt &return_sym = get_fresh_aux_symbol(
751  java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
752  const auto return_expr = return_sym.symbol_expr();
753  code.add(code_declt(return_expr), loc);
754  const constant_exprt char_set_expr(char_set, string_typet());
755  code.add(
757  return_expr,
758  ID_cprover_string_constrain_characters_func,
759  {length, pointer, char_set_expr},
760  symbol_table),
761  loc);
762 }
763 
781  const irep_idt &function_name,
782  const exprt::operandst &arguments,
783  const source_locationt &loc,
784  symbol_table_baset &symbol_table,
785  code_blockt &code)
786 {
787  // int return_code;
788  symbolt return_code_sym = get_fresh_aux_symbol(
789  java_int_type(),
790  std::string("return_code_") + function_name.c_str(),
791  std::string("return_code_") + function_name.c_str(),
792  loc,
793  ID_java,
794  symbol_table);
795  const auto return_code = return_code_sym.symbol_expr();
796  code.add(code_declt(return_code), loc);
797 
798  const refined_string_exprt string_expr =
799  make_nondet_string_expr(loc, function_name, symbol_table, code);
800 
801  // args is { str.length, str.content, arguments... }
802  exprt::operandst args;
803  args.push_back(string_expr.length());
804  args.push_back(string_expr.content());
805  args.insert(args.end(), arguments.begin(), arguments.end());
806 
807  // return_code = <function_name>_data(args)
808  code.add(
810  return_code, function_name, args, symbol_table),
811  loc);
812 
813  return string_expr;
814 }
815 
829  const exprt &lhs,
830  const exprt &rhs_array,
831  const exprt &rhs_length,
832  const symbol_table_baset &symbol_table,
833  bool is_constructor)
834 {
837 
838  if(is_constructor)
839  {
840  // A String has a field Object with @clsid = String
841  const symbolt &jlo_symbol = *symbol_table.lookup("java::java.lang.Object");
842  const struct_typet &jlo_struct = to_struct_type(jlo_symbol.type);
843  struct_exprt jlo_init(jlo_struct);
844  irep_idt clsid = get_tag(lhs.type().subtype());
845  java_root_class_init(jlo_init, jlo_struct, clsid);
846 
847  struct_exprt struct_rhs(deref.type());
848  struct_rhs.copy_to_operands(jlo_init);
849  struct_rhs.copy_to_operands(rhs_length);
850  struct_rhs.copy_to_operands(rhs_array);
851  return code_assignt(
852  checked_dereference(lhs, lhs.type().subtype()), struct_rhs);
853  }
854  else
855  {
856  return code_blockt(
857  {code_assignt(get_length(deref, symbol_table), rhs_length),
858  code_assignt(get_data(deref, symbol_table), rhs_array)});
859  }
860 }
861 
874  const exprt &lhs,
875  const refined_string_exprt &rhs,
876  const symbol_table_baset &symbol_table,
877  bool is_constructor)
878 {
880  lhs, rhs.content(), rhs.length(), symbol_table, is_constructor);
881 }
882 
893  const refined_string_exprt &lhs,
894  const exprt &rhs,
895  const source_locationt &loc,
896  const symbol_table_baset &symbol_table,
897  code_blockt &code)
898 {
900 
901  typet deref_type;
902  if(rhs.type().subtype().id() == ID_struct_tag)
903  deref_type =
904  symbol_table
905  .lookup_ref(to_struct_tag_type(rhs.type().subtype()).get_identifier())
906  .type;
907  else
908  deref_type=rhs.type().subtype();
909 
910  const dereference_exprt deref = checked_dereference(rhs, deref_type);
911 
912  // Although we should not reach this code if rhs is null, the association
913  // `pointer -> length` is added to the solver anyway, so we have to make sure
914  // the length is set to something reasonable.
915  auto rhs_length = if_exprt(
917  from_integer(0, lhs.length().type()),
918  get_length(deref, symbol_table));
919  rhs_length.set(ID_mode, ID_java);
920 
921  // Assignments
922  code.add(code_assignt(lhs.length(), rhs_length), loc);
923  const exprt data_as_array = get_data(deref, symbol_table);
924  code.add(code_assignt(lhs.content(), data_as_array), loc);
925 }
926 
939  const std::string &s,
940  const source_locationt &loc,
941  symbol_table_baset &symbol_table,
942  code_blockt &code)
943 {
944  const constant_exprt expr(s, string_typet());
946  ID_cprover_string_literal_func, {expr}, loc, symbol_table, code);
947 }
948 
956  const java_method_typet &type,
957  const source_locationt &loc,
958  const irep_idt &function_id,
959  symbol_table_baset &symbol_table)
960 {
961  // Getting the argument
963  PRECONDITION(params.size()==1);
964  const symbol_exprt arg(params[0].get_identifier(), params[0].type());
965 
966  // Holder for output code
967  code_blockt code;
968 
969  // Declaring and allocating String * str
971  type.return_type(), loc, function_id, symbol_table, code);
972 
973  // Expression representing 0.0
974  ieee_float_spect float_spec(to_floatbv_type(params[0].type()));
975  ieee_floatt zero_float(float_spec);
976  zero_float.from_float(0.0);
977  constant_exprt zero=zero_float.to_expr();
978 
979  // For each possible case with have a condition and a string_exprt
980  std::vector<exprt> condition_list;
981  std::vector<refined_string_exprt> string_expr_list;
982 
983  // Case of computerized scientific notation
984  condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
986  ID_cprover_string_of_float_scientific_notation_func,
987  {arg},
988  loc,
989  symbol_table,
990  code);
991  string_expr_list.push_back(sci_notation);
992 
993  // Subcase of negative scientific notation
994  condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
995  refined_string_exprt minus_sign =
996  string_literal_to_string_expr("-", loc, symbol_table, code);
998  ID_cprover_string_concat_func,
999  {minus_sign, sci_notation},
1000  loc,
1001  symbol_table,
1002  code);
1003  string_expr_list.push_back(neg_sci_notation);
1004 
1005  // Case of NaN
1006  condition_list.push_back(isnan_exprt(arg));
1007  refined_string_exprt nan =
1008  string_literal_to_string_expr("NaN", loc, symbol_table, code);
1009  string_expr_list.push_back(nan);
1010 
1011  // Case of Infinity
1012  extractbit_exprt is_neg(arg, float_spec.width()-1);
1013  condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
1014  refined_string_exprt infinity =
1015  string_literal_to_string_expr("Infinity", loc, symbol_table, code);
1016  string_expr_list.push_back(infinity);
1017 
1018  // Case -Infinity
1019  condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
1020  refined_string_exprt minus_infinity =
1021  string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
1022  string_expr_list.push_back(minus_infinity);
1023 
1024  // Case of simple notation
1025  ieee_floatt bound_inf_float(float_spec);
1026  ieee_floatt bound_sup_float(float_spec);
1027  bound_inf_float.from_float(1e-3f);
1028  bound_sup_float.from_float(1e7f);
1029  bound_inf_float.change_spec(float_spec);
1030  bound_sup_float.change_spec(float_spec);
1031  constant_exprt bound_inf=bound_inf_float.to_expr();
1032  constant_exprt bound_sup=bound_sup_float.to_expr();
1033 
1034  and_exprt is_simple_float(
1035  binary_relation_exprt(arg, ID_ge, bound_inf),
1036  binary_relation_exprt(arg, ID_lt, bound_sup));
1037  condition_list.push_back(is_simple_float);
1038 
1040  ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1041  string_expr_list.push_back(simple_notation);
1042 
1043  // Case of a negative number in simple notation
1044  and_exprt is_neg_simple_float(
1045  binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
1046  binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup)));
1047  condition_list.push_back(is_neg_simple_float);
1048 
1049  refined_string_exprt neg_simple_notation = string_expr_of_function(
1050  ID_cprover_string_concat_func,
1051  {minus_sign, simple_notation},
1052  loc,
1053  symbol_table,
1054  code);
1055  string_expr_list.push_back(neg_simple_notation);
1056 
1057  // Combining all cases
1058  INVARIANT(
1059  string_expr_list.size()==condition_list.size(),
1060  "number of created strings should correspond to number of conditions");
1061 
1062  // We do not check the condition of the first element in the list as it
1063  // will be reached only if all other conditions are not satisfied.
1065  str, string_expr_list[0], symbol_table, true);
1066  for(std::size_t i=1; i<condition_list.size(); i++)
1067  {
1068  tmp_code = code_ifthenelset(
1069  condition_list[i],
1071  str, string_expr_list[i], symbol_table, true),
1072  tmp_code);
1073  }
1074  code.add(tmp_code, loc);
1075 
1076  // Return str
1077  code.add(code_returnt(str), loc);
1078  return code;
1079 }
1080 
1097  const irep_idt &function_name,
1098  const java_method_typet &type,
1099  const source_locationt &loc,
1100  symbol_table_baset &symbol_table,
1101  bool is_constructor)
1102 {
1104 
1105  // The first parameter is the object to be initialized
1106  PRECONDITION(!params.empty());
1107  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1108  if(is_constructor)
1109  params.erase(params.begin());
1110 
1111  // Holder for output code
1112  code_blockt code;
1113 
1114  // Processing parameters
1115  exprt::operandst args=process_parameters(params, loc, symbol_table, code);
1116 
1117  // string_expr <- function(arg1)
1118  refined_string_exprt string_expr =
1119  string_expr_of_function(function_name, args, loc, symbol_table, code);
1120 
1121  // arg_this <- string_expr
1122  code.add(
1124  arg_this, string_expr, symbol_table, is_constructor),
1125  loc);
1126 
1127  return code;
1128 }
1129 
1139  const irep_idt &function_name,
1140  const java_method_typet &type,
1141  const source_locationt &loc,
1142  symbol_table_baset &symbol_table)
1143 {
1144  // This is similar to assign functions except we return a pointer to `this`
1146  PRECONDITION(!params.empty());
1147  code_blockt code;
1148  code.add(
1149  make_assign_function_from_call(function_name, type, loc, symbol_table),
1150  loc);
1151  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1152  code.add(code_returnt(arg_this), loc);
1153  return code;
1154 }
1155 
1164  const irep_idt &function_name,
1165  const java_method_typet &type,
1166  const source_locationt &loc,
1167  symbol_table_baset &symbol_table)
1168 {
1169  // This is similar to initialization function except we do not ignore
1170  // the first argument
1172  function_name, type, loc, symbol_table, false);
1173 }
1174 
1196  const exprt &object,
1197  irep_idt type_name,
1198  const source_locationt &loc,
1199  symbol_table_baset &symbol_table,
1200  code_blockt &code)
1201 {
1202  optionalt<struct_tag_typet> object_type;
1203 
1204  typet value_type;
1205  if(type_name==ID_boolean)
1206  {
1207  value_type=java_boolean_type();
1208  object_type = struct_tag_typet("java::java.lang.Boolean");
1209  }
1210  else if(type_name==ID_char)
1211  {
1212  value_type=java_char_type();
1213  object_type = struct_tag_typet("java::java.lang.Character");
1214  }
1215  else if(type_name==ID_byte)
1216  {
1217  value_type=java_byte_type();
1218  object_type = struct_tag_typet("java::java.lang.Byte");
1219  }
1220  else if(type_name==ID_short)
1221  {
1222  value_type=java_short_type();
1223  object_type = struct_tag_typet("java::java.lang.Short");
1224  }
1225  else if(type_name==ID_int)
1226  {
1227  value_type=java_int_type();
1228  object_type = struct_tag_typet("java::java.lang.Integer");
1229  }
1230  else if(type_name==ID_long)
1231  {
1232  value_type=java_long_type();
1233  object_type = struct_tag_typet("java::java.lang.Long");
1234  }
1235  else if(type_name==ID_float)
1236  {
1237  value_type=java_float_type();
1238  object_type = struct_tag_typet("java::java.lang.Float");
1239  }
1240  else if(type_name==ID_double)
1241  {
1242  value_type=java_double_type();
1243  object_type = struct_tag_typet("java::java.lang.Double");
1244  }
1245  else if(type_name==ID_void)
1246  return {};
1247  else
1248  UNREACHABLE;
1249 
1250  DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");
1251 
1252  // declare tmp_type_name to hold the value
1253  std::string aux_name="tmp_"+id2string(type_name);
1255  value_type, aux_name, aux_name, loc, ID_java, symbol_table);
1256  auto value = symbol.symbol_expr();
1257 
1258  // Check that the type of the object is in the symbol table,
1259  // otherwise there is no safe way of finding its value.
1260  if(
1261  const auto maybe_symbol =
1262  symbol_table.lookup(object_type->get_identifier()))
1263  {
1264  struct_typet struct_type=to_struct_type(maybe_symbol->type);
1265  // Check that the type has a value field
1266  const struct_union_typet::componentt value_comp=
1267  struct_type.get_component("value");
1268  if(!value_comp.is_nil())
1269  {
1271  dereference_exprt deref(
1273  member_exprt deref_value(deref, value_comp.get_name(), value_comp.type());
1274  code.add(code_assignt(value, deref_value), loc);
1275  return value;
1276  }
1277  }
1278 
1279  warning() << object_type->get_identifier()
1280  << " not available to format function" << eom;
1281  code.add(code_declt(value), loc);
1282  return value;
1283 }
1284 
1294  const exprt &argv,
1295  std::size_t index)
1296 {
1297  dereference_exprt deref_objs(argv, argv.type().subtype());
1298  pointer_typet empty_pointer=pointer_type(empty_typet());
1299  pointer_typet pointer_of_pointer=pointer_type(empty_pointer);
1300  member_exprt data_member(deref_objs, "data", pointer_of_pointer);
1301  plus_exprt data_pointer_plus_index(
1302  data_member, from_integer(index, java_int_type()), data_member.type());
1303  return dereference_exprt(
1304  data_pointer_plus_index, data_pointer_plus_index.type().subtype());
1305 }
1306 
1339  const exprt &argv,
1340  std::size_t index,
1341  const struct_typet &structured_type,
1342  const source_locationt &loc,
1343  const irep_idt &function_id,
1344  symbol_table_baset &symbol_table,
1345  code_blockt &code)
1346 {
1347  // Declarations of the fields of arg_i_struct
1348  // arg_i_struct is { arg_i_string_expr, tmp_int, tmp_char, ... }
1349  struct_exprt arg_i_struct(structured_type);
1350  std::list<exprt> field_exprs;
1351  for(const auto & comp : structured_type.components())
1352  {
1353  const irep_idt &name=comp.get_name();
1354  const typet &type=comp.type();
1355  exprt field_expr;
1356  if(name!="string_expr")
1357  {
1358  std::string tmp_name="tmp_"+id2string(name);
1359  symbolt field_symbol = get_fresh_aux_symbol(
1360  type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
1361  auto field_symbol_expr = field_symbol.symbol_expr();
1362  field_expr = field_symbol_expr;
1363  code.add(code_declt(field_symbol_expr), loc);
1364  }
1365  else
1366  field_expr =
1367  make_nondet_string_expr(loc, function_id, symbol_table, code);
1368 
1369  field_exprs.push_back(field_expr);
1370  arg_i_struct.copy_to_operands(field_expr);
1371  }
1372 
1373  // arg_i = argv[index]
1374  exprt obj=get_object_at_index(argv, index);
1375  symbolt object_symbol = get_fresh_aux_symbol(
1376  obj.type(),
1377  id2string(function_id),
1378  "tmp_format_obj",
1379  loc,
1380  ID_java,
1381  symbol_table);
1382  symbol_exprt arg_i=object_symbol.symbol_expr();
1384  arg_i, symbol_table, loc, function_id, code);
1385  code.add(code_assignt(arg_i, obj), loc);
1386  code.add(
1387  code_assumet(
1388  not_exprt(
1389  equal_exprt(arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))),
1390  loc);
1391 
1392  code_blockt code_not_null;
1393 
1394  // Assigning all the fields of arg_i_struct
1395  for(const auto &comp : structured_type.components())
1396  {
1397  const irep_idt &name=comp.get_name();
1398  exprt field_expr=field_exprs.front();
1399  field_exprs.pop_front();
1400 
1401  if(name=="string_expr")
1402  {
1403  pointer_typet string_pointer =
1404  java_reference_type(struct_tag_typet("java::java.lang.String"));
1405  typecast_exprt arg_i_as_string(arg_i, string_pointer);
1407  to_string_expr(field_expr),
1408  arg_i_as_string,
1409  loc,
1410  symbol_table,
1411  code_not_null);
1412  }
1413  else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
1414  {
1415  const auto value = get_primitive_value_of_object(
1416  arg_i, name, loc, symbol_table, code_not_null);
1417  if(value.has_value())
1418  code_not_null.add(code_assignt(field_expr, *value), loc);
1419  else
1420  code_not_null.add(code_assignt(field_expr, nil_exprt()), loc);
1421  }
1422  else
1423  {
1424  // TODO: date_time and hash_code not implemented
1425  }
1426  }
1427 
1428  code.add(code_not_null, loc);
1429  return arg_i_struct;
1430 }
1431 
1445  const java_method_typet &type,
1446  const source_locationt &loc,
1447  const irep_idt &function_id,
1448  symbol_table_baset &symbol_table)
1449 {
1450  PRECONDITION(type.parameters().size()==2);
1451  code_blockt code;
1453  type.parameters(), loc, symbol_table, code);
1454  INVARIANT(args.size()==2, "String.format should have two arguments");
1455 
1456  // The argument can be:
1457  // a string, an integer, a floating point, a character, a boolean,
1458  // an object of which we take the hash code, or a date/time
1459  struct_typet structured_type;
1460  structured_type.components().emplace_back("string_expr", refined_string_type);
1461  structured_type.components().emplace_back(ID_int, java_int_type());
1462  structured_type.components().emplace_back(ID_float, java_float_type());
1463  structured_type.components().emplace_back(ID_char, java_char_type());
1464  structured_type.components().emplace_back(ID_boolean, java_boolean_type());
1465  // TODO: hash_code not implemented for now
1466  structured_type.components().emplace_back("hashcode", java_int_type());
1467  // TODO: date_time type not implemented for now
1468  structured_type.components().emplace_back("date_time", java_int_type());
1469 
1470  // We will process arguments so that each is converted to a `struct_exprt`
1471  // containing each possible type used in format specifiers.
1472  std::vector<exprt> processed_args;
1473  processed_args.push_back(args[0]);
1474  for(std::size_t i=0; i<MAX_FORMAT_ARGS; ++i)
1475  processed_args.push_back(
1477  args[1], i, structured_type, loc, function_id, symbol_table, code));
1478 
1480  ID_cprover_string_format_func, processed_args, loc, symbol_table, code);
1481  exprt java_string = allocate_fresh_string(
1482  type.return_type(), loc, function_id, symbol_table, code);
1483  code.add(
1485  java_string, string_expr, symbol_table, true),
1486  loc);
1487  code.add(code_returnt(java_string), loc);
1488  return code;
1489 }
1490 
1505  const java_method_typet &type,
1506  const source_locationt &loc,
1507  const irep_idt &function_id,
1508  symbol_table_baset &symbol_table)
1509 {
1511  const symbol_exprt this_obj(params[0].get_identifier(), params[0].type());
1512 
1513  // Code to be returned
1514  code_blockt code;
1515 
1516  // > Class class1;
1517  pointer_typet class_type=
1519  symbol_table.lookup_ref("java::java.lang.Class").type);
1520  symbolt class1_sym=get_fresh_aux_symbol(
1521  class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
1522  symbol_exprt class1=class1_sym.symbol_expr();
1523  code.add(code_declt(class1), loc);
1524 
1525  // class_identifier is this->@class_identifier
1526  member_exprt class_identifier(
1527  checked_dereference(this_obj, this_obj.type().subtype()),
1528  "@class_identifier",
1529  string_typet());
1530 
1531  // string_expr = cprover_string_literal(this->@class_identifier)
1533  ID_cprover_string_literal_func,
1534  {class_identifier},
1535  loc,
1536  symbol_table,
1537  code);
1538 
1539  // string_expr1 = substr(string_expr, 6)
1540  // We do this to remove the "java::" prefix
1542  ID_cprover_string_substring_func,
1543  {string_expr, from_integer(6, java_int_type())},
1544  loc,
1545  symbol_table,
1546  code);
1547 
1548  // string1 = (String*) string_expr
1549  pointer_typet string_ptr_type=java_reference_type(
1550  symbol_table.lookup_ref("java::java.lang.String").type);
1551  exprt string1 = allocate_fresh_string(
1552  string_ptr_type, loc, function_id, symbol_table, code);
1553  code.add(
1555  string1, string_expr1, symbol_table, true),
1556  loc);
1557 
1558  // > class1 = Class.forName(string1)
1559  code_function_callt fun_call(
1560  class1,
1561  symbol_exprt(
1562  "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
1563  {string1});
1564  const java_method_typet fun_type(
1565  {java_method_typet::parametert(string_ptr_type)}, class_type);
1566  fun_call.function().type()=fun_type;
1567  code.add(fun_call, loc);
1568 
1569  // > return class1;
1570  code.add(code_returnt(class1), loc);
1571  return code;
1572 }
1573 
1585  const irep_idt &function_name,
1586  const java_method_typet &type,
1587  const source_locationt &loc,
1588  symbol_table_baset &symbol_table)
1589 {
1590  code_blockt code;
1592  type.parameters(), loc, symbol_table, code);
1593  code.add(
1595  function_name, args, type.return_type(), symbol_table),
1596  loc);
1597  return code;
1598 }
1599 
1615  const irep_idt &function_name,
1616  const java_method_typet &type,
1617  const source_locationt &loc,
1618  symbol_table_baset &symbol_table)
1619 {
1620  // Code for the output
1621  code_blockt code;
1622 
1623  // Calling the function
1625  type.parameters(), loc, symbol_table, code);
1626 
1627  // String expression that will hold the result
1628  refined_string_exprt string_expr =
1629  string_expr_of_function(function_name, arguments, loc, symbol_table, code);
1630 
1631  // Assign to string
1633  type.return_type(), loc, function_name, symbol_table, code);
1634  code.add(
1636  str, string_expr, symbol_table, true),
1637  loc);
1638 
1639  // Return value
1640  code.add(code_returnt(str), loc);
1641  return code;
1642 }
1643 
1659  const java_method_typet &type,
1660  const source_locationt &loc,
1661  const irep_idt &function_id,
1662  symbol_table_baset &symbol_table)
1663 {
1664  // Code for the output
1665  code_blockt code;
1666 
1667  // String expression that will hold the result
1668  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
1669 
1670  // Assign the argument to string_expr
1672  symbol_exprt arg0(op.get_identifier(), op.type());
1674  string_expr, arg0, loc, symbol_table, code);
1675 
1676  // Allocate and assign the string
1678  type.return_type(), loc, function_id, symbol_table, code);
1679  code.add(
1681  str, string_expr, symbol_table, true),
1682  loc);
1683 
1684  // Return value
1685  code.add(code_returnt(str), loc);
1686  return code;
1687 }
1688 
1702  const java_method_typet &type,
1703  const source_locationt &loc,
1704  const irep_idt &function_id,
1705  symbol_table_baset &symbol_table)
1706 {
1707  (void)function_id;
1708 
1709  // Code for the output
1710  code_blockt code;
1711 
1712  // String expression that will hold the result
1713  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
1714 
1715  // Assign argument to a string_expr
1717  symbol_exprt arg1(params[1].get_identifier(), params[1].type());
1719  string_expr, arg1, loc, symbol_table, code);
1720 
1721  // Assign string_expr to `this` object
1722  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1723  code.add(
1725  arg_this, string_expr, symbol_table, true),
1726  loc);
1727 
1728  return code;
1729 }
1730 
1743  const java_method_typet &type,
1744  const source_locationt &loc,
1745  const irep_idt &function_id,
1746  symbol_table_baset &symbol_table)
1747 {
1748  (void)function_id;
1749 
1751  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1752  dereference_exprt deref =
1753  checked_dereference(arg_this, arg_this.type().subtype());
1754 
1755  code_returnt ret(get_length(deref, symbol_table));
1756  ret.add_source_location() = loc;
1757 
1758  return ret;
1759 }
1760 
1762  const irep_idt &function_id) const
1763 {
1764  for(const id_mapt *map : id_maps)
1765  if(map->count(function_id) != 0)
1766  return true;
1767 
1768  return conversion_table.count(function_id) != 0;
1769 }
1770 
1771 template <typename TMap, typename TContainer>
1772 void add_keys_to_container(const TMap &map, TContainer &container)
1773 {
1774  static_assert(
1775  std::is_same<typename TMap::key_type,
1776  typename TContainer::value_type>::value,
1777  "TContainer value_type doesn't match TMap key_type");
1778  std::transform(
1779  map.begin(),
1780  map.end(),
1781  std::inserter(container, container.begin()),
1782  [](const typename TMap::value_type &pair) { return pair.first; });
1783 }
1784 
1786  std::unordered_set<irep_idt> &methods) const
1787 {
1788  for(const id_mapt *map : id_maps)
1789  add_keys_to_container(*map, methods);
1790 
1792 }
1793 
1801  const symbolt &symbol,
1802  symbol_table_baset &symbol_table)
1803 {
1804  const irep_idt &function_id = symbol.name;
1805  const java_method_typet &type = to_java_method_type(symbol.type);
1806  const source_locationt &loc = symbol.location;
1807  auto it_id=cprover_equivalent_to_java_function.find(function_id);
1808  if(it_id!=cprover_equivalent_to_java_function.end())
1809  return make_function_from_call(it_id->second, type, loc, symbol_table);
1810 
1814  it_id->second, type, loc, symbol_table);
1815 
1816  it_id=cprover_equivalent_to_java_constructor.find(function_id);
1819  it_id->second, type, loc, symbol_table);
1820 
1824  it_id->second, type, loc, symbol_table);
1825 
1826  it_id=cprover_equivalent_to_java_assign_function.find(function_id);
1829  it_id->second, type, loc, symbol_table);
1830 
1831  auto it=conversion_table.find(function_id);
1832  INVARIANT(
1833  it != conversion_table.end(), "Couldn't retrieve code for string method");
1834 
1835  return it->second(type, loc, function_id, symbol_table);
1836 }
1837 
1843  irep_idt class_name)
1844 {
1845  return string_types.find(class_name)!=string_types.end();
1846 }
1847 
1849 {
1850  string_types = std::unordered_set<irep_idt>{"java.lang.String",
1851  "java.lang.StringBuilder",
1852  "java.lang.CharSequence",
1853  "java.lang.StringBuffer"};
1854 }
1855 
1858 {
1860 
1861  // The following list of function is organized by libraries, with
1862  // constructors first and then methods in alphabetic order.
1863  // Methods that are not supported here should ultimately have Java models
1864  // provided for them in the class-path.
1865 
1866  // String library
1867  conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1868  std::bind(
1870  this,
1871  std::placeholders::_1,
1872  std::placeholders::_2,
1873  std::placeholders::_3,
1874  std::placeholders::_4);
1876  ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1878  this,
1879  std::placeholders::_1,
1880  std::placeholders::_2,
1881  std::placeholders::_3,
1882  std::placeholders::_4);
1884  ["java::java.lang.String.<init>:()V"]=
1885  ID_cprover_string_empty_string_func;
1886 
1887  // CProverString.charAt differs from the Java String.charAt in that no
1888  // exception is raised for the out of bounds case.
1890  ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
1891  ID_cprover_string_char_at_func;
1893  ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1894  ID_cprover_string_code_point_at_func;
1896  ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1897  ID_cprover_string_code_point_before_func;
1899  ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1900  ID_cprover_string_code_point_count_func;
1902  ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1903  ID_cprover_string_compare_to_func;
1905  ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1906  ID_cprover_string_concat_func;
1908  ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1909  ID_cprover_string_contains_func;
1911  ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1912  ID_cprover_string_endswith_func;
1914  ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1915  ID_cprover_string_equals_ignore_case_func;
1917  ["java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)"
1918  "Ljava/lang/String;"] =
1919  std::bind(
1921  this,
1922  std::placeholders::_1,
1923  std::placeholders::_2,
1924  std::placeholders::_3,
1925  std::placeholders::_4);
1927  ["java::java.lang.String.hashCode:()I"]=
1928  ID_cprover_string_hash_code_func;
1930  ["java::java.lang.String.indexOf:(I)I"]=
1931  ID_cprover_string_index_of_func;
1933  ["java::java.lang.String.indexOf:(II)I"]=
1934  ID_cprover_string_index_of_func;
1936  ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1937  ID_cprover_string_index_of_func;
1939  ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1940  ID_cprover_string_index_of_func;
1942  ["java::java.lang.String.intern:()Ljava/lang/String;"]=
1943  ID_cprover_string_intern_func;
1945  ["java::java.lang.String.isEmpty:()Z"]=
1946  ID_cprover_string_is_empty_func;
1948  ["java::java.lang.String.lastIndexOf:(I)I"]=
1949  ID_cprover_string_last_index_of_func;
1951  ["java::java.lang.String.lastIndexOf:(II)I"]=
1952  ID_cprover_string_last_index_of_func;
1954  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1955  ID_cprover_string_last_index_of_func;
1957  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1958  ID_cprover_string_last_index_of_func;
1959  conversion_table["java::java.lang.String.length:()I"] = std::bind(
1961  this,
1962  std::placeholders::_1,
1963  std::placeholders::_2,
1964  std::placeholders::_3,
1965  std::placeholders::_4);
1967  ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1968  "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1970  ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1971  ID_cprover_string_replace_func;
1973  ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
1974  ID_cprover_string_replace_func;
1976  ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1977  ID_cprover_string_startswith_func;
1979  ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1980  ID_cprover_string_startswith_func;
1982  ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1983  "lang/CharSequence;"] = ID_cprover_string_substring_func;
1984  // CProverString.substring differs from the Java String.substring in that no
1985  // exception is raised for the out of bounds case.
1987  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1988  "Ljava/lang/String;"]=
1989  ID_cprover_string_substring_func;
1991  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1992  "Ljava/lang/String;"]=
1993  ID_cprover_string_substring_func;
1995  ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1996  ID_cprover_string_to_lower_case_func;
1997  conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
1998  std::bind(
2000  this,
2001  std::placeholders::_1,
2002  std::placeholders::_2,
2003  std::placeholders::_3,
2004  std::placeholders::_4);
2006  ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
2007  ID_cprover_string_to_upper_case_func;
2009  ["java::java.lang.String.trim:()Ljava/lang/String;"]=
2010  ID_cprover_string_trim_func;
2012  ["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
2013  ID_cprover_string_of_bool_func;
2015  ["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
2016  ID_cprover_string_of_char_func;
2017  conversion_table["java::java.lang.String.valueOf:(D)Ljava/lang/String;"] =
2018  std::bind(
2020  this,
2021  std::placeholders::_1,
2022  std::placeholders::_2,
2023  std::placeholders::_3,
2024  std::placeholders::_4);
2025  conversion_table["java::java.lang.String.valueOf:(F)Ljava/lang/String;"] =
2026  std::bind(
2028  this,
2029  std::placeholders::_1,
2030  std::placeholders::_2,
2031  std::placeholders::_3,
2032  std::placeholders::_4);
2034  ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
2035  ID_cprover_string_of_int_func;
2037  ["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
2038  ID_cprover_string_of_long_func;
2039 
2040  // StringBuilder library
2042  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
2044  this,
2045  std::placeholders::_1,
2046  std::placeholders::_2,
2047  std::placeholders::_3,
2048  std::placeholders::_4);
2050  ["java::java.lang.StringBuilder.<init>:()V"]=
2051  ID_cprover_string_empty_string_func;
2052 
2054  ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
2055  ID_cprover_string_concat_char_func;
2057  ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
2058  ID_cprover_string_concat_double_func;
2060  ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
2061  "lang/CharSequence;II)"
2062  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2064  ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
2065  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2067  ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
2068  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2070  ["java::java.lang.StringBuilder.appendCodePoint:(I)"
2071  "Ljava/lang/StringBuilder;"]=
2072  ID_cprover_string_concat_code_point_func;
2074  ["java::java.lang.StringBuilder.charAt:(I)C"]=
2075  ID_cprover_string_char_at_func;
2077  ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
2078  ID_cprover_string_code_point_at_func;
2080  ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
2081  ID_cprover_string_code_point_before_func;
2083  ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
2084  ID_cprover_string_code_point_count_func;
2086  ["java::org.cprover.CProverString.delete:(Ljava/lang/"
2087  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2088  ID_cprover_string_delete_func;
2090  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
2091  "StringBuilder;I)Ljava/lang/StringBuilder;"] =
2092  ID_cprover_string_delete_char_at_func;
2094  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2095  "StringBuilder;IC)Ljava/lang/StringBuilder;"] =
2096  ID_cprover_string_insert_char_func;
2098  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2099  "StringBuilder;IZ)Ljava/lang/StringBuilder;"] =
2100  ID_cprover_string_insert_bool_func;
2102  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2103  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2104  ID_cprover_string_insert_int_func;
2106  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2107  "StringBuilder;IJ)Ljava/lang/StringBuilder;"] =
2108  ID_cprover_string_insert_long_func;
2110  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
2111  "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
2112  conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
2114  this,
2115  std::placeholders::_1,
2116  std::placeholders::_2,
2117  std::placeholders::_3,
2118  std::placeholders::_4);
2120  ["java::java.lang.StringBuilder.setCharAt:(IC)V"]=
2121  ID_cprover_string_char_set_func;
2123  ["java::java.lang.StringBuilder.setLength:(I)V"]=
2124  ID_cprover_string_set_length_func;
2126  ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
2127  ID_cprover_string_substring_func;
2129  ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
2130  ID_cprover_string_substring_func;
2132  ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
2134  this,
2135  std::placeholders::_1,
2136  std::placeholders::_2,
2137  std::placeholders::_3,
2138  std::placeholders::_4);
2139 
2140  // StringBuffer library
2142  ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
2144  this,
2145  std::placeholders::_1,
2146  std::placeholders::_2,
2147  std::placeholders::_3,
2148  std::placeholders::_4);
2150  ["java::java.lang.StringBuffer.<init>:()V"]=
2151  ID_cprover_string_empty_string_func;
2152 
2154  ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
2155  ID_cprover_string_concat_char_func;
2157  ["java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]=
2158  ID_cprover_string_concat_double_func;
2160  ["java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]=
2161  ID_cprover_string_concat_float_func;
2163  ["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]=
2164  ID_cprover_string_concat_int_func;
2166  ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
2167  ID_cprover_string_concat_long_func;
2169  ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
2170  "Ljava/lang/StringBuffer;"]=
2171  ID_cprover_string_concat_func;
2173  ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
2174  "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
2176  ["java::java.lang.StringBuffer.appendCodePoint:(I)"
2177  "Ljava/lang/StringBuffer;"]=
2178  ID_cprover_string_concat_code_point_func;
2180  ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
2181  ID_cprover_string_char_at_func;
2183  ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
2184  ID_cprover_string_code_point_at_func;
2186  ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
2187  ID_cprover_string_code_point_before_func;
2189  ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
2190  ID_cprover_string_code_point_count_func;
2192  ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
2193  "lang/StringBuffer;"] = ID_cprover_string_delete_func;
2195  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
2196  "StringBufferI)Ljava/lang/StringBuffer;"] =
2197  ID_cprover_string_delete_char_at_func;
2199  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/"
2200  "lang/StringBuffer;"] = ID_cprover_string_insert_char_func;
2202  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/"
2203  "lang/StringBuffer;"] = ID_cprover_string_insert_int_func;
2205  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/"
2206  "lang/StringBuffer;"] = ID_cprover_string_insert_long_func;
2208  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/"
2209  "lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func;
2211  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/"
2212  "lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
2214  ["java::java.lang.StringBuffer.length:()I"]=
2215  conversion_table["java::java.lang.String.length:()I"];
2217  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
2218  ID_cprover_string_char_set_func;
2220  ["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
2221  ID_cprover_string_set_length_func;
2223  ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
2224  ID_cprover_string_substring_func;
2226  ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
2227  "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
2229  ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
2231  this,
2232  std::placeholders::_1,
2233  std::placeholders::_2,
2234  std::placeholders::_3,
2235  std::placeholders::_4);
2236 
2237  // CharSequence library
2239  ["java::java.lang.CharSequence.charAt:(I)C"]=
2240  ID_cprover_string_char_at_func;
2242  ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
2244  this,
2245  std::placeholders::_1,
2246  std::placeholders::_2,
2247  std::placeholders::_3,
2248  std::placeholders::_4);
2250  ["java::java.lang.CharSequence.length:()I"]=
2251  conversion_table["java::java.lang.String.length:()I"];
2252 
2253  // Other libraries
2254  conversion_table["java::java.lang.Float.toString:(F)Ljava/lang/String;"] =
2255  std::bind(
2257  this,
2258  std::placeholders::_1,
2259  std::placeholders::_2,
2260  std::placeholders::_3,
2261  std::placeholders::_4);
2263  ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
2264  ID_cprover_string_parse_int_func;
2266  ["java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
2267  ID_cprover_string_parse_int_func;
2269  ["java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
2270  ID_cprover_string_parse_int_func;
2272  ["java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
2273  ID_cprover_string_parse_int_func;
2275  ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
2276  ID_cprover_string_of_int_hex_func;
2278  ["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
2279  ID_cprover_string_of_int_func;
2281  ["java::java.lang.Integer.toString:(II)Ljava/lang/String;"]=
2282  ID_cprover_string_of_int_func;
2284  ["java::java.lang.Long.toString:(J)Ljava/lang/String;"]=
2285  ID_cprover_string_of_int_func;
2287  ["java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
2288  ID_cprover_string_of_int_func;
2289  conversion_table["java::java.lang.Object.getClass:()Ljava/lang/Class;"] =
2290  std::bind(
2292  this,
2293  std::placeholders::_1,
2294  std::placeholders::_2,
2295  std::placeholders::_3,
2296  std::placeholders::_4);
2297 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:479
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:1658
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:1742
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:119
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
dstringt::c_str
const char * c_str() const
Definition: dstring.h:86
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
code_assign_function_application
static codet code_assign_function_application(const exprt &lhs, const irep_idt &function_name, const exprt::operandst &arguments, symbol_table_baset &symbol_table)
assign the result of a function call
Definition: java_string_library_preprocess.cpp:591
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:96
typet::subtype
const typet & subtype() const
Definition: type.h:38
java_root_class.h
add_character_set_constraint
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_set, symbol_table_baset &symbol_table, const source_locationt &loc, 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:741
arith_tools.h
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
java_double_type
typet java_double_type()
Definition: java_types.cpp:67
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
java_string_library_preprocesst::index_type
const typet index_type
Definition: java_string_library_preprocess.h:98
java_int_type
typet java_int_type()
Definition: java_types.cpp:32
java_string_library_preprocesst::fresh_array
symbol_exprt fresh_array(const typet &type, const source_locationt &loc, symbol_tablet &symbol_table)
add a symbol in the table with static lifetime and name containing cprover_string_array and given typ...
Definition: java_string_library_preprocess.cpp:248
to_string_expr
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:161
typet
The type of an expression, extends irept.
Definition: type.h:27
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
fresh_symbol.h
checked_dereference
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:174
java_boolean_type
typet java_boolean_type()
Definition: java_types.cpp:72
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Definition: fresh_symbol.cpp:30
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:3355
data
Definition: kdev_t.h:24
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
struct_typet::add_base
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:87
java_long_type
typet java_long_type()
Definition: java_types.cpp:42
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
and_exprt
Boolean AND.
Definition: std_expr.h:2409
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
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1044
java_string_library_preprocesst::make_function_from_call
code_blockt make_function_from_call(const irep_idt &function_name, 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:1584
java_string_library_preprocesst::cprover_equivalent_to_java_constructor
id_mapt cprover_equivalent_to_java_constructor
Definition: java_string_library_preprocess.h:123
java_string_library_preprocesst::make_string_returning_function_from_call
code_blockt make_string_returning_function_from_call(const irep_idt &function_name, 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:1614
make_allocate_code
static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating object of size size and assigning it to lhs
Definition: java_string_library_preprocess.cpp:626
struct_union_typet::component_type
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:66
exprt
Base class for all expressions.
Definition: expr.h:54
java_string_library_preprocesst::implements_function
bool implements_function(const irep_idt &function_id) const
Definition: java_string_library_preprocess.cpp:1761
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:517
java_string_library_preprocesst::make_assign_and_return_function_from_call
code_blockt make_assign_and_return_function_from_call(const irep_idt &function_name, 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:1138
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1848
irep_idt
dstringt irep_idt
Definition: irep.h:32
messaget::eom
static eomt eom
Definition: message.h:284
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:136
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:640
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
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:892
equal_exprt
Equality.
Definition: std_expr.h:1484
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:81
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:172
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:614
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4625
java_string_library_preprocesst::make_argument_for_format
struct_exprt make_argument_for_format(const exprt &argv, std::size_t index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
Helper for format function.
Definition: java_string_library_preprocess.cpp:1338
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:182
refined_string_exprt
Definition: string_expr.h:114
refined_string_exprt::length
const exprt & length() const
Definition: string_expr.h:139
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
ieee_float_spect
Definition: ieee_float.h:25
java_class_typet
Definition: java_types.h:101
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:938
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1920
array_typet::size
const exprt & size() const
Definition: std_types.h:1010
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:208
java_string_library_preprocesst::make_object_get_class_code
code_blockt make_object_get_class_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 java.lang.Object.getClass() function.
Definition: java_string_library_preprocess.cpp:1504
make_function_application
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
Create a function application expression.
Definition: java_utils.cpp:275
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
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::process_parameters
exprt::operandst process_parameters(const java_method_typet::parameterst &params, const source_locationt &loc, 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:271
java_object_factory.h
empty_typet
The empty type.
Definition: std_types.h:48
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, 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:706
java_string_library_preprocesst::process_equals_function_operands
exprt::operandst process_equals_function_operands(const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
Converts the operands of the equals function to string expressions and outputs these conversions.
Definition: java_string_library_preprocess.cpp:356
java_string_library_preprocesst::conversion_table
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Definition: java_string_library_preprocess.h:111
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, code_blockt &init_code)
Creates a string_exprt from the input exprt representing a char sequence.
Definition: java_string_library_preprocess.cpp:301
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4471
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:132
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition: std_types.h:227
java_string_library_preprocesst::decl_string_expr
refined_string_exprt decl_string_expr(const source_locationt &loc, 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:499
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, 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:672
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:1701
java_string_library_preprocesst::string_expr_of_function
refined_string_exprt string_expr_of_function(const irep_idt &function_name, 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:780
java_byte_type
typet java_byte_type()
Definition: java_types.cpp:52
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:496
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:1785
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:150
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:534
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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:1800
java_string_library_preprocesst::get_primitive_value_of_object
optionalt< symbol_exprt > get_primitive_value_of_object(const exprt &object, irep_idt type_name, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Adds to the code an assignment of the form.
Definition: java_string_library_preprocess.cpp:1195
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:469
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:127
java_string_library_preprocesst::process_operands
exprt::operandst process_operands(const exprt::operandst &operands, const source_locationt &loc, 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:326
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:543
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
code_blockt::add
void add(const codet &code)
Definition: std_code.h:189
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
java_string_library_preprocesst::code_return_function_application
codet code_return_function_application(const irep_idt &function_name, 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:611
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
java_string_library_preprocesst::fresh_string
symbol_exprt fresh_string(const typet &type, const source_locationt &loc, 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:482
java_string_library_preprocesst::make_init_function_from_call
code_blockt make_init_function_from_call(const irep_idt &function_name, 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:1096
std_code.h
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:405
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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:51
java_string_library_preprocesst::character_preprocess
character_refine_preprocesst character_preprocess
Definition: java_string_library_preprocess.h:95
java_string_library_preprocesst::make_string_format_code
code_blockt make_string_format_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide code for the Java String.format function.
Definition: java_string_library_preprocess.cpp:1444
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:63
java_short_type
typet java_short_type()
Definition: java_types.cpp:47
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:1633
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:159
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:3080
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
struct_union_typet::componentt
Definition: std_types.h:121
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:955
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:104
refined_string_exprt::content
const exprt & content() const
Definition: string_expr.h:149
java_class_typet::set_access
void set_access(const irep_idt &access)
Definition: java_types.h:109
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
array_typet
Arrays with given size.
Definition: std_types.h:1000
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
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:828
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:113
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:4035
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:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
symbolt::is_type
bool is_type
Definition: symbol.h:61
string_typet
String type.
Definition: std_types.h:1662
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
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:1842
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:828
code_typet::parametert
Definition: std_types.h:788
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:130
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:240
allocate_dynamic_object_with_decl
exprt allocate_dynamic_object_with_decl(const exprt &target_expr, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code)
Generates code for allocating a dynamic object.
Definition: java_object_factory.cpp:251
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
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:570
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
java_char_type
typet java_char_type()
Definition: java_types.cpp:57
loc
#define loc()
Definition: ansi_c_lex.yy.cpp:4256
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:1857
java_string_library_preprocesst::get_object_at_index
dereference_exprt get_object_at_index(const exprt &argv, std::size_t index)
Helper for format function.
Definition: java_string_library_preprocess.cpp:1293
java_string_library_preprocesst::make_assign_function_from_call
code_blockt make_assign_function_from_call(const irep_idt &function_name, 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:1163
index_exprt
Array index operator.
Definition: std_expr.h:1595
get_length
static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
access length member
Definition: java_string_library_preprocess.cpp:424
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
java_types.h
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
is_constructor
static bool is_constructor(const irep_idt &method_name)
Definition: java_bytecode_convert_method.cpp:126
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
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:59
java_utils.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
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:873
messaget::warning
mstreamt & warning() const
Definition: message.h:391
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
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
java_method_typet
Definition: java_types.h:264
get_data
static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
access data member
Definition: java_string_library_preprocess.cpp:434
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:1772
java_string_library_preprocesst::is_java_string_type
static bool is_java_string_type(const typet &type)
Definition: java_string_library_preprocess.cpp:73
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1560
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:90
validation_modet::INVARIANT
java_string_library_preprocesst::replace_char_array
refined_string_exprt replace_char_array(const exprt &array_pointer, const source_locationt &loc, 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:446
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3989
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:385
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:1390
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
not_exprt
Boolean negation.
Definition: std_expr.h:3308
java_float_type
typet java_float_type()
Definition: java_types.cpp:62
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:36
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470