Skip to content
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

Remove all references to optionalt #8099

Merged
merged 1 commit into from
Dec 15, 2023
Merged

Remove all references to optionalt #8099

merged 1 commit into from
Dec 15, 2023

Conversation

tautschnig
Copy link
Collaborator

We now use std::optional instead.

I am not sure it's worth the code churn to review/merge this at this point. Most of the changes were implemented using git grep -wl optionalt | xargs sed -i 's/optionalt/std::optional/g' followed by removal of #include <util/optional.h> and then manually re-adding #include <optional> as needed (plus clang-format). My main reason for even embarking on this was to figure out what changes are needed so as to get rid of -Wno-deprecated-declarations.

  • 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/
  • 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 tautschnig self-assigned this Dec 13, 2023
@tautschnig tautschnig force-pushed the cleanup/optionalt branch 2 times, most recently from 7163984 to d59b89b Compare December 13, 2023 10:43
@codecov Codecov
Copy link

codecov bot commented Dec 13, 2023 •
edited
Loading

Codecov Report

Attention: 21 lines in your changes are missing coverage. Please review.

Comparison is base (97ab133) 79.08% compared to head (851c486) 79.08%.

Files Patch % Lines
src/cpp/parse.cpp 66.66% 6 Missing ⚠️
src/solvers/strings/string_builtin_function.cpp 33.33% 4 Missing ⚠️
src/goto-cc/ms_cl_cmdline.cpp 0.00% 2 Missing ⚠️
src/analyses/call_graph.cpp 50.00% 1 Missing ⚠️
src/goto-cc/armcc_cmdline.cpp 0.00% 1 Missing ⚠️
src/goto-cc/ms_link_cmdline.cpp 0.00% 1 Missing ⚠️
src/goto-instrument/accelerate/polynomial.cpp 0.00% 1 Missing ⚠️
...o-instrument/accelerate/polynomial_accelerator.cpp 0.00% 1 Missing ⚠️
...strument/contracts/dynamic-frames/dfcc_library.cpp 0.00% 1 Missing ⚠️
src/goto-programs/destructor_tree.cpp 50.00% 1 Missing ⚠️
... and 2 more
Additional details and impacted files 
@@           Coverage Diff            @@
##           develop    #8099   +/-   ##
========================================
  Coverage    79.08%   79.08%           
========================================
  Files         1698     1698           
  Lines       196457   196460    +3     
========================================
+ Hits        155370   155376    +6     
+ Misses       41087    41084    -3

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@tautschnig tautschnig force-pushed the cleanup/optionalt branch 6 times, most recently from 1484567 to 16aed20 Compare December 13, 2023 12:04
thomasspriggs
thomasspriggs approved these changes Dec 13, 2023
View reviewed changes
Copy link
Contributor

@thomasspriggs thomasspriggs left a comment

Choose a reason for hiding this comment

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

Getting this merged for version 6 should be given a reasonably high priority. The reason being that you cannot construct or assign an optionalt using an std::optional (or the other way around.) So if we don't get rid of optionalt, then this could lead to awkward maintenance where maintainers need to consider which type of optional to use in which place.

jbmc/src/java_bytecode/jar_file.h
@@ -13,8 +13,6 @@ Author: Diffblue Ltd
#include <string>
#include <vector>

#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ Shouldn't this be replaced by #include <optional>? If this is working at the moment, I'd guess it was down to transitive includes.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It seemed to work fine on my Ubuntu 20.04, but other OS/compiler combinations indeed make those includes necessary. I had naively assumed that standard library headers would likely (transitively) include that anyway, but as experimenting shows that's not always the case. So, yes, I may well end up putting this back in.

Copy link
Contributor

Choose a reason for hiding this comment

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

Good to see this being fixed.

I'd prefer to avoid relying on transitive header includes where possible. With optional as an example my reasoning goes something like -

  1. Header "A" depends on optional so #include <optional> is added to it.
  2. .cpp file "B" depends on header "A" and uses std::optional in its implementation. It therefore depends on optional, but as this .cpp already includes header "A" #include <optional> is not added to it.
  3. Maintainer of header "A" decides they no longer need to depend on optional. Lets say they were using it for the type of a private member function rather than as part of the exposed API. They remove the #include <optional> from header "A", because it no longer needs it itself.
  4. The compilation of .cpp "B" now fails. This means that the maintainer of header "A" now needs to either add the include to the .cpp file, or to leave the extra include in their header.

Leaving the extra include in could potentially extend compile times. Adding it to the .cpp increases the number of changes in their PR and potentially requires approval from more code owners. The decision and additional work could have been avoided if the reliance on transitive includes had been avoided.

src/goto-harness/memory_snapshot_harness_generator.h
@@ -9,8 +9,6 @@ Author: Daniel Poetzl
#ifndef CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H
#define CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H

#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ See previous comment about #include <optional>

src/goto-harness/recursive_initialization.h
@@ -14,7 +14,6 @@ Author: Diffblue Ltd.
#include <unordered_set>

#include <util/cprover_prefix.h>
#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ See previous comment about #include <optional>

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp
@@ -16,7 +16,6 @@ Author: Remi Delmas, [email protected]
#include <util/mathematical_expr.h>
#include <util/mathematical_types.h>
#include <util/namespace.h>
#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ See previous comment about #include <optional>

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h
@@ -17,7 +17,6 @@ Date: August 2022

#include <util/message.h>
#include <util/namespace.h>
#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ See previous comment about #include <optional>

src/goto-programs/restrict_function_pointers.h
@@ -22,7 +22,6 @@ Author: Diffblue Ltd.

#include <util/exception_utils.h>
#include <util/irep.h>
#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ See previous comment about #include <optional>

src/goto-programs/show_properties.h Show resolved Hide resolved
src/pointer-analysis/add_failed_symbols.h
@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
#define CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H

#include <util/expr.h>
#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ See previous comment about #include <optional>

src/util/arith_tools.h
@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]

#include "invariant.h"
#include "mp_arith.h"
#include "optional.h"
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ See previous comment about #include <optional>

src/util/dense_integer_map.h
@@ -17,7 +17,6 @@ Author: Diffblue Ltd
#include <vector>

#include <util/invariant.h>
#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ See previous comment about #include <optional>

@thomasspriggs thomasspriggs added the Version 6 Pull requests and issues requiring a major version bump label Dec 13, 2023
@tautschnig tautschnig force-pushed the cleanup/optionalt branch 2 times, most recently from 56a6b7d to f943b6b Compare December 13, 2023 12:20
@kroening
Copy link
Member

I am not sure it's worth the code churn

Maybe not under normal circumstances, but I'd be inclined to say that the transition to 6.0 makes it appropriate.

@tautschnig tautschnig force-pushed the cleanup/optionalt branch 3 times, most recently from 409998b to 3294030 Compare December 13, 2023 13:43
@tautschnig tautschnig force-pushed the cleanup/optionalt branch 5 times, most recently from 1ed1640 to d7629f1 Compare December 13, 2023 15:39
@tautschnig
Remove all references to optionalt
851c486 
We now use `std::optional` instead.
@tautschnig tautschnig removed their assignment Dec 13, 2023
@thomasspriggs thomasspriggs mentioned this pull request Dec 15, 2023
Merged
@tautschnig tautschnig assigned feliperodri and unassigned TGWDB Dec 15, 2023
feliperodri
feliperodri approved these changes Dec 15, 2023
View reviewed changes
Copy link
Collaborator

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

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

LGTM in all contracts related changes.

@feliperodri feliperodri removed their assignment Dec 15, 2023
@kroening kroening merged commit 8e11ee9 into diffblue:develop Dec 15, 2023
36 checks passed
@tautschnig tautschnig deleted the cleanup/optionalt branch December 15, 2023 20:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@thomasspriggs thomasspriggs thomasspriggs approved these changes

@kroening kroening kroening approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@feliperodri feliperodri feliperodri approved these changes

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@NlightNFotis NlightNFotis Awaiting requested review from NlightNFotis

@TGWDB TGWDB Awaiting requested review from TGWDB TGWDB is a code owner

@qinheping qinheping Awaiting requested review from qinheping qinheping is a code owner

@remi-delmas-3000 remi-delmas-3000 Awaiting requested review from remi-delmas-3000 remi-delmas-3000 is a code owner

Assignees

@kroening kroening

Labels
cleanup Version 6 Pull requests and issues requiring a major version bump
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@tautschnig @kroening @peterschrammel @feliperodri @thomasspriggs @TGWDB