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 loss of precision with bitwise XOR

  • Subject: [Frama-c-discuss] Value analysis loss of precision with bitwise XOR
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Thu, 6 Apr 2017 16:42:36 +0200
  • In-reply-to: <87a87tabwh.fsf@is230028.cea.fr>
  • References: <CAK2NOcXuRwwjxwBdfK5HMXwGaLSpmbgLWi1SaRS4Lng8=fDWQg@mail.gmail.com> <87a87tabwh.fsf@is230028.cea.fr>
Hi Sergio,

As explained by Matthieu, to prove your first program you need some
relational information between topBitOnly and something -- at least for the
highest bit. For now, you can sucessfully analyse this function by
- adding an annotation that will force the analyser to proceed by case
analysis
- have enough slevel (here, 2)
- use the bitwise domain : -eva-bitwise-domain

Here is the full code, and the full command-line:

int isTopBit(unsigned something)
{
  //@ assert something >= 0x80000000 || something < 0x80000000;
  unsigned topBitOnly = something & 0x80000000;
  Frama_C_show_each_1(something,topBitOnly);
  something ^= topBitOnly;
  Frama_C_show_each_2(something,something & 0x80000000,topBitOnly);
  if (something & 0x80000000) {
    Frama_C_show_each_true(something);
    return 0;
  }
  else {
    Frama_C_show_each_false(something);
    return 1;
  }
}

frama-c -val ~/c/bitw.c -main isTopBit -slevel 2 -eva-bitwise-domain
-big-ints-hex 256
# Option -big-ints-hex is helpful to understand bitmasks

Reading the code of the abstract transformers for xor, I noticed a few
cases that are currently handled imprecisely cases. In the future, it might
be possible to analyse this example by adding only the assertion.

Hope this helps,




On Thu, Apr 6, 2017 at 3:44 PM, Matthieu Lemerre <matthieu.lemerre at cea.fr>
wrote:

>
> Dear Sergio,
>
> The loss of precision is normal: abstract-interpretation based analyzers
> compute only over-approximations of the possible values of a program, as
> computing the exact set of these values is undecidable.
>
> Here, the specific issue comes from the default abstractions of the Frama-C
> Value analysis, which is an interval of value. In the second example, we
> can deduce that:
>
> 0 <= something & 0x7FFFFFFF < 0x80000000
>
> i.e. that the highest 5 bits are cleared.
>
> And thus that (something & 0x7FFFFFFFFF) & 0x80000000 is false.
>
> The first example is much more complex to prove, because it relies on a
> relation between topBitOnly and something (i.e. that a specific bit has
> the same value on both variables). The default abstraction of Values
> cannot prove this.
>
> One way to work around this problem would be to perform a case split at
> the beginning of the function on the value of this bit in something, and
> use another abstraction that records the possible values for each bit in
> a bitvector -- but I don't remember if this abstraction was incorporated
> in Eva.
>
> Best,
> Matthieu
>
>
>
>
> Sergio Feo <sergio.feo at gmail.com> writes:
>
> > Dear all,
> > We have encountered the issue that Frama-C value analysis loses precision
> > when dealing with bitwise xor operations. Consider the following program:
> >
> > int isTopBit(unsigned something)
> > {
> > unsigned topBitOnly = something & 0x80000000;
> > something ^= topBitOnly;
> > if (something & 0x80000000) {
> > Frama_C_show_each_true(something);
> > return 0;
> > }
> > else {
> > Frama_C_show_each_false(something);
> > return 1;
> > }
> > }
> >
> > Here, the _if_ branch is dead code, since the lines before clear the bit
> > that is tested as the if condition. However, Frama-C outputs the
> following:
> >
> > [value] Called Frama_C_show_each_true([0..4294967295])
> > [value] Called Frama_C_show_each_false([0..4294967295])
> > [value] Recording results for isTopBit
> > [value] done for function isTopBit
> > [value] ====== VALUES COMPUTED ======
> > [value] Values at end of function isTopBit:
> >   something ∈ [--..--]
> >   topBitOnly ∈ {0; 2147483648}
> >   __retres ∈ {0; 1}
> >
> > Modifying the program to achieve the same result without the XOR
> operation
> > as in:
> >
> > int isTopBit(unsigned something)
> > {
> > something &= 0x7fffffff;
> > if (something & 0x80000000) {
> > Frama_C_show_each_true(something);
> > return 0;
> > }
> > else {
> > Frama_C_show_each_false(something);
> > return 1;
> > }
> > }
> >
> > then we obtain the following:
> >
> > [value] Called Frama_C_show_each_false([0..2147483647])
> > [value] Recording results for isTopBit
> > [value] done for function isTopBit
> > [value] ====== VALUES COMPUTED ======
> > [value] Values at end of function isTopBit:
> >   something ∈ [0..2147483647]
> >   __retres ∈ {1}
> >
> > which is the result we would expect from both versions.
> >
> > Could you provide a pointer to the reasons why the abstract transformer
> for
> > the bitwise XOR behaves in this particular way?
> >
> > Thanks a lot!
> >
> > -- Sergio
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss




-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170406/5cb51a19/attachment-0001.html>