cprover
java_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_utils.h"
10 
11 #include "java_root_class.h"
13 
14 #include <util/fresh_symbol.h>
15 #include <util/invariant.h>
16 #include <util/mathematical_expr.h>
18 #include <util/message.h>
19 #include <util/prefix.h>
20 #include <util/std_types.h>
21 #include <util/string_utils.h>
22 
23 #include <set>
24 #include <unordered_set>
25 
26 bool java_is_array_type(const typet &type)
27 {
28  if(type.id() != ID_struct)
29  return false;
31 }
32 
33 bool is_java_string_type(const struct_typet &struct_type)
34 {
36  struct_type) &&
37  struct_type.has_component("length") &&
38  struct_type.has_component("data");
39 }
40 
43 {
44  static std::unordered_map<irep_idt, java_boxed_type_infot> type_info_by_name =
45  {
46  {"java::java.lang.Boolean",
47  {"java::java.lang.Boolean.booleanValue:()Z", java_boolean_type()}},
48  {"java::java.lang.Byte",
49  {"java::java.lang.Byte.byteValue:()B", java_byte_type()}},
50  {"java::java.lang.Character",
51  {"java::java.lang.Character.charValue:()C", java_char_type()}},
52  {"java::java.lang.Double",
53  {"java::java.lang.Double.doubleValue:()D", java_double_type()}},
54  {"java::java.lang.Float",
55  {"java::java.lang.Float.floatValue:()F", java_float_type()}},
56  {"java::java.lang.Integer",
57  {"java::java.lang.Integer.intValue:()I", java_int_type()}},
58  {"java::java.lang.Long",
59  {"java::java.lang.Long.longValue:()J", java_long_type()}},
60  {"java::java.lang.Short",
61  {"java::java.lang.Short.shortValue:()S", java_short_type()}},
62  };
63 
64  auto found = type_info_by_name.find(type_name);
65  return found == type_info_by_name.end() ? nullptr : &found->second;
66 }
67 
69 get_java_primitive_type_info(const typet &maybe_primitive_type)
70 {
71  static std::unordered_map<typet, java_primitive_type_infot, irep_hash>
72  type_info_by_primitive_type = {
74  {"java::java.lang.Boolean",
75  "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;",
76  "java::java.lang.Boolean.booleanValue:()Z"}},
77  {java_byte_type(),
78  {"java::java.lang.Byte",
79  "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;",
80  "java::java.lang.Number.byteValue:()B"}},
81  {java_char_type(),
82  {"java::java.lang.Character",
83  "java::java.lang.Character.valueOf:(C)"
84  "Ljava/lang/Character;",
85  "java::java.lang.Character.charValue:()C"}},
87  {"java::java.lang.Double",
88  "java::java.lang.Double.valueOf:(D)"
89  "Ljava/lang/Double;",
90  "java::java.lang.Number.doubleValue:()D"}},
91  {java_float_type(),
92  {"java::java.lang.Float",
93  "java::java.lang.Float.valueOf:(F)"
94  "Ljava/lang/Float;",
95  "java::java.lang.Number.floatValue:()F"}},
96  {java_int_type(),
97  {"java::java.lang.Integer",
98  "java::java.lang.Integer.valueOf:(I)"
99  "Ljava/lang/Integer;",
100  "java::java.lang.Number.intValue:()I"}},
101  {java_long_type(),
102  {"java::java.lang.Long",
103  "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;",
104  "java::java.lang.Number.longValue:()J"}},
105  {java_short_type(),
106  {"java::java.lang.Short",
107  "java::java.lang.Short.valueOf:(S)"
108  "Ljava/lang/Short;",
109  "java::java.lang.Number.shortValue:()S"}}};
110 
111  auto found = type_info_by_primitive_type.find(maybe_primitive_type);
112  return found == type_info_by_primitive_type.end() ? nullptr : &found->second;
113 }
114 
116 {
117  return get_boxed_type_info_by_name(id) != nullptr;
118 }
119 
120 bool is_primitive_wrapper_type_name(const std::string &type_name)
121 {
122  static const std::unordered_set<std::string> primitive_wrapper_type_names = {
123  "java.lang.Boolean",
124  "java.lang.Byte",
125  "java.lang.Character",
126  "java.lang.Double",
127  "java.lang.Float",
128  "java.lang.Integer",
129  "java.lang.Long",
130  "java.lang.Short"};
131  return primitive_wrapper_type_names.count(type_name) > 0;
132 }
133 
135 {
136 
137  // Even on a 64-bit platform, Java pointers occupy one slot:
138  if(t.id()==ID_pointer)
139  return 1;
140 
141  const std::size_t bitwidth = to_bitvector_type(t).get_width();
142  INVARIANT(
143  bitwidth==8 ||
144  bitwidth==16 ||
145  bitwidth==32 ||
146  bitwidth==64,
147  "all types constructed in java_types.cpp encode JVM types "
148  "with these bit widths");
149 
150  return bitwidth == 64 ? 2u : 1u;
151 }
152 
154 {
155  unsigned slots=0;
156 
157  for(const auto &p : t.parameters())
158  slots+=java_local_variable_slots(p.type());
159 
160  return slots;
161 }
162 
163 const std::string java_class_to_package(const std::string &canonical_classname)
164 {
165  return trim_from_last_delimiter(canonical_classname, '.');
166 }
167 
169  const irep_idt &class_name,
170  symbol_table_baset &symbol_table,
171  message_handlert &message_handler,
172  const struct_union_typet::componentst &componentst)
173 {
174  java_class_typet class_type;
175 
176  class_type.set_tag(class_name);
177  class_type.set_is_stub(true);
178 
179  // produce class symbol
180  symbolt new_symbol;
181  new_symbol.base_name=class_name;
182  new_symbol.pretty_name=class_name;
183  new_symbol.name="java::"+id2string(class_name);
184  class_type.set_name(new_symbol.name);
185  new_symbol.type=class_type;
186  new_symbol.mode=ID_java;
187  new_symbol.is_type=true;
188 
189  std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
190 
191  if(!res.second)
192  {
193  messaget message(message_handler);
194  message.warning() <<
195  "stub class symbol " <<
196  new_symbol.name <<
197  " already exists" << messaget::eom;
198  }
199  else
200  {
201  // create the class identifier etc
202  java_root_class(res.first);
203  java_add_components_to_class(res.first, componentst);
204  }
205 }
206 
208  exprt &expr,
209  const source_locationt &source_location)
210 {
211  expr.add_source_location().merge(source_location);
212  for(exprt &op : expr.operands())
213  merge_source_location_rec(op, source_location);
214 }
215 
217 {
219 }
220 
222  const std::string &friendly_name,
223  const symbol_table_baset &symbol_table,
224  std::string &error)
225 {
226  std::string qualified_name="java::"+friendly_name;
227  if(friendly_name.rfind(':')==std::string::npos)
228  {
229  std::string prefix=qualified_name+':';
230  std::set<irep_idt> matches;
231 
232  for(const auto &s : symbol_table.symbols)
233  if(has_prefix(id2string(s.first), prefix) &&
234  s.second.type.id()==ID_code)
235  matches.insert(s.first);
236 
237  if(matches.empty())
238  {
239  error="'"+friendly_name+"' not found";
240  return irep_idt();
241  }
242  else if(matches.size()>1)
243  {
244  std::ostringstream message;
245  message << "'"+friendly_name+"' is ambiguous between:";
246 
247  // Trim java:: prefix so we can recommend an appropriate input:
248  for(const auto &s : matches)
249  message << "\n " << id2string(s).substr(6);
250 
251  error=message.str();
252  return irep_idt();
253  }
254  else
255  {
256  return *matches.begin();
257  }
258  }
259  else
260  {
261  auto findit=symbol_table.symbols.find(qualified_name);
262  if(findit==symbol_table.symbols.end())
263  {
264  error="'"+friendly_name+"' not found";
265  return irep_idt();
266  }
267  else if(findit->second.type.id()!=ID_code)
268  {
269  error="'"+friendly_name+"' not a function";
270  return irep_idt();
271  }
272  else
273  {
274  return findit->first;
275  }
276  }
277 }
278 
280  const pointer_typet &given_pointer_type,
281  const java_class_typet &replacement_class_type)
282 {
283  if(can_cast_type<struct_tag_typet>(given_pointer_type.subtype()))
284  {
285  struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
286  return pointer_type(struct_tag_subtype);
287  }
288  return pointer_type(replacement_class_type);
289 }
290 
292 {
293  dereference_exprt result(expr);
294  // tag it so it's easy to identify during instrumentation
295  result.set(ID_java_member_access, true);
296  return result;
297 }
298 
313  const std::string &src,
314  size_t open_pos,
315  char open_char,
316  char close_char)
317 {
318  // having the same opening and closing delimiter does not allow for hierarchic
319  // structuring
320  PRECONDITION(open_char!=close_char);
321  PRECONDITION(src[open_pos]==open_char);
322  size_t c_pos=open_pos+1;
323  const size_t end_pos=src.size()-1;
324  size_t depth=0;
325 
326  while(c_pos<=end_pos)
327  {
328  if(src[c_pos] == open_char)
329  depth++;
330  else if(src[c_pos] == close_char)
331  {
332  if(depth==0)
333  return c_pos;
334  depth--;
335  }
336  c_pos++;
337  // limit depth to sensible values
338  INVARIANT(
339  depth<=(src.size()-open_pos),
340  "No closing \'"+std::to_string(close_char)+
341  "\' found in signature to parse.");
342  }
343  // did not find corresponding closing '>'
344  return std::string::npos;
345 }
346 
352  symbolt &class_symbol,
353  const struct_union_typet::componentst &components_to_add)
354 {
355  PRECONDITION(class_symbol.is_type);
356  PRECONDITION(class_symbol.type.id()==ID_struct);
357  struct_typet &struct_type=to_struct_type(class_symbol.type);
358  struct_typet::componentst &components=struct_type.components();
359  components.insert(
360  components.end(), components_to_add.begin(), components_to_add.end());
361 }
362 
369  const irep_idt &function_name,
370  const mathematical_function_typet &type,
371  symbol_table_baset &symbol_table)
372 {
373  auxiliary_symbolt func_symbol;
374  func_symbol.base_name=function_name;
375  func_symbol.pretty_name=function_name;
376  func_symbol.is_static_lifetime=false;
377  func_symbol.is_state_var = false;
378  func_symbol.mode=ID_java;
379  func_symbol.name=function_name;
380  func_symbol.type=type;
381  symbol_table.add(func_symbol);
382 
383  return func_symbol;
384 }
385 
395  const irep_idt &function_name,
396  const exprt::operandst &arguments,
397  const typet &range,
398  symbol_table_baset &symbol_table)
399 {
400  std::vector<typet> argument_types;
401  for(const auto &arg : arguments)
402  argument_types.push_back(arg.type());
403 
404  // Declaring the function
405  const auto symbol = declare_function(
406  function_name,
407  mathematical_function_typet(std::move(argument_types), range),
408  symbol_table);
409 
410  // Function application
411  return function_application_exprt(symbol.symbol_expr(), arguments, range);
412 }
413 
418 {
419  const std::string to_strip_str=id2string(to_strip);
420  const std::string prefix="java::";
421 
422  PRECONDITION(has_prefix(to_strip_str, prefix));
423  return to_strip_str.substr(prefix.size(), std::string::npos);
424 }
425 
431 std::string pretty_print_java_type(const std::string &fqn_java_type)
432 {
433  std::string result(fqn_java_type);
434  const std::string java_cbmc_string("java::");
435  // Remove the CBMC internal java identifier
436  if(has_prefix(fqn_java_type, java_cbmc_string))
437  result = fqn_java_type.substr(java_cbmc_string.length());
438  // If the class is in package java.lang strip
439  // package name due to default import
440  const std::string java_lang_string("java.lang.");
441  if(has_prefix(result, java_lang_string))
442  result = result.substr(java_lang_string.length());
443  return result;
444 }
445 
459  const irep_idt &component_class_id,
460  const irep_idt &component_name,
461  const symbol_tablet &symbol_table,
462  bool include_interfaces)
463 {
464  resolve_inherited_componentt component_resolver{symbol_table};
465  const auto resolved_component =
466  component_resolver(component_class_id, component_name, include_interfaces);
467 
468  // resolved_component is a pair (class-name, component-name) found by walking
469  // the chain of class inheritance (not interfaces!) and stopping on the first
470  // class that contains a component of equal name and type to `component_name`
471 
472  if(resolved_component)
473  {
474  // Directly defined on the class referred to?
475  if(component_class_id == resolved_component->get_class_identifier())
476  return *resolved_component;
477 
478  // No, may be inherited from some parent class; check it is visible:
479  const symbolt &component_symbol = symbol_table.lookup_ref(
480  resolved_component->get_full_component_identifier());
481 
482  irep_idt access = component_symbol.type.get(ID_access);
483  if(access.empty())
484  access = component_symbol.type.get(ID_C_access);
485 
486  if(access==ID_public || access==ID_protected)
487  {
488  // since the component is public, it is inherited
489  return *resolved_component;
490  }
491 
492  // components with the default access modifier are only
493  // accessible within the same package.
494  if(access==ID_default)
495  {
496  const std::string &class_package=
497  java_class_to_package(id2string(component_class_id));
498  const std::string &component_package = java_class_to_package(
499  id2string(resolved_component->get_class_identifier()));
500  if(component_package == class_package)
501  return *resolved_component;
502  else
503  return {};
504  }
505 
506  if(access==ID_private)
507  {
508  // We return not-found because the component found by the
509  // component_resolver above proves that `component_name` cannot be
510  // inherited (assuming that the original Java code compiles). This is
511  // because, as we walk the inheritance chain for `classname` from Object
512  // to `classname`, a component can only become "more accessible". So, if
513  // the last occurrence is private, all others before must be private as
514  // well, and none is inherited in `classname`.
515  return {};
516  }
517 
518  UNREACHABLE; // Unexpected access modifier
519  }
520  else
521  {
522  return {};
523  }
524 }
525 
530 {
531  static const irep_idt in = "java::java.lang.System.in";
532  static const irep_idt out = "java::java.lang.System.out";
533  static const irep_idt err = "java::java.lang.System.err";
534  return symbolid == in || symbolid == out || symbolid == err;
535 }
536 
539 const std::unordered_set<std::string> cprover_methods_to_ignore
540 {
541  "nondetBoolean",
542  "nondetByte",
543  "nondetChar",
544  "nondetShort",
545  "nondetInt",
546  "nondetLong",
547  "nondetFloat",
548  "nondetDouble",
549  "nondetWithNull",
550  "nondetWithoutNull",
551  "notModelled",
552  "atomicBegin",
553  "atomicEnd",
554  "startThread",
555  "endThread",
556  "getCurrentThreadID"
557 };
558 
567  const typet &type,
568  const std::string &basename_prefix,
569  const source_locationt &source_location,
570  const irep_idt &function_name,
571  symbol_table_baset &symbol_table)
572 {
573  PRECONDITION(!function_name.empty());
574  const std::string name_prefix = id2string(function_name);
575  return get_fresh_aux_symbol(
576  type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
577 }
578 
580 {
581  const irep_idt &class_id = symbol.type.get(ID_C_class);
582  return class_id.empty() ? optionalt<irep_idt>{} : class_id;
583 }
584 
586 {
587  symbol.type.set(ID_C_class, declaring_class);
588 }
589 
591 class_name_from_method_name(const std::string &method_name)
592 {
593  const auto signature_index = method_name.rfind(":");
594  const auto method_index = method_name.rfind(".", signature_index);
595  if(method_index == std::string::npos)
596  return {};
597  return method_name.substr(0, method_index);
598 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_root_class.h
is_primitive_wrapper_type_name
bool is_primitive_wrapper_type_name(const std::string &type_name)
Returns true iff the argument is the fully qualified name of a Java primitive wrapper type (for examp...
Definition: java_utils.cpp:120
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
is_java_string_literal_id
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:216
set_declaring_class
void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
Sets the identifier of the class which declared a given symbol to declaring_class.
Definition: java_utils.cpp:585
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
Fresh auxiliary symbol creation.
java_long_type
signedbv_typet java_long_type()
Definition: java_types.cpp:44
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
checked_dereference
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:291
make_function_application
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &range, symbol_table_baset &symbol_table)
Create a (mathematical) function application expression.
Definition: java_utils.cpp:394
java_class_to_package
const std::string java_class_to_package(const std::string &canonical_classname)
Definition: java_utils.cpp:163
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:579
prefix.h
invariant.h
java_is_array_type
bool java_is_array_type(const typet &type)
Definition: java_utils.cpp:26
generate_class_stub
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
Definition: java_utils.cpp:168
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:232
java_string_library_preprocess.h
Produce code for simple implementation of String Java libraries.
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
irep_idt
dstringt irep_idt
Definition: irep.h:32
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:160
trim_from_last_delimiter
std::string trim_from_last_delimiter(const std::string &s, const char delim)
Definition: string_utils.cpp:128
class_name_from_method_name
NODISCARD optionalt< std::string > class_name_from_method_name(const std::string &method_name)
Get JVM type name of the class in which method_name is defined.
Definition: java_utils.cpp:591
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
java_class_typet
Definition: java_types.h:199
mathematical_types.h
Mathematical types.
strip_java_namespace_prefix
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:417
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
find_closing_delimiter
size_t find_closing_delimiter(const std::string &src, size_t open_pos, char open_char, char close_char)
Finds the corresponding closing delimiter to the given opening delimiter.
Definition: java_utils.cpp:312
java_boxed_type_infot
Return type for get_boxed_type_info_by_name.
Definition: java_utils.h:57
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
is_java_string_type
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
Definition: java_utils.cpp:33
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition: std_types.h:164
can_cast_type< struct_tag_typet >
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
Definition: std_types.h:502
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
source_locationt::merge
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
Definition: source_location.cpp:73
std_types.h
Pre-defined types.
java_add_components_to_class
void java_add_components_to_class(symbolt &class_symbol, const struct_union_typet::componentst &components_to_add)
Add the components in components_to_add to the class denoted by class symbol.
Definition: java_utils.cpp:351
resolve_friendly_method_name
irep_idt resolve_friendly_method_name(const std::string &friendly_name, const symbol_table_baset &symbol_table, std::string &error)
Resolves a user-friendly method name (like packagename.Class.method) into an internal name (like java...
Definition: java_utils.cpp:221
is_non_null_library_global
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
Definition: java_utils.cpp:529
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
java_string_library_preprocesst::implements_java_char_sequence
static bool implements_java_char_sequence(const typet &type)
Definition: java_string_library_preprocess.h:70
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:152
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
java_local_variable_slots
unsigned java_local_variable_slots(const typet &t)
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to ...
Definition: java_utils.cpp:134
cprover_methods_to_ignore
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
Definition: java_utils.cpp:540
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
pointer_to_replacement_type
pointer_typet pointer_to_replacement_type(const pointer_typet &given_pointer_type, const java_class_typet &replacement_class_type)
Given a pointer type to a Java class and a type representing a more specific Java class,...
Definition: java_utils.cpp:279
fresh_java_symbol
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
Definition: java_utils.cpp:566
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
get_inherited_component
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:458
java_primitive_type_infot
Return type for get_java_primitive_type_info.
Definition: java_utils.h:37
java_short_type
signedbv_typet java_short_type()
Definition: java_types.cpp:50
declare_function
static auxiliary_symbolt declare_function(const irep_idt &function_name, const mathematical_function_typet &type, symbol_table_baset &symbol_table)
Declare a function with the given name and type.
Definition: java_utils.cpp:368
source_locationt
Definition: source_location.h:20
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
java_class_typet::get_name
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:559
java_class_typet::set_is_stub
void set_is_stub(bool is_stub)
Definition: java_types.h:395
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
merge_source_location_rec
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
Definition: java_utils.cpp:207
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
java_double_type
floatbv_typet java_double_type()
Definition: java_types.cpp:74
java_method_parameter_slots
unsigned java_method_parameter_slots(const java_method_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call,...
Definition: java_utils.cpp:153
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
symbolt::is_type
bool is_type
Definition: symbol.h:61
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
java_class_typet::set_name
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:566
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
symbol_table_baset::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
java_root_class
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
Definition: java_root_class.cpp:22
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
exprt::operands
operandst & operands()
Definition: expr.h:95
get_boxed_type_info_by_name
const java_boxed_type_infot * get_boxed_type_info_by_name(const irep_idt &type_name)
If type_name is a Java boxed type tag, return information about it, otherwise return null.
Definition: java_utils.cpp:42
pretty_print_java_type
std::string pretty_print_java_type(const std::string &fqn_java_type)
Strip the package name from a java type, for the type to be pretty printed (java::java....
Definition: java_utils.cpp:431
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
is_primitive_wrapper_type_id
bool is_primitive_wrapper_type_id(const irep_idt &id)
Returns true iff the argument is the symbol-table identifier of a Java primitive wrapper type (for ex...
Definition: java_utils.cpp:115
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
message.h
java_utils.h
java_method_typet
Definition: java_types.h:103
mathematical_function_typet
A type for mathematical functions (do not confuse with functions/methods in code)
Definition: mathematical_types.h:59
get_java_primitive_type_info
const java_primitive_type_infot * get_java_primitive_type_info(const typet &maybe_primitive_type)
If primitive_type is a Java primitive type, return information about it, otherwise return null.
Definition: java_utils.cpp:69
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
JAVA_STRING_LITERAL_PREFIX
#define JAVA_STRING_LITERAL_PREFIX
Definition: java_utils.h:107
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
java_float_type
floatbv_typet java_float_type()
Definition: java_types.cpp:68
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
resolve_inherited_componentt
Definition: resolve_inherited_component.h:22
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:38