[Do not review just yet] Cleanup exprt and expr_util #8451

tautschnig · 2024-09-10T14:43:25Z

This PR combines a series of changes that will mostly become PRs of their own.

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.
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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Cleaning of &&/|| introduced `GOTO` and `SKIP` instructions without a source location.

Removes one of the functions from the expr_util translation unit that is supposed to be deprecated.

Avoids use of the now-deprecated exprt methods.

The value representation is an implementation detail. Callers should use methods at a higher level of abstraction.

This will eventually replace `make_boolean_expr` to remove one of the functions from the expr_util translation unit, which is supposed to be deprecated.

When the operand can be a Boolean constant we can don't need to wait for simplify_exprt to clean up the avoidable not_exprt.

`make_and` does not necessarily produce an `and_exprt`, so its name is misleading. We already have `conjunction(exprt::operandst)`, and will now have a variant thereof that takes exactly two operands.

We did not consistently use it, and the three methods that did so can easily be adjusted to match the remaining ones in directly taking `exprt` instead.

This will eventually remove one of the functions from the expr_util translation unit, which is supposed to be deprecated.

This is no longer used and can easily be avoided by constructing a fixedbvt from an integer.

Use constructor chaining to avoid code duplication and remove the unused operator==(int).

tautschnig added 11 commits September 10, 2024 12:59

Goto conversion: fix missing source locations

71c77d2

Cleaning of &&/|| introduced `GOTO` and `SKIP` instructions without a source location.

Move is_null_pointer to constant_exprt

870cefd

Removes one of the functions from the expr_util translation unit that is supposed to be deprecated.

Use constant_exprt::is_{true,false,zero,one}

bcf33c1

Avoids use of the now-deprecated exprt methods.

Mark constant_exprt::value_is_zero_string protected

3ce6e43

The value representation is an implementation detail. Callers should use methods at a higher level of abstraction.

Introduce constant_exprt::constant_exprt(bool)

722063f

This will eventually replace `make_boolean_expr` to remove one of the functions from the expr_util translation unit, which is supposed to be deprecated.

Use boolean_negate for immediate simplification

fab1065

When the operand can be a Boolean constant we can don't need to wait for simplify_exprt to clean up the avoidable not_exprt.

Deprecate make_and in favour of conjunction(expr, expr)

2cd886a

`make_and` does not necessarily produce an `and_exprt`, so its name is misleading. We already have `conjunction(exprt::operandst)`, and will now have a variant thereof that takes exactly two operands.

Remove renamedt from symex_targett interface

5c3fd20

We did not consistently use it, and the three methods that did so can easily be adjusted to match the remaining ones in directly taking `exprt` instead.

Move make_with_expr to update_exprt

3b82cc3

This will eventually remove one of the functions from the expr_util translation unit, which is supposed to be deprecated.

Remove fixedbvt::operator==(int)

6be3d4d

This is no longer used and can easily be avoided by constructing a fixedbvt from an integer.

Cleanup ieee_floatt interface

f09a19b

Use constructor chaining to avoid code duplication and remove the unused operator==(int).

tautschnig added the do not review label Sep 10, 2024

tautschnig self-assigned this Sep 10, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Do not review just yet] Cleanup exprt and expr_util #8451

[Do not review just yet] Cleanup exprt and expr_util #8451

tautschnig commented Sep 10, 2024

[Do not review just yet] Cleanup exprt and expr_util #8451

Are you sure you want to change the base?

[Do not review just yet] Cleanup exprt and expr_util #8451

Conversation

tautschnig commented Sep 10, 2024