--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on August 2015 ---
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>