Add code_typet::get_parameter_indices

[smowton]

This is simply the opposite of the existing get_parameter_indentifiers, useful for mapping from parameter identifier to its argument or parameter index.

Another simple utility that the sec product currently has but is generally handy.

[tautschnig]

I have restarted the failing Travis jobs.

[tautschnig]

The current code will work for Java (I think), but not necessarily for C. Thus any user (beyond the provided unit-test) needs to be revisited in addition to the proposed implementation.

[tautschnig]

Parameters need not have an identifier, in which case the results will at best cause confusion. Thus parameter_identifiers exists in goto_function_templatet.

[smowton]

@tautschnig have amended this to check for empty identifiers as suggested.

[tautschnig]

I still have a design problem here: we have parameter_identifiers in goto_function_templatet, but now introduce a different way of seemingly obtaining the same. The one in goto_function_templatet will always work, while this new one will sometimes work. Can we please only have one of these?

[smowton]

That appears to clash with the function I'm not adding. code_typet::parameter_identifiers() already exists, and I suppose that goto_functiont::parameter_identifiers and goto_functiont::type.parameter_identifiers() should always produce the same information. However I note that in-tree, there do not appear to be any users of either parameter_identifiers version, and nobody seems to initialise the goto-function version.

[smowton]

Please disregard the weird "infinite wisdom" stuff, was being trolled by @owen-jones-diffblue (or possibly @forejtv?) while my screen was left unlocked ;)

I confused two different mappings.

[tautschnig]

My apologies for the confusion! I have created #1695 to eventually do some cleanup.

[tautschnig]

You might use p here.

[tautschnig]

Use index here. (Related to the second half of my suggestion below.)

[tautschnig]

Just do ++index; at the end of the loop body.

[tautschnig]

I'm afraid this might not work as nicely as intended: hash values of dstringt (which irep_idt by default is) aren't uniformly distributed across 2^32 or 2^64. Given that the number of parameters is typically fairly small, chances are that all your elements end up in one bucket despite all the effort.

If you have some time to spare, it would be really interesting if you could do some debug runs where you log the distribution across buckets that you get to see in this bit of code (at the end of the function).

[smowton]

I haven't run the test, but I note that the hash value of dstringt is just its number, and the std::hash specialisations shipped with libstdc++ for all primitive types of size <= sizeof(size_t) simply cast to size_t. The authors of the standard library will surely have anticipated std::unordered_map keyed by densely packed integers, so dstring seems likely to perform just as well.

[smowton]

The specific relevant excerpt from bits/functional_hash.h:

#define _Cxx_hashtable_define_trivial_hash(_Tp)         \
  template<>                                            \
    struct hash<_Tp> : public __hash_base<size_t, _Tp>  \
    {                                                   \
      size_t                                            \
      operator()(_Tp __val) const noexcept              \
      { return static_cast<size_t>(__val); }            \
    };

  ...

  _Cxx_hashtable_define_trivial_hash(long)

[tautschnig]

The authors of the standard library will surely have anticipated std::unordered_map keyed by densely packed integers, so dstring seems likely to perform just as well.

I'd love to believe this, had I not done the painful experiments behind the write-up at

cbmc/src/util/irep_hash.h

Line 95 in fabc99e

// This is because Visual Studio's STL masks away anything

So maybe you are right, maybe you aren't. The only thing I'd truly trust is data across different platforms.

Note that all this isn't a big deal here for we are likely not dealing with big data sets and probably aren't on a hot path. Just saying this as data must prevail over instincts.

[smowton]

That looks like the opposite problem to me -- lots of the irep's hash is in high bits, which get ignored when picking a bucket, whereas for dense integers there's lots of useful information in low bits. I believe https://tessil.github.io/2016/08/29/benchmark-hopscotch-map.html for example is testing this exact case with unordered_map, though tests with libc++ and MSVC's STL implementation would be good to see too.

[tautschnig]

Just to be very clear: this is a purely academic discussion here, given the anticipated small data and rare use.

I do agree that you've got the opposite case, but that would just imply that you observe the opposite performance penalty between GNU STL vs. MSVC. The comparison you pointed to is a good read, but is of course on completely artificial data. It is important to contrast this with the profile of actual data to be observed at the point of use. In your specific case, I'd expect many uses might have just 2 or 3 buckets. The parameter identifiers will likely have been created in immediate succession. Thus, for the 2-parameter case we'd have an even and an odd number, and you'll be doing great with MSVC. But really you'll not even be able to observe a difference over using a map that does not use hashing, or using whatever the worst performing hash map for the given hash function.

My view is: keep things simple where possible, else optimise as far as possible and back that up by data.

[smowton]

@tautschnig hash function is fine I think; other changes implemented

[tautschnig]

Approving as the remaining discussion item isn't a blocker for this piece of code.