CBMC
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
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);
31 input1 = array_pool.find(arg1.op1(), arg1.op0());
33 input2 = array_pool.find(arg2.op1(), arg2.op0());
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
52 const auto end =
53 args_value.size() > 2
54 ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
56
57 std::vector<mp_integer> eval_result(input1_value);
58 eval_result.insert(
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
91 message_handlert &message_handler) const
92{
93 PRECONDITION(args.size() == 1);
94 const exprt &offset = args[0];
95 PRECONDITION(offset.type() == input1.length_type());
96 const typet &index_type = input1.length_type();
97 const exprt offset1 = maximum(
98 from_integer(0, index_type),
100
102
103 // Axiom 1.
105
106 // Axiom 2.
107 constraints.universal.push_back([&] { // NOLINT
108 const symbol_exprt i = generator.fresh_symbol("QA_insert1", index_type);
109 return string_constraintt(
110 i, offset1, equal_exprt(result[i], input1[i]), message_handler);
111 }());
112
113 // Axiom 3.
114 constraints.universal.push_back([&] { // NOLINT
115 const symbol_exprt i = generator.fresh_symbol("QA_insert2", index_type);
116 return string_constraintt(
117 i,
120 message_handler);
121 }());
122
123 // Axiom 4.
124 constraints.universal.push_back([&] { // NOLINT
125 const symbol_exprt i = generator.fresh_symbol("QA_insert3", index_type);
126 return string_constraintt(
127 i,
128 offset1,
132 input1[i]),
133 message_handler);
134 }());
135
136 // return_code = 0
137 constraints.existential.push_back(
139
140 return constraints;
141}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
const typet & length_type() const
Definition string_expr.h:70
Arrays with given size.
Definition std_types.h:807
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
The plus expression Associativity is not specified.
Definition std_expr.h:1002
Base class for string functions that are built in the solver.
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) const override
Constraints ensuring the result corresponds to input1 where we inserted input2 at position offset giv...
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.
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:131
The type of an expression, extends irept.
Definition type.h:29
BigInt mp_integer
Definition smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition invariant.h:463
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
std::optional< 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:208