Re: [GSoC][Static Analyzer] Ideas for proposal

[David Malcolm <dmalcolm@redhat.com>]

On Tue, 2023-02-28 at 15:46 +0100, Shengyu Huang wrote:
> Hi Dave,
> 
> > On 22 Feb 2023, at 15:11, Shengyu Huang <kumom.huang@gmail.com>
> > wrote:
> > 
> > > But a better place to look would probably be in our bugzilla; see
> > > the
> > > links on the wiki page:
> > >  https://gcc.gnu.org/wiki/StaticAnalyzer 
> > > The "open bugs" list currently has 41 "RFE" bugs ("request for
> > > enhancement" i.e. ideas for new features), some of which might
> > > make
> > > suitable GSoC ideas, and/or be of interest to you (ideally both!)
> > > 
> > > Also, the GSoC wiki page has some project ideas:
> > >  https://gcc.gnu.org/wiki/SummerOfCode#Selected_Project_Ideas
> > > 
> > 
> > Yeah I was also searching for interesting ideas on the bugzilla,
> > and I will communicate to you once I have any more concrete ideas.
> 
> I spent some time searching through Bugzilla this weekend while
> familiarizing with the analyzer internals, and I found the following
> things interesting, and it’d be great if you can give me some
> preliminary feedback:

Great; thanks.

> 
> 1. I am not sure why we added the class
> `shift_count_negative_diagnostic` in region-model.cc
> <http://region-model.cc/>, because there is a similar warning issued
> from c/c-typeck.cc <http://c-typeck.cc/>, and when I compiled with -
> fanalyzer that has the code `b = b << -1`, I got two warnings that
> mean the same thing. 

The analyzer works based on execution paths, and so can potentially
find more things that a purely AST-based approach.  That said, I'm not
happy with the signal:noise ratio of that analyzer warning; maybe it
needs some tuning?

> Maybe interestingly, when I compiled my test case with -O2, I got the
> warning from -Wshift-count-negative but not from -Wanalyzer-shift-
> count-negative. Would it be considered as a false negative for the
> analyzer? 

The analyzer runs relatively late compared to most analyzers, on the
gimple-ssa representation after some optimizations have already run, so
that's probably why you didn't get the warning at -O2.

> 
> 2. Something related to 1. is PR98447
> (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=98447)


> 
> 3. PR104955 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104955)
> still takes a long without -Wno-analyzer-double-free. I’d be
> interested in further investigating the problem (probably as you said
> sharing one feasible_graph can fix the problem).

That one involves deep surgery that could affect every analyzer
warning, so I'm worried that it could turn out to be too hard to do as
a first project on the analyzer.  Also, some warnings that have grown a
pending_diagnostic::check_valid_fpath_p vfunc since I wrote that
comment, which could complicate the implementation :-/

> 
> 4. What’s the most interesting to me are PR103533
> (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=103533),

Turning on taint detection by default would be a great project.  It
would be good to run the integration tests:
  https://github.com/davidmalcolm/gcc-analyzer-integration-tests
to see if anything regresses, or if it adds noise - so this might be a
bit of an open-ended project, in that we'd want to fix whatever issues
show up there, as well as the known ones that are documented in that
bug.


>  PR104940 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940)

I've actually been prototyping SMT solver support in a private branch,
but based on writing out SMT-LIB scripts and invoking z3 as a
subprocess, and parsing the results, which is much slower than it could
be, as I'm reevaluating all the constraints as each one is added,
rather than using an API and sharing/pushing/popping state.

Taking my SMT prototype and turning it into something usable could be a
good project, I think.  I'll look at posting what I've got somewhere
public if you're interested.

> because I focus on formal methods in my university studies, and I’m
> currently looking into Dafny internals for my semester project.
> 
> 5. PR105891 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105891)
> seems fitted to get started during the project phase, or be used as a
> warm-up before the official project phase.

Yeah, but probably would only count as part of full GSoC project.  Last
year Tim Lange did a highly successful GSoC project on the analyzer
which was a grab-bag of adding various new warnings, each of which
wasn't quite a full project.

Could be a good warmup; though I wonder what would show up when running
it on real world C examples (e.g. via my integration test suite).

> 
> 6. PR106147 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=106147)
> says you are implementing a prototype already, so I guess I’ll leave
> it out, but I am also quite interested in this analysis. 

GCC 13 has the infinite recursion detection, but I didn't get the
infinite loop detection ready before feature freeze.

If you're interested, I can post my prototype of the latter if you or
someone else wants to take it up and finish it.

> At a glimpse I am not quite sure why infinite recursion and infinite
> loop should be treated differently (maybe it’ll become clearer to me
> once I am more familiar with the internals). In addition, a simple
> function that looks like this
> 
> void re (int c)
> {
>   if (c > 0)
>     re (c + 1);
>   else
>     re (1);
> }
> 
> can also be concluded as infinite recursion because there is no base
> case in all possible paths.

Bother, we don't complain about that yet; so fixing that could be part
of a GSoC project, and would be a good fit with the infinite loop idea.

FWIW I'm about to commit a fix for
  https://gcc.gnu.org/bugzilla/show_bug.cgi?id=108935
(assuming it passes testing) so the inf-recursion warning is about to
change implementation slightly.

> 
> 7. Other PRs that interest me: PR106006
> (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=106006) 

i.e.  RFE: analyzer should treat data from a socket as "tainted" 

This might work well with the "Turning on taint detection by default"
project (PR103533).


> and PR107017 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=107017,
> already mentioned in the GSoC page).

i.e. "RFE: support printf-style formatted functions in -fanalyzer"

yeah, having someone work on this would be most welcome.


Hope this is helpful; I think there are quite a few viable GSoC
projects in the above.

Thanks
Dave