Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2601
Closed
Open
Issue created Mar 15, 2022 by Costava@Costava

[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed index when array is function parameter

Steps to reproduce the issue

With Alt-Ergo 2.4.1 installed:
frama-c -wp -wp-rte poc.c / frama-c-gui -wp -wp-rte poc.c

using poc.c :

/*@
  requires \valid_read(arr + (0 .. 3));
  assigns \nothing;
*/
int foo(const int arr[const static 4]) {
	const unsigned int h = 7 & 0b11;
	//@ assert 0 <= h < 4;
	const int hvalue = arr[h];

	const unsigned int i = 7 % 4;
	//@ assert 0 <= i < 4;
	const int ivalue = arr[i];

	/*@
	  loop invariant 0 <= s <= 8;
	  loop assigns s;
	  loop variant 8 - s;
	*/
	for (unsigned int s = 0; s < 8; s += 1) {
		const unsigned int j = s & 0b11;
		//@ assert 0 <= j < 4;
		const int jvalue = arr[j];

		const unsigned int k = s % 4;
		//@ assert 0 <= k < 4;
		const int kvalue = arr[k];
	}

	return 0;
}

/*@
  assigns \nothing;
*/
int main(void) {
	const int arr[4] = {0, 1, 2, 3};

	const unsigned int h = 7 & 0b11;
	//@ assert 0 <= h < 4;
	const int hvalue = arr[h];

	const unsigned int i = 7 % 4;
	//@ assert 0 <= i < 4;
	const int ivalue = arr[i];

	/*@
	  loop invariant 0 <= s <= 8;
	  loop assigns s;
	  loop variant 8 - s;
	*/
	for (unsigned int s = 0; s < 8; s += 1) {
		const unsigned int j = s & 0b11;
		//@ assert 0 <= j < 4;
		const int jvalue = arr[j];

		const unsigned int k = s % 4;
		//@ assert 0 <= k < 4;
		const int kvalue = arr[k];
	}

	foo(arr);

	return 0;
}

Expected behaviour

All goals proved.

Actual behaviour

$ frama-c -wp -wp-rte poc.c
[kernel] Parsing poc.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 34 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_foo_assert_rte_mem_access_3 : Timeout (Qed:9ms) (10s)
[wp] Proved goals:   33 / 34
  Qed:              23  (2ms-5ms-14ms)
  Alt-Ergo 2.4.1:   10  (7ms-17ms-30ms) (556) (interrupted: 1)

33/34 goals proved.
The verification of /*@ assert rte: mem_access: \valid_read(arr + j); */ for code const int jvalue = arr[j]; in function foo is not successful.
From a naive perspective, the arr[j] accesses in main and foo are equivalent, so the assert in foo should be verifiable if the assert in main is.
(I am aware that a different assert is generated in main: /*@ assert rte: index_bound: j < 4; */)
Also, the //@ assert 0 <= j < 4; immediately before the access can be verified, both in main and foo, so it seems the rte assert should be able to be verified also.

Contextual information

  • Frama-C installation mode: opam
  • Frama-C version: 24.0 (Chromium)
  • Plug-in used: WP, RTE
  • OS name: Manjaro Linux
  • OS version: Qonos 21.2.4

Additional information (optional)

The poc.c is a simplified proof of concept, but I did hit this situation when working on a real program.

To be explicit about the provers involved:

$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/user/.why3.conf

I was uncertain whether to submit this here or at the alt-ergo issues.
Apologies if this is the wrong place. Let me know if I should post there instead.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking