<div dir="ltr">Hi,<div><br></div><div>Apologies, but, I am back again. </div><div><br></div><div>I have two SymbolRef pointers (SymExpr *). One SymbolRef is (reg_$0<x>) + 3$117. The other SymbolRef is (reg_$0<x>) + 2$130. x is a variable in my program and these SymbolRefs respresent an assignment of x + y to a variable "a". y has the value 3 along one path to the program point where "a" is assigned and it has the value 2 along a second path to the same point, hence the two SymbolRefs differ in the constants.</div><div><br></div><div>I want to compare these two SymbolRefs and find out where they differ. In this case, I want to be able to say that they differ in the constant value. I thought of using symbol_iterator to iterate over each SymbolRef or SymExpr * in lock-step fashion and find the first point where it differs. But these is no operator== defined in the SymExpr class and hence I am unable to check the equality or otherwise of two symbols in the SymbolRefs.</div><div><br></div><div>Is there a way to compare two SymbolRefs and check for the differences? Otherwise, is there a better way to check whether the symbolic value at the same program point but in two different program states are the same or not, and if they are different, is there a way to identify the difference? Maybe, my approach of comparing two symbolic expressions at a program point is not the right approach in the first place.</div><div><br></div><div>Thanks.</div><div><br></div><div>Regards,</div><div>Venu.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 6, 2017 at 2:42 PM, Venugopal Raghavan <span dir="ltr"><<a href="mailto:venur2005@gmail.com" target="_blank">venur2005@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi Aleksei,<div><br></div><div>Thanks. That seems to work.</div><div><br></div><div>Regards,</div><div>Venu.</div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 6, 2017 at 2:05 PM, Aleksei Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div bgcolor="#FFFFFF" text="#000000">
    <div class="m_-1035519723042365625m_4390566528069532645moz-cite-prefix">Hello,<br>
      <br>
      On the point where PreStmt callbacks are called, the expression
      value is still not computed so the result of getSVal() is always
      UnknownVal and not a symbol. You should probably use PostStmt
      callback instead.<br>
      <br>
      <br>
      06.02.2017 08:21, Venugopal Raghavan пишет:<br>
    </div><div><div class="m_-1035519723042365625h5">
    <blockquote type="cite">
      <div dir="ltr">Hi Aleksei,
        <div><br>
        </div>
        <div>Thanks for the reply. Unfortunately, I am having further
          trouble with my checker implementation. I have the following
          code in my checker (called ConstantChecker):</div>
        <div><br>
        </div>
        <div>
          <div> void ConstantChecker::checkPreStmt(<wbr>const Stmt *S,
            CheckerContext &C) const {</div>
          <div>        ProgramStateRef state = C.getState();</div>
          <div>        const LocationContext *lctx =
            C.getLocationContext();</div>
          <div>        SVal val = state->getSVal(S, lctx);</div>
          <div>        SymbolRef Sym = val.getAsSymbol();   </div>
        </div>
        <div>        // Stmt 1</div>
        <div>                      .</div>
        <div>                      .</div>
        <div>                      .</div>
        <div>}</div>
        <div>       </div>
        <div>My input test case for the checker is test1.c and I run the
          command clang -cc1 -analyze
          -analyzer-checker=optin.perfor<wbr>mance.PathSpecificConstants
          test1.c where PathSpecificConstants is the name of my checker:</div>
        <div><br>
        </div>
        <div>
          <div>test(int x) {</div>
          <div>   int y;</div>
          <div>   int a;</div>
          <div>   if (x > 0) {</div>
          <div>     y = 2;</div>
          <div>   }</div>
          <div>   else {</div>
          <div>     y = 3;</div>
          <div>   }</div>
          <div>   a = x + y;</div>
          <div>   printf("a = %d\n", a);</div>
          <div>}</div>
        </div>
        <div><br>
        </div>
        <div>When I print "Sym" in gdb at the break point Stmt 1, I
          always get Sym as 0x0. This probably means that val is never a
          symbol for my test case and hence val.getAsSymbol() fails. I
          do not understand this. I would have thought that at least the
          expression x + y would be represented by a symbolic value such
          as $0. I tried doing const MemRegion *mem = val.getAsRegion()
          also at that  point and tried to print out mem in gdb. That
          also has a value 0x0 except for the printf statement. I cannot
          understand this too. I would have expected variables such as
          "x", "y" and "a" to be associated with a memory region and
          hence mem to have a non-null value at least at the points
          where y and a are being assigned to.</div>
        <div><br>
        </div>
        <div>My plan was to use Sym as the index into a custom map that
          I have created where I am storing the values of constants seen
          in the test case. I am unable to get this plan working since
          Sym is always 0x0.</div>
        <div><br>
        </div>
        <div>I have gone through the Checker Developer Manual. I am
          sorry to be asking specific questions about my code in this
          fashion, but, unfortunately, I am stuck at this point.</div>
        <div><br>
        </div>
        <div>Thanks.</div>
        <div><br>
        </div>
        <div>Regards,</div>
        <div>Venugopal Raghavan.</div>
      </div>
      <div class="gmail_extra"><br>
        <div class="gmail_quote">On Wed, Feb 1, 2017 at 11:13 PM,
          Aleksei Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
          wrote:<br>
          <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
            <div bgcolor="#FFFFFF" text="#000000">
              <div class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662moz-cite-prefix">Hello
                Venugopal,<br>
                <br>
                You will need to extract all the information from
                ExplodedNodes.<br>
                For example, state is a part of ExplodedNode. So, you
                can iterate over ExplodedNodes of graph using smth like:<br>
                for (auto Iter = G.nodes_begin(), E = G.nodes_end(); I
                != E; ++I) {<br>
                  ProgramStateRef State = I->getState();<br>
                  // Do the stuff with State<br>
                }<br>
                <br>
                <br>
                <br>
                <br>
                01.02.2017 12:19, Venugopal Raghavan пишет:<br>
              </div>
              <div>
                <div class="m_-1035519723042365625m_4390566528069532645h5">
                  <blockquote type="cite">
                    <div dir="ltr">Hi,
                      <div><br>
                      </div>
                      <div>I am registering my own map in the program
                        state using the the following:</div>
                      <div><br>
                      </div>
                      <div>REGISTER_MAP_WITH_PROGRAMSTATE<wbr>(ConstantMap,
                        SymbolRef, VariableConstVal)<br>
                      </div>
                      <div><br>
                      </div>
                      <div>where VariableConstVal is the structure
                        containing the information I want in this map. </div>
                      <div><br>
                      </div>
                      <div>I am populating this map in the
                        callback checkPostStmt() using state =
                        state->set<ConstantMap>(sym, ...) while
                        the state graph is being constructed.</div>
                      <div><br>
                      </div>
                      <div>At the end of analysis, I want to now read
                        the information stored in this map in the
                        callback checkEndAnalysis(Expl<wbr>odedGraph
                        &G, BugReporter &B, ExprEngine
                        &Eng). However, I am not sure how to get the
                        SymbolRef associated with an ExplodedNode which
                        is what I get when I iterate over the
                        ExplodedGraph at the end of the analysis.</div>
                      <div><br>
                      </div>
                      <div>How can I get the SymbolRef that I can use to
                        index into my map? In checkPostStmt(stmt* S,
                        CheckerContext &C), I used the following
                        code to get the SymbolRef that I can use to
                        store the information in the map:</div>
                      <div><br>
                      </div>
                      <div>
                        <div>  SVal val = state->getSVal(S, lctx);</div>
                        <div>  SymbolRef Sym = val.getAsSymbol();</div>
                      </div>
                      <div><br>
                      </div>
                      <div>but in checkEndAnalysis(ExplodedGraph &G,
                        BugReporter &B, ExprEngine &Eng) I do
                        not seem to have a handle to stmt* to get the
                        SVal.</div>
                      <div><br>
                      </div>
                      <div>I guess my question is probably not phrased
                        very well, but I hope some one can make some
                        sense out of it. Also, I guess I have a long way
                        to go before I understand the data structures in
                        the analyzer well. I checked the other checkers,
                        but none of them seem to exhibit exactly my
                        requirement.</div>
                      <div><br>
                      </div>
                      <div>Thanks.</div>
                      <div><br>
                      </div>
                      <div>Regards,</div>
                      <div>Venugopal Raghavan.</div>
                    </div>
                    <div class="gmail_extra"><br>
                      <div class="gmail_quote">On Wed, Jan 25, 2017 at
                        3:19 PM, Venugopal Raghavan <span dir="ltr"><<a href="mailto:venur2005@gmail.com" target="_blank">venur2005@gmail.com</a>></span>
                        wrote:<br>
                        <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
                          <div dir="ltr">Hi Aleksei,
                            <div><br>
                            </div>
                            <div>Thanks. I will check this.</div>
                            <div><br>
                            </div>
                            <div>Regards,</div>
                            <div>Venu.</div>
                          </div>
                          <div class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662HOEnZb">
                            <div class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662h5">
                              <div class="gmail_extra"><br>
                                <div class="gmail_quote">On Wed, Jan 25,
                                  2017 at 3:15 PM, Aleksei Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
                                  wrote:<br>
                                  <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
                                    <div bgcolor="#FFFFFF" text="#000000">
                                      <div class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-cite-prefix">Hello
                                        Venugopal,<br>
                                        <br>
                                        During analysis, you have access
                                        to a single path only. But after
                                        the analysis is done, you can
                                        summarize information across
                                        different paths using
                                        checkEndAnalysis() callback. You
                                        will get full ExplodedGraph
                                        built for the function so you
                                        will be able to look into its
                                        every node.<br>
                                        <br>
                                        <br>
                                        25.01.2017 09:25, Venugopal
                                        Raghavan via cfe-dev пишет:<br>
                                      </div>
                                      <blockquote type="cite">
                                        <div>
                                          <div class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944h5">
                                            <div dir="ltr">Hi,
                                              <div><br>
                                              </div>
                                              <div>Firstly, apologies
                                                for the long email
                                                below.</div>
                                              <div><br>
                                              </div>
                                              <div>I am new to the Clang
                                                Static Analyzer (CLA).
                                                My interest in CLA was
                                                more to see if I can
                                                solve quickly
                                                path-sensitive data-flow
                                                analysis problems than
                                                as a vehicle to build
                                                bug-finding checkers. I
                                                needed the solutions to
                                                such data flow problems
                                                to extract some
                                                behavioral properties
                                                from some test cases I
                                                have. For example,
                                                consider the following
                                                piece of code:</div>
                                              <div><br>
                                              </div>
                                              <div>if (cond) {</div>
                                              <div>   x = 4;</div>
                                              <div>}</div>
                                              <div>else {</div>
                                              <div>   x = 5;</div>
                                              <div>}</div>
                                              <div><br>
                                              </div>
                                              <div>L: .... = ...x..; //
                                                Use of variable x</div>
                                              <div><br>
                                              </div>
                                              <div>I want to identify
                                                program locations such
                                                as "L" in the code above
                                                where x is not a
                                                constant if you
                                                aggregate data-flow
                                                information across
                                                paths, but, on the other
                                                hand, is actually a
                                                constant if you have
                                                path-specific data flow
                                                information. Since CFA
                                                does path-specific
                                                analysis, I was curious
                                                to know if it would help
                                                me with such tasks. The
                                                "bug-report" I want at
                                                location L is that x has
                                                a value 4, given the
                                                path constraint for the
                                                path including the
                                                "then-path" of the if
                                                statement and that x has
                                                a value 5 along the
                                                else-path.</div>
                                              <div><br>
                                              </div>
                                              <div>I started writing a
                                                checker to accomplish
                                                the above task, but was
                                                quickly blocked by some
                                                basic doubts. My rough
                                                plan for the checker was
                                                to maintain a map in
                                                ProgramState which maps
                                                ProgramPoints (or, maybe
                                                program symbols) to
                                                constants when those
                                                variables indeed have
                                                constant values at the
                                                ProgramPoint. For
                                                example, when CFA
                                                expands states along the
                                                then-path and reaches
                                                "L", my map would say
                                                that at ProgramPoint
                                                "L", variable x has a
                                                constant value 4. Then,
                                                when CFA expands nodes
                                                along the else-path, I
                                                guess it would again
                                                create a state
                                                corresponding to L which
                                                now says that x has the
                                                constant value 5. I want
                                                to be able to catch this
                                                scenario where the same
                                                variable at the same
                                                ProgramPoint has two
                                                different constant
                                                values depending on the
                                                path taken.</div>
                                              <div><br>
                                              </div>
                                              <div>However, the issue is
                                                that, when the state
                                                graph along the
                                                else-path is expanded,
                                                it would no longer have
                                                any of the map contents
                                                that was built along the
                                                disjoint then-path. How
                                                then can I get access to
                                                the then-path
                                                information when I am
                                                expanding the path along
                                                the else-path? Since the
                                                checker is also required
                                                to be stateless, I
                                                cannot maintain
                                                auxiliary information in
                                                the checker that is
                                                persistent across
                                                multiple calls to the
                                                call-back function. </div>
                                              <div><br>
                                              </div>
                                              <div>Can you help me with
                                                this question? Maybe, I
                                                am trying to use CFA in
                                                ways it was not meant to
                                                be used viz. as a
                                                vehicle to solve data
                                                flow problems which
                                                consults information
                                                cutting across paths.
                                                Maybe, the CFA is meant
                                                to handle problems which
                                                require the examination
                                                of information
                                                restricted to single
                                                paths. Is that the case?
                                                Or, am I missing
                                                something?</div>
                                              <div><br>
                                              </div>
                                              <div>Thanks.</div>
                                              <div><br>
                                              </div>
                                              <div>Regards,</div>
                                              <div>Venugopal Raghavan.</div>
                                            </div>
                                            <br>
                                            <fieldset class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759mimeAttachmentHeader"></fieldset>
                                            <br>
                                          </div>
                                        </div>
                                        <pre>______________________________<wbr>_________________
cfe-dev mailing list
<a class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>
<a class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><span class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
</font></span></pre><span class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
    </font></span></blockquote><span class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
    

    <p>

    </p>
    <pre class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre>
  </font></span></div>

</blockquote></div>
</div>
</div></div></blockquote></div>
</div>



</blockquote>
<p>
</p><pre class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div>
</div>



</blockquote>
<p>
</p><pre class="m_-1035519723042365625m_4390566528069532645moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>