Skip to content

Commit ffdef62

Browse files
romainbrenguierromainbrenguier
committed
Adding more comments in refined_string_type and string_constraint
Also some comments in string_constraint_generator.cpp and comments on the string_refinement module
1 parent d6d4627 commit ffdef62

8 files changed

+253
-52
lines changed

‎src/solvers/refinement/refined_string_type.cpp

Lines changed: 60 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
/** -*- C++ -*- *****************************************************\
22
3-
Module: Type of string expressions for PASS algorithm
4-
(see the PASS paper at HVC'13)
3+
Module: Type for string expressions used by the string solver.
4+
These string expressions contains a field `length`, of type
5+
`index_type`, a field `content` of type `content_type`.
6+
This module also defines function to recognise the C and java
7+
string types.
58
69
Author: Romain Brenguier, romain.brenguier@diffblue.com
710
@@ -10,6 +13,13 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
1013
#include <solvers/refinement/refined_string_type.h>
1114
#include <ansi-c/string_constant.h>
1215

16+
/*******************************************************************\
17+
18+
Constructor: refined_string_typet::refined_string_typet
19+
20+
Inputs: type of characters
21+
22+
\*******************************************************************/
1323
refined_string_typet::refined_string_typet(unsignedbv_typet char_type)
1424
:struct_typet()
1525
{
@@ -25,6 +35,15 @@ refined_string_typet::refined_string_typet(unsignedbv_typet char_type)
2535
components()[1].type()=char_array;
2636
}
2737

38+
/*******************************************************************\
39+
40+
Function: refined_string_typet::is_c_string_type
41+
42+
Inputs: a type
43+
44+
Outputs: Boolean telling whether the type is that of C strings
45+
46+
\*******************************************************************/
2847
bool refined_string_typet::is_c_string_type(const typet &type)
2948
{
3049
if(type.id()==ID_struct)
@@ -35,18 +54,36 @@ bool refined_string_typet::is_c_string_type(const typet &type)
3554
return false;
3655
}
3756

38-
bool refined_string_typet::is_java_string_type(const typet &type)
57+
/*******************************************************************\
58+
59+
Function: refined_string_typet::is_java_string_pointer_type
60+
61+
Inputs: a type
62+
63+
Outputs: Boolean telling whether the type is that of java string pointers
64+
65+
\*******************************************************************/
66+
bool refined_string_typet::is_java_string_pointer_type(const typet &type)
3967
{
4068
if(type.id()==ID_pointer)
4169
{
4270
pointer_typet pt=to_pointer_type(type);
4371
typet subtype=pt.subtype();
44-
return is_java_deref_string_type(subtype);
72+
return is_java_string_type(subtype);
4573
}
4674
return false;
4775
}
4876

49-
bool refined_string_typet::is_java_deref_string_type(const typet &type)
77+
/*******************************************************************\
78+
79+
Function: refined_string_typet::is_java_string_type
80+
81+
Inputs: a type
82+
83+
Outputs: Boolean telling whether the type is that of java string
84+
85+
\*******************************************************************/
86+
bool refined_string_typet::is_java_string_type(const typet &type)
5087
{
5188
if(type.id()==ID_symbol)
5289
{
@@ -61,6 +98,15 @@ bool refined_string_typet::is_java_deref_string_type(const typet &type)
6198
return false;
6299
}
63100

101+
/*******************************************************************\
102+
103+
Function: refined_string_typet::is_java_string_builder_type
104+
105+
Inputs: a type
106+
107+
Outputs: Boolean telling whether the type is that of java string builder
108+
109+
\*******************************************************************/
64110
bool refined_string_typet::is_java_string_builder_type(const typet &type)
65111
{
66112
if(type.id()==ID_pointer)
@@ -76,6 +122,15 @@ bool refined_string_typet::is_java_string_builder_type(const typet &type)
76122
return false;
77123
}
78124

125+
/*******************************************************************\
126+
127+
Function: refined_string_typet::is_java_char_sequence_type
128+
129+
Inputs: a type
130+
131+
Outputs: Boolean telling whether the type is that of java char sequence
132+
133+
\*******************************************************************/
79134
bool refined_string_typet::is_java_char_sequence_type(const typet &type)
80135
{
81136
if(type.id()==ID_pointer)

‎src/solvers/refinement/refined_string_type.h

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
/** -*- C++ -*- *****************************************************\
22
3-
Module: Type of string expressions for PASS algorithm
4-
(see the PASS paper at HVC'13)
3+
Module: Type for string expressions used by the string solver.
4+
These string expressions contains a field `length`, of type
5+
`index_type`, a field `content` of type `content_type`.
6+
This module also defines function to recognise the C and java
7+
string types.
58
69
Author: Romain Brenguier, romain.brenguier@diffblue.com
710
@@ -49,9 +52,9 @@ class refined_string_typet: public struct_typet
4952

5053
static bool is_c_string_type(const typet & type);
5154

52-
static bool is_java_string_type(const typet & type);
55+
static bool is_java_string_pointer_type(const typet & type);
5356

54-
static bool is_java_deref_string_type(const typet & type);
57+
static bool is_java_string_type(const typet & type);
5558

5659
static bool is_java_string_builder_type(const typet & type);
5760

@@ -68,7 +71,7 @@ class refined_string_typet: public struct_typet
6871
static inline bool is_unrefined_string_type(const typet & type)
6972
{
7073
return (is_c_string_type(type)
71-
|| is_java_string_type(type)
74+
|| is_java_string_pointer_type(type)
7275
|| is_java_string_builder_type(type)
7376
|| is_java_char_sequence_type(type));
7477
}

‎src/solvers/refinement/string_constraint.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
11
/** -*- C++ -*- *****************************************************\
22
3-
Module: String constraints
4-
(see the PASS paper at HVC'13)
3+
Module: String constraints.
4+
These are formulas talking about strings. We implemented two
5+
forms of constraints: `string_constraintt` implements formulas
6+
of the form $\forall univ_var \in [lb,ub[. premise => body$,
7+
and not_contains_constraintt implements those of the form:
8+
$\forall x in [lb,ub[. p(x) => \exists y in [lb,ub[.
9+
s1[x+y] != s2[y]$.
510
611
Author: Romain Brenguier, romain.brenguier@diffblue.com
712
813
\*******************************************************************/
914

1015
#include <solvers/refinement/string_constraint.h>
11-

‎src/solvers/refinement/string_constraint.h

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,12 @@
11
/** -*- C++ -*- *****************************************************\
22
3-
Module: String constraints
4-
(see the PASS paper at HVC'13
3+
Module: String constraints.
4+
These are formulas talking about strings. We implemented two
5+
forms of constraints: `string_constraintt` implements formulas
6+
of the form $\forall univ_var \in [lb,ub[. premise => body$,
7+
and not_contains_constraintt implements those of the form:
8+
$\forall x in [lb,ub[. p(x) => \exists y in [lb,ub[.
9+
s1[x+y] != s2[y]$.
510
611
Author: Romain Brenguier, romain.brenguier@diffblue.com
712
@@ -18,7 +23,7 @@ class string_constraintt: public exprt
1823
{
1924
public:
2025
// String constraints are of the form
21-
// forall univ_var in [0,bound[. premise => body
26+
// forall univ_var in [lower_bound,upper_bound[. premise => body
2227
// or premise => body
2328

2429
inline const exprt &premise() const
@@ -53,7 +58,6 @@ class string_constraintt: public exprt
5358
copy_to_operands(true_exprt(), true_exprt());
5459
}
5560

56-
// Returns a new constraints with an universal quantifier added
5761
string_constraintt(
5862
const symbol_exprt &univ,
5963
const exprt &bound_inf,

‎src/solvers/refinement/string_constraint_generator.cpp

Lines changed: 32 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
/** -*- C++ -*- *****************************************************\
22
3-
Module: Constraint generation from string function calls
4-
for the PASS algorithm (see the PASS paper at HVC'13)
3+
Module: Generates string constraints to link results from string functions
4+
with their arguments. This is inspired by the PASS paper at HVC'13
5+
which gives examples of constraints for several functions.
56
67
Author: Romain Brenguier, romain.brenguier@diffblue.com
78
@@ -71,6 +72,19 @@ symbol_exprt string_constraint_generatort::fresh_boolean
7172
}
7273

7374

75+
/*******************************************************************\
76+
77+
Function: string_constraint_generatort::add_axioms_for_string_expr
78+
79+
Inputs: an expression of type string
80+
81+
Outputs: a string expression that is link to the argument through
82+
axioms that are added to the list
83+
84+
Purpose: obtain a refined string expression corresponding to string
85+
variable of string function call
86+
87+
\*******************************************************************/
7488
string_exprt string_constraint_generatort::add_axioms_for_string_expr
7589
(const exprt & unrefined_string)
7690
{
@@ -144,7 +158,19 @@ string_exprt string_constraint_generatort::find_or_add_string_of_symbol
144158
return symbol_to_string[id];
145159
}
146160

161+
/*******************************************************************\
147162
163+
Function: string_constraint_generatort::add_axioms_for_function_application
164+
165+
Inputs: an expression containing a function application
166+
167+
Outputs: expression corresponding to the result of the function application
168+
169+
Purpose: strings contained in this call are converted to objects of type
170+
`string_exprt`, through adding axioms. Axioms are then added to
171+
enforce that the result corresponds to the function application.
172+
173+
\*******************************************************************/
148174
exprt string_constraint_generatort::add_axioms_for_function_application
149175
(const function_application_exprt & expr)
150176
{
@@ -159,7 +185,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application
159185
else if(id==ID_cprover_string_length_func)
160186
return add_axioms_for_length(expr);
161187
else if(id==ID_cprover_string_equal_func)
162-
return add_axioms_for_equal(expr);
188+
return add_axioms_for_equals(expr);
163189
else if(id==ID_cprover_string_equals_ignore_case_func)
164190
return add_axioms_for_equals_ignore_case(expr);
165191
else if(id==ID_cprover_string_is_empty_func)
@@ -1202,7 +1228,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_float
12021228
}
12031229

12041230

1205-
exprt string_constraint_generatort::add_axioms_for_equal
1231+
exprt string_constraint_generatort::add_axioms_for_equals
12061232
(const function_application_exprt &f)
12071233
{
12081234
assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
@@ -1720,7 +1746,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of
17201746
else
17211747
assert(false);
17221748

1723-
if(refined_string_typet::is_java_string_type(c.type()))
1749+
if(refined_string_typet::is_java_string_pointer_type(c.type()))
17241750
{
17251751
string_exprt sub=add_axioms_for_string_expr(c);
17261752
return add_axioms_for_index_of_string(str, sub, from_index);
@@ -1788,7 +1814,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of
17881814
else
17891815
assert(false);
17901816

1791-
if(refined_string_typet::is_java_string_type(c.type()))
1817+
if(refined_string_typet::is_java_string_pointer_type(c.type()))
17921818
{
17931819
string_exprt sub=add_axioms_for_string_expr(c);
17941820
return add_axioms_for_last_index_of_string(str, sub, from_index);

0 commit comments

Comments
 (0)