search

seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

Behavior of `accessedTypes` with respect to memset/memcpy operations #88

Closed shaobo-he closed 4 years ago

shaobo-he commented 4 years ago

Hello sea-dsa developers,

I encountered an issue where accessedTypes does not contain i8 for node that involves store a i64 and memset (please see the C program below). I was wondering if it's expected. The accessedTypes only contains a 'i64'.

#include <string.h>
#include "smack.h"

int main(void) {
  unsigned long long x = 0;
  memset(&x, 1, sizeof(x));
  assert(x == 1);
  return 0;
}

I also attached a bitcode file generated for this program. I used llvm8.

memset1.txt

Thanks, Shaobo

agurfinkel commented 4 years ago

This is intentional. Certainly other interpretations are possible, but these best done as a another analysis on top of the memory dependence that sea-dsa provides.

I am assuming that you would like to treat memset as store of i8 to &x. Technically, this is too pessimistic for this examples. In most architectures, since &x is aligned, the memset will write an i64 word to &x. So the access type is i64.

For the large part, we leave memset (and other wide memory instructions) uninterpreted. The only exceptions is when memory that is being set / copied contains pointers. In which case the corresponding DSA nodes are collapsed because filed sensitivity is lost.

shaobo-he commented 4 years ago

This is intentional. Certainly other interpretations are possible, but these best done as a another analysis on top of the memory dependence that sea-dsa provides.

I am assuming that you would like to treat memset as store of i8 to &x. Technically, this is too pessimistic for this examples. In most architectures, since &x is aligned, the memset will write an i64 word to &x. So the access type is i64.

For the large part, we leave memset (and other wide memory instructions) uninterpreted. The only exceptions is when memory that is being set / copied contains pointers. In which case the corresponding DSA nodes are collapsed because filed sensitivity is lost.

Thank you for your reply, @agurfinkel. It makes sense. I closed this issue because my question has been answered.