DieracDelta

real	1m3.383s
user	1m0.163s
sys	0m3.191s
result)
0012a704: mb_copy_result :: out u32 = RAX
0000196e: 
00001975: #259 := RBP
00001978: RSP := RSP - 8
0000197b: mem := mem with [RSP, el]:u64 <- #259

DieracDelta

real	0m31.930s
user	0m28.753s
sys	0m3.158s
dir_result)
0012a6c7: is_dumpdir_result :: out u32 = RAX
000ccd2c: 
000ccd31: RAX := pad:64[pad:32[mem[RDI + 0x188]]]
000ccd3e: #27613 := low:8[RAX]
000ccd41: OF := 0

DieracDelta

rm -f main
gcc-8 -O2 -Wall -o main main.c
#gcc -O0 -Wall -o main main.c
#clang -O3 -o main main.c
Evaluating precondition.
Checking precondition with Z3.
Z3 : 
 (declare-fun RDI0 () (_ BitVec 64))
(declare-fun RSP0 () (_ BitVec 64))
(declare-fun RBX0 () (_ BitVec 64))

DieracDelta

digraph {
node[shape=box];

subgraph "cluster__start" {
  label="_start"
  
  "\%0000002b"[label="\%0000002b
0000003e: RSP := RSP - 8\l00000041: mem := mem with [RSP, el]:u64 <- 0x4000E6\l00000044: call @main with noreturn\l"]
}
"\%0000002b" -> "\%0000003a";

DieracDelta

digraph {
node[shape=box];

subgraph "cluster__start" {
  label="_start"
  
  "\%0000001c"[label="\%0000001c
0000002f: RSP := RSP - 8\l00000032: mem := mem with [RSP, el]:u64 <- 0x4000E5\l00000035: call @main with noreturn\l"]
}
"\%0000001c" -> "\%0000002b";

DieracDelta

Model:
	ZF  |->  0x0
	SF  |->  0x0
	RSP |->  0x0000000040000000
	RBX |->  0x000000003fffffed
	RAX |->  0x0000000000000000
	PF  |->  0x0
	OF  |->  0x0
	CF  |->  0x0
	AF  |->  0x0

DieracDelta

.global _start

.text

safe_hasher:

push %rbx
#callq *0x30(%rbx)
callq _start
add (%rbx),%rax

DieracDelta

rm main_1 main_2 main_1.bpj main_2.bpj
gcc  -nostdlib main_1.S -o main_1
gcc  -nostdlib main_2.S -o main_2
bap --pass=save-project --no-byteweight --save-project-filename=main_1.bpj main_1
bap --pass=save-project --no-byteweight --save-project-filename=main_2.bpj main_2

BAP_DEBUG=1 bap /bin/echo --pass=wp --wp-compare=true --wp-file1=main_1.bpj --wp-file2=main_2.bpj --wp-function=safe_hasher --wp-inline=false --wp-num-unroll=0 --no-byteweight --wp-use-fun-input-regs=false --wp-mem-offset=false --wp-compare-post-reg-values=R12,R13,R14,R15,RBX,RSP,RBP,RAX --wp-show=bir,refuted-goals,paths

DieracDelta

digraph {
node[shape=box];

subgraph "cluster__start" {
  label="_start"
  
  "\%0000002b"[label="\%0000002b
0000003e: RSP := RSP - 8\l00000041: mem := mem with [RSP, el]:u64 <- 0x4000E5\l00000044: call @main with noreturn\l"]
}
"\%0000002b" -> "\%0000003a";

DieracDelta

digraph {
node[shape=box];

subgraph "cluster__start" {
  label="_start"
  
  "\%0000001c"[label="\%0000001c
0000002f: RSP := RSP - 8\l00000032: mem := mem with [RSP, el]:u64 <- 0x4000E4\l00000035: call @main with noreturn\l"]
}
"\%0000001c" -> "\%0000002b";