5 ms·

> This is why, for D, I was determined to use DFA to catch 100% of the positives with 0% negatives. I knew this could be done because my compilers were using DF

> This is why, for D, I was determined to use DFA to catch 100% of the positives with 0% negatives. I knew this could be done because my compilers were using DFA in the optimization pass. Is this really true? I thought this was impossible due to Rice's theorem

WalterBright 7y ago
Fortunately, I am unaware that it was impossible and did it anyway :-) But it is possible I made a mistake. It is also true that for it to work, one has to change the way one writes code, like Rust does. This is why D requires and @live attribute be added to functions to enable the checking for just those functions, so it doesn't break every program out there. It will enable incremental use of the checking at the user's option.
- nullc 7y ago
  You're probably using a different definition of 100% than any impossibility proof would use. Consider some code: --- a=malloc(1); needfree=true; if (hashfn(first_factor(huge_static_rsanum1))&1){needfree=false;free(a);} if (hashfn(first_factor(huge_static_rsanum2))&1){needfree=false;free(a);} if(needfree)free(a); --- The decision if this has a double free or not depends on the factorizations of two huge difficult to factor constants. It either double-frees or not depending on those constants. Surely your software cannot decide that... What you probably mean is something like "100% on real programs rather than contrived cases". Of course, in that case, your definition of 'real programs' is the catch. :P Sometimes things that seem like they should always work except on contrived junk like the above example actually run into limitations in practice because macros and machine code generation produce ... well ... contrived junk from time to time.
  - jjnoakes 7y ago
    I personally would want code like this flagged by static analysis. I would fix the code by not calling free in the second 'if' body if needfree was already false (just like the call at the end of the function is guarded).
    - nullc 7y ago
      You might want it flagged-- I would--, but it would still be a false positive if it did so (assuming the constants didn't result in a double-free). :)
      - kccqzy 7y ago
        I think the argument is that static analyzers don't have to work on completely unchanged code, but rather rely on humans to structure the code in a way to avoid issues. Many years ago people regularly wrote things like "if (retval = f())" but after compilers started to complain about it people changed to write "if ((retval = f()))" instead, if they want an assignment and truthfulness testing at the same time.
    - deleted 7y ago
      [deleted]
  - WalterBright 7y ago
    > Surely your software cannot decide that... The D implementation would reject such code. The DFA assumes all control paths are executed. For example, if (c) free(p); *p = 3; is rejected as use-after-free. if (c) free(p); if (!c) *p = 3; is also rejected as use-after-free. If the DFA is done properly, you will not be able to trick it.
    - Ygg2 7y ago
      Ok. And if you call into non-D code, like C or assembly? I think this is just moving potential problem under rug, which is best it can do, given Rice Theorem
      - WalterBright 7y ago
        Calling non-D functions means the compiler cannot check them, and will rely on the user having correctly specified and annotated the function signature. I.e. you can have "unsafe" annotated code which the compiler doesn't check, which is indeed where the dirty deeds get swept. For example, I doubt someone could write a guaranteed safe implementation of malloc(). The idea, naturally, is to specifically mark such sections so that your crack QA team knows what to focus on, and to minimize the amount of such code. The trick is to make the safe sections expressive enough that it is practical to write the bulk of the code in safe sections, thereby minimizing the "threat surface".
    - UncleMeat 7y ago
      Then that doesn't mean "0% of the negatives".
      - bonzini 7y ago
        No, it means you have false positives. But no false negatives.
        UncleMeat 7y ago
        And that's a "negative" in a practical sense. An abstract interpretation that outputs Top for all programs is sound but useless. In practice, most sound static analyses for complex problems aren't too far from that.
  - rq1 7y ago
    There’s definitely a double free, provided that nowhere you proved that your conditions can’t be simultaneously true.
- 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 ago
        Please stop making accounts to break the site guidelines with. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html

WalterBright 7y ago

Fortunately, I am unaware that it was impossible and did it anyway :-) But it is possible I made a mistake. It is also true that for it to work, one has to change the way one writes code, like Rust does. This is why D requires and @live attribute be added to functions to enable the checking for just those functions, so it doesn't break every program out there. It will enable incremental use of the checking at the user's option.

nullc 7y ago
You're probably using a different definition of 100% than any impossibility proof would use. Consider some code: --- a=malloc(1); needfree=true; if (hashfn(first_factor(huge_static_rsanum1))&1){needfree=false;free(a);} if (hashfn(first_factor(huge_static_rsanum2))&1){needfree=false;free(a);} if(needfree)free(a); --- The decision if this has a double free or not depends on the factorizations of two huge difficult to factor constants. It either double-frees or not depending on those constants. Surely your software cannot decide that... What you probably mean is something like "100% on real programs rather than contrived cases". Of course, in that case, your definition of 'real programs' is the catch. :P Sometimes things that seem like they should always work except on contrived junk like the above example actually run into limitations in practice because macros and machine code generation produce ... well ... contrived junk from time to time.
- jjnoakes 7y ago
  I personally would want code like this flagged by static analysis. I would fix the code by not calling free in the second 'if' body if needfree was already false (just like the call at the end of the function is guarded).
  - nullc 7y ago
    You might want it flagged-- I would--, but it would still be a false positive if it did so (assuming the constants didn't result in a double-free). :)
    - kccqzy 7y ago
      I think the argument is that static analyzers don't have to work on completely unchanged code, but rather rely on humans to structure the code in a way to avoid issues. Many years ago people regularly wrote things like "if (retval = f())" but after compilers started to complain about it people changed to write "if ((retval = f()))" instead, if they want an assignment and truthfulness testing at the same time.
  - deleted 7y ago
    [deleted]
- WalterBright 7y ago
  > Surely your software cannot decide that... The D implementation would reject such code. The DFA assumes all control paths are executed. For example, if (c) free(p); *p = 3; is rejected as use-after-free. if (c) free(p); if (!c) *p = 3; is also rejected as use-after-free. If the DFA is done properly, you will not be able to trick it.
  - Ygg2 7y ago
    Ok. And if you call into non-D code, like C or assembly? I think this is just moving potential problem under rug, which is best it can do, given Rice Theorem
    - WalterBright 7y ago
      Calling non-D functions means the compiler cannot check them, and will rely on the user having correctly specified and annotated the function signature. I.e. you can have "unsafe" annotated code which the compiler doesn't check, which is indeed where the dirty deeds get swept. For example, I doubt someone could write a guaranteed safe implementation of malloc(). The idea, naturally, is to specifically mark such sections so that your crack QA team knows what to focus on, and to minimize the amount of such code. The trick is to make the safe sections expressive enough that it is practical to write the bulk of the code in safe sections, thereby minimizing the "threat surface".
  - UncleMeat 7y ago
    Then that doesn't mean "0% of the negatives".
    - bonzini 7y ago
      No, it means you have false positives. But no false negatives.
      - UncleMeat 7y ago
        And that's a "negative" in a practical sense. An abstract interpretation that outputs Top for all programs is sound but useless. In practice, most sound static analyses for complex problems aren't too far from that.
- rq1 7y ago
  There’s definitely a double free, provided that nowhere you proved that your conditions can’t be simultaneously true.
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 ago
      Please stop making accounts to break the site guidelines with. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html