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
26bool is_java_string_type(const struct_typet &struct_type)
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
62get_java_primitive_type_info(const typet &maybe_primitive_type)
63{
64 static std::unordered_map<typet, java_primitive_type_infot, irep_hash>
65 type_info_by_primitive_type = {
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
104 auto found = type_info_by_primitive_type.find(maybe_primitive_type);
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
113bool is_primitive_wrapper_type_name(const std::string &type_name)
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())
151 slots+=java_local_variable_slots(p.type());
152
153 return slots;
154}
155
156const std::string java_class_to_package(const std::string &canonical_classname)
157{
158 return trim_from_last_delimiter(canonical_classname, '.');
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{
167 java_class_typet class_type;
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
210{
212}
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
273 const pointer_typet &given_pointer_type,
274 const java_class_typet &replacement_class_type)
275{
276 if(can_cast_type<struct_tag_typet>(given_pointer_type.base_type()))
277 {
278 struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
279 return pointer_type(struct_tag_subtype);
280 }
281 return pointer_type(replacement_class_type);
282}
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
313 PRECONDITION(open_char!=close_char);
314 PRECONDITION(src[open_pos]==open_char);
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
345 symbolt &class_symbol,
346 const struct_union_typet::componentst &components_to_add)
347{
348 PRECONDITION(class_symbol.is_type);
349 PRECONDITION(class_symbol.type.id()==ID_struct);
350 struct_typet &struct_type=to_struct_type(class_symbol.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{
366 auxiliary_symbolt func_symbol;
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,
400 mathematical_function_typet(std::move(argument_types), range),
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
415 PRECONDITION(has_prefix(to_strip_str, prefix));
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
429 if(has_prefix(fqn_java_type, java_cbmc_string))
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
452 const irep_idt &component_class_id,
453 const irep_idt &component_name,
454 const symbol_tablet &symbol_table,
455 bool include_interfaces)
456{
457 resolve_inherited_componentt component_resolver{symbol_table};
458 const auto resolved_component =
459 component_resolver(component_class_id, component_name, include_interfaces);
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
465 if(resolved_component)
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
475 irep_idt access = component_symbol.type.get(ID_access);
476 if(access.empty())
477 access = component_symbol.type.get(ID_C_access);
478
479 if(access==ID_public || access==ID_protected)
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=
490 java_class_to_package(id2string(component_class_id));
491 const std::string &component_package = java_class_to_package(
492 id2string(resolved_component->get_class_identifier()));
493 if(component_package == class_package)
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
578{
579 symbol.type.set(ID_C_class, declaring_class);
580}
581
583class_name_from_method_name(const std::string &method_name)
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
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 irept & find(const irep_idt &name) const
Definition irep.cpp:106
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
void set_is_stub(bool is_stub)
Definition java_types.h:393
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:557
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:564
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 ...
const typet & base_type() const
The type of the data what we point to.
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
void set_tag(const irep_idt &tag)
Definition std_types.h:169
const componentst & components() const
Definition std_types.h:147
bool has_component(const irep_idt &component_name) const
Definition std_types.h:157
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
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
bool is_static_lifetime
Definition symbol.h:65
bool is_type
Definition symbol.h:61
bool is_state_var
Definition symbol.h:62
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 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
nonstd::optional< T > optionalt
Definition optional.h:35
#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.
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:461
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