rawCopyS2L.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 = 0x0000000000000000
starting from <rawCopyS2L> with
    
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] = 0x43e1f593f0000001)
  ## 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
  if src >= 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, 8] - 0x43e1f593f0000001 = src
  end
  
  assert eq
  halt
end

explore all