cprover
Loading...
Searching...
No Matches
java_utils.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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>
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
27{
29 struct_type) &&
30 struct_type.has_component("length") &&
31 struct_type.has_component("data");
32}
33
36{
37 static std::unordered_map<irep_idt, java_boxed_type_infot> type_info_by_name =
38 {
39 {"java::java.lang.Boolean",
40 {"java::java.lang.Boolean.booleanValue:()Z", java_boolean_type()}},
41 {"java::java.lang.Byte",
42 {"java::java.lang.Byte.byteValue:()B", java_byte_type()}},
43 {"java::java.lang.Character",
44 {"java::java.lang.Character.charValue:()C", java_char_type()}},
45 {"java::java.lang.Double",
46 {"java::java.lang.Double.doubleValue:()D", java_double_type()}},
47 {"java::java.lang.Float",
48 {"java::java.lang.Float.floatValue:()F", java_float_type()}},
49 {"java::java.lang.Integer",
50 {"java::java.lang.Integer.intValue:()I", java_int_type()}},
51 {"java::java.lang.Long",
52 {"java::java.lang.Long.longValue:()J", java_long_type()}},
53 {"java::java.lang.Short",
54 {"java::java.lang.Short.shortValue:()S", java_short_type()}},
55 };
56
57 auto found = type_info_by_name.find(type_name);
58 return found == type_info_by_name.end() ? nullptr : &found->second;
59}
60
63{
64 static std::unordered_map<typet, java_primitive_type_infot, irep_hash>
67 {"java::java.lang.Boolean",
68 "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;",
69 "java::java.lang.Boolean.booleanValue:()Z"}},
71 {"java::java.lang.Byte",
72 "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;",
73 "java::java.lang.Number.byteValue:()B"}},
75 {"java::java.lang.Character",
76 "java::java.lang.Character.valueOf:(C)"
77 "Ljava/lang/Character;",
78 "java::java.lang.Character.charValue:()C"}},
80 {"java::java.lang.Double",
81 "java::java.lang.Double.valueOf:(D)"
82 "Ljava/lang/Double;",
83 "java::java.lang.Number.doubleValue:()D"}},
85 {"java::java.lang.Float",
86 "java::java.lang.Float.valueOf:(F)"
87 "Ljava/lang/Float;",
88 "java::java.lang.Number.floatValue:()F"}},
90 {"java::java.lang.Integer",
91 "java::java.lang.Integer.valueOf:(I)"
92 "Ljava/lang/Integer;",
93 "java::java.lang.Number.intValue:()I"}},
95 {"java::java.lang.Long",
96 "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;",
97 "java::java.lang.Number.longValue:()J"}},
99 {"java::java.lang.Short",
100 "java::java.lang.Short.valueOf:(S)"
101 "Ljava/lang/Short;",
102 "java::java.lang.Number.shortValue:()S"}}};
103
105 return found == type_info_by_primitive_type.end() ? nullptr : &found->second;
106}
107
109{
110 return get_boxed_type_info_by_name(id) != nullptr;
111}
112
114{
115 static const std::unordered_set<std::string> primitive_wrapper_type_names = {
116 "java.lang.Boolean",
117 "java.lang.Byte",
118 "java.lang.Character",
119 "java.lang.Double",
120 "java.lang.Float",
121 "java.lang.Integer",
122 "java.lang.Long",
123 "java.lang.Short"};
124 return primitive_wrapper_type_names.count(type_name) > 0;
125}
126
128{
129
130 // Even on a 64-bit platform, Java pointers occupy one slot:
131 if(t.id()==ID_pointer)
132 return 1;
133
134 const std::size_t bitwidth = to_bitvector_type(t).get_width();
135 INVARIANT(
136 bitwidth==8 ||
137 bitwidth==16 ||
138 bitwidth==32 ||
139 bitwidth==64,
140 "all types constructed in java_types.cpp encode JVM types "
141 "with these bit widths");
142
143 return bitwidth == 64 ? 2u : 1u;
144}
145
147{
148 unsigned slots=0;
149
150 for(const auto &p : t.parameters())
152
153 return slots;
154}
155
156const std::string java_class_to_package(const std::string &canonical_classname)
157{
159}
160
162 const irep_idt &class_name,
163 symbol_table_baset &symbol_table,
164 message_handlert &message_handler,
165 const struct_union_typet::componentst &componentst)
166{
168
169 class_type.set_tag(class_name);
170 class_type.set_is_stub(true);
171
172 // produce class symbol
173 symbolt new_symbol;
174 new_symbol.base_name=class_name;
175 new_symbol.pretty_name=class_name;
176 new_symbol.name="java::"+id2string(class_name);
177 class_type.set_name(new_symbol.name);
178 new_symbol.type=class_type;
179 new_symbol.mode=ID_java;
180 new_symbol.is_type=true;
181
182 std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
183
184 if(!res.second)
185 {
186 messaget message(message_handler);
187 message.warning() <<
188 "stub class symbol " <<
189 new_symbol.name <<
190 " already exists" << messaget::eom;
191 }
192 else
193 {
194 // create the class identifier etc
195 java_root_class(res.first);
196 java_add_components_to_class(res.first, componentst);
197 }
198}
199
201 exprt &expr,
202 const source_locationt &source_location)
203{
204 expr.add_source_location().merge(source_location);
205 for(exprt &op : expr.operands())
206 merge_source_location_rec(op, source_location);
207}
208
213
215 const std::string &friendly_name,
216 const symbol_table_baset &symbol_table,
217 std::string &error)
218{
219 std::string qualified_name="java::"+friendly_name;
220 if(friendly_name.rfind(':')==std::string::npos)
221 {
222 std::string prefix=qualified_name+':';
223 std::set<irep_idt> matches;
224
225 for(const auto &s : symbol_table.symbols)
226 if(has_prefix(id2string(s.first), prefix) &&
227 s.second.type.id()==ID_code)
228 matches.insert(s.first);
229
230 if(matches.empty())
231 {
232 error="'"+friendly_name+"' not found";
233 return irep_idt();
234 }
235 else if(matches.size()>1)
236 {
237 std::ostringstream message;
238 message << "'"+friendly_name+"' is ambiguous between:";
239
240 // Trim java:: prefix so we can recommend an appropriate input:
241 for(const auto &s : matches)
242 message << "\n " << id2string(s).substr(6);
243
244 error=message.str();
245 return irep_idt();
246 }
247 else
248 {
249 return *matches.begin();
250 }
251 }
252 else
253 {
254 auto findit=symbol_table.symbols.find(qualified_name);
255 if(findit==symbol_table.symbols.end())
256 {
257 error="'"+friendly_name+"' not found";
258 return irep_idt();
259 }
260 else if(findit->second.type.id()!=ID_code)
261 {
262 error="'"+friendly_name+"' not a function";
263 return irep_idt();
264 }
265 else
266 {
267 return findit->first;
268 }
269 }
270}
271
283
285{
286 dereference_exprt result(expr);
287 // tag it so it's easy to identify during instrumentation
288 result.set(ID_java_member_access, true);
289 return result;
290}
291
306 const std::string &src,
307 size_t open_pos,
308 char open_char,
309 char close_char)
310{
311 // having the same opening and closing delimiter does not allow for hierarchic
312 // structuring
315 size_t c_pos=open_pos+1;
316 const size_t end_pos=src.size()-1;
317 size_t depth=0;
318
319 while(c_pos<=end_pos)
320 {
321 if(src[c_pos] == open_char)
322 depth++;
323 else if(src[c_pos] == close_char)
324 {
325 if(depth==0)
326 return c_pos;
327 depth--;
328 }
329 c_pos++;
330 // limit depth to sensible values
331 INVARIANT(
332 depth<=(src.size()-open_pos),
333 "No closing \'"+std::to_string(close_char)+
334 "\' found in signature to parse.");
335 }
336 // did not find corresponding closing '>'
337 return std::string::npos;
338}
339
347{
348 PRECONDITION(class_symbol.is_type);
351 struct_typet::componentst &components=struct_type.components();
352 components.insert(
353 components.end(), components_to_add.begin(), components_to_add.end());
354}
355
362 const irep_idt &function_name,
363 const mathematical_function_typet &type,
364 symbol_table_baset &symbol_table)
365{
367 func_symbol.base_name=function_name;
368 func_symbol.pretty_name=function_name;
369 func_symbol.is_static_lifetime=false;
370 func_symbol.is_state_var = false;
371 func_symbol.mode=ID_java;
372 func_symbol.name=function_name;
373 func_symbol.type=type;
374 symbol_table.add(func_symbol);
375
376 return func_symbol;
377}
378
388 const irep_idt &function_name,
389 const exprt::operandst &arguments,
390 const typet &range,
391 symbol_table_baset &symbol_table)
392{
393 std::vector<typet> argument_types;
394 for(const auto &arg : arguments)
395 argument_types.push_back(arg.type());
396
397 // Declaring the function
398 const auto symbol = declare_function(
399 function_name,
401 symbol_table);
402
403 // Function application
404 return function_application_exprt{symbol.symbol_expr(), arguments};
405}
406
411{
412 const std::string to_strip_str=id2string(to_strip);
413 const std::string prefix="java::";
414
416 return to_strip_str.substr(prefix.size(), std::string::npos);
417}
418
424std::string pretty_print_java_type(const std::string &fqn_java_type)
425{
426 std::string result(fqn_java_type);
427 const std::string java_cbmc_string("java::");
428 // Remove the CBMC internal java identifier
430 result = fqn_java_type.substr(java_cbmc_string.length());
431 // If the class is in package java.lang strip
432 // package name due to default import
433 const std::string java_lang_string("java.lang.");
434 if(has_prefix(result, java_lang_string))
435 result = result.substr(java_lang_string.length());
436 return result;
437}
438
453 const irep_idt &component_name,
454 const symbol_tablet &symbol_table,
456{
458 const auto resolved_component =
460
461 // resolved_component is a pair (class-name, component-name) found by walking
462 // the chain of class inheritance (not interfaces!) and stopping on the first
463 // class that contains a component of equal name and type to `component_name`
464
466 {
467 // Directly defined on the class referred to?
468 if(component_class_id == resolved_component->get_class_identifier())
469 return *resolved_component;
470
471 // No, may be inherited from some parent class; check it is visible:
472 const symbolt &component_symbol = symbol_table.lookup_ref(
473 resolved_component->get_full_component_identifier());
474
476 if(access.empty())
478
480 {
481 // since the component is public, it is inherited
482 return *resolved_component;
483 }
484
485 // components with the default access modifier are only
486 // accessible within the same package.
487 if(access==ID_default)
488 {
489 const std::string &class_package=
491 const std::string &component_package = java_class_to_package(
492 id2string(resolved_component->get_class_identifier()));
494 return *resolved_component;
495 else
496 return {};
497 }
498
499 if(access==ID_private)
500 {
501 // We return not-found because the component found by the
502 // component_resolver above proves that `component_name` cannot be
503 // inherited (assuming that the original Java code compiles). This is
504 // because, as we walk the inheritance chain for `classname` from Object
505 // to `classname`, a component can only become "more accessible". So, if
506 // the last occurrence is private, all others before must be private as
507 // well, and none is inherited in `classname`.
508 return {};
509 }
510
511 UNREACHABLE; // Unexpected access modifier
512 }
513 else
514 {
515 return {};
516 }
517}
518
523{
524 static const irep_idt in = "java::java.lang.System.in";
525 static const irep_idt out = "java::java.lang.System.out";
526 static const irep_idt err = "java::java.lang.System.err";
527 return symbolid == in || symbolid == out || symbolid == err;
528}
529
532const std::unordered_set<std::string> cprover_methods_to_ignore{
533 "nondetBoolean",
534 "nondetByte",
535 "nondetChar",
536 "nondetShort",
537 "nondetInt",
538 "nondetLong",
539 "nondetFloat",
540 "nondetDouble",
541 "nondetWithNull",
542 "nondetWithoutNull",
543 "notModelled",
544 "atomicBegin",
545 "atomicEnd",
546 "startThread",
547 "endThread",
548 "getCurrentThreadId",
549 "getMonitorCount"};
550
559 const typet &type,
560 const std::string &basename_prefix,
561 const source_locationt &source_location,
562 const irep_idt &function_name,
563 symbol_table_baset &symbol_table)
564{
565 PRECONDITION(!function_name.empty());
566 const std::string name_prefix = id2string(function_name);
568 type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
569}
570
572{
573 const irep_idt &class_id = symbol.type.get(ID_C_class);
574 return class_id.empty() ? optionalt<irep_idt>{} : class_id;
575}
576
581
584{
585 const auto signature_index = method_name.rfind(":");
586 const auto method_index = method_name.rfind(".", signature_index);
587 if(method_index == std::string::npos)
588 return {};
589 return method_name.substr(0, method_index);
590}
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:147
std::size_t get_width() const
Definition std_types.h:864
const parameterst & parameters() const
Definition std_types.h:655
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
operandst & operands()
Definition expr.h:92
source_locationt & add_source_location()
Definition expr.h:235
Application of (mathematical) function.
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
const irep_idt & id() const
Definition irep.h:396
static bool implements_java_char_sequence(const typet &type)
A type for mathematical functions (do not confuse with functions/methods in code)
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
Structure type, corresponds to C style structs.
Definition std_types.h:231
std::vector< componentt > componentst
Definition std_types.h:140
The symbol table base class interface.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_type
Definition symbol.h:61
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
irep_idt mode
Language mode.
Definition symbol.h:49
The type of an expression, extends irept.
Definition type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
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 ...
Fresh auxiliary symbol creation.
dstringt irep_idt
Definition irep.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
Produce code for simple implementation of String Java libraries.
signedbv_typet java_int_type()
signedbv_typet java_byte_type()
signedbv_typet java_short_type()
floatbv_typet java_double_type()
floatbv_typet java_float_type()
c_bool_typet java_boolean_type()
unsignedbv_typet java_char_type()
signedbv_typet java_long_type()
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.
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...
bool is_java_string_literal_id(const irep_idt &id)
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.
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.
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.
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
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...
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.
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.
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...
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.
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
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,...
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given 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)
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.
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
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.
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,...
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 ...
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
const std::string java_class_to_package(const std::string &canonical_classname)
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....
#define JAVA_STRING_LITERAL_PREFIX
Definition java_utils.h:104
API to expression classes for 'mathematical' expressions.
Mathematical types.
#define NODISCARD
Definition nodiscard.h:22
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
std::string trim_from_last_delimiter(const std::string &s, const char delim)
Return type for get_boxed_type_info_by_name.
Definition java_utils.h:54
Return type for get_java_primitive_type_info.
Definition java_utils.h:34