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] Value analysis : How to use the value analysis plugin from another one ?

  • Subject: [Frama-c-discuss] Value analysis : How to use the value analysis plugin from another one ?
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Wed, 11 May 2011 21:48:59 +0200
On Tue, May 10, 2011 at 12:05 PM, florent garnier <florent.garnier at gmail.com
> wrote:

>
>  Thank you Anne for your fast and useful answer. Maxime and I made some
> progress,
>  and we reached the situation described below :
>
> We  can now :
>  _ Initialize the value analysis using the functions you were speaking
> about in your previous mail,
> _ We can pretty print those information using the API pretty printer, for
> any lvalue at any
> location.
>
> At a glance, we get some results which type is Cvalue_type.V and that
> encodes ranges
> of values, however we have no clue about how to get the information that
> follow :
>
> -> Gettng the infimum and the supremum bounds of this range of values.
> -> Getting the set of the elements whenever it is possible.
>
> Hi,

Warning for the others readers: very technical post. Moreover, it discusses
the current Caml representation of some parts of the value analysis, and
some bits may evolve one day.


As you said, values at a given location are indeed of type Cvalue_type.V,
but this type is itself an alias for Locations.Location_Bytes.t (also in
src/memory_state). A lot of useful functions are contained in
Location_Bytes, and there is an mli to abstract a few things. After some
steps of definition unfolding, you can deduce the following facts:

Roughly speaking, a value is a map from a set of bases to some offsets.
Alternatively, it can be a Top, with the origin of the imprecision, but I
will not detail those here.

- the bases are all the variables of the program, plus the NULL one, and the
constant strings of the program; see ai/base.ml. Hence there are only a
finite number of bases, and the map itself has a finite support. The NULL
base is used to encode standard integers, or alternatively absolute memory
adresses; however there is no difference in the representation of the two.

- the offsets have value Ival.t (in ai/ival.ml), which is an alias for
Ival.tt. These are either
  * (finite) sets of arbitrary precision integers, by the constructor 'Set
of O.t'.  O.t is also Abstract_interp.Int.t, itself being ultimately
Bigint.t
  * sets of floats, by the constructor 'Float of Float_abstract.t'.
Float_abstract.t is abstract, and currently encodes intervals of floats.
  *potentially infinite sets of arbitrary precision integers, by the
constructor 'Top of Abstract_interp.Int.t option * Abstract_interp.Int.t
option * Abstract_interp.Int.t * Abstract_interp.Int.t'. The first option is
the min (None if minus_infinity), the second option is the max (None if
plus_infinity). The last two ints are used to encode 'modulo' sets.

As an example, using a lot of hopefully clear notations,
NULL -> (]-infty;+infty[ | 1 mod 64); &g-> {0; 4} ; "abc" -> {2}; &h ->
[0...+\infty[ represents the value that can be
- all the integers that have a remainder of 1 in a modular division by 64
- the address of the variable g, and the address of g+32 bits (for example
&g+1 is g has type int on a 32 bits platform)
- the character 'c' in the constant string "abc", ie. &abc+2 bytes
- the address of the variable h shifted by any positive amount

A few remarks:
* some things in the representation make no sense, eg. &g -> [-1.3...1.5]
* integers (ie. values based on the NULL base) must be taken as is, while
offsets from variables are in numbers of bytes
* Most of the times, you won't see infinity in the pretty-printed values.
Frama-C use the variable storage information to deduce the interval range,
ie -128..127, 0..65535, etc.

So, to start answering your questions, what you want to obtain does not
exist in general. What you should do is use the various iterators (fold,
mainly) provided by all the structures above to traverse the Caml value.
While doing so, raise an exception when there is a subvalue that you cannot
handle ---be it floats, one of the various Top, etc. And the accumulator of
those folds should be your result.

Now, for prototyping, or because your are sure your are in a favorable case,
you can use one of the pre-written functions that make assumptions on the
shape of its arguments. For example, Cvalue_type.V.project_ival takes a
value and return an Ival.t. It makes the hypothesis that its argument is
purely an integer range, ie. purely based on the NULL base. Then you can
combine it with eg. Ival.min_int which will give you the min of an Ival.t if
it exists. If you detect that the range of integer is finite, because
project_ival returned a constructor Set, you can enumerate the different
values using Ival.O.fold.

Note that project_ival will raise Not_based_on_null if its argument is not
an integer, while min_int can return None if its argument is unbounded, and
raise Error_Bottom if its argument is Ival.bottom. You will still need to
decide what to do in some of those cases. Typically, unbounded sets can
appear even in very constrained programs.

Hope this helps, and was understandable.

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