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
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
59 return found == type_info_by_name.end() ? nullptr : &found->second;
60}
61
64{
65 static std::unordered_map<typet, java_primitive_type_infot, irep_hash>
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
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
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())
153
154 return slots;
155}
156
157const std::string java_class_to_package(const std::string &canonical_classname)
158{
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{
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);
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
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(has_prefix(id2string(s.first), prefix) &&
225 s.second.type.id()==ID_code)
226 matches.insert(s.first);
227
228 if(matches.empty())
229 {
230 error="'"+friendly_name+"' not found";
231 return irep_idt();
232 }
233 else if(matches.size()>1)
234 {
235 std::ostringstream message;
236 message << "'"+friendly_name+"' is ambiguous between:";
237
238 // Trim java:: prefix so we can recommend an appropriate input:
239 for(const auto &s : matches)
240 message << "\n " << id2string(s).substr(6);
241
242 error=message.str();
243 return irep_idt();
244 }
245 else
246 {
247 return *matches.begin();
248 }
249 }
250 else
251 {
252 auto findit=symbol_table.symbols.find(qualified_name);
253 if(findit==symbol_table.symbols.end())
254 {
255 error="'"+friendly_name+"' not found";
256 return irep_idt();
257 }
258 else if(findit->second.type.id()!=ID_code)
259 {
260 error="'"+friendly_name+"' not a function";
261 return irep_idt();
262 }
263 else
264 {
265 return findit->first;
266 }
267 }
268}
269
281
283{
284 dereference_exprt result(expr);
285 // tag it so it's easy to identify during instrumentation
286 result.set(ID_java_member_access, true);
287 return result;
288}
289
304 const std::string &src,
305 size_t open_pos,
306 char open_char,
307 char close_char)
308{
309 // having the same opening and closing delimiter does not allow for hierarchic
310 // structuring
313 size_t c_pos=open_pos+1;
314 const size_t end_pos=src.size()-1;
315 size_t depth=0;
316
317 while(c_pos<=end_pos)
318 {
319 if(src[c_pos] == open_char)
320 depth++;
321 else if(src[c_pos] == close_char)
322 {
323 if(depth==0)
324 return c_pos;
325 depth--;
326 }
327 c_pos++;
328 // limit depth to sensible values
329 INVARIANT(
330 depth<=(src.size()-open_pos),
331 "No closing \'"+std::to_string(close_char)+
332 "\' found in signature to parse.");
333 }
334 // did not find corresponding closing '>'
335 return std::string::npos;
336}
337
345{
346 PRECONDITION(class_symbol.is_type);
349 struct_typet::componentst &components=struct_type.components();
350 components.insert(
351 components.end(), components_to_add.begin(), components_to_add.end());
352}
353
360 const irep_idt &function_name,
361 const mathematical_function_typet &type,
362 symbol_table_baset &symbol_table)
363{
365 func_symbol.base_name=function_name;
366 func_symbol.pretty_name=function_name;
367 func_symbol.is_static_lifetime=false;
368 func_symbol.is_state_var = false;
369 func_symbol.mode=ID_java;
370 func_symbol.name=function_name;
371 func_symbol.type=type;
372 symbol_table.add(func_symbol);
373
374 return func_symbol;
375}
376
386 const irep_idt &function_name,
387 const exprt::operandst &arguments,
388 const typet &range,
389 symbol_table_baset &symbol_table)
390{
391 std::vector<typet> argument_types;
392 for(const auto &arg : arguments)
393 argument_types.push_back(arg.type());
394
395 // Declaring the function
396 const auto symbol = declare_function(
397 function_name,
399 symbol_table);
400
401 // Function application
402 return function_application_exprt{symbol.symbol_expr(), arguments};
403}
404
409{
410 const std::string to_strip_str=id2string(to_strip);
411 const std::string prefix="java::";
412
414 return to_strip_str.substr(prefix.size(), std::string::npos);
415}
416
422std::string pretty_print_java_type(const std::string &fqn_java_type)
423{
424 std::string result(fqn_java_type);
425 const std::string java_cbmc_string("java::");
426 // Remove the CBMC internal java identifier
428 result = fqn_java_type.substr(java_cbmc_string.length());
429 // If the class is in package java.lang strip
430 // package name due to default import
431 const std::string java_lang_string("java.lang.");
432 if(has_prefix(result, java_lang_string))
433 result = result.substr(java_lang_string.length());
434 return result;
435}
436
451 const irep_idt &component_name,
452 const symbol_table_baset &symbol_table,
454{
456 const auto resolved_component =
458
459 // resolved_component is a pair (class-name, component-name) found by walking
460 // the chain of class inheritance (not interfaces!) and stopping on the first
461 // class that contains a component of equal name and type to `component_name`
462
464 {
465 // Directly defined on the class referred to?
466 if(component_class_id == resolved_component->get_class_identifier())
467 return *resolved_component;
468
469 // No, may be inherited from some parent class; check it is visible:
470 const symbolt &component_symbol = symbol_table.lookup_ref(
471 resolved_component->get_full_component_identifier());
472
474 if(access.empty())
476
478 {
479 // since the component is public, it is inherited
480 return *resolved_component;
481 }
482
483 // components with the default access modifier are only
484 // accessible within the same package.
485 if(access==ID_default)
486 {
487 const std::string &class_package=
489 const std::string &component_package = java_class_to_package(
490 id2string(resolved_component->get_class_identifier()));
492 return *resolved_component;
493 else
494 return {};
495 }
496
497 if(access==ID_private)
498 {
499 // We return not-found because the component found by the
500 // component_resolver above proves that `component_name` cannot be
501 // inherited (assuming that the original Java code compiles). This is
502 // because, as we walk the inheritance chain for `classname` from Object
503 // to `classname`, a component can only become "more accessible". So, if
504 // the last occurrence is private, all others before must be private as
505 // well, and none is inherited in `classname`.
506 return {};
507 }
508
509 UNREACHABLE; // Unexpected access modifier
510 }
511 else
512 {
513 return {};
514 }
515}
516
521{
522 static const irep_idt in = "java::java.lang.System.in";
523 static const irep_idt out = "java::java.lang.System.out";
524 static const irep_idt err = "java::java.lang.System.err";
525 return symbolid == in || symbolid == out || symbolid == err;
526}
527
530const std::unordered_set<std::string> cprover_methods_to_ignore{
531 "nondetBoolean",
532 "nondetByte",
533 "nondetChar",
534 "nondetShort",
535 "nondetInt",
536 "nondetLong",
537 "nondetFloat",
538 "nondetDouble",
539 "nondetWithNull",
540 "nondetWithoutNull",
541 "notModelled",
542 "atomicBegin",
543 "atomicEnd",
544 "startThread",
545 "endThread",
546 "getCurrentThreadId",
547 "getMonitorCount"};
548
557 const typet &type,
558 const std::string &basename_prefix,
559 const source_locationt &source_location,
560 const irep_idt &function_name,
561 symbol_table_baset &symbol_table)
562{
563 PRECONDITION(!function_name.empty());
564 const std::string name_prefix = id2string(function_name);
566 type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
567}
568
570{
571 const irep_idt &class_id = symbol.type.get(ID_C_class);
572 return class_id.empty() ? optionalt<irep_idt>{} : class_id;
573}
574
579
582{
583 const auto signature_index = method_name.rfind(":");
584 const auto method_index = method_name.rfind(".", signature_index);
585 if(method_index == std::string::npos)
586 return {};
587 return method_name.substr(0, method_index);
588}
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:240
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:153
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:39
bool empty() const
Definition dstring.h:90
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:228
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: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.
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
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: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...
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.
optionalt< 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.
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: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.
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
Author: Diffblue Ltd.
dstringt irep_idt