Skip to content

Commit

Permalink
Merge pull request diffblue#2347 from diffblue/smt2-bounds-checks
Browse files Browse the repository at this point in the history 
smt2_parser: avoid access to vector without prior size check
  • Loading branch information
Daniel Kroening authored Jun 12, 2018
2 parents dfff111 + bffb1ca commit 43d008a
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 55 deletions.
80 changes: 30 additions & 50 deletions src/solvers/smt2/smt2_parser.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -313,24 +313,26 @@ exprt smt2_parsert::function_application(
return nil_exprt();
}

exprt smt2_parsert::cast_bv_to_signed(const exprt &expr)
exprt::operandst smt2_parsert::cast_bv_to_signed(const exprt::operandst &op)
{
if(expr.type().id()==ID_signedbv) // no need to cast
return expr;
exprt::operandst result = op;

if(expr.type().id()!=ID_unsignedbv)
for(auto &expr : result)
{
error() << "expected unsigned bitvector" << eom;
return expr;
if(expr.type().id() == ID_signedbv) // no need to cast
{
}
else if(expr.type().id() != ID_unsignedbv)
{
error() << "expected unsigned bitvector" << eom;
}
else
{
const auto width = to_unsignedbv_type(expr.type()).get_width();
expr = typecast_exprt(expr, signedbv_typet(width));
}
}

auto width=to_unsignedbv_type(expr.type()).get_width();
signedbv_typet signed_type(width);

typecast_exprt result(expr, signed_type);
result.op0()=expr;
result.type()=signed_type;

return result;
}

Expand All @@ -345,17 +347,11 @@ exprt smt2_parsert::cast_bv_to_unsigned(const exprt &expr)
return expr;
}

auto width=to_signedbv_type(expr.type()).get_width();
unsignedbv_typet unsigned_type(width);

typecast_exprt result(expr, unsigned_type);
result.op0()=expr;
result.type()=unsigned_type;

return result;
const auto width=to_signedbv_type(expr.type()).get_width();
return typecast_exprt(expr, unsignedbv_typet(width));
}

exprt smt2_parsert::multi_ary(irep_idt id, exprt::operandst &op)
exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op)
{
if(op.empty())
{
Expand All @@ -377,12 +373,12 @@ exprt smt2_parsert::multi_ary(irep_idt id, exprt::operandst &op)
}

exprt result(id, op[0].type());
result.operands().swap(op);
result.operands() = op;
return result;
}
}

exprt smt2_parsert::binary_predicate(irep_idt id, exprt::operandst &op)
exprt smt2_parsert::binary_predicate(irep_idt id, const exprt::operandst &op)
{
if(op.size()!=2)
{
Expand All @@ -404,7 +400,7 @@ exprt smt2_parsert::binary_predicate(irep_idt id, exprt::operandst &op)
}
}

exprt smt2_parsert::unary(irep_idt id, exprt::operandst &op)
exprt smt2_parsert::unary(irep_idt id, const exprt::operandst &op)
{
if(op.size()!=1)
{
Expand All @@ -415,7 +411,7 @@ exprt smt2_parsert::unary(irep_idt id, exprt::operandst &op)
return unary_exprt(id, op[0], op[0].type());
}

exprt smt2_parsert::binary(irep_idt id, exprt::operandst &op)
exprt smt2_parsert::binary(irep_idt id, const exprt::operandst &op)
{
if(op.size()!=2)
{
Expand Down Expand Up @@ -510,45 +506,35 @@ exprt smt2_parsert::function_application()
}
else if(id=="bvsle")
{
op[0]=cast_bv_to_signed(op[0]);
op[1]=cast_bv_to_signed(op[1]);
return binary_predicate(ID_le, op);
return binary_predicate(ID_le, cast_bv_to_signed(op));
}
else if(id=="bvuge")
{
return binary_predicate(ID_ge, op);
}
else if(id=="bvsge")
{
op[0]=cast_bv_to_signed(op[0]);
op[1]=cast_bv_to_signed(op[1]);
return binary_predicate(ID_ge, op);
return binary_predicate(ID_ge, cast_bv_to_signed(op));
}
else if(id=="bvult")
{
return binary_predicate(ID_lt, op);
}
else if(id=="bvslt")
{
op[0]=cast_bv_to_signed(op[0]);
op[1]=cast_bv_to_signed(op[1]);
return binary_predicate(ID_lt, op);
return binary_predicate(ID_lt, cast_bv_to_signed(op));
}
else if(id=="bvugt")
{
return binary_predicate(ID_gt, op);
}
else if(id=="bvsgt")
{
op[0]=cast_bv_to_signed(op[0]);
op[1]=cast_bv_to_signed(op[1]);
return binary_predicate(ID_gt, op);
return binary_predicate(ID_gt, cast_bv_to_signed(op));
}
else if(id=="bvashr")
{
op[0]=cast_bv_to_signed(op[0]);
op[1]=cast_bv_to_signed(op[1]);
return cast_bv_to_unsigned(binary(ID_ashr, op));
return cast_bv_to_unsigned(binary(ID_ashr, cast_bv_to_signed(op)));
}
else if(id=="bvlshr" || id=="bvshr")
{
Expand Down Expand Up @@ -608,9 +594,7 @@ exprt smt2_parsert::function_application()
}
else if(id=="bvsdiv")
{
op[0]=cast_bv_to_signed(op[0]);
op[1]=cast_bv_to_signed(op[1]);
return cast_bv_to_unsigned(binary(ID_div, op));
return cast_bv_to_unsigned(binary(ID_div, cast_bv_to_signed(op)));
}
else if(id=="bvudiv")
{
Expand All @@ -624,17 +608,13 @@ exprt smt2_parsert::function_application()
{
// 2's complement signed remainder (sign follows dividend)
// This matches our ID_mod, and what C does since C99.
op[0]=cast_bv_to_signed(op[0]);
op[1]=cast_bv_to_signed(op[1]);
return cast_bv_to_unsigned(binary(ID_mod, op));
return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op)));
}
else if(id=="bvsmod")
{
// 2's complement signed remainder (sign follows divisor)
// We don't have that.
op[0]=cast_bv_to_signed(op[0]);
op[1]=cast_bv_to_signed(op[1]);
return cast_bv_to_unsigned(binary(ID_mod, op));
return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op)));
}
else if(id=="bvurem" || id=="%")
{
Expand Down
14 changes: 9 additions & 5 deletions src/solvers/smt2/smt2_parser.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,17 +64,21 @@ class smt2_parsert:public smt2_tokenizert
exprt::operandst operands();
typet function_signature_declaration();
typet function_signature_definition();
exprt multi_ary(irep_idt, exprt::operandst &);
exprt binary_predicate(irep_idt, exprt::operandst &);
exprt binary(irep_idt, exprt::operandst &);
exprt unary(irep_idt, exprt::operandst &);
exprt multi_ary(irep_idt, const exprt::operandst &);
exprt binary_predicate(irep_idt, const exprt::operandst &);
exprt binary(irep_idt, const exprt::operandst &);
exprt unary(irep_idt, const exprt::operandst &);

exprt let_expression();
exprt quantifier_expression(irep_idt);
exprt function_application(
const irep_idt &identifier,
const exprt::operandst &op);
exprt cast_bv_to_signed(const exprt &);

/// Apply typecast to signedbv to expressions in vector
exprt::operandst cast_bv_to_signed(const exprt::operandst &);

/// Apply typecast to unsignedbv to given expression
exprt cast_bv_to_unsigned(const exprt &);
};

Expand Down

0 comments on commit 43d008a

Please sign in to comment.