Skip to content

Various improvements in string refinement #806

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 12, 2017
Merged

Various improvements in string refinement #806

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f0004a5
Corrections on generated axioms
romainbrenguier Apr 6, 2017
94e9c64
Various improvements in string refinement
romainbrenguier Apr 7, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions src/solvers/refinement/string_constraint_generator_main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -177,6 +177,7 @@ string_exprt string_constraint_generatort::fresh_string(
symbol_exprt content=fresh_symbol("string_content", type.get_content_type());
string_exprt str(length, content, type);
created_strings.insert(str);
add_default_axioms(str);
return str;
}

Expand Down Expand Up @@ -246,7 +247,7 @@ string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(

/*******************************************************************\

Function: string_constraint_generatort::add_default_constraints
Function: string_constraint_generatort::add_default_axioms

Inputs:
s - a string expression
Expand All @@ -267,7 +268,8 @@ Function: string_constraint_generatort::add_default_constraints
void string_constraint_generatort::add_default_axioms(
const string_exprt &s)
{
s.axiom_for_is_longer_than(from_integer(0, s.length().type()));
axioms.push_back(
s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
if(max_string_length!=std::numeric_limits<size_t>::max())
axioms.push_back(s.axiom_for_is_shorter_than(max_string_length));

Expand Down
62 changes: 44 additions & 18 deletions src/solvers/refinement/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,12 @@ Author: Alberto Griggio, [email protected]

Constructor: string_refinementt

Inputs: a namespace, a decision procedure, a bound on the number
of refinements and a boolean flag `concretize_result`
Inputs:
_ns - a namespace
_prop - a decision procedure
refinement_bound - a bound on the number of refinements

Purpose: refinement_bound is a bound on the number of refinement allowed.
if `concretize_result` is set to true, at the end of the decision
procedure, the solver try to find a concrete value for each
character

\*******************************************************************/

Expand Down Expand Up @@ -167,15 +166,17 @@ void string_refinementt::add_instantiations()

Function: string_refinementt::add_symbol_to_symbol_map()

Inputs: a symbol and the expression to map it to
Inputs:
lhs - a symbol expression
rhs - an expression to map it to

Purpose: keeps a map of symbols to expressions, such as none of the
mapped values exist as a key

\*******************************************************************/

void string_refinementt::add_symbol_to_symbol_map
(const exprt &lhs, const exprt &rhs)
void string_refinementt::add_symbol_to_symbol_map(
const exprt &lhs, const exprt &rhs)
{
assert(lhs.id()==ID_symbol);

Expand Down Expand Up @@ -259,6 +260,21 @@ exprt string_refinementt::substitute_function_applications(exprt expr)
return expr;
}

/*******************************************************************\

Function: string_refinementt::is_char_array

Inputs:
type - a type

Outputs: true if the given type is an array of java characters

Purpose: distinguish char array from other types

TODO: this is only for java char array and does not work for other languages

\*******************************************************************/

bool string_refinementt::is_char_array(const typet &type) const
{
if(type.id()==ID_symbol)
Expand All @@ -269,18 +285,20 @@ bool string_refinementt::is_char_array(const typet &type) const

/*******************************************************************\

Function: string_refinementt::boolbv_set_equality_to_true
Function: string_refinementt::add_axioms_for_string_assigns

Inputs: the lhs and rhs of an equality expression
Inputs:
lhs - left hand side of an equality expression
rhs - right and side of the equality

Outputs: false if the lemmas were added successfully, true otherwise

Purpose: add lemmas to the solver corresponding to the given equation

\*******************************************************************/

bool string_refinementt::add_axioms_for_string_assigns(const exprt &lhs,
const exprt &rhs)
bool string_refinementt::add_axioms_for_string_assigns(
const exprt &lhs, const exprt &rhs)
{
if(is_char_array(rhs.type()))
{
Expand Down Expand Up @@ -332,7 +350,6 @@ void string_refinementt::concretize_string(const exprt &expr)
{
string_exprt str=to_string_expr(expr);
exprt length=get(str.length());
add_lemma(equal_exprt(str.length(), length));
exprt content=str.content();
replace_expr(symbol_resolve, content);
found_length[content]=length;
Expand All @@ -350,6 +367,7 @@ void string_refinementt::concretize_string(const exprt &expr)
else
{
size_t concretize_limit=found_length.to_long();
assert(concretize_limit<=generator.max_string_length);
concretize_limit=concretize_limit>generator.max_string_length?
generator.max_string_length:concretize_limit;
exprt content_expr=str.content();
Expand Down Expand Up @@ -443,6 +461,8 @@ void string_refinementt::set_to(const exprt &expr, bool value)
{
debug() << "(sr::set_to) WARNING: ignoring "
<< from_expr(expr) << " [inconsistent types]" << eom;
debug() << "lhs has type: " << eq_expr.lhs().type().pretty(12) << eom;
debug() << "rhs has type: " << eq_expr.rhs().type().pretty(12) << eom;
return;
}

Expand Down Expand Up @@ -596,7 +616,11 @@ decision_proceduret::resultt string_refinementt::dec_solve()
do_concretizing=false;
}
else
{
debug() << "check_SAT: the model is correct and "
<< "does not need concretizing" << eom;
return D_SATISFIABLE;
}
}

display_index_set();
Expand All @@ -611,6 +635,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
}
break;
default:
debug() << "check_SAT: default return " << res << eom;
return res;
}
}
Expand Down Expand Up @@ -1032,16 +1057,17 @@ void string_refinementt::substitute_array_access(exprt &expr) const
}

auto op_it=++array_expr.operands().rbegin();

for(size_t i=last_index-1;
op_it!=array_expr.operands().rend(); ++op_it, --i)
{
equal_exprt equals(index_expr.index(), from_integer(i, java_int_type()));
ite=if_exprt(equals, *op_it, ite);
if(ite.type()!=char_type)
if(op_it->type()!=char_type)
{
assert(ite.id()==ID_unknown);
ite.type()=char_type;
assert(op_it->id()==ID_unknown);
op_it->type()=char_type;
}
ite=if_exprt(equals, *op_it, ite);
}
expr=ite;
}
Expand Down Expand Up @@ -1747,7 +1773,7 @@ exprt string_refinementt::substitute_array_lists(exprt expr) const
expr.operands()[0],
expr.operands()[1]);

for(size_t i=2; i<expr.operands().size()/2; i++)
for(size_t i=1; i<expr.operands().size()/2; i++)
{
ret_expr=with_exprt(ret_expr,
expr.operands()[i*2],
Expand Down