rawCopyS2L_Intel.ini

rdi := nondet as dst            ## initialize the destination address
rsi := nondet as src            ## initialize the source integer

assume dst & 0b111 = 0          ## alignment constraint for destination
assume 0x4000 <= dst <= 0x5000  ## arbitrary range for destination
#assume src = 0x7FFFFFFFFFFFFFFF

starting from <rawCopyS2L> with
  assume 0x7ffff000000 <= rsp <= 0x7ffff800000 # arbitrary stack range
  @[rsp, 8] := <rawCopyS2L:last>   # set the return address
end

replace <rawCopyS2L:last> by
  
  eq<1> := true
  
  ## Check if the first 8 bytes of the destination have the long format identifier set correctly
  #eq := eq && (@[dst + 8, 8] = 0x43e1f593f0000001 + src)
  ## Check if the first 8 bytes of the destination have the long format identifier set correctly
  eq := eq && (@[dst, 8] = 0x8000000000000000)
  ## For a positive source integer, check if it is correctly copied to the second 8-byte block
  ## and the rest of the destination is zeroed out
  print src
  print @[dst, 40]
  if (src & 0x8000000000000000) = 0 then
    eq := eq && @[dst + 8, 8] = src && @[dst + 16, 8] = 0 && @[dst + 24, 8] = 0 && @[dst + 32, 8] = 0
  else
    #eq := eq && @[dst + 8, 32] - 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 = src<256>
    eq := eq && @[dst + 8, 32] - 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 = sext256 src
  end
  
  assert eq
  halt
end

explore all