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] How Jessie plug-in handles aliasing of pointers

Hi Stephen,

-- Stephen Siegel (2013-10-26)
> Thanks, Yannick, that's very interesting and I will loop up the papers.

You're welcome.

> I have been playing around with this example to see how well Frama-C/Jessie/Why... is able to deal with pointers and aliasing.  Below is a variation in which I believe the contract for f holds but I can't verify it.

I suggest that newt time you start a new thread for another issue like this one, as it may interest other people. I'll answer about the Jessie plug-in, but others will probably have more things to say about the WP plug-in.

The fact that Frama-C cannot verify the code you sent is expected with Jessie. As with many properties that you can figure out in a few seconds on a few lines of code, the analyzer here cannot reach the precision of the human, because it was designed to scale to much larger programs, so the analysis it does on your small program cannot be as precise as if it was designed for analyzing as precisely as possible 10 lines of code.

This is particularly true for pointer analysis, which has quickly a prohibitive cost as soon as you grow your program. This is one of the reasons why a simple alias analysis was chosen in Jessie, which is described in section 4.1 "Inferring regions: a type-based approach" of this paper: http://hal.inria.fr/inria-00534331/en/ (maybe there are better more recent references, I point to one I know because I wrote it!)

With this analysis, the pointers p, q, \result of choosePtr end up in the same "region" (so they're potentially aliased for Jessie unless you prove otherwise), because you're comparing them with "==", while the pointers p and q of doNothing2 end up in two different regions (so they cannot be aliased from the point of view of Jessie).

> If you comment out the call to choosePtr, the verification goes through fine.  Frama-C/... correctly figures out that the pointer p must point to k1 or k2 and therefore cannot affect i, j, n, or m.  Pretty smart.   

I find it smart too! That's the result of the analysis done in Jessie, based on the work of Hubert and March?, see subsection 4.1.2 of the above paper for details.

> However if you keep the call to choosePtr in the code, I can't verify the VCs with anything (at least, so far, giving big time limits to all the provers).

That's a result of the imprecision of the alias analysis used, which unifies the regions of k1, k2, i and p. I would expect that, in your small program, the VC would still be provable if you add to the loop invariant of the inner loop that i does not change, because it should be known that &i is different from &k1, &k2 and &p. Try adding "i = i at start" with start a label that you add before the inner loop in the loop invariant.

> I don't think that call should affect anything since the contract to choosePtr says "assign \nothing" and the result of this call is not even used.  

The thing it affects is the separation of memory into distinct regions, which has an influence on which VCs are generated.

> Note that the call doNothing2 does not cause any problems.

Yes, as I indicate above, it does not lead to any unification of regions, so it's a noop from this point of view.
--
Yannick Moy, Senior Software Engineer, AdaCore