cprover
string_refinement_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String solver
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 #include <algorithm>
12 #include <functional>
13 #include <iostream>
14 #include <numeric>
15 #include <unordered_set>
16 #include <util/arith_tools.h>
17 #include <util/expr_iterator.h>
18 #include <util/expr_util.h>
19 #include <util/graph.h>
20 #include <util/magic.h>
21 #include <util/make_unique.h>
22 #include <util/ssa_expr.h>
23 #include <util/std_expr.h>
24 #include <util/unicode.h>
25 
26 bool is_char_type(const typet &type)
27 {
28  return type.id() == ID_unsignedbv && to_unsignedbv_type(type).get_width() <=
30 }
31 
32 bool is_char_array_type(const typet &type, const namespacet &ns)
33 {
34  if(type.id() == ID_struct_tag)
35  return is_char_array_type(ns.follow_tag(to_struct_tag_type(type)), ns);
36  return type.id() == ID_array && is_char_type(type.subtype());
37 }
38 
39 bool is_char_pointer_type(const typet &type)
40 {
41  return type.id() == ID_pointer && is_char_type(type.subtype());
42 }
43 
44 bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
45 {
46  return has_subtype(type, is_char_pointer_type, ns);
47 }
48 
49 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
50 {
51  return has_subexpr(
52  expr, [&](const exprt &e) { return is_char_array_type(e.type(), ns); });
53 }
54 
55 std::string
56 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
57 {
58  for(const auto &op : arr.operands())
59  PRECONDITION(op.id() == ID_constant);
60 
61  std::wstring out(length, '?');
62 
63  for(std::size_t i = 0; i < arr.operands().size() && i < length; i++)
64  out[i] = numeric_cast_v<unsigned>(to_constant_expr(arr.operands()[i]));
65 
67 }
68 
70 {
71  auto ref = std::ref(static_cast<const exprt &>(expr));
72  while(can_cast_expr<with_exprt>(ref.get()))
73  {
74  const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
75  const auto current_index =
76  numeric_cast_v<std::size_t>(to_constant_expr(with_expr.where()));
77  entries[current_index] = with_expr.new_value();
78  ref = with_expr.old();
79  }
80 
81  // This function only handles 'with' and 'array_of' expressions
82  PRECONDITION(ref.get().id() == ID_array_of);
83  default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
84 }
85 
87  const with_exprt &expr,
88  const exprt &index)
89 {
90  sparse_arrayt sparse_array(expr);
91 
92  return std::accumulate(
93  sparse_array.entries.begin(),
94  sparse_array.entries.end(),
95  sparse_array.default_value,
96  [&](
97  const exprt if_expr,
98  const std::pair<std::size_t, exprt> &entry) { // NOLINT
99  const exprt entry_index = from_integer(entry.first, index.type());
100  const exprt &then_expr = entry.second;
101  CHECK_RETURN(then_expr.type() == if_expr.type());
102  const equal_exprt index_equal(index, entry_index);
103  return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
104  });
105 }
106 
108 {
109  return std::accumulate(
110  entries.rbegin(),
111  entries.rend(),
113  [&](
114  const exprt if_expr,
115  const std::pair<std::size_t, exprt> &entry) { // NOLINT
116  const exprt entry_index = from_integer(entry.first, index.type());
117  const exprt &then_expr = entry.second;
118  CHECK_RETURN(then_expr.type() == if_expr.type());
119  const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
120  return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
121  });
122 }
123 
125  const array_exprt &expr,
126  const exprt &extra_value)
127  : sparse_arrayt(extra_value)
128 {
129  const auto &operands = expr.operands();
130  exprt last_added = extra_value;
131  for(std::size_t i = 0; i < operands.size(); ++i)
132  {
133  const std::size_t index = operands.size() - 1 - i;
134  if(operands[index].id() != ID_unknown && operands[index] != last_added)
135  {
136  entries[index] = operands[index];
137  last_added = operands[index];
138  }
139  }
140 }
141 
143  const array_list_exprt &expr,
144  const exprt &extra_value)
145  : interval_sparse_arrayt(extra_value)
146 {
147  PRECONDITION(expr.operands().size() % 2 == 0);
148  for(std::size_t i = 0; i < expr.operands().size(); i += 2)
149  {
150  const auto index = numeric_cast<std::size_t>(expr.operands()[i]);
151  INVARIANT(
152  expr.operands()[i + 1].type() == extra_value.type(),
153  "all values in array should have the same type");
154  if(index.has_value() && expr.operands()[i + 1].id() != ID_unknown)
155  entries[*index] = expr.operands()[i + 1];
156  }
157 }
158 
160 interval_sparse_arrayt::of_expr(const exprt &expr, const exprt &extra_value)
161 {
162  if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(expr))
163  return interval_sparse_arrayt(*array_expr, extra_value);
164  if(const auto &with_expr = expr_try_dynamic_cast<with_exprt>(expr))
165  return interval_sparse_arrayt(*with_expr);
166  if(const auto &array_list = expr_try_dynamic_cast<array_list_exprt>(expr))
167  return interval_sparse_arrayt(*array_list, extra_value);
168  return {};
169 }
170 
171 exprt interval_sparse_arrayt::at(const std::size_t index) const
172 {
173  // First element at or after index
174  const auto it = entries.lower_bound(index);
175  return it != entries.end() ? it->second : default_value;
176 }
177 
179  std::size_t size,
180  const typet &index_type) const
181 {
182  const array_typet array_type(
184  array_exprt array({}, array_type);
185  array.operands().reserve(size);
186 
187  auto it = entries.begin();
188  for(; it != entries.end() && it->first < size; ++it)
189  array.operands().resize(it->first + 1, it->second);
190 
191  array.operands().resize(
192  size, it == entries.end() ? default_value : it->second);
193  return array;
194 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
typet::subtype
const typet & subtype() const
Definition: type.h:47
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:139
arith_tools.h
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
typet
The type of an expression, extends irept.
Definition: type.h:29
sparse_arrayt
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
Definition: string_refinement_util.h:75
is_char_type
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
Definition: string_refinement_util.cpp:26
interval_sparse_arrayt
Represents arrays by the indexes up to which the value remains the same.
Definition: string_refinement_util.h:100
interval_sparse_arrayt::to_if_expression
exprt to_if_expression(const exprt &index) const
Definition: string_refinement_util.cpp:107
exprt
Base class for all expressions.
Definition: expr.h:53
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
interval_sparse_arrayt::of_expr
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor,...
Definition: string_refinement_util.cpp:160
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
magic.h
Magic numbers used throughout the codebase.
utf16_constant_array_to_java
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
Definition: string_refinement_util.cpp:56
sparse_arrayt::sparse_arrayt
sparse_arrayt(const with_exprt &expr)
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ....
Definition: string_refinement_util.cpp:69
sparse_arrayt::to_if_expression
static exprt to_if_expression(const with_exprt &expr, const exprt &index)
Creates an if_expr corresponding to the result of accessing the array at the given index.
Definition: string_refinement_util.cpp:86
sparse_arrayt::default_value
exprt default_value
Definition: string_refinement_util.h:88
interval_sparse_arrayt::interval_sparse_arrayt
interval_sparse_arrayt(const with_exprt &expr)
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for ...
Definition: string_refinement_util.h:106
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
interval_sparse_arrayt::at
exprt at(std::size_t index) const
Get the value at the specified index.
Definition: string_refinement_util.cpp:171
is_char_pointer_type
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
Definition: string_refinement_util.cpp:39
make_unique.h
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
STRING_REFINEMENT_MAX_CHAR_WIDTH
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH
Definition: magic.h:12
string_refinement_util.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
has_subtype
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Definition: expr_util.cpp:153
utf16_native_endian_to_java_string
static void utf16_native_endian_to_java_string(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
Escapes non-printable characters, whitespace except for spaces, double quotes and backslashes.
Definition: unicode.cpp:274
is_char_array_type
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
Definition: string_refinement_util.cpp:32
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
string_format_builtin_function.h
Built-in function for String.format.
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
expr_util.h
Deprecated expression utility functions.
ssa_expr.h
interval_sparse_arrayt::concretize
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
Definition: string_refinement_util.cpp:178
graph.h
A Template Class for Graphs.
array_typet
Arrays with given size.
Definition: std_types.h:965
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
has_char_pointer_subtype
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
Definition: string_refinement_util.cpp:44
sparse_arrayt::entries
std::map< std::size_t, exprt > entries
Definition: string_refinement_util.h:89
unicode.h
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1478
exprt::operands
operandst & operands()
Definition: expr.h:95
std_expr.h
API to expression classes.
has_char_array_subexpr
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
Definition: string_refinement_util.cpp:49
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
can_cast_expr< with_exprt >
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3092
validation_modet::INVARIANT
@ INVARIANT
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939