cprover
Loading...
Searching...
No Matches
string_constraint_generator_constants.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generates string constraints for constant strings
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
11
13
15#include <util/unicode.h>
16
23std::pair<exprt, string_constraintst>
25 const array_string_exprt &res,
26 irep_idt sval,
27 const exprt &guard)
28{
29 string_constraintst constraints;
32 std::string c_str = id2string(sval);
33 std::wstring str;
34
37#if 0
38 if(mode==ID_java)
39 str=utf8_to_utf16_little_endian(c_str);
40 else
41#endif
42 str = widen(c_str);
43
44 for(std::size_t i = 0; i < str.size(); i++)
45 {
46 const exprt idx = from_integer(i, index_type);
47 const exprt c = from_integer(str[i], char_type);
48 const equal_exprt lemma(res[idx], c);
49 constraints.existential.push_back(implies_exprt(guard, lemma));
50 }
51
52 const exprt s_length = from_integer(str.size(), index_type);
53
54 constraints.existential.push_back(implies_exprt(
56 return {from_integer(0, get_return_code_type()), std::move(constraints)};
57}
58
63std::pair<exprt, string_constraintst>
66{
67 PRECONDITION(f.arguments().size() == 2);
68 string_constraintst constraints;
69 exprt length = f.arguments()[0];
70 constraints.existential.push_back(
71 equal_exprt(length, from_integer(0, length.type())));
72 return {from_integer(0, get_return_code_type()), std::move(constraints)};
73}
74
82std::pair<exprt, string_constraintst>
84 const array_string_exprt &res,
85 const exprt &arg,
86 const exprt &guard)
87{
88 if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
89 {
90 const and_exprt guard_true(guard, if_expr->cond());
91 const and_exprt guard_false(guard, not_exprt(if_expr->cond()));
92 return combine_results(
93 add_axioms_for_cprover_string(res, if_expr->true_case(), guard_true),
94 add_axioms_for_cprover_string(res, if_expr->false_case(), guard_false));
95 }
96 else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
97 return add_axioms_for_constant(res, constant_expr->get_value(), guard);
98 else
99 return {from_integer(1, get_return_code_type()), {}};
100}
101
110std::pair<exprt, string_constraintst>
113{
115 PRECONDITION(args.size() == 3); // Bad args to string literal?
116 const array_string_exprt res = array_pool.find(args[1], args[0]);
117 return add_axioms_for_cprover_string(res, args[2], true_exprt());
118}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static exprt guard(const exprt::operandst &guards, exprt cond)
bitvector_typet index_type()
Definition c_types.cpp:22
bitvector_typet char_type()
Definition c_types.cpp:111
Boolean AND.
Definition std_expr.h:2071
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
Application of (mathematical) function.
Boolean implication.
Definition std_expr.h:2134
Boolean negation.
Definition std_expr.h:2278
std::pair< exprt, string_constraintst > add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
std::pair< exprt, string_constraintst > add_axioms_for_cprover_string(const array_string_exprt &res, const exprt &arg, const exprt &guard)
Convert an expression of type string_typet to a string_exprt.
std::pair< exprt, string_constraintst > add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
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 ...
The Boolean constant true.
Definition std_expr.h:3008
const typet & subtype() const
Definition type.h:154
The type of an expression, extends irept.
Definition type.h:29
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:81
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for 'mathematical' expressions.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Generates string constraints to link results from string functions with their arguments.
signedbv_typet get_return_code_type()
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175
std::wstring widen(const char *s)
Definition unicode.cpp:49