<html>
  <head>
    <meta content="text/html; charset=utf-8" http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    Hello,<br>
    <br>
    On 31.05.2016 16:53, Gábor Horváth wrote:<br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">Hi!<br>
        <div class="gmail_extra"><br>
          <div class="gmail_quote">On 26 May 2016 at 14:56, Artem
            Dergachev via cfe-dev <span dir="ltr"><<a
                moz-do-not-send="true"
                href="mailto:cfe-dev@lists.llvm.org" target="_blank"><a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a></a>></span>
            wrote:<br>
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">I've got an idea. The
              idea comes as a replacement for fixing current issues with
              the GDM (sharing traits across checkers, automating the
              routine work on checker side). The idea is: GDM is not the
              right place to model most of the checker-controlled
              program state traits, instead we should encourage checkers
              to use the Store, which already has most of the necessary
              features.<br>
            </blockquote>
            <div><br>
            </div>
            <div>Sharing traits and automating clean-up and other
              tedious tasks would be awesome. However isn't a dependency
              graph of checkers (to restrict the order of execution) is
              a prerequirement for sharing traits?<br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    Yeah, i guess it's inevitably necessary. For this proof of concept,
    when i was playing with SimpleStreamChecker, i put checking into
    PreCall ("first check our invariant then close the file") and
    modeling in post-call ("before the call it's not closed yet"). But
    i've little hope that such tricks would work in the generic case.<br>
    <br>
    By the way, forgot to mention after a few rewrites: in all examples
    i provide the checker is split into the "modeling" checker (which
    throws no reports) and the "checking" checker (which doesn't change
    the program state), which interact through the smart traits.
    PthreadLockChecker example is split into three parts. So this
    facility seems to allow splitting large checkers, like MallocChecker
    (4000+ lines of code) into smaller checkers.<br>
    <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
              Specifically, whenever the checker tries to model a
              certain data structure, which exists (or could have
              existed) somewhere in the program (be it user or kernel
              memory, or CPU registers, or shadow memory of some
              sanitizer-like tool which could have been run alongside
              the program), then the checker should model this data
              structure directly in the Store(?)<br>
            </blockquote>
            <div><br>
            </div>
            <div>How would you implement this? Wouldn't this kind of
              approach make the store heavier? I think the common case
              should be that, no extra data is associated with the live
              "objects". Making the common case more heavy weight might
              imply a performance problem.<br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    I just hope that we're logarithmic enough to avoid performance drops
    due to that issue. If we're not, then i'd suggest putting most of
    the "ghost" objects into some separate bucket, because very often we
    known where to find what we're looking for - if we're looking for a
    ghost object or for a real object. Finally, performance of
    removeDeadBindings() would drop because of the single worklist, but
    that's intentional - we need the single worklist. We shouldn't be
    suffering from significant memory overhead though, because the
    amount of stuff to store is roughly the same anyway.<br>
    <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <div>Also note that, checkers are not always modelling a
              data structure. It might model a property of a path e.g.:
              was something locked on this path? Of course, you could
              still attach this kind of information to a mutex or
              something like that, but if you are only curious whether a
              certain method was invoked in a critical session, it is
              easier to only track the lock deepness for each path, this
              way you only have one integer to deal with in the state
              instead of several on/or switches for each mutexes along
              the paths. <br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    For the lock deepness use case, i'd suggest a single ghost variable
    that gets incremented by the checker when something is locked and
    decremented when something is unlocked. This variable is essentially
    a simple data structure that does not instantly exist in the
    program, but can probably be implemented by some dynamic
    instrumentation technique, so i'm still fine with imagining such
    data structure for the purpose of static analysis. My last
    experiment with PthreadLockChecker provides an even more complicated
    example - it models the stack of mutexes for catching lock order
    reversal.<br>
    <br>
    So far the only thing i'm expecting troubles with is constraint-like
    information (eg. range constraints on symbols) - which is truly a
    kind of meta-information that truly cannot be represented as a data
    structure. For such constraints, i've no plan so far but to leave
    them in the GDM; see below though for criteria.<br>
    <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
              This approach may be thought of as bringing the idea of
              "ghost code" from model checking into our analyzer. We're
              supposed construct ghost structures during analysis, which
              mimic real or imaginary things that happen during program
              execution.<br>
              <br>
              With the current region hierarchy, it's a bit hard to
              follow this approach, because memory regions are hard to
              construct. So my proposal is to add a few more region
              classes, which would allow checkers to cheaply, probably
              even transparently, construct the necessary structures in
              the Store.<br>
              <br>
              A few reasons why i ended up liking this idea:<br>
              <br>
              1. It's natural. After all, the program doesn't have
              anything like GDM when it executes dynamically - it only
              has memory, which means that the Store, being our memory
              model, should easily take care of modeling anything that
              is going on in the program, and useful features of the
              Store are still useful for such modeling, so why don't we
              use them. In other words, the most natural way to explain
              how exactly should the smart data map automate routine
              tasks would be to say that it should behave exactly like
              the Store. So why don't we just use the Store.<br>
            </blockquote>
            <div><br>
            </div>
            <div>They have a lot in common indeed, it is a good
              observation! However I think there are some subtle
              details. The lifetime of the information that is attached
              to a data structure might not be the same as the lifetime
              of the data structure itself. E.g.: one might use the
              return value of strlen after the argument of strlen is
              already garbage collected. With some checker participation
              though this might be worked around (in fact there are
              workarounds for this same problem with GDM as fas as I
              remember). <br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    Hmm. That's a problem we seem to automagically solve - behavior of
    GDM is very store-like in that case. We used to have SymbolMetadata
    for string length, for which liveness is checker-managed. Now, with
    modeling string length as ghost object, strlen() returns a
    SymbolRegionValue of the ghost object, which lives exactly as long
    as we need, even if the ghost object dies.<br>
    <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
              2. There's no problem with sharing the trait. Any checker
              can see what's going on with a plain getSVal(). Of course,
              we can hide the key for getSVal() in anonymous namespace
              and probably provide getters/setters instead, which
              wouldn't stop the Store from iterating over bindings.<br>
            </blockquote>
            <div><br>
            </div>
            <div>In order to truly be able to participate, guarantees
              for execution order should be introduced, se one of my
              previous comments. <br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    Yep.<br>
    <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
              3. There's no problem with routine work and code
              duplication in checkers, which makes writing checkers a
              lot easier:<br>
                a. Store transparently takes care of cleaning up
              live/dead symbols, there's no more problems with different
              worklists for store and checkers.<br>
            </blockquote>
            <div><br>
            </div>
            <div>This would be awesome!<br>
            </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">
                b. The store takes care of invalidation, eg.
              checkRegionChanges could probably be automated with this
              approach, by simply choosing a good parent region for our
              checker data structures.<br>
            </blockquote>
            <div><br>
            </div>
            <div>The invalidation rules might be different for the
              associated information than for the object. E.g.: one
              might assume that a private property is only modified by
              friends (even tough it is possible in C++ to modify
              private members, it is very rare). Is it possible to also
              have custom invalidation schemes for these traits? Or the
              checkers would fall back to GDM in those cases? (You think
              of this as a GDM alternative or replacement?)<br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    I'd agree that invalidation of ghost-fields is so far the most
    unclear part of the proposal. Even for SimpleStreamChecker "version
    3" it didn't work very well - we're losing positives on test due to
    lack of ability to manage invalidation manually. But that's about
    pointer-escape, not region-changes. I've not tested much of the
    region-changes stuff yet.<br>
    <br>
    I'm thinking more on that, with two ideas - either add some helpers
    into the trait objects ("this trait doesn't want to be
    auto-invalidated by functions matching certain criteria"), or
    disable auto-invalidation completely for ghost-fields (they'd no
    longer have a symbolic offset, but some new kind of offset that's
    neither concrete nor symbolic).<br>
    <br>
    Most importantly, binding to ghost fields shouldn't invalidate
    regular fields.<br>
    <br>
    Maybe i'd find out that ghost fields won't work as nicely as i
    expected, so i'd have to think of them as "shadow memory" instead -
    pretend that ghost values mapped to memregions are actually
    "outside" memregions. But i still hope that it's not the case and
    managing superregions would be helpful; the 'errno' ghost variable
    is my primary motivation for this (we don't always have it in the
    AST, as it could be macroed into some `*__errno()', but we still
    know in which memspace it should reside).<br>
     <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
                c. Also, Store provides us with SymbolRegionValue-class
              and SymbolDerived-class symbols for our structures when
              values in them are unknown; this way we can reason if it's
              the same unknown or a probably-different unknown.<br>
            </blockquote>
            <div><br>
            </div>
            <div>This is a very interesting property! Tracking this
              would be automatic? Do you know how much extra overhead
              would that be?<br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    The Store just auto-creates them for regions initialized in a
    certain manner (eg. not initialized at all -> create
    SymbolRegionValue), and i guess it just shouldn't make an exception
    for ghost regions.<br>
    <br>
    When this feature is not used, as in my examples with stream
    checker, we simply see if the value is constant or not, and we don't
    care if it's constant.<br>
    <br>
    There's slight problem with marking the stream state as unknown -
    right now i bind an UnknownVal into it. Once we do want to use such
    feature, we'd have to call a standard invalidation method on that
    region. With GDM, we could simply remove it from GDM - "stop
    tracking", then "start tracking" again. But we cannot remove
    bindings from the Store, because we want to avoid reincarnation of
    SymbolRegionValue. This UnknownVal binding would be automatically
    removed once the stream dies, but i agree that it's still some
    overhead to measure.<br>
     <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
                d. The store can be easily dump()'ed, we no longer need
              hooks for printing the program state on checker side.<br>
            </blockquote>
            <div><br>
            </div>
            <div>I think still need a way to stringify the metadata we
              attached to the "objects". <br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    Yeah, it'd be nice to have constants mapped to some string values,
    eg. right now the dump looks like:<br>
    <br>
        (StreamState{conj_$0<void *>}, 0, Direct): 1 S32b<br>
    <br>
    But it'd be better as:<br>
    <br>
        (StreamState{conj_$0<void *>}, 0, Direct): Open<br>
    <br>
    We could do that by adding a helper method to the state trait, maybe
    merge the whole enum into the trait.<br>
     
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
                e. In the future, we can probably add alpha-renaming,
              and then problems and solutions would most likely be
              exactly the same for the Store itself and for checker data
              structures.<br>
            </blockquote>
            <div><br>
            </div>
            <div>Good point!<br>
            </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">
              <br>
              4. This approach is very easy to implement and to explain.
              Most of the time, we just use the standard
              getSVal()/bindLoc() API for everything, probably some
              overrides.<br>
            </blockquote>
            <div><br>
            </div>
            <div>If you think of this as an alternative to GDM, a guide
              explaining when to choose the GDM would be awesome.<br>
            </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">
              <br>
              A few arguments against this approach:<br>
              <br>
              1. Some program state traits do not try to model data
              structures that already exist in the program. The best
              example is probably range constraints. Constraints are
              immaterial for dynamic execution - they're a
              meta-information about chosen execution path. For such
              traits, i do not yet present a solution, though i have a
              couple of thoughts - if anybody's curious, i can dump. In
              particular, i feel as if constraint-like traits can be
              easily supported with a separate generic approach, and
              it'd cover all of our problems.<br>
            </blockquote>
            <div><br>
            </div>
            <div>What kind of ranges are we talking about? Aren't we
              only store ranges for symbols using the constraint
              manager?<br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    A few more info on this matter, as it seems important. Yeah, the
    primary example is ranges for symbols. One more example would be
    dynamic type map, but it's a bit more complicated.<br>
    <br>
    So i propose the following reasoning as an approximation for a
    criteria of using GDM vs. using Store: it's somehow similar to
    difference between symbols and regions. I'm not possessing a
    perfectly clear understanding right now, but i'd try my best to
    explain my thoughts below:<br>
    <br>
    Region contents are essentially mutable. Today they contain one
    thing, tomorrow they contain another thing, but it's still the same
    region. You can overwrite it, you can move it to another region, you
    can invalidate it, you can placement-new on top of it.<br>
    <br>
    Symbols, on the other hand, are essentially immutable. Any
    information about the symbol which we managed to gather about the
    symbol was true since forever and shall remain true forever. A
    symbol of range [1, 2] would never take value '3', and has never
    taken before, during execution of the program over that particular
    branch.<br>
    <br>
    These two concepts - of regions and symbols - work together to make
    the analyzer model simple operations.<br>
    <br>
    GDM was designed to let the analyzer model more complex operations.
    However, my point is that all GDM traits are either "Store-like",
    which means, their keys behave like regions into which we bind
    values, then re-bind different values, or they are
    "Constraint-like", which means their keys behave like symbols, and
    information bound to them can only be expanded, but not mutated.<br>
    <br>
    For instance, despite SimpleStreamChecker's key is a symbol, the
    trait is essentially "Store-like": the same file descriptor is first
    open, then closed. Which is why i propose first fixing the situation
    by providing a region tied to that symbol, and then bind values to
    represent file descriptor operations.<br>
    <br>
    Now we're ready to consider the DynamicTypePropagation example. In
    fact, dynamic type information sounds like "Constraint-like" trait,
    because we can only know more about the dynamic type of every
    object. However, currently dynamic type is bound to a region.
    There's a problem with that - we can placement-new into the region,
    and the dynamic type shall mutate. Because region contents are
    mutable. So, in my opinion, dynamic type map in its current
    implementation is not a well-defined trait - it should be refactored
    into two traits, one of which is "Store-like" (bind an object ID
    symbol to every region; it can be copied, moved, invalidated, or
    affected by placement-new as much as we want), and another is
    "Constraint-like" (map object ID symbol to its dynamic type) - which
    is truly immutable. And, again, these two concepts - "Store-like"
    things and "Constraint-like things" - work together.<br>
    <br>
    So my criterion so far is to move "Store-like" objects to the Store,
    where they seem to belong, and keep "Constraint-like" objects in the
    GDM. <br>
    <br>
    Additionally, I believe that "Constraint-like" objects are always
    mapped to symbols (i.e. a map from symbols to something - because
    you can't tie them to regions, because region contents are mutable).
    So i believe that stuff like liveness or alpha-renaming should be
    very simple for "Constraint-like" traits - i.e. never keep alive,
    just clean up symbols, merge info on alpha-renaming - and we can
    still automate everything.<br>
    <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
              2. GDM is done in terms of sets and maps, however Store
              doesn't have sets or maps, it only works with C-like
              memory with at best 1-dimensional arrays. Of course we can
              model maps of ints to ints as ghost arrays with symbolic
              bindings to elements, and it's a safe and sane
              implementation. For a map from int to set of ints, it gets
              harder. But i think it's a non-issue: it's still more
              important to figure out how do we model more complicated
              containers (i still dream of container symbols and
              container constraints, which would reduce this issue to
              issue '1.'), and then we could re-visit this issue.<br>
            </blockquote>
            <div><br>
            </div>
            <div>We should solve this problem without too much execution
              overhead on the common case (no information stored by a
              checker).<br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    In fact, i'm thinking^W dreaming about the same thing here -
    container constraints should be "Constraint-like", tied to container
    content symbols.<br>
    <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">
              I've made proof-of-concept patchs to SimpleStreamChecker
              (two different approaches) and PthreadLockChecker. The
              patch introduces four kinds of ghost regions - each "smart
              trait" owns its own memory space which doesn't get
              invalidated (for things that don't need to be invalidated,
              or for manual control), and allows creating one variable
              inside that (or any other) memory space, one field inside
              any region, or one symbol-based region for any symbol
              (unlike SymbolicRegion, the ghost symbol-based region
              doesn't need to be based on a pointer-type symbol, any
              symbol will do fine).<br>
              <br>
              The patches are on my github because i'd re-arrange them
              if i was to put them on phabricator, and not sure what to
              do with multiple checker variants. So i'm asking to have a
              look at the checkers and see if you want to write checkers
              *that* way, instead of the traditional GDM, then i'd focus
              on fixing smaller issues, or i'd have to come up with
              something different.<br>
              <br>
              SimpleStreamCheckerV2 defines symbol-based ghost regions
              for file descriptor symbols and stores constant values (0
              or 1) inside them, indicating opened and closed streams.
              It doesn't need to store the "unknown" state - it is
              represented by non-constant values, eg. SymbolRegionValue
              of the ghost region. Link: <a moz-do-not-send="true"
href="https://github.com/haoNoQ/clang/commit/578e79009bbac81c129daff19e14dbad16e2e43d"
                rel="noreferrer" target="_blank">https://githubnValue of
                the ghost
                r.com/haoNoQ/clang/commit/578e79009bbac81c129daff19e14dbad16e2e43d</a></blockquote>
            <div><br>
            </div>
            <div>As a patch against an existing checker this would be
              easier to evaluate what the differences are. But at first
              glance I did like the UX of checker development this
              provides except for registering the trait :)<br>
            </div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    One sec. Here. Hope these links don't die too soon. Just wasn't sure
    how to organize that on github.<br>
    <br>
    Original SimpleStreamChecker vs. SimpleStreamCheckerV2:<br>
    <a class="moz-txt-link-freetext" href="https://www.diffchecker.com/a9fqicng">https://www.diffchecker.com/a9fqicng</a><br>
    <br>
    Original SimpleStreamChecker vs. SimpleStreamCheckerV3:<br>
    <a class="moz-txt-link-freetext" href="https://www.diffchecker.com/3ketimia">https://www.diffchecker.com/3ketimia</a><br>
    <br>
    SimpleStreamCheckerV2 vs. SimpleStreamCheckerV3:<br>
    <a class="moz-txt-link-freetext" href="https://www.diffchecker.com/ebac2icl">https://www.diffchecker.com/ebac2icl</a><br>
    <br>
    PthreadLockChecker vs. PthreadLockCheckerV2:<br>
    <a class="moz-txt-link-freetext" href="https://www.diffchecker.com/mixtsmra">https://www.diffchecker.com/mixtsmra</a><br>
    <br>
    <br>
    <blockquote
cite="mid:CAPRL4a2QDg5ht7RPSHUmAUb=Z=gkUUY+5DgBbs-bW912-Rzpng@mail.gmail.com"
      type="cite">
      <div dir="ltr">
        <div class="gmail_extra">
          <div class="gmail_quote">
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
              0.8ex;border-left:1px solid
              rgb(204,204,204);padding-left:1ex">SimpleStreamCheckerV3
              defines a ghost field inside each symbolic region
              corresponding to the each stream's pointer symbol, and
              stores the same constants inside these fields. It has
              troubles suppressing invalidation of these fields, which,
              in my opinion, should ideally be solved through
              evalcall/bodyfarm of library functions. Both versions do
              not suffer from the "zombie symbols" issue. Link: <a
                moz-do-not-send="true"
href="https://github.com/haoNoQ/clang/commit/bb63471fa6d70502e61728052b6b7a649c4d80d1"
                rel="noreferrer" target="_blank"><a class="moz-txt-link-freetext" href="https://github.com/haoNoQ/clang/commit/bb63471fa6d70502e61728052b6b7a649c4d80d1">https://github.com/haoNoQ/clang/commit/bb63471fa6d70502e61728052b6b7a649c4d80d1</a></a><br>
              <br>
              PthreadLockCheckerV2 defines a ghost field inside each
              mutex, indicating one of the four states (Initialized,
              Locked, Unlocked, Destroyed), which allows it to find
              double locks/unlocks etc. Additionally, it models the
              stack of locks in order to find lock order reversals. This
              is modeled through a single ghost variable of type
              `void**', which represents the stack pointer - the checker
              dereferences this pointer to access or modify the stack
              and increments/decrements it. Link: <a
                moz-do-not-send="true"
href="https://github.com/haoNoQ/clang/commit/ab581e4da9c3ef2ddfc0fe75a20ffa9ce789fe8d"
                rel="noreferrer" target="_blank"><a class="moz-txt-link-freetext" href="https://github.com/haoNoQ/clang/commit/ab581e4da9c3ef2ddfc0fe75a20ffa9ce789fe8d">https://github.com/haoNoQ/clang/commit/ab581e4da9c3ef2ddfc0fe75a20ffa9ce789fe8d</a></a><br>
              <br>
              None of these checker's code actually deals with ghost
              regions through MemRegionManager - they always use
              wrappers in the ProgramState class, which in my opinion
              are easy and intuitive, though probably more such wrappers
              need to be introduced.<br>
              <br>
              All the newly introduced terminology is worth discussing,
              i don't really like it.<br>
              _______________________________________________<br>
              cfe-dev mailing list<br>
              <a moz-do-not-send="true"
                href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
              <a moz-do-not-send="true"
                href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev"
                rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
            </blockquote>
          </div>
          <br>
        </div>
      </div>
    </blockquote>
    <br>
  </body>
</html>