[Analyzer] Stores to symbolic region

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

[Analyzer] Stores to symbolic region

Kristóf Umann via cfe-dev
I noticed the static analyzer cannot detect a division by zero problem as shown in the "divxy" function, if it is analyzed without a caller context. The value assigned to variable "res" looks like "100 / ((reg_$2<int x>) - (reg_$1<int SymRegion{reg_$0<struct xy * pxy>}->y>))"

But if I assign to pxy's fields as in the commented part, the division by zero bug can be detected.

What is the reason behind this and how can I make the analyzer detect the division by zero bug in this case? I suspect this is related to handling stores to symbolic region but I haven't figured out.

struct xy {
  int x;
  int y;
}

int intdiv(int x, int y) { return 100 / (x - y); }

void divxy(struct xy *pxy)
{
  struct xy val;

  val.x = 10;
  val.y = val.x;
  *pxy = val;

  // Division by zero can be detected if assign to individual fields.
  // pxy->x = val.x;
  // pxy->y = val.y;

  int res = intdiv(pxy->x, pxy->y);

  printf("Result is %d\n", res);
}


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [Analyzer] Stores to symbolic region

Kristóf Umann via cfe-dev
Ugh, this looks like a bug. The values are there:

  (SymRegion{reg_$0<struct xy * pxy>}, 0, direct): lazyCompoundVal{0x7fb05e8ac060,val}

Where Store 0x7fb05e8ac060 has the contents that we're looking for:

  (val, 0, direct): 10 S32b
  (val, 32, direct): 10 S32b

But we don't *load* them correctly.

I suspect that this is happening because the lazyCompoundVal binding is direct even though normally it should be a default binding. I'll take a look. This sounds pretty bad, but also it's not as bad as it sounds because it's a combination of specific kinds of values when classified by their origin rather than by their structure. Normally assigning structures into each other works correctly.

On 7/29/19 2:29 PM, Torry Chen via cfe-dev wrote:
I noticed the static analyzer cannot detect a division by zero problem as shown in the "divxy" function, if it is analyzed without a caller context. The value assigned to variable "res" looks like "100 / ((reg_$2<int x>) - (reg_$1<int SymRegion{reg_$0<struct xy * pxy>}->y>))"

But if I assign to pxy's fields as in the commented part, the division by zero bug can be detected.

What is the reason behind this and how can I make the analyzer detect the division by zero bug in this case? I suspect this is related to handling stores to symbolic region but I haven't figured out.

struct xy {
  int x;
  int y;
}

int intdiv(int x, int y) { return 100 / (x - y); }

void divxy(struct xy *pxy)
{
  struct xy val;

  val.x = 10;
  val.y = val.x;
  *pxy = val;

  // Division by zero can be detected if assign to individual fields.
  // pxy->x = val.x;
  // pxy->y = val.y;

  int res = intdiv(pxy->x, pxy->y);

  printf("Result is %d\n", res);
}


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [Analyzer] Stores to symbolic region

Kristóf Umann via cfe-dev
Thank you Artem! Another observation: If I re-assign "pxy" as follows, it detects division by zero.

pxy = malloc(sizeof(struct xy)); // <- dected if add this line
val.x = 10;
val.y = val.x;
*pxy = val;

int res = intdiv(pxy->x, pxy->y); 
printf("Result is %d\n", res); 

On Mon, 29 Jul 2019 at 17:34, Artem Dergachev <[hidden email]> wrote:
Ugh, this looks like a bug. The values are there:

  (SymRegion{reg_$0<struct xy * pxy>}, 0, direct): lazyCompoundVal{0x7fb05e8ac060,val}

Where Store 0x7fb05e8ac060 has the contents that we're looking for:

  (val, 0, direct): 10 S32b
  (val, 32, direct): 10 S32b

But we don't *load* them correctly.

I suspect that this is happening because the lazyCompoundVal binding is direct even though normally it should be a default binding. I'll take a look. This sounds pretty bad, but also it's not as bad as it sounds because it's a combination of specific kinds of values when classified by their origin rather than by their structure. Normally assigning structures into each other works correctly.

On 7/29/19 2:29 PM, Torry Chen via cfe-dev wrote:
I noticed the static analyzer cannot detect a division by zero problem as shown in the "divxy" function, if it is analyzed without a caller context. The value assigned to variable "res" looks like "100 / ((reg_$2<int x>) - (reg_$1<int SymRegion{reg_$0<struct xy * pxy>}->y>))"

But if I assign to pxy's fields as in the commented part, the division by zero bug can be detected.

What is the reason behind this and how can I make the analyzer detect the division by zero bug in this case? I suspect this is related to handling stores to symbolic region but I haven't figured out.

struct xy {
  int x;
  int y;
}

int intdiv(int x, int y) { return 100 / (x - y); }

void divxy(struct xy *pxy)
{
  struct xy val;

  val.x = 10;
  val.y = val.x;
  *pxy = val;

  // Division by zero can be detected if assign to individual fields.
  // pxy->x = val.x;
  // pxy->y = val.y;

  int res = intdiv(pxy->x, pxy->y);

  printf("Result is %d\n", res);
}


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev