cprover
array_pool.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String solver
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include "array_pool.h"
10 
12 operator()(const irep_idt &prefix, const typet &type)
13 {
14  std::ostringstream buf;
15  buf << "string_refinement#" << prefix << "#" << ++symbol_count;
16  irep_idt name(buf.str());
17  symbol_exprt result(name, type);
18 #ifdef DEBUG
19  created_symbols.push_back(result);
20 #endif
21  return result;
22 }
23 
25 {
26  if(const auto &if_expr = expr_try_dynamic_cast<if_exprt>((exprt)s))
27  {
28  return if_exprt{
29  if_expr->cond(),
30  get_or_create_length(to_array_string_expr(if_expr->true_case())),
31  get_or_create_length(to_array_string_expr(if_expr->false_case()))};
32  }
33 
34  auto emplace_result =
35  length_of_array.emplace(s, symbol_exprt(s.length_type()));
36  if(emplace_result.second)
37  {
38  emplace_result.first->second =
39  fresh_symbol("string_length", s.length_type());
40  }
41 
42  return emplace_result.first->second;
43 }
44 
47 {
48  auto find_result = length_of_array.find(s);
49  if(find_result != length_of_array.end())
50  return find_result->second;
51  return {};
52 }
53 
56 {
58  symbol_exprt content = fresh_symbol("string_content", array_type);
60  arrays_of_pointers.emplace(
62 
63  // add length to length_of_array map
65 
66  return str;
67 }
68 
73  const exprt &char_pointer,
74  const typet &char_array_type)
75 {
76  PRECONDITION(char_pointer.type().id() == ID_pointer);
77  PRECONDITION(char_array_type.id() == ID_array);
79  char_array_type.subtype().id() == ID_unsignedbv ||
80  char_array_type.subtype().id() == ID_signedbv);
81 
82  if(char_pointer.id() == ID_if)
83  {
84  const if_exprt &if_expr = to_if_expr(char_pointer);
85  const array_string_exprt t =
86  make_char_array_for_char_pointer(if_expr.true_case(), char_array_type);
87  const array_string_exprt f =
88  make_char_array_for_char_pointer(if_expr.false_case(), char_array_type);
89  const array_typet array_type(
90  char_array_type.subtype(),
91  if_exprt(
92  if_expr.cond(),
93  to_array_type(t.type()).size(),
94  to_array_type(f.type()).size()));
95  // BEWARE: this expression is possibly type-inconsistent and must not be
96  // used for any purposes other than passing it to concretization.
97  // Array if-exprts must be replaced (using substitute_array_access) before
98  // passing the lemmas to the solver.
99  return to_array_string_expr(if_exprt(if_expr.cond(), t, f, array_type));
100  }
101 
102  const bool is_constant_array =
103  char_pointer.id() == ID_address_of &&
104  to_address_of_expr(char_pointer).object().id() == ID_index &&
105  to_index_expr(to_address_of_expr(char_pointer).object()).array().id() ==
106  ID_array;
107 
108  if(is_constant_array)
109  {
110  return to_array_string_expr(
111  to_index_expr(to_address_of_expr(char_pointer).object()).array());
112  }
113  const std::string symbol_name = "char_array_" + id2string(char_pointer.id());
114  const auto array_sym =
115  to_array_string_expr(fresh_symbol(symbol_name, char_array_type));
116  const auto insert_result =
117  arrays_of_pointers.insert({char_pointer, array_sym});
118 
119  // add length to length_of_array map
120  get_or_create_length(array_sym);
121 
122  return to_array_string_expr(insert_result.first->second);
123 }
124 
134  const array_string_exprt &array_expr,
135  std::unordered_map<array_string_exprt, exprt, irep_hash> &length_of_array,
136  symbol_generatort &symbol_generator)
137 {
139  array_expr.id() != ID_if,
140  "attempt_assign_length_from_type does not handle if exprts");
141  // This invariant seems always true, but I don't know why.
142  // If we find a case where this is violated, try calling
143  // attempt_assign_length_from_type on the true and false cases.
144  const exprt &size_from_type = to_array_type(array_expr.type()).size();
145  const exprt &size_to_assign =
146  size_from_type != infinity_exprt(size_from_type.type())
147  ? size_from_type
148  : symbol_generator("string_length", array_expr.length_type());
149 
150  const auto emplace_result =
151  length_of_array.emplace(array_expr, size_to_assign);
152  INVARIANT(
153  emplace_result.second,
154  "attempt_assign_length_from_type should only be called when no entry"
155  "for the array_string_exprt exists in the length_of_array map");
156 }
157 
159  const exprt &pointer_expr,
160  const array_string_exprt &array_expr)
161 {
162  const auto it_bool =
163  arrays_of_pointers.insert(std::make_pair(pointer_expr, array_expr));
164 
165  INVARIANT(
166  it_bool.second, "should not associate two arrays to the same pointer");
167 
168  if(length_of_array.find(array_expr) == length_of_array.end())
169  {
171  }
172 }
173 
176 const std::unordered_map<array_string_exprt, exprt, irep_hash> &
178 {
179  return length_of_array;
180 }
181 
182 array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length)
183 {
184  const array_typet array_type(pointer.type().subtype(), length);
185  const array_string_exprt array =
186  make_char_array_for_char_pointer(pointer, array_type);
187  return array;
188 }
189 
191 {
192  const auto string_argument = expr_checked_cast<struct_exprt>(arg);
193  return array_pool.find(string_argument.op1(), string_argument.op0());
194 }
195 
197 {
199  const refined_string_exprt &str = to_string_expr(expr);
200  return array_pool.find(str.content(), str.length());
201 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
array_poolt::created_strings
const std::unordered_map< array_string_exprt, exprt, irep_hash > & created_strings() const
Return a map mapping all array_string_exprt of the array_pool to their length.
Definition: array_pool.cpp:177
array_string_exprt::length_type
const typet & length_type() const
Definition: string_expr.h:69
symbol_generatort::operator()
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
Generate a new symbol expression of the given type with some prefix.
Definition: array_pool.cpp:12
typet::subtype
const typet & subtype() const
Definition: type.h:47
attempt_assign_length_from_type
static void attempt_assign_length_from_type(const array_string_exprt &array_expr, std::unordered_map< array_string_exprt, exprt, irep_hash > &length_of_array, symbol_generatort &symbol_generator)
Given an array_string_exprt, get the size of the underlying array.
Definition: array_pool.cpp:133
array_pool.h
Associates arrays and length to pointers, so that the string refinement can transform builtin functio...
array_poolt::find
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: array_pool.cpp:182
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
to_string_expr
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:150
typet
The type of an expression, extends irept.
Definition: type.h:29
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
array_poolt
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:43
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
array_poolt::get_or_create_length
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:24
get_string_expr
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
Definition: array_pool.cpp:196
exprt
Base class for all expressions.
Definition: expr.h:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4111
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
refined_string_exprt
Definition: string_expr.h:109
refined_string_exprt::length
const exprt & length() const
Definition: string_expr.h:128
array_typet::size
const exprt & size() const
Definition: std_types.h:973
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
symbol_generatort
Generation of fresh symbols of a given type.
Definition: array_pool.h:23
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_array_string_expr
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:95
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
symbol_generatort::symbol_count
unsigned symbol_count
Definition: array_pool.h:32
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
refined_string_exprt::content
const exprt & content() const
Definition: string_expr.h:138
array_typet
Arrays with given size.
Definition: std_types.h:965
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
array_poolt::get_length_if_exists
optionalt< exprt > get_length_if_exists(const array_string_exprt &s) const
As opposed to get_length(), do not create a new symbol if the length of the array_string_exprt does n...
Definition: array_pool.cpp:46
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
array_poolt::fresh_symbol
symbol_generatort & fresh_symbol
Generate fresh symbols.
Definition: array_pool.h:102
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
is_refined_string_type
bool is_refined_string_type(const typet &type)
Definition: refined_string_type.h:52
array_poolt::length_of_array
std::unordered_map< array_string_exprt, exprt, irep_hash > length_of_array
Associate length to arrays of infinite size.
Definition: array_pool.h:99
of_argument
array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
Converts a struct containing a length and pointer to an array.
Definition: array_pool.cpp:190
array_poolt::make_char_array_for_char_pointer
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
Helper function for find.
Definition: array_pool.cpp:72
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
array_poolt::insert
void insert(const exprt &pointer_expr, const array_string_exprt &array)
Definition: array_pool.cpp:158
array_string_exprt
Definition: string_expr.h:67
array_poolt::arrays_of_pointers
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
Associate arrays to char pointers Invariant: Each array_string_exprt in this map has a corresponding ...
Definition: array_pool.h:96
validation_modet::INVARIANT
@ INVARIANT
array_poolt::fresh_string
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
Definition: array_pool.cpp:55