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 irep_idt get_tag(const typet &type)
37 {
39  if(type.id() == ID_symbol)
40  return to_symbol_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 
174 {
175  symbolt sym=*symbol_table.lookup("java::java.lang.String");
176  typet concrete_type=sym.type;
177  struct_typet struct_type=to_struct_type(concrete_type);
178  std::size_t index=struct_type.component_number("data");
179  typet data_type=struct_type.components()[index].type();
180  return data_type;
181 }
182 
185 {
186  return java_int_type();
187 }
188 
193 std::vector<irep_idt>
195  const irep_idt &class_name)
196 {
197  if(!is_known_string_type(class_name))
198  return {};
199 
200  std::vector<irep_idt> bases;
201  bases.reserve(3);
202  if(class_name != "java.lang.CharSequence")
203  {
204  bases.push_back("java.io.Serializable");
205  bases.push_back("java.lang.CharSequence");
206  }
207  if(class_name == "java.lang.String")
208  bases.push_back("java.lang.Comparable");
209 
210  if(class_name == "java.lang.StringBuilder" ||
211  class_name == "java.lang.StringBuffer")
212  bases.push_back("java.lang.AbstractStringBuilder");
213 
214  return bases;
215 }
216 
221  const irep_idt &class_name, symbol_tablet &symbol_table)
222 {
223  java_class_typet string_type;
224  string_type.set_tag(class_name);
225  string_type.set_name("java::" + id2string(class_name));
226  string_type.components().resize(3);
227  string_type.components()[0].set_name("@java.lang.Object");
228  string_type.components()[0].set_pretty_name("@java.lang.Object");
229  string_type.components()[0].type()=symbol_typet("java::java.lang.Object");
230  string_type.components()[1].set_name("length");
231  string_type.components()[1].set_pretty_name("length");
232  string_type.components()[1].type()=string_length_type();
233  string_type.components()[2].set_name("data");
234  string_type.components()[2].set_pretty_name("data");
235  string_type.components()[2].type() = pointer_type(java_char_type());
236  string_type.set_access(ID_public);
237  string_type.add_base(symbol_typet("java::java.lang.Object"));
238 
239  std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
240  for(const irep_idt &base_name : bases)
241  string_type.add_base(symbol_typet("java::" + id2string(base_name)));
242 
243  symbolt tmp_string_symbol;
244  tmp_string_symbol.name="java::"+id2string(class_name);
245  symbolt *string_symbol=nullptr;
246  symbol_table.move(tmp_string_symbol, string_symbol);
247  string_symbol->base_name=id2string(class_name);
248  string_symbol->pretty_name=id2string(class_name);
249  string_symbol->type=string_type;
250  string_symbol->is_type=true;
251  string_symbol->mode = ID_java;
252 }
253 
260  const typet &type,
261  const source_locationt &location,
262  symbol_tablet &symbol_table)
263 {
264  symbolt array_symbol=get_fresh_aux_symbol(
265  type,
266  "cprover_string_array",
267  "cprover_string_array",
268  location,
269  ID_java,
270  symbol_table);
271  array_symbol.is_static_lifetime=true;
272  return array_symbol.symbol_expr();
273 }
274 
283  const java_method_typet::parameterst &params,
284  const source_locationt &loc,
285  symbol_table_baset &symbol_table,
286  code_blockt &init_code)
287 {
288  exprt::operandst ops;
289  for(const auto &p : params)
290  {
291  symbol_exprt sym(p.get_identifier(), p.type());
292  ops.push_back(sym);
293  }
294  return process_operands(ops, loc, symbol_table, init_code);
295 }
296 
313  const exprt &expr_to_process,
314  const source_locationt &loc,
315  symbol_table_baset &symbol_table,
316  code_blockt &init_code)
317 {
319  const refined_string_exprt string_expr =
320  decl_string_expr(loc, symbol_table, init_code);
322  string_expr, expr_to_process, loc, symbol_table, init_code);
323  return string_expr;
324 }
325 
338  const exprt::operandst &operands,
339  const source_locationt &loc,
340  symbol_table_baset &symbol_table,
341  code_blockt &init_code)
342 {
343  exprt::operandst ops;
344  for(const auto &p : operands)
345  {
347  ops.push_back(
348  convert_exprt_to_string_exprt(p, loc, symbol_table, init_code));
349  else if(is_java_char_array_pointer_type(p.type()))
350  ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
351  else
352  ops.push_back(p);
353  }
354  return ops;
355 }
356 
368  const exprt::operandst &operands,
369  const source_locationt &loc,
370  symbol_table_baset &symbol_table,
371  code_blockt &init_code)
372 {
373  PRECONDITION(operands.size()==2);
374  exprt::operandst ops;
375  const exprt &op0=operands[0];
376  const exprt &op1 = operands[1];
378 
379  ops.push_back(
380  convert_exprt_to_string_exprt(op0, loc, symbol_table, init_code));
381 
382  // TODO: Manage the case where we have a non-String Object (this should
383  // probably be handled upstream. At any rate, the following code should be
384  // protected with assertions on the type of op1.
385  typecast_exprt tcast(op1, to_pointer_type(op0.type()));
386  ops.push_back(
387  convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code));
388  return ops;
389 }
390 
395 static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
396 {
397  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
398  if(type.id()==ID_symbol)
399  {
400  symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
401  CHECK_RETURN(sym.type.id()!=ID_symbol);
402  return get_data_type(sym.type, symbol_table);
403  }
404  // else type id is ID_struct
405  const struct_typet &struct_type=to_struct_type(type);
406  return struct_type.component_type("data");
407 }
408 
413 static typet
414 get_length_type(const typet &type, const symbol_tablet &symbol_table)
415 {
416  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
417  if(type.id()==ID_symbol)
418  {
419  symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
420  CHECK_RETURN(sym.type.id()!=ID_symbol);
421  return get_length_type(sym.type, symbol_table);
422  }
423  // else type id is ID_struct
424  const struct_typet &struct_type=to_struct_type(type);
425  return struct_type.component_type("length");
426 }
427 
432 static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
433 {
434  return member_exprt(
435  expr, "length", get_length_type(expr.type(), symbol_table));
436 }
437 
442 static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
443 {
444  return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
445 }
446 
455  const exprt &array_pointer,
456  const source_locationt &loc,
457  symbol_table_baset &symbol_table,
458  code_blockt &code)
459 {
460  // array is *array_pointer
461  dereference_exprt array=
462  checked_dereference(array_pointer, array_pointer.type().subtype());
463  // array_data is array_pointer-> data
464  const exprt array_data = get_data(array, symbol_table);
465  symbolt sym_char_array = get_fresh_aux_symbol(
466  array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
467  symbol_exprt char_array=sym_char_array.symbol_expr();
468  // char_array = array_pointer->data
469  code.add(code_assignt(char_array, array_data), loc);
470 
471  // string_expr is `{ rhs->length; string_array }`
472  refined_string_exprt string_expr(
473  get_length(array, symbol_table), char_array, refined_string_type);
474 
475  dereference_exprt inf_array(
477 
479  string_expr.content(), inf_array, symbol_table, loc, code);
480 
481  return string_expr;
482 }
483 
491  const typet &type,
492  const source_locationt &loc,
493  symbol_table_baset &symbol_table)
494 {
495  symbolt string_symbol=get_fresh_aux_symbol(
496  type, "cprover_string", "cprover_string", loc, ID_java, symbol_table);
497  string_symbol.is_static_lifetime=true;
498  return string_symbol.symbol_expr();
499 }
500 
508  const source_locationt &loc,
509  symbol_table_baset &symbol_table,
510  code_blockt &code)
511 {
512  symbolt sym_length = get_fresh_aux_symbol(
513  index_type,
514  "cprover_string_length",
515  "cprover_string_length",
516  loc,
517  ID_java,
518  symbol_table);
519  symbol_exprt length_field=sym_length.symbol_expr();
520  pointer_typet array_type = pointer_type(java_char_type());
521  symbolt sym_content = get_fresh_aux_symbol(
522  array_type,
523  "cprover_string_content",
524  "cprover_string_content",
525  loc,
526  ID_java,
527  symbol_table);
528  symbol_exprt content_field = sym_content.symbol_expr();
529  code.add(code_declt(content_field), loc);
530  refined_string_exprt str(length_field, content_field, refined_string_type);
531  code.add(code_declt(length_field), loc);
532  return str;
533 }
534 
543  const source_locationt &loc,
544  const irep_idt &function_id,
545  symbol_table_baset &symbol_table,
546  code_blockt &code)
547 {
549  const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
550 
551  const side_effect_expr_nondett nondet_length(str.length().type(), loc);
552  code.add(code_assignt(str.length(), nondet_length), loc);
553 
554  exprt nondet_array_expr =
555  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
556 
557  address_of_exprt array_pointer(
558  index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
559 
561  array_pointer, nondet_array_expr, symbol_table, loc, code);
562 
564  nondet_array_expr, str.length(), symbol_table, loc, code);
565 
566  code.add(code_assignt(str.content(), array_pointer), loc);
567 
568  return refined_string_exprt(str.length(), str.content());
569 }
570 
578  const typet &type,
579  const source_locationt &loc,
580  const irep_idt &function_id,
581  symbol_table_baset &symbol_table,
582  code_blockt &code)
583 {
584  exprt str=fresh_string(type, loc, symbol_table);
585  allocate_dynamic_object_with_decl(str, symbol_table, loc, function_id, code);
586  return str;
587 }
588 
596  const typet &type,
597  const source_locationt &loc,
598  const irep_idt &function_id,
599  symbol_tablet &symbol_table,
600  code_blockt &code)
601 {
602  exprt array=fresh_array(type, loc, symbol_table);
603  code.add(code_declt(array), loc);
605  array, symbol_table, loc, function_id, code);
606  return array;
607 }
608 
619  const exprt &lhs,
620  const irep_idt &function_name,
621  const exprt::operandst &arguments,
622  symbol_table_baset &symbol_table)
623 {
625  function_name, arguments, lhs.type(), symbol_table);
626  return code_assignt(lhs, fun_app);
627 }
628 
639  const irep_idt &function_name,
640  const exprt::operandst &arguments,
641  const typet &type,
642  symbol_table_baset &symbol_table)
643 {
645  function_name, arguments, type, symbol_table);
646  return code_returnt(fun_app);
647 }
648 
656  symbol_table_baset &symbol_table,
657  const source_locationt &loc,
658  const irep_idt &function_id,
659  code_blockt &code)
660 {
661  const array_typet array_type(
663  const symbolt data_sym = get_fresh_aux_symbol(
664  array_type,
665  id2string(function_id),
666  "nondet_infinite_array",
667  loc,
668  ID_java,
669  symbol_table);
670  const symbol_exprt data_expr = data_sym.symbol_expr();
671  code.add(code_declt(data_expr), loc);
672  const side_effect_expr_nondett nondet_data(data_expr.type(), loc);
673  code.add(code_assignt(data_expr, nondet_data), loc);
674  return data_expr;
675 }
676 
685  const exprt &pointer,
686  const exprt &array,
687  symbol_table_baset &symbol_table,
688  const source_locationt &loc,
689  code_blockt &code)
690 {
691  PRECONDITION(array.type().id() == ID_array);
692  PRECONDITION(pointer.type().id() == ID_pointer);
693  symbolt &return_sym = get_fresh_aux_symbol(
694  java_int_type(),
695  "return_array",
696  "return_array",
697  loc,
698  ID_java,
699  symbol_table);
700  exprt return_expr = return_sym.symbol_expr();
701  code.add(code_declt(return_expr), loc);
702  code.add(
704  return_expr,
705  ID_cprover_associate_array_to_pointer_func,
706  {array, pointer},
707  symbol_table),
708  loc);
709 }
710 
719  const exprt &array,
720  const exprt &length,
721  symbol_table_baset &symbol_table,
722  const source_locationt &loc,
723  code_blockt &code)
724 {
725  symbolt &return_sym = get_fresh_aux_symbol(
726  java_int_type(),
727  "return_array",
728  "return_array",
729  loc,
730  ID_java,
731  symbol_table);
732  const exprt return_expr = return_sym.symbol_expr();
733  code.add(code_declt(return_expr), loc);
734  code.add(
736  return_expr,
737  ID_cprover_associate_length_to_array_func,
738  {array, length},
739  symbol_table),
740  loc);
741 }
742 
754  const exprt &pointer,
755  const exprt &length,
756  const irep_idt &char_set,
757  symbol_table_baset &symbol_table,
758  const source_locationt &loc,
759  code_blockt &code)
760 {
761  PRECONDITION(pointer.type().id() == ID_pointer);
762  symbolt &return_sym = get_fresh_aux_symbol(
763  java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
764  const exprt return_expr = return_sym.symbol_expr();
765  code.add(code_declt(return_expr), loc);
766  const constant_exprt char_set_expr(char_set, string_typet());
767  code.add(
769  return_expr,
770  ID_cprover_string_constrain_characters_func,
771  {length, pointer, char_set_expr},
772  symbol_table),
773  loc);
774 }
775 
793  const irep_idt &function_name,
794  const exprt::operandst &arguments,
795  const source_locationt &loc,
796  symbol_table_baset &symbol_table,
797  code_blockt &code)
798 {
799  // int return_code;
800  symbolt return_code_sym = get_fresh_aux_symbol(
801  java_int_type(),
802  std::string("return_code_") + function_name.c_str(),
803  std::string("return_code_") + function_name.c_str(),
804  loc,
805  ID_java,
806  symbol_table);
807  const exprt return_code = return_code_sym.symbol_expr();
808  code.add(code_declt(return_code), loc);
809 
810  const refined_string_exprt string_expr =
811  make_nondet_string_expr(loc, function_name, symbol_table, code);
812 
813  // args is { str.length, str.content, arguments... }
814  exprt::operandst args;
815  args.push_back(string_expr.length());
816  args.push_back(string_expr.content());
817  args.insert(args.end(), arguments.begin(), arguments.end());
818 
819  // return_code = <function_name>_data(args)
820  code.add(
822  return_code, function_name, args, symbol_table),
823  loc);
824 
825  return string_expr;
826 }
827 
838  const exprt &lhs,
839  const exprt &rhs_array,
840  const exprt &rhs_length,
841  const symbol_table_baset &symbol_table)
842 {
845 
846  // A String has a field Object with @clsid = String
847  const symbolt &jlo_symbol=*symbol_table.lookup("java::java.lang.Object");
848  const struct_typet &jlo_struct=to_struct_type(jlo_symbol.type);
849  struct_exprt jlo_init(jlo_struct);
850  irep_idt clsid = get_tag(lhs.type().subtype());
851  java_root_class_init(jlo_init, jlo_struct, clsid);
852 
853  struct_exprt struct_rhs(deref.type());
854  struct_rhs.copy_to_operands(jlo_init);
855  struct_rhs.copy_to_operands(rhs_length);
856  struct_rhs.copy_to_operands(rhs_array);
857  return code_assignt(
858  checked_dereference(lhs, lhs.type().subtype()), struct_rhs);
859 }
860 
870  const exprt &lhs,
871  const refined_string_exprt &rhs,
872  const symbol_table_baset &symbol_table)
873 {
875  lhs, rhs.content(), rhs.length(), symbol_table);
876 }
877 
888  const refined_string_exprt &lhs,
889  const exprt &rhs,
890  const source_locationt &loc,
891  const symbol_table_baset &symbol_table,
892  code_blockt &code)
893 {
895 
896  typet deref_type;
897  if(rhs.type().subtype().id()==ID_symbol)
898  deref_type=symbol_table.lookup_ref(
899  to_symbol_type(rhs.type().subtype()).get_identifier()).type;
900  else
901  deref_type=rhs.type().subtype();
902 
903  const dereference_exprt deref = checked_dereference(rhs, deref_type);
904 
905  // Although we should not reach this code if rhs is null, the association
906  // `pointer -> length` is added to the solver anyway, so we have to make sure
907  // the length is set to something reasonable.
908  auto rhs_length = if_exprt(
910  from_integer(0, lhs.length().type()),
911  get_length(deref, symbol_table));
912  rhs_length.set(ID_mode, ID_java);
913 
914  // Assignments
915  code.add(code_assignt(lhs.length(), rhs_length), loc);
916  const exprt data_as_array = get_data(deref, symbol_table);
917  code.add(code_assignt(lhs.content(), data_as_array), loc);
918 }
919 
932  const std::string &s,
933  const source_locationt &loc,
934  symbol_table_baset &symbol_table,
935  code_blockt &code)
936 {
937  const constant_exprt expr(s, string_typet());
939  ID_cprover_string_literal_func, {expr}, loc, symbol_table, code);
940 }
941 
959  const java_method_typet &type,
960  const source_locationt &loc,
961  const irep_idt &function_id,
962  symbol_table_baset &symbol_table)
963 {
964  const typet &return_type = type.return_type();
965  exprt::operandst ops;
966  for(const auto &p : type.parameters())
967  {
968  symbol_exprt sym(p.get_identifier(), p.type());
969  ops.push_back(sym);
970  }
971 
972  code_ifthenelset code;
973  code.cond() = [&] {
974  const member_exprt class_identifier(
975  checked_dereference(ops[1], ops[1].type().subtype()),
976  "@class_identifier",
977  string_typet());
978  return equal_exprt(
979  class_identifier,
980  constant_exprt("java::java.lang.String", string_typet()));
981  }();
982 
983  code.then_case() = [&] {
984  code_blockt instance_case;
985  // Check content equality
986  const symbolt string_equals_sym = get_fresh_aux_symbol(
987  return_type,
988  id2string(function_id),
989  "str_eq",
990  loc,
991  ID_java,
992  symbol_table);
993  const symbol_exprt string_equals = string_equals_sym.symbol_expr();
994  instance_case.add(code_declt(string_equals), loc);
995  const exprt::operandst args =
996  process_equals_function_operands(ops, loc, symbol_table, instance_case);
997  const auto fun_app = make_function_application(
998  ID_cprover_string_equal_func, args, return_type, symbol_table);
999  instance_case.add(code_assignt(string_equals, fun_app), loc);
1000  instance_case.add(code_returnt(string_equals), loc);
1001  return instance_case;
1002  }();
1003 
1004  code.else_case() = code_returnt(from_integer(false, return_type));
1005  return code;
1006 }
1007 
1014  const java_method_typet &type,
1015  const source_locationt &loc,
1016  const irep_idt &function_id,
1017  symbol_table_baset &symbol_table)
1018 {
1019  // Getting the argument
1021  PRECONDITION(params.size()==1);
1022  const symbol_exprt arg(params[0].get_identifier(), params[0].type());
1023 
1024  // Holder for output code
1025  code_blockt code;
1026 
1027  // Declaring and allocating String * str
1029  type.return_type(), loc, function_id, symbol_table, code);
1030 
1031  // Expression representing 0.0
1032  ieee_float_spect float_spec(to_floatbv_type(params[0].type()));
1033  ieee_floatt zero_float(float_spec);
1034  zero_float.from_float(0.0);
1035  constant_exprt zero=zero_float.to_expr();
1036 
1037  // For each possible case with have a condition and a string_exprt
1038  std::vector<exprt> condition_list;
1039  std::vector<refined_string_exprt> string_expr_list;
1040 
1041  // Case of computerized scientific notation
1042  condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
1044  ID_cprover_string_of_float_scientific_notation_func,
1045  {arg},
1046  loc,
1047  symbol_table,
1048  code);
1049  string_expr_list.push_back(sci_notation);
1050 
1051  // Subcase of negative scientific notation
1052  condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
1053  refined_string_exprt minus_sign =
1054  string_literal_to_string_expr("-", loc, symbol_table, code);
1055  refined_string_exprt neg_sci_notation = string_expr_of_function(
1056  ID_cprover_string_concat_func,
1057  {minus_sign, sci_notation},
1058  loc,
1059  symbol_table,
1060  code);
1061  string_expr_list.push_back(neg_sci_notation);
1062 
1063  // Case of NaN
1064  condition_list.push_back(isnan_exprt(arg));
1065  refined_string_exprt nan =
1066  string_literal_to_string_expr("NaN", loc, symbol_table, code);
1067  string_expr_list.push_back(nan);
1068 
1069  // Case of Infinity
1070  extractbit_exprt is_neg(arg, float_spec.width()-1);
1071  condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
1072  refined_string_exprt infinity =
1073  string_literal_to_string_expr("Infinity", loc, symbol_table, code);
1074  string_expr_list.push_back(infinity);
1075 
1076  // Case -Infinity
1077  condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
1078  refined_string_exprt minus_infinity =
1079  string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
1080  string_expr_list.push_back(minus_infinity);
1081 
1082  // Case of simple notation
1083  ieee_floatt bound_inf_float(float_spec);
1084  ieee_floatt bound_sup_float(float_spec);
1085  bound_inf_float.from_float(1e-3f);
1086  bound_sup_float.from_float(1e7f);
1087  bound_inf_float.change_spec(float_spec);
1088  bound_sup_float.change_spec(float_spec);
1089  constant_exprt bound_inf=bound_inf_float.to_expr();
1090  constant_exprt bound_sup=bound_sup_float.to_expr();
1091 
1092  and_exprt is_simple_float(
1093  binary_relation_exprt(arg, ID_ge, bound_inf),
1094  binary_relation_exprt(arg, ID_lt, bound_sup));
1095  condition_list.push_back(is_simple_float);
1096 
1098  ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1099  string_expr_list.push_back(simple_notation);
1100 
1101  // Case of a negative number in simple notation
1102  and_exprt is_neg_simple_float(
1103  binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
1104  binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup)));
1105  condition_list.push_back(is_neg_simple_float);
1106 
1107  refined_string_exprt neg_simple_notation = string_expr_of_function(
1108  ID_cprover_string_concat_func,
1109  {minus_sign, simple_notation},
1110  loc,
1111  symbol_table,
1112  code);
1113  string_expr_list.push_back(neg_simple_notation);
1114 
1115  // Combining all cases
1116  INVARIANT(
1117  string_expr_list.size()==condition_list.size(),
1118  "number of created strings should correspond to number of conditions");
1119 
1120  // We do not check the condition of the first element in the list as it
1121  // will be reached only if all other conditions are not satisfied.
1123  str, string_expr_list[0], symbol_table);
1124  for(std::size_t i=1; i<condition_list.size(); i++)
1125  {
1126  code_ifthenelset ife;
1127  ife.cond()=condition_list[i];
1129  str, string_expr_list[i], symbol_table);
1130  ife.else_case()=tmp_code;
1131  tmp_code=ife;
1132  }
1133  code.add(tmp_code, loc);
1134 
1135  // Return str
1136  code.add(code_returnt(str), loc);
1137  return code;
1138 }
1139 
1157  const irep_idt &function_name,
1158  const java_method_typet &type,
1159  const source_locationt &loc,
1160  symbol_table_baset &symbol_table,
1161  bool ignore_first_arg)
1162 {
1164 
1165  // The first parameter is the object to be initialized
1166  PRECONDITION(!params.empty());
1167  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1168  if(ignore_first_arg)
1169  params.erase(params.begin());
1170 
1171  // Holder for output code
1172  code_blockt code;
1173 
1174  // Processing parameters
1175  exprt::operandst args=process_parameters(params, loc, symbol_table, code);
1176 
1177  // string_expr <- function(arg1)
1178  refined_string_exprt string_expr =
1179  string_expr_of_function(function_name, args, loc, symbol_table, code);
1180 
1181  // arg_this <- string_expr
1182  code.add(
1183  code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1184  loc);
1185 
1186  return code;
1187 }
1188 
1198  const irep_idt &function_name,
1199  const java_method_typet &type,
1200  const source_locationt &loc,
1201  symbol_table_baset &symbol_table)
1202 {
1203  // This is similar to assign functions except we return a pointer to `this`
1205  PRECONDITION(!params.empty());
1206  code_blockt code;
1207  code.add(
1208  make_assign_function_from_call(function_name, type, loc, symbol_table),
1209  loc);
1210  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1211  code.add(code_returnt(arg_this), loc);
1212  return code;
1213 }
1214 
1223  const irep_idt &function_name,
1224  const java_method_typet &type,
1225  const source_locationt &loc,
1226  symbol_table_baset &symbol_table)
1227 {
1228  // This is similar to initialization function except we do not ignore
1229  // the first argument
1231  function_name, type, loc, symbol_table, false);
1232  return code;
1233 }
1234 
1255  const exprt &object,
1256  irep_idt type_name,
1257  const source_locationt &loc,
1258  symbol_table_baset &symbol_table,
1259  code_blockt &code)
1260 {
1261  optionalt<symbol_typet> object_type;
1262 
1263  typet value_type;
1264  if(type_name==ID_boolean)
1265  {
1266  value_type=java_boolean_type();
1267  object_type=symbol_typet("java::java.lang.Boolean");
1268  }
1269  else if(type_name==ID_char)
1270  {
1271  value_type=java_char_type();
1272  object_type=symbol_typet("java::java.lang.Character");
1273  }
1274  else if(type_name==ID_byte)
1275  {
1276  value_type=java_byte_type();
1277  object_type=symbol_typet("java::java.lang.Byte");
1278  }
1279  else if(type_name==ID_short)
1280  {
1281  value_type=java_short_type();
1282  object_type=symbol_typet("java::java.lang.Short");
1283  }
1284  else if(type_name==ID_int)
1285  {
1286  value_type=java_int_type();
1287  object_type=symbol_typet("java::java.lang.Integer");
1288  }
1289  else if(type_name==ID_long)
1290  {
1291  value_type=java_long_type();
1292  object_type=symbol_typet("java::java.lang.Long");
1293  }
1294  else if(type_name==ID_float)
1295  {
1296  value_type=java_float_type();
1297  object_type=symbol_typet("java::java.lang.Float");
1298  }
1299  else if(type_name==ID_double)
1300  {
1301  value_type=java_double_type();
1302  object_type=symbol_typet("java::java.lang.Double");
1303  }
1304  else if(type_name==ID_void)
1305  return nil_exprt();
1306  else
1307  UNREACHABLE;
1308 
1309  DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");
1310 
1311  // declare tmp_type_name to hold the value
1312  std::string aux_name="tmp_"+id2string(type_name);
1314  value_type, aux_name, aux_name, loc, ID_java, symbol_table);
1315  exprt value=symbol.symbol_expr();
1316 
1317  // Check that the type of the object is in the symbol table,
1318  // otherwise there is no safe way of finding its value.
1319  if(
1320  const auto maybe_symbol =
1321  symbol_table.lookup(object_type->get_identifier()))
1322  {
1323  struct_typet struct_type=to_struct_type(maybe_symbol->type);
1324  // Check that the type has a value field
1325  const struct_union_typet::componentt value_comp=
1326  struct_type.get_component("value");
1327  if(!value_comp.is_nil())
1328  {
1330  dereference_exprt deref(
1332  member_exprt deref_value(deref, value_comp.get_name(), value_comp.type());
1333  code.add(code_assignt(value, deref_value), loc);
1334  return value;
1335  }
1336  }
1337 
1338  warning() << object_type->get_identifier()
1339  << " not available to format function" << eom;
1340  code.add(code_declt(value), loc);
1341  return value;
1342 }
1343 
1353  const exprt &argv,
1354  std::size_t index)
1355 {
1356  dereference_exprt deref_objs(argv, argv.type().subtype());
1357  pointer_typet empty_pointer=pointer_type(empty_typet());
1358  pointer_typet pointer_of_pointer=pointer_type(empty_pointer);
1359  member_exprt data_member(deref_objs, "data", pointer_of_pointer);
1360  plus_exprt data_pointer_plus_index(
1361  data_member, from_integer(index, java_int_type()), data_member.type());
1362  dereference_exprt data_at_index(
1363  data_pointer_plus_index, data_pointer_plus_index.type().subtype());
1364  return data_at_index;
1365 }
1366 
1401  const exprt &argv,
1402  std::size_t index,
1403  const struct_typet &structured_type,
1404  const source_locationt &loc,
1405  const irep_idt &function_id,
1406  symbol_table_baset &symbol_table,
1407  code_blockt &code)
1408 {
1409  // Declarations of the fields of arg_i_struct
1410  // arg_i_struct is { arg_i_string_expr, tmp_int, tmp_char, ... }
1411  struct_exprt arg_i_struct(structured_type);
1412  std::list<exprt> field_exprs;
1413  for(const auto & comp : structured_type.components())
1414  {
1415  const irep_idt &name=comp.get_name();
1416  const typet &type=comp.type();
1417  exprt field_expr;
1418  if(name!="string_expr")
1419  {
1420  std::string tmp_name="tmp_"+id2string(name);
1421  symbolt field_symbol = get_fresh_aux_symbol(
1422  type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
1423  field_expr=field_symbol.symbol_expr();
1424  code.add(code_declt(field_expr), loc);
1425  }
1426  else
1427  field_expr =
1428  make_nondet_string_expr(loc, function_id, symbol_table, code);
1429 
1430  field_exprs.push_back(field_expr);
1431  arg_i_struct.copy_to_operands(field_expr);
1432  }
1433 
1434  // arg_i = argv[index]
1435  exprt obj=get_object_at_index(argv, index);
1436  symbolt object_symbol = get_fresh_aux_symbol(
1437  obj.type(),
1438  id2string(function_id),
1439  "tmp_format_obj",
1440  loc,
1441  ID_java,
1442  symbol_table);
1443  symbol_exprt arg_i=object_symbol.symbol_expr();
1445  arg_i, symbol_table, loc, function_id, code);
1446  code.add(code_assignt(arg_i, obj), loc);
1447  code.add(
1448  code_assumet(
1449  not_exprt(
1450  equal_exprt(arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))),
1451  loc);
1452 
1453  // if arg_i != null then [code_not_null]
1454  code_ifthenelset code_avoid_null_arg;
1455  code_avoid_null_arg.cond()=not_exprt(equal_exprt(
1456  arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))));
1457  code_blockt code_not_null;
1458 
1459  // Assigning all the fields of arg_i_struct
1460  for(const auto &comp : structured_type.components())
1461  {
1462  const irep_idt &name=comp.get_name();
1463  exprt field_expr=field_exprs.front();
1464  field_exprs.pop_front();
1465 
1466  if(name=="string_expr")
1467  {
1468  pointer_typet string_pointer=
1469  java_reference_type(symbol_typet("java::java.lang.String"));
1470  typecast_exprt arg_i_as_string(arg_i, string_pointer);
1472  to_string_expr(field_expr),
1473  arg_i_as_string,
1474  loc,
1475  symbol_table,
1476  code_not_null);
1477  }
1478  else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
1479  {
1481  arg_i, name, loc, symbol_table, code_not_null);
1482  code_not_null.add(code_assignt(field_expr, value), loc);
1483  }
1484  else
1485  {
1486  // TODO: date_time and hash_code not implemented
1487  }
1488  }
1489 
1490  code.add(code_not_null, loc);
1491  return arg_i_struct;
1492 }
1493 
1506  const java_method_typet &type,
1507  const source_locationt &loc,
1508  const irep_idt &function_id,
1509  symbol_table_baset &symbol_table)
1510 {
1511  PRECONDITION(type.parameters().size()==2);
1512  code_blockt code;
1514  type.parameters(), loc, symbol_table, code);
1515  INVARIANT(args.size()==2, "String.format should have two arguments");
1516 
1517  // The argument can be:
1518  // a string, an integer, a floating point, a character, a boolean,
1519  // an object of which we take the hash code, or a date/time
1520  struct_typet structured_type;
1521  structured_type.components().emplace_back("string_expr", refined_string_type);
1522  structured_type.components().emplace_back(ID_int, java_int_type());
1523  structured_type.components().emplace_back(ID_float, java_float_type());
1524  structured_type.components().emplace_back(ID_char, java_char_type());
1525  structured_type.components().emplace_back(ID_boolean, java_boolean_type());
1526  // TODO: hash_code not implemented for now
1527  structured_type.components().emplace_back("hashcode", java_int_type());
1528  // TODO: date_time type not implemented for now
1529  structured_type.components().emplace_back("date_time", java_int_type());
1530 
1531  // We will process arguments so that each is converted to a `struct_exprt`
1532  // containing each possible type used in format specifiers.
1533  std::vector<exprt> processed_args;
1534  processed_args.push_back(args[0]);
1535  for(std::size_t i=0; i<MAX_FORMAT_ARGS; ++i)
1536  processed_args.push_back(
1538  args[1], i, structured_type, loc, function_id, symbol_table, code));
1539 
1541  ID_cprover_string_format_func, processed_args, loc, symbol_table, code);
1542  exprt java_string = allocate_fresh_string(
1543  type.return_type(), loc, function_id, symbol_table, code);
1544  code.add(
1546  java_string, string_expr, symbol_table),
1547  loc);
1548  code.add(code_returnt(java_string), loc);
1549  return code;
1550 }
1551 
1565  const java_method_typet &type,
1566  const source_locationt &loc,
1567  const irep_idt &function_id,
1568  symbol_table_baset &symbol_table)
1569 {
1571  const symbol_exprt this_obj(params[0].get_identifier(), params[0].type());
1572 
1573  // Code to be returned
1574  code_blockt code;
1575 
1576  // > Class class1;
1577  pointer_typet class_type=
1579  symbol_table.lookup_ref("java::java.lang.Class").type);
1580  symbolt class1_sym=get_fresh_aux_symbol(
1581  class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
1582  symbol_exprt class1=class1_sym.symbol_expr();
1583  code.add(code_declt(class1), loc);
1584 
1585  // class_identifier is this->@class_identifier
1586  member_exprt class_identifier(
1587  checked_dereference(this_obj, this_obj.type().subtype()),
1588  "@class_identifier",
1589  string_typet());
1590 
1591  // string_expr = cprover_string_literal(this->@class_identifier)
1593  ID_cprover_string_literal_func,
1594  {class_identifier},
1595  loc,
1596  symbol_table,
1597  code);
1598 
1599  // string_expr1 = substr(string_expr, 6)
1600  // We do this to remove the "java::" prefix
1602  ID_cprover_string_substring_func,
1603  {string_expr, from_integer(6, java_int_type())},
1604  loc,
1605  symbol_table,
1606  code);
1607 
1608  // string1 = (String*) string_expr
1609  pointer_typet string_ptr_type=java_reference_type(
1610  symbol_table.lookup_ref("java::java.lang.String").type);
1611  exprt string1 = allocate_fresh_string(
1612  string_ptr_type, loc, function_id, symbol_table, code);
1613  code.add(
1614  code_assign_string_expr_to_java_string(string1, string_expr1, symbol_table),
1615  loc);
1616 
1617  // > class1 = Class.forName(string1)
1618  code_function_callt fun_call;
1619  fun_call.function()=symbol_exprt(
1620  "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
1621  fun_call.lhs()=class1;
1622  fun_call.arguments().push_back(string1);
1623  const java_method_typet fun_type(
1624  {java_method_typet::parametert(string_ptr_type)}, class_type);
1625  fun_call.function().type()=fun_type;
1626  code.add(fun_call, loc);
1627 
1628  // > return class1;
1629  code.add(code_returnt(class1), loc);
1630  return code;
1631 }
1632 
1644  const irep_idt &function_name,
1645  const java_method_typet &type,
1646  const source_locationt &loc,
1647  symbol_table_baset &symbol_table)
1648 {
1649  code_blockt code;
1651  type.parameters(), loc, symbol_table, code);
1652  code.add(
1654  function_name, args, type.return_type(), symbol_table),
1655  loc);
1656  return code;
1657 }
1658 
1673  const irep_idt &function_name,
1674  const java_method_typet &type,
1675  const source_locationt &loc,
1676  symbol_table_baset &symbol_table)
1677 {
1678  // Code for the output
1679  code_blockt code;
1680 
1681  // Calling the function
1683  type.parameters(), loc, symbol_table, code);
1684 
1685  // String expression that will hold the result
1686  refined_string_exprt string_expr =
1687  string_expr_of_function(function_name, arguments, loc, symbol_table, code);
1688 
1689  // Assign to string
1691  type.return_type(), loc, function_name, symbol_table, code);
1692  code.add(
1693  code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
1694  loc);
1695 
1696  // Return value
1697  code.add(code_returnt(str), loc);
1698  return code;
1699 }
1700 
1715  const java_method_typet &type,
1716  const source_locationt &loc,
1717  const irep_idt &function_id,
1718  symbol_table_baset &symbol_table)
1719 {
1720  // Code for the output
1721  code_blockt code;
1722 
1723  // String expression that will hold the result
1724  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
1725 
1726  // Assign the argument to string_expr
1728  symbol_exprt arg0(op.get_identifier(), op.type());
1730  string_expr, arg0, loc, symbol_table, code);
1731 
1732  // Allocate and assign the string
1734  type.return_type(), loc, function_id, symbol_table, code);
1735  code.add(
1736  code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
1737  loc);
1738 
1739  // Return value
1740  code.add(code_returnt(str), loc);
1741  return code;
1742 }
1743 
1757  const java_method_typet &type,
1758  const source_locationt &loc,
1759  const irep_idt &function_id,
1760  symbol_table_baset &symbol_table)
1761 {
1762  (void)function_id;
1763 
1764  // Code for the output
1765  code_blockt code;
1766 
1767  // String expression that will hold the result
1768  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
1769 
1770  // Assign argument to a string_expr
1772  symbol_exprt arg1(params[1].get_identifier(), params[1].type());
1774  string_expr, arg1, loc, symbol_table, code);
1775 
1776  // Assign string_expr to `this` object
1777  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1778  code.add(
1779  code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1780  loc);
1781 
1782  return code;
1783 }
1784 
1795  const java_method_typet &type,
1796  const source_locationt &loc,
1797  const irep_idt &function_id,
1798  symbol_table_baset &symbol_table)
1799 {
1800  (void)function_id;
1801 
1802  // Code for the output
1803  code_blockt code;
1804 
1806  PRECONDITION(params.size() == 4);
1807  exprt::operandst args =
1808  process_parameters(type.parameters(), loc, symbol_table, code);
1809  INVARIANT(
1810  args.size() == 4, "process_parameters preserves number of arguments");
1811 
1814  refined_string_exprt string_arg = to_string_expr(args[1]);
1815 
1816  // The third argument is `count`, whereas the third argument of substring
1817  // is `end` which corresponds to `offset+count`
1819  ID_cprover_string_substring_func,
1820  {args[1], args[2], plus_exprt(args[2], args[3])},
1821  loc,
1822  symbol_table,
1823  code);
1824 
1825  // Assign string_expr to `this` object
1826  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1827  code.add(
1828  code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1829  loc);
1830 
1831  return code;
1832 }
1833 
1846  const java_method_typet &type,
1847  const source_locationt &loc,
1848  const irep_idt &function_id,
1849  symbol_table_baset &symbol_table)
1850 {
1851  (void)function_id;
1852 
1854  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1855  dereference_exprt deref =
1856  checked_dereference(arg_this, arg_this.type().subtype());
1857 
1858  code_returnt ret(get_length(deref, symbol_table));
1859  ret.add_source_location() = loc;
1860 
1861  return ret;
1862 }
1863 
1865  const irep_idt &function_id) const
1866 {
1867  for(const id_mapt *map : id_maps)
1868  if(map->count(function_id) != 0)
1869  return true;
1870 
1871  return conversion_table.count(function_id) != 0;
1872 }
1873 
1874 template <typename TMap, typename TContainer>
1875 void add_keys_to_container(const TMap &map, TContainer &container)
1876 {
1877  static_assert(
1878  std::is_same<typename TMap::key_type,
1879  typename TContainer::value_type>::value,
1880  "TContainer value_type doesn't match TMap key_type");
1881  std::transform(
1882  map.begin(),
1883  map.end(),
1884  std::inserter(container, container.begin()),
1885  [](const typename TMap::value_type &pair) { return pair.first; });
1886 }
1887 
1889  std::unordered_set<irep_idt> &methods) const
1890 {
1891  for(const id_mapt *map : id_maps)
1892  add_keys_to_container(*map, methods);
1893 
1895 }
1896 
1906  const symbolt &symbol,
1907  symbol_table_baset &symbol_table)
1908 {
1909  const irep_idt &function_id = symbol.name;
1910  const java_method_typet &type = to_java_method_type(symbol.type);
1911  const source_locationt &loc = symbol.location;
1912  auto it_id=cprover_equivalent_to_java_function.find(function_id);
1913  if(it_id!=cprover_equivalent_to_java_function.end())
1914  return make_function_from_call(it_id->second, type, loc, symbol_table);
1915 
1919  it_id->second, type, loc, symbol_table);
1920 
1921  it_id=cprover_equivalent_to_java_constructor.find(function_id);
1924  it_id->second, type, loc, symbol_table);
1925 
1929  it_id->second, type, loc, symbol_table);
1930 
1931  it_id=cprover_equivalent_to_java_assign_function.find(function_id);
1934  it_id->second, type, loc, symbol_table);
1935 
1936  auto it=conversion_table.find(function_id);
1937  if(it!=conversion_table.end())
1938  return it->second(type, loc, function_id, symbol_table);
1939 
1940  return nil_exprt();
1941 }
1942 
1948  irep_idt class_name)
1949 {
1950  return string_types.find(class_name)!=string_types.end();
1951 }
1952 
1954 {
1955  string_types = std::unordered_set<irep_idt>{"java.lang.String",
1956  "java.lang.StringBuilder",
1957  "java.lang.CharSequence",
1958  "java.lang.StringBuffer"};
1959 }
1960 
1963 {
1965 
1966  // The following list of function is organized by libraries, with
1967  // constructors first and then methods in alphabetic order.
1968  // Methods that are not supported here should ultimately have Java models
1969  // provided for them in the class-path.
1970 
1971  // String library
1972  conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1973  std::bind(
1975  this,
1976  std::placeholders::_1,
1977  std::placeholders::_2,
1978  std::placeholders::_3,
1979  std::placeholders::_4);
1981  ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1983  this,
1984  std::placeholders::_1,
1985  std::placeholders::_2,
1986  std::placeholders::_3,
1987  std::placeholders::_4);
1988  conversion_table["java::java.lang.String.<init>:([CII)V"] = std::bind(
1990  this,
1991  std::placeholders::_1,
1992  std::placeholders::_2,
1993  std::placeholders::_3,
1994  std::placeholders::_4);
1996  ["java::java.lang.String.<init>:()V"]=
1997  ID_cprover_string_empty_string_func;
1998 
1999  // CProverString.charAt differs from the Java String.charAt in that no
2000  // exception is raised for the out of bounds case.
2002  ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
2003  ID_cprover_string_char_at_func;
2005  ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
2006  ID_cprover_string_code_point_at_func;
2008  ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
2009  ID_cprover_string_code_point_before_func;
2011  ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
2012  ID_cprover_string_code_point_count_func;
2014  ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
2015  ID_cprover_string_compare_to_func;
2017  ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
2018  ID_cprover_string_concat_func;
2020  ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
2021  ID_cprover_string_contains_func;
2023  ["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
2024  ID_cprover_string_copy_func;
2026  ["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
2027  ID_cprover_string_copy_func;
2029  ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
2030  ID_cprover_string_endswith_func;
2031 
2032  conversion_table["java::java.lang.String.equals:(Ljava/lang/Object;)Z"] =
2033  std::bind(
2035  this,
2036  std::placeholders::_1,
2037  std::placeholders::_2,
2038  std::placeholders::_3,
2039  std::placeholders::_4);
2041  ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
2042  ID_cprover_string_equals_ignore_case_func;
2044  ["java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)"
2045  "Ljava/lang/String;"] =
2046  std::bind(
2048  this,
2049  std::placeholders::_1,
2050  std::placeholders::_2,
2051  std::placeholders::_3,
2052  std::placeholders::_4);
2054  ["java::java.lang.String.hashCode:()I"]=
2055  ID_cprover_string_hash_code_func;
2057  ["java::java.lang.String.indexOf:(I)I"]=
2058  ID_cprover_string_index_of_func;
2060  ["java::java.lang.String.indexOf:(II)I"]=
2061  ID_cprover_string_index_of_func;
2063  ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
2064  ID_cprover_string_index_of_func;
2066  ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
2067  ID_cprover_string_index_of_func;
2069  ["java::java.lang.String.intern:()Ljava/lang/String;"]=
2070  ID_cprover_string_intern_func;
2072  ["java::java.lang.String.isEmpty:()Z"]=
2073  ID_cprover_string_is_empty_func;
2075  ["java::java.lang.String.lastIndexOf:(I)I"]=
2076  ID_cprover_string_last_index_of_func;
2078  ["java::java.lang.String.lastIndexOf:(II)I"]=
2079  ID_cprover_string_last_index_of_func;
2081  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
2082  ID_cprover_string_last_index_of_func;
2084  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
2085  ID_cprover_string_last_index_of_func;
2086  conversion_table["java::java.lang.String.length:()I"] = std::bind(
2088  this,
2089  std::placeholders::_1,
2090  std::placeholders::_2,
2091  std::placeholders::_3,
2092  std::placeholders::_4);
2094  ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
2095  "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
2097  ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
2098  ID_cprover_string_replace_func;
2100  ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
2101  ID_cprover_string_replace_func;
2103  ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
2104  ID_cprover_string_startswith_func;
2106  ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
2107  ID_cprover_string_startswith_func;
2109  ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
2110  "lang/CharSequence;"] = ID_cprover_string_substring_func;
2111  // CProverString.substring differs from the Java String.substring in that no
2112  // exception is raised for the out of bounds case.
2114  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
2115  "Ljava/lang/String;"]=
2116  ID_cprover_string_substring_func;
2118  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
2119  "Ljava/lang/String;"]=
2120  ID_cprover_string_substring_func;
2122  ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
2123  ID_cprover_string_to_lower_case_func;
2124  conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
2125  std::bind(
2127  this,
2128  std::placeholders::_1,
2129  std::placeholders::_2,
2130  std::placeholders::_3,
2131  std::placeholders::_4);
2133  ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
2134  ID_cprover_string_to_upper_case_func;
2136  ["java::java.lang.String.trim:()Ljava/lang/String;"]=
2137  ID_cprover_string_trim_func;
2139  ["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
2140  ID_cprover_string_of_bool_func;
2142  ["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
2143  ID_cprover_string_of_char_func;
2144  conversion_table["java::java.lang.String.valueOf:(D)Ljava/lang/String;"] =
2145  std::bind(
2147  this,
2148  std::placeholders::_1,
2149  std::placeholders::_2,
2150  std::placeholders::_3,
2151  std::placeholders::_4);
2152  conversion_table["java::java.lang.String.valueOf:(F)Ljava/lang/String;"] =
2153  std::bind(
2155  this,
2156  std::placeholders::_1,
2157  std::placeholders::_2,
2158  std::placeholders::_3,
2159  std::placeholders::_4);
2161  ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
2162  ID_cprover_string_of_int_func;
2164  ["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
2165  ID_cprover_string_of_long_func;
2166 
2167  // StringBuilder library
2169  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
2171  this,
2172  std::placeholders::_1,
2173  std::placeholders::_2,
2174  std::placeholders::_3,
2175  std::placeholders::_4);
2177  ["java::java.lang.StringBuilder.<init>:()V"]=
2178  ID_cprover_string_empty_string_func;
2179 
2181  ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
2182  ID_cprover_string_concat_char_func;
2184  ["java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] =
2185  ID_cprover_string_concat_func;
2187  ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
2188  ID_cprover_string_concat_double_func;
2190  ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
2191  "lang/CharSequence;II)"
2192  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2194  ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
2195  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2197  ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
2198  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2200  ["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]=
2201  ID_cprover_string_concat_bool_func;
2203  ["java::java.lang.StringBuilder.appendCodePoint:(I)"
2204  "Ljava/lang/StringBuilder;"]=
2205  ID_cprover_string_concat_code_point_func;
2207  ["java::java.lang.StringBuilder.charAt:(I)C"]=
2208  ID_cprover_string_char_at_func;
2210  ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
2211  ID_cprover_string_code_point_at_func;
2213  ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
2214  ID_cprover_string_code_point_before_func;
2216  ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
2217  ID_cprover_string_code_point_count_func;
2219  ["java::org.cprover.CProverString.delete:(Ljava/lang/"
2220  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2221  ID_cprover_string_delete_func;
2223  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
2224  "StringBuilder;I)Ljava/lang/StringBuilder;"] =
2225  ID_cprover_string_delete_char_at_func;
2227  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2228  "StringBuilder;IC)Ljava/lang/StringBuilder;"] =
2229  ID_cprover_string_insert_char_func;
2231  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2232  "StringBuilder;IZ)Ljava/lang/StringBuilder;"] =
2233  ID_cprover_string_insert_bool_func;
2235  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2236  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2237  ID_cprover_string_insert_int_func;
2239  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2240  "StringBuilder;IJ)Ljava/lang/StringBuilder;"] =
2241  ID_cprover_string_insert_long_func;
2243  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
2244  "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
2245  conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
2247  this,
2248  std::placeholders::_1,
2249  std::placeholders::_2,
2250  std::placeholders::_3,
2251  std::placeholders::_4);
2253  ["java::java.lang.StringBuilder.setCharAt:(IC)V"]=
2254  ID_cprover_string_char_set_func;
2256  ["java::java.lang.StringBuilder.setLength:(I)V"]=
2257  ID_cprover_string_set_length_func;
2259  ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
2260  ID_cprover_string_substring_func;
2262  ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
2263  ID_cprover_string_substring_func;
2265  ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
2267  this,
2268  std::placeholders::_1,
2269  std::placeholders::_2,
2270  std::placeholders::_3,
2271  std::placeholders::_4);
2272 
2273  // StringBuffer library
2275  ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
2277  this,
2278  std::placeholders::_1,
2279  std::placeholders::_2,
2280  std::placeholders::_3,
2281  std::placeholders::_4);
2283  ["java::java.lang.StringBuffer.<init>:()V"]=
2284  ID_cprover_string_empty_string_func;
2285 
2287  ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
2288  ID_cprover_string_concat_char_func;
2290  ["java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]=
2291  ID_cprover_string_concat_double_func;
2293  ["java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]=
2294  ID_cprover_string_concat_float_func;
2296  ["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]=
2297  ID_cprover_string_concat_int_func;
2299  ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
2300  ID_cprover_string_concat_long_func;
2302  ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
2303  "Ljava/lang/StringBuffer;"]=
2304  ID_cprover_string_concat_func;
2306  ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
2307  "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
2309  ["java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"] =
2310  ID_cprover_string_concat_bool_func;
2312  ["java::java.lang.StringBuffer.appendCodePoint:(I)"
2313  "Ljava/lang/StringBuffer;"]=
2314  ID_cprover_string_concat_code_point_func;
2316  ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
2317  ID_cprover_string_char_at_func;
2319  ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
2320  ID_cprover_string_code_point_at_func;
2322  ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
2323  ID_cprover_string_code_point_before_func;
2325  ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
2326  ID_cprover_string_code_point_count_func;
2328  ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
2329  "lang/StringBuffer;"] = ID_cprover_string_delete_func;
2331  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
2332  "StringBufferI)Ljava/lang/StringBuffer;"] =
2333  ID_cprover_string_delete_char_at_func;
2335  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/"
2336  "lang/StringBuffer;"] = ID_cprover_string_insert_char_func;
2338  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/"
2339  "lang/StringBuffer;"] = ID_cprover_string_insert_int_func;
2341  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/"
2342  "lang/StringBuffer;"] = ID_cprover_string_insert_long_func;
2344  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/"
2345  "lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func;
2347  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/"
2348  "lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
2350  ["java::java.lang.StringBuffer.length:()I"]=
2351  conversion_table["java::java.lang.String.length:()I"];
2353  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
2354  ID_cprover_string_char_set_func;
2356  ["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
2357  ID_cprover_string_set_length_func;
2359  ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
2360  ID_cprover_string_substring_func;
2362  ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
2363  "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
2365  ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
2367  this,
2368  std::placeholders::_1,
2369  std::placeholders::_2,
2370  std::placeholders::_3,
2371  std::placeholders::_4);
2372 
2373  // CharSequence library
2375  ["java::java.lang.CharSequence.charAt:(I)C"]=
2376  ID_cprover_string_char_at_func;
2378  ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
2380  this,
2381  std::placeholders::_1,
2382  std::placeholders::_2,
2383  std::placeholders::_3,
2384  std::placeholders::_4);
2386  ["java::java.lang.CharSequence.length:()I"]=
2387  conversion_table["java::java.lang.String.length:()I"];
2388 
2389  // Other libraries
2390  conversion_table["java::java.lang.Float.toString:(F)Ljava/lang/String;"] =
2391  std::bind(
2393  this,
2394  std::placeholders::_1,
2395  std::placeholders::_2,
2396  std::placeholders::_3,
2397  std::placeholders::_4);
2399  ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
2400  ID_cprover_string_parse_int_func;
2402  ["java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
2403  ID_cprover_string_parse_int_func;
2405  ["java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
2406  ID_cprover_string_parse_int_func;
2408  ["java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
2409  ID_cprover_string_parse_int_func;
2411  ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
2412  ID_cprover_string_of_int_hex_func;
2414  ["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
2415  ID_cprover_string_of_int_func;
2417  ["java::java.lang.Integer.toString:(II)Ljava/lang/String;"]=
2418  ID_cprover_string_of_int_func;
2420  ["java::java.lang.Long.toString:(J)Ljava/lang/String;"]=
2421  ID_cprover_string_of_int_func;
2423  ["java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
2424  ID_cprover_string_of_int_func;
2425  conversion_table["java::java.lang.Object.getClass:()Ljava/lang/Class;"] =
2426  std::bind(
2428  this,
2429  std::placeholders::_1,
2430  std::placeholders::_2,
2431  std::placeholders::_3,
2432  std::placeholders::_4);
2433 }
#define loc()
const irep_idt & get_name() const
Definition: std_types.h:182
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
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:221
const codet & then_case() const
Definition: std_code.h:486
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
Boolean negation.
Definition: std_expr.h:3228
semantic type conversion
Definition: std_expr.h:2111
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.
static bool is_java_string_type(const typet &type)
codet make_equals_function_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.equals(Object) function.
bool is_nil() const
Definition: irep.h:172
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
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:176
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...
static bool is_java_string_pointer_type(const typet &type)
typet java_boolean_type()
Definition: java_types.cpp:72
static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the data component.
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
typet java_double_type()
Definition: java_types.cpp:67
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...
irep_idt mode
Language mode.
Definition: symbol.h:52
const exprt & cond() const
Definition: std_code.h:476
Evaluates to true if the operand is infinite.
Definition: std_expr.h:4038
irep_idt get_tag(const typet &type)
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
typet java_int_type()
Definition: java_types.cpp:32
const exprt & content() const
Definition: string_expr.h:216
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Type for string expressions used by the string solver.
const refined_string_typet refined_string_type
#define MAX_FORMAT_ARGS
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
Fresh auxiliary symbol creation.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
The null pointer constant.
Definition: std_expr.h:4518
codet 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.
std::vector< parametert > parameterst
Definition: std_types.h:767
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.
const componentst & components() const
Definition: std_types.h:245
The trinary if-then-else operator.
Definition: std_expr.h:3359
static bool is_java_char_sequence_pointer_type(const typet &type)
typet java_long_type()
Definition: java_types.cpp:42
typet string_data_type(const symbol_tablet &symbol_table)
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
typet & type()
Definition: expr.h:56
std::unordered_set< irep_idt > string_types
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
A constant literal expression.
Definition: std_expr.h:4422
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
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...
void set_access(const irep_idt &access)
Definition: java_types.h:109
static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
access length member
static bool is_java_string_buffer_pointer_type(const typet &type)
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
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...
Extract member of struct or union.
Definition: std_expr.h:3869
TO_BE_DOCUMENTED.
Definition: std_types.h:1578
void change_spec(const ieee_float_spect &dest_spec)
mstreamt & warning() const
Definition: message.h:307
equality
Definition: std_expr.h:1354
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
const irep_idt & id() const
Definition: irep.h:259
static bool is_java_string_builder_type(const typet &type)
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3986
An expression denoting infinity.
Definition: std_expr.h:4692
void add(const codet &code)
Definition: std_code.h:112
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:890
A reference into the symbol table.
Definition: std_types.h:110
A declaration of a local variable.
Definition: std_code.h:254
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
The NIL expression.
Definition: std_expr.h:4508
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
The pointer type.
Definition: std_types.h:1435
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
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:277
The empty type.
Definition: std_types.h:54
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 ...
Operator to dereference a pointer.
Definition: std_expr.h:3282
nonstd::optional< T > optionalt
Definition: optional.h:35
boolean AND
Definition: std_expr.h:2255
const std::array< id_mapt *, 5 > id_maps
API to expression classes.
std::unordered_map< irep_idt, irep_idt > id_mapt
The symbol table.
Definition: symbol_table.h:19
codet 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.
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:230
exprt get_object_at_index(const exprt &argv, std::size_t index)
Helper for format function.
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
void set_tag(const irep_idt &tag)
Definition: std_types.h:267
void from_float(const float f)
A function call.
Definition: std_code.h:858
The plus expression.
Definition: std_expr.h:893
typet string_length_type()
typet java_byte_type()
Definition: java_types.cpp:52
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.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
typet component_type(const irep_idt &component_name) const
Definition: std_types.cpp:68
Operator to return the address of an object.
Definition: std_expr.h:3168
static bool is_java_char_array_pointer_type(const typet &type)
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...
The unary minus expression.
Definition: std_expr.h:444
typet java_short_type()
Definition: java_types.cpp:47
codet 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.
codet make_init_from_array_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 constructor from a char array.
codet code_assign_string_expr_to_java_string(const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table)
Produce code for an assignemnt of a string expr to a Java string.
bool implements_function(const irep_idt &function_id) const
std::vector< exprt > operandst
Definition: expr.h:45
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
codet 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.
An assumption, which must hold in subsequent code.
Definition: std_code.h:357
String expressions for the string solver.
void add_keys_to_container(const TMap &map, TContainer &container)
static bool is_java_char_array_type(const typet &type)
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
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.
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.
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:289
static typet get_length_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the length component.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
exprt 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...
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.
exprt & function()
Definition: std_code.h:878
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
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).
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
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.
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
codet 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.
codet 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...
codet 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.
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
character_refine_preprocesst character_preprocess
#define UNREACHABLE
Definition: invariant.h:271
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const exprt & length() const
Definition: string_expr.h:206
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.
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...
static bool java_type_matches_tag(const typet &type, const std::string &tag)
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Sequential composition.
Definition: std_code.h:89
static bool implements_java_char_sequence_pointer(const typet &type)
exprt allocate_fresh_array(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &code)
declare a new character array and allocate it
arrays with given size
Definition: std_types.h:1013
An if-then-else.
Definition: std_code.h:466
static bool is_java_string_buffer_type(const typet &type)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const char * c_str() const
Definition: dstring.h:84
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
codet 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.
dstringt irep_idt
Definition: irep.h:32
A statement in a programming language.
Definition: std_code.h:21
Return from a function.
Definition: std_code.h:923
bool is_type
Definition: symbol.h:63
typet java_char_type()
Definition: java_types.cpp:57
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...
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
codet 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...
codet 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. ...
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static bool is_java_string_builder_pointer_type(const typet &type)
codet 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 ignore_first_arg=true)
Generate the goto code for string initialization.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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)
struct constructor from list of elements
Definition: std_expr.h:1815
typet java_float_type()
Definition: java_types.cpp:62
const codet & else_case() const
Definition: std_code.h:496
const irep_idt & get_identifier() const
Definition: std_types.h:840
const typet & return_type() const
Definition: std_types.h:895
codet code_assign_components_to_java_string(const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table)
Produce code for an assignment of a string expr to a Java string.
const irep_idt & get_identifier() const
Definition: std_types.h:123
Assignment.
Definition: std_code.h:196
void add_base(const typet &base)
Definition: std_types.h:396
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...
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...
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
const componentt & get_component(const irep_idt &component_name) const
Definition: std_types.cpp:51
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.
static bool is_java_char_sequence_type(const typet &type)
static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
access data member
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2989
Produce code for simple implementation of String Java libraries.
array index operator
Definition: std_expr.h:1462
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 type_name tmp_type_name tmp_type_name = ((Classname*)arg_i...