0002401: Newer releases of FramaC produce apparent WP plug-in bug

(0006650)
jmaytac (reporter)
2018-10-02 00:39

We've attached just now an even smaller example producing the bug, where the ACSL definition of the involved logic function is to be found on line 21 of mac.h
/*@
logic boolean isAMessage(mac_t mac) = (mac->mac_packet.object_high == 0x0A);
*/

and the altergo produced is on line 5 of Axiomatic11.ergo
function L_isAMessage() : bool = eqb(#{w_0}, 10)

(0006653)
correnson (manager)
2018-10-02 10:43
edited on: 2018-10-02 10:44

After *much further reduction* the bug can be reduced to:

/* Generated by Frama-C */

typedef struct {
   unsigned char object_high ;
} mac_packet_t ;

typedef struct mac {
  mac_packet_t volatile mac_packet ;
} *mac_t;

/*@
logic 𝔹 isAMessage{L}(mac_t mac) =
  \at(mac->mac_packet.object_high ≡ 0x0A,L);

*/

/*@ behavior NO:
      assumes mac->mac_packet.object_high ≢ 0x0A;

    behavior A:
      assumes isAMessage(mac) ≡ \true;

    complete behaviors A, NO;
    disjoint behaviors A, NO;
*/
int mac_getBusMsg(mac_t mac)
{
  return 0;
}

The problem comes from the **volatile** field of structure mac, which is read from a logic function.

Reading something volatile inside a logic term has absolutely *NO* concrete meaning in ACSL.
The WP generates fresh variables (aka: random values) when accessing volatiles from logic, in an attempt of remaining consistent. This strategy fails when being inside a logic function body since those variables escape any definition scope.

In previous versions of Frama-C/WP, accessing volatiles inside logic was silently accepted with an inconsistent semantics ;-)

However, I agree that such such a situation shall be detected with a more user-friendly error message!

(0006654)
correnson (manager)
2018-10-02 10:44

Frama-C / WP shall properly detect and reject access to volatile locations inside body of logic function and predicates.

(0006655)
correnson (manager)
2018-10-02 10:45

Workaround: you can use -wp-no-volatile option to (inconsistently) ignore all volatile flags.

Issue History
Date Modified	Username	Field	Change
2018-10-01 10:01	jmaytac	New Issue
2018-10-01 10:01	jmaytac	Status	new => assigned
2018-10-01 10:01	jmaytac	Assigned To	=> correnson
2018-10-01 10:01	jmaytac	File Added: framaBug.tar.gz
2018-10-02 00:39	jmaytac	Note Added: 0006650
2018-10-02 00:40	jmaytac	File Added: frmaBug.tar.gz
2018-10-02 08:36	virgile	Relationship added	has duplicate 0002403
2018-10-02 08:40	virgile	View Status	private => public
2018-10-02 10:43	correnson	Note Added: 0006653
2018-10-02 10:44	correnson	Note Edited: 0006653	View Revisions
2018-10-02 10:44	correnson	Note Added: 0006654
2018-10-02 10:44	correnson	Status	assigned => acknowledged
2018-10-02 10:45	correnson	Note Added: 0006655

Notes
(0006650) jmaytac (reporter) 2018-10-02 00:39	We've attached just now an even smaller example producing the bug, where the ACSL definition of the involved logic function is to be found on line 21 of mac.h /@ logic boolean isAMessage(mac_t mac) = (mac->mac_packet.object_high == 0x0A); / and the altergo produced is on line 5 of Axiomatic11.ergo function L_isAMessage() : bool = eqb(#{w_0}, 10)

(0006653) correnson (manager) 2018-10-02 10:43 edited on: 2018-10-02 10:44	After much further reduction the bug can be reduced to: /* Generated by Frama-C / typedef struct { unsigned char object_high ; } mac_packet_t ; typedef struct mac { mac_packet_t volatile mac_packet ; } mac_t; /@ logic 𝔹 isAMessage{L}(mac_t mac) = \at(mac->mac_packet.object_high ≡ 0x0A,L); / /@ behavior NO: assumes mac->mac_packet.object_high ≢ 0x0A; behavior A: assumes isAMessage(mac) ≡ \true; complete behaviors A, NO; disjoint behaviors A, NO; / int mac_getBusMsg(mac_t mac) { return 0; } The problem comes from the volatile field of structure mac, which is read from a logic function. Reading something volatile inside a logic term has absolutely NO concrete meaning in ACSL. The WP generates fresh variables (aka: random values) when accessing volatiles from logic, in an attempt of remaining consistent. This strategy fails when being inside a logic function body since those variables escape any definition scope. In previous versions of Frama-C/WP, accessing volatiles inside logic was silently accepted with an inconsistent semantics ;-) However, I agree that such such a situation shall be detected with a more user-friendly error message!

(0006654) correnson (manager) 2018-10-02 10:44	Frama-C / WP shall properly detect and reject access to volatile locations inside body of logic function and predicates.

(0006655) correnson (manager) 2018-10-02 10:45	Workaround: you can use -wp-no-volatile option to (inconsistently) ignore all volatile flags.