Fr_rawSwap.ini

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


assume dst & 0b111 = 0           ## alignment constraint for dst
assume src & 0b111 = 0           ## alignment constraint for src

assume 0x3000 <= dst <= 0x4000   ## arbitrary range for dst
assume 0x4019 <= src <= 0x6000   ## arbitrary range for src


starting from <Fr_rawSwap> with
  ## Initialize the source and destination with specific values
  old_dst_values[0, 32] := @[dst, 32]
  old_src_values[0, 32] := @[src, 32]
end

replace <Fr_rawSwap:last> by
  ## Check if the values at src and dst are swapped correctly
  eq<1> := true
  for i<64> in 0 to 3 do
    eq := eq && (@[dst + 8 * i, 8] = old_src_values[8 * i, 8]) && (@[src + 8 * i, 8] = old_dst_values[8 * i, 8])
  end
  assert eq                      ## assert that swapping is performed as expected
  halt
end

explore all