add constant_exprt variants of numeric_cast #3998

kroening · 2019-01-30T18:43:06Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig

What is the desired benefit? (Commit message is lacking this info...)

tautschnig · 2019-01-30T18:49:39Z

src/util/arith_tools.h

  {
    mp_integer out;
-    if(expr.id() != ID_constant || to_integer(to_constant_expr(expr), out))
+    if(to_integer(to_constant_expr(expr), out))


to_constant_expr isn't necessary anymore.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: c8be185).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99177767

smowton

Except as per @tautschnig

numeric_cast is frequently used on constant_exprt typed arguments. The specialised version saves two branches.

tautschnig

I find "numeric_cast is frequently used on constant_exprt typed arguments." somewhat surprising, but if that's the case then of course this makes sense.

kroening · 2019-01-31T08:44:12Z

@tautschnig There's the somewhat stylistic point here whether you want the caller to check the interface at runtime or let the compiler enforce it.

I am in favour of compile-time type checking (I even like predicate subtyping).

A more extreme version of this PR would remove the exprt variant, as calling with anything but constant_exprt will never work.

tautschnig · 2019-01-31T08:51:16Z

There's the somewhat stylistic point here whether you want the caller to check the interface at runtime or let the compiler enforce it.

Yes, but that was not something that the commit message talked about.

I am in favour of compile-time type checking (I even like predicate subtyping).

Certainly.

A more extreme version of this PR would remove the exprt variant, as calling with anything but constant_exprt will never work.

The current approach, however, avoids a lot of redundancy: instead of first checking in each an every place, just call the function. In places where we do know that it is a constant and do expect that we have a numeric constant we ought to be using numeric_cast_v.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 3437e52).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99243396
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

kroening added work in progress do not review labels Jan 30, 2019

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners January 30, 2019 18:43

tautschnig reviewed Jan 30, 2019

View reviewed changes

allredj reviewed Jan 30, 2019

View reviewed changes

smowton approved these changes Jan 30, 2019

View reviewed changes

tautschnig assigned kroening Jan 31, 2019

add constant_exprt variants of numeric_cast

3437e52

numeric_cast is frequently used on constant_exprt typed arguments. The specialised version saves two branches.

kroening force-pushed the numeric_cast_constant_expr branch from c8be185 to 3437e52 Compare January 31, 2019 08:05

kroening removed do not review work in progress labels Jan 31, 2019

kroening assigned tautschnig and unassigned kroening Jan 31, 2019

tautschnig approved these changes Jan 31, 2019

View reviewed changes

kroening merged commit 2376058 into develop Jan 31, 2019

kroening deleted the numeric_cast_constant_expr branch January 31, 2019 09:14

allredj reviewed Jan 31, 2019

View reviewed changes

kroening mentioned this pull request Jan 31, 2019

numeric_cast_v(expr) now requires constant_expr #4004

Merged

2 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

add constant_exprt variants of numeric_cast #3998

add constant_exprt variants of numeric_cast #3998

Uh oh!

kroening commented Jan 30, 2019 •

edited

Loading

Uh oh!

tautschnig left a comment

Uh oh!

tautschnig Jan 30, 2019

Uh oh!

kroening Jan 31, 2019

Uh oh!

allredj left a comment

Uh oh!

smowton left a comment

Uh oh!

tautschnig left a comment

Uh oh!

kroening commented Jan 31, 2019

Uh oh!

tautschnig commented Jan 31, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

add constant_exprt variants of numeric_cast #3998

add constant_exprt variants of numeric_cast #3998

Uh oh!

Conversation

kroening commented Jan 30, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 30, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Jan 31, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Jan 31, 2019

Uh oh!

tautschnig commented Jan 31, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kroening commented Jan 30, 2019 •

edited

Loading