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

[Artem Dergachev 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
> cfe-dev at lists.llvm.org
> https://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/3d46a808/attachment.html>