--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on April 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis loss of precision with bitwise XOR



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