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: matthieu.lemerre at cea.fr (Matthieu Lemerre)
  • Date: Thu, 06 Apr 2017 15:44:30 +0200
  • In-reply-to: <CAK2NOcXuRwwjxwBdfK5HMXwGaLSpmbgLWi1SaRS4Lng8=fDWQg@mail.gmail.com>
  • References: <CAK2NOcXuRwwjxwBdfK5HMXwGaLSpmbgLWi1SaRS4Lng8=fDWQg@mail.gmail.com>
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