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
- Subject: [Frama-c-discuss] Issue with obfuscated C code
- From: loic.correnson at cea.fr (Loïc Correnson)
- Date: Tue, 11 Jun 2019 17:33:35 +0200
- In-reply-to: <683894987.8901748.1560256473042.JavaMail.zimbra@irisa.fr>
- References: <683894987.8901748.1560256473042.JavaMail.zimbra@irisa.fr>
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>
- References:
- [Frama-c-discuss] Issue with obfuscated C code
- From: dorian.dumanget at irisa.fr (Dorian Dumanget)
- [Frama-c-discuss] Issue with obfuscated C code
- Prev by Date: [Frama-c-discuss] Issue with obfuscated C code
- Next by Date: [Frama-c-discuss] Help with using user-declared functions in preconditions
- Previous by thread: [Frama-c-discuss] Issue with obfuscated C code
- Next by thread: [Frama-c-discuss] Help with using user-declared functions in preconditions
- Index(es):