--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t



Hi

I think need to add some general axiom aboud mod (not for safe_comp_not). Like this

axiom mod_axiom : forall x,y : int. ( (x < 0) and (y < x) ) or ( (x = 0) and (y <> 0) ) or ( (x > 0) and (y > x) ) -> (x = (x % y))

http://www.wolframalpha.com/input/?i=x%3Dmod%28x,y%29 seems legit

I also want to try validate this transforms from GCC https://gcc.gnu.org/viewcvs/gcc/trunk/gcc/simplify-rtx.c?view=markup&pathrev=232689#l2062

I hope Alt-Ergo can do this

21.03.2016, 09:12, "Mohamed Iguernlala" <iguer.pro at gmail.com>:
> Hi,
>
> Axioms about safe_comp_mod are in the model. However, axioms that
> give the behavior of to_uint8(i) when (0 <= i < 256) is not true are
> probably missing.
>
> I modified a little bit your C code (see below). I have one unproved VC,
> for which I get safe_comp_mod(i,256) = 44 in the model.
> An axiom like "A_1" would allow to conclude in this case.
>
> For the generic axiom, a case 0 <= i and i >= j is missing ...
>
> Regards,
> Mohamed.
>
> #include <stdio.h>
>
> // Proved by Alt-Ergo //
> /*@ requires (1 <= a <= 255);
>      ensures \result == 1;
> */
> int test_uint8_cast_mod256_eq (int a)
> { return ((a)%256 == (unsigned char)(a)); }
>
> // Proved by Qed //
> /*@ requires 300 <= a <= 300;
>      ensures \result == 1;
> */
> int test_uint8_cast_mod256_eq__v2 (int a)
> { return ((a)%256 == (unsigned char)(a)); }
>
> // Not Proved //
> /*@ requires 300 <= a <= 302;
>     ensures \result == 1;
> */
> int test_uint8_cast_mod256_eq__v3 (int a)
> { return ((a)%256 == (unsigned char)(a)); }
>
> int main (){
>   int b = 300;
>   printf("mod      = %d\n", b%256);
>   printf("unsigned = %d\n", (unsigned char) (b));
> }
>
> Le 21/03/2016 02:57, sztfg at yandex.ru a écrit :
>
>> I was trying to prove this code using alt-ergo: /* ALWAYS TRUE */ /*@ ensures \result == 1; */ uint8_t test_uint8_cast_mod256_eq (uint64_t a) { return ((a)%256 == (uint8_t)(a)); } how it looks like: goal test_uint8_cast_mod256_eq_post: forall i : int. is_uint64(i) -> (to_uint8(i) = (safe_comp_mod(i, 256))) but it failed. Maybe need to add some axioms related safe_comp_mod? Adding new axioms to .mlw file: axiom A_1 : forall i : int. (0 <= i) -> (to_uint8(i) = (safe_comp_mod(i, 256))) axiom A_2 : forall i : int. (0 <= i) -> (to_uint16(i) = (safe_comp_mod(i, 65536))) axiom A_3 : forall i : int. (0 <= i) -> (to_uint32(i) = (safe_comp_mod(i, 4294967296))) axiom A_4 : forall i : int. (0 <= i) -> (to_uint64(i) = (safe_comp_mod(i, 18446744073709551616))) ... and after that I can prove it. But maybe I doing something wrong, and this thing can be proved without adding axioms? Or maybe need to add more general axiom? I tried this axiom: axiom A_GENERIC : forall i,j : int. ((0 <= i) and (i < j)) -> (i = (safe_comp_mod(i, j))) but it doesn't work _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss