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] WP-RTE on simple bitwise shift operation

Hello Quentin, 

We should probably add a simplifier for this operation. 
Let us see 2 possible solutions to this problem. 

First, try with Z3, sometimes you will get better results on bits operations. 
Here, I can discharge this proof obligations automatically with Z3 4.8.4 (even if it still takes about 8 seconds). 

Second, we can use the interactive theorem prover integrated to the GUI. 
Once your proof as failed, double click on the failed proof obligation, you'll get the proof obligation. 

Here, as you said: 

> If E1 has an unsigned type […], the value of the result is the integral part of the quotient of E1 / 2**E2.” 

And Alt-Ergo is often better at dealing with divisions than bits operation. 
So here for example you can select the term `lsr(x, 7)` and use the tactic "LogicalShift". 
This will basically replace the shift operation with a division, use the tactic by clicking on the green arrow. 

The two generated subgoals should be instantly proved. 

This proof can then be reused when replaying proofs. See the end of this SO reply: 

[ https://stackoverflow.com/a/63226309/4628125 | https://stackoverflow.com/a/63226309/4628125 ] 

Best regards, 
Allan 


De: "Quentin Santos" <qsantos at qsantos.fr> 
À: "Frama-c-discuss" <frama-c-discuss at lists.gforge.inria.fr> 
Envoyé: Samedi 19 Septembre 2020 16:36:26 
Objet: [Frama-c-discuss] WP-RTE on simple bitwise shift operation 



Hello everyone, 

I have recently been experimenting with Frama-C (21.1), and I noticed something surprising in the code below: the first function is automatically verified by Qed+Alt-Ergo, but not the second, no matter how many assertions I throw in. 

>From 6.5.7.5 of the C99 standard, “If E1 has an unsigned type […], the value of the result is the integral part of the quotient of E1 / 2**E2.”, so it's not about non two's complement representation, but division by 128 works as expected. 

The goal that could not be reached corresponds to the assertion that 0 ≤ (int)((int)x >> 7), although, 0 ≤ (int) x >> 7 is automatically verified (shouldn't the right-hand side expression already be of type int?). To add a layer to the mystery, both functions are verified if the shift is 1; if << 7 is used instead, both functions fail because of the assertion (int)x << 7 ≤ 2147483647. Is this a bug with Qed? Did I miss something? 

Thank you by advance for any advice. 
$ cat example.c 
unsigned int a(unsigned char x) { 
int y = x >> 7; 
return (unsigned int) y; 
} 
unsigned int b(unsigned char x) { 
return (unsigned int) (x >> 7); 
} 
$ frama-c -wp -wp-rte -warn-unsigned-downcast example.c -wp-print 
[kernel] Parsing example.c (with preprocessing) 
[rte] annotating function a 
[rte] annotating function b 
[wp] 4 goals scheduled 
[wp] [Alt-Ergo 2.3.3] Goal typed_b_assert_rte_unsigned_downcast_2 : Timeout (Qed:0.65ms) (10s) 
[wp] [Cache] found:2, updated:1 
[wp] Proved goals: 3 / 4 
Qed: 1 (0.64ms-0.82ms) 
Alt-Ergo 2.3.3: 2 (19ms-33ms) (28) (interrupted: 1) (cached: 2) 
[…] 
Goal Assertion 'rte,unsigned_downcast' (file example.c, line 6): 
Assume { Type: is_uint8(x). } 
Prove: 0 <= to_sint32(lsr(x, 7)). 
-- 
Best regards,
Quentin Santos 

_______________________________________________ 
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/20200920/b0ab839d/attachment.html>