Skip to content

Commit 8bb39ca

Browse files
smowtonsmowton
authored
Merge pull request #1427 from LAJW/feature/string-replace-single-character-strings
String.replace for single-character strings TG-810
2 parents c063d01 + 00af153 commit 8bb39ca

File tree

4 files changed

+134
-83
lines changed

4 files changed

+134
-83
lines changed

‎src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1944,6 +1944,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
19441944
cprover_equivalent_to_java_string_returning_function
19451945
["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
19461946
ID_cprover_string_replace_func;
1947+
cprover_equivalent_to_java_string_returning_function
1948+
["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
1949+
ID_cprover_string_replace_func;
19471950
cprover_equivalent_to_java_function
19481951
["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
19491952
ID_cprover_string_startswith_func;

‎src/solvers/refinement/expr_cast.h

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
/*******************************************************************\
2+
3+
Module: exprt conversion functions
4+
5+
Author: Diffblue ltd. All Rights Reserved
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Abstraction Refinement Loop
11+
12+
#ifndef CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H
13+
#define CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H
14+
15+
#include <util/optional.h>
16+
17+
/// Convert exprt to a specific type. Remove empty optional if
18+
/// conversion cannot be performed
19+
/// Generic case doesn't exist, specialize for different types accordingly
20+
/// TODO: this should go to util
21+
template<typename T>
22+
struct expr_cast_implt final { };
23+
24+
template<>
25+
struct expr_cast_implt<mp_integer> final
26+
{
27+
optionalt<mp_integer> operator()(const exprt &expr) const
28+
{
29+
mp_integer out;
30+
if(to_integer(expr, out))
31+
return {};
32+
return out;
33+
}
34+
};
35+
36+
template<>
37+
struct expr_cast_implt<std::size_t> final
38+
{
39+
optionalt<std::size_t> operator()(const exprt &expr) const
40+
{
41+
if(const auto tmp=expr_cast_implt<mp_integer>()(expr))
42+
if(tmp->is_long() && *tmp>=0)
43+
return tmp->to_long();
44+
return {};
45+
}
46+
};
47+
48+
template<>
49+
struct expr_cast_implt<string_exprt> final
50+
{
51+
optionalt<string_exprt> operator()(const exprt &expr) const
52+
{
53+
if(is_refined_string_type(expr.type()))
54+
return to_string_expr(expr);
55+
return {};
56+
}
57+
};
58+
59+
template<typename T>
60+
optionalt<T> expr_cast(const exprt& expr)
61+
{ return expr_cast_implt<T>()(expr); }
62+
63+
template<typename T>
64+
T expr_cast_v(const exprt &expr)
65+
{
66+
const auto maybe=expr_cast<T>(expr);
67+
INVARIANT(maybe, "Bad conversion");
68+
return *maybe;
69+
}
70+
71+
#endif // CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H

‎src/solvers/refinement/string_constraint_generator_transformation.cpp

Lines changed: 59 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
1313

1414
#include <solvers/refinement/string_refinement_invariant.h>
1515
#include <solvers/refinement/string_constraint_generator.h>
16+
#include "expr_cast.h"
1617

1718
/// add axioms to say that the returned string expression `res` has length `k`
1819
/// and characters at position `i` in `res` are equal to the character at
@@ -359,38 +360,70 @@ string_exprt string_constraint_generatort::add_axioms_for_char_set(
359360
return res;
360361
}
361362

362-
/// add axioms corresponding to the String.replace java function
363-
/// \par parameters: function application with three arguments, the first is a
364-
/// string,
365-
/// the second and the third are characters
363+
/// Convert two expressions to pair of chars
364+
/// If both expressions are characters, return pair of them
365+
/// If both expressions are 1-length strings, return first character of each
366+
/// Otherwise return empty optional
367+
/// \param expr1 First expression
368+
/// \param expr2 Second expression
369+
/// \return Optional pair of two expressions
370+
static optionalt<std::pair<exprt, exprt>> to_char_pair(
371+
exprt expr1, exprt expr2)
372+
{
373+
if((expr1.type().id()==ID_unsignedbv
374+
|| expr1.type().id()==ID_char)
375+
&& (expr2.type().id()==ID_char
376+
|| expr2.type().id()==ID_unsignedbv))
377+
return std::make_pair(expr1, expr2);
378+
const auto expr1_str=to_string_expr(expr1);
379+
const auto expr2_str=to_string_expr(expr2);
380+
const auto expr1_length=expr_cast<size_t>(expr1_str.length());
381+
const auto expr2_length=expr_cast<size_t>(expr2_str.length());
382+
if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
383+
return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
384+
return { };
385+
}
386+
387+
/// Add axioms corresponding to the String.replace java function
388+
/// Only supports String.replace(char, char) and
389+
/// String.replace(String, String) for single-character strings
390+
/// Returns original string in every other case (that behaviour is to
391+
/// be fixed in the future)
392+
/// \param f function application with three arguments, the first is a
393+
/// string, the second and the third are either pair of characters or
394+
/// a pair of strings
366395
/// \return a new string expression
367396
string_exprt string_constraint_generatort::add_axioms_for_replace(
368397
const function_application_exprt &f)
369398
{
370399
string_exprt str=get_string_expr(args(f, 3)[0]);
371400
const refined_string_typet &ref_type=to_refined_string_type(str.type());
372-
const exprt &old_char=args(f, 3)[1];
373-
const exprt &new_char=args(f, 3)[2];
374-
string_exprt res=fresh_string(ref_type);
375-
376-
// We add axioms:
377-
// a1 : |res| = |str|
378-
// a2 : forall qvar, 0<=qvar<|res|,
379-
// str[qvar]=oldChar => res[qvar]=newChar
380-
// !str[qvar]=oldChar => res[qvar]=str[qvar]
381-
382-
m_axioms.push_back(res.axiom_for_has_same_length_as(str));
383-
384-
symbol_exprt qvar=fresh_univ_index("QA_replace", ref_type.get_index_type());
385-
implies_exprt case1(
386-
equal_exprt(str[qvar], old_char),
387-
equal_exprt(res[qvar], new_char));
388-
implies_exprt case2(
389-
not_exprt(equal_exprt(str[qvar], old_char)),
390-
equal_exprt(res[qvar], str[qvar]));
391-
string_constraintt a2(qvar, res.length(), and_exprt(case1, case2));
392-
m_axioms.push_back(a2);
393-
return res;
401+
if(const auto maybe_chars=to_char_pair(args(f, 3)[1], args(f, 3)[2]))
402+
{
403+
const auto old_char=maybe_chars->first;
404+
const auto new_char=maybe_chars->second;
405+
string_exprt res=fresh_string(ref_type);
406+
407+
// We add axioms:
408+
// a1 : |res| = |str|
409+
// a2 : forall qvar, 0<=qvar<|res|,
410+
// str[qvar]=oldChar => res[qvar]=newChar
411+
// !str[qvar]=oldChar => res[qvar]=str[qvar]
412+
413+
m_axioms.push_back(res.axiom_for_has_same_length_as(str));
414+
415+
symbol_exprt qvar=fresh_univ_index("QA_replace", ref_type.get_index_type());
416+
implies_exprt case1(
417+
equal_exprt(str[qvar], old_char),
418+
equal_exprt(res[qvar], new_char));
419+
implies_exprt case2(
420+
not_exprt(equal_exprt(str[qvar], old_char)),
421+
equal_exprt(res[qvar], str[qvar]));
422+
string_constraintt a2(qvar, res.length(), and_exprt(case1, case2));
423+
m_axioms.push_back(a2);
424+
return res;
425+
}
426+
return str;
394427
}
395428

396429
/// add axioms corresponding to the StringBuilder.deleteCharAt java function

‎src/solvers/refinement/string_refinement.cpp

Lines changed: 1 addition & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
2626
#include <solvers/sat/satcheck.h>
2727
#include <solvers/refinement/string_constraint_instantiation.h>
2828
#include <java_bytecode/java_types.h>
29+
#include "expr_cast.h"
2930

3031
static exprt substitute_array_with_expr(const exprt &expr, const exprt &index);
3132

@@ -95,63 +96,6 @@ static exprt get_array(
9596
const std::function<exprt(const exprt &)> &super_get,
9697
const exprt &arr);
9798

98-
/// Convert exprt to a specific type. Throw bad_cast if conversion
99-
/// cannot be performed
100-
/// Generic case doesn't exist, specialize for different types accordingly
101-
/// TODO: this should go to util
102-
103-
// Tag dispatching struct
104-
105-
template<typename T>
106-
struct expr_cast_implt final { };
107-
108-
template<>
109-
struct expr_cast_implt<mp_integer> final
110-
{
111-
optionalt<mp_integer> operator()(const exprt &expr) const
112-
{
113-
mp_integer out;
114-
if(to_integer(expr, out))
115-
return {};
116-
return out;
117-
}
118-
};
119-
120-
template<>
121-
struct expr_cast_implt<std::size_t> final
122-
{
123-
optionalt<std::size_t> operator()(const exprt &expr) const
124-
{
125-
if(const auto tmp=expr_cast_implt<mp_integer>()(expr))
126-
if(tmp->is_long() && *tmp>=0)
127-
return tmp->to_long();
128-
return {};
129-
}
130-
};
131-
132-
template<>
133-
struct expr_cast_implt<string_exprt> final
134-
{
135-
optionalt<string_exprt> operator()(const exprt &expr) const
136-
{
137-
if(is_refined_string_type(expr.type()))
138-
return to_string_expr(expr);
139-
return {};
140-
}
141-
};
142-
143-
template<typename T>
144-
optionalt<T> expr_cast(const exprt& expr)
145-
{ return expr_cast_implt<T>()(expr); }
146-
147-
template<typename T>
148-
T expr_cast_v(const exprt &expr)
149-
{
150-
const auto maybe=expr_cast<T>(expr);
151-
INVARIANT(maybe, "Bad conversion");
152-
return *maybe;
153-
}
154-
15599
/// Convert index-value map to a vector of values. If a value for an
156100
/// index is not defined, set it to the value referenced by the next higher
157101
/// index. The length of the resulting vector is the key of the map's

0 commit comments

Comments
 (0)