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] Issue with obfuscated C code

Hi,
You are facing several issues here.

First, your property is surely not compatible with the default arithmetic model, which requires to handle overflows with care !
Second, I’m not sure the property is the same when written for ACSL unbounded integers and on C bounded integers.
Beware that with Frama-C, (+) has not the same meaning in ACSL and in C unless there is no overflow nor downcasts !

Although WP has nice tactics to deal with bitwise operations, I’m afraid this kind of relation is out of reach. As Richard said, BV SMT solvers are better useful for such a purpose.

Finally, when dealing with SMT provers and axioms, you must be aware of how to generate instances of axioms. Here, you might want to instantiate your axiom on « x+y »
which would cause an infinite loop since it can be applied to its own result ! Typically, Alt-Ergo has no way to apply your axiom on every occurence of « x+y ».
It would be better to go into the other direction, let say :

1. define BVADD(x,y) := (x & y) + (x | y) with all the necessary casts
2. introduce axiom : \forall x,y; BVADD(x,y) = x+y ; // Here, Alt-Ergo will apply it on every occurence of BVADD(_,_)
3. now you can easily prove that BVADD(BVADD(x,y),z) = x+y+z ;

Example :






> Le 11 juin 2019 à 14:34, Dorian Dumanget <dorian.dumanget at irisa.fr> a écrit :
> 
> Hi,
> 
> I work on obfuscated C code and some operation have been reworked to made it hardly understandable. I had then to make them clearer for the different provers.
> I have proven that the operation 'a+b == (a&b) + (a|b)' for every 'int a' and 'int b' with '&' and '|' the bitwise operations.
> I then wanted every prover to "know" it and added it as an axiom.
> The issue is that I try to prove that 'a+b+c == (((a&b)+(a|b)) & c) + (((a&b)+(a|b)) | c)' but the provers can't reduce it with the axiom.
> 
> Is there a way to make it understandable to provers ? (I can't add it directly as axiom too because the same problem will occur with 'a+b+c+d')
> 
> Dorian.
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190611/5a5ff3a6/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: btrick.i
Type: application/octet-stream
Size: 486 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190611/5a5ff3a6/attachment.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190611/5a5ff3a6/attachment-0001.html>