Skip to content

move floating-point-related expression classes into separate header file #5760

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

Jump to bottom
Merged
merged 1 commit into from
Jan 18, 2021
Merged

move floating-point-related expression classes into separate header file #5760

merged 1 commit into from
Jan 18, 2021

Conversation

kroening
Copy link
Member

std_expr.h is by far the largest header file, which impedes on readability.
This commit moves the floating-point-related expression classes into a
separate header file, following the pattern in mathematical_expr.h.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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/
  • n/a 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.

@kroening
move floating-point-related expression classes into separate header file
d140f15 
std_expr.h is by far the largest header file, which impedes on readability.
This commit moves the floating-point-related expression classes into a
separate header file, following the pattern in mathematical_expr.h.
@codecov
Copy link

codecov bot commented Jan 18, 2021 •
edited
Loading

Codecov Report

Merging #5760 (d140f15) into develop (6c59fc8) will not change coverage.
The diff coverage is 64.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5760   +/-   ##
========================================
  Coverage    69.65%   69.65%           
========================================
  Files         1245     1246    +1     
  Lines       100842   100842           
========================================
  Hits         70242    70242           
  Misses       30600    30600
Flag Coverage Δ
cproversmt2 43.39% <40.81%> (ø)
regression 66.56% <48.00%> (ø)
unit 32.20% <0.00%> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
...src/java_bytecode/java_bytecode_convert_method.cpp 97.44% <ø> (ø)
...c/java_bytecode/java_string_library_preprocess.cpp 96.86% <ø> (ø)
src/analyses/goto_check.cpp 88.35% <ø> (ø)
src/ansi-c/c_typecheck_expr.cpp 75.47% <ø> (ø)
src/ansi-c/expr2c.cpp 69.50% <ø> (ø)
src/goto-programs/adjust_float_expressions.cpp 92.53% <ø> (ø)
src/solvers/flattening/boolbv.cpp 69.09% <ø> (ø)
src/solvers/flattening/boolbv.h 78.57% <ø> (ø)
src/solvers/flattening/boolbv_floatbv_op.cpp 64.28% <ø> (ø)
src/solvers/floatbv/float_bv.cpp 74.17% <ø> (ø)
... and 9 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 6c59fc8...d140f15. Read the comment docs.

martin-cs
martin-cs approved these changes Jan 18, 2021
View reviewed changes
src/solvers/flattening/boolbv.h
@@ -31,6 +31,8 @@ class bswap_exprt;
class concatenation_exprt;
class extractbit_exprt;
class extractbits_exprt;
class floatbv_typecast_exprt;
class ieee_float_op_exprt;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why are these forward declared when other types are not. I can see cases for forward declaration or inclusion but the mix seems unclear.

Copy link
Member Author

Choose a reason for hiding this comment

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

The algorithm is to count the .cpp files that includes this .h file that include the omitted header file. If that is a high percentage, then use the include, otherwise use the forward declaration.

In this case, a lot of .cpp files (46) include boolbv.h but do not need the full floatbv_expr.h (32).

@kroening kroening marked this pull request as ready for review January 18, 2021 15:38
@tautschnig tautschnig merged commit 88d8868 into develop Jan 18, 2021
@tautschnig tautschnig deleted the floatbv_expr_h branch January 18, 2021 20:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@martin-cs martin-cs martin-cs approved these changes

@allredj allredj Awaiting requested review from allredj

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

@smowton smowton Awaiting requested review from smowton

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@kroening @tautschnig @peterschrammel @martin-cs