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 #include <util/arith_tools.h>
17 
37 std::pair<exprt, string_constraintst> add_axioms_for_set_length(
38  symbol_generatort &fresh_symbol,
40  array_poolt &array_pool)
41 {
42  PRECONDITION(f.arguments().size() == 4);
43  string_constraintst constraints;
44  const array_string_exprt res =
45  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
46  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
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|=k
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(length_eq(res, k));
57 
58  const symbol_exprt idx = fresh_symbol("QA_index_set_length", index_type);
59  const string_constraintt a2(
60  idx,
61  zero_if_negative(minimum(s1.length(), k)),
62  equal_exprt(s1[idx], res[idx]));
63  constraints.universal.push_back(a2);
64 
65  symbol_exprt idx2 = fresh_symbol("QA_index_set_length2", index_type);
67  idx2,
68  zero_if_negative(s1.length()),
69  zero_if_negative(res.length()),
70  equal_exprt(res[idx2], from_integer(0, char_type)));
71  constraints.universal.push_back(a3);
72 
73  return {from_integer(0, get_return_code_type()), std::move(constraints)};
74 }
75 
78 // NOLINTNEXTLINE
80 // NOLINTNEXTLINE
94 std::pair<exprt, string_constraintst> add_axioms_for_substring(
95  symbol_generatort &fresh_symbol,
97  array_poolt &array_pool)
98 {
100  PRECONDITION(args.size() == 4 || args.size() == 5);
101  const array_string_exprt str = get_string_expr(array_pool, args[2]);
102  const array_string_exprt res =
103  char_array_of_pointer(array_pool, args[1], args[0]);
104  const exprt &i = args[3];
105  const exprt j = args.size() == 5 ? args[4] : str.length();
106  return add_axioms_for_substring(fresh_symbol, res, str, i, j);
107 }
108 
124 std::pair<exprt, string_constraintst> add_axioms_for_substring(
125  symbol_generatort &fresh_symbol,
126  const array_string_exprt &res,
127  const array_string_exprt &str,
128  const exprt &start,
129  const exprt &end)
130 {
131  const typet &index_type = str.length().type();
132  PRECONDITION(start.type()==index_type);
133  PRECONDITION(end.type()==index_type);
134 
135  string_constraintst constraints;
136  const exprt start1 = maximum(start, from_integer(0, start.type()));
137  const exprt end1 = maximum(minimum(end, str.length()), start1);
138 
139  // Axiom 1.
140  constraints.existential.push_back(
141  equal_exprt(res.length(), minus_exprt(end1, start1)));
142 
143  // Axiom 2.
144  constraints.universal.push_back([&] {
145  const symbol_exprt idx = fresh_symbol("QA_index_substring", index_type);
146  return string_constraintt(
147  idx,
148  zero_if_negative(res.length()),
149  equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
150  }());
151 
152  return {from_integer(0, get_return_code_type()), std::move(constraints)};
153 }
154 
183 std::pair<exprt, string_constraintst> add_axioms_for_trim(
184  symbol_generatort &fresh_symbol,
186  array_poolt &array_pool)
187 {
188  PRECONDITION(f.arguments().size() == 3);
189  string_constraintst constraints;
190  const array_string_exprt &str = get_string_expr(array_pool, f.arguments()[2]);
191  const array_string_exprt &res =
192  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
193  const typet &index_type = str.length().type();
194  const typet &char_type = str.content().type().subtype();
195  const symbol_exprt idx = fresh_symbol("index_trim", index_type);
196  const exprt space_char = from_integer(' ', char_type);
197 
198  // Axiom 1.
199  constraints.existential.push_back(
200  length_ge(str, plus_exprt(idx, res.length())));
201 
202  binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type));
203  constraints.existential.push_back(a2);
204 
205  const exprt a3 = length_ge(str, idx);
206  constraints.existential.push_back(a3);
207 
208  const exprt a4 = length_ge(res, from_integer(0, index_type));
209  constraints.existential.push_back(a4);
210 
211  const exprt a5 = length_le(res, str.length());
212  constraints.existential.push_back(a5);
213 
214  symbol_exprt n = fresh_symbol("QA_index_trim", index_type);
215  binary_relation_exprt non_print(str[n], ID_le, space_char);
216  string_constraintt a6(n, zero_if_negative(idx), non_print);
217  constraints.universal.push_back(a6);
218 
219  // Axiom 7.
220  constraints.universal.push_back([&] {
221  const symbol_exprt n2 = fresh_symbol("QA_index_trim2", index_type);
222  const minus_exprt bound(minus_exprt(str.length(), idx), res.length());
223  const binary_relation_exprt eqn2(
224  str[plus_exprt(idx, plus_exprt(res.length(), n2))], ID_le, space_char);
225  return string_constraintt(n2, zero_if_negative(bound), eqn2);
226  }());
227 
228  symbol_exprt n3 = fresh_symbol("QA_index_trim3", index_type);
229  equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
230  string_constraintt a8(n3, zero_if_negative(res.length()), eqn3);
231  constraints.universal.push_back(a8);
232 
233  // Axiom 9.
234  constraints.existential.push_back([&] {
235  const plus_exprt index_before(
236  idx, minus_exprt(res.length(), from_integer(1, index_type)));
237  const binary_relation_exprt no_space_before(
238  str[index_before], ID_gt, space_char);
239  return or_exprt(
240  equal_exprt(idx, str.length()),
241  and_exprt(
242  binary_relation_exprt(str[idx], ID_gt, space_char), no_space_before));
243  }());
244  return {from_integer(0, f.type()), constraints};
245 }
246 
258  exprt expr1,
259  exprt expr2,
260  std::function<array_string_exprt(const exprt &)> get_string_expr)
261 {
262  if((expr1.type().id()==ID_unsignedbv
263  || expr1.type().id()==ID_char)
264  && (expr2.type().id()==ID_char
265  || expr2.type().id()==ID_unsignedbv))
266  return std::make_pair(expr1, expr2);
267  const auto expr1_str = get_string_expr(expr1);
268  const auto expr2_str = get_string_expr(expr2);
269  const auto expr1_length = numeric_cast<std::size_t>(expr1_str.length());
270  const auto expr2_length = numeric_cast<std::size_t>(expr2_str.length());
271  if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
272  return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
273  return { };
274 }
275 
297 std::pair<exprt, string_constraintst> add_axioms_for_replace(
298  symbol_generatort &fresh_symbol,
300  array_poolt &array_pool)
301 {
302  PRECONDITION(f.arguments().size() == 5);
303  string_constraintst constraints;
304  array_string_exprt str = get_string_expr(array_pool, f.arguments()[2]);
305  array_string_exprt res =
306  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
307  if(
308  const auto maybe_chars =
309  to_char_pair(f.arguments()[3], f.arguments()[4], [&](const exprt &e) {
310  return get_string_expr(array_pool, e);
311  }))
312  {
313  const auto old_char=maybe_chars->first;
314  const auto new_char=maybe_chars->second;
315 
316  constraints.existential.push_back(equal_exprt(res.length(), str.length()));
317 
318  symbol_exprt qvar = fresh_symbol("QA_replace", str.length().type());
319  implies_exprt case1(
320  equal_exprt(str[qvar], old_char),
321  equal_exprt(res[qvar], new_char));
322  implies_exprt case2(
323  not_exprt(equal_exprt(str[qvar], old_char)),
324  equal_exprt(res[qvar], str[qvar]));
326  qvar, zero_if_negative(res.length()), and_exprt(case1, case2));
327  constraints.universal.push_back(a2);
328  return {from_integer(0, f.type()), std::move(constraints)};
329  }
330  return {from_integer(1, f.type()), std::move(constraints)};
331 }
332 
339 std::pair<exprt, string_constraintst> add_axioms_for_delete_char_at(
340  symbol_generatort &fresh_symbol,
342  array_poolt &array_pool)
343 {
344  PRECONDITION(f.arguments().size() == 4);
345  const array_string_exprt res =
346  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
347  const array_string_exprt str = get_string_expr(array_pool, f.arguments()[2]);
348  exprt index_one=from_integer(1, str.length().type());
349  return add_axioms_for_delete(
350  fresh_symbol,
351  res,
352  str,
353  f.arguments()[3],
354  plus_exprt(f.arguments()[3], index_one),
355  array_pool);
356 }
357 
374 std::pair<exprt, string_constraintst> add_axioms_for_delete(
375  symbol_generatort &fresh_symbol,
376  const array_string_exprt &res,
377  const array_string_exprt &str,
378  const exprt &start,
379  const exprt &end,
380  array_poolt &array_pool)
381 {
382  PRECONDITION(start.type()==str.length().type());
383  PRECONDITION(end.type()==str.length().type());
384  const typet &index_type = str.length().type();
385  const typet &char_type = str.content().type().subtype();
386  const array_string_exprt sub1 =
387  array_pool.fresh_string(index_type, char_type);
388  const array_string_exprt sub2 =
389  array_pool.fresh_string(index_type, char_type);
390  return combine_results(
392  fresh_symbol, sub1, str, from_integer(0, str.length().type()), start),
394  add_axioms_for_substring(fresh_symbol, sub2, str, end, str.length()),
395  add_axioms_for_concat(fresh_symbol, res, sub1, sub2)));
396 }
397 
400 // NOLINTNEXTLINE
402 // NOLINTNEXTLINE
412 std::pair<exprt, string_constraintst> add_axioms_for_delete(
413  symbol_generatort &fresh_symbol,
415  array_poolt &array_pool)
416 {
417  PRECONDITION(f.arguments().size() == 5);
418  const array_string_exprt res =
419  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
420  const array_string_exprt arg = get_string_expr(array_pool, f.arguments()[2]);
421  return add_axioms_for_delete(
422  fresh_symbol, res, arg, f.arguments()[3], f.arguments()[4], array_pool);
423 }
function_application_exprt::arguments
argumentst & arguments()
Definition: std_expr.h:4506
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
length_ge
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
Definition: string_expr.h:21
length_eq
equal_exprt length_eq(const T &lhs, const exprt &rhs)
Definition: string_expr.h:54
arith_tools.h
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:578
add_axioms_for_substring
std::pair< exprt, string_constraintst > add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Substring of a string between two indices.
Definition: string_constraint_generator_transformation.cpp:94
add_axioms_for_trim
std::pair< exprt, string_constraintst > add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Remove leading and trailing whitespaces.
Definition: string_constraint_generator_transformation.cpp:183
typet
The type of an expression, extends irept.
Definition: type.h:27
add_axioms_for_replace
std::pair< exprt, string_constraintst > add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Replace a character by another in a string.
Definition: string_constraint_generator_transformation.cpp:297
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
string_constraintt
Definition: string_constraint.h:58
and_exprt
Boolean AND.
Definition: std_expr.h:2409
s1
int8_t s1
Definition: bytecode_info.h:59
string_refinement_invariant.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
char_array_of_pointer
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Definition: string_constraint_generator_main.cpp:325
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
array_string_exprt::content
exprt & content()
Definition: string_expr.h:80
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)
Convert two expressions to pair of chars If both expressions are characters, return pair of them If b...
Definition: string_constraint_generator_transformation.cpp:257
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: std_expr.h:4484
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:598
get_string_expr
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
Definition: string_constraint_generator_main.cpp:210
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:583
or_exprt
Boolean OR.
Definition: std_expr.h:2531
add_axioms_for_delete
std::pair< exprt, string_constraintst > add_axioms_for_delete(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
Definition: string_constraint_generator_transformation.cpp:374
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:339
minus_exprt
Binary minus.
Definition: std_expr.h:1106
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
length_le
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
Definition: string_expr.h:41
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:591
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
add_axioms_for_concat
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, 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_constraint_generator_concat.cpp:126
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
add_axioms_for_set_length
std::pair< exprt, string_constraintst > add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Reduce or extend a string to have the given length.
Definition: string_constraint_generator_transformation.cpp:37
string_constraint_generator.h
array_string_exprt
Definition: string_expr.h:67
add_axioms_for_delete_char_at
std::pair< exprt, string_constraintst > add_axioms_for_delete_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
add axioms corresponding to the StringBuilder.deleteCharAt java function
Definition: string_constraint_generator_transformation.cpp:339
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: string_constraint_generator_main.cpp:87
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
not_exprt
Boolean negation.
Definition: std_expr.h:3308
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:111