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 #include "java_types.h"
13 
14 #include <util/invariant.h>
15 #include <util/message.h>
16 #include <util/prefix.h>
17 #include <util/std_types.h>
18 #include <util/string_utils.h>
19 
20 #include <set>
21 #include <unordered_set>
22 
23 bool java_is_array_type(const typet &type)
24 {
25  if(type.id() != ID_struct)
26  return false;
28 }
29 
30 unsigned java_local_variable_slots(const typet &t)
31 {
32 
33  // Even on a 64-bit platform, Java pointers occupy one slot:
34  if(t.id()==ID_pointer)
35  return 1;
36 
37  unsigned bitwidth;
38 
39  bitwidth=t.get_unsigned_int(ID_width);
40  INVARIANT(
41  bitwidth==8 ||
42  bitwidth==16 ||
43  bitwidth==32 ||
44  bitwidth==64,
45  "all types constructed in java_types.cpp encode JVM types "
46  "with these bit widths");
47 
48  return bitwidth==64 ? 2 : 1;
49 }
50 
52 {
53  unsigned slots=0;
54 
55  for(const auto &p : t.parameters())
56  slots+=java_local_variable_slots(p.type());
57 
58  return slots;
59 }
60 
61 const std::string java_class_to_package(const std::string &canonical_classname)
62 {
63  return trim_from_last_delimiter(canonical_classname, '.');
64 }
65 
67  const irep_idt &class_name,
68  symbol_table_baset &symbol_table,
70  const struct_union_typet::componentst &componentst)
71 {
72  class_typet class_type;
73 
74  class_type.set_tag(class_name);
75  class_type.set(ID_base_name, class_name);
76 
77  class_type.set(ID_incomplete_class, true);
78 
79  // produce class symbol
80  symbolt new_symbol;
81  new_symbol.base_name=class_name;
82  new_symbol.pretty_name=class_name;
83  new_symbol.name="java::"+id2string(class_name);
84  class_type.set(ID_name, new_symbol.name);
85  new_symbol.type=class_type;
86  new_symbol.mode=ID_java;
87  new_symbol.is_type=true;
88 
89  std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
90 
91  if(!res.second)
92  {
93  messaget message(message_handler);
94  message.warning() <<
95  "stub class symbol " <<
96  new_symbol.name <<
97  " already exists" << messaget::eom;
98  }
99  else
100  {
101  // create the class identifier etc
102  java_root_class(res.first);
103  java_add_components_to_class(res.first, componentst);
104  }
105 }
106 
108  exprt &expr,
109  const source_locationt &source_location)
110 {
111  expr.add_source_location().merge(source_location);
112  for(exprt &op : expr.operands())
113  merge_source_location_rec(op, source_location);
114 }
115 
117 {
119 }
120 
122  const std::string &friendly_name,
123  const symbol_table_baset &symbol_table,
124  std::string &error)
125 {
126  std::string qualified_name="java::"+friendly_name;
127  if(friendly_name.rfind(':')==std::string::npos)
128  {
129  std::string prefix=qualified_name+':';
130  std::set<irep_idt> matches;
131 
132  for(const auto &s : symbol_table.symbols)
133  if(has_prefix(id2string(s.first), prefix) &&
134  s.second.type.id()==ID_code)
135  matches.insert(s.first);
136 
137  if(matches.empty())
138  {
139  error="'"+friendly_name+"' not found";
140  return irep_idt();
141  }
142  else if(matches.size()>1)
143  {
144  std::ostringstream message;
145  message << "'"+friendly_name+"' is ambiguous between:";
146 
147  // Trim java:: prefix so we can recommend an appropriate input:
148  for(const auto &s : matches)
149  message << "\n " << id2string(s).substr(6);
150 
151  error=message.str();
152  return irep_idt();
153  }
154  else
155  {
156  return *matches.begin();
157  }
158  }
159  else
160  {
161  auto findit=symbol_table.symbols.find(qualified_name);
162  if(findit==symbol_table.symbols.end())
163  {
164  error="'"+friendly_name+"' not found";
165  return irep_idt();
166  }
167  else if(findit->second.type.id()!=ID_code)
168  {
169  error="'"+friendly_name+"' not a function";
170  return irep_idt();
171  }
172  else
173  {
174  return findit->first;
175  }
176  }
177 }
178 
180 {
181  dereference_exprt result(expr, type);
182  // tag it so it's easy to identify during instrumentation
183  result.set(ID_java_member_access, true);
184  return result;
185 }
186 
201  const std::string &src,
202  size_t open_pos,
203  char open_char,
204  char close_char)
205 {
206  // having the same opening and closing delimiter does not allow for hierarchic
207  // structuring
208  PRECONDITION(open_char!=close_char);
209  PRECONDITION(src[open_pos]==open_char);
210  size_t c_pos=open_pos+1;
211  const size_t end_pos=src.size()-1;
212  size_t depth=0;
213 
214  while(c_pos<=end_pos)
215  {
216  if(src[c_pos] == open_char)
217  depth++;
218  else if(src[c_pos] == close_char)
219  {
220  if(depth==0)
221  return c_pos;
222  depth--;
223  }
224  c_pos++;
225  // limit depth to sensible values
226  INVARIANT(
227  depth<=(src.size()-open_pos),
228  "No closing \'"+std::to_string(close_char)+
229  "\' found in signature to parse.");
230  }
231  // did not find corresponding closing '>'
232  return std::string::npos;
233 }
234 
240  symbolt &class_symbol,
241  const struct_union_typet::componentst &components_to_add)
242 {
243  PRECONDITION(class_symbol.is_type);
244  PRECONDITION(class_symbol.type.id()==ID_struct);
245  struct_typet &struct_type=to_struct_type(class_symbol.type);
246  struct_typet::componentst &components=struct_type.components();
247 
248  for(const struct_union_typet::componentt &component : components_to_add)
249  {
250  components.push_back(component);
251  }
252 }
253 
259  irep_idt function_name,
260  const typet &type,
261  symbol_table_baset &symbol_table)
262 {
263  auxiliary_symbolt func_symbol;
264  func_symbol.base_name=function_name;
265  func_symbol.pretty_name=function_name;
266  func_symbol.is_static_lifetime=false;
267  func_symbol.mode=ID_java;
268  func_symbol.name=function_name;
269  func_symbol.type=type;
270  symbol_table.add(func_symbol);
271 }
272 
281  const irep_idt &function_name,
282  const exprt::operandst &arguments,
283  const typet &type,
284  symbol_table_baset &symbol_table)
285 {
286  // Names of function to call
287  std::string fun_name=id2string(function_name);
288 
289  // Declaring the function
290  declare_function(fun_name, type, symbol_table);
291 
292  // Function application
293  function_application_exprt call(symbol_exprt(fun_name), type);
294  call.arguments()=arguments;
295  return call;
296 }
297 
302 {
303  const std::string to_strip_str=id2string(to_strip);
304  const std::string prefix="java::";
305 
306  PRECONDITION(has_prefix(to_strip_str, prefix));
307  return to_strip_str.substr(prefix.size(), std::string::npos);
308 }
309 
314 // qualifiers, or the type as it was passed otherwise.
315 std::string pretty_print_java_type(const std::string &fqn_java_type)
316 {
317  std::string result(fqn_java_type);
318  const std::string java_cbmc_string("java::");
319  // Remove the CBMC internal java identifier
320  if(has_prefix(fqn_java_type, java_cbmc_string))
321  result = fqn_java_type.substr(java_cbmc_string.length());
322  // If the class is in package java.lang strip
323  // package name due to default import
324  const std::string java_lang_string("java.lang.");
325  if(has_prefix(result, java_lang_string))
326  result = result.substr(java_lang_string.length());
327  return result;
328 }
329 
346  const irep_idt &component_class_id,
347  const irep_idt &component_name,
348  const irep_idt &user_class_id,
349  const symbol_tablet &symbol_table,
350  const class_hierarchyt &class_hierarchy,
351  bool include_interfaces)
352 {
353  resolve_inherited_componentt component_resolver(
354  symbol_table, class_hierarchy);
355  const resolve_inherited_componentt::inherited_componentt resolved_component =
356  component_resolver(component_class_id, component_name, include_interfaces);
357 
358  // resolved_component is a pair (class-name, component-name) found by walking
359  // the chain of class inheritance (not interfaces!) and stopping on the first
360  // class that contains a component of equal name and type to `component_name`
361 
362  if(resolved_component.is_valid())
363  {
364  // Directly defined on the class referred to?
365  if(component_class_id == resolved_component.get_class_identifier())
366  return resolved_component;
367 
368  // No, may be inherited from some parent class; check it is visible:
369  const symbolt &component_symbol=
370  *symbol_table.lookup(resolved_component.get_full_component_identifier());
371 
372  irep_idt access = component_symbol.type.get(ID_access);
373  if(access.empty())
374  access = component_symbol.type.get(ID_C_access);
375 
376  if(access==ID_public || access==ID_protected)
377  {
378  // since the component is public, it is inherited
379  return resolved_component;
380  }
381 
382  // components with the default access modifier are only
383  // accessible within the same package.
384  if(access==ID_default)
385  {
386  const std::string &class_package=
387  java_class_to_package(id2string(component_class_id));
388  const std::string &component_package=
390  id2string(
391  resolved_component.get_class_identifier()));
392  if(component_package == class_package)
393  return resolved_component;
394  else
396  }
397 
398  if(access==ID_private)
399  {
400  // We return not-found because the component found by the
401  // component_resolver above proves that `component_name` cannot be
402  // inherited (assuming that the original Java code compiles). This is
403  // because, as we walk the inheritance chain for `classname` from Object
404  // to `classname`, a component can only become "more accessible". So, if
405  // the last occurrence is private, all others before must be private as
406  // well, and none is inherited in `classname`.
408  }
409 
410  UNREACHABLE; // Unexpected access modifier
411  }
412  else
413  {
415  }
416 }
417 
422 {
423  static const std::unordered_set<irep_idt> non_null_globals = {
424  "java::java.lang.System.out",
425  "java::java.lang.System.err",
426  "java::java.lang.System.in"};
427  return non_null_globals.count(symbolid);
428 }
429 
432 const std::unordered_set<std::string> cprover_methods_to_ignore
433 {
434  "nondetBoolean",
435  "nondetByte",
436  "nondetChar",
437  "nondetShort",
438  "nondetInt",
439  "nondetLong",
440  "nondetFloat",
441  "nondetDouble",
442  "nondetWithNull",
443  "nondetWithoutNull",
444  "notModelled",
445  "atomicBegin",
446  "atomicEnd",
447  "startThread",
448  "endThread",
449  "getCurrentThreadID"
450 };
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
#define JAVA_STRING_LITERAL_PREFIX
Definition: java_utils.h:51
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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
application of (mathematical) function
Definition: std_expr.h:4531
void java_root_class(symbolt &class_symbol)
irep_idt mode
Language mode.
Definition: symbol.h:52
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:116
bool java_is_array_type(const typet &type)
Definition: java_utils.cpp:23
const std::string java_class_to_package(const std::string &canonical_classname)
Definition: java_utils.cpp:61
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:4564
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:66
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:137
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
unsigned java_method_parameter_slots(const code_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call...
Definition: java_utils.cpp:51
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:200
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:189
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:301
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
Operator to dereference a pointer.
Definition: std_expr.h:3284
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:239
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:230
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:433
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:30
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:121
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:258
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
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:421
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:107
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:250
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:250
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:31
bool is_type
Definition: symbol.h:63
C++ class type.
Definition: std_types.h:341
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const irep_idt &user_class_id, 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:345
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::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:315
bool empty() const
Definition: dstring.h:61
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:214