cprover
java_string_literals.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java string literal processing
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include "java_string_literals.h"
10 #include "java_root_class.h"
11 #include "java_types.h"
12 #include "java_utils.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/expr_initializer.h>
16 #include <util/namespace.h>
17 #include <util/unicode.h>
18 
19 #include <iomanip>
20 #include <sstream>
21 
26 static std::string escape_non_alnum(const std::string &to_escape)
27 {
28  std::ostringstream escaped;
29  for(auto &ch : to_escape)
30  {
31  if(ch=='_')
32  escaped << "__";
33  else if(isalnum(ch))
34  escaped << ch;
35  else
36  escaped << '_'
37  << std::hex
38  << std::setfill('0')
39  << std::setw(2)
40  << (unsigned int)ch;
41  }
42  return escaped.str();
43 }
44 
48 static array_exprt utf16_to_array(const std::wstring &in)
49 {
50  const auto jchar=java_char_type();
51  array_exprt ret(
52  array_typet(jchar, from_integer(in.length(), java_int_type())));
53  for(const auto c : in)
54  ret.copy_to_operands(from_integer(c, jchar));
55  return ret;
56 }
57 
67  const exprt &string_expr,
68  symbol_table_baset &symbol_table,
69  bool string_refinement_enabled)
70 {
71  PRECONDITION(string_expr.id() == ID_java_string_literal);
72  const irep_idt value = string_expr.get(ID_value);
73  const struct_tag_typet string_type("java::java.lang.String");
74 
75  const std::string escaped_symbol_name = escape_non_alnum(id2string(value));
76  const std::string escaped_symbol_name_with_prefix =
77  JAVA_STRING_LITERAL_PREFIX "." + escaped_symbol_name;
78 
79  auto findit = symbol_table.symbols.find(escaped_symbol_name_with_prefix);
80  if(findit != symbol_table.symbols.end())
81  return findit->second.symbol_expr();
82 
83  // Create a new symbol:
84  symbolt new_symbol;
85  new_symbol.name = escaped_symbol_name_with_prefix;
86  new_symbol.type = string_type;
87  new_symbol.type.set(ID_C_constant, true);
88  new_symbol.base_name = escaped_symbol_name;
89  new_symbol.pretty_name = value;
90  new_symbol.mode = ID_java;
91  new_symbol.is_type = false;
92  new_symbol.is_lvalue = true;
93  new_symbol.is_static_lifetime = true;
94 
95  namespacet ns(symbol_table);
96 
97  // Regardless of string refinement setting, at least initialize
98  // the literal with @clsid = String
99  struct_tag_typet jlo_symbol("java::java.lang.Object");
100  const auto &jlo_struct = to_struct_type(ns.follow(jlo_symbol));
101  struct_exprt jlo_init(jlo_symbol);
102  const auto &jls_struct = to_struct_type(ns.follow(string_type));
103  java_root_class_init(jlo_init, jlo_struct, "java::java.lang.String");
104 
105  // If string refinement *is* around, populate the actual
106  // contents as well:
107  if(string_refinement_enabled)
108  {
109  const array_exprt data =
111 
112  struct_exprt literal_init(new_symbol.type);
113  literal_init.operands().resize(jls_struct.components().size());
114  const std::size_t jlo_nb = jls_struct.component_number("@java.lang.Object");
115  literal_init.operands()[jlo_nb] = jlo_init;
116 
117  const std::size_t length_nb = jls_struct.component_number("length");
118  const typet &length_type = jls_struct.components()[length_nb].type();
119  const exprt length = from_integer(data.operands().size(), length_type);
120  literal_init.operands()[length_nb] = length;
121 
122  // Initialize the string with a constant utf-16 array:
123  symbolt array_symbol;
124  array_symbol.name = escaped_symbol_name_with_prefix + "_constarray";
125  array_symbol.base_name = escaped_symbol_name + "_constarray";
126  array_symbol.pretty_name = value;
127  array_symbol.mode = ID_java;
128  array_symbol.is_type = false;
129  array_symbol.is_lvalue = true;
130  // These are basically const global data:
131  array_symbol.is_static_lifetime = true;
132  array_symbol.is_state_var = true;
133  array_symbol.value = data;
134  array_symbol.type = array_symbol.value.type();
135  array_symbol.type.set(ID_C_constant, true);
136 
137  if(symbol_table.add(array_symbol))
138  throw "failed to add constarray symbol to symbol table";
139 
140  const symbol_exprt array_expr = array_symbol.symbol_expr();
141  const address_of_exprt array_pointer(
142  index_exprt(array_expr, from_integer(0, java_int_type())));
143 
144  const std::size_t data_nb = jls_struct.component_number("data");
145  literal_init.operands()[data_nb] = array_pointer;
146 
147  // Associate array with pointer
148  symbolt return_symbol;
149  return_symbol.name = escaped_symbol_name_with_prefix + "_return_value";
150  return_symbol.base_name = escaped_symbol_name + "_return_value";
151  return_symbol.pretty_name =
152  escaped_symbol_name.length() > 10
153  ? escaped_symbol_name.substr(0, 10) + "..._return_value"
154  : escaped_symbol_name + "_return_value";
155  return_symbol.mode = ID_java;
156  return_symbol.is_type = false;
157  return_symbol.is_lvalue = true;
158  return_symbol.is_static_lifetime = true;
159  return_symbol.is_state_var = true;
160  return_symbol.value = make_function_application(
161  ID_cprover_associate_array_to_pointer_func,
162  {array_symbol.value, array_pointer},
163  java_int_type(),
164  symbol_table);
165  return_symbol.type = return_symbol.value.type();
166  return_symbol.type.set(ID_C_constant, true);
167  if(symbol_table.add(return_symbol))
168  throw "failed to add return symbol to symbol table";
169 
170  // Initialise the literal structure with
171  // (ABC_return_value, { ..., .length = N, .data = &ABC_constarray }),
172  // using a C-style comma expression to indicate that we need the
173  // _return_value global for its side-effects.
174  exprt init_comma_expr(ID_comma);
175  init_comma_expr.type() = literal_init.type();
176  init_comma_expr.copy_to_operands(return_symbol.symbol_expr());
177  init_comma_expr.move_to_operands(literal_init);
178  new_symbol.value = init_comma_expr;
179  }
180  else if(jls_struct.components().size()>=1 &&
181  jls_struct.components()[0].get_name()=="@java.lang.Object")
182  {
183  // Case where something defined java.lang.String, so it has
184  // a proper base class (always java.lang.Object in practical
185  // JDKs seen so far)
186  struct_exprt literal_init(new_symbol.type);
187  literal_init.move_to_operands(jlo_init);
188  for(const auto &comp : jls_struct.components())
189  {
190  if(comp.get_name()=="@java.lang.Object")
191  continue;
192  // Other members of JDK's java.lang.String we don't understand
193  // without string-refinement. Just zero-init them; consider using
194  // test-gen-like nondet object trees instead.
195  const auto init =
196  zero_initializer(comp.type(), string_expr.source_location(), ns);
197  CHECK_RETURN(init.has_value());
198  literal_init.copy_to_operands(*init);
199  }
200  new_symbol.value = literal_init;
201  }
202  else if(to_java_class_type(jls_struct).get_is_stub())
203  {
204  // Case where java.lang.String was stubbed, and so directly defines
205  // @class_identifier
206  new_symbol.value = jlo_init;
207  }
208 
209  bool add_failed = symbol_table.add(new_symbol);
210  INVARIANT(
211  !add_failed,
212  "string literal symbol was already checked not to be "
213  "in the symbol table, so adding it should succeed");
214 
215  return new_symbol.symbol_expr();
216 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
java_root_class_init
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
Definition: java_root_class.cpp:43
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
exprt::move_to_operands
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Definition: expr.cpp:29
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:61
java_root_class.h
utf16_to_array
static array_exprt utf16_to_array(const std::wstring &in)
Convert UCS-2 or UTF-16 to an array expression.
Definition: java_string_literals.cpp:48
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
java_int_type
typet java_int_type()
Definition: java_types.cpp:32
java_string_literals.h
typet
The type of an expression, extends irept.
Definition: type.h:27
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
data
Definition: kdev_t.h:24
exprt
Base class for all expressions.
Definition: expr.h:54
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
namespace.h
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:322
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1920
make_function_application
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
Create a function application expression.
Definition: java_utils.cpp:275
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
expr_initializer.h
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
data::size
int size
Definition: kdev_t.h:25
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
escape_non_alnum
static std::string escape_non_alnum(const std::string &to_escape)
Replace non-alphanumeric characters with _xx escapes, where xx are hex digits.
Definition: java_string_literals.cpp:26
irept::id
const irep_idt & id() const
Definition: irep.h:259
utf8_to_utf16_native_endian
std::wstring utf8_to_utf16_native_endian(const std::string &in)
Convert UTF8-encoded string to UTF-16 with architecture-native endianness.
Definition: unicode.cpp:196
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
array_typet
Arrays with given size.
Definition: std_types.h:1000
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
symbolt::is_type
bool is_type
Definition: symbol.h:61
unicode.h
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
java_char_type
typet java_char_type()
Definition: java_types.cpp:57
get_or_create_string_literal_symbol
symbol_exprt get_or_create_string_literal_symbol(const exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
Definition: java_string_literals.cpp:66
exprt::operands
operandst & operands()
Definition: expr.h:78
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
index_exprt
Array index operator.
Definition: std_expr.h:1595
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
java_types.h
java_utils.h
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
JAVA_STRING_LITERAL_PREFIX
#define JAVA_STRING_LITERAL_PREFIX
Definition: java_utils.h:53
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470