<div dir="ltr"><div class="gmail_default" style="font-family:monospace">What I think now about this:</div><div class="gmail_default" style="font-family:monospace">It may be better but more work to make a kind of generic interface that supports modeling of these summaries. This interface should make specification and apply of summaries easy enough to use at any checker, extensible with checker-specific behavior. Then we can have specific checkers for specific groups of functions. These can model every aspect of the functions so that responsibility for one function is not spread between multiple checkers.</div><div class="gmail_default" style="font-family:monospace">(About 'popen': This is and will be not handled by StreamChecker because it is part of another API with integer "file descriptors". StreamChecker works with 'FILE *' stream handle. Bigger problem is that the integer file descriptor API works relatively similar to the 'FILE *' API so if there is a new checker for these functions it can work similar as StreamChecker, maybe it would be even more simple.)</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Artem Dergachev via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> ezt írta (időpont: 2020. jún. 25., Cs, 18:45):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
  
    
  
  <div>
    No matter how far do we want to push the flexibility of our
    summaries, this checker will always have limitations. I suggest we
    treat it as yet another method of interprocedural analysis, i.e.
    simply an improvement over conservative evaluation of the call.<br>
    <br>
    I don't see a need for a specific one-size-fits-all policy here. We
    can decide every time on per-function basis. Doing evalCall in two
    different checkers is obviously bad (and we have an assertion that
    protects against that, so it won't be "anarchy" but merely a crash,
    at least in non-release builds but i'd expect such crash to be
    fairly apparent) but any other separation of concerns sounds
    reasonable to me.<br>
    <br>
    Like, for some functions it makes sense to have
    StdLibraryFunctionsChecker do the evalCall and the ranges and let
    other checkers model various aspects of the call that are of
    interest to them in their PreCall/PostCall. Specific checkers can
    also do a better job at reporting bugs than the generic checker. For
    functions for which StdLibraryFunctionsChecker doesn't do evalCall
    this makes even more sense.<br>
    <br>
    It probably doesn't make much sense to keep
    StdLibraryFunctionsChecker's pre/post-call modeling if we have a
    specific checker for that function.<br>
    <br>
    I suspect that if you end up setting up dependencies, it's almost
    always better to move the functionality to one checker. But there's
    no need to merge different aspects of modeling that are completely
    orthogonal. Note that state splits are idempotent which means that
    it's often ok to duplicate the post-call state-splitting code in
    multiple checkers without making them aware of each other.<br>
    <br>
    <div>On 6/25/20 7:19 AM, Kristóf Umann via
      cfe-dev wrote:<br>
    </div>
    <blockquote type="cite">
      
      <div dir="ltr"><br>
        <div class="gmail_quote">
          <div class="gmail_attr">+Balázs Kéri<br>
          </div>
          <div dir="ltr" class="gmail_attr"><br>
          </div>
          <div dir="ltr" class="gmail_attr">On Thu, 25 Jun 2020 at
            10:39, Gábor Márton <<a href="mailto:martongabesz@gmail.com" target="_blank">martongabesz@gmail.com</a>>
            wrote:</div>
          <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
            <div dir="ltr">
              <div>One of my goals with StdLibraryFunctionsChecker is to
                add argument constraints to functions in the C, C++ and
                POSIX standard. It is very easy to gather these argument
                constraints and apply them massively. By doing this, the
                analysis can be more precise, so, I see a lot of gain
                here. However, some of these argument constraints could
                be handled in more specific checkers too, e.g. in
                CStringModeling, MallocChecker or in StreamChecker.</div>
            </div>
          </blockquote>
          <div><br>
          </div>
          <div>For those that didn't follow development closely,
            argument constraints in this context mean the following: For
            select functions, we define a signature we can use to match
            a call to this function (for C functions, that is return
            value, function name and argument types), and a so called
            "summary", which is a list of constraints on the arguments
            or the return value. For a function like fread(), the
            signature is <font face="monospace">size_t fread(void *,
              size_t, size_t, FILE *)</font>, and the summary is that
            the stream argument and the buffer must be non-null, and
            that the buffer must be at least the size of (2nd arg * 3rd
            arg). We can also constrain the return value, that is is at
            least (2nd arg * 3rd arg).</div>
          <div><br>
          </div>
          <div>If on the function call any of the preconditions isn't
            met, we can emit a warning, otherwise we can increase the
            precision of the analysis by constraining the arguments.</div>
          <div><br>
          </div>
          <div>This is a form of summary based analysis, and its pretty
            easy to pull off on standard functions because they have,
            well, standardized signatures and constraints.</div>
          <div><br>
          </div>
          <div>(this isn't pulled from the checker, just a theoretical
            example)</div>
          <div> </div>
          <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
            <div dir="ltr">
              <div>Let's take for instance `popen`. In the mentioned
                patch I am adding a simple summary with argument
                constraints. However, sooner or later popen could be
                modeled in StreamChecker once that is mature enough. (1)
                Should we remove the summary
                from StdLibraryFunctionsChecker when that happens? (2)
                Or should we have a declaration that ranges and
                nullability are checked with summaries while more
                specific things are checked in their respective
                checkers? (3) Or the specialized checkers could be
                dependencies to the generic StdLibraryFunctionsChecker,
                so any bug related to e.g. popen is prioritized to
                StreamChecker?</div>
            </div>
          </blockquote>
          <div><br>
          </div>
          <div>Yes, this this the big one. What role should batch
            modeling checkers play in the analyzer alongside specific
            modeling checkers? Lets take an example that has already
            presents a problem, and the most glaring of them, to me at
            least, is stream modeling functions.</div>
          <div><br>
          </div>
          <div>Take for instance the above mentioned fread. The
            *numerical* pre- and postconditions can be enforced just as
            I detailed. However, the most important effect of this
            function is of course the stream operation, what happens
            depending on the validity of the stream object (which is not
            a numerical property), and what happens to it after the call
            has finished, successful or not. If the stream hits EOF
            during the read, the return value is less then (2nd arg *
            3rd arg), and is equal to it if the read was successful.
            What this implies to me is that StdLibraryFunctionChecker
            cannot really take on the responsibility of establishing a
            post condition, **unless** the function is question can be
            described by numerical properties only (like isalpha()).</div>
          <div><br>
          </div>
          <div>This is something that this checker already does well I
            think. Its clear that we don't want to expand it to cover
            non-numeric cases. So, onto the topic that brought us here.</div>
          <div><br>
          </div>
          <div>(2.) This sounds great. I think precondition checking is
            something that introduces a lot of code duplication in
            checkers, and I don't think that fread()ing a nullpointer is
            a stream mismanagement issue necessarily. A notable
            challenge to overcome, however, is how can we ask
            StreamChecker to add NoteTags from other checkers' reports
            (see: <a href="https://reviews.llvm.org/D81407?id=270161#inline-750832" target="_blank">https://reviews.llvm.org/D81407?id=270161#inline-750832</a>).</div>
          <div><br>
          </div>
          <div>(1.) I think the only thing we could do with this idea is
            to implement an incomplete post condition modeling until a
            checker comes along and does it properly. However, even this
            would only make sense if we have a single post-condition (<a href="https://reviews.llvm.org/D79432#inline-757474" target="_blank">https://reviews.llvm.org/D79432#inline-757474</a>).</div>
          <div><br>
          </div>
          <div>(3.) If we go with option (2), we must introduce strong
            dependencies so that numerical preconditions are checked
            beforehand. However, if we *duplicate* the same checking in
            multiple checkers and want to use dependencies to make the
            correct code runs first, we would introduce deadcode, or
            possibly running the same check twice, and the problem of
            inconsistently distributing the responsibility of analysis
            gets even worse.</div>
          <div> </div>
          <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
            <div dir="ltr">
              <div>My other goal would be to make it possible to add
                argument constraints (or branches/cases) to any library
                functions. These libraries may never be modeled in the
                analyzer. In this case the above problem is
                non-existent. Perhaps, we should divide the checker to
                two different checkers once we reach that point,
                shouldn't we? We are very close to
                rename StdLibraryFunctionsChecker to
                LibraryFunctionsChecker anyway by now.</div>
            </div>
          </blockquote>
          <div><br>
          </div>
          <div>If we want to implement summary based analysis, it would
            only be fitting to bear the name
            SpeculativeSummaryBasedFunctionModeling and
            StdSummaryBasedFunctionModeling or something, right? ;)
            Anyway, this is the least of the worries.</div>
          <div><br>
          </div>
          <div>I agree, pure functions (like the above mentioned
            isalpha()) is the real learning opportunities for
            generalized summary based analysis for the time being.</div>
          <div> </div>
          <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
            <div dir="ltr">
              <div>There is more. In `evalCall` if a checker returns
                true then that function is no longer processed by any
                subsequent checkers. That is the case with pure
                functions in StdLibraryFunctionsChecker. In this case,
                however, it would be anarchy if another checker also
                returns true from its own evalCall callback. Only one
                can rule. It would be great if we could enforce that no
                two checkers evaluate the same function this way. But I
                don't see any clear solution to achieve that right now,
                this is really challenging.</div>
            </div>
          </blockquote>
          <div><br>
          </div>
          <div>Yup, the problem is that checker callbacks from
            CheckerManager's perspective (I might be wrong here!) takes
            a set of ingoing nodes and returns a set of outgoing ones.
            So the solution might not be terribly complicated, just ugly
            (large #ifs).</div>
        </div>
      </div>
      <br>
      <fieldset></fieldset>
      <pre>_______________________________________________
cfe-dev mailing list
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
    </blockquote>
    <br>
  </div>

_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote></div>