Skip to content

Partial solver cleanup (straightforward changes part 2) #1956

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 6 commits into from
Jun 5, 2018
Merged

Partial solver cleanup (straightforward changes part 2) #1956

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
2dc7bee
Replacing throws by invariants in boolbv convert
romainbrenguier Feb 7, 2018
52d0fe4
Make build_offset_map return an offset_mapt
romainbrenguier Feb 7, 2018
b837b8a
Remove useless throws in boolbvt::convert_index
romainbrenguier Feb 7, 2018
adc2d5d
Make convert_abs take an abs_exprt parameter
romainbrenguier Feb 8, 2018
1b43ee9
Refactoring in boolbvt::convert_bitwise
romainbrenguier Feb 8, 2018
d35c2ac
Refactoring in boolbvt::convert_byte_extract
romainbrenguier Feb 8, 2018
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
100 changes: 30 additions & 70 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
return convert_bitvector(expr.op0());
}
else if(expr.id()==ID_abs)
return convert_abs(expr);
return convert_abs(to_abs_expr(expr));
else if(expr.id() == ID_bswap)
return convert_bswap(to_bswap_expr(expr));
else if(expr.id()==ID_byte_extract_little_endian ||
Expand Down Expand Up @@ -433,13 +433,7 @@ bvt boolbvt::convert_function_application(

literalt boolbvt::convert_rest(const exprt &expr)
{
if(expr.type().id()!=ID_bool)
{
error() << "boolbvt::convert_rest got non-boolean operand: "
<< expr.pretty() << eom;
throw 0;
}

PRECONDITION(expr.type().id() == ID_bool);
const exprt::operandst &operands=expr.operands();

if(expr.id()==ID_typecast)
Expand All @@ -451,9 +445,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
return convert_verilog_case_equality(to_binary_relation_expr(expr));
else if(expr.id()==ID_notequal)
{
if(expr.operands().size()!=2)
throw "notequal expects two operands";

DATA_INVARIANT(expr.operands().size() == 2, "notequal expects two operands");
return !convert_equality(equal_exprt(expr.op0(), expr.op1()));
}
else if(expr.id()==ID_ieee_float_equal ||
Expand All @@ -480,57 +472,37 @@ literalt boolbvt::convert_rest(const exprt &expr)
else if(expr.id()==ID_index)
{
bvt bv=convert_index(to_index_expr(expr));

if(bv.size()!=1)
throw "convert_index returned non-bool bitvector";

CHECK_RETURN(bv.size() == 1);
return bv[0];
}
else if(expr.id()==ID_member)
{
bvt bv=convert_member(to_member_expr(expr));

if(bv.size()!=1)
throw "convert_member returned non-bool bitvector";

CHECK_RETURN(bv.size() == 1);
return bv[0];
}
else if(expr.id()==ID_case)
{
bvt bv=convert_case(expr);

if(bv.size()!=1)
throw "convert_case returned non-bool bitvector";

CHECK_RETURN(bv.size() == 1);
return bv[0];
}
else if(expr.id()==ID_cond)
{
bvt bv=convert_cond(expr);

if(bv.size()!=1)
throw "convert_cond returned non-bool bitvector";

CHECK_RETURN(bv.size() == 1);
return bv[0];
}
else if(expr.id()==ID_sign)
{
if(expr.operands().size()!=1)
throw "sign expects one operand";

DATA_INVARIANT(expr.operands().size() == 1, "sign expects one operand");
const bvt &bv=convert_bv(operands[0]);

if(bv.empty())
throw "sign operator takes one non-empty operand";

if(operands[0].type().id()==ID_signedbv)
CHECK_RETURN(!bv.empty());
const irep_idt type_id = operands[0].type().id();
if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
return bv[bv.size()-1];
else if(operands[0].type().id()==ID_unsignedbv)
if(type_id == ID_unsignedbv)
return const_literal(false);
else if(operands[0].type().id()==ID_fixedbv)
return bv[bv.size()-1];
else if(operands[0].type().id()==ID_floatbv)
return bv[bv.size()-1];
}
else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
Expand All @@ -542,64 +514,53 @@ literalt boolbvt::convert_rest(const exprt &expr)
return convert_overflow(expr);
else if(expr.id()==ID_isnan)
{
if(expr.operands().size()!=1)
throw "isnan expects one operand";

DATA_INVARIANT(expr.operands().size() == 1, "isnan expects one operand");
const bvt &bv=convert_bv(operands[0]);

if(expr.op0().type().id()==ID_floatbv)
{
float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
return float_utils.is_NaN(bv);
}
else if(expr.op0().type().id()==ID_fixedbv)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why remove the else here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I reverted these changes

else if(expr.op0().type().id() == ID_fixedbv)
return const_literal(false);
}
else if(expr.id()==ID_isfinite)
{
if(expr.operands().size()!=1)
throw "isfinite expects one operand";

DATA_INVARIANT(expr.operands().size() == 1, "isfinite expects one operand");
const bvt &bv=convert_bv(operands[0]);

if(expr.op0().type().id()==ID_floatbv)
{
float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
return prop.land(
!float_utils.is_infinity(bv),
!float_utils.is_NaN(bv));
}
else if(expr.op0().type().id()==ID_fixedbv)
else if(expr.op0().type().id() == ID_fixedbv)
return const_literal(true);
}
else if(expr.id()==ID_isinf)
{
if(expr.operands().size()!=1)
throw "isinf expects one operand";

DATA_INVARIANT(expr.operands().size() == 1, "isinf expects one operand");
const bvt &bv=convert_bv(operands[0]);

if(expr.op0().type().id()==ID_floatbv)
{
float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
return float_utils.is_infinity(bv);
}
else if(expr.op0().type().id()==ID_fixedbv)
else if(expr.op0().type().id() == ID_fixedbv)
return const_literal(false);
}
else if(expr.id()==ID_isnormal)
{
if(expr.operands().size()!=1)
throw "isnormal expects one operand";

const bvt &bv=convert_bv(operands[0]);

DATA_INVARIANT(expr.operands().size() == 1, "isnormal expects one operand");
if(expr.op0().type().id()==ID_floatbv)
{
const bvt &bv = convert_bv(operands[0]);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes; good catch!

float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
return float_utils.is_normal(bv);
}
else if(expr.op0().type().id()==ID_fixedbv)
else if(expr.op0().type().id() == ID_fixedbv)
return const_literal(true);
}

Expand Down Expand Up @@ -699,17 +660,16 @@ void boolbvt::print_assignment(std::ostream &out) const
out << pair.first << "=" << pair.second.get_value(prop) << '\n';
}

void boolbvt::build_offset_map(const struct_typet &src, offset_mapt &dest)
boolbvt::offset_mapt boolbvt::build_offset_map(const struct_typet &src)
{
const struct_typet::componentst &components=
src.components();

dest.resize(components.size());
std::size_t offset=0;
for(std::size_t i=0; i<components.size(); i++)
const struct_typet::componentst &components = src.components();
offset_mapt dest;
dest.reserve(components.size());
std::size_t offset = 0;
for(const auto &comp : components)
{
std::size_t comp_width=boolbv_width(components[i].type());
dest[i]=offset;
offset+=comp_width;
dest.push_back(offset);
offset += boolbv_width(comp.type());
}
return dest;
}
4 changes: 2 additions & 2 deletions src/solvers/flattening/boolbv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ class boolbvt:public arrayst
virtual bvt convert_shift(const binary_exprt &expr);
virtual bvt convert_bitwise(const exprt &expr);
virtual bvt convert_unary_minus(const unary_exprt &expr);
virtual bvt convert_abs(const exprt &expr);
virtual bvt convert_abs(const abs_exprt &expr);
virtual bvt convert_concatenation(const exprt &expr);
virtual bvt convert_replication(const replication_exprt &expr);
virtual bvt convert_bv_literals(const exprt &expr);
Expand Down Expand Up @@ -250,7 +250,7 @@ class boolbvt:public arrayst
void post_process_quantifiers();

typedef std::vector<std::size_t> offset_mapt;
void build_offset_map(const struct_typet &src, offset_mapt &dest);
offset_mapt build_offset_map(const struct_typet &src);

// strings
numbering<irep_idt> string_numbering;
Expand Down
17 changes: 5 additions & 12 deletions src/solvers/flattening/boolbv_abs.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,26 +14,19 @@ Author: Daniel Kroening, [email protected]

#include <solvers/floatbv/float_utils.h>

bvt boolbvt::convert_abs(const exprt &expr)
bvt boolbvt::convert_abs(const abs_exprt &expr)
{
std::size_t width=boolbv_width(expr.type());
const std::size_t width = boolbv_width(expr.type());

if(width==0)
return conversion_failed(expr);

const exprt::operandst &operands=expr.operands();
const bvt &op_bv=convert_bv(expr.op());

if(operands.size()!=1)
throw "abs takes one operand";

const exprt &op0=expr.op0();

const bvt &op_bv=convert_bv(op0);

if(op0.type()!=expr.type())
if(expr.op().type()!=expr.type())
return conversion_failed(expr);

bvtypet bvtype=get_bvtype(expr.type());
const bvtypet bvtype = get_bvtype(expr.type());

if(bvtype==bvtypet::IS_FIXED ||
bvtype==bvtypet::IS_SIGNED ||
Expand Down
21 changes: 6 additions & 15 deletions src/solvers/flattening/boolbv_bitwise.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,23 +11,16 @@ Author: Daniel Kroening, [email protected]

bvt boolbvt::convert_bitwise(const exprt &expr)
{
std::size_t width=boolbv_width(expr.type());

const std::size_t width = boolbv_width(expr.type());
if(width==0)
return conversion_failed(expr);

if(expr.id()==ID_bitnot)
{
if(expr.operands().size()!=1)
throw "bitnot takes one operand";

DATA_INVARIANT(expr.operands().size() == 1, "bitnot takes one operand");
const exprt &op0=expr.op0();

const bvt &op_bv=convert_bv(op0);

if(op_bv.size()!=width)
throw "convert_bitwise: unexpected operand width";

CHECK_RETURN(op_bv.size() == width);
return bv_utils.inverted(op_bv);
}
else if(expr.id()==ID_bitand || expr.id()==ID_bitor ||
Expand All @@ -41,9 +34,7 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
forall_operands(it, expr)
{
const bvt &op=convert_bv(*it);

if(op.size()!=width)
throw "convert_bitwise: unexpected operand width";
CHECK_RETURN(op.size() == width);

if(it==expr.operands().begin())
bv=op;
Expand All @@ -64,13 +55,13 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
else if(expr.id()==ID_bitxnor)
bv[i]=prop.lequal(bv[i], op[i]);
else
throw "unexpected operand";
UNIMPLEMENTED;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes; good use of a legacy invariant macro!

}
}
}

return bv;
}

throw "unexpected bitwise operand";
UNIMPLEMENTED;
}
35 changes: 9 additions & 26 deletions src/solvers/flattening/boolbv_byte_extract.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,33 +23,28 @@ Author: Daniel Kroening, [email protected]

bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
{
assert(map.number_of_bits()==src.size());

PRECONDITION(map.number_of_bits() == src.size());
bvt result;
result.resize(src.size(), const_literal(false));
result.reserve(src.size());

for(std::size_t i=0; i<src.size(); i++)
{
size_t mapped_index=map.map_bit(i);
assert(mapped_index<src.size());
result[i]=src[mapped_index];
const size_t mapped_index = map.map_bit(i);
CHECK_RETURN(mapped_index < src.size());
result.push_back(src[mapped_index]);
}

return result;
}

bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
{
if(expr.operands().size()!=2)
throw "byte_extract takes two operands";

// if we extract from an unbounded array, call the flattening code
if(is_unbounded_array(expr.op().type()))
{
try
{
exprt tmp = flatten_byte_extract(expr, ns);
return convert_bv(tmp);
return convert_bv(flatten_byte_extract(expr, ns));
}
catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception)
{
Expand All @@ -58,7 +53,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
}
}

std::size_t width=boolbv_width(expr.type());
const std::size_t width = boolbv_width(expr.type());

// special treatment for bit-fields and big-endian:
// we need byte granularity
Expand Down Expand Up @@ -105,22 +100,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)

const exprt &op=expr.op();
const exprt &offset=expr.offset();

bool little_endian;

if(expr.id()==ID_byte_extract_little_endian)
little_endian=true;
else if(expr.id()==ID_byte_extract_big_endian)
little_endian=false;
else
{
little_endian=false;
assert(false);
}
const bool little_endian = expr.id() == ID_byte_extract_little_endian;

// first do op0

bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
const bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
const bvt op_bv=map_bv(op_map, convert_bv(op));

// do result
Expand Down
6 changes: 0 additions & 6 deletions src/solvers/flattening/boolbv_index.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,6 @@ Author: Daniel Kroening, [email protected]

bvt boolbvt::convert_index(const index_exprt &expr)
{
if(expr.id()!=ID_index)
throw "expected index expression";

if(expr.operands().size()!=2)
throw "index takes two operands";

const exprt &array=expr.array();
const exprt &index=expr.index();

Expand Down
Loading