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

Hello Tim and David,

On Fri, Aug 21, 2015 at 9:28 AM, David MENTRE <dmentre at linux-france.org>
wrote:

> Hello Tim,
>
> Le 20/08/2015 18:58, Tim Newsham a écrit :
>
>> It doesn't seem that will work to verify all buffer
>> sizes (for example, l=0xffffffffffffffff on 64-bit memory spaces).
>>
>
> Yes. For such big values, you might have more success with Deductive
> Verification, thus WP or Jessie plug-ins. But it is also a lot of more work
> to prove, e.g., absence of Run Time Error.
>
> The main advantage of Frama-C is that you can combine both techniques,
> i.e. Value Analysis and WP.


One relatively efficient technique for combining them could be this:

A/

Frama-C's value analysis supports memory blocks the size of which is not
known precisely. Any access to such a block beyond the first byte causes an
alarm to be emitted BUT the possibility that the memory access might be
valid is also taken into account.

One way to cause the creation of such a memory block by the analyzer was
malloc(Frama_C_interval(1, 0x7fffffff)). Unfortunately this doesn't work
any more with the open-source version because the built-in for malloc has
been removed. However, you can still declare an extern array with an
incomplete type, and this has some of the same effects.

(Note: the support for extern arrays with an incomplete type could
disappear too, because it singlehandedly causes a lot of special cases that
need to be taken into account in a lot of places in the analyzer, and
removing support for these variables would simply the analyzer a lot.
Anyway, in the current version, this support appears to be available, so
you can use this to get an idea of how the method works on small examples,
bearing in mind that you might encounter bugs that, if you report them,
might push the Frama-C developers to simply remove support for extern
arrays with an incomplete type.)

An example looks like this:

extern char t[];

int main(void){
  t[1] = 1;
  t[2] = 2;
  t[3] = 3;
  Frama_C_dump_each();
}

Analyzed, this produces:

$ frama-c -val t.c
...
[value] Computing initial state
t.c:1:[kernel] imprecise size for variable t
t.c:1:[value] warning: during initialization of variable 't', size of type
'char []' cannot be
                 computed (Size of array without number of elements.)
...
t.c:4:[kernel] warning: out of bounds write. assert \valid(&t[1]);
t.c:5:[kernel] warning: out of bounds write. assert \valid(&t[2]);
t.c:6:[kernel] warning: out of bounds write. assert \valid(&t[3]);
[value] DUMPING STATE of file t.c line 7
        t[0] ∈ [--..--]
         [1] ∈ {1}
         [2] ∈ {2}
         [3] ∈ {3}
         [4..4294967295] ∈ [--..--]
        __retres ∈ UNINITIALIZED
        =END OF DUMP==

Note how the analyzer did not assume that execution stopped when t[1] (and
then t[2] and t[3]) were accessed, although it emitted an alarm for them.
Because it had to take into account the possibility that these memory
locations were valid, it considered the possibility that execution
continued too (in this case the value at t[1] can only be 1).
The values displayed at Frama_C_dump_each() are of course only for the
executions that reach that point. Executions that have become stuck while
accessing memory illegally are not shown there because they stopped
earlier. So the analyzer guarantees that t[1] is 1 at that point.

If this is not clear, contrast with the behavior of the analyzer on the
same program where the array t is declared with a known size of 1 instead.

B/ Use any other Frama-C plug-in to verify the assertions generated by the
value analysis, including those about memory accesses that are caused by
the value analysis' unusual behavior for the array t.

The deductive plug-ins available for Frama-C may not completely handle all
aspects of dynamic allocation yet, but for the usecase being discussed, I
think that they already have pretty much all the features that are needed,
that is, the ability to reason symbolically about a valid block of size n.
I assume that the pre-condition \valid(&t[0 .. n-1]) would appear somewhere.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150821/782a148b/attachment.html>