cprover
string_constraint_generator_concat.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for functions adding content
4  add the end of strings
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
15 
38 std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
39  symbol_generatort &fresh_symbol,
40  const array_string_exprt &res,
41  const array_string_exprt &s1,
42  const array_string_exprt &s2,
43  const exprt &start_index,
44  const exprt &end_index)
45 {
46  string_constraintst constraints;
47  const typet &index_type = start_index.type();
48  const exprt start1 = maximum(start_index, from_integer(0, index_type));
49  const exprt end1 = maximum(minimum(end_index, s2.length()), start1);
50 
51  // Axiom 1.
52  constraints.existential.push_back(
53  length_constraint_for_concat_substr(res, s1, s2, start_index, end_index));
54 
55  // Axiom 2.
56  constraints.universal.push_back([&] {
57  const symbol_exprt idx =
58  fresh_symbol("QA_index_concat", res.length().type());
59  return string_constraintt(
60  idx, zero_if_negative(s1.length()), equal_exprt(s1[idx], res[idx]));
61  }());
62 
63  // Axiom 3.
64  constraints.universal.push_back([&] {
65  const symbol_exprt idx2 =
66  fresh_symbol("QA_index_concat2", res.length().type());
67  const equal_exprt res_eq(
68  res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
69  const minus_exprt upper_bound(res.length(), s1.length());
70  return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
71  }());
72 
73  return {from_integer(0, get_return_code_type()), std::move(constraints)};
74 }
75 
82  const array_string_exprt &res,
83  const array_string_exprt &s1,
84  const array_string_exprt &s2,
85  const exprt &start,
86  const exprt &end)
87 {
88  PRECONDITION(res.length().type().id() == ID_signedbv);
89  const exprt start1 = maximum(start, from_integer(0, start.type()));
90  const exprt end1 = maximum(minimum(end, s2.length()), start1);
91  const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
92  const exprt overflow = sum_overflows(res_length);
93  const exprt max_int = to_signedbv_type(res.length().type()).largest_expr();
94  return equal_exprt(res.length(), if_exprt(overflow, max_int, res_length));
95 }
96 
100  const array_string_exprt &res,
101  const array_string_exprt &s1,
102  const array_string_exprt &s2)
103 {
104  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
105 }
106 
110  const array_string_exprt &res,
111  const array_string_exprt &s1)
112 {
113  return equal_exprt(
114  res.length(), plus_exprt(s1.length(), from_integer(1, s1.length().type())));
115 }
116 
126 std::pair<exprt, string_constraintst> add_axioms_for_concat(
127  symbol_generatort &fresh_symbol,
128  const array_string_exprt &res,
129  const array_string_exprt &s1,
130  const array_string_exprt &s2)
131 {
132  exprt index_zero=from_integer(0, s2.length().type());
134  fresh_symbol, res, s1, s2, index_zero, s2.length());
135 }
136 
143 std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
144  symbol_generatort &fresh_symbol,
146  array_poolt &array_pool)
147 {
148  PRECONDITION(f.arguments().size() == 4);
149  const array_string_exprt res =
150  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
151  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
152  const typet &char_type = s1.content().type().subtype();
153  const typet &index_type = s1.length().type();
154  const array_string_exprt code_point =
155  array_pool.fresh_string(index_type, char_type);
156  return combine_results(
157  add_axioms_for_code_point(code_point, f.arguments()[3]),
158  add_axioms_for_concat(fresh_symbol, res, s1, code_point));
159 }
The type of an expression, extends irept.
Definition: type.h:27
Generates string constraints to link results from string functions with their arguments.
Application of (mathematical) function.
Definition: std_expr.h:4481
std::pair< exprt, string_constraintst > add_axioms_for_concat_substr(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index â...
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
Generation of fresh symbols of a given type.
argumentst & arguments()
Definition: std_expr.h:4506
The trinary if-then-else operator.
Definition: std_expr.h:3427
typet & type()
Return the type of the expression.
Definition: expr.h:68
exprt length_constraint_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start, const exprt &end)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
signedbv_typet get_return_code_type()
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas,...
exprt minimum(const exprt &a, const exprt &b)
std::pair< exprt, string_constraintst > add_axioms_for_concat_code_point(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
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 ...
Equality.
Definition: std_expr.h:1484
const irep_idt & id() const
Definition: irep.h:259
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...
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
std::pair< exprt, string_constraintst > add_axioms_for_code_point(const array_string_exprt &res, const exprt &code_point)
add axioms for the conversion of an integer representing a java code point to a utf-16 string
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
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.
bitvector_typet index_type()
Definition: c_types.cpp:16
exprt maximum(const exprt &a, const exprt &b)
std::vector< exprt > existential
exprt & length()
Definition: string_expr.h:70
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2
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.
Base class for all expressions.
Definition: expr.h:54
std::vector< string_constraintt > universal
exprt sum_overflows(const plus_exprt &sum)
Binary minus.
Definition: std_expr.h:1106
Expression to hold a symbol (variable)
Definition: std_expr.h:143
int8_t s1
Definition: bytecode_info.h:59
int16_t s2
Definition: bytecode_info.h:60
const typet & subtype() const
Definition: type.h:38
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet char_type()
Definition: c_types.cpp:114