Skip to content

Commit

Permalink
Drop inheritance from constraint on exprt
Browse files Browse the repository at this point in the history 
There is no strong reason for making string_constraintt inherit from
exprt. Getting rid of this inheritance makes usage of the class safer by
preventing the application of exprt method that do not make sense for
string constraints.
  • Loading branch information
@romainbrenguier
romainbrenguier committed May 22, 2018
1 parent dd30bbb commit 5ec351b
Show file tree
Hide file tree
Showing 4 changed files with 84 additions and 145 deletions.
6 changes: 2 additions & 4 deletions jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,10 +206,8 @@ SCENARIO("instantiate_not_contains",
constraints.end(),
axioms,
[&](const std::string &accu, string_constraintt sc) {
simplify(sc, ns);
std::string s;
java_lang->from_expr(sc, s, ns);
return accu + s + "\n\n";
simplify(sc.body, ns);
return accu + to_string(sc) + "\n\n";
});

const auto nc_contraints = generator.get_not_contains_constraints();
Expand Down
100 changes: 36 additions & 64 deletions src/solvers/refinement/string_constraint.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ Author: Romain Brenguier, [email protected]
#include <util/format_type.h>
#include <util/refined_string_type.h>
#include <util/string_expr.h>
#include <util/union_find_replace.h>

/// ### Universally quantified string constraint
///
Expand Down Expand Up @@ -54,89 +55,60 @@ Author: Romain Brenguier, [email protected]
/// \f$f\f$ [explicitly stated, implied].
///
/// \todo The fact that we follow this grammar is not enforced at the moment.
class string_constraintt : public exprt
class string_constraintt final
{
public:
// String constraints are of the form
// forall univ_var in [lower_bound,upper_bound[. premise => body
// forall univ_var in [lower_bound,upper_bound[. body
symbol_exprt univ_var;
exprt lower_bound;
exprt upper_bound;
exprt body;

const exprt &premise() const
{
return op0();
}

const exprt &body() const
{
return op1();
}
string_constraintt() = delete;

const symbol_exprt &univ_var() const
string_constraintt(
symbol_exprt _univ_var,
exprt lower_bound,
exprt upper_bound,
exprt body)
: univ_var(_univ_var),
lower_bound(lower_bound),
upper_bound(upper_bound),
body(body)
{
return to_symbol_expr(op2());
}

const exprt &upper_bound() const
{
return op3();
}

const exprt &lower_bound() const
// Default bound inferior is 0
string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)
: string_constraintt(
univ_var,
from_integer(0, univ_var.type()),
upper_bound,
body)
{
return operands()[4];
}

private:
string_constraintt();

public:
string_constraintt(
const symbol_exprt &_univ_var,
const exprt &bound_inf,
const exprt &bound_sup,
const exprt &body):
exprt(ID_string_constraint)
exprt univ_within_bounds() const
{
copy_to_operands(true_exprt(), body);
copy_to_operands(_univ_var, bound_sup, bound_inf);
return and_exprt(
binary_relation_exprt(lower_bound, ID_le, univ_var),
binary_relation_exprt(upper_bound, ID_gt, univ_var));
}

// Default bound inferior is 0
string_constraintt(
const symbol_exprt &_univ_var,
const exprt &bound_sup,
const exprt &body):
string_constraintt(
_univ_var,
from_integer(0, _univ_var.type()),
bound_sup,
body)
{}

exprt univ_within_bounds() const
void replace_expr(union_find_replacet &replace_map)
{
return and_exprt(
binary_relation_exprt(lower_bound(), ID_le, univ_var()),
binary_relation_exprt(upper_bound(), ID_gt, univ_var()));
replace_map.replace_expr(lower_bound);
replace_map.replace_expr(upper_bound);
replace_map.replace_expr(body);
}

exprt negation() const
{
return and_exprt(univ_within_bounds(), not_exprt(body()));
return and_exprt(univ_within_bounds(), not_exprt(body));
}
};

extern inline const string_constraintt &to_string_constraint(const exprt &expr)
{
PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
return static_cast<const string_constraintt &>(expr);
}

extern inline string_constraintt &to_string_constraint(exprt &expr)
{
PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
return static_cast<string_constraintt &>(expr);
}

/// Used for debug printing.
/// \param [in] ns: namespace for `from_expr`
/// \param [in] identifier: identifier for `from_expr`
Expand All @@ -145,9 +117,9 @@ extern inline string_constraintt &to_string_constraint(exprt &expr)
inline std::string to_string(const string_constraintt &expr)
{
std::ostringstream out;
out << "forall " << format(expr.univ_var()) << " in ["
<< format(expr.lower_bound()) << ", " << format(expr.upper_bound())
<< "). " << format(expr.premise()) << " => " << format(expr.body());
out << "forall " << format(expr.univ_var) << " in ["
<< format(expr.lower_bound) << ", " << format(expr.upper_bound) << "). "
<< format(expr.body);
return out.str();
}

Expand Down
122 changes: 46 additions & 76 deletions src/solvers/refinement/string_refinement.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ Author: Alberto Griggio, [email protected]
static bool is_valid_string_constraint(
messaget::mstreamt &stream,
const namespacet &ns,
const string_constraintt &expr);
const string_constraintt &constraint);

static optionalt<exprt> find_counter_example(
const namespacet &ns,
Expand Down Expand Up @@ -697,7 +697,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
constraints.end(),
std::back_inserter(axioms.universal),
[&](string_constraintt constraint) {
symbol_resolve.replace_expr(constraint);
constraint.replace_expr(symbol_resolve);
DATA_INVARIANT(
is_valid_string_constraint(error(), ns, constraint),
string_refinement_invariantt(
Expand Down Expand Up @@ -1238,34 +1238,23 @@ static exprt negation_of_not_contains_constraint(

/// Debugging function which outputs the different steps an axiom goes through
/// to be checked in check axioms.
/// \tparam T: can be either string_constraintt or
/// string_not_contains_constraintt
template <typename T>
static void debug_check_axioms_step(
messaget::mstreamt &stream,
const namespacet &ns,
const exprt &axiom,
const exprt &axiom_in_model,
const T &axiom,
const T &axiom_in_model,
const exprt &negaxiom,
const exprt &with_concretized_arrays)
{
static const std::string indent = " ";
static const std::string indent2 = " ";
stream << indent2 << "- axiom:\n" << indent2 << indent;

if(axiom.id() == ID_string_constraint)
stream << to_string(to_string_constraint(axiom));
else if(axiom.id() == ID_string_not_contains_constraint)
stream << to_string(to_string_not_contains_constraint(axiom));
else
stream << format(axiom);
stream << to_string(axiom);
stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent;

if(axiom_in_model.id() == ID_string_constraint)
stream << to_string(to_string_constraint(axiom_in_model));
else if(axiom_in_model.id() == ID_string_not_contains_constraint)
stream << to_string(to_string_not_contains_constraint(axiom_in_model));
else
stream << format(axiom_in_model);

stream << '\n'
stream << to_string(axiom_in_model) << '\n'
<< indent2 << "- negated_axiom:\n"
<< indent2 << indent << format(negaxiom) << '\n';
stream << indent2 << "- negated_axiom_with_concretized_arrays:\n"
Expand Down Expand Up @@ -1322,16 +1311,11 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
for(size_t i=0; i<axioms.universal.size(); i++)
{
const string_constraintt &axiom=axioms.universal[i];
const symbol_exprt &univ_var=axiom.univ_var();
const exprt &bound_inf=axiom.lower_bound();
const exprt &bound_sup=axiom.upper_bound();
const exprt &prem=axiom.premise();
INVARIANT(
prem == true_exprt(), "string constraint premises are not supported");
const exprt &body=axiom.body();

const string_constraintt axiom_in_model(
univ_var, get(bound_inf), get(bound_sup), get(body));
axiom.univ_var,
get(axiom.lower_bound),
get(axiom.upper_bound),
get(axiom.body));

exprt negaxiom = axiom_in_model.negation();
negaxiom = simplify_expr(negaxiom, ns);
Expand All @@ -1342,11 +1326,12 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
debug_check_axioms_step(
stream, ns, axiom, axiom_in_model, negaxiom, with_concretized_arrays);

if(const auto &witness=
find_counter_example(ns, ui, with_concretized_arrays, univ_var))
if(
const auto &witness =
find_counter_example(ns, ui, with_concretized_arrays, axiom.univ_var))
{
stream << indent2 << "- violated_for: " << univ_var.get_identifier()
<< "=" << format(*witness) << eom;
stream << indent2 << "- violated_for: " << format(axiom.univ_var) << "="
<< format(*witness) << eom;
violated[i]=*witness;
}
else
Expand Down Expand Up @@ -1402,13 +1387,13 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
const exprt &val=v.second;
const string_constraintt &axiom=axioms.universal[v.first];

implies_exprt instance(axiom.premise(), axiom.body());
replace_expr(axiom.univ_var(), val, instance);
exprt instance(axiom.body);
replace_expr(axiom.univ_var, val, instance);
// We are not sure the index set contains only positive numbers
and_exprt bounds(
axiom.univ_within_bounds(),
binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
replace_expr(axiom.univ_var(), val, bounds);
replace_expr(axiom.univ_var, val, bounds);
const implies_exprt counter(bounds, instance);
lemmas.push_back(counter);
}
Expand Down Expand Up @@ -1766,10 +1751,10 @@ static void initial_index_set(
const namespacet &ns,
const string_constraintt &axiom)
{
const symbol_exprt &qvar=axiom.univ_var();
const auto &bound = axiom.upper_bound();
auto it = axiom.body().depth_begin();
const auto end = axiom.body().depth_end();
const symbol_exprt &qvar = axiom.univ_var;
const auto &bound = axiom.upper_bound;
auto it = axiom.body.depth_begin();
const auto end = axiom.body.depth_end();
while(it != end)
{
if(it->id() == ID_index && is_char_type(it->type()))
Expand Down Expand Up @@ -1912,18 +1897,17 @@ static exprt instantiate(
const exprt &str,
const exprt &val)
{
const optionalt<exprt> idx = find_index(axiom.body(), str, axiom.univ_var());
const optionalt<exprt> idx = find_index(axiom.body, str, axiom.univ_var);
if(!idx.has_value())
return true_exprt();

const exprt r = compute_inverse_function(stream, axiom.univ_var(), val, *idx);
const exprt r = compute_inverse_function(stream, axiom.univ_var, val, *idx);
implies_exprt instance(
and_exprt(
binary_relation_exprt(axiom.univ_var(), ID_ge, axiom.lower_bound()),
binary_relation_exprt(axiom.univ_var(), ID_lt, axiom.upper_bound()),
axiom.premise()),
axiom.body());
replace_expr(axiom.univ_var(), r, instance);
binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)),
axiom.body);
replace_expr(axiom.univ_var, r, instance);
return instance;
}

Expand Down Expand Up @@ -2175,11 +2159,11 @@ is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
/// \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)
static bool universal_only_in_index(const string_constraintt &constr)
{
for(auto it = expr.body().depth_begin(); it != expr.body().depth_end();)
for(auto it = constr.body.depth_begin(); it != constr.body.depth_end();)
{
if(*it == expr.univ_var())
if(*it == constr.univ_var)
return false;
if(it->id() == ID_index)
it.next_sibling_or_parent();
Expand All @@ -2193,35 +2177,20 @@ static bool universal_only_in_index(const string_constraintt &expr)
/// \related string_constraintt
/// \param stream: message stream
/// \param ns: namespace
/// \param [in] expr: the string constraint to check
/// \param [in] constraint: the string constraint to check
/// \return whether the constraint satisfies the invariant
static bool is_valid_string_constraint(
messaget::mstreamt &stream,
const namespacet &ns,
const string_constraintt &expr)
const string_constraintt &constraint)
{
const auto eom=messaget::eom;
// Condition 1: The premise cannot contain any string indices
const array_index_mapt premise_indices=gather_indices(expr.premise());
if(!premise_indices.empty())
{
stream << "Premise has indices: " << format(expr) << ", map: {";
for(const auto &pair : premise_indices)
{
stream << format(pair.first) << ": {";
for(const auto &i : pair.second)
stream << format(i) << ", ";
}
stream << "}}" << eom;
return false;
}

const array_index_mapt body_indices=gather_indices(expr.body());
const array_index_mapt body_indices = gather_indices(constraint.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
// Condition 1: 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++)
{
Expand All @@ -2230,25 +2199,26 @@ static bool is_valid_string_constraint(
const exprt result=simplify_expr(equals, ns);
if(result.is_false())
{
stream << "Indices not equal: " << format(expr)
stream << "Indices not equal: " << to_string(constraint)
<< ", str: " << format(pair.first) << eom;
return false;
}
}

// Condition 3: f must be linear in the quantified variable
if(!is_linear_arithmetic_expr(rep, expr.univ_var()))
// Condition 2: f must be linear in the quantified variable
if(!is_linear_arithmetic_expr(rep, constraint.univ_var))
{
stream << "f is not linear: " << format(expr)
stream << "f is not linear: " << to_string(constraint)
<< ", str: " << format(pair.first) << eom;
return false;
}

// Condition 4: the quantified variable can only occur in indices in the
// Condition 3: the quantified variable can only occur in indices in the
// body
if(!universal_only_in_index(expr))
if(!universal_only_in_index(constraint))
{
stream << "Universal variable outside of index:" << format(expr) << eom;
stream << "Universal variable outside of index:" << to_string(constraint)
<< eom;
return false;
}
}
Expand Down
Loading

0 comments on commit 5ec351b

Please sign in to comment.