[WP] no trivial separation of the allocation status of heap and local variables whose address are taken
Description
I'm currently working on specifying and proving functions focused on linked list structures using previous works based on ACSL logic lists (cf this paper), and I've encountered some issues proving relatively simple assertions when certain types of memory separation between pointers are involved.
Steps to reproduce the issue
Running Frama-C with WP on the minimal code inlined below, or running frama-c-gui linked_ll_dptr_proof.c -wp -wp-rte -wp-prover altergo,cvc4,cvc4-ce -wp-smoke-tests -wp-fct="dummyCaller, dummyCaller_bis" &
using the attachments.
I've also taken the liberty of attaching an extended version of the code below in linked_ll_dptr_proof.c
including all the logic definitions (modulo name changes) used in the "Logic against Ghosts" paper, as well as the corresponding lemmas in lemmas_list.h
, but I'm not really sure of their relevance, as the issue also occurs on variants of the original logic definitions of the paper that are not used by said lemmas.
#include <stdlib.h>
typedef struct LIST {
int handle;
struct LIST * next;
} LIST;
/**** Logic definitions from the "Logic against Ghosts" paper (modulo renaming for node_to_ll) ****/
/*@
predicate ptr_separated_from_range{L}
(LIST* e, \list<LIST*> ll, integer beg, integer end) =
\forall integer n ; 0 <= beg <= n < end <= \length(ll) ==> \separated(\nth(ll, n), e);
predicate dptr_separated_from_range{L}
(LIST** e, \list<LIST*> ll, integer beg, integer end) =
\forall integer n ; 0 <= beg <= n < end <= \length(ll) ==> \separated(\nth(ll, n), e);
predicate ptr_separated_from_list{L}(LIST* e, \list<LIST*> ll) =
ptr_separated_from_range(e, ll, 0, \length(ll));
predicate dptr_separated_from_list{L}(LIST** e, \list<LIST*> ll) =
dptr_separated_from_range(e, ll, 0, \length(ll));
*/
/*@
predicate in_list{L}(LIST* e, \list<LIST*> ll) =
\exists integer n ; 0 <= n < \length(ll) && \nth(ll, n) == e ;
*/
/*@
inductive linked_ll{L}(LIST *bl, LIST *el, \list<LIST*> ll) {
case linked_ll_nil{L}:
\forall LIST *el ; linked_ll{L}(el, el, \Nil);
case linked_ll_cons{L}:
\forall LIST *bl, *el, \list<LIST*> tail ;
\separated(bl, el) ==> \valid(bl) ==>
linked_ll{L}(bl->next, el, tail) ==>
ptr_separated_from_list(bl, tail) ==>
linked_ll{L}(bl, el, \Cons(bl, tail)) ;
}
*/
/*@
axiomatic Node_To_ll {
logic \list<LIST*> node_to_ll{L}(LIST* beg_node, LIST* end_node)
reads { node->next | LIST* node ; \valid(node) && in_list(node, node_to_ll(beg_node, end_node)) } ;
axiom to_ll_nil{L}:
\forall LIST *node ; node_to_ll{L}(node, node) == \Nil ;
axiom to_ll_cons{L}:
\forall LIST *beg_node, *end_node ;
\separated(beg_node, end_node) ==>
\valid{L}(beg_node) ==>
ptr_separated_from_list{L}(beg_node, node_to_ll{L}(beg_node->next, end_node)) ==>
node_to_ll{L}(beg_node, end_node) == (\Cons(beg_node, node_to_ll{L}(beg_node->next, end_node))) ;
}
*/
/*******************************************************************/
/*@
requires node_separation_to_list : dptr_separated_from_list(out_node, node_to_ll(rsrc_list, NULL)); //if uncommented, linked_assert cannot be proved
assigns \nothing;
ensures \result == 616;
*/
int dummyCallee(LIST * rsrc_list, LIST ** out_node);
/*@
requires linked_ll(rsrc_list, NULL, node_to_ll(rsrc_list, NULL));
assigns \nothing;
ensures \result == 616;
*/
int dummyCaller(LIST * rsrc_list, LIST ** out_node)
{
/*@ assert linked_assert : linked_ll(rsrc_list, NULL, node_to_ll(rsrc_list, NULL));*/ // should be proved from the precondition
int r;
LIST *test_node;
r = dummyCallee(rsrc_list, &test_node);
return r;
}
Expected behaviour
The linked_assert
assertion in dummyCaller (or dummyCaller_bis in the attached files) should be always proved, even when the node_separation_to_list
(and/or int_separation_to_list
in attachments) preconditions are uncommented.
Actual behaviour
None of the linked_assert assertions are proved.
The situation depicted by dummyCaller
and dummyCallee
, using node_separation_to_list
as a precondition, is the closest to the code I'm currently working on.
In the code in attachments, I also tried using node_separation_to_nil
as precondition to test whether the issue also occured using a \Nil
logic list, and the dummyCaller_bis
and dummyCallee_bis
functions to test if eliminating lemmas, or changing the datatype used for separation in dummyCallees
, had any influence on the issue, but they don't seem to.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 26.0 (Iron) (As well as version 25.0)
- Plug-in used: WP and RTE
- OS name: Ubuntu
- OS version: 20.04.4 LTS
Additional information (optional)
- Alt-Ergo version : 2.4.2
- CVC4 version : 1.7
Edit: I completely forgot to add those attachments earlier :