Skip to content

util/simplify_expr: guard string simplifiers against non-string arguments #9133

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

Open
tautschnig wants to merge 1 commit into
base: develop
Choose a base branch
from
+48 −0
Open

util/simplify_expr: guard string simplifiers against non-string arguments #9133

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
48 changes: 48 additions & 0 deletions src/util/simplify_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,15 @@ static simplify_exprt::resultt<> simplify_string_endswith(
const function_application_exprt &expr,
const namespacet &ns)
{
// Bail out cleanly if either argument is not a refined_string_exprt;
// upstream code (e.g. the Python frontend) may sometimes hand us a
// single-character expression that hasn't been wrapped as a string.
if(
expr.arguments().size() < 2 ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(0)) ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(1)))
return simplify_exprt::unchanged(expr);
Comment on lines +233 to +240

const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);

Expand Down Expand Up @@ -261,6 +270,12 @@ static simplify_exprt::resultt<> simplify_string_contains(
// We want to get both arguments of any starts-with comparison, and
// trace them back to the actual string instance. All variables on the
// way must be constant for us to be sure this will work.
if(
expr.arguments().size() < 2 ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(0)) ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(1)))
return simplify_exprt::unchanged(expr);
Comment on lines +273 to +277

auto &first_argument = to_string_expr(expr.arguments().at(0));
auto &second_argument = to_string_expr(expr.arguments().at(1));

Expand Down Expand Up @@ -305,6 +320,11 @@ static simplify_exprt::resultt<> simplify_string_is_empty(
{
const function_application_exprt &function_app =
to_function_application_expr(expr);
if(
function_app.arguments().empty() ||
!can_cast_expr<refined_string_exprt>(function_app.arguments().at(0)))
return simplify_exprt::unchanged(expr);

const refined_string_exprt &s =
to_string_expr(function_app.arguments().at(0));

Expand All @@ -328,6 +348,12 @@ static simplify_exprt::resultt<> simplify_string_compare_to(
const function_application_exprt &expr,
const namespacet &ns)
{
if(
expr.arguments().size() < 2 ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(0)) ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(1)))
return simplify_exprt::unchanged(expr);

const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);

Expand Down Expand Up @@ -400,6 +426,11 @@ static simplify_exprt::resultt<> simplify_string_index_of(
}
}

if(
expr.arguments().empty() ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(0)))
return simplify_exprt::unchanged(expr);
Comment on lines +429 to +432

const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));

const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
Expand Down Expand Up @@ -522,6 +553,11 @@ static simplify_exprt::resultt<> simplify_string_char_at(
const function_application_exprt &expr,
const namespacet &ns)
{
if(
expr.arguments().size() < 2 ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(0)))
return simplify_exprt::unchanged(expr);

if(!expr.arguments().at(1).is_constant())
{
return simplify_exprt::unchanged(expr);
Expand Down Expand Up @@ -593,6 +629,12 @@ static simplify_exprt::resultt<> simplify_string_equals_ignore_case(
// We want to get both arguments of any starts-with comparison, and
// trace them back to the actual string instance. All variables on the
// way must be constant for us to be sure this will work.
if(
expr.arguments().size() < 2 ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(0)) ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(1)))
return simplify_exprt::unchanged(expr);

auto &first_argument = to_string_expr(expr.arguments().at(0));
auto &second_argument = to_string_expr(expr.arguments().at(1));

Expand Down Expand Up @@ -638,6 +680,12 @@ static simplify_exprt::resultt<> simplify_string_startswith(
// We want to get both arguments of any starts-with comparison, and
// trace them back to the actual string instance. All variables on the
// way must be constant for us to be sure this will work.
if(
expr.arguments().size() < 2 ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(0)) ||
!can_cast_expr<refined_string_exprt>(expr.arguments().at(1)))
return simplify_exprt::unchanged(expr);

auto &first_argument = to_string_expr(expr.arguments().at(0));
auto &second_argument = to_string_expr(expr.arguments().at(1));

Expand Down
Loading