Hi Dave,
> On 26 Mar 2023, at 19:14, David Malcolm <dmalc...@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
