[Analyzer] Stores to symbolic region

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) - (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);
}

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.

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);