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,
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(ID_base_name, class_name);
73 
74  class_type.set(ID_incomplete_class, true);
75 
76  // produce class symbol
77  symbolt new_symbol;
78  new_symbol.base_name=class_name;
79  new_symbol.pretty_name=class_name;
80  new_symbol.name="java::"+id2string(class_name);
81  class_type.set_name(new_symbol.name);
82  new_symbol.type=class_type;
83  new_symbol.mode=ID_java;
84  new_symbol.is_type=true;
85 
86  std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
87 
88  if(!res.second)
89  {
90  messaget message(message_handler);
91  message.warning() <<
92  "stub class symbol " <<
93  new_symbol.name <<
94  " already exists" << messaget::eom;
95  }
96  else
97  {
98  // create the class identifier etc
99  java_root_class(res.first);
100  java_add_components_to_class(res.first, componentst);
101  }
102 }
103 
105  exprt &expr,
106  const source_locationt &source_location)
107 {
108  expr.add_source_location().merge(source_location);
109  for(exprt &op : expr.operands())
110  merge_source_location_rec(op, source_location);
111 }
112 
114 {
116 }
117 
119  const std::string &friendly_name,
120  const symbol_table_baset &symbol_table,
121  std::string &error)
122 {
123  std::string qualified_name="java::"+friendly_name;
124  if(friendly_name.rfind(':')==std::string::npos)
125  {
126  std::string prefix=qualified_name+':';
127  std::set<irep_idt> matches;
128 
129  for(const auto &s : symbol_table.symbols)
130  if(has_prefix(id2string(s.first), prefix) &&
131  s.second.type.id()==ID_code)
132  matches.insert(s.first);
133 
134  if(matches.empty())
135  {
136  error="'"+friendly_name+"' not found";
137  return irep_idt();
138  }
139  else if(matches.size()>1)
140  {
141  std::ostringstream message;
142  message << "'"+friendly_name+"' is ambiguous between:";
143 
144  // Trim java:: prefix so we can recommend an appropriate input:
145  for(const auto &s : matches)
146  message << "\n " << id2string(s).substr(6);
147 
148  error=message.str();
149  return irep_idt();
150  }
151  else
152  {
153  return *matches.begin();
154  }
155  }
156  else
157  {
158  auto findit=symbol_table.symbols.find(qualified_name);
159  if(findit==symbol_table.symbols.end())
160  {
161  error="'"+friendly_name+"' not found";
162  return irep_idt();
163  }
164  else if(findit->second.type.id()!=ID_code)
165  {
166  error="'"+friendly_name+"' not a function";
167  return irep_idt();
168  }
169  else
170  {
171  return findit->first;
172  }
173  }
174 }
175 
177 {
178  dereference_exprt result(expr, type);
179  // tag it so it's easy to identify during instrumentation
180  result.set(ID_java_member_access, true);
181  return result;
182 }
183 
198  const std::string &src,
199  size_t open_pos,
200  char open_char,
201  char close_char)
202 {
203  // having the same opening and closing delimiter does not allow for hierarchic
204  // structuring
205  PRECONDITION(open_char!=close_char);
206  PRECONDITION(src[open_pos]==open_char);
207  size_t c_pos=open_pos+1;
208  const size_t end_pos=src.size()-1;
209  size_t depth=0;
210 
211  while(c_pos<=end_pos)
212  {
213  if(src[c_pos] == open_char)
214  depth++;
215  else if(src[c_pos] == close_char)
216  {
217  if(depth==0)
218  return c_pos;
219  depth--;
220  }
221  c_pos++;
222  // limit depth to sensible values
223  INVARIANT(
224  depth<=(src.size()-open_pos),
225  "No closing \'"+std::to_string(close_char)+
226  "\' found in signature to parse.");
227  }
228  // did not find corresponding closing '>'
229  return std::string::npos;
230 }
231 
237  symbolt &class_symbol,
238  const struct_union_typet::componentst &components_to_add)
239 {
240  PRECONDITION(class_symbol.is_type);
241  PRECONDITION(class_symbol.type.id()==ID_struct);
242  struct_typet &struct_type=to_struct_type(class_symbol.type);
243  struct_typet::componentst &components=struct_type.components();
244 
245  for(const struct_union_typet::componentt &component : components_to_add)
246  {
247  components.push_back(component);
248  }
249 }
250 
256  irep_idt function_name,
257  const typet &type,
258  symbol_table_baset &symbol_table)
259 {
260  auxiliary_symbolt func_symbol;
261  func_symbol.base_name=function_name;
262  func_symbol.pretty_name=function_name;
263  func_symbol.is_static_lifetime=false;
264  func_symbol.mode=ID_java;
265  func_symbol.name=function_name;
266  func_symbol.type=type;
267  symbol_table.add(func_symbol);
268 }
269 
278  const irep_idt &function_name,
279  const exprt::operandst &arguments,
280  const typet &type,
281  symbol_table_baset &symbol_table)
282 {
283  // Names of function to call
284  std::string fun_name=id2string(function_name);
285 
286  // Declaring the function
287  declare_function(fun_name, type, symbol_table);
288 
289  // Function application
290  function_application_exprt call(symbol_exprt(fun_name), type);
291  call.arguments()=arguments;
292  return call;
293 }
294 
299 {
300  const std::string to_strip_str=id2string(to_strip);
301  const std::string prefix="java::";
302 
303  PRECONDITION(has_prefix(to_strip_str, prefix));
304  return to_strip_str.substr(prefix.size(), std::string::npos);
305 }
306 
311 // qualifiers, or the type as it was passed otherwise.
312 std::string pretty_print_java_type(const std::string &fqn_java_type)
313 {
314  std::string result(fqn_java_type);
315  const std::string java_cbmc_string("java::");
316  // Remove the CBMC internal java identifier
317  if(has_prefix(fqn_java_type, java_cbmc_string))
318  result = fqn_java_type.substr(java_cbmc_string.length());
319  // If the class is in package java.lang strip
320  // package name due to default import
321  const std::string java_lang_string("java.lang.");
322  if(has_prefix(result, java_lang_string))
323  result = result.substr(java_lang_string.length());
324  return result;
325 }
326 
340  const irep_idt &component_class_id,
341  const irep_idt &component_name,
342  const symbol_tablet &symbol_table,
343  const class_hierarchyt &class_hierarchy,
344  bool include_interfaces)
345 {
346  resolve_inherited_componentt component_resolver(
347  symbol_table, class_hierarchy);
348  const resolve_inherited_componentt::inherited_componentt resolved_component =
349  component_resolver(component_class_id, component_name, include_interfaces);
350 
351  // resolved_component is a pair (class-name, component-name) found by walking
352  // the chain of class inheritance (not interfaces!) and stopping on the first
353  // class that contains a component of equal name and type to `component_name`
354 
355  if(resolved_component.is_valid())
356  {
357  // Directly defined on the class referred to?
358  if(component_class_id == resolved_component.get_class_identifier())
359  return resolved_component;
360 
361  // No, may be inherited from some parent class; check it is visible:
362  const symbolt &component_symbol=
363  *symbol_table.lookup(resolved_component.get_full_component_identifier());
364 
365  irep_idt access = component_symbol.type.get(ID_access);
366  if(access.empty())
367  access = component_symbol.type.get(ID_C_access);
368 
369  if(access==ID_public || access==ID_protected)
370  {
371  // since the component is public, it is inherited
372  return resolved_component;
373  }
374 
375  // components with the default access modifier are only
376  // accessible within the same package.
377  if(access==ID_default)
378  {
379  const std::string &class_package=
380  java_class_to_package(id2string(component_class_id));
381  const std::string &component_package=
383  id2string(
384  resolved_component.get_class_identifier()));
385  if(component_package == class_package)
386  return resolved_component;
387  else
389  }
390 
391  if(access==ID_private)
392  {
393  // We return not-found because the component found by the
394  // component_resolver above proves that `component_name` cannot be
395  // inherited (assuming that the original Java code compiles). This is
396  // because, as we walk the inheritance chain for `classname` from Object
397  // to `classname`, a component can only become "more accessible". So, if
398  // the last occurrence is private, all others before must be private as
399  // well, and none is inherited in `classname`.
401  }
402 
403  UNREACHABLE; // Unexpected access modifier
404  }
405  else
406  {
408  }
409 }
410 
415 {
416  static const irep_idt in = "java::java.lang.System.in";
417  static const irep_idt out = "java::java.lang.System.out";
418  static const irep_idt err = "java::java.lang.System.err";
419  return symbolid == in || symbolid == out || symbolid == err;
420 }
421 
424 const std::unordered_set<std::string> cprover_methods_to_ignore
425 {
426  "nondetBoolean",
427  "nondetByte",
428  "nondetChar",
429  "nondetShort",
430  "nondetInt",
431  "nondetLong",
432  "nondetFloat",
433  "nondetDouble",
434  "nondetWithNull",
435  "nondetWithoutNull",
436  "notModelled",
437  "atomicBegin",
438  "atomicEnd",
439  "startThread",
440  "endThread",
441  "getCurrentThreadID"
442 };
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table...
Definition: java_types.h:221
#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:176
application of (mathematical) function
Definition: std_expr.h:4529
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:52
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:113
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
irep_idt get_tag(const typet &type)
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
std::vector< componentt > componentst
Definition: std_types.h:243
argumentst & arguments()
Definition: std_expr.h:4562
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
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
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:174
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
mstreamt & warning() const
Definition: message.h:307
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:197
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:339
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:298
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
Create a function application expression.
Definition: java_utils.cpp:277
Operator to dereference a pointer.
Definition: std_expr.h:3282
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:236
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
void set_tag(const irep_idt &tag)
Definition: std_types.h:267
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:425
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
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:118
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:255
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:414
const symbolst & symbols
std::vector< exprt > operandst
Definition: expr.h:45
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
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:104
std::string trim_from_last_delimiter(const std::string &s, const char delim)
Base class for all expressions.
Definition: expr.h:42
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.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define UNREACHABLE
Definition: invariant.h:271
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:130
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
dstringt irep_idt
Definition: irep.h:32
bool is_type
Definition: symbol.h:63
operandst & operands()
Definition: expr.h:66
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:255
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:312
bool empty() const
Definition: dstring.h:73
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