cprover
Loading...
Searching...
No Matches
string_insertion_builtin_function.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String solver
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
10#include <algorithm>
11#include <iterator>
12
14{
15 PRECONDITION(args.size() == 1);
16 return equal_exprt(
21}
22
24 const exprt &return_code,
25 const std::vector<exprt> &fun_args,
26 array_poolt &array_pool)
27 : string_builtin_functiont(return_code, array_pool)
28{
29 PRECONDITION(fun_args.size() > 4);
30 const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
31 input1 = array_pool.find(arg1.op1(), arg1.op0());
32 const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[4]);
33 input2 = array_pool.find(arg2.op1(), arg2.op0());
34 result = array_pool.find(fun_args[1], fun_args[0]);
35 args.push_back(fun_args[3]);
36 args.insert(args.end(), fun_args.begin() + 5, fun_args.end());
37}
38
40 const std::vector<mp_integer> &input1_value,
41 const std::vector<mp_integer> &input2_value,
42 const std::vector<mp_integer> &args_value) const
43{
44 PRECONDITION(args_value.size() >= 1 && args_value.size() <= 3);
45 const auto offset = std::min(
46 std::max(args_value[0], mp_integer(0)), mp_integer(input1_value.size()));
47 const auto start = args_value.size() > 1
48 ? std::max(args_value[1], mp_integer(0))
49 : mp_integer(0);
50
51 const mp_integer input2_size(input2_value.size());
52 const auto end =
53 args_value.size() > 2
54 ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
55 : input2_size;
56
57 std::vector<mp_integer> eval_result(input1_value);
58 eval_result.insert(
59 eval_result.begin() + numeric_cast_v<std::size_t>(offset),
60 input2_value.begin() + numeric_cast_v<std::size_t>(start),
61 input2_value.begin() + numeric_cast_v<std::size_t>(end));
62 return eval_result;
63}
64
66 const std::function<exprt(const exprt &)> &get_value) const
67{
68 const auto &input1_value = eval_string(input1, get_value);
69 const auto &input2_value = eval_string(input2, get_value);
70 if(!input2_value.has_value() || !input1_value.has_value())
71 return {};
72
73 std::vector<mp_integer> arg_values;
74 const auto &insert = std::back_inserter(arg_values);
75 const mp_integer unknown('?');
76 std::transform(
77 args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
78 if(const auto val = numeric_cast<mp_integer>(get_value(e)))
79 return *val;
80 return unknown;
81 });
82
83 const auto result_value = eval(*input1_value, *input2_value, arg_values);
84 const auto length = from_integer(result_value.size(), result.length_type());
85 const array_typet type(to_type_with_subtype(result.type()).subtype(), length);
86 return make_string(result_value, type);
87}
88
90 string_constraint_generatort &generator) const
91{
92 PRECONDITION(args.size() == 1);
93 const exprt &offset = args[0];
94 PRECONDITION(offset.type() == input1.length_type());
96 const exprt offset1 = maximum(
99
101
102 // Axiom 1.
104
105 // Axiom 2.
106 constraints.universal.push_back([&] { // NOLINT
107 const symbol_exprt i = generator.fresh_symbol("QA_insert1", index_type);
108 return string_constraintt(i, offset1, equal_exprt(result[i], input1[i]));
109 }());
110
111 // Axiom 3.
112 constraints.universal.push_back([&] { // NOLINT
113 const symbol_exprt i = generator.fresh_symbol("QA_insert2", index_type);
114 return string_constraintt(
115 i,
117 equal_exprt(result[plus_exprt(i, offset1)], input2[i]));
118 }());
119
120 // Axiom 4.
121 constraints.universal.push_back([&] { // NOLINT
122 const symbol_exprt i = generator.fresh_symbol("QA_insert3", index_type);
123 return string_constraintt(
124 i,
125 offset1,
129 input1[i]));
130 }());
131
132 // return_code = 0
133 constraints.existential.push_back(
135
136 return constraints;
137}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet index_type()
Definition: c_types.cpp:22
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
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:26
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:184
const typet & length_type() const
Definition: string_expr.h:69
Arrays with given size.
Definition: std_types.h:763
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
The plus expression Associativity is not specified.
Definition: std_expr.h:914
Base class for string functions that are built in the solver.
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.
string_constraintst constraints(string_constraint_generatort &generator) const override
Constraints ensuring the result corresponds to input1 where we inserted input2 at position offset giv...
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.
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const typet & subtype() const
Definition: type.h:156
The type of an expression, extends irept.
Definition: type.h:29
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
optionalt< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Given a function get_value which gives a valuation to expressions, attempt to find the current value ...
exprt maximum(const exprt &a, const exprt &b)
exprt minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
signedbv_typet get_return_code_type()
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
std::vector< string_constraintt > universal
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177