5 ms·
Imagine this pseudocode: void main() { check_goldbach(); // iterates over every integer > 2 // to see if it is an excepti
by anchpop 7y ago
Imagine this pseudocode:
void main() {
check_goldbach(); // iterates over every integer > 2
// to see if it is an exception to
// the goldbach conjecture, and
// returns if so
use_after_free();
}
This program may be memory safe. It's possible that there is no exception to the goldbach conjecture, so check_goldbach will never halt, so use_after_free will never be called. It also may not be memory safe. If the goldbach conjecture is not true, check_goldbach will eventually return and then we'll call use_after_free.
You say your compiler accepts all programs which are memory safe, and rejects all that aren't. If so, you can use it to prove or disprove the goldbach conjecture. Since proving or disproving that conjecture comes with a one million dollar prize, it is surprising that you can solve it with your method
edit: I didn't mean to disparage WatlerBright's work, I only was taking issue with the idea that any method of static analysis can accept 100% of correct programs and reject 100% incorrect programs. This is an unavoidable consequence of the halting problem and being aware of it allows you to decide where you want the tradeoff to be. it sounds like his implementation has no false negatives at the cost of a few false positives that are rare enough for them not to really be an issue, which is still really cool
- WalterBright 7y ago> You say your compiler accepts all programs which are memory safe, and rejects all that aren't. It does it by implementing O/B rules, which force changes in the way one writes code. This may sidestep the goldbach conjecture, which I don't understand.
- funglewest 7y ago> the goldbach conjecture, which I don't understand Clearly.
- dang 7y agoPlease stop making accounts to break the site guidelines with. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- jjnoakes 7y agoIt is possible that the compiler simply rejects any definition of a function that has a use after free, which would both uphold the compiler's claim and also not prove or disprove the goldbach conjecture.
- WalterBright 7y agoWhich it does, if such use is on any control flow path after the free(). For example, bool first = true; while (f()) { if (first) free(p); first = false; } is rejected as double-free.
- deleted 7y ago[deleted]
- bonzini 7y agoWhat about while (f()) { free(p); p = NULL; }
- WalterBright 7y agoIt'll compile because although free(p) consumes p and p is undefined immediately afterwards, p then becomes defined again via the assignment and so the while loop always enters with a defined value for p.
- anchpop 7y agoIf that is the case then his approach has false negatives, because a function that is never called cannot introduce memory unsafety but would incorrectly be flagged as unsafe
- WalterBright 7y ago> incorrectly be flagged as unsafe It depends on what that means. For example, one can write perfectly correct code in a block of code marked "unsafe", it's just that the compiler cannot check it. In D, these are marked with the @system attribute. We actually had a discussion about what to call such unsafe blocks. Other languages call them "unsafe", but I didn't care for that as it implied the blocks were actually broken. Hence we call such code "system" code. There aren't false negatives by the design of the rules. This is different from what linters do, as linters issue warnings for code that is acceptable by the language rules.
- bjoli 7y agohaving your static analyser solving million dollar problems seems like an unnecessary high bar. how is your comment, under any reasonable interpretation of what Walter wrote, not pointless pedantry?
- anchpop 7y agoWhat Walter meant in his comment was that his static analyzer has no false positives (it never allows a memory unsafe program to compile). He's provided a few simpler examples in this thread of cases where his analyzer produces false negatives. I knew that was going to be the case because no program can flag 100% of negatives without also flagging a few positives by accident (as a consequence of Rice's theorem). I just meant to demonstrate that, but I don't know anything about D so I wanted to pick something that I was certain his analyzer would fail one way or the other. That doesn't mean that his analyzer isn't useful. I find rust extremely useful because it catches almost me whenever I accidentally write memory unsafe code without burdening me too much otherwise. But almost every rust coder has run into a case where they wrote some code that was safe, but not allowed. That's just a fact of life and it serves no one to make incorrect claims about one's software
- WalterBright 7y agohttps://news.ycombinator.com/item?id=22714673 https://news.ycombinator.com/item?id=22714673
- exiled13 7y ago> I don't know anything about D so I wanted to pick something that I was certain his analyzer would fail one way or the other. What he is talking about is a proposed implementation of the solution. It isn't actually in the D language yet. No one's tested it (except for Walter). So I would definitely take its' validity with a grain of salt.
- WalterBright 7y ago> It isn't actually in the D language yet. It is in the released compiler as a preview feature.