cprover
string_constraint_generator_transformation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for string transformations,
4  that is, functions taking one string and returning another
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
16 
17 #include <util/arith_tools.h>
18 
38 std::pair<exprt, string_constraintst>
41 {
42  PRECONDITION(f.arguments().size() == 4);
43  string_constraintst constraints;
44  const array_string_exprt res =
45  array_pool.find(f.arguments()[1], f.arguments()[0]);
47  const exprt &k = f.arguments()[3];
48  const typet &index_type = s1.length_type();
49  const typet &char_type = s1.content().type().subtype();
50 
51  // We add axioms:
52  // a1 : |res|=max(k, 0)
53  // a2 : forall i< min(|s1|, k) .res[i] = s1[i]
54  // a3 : forall |s1| <= i < |res|. res[i] = 0
55 
56  constraints.existential.push_back(
58 
59  const symbol_exprt idx = fresh_symbol("QA_index_set_length", index_type);
60  const string_constraintt a2(
61  idx,
63  equal_exprt(s1[idx], res[idx]));
64  constraints.universal.push_back(a2);
65 
66  symbol_exprt idx2 = fresh_symbol("QA_index_set_length2", index_type);
68  idx2,
71  equal_exprt(res[idx2], from_integer(0, char_type)));
72  constraints.universal.push_back(a3);
73 
74  return {from_integer(0, get_return_code_type()), std::move(constraints)};
75 }
76 
79 // NOLINTNEXTLINE
81 // NOLINTNEXTLINE
93 std::pair<exprt, string_constraintst>
96 {
98  PRECONDITION(args.size() == 4 || args.size() == 5);
99  const array_string_exprt str = get_string_expr(array_pool, args[2]);
100  const array_string_exprt res = array_pool.find(args[1], args[0]);
101  const exprt &i = args[3];
102  const exprt j =
103  args.size() == 5 ? args[4] : array_pool.get_or_create_length(str);
104  return add_axioms_for_substring(res, str, i, j);
105 }
106 
121 std::pair<exprt, string_constraintst>
123  const array_string_exprt &res,
124  const array_string_exprt &str,
125  const exprt &start,
126  const exprt &end)
127 {
128  const typet &index_type = str.length_type();
129  PRECONDITION(start.type() == index_type);
130  PRECONDITION(end.type() == index_type);
131 
132  string_constraintst constraints;
133  const exprt start1 = maximum(start, from_integer(0, start.type()));
134  const exprt end1 =
135  maximum(minimum(end, array_pool.get_or_create_length(str)), start1);
136 
137  // Axiom 1.
138  constraints.existential.push_back(equal_exprt(
139  array_pool.get_or_create_length(res), minus_exprt(end1, start1)));
140 
141  // Axiom 2.
142  constraints.universal.push_back([&] {
143  const symbol_exprt idx = fresh_symbol("QA_index_substring", index_type);
144  return string_constraintt(
145  idx,
147  equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
148  }());
149 
150  return {from_integer(0, get_return_code_type()), std::move(constraints)};
151 }
152 
179 std::pair<exprt, string_constraintst>
182 {
183  PRECONDITION(f.arguments().size() == 3);
184  string_constraintst constraints;
186  const array_string_exprt &res =
187  array_pool.find(f.arguments()[1], f.arguments()[0]);
188  const typet &index_type = str.length_type();
189  const typet &char_type = str.content().type().subtype();
190  const symbol_exprt idx = fresh_symbol("index_trim", index_type);
191  const exprt space_char = from_integer(' ', char_type);
192 
193  // Axiom 1.
194  constraints.existential.push_back(greater_or_equal_to(
197 
198  binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type));
199  constraints.existential.push_back(a2);
200 
201  const exprt a3 =
203  constraints.existential.push_back(a3);
204 
205  const exprt a4 = greater_or_equal_to(
207  constraints.existential.push_back(a4);
208 
209  const exprt a5 = less_than_or_equal_to(
211  constraints.existential.push_back(a5);
212 
213  symbol_exprt n = fresh_symbol("QA_index_trim", index_type);
214  binary_relation_exprt non_print(str[n], ID_le, space_char);
215  string_constraintt a6(n, zero_if_negative(idx), non_print);
216  constraints.universal.push_back(a6);
217 
218  // Axiom 7.
219  constraints.universal.push_back([&] {
220  const symbol_exprt n2 = fresh_symbol("QA_index_trim2", index_type);
221  const minus_exprt bound(
224  const binary_relation_exprt eqn2(
225  str[plus_exprt(
226  idx, plus_exprt(array_pool.get_or_create_length(res), n2))],
227  ID_le,
228  space_char);
229  return string_constraintt(n2, zero_if_negative(bound), eqn2);
230  }());
231 
232  symbol_exprt n3 = fresh_symbol("QA_index_trim3", index_type);
233  equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
236  constraints.universal.push_back(a8);
237 
238  // Axiom 9.
239  constraints.existential.push_back([&] {
240  const plus_exprt index_before(
241  idx,
242  minus_exprt(
244  const binary_relation_exprt no_space_before(
245  str[index_before], ID_gt, space_char);
246  return or_exprt(
248  and_exprt(
249  binary_relation_exprt(str[idx], ID_gt, space_char), no_space_before));
250  }());
251  return {from_integer(0, f.type()), constraints};
252 }
253 
266  exprt expr1,
267  exprt expr2,
268  std::function<array_string_exprt(const exprt &)> get_string_expr,
269  array_poolt &array_pool)
270 {
271  if(
272  (expr1.type().id() == ID_unsignedbv || expr1.type().id() == ID_char) &&
273  (expr2.type().id() == ID_char || expr2.type().id() == ID_unsignedbv))
274  return std::make_pair(expr1, expr2);
275  const auto expr1_str = get_string_expr(expr1);
276  const auto expr2_str = get_string_expr(expr2);
277  const auto expr1_length =
278  numeric_cast<std::size_t>(array_pool.get_or_create_length(expr1_str));
279  const auto expr2_length =
280  numeric_cast<std::size_t>(array_pool.get_or_create_length(expr2_str));
281  if(expr1_length && expr2_length && *expr1_length == 1 && *expr2_length == 1)
282  return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
283  return {};
284 }
285 
305 std::pair<exprt, string_constraintst>
308 {
309  PRECONDITION(f.arguments().size() == 5);
310  string_constraintst constraints;
312  array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]);
313  if(
314  const auto maybe_chars = to_char_pair(
315  f.arguments()[3],
316  f.arguments()[4],
317  [&](const exprt &e) { return get_string_expr(array_pool, e); },
318  array_pool))
319  {
320  const auto old_char = maybe_chars->first;
321  const auto new_char = maybe_chars->second;
322 
323  constraints.existential.push_back(equal_exprt(
326 
327  symbol_exprt qvar = fresh_symbol("QA_replace", str.length_type());
328  implies_exprt case1(
329  equal_exprt(str[qvar], old_char), equal_exprt(res[qvar], new_char));
330  implies_exprt case2(
331  not_exprt(equal_exprt(str[qvar], old_char)),
332  equal_exprt(res[qvar], str[qvar]));
334  qvar,
336  and_exprt(case1, case2));
337  constraints.universal.push_back(a2);
338  return {from_integer(0, f.type()), std::move(constraints)};
339  }
340  return {from_integer(1, f.type()), std::move(constraints)};
341 }
342 
347 std::pair<exprt, string_constraintst>
350 {
351  PRECONDITION(f.arguments().size() == 4);
352  const array_string_exprt res =
353  array_pool.find(f.arguments()[1], f.arguments()[0]);
355  exprt index_one = from_integer(1, str.length_type());
356  return add_axioms_for_delete(
357  res, str, f.arguments()[3], plus_exprt(f.arguments()[3], index_one));
358 }
359 
374 std::pair<exprt, string_constraintst>
376  const array_string_exprt &res,
377  const array_string_exprt &str,
378  const exprt &start,
379  const exprt &end)
380 {
381  PRECONDITION(start.type() == str.length_type());
382  PRECONDITION(end.type() == str.length_type());
383  const typet &index_type = str.length_type();
384  const typet &char_type = str.content().type().subtype();
385  const array_string_exprt sub1 =
387  const array_string_exprt sub2 =
389  return combine_results(
391  sub1, str, from_integer(0, str.length_type()), start),
394  sub2, str, end, array_pool.get_or_create_length(str)),
395  add_axioms_for_concat(res, sub1, sub2)));
396 }
397 
400 // NOLINTNEXTLINE
402 // NOLINTNEXTLINE
409 std::pair<exprt, string_constraintst>
412 {
413  PRECONDITION(f.arguments().size() == 5);
414  const array_string_exprt res =
415  array_pool.find(f.arguments()[1], f.arguments()[0]);
417  return add_axioms_for_delete(res, arg, f.arguments()[3], f.arguments()[4]);
418 }
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
array_string_exprt::length_type
const typet & length_type() const
Definition: string_expr.h:69
typet::subtype
const typet & subtype() const
Definition: type.h:47
greater_or_equal_to
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:19
string_constraint_generatort::add_axioms_for_substring
std::pair< exprt, string_constraintst > add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start,...
Definition: string_constraint_generator_transformation.cpp:122
arith_tools.h
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
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:395
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
array_poolt
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:43
string_constraintt
Definition: string_constraint.h:60
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:56
string_constraint_generatort::add_axioms_for_delete
std::pair< exprt, string_constraintst > add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
Definition: string_constraint_generator_transformation.cpp:375
string_constraint_generatort::add_axioms_for_trim
std::pair< exprt, string_constraintst > add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
Definition: string_constraint_generator_transformation.cpp:180
and_exprt
Boolean AND.
Definition: std_expr.h:2137
s1
int8_t s1
Definition: bytecode_info.h:59
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
string_refinement_invariant.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:36
array_string_exprt::content
exprt & content()
Definition: string_expr.h:74
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1190
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: mathematical_expr.h:193
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:400
string_constraint_generatort::add_axioms_for_replace
std::pair< exprt, string_constraintst > add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
Definition: string_constraint_generator_transformation.cpp:306
or_exprt
Boolean OR.
Definition: std_expr.h:2245
to_char_pair
static optionalt< std::pair< exprt, exprt > > to_char_pair(exprt expr1, exprt expr2, std::function< array_string_exprt(const exprt &)> get_string_expr, array_poolt &array_pool)
Convert two expressions to pair of chars If both expressions are characters, return pair of them If b...
Definition: string_constraint_generator_transformation.cpp:265
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
string_constraint_generatort::add_axioms_for_delete_char_at
std::pair< exprt, string_constraintst > add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
Definition: string_constraint_generator_transformation.cpp:348
less_than_or_equal_to
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:36
irept::id
const irep_idt & id() const
Definition: irep.h:418
string_constraint_generatort::add_axioms_for_set_length
std::pair< exprt, string_constraintst > add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
Definition: string_constraint_generator_transformation.cpp:39
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
get_return_code_type
signedbv_typet get_return_code_type()
Definition: string_constraint_generator_main.cpp:180
minus_exprt
Binary minus.
Definition: std_expr.h:940
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:408
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
string_constraint_generatort::combine_results
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
Definition: string_constraint_generator_main.cpp:416
string_constraint_generatort::add_axioms_for_concat
std::pair< exprt, string_constraintst > add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
Definition: string_concatenation_builtin_function.cpp:158
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
equal_to
equal_exprt equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:54
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
array_string_exprt
Definition: string_expr.h:67
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
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:37
not_exprt
Boolean negation.
Definition: std_expr.h:2843
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:38