Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002407Frama-CPlug-in > wppublic2018-10-31 02:302018-10-31 14:50
Reporterjmaytac 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 17 Chlorine 
Target VersionFixed in Version 
Summary0002407: contracts about memory mapped I/O through volatile memory locations
DescriptionWe've attached a small example in which a state machine communicates a peripheral through a volatile variable , on line 6 of constants.h:
volatile uint32_t rxBuffer;

The state of the machine is held by a struct mac, declared on line 21 of mac.h:
struct mac {
   mac_packet_t mac_packet;
   MessageType latestMessage;
   mac_bridge_t MAC_BRIDGE_A;
}

the mac_bridge_t represents the machine's memory mapped I/O interface, as declared on line 15 of mac_bridge.h:
struct mac_bridge
{
   volatile uint32_t *cmd_rx_buffer;
}

on line 13 of main.c,

   mac_t mac = the_mac();

mac becomes a pointer to singleton_mac instance of struct mac declared on line 8 of mac.c and returned by the function the_mac() defined on line 17 of mac.c. On line 14 of main.c,

   mac->MAC_BRIDGE_A = theMacBridge();

 mac's IO interface MAC_BRIDGE_A becomes the singletonMacBridgeA instance of struct mac_bridge returned by the function theMacBridge() defined on line 11 of mac.c

mac_bridge_t theMacBridge() {
   singletonMacBridgeA.cmd_rx_buffer = &rxBuffer;
   return &singletonMacBridgeA;
}

thus, mac has as MAC_BRIDGE_A singletonMacBridgeA whose cmd_rx_buffer is a reference to the volatile rxBuffer. The volatile rxBuffer reads and writes from ghost state as given on line 7 of constants.h:

//@ ghost uint32_t injectorAPBBuffer[4294967296];
//@ ghost uint32_t injectorAPBBufferCount=0;

/*@ ghost //@ requires buffer == &(rxBuffer);
  @ uint32_t readsBuffer(volatile uint32_t *buffer) {
  @ static uint32_t injectorAPBBufferCount = 0;
  @ for (int i=0; i<4294967296; i++) {
  @ injectorAPBBuffer[i%4294967296]=i%42949967296;
  @ }
  @ if (buffer == &(rxBuffer)) {
  @ return injectorAPBBuffer[injectorAPBBufferCount++];
  @ }
  @ else
  @ return 0;
  @ }
  @ */

//@ ghost uint32_t bufferAPBCollector[4294967296];
//@ ghost uint32_t bufferAPBCollectorCount = 0;

/*@ ghost //@ requires buffer == &(rxBuffer);
  @ uint32_t writesBuffer(volatile uint32_t *buffer, uint32_t v) {
  @ if (buffer == &(rxBuffer)){
  @ return bufferAPBCollector[(bufferAPBCollectorCount++)%64] = v;
  @ }
  @ else {
  @ return 0;
  @ }
  @ }
@*/
//@ volatile (rxBuffer) reads readsBuffer writes writesBuffer;

mac implements a transition system driven by an alphabet of labels obtained through calls to macbridge_get_packet, defined on line 3 of mac_bridge.c

mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge)
{
   mac_packet_t received_packet={0};
  received_packet.object_high=(uint8_t)(*(mac_bridge->cmd_rx_buffer));
  return(received_packet);
}


when the given macbridge_t is the reference to the singletonMacBridgeA, we want this function to have as postcondition that the packet this function returns has the value found in the appropriate ghost state
/*@
  behavior A:
  assumes mac_bridge == &singletonMacBridgeA;
  ensures \result.object_high == (uint8_t)injectorAPBBuffer[(injectorAPBBufferCount-1)%4294967296];
*/
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge);

The resulting Alt-ergo doesn't seem to capture the post-condition.

(* ---------------------------------------------------------- *)
(* --- Post-condition (file mac_bridge.h, line 24) in 'macbridge_get_packet' --- *)
(* ---------------------------------------------------------- *)

goal macbridge_get_packet_post:
  forall t : int farray.
  forall t_1 : (addr,int) farray.
  forall t_2 : (addr,addr) farray.
  forall a : addr.
  let a_1 = shiftfield_F7_mac_bridge_cmd_rx_buffer(a) : addr in
  let a_2 = t_2[a_1] : addr in
  let x = t_1[a_2] : int in
  (region(a.base) <= 0) ->
  framed(t_2) ->
  linked(t) ->
  valid_rd(t, a_1, 1) ->
  is_uint32(x) ->
  valid_rd(t, a_2, 1) ->
  (x = to_uint8(x))

TagsNo tags attached.
Attached Filesgz file icon framaExample.tar.gz [^] (2,585 bytes) 2018-10-31 02:30

- Relationships

-  Notes
(0006675)
correnson (manager)
2018-10-31 14:50

Your approach in using explicit volatile reads & writes clauses is good one.

However, without using the Volatile plug-in, these clauses are _not_ taken into account by Frama-C kernel, and access to volatile memories simply leads to introduce random values (aka: fresh variables) into the proof obligations.

The Volatile plug-in is not part of the open-source distribution.
Please contact us for dedicated support if you need so.

- Issue History
Date Modified Username Field Change
2018-10-31 02:30 jmaytac New Issue
2018-10-31 02:30 jmaytac Status new => assigned
2018-10-31 02:30 jmaytac Assigned To => correnson
2018-10-31 02:30 jmaytac File Added: framaExample.tar.gz
2018-10-31 14:50 correnson Note Added: 0006675


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker