Add nonstd/optional.hpp library #1291

LAJW · 2017-08-23T15:11:12Z

This will allow us to unify and enforce proper error handling while at the same time avoid exceptions.

I'd like to include it as a submodule but @peterschrammel suggested I should just drop it in as a single file.

All credit goes to: https://github.com/martinmoene/optional-lite

LAJW · 2017-08-23T15:15:11Z

@reuk @tautschnig @smowton You might want to chip in as well.

reuk · 2017-08-23T15:24:27Z

Seems good - not sure what else there is to say.

tautschnig · 2017-08-23T15:27:01Z

@LAJW Would you mind implementing some first use case as well? I can see that it is a nice language feature, but I would like to understand better how to make it a useful language feature in the context of this code base. Thanks!

reuk · 2017-08-23T15:35:54Z

I thought of something to say: the code itself is obviously useful. Having stack-bound nullable objects is invaluable.

What's not so great is including the file directly into the repository. The number of external dependencies that are being added to this project are steadily growing (miniz, minisat, catch, this file...), and there are better approaches to dependency management than directly including the dependencies in the source tree. I recommend using CMake in conjunction with Hunter.

LAJW · 2017-08-23T15:43:59Z

@tautschnig I don't want to include a random change (as there are too many potential candidates).

Here's a clear example showing why it's superior to what we have now:

The old way:

exprt expr; // Can't be made const even if it's used in a const way
if (some_function(expr)) // Easy to forget the check, also did the function succeed or fail here?
{
   // do stuff with expr
}

The new way:

const optional<exprt> maybe_expr=some_function();
if (maybe_expr.has_value())
{
  const expr=maybe_expr.value(); // Throws if there's no value. Enforces error checking.
  // do stuff with expr
}

As you can see the problem with returning boolean to signal the error is that it's easy to forget whether false or true means success or the other way around and easy to use invalid object and the object can't be made const and it's easy to forget to check in the first place.

And if you don't like verbosity, you can use operators:

const optional<exprt> maybe_expr=some_function();
if (maybe_expr)
{
  const expr=*maybe_expr;
  // do stuff with expr
}

tautschnig · 2017-08-23T16:03:52Z

What's not so great is including the file directly into the repository. The number of external dependencies that are being added to this project are steadily growing (miniz, minisat, catch, this file...), and there are better approaches to dependency management than directly including the dependencies in the source tree. I recommend using CMake in conjunction with Hunter.

I do agree that including external source is not great as it has both maintenance (including security) and legal ramifications. Until recently, the number of such external components has been very limited and been growing at a very slow pace (miniz just being the second one after big-int, then catch came along). The conflict here is: what is best for the customer vs. what is best for developers. Customers need to be able to build the tool in/for their desired environment.

(I do refrain from naming particular technology or tools as solution at this point.)

martin-cs · 2017-08-23T16:08:05Z

On Wed, 2017-08-23 at 16:03 +0000, Michael Tautschnig wrote: > What's not so great is including the file directly into the repository. The number of external dependencies that are being added to this project are steadily growing (miniz, minisat, catch, this file...), and there are better approaches to dependency management than directly including the dependencies in the source tree. I recommend using CMake in conjunction with Hunter. I do agree that including external source is not great as it has both maintenance (including security) and legal ramifications. Until recently, the number of such external components has been very limited and been growing at a very slow pace (miniz just being the second one after big-int, then catch came along). The conflict here is: what is best for the customer vs. what is best for developers. Customers need to be able to build the tool in/for their desired environment. (I do refrain from naming particular technology or tools as solution at this point.)

Adding dependencies used to be a very frowned upon activity. I do not know if this is still the case.

LAJW · 2017-08-23T16:23:01Z

@martin-cs

Adding dependencies used to be a very frowned upon activity. I do not know if this is still the case.

I believe this refers to system dependencies (requiring users to apt-get install libz-dev for example). Which indeed introduces a lot of problems (since we're trying to be multiplatform) and should be avoided at all costs.

Using locally compiled static libraries (or header-only libraries as in this case) isn't a huge problem as long as they compile under platforms we support. We just don't have a streamlined way of handling these. Including the source is a solution, but not the ideal one, as we don't have a reference to the original repository so updating the library requires unnecessary effort. Submodules or package managers are a solution to that problem.

What isn't a solution is not including libraries whatsoever and reinventing the wheel introducing bugs along the way.

tautschnig · 2017-08-23T18:40:50Z

@LAJW Thank you very much for the example. How about switching to C++ 17 instead of using an external workaround?

LAJW · 2017-08-23T18:43:47Z

@tautschnig That would be the ideal solution. Sadly Visual Studio 2013 (AppVeyor) doesn't support it. And I'm not sure about clang/gcc since C++17 was standardized just this year.

tautschnig · 2017-08-23T18:52:44Z

What is the urgency? Does it justify introducing an external dependency? (I am not necessarily expecting public answers, you might just want to elaborate this with your management chain.)

LAJW · 2017-08-23T18:54:13Z

@tautschnig Because we're gonna be stuck with C++11 (for backward compatibility) for the foreseeable future and we don't have 6 years to wait.

tautschnig · 2017-08-23T19:01:51Z

Using locally compiled static libraries (or header-only libraries as in this case) isn't a huge problem as long as they compile under platforms we support. We just don't have a streamlined way of handling these. Including the source is a solution, but not the ideal one, as we don't have a reference to the original repository so updating the library requires unnecessary effort. Submodules or package managers are a solution to that problem.

Please do keep reproducibility in mind: at present, checking out a particular version of the git repository is guaranteed to produce exactly the same results. (MiniSat being a slight caveat, but in practice it hasn't changed in years.) With any external dependencies there need to be additional measures in place to cater for this. git submodules of course would be such a means. Package managers (whether distributions or language-specific ones) do require additional care.

Another aspect to consider is: can you build from source without a network connection? This is essential in some current users' scenarios.

peterschrammel · 2017-08-23T19:14:01Z

Optional is optional and low priority in general, but it would allow us the remove pointer usage and various workarounds with iterators and booleans in many places.
I suggested to create this PR to start the discussion whether we want to consider introducing it in the codebase. Putting it into the source tree is least invasive for our users. I expect that there is minimal maintenance overhead and it is easy to kick out again once we switch to C++17.

martin-cs · 2017-08-23T19:18:15Z

On Wed, 2017-08-23 at 16:23 +0000, Łukasz A.J. Wrona wrote: > Adding dependencies used to be a very frowned upon activity. I do not know if this is still the case. I believe this refers to system dependencies (requiring users to `apt-get install libz-dev` for example).

<snip>

What isn't a solution is not including libraries whatsoever and reinventing the wheel introducing bugs along with it.

You misunderstand my comment. I'm not saying about what's right or wrong, I'm saying about what is at the moment. The last I heard, the policy is to not add external dependencies unless it is absolutely non-impossible to solve an immediate user / customer need without doing so. I would not recommend attempting a change of policy via PR; other people have tried and it has descended into argument and got ignored. I would suggest getting Daniel (project over-all), Peter (diffblue) or Michael (most experienced / senior dev) to clarify what the policy is and then go from there. If you want to change the policy, make the case to them. However be warned that there are a significant number of users of CPROVER outside of Diffblue and you may not be aware of their deployment platforms, licensing restrictions, development environments, etc. This is one of the reasons why the project has traditionally been quite conservative with regard to deprecating older compilers, moving to newer language versions, etc. HTH

NathanJPhillips

This is quite long to review - if we're going to adopt it without proper review then should we take the Boost version that is better known and perhaps better peer reviewed?
Either way some unit tests would be very useful, both to help us know that it works and to demonstrate its use. In particular I'm concerned to make sure it handles optional references, including move (though obviously not copy) operations.
In general the code doesn't adhere to our (or any other consistent) coding standard. This may not matter as long as we're taking it as a black-box never to be reviewed.

NathanJPhillips · 2017-08-24T13:18:31Z

src/nonstd/optional.hpp

+class optional
+{
+private:
+    typedef void (optional::*safe_bool)() const;


Inconsistent indentation (previous class used our standard of two spaces).

NathanJPhillips · 2017-08-24T13:19:48Z

src/nonstd/optional.hpp

+#endif
+
+#ifndef  optional_CONFIG_ALIGN_AS_FALLBACK
+# define optional_CONFIG_ALIGN_AS_FALLBACK  double


Including this file leaves macros defined that are only for internal use.

NathanJPhillips · 2017-08-24T13:21:20Z

src/nonstd/optional.hpp

+
+// Compiler detection (C++17 is speculative):
+
+#define optional_CPP11_OR_GREATER  ( __cplusplus >= 201103L )


We already assume C++11 in our code, doing so here could greatly simplify things.

NathanJPhillips · 2017-08-24T13:23:30Z

src/nonstd/optional.hpp

+    optional_ALIGN_TYPE( Unknown ( Unknown::* )( Unknown ) ),
+
+    nulltype
+    > > > > > > >    > > > > > > >


This definitely needs a comment explaining it.

LAJW · 2017-08-24T13:35:30Z

@NathanJPhillips I'm not the author, here's the original version: https://github.com/martinmoene/optional-lite It's already tested, no need to add any of our own.

It's supposed to be a shim for the C++17 std::optional which doesn't support reference types (but can be used with std::reference_wrapper as other std::containers). It adheres to standard unlike Boost version (which in addition has several dependencies of its own).

tautschnig · 2017-08-24T13:38:42Z

It's already tested, no need to add any of our own.

This level of trust on someone else's QA work seems inappropriate to me. In addition to plain QA, and as @NathanJPhillips pointed out, tests would also serve as guidance and documentation.

LAJW · 2017-08-25T10:26:56Z

@tautschnig Added unit tests. Hope that this proves that this code works with our codebase.

LAJW · 2017-08-30T12:55:41Z

I admit my trust in the library's correctness has been misplaced.

Pragma's couldn't fix the problem. Switched to a different library (Which passes on our CI without warnings): https://github.com/akrzemi1/Optional/
Added a header wrapping optional as a optionalt so we can easily replace it later when we gain access to C++17.

Edit: Library completely incompatible with VS.

LAJW · 2017-08-31T08:59:59Z

Alright, I've manually fixed the library (there were 2 lines in need of changing). Re-requesting review.

thk123

I've not reviewed the optional.hpp file. I've also not used the C++17 optional so I'm not an expert in exactly how it should be used, so take comments with a pinch of salt if they don't make sense.

Since as pointed out in the discussion we are assuming the validity of others code, it might be good to add unit tests for:

optional with pointers
optional references (const and non-const)

thk123 · 2017-09-01T09:16:27Z

src/util/optional.h

@@ -0,0 +1,38 @@
+/*******************************************************************\


I'm not sure I understand the purpose of this file?

Description updated.

thk123 · 2017-09-01T09:21:28Z

unit/Makefile

@@ -6,6 +6,7 @@ SRC = src/expr/require_expr.cpp \
      unit_tests.cpp \
      catch_example.cpp \
      util/expr_iterator.cpp \
+      optional.cpp \


This should be in the util subfolder.

thk123 · 2017-09-01T09:30:11Z

unit/optional.cpp

+#include <catch.hpp>
+#include <util/optional.h>
+
+TEST_CASE("Optional without a value")


As per the guidelines could you tag your tests appropriately:

[core][util][optional]

thk123 · 2017-09-01T09:30:29Z

unit/optional.cpp

+    maybe_value.value();
+    REQUIRE(false); // Should have thrown an exception
+  }
+  catch(const bad_optional_accesst&) { }


Catch provides the ability to verify exceptions: https://github.com/philsquared/Catch/blob/master/docs/assertions.md#exceptions

LAJW · 2017-09-01T12:02:17Z

@thk123 This and std::optional doesn't allow references. boost::optional does.

thk123

Seems reasonable

peterschrammel · 2017-09-04T15:19:25Z

@LAJW, rebase please

08f269c Merge pull request diffblue#1388 from smowton/merge-develop-20170914 e3f3abd Merge remote-tracking branch 'upstream/develop' into merge-develop-20170914 4df244c Merge pull request diffblue#1383 from reuk/reuk/sync-projects f25db0a Merge pull request diffblue#189 from diffblue/smowton/fix/remove_debug_code 1fae64c Remove stray use of overlay_map 1264b4d Re-enable old function signatures for test-gen compat e54c0e9 Merge pull request diffblue#338 from thk123/bug/function-flag-on-goto-program 63c9a1e Merge pull request diffblue#1374 from reuk/reuk/maintain-pointer-invariants 00e4555 Fix up CMake build (unrelated) 81f1300 Use PRECONDITION in std_types.h a9806c0 Ensure pointer invariants are maintained a46ad62 Regenerate malformed binary blobs f77822b Merge pull request diffblue#1380 from diffblue/remove-musketeer 22f06fd Correcting windows build 3ede81b Merge pull request diffblue#1293 from reuk/cmake-develop 92a52a5 Corrected doxygen errors c6f1430 Ensure symex and goto-analyzer regenerate functions e37d3d5 Disable failing test in the symex directory 15b89fc Weaked the tests for pointer-function-parameters dee89b0 Fixing the method to work with java_bytecode 1ccd1a2 Add support for using the --function flag to goto-analyze and symex 0732580 Adding missing overrides 71dec3d Use ID_main as the default name for entry function 2aea88d Made generate_start_function abstract f0d6d72 Refactored the regenerate function into goto-programs 71e6800 Added regression test for using --function on a GOTO program 94b7185 Implemented generate_start_function for Java cd416bc Call generate_start_function only when regenerating the start function ee5fb93 Protect against invalid function label 2a3d876 Adding explanatory comment f347a22 Cause a regeneration of the entry method if a --function is provided 69d05a9 Merge pull request diffblue#1382 from pkesseli/bugfix/language-opaque-stubs d45325c Merge pull request diffblue#1378 from thk123/bugfix/fix-symex-appveyor 444f256 Add initial value to languaget::generate_opaque_stubs 91e733d Manually disable some failing tests 41bafc0 Merge pull request diffblue#1375 from pkesseli/bugfix/uncaught-exceptions-invariant a31f1d9 remove musketeer af8d46f Reverting manually commited fixes e73a884 Attempt to fix the symex appveyor build 0496142 Account for replaced functions in exceptions_map 2816b80 revert symex regression until Appvoyer works 6a2fd50 added symex to Appveyor build a2834d0 Map wrappers: forward more of the std::map interface 0a668ae Merge commit '6f386e5eeffa223e7213b596403085f8b497023e' into pull-support-20170908-2 8cd4490 Merge pull request diffblue#1373 from diffblue/symex-trace-fix 5d2d07b enable symex regression testing 5195d24 avoid confusion between SSA lhs and full lhs during assignment 430218f option is now --trace 746bff5 remove_returns missing in symex 211355d comments on test 3896110 output statements 8fc714d use __CPROVER_assert 728ac5b Merge pull request diffblue#1367 from reuk/reuk/disable-alpine-in-travis 73b4357 Merge pull request diffblue#1339 from diffblue/initialize_goto_model 4febd10 Merge pull request diffblue#1364 from diffblue/phread-create-fix 0cfd7b0 Remove PRE_COMMAND scaffolding 04b4f63 Merge pull request diffblue#186 from diffblue/cleanup/misc 577fa6c Tightened up usage of maps 8782103 Merge pull request diffblue#1365 from smowton/smowton/feature/more_map_forwarding 4dde3c5 Disable glucose in Travis 91684da Clean up CMake files after diffblue#1321 7d4e9b5 Make CMake release flags similar to Makefile build 5ee349f Control SAT library from makefiles ad486f8 Set up glucose externalproject 5afa929 Quote paths in flex/bison commands 9afbced Disable 32-bit builds in Travis d953327 Enable caching for CMake builds (hopefully) 6251055 Fix and refactor library_check target 3c36aa5 Enable CMake in Travis f6e4968 Enable running tests from CMake e609bbb Add CMake howto to COMPILING file 22c2ab9 Add CMakeLists 6facf74 Map wrappers: forward more of the std::map interface b846858 Merge pull request diffblue#1291 from LAJW/optional 3ddd377 clean-out ill-modeled optimization in string comparisons 95c5e63 Disable Alpine in Travis fe60e60 pthread_create arguments null/nonnull fix 7d30cde missing copyright header 8c4ff7b remove spurious references to langapi/language_ui.h e4498ca brief list of symbols, from language_uit fc4d44a use goto_modelt 9469552 use initialize_goto_model in CBMC/goto-analyse/etc 40fe0f8 simplify API of goto_convert 40557df Used range iterators d4e89fd Tidy up symbol_tablet::move c125146 Merge pull request diffblue#1245 from tautschnig/run-diagnostic 435c0bf Merge pull request diffblue#1321 from reuk/reuk/remove-unused-files 08a4077 Make the child process that failed to execvp exit 4928f69 Diagnostic output if run/execve fails 5863a75 Merge pull request diffblue#1333 from tautschnig/remove-c_sizeof 498718f Code readability 2217501 Remove unused files 1c8d81a Merge pull request diffblue#1356 from smowton/smowton/feature/test_pl_add_dry_run 56b5e25 Merge pull request diffblue#1358 from thk123/feature/decrease-message-spam 359a3e3 Modified verbosity for loaded message 296349c Add dry-run mode to test.pl f6d94cf clean out an unused method 3613ebc When possible, update array types before typechecking initializer 3273bf5 Fix type casts from initializer lists to arrays of unspecified size 1fa569f sizeof(*(void*)) is sizeof(char) d79067e Remove long-deprecated c_sizeof in favour of size_of_expr et al. 254f133 Merge pull request diffblue#1323 from janmroczkowski/janmroczkowski/goto_modelt-output-const 388a25e Make uncaught_exceptions_analysis.output const 211fcc2 Make path_nodet.output const 9be84ea Make automatont.output const 567eaa7 Make basic_blockst.output const ebbbf5f Make goto_modelt.output const ae584df Move optional unit tests into util directory 4dbf939 Manually fix optional 43d0602 Add unit tests for nonstd::optional 8584bb0 Add nonstd/optional.hpp library 281e384 Workaround for travis performing shallow clones with wrong branch git-subtree-dir: cbmc git-subtree-split: 08f269c

NathanJPhillips reviewed Aug 24, 2017

View reviewed changes

smowton approved these changes Aug 31, 2017

View reviewed changes

thk123 reviewed Sep 1, 2017

View reviewed changes

thk123 approved these changes Sep 1, 2017

View reviewed changes

Lukasz A.J. Wrona added 4 commits September 4, 2017 16:14

Add nonstd/optional.hpp library

8584bb0

Add unit tests for nonstd::optional

43d0602

Manually fix optional

4dbf939

Move optional unit tests into util directory

ae584df

peterschrammel assigned kroening Sep 4, 2017

kroening merged commit b846858 into diffblue:develop Sep 11, 2017

thk123 mentioned this pull request Sep 18, 2017

TG-374 Feature/java support generics #1322

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add nonstd/optional.hpp library #1291

Add nonstd/optional.hpp library #1291

LAJW commented Aug 23, 2017 •

edited

Loading

LAJW commented Aug 23, 2017

reuk commented Aug 23, 2017

tautschnig commented Aug 23, 2017

reuk commented Aug 23, 2017

LAJW commented Aug 23, 2017 •

edited

Loading

tautschnig commented Aug 23, 2017

martin-cs commented Aug 23, 2017 via email

LAJW commented Aug 23, 2017 •

edited

Loading

tautschnig commented Aug 23, 2017

LAJW commented Aug 23, 2017

tautschnig commented Aug 23, 2017

LAJW commented Aug 23, 2017

tautschnig commented Aug 23, 2017

peterschrammel commented Aug 23, 2017

martin-cs commented Aug 23, 2017 via email

NathanJPhillips left a comment

NathanJPhillips Aug 24, 2017

NathanJPhillips Aug 24, 2017

NathanJPhillips Aug 24, 2017

NathanJPhillips Aug 24, 2017

LAJW commented Aug 24, 2017 •

edited

Loading

tautschnig commented Aug 24, 2017

LAJW commented Aug 25, 2017

LAJW commented Aug 30, 2017 •

edited

Loading

LAJW commented Aug 31, 2017

thk123 left a comment

thk123 Sep 1, 2017

LAJW Sep 1, 2017

thk123 Sep 1, 2017

thk123 Sep 1, 2017

thk123 Sep 1, 2017

LAJW commented Sep 1, 2017

thk123 left a comment

peterschrammel commented Sep 4, 2017


		// Compiler detection (C++17 is speculative):

		#define optional_CPP11_OR_GREATER ( __cplusplus >= 201103L )

		@@ -0,0 +1,38 @@
		/*******************************************************************\

Add nonstd/optional.hpp library #1291

Add nonstd/optional.hpp library #1291

Conversation

LAJW commented Aug 23, 2017 • edited Loading

LAJW commented Aug 23, 2017

reuk commented Aug 23, 2017

tautschnig commented Aug 23, 2017

reuk commented Aug 23, 2017

LAJW commented Aug 23, 2017 • edited Loading

tautschnig commented Aug 23, 2017

martin-cs commented Aug 23, 2017 via email

LAJW commented Aug 23, 2017 • edited Loading

tautschnig commented Aug 23, 2017

LAJW commented Aug 23, 2017

tautschnig commented Aug 23, 2017

LAJW commented Aug 23, 2017

tautschnig commented Aug 23, 2017

peterschrammel commented Aug 23, 2017

martin-cs commented Aug 23, 2017 via email

NathanJPhillips left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW commented Aug 24, 2017 • edited Loading

tautschnig commented Aug 24, 2017

LAJW commented Aug 25, 2017

LAJW commented Aug 30, 2017 • edited Loading

LAJW commented Aug 31, 2017

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW commented Sep 1, 2017

thk123 left a comment

Choose a reason for hiding this comment

peterschrammel commented Sep 4, 2017

LAJW commented Aug 23, 2017 •

edited

Loading

LAJW commented Aug 23, 2017 •

edited

Loading

LAJW commented Aug 23, 2017 •

edited

Loading

LAJW commented Aug 24, 2017 •

edited

Loading

LAJW commented Aug 30, 2017 •

edited

Loading