[cfe-dev] Static Analyzer and signed 64bit constraints

[Artem Dergachev via cfe-dev]

 > The constraint on the above value is printed as 'conj_$0{int32_t} : { 
[-2147483648, -1], [1, 20] }'. What happened to zero? My best guess is 
the static analyzer realizing that 'memcpy(x, y, 0)' is a nop and 
pruning that program state?

Yes, indeed, it is an effect of how we model 'memcpy'. I don't think 
it's the desired behavior though. In particular, we don't display a 
warning on 'memcpy(NULL, y, 0)', even though it's UB. So, yeah, sounds 
like either a minor bug. It's not obvious for me how often paths with 
zero-size memcpys are actually feasible in real-world programs.



 > However, if I switch this to an int64_t I get:
 > conj_$0{int64_t} : { [1, 20] }

Hmm, weird, i'm not able to reproduce it. Could you provide more info? 
I'm trying:


$ cat test.c


   #include <stdlib.h>
   #include <stdio.h>

   void foo(void *x, void *y) {
     int64_t z = -1;
     read(1, &z, sizeof(z));
     if (z > 20)
       exit(-1);
     memcpy(x, y, z);
     // triggers state dump via ExprInspection
     clang_analyzer_printState();
     // don't garbage-collect 'z' until now
     z;
   }


$ clang --analyze test.c -Xclang -analyzer-checker -Xclang 
debug.ExprInspection


Store (direct and default bindings), 0x7fcf3114a5e8 :
  (z,0,direct) : conj_$0{int64_t}
  (GlobalInternalSpaceRegion,0,default) : conj_$1{int}
  (GlobalSystemSpaceRegion,0,default) : conj_$2{int}

Expressions:
  (0x7fcf30579920,0x7fcf3113c0c0) clang_analyzer_printState : 
&code{clang_analyzer_printState}

Ranges of symbol values:
  conj_$0{int64_t} : { [-9223372036854775808, -1], [1, 20] }



On 29/01/2018 12:25 AM, - yrp via cfe-dev wrote:
> Hello,
>
> I'm attempting to write a checker to look for certain signedness 
> issues. I have code similar to the following:
>
> int32_t z = -1;
> read (STDIN_FILENO, &z, sizeof(z));
>
> if (z > 20) exit (EXIT_FAILURE);
>
> memcpy (x, y, z);
>
> Inside the checker I am printing the constraints on the SVal 'z' with 
> a PreCall, filtering on memcpy:
>
> ProgramStateRef State = C.getState();
> State->getConstraintManager().print(State, llvm::outs(), "\n", " ");
>
> I have two questions related to this:
>
> 1. The constraint on the above value is printed as 'conj_$0{int32_t} : 
> { [-2147483648, -1], [1, 20] }'. What happened to zero? My best guess 
> is the static analyzer realizing that 'memcpy(x, y, 0)' is a nop and 
> pruning that program state?
>
> 2. The above code, aside from the zero exception, makes sense when z 
> is an int8_t, int16_t, or an int32_t:
>
>  conj_$0{int8_t} : { [-128, -1], [1, 20] }
>  conj_$0{int16_t} : { [-32768, -1], [1, 20] }
>  conj_$0{int32_t} : { [-2147483648, -1], [1, 20] }
>
> However, if I switch this to an int64_t I get:
>
>  conj_$0{int64_t} : { [1, 20] }
>
> What happened to all the negative numbers?
>
> Apologies if I've missed something obvious.
>
> Cheers!
> -yrp
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev