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.components().resize(3);
226  string_type.components()[0].set_name("@java.lang.Object");
227  string_type.components()[0].set_pretty_name("@java.lang.Object");
228  string_type.components()[0].type()=symbol_typet("java::java.lang.Object");
229  string_type.components()[1].set_name("length");
230  string_type.components()[1].set_pretty_name("length");
231  string_type.components()[1].type()=string_length_type();
232  string_type.components()[2].set_name("data");
233  string_type.components()[2].set_pretty_name("data");
234  string_type.components()[2].type() = pointer_type(java_char_type());
235  string_type.set_access(ID_public);
236  string_type.add_base(symbol_typet("java::java.lang.Object"));
237 
238  std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
239  for(const irep_idt &base_name : bases)
240  string_type.add_base(symbol_typet("java::" + id2string(base_name)));
241 
242  symbolt tmp_string_symbol;
243  tmp_string_symbol.name="java::"+id2string(class_name);
244  symbolt *string_symbol=nullptr;
245  symbol_table.move(tmp_string_symbol, string_symbol);
246  string_symbol->base_name=id2string(class_name);
247  string_symbol->pretty_name=id2string(class_name);
248  string_symbol->type=string_type;
249  string_symbol->is_type=true;
250  string_symbol->mode = ID_java;
251 }
252 
259  const typet &type,
260  const source_locationt &location,
261  symbol_tablet &symbol_table)
262 {
263  symbolt array_symbol=get_fresh_aux_symbol(
264  type,
265  "cprover_string_array",
266  "cprover_string_array",
267  location,
268  ID_java,
269  symbol_table);
270  array_symbol.is_static_lifetime=true;
271  return array_symbol.symbol_expr();
272 }
273 
282  const code_typet::parameterst &params,
283  const source_locationt &loc,
284  symbol_table_baset &symbol_table,
285  code_blockt &init_code)
286 {
287  exprt::operandst ops;
288  for(const auto &p : params)
289  {
290  symbol_exprt sym(p.get_identifier(), p.type());
291  ops.push_back(sym);
292  }
293  return process_operands(ops, loc, symbol_table, init_code);
294 }
295 
312  const exprt &expr_to_process,
313  const source_locationt &loc,
314  symbol_table_baset &symbol_table,
315  code_blockt &init_code)
316 {
318  const refined_string_exprt string_expr =
319  decl_string_expr(loc, symbol_table, init_code);
321  string_expr, expr_to_process, loc, symbol_table, init_code);
322  return string_expr;
323 }
324 
337  const exprt::operandst &operands,
338  const source_locationt &loc,
339  symbol_table_baset &symbol_table,
340  code_blockt &init_code)
341 {
342  exprt::operandst ops;
343  for(const auto &p : operands)
344  {
346  ops.push_back(
347  convert_exprt_to_string_exprt(p, loc, symbol_table, init_code));
348  else if(is_java_char_array_pointer_type(p.type()))
349  ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
350  else
351  ops.push_back(p);
352  }
353  return ops;
354 }
355 
367  const exprt::operandst &operands,
368  const source_locationt &loc,
369  symbol_table_baset &symbol_table,
370  code_blockt &init_code)
371 {
372  PRECONDITION(operands.size()==2);
373  exprt::operandst ops;
374  const exprt &op0=operands[0];
375  const exprt &op1 = operands[1];
377 
378  ops.push_back(
379  convert_exprt_to_string_exprt(op0, loc, symbol_table, init_code));
380 
381  // TODO: Manage the case where we have a non-String Object (this should
382  // probably be handled upstream. At any rate, the following code should be
383  // protected with assertions on the type of op1.
384  typecast_exprt tcast(op1, to_pointer_type(op0.type()));
385  ops.push_back(
386  convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code));
387  return ops;
388 }
389 
394 static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
395 {
396  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
397  if(type.id()==ID_symbol)
398  {
399  symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
400  CHECK_RETURN(sym.type.id()!=ID_symbol);
401  return get_data_type(sym.type, symbol_table);
402  }
403  // else type id is ID_struct
404  const struct_typet &struct_type=to_struct_type(type);
405  return struct_type.component_type("data");
406 }
407 
412 static typet
413 get_length_type(const typet &type, const symbol_tablet &symbol_table)
414 {
415  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
416  if(type.id()==ID_symbol)
417  {
418  symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
419  CHECK_RETURN(sym.type.id()!=ID_symbol);
420  return get_length_type(sym.type, symbol_table);
421  }
422  // else type id is ID_struct
423  const struct_typet &struct_type=to_struct_type(type);
424  return struct_type.component_type("length");
425 }
426 
431 static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
432 {
433  return member_exprt(
434  expr, "length", get_length_type(expr.type(), symbol_table));
435 }
436 
441 static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
442 {
443  return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table));
444 }
445 
454  const exprt &array_pointer,
455  const source_locationt &loc,
456  symbol_table_baset &symbol_table,
457  code_blockt &code)
458 {
459  // array is *array_pointer
460  dereference_exprt array=
461  checked_dereference(array_pointer, array_pointer.type().subtype());
462  // array_data is array_pointer-> data
463  const exprt array_data = get_data(array, symbol_table);
464  symbolt sym_char_array = get_fresh_aux_symbol(
465  array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
466  symbol_exprt char_array=sym_char_array.symbol_expr();
467  // char_array = array_pointer->data
468  code.add(code_assignt(char_array, array_data), loc);
469 
470  // string_expr is `{ rhs->length; string_array }`
471  refined_string_exprt string_expr(
472  get_length(array, symbol_table), char_array, refined_string_type);
473 
474  dereference_exprt inf_array(
476 
478  string_expr.content(), inf_array, symbol_table, loc, code);
479 
480  return string_expr;
481 }
482 
490  const typet &type,
491  const source_locationt &loc,
492  symbol_table_baset &symbol_table)
493 {
494  symbolt string_symbol=get_fresh_aux_symbol(
495  type, "cprover_string", "cprover_string", loc, ID_java, symbol_table);
496  string_symbol.is_static_lifetime=true;
497  return string_symbol.symbol_expr();
498 }
499 
507  const source_locationt &loc,
508  symbol_table_baset &symbol_table,
509  code_blockt &code)
510 {
511  symbolt sym_length = get_fresh_aux_symbol(
512  index_type,
513  "cprover_string_length",
514  "cprover_string_length",
515  loc,
516  ID_java,
517  symbol_table);
518  symbol_exprt length_field=sym_length.symbol_expr();
519  pointer_typet array_type = pointer_type(java_char_type());
520  symbolt sym_content = get_fresh_aux_symbol(
521  array_type,
522  "cprover_string_content",
523  "cprover_string_content",
524  loc,
525  ID_java,
526  symbol_table);
527  symbol_exprt content_field = sym_content.symbol_expr();
528  code.add(code_declt(content_field), loc);
529  refined_string_exprt str(length_field, content_field, refined_string_type);
530  code.add(code_declt(length_field), loc);
531  return str;
532 }
533 
541  const source_locationt &loc,
542  const irep_idt &function_id,
543  symbol_table_baset &symbol_table,
544  code_blockt &code)
545 {
547  const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
548 
549  side_effect_expr_nondett nondet_length(str.length().type());
550  code.add(code_assignt(str.length(), nondet_length), loc);
551 
552  exprt nondet_array_expr =
553  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
554 
555  address_of_exprt array_pointer(
556  index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
557 
559  array_pointer, nondet_array_expr, symbol_table, loc, code);
560 
562  nondet_array_expr, str.length(), symbol_table, loc, code);
563 
564  code.add(code_assignt(str.content(), array_pointer), loc);
565 
566  return refined_string_exprt(str.length(), str.content());
567 }
568 
576  const typet &type,
577  const source_locationt &loc,
578  const irep_idt &function_id,
579  symbol_table_baset &symbol_table,
580  code_blockt &code)
581 {
582  exprt str=fresh_string(type, loc, symbol_table);
583  allocate_dynamic_object_with_decl(str, symbol_table, loc, function_id, code);
584  return str;
585 }
586 
594  const typet &type,
595  const source_locationt &loc,
596  const irep_idt &function_id,
597  symbol_tablet &symbol_table,
598  code_blockt &code)
599 {
600  exprt array=fresh_array(type, loc, symbol_table);
601  code.add(code_declt(array), loc);
603  array, symbol_table, loc, function_id, code);
604  return array;
605 }
606 
617  const exprt &lhs,
618  const irep_idt &function_name,
619  const exprt::operandst &arguments,
620  symbol_table_baset &symbol_table)
621 {
623  function_name, arguments, lhs.type(), symbol_table);
624  return code_assignt(lhs, fun_app);
625 }
626 
637  const irep_idt &function_name,
638  const exprt::operandst &arguments,
639  const typet &type,
640  symbol_table_baset &symbol_table)
641 {
643  function_name, arguments, type, symbol_table);
644  return code_returnt(fun_app);
645 }
646 
653  symbol_table_baset &symbol_table,
654  const source_locationt &loc,
655  const irep_idt &function_id,
656  code_blockt &code)
657 {
658  const array_typet array_type(
660  const symbolt data_sym = get_fresh_aux_symbol(
661  array_type,
662  "nondet_infinite_array",
663  "nondet_infinite_array",
664  loc,
665  ID_java,
666  symbol_table);
667  const symbol_exprt data_expr = data_sym.symbol_expr();
668  code.add(code_declt(data_expr), loc);
669  side_effect_expr_nondett nondet_data(data_expr.type());
670  code.add(code_assignt(data_expr, nondet_data), loc);
671  return data_expr;
672 }
673 
682  const exprt &pointer,
683  const exprt &array,
684  symbol_table_baset &symbol_table,
685  const source_locationt &loc,
686  code_blockt &code)
687 {
688  PRECONDITION(array.type().id() == ID_array);
689  PRECONDITION(pointer.type().id() == ID_pointer);
690  symbolt &return_sym = get_fresh_aux_symbol(
691  java_int_type(),
692  "return_array",
693  "return_array",
694  loc,
695  ID_java,
696  symbol_table);
697  exprt return_expr = return_sym.symbol_expr();
698  code.add(code_declt(return_expr), loc);
699  code.add(
701  return_expr,
702  ID_cprover_associate_array_to_pointer_func,
703  {array, pointer},
704  symbol_table),
705  loc);
706 }
707 
716  const exprt &array,
717  const exprt &length,
718  symbol_table_baset &symbol_table,
719  const source_locationt &loc,
720  code_blockt &code)
721 {
722  symbolt &return_sym = get_fresh_aux_symbol(
723  java_int_type(),
724  "return_array",
725  "return_array",
726  loc,
727  ID_java,
728  symbol_table);
729  const exprt return_expr = return_sym.symbol_expr();
730  code.add(code_declt(return_expr), loc);
731  code.add(
733  return_expr,
734  ID_cprover_associate_length_to_array_func,
735  {array, length},
736  symbol_table),
737  loc);
738 }
739 
751  const exprt &pointer,
752  const exprt &length,
753  const irep_idt &char_set,
754  symbol_table_baset &symbol_table,
755  const source_locationt &loc,
756  code_blockt &code)
757 {
758  PRECONDITION(pointer.type().id() == ID_pointer);
759  symbolt &return_sym = get_fresh_aux_symbol(
760  java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
761  const exprt return_expr = return_sym.symbol_expr();
762  code.add(code_declt(return_expr), loc);
763  const constant_exprt char_set_expr(char_set, string_typet());
764  code.add(
766  return_expr,
767  ID_cprover_string_constrain_characters_func,
768  {length, pointer, char_set_expr},
769  symbol_table),
770  loc);
771 }
772 
790  const irep_idt &function_name,
791  const exprt::operandst &arguments,
792  const source_locationt &loc,
793  symbol_table_baset &symbol_table,
794  code_blockt &code)
795 {
796  // int return_code;
797  symbolt return_code_sym = get_fresh_aux_symbol(
798  java_int_type(),
799  std::string("return_code_") + function_name.c_str(),
800  std::string("return_code_") + function_name.c_str(),
801  loc,
802  ID_java,
803  symbol_table);
804  const exprt return_code = return_code_sym.symbol_expr();
805  code.add(code_declt(return_code), loc);
806 
807  const refined_string_exprt string_expr =
808  make_nondet_string_expr(loc, function_name, symbol_table, code);
809 
810  // args is { str.length, str.content, arguments... }
811  exprt::operandst args;
812  args.push_back(string_expr.length());
813  args.push_back(string_expr.content());
814  args.insert(args.end(), arguments.begin(), arguments.end());
815 
816  // return_code = <function_name>_data(args)
817  code.add(
819  return_code, function_name, args, symbol_table),
820  loc);
821 
822  return string_expr;
823 }
824 
835  const exprt &lhs,
836  const exprt &rhs_array,
837  const exprt &rhs_length,
838  const symbol_table_baset &symbol_table)
839 {
842 
843  // A String has a field Object with @clsid = String and @lock = false:
844  const symbolt &jlo_symbol=*symbol_table.lookup("java::java.lang.Object");
845  const struct_typet &jlo_struct=to_struct_type(jlo_symbol.type);
846  struct_exprt jlo_init(jlo_struct);
847  irep_idt clsid = get_tag(lhs.type().subtype());
848  java_root_class_init(jlo_init, jlo_struct, false, clsid);
849 
850  struct_exprt struct_rhs(deref.type());
851  struct_rhs.copy_to_operands(jlo_init);
852  struct_rhs.copy_to_operands(rhs_length);
853  struct_rhs.copy_to_operands(rhs_array);
854  return code_assignt(
855  checked_dereference(lhs, lhs.type().subtype()), struct_rhs);
856 }
857 
867  const exprt &lhs,
868  const refined_string_exprt &rhs,
869  const symbol_table_baset &symbol_table)
870 {
872  lhs, rhs.content(), rhs.length(), symbol_table);
873 }
874 
885  const refined_string_exprt &lhs,
886  const exprt &rhs,
887  const source_locationt &loc,
888  const symbol_table_baset &symbol_table,
889  code_blockt &code)
890 {
892 
893  typet deref_type;
894  if(rhs.type().subtype().id()==ID_symbol)
895  deref_type=symbol_table.lookup_ref(
896  to_symbol_type(rhs.type().subtype()).get_identifier()).type;
897  else
898  deref_type=rhs.type().subtype();
899 
900  const dereference_exprt deref = checked_dereference(rhs, deref_type);
901 
902  // Although we should not reach this code if rhs is null, the association
903  // `pointer -> length` is added to the solver anyway, so we have to make sure
904  // the length is set to something reasonable.
905  auto rhs_length = if_exprt(
907  from_integer(0, lhs.length().type()),
908  get_length(deref, symbol_table));
909  rhs_length.set(ID_mode, ID_java);
910 
911  // Assignments
912  code.add(code_assignt(lhs.length(), rhs_length), loc);
913  const exprt data_as_array = get_data(deref, symbol_table);
914  code.add(code_assignt(lhs.content(), data_as_array), loc);
915 }
916 
929  const std::string &s,
930  const source_locationt &loc,
931  symbol_table_baset &symbol_table,
932  code_blockt &code)
933 {
934  const constant_exprt expr(s, string_typet());
936  ID_cprover_string_literal_func, {expr}, loc, symbol_table, code);
937 }
938 
955  const code_typet &type,
956  const source_locationt &loc,
957  const irep_idt &function_id,
958  symbol_table_baset &symbol_table)
959 {
960  const typet &return_type = type.return_type();
961  exprt::operandst ops;
962  for(const auto &p : type.parameters())
963  {
964  symbol_exprt sym(p.get_identifier(), p.type());
965  ops.push_back(sym);
966  }
967 
968  code_ifthenelset code;
969  code.cond() = [&] {
970  const member_exprt class_identifier(
971  checked_dereference(ops[1], ops[1].type().subtype()),
972  "@class_identifier",
973  string_typet());
974  return equal_exprt(
975  class_identifier,
976  constant_exprt("java::java.lang.String", string_typet()));
977  }();
978 
979  code.then_case() = [&] {
980  code_blockt instance_case;
981  // Check content equality
982  const symbolt string_equals_sym = get_fresh_aux_symbol(
983  return_type, "string_equals", "str_eq", loc, ID_java, symbol_table);
984  const symbol_exprt string_equals = string_equals_sym.symbol_expr();
985  instance_case.add(code_declt(string_equals), loc);
986  const exprt::operandst args =
987  process_equals_function_operands(ops, loc, symbol_table, instance_case);
988  const auto fun_app = make_function_application(
989  ID_cprover_string_equal_func, args, return_type, symbol_table);
990  instance_case.add(code_assignt(string_equals, fun_app), loc);
991  instance_case.add(code_returnt(string_equals), loc);
992  return instance_case;
993  }();
994 
995  code.else_case() = code_returnt(from_integer(false, return_type));
996  return code;
997 }
998 
1005  const code_typet &type,
1006  const source_locationt &loc,
1007  const irep_idt &function_id,
1008  symbol_table_baset &symbol_table)
1009 {
1010  // Getting the argument
1011  code_typet::parameterst params=type.parameters();
1012  PRECONDITION(params.size()==1);
1013  const symbol_exprt arg(params[0].get_identifier(), params[0].type());
1014 
1015  // Holder for output code
1016  code_blockt code;
1017 
1018  // Declaring and allocating String * str
1020  type.return_type(), loc, function_id, symbol_table, code);
1021 
1022  // Expression representing 0.0
1023  ieee_float_spect float_spec(to_floatbv_type(params[0].type()));
1024  ieee_floatt zero_float(float_spec);
1025  zero_float.from_float(0.0);
1026  constant_exprt zero=zero_float.to_expr();
1027 
1028  // For each possible case with have a condition and a string_exprt
1029  std::vector<exprt> condition_list;
1030  std::vector<refined_string_exprt> string_expr_list;
1031 
1032  // Case of computerized scientific notation
1033  condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
1035  ID_cprover_string_of_float_scientific_notation_func,
1036  {arg},
1037  loc,
1038  symbol_table,
1039  code);
1040  string_expr_list.push_back(sci_notation);
1041 
1042  // Subcase of negative scientific notation
1043  condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
1044  refined_string_exprt minus_sign =
1045  string_literal_to_string_expr("-", loc, symbol_table, code);
1046  refined_string_exprt neg_sci_notation = string_expr_of_function(
1047  ID_cprover_string_concat_func,
1048  {minus_sign, sci_notation},
1049  loc,
1050  symbol_table,
1051  code);
1052  string_expr_list.push_back(neg_sci_notation);
1053 
1054  // Case of NaN
1055  condition_list.push_back(isnan_exprt(arg));
1056  refined_string_exprt nan =
1057  string_literal_to_string_expr("NaN", loc, symbol_table, code);
1058  string_expr_list.push_back(nan);
1059 
1060  // Case of Infinity
1061  extractbit_exprt is_neg(arg, float_spec.width()-1);
1062  condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
1063  refined_string_exprt infinity =
1064  string_literal_to_string_expr("Infinity", loc, symbol_table, code);
1065  string_expr_list.push_back(infinity);
1066 
1067  // Case -Infinity
1068  condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
1069  refined_string_exprt minus_infinity =
1070  string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
1071  string_expr_list.push_back(minus_infinity);
1072 
1073  // Case of simple notation
1074  ieee_floatt bound_inf_float(float_spec);
1075  ieee_floatt bound_sup_float(float_spec);
1076  bound_inf_float.from_float(1e-3f);
1077  bound_sup_float.from_float(1e7f);
1078  bound_inf_float.change_spec(float_spec);
1079  bound_sup_float.change_spec(float_spec);
1080  constant_exprt bound_inf=bound_inf_float.to_expr();
1081  constant_exprt bound_sup=bound_sup_float.to_expr();
1082 
1083  and_exprt is_simple_float(
1084  binary_relation_exprt(arg, ID_ge, bound_inf),
1085  binary_relation_exprt(arg, ID_lt, bound_sup));
1086  condition_list.push_back(is_simple_float);
1087 
1089  ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1090  string_expr_list.push_back(simple_notation);
1091 
1092  // Case of a negative number in simple notation
1093  and_exprt is_neg_simple_float(
1094  binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
1095  binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup)));
1096  condition_list.push_back(is_neg_simple_float);
1097 
1098  refined_string_exprt neg_simple_notation = string_expr_of_function(
1099  ID_cprover_string_concat_func,
1100  {minus_sign, simple_notation},
1101  loc,
1102  symbol_table,
1103  code);
1104  string_expr_list.push_back(neg_simple_notation);
1105 
1106  // Combining all cases
1107  INVARIANT(
1108  string_expr_list.size()==condition_list.size(),
1109  "number of created strings should correspond to number of conditions");
1110 
1111  // We do not check the condition of the first element in the list as it
1112  // will be reached only if all other conditions are not satisfied.
1114  str, string_expr_list[0], symbol_table);
1115  for(std::size_t i=1; i<condition_list.size(); i++)
1116  {
1117  code_ifthenelset ife;
1118  ife.cond()=condition_list[i];
1120  str, string_expr_list[i], symbol_table);
1121  ife.else_case()=tmp_code;
1122  tmp_code=ife;
1123  }
1124  code.add(tmp_code, loc);
1125 
1126  // Return str
1127  code.add(code_returnt(str), loc);
1128  return code;
1129 }
1130 
1148  const irep_idt &function_name,
1149  const code_typet &type,
1150  const source_locationt &loc,
1151  symbol_table_baset &symbol_table,
1152  bool ignore_first_arg)
1153 {
1154  code_typet::parameterst params=type.parameters();
1155 
1156  // The first parameter is the object to be initialized
1157  PRECONDITION(!params.empty());
1158  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1159  if(ignore_first_arg)
1160  params.erase(params.begin());
1161 
1162  // Holder for output code
1163  code_blockt code;
1164 
1165  // Processing parameters
1166  exprt::operandst args=process_parameters(params, loc, symbol_table, code);
1167 
1168  // string_expr <- function(arg1)
1169  refined_string_exprt string_expr =
1170  string_expr_of_function(function_name, args, loc, symbol_table, code);
1171 
1172  // arg_this <- string_expr
1173  code.add(
1174  code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1175  loc);
1176 
1177  return code;
1178 }
1179 
1189  const irep_idt &function_name,
1190  const code_typet &type,
1191  const source_locationt &loc,
1192  symbol_table_baset &symbol_table)
1193 {
1194  // This is similar to assign functions except we return a pointer to `this`
1195  code_typet::parameterst params=type.parameters();
1196  PRECONDITION(!params.empty());
1197  code_blockt code;
1198  code.add(
1199  make_assign_function_from_call(function_name, type, loc, symbol_table),
1200  loc);
1201  const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1202  code.add(code_returnt(arg_this), loc);
1203  return code;
1204 }
1205 
1214  const irep_idt &function_name,
1215  const code_typet &type,
1216  const source_locationt &loc,
1217  symbol_table_baset &symbol_table)
1218 {
1219  // This is similar to initialization function except we do not ignore
1220  // the first argument
1222  function_name, type, loc, symbol_table, false);
1223  return code;
1224 }
1225 
1246  const exprt &object,
1247  irep_idt type_name,
1248  const source_locationt &loc,
1249  symbol_table_baset &symbol_table,
1250  code_blockt &code)
1251 {
1252  optionalt<symbol_typet> object_type;
1253 
1254  typet value_type;
1255  if(type_name==ID_boolean)
1256  {
1257  value_type=java_boolean_type();
1258  object_type=symbol_typet("java::java.lang.Boolean");
1259  }
1260  else if(type_name==ID_char)
1261  {
1262  value_type=java_char_type();
1263  object_type=symbol_typet("java::java.lang.Character");
1264  }
1265  else if(type_name==ID_byte)
1266  {
1267  value_type=java_byte_type();
1268  object_type=symbol_typet("java::java.lang.Byte");
1269  }
1270  else if(type_name==ID_short)
1271  {
1272  value_type=java_short_type();
1273  object_type=symbol_typet("java::java.lang.Short");
1274  }
1275  else if(type_name==ID_int)
1276  {
1277  value_type=java_int_type();
1278  object_type=symbol_typet("java::java.lang.Integer");
1279  }
1280  else if(type_name==ID_long)
1281  {
1282  value_type=java_long_type();
1283  object_type=symbol_typet("java::java.lang.Long");
1284  }
1285  else if(type_name==ID_float)
1286  {
1287  value_type=java_float_type();
1288  object_type=symbol_typet("java::java.lang.Float");
1289  }
1290  else if(type_name==ID_double)
1291  {
1292  value_type=java_double_type();
1293  object_type=symbol_typet("java::java.lang.Double");
1294  }
1295  else if(type_name==ID_void)
1296  return nil_exprt();
1297  else
1298  UNREACHABLE;
1299 
1300  DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");
1301 
1302  // declare tmp_type_name to hold the value
1303  std::string aux_name="tmp_"+id2string(type_name);
1305  value_type, aux_name, aux_name, loc, ID_java, symbol_table);
1306  exprt value=symbol.symbol_expr();
1307 
1308  // Check that the type of the object is in the symbol table,
1309  // otherwise there is no safe way of finding its value.
1310  if(
1311  const auto maybe_symbol =
1312  symbol_table.lookup(object_type->get_identifier()))
1313  {
1314  struct_typet struct_type=to_struct_type(maybe_symbol->type);
1315  // Check that the type has a value field
1316  const struct_union_typet::componentt value_comp=
1317  struct_type.get_component("value");
1318  if(!value_comp.is_nil())
1319  {
1321  dereference_exprt deref(
1323  member_exprt deref_value(deref, value_comp.get_name(), value_comp.type());
1324  code.add(code_assignt(value, deref_value), loc);
1325  return value;
1326  }
1327  }
1328 
1329  warning() << object_type->get_identifier()
1330  << " not available to format function" << eom;
1331  code.add(code_declt(value), loc);
1332  return value;
1333 }
1334 
1344  const exprt &argv,
1345  int index)
1346 {
1347  dereference_exprt deref_objs(argv, argv.type().subtype());
1348  pointer_typet empty_pointer=pointer_type(empty_typet());
1349  pointer_typet pointer_of_pointer=pointer_type(empty_pointer);
1350  member_exprt data_member(deref_objs, "data", pointer_of_pointer);
1351  plus_exprt data_pointer_plus_index(
1352  data_member, from_integer(index, java_int_type()), data_member.type());
1353  dereference_exprt data_at_index(
1354  data_pointer_plus_index, data_pointer_plus_index.type().subtype());
1355  return data_at_index;
1356 }
1357 
1392  const exprt &argv,
1393  int index,
1394  const struct_typet &structured_type,
1395  const source_locationt &loc,
1396  const irep_idt &function_id,
1397  symbol_table_baset &symbol_table,
1398  code_blockt &code)
1399 {
1400  // Declarations of the fields of arg_i_struct
1401  // arg_i_struct is { arg_i_string_expr, tmp_int, tmp_char, ... }
1402  struct_exprt arg_i_struct(structured_type);
1403  std::list<exprt> field_exprs;
1404  for(const auto & comp : structured_type.components())
1405  {
1406  const irep_idt &name=comp.get_name();
1407  const typet &type=comp.type();
1408  exprt field_expr;
1409  if(name!="string_expr")
1410  {
1411  std::string tmp_name="tmp_"+id2string(name);
1412  symbolt field_symbol = get_fresh_aux_symbol(
1413  type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
1414  field_expr=field_symbol.symbol_expr();
1415  code.add(code_declt(field_expr), loc);
1416  }
1417  else
1418  field_expr =
1419  make_nondet_string_expr(loc, function_id, symbol_table, code);
1420 
1421  field_exprs.push_back(field_expr);
1422  arg_i_struct.copy_to_operands(field_expr);
1423  }
1424 
1425  // arg_i = argv[index]
1426  exprt obj=get_object_at_index(argv, index);
1427  symbolt object_symbol = get_fresh_aux_symbol(
1428  obj.type(),
1429  id2string(function_id),
1430  "tmp_format_obj",
1431  loc,
1432  ID_java,
1433  symbol_table);
1434  symbol_exprt arg_i=object_symbol.symbol_expr();
1436  arg_i, symbol_table, loc, function_id, code);
1437  code.add(code_assignt(arg_i, obj), loc);
1438  code.add(
1439  code_assumet(
1440  not_exprt(
1441  equal_exprt(arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))),
1442  loc);
1443 
1444  // if arg_i != null then [code_not_null]
1445  code_ifthenelset code_avoid_null_arg;
1446  code_avoid_null_arg.cond()=not_exprt(equal_exprt(
1447  arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))));
1448  code_blockt code_not_null;
1449 
1450  // Assigning all the fields of arg_i_struct
1451  for(const auto &comp : structured_type.components())
1452  {
1453  const irep_idt &name=comp.get_name();
1454  exprt field_expr=field_exprs.front();
1455  field_exprs.pop_front();
1456 
1457  if(name=="string_expr")
1458  {
1459  pointer_typet string_pointer=
1460  java_reference_type(symbol_typet("java::java.lang.String"));
1461  typecast_exprt arg_i_as_string(arg_i, string_pointer);
1463  to_string_expr(field_expr),
1464  arg_i_as_string,
1465  loc,
1466  symbol_table,
1467  code_not_null);
1468  }
1469  else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
1470  {
1472  arg_i, name, loc, symbol_table, code_not_null);
1473  code_not_null.add(code_assignt(field_expr, value), loc);
1474  }
1475  else
1476  {
1477  // TODO: date_time and hash_code not implemented
1478  }
1479  }
1480 
1481  code.add(code_not_null, loc);
1482  return arg_i_struct;
1483 }
1484 
1497  const code_typet &type,
1498  const source_locationt &loc,
1499  const irep_idt &function_id,
1500  symbol_table_baset &symbol_table)
1501 {
1502  PRECONDITION(type.parameters().size()==2);
1503  code_blockt code;
1505  type.parameters(), loc, symbol_table, code);
1506  INVARIANT(args.size()==2, "String.format should have two arguments");
1507 
1508  // The argument can be:
1509  // a string, an integer, a floating point, a character, a boolean,
1510  // an object of which we take the hash code, or a date/time
1511  struct_typet structured_type;
1512  structured_type.components().emplace_back("string_expr", refined_string_type);
1513  structured_type.components().emplace_back(ID_int, java_int_type());
1514  structured_type.components().emplace_back(ID_float, java_float_type());
1515  structured_type.components().emplace_back(ID_char, java_char_type());
1516  structured_type.components().emplace_back(ID_boolean, java_boolean_type());
1517  // TODO: hash_code not implemented for now
1518  structured_type.components().emplace_back("hashcode", java_int_type());
1519  // TODO: date_time type not implemented for now
1520  structured_type.components().emplace_back("date_time", java_int_type());
1521 
1522  // We will process arguments so that each is converted to a `struct_exprt`
1523  // containing each possible type used in format specifiers.
1524  std::vector<exprt> processed_args;
1525  processed_args.push_back(args[0]);
1526  for(std::size_t i=0; i<MAX_FORMAT_ARGS; ++i)
1527  processed_args.push_back(
1529  args[1], i, structured_type, loc, function_id, symbol_table, code));
1530 
1532  ID_cprover_string_format_func, processed_args, loc, symbol_table, code);
1533  exprt java_string = allocate_fresh_string(
1534  type.return_type(), loc, function_id, symbol_table, code);
1535  code.add(
1537  java_string, string_expr, symbol_table),
1538  loc);
1539  code.add(code_returnt(java_string), loc);
1540  return code;
1541 }
1542 
1556  const code_typet &type,
1557  const source_locationt &loc,
1558  const irep_idt &function_id,
1559  symbol_table_baset &symbol_table)
1560 {
1561  code_typet::parameterst params=type.parameters();
1562  const symbol_exprt this_obj(params[0].get_identifier(), params[0].type());
1563 
1564  // Code to be returned
1565  code_blockt code;
1566 
1567  // > Class class1;
1568  pointer_typet class_type=
1570  symbol_table.lookup_ref("java::java.lang.Class").type);
1571  symbolt class1_sym=get_fresh_aux_symbol(
1572  class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
1573  symbol_exprt class1=class1_sym.symbol_expr();
1574  code.add(code_declt(class1), loc);
1575 
1576  // class_identifier is this->@class_identifier
1577  member_exprt class_identifier(
1578  checked_dereference(this_obj, this_obj.type().subtype()),
1579  "@class_identifier",
1580  string_typet());
1581 
1582  // string_expr = cprover_string_literal(this->@class_identifier)
1584  ID_cprover_string_literal_func,
1585  {class_identifier},
1586  loc,
1587  symbol_table,
1588  code);
1589 
1590  // string_expr1 = substr(string_expr, 6)
1591  // We do this to remove the "java::" prefix
1593  ID_cprover_string_substring_func,
1594  {string_expr, from_integer(6, java_int_type())},
1595  loc,
1596  symbol_table,
1597  code);
1598 
1599  // string1 = (String*) string_expr
1600  pointer_typet string_ptr_type=java_reference_type(
1601  symbol_table.lookup_ref("java::java.lang.String").type);
1602  exprt string1 = allocate_fresh_string(
1603  string_ptr_type, loc, function_id, symbol_table, code);
1604  code.add(
1605  code_assign_string_expr_to_java_string(string1, string_expr1, symbol_table),
1606  loc);
1607 
1608  // > class1 = Class.forName(string1)
1609  code_function_callt fun_call;
1610  fun_call.function()=symbol_exprt(
1611  "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
1612  fun_call.lhs()=class1;
1613  fun_call.arguments().push_back(string1);
1614  const code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type);
1615  fun_call.function().type()=fun_type;
1616  code.add(fun_call, loc);
1617 
1618  // > return class1;
1619  code.add(code_returnt(class1), loc);
1620  return code;
1621 }
1622 
1634  const irep_idt &function_name,
1635  const code_typet &type,
1636  const source_locationt &loc,
1637  symbol_table_baset &symbol_table)
1638 {
1639  code_blockt code;
1641  type.parameters(), loc, symbol_table, code);
1642  code.add(
1644  function_name, args, type.return_type(), symbol_table),
1645  loc);
1646  return code;
1647 }
1648 
1663  const irep_idt &function_name,
1664  const code_typet &type,
1665  const source_locationt &loc,
1666  symbol_table_baset &symbol_table)
1667 {
1668  // Code for the output
1669  code_blockt code;
1670 
1671  // Calling the function
1673  type.parameters(), loc, symbol_table, code);
1674 
1675  // String expression that will hold the result
1676  refined_string_exprt string_expr =
1677  string_expr_of_function(function_name, arguments, loc, symbol_table, code);
1678 
1679  // Assign to string
1681  type.return_type(), loc, function_name, symbol_table, code);
1682  code.add(
1683  code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
1684  loc);
1685 
1686  // Return value
1687  code.add(code_returnt(str), loc);
1688  return code;
1689 }
1690 
1705  const code_typet &type,
1706  const source_locationt &loc,
1707  const irep_idt &function_id,
1708  symbol_table_baset &symbol_table)
1709 {
1710  // Code for the output
1711  code_blockt code;
1712 
1713  // String expression that will hold the result
1714  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
1715 
1716  // Assign the argument to string_expr
1717  code_typet::parametert op=type.parameters()[0];
1718  symbol_exprt arg0(op.get_identifier(), op.type());
1720  string_expr, arg0, loc, symbol_table, code);
1721 
1722  // Allocate and assign the string
1724  type.return_type(), loc, function_id, symbol_table, code);
1725  code.add(
1726  code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
1727  loc);
1728 
1729  // Return value
1730  code.add(code_returnt(str), loc);
1731  return code;
1732 }
1733 
1746  const code_typet &type,
1747  const source_locationt &loc,
1748  const irep_idt &function_id,
1749  symbol_table_baset &symbol_table)
1750 {
1751  // Code for the output
1752  code_blockt code;
1753 
1754  // String expression that will hold the result
1755  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
1756 
1757  // Assign argument to a string_expr
1758  code_typet::parameterst params=type.parameters();
1759  symbol_exprt arg1(params[1].get_identifier(), params[1].type());
1761  string_expr, arg1, loc, symbol_table, code);
1762 
1763  // Assign string_expr to `this` object
1764  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1765  code.add(
1766  code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1767  loc);
1768 
1769  return code;
1770 }
1771 
1781  const code_typet &type,
1782  const source_locationt &loc,
1783  const irep_idt &function_id,
1784  symbol_table_baset &symbol_table)
1785 {
1786  // Code for the output
1787  code_blockt code;
1788 
1789  code_typet::parameterst params = type.parameters();
1790  PRECONDITION(params.size() == 4);
1791  exprt::operandst args =
1792  process_parameters(type.parameters(), loc, symbol_table, code);
1793  INVARIANT(
1794  args.size() == 4, "process_parameters preserves number of arguments");
1795 
1798  refined_string_exprt string_arg = to_string_expr(args[1]);
1799 
1800  // The third argument is `count`, whereas the third argument of substring
1801  // is `end` which corresponds to `offset+count`
1803  ID_cprover_string_substring_func,
1804  {args[1], args[2], plus_exprt(args[2], args[3])},
1805  loc,
1806  symbol_table,
1807  code);
1808 
1809  // Assign string_expr to `this` object
1810  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1811  code.add(
1812  code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1813  loc);
1814 
1815  return code;
1816 }
1817 
1829  const code_typet &type,
1830  const source_locationt &loc,
1831  const irep_idt &function_id,
1832  symbol_table_baset &symbol_table)
1833 {
1834  code_typet::parameterst params=type.parameters();
1835  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1836  dereference_exprt deref=
1837  checked_dereference(arg_this, arg_this.type().subtype());
1838  return code_returnt(get_length(deref, symbol_table));
1839 }
1840 
1842  const irep_idt &function_id) const
1843 {
1844  for(const id_mapt *map : id_maps)
1845  if(map->count(function_id) != 0)
1846  return true;
1847 
1848  return conversion_table.count(function_id) != 0;
1849 }
1850 
1851 template <typename TMap, typename TContainer>
1852 void add_keys_to_container(const TMap &map, TContainer &container)
1853 {
1854  static_assert(
1855  std::is_same<typename TMap::key_type,
1856  typename TContainer::value_type>::value,
1857  "TContainer value_type doesn't match TMap key_type");
1858  std::transform(
1859  map.begin(),
1860  map.end(),
1861  std::inserter(container, container.begin()),
1862  [](const typename TMap::value_type &pair) { return pair.first; });
1863 }
1864 
1866  std::unordered_set<irep_idt> &methods) const
1867 {
1868  for(const id_mapt *map : id_maps)
1869  add_keys_to_container(*map, methods);
1870 
1872 }
1873 
1883  const symbolt &symbol,
1884  symbol_table_baset &symbol_table)
1885 {
1886  const irep_idt &function_id = symbol.name;
1887  const code_typet &type = to_code_type(symbol.type);
1888  const source_locationt &loc = symbol.location;
1889  auto it_id=cprover_equivalent_to_java_function.find(function_id);
1890  if(it_id!=cprover_equivalent_to_java_function.end())
1891  return make_function_from_call(it_id->second, type, loc, symbol_table);
1892 
1896  it_id->second, type, loc, symbol_table);
1897 
1898  it_id=cprover_equivalent_to_java_constructor.find(function_id);
1901  it_id->second, type, loc, symbol_table);
1902 
1906  it_id->second, type, loc, symbol_table);
1907 
1908  it_id=cprover_equivalent_to_java_assign_function.find(function_id);
1911  it_id->second, type, loc, symbol_table);
1912 
1913  auto it=conversion_table.find(function_id);
1914  if(it!=conversion_table.end())
1915  return it->second(type, loc, function_id, symbol_table);
1916 
1917  return nil_exprt();
1918 }
1919 
1925  irep_idt class_name)
1926 {
1927  return string_types.find(class_name)!=string_types.end();
1928 }
1929 
1931 {
1932  string_types = std::unordered_set<irep_idt>{"java.lang.String",
1933  "java.lang.StringBuilder",
1934  "java.lang.CharSequence",
1935  "java.lang.StringBuffer"};
1936 }
1937 
1940 {
1942 
1943  // The following list of function is organized by libraries, with
1944  // constructors first and then methods in alphabetic order.
1945  // Methods that are not supported here should ultimately have Java models
1946  // provided for them in the class-path.
1947 
1948  // String library
1949  conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
1950  std::bind(
1952  this,
1953  std::placeholders::_1,
1954  std::placeholders::_2,
1955  std::placeholders::_3,
1956  std::placeholders::_4);
1958  ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1960  this,
1961  std::placeholders::_1,
1962  std::placeholders::_2,
1963  std::placeholders::_3,
1964  std::placeholders::_4);
1965  conversion_table["java::java.lang.String.<init>:([CII)V"] = std::bind(
1967  this,
1968  std::placeholders::_1,
1969  std::placeholders::_2,
1970  std::placeholders::_3,
1971  std::placeholders::_4);
1973  ["java::java.lang.String.<init>:()V"]=
1974  ID_cprover_string_empty_string_func;
1975 
1976  // CProverString.charAt differs from the Java String.charAt in that no
1977  // exception is raised for the out of bounds case.
1979  ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
1980  ID_cprover_string_char_at_func;
1982  ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1983  ID_cprover_string_code_point_at_func;
1985  ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1986  ID_cprover_string_code_point_before_func;
1988  ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1989  ID_cprover_string_code_point_count_func;
1991  ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1992  ID_cprover_string_compare_to_func;
1994  ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1995  ID_cprover_string_concat_func;
1997  ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1998  ID_cprover_string_contains_func;
2000  ["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
2001  ID_cprover_string_copy_func;
2003  ["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
2004  ID_cprover_string_copy_func;
2006  ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
2007  ID_cprover_string_endswith_func;
2008 
2009  conversion_table["java::java.lang.String.equals:(Ljava/lang/Object;)Z"] =
2010  std::bind(
2012  this,
2013  std::placeholders::_1,
2014  std::placeholders::_2,
2015  std::placeholders::_3,
2016  std::placeholders::_4);
2018  ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
2019  ID_cprover_string_equals_ignore_case_func;
2021  ["java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)"
2022  "Ljava/lang/String;"] =
2023  std::bind(
2025  this,
2026  std::placeholders::_1,
2027  std::placeholders::_2,
2028  std::placeholders::_3,
2029  std::placeholders::_4);
2031  ["java::java.lang.String.hashCode:()I"]=
2032  ID_cprover_string_hash_code_func;
2034  ["java::java.lang.String.indexOf:(I)I"]=
2035  ID_cprover_string_index_of_func;
2037  ["java::java.lang.String.indexOf:(II)I"]=
2038  ID_cprover_string_index_of_func;
2040  ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
2041  ID_cprover_string_index_of_func;
2043  ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
2044  ID_cprover_string_index_of_func;
2046  ["java::java.lang.String.intern:()Ljava/lang/String;"]=
2047  ID_cprover_string_intern_func;
2049  ["java::java.lang.String.isEmpty:()Z"]=
2050  ID_cprover_string_is_empty_func;
2052  ["java::java.lang.String.lastIndexOf:(I)I"]=
2053  ID_cprover_string_last_index_of_func;
2055  ["java::java.lang.String.lastIndexOf:(II)I"]=
2056  ID_cprover_string_last_index_of_func;
2058  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
2059  ID_cprover_string_last_index_of_func;
2061  ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
2062  ID_cprover_string_last_index_of_func;
2063  conversion_table["java::java.lang.String.length:()I"] = std::bind(
2065  this,
2066  std::placeholders::_1,
2067  std::placeholders::_2,
2068  std::placeholders::_3,
2069  std::placeholders::_4);
2071  ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
2072  "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
2074  ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
2075  ID_cprover_string_replace_func;
2077  ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
2078  ID_cprover_string_replace_func;
2080  ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
2081  ID_cprover_string_startswith_func;
2083  ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
2084  ID_cprover_string_startswith_func;
2086  ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
2087  "lang/CharSequence;"] = ID_cprover_string_substring_func;
2088  // CProverString.substring differs from the Java String.substring in that no
2089  // exception is raised for the out of bounds case.
2091  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
2092  "Ljava/lang/String;"]=
2093  ID_cprover_string_substring_func;
2095  ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
2096  "Ljava/lang/String;"]=
2097  ID_cprover_string_substring_func;
2099  ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
2100  ID_cprover_string_to_lower_case_func;
2101  conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
2102  std::bind(
2104  this,
2105  std::placeholders::_1,
2106  std::placeholders::_2,
2107  std::placeholders::_3,
2108  std::placeholders::_4);
2110  ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
2111  ID_cprover_string_to_upper_case_func;
2113  ["java::java.lang.String.trim:()Ljava/lang/String;"]=
2114  ID_cprover_string_trim_func;
2116  ["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
2117  ID_cprover_string_of_bool_func;
2119  ["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
2120  ID_cprover_string_of_char_func;
2121  conversion_table["java::java.lang.String.valueOf:(D)Ljava/lang/String;"] =
2122  std::bind(
2124  this,
2125  std::placeholders::_1,
2126  std::placeholders::_2,
2127  std::placeholders::_3,
2128  std::placeholders::_4);
2129  conversion_table["java::java.lang.String.valueOf:(F)Ljava/lang/String;"] =
2130  std::bind(
2132  this,
2133  std::placeholders::_1,
2134  std::placeholders::_2,
2135  std::placeholders::_3,
2136  std::placeholders::_4);
2138  ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
2139  ID_cprover_string_of_int_func;
2141  ["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
2142  ID_cprover_string_of_long_func;
2143 
2144  // StringBuilder library
2146  ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
2148  this,
2149  std::placeholders::_1,
2150  std::placeholders::_2,
2151  std::placeholders::_3,
2152  std::placeholders::_4);
2154  ["java::java.lang.StringBuilder.<init>:()V"]=
2155  ID_cprover_string_empty_string_func;
2156 
2158  ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
2159  ID_cprover_string_concat_char_func;
2161  ["java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] =
2162  ID_cprover_string_concat_func;
2164  ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
2165  ID_cprover_string_concat_double_func;
2167  ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
2168  "lang/CharSequence;II)"
2169  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2171  ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
2172  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2174  ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
2175  "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2177  ["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]=
2178  ID_cprover_string_concat_bool_func;
2180  ["java::java.lang.StringBuilder.appendCodePoint:(I)"
2181  "Ljava/lang/StringBuilder;"]=
2182  ID_cprover_string_concat_code_point_func;
2184  ["java::java.lang.StringBuilder.charAt:(I)C"]=
2185  ID_cprover_string_char_at_func;
2187  ["java::java.lang.StringBuilder.codePointAt:(I)I"]=
2188  ID_cprover_string_code_point_at_func;
2190  ["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
2191  ID_cprover_string_code_point_before_func;
2193  ["java::java.lang.StringBuilder.codePointCount:(II)I"]=
2194  ID_cprover_string_code_point_count_func;
2196  ["java::org.cprover.CProverString.delete:(Ljava/lang/"
2197  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2198  ID_cprover_string_delete_func;
2200  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
2201  "StringBuilder;I)Ljava/lang/StringBuilder;"] =
2202  ID_cprover_string_delete_char_at_func;
2204  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2205  "StringBuilder;IC)Ljava/lang/StringBuilder;"] =
2206  ID_cprover_string_insert_char_func;
2208  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2209  "StringBuilder;IZ)Ljava/lang/StringBuilder;"] =
2210  ID_cprover_string_insert_bool_func;
2212  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2213  "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2214  ID_cprover_string_insert_int_func;
2216  ["java::org.cprover.CProverString.insert:(Ljava/lang/"
2217  "StringBuilder;IJ)Ljava/lang/StringBuilder;"] =
2218  ID_cprover_string_insert_long_func;
2220  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
2221  "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
2222  conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
2224  this,
2225  std::placeholders::_1,
2226  std::placeholders::_2,
2227  std::placeholders::_3,
2228  std::placeholders::_4);
2230  ["java::java.lang.StringBuilder.setCharAt:(IC)V"]=
2231  ID_cprover_string_char_set_func;
2233  ["java::java.lang.StringBuilder.setLength:(I)V"]=
2234  ID_cprover_string_set_length_func;
2236  ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
2237  ID_cprover_string_substring_func;
2239  ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
2240  ID_cprover_string_substring_func;
2242  ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
2244  this,
2245  std::placeholders::_1,
2246  std::placeholders::_2,
2247  std::placeholders::_3,
2248  std::placeholders::_4);
2249 
2250  // StringBuffer library
2252  ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
2254  this,
2255  std::placeholders::_1,
2256  std::placeholders::_2,
2257  std::placeholders::_3,
2258  std::placeholders::_4);
2260  ["java::java.lang.StringBuffer.<init>:()V"]=
2261  ID_cprover_string_empty_string_func;
2262 
2264  ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
2265  ID_cprover_string_concat_char_func;
2267  ["java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]=
2268  ID_cprover_string_concat_double_func;
2270  ["java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]=
2271  ID_cprover_string_concat_float_func;
2273  ["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]=
2274  ID_cprover_string_concat_int_func;
2276  ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
2277  ID_cprover_string_concat_long_func;
2279  ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
2280  "Ljava/lang/StringBuffer;"]=
2281  ID_cprover_string_concat_func;
2283  ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
2284  "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
2286  ["java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"] =
2287  ID_cprover_string_concat_bool_func;
2289  ["java::java.lang.StringBuffer.appendCodePoint:(I)"
2290  "Ljava/lang/StringBuffer;"]=
2291  ID_cprover_string_concat_code_point_func;
2293  ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
2294  ID_cprover_string_char_at_func;
2296  ["java::java.lang.StringBuffer.codePointAt:(I)I"]=
2297  ID_cprover_string_code_point_at_func;
2299  ["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
2300  ID_cprover_string_code_point_before_func;
2302  ["java::java.lang.StringBuffer.codePointCount:(II)I"]=
2303  ID_cprover_string_code_point_count_func;
2305  ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
2306  "lang/StringBuffer;"] = ID_cprover_string_delete_func;
2308  ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
2309  "StringBufferI)Ljava/lang/StringBuffer;"] =
2310  ID_cprover_string_delete_char_at_func;
2312  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/"
2313  "lang/StringBuffer;"] = ID_cprover_string_insert_char_func;
2315  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/"
2316  "lang/StringBuffer;"] = ID_cprover_string_insert_int_func;
2318  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/"
2319  "lang/StringBuffer;"] = ID_cprover_string_insert_long_func;
2321  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/"
2322  "lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func;
2324  ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/"
2325  "lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
2327  ["java::java.lang.StringBuffer.length:()I"]=
2328  conversion_table["java::java.lang.String.length:()I"];
2330  ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
2331  ID_cprover_string_char_set_func;
2333  ["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
2334  ID_cprover_string_set_length_func;
2336  ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
2337  ID_cprover_string_substring_func;
2339  ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
2340  "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
2342  ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
2344  this,
2345  std::placeholders::_1,
2346  std::placeholders::_2,
2347  std::placeholders::_3,
2348  std::placeholders::_4);
2349 
2350  // CharSequence library
2352  ["java::java.lang.CharSequence.charAt:(I)C"]=
2353  ID_cprover_string_char_at_func;
2355  ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
2357  this,
2358  std::placeholders::_1,
2359  std::placeholders::_2,
2360  std::placeholders::_3,
2361  std::placeholders::_4);
2363  ["java::java.lang.CharSequence.length:()I"]=
2364  conversion_table["java::java.lang.String.length:()I"];
2365 
2366  // Other libraries
2367  conversion_table["java::java.lang.Float.toString:(F)Ljava/lang/String;"] =
2368  std::bind(
2370  this,
2371  std::placeholders::_1,
2372  std::placeholders::_2,
2373  std::placeholders::_3,
2374  std::placeholders::_4);
2376  ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
2377  ID_cprover_string_parse_int_func;
2379  ["java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
2380  ID_cprover_string_parse_int_func;
2382  ["java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
2383  ID_cprover_string_parse_int_func;
2385  ["java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
2386  ID_cprover_string_parse_int_func;
2388  ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
2389  ID_cprover_string_of_int_hex_func;
2391  ["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
2392  ID_cprover_string_of_int_func;
2394  ["java::java.lang.Integer.toString:(II)Ljava/lang/String;"]=
2395  ID_cprover_string_of_int_func;
2397  ["java::java.lang.Long.toString:(J)Ljava/lang/String;"]=
2398  ID_cprover_string_of_int_func;
2400  ["java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
2401  ID_cprover_string_of_int_func;
2402  conversion_table["java::java.lang.Object.getClass:()Ljava/lang/Class;"] =
2403  std::bind(
2405  this,
2406  std::placeholders::_1,
2407  std::placeholders::_2,
2408  std::placeholders::_3,
2409  std::placeholders::_4);
2410 }
#define loc()
codet make_copy_string_code(const code_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.
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
const codet & then_case() const
Definition: std_code.h:481
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:3230
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)
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
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:43
exprt make_argument_for_format(const exprt &argv, int 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 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:179
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.
codet make_assign_function_from_call(const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function and assign the result to object this.
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
codet make_init_from_array_code(const code_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.
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:471
Evaluates to true if the operand is infinite.
Definition: std_expr.h:4040
irep_idt get_tag(const typet &type)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
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
codet make_assign_and_return_function_from_call(const irep_idt &function_name, const code_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. ...
#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:4520
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:3361
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:4424
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
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:205
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:3871
TO_BE_DOCUMENTED.
Definition: std_types.h:1569
void change_spec(const ieee_float_spect &dest_spec)
mstreamt & warning() const
Definition: message.h:307
equality
Definition: std_expr.h:1354
codet make_float_to_string_code(const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Provide code for the String.valueOf(F) function.
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:189
static bool is_java_string_builder_type(const typet &type)
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3988
An expression denoting infinity.
Definition: std_expr.h:4694
void add(const codet &code)
Definition: std_code.h:111
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:860
A reference into the symbol table.
Definition: std_types.h:110
codet make_copy_constructor_code(const code_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.
A declaration of a local variable.
Definition: std_code.h:253
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
The NIL expression.
Definition: std_expr.h:4510
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:1426
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:280
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:3284
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
exprt::operandst process_parameters(const code_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.
The symbol table.
Definition: symbol_table.h:19
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:230
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
codet make_init_function_from_call(const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool ignore_first_arg=true)
Generate the goto code for string initialization.
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
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:828
The plus expression.
Definition: std_expr.h:893
typet string_length_type()
typet java_byte_type()
Definition: java_types.cpp:52
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
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:3170
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 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
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const bool lock, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
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
An assumption, which must hold in subsequent code.
Definition: std_code.h:354
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.
codet make_string_format_code(const code_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.
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:1373
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:848
Base class for all expressions.
Definition: expr.h:42
codet make_function_from_call(const irep_idt &function_name, const code_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...
const parameterst & parameters() const
Definition: std_types.h:905
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
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:250
codet make_object_get_class_code(const code_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.
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const exprt & length() const
Definition: string_expr.h:206
codet make_string_length_code(const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for the String.length method.
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:88
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:1004
An if-then-else.
Definition: std_code.h:461
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:72
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
dstringt irep_idt
Definition: irep.h:31
A statement in a programming language.
Definition: std_code.h:21
Return from a function.
Definition: std_code.h:893
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:257
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)
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:491
const irep_idt & get_identifier() const
Definition: std_types.h:840
exprt get_object_at_index(const exprt &argv, int index)
Helper for format function.
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.
codet make_equals_function_code(const code_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.
const irep_idt & get_identifier() const
Definition: std_types.h:123
Assignment.
Definition: std_code.h:195
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:214
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:2991
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...
codet make_string_returning_function_from_call(const irep_idt &function_name, const code_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...