[cfe-dev] Suggested starter bug on clang analyzer codebase

Malhar Thakkar via cfe-dev cfe-dev at lists.llvm.org
Wed May 17 04:29:58 PDT 2017


Never mind. I was using the wrong command.

Now, I'm using the following command
*./clang -cc1 -analyze -analyzer-checker=alpha.unix.PthreadLock
../../llvm/tools/clang/test/Analysis/pthreadlock.c*

Added -analyze and removed -verify.
Now, it's working as expected.

Thank you.

Regards,
Malhar Thakkar
ᐧ

On Wed, May 17, 2017 at 4:35 PM, Malhar Thakkar <cs13b1031 at iith.ac.in>
wrote:

> As I wanted to start afresh, I downloaded LLVM and clang source from their
> mirror repositories from GitHub and built them yesterday. Then, I modified
> PthreadLockChecker.cpp and then performed *make clang* and *make install*
> in the build directory. It built without any errors.
>
> Then, I went to build/bin and performed
>
> *./clang -cc1 -analyzer-checker=alpha.unix.PthreadLock -verify
> ../../llvm/tools/clang/test/Analysis/pthreadlock.c*
>
> I encountered an error saying, *'warning' diagnostics expected but not
> seen: *
>
> Also, the llvm::errs() statement that I added in PthreadLockChecker.cpp is
> not getting displayed on the terminal.
>
> What do you think the problem is?
>
>
>
> Thank you.
>
>
>
> Regards,
>
> Malhar
>>
> On Thu, Apr 20, 2017 at 11:28 PM, Devin Coughlin <dcoughlin at apple.com>
> wrote:
>
>> Malhar,
>>
>> It would be great if you could upload your diff to our Phabricator at
>> http://reviews.llvm.org — this is the online tool we use for code
>> reviews. We can comment on specific code (rather than the overall approach)
>> there.
>>
>> There are instructions for using Phabricator at
>> http://llvm.org/docs/Phabricator.html
>>
>> Devin
>>
>>
>> On Apr 20, 2017, at 9:16 AM, Artem Dergachev <noqnoqneo at gmail.com> wrote:
>>
>> Yep, you're right, no need for SchrodingerLocked!
>>
>> (we'd need to come up with better names, because "Shrodinger mutex" is
>> something i just came up with for explaining... Eg.,
>> UnlockedAndPossiblyDestroyed. Or just remove the new verbose enum values
>> for the new states and look at if the symbol is present in the
>> DestroyRetVal map instead). Note that when you have a DestroyRetVal symbol
>> for a mutex, then the mutex  *definitely* has a state, which is one of the
>> "Shrodinger" states, and vice versa; you can replace quite a lot of your
>> "else" branches with *assertions*, because that's entirely within your
>> checker's area of expertise to keep it that way. You may also probably try
>> to de-duplicate some code into auxiliary functions.
>>
>> lck_mtx_destroy() is void. It doesn't have a return value. Seems that
>> it's good as is :) You can vary behavior depending on the LockingSemantics
>> argument (if it's XNUSemantics, skip stuff).
>>
>> I'd probably also have a closer look tomorrow.
>>
>>
>>
>>
>> On 4/20/17 5:51 PM, Malhar Thakkar wrote:
>>
>> Dear Dr. Artem,
>>
>> I have the following queries.
>>
>>  * Will I ever require SchrodingerLocked? (As you mentioned, a mutex
>>    becomes a Schrodinger only when pthread_mutex_destroy() is called.
>>    Now, calling pthread_mutex_destroy() after pthread_mutex_lock() is
>>    anyway wrong. So, a warning should be raised in this case.)
>>  * SVal corresponding to lck_mtx_destroy() is Unknown or Undefined.
>>    Hence, I am not able to obtain a symbol for the return value of
>>    lck_mtx_destroy() which is leading to incorrect output on the
>>    testcase pthreadlock.c.
>>
>> I'm also attaching the modified code.
>> I want you to check certain parts of the code. (I have added capitalized
>> comments just before the parts which I want you to check.)
>>
>> Thank you.
>>
>>
>> Regards,
>> Malhar
>>>>
>> On Wed, Apr 19, 2017 at 12:11 PM, Artem Dergachev <noqnoqneo at gmail.com <
>> mailto:noqnoqneo at gmail.com <noqnoqneo at gmail.com>>> wrote:
>>
>>    For completeness, i'd point out that there's a simpler alternative
>>    approach to this: force the analyzer to split the state
>>    immediately on pthread_mutex_destroy(): construct a state where
>>    the mutex is destroyed and symbol is known-to-be-zero, construct a
>>    state where the mutex remains the same and symbol is
>>    known-to-be-non-zero, and addTransition to both of them. This
>>    forces the analyzer to investigate two concrete states in
>>    parallel, rather than one "Schrödinger" state that would still be
>>    split when the return value is checked.
>>
>>    However, that approach pays a huge price of doubling analysis time
>>    - the time we would spend in the "Schrödinger" state in the
>>    original approach would be doubled here (and if the return value
>>    is truly unchecked, that may go on until the end of the analysis,
>>    because even after the symbol dies the mutex state is still
>>    different, so the paths wouldn't be merged). This is why we try to
>>    avoid state splits unless it is definitely necessary.
>>
>>
>>    On 4/19/17 9:22 AM, Artem Dergachev wrote:
>>
>>        Yep!
>>
>>        You are right that simply unlocking the failed-to-be-destroyed
>>        mutex in checkDeadSymbols is not enough. The reason for that
>>        is, the moment when the symbol dies is quite unpredictable,
>>        and we don't know how many things have happened to the mutex
>>        between the failed destroy and the symbol death - it might
>>        have been locked and unlocked many times in between.
>>
>>        I'd propose that in order to maintain the correct mutex state
>>        you'd need to check the destruction-return-value symbol in
>>        every operation as well. For instance, when somebody tries to
>>        lock a mutex, see if it was destroyed previously. If it was
>>        destroyed, look at the symbol:
>>        * If the destruction was checked and failed on that execution
>>        path (as you can find out by looking at the symbol's
>>        constraints in the program state), then it's ok, remove that
>>        symbol from the program state and mark the mutex as locked.
>>        * If the destruction cannot be proven to have failed on this
>>        path, then either it is known to have succeeded, or
>>        destruction wasn't checked for failure properly on this path.
>>        It means we have a use-after-destroy, and we report the
>>        warning accordingly.
>>
>>        At the same time, checkDeadSymbols is still necessary: if no
>>        mutex state changes happen after destroy before symbol death,
>>        we need to collect the information from the dying symbol.
>>        Because the symbol is dying, this information will no longer
>>        ever be made more accurate (that is, constraints wouldn't ever
>>        become more strict anymore), so it's as accurate as possible.
>>        So we can be sure if the symbol should be truly set to
>>        destroyed or reverted to the previous state.
>>
>>        Most path-sensitive checkers are kind of state machines (see
>>        also "typestate"). They assign a state to an object, and then
>>        various events (coming from checker callbacks) affect this
>>        state in one way or another. You can draw the state diagram.
>>
>>        So my proposal is to have the following states: Initialized,
>>        Locked, Unlocked, SchrödingerInitialized, SchrödingerLocked,
>>        SchrödingerUnlocked, Destroyed. Schrödinger states indicate
>>        that we're having a Schrödinger mutex that is alive and
>>        destroyed at the same time on different execution paths. The
>>        mutex becomes a Schrödinger mutex after
>>        pthread_mutex_destroy() and remains there until the box is
>>        opened^W^W^W^W either we try to conduct more operations on the
>>        mutex, or the return-symbol of pthread_mutex_destroy() is
>>        dead. At such moments we collapse the mutex state to either
>>        the previous state (eg. SchrödingerLocked -> Locked)  or to
>>        Destroyed. The easiest way to represent Schrödinger states
>>        would be something like "still Locked, but with
>>        destroy-return-symbol set present for this mutex"; upon
>>        collapse we remove the return symbol.
>>
>>        On 4/19/17 8:54 AM, Malhar Thakkar wrote:
>>
>>            Dear Dr. Artem,
>>
>>            Thank you for your response. After incorporating
>>            'addTransition', I was able to suppress the
>>            double-destroy. But, when 'pthread_mutex_destroy' was
>>            called for the second time (i.e., inside the if branch),
>>            LockState was found to be NULL (which it should be
>>            according to my code) but ideally it should be in the
>>            Unlocked state. For, it to be in Unlocked state, I think
>>            state->set<LockMap>() should be executed inside
>>            checkDeadSymbols() instead of executing it inside
>>            AcquireLock(), ReleaseLock(), DestroyLock() and InitLock()
>>            as I am unable to find a way to do it otherwise.
>>
>>            Regards,
>>            Malhar
>>>>
>>            On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev
>>            <noqnoqneo at gmail.com <mailto:noqnoqneo at gmail.com
>> <noqnoqneo at gmail.com>>
>>            <mailto:noqnoqneo at gmail.com <noqnoqneo at gmail.com> <
>> mailto:noqnoqneo at gmail.com <noqnoqneo at gmail.com>>>>
>>            wrote:
>>
>>                Before anything, please note that `State' is your
>>            local variable;
>>                assigning to `State' doesn't immediately affect
>>            analysis in any
>>                way. In order to make your changes to the program
>>            state take
>>                effect, you'd need to put the changed state back into the
>>                `CheckerContext' by calling its `addTransition'
>>            method, like other
>>                checker callbacks do.
>>
>>                Otherwise, your code looks reasonable to me. If
>>            everything is
>>                implemented correctly, i believe that your code would
>>            already
>>                suppress the double-destroy warning on this branch.
>>
>>
>>                On 4/18/17 5:53 PM, Malhar Thakkar wrote:
>>
>>                    Test-case:
>>
>>                    pthread_mutex_lock(&mtx1);
>>                    pthread_mutex_unlock(&mtx1);
>>                    int retval = pthread_mutex_destroy(&mtx1);
>>                    if(retval != 0){
>>                    pthread_mutex_destroy(&mtx1); (1)
>>                    }
>>                    else
>>                    printf("Already destroyed\n");
>>
>>
>>                    Regarding my previous query about reverting the
>>            LockState, how
>>                    would I ensure that the LockState at (1) is
>>            Unlocked and not
>>                    Destroyed?
>>
>>                    Following is the code for checkDeadSymbols()
>>                    void
>>            PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,
>>                                       CheckerContext &C) const {
>>                      ProgramStateRef State = C.getState();
>>                      ConstraintManager &CMgr =
>>            State->getConstraintManager();
>>
>>                      RetValConstraintTy TrackedSymbols =
>>                    State->get<RetValConstraint>();
>>                      for (RetValConstraintTy::iterator I =
>>            TrackedSymbols.begin(),
>>                         E = TrackedSymbols.end(); I != E; ++I) {
>>                        SymbolRef Sym = I->second;
>>                        const MemRegion* lockR = I->first;
>>                        bool IsSymDead = SymReaper.isDead(Sym);
>>                        const LockState* LState =
>>            State->get<LockMap>(lockR);
>>                        // Remove the dead symbol from the return
>>            value symbols map.
>>                        if (IsSymDead){
>>                          ConditionTruthVal retZero =
>>            CMgr.isNull(State, Sym);
>>                    if(retZero.isConstrainedFalse()){
>>                            // Update LockMap
>>                            State = State->remove<LockMap>(lockR); //
>>            I know this
>>                    is incorrect but even after removing this entry
>>                                 from the map, (1) raises a warning
>>            saying, "This lock has
>>                    already been destroyed".
>>                          }
>>                          State = State->remove<RetValConstraint>(lockR);
>>                        }
>>                      }
>>                    }
>>
>>                    Thank you.
>>
>>
>>                    Regards,
>>                    Malhar
>>
>>
>>>>
>>                    On Mon, Apr 17, 2017 at 8:34 PM, Devin Coughlin
>>                    <dcoughlin at apple.com <mailto:dcoughlin at apple.com
>> <dcoughlin at apple.com>>
>>            <mailto:dcoughlin at apple.com <dcoughlin at apple.com> <
>> mailto:dcoughlin at apple.com <dcoughlin at apple.com>>>
>>                    <mailto:dcoughlin at apple.com <dcoughlin at apple.com>
>>            <mailto:dcoughlin at apple.com <dcoughlin at apple.com>> <
>> mailto:dcoughlin at apple.com <dcoughlin at apple.com>
>>            <mailto:dcoughlin at apple.com <dcoughlin at apple.com>>>>> wrote:
>>
>>
>>                            On Apr 17, 2017, at 4:55 AM, Malhar Thakkar
>>                        <cs13b1031 at iith.ac.in
>>            <mailto:cs13b1031 at iith.ac.in <cs13b1031 at iith.ac.in>> <
>> mailto:cs13b1031 at iith.ac.in <cs13b1031 at iith.ac.in>
>>            <mailto:cs13b1031 at iith.ac.in <cs13b1031 at iith.ac.in>>>
>>                            <mailto:cs13b1031 at iith.ac.in
>> <cs13b1031 at iith.ac.in>
>>            <mailto:cs13b1031 at iith.ac.in <cs13b1031 at iith.ac.in>>
>>                        <mailto:cs13b1031 at iith.ac.in
>> <cs13b1031 at iith.ac.in>
>>            <mailto:cs13b1031 at iith.ac.in <cs13b1031 at iith.ac.in>>>>> wrote:
>>
>>                            Consider the following test-case:
>>
>>                            int retval = pthread_mutex_destroy(&mtx1);
>>                            if(retval == 0){
>>                            pthread_mutex_lock(&mtx1);
>>                            }
>>
>>
>>                                       REGISTER_MAP_WITH_PROGRAMSTATE(RetValConstraint,
>> const
>>                        MemRegion
>>                            *, SymbolRef)
>>
>>                            I have added the following snippet for
>>            checkDeadSymbols:
>>                            void
>>            PthreadLockChecker::checkDeadSymbols(SymbolReaper
>>                        &SymReaper,
>>                             CheckerContext &C) const {
>>                              // std::cout<<"Checking dead symbols\n";
>>                            ProgramStateRef State = C.getState();
>>                            ConstraintManager &CMgr =
>>            State->getConstraintManager();
>>
>>                            RetValConstraintTy TrackedSymbols =
>>                        State->get<RetValConstraint>();
>>                              // int counter = 0;
>>                              for (RetValConstraintTy::iterator I =
>>                        TrackedSymbols.begin(),
>>                                                   E =
>>            TrackedSymbols.end(); I !=
>>                        E; ++I) {
>>                            // counter++;
>>                            // std::cout << "Counter:
>>            "<<counter<<std::endl;
>>                            SymbolRef Sym = I->second;
>>                            const MemRegion* lockR = I->first;
>>                            bool IsSymDead = SymReaper.isDead(Sym);
>>
>>                            // Remove the dead symbol from the return
>>            value
>>                        symbols map.
>>                            if (IsSymDead){
>>                            ConditionTruthVal retZero =
>>            CMgr.isNull(State, Sym);
>>                            if(retZero.isConstrainedFalse()){
>>                              std::cout<<"False\n";
>>                              // Update LockMap
>>                            }
>>                            else if(retZero.isConstrainedTrue()){
>>                              std::cout<<"True\n";
>>                            }
>>                            State =
>>            State->remove<RetValConstraint>(lockR);
>>                            std::cout<<"Removed\n";
>>                                }
>>                              }
>>                            }
>>
>>                            Now, after the execution of
>>                        PthreadLockChecker::DestroyLock(),
>>                            checkDeadSymbols() is executed twice before
>>                            PthreadLockChecker::AcquireLock() is executed.
>>
>>                            When checkDeadSymbols is first executed,
>>            there is just
>>                        one symbol
>>                            in RetValConstraint(trivial). But, this
>>            symbol is
>>                        constrained
>>                            /not /to be NULL. Then, the symbol is
>>            removed. During the
>>
>>                            execution of checkDeadSymbols for the
>>            second time,
>>                        there is again
>>                            one symbol in RetValConstraint(I don't
>>            understand
>>                        this. Shouldn't
>>                            this symbol have been destroyed during the
>>            previous
>>                        execution?).
>>                            Nevertheless, this time, this symbol is
>>            constrained to
>>                        be NULL.
>>
>>
>>                        The static analyzer performs a path-sensitive
>>            exploration
>>                    of the
>>                        program. This means that when it sees a branch
>>            it will explore
>>                        both both sides of the branch independently
>>            (unless it can
>>                    tell
>>                        that one side is infeasible). In this case it
>>            means the
>>                    analyzer
>>                        will explore the path when retval is 0 and
>>            when it is not.
>>                    If you
>>                        haven’t read it yet, the “Debugging” section
>>            the the checker
>>                        development manual describes some tricks for
>>            how to
>>                    visualize the
>>                        analyzer’s exploration.
>>            <https://clang-analyzer.llvm.org/checker_dev_manu
>> al.html#commands
>>            <https://clang-analyzer.llvm.org/checker_dev_manu
>> al.html#commands>
>>            <https://clang-analyzer.llvm.org/checker_dev_manu
>> al.html#commands
>>            <https://clang-analyzer.llvm.org/checker_dev_manu
>> al.html#commands>>
>>            <https://clang-analyzer.llvm.org/checker_dev_manu
>> al.html#commands
>>            <https://clang-analyzer.llvm.org/checker_dev_manu
>> al.html#commands>
>>            <https://clang-analyzer.llvm.org/checker_dev_manu
>> al.html#commands
>>            <https://clang-analyzer.llvm.org/checker_dev_manu
>> al.html#commands>>>>.
>>                        I find the debug.ViewExplodedGraph checker
>>            particularly
>>                    helpful.
>>
>>                            Also, I have one more query. After fixing
>>            the above
>>                        mentioned
>>                            issue, how do I update LockMap in the
>>            sense that I'll
>>                        need to
>>                            revert the change made to it if the symbol is
>>                        constrained not to
>>                            be NULL. Apart from keeping track of the
>>            previous
>>                        LockState, is
>>                            there any other way to do it?
>>
>>
>>                        Since the analyzer keeps its representation of
>>            the program
>>                    state
>>                        per-path and explores paths independently, you
>>            shouldn’t
>>                    need to
>>                        do any reverting to undo the effects of
>>            simulating other
>>                    paths to
>>                        reaching a particular program point.
>>
>>                        Devin
>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20170517/f98cb22c/attachment.html>


More information about the cfe-dev mailing list