Skip to content

Commit 673b3a4

Browse files
Move utility functions to string_refinement_util
This reduces the size of string_refinement files and seperate functions that could be reused outside of string_refinement, for instace for unit testing.
1 parent 80bbb03 commit 673b3a4

File tree

4 files changed

+119
-107
lines changed

4 files changed

+119
-107
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 0 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -283,107 +283,6 @@ static void substitute_function_applications_in_equations(
283283
eq.rhs() = substitute_function_applications(eq.rhs(), generator);
284284
}
285285

286-
/// For now, any unsigned bitvector type of width smaller or equal to 16 is
287-
/// considered a character.
288-
/// \note type that are not characters maybe detected as characters (for
289-
/// instance unsigned char in C), this will make dec_solve do unnecessary
290-
/// steps for these, but should not affect correctness.
291-
/// \param type: a type
292-
/// \return true if the given type represents characters
293-
bool is_char_type(const typet &type)
294-
{
295-
return type.id() == ID_unsignedbv &&
296-
to_unsignedbv_type(type).get_width() <= 16;
297-
}
298-
299-
/// Distinguish char array from other types.
300-
/// For now, any unsigned bitvector type is considered a character.
301-
/// \param type: a type
302-
/// \param ns: namespace
303-
/// \return true if the given type is an array of characters
304-
bool is_char_array_type(const typet &type, const namespacet &ns)
305-
{
306-
if(type.id()==ID_symbol)
307-
return is_char_array_type(ns.follow(type), ns);
308-
return type.id() == ID_array && is_char_type(type.subtype());
309-
}
310-
311-
/// For now, any unsigned bitvector type is considered a character.
312-
/// \param type: a type
313-
/// \return true if the given type represents a pointer to characters
314-
bool is_char_pointer_type(const typet &type)
315-
{
316-
return type.id() == ID_pointer && is_char_type(type.subtype());
317-
}
318-
319-
/// \param type: a type
320-
/// \param pred: a predicate
321-
/// \return true if one of the subtype of `type` satisfies predicate `pred`.
322-
/// The meaning of "subtype" is in the algebraic datatype sense:
323-
/// for example, the subtypes of a struct are the types of its
324-
/// components, the subtype of a pointer is the type it points to,
325-
/// etc...
326-
/// For instance in the type `t` defined by
327-
/// `{ int a; char[] b; double * c; { bool d} e}`, `int`, `char`,
328-
/// `double` and `bool` are subtypes of `t`.
329-
bool has_subtype(
330-
const typet &type,
331-
const std::function<bool(const typet &)> &pred)
332-
{
333-
if(pred(type))
334-
return true;
335-
336-
if(type.id() == ID_struct || type.id() == ID_union)
337-
{
338-
const struct_union_typet &struct_type = to_struct_union_type(type);
339-
return std::any_of(
340-
struct_type.components().begin(),
341-
struct_type.components().end(), // NOLINTNEXTLINE
342-
[&](const struct_union_typet::componentt &comp) {
343-
return has_subtype(comp.type(), pred);
344-
});
345-
}
346-
347-
return std::any_of( // NOLINTNEXTLINE
348-
type.subtypes().begin(), type.subtypes().end(), [&](const typet &t) {
349-
return has_subtype(t, pred);
350-
});
351-
}
352-
353-
/// \param type: a type
354-
/// \return true if a subtype of `type` is an pointer of characters.
355-
/// The meaning of "subtype" is in the algebraic datatype sense:
356-
/// for example, the subtypes of a struct are the types of its
357-
/// components, the subtype of a pointer is the type it points to,
358-
/// etc...
359-
static bool has_char_pointer_subtype(const typet &type)
360-
{
361-
return has_subtype(type, is_char_pointer_type);
362-
}
363-
364-
/// \param type: a type
365-
/// \return true if a subtype of `type` is string_typet.
366-
/// The meaning of "subtype" is in the algebraic datatype sense:
367-
/// for example, the subtypes of a struct are the types of its
368-
/// components, the subtype of a pointer is the type it points to,
369-
/// etc...
370-
static bool has_string_subtype(const typet &type)
371-
{
372-
// NOLINTNEXTLINE
373-
return has_subtype(
374-
type, [](const typet &subtype) { return subtype == string_typet(); });
375-
}
376-
377-
/// \param expr: an expression
378-
/// \param ns: namespace
379-
/// \return true if a subexpression of `expr` is an array of characters
380-
static bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
381-
{
382-
for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
383-
if(is_char_array_type(it->type(), ns))
384-
return true;
385-
return false;
386-
}
387286

388287
void replace_symbols_in_equations(
389288
const union_find_replacet &symbol_resolve,

src/solvers/refinement/string_refinement.h

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -93,12 +93,6 @@ exprt concretize_arrays_in_expression(
9393
std::size_t string_max_length,
9494
const namespacet &ns);
9595

96-
bool is_char_array_type(const typet &type, const namespacet &ns);
97-
98-
bool has_subtype(
99-
const typet &type,
100-
const std::function<bool(const typet &)> &pred);
101-
10296
// Declaration required for unit-test:
10397
union_find_replacet string_identifiers_resolution_from_equations(
10498
std::vector<equal_exprt> &equations,

src/solvers/refinement/string_refinement_util.cpp

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,71 @@
1010
#include <numeric>
1111
#include <util/arith_tools.h>
1212
#include <util/std_expr.h>
13+
#include <util/expr_iterator.h>
1314
#include "string_refinement_util.h"
1415

16+
bool is_char_type(const typet &type)
17+
{
18+
return type.id() == ID_unsignedbv &&
19+
to_unsignedbv_type(type).get_width() <= 16;
20+
}
21+
22+
bool is_char_array_type(const typet &type, const namespacet &ns)
23+
{
24+
if(type.id() == ID_symbol)
25+
return is_char_array_type(ns.follow(type), ns);
26+
return type.id() == ID_array && is_char_type(type.subtype());
27+
}
28+
29+
bool is_char_pointer_type(const typet &type)
30+
{
31+
return type.id() == ID_pointer && is_char_type(type.subtype());
32+
}
33+
34+
bool has_subtype(
35+
const typet &type,
36+
const std::function<bool(const typet &)> &pred)
37+
{
38+
if(pred(type))
39+
return true;
40+
41+
if(type.id() == ID_struct || type.id() == ID_union)
42+
{
43+
const struct_union_typet &struct_type = to_struct_union_type(type);
44+
return std::any_of(
45+
struct_type.components().begin(),
46+
struct_type.components().end(), // NOLINTNEXTLINE
47+
[&](const struct_union_typet::componentt &comp) {
48+
return has_subtype(comp.type(), pred);
49+
});
50+
}
51+
52+
return std::any_of( // NOLINTNEXTLINE
53+
type.subtypes().begin(), type.subtypes().end(), [&](const typet &t) {
54+
return has_subtype(t, pred);
55+
});
56+
}
57+
58+
bool has_char_pointer_subtype(const typet &type)
59+
{
60+
return has_subtype(type, is_char_pointer_type);
61+
}
62+
63+
bool has_string_subtype(const typet &type)
64+
{
65+
// NOLINTNEXTLINE
66+
return has_subtype(
67+
type, [](const typet &subtype) { return subtype == string_typet(); });
68+
}
69+
70+
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
71+
{
72+
for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
73+
if(is_char_array_type(it->type(), ns))
74+
return true;
75+
return false;
76+
}
77+
1578
sparse_arrayt::sparse_arrayt(const with_exprt &expr)
1679
{
1780
auto ref = std::ref(static_cast<const exprt &>(expr));

src/solvers/refinement/string_refinement_util.h

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,62 @@
1111

1212
#include "string_constraint.h"
1313

14+
/// For now, any unsigned bitvector type of width smaller or equal to 16 is
15+
/// considered a character.
16+
/// \note type that are not characters maybe detected as characters (for
17+
/// instance unsigned char in C), this will make dec_solve do unnecessary
18+
/// steps for these, but should not affect correctness.
19+
/// \param type: a type
20+
/// \return true if the given type represents characters
21+
bool is_char_type(const typet &type);
22+
23+
/// Distinguish char array from other types.
24+
/// For now, any unsigned bitvector type is considered a character.
25+
/// \param type: a type
26+
/// \param ns: namespace
27+
/// \return true if the given type is an array of characters
28+
bool is_char_array_type(const typet &type, const namespacet &ns);
29+
30+
/// For now, any unsigned bitvector type is considered a character.
31+
/// \param type: a type
32+
/// \return true if the given type represents a pointer to characters
33+
bool is_char_pointer_type(const typet &type);
34+
35+
/// \param type: a type
36+
/// \param pred: a predicate
37+
/// \return true if one of the subtype of `type` satisfies predicate `pred`.
38+
/// The meaning of "subtype" is in the algebraic datatype sense:
39+
/// for example, the subtypes of a struct are the types of its
40+
/// components, the subtype of a pointer is the type it points to,
41+
/// etc...
42+
/// For instance in the type `t` defined by
43+
/// `{ int a; char[] b; double * c; { bool d} e}`, `int`, `char`,
44+
/// `double` and `bool` are subtypes of `t`.
45+
bool has_subtype(
46+
const typet &type,
47+
const std::function<bool(const typet &)> &pred);
48+
49+
/// \param type: a type
50+
/// \return true if a subtype of `type` is an pointer of characters.
51+
/// The meaning of "subtype" is in the algebraic datatype sense:
52+
/// for example, the subtypes of a struct are the types of its
53+
/// components, the subtype of a pointer is the type it points to,
54+
/// etc...
55+
bool has_char_pointer_subtype(const typet &type);
56+
57+
/// \param type: a type
58+
/// \return true if a subtype of `type` is string_typet.
59+
/// The meaning of "subtype" is in the algebraic datatype sense:
60+
/// for example, the subtypes of a struct are the types of its
61+
/// components, the subtype of a pointer is the type it points to,
62+
/// etc...
63+
bool has_string_subtype(const typet &type);
64+
65+
/// \param expr: an expression
66+
/// \param ns: namespace
67+
/// \return true if a subexpression of `expr` is an array of characters
68+
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
69+
1470
struct index_set_pairt
1571
{
1672
std::map<exprt, std::set<exprt>> cumulative;

0 commit comments

Comments
 (0)