problem with bit vector

[bejab2020]

hi
i have a function with two integer inputs. i want to execute this function symbolically with Bit vector of size 64 .
but angr restict the constraints with only 32 bit of them for example these are the constraints of one path in my function :

[<Bool var_1[31:0] != 0x0>,
 <Bool var_2[31:0] != 0x0>,
 <Bool var_2[31:0] == 0x8>,
 <Bool 0xfffffffb + var_2[31:0] + var_1[31:0] >s 0x64>]

which var_1 and var_2 are:

x=claripy.BVS('var_1',64,explicit_name=True)
y=claripy.BVS('var_2',64,explicit_name=True)

when i want to add extra constraints in solver to generate inputs that lead me to buffer overflow for example consider there is a write with the content of t in heap in this path with those constrains i want to generate inputs that satisfy the constraints which lead me to the path and also satisfy this extra constraint which leads me to heap overflow:

t=<BV32 (0#32 .. var_1[31:0]) + 0xfffffffffffffffe[31:0]> 
size=2**32 # i got error here
s.satisfiable(extra_constraints=(t>size,)) 

I got an error and when I resize the 't' to 64 with zero_extend it is not satisfiable!!
is there any way that I can force angr to consider the whole size of bit vector instead of the first 32 bits?

[rhelmot]

There is no logic in angr which truncates variables to 32 bits before using them. Are you sure the binary doesn't only operate on the low 32 bits?

[bejab2020]

in this source code:

int weird(int *x,int *y){

        if(*x==0 || *y==0)
                return -2;
        if(*y==8){
                printf("back door");
                *x=*x - 2;
                (*y)++;
                *y= *y - 4;
        }

        int result=*x + *y;
        if(result >100 || result <0)
                return -1;

        *x=(*y) * 6;
        return result;
}

for expression bellow:

t=<Bool var_1[31:0] != 0x0>
In [25]: t.args[0].op                                                                                                                                 
Out[25]: 'Extract'

In [26]: t.args[0].args                                                                                                                               
Out[26]: (31, 0, <BV64 var_1>)

it consider 32 bits?

[rhelmot]

int *x,int *y

an int is only 32 bits.

[bejab2020]

Thank you, I realized my mistake,it's based on type length.