Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arbitrary buffers in analysis

On Tue, Aug 25, 2015 at 8:02 PM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:

>
> You are looking for the value analysis built-in Frama_C_interval_split,
> documented at
> http://blog.frama-c.com/index.php?post/2012/10/10/RERS-2012-competition-problems-1-9
> You will need to have the slevel option set high enough in conjunction
> with it for it to work properly.
>
>
Unfortunately, this builtin has been removed from the open source version
of Frama-C (probably around the same time as the one for dynamic allocation
alluded to earlier in this thread), because it was to be commercialized ---
including by a certain startup :-)


>
> It is not that clear-cut. You have information that the analyzer does not
> have: you know that a memory state with n equal to 1 is never included in a
> memory state with n equal to 2 and so on. The analyzer does not know that,
> and will at each statement of your program ask itself whether the new
> memory state it has just computed (including the binding of variable n to
> 2) is included in a memory state that it saw before (that included the
> binding of n to 1). This is just an example, but generally speaking the
> cost of larger analyses may be more than linear in the number of states the
> analyzer has to handle—though I did my best to ensure that it scales
> smoothly.
>

Indeed. I also want to emphasize this point, because as you inferred it is
the main reason why Tim's analysis requires so much time as is.

First, the algorithmic optimizations currently used to scale do not work
well with multiple loops. In fact, I would not be surprised if the analysis
time depended on the order in which sz and ksz are declared in the function
main. Second, only one of the two relevant datastructures is optimized.
Here, we are propagating simultaneously 64 * 128 distinct states, and the
inclusion tests have a quadratic complexity in that number.

Interestingly, most of those useless tests can be waived by rewriting the
main function in the following way:

//@ assigns p[0..size-1] \from \nothing; ensures
\initialized(&p[0..size-1]);
void init_buf(char *p, unsigned int size);

int run(unsigned int sz, unsigned int ksz)
{
    char kbuf[MAXKEYSZ];
    unsigned char buf[MAXBUFSZ], *pay;
    unsigned int paysz, i, work;
    int ok;

    /* init buf[0..sz-1] and kbuf[0..ksz-1] */
    init_buf(buf, sz);
    init_buf(kbuf, ksz);

    work = Frama_C_interval(0, MAXWORK);

    /*@ assert \initialized(buf + (0..sz-1)); */
    pay = NULL;
    paysz = 0;
    ok = auth(buf, sz, kbuf, ksz, work, &pay, &paysz);
    /*@ assert (ok == 0) || \initialized(pay + (0..paysz-1)); */

    if(ok) {
        /*@ assert \initialized(pay + (0..paysz-1)); */
        for(i = 0; i < paysz; i++)
            printf("%d\n", pay[i]);
    }
    return 0;
}

void main() {
  for (unsigned int sz=0; sz<MAXBUFSZ; sz++)
    for (unsigned int ksz=0; ksz<MAXKEYSZ; ksz++)
      run(sz, ksz);
}

Using the auxiliary function run ensures that the states for different
sizes are checked against each other only in a few statements of the
function main. This speeds up the analysis dramatically.

Also, while this is not strictly required, I completely rewrote the way buf
and kbuf are initialized. The call to the function init_buf has exactly the
same effect (w.r.t. the values in the buffer) as the loops previously used,
but is *much* more efficient.

Using this driver -- plus option -memexec-all, which speeds things up
significantly -- the analysis takes 55 minutes and proves everything except
the assertion
 /*@ assert \initialized(buf + (32..40)); */

This is good because
- I'm not convinced it is a true assertion
-  /*@ assert \initialized(buf + (32..39)); */  is sufficient, and can be
proven

Disclaimer: I used the development version of Frama-C for those
experiments, since a new release is forthcoming. This should have a limited
impact on the results of this particular analysis. One difference is in the
handling of ensures \initialized(&p[0..size-1]); Frama-C Sodium was less
efficient on this kind of annotation, and was precise only up to -plevel
array cells.

HTH,

-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150827/52794037/attachment.html>