type_dynamic_cast (extension of expr_cast) #1667

romainbrenguier · 2017-12-13T11:23:46Z

This is similar to expr_cast (added by @NathanJPhillips), with some code duplication.
Allows to use type_dynamic_cast<> for typet objects in the same way we
use expr_dynamic_cast<> for exprt.
This PR adds an example use of this for pointer_typet.

smowton · 2017-12-13T11:26:47Z

@NathanJPhillips could you review please?

romainbrenguier · 2017-12-13T11:29:41Z

@NathanJPhillips could you review please?

By the way, is there a reason I cannot add @NathanJPhillips as a reviewer?

smowton · 2017-12-13T11:30:38Z

I think it's because he's a "grey tick," for unknown reasons

tautschnig · 2017-12-13T11:55:17Z

src/solvers/flattening/boolbv_width.cpp

-    entry.total_width=to_pointer_type(type).get_width();
-    DATA_INVARIANT(entry.total_width!=0, "pointer must have width");
-  }
+    entry.total_width=type_dynamic_cast<pointer_typet>(type).get_width();


When is it considered ok to use a type_dynamic_cast and when should a type_checked_cast be used instead?

type_dynamic_cast throws an exception if it cannot cast while type_checked_cast has a precondition.
Actually I think the checked one would be better here since we don't catch the exception.

NathanJPhillips · 2017-12-13T18:25:45Z

src/util/std_types.h

+
+inline void validate_type(const pointer_typet &type)
+{
+  INVARIANT(type.get_width() > 0, "pointer must have non-zero width");


This is a DATA_INVARIANT

NathanJPhillips · 2017-12-13T18:27:33Z

src/util/std_types.h

@@ -1402,6 +1403,16 @@ inline pointer_typet &to_pointer_type(typet &type)
  return static_cast<pointer_typet &>(type);
 }

+template<> inline bool can_cast_type<pointer_typet>(const typet &type)
+{
+  return type.id()==ID_pointer && !type.get(ID_width).empty();


The latter part of this looks like a validation - can we have something that has type.id()==ID_pointer without also having an ID_width field?

NathanJPhillips · 2017-12-13T18:29:06Z

src/util/expr_cast.h

@@ -29,6 +29,9 @@ Author: Nathan Phillips <[email protected]>
 /// \return true if \a base is of type \a T
 template<typename T> inline bool can_cast_expr(const exprt &base);

+/// Similar to can_cast_expr(const exprt &base) but for typet.


This comment will appear in generated docs so it is worth copying the more expressive comment above.

NathanJPhillips · 2017-12-13T18:29:16Z

src/util/expr_cast.h

@@ -37,6 +40,9 @@ template<typename T> inline bool can_cast_expr(const exprt &base);
 /// validate objects in this way at any time.
 inline void validate_expr(const exprt &) {}

+/// Similar to validate_expr(const exprt &) but for typet.


Again here.

NathanJPhillips · 2017-12-13T18:29:43Z

src/util/expr_cast.h

@@ -86,6 +92,26 @@ auto expr_try_dynamic_cast(TExpr &base)
  return ret;
 }

+template <typename T, typename TType>


Add documentation based on that above.

romainbrenguier · 2017-12-15T12:35:01Z

@NathanJPhillips this is ready for being reviewed again

tautschnig · 2017-12-15T13:19:55Z

I'd say this is now in @NathanJPhillips' hands.

martin-cs

I agree that if total_width != 0 is actually a data invariant then it should be checked as part of the conversion / general "well formed"-ness checks. I think I also agree these should be independent of the conversion functions.

martin-cs · 2017-12-15T13:33:34Z

src/solvers/flattening/boolbv_width.cpp

-    entry.total_width=to_pointer_type(type).get_width();
-    DATA_INVARIANT(entry.total_width!=0, "pointer must have width");
-  }
+    entry.total_width=type_checked_cast<pointer_typet>(type).get_width();


Again, the commit message needs to be adjusted.

martin-cs · 2017-12-15T13:34:47Z

src/util/expr_cast.h

+/// validate particular types.  Should always succeed unless the program has
+/// entered an invalid state.  We validate objects at cast time as that is when
+/// these checks have been used historically, but it would be reasonable to
+/// validate objects in this way at any time.


Can we say the word "invariant" here, or "data invariant"?

martin-cs · 2017-12-15T13:38:42Z

src/util/std_types.h

+inline void validate_type(const pointer_typet &type)
+{
+  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
+  DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width");


To check that these really are invariants (I believe they should be but it is always good to check), could we add a call to this validate_type to to_pointer_type, that was we aren't enforcing different invariants depending on which system you use.

tautschnig

Can I just throw a brief block in here: why do we have both type_dynamic_cast and type_checked_cast when the choice between assertions and exceptions is actually configurable (to be configured?) via invariant.h?

peterschrammel · 2017-12-19T13:18:04Z

src/util/expr_cast.h

+auto type_checked_cast(TType &base)
+  -> typename detail::expr_dynamic_cast_return_typet<T, TType>::type
+{
+  PRECONDITION(can_cast_type<T>(base));


This looks non-optimal as can_cast_type is called twice (here and in type_try_dynamic_cast). Wouldn't it better to put the assertion on the return value of type_try_dynamic_cast?

NathanJPhillips · 2017-12-19T14:10:35Z

@tautschnig - turning INVARIANT into exceptions would be a global (not per-INVARIANT) setting that will probably never be enabled for our purposes. Conversely turning INVARIANT off totally in release versions could well be a valid choice in some situations. A version that emits a known exception that can be caught is unlikely to be used much here but matches the static_cast/dynamic_cast pattern from the STL.

tautschnig · 2017-12-19T14:26:56Z

At present, it seems actually a bit weird: type_checked_cast can be configured (via invariant.h) not to do any checks (with a current default of throwing an exception); type_dynamic_cast will always raise an exception if the conversion failed. The latter fits what the STL does in case of references, else dynamic_cast will just return a nullptr (for pointers).

What I'd like to see argued for is a case where people explicitly want to raise and catch an exception, i.e., strictly need the present type_dynamic_cast over type_checked_cast.

romainbrenguier · 2018-01-08T13:58:53Z

@tautschnig @peterschrammel I removed type_dynamic_cast (redundant with type_ckecked_cast) and improved type_checked_cast

tautschnig

I'm fine with this once the commit messages are updated.

tautschnig · 2018-01-08T14:01:44Z

src/util/expr_cast.h

+/// \param base Reference to a generic \ref typet
+/// \return Reference to object of type \a T
+template<typename T, typename TType>
+auto type_checked_cast(TType &base)


It seems the commit message doesn't match anymore?

tautschnig · 2018-01-08T14:03:29Z

src/solvers/flattening/boolbv_width.cpp

-    entry.total_width=to_pointer_type(type).get_width();
-    DATA_INVARIANT(entry.total_width!=0, "pointer must have width");
-  }
+    entry.total_width=type_checked_cast<pointer_typet>(type).get_width();


Again, the commit message needs to be adjusted.

romainbrenguier · 2018-01-08T14:10:12Z

@tautschnig commit messages updated

tautschnig

It may be worth adjusting the changes to make clang-format happy.

tautschnig · 2018-01-08T14:39:51Z

Assigning to @romainbrenguier to possibly add clang-format fixes and then merge once happy.

This is similar to expr_cast functions, with some code duplication. Allows to use type_try_dynamic_cast<> and type_checked_cast<> for typet objects in the same way we use expr_try_dynamic_cast<> and expr_checked_cast<> for exprt.

This performs the necessary checks to ensure the type is a well formed pointer type.

d190fd8 Merge remote-tracking branch 'upstream/develop' into pull-support-20180112 5bd5962 Merge pull request diffblue#1667 from romainbrenguier/feature/type_cast 8ecb55a Merge pull request diffblue#1717 from smowton/smowton/feature/remove_virtual_functions_per_function 0d7310a Merge pull request diffblue#1691 from romainbrenguier/bugfix/getClass#TG-1245 2064849 Use type_checked_cast in boolbv_width c5fc351 Validate data in pointer_typet in to_pointer_typet 35905c6 Add can_cast_type, validate_type for pointer_typet b72bacf Define type_try_dynamic_cast and type_checked_cast 23c3561 Unit test for string symbol resolution c13e602 Adding only needed equations in symbol resolution ae4deff Debug information for string equations 912828d JBMC: Run remove-virtual-functions as each function is converted a711c64 Introduce mechanism for renumbering an individual GOTO program e308a32 Merge pull request diffblue#1679 from NlightNFotis/nondet_extra_test e6ceb91 Merge pull request diffblue#1724 from tautschnig/fix-visitor ea74bed Add extra test for nondet-static flag and arrays 4f74896 Use irept API, not implementation-level API c55b4a5 Merge pull request diffblue#1682 from martin-cs/fix/dependence-graph-namespace-lifespan 1a2c14b Merge pull request diffblue#1722 from diffblue/unsafe_type_constructors 957a568 Merge pull request diffblue#1677 from NlightNFotis/pb4_develop 9c5add4 remove deprecated constructors for three bitvector types c96e02a no longer use deprecated constructors for some bitvector types 954060e Add unit test for has_subtype 3dd3877 Refactor has_char_pointer_subtype with has_subtype 4699c13 Extend symbol resolution to string_typet 74144fc Handle if_exprt in add_axioms_for_string_literal c6c1b3f Add an optional guard to add_axioms_for_constant 933d635 Merge pull request diffblue#1716 from mgudemann/fix/null_check_for_java_instanceof 1659314 Merge pull request diffblue#1715 from smowton/smowton/cleanup/jbmc_unused_passes 9c457b7 Add regression test for null instanceof. 2080cd3 Complete instanceof for Java. d4300d0 Merge pull request diffblue#1697 from diffblue/nondet_symbol_exprt 1c68dd4 Merge pull request diffblue#1714 from tautschnig/c-library-strcat 44b5bae Merge pull request diffblue#1698 from thomasspriggs/tg1633 c4304ba JBMC: Remove C-only passes bb8cfaa C library: Check upper bounds in memset, memcpy, memmove 7d4984f C library: Implement strcat, strncat 2a5cea2 This introduces nondet_symbol_exprt, which is generated by symbolic execution in response to side_effect_expr_nondett 85193a0 Merge pull request diffblue#1694 from NathanJPhillips/feature/add-raw-lhs-to-trace d9122dc Merge pull request diffblue#1710 from NathanJPhillips/feature/remove_instanceof_per_function 092df69 Switch from custom file / path routines to Boost-filesystem c8821b2 Allow to remove instanceof when remove exceptions 94b7658 Don't pass iterators into function calls a9c4e4f Added regression tests 76318ce Protect extended trace behind a command line option 69b0ff1 Added base_name in comments for all symbols e86080a Add raw LHS irep field to trace output ddd1b7a Add remove_instanceof overload to remove from a particular instruction 1c227b7 Merge pull request diffblue#1660 from smowton/smowton/fix/lazy_methods_array_parameters ae89c94 Lazy loading: assume concrete generic parameter types are needed 80eb6a6 TG-1877: Include array pointer types in needed classes 1053e5f Fix for [TG-1633] Inner generic types have incorrect type identifier e2cda1a Merge pull request diffblue#1704 from tautschnig/fix-copy-paste ef4a65e Fix op1/op0 copy&paste typo 21ea31f Merge pull request diffblue#1702 from peterschrammel/goto-diff-java c4bc953 Merge pull request diffblue#1701 from peterschrammel/allow-instrument-jdk 2811363 Java regression test for goto-diff 43d2e09 Also reset fresh temporary symbol counter 9ef28f4 Compare relative goto target offsets eaf3a7d Get source location from symbol table ab59659 Allow instrumentation of java.* and org.cprover.* 6fbd59c Merge pull request diffblue#1631 from tautschnig/fix-pointer-minus 7c04b5c Merge pull request diffblue#1699 from NathanJPhillips/feature/reset-main-in-tests 5e0f186 Pointer difference over void* is difference over char* faf8f00 Merge commit 'a83b52cddbed22304372c276512c63701eb3aedb' into pull-support-20180104 8236db4 Merge pull request diffblue#1419 from peterschrammel/refactor/cover-instrument a580e27 Merge pull request diffblue#1689 from smowton/smowton/feature/get_this 591511a Allow callers of load_java_class to pass the name of the main function 1b86b27 Merge pull request diffblue#1687 from smowton/smowton/feature/class-hierarchy-dot fd2bf6a Merge pull request diffblue#1688 from smowton/smowton/feature/parameter_indices f570ce5 Merge pull request diffblue#1696 from smowton/smowton/fix/identical_struct_equality 61b0d6d Merge pull request diffblue#1666 from mgudemann/bugfix/removed_required_virtual_calls 3365054 Add regression test 2b6dc8b Resolve concrete function call if no implementation is found 3f1fd64 Add code_typet::get_parameter_indices 42cf61a Fix testing for empty line in test desc file 2090000 Fix missing newline at end of desc file e448d5f Fix unsatisfiable test line f7f033d String smoke tests: ensure no type mismatches are seen b627c3d Replace unsound struct-cast simplification 8fa42b3 Class hierarchy: add DOT output, unit tests 04f2faf Mark GOTO instructions with unresolved virtual calls aac181f Pass command line options via optionst b6fa3e8 Factorize source location initialization 8da5395 Document cover functions a7f0c3d Introduce cover instrumenter 873627a Split cover into several files 0fc08f3 Replace cover-function-only by cover-include-pattern 1f2102c Add code_typet::get_this 2801f0f Avoid crashing when --dependence-graph is used by correcting namespace scoping. acac776 Add a test for the same-named static functions crashing dependence graph in the goto-analyser 05f46a9 Fix the problem where two static functions with the same name would cause the dependency graph to fail. git-subtree-dir: cbmc git-subtree-split: d190fd8

romainbrenguier requested review from kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners December 13, 2017 11:23

tautschnig reviewed Dec 13, 2017

View reviewed changes

NathanJPhillips suggested changes Dec 13, 2017

View reviewed changes

romainbrenguier force-pushed the feature/type_cast branch from 9f9e1df to 1604523 Compare December 15, 2017 08:03

tautschnig approved these changes Dec 15, 2017

View reviewed changes

martin-cs reviewed Dec 15, 2017

View reviewed changes

romainbrenguier force-pushed the feature/type_cast branch from 1604523 to 9c49720 Compare December 15, 2017 14:26

NathanJPhillips approved these changes Dec 19, 2017

View reviewed changes

tautschnig requested changes Dec 19, 2017

View reviewed changes

peterschrammel reviewed Dec 19, 2017

View reviewed changes

romainbrenguier force-pushed the feature/type_cast branch from 9c49720 to 6c31272 Compare January 8, 2018 13:56

tautschnig reviewed Jan 8, 2018

View reviewed changes

romainbrenguier force-pushed the feature/type_cast branch from 6c31272 to 5460f04 Compare January 8, 2018 14:09

tautschnig approved these changes Jan 8, 2018

View reviewed changes

tautschnig assigned romainbrenguier Jan 8, 2018

romainbrenguier force-pushed the feature/type_cast branch from 5460f04 to ffc9a13 Compare January 8, 2018 14:59

romainbrenguier force-pushed the feature/type_cast branch from ffc9a13 to 482287d Compare January 9, 2018 11:04

romainbrenguier added 4 commits January 12, 2018 07:29

Define type_try_dynamic_cast and type_checked_cast

b72bacf

This is similar to expr_cast functions, with some code duplication. Allows to use type_try_dynamic_cast<> and type_checked_cast<> for typet objects in the same way we use expr_try_dynamic_cast<> and expr_checked_cast<> for exprt.

Add can_cast_type, validate_type for pointer_typet

35905c6

Validate data in pointer_typet in to_pointer_typet

c5fc351

Use type_checked_cast in boolbv_width

2064849

This performs the necessary checks to ensure the type is a well formed pointer type.

romainbrenguier force-pushed the feature/type_cast branch from 482287d to 2064849 Compare January 12, 2018 07:45

romainbrenguier merged commit 5bd5962 into diffblue:develop Jan 12, 2018

romainbrenguier deleted the feature/type_cast branch January 12, 2018 11:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

type_dynamic_cast (extension of expr_cast) #1667

type_dynamic_cast (extension of expr_cast) #1667

romainbrenguier commented Dec 13, 2017

smowton commented Dec 13, 2017

romainbrenguier commented Dec 13, 2017

smowton commented Dec 13, 2017

tautschnig Dec 13, 2017

romainbrenguier Dec 13, 2017

NathanJPhillips Dec 13, 2017

NathanJPhillips Dec 13, 2017

NathanJPhillips Dec 13, 2017

NathanJPhillips Dec 13, 2017

NathanJPhillips Dec 13, 2017

romainbrenguier commented Dec 15, 2017

tautschnig commented Dec 15, 2017

martin-cs left a comment

martin-cs Dec 15, 2017

tautschnig Jan 8, 2018

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

tautschnig left a comment

peterschrammel Dec 19, 2017

NathanJPhillips commented Dec 19, 2017

tautschnig commented Dec 19, 2017

romainbrenguier commented Jan 8, 2018

tautschnig left a comment

tautschnig Jan 8, 2018

tautschnig Jan 8, 2018

romainbrenguier commented Jan 8, 2018

tautschnig left a comment

tautschnig commented Jan 8, 2018

type_dynamic_cast (extension of expr_cast) #1667

type_dynamic_cast (extension of expr_cast) #1667

Conversation

romainbrenguier commented Dec 13, 2017

smowton commented Dec 13, 2017

romainbrenguier commented Dec 13, 2017

smowton commented Dec 13, 2017

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

Choose a reason for hiding this comment

romainbrenguier commented Dec 15, 2017

tautschnig commented Dec 15, 2017

martin-cs 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

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NathanJPhillips commented Dec 19, 2017

tautschnig commented Dec 19, 2017

romainbrenguier commented Jan 8, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

romainbrenguier commented Jan 8, 2018

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig commented Jan 8, 2018