Skip to content

smt2_parser: avoid access to vector without prior size check #2347

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
Jun 12, 2018
Merged

smt2_parser: avoid access to vector without prior size check #2347

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
80 changes: 30 additions & 50 deletions src/solvers/smt2/smt2_parser.cpp
View file
Open in desktop
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)
Copy link
Collaborator

Choose a reason for hiding this comment

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

API/function documentation would be nice to have.

{
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
Open in desktop
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