Re: [GSoC][Static Analyzer] First proposal draft and a few more questions/requests

[Shengyu Huang <kumom.huang@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3963 bytes --]

Hi Dave,

> Overall, it looks great.  Some notes:
> - maybe specify the *GCC* static analyzer you first mention it

Done.

> - you talk about "timeout" warnings.  The analyzer already can emit a
> "timeout" warning of sorts, via -Wanalyzer-too-complex, though this is
> based on the complexity of the exploded graph (e.g. # of nodes), rather
> than actual timings.  Is the latter the kind of thing you had in mind,
> or where you thinking about ways of making the "too complex" heuristics
> smarter?  (I confess that you seem much more familiar with the theory
> of this than I am!)

I was not ware of `-Wanalyzer-too-complex` when I wrote that proposal, and I forgot to rewrite this part. I planned to ask you why we did not turn on this flag by default. To avoid state explosion altogether, it is for sure that we need to bear with false positives in some cases. I am not yet sure what is a good approach to balance the soundness and completeness in symbolic execution, but my intuition (just based on my limited experience with other kinds of formal methods) is that we don’t want to avoid state explosion in all cases because we want to have more precision (that is, we don’t want too many false positives). Imagine a dummy static analyzer that just reports warnings regardless the program. It will not have any state explosion problems, but it will have lots of false positives. Therefore, I think we should consider turning it on by default. Maybe you have other considerations that I missed?

Another point but irrelevant for this project is that we will surely encounter timeout when we integrate SMT solvers in the future (I don’t know whether it is the plan for GCC14). It is just unavoidable…the current approach does not sound transferable to the timeout issued by, say, Z3. Maybe we want a unified approach at some point?

Anyway, this part does not seem too urgent anymore after I know the flag -Wanalyzer-too-complex exists…if you have some working solution in terms of how to handle timeout from SMT solvers, I’d be happy to know.

> - the numbering of your references seems to have gotten out-of-sync; I
> see references to [3] as a paper "Schwartz et al", but that's a link to
> one of my blog posts.

Thanks for letting me know that. Indeed I forgot to fix the numbering after adding your blog to the references.

> - do you a link to a github account, or somewhere else that
> demonstrates code you've written?  In particular, how is your C++ ?
> 

My Github account is https://github.com/kumom, but I would not post any code from my course projects there since it will violate honor code and promote plagiarism (I will attach a small? lab project to you in another private email). I have taken courses like systems programming and computer architecture, where I wrote plenty of C code and some C++ code. For C++, I’ve written maybe just a few thousand lines of code. Unfortunately, in all my previous jobs as student assistant where I coded mainly in Python and TypeScript, my code was neither open source nor owned by me…Now I am working on a semester project (on formal verification) using Dafny and a course project (on compiler design) using Scala, but I admit they are a bit far from C++. I have planned to read Effective C++ after the Easter break before you raised this question, but maybe you can recommend something else that you find helpful. Since I am relative familiar with programming language concepts in general, I believe I will get more fluent at C++ within a short amount of time once I get my hands dirty.

> Note that the deadline for submitting proposals to the official GSoC
> website is April 4 - 18:00 UTC (i.e. this coming Tuesday) and that
> Google are very strict about that deadline; see:
> https://developers.google.com/open-source/gsoc/timeline

Thanks for the reminder. I have kept this in mind and will submit it before the deadline.

Best,
Shengyu