Big-int: Fix copy-assign, add move ops, enable implicit conversions

[reuk]

The big-int class has a bunch of problems that are addressed by this PR:

• Unsafe copy assign which may leave objects in an inconsistent state: Big-int copy constructor unsafe #1340
• No move operations
• No cheap swap
• Arithmetic operations and comparisons only allow implicit conversions on the RHS, whereas they would be expected on both the LHS and RHS

[reuk]

In terms of formatting, I've tried to keep it internally consistent with the rest of the file. I'm not going to manually change the entire file just to keep the linter happy.

[tautschnig]

Please add "Fixes: #1340" to your commit message to avoid leaving it dangling.

[tautschnig]

Looks good to me (save for that one whitespace change as remarked) - waiting for CI to complete.

[tautschnig]

Unnecessary?

[reuk]

Fixed

[tautschnig]

Would you mind rebasing to force another Travis run? I can't seem to get it to work by clicking "Restart" in the Travis UI.

[reuk]

@LAJW Could you review too please?

[kroening]

This removes some of the operators that work on bigint and an llong; sure that the path through conversion isn't slower than the specialised version?

[tautschnig]

In line with the recent update: shouldn't those also be kept (and be implemented via swap)?

[reuk]

I don't think so. The best way to implement copy-assign safely is to set up another object with the desired state after assignment, and then to do a nothrow swap to exchange the states. That way, exceptions can only be thrown during the "setting up a new object" stage, which doesn't affect the logical state of the current object.

[reuk]

With this in mind, there's no benefit between having explicit overloads for assignment from primitive types, and allowing BigInts to be implicitly constructed during assignment. We'll end up allocating a fresh temporary object in both cases.

[reuk]

I believe this is ready for re-review now (I'll squash all commits once I get two approvals)

[LAJW]

Could these macros be implemented as template operator overloads with typename std::enable_if<std::is_integral<T>::value>::type?

[LAJW]

Again, this looks like a decent template candidate.

[reuk]

I attempted to provide nice templated operators, but getting the overload resolution right proved to be quite tricky. Given that the current version works, we'll leave it as-is for now, but I've sent @LAJW a copy of the WIP branch that he can fix up if he feels so inclined

[reuk]

Can this be merged now?

[tautschnig]

Can this be merged now?

From my point of view this looks ok, save for the necessary performance evaluation. I don't trust my (or in fact anyone else's) beliefs, we need data. A past summary profile from SV-COMP looked rather innocent, so I'd hope this does not change:

  %   cumulative   self              self     total
 time   seconds   seconds    calls   s/call   s/call  name
[...] (below is grep BigInt sum.profile | head -n10)
  0.03 159275.18    46.61 426710055     0.00     0.00  BigInt::as_string(char*, unsigned int, unsigned int) const
  0.01 161474.76    22.85 519850695     0.00     0.00  BigInt::compare(BigInt const&) const
  0.01 161583.75    21.23 6503690386     0.00     0.00  BigInt::~BigInt()
  0.01 161763.05    19.18 1621868144     0.00     0.00  BigInt::add(unsigned int const*, unsigned int, bool)
  0.01 162596.58    12.89 366825785     0.00     0.00  to_integer(constant_exprt const&, BigInt&)
  0.01 162659.12    12.22 2699062185     0.00     0.00  BigInt::BigInt(BigInt const&)
  0.01 162968.34    10.24 266398661     0.00     0.00  integer2binary(BigInt const&, unsigned long)
  0.01 162997.82     9.70 1411311148     0.00     0.00  BigInt::operator=(BigInt const&)
  0.00 163267.72     7.94 419146165     0.00     0.00  BigInt::assign(long long)
  0.00 163275.65     7.93                             BigInt::BigInt(unsigned long long)

[reuk]

Is there a wiki page on obtaining performance metrics anywhere? It's not clear how I would go about producing meaningful benchmarks at the moment. Indeed, I probably couldn't benchmark on my own machine because any work I do at the same time might skew the results.

I'd argue that the fix for copy assignment improves the correctness of the code, and should be merged regardless of the performance implications (no point getting fast results if they're wrong). Should I split that into a separate PR which can be merged faster?

[tautschnig]

Is there a wiki page on obtaining performance metrics anywhere? It's not clear how I would go about producing meaningful benchmarks at the moment. Indeed, I probably couldn't benchmark on my own machine because any work I do at the same time might skew the results.

There isn't any documentation I'm aware of. It's one of many tasks that I have had on my todo list for a long time already, and still I haven't been able to find sufficient time for doing it. The most important non-technical part is understanding what customer's input might look like, and thus build a benchmark suite that as closely as possible mimics the code base of potential customers. The technical bit is setting up infrastructure to enable reproducible measurements (though several tool kits already exist for doing so). My own current set up isn't completely ad hoc, but also not quite sufficiently agile.

I'd argue that the fix for copy assignment improves the correctness of the code, and should be merged regardless of the performance implications (no point getting fast results if they're wrong). Should I split that into a separate PR which can be merged faster?

I had thought about this last night - my understanding (which may be wrong!) is that the only broken case is when memory cannot be allocated. This, however, is a situation we currently cannot recover from anyway, and thus I don't see how a customer would be impacted by this bug. A negative performance hit, however, would impact customers.

We've had a similar conversation on more than one pull request already: what I struggle with is what I perceive as a throwing-over-the-fence approach. Personally I would expect anyone proposing patches to wholly own them, with all their implications (I emphasize that this is my personal view). Of course you might choose to take this ownership in some form of team to avoid everyone-doing-everything.

Results like https://sv-comp.sosy-lab.org/2017/results/results-verified/quantilePlot-FalsificationOverall.svg do not come about solely by impressive git commit stats, but do require analysis of implications of each change. It's not a coincidence that CBMC would still have won this category at a 1-second (instead of 900 seconds) time-out, but rather is the result of 15 years of work by @kroening and others. Also success in the world of program analysis is the product of correctness, performance, and features, and not one of them alone.

[reuk]

I understand your concerns. I don't have the time or expertise to produce a suitable benchmarking suite, therefore I'm closing this PR for now.

[tautschnig]

Adding to my to-do list.

[tautschnig]

I am attaching performance comparison results for this change and its base commit. There are no differences in the overall results (release build without profiling enabled), and the profile does not show a notable jump in any of the BigInt functions.

Assigning to @kroening for final review and approval.
comparison.zip