Question about external nodetype

[shaobo-he]

Hello sea-dsa developers,

Consider the following program,

#include <stdlib.h>
#include <stdbool.h>

void __VERIFIER_assert(bool);

void foo(int *);
int *bar();

int main() {
  int *x = malloc(4);
  int *y;

  foo(x);
  y = bar();

  *x = 1;
  *y = 2;

  __VERIFIER_assert(x != y);
}

clang-8 -O0 -c -emit-llvm -S -Xclang -disable-O0-optnone extern_mem_fail.c
opt-8 extern_mem_fail.ll -mem2reg -S -o extern_mem_fail.ll
seadsa -sea-dsa=ci -sea-dsa-type-aware -sea-dsa-dot extern_mem_fail.ll

main.mem.pdf

The malloced node is not labeled as an external node as opposed to what llvm-dsa does. I was wondering if it should be since x is passed to an external function foo, which may store this pointer elsewhere such that bar can obtain it and return it.

[agurfinkel]

Good point. We did not consider this case. I think the meaning of external is different between llvm-dsa and sea-dsa. In our case, external meant to mean pointer to an externally allocated memory. However, the flag does not work properly in the current implementation. It is not clear how it is maintained.

You are suggesting that we need an escaped flag to indicate that a pointer is escaped to an external function. A safe sound behavior would be to collapse all such pointers because they can be changed arbitrarily and to unify all escaped pointers because external functions can communicate beyond what is observable in the code.

This seems a bit too conservative for typical verification tasks since without good model of library functions it will likely make analysis very imprecise.

Is that the expected behavior for you? We could add something like that under a flag.

[shaobo-he]

Good point. We did not consider this case. I think the meaning of external is different between llvm-dsa and sea-dsa. In our case, external meant to mean pointer to an externally allocated memory. However, the flag does not work properly in the current implementation. It is not clear how it is maintained.

You are suggesting that we need an escaped flag to indicate that a pointer is escaped to an external function. A safe sound behavior would be to collapse all such pointers because they can be changed arbitrarily and to unify all escaped pointers because external functions can communicate beyond what is observable in the code.

This seems a bit too conservative for typical verification tasks since without good model of library functions it will likely make analysis very imprecise.

Is that the expected behavior for you? We could add something like that under a flag.

We agree that collapsing all the escaped nodes would be too conservative. So let's leave it as it is unless we observe some benchmarks that require such a functionality.