Question about ptrtoint nodetype

[shaobo-he]

Hello sea-dsa developers,

Consider the following example,

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

void __VERIFIER_assert(bool);

int main(void) {
  int *a = (int *)malloc(sizeof(int));
  intptr_t b;

  b = (intptr_t)a;
  *((int *)b) = 1;
  __VERIFIER_assert(*a == 1);
  free(a);
  return 0;
}

The attached graph is generated using the following commands,

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

main.mem.pdf

In this graph, the node %4 points to is labeled as SMP whereas the node %1 points to is not considered as a node having the ptrtoint type. Although I know that we should probably try to eliminate ptrtoint/inttoptr instructions first, I was wondering if the node %1 points to should have ptrtoint type.

[shaobo-he]

@caballa @agurfinkel any updates on this issue?

Thanks, Shaobo

[agurfinkel]

I think we never set ptrtoint flag since we never had a use for it.

Is the intended semantics is that a node is marked with ptrtoint flag if there is a pointer to that node that is ever an argument to ptrtoint operation? Is that correct?

@caballa if this looks ok to you, I can commit a fix.

[zvonimir]

What you wrote is I believe correct. A sound analysis would assume that every node with ptrtoint flag can alias any node with inttoptr flag. Thanks @agurfinkel!

[agurfinkel]

fixed by ea3eea3

We mark the nodes with the right flags, but do not unify them. If there is a need to soundly but precisely analyze code with inttoptr and ptrtoint conversions, an additional pass is required after sea-dsa to resolve left over ambiguity. Similar to how the call graph construction is done right now.

[shaobo-he]

Thank you, @agurfinkel