1

I need to solve this code (the code in C) 

if ( ((0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1)+ len_input_serial- 3 * ((0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1) != 14)
    return 0xFFFFFFFFLL;

that's my python script 

from z3 import *
len_input_serial = BitVec("serial_len",64)
solve(LShR(LShR(0xAAAAAAAAAAAAAAABL * len_input_serial,64),1) + len_input_serial - 3 * LShR(LShR(0xAAAAAAAAAAAAAAABL * len_input_serial,64),1) == 14)

However this gives me [serial_len = 14]

I know the solution should be around [42,38,40], so what's wrong here ?

ShivaGaire
  • 2,283
  • 1
  • 20
  • 31
Ahmed Ezzat
  • 65
  • 10
  • 2
    is it intentional that your python code uses `A...ABL` instead of `A...ABLL`? – voiDnyx Mar 14 '18 at 15:21
  • i guess it doesn't matter .. i tried to set len_input_serial to 40 and run the code in python i got 14 which is the right number – Ahmed Ezzat Mar 14 '18 at 15:34
  • What do you mean "solve?" Are you trying to find a value for `len_input_serial` so that the test of `if` statement would evaluate to true? – alias Mar 14 '18 at 15:38
  • No i need values which evaluates false which i know is 40,38,42 – Ahmed Ezzat Mar 14 '18 at 15:44

1 Answers1

1

This expression:

(0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1

Is always equivalent to 0. If you right shift a 64-bit quantity to the right by 64 bits, you get 0. (Note that you are using LShr, which treats its input as an unsigned quantity.)

Therefore the whole thing simplifies to solving len_input_serial == 14, which is the answer Z3 is producing.

Note that when you write a long integer in Python (i.e., 0x123L etc.), you get infinite precision. (See here: Maximum value for long integer). In C, you get (most-likely) 64-bit integer. So, your Z3 code is actually correct; it's Python that's using a bigger precision here and thus causing the confusion.

alias
  • 28,120
  • 2
  • 23
  • 40