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 
21  const string_exprt &s1, const string_exprt &s2)
22 {
23  const refined_string_typet &ref_type=to_refined_string_type(s1.type());
24  string_exprt res=fresh_string(ref_type);
25 
26  // We add axioms:
27  // a1 : |res|=|s1|+|s2|
28  // a2 : |s1| <= |res| (to avoid overflow with very long strings)
29  // a3 : |s2| <= |res| (to avoid overflow with very long strings)
30  // a4 : forall i<|s1|. res[i]=s1[i]
31  // a5 : forall i<|s2|. res[i+|s1|]=s2[i]
32 
33  exprt a1=res.axiom_for_has_length(
34  plus_exprt(s1.length(), s2.length()));
35  axioms.push_back(a1);
36  axioms.push_back(s1.axiom_for_is_shorter_than(res));
37  axioms.push_back(s2.axiom_for_is_shorter_than(res));
38 
39  symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type());
40  string_constraintt a4(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
41  axioms.push_back(a4);
42 
43  symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type());
44  equal_exprt res_eq(s2[idx2], res[plus_exprt(idx2, s1.length())]);
45  string_constraintt a5(idx2, s2.length(), res_eq);
46  axioms.push_back(a5);
47 
48  return res;
49 }
50 
57 {
59  assert(args.size()==2);
60 
63 
64  return add_axioms_for_concat(s1, s2);
65 }
66 
73 {
77  args(f, 2)[1], MAX_INTEGER_LENGTH, ref_type);
78  return add_axioms_for_concat(s1, s2);
79 }
80 
87 {
91  return add_axioms_for_concat(s1, s2);
92 }
93 
99 {
101  const refined_string_typet &ref_type=to_refined_string_type(s1.type());
102  string_exprt s2=add_axioms_from_bool(args(f, 2)[1], ref_type);
103  return add_axioms_for_concat(s1, s2);
104 }
105 
112 {
114  const refined_string_typet &ref_type=to_refined_string_type(s1.type());
115  string_exprt s2=add_axioms_from_char(args(f, 2)[1], ref_type);
116  return add_axioms_for_concat(s1, s2);
117 }
118 
125 {
128  args(f, 2)[1], MAX_DOUBLE_LENGTH);
129  return add_axioms_for_concat(s1, s2);
130 }
131 
138 {
141  return add_axioms_for_concat(s1, s2);
142 }
143 
150 {
152  const refined_string_typet &ref_type=to_refined_string_type(s1.type());
153  string_exprt s2=add_axioms_for_code_point(args(f, 2)[1], ref_type);
154  return add_axioms_for_concat(s1, s2);
155 }
Generates string constraints to link results from string functions with their arguments.
string_exprt add_axioms_for_concat_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(D) java function
application of (mathematical) function
Definition: std_expr.h:3785
string_exprt add_axioms_from_bool(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(Z) java function
string_exprt add_axioms_for_concat_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(I) java function
argumentst & arguments()
Definition: std_expr.h:3805
string_exprt add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
typet & type()
Definition: expr.h:60
string_exprt add_axioms_for_concat_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(F) java function
equality
Definition: std_expr.h:1082
string_exprt fresh_string(const refined_string_typet &type)
construct a string expression whose length and content are new variables
string_exprt add_axioms_for_concat_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(Z) java function
string_exprt add_axioms_from_float(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(F) java function
exprt::operandst argumentst
Definition: std_expr.h:3803
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
string_exprt add_axioms_for_concat(const string_exprt &s1, const string_exprt &s2)
add axioms to say that the returned string expression is equal to the concatenation of the two string...
The plus expression.
Definition: std_expr.h:702
string_exprt add_axioms_from_char(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(C) java function
Base class for all expressions.
Definition: expr.h:46
string_exprt add_axioms_from_int(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(I) java function
Expression to hold a symbol (variable)
Definition: std_expr.h:82
int8_t s1
Definition: bytecode_info.h:59
string_exprt add_axioms_for_concat_long(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.append(J) java function.
string_exprt add_axioms_for_concat_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(C) java function
int16_t s2
Definition: bytecode_info.h:60
string_exprt add_axioms_for_code_point(const exprt &code_point, const refined_string_typet &ref_type)
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)