Skip to content

Commit f747a29

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #374 from romainbrenguier/string-refine-solver
String solver back-end
2 parents ba874a4 + 20f4970 commit f747a29

22 files changed

+5821
-2
lines changed

‎src/solvers/refinement/bv_refinement.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -83,8 +83,8 @@ class bv_refinementt:public bv_pointerst
8383
void get_values(approximationt &approximation);
8484
bool is_in_conflict(approximationt &approximation);
8585

86-
void check_SAT();
87-
void check_UNSAT();
86+
virtual void check_SAT();
87+
virtual void check_UNSAT();
8888
bool progress;
8989

9090
// we refine the theory of arrays

‎src/solvers/refinement/refined_string_type.cpp

+144
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
/********************************************************************\
2+
3+
Module: Type for string expressions used by the string solver.
4+
These string expressions contain a field `length`, of type
5+
`index_type`, a field `content` of type `content_type`.
6+
This module also defines functions to recognise the C and java
7+
string types.
8+
9+
Author: Romain Brenguier, [email protected]
10+
11+
\*******************************************************************/
12+
13+
#include <solvers/refinement/refined_string_type.h>
14+
#include <ansi-c/string_constant.h>
15+
#include <util/cprover_prefix.h>
16+
17+
/*******************************************************************\
18+
19+
Constructor: refined_string_typet::refined_string_typet
20+
21+
Inputs: type of characters
22+
23+
\*******************************************************************/
24+
25+
refined_string_typet::refined_string_typet(typet char_type)
26+
{
27+
infinity_exprt infinite_index(refined_string_typet::index_type());
28+
array_typet char_array(char_type, infinite_index);
29+
components().emplace_back("length", refined_string_typet::index_type());
30+
components().emplace_back("content", char_array);
31+
}
32+
33+
/*******************************************************************\
34+
35+
Function: refined_string_typet::is_c_string_type
36+
37+
Inputs: a type
38+
39+
Outputs: Boolean telling whether the type is that of C strings
40+
41+
\*******************************************************************/
42+
43+
bool refined_string_typet::is_c_string_type(const typet &type)
44+
{
45+
return
46+
type.id()==ID_struct &&
47+
to_struct_type(type).get_tag()==CPROVER_PREFIX"string";
48+
}
49+
50+
/*******************************************************************\
51+
52+
Function: refined_string_typet::is_java_string_pointer_type
53+
54+
Inputs: a type
55+
56+
Outputs: Boolean telling whether the type is that of java string pointers
57+
58+
\*******************************************************************/
59+
60+
bool refined_string_typet::is_java_string_pointer_type(const typet &type)
61+
{
62+
if(type.id()==ID_pointer)
63+
{
64+
const pointer_typet &pt=to_pointer_type(type);
65+
const typet &subtype=pt.subtype();
66+
return is_java_string_type(subtype);
67+
}
68+
return false;
69+
}
70+
71+
/*******************************************************************\
72+
73+
Function: refined_string_typet::is_java_string_type
74+
75+
Inputs: a type
76+
77+
Outputs: Boolean telling whether the type is that of java string
78+
79+
\*******************************************************************/
80+
81+
bool refined_string_typet::is_java_string_type(const typet &type)
82+
{
83+
if(type.id()==ID_symbol)
84+
{
85+
irep_idt tag=to_symbol_type(type).get_identifier();
86+
return tag=="java::java.lang.String";
87+
}
88+
else if(type.id()==ID_struct)
89+
{
90+
irep_idt tag=to_struct_type(type).get_tag();
91+
return tag=="java.lang.String";
92+
}
93+
return false;
94+
}
95+
96+
/*******************************************************************\
97+
98+
Function: refined_string_typet::is_java_string_builder_type
99+
100+
Inputs: a type
101+
102+
Outputs: Boolean telling whether the type is that of java string builder
103+
104+
\*******************************************************************/
105+
106+
bool refined_string_typet::is_java_string_builder_type(const typet &type)
107+
{
108+
if(type.id()==ID_pointer)
109+
{
110+
const pointer_typet &pt=to_pointer_type(type);
111+
const typet &subtype=pt.subtype();
112+
if(subtype.id()==ID_struct)
113+
{
114+
irep_idt tag=to_struct_type(subtype).get_tag();
115+
return tag=="java.lang.StringBuilder";
116+
}
117+
}
118+
return false;
119+
}
120+
121+
/*******************************************************************\
122+
123+
Function: refined_string_typet::is_java_char_sequence_type
124+
125+
Inputs: a type
126+
127+
Outputs: Boolean telling whether the type is that of java char sequence
128+
129+
\*******************************************************************/
130+
131+
bool refined_string_typet::is_java_char_sequence_type(const typet &type)
132+
{
133+
if(type.id()==ID_pointer)
134+
{
135+
const pointer_typet &pt=to_pointer_type(type);
136+
const typet &subtype=pt.subtype();
137+
if(subtype.id()==ID_struct)
138+
{
139+
const irep_idt &tag=to_struct_type(subtype).get_tag();
140+
return tag=="java.lang.CharSequence";
141+
}
142+
}
143+
return false;
144+
}

‎src/solvers/refinement/refined_string_type.h

+112
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
/********************************************************************\
2+
3+
Module: Type for string expressions used by the string solver.
4+
These string expressions contain a field `length`, of type
5+
`index_type`, a field `content` of type `content_type`.
6+
This module also defines functions to recognise the C and java
7+
string types.
8+
9+
Author: Romain Brenguier, [email protected]
10+
11+
\*******************************************************************/
12+
13+
#ifndef CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H
14+
#define CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H
15+
16+
#include <util/std_types.h>
17+
#include <util/std_expr.h>
18+
#include <util/arith_tools.h>
19+
#include <util/expr_util.h>
20+
#include <ansi-c/c_types.h>
21+
#include <java_bytecode/java_types.h>
22+
23+
// Internal type used for string refinement
24+
class refined_string_typet: public struct_typet
25+
{
26+
public:
27+
explicit refined_string_typet(typet char_type);
28+
29+
// Type for the content (list of characters) of a string
30+
const array_typet &get_content_type() const
31+
{
32+
assert(components().size()==2);
33+
return to_array_type(components()[1].type());
34+
}
35+
36+
const typet &get_char_type()
37+
{
38+
assert(components().size()==2);
39+
return components()[0].type();
40+
}
41+
42+
const typet &get_index_type() const
43+
{
44+
return get_content_type().size().type();
45+
}
46+
47+
static typet index_type()
48+
{
49+
return signed_int_type();
50+
}
51+
52+
static typet java_index_type()
53+
{
54+
return java_int_type();
55+
}
56+
57+
// For C the unrefined string type is __CPROVER_string, for java it is a
58+
// pointer to a struct with tag java.lang.String
59+
60+
static bool is_c_string_type(const typet &type);
61+
62+
static bool is_java_string_pointer_type(const typet &type);
63+
64+
static bool is_java_string_type(const typet &type);
65+
66+
static bool is_java_string_builder_type(const typet &type);
67+
68+
static bool is_java_char_sequence_type(const typet &type);
69+
70+
static typet get_char_type(const exprt &expr)
71+
{
72+
if(is_c_string_type(expr.type()))
73+
return char_type();
74+
else
75+
return java_char_type();
76+
}
77+
78+
static typet get_index_type(const exprt &expr)
79+
{
80+
if(is_c_string_type(expr.type()))
81+
return index_type();
82+
else
83+
return java_index_type();
84+
}
85+
86+
static bool is_unrefined_string_type(const typet &type)
87+
{
88+
return (
89+
is_c_string_type(type) ||
90+
is_java_string_pointer_type(type) ||
91+
is_java_string_builder_type(type) ||
92+
is_java_char_sequence_type(type));
93+
}
94+
95+
static bool is_unrefined_string(const exprt &expr)
96+
{
97+
return (is_unrefined_string_type(expr.type()));
98+
}
99+
100+
constant_exprt index_of_int(int i) const
101+
{
102+
return from_integer(i, get_index_type());
103+
}
104+
};
105+
106+
const refined_string_typet &to_refined_string_type(const typet &type)
107+
{
108+
assert(type.id()==ID_struct);
109+
return static_cast<const refined_string_typet &>(type);
110+
}
111+
112+
#endif

0 commit comments

Comments
 (0)