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
- Subject: [Frama-c-discuss] arbitrary buffers in analysis
- From: boris at yakobowski.org (Boris Yakobowski)
- Date: Thu, 27 Aug 2015 00:01:22 +0200
- In-reply-to: <CAOH62Jg58aD+5Z4Hgv4ZtNff9giXZagoQgLj=L-TT3shQztfWw@mail.gmail.com>
- References: <CAGSRWbgQaaaBnjhBWamzidNa4Q+rqwoeJY9NDir98jebQFzmfQ@mail.gmail.com> <55D587D9.2080300@linux-france.org> <CAGSRWbg_bsifsWpGGb8Z0-40ZZbhW5aAOw-5L4Np+r0vrA2jbA@mail.gmail.com> <CAOH62Jg58aD+5Z4Hgv4ZtNff9giXZagoQgLj=L-TT3shQztfWw@mail.gmail.com>
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>
- Follow-Ups:
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- References:
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] arbitrary buffers in analysis
- Prev by Date: [Frama-c-discuss] my first frama verification
- Next by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Previous by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Next by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Index(es):