[cfe-dev] [Analyzer] Stores to symbolic region

[Torry Chen 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 <noqnoqneo at gmail.com> 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 listcfe-dev at lists.llvm.orghttps://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20190729/be2da245/attachment.html>