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_root_class.h"
10
11#include <util/fresh_symbol.h>
12#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>
20
22#include "java_utils.h"
23
24#include <set>
25#include <unordered_set>
26
27bool is_java_string_type(const struct_typet &struct_type)
28{
30 struct_type) &&
31 struct_type.has_component("length") &&
32 struct_type.has_component("data");
33}
34
37{
38 static std::unordered_map<irep_idt, java_boxed_type_infot> type_info_by_name =
39 {
40 {"java::java.lang.Boolean",
41 {"java::java.lang.Boolean.booleanValue:()Z", java_boolean_type()}},
42 {"java::java.lang.Byte",
43 {"java::java.lang.Byte.byteValue:()B", java_byte_type()}},
44 {"java::java.lang.Character",
45 {"java::java.lang.Character.charValue:()C", java_char_type()}},
46 {"java::java.lang.Double",
47 {"java::java.lang.Double.doubleValue:()D", java_double_type()}},
48 {"java::java.lang.Float",
49 {"java::java.lang.Float.floatValue:()F", java_float_type()}},
50 {"java::java.lang.Integer",
51 {"java::java.lang.Integer.intValue:()I", java_int_type()}},
52 {"java::java.lang.Long",
53 {"java::java.lang.Long.longValue:()J", java_long_type()}},
54 {"java::java.lang.Short",
55 {"java::java.lang.Short.shortValue:()S", java_short_type()}},
56 };
57
58 auto found = type_info_by_name.find(type_name);
59 return found == type_info_by_name.end() ? nullptr : &found->second;
60}
61
63get_java_primitive_type_info(const typet &maybe_primitive_type)
64{
65 static std::unordered_map<typet, java_primitive_type_infot, irep_hash>
66 type_info_by_primitive_type = {
68 {"java::java.lang.Boolean",
69 "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;",
70 "java::java.lang.Boolean.booleanValue:()Z"}},
72 {"java::java.lang.Byte",
73 "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;",
74 "java::java.lang.Number.byteValue:()B"}},
76 {"java::java.lang.Character",
77 "java::java.lang.Character.valueOf:(C)"
78 "Ljava/lang/Character;",
79 "java::java.lang.Character.charValue:()C"}},
81 {"java::java.lang.Double",
82 "java::java.lang.Double.valueOf:(D)"
83 "Ljava/lang/Double;",
84 "java::java.lang.Number.doubleValue:()D"}},
86 {"java::java.lang.Float",
87 "java::java.lang.Float.valueOf:(F)"
88 "Ljava/lang/Float;",
89 "java::java.lang.Number.floatValue:()F"}},
91 {"java::java.lang.Integer",
92 "java::java.lang.Integer.valueOf:(I)"
93 "Ljava/lang/Integer;",
94 "java::java.lang.Number.intValue:()I"}},
96 {"java::java.lang.Long",
97 "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;",
98 "java::java.lang.Number.longValue:()J"}},
100 {"java::java.lang.Short",
101 "java::java.lang.Short.valueOf:(S)"
102 "Ljava/lang/Short;",
103 "java::java.lang.Number.shortValue:()S"}}};
104
105 auto found = type_info_by_primitive_type.find(maybe_primitive_type);
106 return found == type_info_by_primitive_type.end() ? nullptr : &found->second;
107}
108
110{
111 return get_boxed_type_info_by_name(id) != nullptr;
112}
113
114bool is_primitive_wrapper_type_name(const std::string &type_name)
115{
116 static const std::unordered_set<std::string> primitive_wrapper_type_names = {
117 "java.lang.Boolean",
118 "java.lang.Byte",
119 "java.lang.Character",
120 "java.lang.Double",
121 "java.lang.Float",
122 "java.lang.Integer",
123 "java.lang.Long",
124 "java.lang.Short"};
125 return primitive_wrapper_type_names.count(type_name) > 0;
126}
127
129{
130
131 // Even on a 64-bit platform, Java pointers occupy one slot:
132 if(t.id()==ID_pointer)
133 return 1;
134
135 const std::size_t bitwidth = to_bitvector_type(t).get_width();
136 INVARIANT(
137 bitwidth==8 ||
138 bitwidth==16 ||
139 bitwidth==32 ||
140 bitwidth==64,
141 "all types constructed in java_types.cpp encode JVM types "
142 "with these bit widths");
143
144 return bitwidth == 64 ? 2u : 1u;
145}
146
148{
149 unsigned slots=0;
150
151 for(const auto &p : t.parameters())
152 slots+=java_local_variable_slots(p.type());
153
154 return slots;
155}
156
157const std::string java_class_to_package(const std::string &canonical_classname)
158{
159 return trim_from_last_delimiter(canonical_classname, '.');
160}
161
163 const irep_idt &class_name,
164 symbol_table_baset &symbol_table,
165 message_handlert &message_handler,
166 const struct_union_typet::componentst &componentst)
167{
168 java_class_typet class_type;
169
170 class_type.set_tag(class_name);
171 class_type.set_is_stub(true);
172
173 // produce class symbol
174 irep_idt qualified_class_name = "java::" + id2string(class_name);
175 class_type.set_name(qualified_class_name);
176 type_symbolt new_symbol{qualified_class_name, std::move(class_type), ID_java};
177 new_symbol.base_name=class_name;
178 new_symbol.pretty_name=class_name;
179
180 std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
181
182 if(!res.second)
183 {
184 messaget message(message_handler);
185 message.warning() <<
186 "stub class symbol " <<
187 new_symbol.name <<
188 " already exists" << messaget::eom;
189 }
190 else
191 {
192 // create the class identifier etc
193 java_root_class(res.first);
194 java_add_components_to_class(res.first, componentst);
195 }
196}
197
199 exprt &expr,
200 const source_locationt &source_location)
201{
202 expr.add_source_location().merge(source_location);
203 for(exprt &op : expr.operands())
204 merge_source_location_rec(op, source_location);
205}
206
208{
209 return id.starts_with(JAVA_STRING_LITERAL_PREFIX);
210}
211
213 const std::string &friendly_name,
214 const symbol_table_baset &symbol_table,
215 std::string &error)
216{
217 std::string qualified_name="java::"+friendly_name;
218 if(friendly_name.rfind(':')==std::string::npos)
219 {
220 std::string prefix=qualified_name+':';
221 std::set<irep_idt> matches;
222
223 for(const auto &s : symbol_table.symbols)
224 if(s.first.starts_with(prefix) && s.second.type.id() == ID_code)
225 matches.insert(s.first);
226
227 if(matches.empty())
228 {
229 error="'"+friendly_name+"' not found";
230 return irep_idt();
231 }
232 else if(matches.size()>1)
233 {
234 std::ostringstream message;
235 message << "'"+friendly_name+"' is ambiguous between:";
236
237 // Trim java:: prefix so we can recommend an appropriate input:
238 for(const auto &s : matches)
239 message << "\n " << id2string(s).substr(6);
240
241 error=message.str();
242 return irep_idt();
243 }
244 else
245 {
246 return *matches.begin();
247 }
248 }
249 else
250 {
251 auto findit=symbol_table.symbols.find(qualified_name);
252 if(findit==symbol_table.symbols.end())
253 {
254 error="'"+friendly_name+"' not found";
255 return irep_idt();
256 }
257 else if(findit->second.type.id()!=ID_code)
258 {
259 error="'"+friendly_name+"' not a function";
260 return irep_idt();
261 }
262 else
263 {
264 return findit->first;
265 }
266 }
267}
268
270 const pointer_typet &given_pointer_type,
271 const java_class_typet &replacement_class_type)
272{
273 if(can_cast_type<struct_tag_typet>(given_pointer_type.base_type()))
274 {
275 struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
276 return pointer_type(struct_tag_subtype);
277 }
278 return pointer_type(replacement_class_type);
279}
280
282{
283 dereference_exprt result(expr);
284 // tag it so it's easy to identify during instrumentation
285 result.set(ID_java_member_access, true);
286 return result;
287}
288
303 const std::string &src,
304 size_t open_pos,
305 char open_char,
306 char close_char)
307{
308 // having the same opening and closing delimiter does not allow for hierarchic
309 // structuring
310 PRECONDITION(open_char!=close_char);
311 PRECONDITION(src[open_pos]==open_char);
312 size_t c_pos=open_pos+1;
313 const size_t end_pos=src.size()-1;
314 size_t depth=0;
315
316 while(c_pos<=end_pos)
317 {
318 if(src[c_pos] == open_char)
319 depth++;
320 else if(src[c_pos] == close_char)
321 {
322 if(depth==0)
323 return c_pos;
324 depth--;
325 }
326 c_pos++;
327 // limit depth to sensible values
328 INVARIANT(
329 depth<=(src.size()-open_pos),
330 "No closing \'"+std::to_string(close_char)+
331 "\' found in signature to parse.");
332 }
333 // did not find corresponding closing '>'
334 return std::string::npos;
335}
336
342 symbolt &class_symbol,
343 const struct_union_typet::componentst &components_to_add)
344{
345 PRECONDITION(class_symbol.is_type);
346 PRECONDITION(class_symbol.type.id()==ID_struct);
347 struct_typet &struct_type=to_struct_type(class_symbol.type);
348 struct_typet::componentst &components=struct_type.components();
349 components.insert(
350 components.end(), components_to_add.begin(), components_to_add.end());
351}
352
359 const irep_idt &function_name,
360 const mathematical_function_typet &type,
361 symbol_table_baset &symbol_table)
362{
363 auxiliary_symbolt func_symbol;
364 func_symbol.base_name=function_name;
365 func_symbol.pretty_name=function_name;
366 func_symbol.is_static_lifetime=false;
367 func_symbol.is_state_var = false;
368 func_symbol.mode=ID_java;
369 func_symbol.name=function_name;
370 func_symbol.type=type;
371 symbol_table.add(func_symbol);
372
373 return func_symbol;
374}
375
385 const irep_idt &function_name,
386 const exprt::operandst &arguments,
387 const typet &range,
388 symbol_table_baset &symbol_table)
389{
390 std::vector<typet> argument_types;
391 for(const auto &arg : arguments)
392 argument_types.push_back(arg.type());
393
394 // Declaring the function
395 const auto symbol = declare_function(
396 function_name,
397 mathematical_function_typet(std::move(argument_types), range),
398 symbol_table);
399
400 // Function application
401 return function_application_exprt{symbol.symbol_expr(), arguments};
402}
403
408{
409 const std::string to_strip_str=id2string(to_strip);
410 const std::string prefix="java::";
411
412 PRECONDITION(has_prefix(to_strip_str, prefix));
413 return to_strip_str.substr(prefix.size(), std::string::npos);
414}
415
421std::string pretty_print_java_type(const std::string &fqn_java_type)
422{
423 std::string result(fqn_java_type);
424 const std::string java_cbmc_string("java::");
425 // Remove the CBMC internal java identifier
426 if(has_prefix(fqn_java_type, java_cbmc_string))
427 result = fqn_java_type.substr(java_cbmc_string.length());
428 // If the class is in package java.lang strip
429 // package name due to default import
430 const std::string java_lang_string("java.lang.");
431 if(has_prefix(result, java_lang_string))
432 result = result.substr(java_lang_string.length());
433 return result;
434}
435
447std::optional<resolve_inherited_componentt::inherited_componentt>
449 const irep_idt &component_class_id,
450 const irep_idt &component_name,
451 const symbol_table_baset &symbol_table,
452 bool include_interfaces)
453{
454 resolve_inherited_componentt component_resolver{symbol_table};
455 const auto resolved_component =
456 component_resolver(component_class_id, component_name, include_interfaces);
457
458 // resolved_component is a pair (class-name, component-name) found by walking
459 // the chain of class inheritance (not interfaces!) and stopping on the first
460 // class that contains a component of equal name and type to `component_name`
461
462 if(resolved_component)
463 {
464 // Directly defined on the class referred to?
465 if(component_class_id == resolved_component->get_class_identifier())
466 return *resolved_component;
467
468 // No, may be inherited from some parent class; check it is visible:
469 const symbolt &component_symbol = symbol_table.lookup_ref(
470 resolved_component->get_full_component_identifier());
471
472 irep_idt access = component_symbol.type.get(ID_access);
473 if(access.empty())
474 access = component_symbol.type.get(ID_C_access);
475
476 if(access==ID_public || access==ID_protected)
477 {
478 // since the component is public, it is inherited
479 return *resolved_component;
480 }
481
482 // components with the default access modifier are only
483 // accessible within the same package.
484 if(access==ID_default)
485 {
486 const std::string &class_package=
487 java_class_to_package(id2string(component_class_id));
488 const std::string &component_package = java_class_to_package(
489 id2string(resolved_component->get_class_identifier()));
490 if(component_package == class_package)
491 return *resolved_component;
492 else
493 return {};
494 }
495
496 if(access==ID_private)
497 {
498 // We return not-found because the component found by the
499 // component_resolver above proves that `component_name` cannot be
500 // inherited (assuming that the original Java code compiles). This is
501 // because, as we walk the inheritance chain for `classname` from Object
502 // to `classname`, a component can only become "more accessible". So, if
503 // the last occurrence is private, all others before must be private as
504 // well, and none is inherited in `classname`.
505 return {};
506 }
507
508 UNREACHABLE; // Unexpected access modifier
509 }
510 else
511 {
512 return {};
513 }
514}
515
520{
521 static const irep_idt in = "java::java.lang.System.in";
522 static const irep_idt out = "java::java.lang.System.out";
523 static const irep_idt err = "java::java.lang.System.err";
524 return symbolid == in || symbolid == out || symbolid == err;
525}
526
529const std::unordered_set<std::string> cprover_methods_to_ignore{
530 "nondetBoolean",
531 "nondetByte",
532 "nondetChar",
533 "nondetShort",
534 "nondetInt",
535 "nondetLong",
536 "nondetFloat",
537 "nondetDouble",
538 "nondetWithNull",
539 "nondetWithoutNull",
540 "notModelled",
541 "atomicBegin",
542 "atomicEnd",
543 "startThread",
544 "endThread",
545 "getCurrentThreadId",
546 "getMonitorCount"};
547
556 const typet &type,
557 const std::string &basename_prefix,
558 const source_locationt &source_location,
559 const irep_idt &function_name,
560 symbol_table_baset &symbol_table)
561{
562 PRECONDITION(!function_name.empty());
563 const std::string name_prefix = id2string(function_name);
565 type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
566}
567
568std::optional<irep_idt> declaring_class(const symbolt &symbol)
569{
570 const irep_idt &class_id = symbol.type.get(ID_C_class);
571 return class_id.empty() ? std::optional<irep_idt>{} : class_id;
572}
573
575{
576 symbol.type.set(ID_C_class, declaring_class);
577}
578
579[[nodiscard]] std::optional<std::string>
580class_name_from_method_name(const std::string &method_name)
581{
582 const auto signature_index = method_name.rfind(":");
583 const auto method_index = method_name.rfind(".", signature_index);
584 if(method_index == std::string::npos)
585 return {};
586 return method_name.substr(0, method_index);
587}
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:235
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:153
std::size_t get_width() const
Definition std_types.h:920
const parameterst & parameters() const
Definition std_types.h:699
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:38
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:236
Application of (mathematical) function.
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
void set_is_stub(bool is_stub)
Definition java_types.h:392
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:556
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:563
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:154
mstreamt & warning() const
Definition message.h:396
static eomt eom
Definition message.h:289
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:493
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
std::vector< componentt > componentst
Definition std_types.h:140
bool has_component(const irep_idt &component_name) const
Definition std_types.h:157
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.
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:70
bool is_type
Definition symbol.h:61
bool is_state_var
Definition symbol.h:66
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
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition symbol.h:139
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.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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()
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...
std::optional< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
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...
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,...
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 ...
std::optional< 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.
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::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_table_baset &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
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:103
API to expression classes for 'mathematical' expressions.
Mathematical types.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#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:505
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:53
Return type for get_java_primitive_type_info.
Definition java_utils.h:33
Author: Diffblue Ltd.
dstringt irep_idt