Implementation of expr_dynamic_cast

[NathanJPhillips]

expr_dynamic_cast is proposed as a replacement for the family of to_*_expr functions such as to_symbol_expr. Its use can be adopted over time and this PR simply introduces the mechanism, implementations for each exprt derived type in std_expr.h and unit tests.
The primary advantage of expr_dynamic_cast is that it reduces from three to one the number of things you need to remember to ensure consistency, all you need now is the name of the type to which you are casting.
Previously code has looked like this:

void f(exprt *expr)
{
  if(expr.id() == ID_symbol)
  {
    symbol_exprt *symbol=to_symbol_expr(expr);
    use_symbol(symbol);
  }
}

Now code could look like this:

void f(exprt *expr)
{
  symbol_exprt *symbol=expr_dynamic_cast<symbol_exprt *>(expr);
  if(symbol!=nullptr)
  {
    use_symbol(symbol);
  }
}

Instead of having to get the right ID and to_*_expr function you simply call expr_dynamic_cast with the type you wish to convert to and template specialization checks the ID for you.
Additionally this code allows for conversion of const or non-const pointers and references.
Consistently with the STL, conversion of an invalid reference throws std::bad_cast, while conversion of an invalid pointer returns nullptr.

[kroening]

We want to get rid of all pointers, and thus I am no fan of the new idiom.

[NathanJPhillips]

@kroening, that's a fair point. This code does also allow for the following mode of operation:

void f(exprt &expr)
{
  if(check_expr_type<symbol_exprt>(expr))
  {
    symbol_exprt &symbol=expr_dynamic_cast<symbol_exprt &>(expr);
    use_symbol(symbol);
  }
}

This has the same advantages mentioned above and might be a better way of using it.

[peterschrammel]

use ///

[peterschrammel]

Move comment header with author here (look at other files)

[peterschrammel]

// CPROVER_UTIL_EXPR_CAST_H

[peterschrammel]

Why is this commented out?

[peterschrammel]

remove spaces around =

[peterschrammel]

put message on separate line

[peterschrammel]

I'd provide only ref and const ref versions.

[reuk]

These metafunctions can be found in <type_traits>

[NathanJPhillips]

Are you sure? I thought those versions only removed the const/ref if it's there, returning the basic type otherwise, which would cause the template to be resolved in unwanted situations.

[reuk]

I think plain function overloading would be better than specialization. Also, I'd consider combining check_expr_type and validate_expr seeing as their roles are so similar. If we just used validate_expr, we could ignore template specialization completely, and simply provide overloads for all the different types we want to support.

[marek-trtik]

Original Nathan's examples can be shortened into typical use of down-casting:

void f(exprt *expr)
{
  if(auto *symbol=expr_dynamic_cast<symbol_exprt *>(expr))
    use_symbol(symbol);
}

void f(exprt &expr)
{
  if(auto *symbol=expr_dynamic_cast<symbol_exprt *>(&expr))
    use_symbol(*symbol);
}

In the second case (i.e. void f(exprt &expr)) the expression expr_dynamic_cast<symbol_exprt *>(expr) should throw, if expr is not of symbol_exprt. That is why &expr is used (to prevent throwing).

[marek-trtik]

Besides expr_dynamic_cast I'd also like to have type_dynamic_cast so that I could do down-casting in typet hierarchy.

[NathanJPhillips]

I think all the requested changes are now implemented. @peterschrammel @reuk

[smowton]

Mostly looks good, one other point: the current to_* functions raise an invariant rather than throw std::bad_cast. We should probably keep doing that at least for now -- with the std::bad_cast solution at the moment we would catch it at top level and thus lose the backtrace.

[smowton]

Think of a synonym for type (class? kind? Simply check_expr_cast?) since the current name suggests we're talking about the unrelated base.type().

[thk123]

I like kind fwiw

[smowton]

Document TExpr

[smowton]

assert that TExpr is (const?) exprt (*?)?

[smowton]

camelCase -> under_scores

[smowton]

Delete or uncomment (other commented validate operations too)

[NathanJPhillips]

As discussed, these match the commented code above.

[NathanJPhillips]

@smowton - are you saying that we currently do not support the use of exceptions in the CBMC code-base? That's amazing!

[NathanJPhillips]

@smowton All your comments addressed.

[smowton]

@NathanJPhillips the docs still say \throw std::bad_cast. Otherwise LGTM.

[smowton]

(Exceptions will work, they just won't result in as thorough a trace dump as an invariant failure)

[smowton]

I'd like to try to get this in, since I think it improves on the existing if(e.id()==ID_something) { const auto &derived=to_derived_type(e) } both by avoiding repeated id() checks (in the if-test and in the cast op) and by ensuring the two are consistent, and allowing more thorough validation (e.g. that the operands are correct).

@kroening @peterschrammel if we used the new nonstd::optional would that address your concerns? The cast would return optional<std::reference_wrapper<target_type>>, which supports an operator-> to get the target expr. Example usage:

if(auto symbol_expr=dynamic_cast_expr<symbol_exprt>(expr))
{
  irep_idt identifier=symbol_expr->get_identifier();
}

As you can see the syntax is pointer-like, but optional<reference_wrapper<T>> guards the pointer such that its referee can't be changed.

[smowton]

@peterschrammel @kroening changed from pointer to optional style, please re-review

@NathanJPhillips please check I haven't vandalised your code too badly

[peterschrammel]

use invariant.h?

[reuk]

This is a compile-time assertion.

[peterschrammel]

They will be made throw exceptions soon.

[peterschrammel]

Remove rather than commenting out.

[smowton]

This is intended to mirror the commented-out validation for the same expressions in the classic to_*_expr functions. I presume those are intended to be brought back in eventually but sometimes in the product we still encounter and_exprt with a single or zero operands (logically sound but undesirable)

[peterschrammel]

remove (several instances)

[smowton]

@peterschrammel I think I have nothing to do here, happy that your comments are addressed?