contracts about memory mapped I/O through volatile memory locations

ID0002407: This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002407	Frama-C	Plug-in > wp	public	2018-10-31	2019-10-17

Reporter	jmaytac	Assigned To	correnson	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C 17-Chlorine	Target Version	-	Fixed in Version	-

Description :

We'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))

Attachments

• framaExample.tar.gz