Re: -ftree-check for review

[Tom Tromey <tromey at redhat dot com>]

>>>>> "Sebastian" == Sebastian Pop <sebastian.pop@inria.fr> writes:

Sebastian> Here is the patch that implements the tree-checker proposed
Sebastian> by Nic for performing user-defined checks on the tree/CFG
Sebastian> form.

Hi Sebastian.  I think this is awesome -- I'm very happy to see static
analysis work being done in GCC.

I do have a number of questions and concerns about this though.
Mostly my concerns come from the idea that this is very important, and
hopefully will be widely used, so it would be nice to start on very
solid footing.

At the same time I don't want to go overboard and require everything
to be completely perfect.  I've listed everything I thought of here;
push back as necessary.

Sebastian> +Atomic syntactic patterns are plain C code fragments but possibly
Sebastian> +containing pattern variables.

I found the documentation somewhat confusing.  It seems to me that we
aren't really dealing with C code fragments exactly, but rather some
simpler, gimple-ized, variant.  Instead of mentioning C and atomic
patterns, how about trying instead to specify this language as its own
entity, and discussing how user source code will look to the checker?

My view is that the condate language is just that -- a new language --
and we've been burned a few times in the past in GCC with new
extensions that are not rigorously laid out.  It would be nice, for a
change :), to start with something tightly defined and even overly
strict on the parsing side, so that we have more room to mutate it
over time.  What do you think of this?

I'd like to see even more documentation than there currently is.  And,
there are various nits in the docs.  But perhaps these things can
comfortably be addressed as separate patches.

I'm a bit concerned about linking the checker syntax too tightly to
GCC's internal representation.  I suppose we just have to hope that
SSA is here to stay :).  However, at least the bit about using "0B" to
mean "NULL" seemed strange to me (not the "0" but the "B" I find
particularly perplexing).  This is the sort of thing that I would hope
would be addressed by the condate parser, so that users can write
something a bit more natural and not have to know every detail of
GIMPLE.  Likewise, suggesting that people use -fdump-tree-gimple in
order to see what patterns to write seems to tie things together too
much.

A few specific questions:

* Why allow unnamed condates at all?  I think always requiring some
  warning message is fine, and conversely that printing the index of
  the condate doesn't seem very user-friendly.

* Why have CONDMAX?  (I didn't generally try to review the code but
  this jumped out at me.)

* Do you have any information on using condates?  E.g., a paper
  comparing it to other technology (sparse?), or describing bugs found
  with it?  I'm just curious about this.

* Any plans or ideas for doing checks across function boundaries?

* Any thoughts about somehow exposing types to the check scripts?

Anyway, this is a great feature, and I think it will provide a big
benefit to GCC users.  I think that this deserves a news item on the
GCC web page once it goes in.

Tom