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"
12 
13 #include <util/invariant.h>
14 #include <util/message.h>
15 #include <util/prefix.h>
16 #include <util/std_types.h>
17 #include <util/string_utils.h>
18 
19 #include <set>
20 #include <unordered_set>
21 
22 bool java_is_array_type(const typet &type)
23 {
24  if(type.id() != ID_struct)
25  return false;
27 }
28 
29 unsigned java_local_variable_slots(const typet &t)
30 {
31 
32  // Even on a 64-bit platform, Java pointers occupy one slot:
33  if(t.id()==ID_pointer)
34  return 1;
35 
36  const std::size_t bitwidth = t.get_size_t(ID_width);
37  INVARIANT(
38  bitwidth==8 ||
39  bitwidth==16 ||
40  bitwidth==32 ||
41  bitwidth==64,
42  "all types constructed in java_types.cpp encode JVM types "
43  "with these bit widths");
44 
45  return bitwidth == 64 ? 2u : 1u;
46 }
47 
49 {
50  unsigned slots=0;
51 
52  for(const auto &p : t.parameters())
53  slots+=java_local_variable_slots(p.type());
54 
55  return slots;
56 }
57 
58 const std::string java_class_to_package(const std::string &canonical_classname)
59 {
60  return trim_from_last_delimiter(canonical_classname, '.');
61 }
62 
64  const irep_idt &class_name,
65  symbol_table_baset &symbol_table,
66  message_handlert &message_handler,
67  const struct_union_typet::componentst &componentst)
68 {
69  java_class_typet class_type;
70 
71  class_type.set_tag(class_name);
72  class_type.set_is_stub(true);
73 
74  // produce class symbol
75  symbolt new_symbol;
76  new_symbol.base_name=class_name;
77  new_symbol.pretty_name=class_name;
78  new_symbol.name="java::"+id2string(class_name);
79  class_type.set_name(new_symbol.name);
80  new_symbol.type=class_type;
81  new_symbol.mode=ID_java;
82  new_symbol.is_type=true;
83 
84  std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
85 
86  if(!res.second)
87  {
88  messaget message(message_handler);
89  message.warning() <<
90  "stub class symbol " <<
91  new_symbol.name <<
92  " already exists" << messaget::eom;
93  }
94  else
95  {
96  // create the class identifier etc
97  java_root_class(res.first);
98  java_add_components_to_class(res.first, componentst);
99  }
100 }
101 
103  exprt &expr,
104  const source_locationt &source_location)
105 {
106  expr.add_source_location().merge(source_location);
107  for(exprt &op : expr.operands())
108  merge_source_location_rec(op, source_location);
109 }
110 
112 {
114 }
115 
117  const std::string &friendly_name,
118  const symbol_table_baset &symbol_table,
119  std::string &error)
120 {
121  std::string qualified_name="java::"+friendly_name;
122  if(friendly_name.rfind(':')==std::string::npos)
123  {
124  std::string prefix=qualified_name+':';
125  std::set<irep_idt> matches;
126 
127  for(const auto &s : symbol_table.symbols)
128  if(has_prefix(id2string(s.first), prefix) &&
129  s.second.type.id()==ID_code)
130  matches.insert(s.first);
131 
132  if(matches.empty())
133  {
134  error="'"+friendly_name+"' not found";
135  return irep_idt();
136  }
137  else if(matches.size()>1)
138  {
139  std::ostringstream message;
140  message << "'"+friendly_name+"' is ambiguous between:";
141 
142  // Trim java:: prefix so we can recommend an appropriate input:
143  for(const auto &s : matches)
144  message << "\n " << id2string(s).substr(6);
145 
146  error=message.str();
147  return irep_idt();
148  }
149  else
150  {
151  return *matches.begin();
152  }
153  }
154  else
155  {
156  auto findit=symbol_table.symbols.find(qualified_name);
157  if(findit==symbol_table.symbols.end())
158  {
159  error="'"+friendly_name+"' not found";
160  return irep_idt();
161  }
162  else if(findit->second.type.id()!=ID_code)
163  {
164  error="'"+friendly_name+"' not a function";
165  return irep_idt();
166  }
167  else
168  {
169  return findit->first;
170  }
171  }
172 }
173 
175 {
176  dereference_exprt result(expr, type);
177  // tag it so it's easy to identify during instrumentation
178  result.set(ID_java_member_access, true);
179  return result;
180 }
181 
196  const std::string &src,
197  size_t open_pos,
198  char open_char,
199  char close_char)
200 {
201  // having the same opening and closing delimiter does not allow for hierarchic
202  // structuring
203  PRECONDITION(open_char!=close_char);
204  PRECONDITION(src[open_pos]==open_char);
205  size_t c_pos=open_pos+1;
206  const size_t end_pos=src.size()-1;
207  size_t depth=0;
208 
209  while(c_pos<=end_pos)
210  {
211  if(src[c_pos] == open_char)
212  depth++;
213  else if(src[c_pos] == close_char)
214  {
215  if(depth==0)
216  return c_pos;
217  depth--;
218  }
219  c_pos++;
220  // limit depth to sensible values
221  INVARIANT(
222  depth<=(src.size()-open_pos),
223  "No closing \'"+std::to_string(close_char)+
224  "\' found in signature to parse.");
225  }
226  // did not find corresponding closing '>'
227  return std::string::npos;
228 }
229 
235  symbolt &class_symbol,
236  const struct_union_typet::componentst &components_to_add)
237 {
238  PRECONDITION(class_symbol.is_type);
239  PRECONDITION(class_symbol.type.id()==ID_struct);
240  struct_typet &struct_type=to_struct_type(class_symbol.type);
241  struct_typet::componentst &components=struct_type.components();
242 
243  for(const struct_union_typet::componentt &component : components_to_add)
244  {
245  components.push_back(component);
246  }
247 }
248 
254  irep_idt function_name,
255  const typet &type,
256  symbol_table_baset &symbol_table)
257 {
258  auxiliary_symbolt func_symbol;
259  func_symbol.base_name=function_name;
260  func_symbol.pretty_name=function_name;
261  func_symbol.is_static_lifetime=false;
262  func_symbol.mode=ID_java;
263  func_symbol.name=function_name;
264  func_symbol.type=type;
265  symbol_table.add(func_symbol);
266 }
267 
276  const irep_idt &function_name,
277  const exprt::operandst &arguments,
278  const typet &type,
279  symbol_table_baset &symbol_table)
280 {
281  // Names of function to call
282  std::string fun_name=id2string(function_name);
283 
284  // Declaring the function
285  declare_function(fun_name, type, symbol_table);
286 
287  // Function application
288  return function_application_exprt(symbol_exprt(fun_name), arguments, type);
289 }
290 
295 {
296  const std::string to_strip_str=id2string(to_strip);
297  const std::string prefix="java::";
298 
299  PRECONDITION(has_prefix(to_strip_str, prefix));
300  return to_strip_str.substr(prefix.size(), std::string::npos);
301 }
302 
307 // qualifiers, or the type as it was passed otherwise.
308 std::string pretty_print_java_type(const std::string &fqn_java_type)
309 {
310  std::string result(fqn_java_type);
311  const std::string java_cbmc_string("java::");
312  // Remove the CBMC internal java identifier
313  if(has_prefix(fqn_java_type, java_cbmc_string))
314  result = fqn_java_type.substr(java_cbmc_string.length());
315  // If the class is in package java.lang strip
316  // package name due to default import
317  const std::string java_lang_string("java.lang.");
318  if(has_prefix(result, java_lang_string))
319  result = result.substr(java_lang_string.length());
320  return result;
321 }
322 
336  const irep_idt &component_class_id,
337  const irep_idt &component_name,
338  const symbol_tablet &symbol_table,
339  const class_hierarchyt &class_hierarchy,
340  bool include_interfaces)
341 {
342  resolve_inherited_componentt component_resolver(
343  symbol_table, class_hierarchy);
344  const resolve_inherited_componentt::inherited_componentt resolved_component =
345  component_resolver(component_class_id, component_name, include_interfaces);
346 
347  // resolved_component is a pair (class-name, component-name) found by walking
348  // the chain of class inheritance (not interfaces!) and stopping on the first
349  // class that contains a component of equal name and type to `component_name`
350 
351  if(resolved_component.is_valid())
352  {
353  // Directly defined on the class referred to?
354  if(component_class_id == resolved_component.get_class_identifier())
355  return resolved_component;
356 
357  // No, may be inherited from some parent class; check it is visible:
358  const symbolt &component_symbol=
359  *symbol_table.lookup(resolved_component.get_full_component_identifier());
360 
361  irep_idt access = component_symbol.type.get(ID_access);
362  if(access.empty())
363  access = component_symbol.type.get(ID_C_access);
364 
365  if(access==ID_public || access==ID_protected)
366  {
367  // since the component is public, it is inherited
368  return resolved_component;
369  }
370 
371  // components with the default access modifier are only
372  // accessible within the same package.
373  if(access==ID_default)
374  {
375  const std::string &class_package=
376  java_class_to_package(id2string(component_class_id));
377  const std::string &component_package=
379  id2string(
380  resolved_component.get_class_identifier()));
381  if(component_package == class_package)
382  return resolved_component;
383  else
385  }
386 
387  if(access==ID_private)
388  {
389  // We return not-found because the component found by the
390  // component_resolver above proves that `component_name` cannot be
391  // inherited (assuming that the original Java code compiles). This is
392  // because, as we walk the inheritance chain for `classname` from Object
393  // to `classname`, a component can only become "more accessible". So, if
394  // the last occurrence is private, all others before must be private as
395  // well, and none is inherited in `classname`.
397  }
398 
399  UNREACHABLE; // Unexpected access modifier
400  }
401  else
402  {
404  }
405 }
406 
411 {
412  static const irep_idt in = "java::java.lang.System.in";
413  static const irep_idt out = "java::java.lang.System.out";
414  static const irep_idt err = "java::java.lang.System.err";
415  return symbolid == in || symbolid == out || symbolid == err;
416 }
417 
420 const std::unordered_set<std::string> cprover_methods_to_ignore
421 {
422  "nondetBoolean",
423  "nondetByte",
424  "nondetChar",
425  "nondetShort",
426  "nondetInt",
427  "nondetLong",
428  "nondetFloat",
429  "nondetDouble",
430  "nondetWithNull",
431  "nondetWithoutNull",
432  "notModelled",
433  "atomicBegin",
434  "atomicEnd",
435  "startThread",
436  "endThread",
437  "getCurrentThreadID"
438 };
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table...
Definition: java_types.h:240
#define JAVA_STRING_LITERAL_PREFIX
Definition: java_utils.h:53
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:174
Application of (mathematical) function.
Definition: std_expr.h:4481
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically, we add a new component, &#39;@class_identifier&#39;.
Non-graph-based representation of the class hierarchy.
irep_idt mode
Language mode.
Definition: symbol.h:49
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:111
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool java_is_array_type(const typet &type)
Definition: java_utils.cpp:22
const std::string java_class_to_package(const std::string &canonical_classname)
Definition: java_utils.cpp:58
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
std::vector< componentt > componentst
Definition: std_types.h:203
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
Symbol table entry.
Definition: symbol.h:27
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:63
Structure type, corresponds to C style structs.
Definition: std_types.h:276
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:173
bool is_static_lifetime
Definition: symbol.h:65
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function &#39;invariant_violated_string&#39;.
Definition: invariant.h:400
mstreamt & warning() const
Definition: message.h:391
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:195
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in &#39;from&#39;.
const irep_idt & id() const
Definition: irep.h:259
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:335
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:294
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
Create a function application expression.
Definition: java_utils.cpp:275
Operator to dereference a pointer.
Definition: std_expr.h:3355
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:234
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:148
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
void set_tag(const irep_idt &tag)
Definition: std_types.h:227
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted), leaving the driver program to stub them if it wishes.
Definition: java_utils.cpp:421
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:29
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
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:116
void declare_function(irep_idt function_name, const typet &type, symbol_table_baset &symbol_table)
Declare a function with the given name and type.
Definition: java_utils.cpp:253
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
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:410
const symbolst & symbols
std::vector< exprt > operandst
Definition: expr.h:57
static irep_idt get_tag(const typet &type)
static eomt eom
Definition: message.h:284
typet type
Type of symbol.
Definition: symbol.h:31
Pre-defined types.
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:102
void set_is_stub(const bool &is_stub)
Definition: java_types.h:174
std::string trim_from_last_delimiter(const std::string &s, const char delim)
Base class for all expressions.
Definition: expr.h:54
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
The symbol table base class interface.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
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:48
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
source_locationt & add_source_location()
Definition: expr.h:233
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
dstringt irep_idt
Definition: irep.h:32
bool is_type
Definition: symbol.h:61
operandst & operands()
Definition: expr.h:78
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
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.lang.Integer -> Integer).
Definition: java_utils.cpp:308
bool empty() const
Definition: dstring.h:75
irep_idt get_full_component_identifier() const
Get the full name of this function.
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286