--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2019 ---
Hi David, Actually, SMT-provers do not need any axiom to prove your theorem as the SMT script below shows. ``` (set-logic QF_ABV) (set-info :smt-lib-version 2.0) (declare-fun a () (_ BitVec 32)) (declare-fun b () (_ BitVec 32)) (declare-fun c () (_ BitVec 32)) ;; a+b+c == (((a&b)+(a|b)) & c) + (((a&b)+(a|b)) | c) (assert (distinct (bvadd a b c) (bvadd (bvand (bvadd (bvand a b) (bvor a b)) c) (bvor (bvadd (bvand a b) (bvor a b)) c) ))) (check-sat) ``` Feeding that to Z3 gives me UNSAT, as expected. I guess you are using WP since you want to prove some kind of functional equivalence. Which SMT-solver do you rely on ? Alt-Ergo (default Frama-C WP SMT solver) is not the best for BitVector related stuff (Z3 is better, but solvers like Boolector or Yices are better, but are usually not used since they do not handle other useful theories) All in all, I would not be surprised if you were still encountering issues even with Z3 since, to the best of my knowledge, Frama-C's WP is not well suited to the kind of bitwise tricks you will encounter in obfuscated code, for its default theory used to encode the logical constraints will be based on (mathematical) integers ... On Tue, Jun 11, 2019 at 2:34 PM Dorian Dumanget <dorian.dumanget at irisa.fr> wrote: > > 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 -- Richard Bonichon