Hi Dave,

> On 26 Mar 2023, at 19:14, David Malcolm <dmalcolm@redhat.com> wrote:
> 
> I has looked into compiling those files with the patch some time ago;
> looking at my notes, one issue was with this on-stack buffer:
>    char extra[1024];
> declared outside the loop.  Inside the loop, it gets modified in
> various ways:
>    extra[0] = '\0';
> and
>    if (fread(extra, 1, extsize, fpZip) == extsize) {
> where the latter means "extra" becomes tainted.
> 
> However "extra" is barely used, and is effectively reset each time
> through the loop - but the analyzer doesn't figure that out.  So the
> loop analysis explodes, as it tries to keep track of the possibility
> that "extra" is still tainted from previous iteration(s), despite the
> fact that it's going to be clobbered before it ever gets used.
> 
> So one fix might be to extend the state-purging code so that it somehow
> "sees" that "extra" gets clobbered before it gets used, and thus we can
> purge the tainted state from it.

Thanks for your notes. I think we may be talking about the same thing? If you look at the updated proposal (I have changed it quite a lot since I first sent it out), you’ll see there is one relevant paper for state merging (although it is slightly different from state purging, I think the goal and general methodology is similar): https://dslab.epfl.ch/pubs/stateMerging.pdf 

I was trying to say if some similar situation happened for other types of checkers, I expected state explosion would also happen. I tried to construct a similar example (with the same kind of reset and nested conditionals + a loop) but for double-free, so far no success yet. I’ll pick it up afterwards, at latest by next Saturday, because I need to prepare for a coming midterm on Friday. I will also put this test case to the proposal because it seems like a very good starting point for the project.

Best,
Shengyu