Skip to content

[CPP-434] Detect signed overflow checks#2075

Merged
jbj merged 33 commits intogithub:masterfrom
zlaski-semmle:zlaski/cpp434
Nov 9, 2019
Merged

[CPP-434] Detect signed overflow checks#2075
jbj merged 33 commits intogithub:masterfrom
zlaski-semmle:zlaski/cpp434

Conversation

@zlaski-semmle
Copy link
Contributor

No description provided.

@zlaski-semmle zlaski-semmle requested review from a team and semmledocs-ac as code owners October 2, 2019 19:30
@rdmarsh2
Copy link
Contributor

rdmarsh2 commented Oct 2, 2019

I think this overlaps with cpp/bad-addition-overflow-check when the check is done on two small signed integers. Should it be a modification to that query to look for signed types as well as small types?

@zlaski-semmle
Copy link
Contributor Author

Ran the query against a larger (66) suite of projects, and there are too many false positives for it to be usable.

@zlaski-semmle
Copy link
Contributor Author

I think this overlaps with cpp/bad-addition-overflow-check when the check is done on two small signed integers. Should it be a modification to that query to look for signed types as well as small types?

Here is what @jbj wrote in the Jira ticket:
cpp/bad-addition-overflow-check also flags expressions that look like x + y < x, but it's looking for a very different problem. It applies to both signed and unsigned types but only to types smaller than int.

@jbj
Copy link
Contributor

jbj commented Oct 3, 2019

I think @rdmarsh2 is right. These queries will have to be merged before we can put them in production, but during initial development it's probably easier to keep them separate.

@zlaski-semmle Are there false positives because the query isn't good enough yet or because it turns out there are cases where it's defined behaviour to check x + y < x for signed addition and positive y?

@zlaski-semmle
Copy link
Contributor Author

@zlaski-semmle Are there false positives because the query isn't good enough yet or because it turns out there are cases where it's defined behaviour to check x + y < x for signed addition and positive y?
The former. But I've improved the query since.

@jbj jbj added the C++ label Oct 3, 2019
Copy link
Contributor

@hubwriter hubwriter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Documentation reviewed

<qhelp>
<overview>
<p>
Testing for <code>signed</code> integer overflow by adding a
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Testing for <code>signed</code> integer overflow by adding a
Testing for a <code>signed</code> integer overflow by adding a

Copy link
Contributor Author

@zlaski-semmle zlaski-semmle Oct 8, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm... Adding a feels unnatural to me. We may very well find multiple occurrences of these overflows, so neither a nor the seem sensible.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm with @zlaski-semmle on that one. In this context, overflow behaves grammatically like death or malice.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fair enough. You guys are closer to the audience than me.

<overview>
<p>
Testing for <code>signed</code> integer overflow by adding a
value to a variable and then comparing the result to said variable
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
value to a variable and then comparing the result to said variable
value to a variable and then comparing the result to that variable

This use of "said" seems overly formal for query help

<sample src="SignedOverflowCheck-bad.cpp" />
<p>
In the next example, a value of type <code>signed int</code> is
getting added to a value ot type <code>unsigned int</code>. Because
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
getting added to a value ot type <code>unsigned int</code>. Because
added to a value of type <code>unsigned int</code>. Because

Delete "getting". Fix typo.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

<sample src="SignedOverflowCheck-good.cpp" />
</example>
<references>
<li><a href="http://c-faq.com/expr/preservingrules.html">Preserving Rules</a></li>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe better to use the title that's on this page:
comp.lang.c FAQ list · Question 3.19 (Preserving rules)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good idea.

</example>
<references>
<li><a href="http://c-faq.com/expr/preservingrules.html">Preserving Rules</a></li>
<li><a href="https://www.securecoding.cert.org/confluence/plugins/servlet/mobile#content/view/20086942">Understand integer conversion rules</a></li>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a good reference to use? It requires a logon.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Admittedly, I just copied the references from another query; thank you for catching this.

@@ -0,0 +1,30 @@
/**
* @name Undefined result of signed test for overflow
* @description Testing for oveflow by adding a value to a variable
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
* @description Testing for oveflow by adding a value to a variable
* @description Testing for overflow by adding a value to a variable

@geoffw0
Copy link
Contributor

geoffw0 commented Oct 10, 2019

Looking at the results on 78 projects they look pretty good to me now. This was an interesting case:

if ((int)(ioff + c.length) < (int)ioff) return 0;

because the addition is done on unsigned integers (so is OK), before converting to signed for the comparison (so it's the conversion that may produce undefined behaviour).

Part of me also wants a sister query that flags testing for signed overflow without a comment explaining what's going on. :)

add.getAnOperand() = va1 and
ro.getAnOperand() = va2 and
globalValueNumber(va1) = globalValueNumber(va2) and
add.getFullyConverted().getType().getUnspecifiedType().(IntegralType).isSigned() and
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think we want getFullyConverted here in the signedness check. We want to check whether the addition is signed, not whether the result is converted to signed. That might fix the FP that Geoffrey mentioned today.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that did the trick. Also needed to check that the other side of the comparison was also signed (and not cast to an unsigned type).

@jbj
Copy link
Contributor

jbj commented Oct 10, 2019

because the addition is done on unsigned integers (so is OK), before converting to signed for the comparison (so it's the conversion that may produce undefined behaviour).

@geoffw0, I think conversion from unsigned to signed is well defined even when the value doesn't fit. From https://en.cppreference.com/w/cpp/language/implicit_conversion:

If the destination type is signed, the value does not change if the source integer can be represented in the destination type. Otherwise the result is [implementation-defined (until C++20)] [the unique value of the destination type equal to the source value modulo 2^n
where n is the number of bits used to represent the destination type. (since C++20)]. (Note that this is different from signed integer arithmetic overflow, which is undefined).

So it's implementation-defined what happens, and I'm guessing that all implementations define that they translate the bit representation into two's complement.

#define AV_INPUT_BUFFER_PADDING_SIZE 64

int overflow12(int codecdata_length) {
if(codecdata_length + AV_INPUT_BUFFER_PADDING_SIZE <= (unsigned)codecdata_length) { // GOOD
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see why this should be GOOD. If codecdata_length is INT_MAX (0x7fffffff), then the + will do a signed overflow, which is undefined behaviour. Assuming that doesn't make the program explode, I think it's likely that the signed addition overflows to the bit pattern 0x8000003f. When converted back to unsigned (implicitly, to match the RHS of <=), that's not smaller than (unsigned)0x7fffffff, so overflow12 returns 1 as if there was no overflow.

I can observe both of these problems with the following test:

#define AV_INPUT_BUFFER_PADDING_SIZE 64

int overflow12(int codecdata_length) {
	if(codecdata_length + AV_INPUT_BUFFER_PADDING_SIZE <= (unsigned)codecdata_length) { // GOOD
	  return -1;
	}
	return 1;
}

int main(int argc, char **argv) {
  int k = 0x7fffffff;
  if (overflow12(k) == -1)
    return 1;
  return 0;
}

Compile with on Clang with UBSan (the undefined-behaviour sanitizer) turned on:

$ clang++ -fsanitize=undefined test.cc
$ ./a.out
test.cc:4:22: runtime error: signed integer overflow: 2147483647 + 64 cannot be represented in type 'int'
$ echo $?
0

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree with your analysis, though I wonder why neither gcc nor clang delete the comparison expression (which convinced me that the expression was GOOD). Either they consider the semantics to be defined, or perhaps they missed an optimization opportunity.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've analyzed the codegen for both gcc and clang; the code generated by gcc is straightforward, but clang is a tad clever:

return (n + 32 <= (unsigned)n? -1: 1);

gcc 9.2:

overflow12(int):
 lea 0x20(%rdi),%eax            ; eax = rdi + 32 = n + 32  
 cmp %eax,%edi                  ; n vs. (n + 32)
 sbb %eax,%eax                  ; if n < n + 32, eax = -1, otherwise eax = 0
 and $0x2,%eax                  ; if n < n + 32, eax = 2, otherwise eax = 0
 sub $0x1,%eax                  ; if n < n + 32, eax = 1, otherwise eax = -1
 retq 

clang 9.0.0:

overflow12(int):
 xor %eax,%eax                  ; eax = 0
 cmp $0xffffffe0,%edi           ; n vs. -32
 setb %al                       ; if n < -32, eax = 1, otherwise eax = 0
 lea (%rax,%rax,1),%eax         ; if n < -32, eax = 2, otherwise eax = 0
 add $0xffffffff,%eax           ; if n < -32, eax = 1, otherwise eax = -1
 retq  

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So I guess, the philosophical question remains: Since both mainstream compilers appear to treat the expression as semantically valid, should we be warning users against it? (I do agree with @jbj 's analysis, though.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For the time being, I've incorporated @jbj's suggestions into my last commit/push. We can still discuss whether comparisons not deleted by compilers should receive their own warnings or not (they currently will).

As I wrote in the Jira ticket, It is my opinion that the present query (cpp/signed-overflow-check) subsumes cpp/bad-addition-overflow-check and that the latter could be safely deleted.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The cpp/bad-addition-overflow-check query has only one test case:

$ cat BadAdditionOverflowCheck.expected
| test.cpp:3:11:3:19 | ... < ... | Bad overflow check. |

With our cpp/signed-overflow-check query, we catch the same problem, plus several others:

$ cat SignedOverflowCheck.actual
| SignedOverflowCheck.cpp:8:12:8:22 | ... < ... | Testing for signed overflow may produce undefined results. |
| SignedOverflowCheck.cpp:18:12:18:26 | ... < ... | Testing for signed overflow may produce undefined results. |
| SignedOverflowCheck.cpp:35:9:35:23 | ... < ... | Testing for signed overflow may produce undefined results. |
| SignedOverflowCheck.cpp:99:10:99:30 | ... <= ... | Testing for signed overflow may produce undefined results. |
| test.cpp:3:11:3:19 | ... < ... | Testing for signed overflow may produce undefined results. |

So I would argue that cpp/signed-overflow-check does subsume cpp/bad-addition-overflow-check, though I'm always open to test cases showing otherwise.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If both operands of the addition have small unsigned integer types, then there won't be any undefined behavior, but it will be impossible for the addition to overflow. I think that's going to merit a separate qhelp, since both the fix and the explanation of the behavior will differ

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm suggesting that you actually merge the two test directories and push it to this PR, regardless of whether we choose to merge the queries.

I agree with @rdmarsh2, which means that signed-overflow-check should ideally be adjusted so it doesn't repeat any of the results from bad-addition-overflow-check since the qhelp won't be appropriate for those. You'll want to add some test cases that are on the border, like (int)(unsigned short)x + 2 < (int)(unsigned short)x.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of adjusting signed-overflow-check (which may introduce false positives/negatives along the way), I think it would be appropriate to simply delete bad-addition-overflow-check. The .qhelp for signed-overflow-check may need adjusting.

I can certainly migrate the signed-overflow-check test bits over to the bad-addition-overflow-check directory (as several other queries live there already). I'll also add your test case.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've turned @jbj 's test case into a function:

bool multipleCasts(char x) {
    // clang 9.0.0 -O2: deleted
    // gcc 9.2 -O2: deleted
    // msvc 19.22 /O2: deleted
    return (int)(unsigned short)x + 2 < (int)(unsigned short)x;
}

As you can see, all three compilers delete the relational expression in the function, replacing it with

xor %eax,%eax
retq 

So the fact that the parameter started its life as a smaller type does not matter;.

hubwriter
hubwriter previously approved these changes Oct 14, 2019
@zlaski-semmle
Copy link
Contributor Author

I cooked up another test case:

bool multipleCasts2(char x) {
    // clang 9.0.0 -O2: not deleted
    // gcc 9.2 -O2: not deleted
    // msvc 19.22 /O2: not deleted
    return (int)(unsigned short)(x + '1') < (int)(unsigned short)x; // GOOD [FALSE POSITIVE]
}

This one is not deleted by any compiler -- I'm guessing because there is only one top-level expression on the left side, and so we have a plain comparison instead of an overflow check. Since our AST implementation strips away casts, QL only sees x + '1' < x, hence the alert. But given that this example is rather contrived, I wouldn't worry about it.

ro.getAnOperand() = expr2 and
globalValueNumber(expr1) = globalValueNumber(expr2) and
add.getUnspecifiedType().(IntegralType).isSigned() and
exprMightOverflowPositively(add)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this query have lots of false positives from code like this:

bool cannotHoldAnotherInt(int n1, int delta) {
    return n1 + delta < n1; // GOOD (delta could be negative)
}

We could add a check here that delta is non-negative according to the range analysis. On the other hand, why would someone write n1 + delta < n1 instead of delta < 0?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, Clang transforms the former into the latter: https://godbolt.org/z/FvTwxs

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll re-run the query in the LGTM query console, but I haven't seen any cases with a negative delta.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

https://lgtm.com/query/4231059764463143298/

Note that if delta is negative and sufficiently small, we may have to contend with negative overflow. Perhaps we can use exprMightOverflowNegatively() as well?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for sharing the query console link. I don't see any results that would benefit from a check that delta is non-negative. Do you?

I do see some dubious results that the query will need to exclude. An easy starting point would be to filter out results that come from macro expansions.

I agree that in principle we should add exprMightOverflowNegatively. Do you then want to tie the overflow direction to the direction of the comparison operator?

Copy link
Contributor

@zlaski zlaski Oct 31, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for sharing the query console link. I don't see any results that would benefit from a check that delta is non-negative. Do you?

No, I do not either.

I do see some dubious results that the query will need to exclude. An easy starting point would be to filter out results that come from macro expansions.

I agree. I've analyzed the results a bit more closely, and seems that the query always flags the problem correctly. But the layer of obfuscation created by a macro renders our query rather useless.

I agree that in principle we should add exprMightOverflowNegatively. Do you then want to tie the overflow direction to the direction of the comparison operator?

I don't think we should involve the direction of operators, since they're always two sides of the same coin, i.e., one can use < to test for overflow or >= to test for absence of overflow.

But another question comes to mind: should we handle subtraction/underflow? The use of exprMightOverflowNegatively would make sense in that context. But I'll add exprMightOverflowNegatively to the current query to see if it uncovers any more problems.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Re-ran the 73 project suite with exprMightOverflowPositively or exprMightOverflowNegatively and did not unearth anything further.

<p>
When checking for overflow by adding two values, first make sure that <code>a</code>
or <code>b</code> are (converted into) unsigned values, unless it is
certain that the signed addition cannot overflow.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My point about recommendations is that it's not good enough to give examples of some overflow checks that are bad and some overflow checks that are good. The "Recommendation" section of the qhelp is there to help the developer fix the problem in the code they have, as locally as possible. Each of the "bad" examples must be accompanied by a "good" example that performs the same function as what the developer intended. In practical terms, we must suggest a replacement that performs the same function when compiled with gcc -fwrapv (compiled with overflow-related optimisations disabled).

In particular, just casting the variables to unsigned is not a fix because it changes the overflow check so it's now doing something else. For int a, the expression a + 1 < a is intended to be false when a == 0x7fffffff and true otherwise. We can't recommend changing that to (unsigned)a + 1 < a since that's instead false when a == 0xffffffff and true otherwise.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My point about recommendations is that it's not good enough to give examples of some overflow checks that are bad and some overflow checks that are good.

Why not? What kind of assumptions are we making about the competence of the developer?

In particular, just casting the variables to unsigned is not a fix because it changes the overflow check so it's now doing something else. For int a, the expression a + 1 < a is intended to be false when a == 0x7fffffff and true otherwise. We can't recommend changing that to (unsigned)a + 1 < a since that's instead false when a == 0xffffffff and true otherwise.

The example is contrived as it involves a constant addend, but even then it can be used to illustrate my point. Given s + 1 < s using signed arithmetic, how would one express it using unsigned values? Assuming that the developer "reasonably" expects that s + 1 will never be undefined, the answer seems to be u !== 0x7fffffff. What if we instead have s + 10 < s? We then would have u < 0x7ffffff6 || u > 0x7fffffff. Is this the recommendation we should offer developers? For an arbitrary s + d < s, we would have something like u < INT_MAX - d + 1 || u > 0x7fffffff.

So I guess my point here is that, in the general case, there does not exist a clean signed-to-unsigned transformation that preserves the semantics of the former. When we tell the developer that their expression has undefined behavior, we are therefore asking them to rethink their design. For example, s + 10 < s could be rewritten as s >= INT_MAX - 9 (or, more likely, s + 10 > s would become s < INT_MAX - 9).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You've pretty much written the advice we should give: tell the developer to replace s + 10 < s with s > INT_MAX - 10. That seems clean and simple to me. It's also what @geoffw0 suggested in the Slack link I put in my earlier review. Notice that there is no unsigned arithmetic going on here at all -- only signed but well-defined arithmetic.

Cases for non-constant deltas will be more difficult. I googled it and found http://www.cs.utah.edu/~regehr/papers/overflow12.pdf, which would be an excellent addition to the qhelp references. It spells out how to check for signed int addition overflow in III.B.1. Instead of applying that advice, I'd encourage developers to redesign their data types to be unsigned; the problem is just that changing a declaration from signed to unsigned may not be possible without breaking an API.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the paper reference; I'll be sure to include it in Qhelp.

I'm thinking about the Recommendation section, and perhaps the best way of constructing it is to include a table mapping out possible transformations. What do you think? It seems that we have gotten bogged down in "i before e except after c" discussions, and a table would greatly simplify things.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A table sounds good. If the qhelp file format doesn't actually have support for table mark-up, then at least a bullet list might work.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tables seem to work

@zlaski
Copy link
Contributor

zlaski commented Nov 1, 2019

I've just pushed out another rewrite of Qhelp. Please review content, but also FORMATTING. I'm especially concerned about the table of constructs in the Recommendation section. The MD result renders fine in my Chrome browser with a mark-down plug-in. I'm attaching my MD generation script as well.
qhelp_to_md.txt

@jbj
Copy link
Contributor

jbj commented Nov 1, 2019

Here are the errors from QHelp-Preview: https://gist.github.com/jbj/3cc7d8909268195858b5d29f76c05a3d

Copy link
Contributor

@jbj jbj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The new qhelp LGTM, although I haven't seen it rendered yet.

What's next? You're still investigating how to suppress the unhelpful results we saw in the query console run, right?

@zlaski
Copy link
Contributor

zlaski commented Nov 1, 2019

What's next? You're still investigating how to suppress the unhelpful results we saw in the query console run, right?

Yes, once I get done with the documentation formatting, I'll tackle the exclusion of macro invocations from alerts.

@zlaski
Copy link
Contributor

zlaski commented Nov 1, 2019

Latest results at https://lgtm.com/query/6923897885970565767/. We did manage to squelch alerts for macro invocations.

@zlaski
Copy link
Contributor

zlaski commented Nov 2, 2019

So my check-in died in Qhelp preview again, but I cannot see what's wrong since I don't have access to Jenkins.

@jbj
Copy link
Contributor

jbj commented Nov 6, 2019

I added a commit to insert <p> tags in the qhelp.

@jbj
Copy link
Contributor

jbj commented Nov 7, 2019

The qhelp LGTM.

I ran a test where I added

  ... and
  forall(Compilation c |
    c.getAFileCompiled() = ro.getFile()
  |
    not c.getAnArgument() = "-fwrapv" and
    not c.getAnArgument() = "-fno-strict-overflow"
  )

to suppress the results on Linux and CoreCLR. Here are the remaining results: https://lgtm.com/query/4587217464269309481/. What do you say to incorporating that forall into the query? I haven't tested for performance.

I'm still not sure what to think about the x + 1 >= 1 tests that also show up among the results. They don't seem to be dangerous but are just convoluted ways of writing x >= 0, and so I'm not sure they belong in the results of a security query. What do you think? They could be suppressed by requiring that expr2 is not a constant.

@zlaski
Copy link
Contributor

zlaski commented Nov 7, 2019

I added a commit to insert <p> tags in the qhelp.

Thank you for doing this. For some reason, the Qhelp rendered correctly when using my local QHelp-to-MD script.

@zlaski
Copy link
Contributor

zlaski commented Nov 7, 2019

I'm currently running timing tests (-fwrapv / -fno-strict-overflow vs. without). I'm on the fence as to whether alerts should be produced even in the presence of these command-line parameters. My only concern, really, is that the build system may get inadvertently changed at some point. Aside from that, though, I'm OK for incorporating the conjunct you provided.

@zlaski
Copy link
Contributor

zlaski commented Nov 7, 2019

So I've run the tests, and judging by wall-clock, cold-cache running time, I don't actually see any performance degradation as a result of adding the -fwrapv / -fno-strict-overflow checks. Of course, the margin of error is quite large here, but I think it's safe to say that performance is not something we should worry about.

@jbj I'm thinking that the forall in your conjunct should perhaps be replaced by exists? I'll try an LGTM run with that change.

@zlaski
Copy link
Contributor

zlaski commented Nov 7, 2019

I'm still not sure what to think about the x + 1 >= 1 tests that also show up among the results.

Actually, I don't see such results. Where did you see them? The closest I found is i-binwidth*k+1 >= 1 in igraph/igraph - perhaps that's what you meant? But I'd guess that, by writing x + 1 >= 1, the developer is testing for overflow, which the much simpler x >= 0 would not accomplish. In fact, I believe the correct recommendation here would be x < MAX_INT.

          with `-fwrapv` or `-fno-strict-overflow`
@jbj
Copy link
Contributor

jbj commented Nov 8, 2019

I'm thinking that the forall in your conjunct should perhaps be replaced by exists?

Good catch. I did indeed have this the wrong way around.

@jbj
Copy link
Contributor

jbj commented Nov 9, 2019

I think this is good to merge now. Thank you for your patience with my many rounds of reviewing. We can decide about the x + 1 >= 1 results when we see some more of them in the wild.

@jbj jbj merged commit f3e691b into github:master Nov 9, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

6 participants