Skip to content

added support for rotation operators #1941

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 1 commit into from
Mar 21, 2018
Merged

added support for rotation operators #1941

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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: 5 additions & 1 deletion regression/smt2_solver/basic-bv1/basic-bv1.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,10 @@
(define-fun b09 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right
(define-fun b10 () Bool (= (bvashr #xf0 #x03) #xfe)) ; signed (arithmetical) shift right#x0a

; rotation
(define-fun b11 () Bool (= ((_ rotate_left 2) #xf7) #xdf)) ; rotation left
(define-fun b12 () Bool (= ((_ rotate_right 2) #x07) #xc1)) ; rotation right

; Bitwise Operations

(define-fun w1 () Bool (= (bvor #x6 #x3) #x7)) ; bitwise or
Expand Down Expand Up @@ -56,7 +60,7 @@
; all must be true

(assert (not (and
b01 b02 b03 b04 b05 b06 b07 b08 b09 b10
b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 b11 b12
d01
power-test
p1 p2 p3 p4 p5 p6 p7 p8)))
Expand Down
3 changes: 2 additions & 1 deletion src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -216,7 +216,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
return convert_div(to_div_expr(expr));
else if(expr.id()==ID_mod)
return convert_mod(to_mod_expr(expr));
else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
expr.id()==ID_rol || expr.id()==ID_ror)
return convert_shift(to_shift_expr(expr));
else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_overflow.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ literalt boolbvt::convert_overflow(const exprt &expr)

bvt bv_ext=bv_utils.extension(bv0, new_size, rep);

bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::LEFT, bv1);
bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1);

// a negative shift is undefined; yet this isn't an overflow
literalt neg_shift =
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_power.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ bvt boolbvt::convert_power(const binary_exprt &expr)
bv_utils.equal(op0, bv_utils.build_constant(2, op0.size()));

bvt one=bv_utils.build_constant(1, width);
bvt shift=bv_utils.shift(one, bv_utilst::shiftt::LEFT, op1);
bvt shift=bv_utils.shift(one, bv_utilst::shiftt::SHIFT_LEFT, op1);

bvt nondet=prop.new_variables(width);

Expand Down
13 changes: 7 additions & 6 deletions src/solvers/flattening/boolbv_shift.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,6 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
if(width==0)
return conversion_failed(expr);

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

Copy link
Collaborator

Choose a reason for hiding this comment

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

Is util/std_expr.h in sync with this?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, that's why the if(...) can go away.

Copy link
Collaborator

Choose a reason for hiding this comment

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

If it is something we assume then a DATA_INVARIANT would be best until we have the invariants in util/std_expr.h full enforced everywhere. This is what I (and others) have been doing.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Would still prefer a DATA_INVARIANT here until it is actually enforced by the code.

const bvt &op=convert_bv(expr.op0());

if(op.size()!=width)
Expand All @@ -41,11 +38,15 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
bv_utilst::shiftt shift;

if(expr.id()==ID_shl)
shift=bv_utilst::shiftt::LEFT;
shift=bv_utilst::shiftt::SHIFT_LEFT;
else if(expr.id()==ID_ashr)
shift=bv_utilst::shiftt::ARIGHT;
shift=bv_utilst::shiftt::SHIFT_ARIGHT;
else if(expr.id()==ID_lshr)
shift=bv_utilst::shiftt::LRIGHT;
shift=bv_utilst::shiftt::SHIFT_LRIGHT;
else if(expr.id()==ID_rol)
shift=bv_utilst::shiftt::ROTATE_LEFT;
else if(expr.id()==ID_ror)
shift=bv_utilst::shiftt::ROTATE_RIGHT;
else
throw "unexpected shift operator";

Expand Down
31 changes: 25 additions & 6 deletions src/solvers/flattening/bv_utils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -482,26 +482,45 @@ bvt bv_utilst::shift(const bvt &src, const shiftt s, std::size_t dist)
bvt result;
result.resize(src.size());

// 'dist' is user-controlled, and thus arbitary.
// We thus must guard against the case in which i+dist overflows.
// We do so by considering the case dist>=src.size().

for(std::size_t i=0; i<src.size(); i++)
{
literalt l;

switch(s)
{
case shiftt::LEFT:
case shiftt::SHIFT_LEFT:
// no underflow on i-dist because of condition dist<=i
l=(dist<=i?src[i-dist]:const_literal(false));
break;

case shiftt::ARIGHT:
l=(i+dist<src.size()?src[i+dist]:src[src.size()-1]); // sign bit
case shiftt::SHIFT_ARIGHT:
// src.size()-i won't underflow as i<src.size()
// Then, if dist<src.size()-i, then i+dist<src.size()
l=(dist<src.size()-i?src[i+dist]:src[src.size()-1]); // sign bit
break;

case shiftt::SHIFT_LRIGHT:
// src.size()-i won't underflow as i<src.size()
// Then, if dist<src.size()-i, then i+dist<src.size()
l=(dist<src.size()-i?src[i+dist]:const_literal(false));
break;

case shiftt::LRIGHT:
l=(i+dist<src.size()?src[i+dist]:const_literal(false));
case shiftt::ROTATE_LEFT:
// prevent overflows by using dist%src.size()
l=src[(src.size()+i-(dist%src.size()))%src.size()];
break;

case shiftt::ROTATE_RIGHT:
// prevent overflows by using dist%src.size()
l=src[(i+(dist%src.size()))%src.size()];
break;

default:
assert(false);
UNREACHABLE;
}

result[i]=l;
Expand Down
6 changes: 5 additions & 1 deletion src/solvers/flattening/bv_utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,11 @@ class bv_utilst
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep);
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in);

enum class shiftt { LEFT, LRIGHT, ARIGHT };
enum class shiftt
{
SHIFT_LEFT, SHIFT_LRIGHT, SHIFT_ARIGHT, ROTATE_LEFT, ROTATE_RIGHT
};

bvt shift(const bvt &op, const shiftt shift, std::size_t distance);
bvt shift(const bvt &op, const shiftt shift, const bvt &distance);

Expand Down
3 changes: 2 additions & 1 deletion src/solvers/floatbv/float_approximation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,8 @@ void float_approximationt::normalization_shift(bvt &fraction, bvt &exponent)
if(over_approximate)
shifted_fraction=overapproximating_left_shift(fraction, i);
else
shifted_fraction=bv_utils.shift(fraction, bv_utilst::shiftt::LEFT, i);
shifted_fraction=bv_utils.shift(
fraction, bv_utilst::shiftt::SHIFT_LEFT, i);

bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);

Expand Down
6 changes: 3 additions & 3 deletions src/solvers/floatbv/float_utils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ bvt float_utilst::to_integer(
unpacked.exponent.size());
bvt distance=bv_utils.sub(offset, unpacked.exponent);
bvt shift_result=bv_utils.shift(
fraction, bv_utilst::shiftt::LRIGHT, distance);
fraction, bv_utilst::shiftt::SHIFT_LRIGHT, distance);

// if the exponent is negative, we have zero anyways
bvt result=shift_result;
Expand Down Expand Up @@ -809,7 +809,7 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
// If so, shift the zeros out left by 'distance'.
// Otherwise, leave as is.
const bvt shifted=
bv_utils.shift(fraction, bv_utilst::shiftt::LEFT, distance);
bv_utils.shift(fraction, bv_utilst::shiftt::SHIFT_LEFT, distance);

fraction=
bv_utils.select(prefix_is_zero, shifted, fraction);
Expand Down Expand Up @@ -1281,7 +1281,7 @@ bvt float_utilst::sticky_right_shift(
{
if(dist[stage]!=const_literal(false))
{
bvt tmp=bv_utils.shift(result, bv_utilst::shiftt::LRIGHT, d);
bvt tmp=bv_utils.shift(result, bv_utilst::shiftt::SHIFT_LRIGHT, d);

bvt lost_bits;

Expand Down