cprover
string_builtin_function.cpp
Go to the documentation of this file.
1 
5 
6 #include <algorithm>
7 #include <iterator>
8 
10 
13  const array_string_exprt &a,
14  const std::function<exprt(const exprt &)> &get_value);
15 
18  const std::vector<mp_integer> &array,
19  const array_typet &array_type);
20 
23  const exprt &return_code,
24  const std::vector<exprt> &fun_args,
25  array_poolt &array_pool)
26  : string_builtin_functiont(return_code)
27 {
28  PRECONDITION(fun_args.size() > 2);
29  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
30  input = array_pool.find(arg1.op1(), arg1.op0());
31  result = array_pool.find(fun_args[1], fun_args[0]);
32  args.insert(args.end(), fun_args.begin() + 3, fun_args.end());
33 }
34 
36  const std::function<exprt(const exprt &)> &get_value) const
37 {
38  const auto &input_value = eval_string(input, get_value);
39  if(!input_value.has_value())
40  return {};
41 
42  std::vector<mp_integer> arg_values;
43  const auto &insert = std::back_inserter(arg_values);
44  const mp_integer unknown('?');
45  std::transform(
46  args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
47  if(const auto val = numeric_cast<mp_integer>(get_value(e)))
48  return *val;
49  INVARIANT(
50  get_value(e).id() == ID_unknown,
51  "array valuation should only contain constants and unknown");
52  return unknown;
53  });
54 
55  const auto result_value = eval(*input_value, arg_values);
56  const auto length = from_integer(result_value.size(), result.length().type());
57  const array_typet type(result.type().subtype(), length);
58  return make_string(result_value, type);
59 }
60 
62  const exprt &return_code,
63  const std::vector<exprt> &fun_args,
64  array_poolt &array_pool)
65  : string_builtin_functiont(return_code)
66 {
67  PRECONDITION(fun_args.size() > 4);
68  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
69  input1 = array_pool.find(arg1.op1(), arg1.op0());
70  const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[4]);
71  input2 = array_pool.find(arg2.op1(), arg2.op0());
72  result = array_pool.find(fun_args[1], fun_args[0]);
73  args.push_back(fun_args[3]);
74  args.insert(args.end(), fun_args.begin() + 5, fun_args.end());
75 }
76 
78  const exprt &return_code,
79  const std::vector<exprt> &fun_args,
80  array_poolt &array_pool)
82 {
83  PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
84  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
85  input1 = array_pool.find(arg1.op1(), arg1.op0());
86  const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[3]);
87  input2 = array_pool.find(arg2.op1(), arg2.op0());
88  result = array_pool.find(fun_args[1], fun_args[0]);
89  args.insert(args.end(), fun_args.begin() + 4, fun_args.end());
90 }
91 
93  const array_string_exprt &a,
94  const std::function<exprt(const exprt &)> &get_value)
95 {
96  if(a.id() == ID_if)
97  {
98  const if_exprt &ite = to_if_expr(a);
99  const exprt cond = get_value(ite.cond());
100  if(!cond.is_constant())
101  return {};
102  return cond.is_true()
103  ? eval_string(to_array_string_expr(ite.true_case()), get_value)
104  : eval_string(to_array_string_expr(ite.false_case()), get_value);
105  }
106 
107  const exprt content = get_value(a.content());
108  const auto &array = expr_try_dynamic_cast<array_exprt>(content);
109  if(!array)
110  return {};
111 
112  const auto &ops = array->operands();
113  std::vector<mp_integer> result;
114  const mp_integer unknown('?');
115  const auto &insert = std::back_inserter(result);
116  std::transform(
117  ops.begin(), ops.end(), insert, [unknown](const exprt &e) { // NOLINT
118  if(const auto i = numeric_cast<mp_integer>(e))
119  return *i;
120  return unknown;
121  });
122  return result;
123 }
124 
126 make_string(const std::vector<mp_integer> &array, const array_typet &array_type)
127 {
128  const typet &char_type = array_type.subtype();
129  array_exprt array_expr(array_type);
130  const auto &insert = std::back_inserter(array_expr.operands());
131  std::transform(
132  array.begin(), array.end(), insert, [&](const mp_integer &i) { // NOLINT
133  return from_integer(i, char_type);
134  });
135  return to_array_string_expr(array_expr);
136 }
137 
139  const std::vector<mp_integer> &input1_value,
140  const std::vector<mp_integer> &input2_value,
141  const std::vector<mp_integer> &args_value) const
142 {
143  const auto start_index =
144  args_value.size() > 0 && args_value[0] > 0 ? args_value[0] : mp_integer(0);
145  const mp_integer input2_size(input2_value.size());
146  const auto end_index =
147  args_value.size() > 1
148  ? std::max(std::min(args_value[1], input2_size), start_index)
149  : input2_size;
150 
151  std::vector<mp_integer> result(input1_value);
152  result.insert(
153  result.end(),
154  input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
155  input2_value.begin() + numeric_cast_v<std::size_t>(end_index));
156  return result;
157 }
158 
160  const std::vector<mp_integer> &input_value,
161  const std::vector<mp_integer> &args_value) const
162 {
163  PRECONDITION(args_value.size() == 1);
164  std::vector<mp_integer> result(input_value);
165  result.push_back(args_value[0]);
166  return result;
167 }
168 
170  const std::vector<mp_integer> &input1_value,
171  const std::vector<mp_integer> &input2_value,
172  const std::vector<mp_integer> &args_value) const
173 {
174  PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
175  const auto offset = std::min(
176  std::max(args_value[0], mp_integer(0)), mp_integer(input1_value.size()));
177  const auto start = args_value.size() > 1
178  ? std::max(args_value[1], mp_integer(0))
179  : mp_integer(0);
180 
181  const mp_integer input2_size(input2_value.size());
182  const auto end =
183  args_value.size() > 2
184  ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
185  : input2_size;
186 
187  std::vector<mp_integer> result(input1_value);
188  result.insert(
189  result.begin() + numeric_cast_v<std::size_t>(offset),
190  input2_value.begin() + numeric_cast_v<std::size_t>(start),
191  input2_value.begin() + numeric_cast_v<std::size_t>(end));
192  return result;
193 }
194 
196  const std::function<exprt(const exprt &)> &get_value) const
197 {
198  const auto &input1_value = eval_string(input1, get_value);
199  const auto &input2_value = eval_string(input2, get_value);
200  if(!input2_value.has_value() || !input1_value.has_value())
201  return {};
202 
203  std::vector<mp_integer> arg_values;
204  const auto &insert = std::back_inserter(arg_values);
205  const mp_integer unknown('?');
206  std::transform(
207  args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
208  if(const auto val = numeric_cast<mp_integer>(get_value(e)))
209  return *val;
210  return unknown;
211  });
212 
213  const auto result_value = eval(*input1_value, *input2_value, arg_values);
214  const auto length = from_integer(result_value.size(), result.length().type());
215  const array_typet type(result.type().subtype(), length);
216  return make_string(result_value, type);
217 }
218 
220  const exprt &return_code,
222  array_poolt &array_pool)
223  : string_builtin_functiont(return_code), function_application(f)
224 {
225  const std::vector<exprt> &fun_args = f.arguments();
226  std::size_t i = 0;
227  if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
228  {
229  string_res = array_pool.find(fun_args[1], fun_args[0]);
230  i = 2;
231  }
232 
233  for(; i < fun_args.size(); ++i)
234  {
235  const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
236  // TODO: use is_refined_string_type ?
237  if(
238  arg && arg->operands().size() == 2 &&
239  arg->op1().type().id() == ID_pointer)
240  {
241  INVARIANT(is_refined_string_type(arg->type()), "should be a string");
242  string_args.push_back(array_pool.find(arg->op1(), arg->op0()));
243  }
244  else
245  args.push_back(fun_args[i]);
246  }
247 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
The type of an expression.
Definition: type.h:22
exprt & true_case()
Definition: std_expr.h:3395
BigInt mp_integer
Definition: mp_arith.h:22
Generates string constraints to link results from string functions with their arguments.
virtual std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const
Evaluate the result from a concrete valuation of the arguments.
application of (mathematical) function
Definition: std_expr.h:4531
string_concatenation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
argumentst & arguments()
Definition: std_expr.h:4564
String inserting a string into another one.
std::vector< array_string_exprt > string_args
string_insertion_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
static optionalt< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Module: String solver Author: Diffblue Ltd.
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
static array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
const irep_idt & id() const
Definition: irep.h:189
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
virtual std::vector< mp_integer > eval(const std::vector< mp_integer > &input_value, const std::vector< mp_integer > &args_value) const =0
Evaluate the result from a concrete valuation of the arguments.
nonstd::optional< T > optionalt
Definition: optional.h:35
std::vector< mp_integer > eval(const std::vector< mp_integer > &input_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:184
exprt & false_case()
Definition: std_expr.h:3405
bool is_constant() const
Definition: expr.cpp:119
string_transformation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
Base class for all expressions.
Definition: expr.h:42
bool is_refined_string_type(const typet &type)
optionalt< array_string_exprt > string_res
arrays with given size
Definition: std_types.h:1004
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1815
std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
bitvector_typet char_type()
Definition: c_types.cpp:114
array constructor from list of elements
Definition: std_expr.h:1617
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:162
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:91