replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #1162 from jasigal/fix/invalid-string-constraint-transformations#779 

Fixed invalid transformations on string constraints and added invariant checking.
This commit is contained in:
Chris Smowton 2017-07-26 15:54:32 +01:00 committed by GitHub
parent f798feff6a c306d56e72
commit bcbb6fa0fb
10 changed files with 343 additions and 245 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
regression/strings-smoke-tests/java_case/test_case.class
View File

Binary file not shown.

2
regression/strings-smoke-tests/java_contains/test.desc
View File

@ -1,6 +1,6 @@
CORE
test_contains.class
--refine-strings
--refine-strings --string-max-length 100
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$

2
src/doxyfile
View File

@ -1473,7 +1473,7 @@ FORMULA_TRANSPARENT = YES
# The default value is: NO.
# This tag requires that the tag GENERATE_HTML is set to YES.
USE_MATHJAX = NO
USE_MATHJAX = YES
# When MathJax is enabled you can set the default output format to be used for
# the MathJax output. See the MathJax site (see:

33
src/solvers/refinement/string_constraint.h
View File

@ -24,6 +24,30 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
#include <solvers/refinement/bv_refinement.h>
#include <solvers/refinement/string_refinement_invariant.h>
#include <util/refined_string_type.h>
#include <langapi/language_util.h>
/*! \brief Universally quantified string constraint
This represents a universally quantified string constraint as laid out in
DOI: 10.1007/978-3-319-03077-7. The paper seems to specify a universal
constraint as follows.
A universal constraint is of the form \f$\forall n. L(n) \rightarrow
P(n, s_0,\ldots, s_k)\f$ where
1. \f$L(n)\f$ does not contain string indices [possibly not required, but
implied by examples]
2. \f$\forall n. L(n) \rightarrow P'\left(s_0[f_0(n)],\ldots, s_k[f_k(n)]
\right)\f$, i.e. when focusing on one specific string, all indices are
the same [stated in a roundabout manner]
3. Each \f$f\f$ is linear and therefore has an inverse [explicitly stated]
4. \f$L(n)\f$ and \f$P(n, s_0,\ldots, s_k)\f$ may contain other (free)
variables, but in \f$P\f$, \f$n\f$ can only occur as an argument to an
\f$f\f$ [explicitly stated, implied]
We extend this slightly by restricting n to be in a specific range, but this
is another implication which can be pushed in to \f$L(n)\f$.
*/
class string_constraintt: public exprt
{
@ -114,6 +138,15 @@ extern inline string_constraintt &to_string_constraint(exprt &expr)
return static_cast<string_constraintt &>(expr);
}
inline static std::string from_expr(
const namespacet &ns,
const irep_idt &identifier,
const string_constraintt &expr)
{
return from_expr(ns, identifier, expr.premise())+" => "+
from_expr(ns, identifier, expr.body());
}
class string_not_contains_constraintt: public exprt
{
public:

164
src/solvers/refinement/string_constraint_generator_indexof.cpp
View File

@ -15,7 +15,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
#include <solvers/refinement/string_constraint_generator.h>
/// Add axioms stating that the returned value is the index within str of the
/// first occurence of c starting the search at from_index, or -1 if no such
/// first occurrence of c starting the search at from_index, or -1 if no such
/// character occurs at or after position from_index.
/// \param str: a string expression
/// \param c: an expression representing a character
@ -69,7 +69,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
}
/// Add axioms stating that the returned value is the index within haystack of
/// the first occurence of needle starting the search at from_index, or -1 if
/// the first occurrence of needle starting the search at from_index, or -1 if
/// needle does not occur at or after position from_index.
/// \param haystack: a string expression
/// \param needle: a string expression
@ -92,7 +92,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
// contains ==> haystack[n+offset]=needle[n]
// a4 : forall n:[from_index,offset[.
// contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]])
// a5: forall n:[from_index,|haystack|-|needle|[.
// a5: forall n:[from_index,|haystack|-|needle|].
// !contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m])
implies_exprt a1(
@ -116,70 +116,35 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]));
axioms.push_back(a3);
if(!is_constant_string(needle))
{
// string_not contains_constraintt are formulas of the form:
// forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
string_not_contains_constraintt a4(
from_index,
offset,
contains,
from_integer(0, index_type),
needle.length(),
haystack,
needle);
axioms.push_back(a4);
// string_not contains_constraintt are formulas of the form:
// forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
string_not_contains_constraintt a4(
from_index,
offset,
contains,
from_integer(0, index_type),
needle.length(),
haystack,
needle);
axioms.push_back(a4);
string_not_contains_constraintt a5(
from_index,
string_not_contains_constraintt a5(
from_index,
plus_exprt( // Add 1 for inclusive upper bound.
minus_exprt(haystack.length(), needle.length()),
not_exprt(contains),
from_integer(0, index_type),
needle.length(),
haystack,
needle);
axioms.push_back(a5);
}
else
{
// Unfold the existential quantifier as a disjunction in case of a constant
// a4 && a5 <=> a6:
// forall n:[from_index,|haystack|-|needle|].
// !contains || n < offset ==>
// haystack[n] != needle[0] || ... ||
// haystack[n+|needle|-1] != needle[|needle|-1]
symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
mp_integer sub_length;
INVARIANT(
!to_integer(needle.length(), sub_length),
string_refinement_invariantt("a constant string must have constant "
"length"));
exprt::operandst disjuncts;
for(mp_integer offset=0; offset<sub_length; ++offset)
{
exprt expr_offset=from_integer(offset, index_type);
plus_exprt shifted(expr_offset, qvar2);
disjuncts.push_back(
not_exprt(equal_exprt(haystack[shifted], needle[expr_offset])));
}
or_exprt premise(
not_exprt(contains), binary_relation_exprt(qvar2, ID_lt, offset));
minus_exprt length_diff(haystack.length(), needle.length());
string_constraintt a6(
qvar2,
from_index,
plus_exprt(from_integer(1, index_type), length_diff),
premise,
disjunction(disjuncts));
axioms.push_back(a6);
}
from_integer(1, index_type)),
not_exprt(contains),
from_integer(0, index_type),
needle.length(),
haystack,
needle);
axioms.push_back(a5);
return offset;
}
/// Add axioms stating that the returned value is the index within haystack of
/// the last occurence of needle starting the search backward at from_index (ie
/// the last occurrence of needle starting the search backward at from_index (ie
/// the index is smaller or equal to from_index), or -1 if needle does not occur
/// before from_index.
/// \param haystack: a string expression
@ -235,62 +200,25 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
from_index,
length_diff);
if(!is_constant_string(needle))
{
string_not_contains_constraintt a4(
plus_exprt(offset, from_integer(1, index_type)),
plus_exprt(end_index, from_integer(1, index_type)),
contains,
from_integer(0, index_type),
needle.length(),
haystack,
needle);
axioms.push_back(a4);
string_not_contains_constraintt a4(
plus_exprt(offset, from_integer(1, index_type)),
plus_exprt(end_index, from_integer(1, index_type)),
contains,
from_integer(0, index_type),
needle.length(),
haystack,
needle);
axioms.push_back(a4);
string_not_contains_constraintt a5(
from_integer(0, index_type),
plus_exprt(end_index, from_integer(1, index_type)),
not_exprt(contains),
from_integer(0, index_type),
needle.length(),
haystack,
needle);
axioms.push_back(a5);
}
else
{
// Unfold the existential quantifier as a disjunction in case of a constant
// a4 && a5 <=> a6:
// forall n:[0, min(from_index, |haystack| - |needle|)].
// !contains || (n > offset) ==>
// haystack[n] != needle[0] || ... ||
// haystack[n+|needle|-1] != needle[|needle|-1]
symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
mp_integer sub_length;
INVARIANT(
!to_integer(needle.length(), sub_length),
string_refinement_invariantt("a constant string must have constant "
"length"));
exprt::operandst disjuncts;
for(mp_integer offset=0; offset<sub_length; ++offset)
{
exprt expr_offset=from_integer(offset, index_type);
plus_exprt shifted(expr_offset, qvar2);
disjuncts.push_back(
not_exprt(equal_exprt(haystack[shifted], needle[expr_offset])));
}
or_exprt premise(
not_exprt(contains), binary_relation_exprt(qvar2, ID_gt, offset));
string_constraintt a6(
qvar2,
from_integer(0, index_type),
plus_exprt(from_integer(1, index_type), end_index),
premise,
disjunction(disjuncts));
axioms.push_back(a6);
}
string_not_contains_constraintt a5(
from_integer(0, index_type),
plus_exprt(end_index, from_integer(1, index_type)),
not_exprt(contains),
from_integer(0, index_type),
needle.length(),
haystack,
needle);
axioms.push_back(a5);
return offset;
}
@ -333,7 +261,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
}
/// Add axioms stating that the returned value is the index within str of the
/// last occurence of c starting the search backward at from_index, or -1 if no
/// last occurrence of c starting the search backward at from_index, or -1 if no
/// such character occurs at or before position from_index.
/// \param str: a string expression
/// \param c: an expression representing a character
@ -373,7 +301,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
equal_exprt(str[index], c)));
axioms.push_back(a3);
symbol_exprt n=fresh_univ_index("QA_last_index_of", index_type);
symbol_exprt n=fresh_univ_index("QA_last_index_of1", index_type);
string_constraintt a4(
n,
plus_exprt(index, index1),
@ -382,7 +310,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
not_exprt(equal_exprt(str[n], c)));
axioms.push_back(a4);
symbol_exprt m=fresh_univ_index("QA_last_index_of", index_type);
symbol_exprt m=fresh_univ_index("QA_last_index_of2", index_type);
string_constraintt a5(
m,
from_index_plus_one,

1
src/solvers/refinement/string_constraint_generator_main.cpp
View File

@ -164,7 +164,6 @@ string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
{
java_content=dereference_exprt(java_content, java_content.type());
}
refined_string_typet type(java_int_type(), java_char_type());
return string_exprt(length, java_content, type);

77
src/solvers/refinement/string_constraint_generator_testing.cpp
View File

@ -187,7 +187,6 @@ exprt string_constraint_generatort::add_axioms_for_contains(
PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
string_exprt s0=get_string_expr(args(f, 2)[0]);
string_exprt s1=get_string_expr(args(f, 2)[1]);
bool constant=is_constant_string(s1);
symbol_exprt contains=fresh_boolean("contains");
const refined_string_typet ref_type=to_refined_string_type(s0.type());
@ -218,66 +217,24 @@ exprt string_constraint_generatort::add_axioms_for_contains(
equal_exprt(startpos, from_integer(-1, index_type)));
axioms.push_back(a3);
if(constant)
{
// If the string is constant, we can use a more efficient axiom for a4:
// contains ==> AND_{i < |s1|} s1[i] = s0[startpos + i]
mp_integer s1_length;
INVARIANT(
!to_integer(s1.length(), s1_length),
string_refinement_invariantt("a constant string expression must have a "
"constant length"));
exprt::operandst conjuncts;
for(mp_integer i=0; i<s1_length; ++i)
{
exprt expr_i=from_integer(i, index_type);
plus_exprt shifted_i(expr_i, startpos);
conjuncts.push_back(equal_exprt(s1[expr_i], s0[shifted_i]));
}
implies_exprt a4(contains, conjunction(conjuncts));
axioms.push_back(a4);
symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
exprt qvar_shifted=plus_exprt(qvar, startpos);
string_constraintt a4(
qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
axioms.push_back(a4);
// The a5 constraint for constant strings translates to:
// !contains ==> |s1| > |s0| ||
// (forall qvar <= |s0| - |s1|.
// !(AND_{i < |s1|} s1[i] == s0[i + qvar])
//
// which we implement as:
// forall qvar <= |s0| - |s1|. (!contains && |s0| >= |s1|)
// ==> !(AND_{i < |s1|} (s1[i] == s0[qvar+i]))
symbol_exprt qvar=fresh_univ_index("QA_contains_constant", index_type);
exprt::operandst conjuncts1;
for(mp_integer i=0; i<s1_length; ++i)
{
exprt expr_i=from_integer(i, index_type);
plus_exprt shifted_i(expr_i, qvar);
conjuncts1.push_back(equal_exprt(s1[expr_i], s0[shifted_i]));
}
// We rewrite axiom a4 as:
// forall startpos <= |s0|-|s1|. (!contains && |s0| >= |s1|)
// ==> exists witness < |s1|. s1[witness] != s0[startpos+witness]
string_not_contains_constraintt a5(
from_integer(0, index_type),
plus_exprt(from_integer(1, index_type), length_diff),
and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)),
from_integer(0, index_type),
s1.length(),
s0,
s1);
axioms.push_back(a5);
string_constraintt a5(
qvar,
plus_exprt(from_integer(1, index_type), length_diff),
and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)),
not_exprt(conjunction(conjuncts1)));
axioms.push_back(a5);
}
else
{
symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
exprt qvar_shifted=plus_exprt(qvar, startpos);
string_constraintt a4(
qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
axioms.push_back(a4);
// We rewrite axiom a4 as:
// forall startpos <= |s0|-|s1|. (!contains && |s0| >= |s1|)
// ==> exists witness < |s1|. s1[witness] != s0[startpos+witness]
string_not_contains_constraintt a5(
from_integer(0, index_type),
plus_exprt(from_integer(1, index_type), length_diff),
and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)),
from_integer(0, index_type), s1.length(), s0, s1);
axioms.push_back(a5);
}
return typecast_exprt(contains, f.type());
}

28
src/solvers/refinement/string_constraint_generator_transformation.cpp
View File

@ -287,30 +287,38 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case(
exprt char_a=constant_char('a', char_type);
exprt char_A=constant_char('A', char_type);
exprt char_z=constant_char('z', char_type);
exprt char_Z=constant_char('Z', char_type);
// TODO: add support for locales using case mapping information
// from the UnicodeData file.
// We add axioms:
// a1 : |res| = |str|
// a2 : forall idx<str.length, 'a'<=str[idx]<='z' => res[idx]=str[idx]+'A'-'a'
// a3 : forall idx<str.length, !('a'<=str[idx]<='z') => res[idx]=str[idx]
// a2 : forall idx1<str.length, 'a'<=str[idx1]<='z' =>
// res[idx1]=str[idx1]+'A'-'a'
// a3 : forall idx2<str.length, !('a'<=str[idx2]<='z') => res[idx2]=str[idx2]
// Note that index expressions are only allowed in the body of universal
// axioms, so we use a trivial premise and push our premise into the body.
exprt a1=res.axiom_for_has_same_length_as(str);
axioms.push_back(a1);
symbol_exprt idx=fresh_univ_index("QA_upper_case", index_type);
symbol_exprt idx1=fresh_univ_index("QA_upper_case1", index_type);
exprt is_lower_case=and_exprt(
binary_relation_exprt(char_a, ID_le, str[idx]),
binary_relation_exprt(str[idx], ID_le, char_z));
binary_relation_exprt(char_a, ID_le, str[idx1]),
binary_relation_exprt(str[idx1], ID_le, char_z));
minus_exprt diff(char_A, char_a);
equal_exprt convert(res[idx], plus_exprt(str[idx], diff));
string_constraintt a2(idx, res.length(), is_lower_case, convert);
equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff));
implies_exprt body1(is_lower_case, convert);
string_constraintt a2(idx1, res.length(), body1);
axioms.push_back(a2);
equal_exprt eq(res[idx], str[idx]);
string_constraintt a3(idx, res.length(), not_exprt(is_lower_case), eq);
symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type);
exprt is_not_lower_case=not_exprt(and_exprt(
binary_relation_exprt(char_a, ID_le, str[idx2]),
binary_relation_exprt(str[idx2], ID_le, char_z)));
equal_exprt eq(res[idx2], str[idx2]);
implies_exprt body2(is_not_lower_case, eq);
string_constraintt a3(idx2, res.length(), body2);
axioms.push_back(a3);
return res;
}

274
src/solvers/refinement/string_refinement.cpp
View File

@ -19,6 +19,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
#include <sstream>
#include <iomanip>
#include <stack>
#include <ansi-c/string_constant.h>
#include <util/cprover_prefix.h>
#include <util/replace_expr.h>
@ -210,7 +211,7 @@ void string_refinementt::set_char_array_equality(
/// remove functions applications and create the necessary axioms
/// \par parameters: an expression containing function applications
/// \return an epression containing no function application
/// \return an expression containing no function application
exprt string_refinementt::substitute_function_applications(exprt expr)
{
for(size_t i=0; i<expr.operands().size(); ++i)
@ -517,6 +518,10 @@ decision_proceduret::resultt string_refinementt::dec_solve()
if(axiom.id()==ID_string_constraint)
{
string_constraintt c=to_string_constraint(axiom);
DATA_INVARIANT(
is_valid_string_constraint(c),
string_refinement_invariantt(
"string constraints satisfy their invariant"));
universal_axioms.push_back(c);
}
else if(axiom.id()==ID_string_not_contains_constraint)
@ -790,7 +795,7 @@ exprt string_refinementt::get_array(const exprt &arr) const
}
/// convert the content of a string to a more readable representation. This
/// should only be used for debbuging.
/// should only be used for debugging.
/// \par parameters: a constant array expression and a integer expression
/// \return a string
std::string string_refinementt::string_of_array(const array_exprt &arr)
@ -1017,20 +1022,19 @@ void string_refinementt::substitute_array_access(exprt &expr) const
}
/// Negates the constraint to be fed to a solver. The intended usage is to find
/// an assignement of the universal variable that would violate the axiom. To
/// an assignment of the universal variable that would violate the axiom. To
/// avoid false positives, the symbols other than the universal variable should
/// have been replaced by their valuation in the current model.
/// \pre Symbols other than the universal variable should have been replaced by
/// their valuation in the current model.
/// \param axiom: the not_contains constraint to add the negation of
/// \param val: the existential witness for the axiom
/// \param univ_var: the universal variable for the negation of the axiom
/// \return: the negation of the axiom under the current evaluation
exprt string_refinementt::negation_of_not_contains_constraint(
static exprt negation_of_not_contains_constraint(
const string_not_contains_constraintt &axiom,
const exprt &val,
const symbol_exprt &univ_var)
{
// If the for all is vacuously true, the negation is false.
exprt lbu=axiom.univ_lower_bound();
exprt ubu=axiom.univ_upper_bound();
if(lbu.id()==ID_constant && ubu.id()==ID_constant)
@ -1039,51 +1043,53 @@ exprt string_refinementt::negation_of_not_contains_constraint(
to_integer(to_constant_expr(lbu), lb_int);
to_integer(to_constant_expr(ubu), ub_int);
if(ub_int<=lb_int)
{
debug() << "empty constraint with current model" << eom;
return false_exprt();
}
}
exprt lbe=axiom.exists_lower_bound();
exprt ube=axiom.exists_upper_bound();
if(axiom.premise()==false_exprt())
{
debug() << "(string_refinement::check_axioms) adding false" << eom;
return false_exprt();
}
mp_integer lbe_int, ube_int;
to_integer(to_constant_expr(lbe), lbe_int);
to_integer(to_constant_expr(ube), ube_int);
// If the premise is false, the implication is trivially true, so the
// negation is false.
if(axiom.premise()==false_exprt())
return false_exprt();
// Witness is the Skolem function for the existential, which we evaluate at
// univ_var.
and_exprt univ_bounds(
binary_relation_exprt(lbu, ID_le, univ_var),
binary_relation_exprt(ubu, ID_gt, univ_var));
and_exprt exists_bounds(
binary_relation_exprt(lbe, ID_le, val),
binary_relation_exprt(ube, ID_gt, val));
equal_exprt equal_chars(
axiom.s0()[plus_exprt(univ_var, val)],
axiom.s1()[val]);
and_exprt negaxiom(univ_bounds, axiom.premise(), exists_bounds, equal_chars);
debug() << "(sr::check_axioms) negated not_contains axiom: "
<< from_expr(ns, "", negaxiom) << eom;
substitute_array_access(negaxiom);
// The negated existential becomes an universal, and this is the unrolling of
// that universal quantifier.
std::vector<exprt> conjuncts;
for(mp_integer i=lbe_int; i<ube_int; ++i)
{
const constant_exprt i_exprt=from_integer(i, univ_var.type());
const equal_exprt equal_chars(
axiom.s0()[plus_exprt(univ_var, i_exprt)],
axiom.s1()[i_exprt]);
conjuncts.push_back(equal_chars);
}
exprt equal_strings=conjunction(conjuncts);
and_exprt negaxiom(univ_bounds, axiom.premise(), equal_strings);
return negaxiom;
}
/// Negates the constraint to be fed to a solver. The intended usage is to find
/// an assignement of the universal variable that would violate the axiom. To
/// an assignment of the universal variable that would violate the axiom. To
/// avoid false positives, the symbols other than the universal variable should
/// have been replaced by their valuation in the current model.
/// \pre Symbols other than the universal variable should have been replaced by
/// their valuation in the current model.
/// \param axiom: the not_contains constraint to add the negation of
/// \return: the negation of the axiom under the current evaluation
exprt string_refinementt::negation_of_constraint(
const string_constraintt &axiom)
static exprt negation_of_constraint(const string_constraintt &axiom)
{
// If the for all is vacuously true, the negation is false.
exprt lb=axiom.lower_bound();
exprt ub=axiom.upper_bound();
if(lb.id()==ID_constant && ub.id()==ID_constant)
@ -1092,24 +1098,17 @@ exprt string_refinementt::negation_of_constraint(
to_integer(to_constant_expr(lb), lb_int);
to_integer(to_constant_expr(ub), ub_int);
if(ub_int<=lb_int)
{
debug() << "empty constraint with current model" << eom;
return false_exprt();
}
}
// If the premise is false, the implication is trivially true, so the
// negation is false.
if(axiom.premise()==false_exprt())
{
debug() << "(string_refinement::check_axioms) adding false" << eom;
return false_exprt();
}
and_exprt premise(axiom.premise(), axiom.univ_within_bounds());
and_exprt negaxiom(premise, not_exprt(axiom.body()));
debug() << "(sr::check_axioms) negated axiom: "
<< from_expr(ns, "", negaxiom) << eom;
substitute_array_access(negaxiom);
return negaxiom;
}
@ -1140,7 +1139,10 @@ bool string_refinementt::check_axioms()
const string_constraintt axiom_in_model(
univ_var, get(bound_inf), get(bound_sup), get(prem), get(body));
const exprt negaxiom=negation_of_constraint(axiom_in_model);
exprt negaxiom=negation_of_constraint(axiom_in_model);
debug() << "(string_refinementt::check_axioms) Adding negated constraint: "
<< from_expr(ns, "", negaxiom) << eom;
substitute_array_access(negaxiom);
exprt witness;
bool is_sat=is_axiom_sat(negaxiom, univ_var, witness);
@ -1172,8 +1174,6 @@ bool string_refinementt::check_axioms()
symbol_exprt univ_var=generator.fresh_univ_index(
"not_contains_univ_var", nc_axiom.s0().length().type());
exprt wit=generator.get_witness_of(nc_axiom, univ_var);
exprt val=get(wit);
const string_not_contains_constraintt nc_axiom_in_model(
get(univ_bound_inf),
get(univ_bound_sup),
@ -1183,8 +1183,11 @@ bool string_refinementt::check_axioms()
to_string_expr(get(s0)),
to_string_expr(get(s1)));
const exprt negaxiom=negation_of_not_contains_constraint(
nc_axiom_in_model, val, univ_var);
exprt negaxiom=negation_of_not_contains_constraint(
nc_axiom_in_model, univ_var);
debug() << "(string_refinementt::check_axioms) Adding negated constraint: "
<< from_expr(ns, "", negaxiom) << eom;
substitute_array_access(negaxiom);
exprt witness;
bool is_sat=is_axiom_sat(negaxiom, univ_var, witness);
@ -1235,7 +1238,7 @@ bool string_refinementt::check_axioms()
}
}
/// \par parameters: an expression with only addition and substraction
/// \par parameters: an expression with only addition and subtraction
/// \return a map where each leaf of the input is mapped to the number of times
/// it is added. For instance, expression $x + x - y$ would give the map x ->
/// 2, y -> -1.
@ -1352,7 +1355,7 @@ exprt string_refinementt::sum_over_map(
}
/// \par parameters: an expression with only plus and minus expr
/// \return an equivalent expression in a cannonical form
/// \return an equivalent expression in a canonical form
exprt string_refinementt::simplify_sum(const exprt &f) const
{
std::map<exprt, int> map=map_representation_of_sum(f);
@ -1372,7 +1375,7 @@ exprt string_refinementt::compute_inverse_function(
exprt positive, negative;
// number of time the element should be added (can be negative)
// qvar has to be equal to val - f(0) if it appears positively in f
// (ie if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively
// (i.e. if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively
// in f. So we start by computing val - f(0).
std::map<exprt, int> elems=map_representation_of_sum(minus_exprt(val, f));
@ -1608,7 +1611,7 @@ exprt find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
/// \return substitute `qvar` the universally quantified variable of `axiom`, by
/// an index `val`, in `axiom`, so that the index used for `str` equals `val`.
/// For instance, if `axiom` corresponds to $\forall q. s[q+x]='a' &&
/// t[q]='b'$, `instantiate(axom,s,v)` would return an expression for
/// t[q]='b'$, `instantiate(axiom,s,v)` would return an expression for
/// $s[v]='a' && t[v-x]='b'$.
exprt string_refinementt::instantiate(
const string_constraintt &axiom, const exprt &str, const exprt &val)
@ -1687,7 +1690,7 @@ void string_refinementt::instantiate_not_contains(
/// replace array-lists by 'with' expressions
/// \par parameters: an expression containing array-list expressions
/// \return an epression containing no array-list
/// \return an expression containing no array-list
exprt string_refinementt::substitute_array_lists(exprt expr) const
{
for(size_t i=0; i<expr.operands().size(); ++i)
@ -1741,6 +1744,16 @@ exprt string_refinementt::get(const exprt &expr) const
if(it!=found_length.end())
return get_array(ecopy, it->second);
}
else if(refined_string_typet::is_refined_string_type(ecopy.type()) &&
ecopy.id()==ID_struct)
{
const string_exprt &string=to_string_expr(ecopy);
const exprt &content=string.content();
const exprt &length=string.length();
const exprt arr=get_array(content, length);
ecopy=string_exprt(length, arr, string.type());
}
ecopy=supert::get(ecopy);
@ -1748,7 +1761,7 @@ exprt string_refinementt::get(const exprt &expr) const
}
/// Creates a solver with `axiom` as the only formula added and runs it. If it
/// is SAT, then true is returned and the given evalutation of `var` is stored
/// is SAT, then true is returned and the given evaluation of `var` is stored
/// in `witness`. If UNSAT, then what witness is is undefined.
/// \param [in] axiom: the axiom to be checked
/// \param [in] var: the variable whose evaluation will be stored in witness
@ -1772,9 +1785,172 @@ bool string_refinementt::is_axiom_sat(
}
case decision_proceduret::resultt::D_UNSATISFIABLE:
return false;
case decision_proceduret::resultt::D_ERROR:
default:
INVARIANT(false, string_refinement_invariantt("failure in checking axiom"));
// To tell the compiler that the previous line bails
throw 0;
}
}
/// \related string_constraintt
typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
/// \related string_constraintt
class gather_indices_visitort: public const_expr_visitort
{
public:
array_index_mapt indices;
gather_indices_visitort(): indices() {}
void operator()(const exprt &expr) override
{
if(expr.id()==ID_index)
{
const index_exprt index=to_index_expr(expr);
const exprt s(index.array());
const exprt i(index.index());
indices[s].push_back(i);
}
}
};
/// \related string_constraintt
static array_index_mapt gather_indices(const exprt &expr)
{
gather_indices_visitort v;
expr.visit(v);
return v.indices;
}
/// \related string_constraintt
class is_linear_arithmetic_expr_visitort: public const_expr_visitort
{
public:
bool correct;
is_linear_arithmetic_expr_visitort(): correct(true) {}
void operator()(const exprt &expr) override
{
if(expr.id()!=ID_plus && expr.id()!=ID_minus && expr.id()!=ID_unary_minus)
{
// This represents that the expr is a valid leaf, may not be future proof
// or 100% enforced, but is correct prescriptively. All non-sum exprs must
// be leaves.
correct&=expr.operands().empty();
}
}
};
/// \related string_constraintt
static bool is_linear_arithmetic_expr(const exprt &expr)
{
is_linear_arithmetic_expr_visitort v;
expr.visit(v);
return v.correct;
}
/// The universally quantified variable is only allowed to occur in index
/// expressions in the body of a string constraint. This function returns true
/// if this is the case and false otherwise.
/// \related string_constraintt
/// \param [in] expr: The string constraint to check
/// \return true if the universal variable only occurs in index expressions,
/// false otherwise.
static bool universal_only_in_index(const string_constraintt &expr)
{
// For efficiency, we do a depth-first search of the
// body. The exprt visitors do a BFS and hide the stack/queue, so we would
// need to store a map from child to parent.
// The unsigned int represents index depth we are. For example, if we are
// considering the fragment `a[b[x]]` (not inside an index expression), then
// the stack would look something like `[..., (a, 0), (b, 1), (x, 2)]`.
typedef std::pair<exprt, unsigned> valuet;
std::stack<valuet> stack;
// We start at 0 since expr is not an index expression, so expr.body() is not
// in an index expression.
stack.push(valuet(expr.body(), 0));
while(!stack.empty())
{
// Inspect current value
const valuet cur=stack.top();
stack.pop();
const exprt e=cur.first;
const unsigned index_depth=cur.second;
const unsigned child_index_depth=index_depth+(e.id()==ID_index?0:1);
// If we found the universal variable not in an index_exprt, fail
if(e==expr.univ_var() && index_depth==0)
return false;
else
forall_operands(it, e)
stack.push(valuet(*it, child_index_depth));
}
return true;
}
/// Checks the data invariant for \link string_constraintt
/// \related string_constraintt
/// \param [in] expr: the string constraint to check
/// \return whether the constraint satisfies the invariant
bool string_refinementt::is_valid_string_constraint(
const string_constraintt &expr)
{
// Condition 1: The premise cannot contain any string indices
const array_index_mapt premise_indices=gather_indices(expr.premise());
if(!premise_indices.empty())
{
error() << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {";
for(const auto &pair : premise_indices)
{
error() << from_expr(ns, "", pair.first) << ": {";
for(const auto &i : pair.second)
error() << from_expr(ns, "", i) << ", ";
}
error() << "}}" << eom;
return false;
}
const array_index_mapt body_indices=gather_indices(expr.body());
// Must validate for each string. Note that we have an invariant that the
// second value in the pair is non-empty.
for(const auto &pair : body_indices)
{
// Condition 2: All indices of the same string must be the of the same form
const exprt rep=pair.second.back();
for(size_t j=0; j<pair.second.size()-1; j++)
{
const exprt i=pair.second[j];
const equal_exprt equals(rep, i);
const exprt result=simplify_expr(equals, ns);
if(result.is_false())
{
error() << "Indices not equal: " << from_expr(ns, "", expr) << ", str: "
<< from_expr(ns, "", pair.first) << eom;
return false;
}
}
// Condition 3: f must be linear
if(!is_linear_arithmetic_expr(rep))
{
error() << "f is not linear: " << from_expr(ns, "", expr) << ", str: "
<< from_expr(ns, "", pair.first) << eom;
return false;
}
// Condition 4: the quantified variable can only occur in indices in the
// body
if(!universal_only_in_index(expr))
{
error() << "Universal variable outside of index:"
<< from_expr(ns, "", expr) << eom;
return false;
}
}
return true;
}

7
src/solvers/refinement/string_refinement.h
View File

@ -118,11 +118,6 @@ private:
void set_to(const exprt &expr, bool value) override;
void add_instantiations();
exprt negation_of_not_contains_constraint(
const string_not_contains_constraintt &axiom,
const exprt &val,
const symbol_exprt &univ_var);
exprt negation_of_constraint(const string_constraintt &axiom);
void debug_model();
bool check_axioms();
bool is_axiom_sat(
@ -151,6 +146,8 @@ private:
exprt sum_over_map(
std::map<exprt, int> &m, const typet &type, bool negated=false) const;
bool is_valid_string_constraint(const string_constraintt &expr);
exprt simplify_sum(const exprt &f) const;
template <typename T1, typename T2>
void pad_vector(