A Python CLI for Verifying Assembly
I’ve been building a system that verifies assembly programs via symbolic execution. I think the following are the most novel points of my approach:
- keeping the assembly file GAS assembleable with regular macros as annotations
- using Ghidra pcode semantics, which gives me a big corpus of extensible and evolving architecture semantics
- Being implemented in python which is a mature language and ecosystem which I think is comfortable to more people who may be interested in such a tool.
- Describing invariants via cuts of the CFG. A CFG which has enough edges (“backedges”) cut becomes acyclic, and hence has a finite number of trace fragments to consider.
I’ve previously described work in progress here
The tool is here https://github.com/philzook58/knuckledragger/tree/main/kdrag/contrib/pcode
Here we go walking through some examples and features!
CLI
Previously I was using the tool in a Jupyter notebook but now I wired it up to be a CLI. There is still the intention to use it as a python library and discharged verification conditions via manual knuckledragger proof if they get hairy or refer to mathematical or higher level functions (sin, fib, List ADT append, etc).
For an example of usage, I took a toy swap function example from frama-C WP tutorial section 1.2 https://www.frama-c.com/download/wp-manual-18.0-Argon.pdf .
%%file /tmp/swap.c
#include <stddef.h>
/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a,int *b);
void swap(int *a,int *b)
{
int tmp = *a ;
*a = *b ;
*b = tmp ;
return ;
}
Overwriting /tmp/swap.c
! frama-c -wp -wp-verbose 0 -wp-rte /tmp/swap.c -then -report
[kernel] Parsing /tmp/swap.c (with preprocessing)
[rte:annot] annotating function swap
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'swap'
--------------------------------------------------------------------------------
[ Valid ] Post-condition 'A'
by Wp.typed.
[ Valid ] Post-condition 'B'
by Wp.typed.
[ Valid ] Exit-condition (generated)
by Unreachable Annotations.
[ Valid ] Termination-condition (generated)
by Trivial Termination.
[ Valid ] Assigns (file /tmp/swap.c, line 5)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file /tmp/swap.c, line 11)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file /tmp/swap.c, line 12)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file /tmp/swap.c, line 12)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file /tmp/swap.c, line 13)
by Wp.typed.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
10 Completely validated
10 Total
--------------------------------------------------------------------------------
We can also compile it. I’ve been sticking to O1, it’s the easiest to read. O0 is so verbose and O2/3 are unpleasantly mangled sometimes.
! gcc -O1 -c /tmp/swap.c -S -o /tmp/swap.S && cat /tmp/swap.S
.file "swap.c"
.text
.globl swap
.type swap, @function
swap:
.LFB0:
.cfi_startproc
endbr64
movl (%rdi), %eax
movl (%rsi), %edx
movl %edx, (%rdi)
movl %eax, (%rsi)
ret
.cfi_endproc
.LFE0:
.size swap, .-swap
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
I then copy out the relevant bits and add my annotations.
We want to save the initial state in olda and oldb using kd_assign. There are updated in ghost state during symbolic executions These variables must be declared in kd_prelude which basically just injects into the smtlib parser.
The entry condition requires RSI and RDI to not overlap. We will see later that removing this enables aliasing that makes the function verification fail. A somewhat subtle problem that happy path thinking tends to not notice. Maybe a helper function to describe this situation less verbosely would be nice. This is also the sort of thing that separation logic is for, so maybe I’ll take inspiration from that direction.
%%file /tmp/swap.S
.include "/tmp/knuckle.s"
kd_prelude "(declare-const olda (_ BitVec 32))"
kd_prelude "(declare-const oldb (_ BitVec 32))"
.file "swap.c"
.text
.globl swap
.type swap, @function
swap:
kd_entry myentry "(distinct RSI (bvadd RSI (_ bv1 64)) (bvadd RSI (_ bv2 64)) (bvadd RSI (_ bv3 64)) RDI (bvadd RDI (_ bv1 64)) (bvadd RDI (_ bv2 64)) (bvadd RDI (_ bv3 64)))"
kd_assign save_olda olda "(select ram32 RDI)"
kd_assign save_oldb oldb "(select ram32 RSI)"
.LFB0:
.cfi_startproc
endbr64
movl (%rdi), %eax
movl (%rsi), %edx
movl %edx, (%rdi)
movl %eax, (%rsi)
kd_exit myexit "(and (= (select ram32 RSI) olda) (= (select ram32 RDI) oldb))"
ret
.cfi_endproc
Overwriting /tmp/swap.S
We can then run it through the CLI and see all those pretty green checkmarks
! python3 -m kdrag.contrib.pcode /tmp/swap.S
Processing /tmp/swap.S with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing SpecStmt: Assign(label='save_olda', addr=4194304, name='olda', expr=ram32[RDI])
Executing SpecStmt: Assign(label='save_oldb', addr=4194304, name='oldb', expr=ram32[RSI])
Executing 0x400000/4: ENDBR64 at (4194304, 0) PCODE IMARK ram[400000:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 0) PCODE IMARK ram[400004:2]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 1) PCODE unique[de00:4] = *[ram]RDI
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 2) PCODE EAX = unique[de00:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 3) PCODE RAX = zext(EAX)
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 0) PCODE IMARK ram[400006:2]
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 1) PCODE unique[de00:4] = *[ram]RSI
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 2) PCODE EDX = unique[de00:4]
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 3) PCODE RDX = zext(EDX)
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 0) PCODE IMARK ram[400008:2]
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 1) PCODE unique[6a80:4] = EDX
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 2) PCODE *[ram]RDI = unique[6a80:4]
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 0) PCODE IMARK ram[40000a:2]
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 1) PCODE unique[6a80:4] = EAX
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 2) PCODE *[ram]RSI = unique[6a80:4]
Executing SpecStmt: Exit(myexit, 0x40000c, And(ram32[RSI] == olda, ram32[RDI] == oldb))
Checking verification conditions...
[✅] Exit(myexit, 0x40000c, And(ram32[RSI] == olda, ram32[RDI] == oldb))
✅✅✅✅ All 1 verification conditions passed! ✅✅✅✅
Countermodels
Here I have not included my no alias constraint. Now this thing fails with a countermodel.
The countermodel prints only the memory locations and variables mentioned in the entry precondition and post condition.
It probably would be nice to print more of the countermodel state during the execution. This is doable.
%%file /tmp/swap.S
.include "/tmp/knuckle.s"
kd_prelude "(declare-const olda (_ BitVec 32))"
kd_prelude "(declare-const oldb (_ BitVec 32))"
.file "swap.c"
.text
.globl swap
.type swap, @function
swap:
kd_entry myentry "true"
kd_assign save_olda olda "(select ram32 RDI)"
kd_assign save_oldb oldb "(select ram32 RSI)"
.LFB0:
.cfi_startproc
endbr64
movl (%rdi), %eax
movl (%rsi), %edx
movl %edx, (%rdi)
movl %eax, (%rsi)
kd_exit myexit "(and (= (select ram32 RSI) olda) (= (select ram32 RDI) oldb))"
ret
.cfi_endproc
Overwriting /tmp/swap.S
! python3 -m kdrag.contrib.pcode /tmp/swap.S
Processing /tmp/swap.S with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing SpecStmt: Assign(label='save_olda', addr=4194304, name='olda', expr=ram32[RDI])
Executing SpecStmt: Assign(label='save_oldb', addr=4194304, name='oldb', expr=ram32[RSI])
Executing 0x400000/4: ENDBR64 at (4194304, 0) PCODE IMARK ram[400000:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 0) PCODE IMARK ram[400004:2]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 1) PCODE unique[de00:4] = *[ram]RDI
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 2) PCODE EAX = unique[de00:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 3) PCODE RAX = zext(EAX)
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 0) PCODE IMARK ram[400006:2]
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 1) PCODE unique[de00:4] = *[ram]RSI
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 2) PCODE EDX = unique[de00:4]
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 3) PCODE RDX = zext(EDX)
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 0) PCODE IMARK ram[400008:2]
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 1) PCODE unique[6a80:4] = EDX
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 2) PCODE *[ram]RDI = unique[6a80:4]
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 0) PCODE IMARK ram[40000a:2]
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 1) PCODE unique[6a80:4] = EAX
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 2) PCODE *[ram]RSI = unique[6a80:4]
Executing SpecStmt: Exit(myexit, 0x40000c, And(ram32[RSI] == olda, ram32[RDI] == oldb))
Checking verification conditions...
---------------------------------------------
[❌] Exit(myexit, 0x40000c, And(ram32[RSI] == olda, ram32[RDI] == oldb))
Trace:
Entry(myentry, 0x400000, True)
0x400000/4: ENDBR64
0x400004/2: MOV EAX,dword ptr [RDI]
0x400006/2: MOV EDX,dword ptr [RSI]
0x400008/2: MOV dword ptr [RDI],EDX
0x40000a/2: MOV dword ptr [RSI],EAX
Exit(myexit, 0x40000c, And(ram32[RSI] == olda, ram32[RDI] == oldb))
Countermodel:
{olda: 134316064,
oldb: 2149580800,
RSI: 18446744073709551612,
RDI: 18446744073709551614,
ram32[RDI]: 2149582849,
ram32[RSI]: 134316064}
---------------------------------------------
❌❌❌❌ 1 verification conditions failed. ❌❌❌❌
.asmspec ELF section
The “/tmp/knuckle” include file now pushes the spec information to be saved in a new section. I think this capability is really useful for assembly verification tooling to have a target. This is sort of a simpler version of the idea of trying to piggy back on DWARF https://www.philipzucker.com/pcode2c-dwarf/ . It’s not that complicated. I’ve also enabled using local labels if you don’t want to pollute your symbol space.
# For injection of SMT commands, e.g., declare-const
.macro kd_prelude expr
.pushsection .asmspec,"a"
.ascii "kd_prelude \"\expr\"\n"
.popsection
.endm
.macro kd_always expr
.pushsection .asmspec,"a"
.ascii "kd_always \"\expr\"\n"
.popsection
.endm
.macro kd_boolstmt kind label expr
.pushsection .asmspec,"a"
.ascii "\kind \label \"\expr\" \n"
.popsection
\label:
.endm
# symbolic execution start points and precondition
.macro kd_entry label smt_bool
kd_boolstmt "kd_entry" \label \smt_bool
.endm
# Assert properties
.macro kd_assert label smt_bool
kd_boolstmt "kd_assert" \label \smt_bool
.endm
.macro kd_assume label smt_bool
kd_boolstmt "kd_assume" \label \smt_bool
.endm
# symbolic execution end points and postcondition
.macro kd_exit label smt_bool
kd_boolstmt "kd_entry" \label \smt_bool
.endm
# invariant
.macro kd_cut label smt_bool
kd_boolstmt "kd_cut" \label \smt_bool
.endm
# For manipulation of executor ghost state. Often for saving values
.macro kd_assign label name value
.pushsection .asmspec,"a"
.ascii "kd_assign \label \name \"\value\"\n"
.popsection
\label :
.endm
Right now, running my CLI assembles to a file /tmp/kdrag_temp.o which is convenient for my debugging. We can quickly inspect the .asmspec section here. It is in the same format as the annotations, enabling taking in specs via inline annotations, from the section, or from a separate spec file.
! objdump --full-contents /tmp/kdrag_temp.o
/tmp/kdrag_temp.o: file format elf64-x86-64
Contents of section .text:
0000 f30f1efa 8b078b16 89178906 c3 .............
Contents of section .asmspec:
0000 6b645f70 72656c75 64652022 28646563 kd_prelude "(dec
0010 6c617265 2d636f6e 7374206f 6c646120 lare-const olda
0020 285f2042 69745665 63203332 2929220a (_ BitVec 32))".
0030 6b645f70 72656c75 64652022 28646563 kd_prelude "(dec
0040 6c617265 2d636f6e 7374206f 6c646220 lare-const oldb
0050 285f2042 69745665 63203332 2929220a (_ BitVec 32))".
0060 6b645f65 6e747279 206d7965 6e747279 kd_entry myentry
0070 20227472 75652220 0a6b645f 61737369 "true" .kd_assi
0080 676e2073 6176655f 6f6c6461 206f6c64 gn save_olda old
0090 61202228 73656c65 63742072 616d3332 a "(select ram32
00a0 20524449 29220a6b 645f6173 7369676e RDI)".kd_assign
00b0 20736176 655f6f6c 6462206f 6c646220 save_oldb oldb
00c0 22287365 6c656374 2072616d 33322052 "(select ram32 R
00d0 53492922 0a6b645f 656e7472 79206d79 SI)".kd_entry my
00e0 65786974 20222861 6e642028 3d287365 exit "(and (=(se
00f0 6c656374 2072616d 33322052 5349296f lect ram32 RSI)o
0100 6c646129 283d2873 656c6563 74207261 lda)(=(select ra
0110 6d333220 52444929 6f6c6462 29292220 m32 RDI)oldb))"
0120 0a .
Contents of section .eh_frame:
0000 14000000 00000000 017a5200 01781001 .........zR..x..
0010 1b0c0708 90010000 14000000 1c000000 ................
0020 00000000 0d000000 00000000 00000000 ................
Inline ASM
You can add inline assembly in C files. At ABI boundaries, you’ve got a good chance of knowing where things are going. This is again an advantage I recieve from using regular GAS macros on regular assembly files as my specs.
I could perhaps work on using the annotations available in extended asm to read from C variables, but I’d need to translate from the GAS names of registers to the Pcode names. Not insurmountable if useful. Here I’m using them (: "r"(res)) just to try and force the ordering of where my annotations will be placed. Where inline asm goes in the output is not really that reliable afaik.
%%file /tmp/test.c
#include <stddef.h>
#include <stdint.h>
__asm__ (".include \"/tmp/knuckle.s\"");
uint64_t add42(uint64_t x) {
__asm__ volatile ("kd_entry myfun \"true\"");
uint64_t res = x + 42;
__asm__ volatile ("kd_exit myexit \"(= RAX (bvadd RDI (_ bv42 64)))\""
:
: "r"(res)
: );
return res;
}
Writing /tmp/test.c
! gcc -c -O1 -S /tmp/test.c -o /tmp/test.s && cat /tmp/test.s
.file "test.c"
.text
#APP
.include "/tmp/knuckle.s"
#NO_APP
.globl add42
.type add42, @function
add42:
.LFB0:
.cfi_startproc
endbr64
#APP
# 6 "/tmp/test.c" 1
kd_entry myfun "true"
# 0 "" 2
#NO_APP
leaq 42(%rdi), %rax
#APP
# 8 "/tmp/test.c" 1
kd_exit myexit "(= RAX (bvadd RDI (_ bv42 64)))"
# 0 "" 2
#NO_APP
ret
.cfi_endproc
.LFE0:
.size add42, .-add42
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
! python3 -m kdrag.contrib.pcode /tmp/test.s
Processing /tmp/test.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing 0x400004/4: LEA RAX,[RDI + 0x2a] at (4194308, 0) PCODE IMARK ram[400004:4]
Executing 0x400004/4: LEA RAX,[RDI + 0x2a] at (4194308, 1) PCODE unique[4700:8] = RDI + 0x2a
Executing 0x400004/4: LEA RAX,[RDI + 0x2a] at (4194308, 2) PCODE RAX = unique[4700:8]
Executing SpecStmt: Exit(myexit, 0x400008, RAX == RDI + 42)
Checking verification conditions...
[✅] Exit(myexit, 0x400008, RAX == RDI + 42)
✅✅✅✅ All 1 verification conditions passed! ✅✅✅✅
Cuts / Invariants
Here is a toy memcopy example. It has a loop which I can help verify using a cut annotation.
This reduces the very large number of trace fragments to just 4
- Entry to cut (loop entry)
- entry to exit (there is a short circuit path that avoids the loop)
- cut to cut (staying in the loop)
- cut to exit (leaving the loop)
It is somewhat painful and explicit to list all the needed invariants, all the relevant things that haven’t changed. I am torn on whether leaving things verbose is ok or whether to start sugaring and inferring stuff. Assembly ought to be kind of explicit. Inferring things (like frames) starts to become subjective, complicated and brittle. But we’ll see.
%%file /tmp/mymemcpy.c
#include <stddef.h>
void mymemcpy(int *dst, const int *src, size_t n) {
for (size_t i = 0; i < n; i++) {
dst[i] = src[i];
}
return;
}
Writing /tmp/mymemcpy.c
! gcc -c -O1 -S /tmp/mymemcpy.c -o /tmp/mymemcpy.s && cat /tmp/mymemcpy.s
.file "mymemcpy.c"
.text
.globl mymemcpy
.type mymemcpy, @function
mymemcpy:
.LFB0:
.cfi_startproc
endbr64
testq %rdx, %rdx
je .L1
movl $0, %eax
.L3:
movl (%rsi,%rax,4), %ecx
movl %ecx, (%rdi,%rax,4)
addq $1, %rax
cmpq %rax, %rdx
jne .L3
.L1:
ret
.cfi_endproc
.LFE0:
.size mymemcpy, .-mymemcpy
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
We copy out the relevant bits and add annotations again. As a technical point, using the constant offset rather than using a forall in the postcondition let’s us see the countermodel. The solver may or may not be slightly happier with this form also.
%%file /tmp/mymemcpy.s
.include "/tmp/knuckle.s"
kd_prelude "(declare-const offset (_ BitVec 64))"
.text
.globl mymemcpy
.type mymemcpy, @function
kd_entry mymemcpy "(and (= RDI (_ bv0 64)) (= RSI (_ bv1024 64)) (bvuge RDX (_ bv0 64)) (bvult RDX (_ bv32 64)))"
.LFB0:
.cfi_startproc
endbr64
testq %rdx, %rdx
je .L1
movl $0, %eax
.L3:
kd_cut mycut "(and (= RDI (_ bv0 64)) (= RSI (_ bv1024 64)) (bvuge RDX (_ bv0 64)) (bvult RDX (_ bv32 64)) (bvult RAX RDX) (forall ((offset (_ BitVec 64))) (=> (and (bvuge offset (_ bv0 64)) (bvult offset RAX)) (= (select ram32 (bvadd RDI (bvshl offset (_ bv2 64)))) (select ram32 (bvadd RSI (bvshl offset (_ bv2 64))))))))"
movl (%rsi,%rax,4), %ecx
movl %ecx, (%rdi,%rax,4)
addq $1, %rax
cmpq %rax, %rdx
jne .L3
.L1:
kd_exit myexit "(=> (and (bvuge offset (_ bv0 64)) (bvult offset RDX)) (= (select ram32 (bvadd RDI (bvshl offset (_ bv2 64)))) (select ram32 (bvadd RSI (bvshl offset (_ bv2 64))))))"
ret
.cfi_endproc
Overwriting /tmp/mymemcpy.s
! python3 -m kdrag.contrib.pcode /tmp/mymemcpy.s
Processing /tmp/mymemcpy.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing 0x400000/4: ENDBR64 at (4194304, 0) PCODE IMARK ram[400000:4]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 0) PCODE IMARK ram[40000e:3]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 1) PCODE unique[4900:8] = RAX * 0x4
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 2) PCODE unique[4a00:8] = RSI + unique[4900:8]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 3) PCODE unique[de00:4] = *[ram]unique[4a00:8]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 4) PCODE ECX = unique[de00:4]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 5) PCODE RCX = zext(ECX)
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 0) PCODE IMARK ram[400011:3]
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 1) PCODE unique[4900:8] = RAX * 0x4
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 2) PCODE unique[4a00:8] = RDI + unique[4900:8]
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 3) PCODE unique[6a80:4] = ECX
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 4) PCODE *[ram]unique[4a00:8] = unique[6a80:4]
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 0) PCODE IMARK ram[400014:4]
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 1) PCODE CF = carry(RAX, 0x1)
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 2) PCODE OF = scarry(RAX, 0x1)
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 3) PCODE RAX = RAX + 0x1
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 4) PCODE SF = RAX s< 0x0
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 5) PCODE ZF = RAX == 0x0
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 6) PCODE unique[28080:8] = RAX & 0xff
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 7) PCODE unique[28100:1] = popcount(unique[28080:8])
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 8) PCODE unique[28180:1] = unique[28100:1] & 0x1
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 9) PCODE PF = unique[28180:1] == 0x0
Executing 0x400018/3: CMP RDX,RAX at (4194328, 0) PCODE IMARK ram[400018:3]
Executing 0x400018/3: CMP RDX,RAX at (4194328, 1) PCODE unique[3af00:8] = RDX
Executing 0x400018/3: CMP RDX,RAX at (4194328, 2) PCODE CF = unique[3af00:8] < RAX
Executing 0x400018/3: CMP RDX,RAX at (4194328, 3) PCODE OF = sborrow(unique[3af00:8], RAX)
Executing 0x400018/3: CMP RDX,RAX at (4194328, 4) PCODE unique[3b000:8] = unique[3af00:8] - RAX
Executing 0x400018/3: CMP RDX,RAX at (4194328, 5) PCODE SF = unique[3b000:8] s< 0x0
Executing 0x400018/3: CMP RDX,RAX at (4194328, 6) PCODE ZF = unique[3b000:8] == 0x0
Executing 0x400018/3: CMP RDX,RAX at (4194328, 7) PCODE unique[28080:8] = unique[3b000:8] & 0xff
Executing 0x400018/3: CMP RDX,RAX at (4194328, 8) PCODE unique[28100:1] = popcount(unique[28080:8])
Executing 0x400018/3: CMP RDX,RAX at (4194328, 9) PCODE unique[28180:1] = unique[28100:1] & 0x1
Executing 0x400018/3: CMP RDX,RAX at (4194328, 10) PCODE PF = unique[28180:1] == 0x0
Executing 0x40001b/2: JNZ 0x40000e at (4194331, 0) PCODE IMARK ram[40001b:2]
Executing 0x40001b/2: JNZ 0x40000e at (4194331, 1) PCODE unique[e800:1] = !ZF
Executing 0x40001b/2: JNZ 0x40000e at (4194331, 2) PCODE if (unique[e800:1]) goto ram[40000e:8]
Executing SpecStmt: Cut(mycut, 0x40000e, And(RDI == 0,
RSI == 1024,
UGE(RDX, 0),
ULT(RDX, 32),
ULT(RAX, RDX),
ForAll(offset,
Implies(And(UGE(offset, 0), ULT(offset, RAX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))))
Executing SpecStmt: Exit(myexit, 0x40001d, Implies(And(UGE(offset, 0), ULT(offset, RDX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))
Executing 0x400004/3: TEST RDX,RDX at (4194308, 0) PCODE IMARK ram[400004:3]
Executing 0x400004/3: TEST RDX,RDX at (4194308, 1) PCODE CF = 0x0
Executing 0x400004/3: TEST RDX,RDX at (4194308, 2) PCODE OF = 0x0
Executing 0x400004/3: TEST RDX,RDX at (4194308, 3) PCODE unique[6c280:8] = RDX & RDX
Executing 0x400004/3: TEST RDX,RDX at (4194308, 4) PCODE SF = unique[6c280:8] s< 0x0
Executing 0x400004/3: TEST RDX,RDX at (4194308, 5) PCODE ZF = unique[6c280:8] == 0x0
Executing 0x400004/3: TEST RDX,RDX at (4194308, 6) PCODE unique[28080:8] = unique[6c280:8] & 0xff
Executing 0x400004/3: TEST RDX,RDX at (4194308, 7) PCODE unique[28100:1] = popcount(unique[28080:8])
Executing 0x400004/3: TEST RDX,RDX at (4194308, 8) PCODE unique[28180:1] = unique[28100:1] & 0x1
Executing 0x400004/3: TEST RDX,RDX at (4194308, 9) PCODE PF = unique[28180:1] == 0x0
Executing 0x400007/2: JZ 0x40001d at (4194311, 0) PCODE IMARK ram[400007:2]
Executing 0x400007/2: JZ 0x40001d at (4194311, 1) PCODE if (ZF) goto ram[40001d:8]
Executing 0x400009/5: MOV EAX,0x0 at (4194313, 0) PCODE IMARK ram[400009:5]
Executing 0x400009/5: MOV EAX,0x0 at (4194313, 1) PCODE RAX = 0x0
Executing SpecStmt: Cut(mycut, 0x40000e, And(RDI == 0,
RSI == 1024,
UGE(RDX, 0),
ULT(RDX, 32),
ULT(RAX, RDX),
ForAll(offset,
Implies(And(UGE(offset, 0), ULT(offset, RAX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))))
Executing SpecStmt: Exit(myexit, 0x40001d, Implies(And(UGE(offset, 0), ULT(offset, RDX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))
Checking verification conditions...
[✅] Exit(myexit, 0x40001d, Implies(And(UGE(offset, 0), ULT(offset, RDX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))
[✅] Cut(mycut, 0x40000e, And(RDI == 0,
RSI == 1024,
UGE(RDX, 0),
ULT(RDX, 32),
ULT(RAX, RDX),
ForAll(offset,
Implies(And(UGE(offset, 0), ULT(offset, RAX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))))
[✅] Exit(myexit, 0x40001d, Implies(And(UGE(offset, 0), ULT(offset, RDX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))
[✅] Cut(mycut, 0x40000e, And(RDI == 0,
RSI == 1024,
UGE(RDX, 0),
ULT(RDX, 32),
ULT(RAX, RDX),
ForAll(offset,
Implies(And(UGE(offset, 0), ULT(offset, RAX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))))
✅✅✅✅ All 4 verification conditions passed! ✅✅✅✅
Bits and Bobbles
The intention is to be sound/complete. For that, I have used a flat memory model that allows for fully symbolic addresses. There are always going to be issues in regards to soundness of the model with respect ot reality. The solutions is to work towards making it better.
Some known soundness issues / concerns:
- I don’t think ghidra semantics updates RIP explicitly. So maybe I need to mirror the
- MMIO and interrupts are of interest and I don’t know how to model them. My best guess is I’ll need the ability to plug in custom models that run between each instructions
- I’m not sure what dividing by 0 or other interrupt throwing instructions will lift to
- I’m not modelling memory permissions yet or relatedly TLB stuff
- No fancy memory model in regards to fences and what have you. Concurrent code.
- I’m not sure any alignment issues will be detected
- The code is loaded at whereever cle says too. Could make loading location symbolic by adding an uninterpreted offset to it
- Other loaded code is not avaiable
- Dynamically generated or self modifying code is not modelled.
Since last time, I have
- Made better countermodel printing
- Wired through support for 32 bit archs
- Made a command line interface
- Have specs being tossed in an asmspec section
- Bigger examples
TODO:
- kd_load for constants that need to be loaded into ram. kd_end_load
- kd_always
- Checking memory reads and writes aren’t really state functions. Hmm. Make ghost tag memory that is a boolean array stating what has been read or written to.
- equivalence checking. kd_sync mylabel “(rax + 7)” kd_sync mylabel “(select ram 17)” Two expressions that should be equal. kd_sync_all? ghost_channels? kd_send mylabel “expr”. kd_recv varname mylabel. Could just enable reading the ghost vars of the other one. And give a fixed composition ordering. Or just tying all labels? kd_sync_cut ?
- bigger more interesting examples. simd?
- Still unclear if hitting Entry should be something like hitting a sealed precondition (whether entry is also a trace killer). I’d need to track which entry can reach which exits to make this work.
- true / false shortcuts
- trace limit, step bounds
- Interactive VC
- tagged memory model (ghost tags)? Taint properties. Actually enable cheriot. which memory touched
- emit reachable addresses
- What does happen when I div 0? Read from unreadable? Mark as read write execute. syscalls?
- kd_observe ghostvar for things to injecg
- kd_decreases. refer to a cut? Globally attach to all cuts?
- elf2/dewarf2asmspec dwarf verification
- writes reads translation validation annotations (extra observations)
- Try new archteicture. wasm nand2tetris td4
- PC is fishy. Ability to read simulator addr?
- external spec file
- Read spec from section
- switch to select32
- Clean up output to be more interpretable
- multiline specs
- DMA challenge problem. MMIO modeling
- Interrupt challenge problem.
- What does div0 do?
- Using C/rust as spec functions. Reflection of simple code to spec. kd_define myfun Reg1 reg2 res. different from entry? Useful for kani/cbmc spec sharing.
- Speerate labels from annotatins. Multiple annotation allowed per label. Placable anywhere. relative label annotation? Then I don’t have to have label in binary. Hmm.
- show trace starting state
- Name traces by start label, VC label, and ordered branches.
myentry.0.0.1.myvcLet CLI pick particular ones. Print out execution with this label.
Done:
- unbalanced parens
- objcopy into biary data. pushsection popsection. local labels https://discuss.systems/@pkhuong/114939754477593015
- 32 bit arch
- Make CLI.
- better countermodel presentation. could always be btter
- Countermodel should maybe include variables from entry condition also.
Memcopy example Play with devices on pico or arduino or something. esp32?
Build toy compiler to output
Floyd flowcharts https://userweb.cs.txstate.edu/~rp31/papersSQ/Floyd.pdf Very interesting. Quite similar to what I’ve been doing. The labelled flowchart is the proof object? Akin to cyclic proofs. What if we took non well founded set something? Then well foundedness is less of a concern. The tree nature of ordinary proofs is like comitting to structured programming. Maybe we’re missing out on something here.
verilog co-verification
https://www.philipzucker.com/assembly_verify/ https://www.philipzucker.com/asm_verify2/
Local labels and pushsection popsection
euclids algo. Sum 1 - n Knuth stuff? list reversal. memcpy s2n examples frama-c vst examples verifast
maybe look at ada stuff?
https://vst.cs.princeton.edu/veric/ vst book. interesting
https://xavierleroy.org/CdF/2023-2024/8.pdf https://xavierleroy.org/CdF/2020-2021/ program logics https://github.com/xavierleroy/cdf-program-logics https://github.com/xavierleroy/cdf-mech-sem
Annotated flochart –> VCs as a semantics. That’s an interesting persepctive.
gries science of programming
typed assembly pcc - knuckeldragger proof objects foundational pcc
If I wanted to hack a C compiler https://sr.ht/~mcf/cproc/ Ember suggestes https://c9x.me/compile/users.html
https://www.youtube.com/watch?v=E-p0HP5bHzQ&t=2772s Michael Sammler - RefinedC: Automating the Foundational Verification of C w/ Refined Ownership Types
ctf security efnorcement? cheri? New pcode semantics? incorrectness logic https://riscv.github.io/riscv-cheri/ https://cheriot.org/cheri/toolchain/2025/03/17/mpact_cheriot.html
Bigger Examples
wp-manual hoare model, typed model, bytes model, region model
assigns foundational pcc
inject helpers?
writeable readable tagged memory
https://diffblue.github.io/cbmc/contracts-requires-ensures.html https://arxiv.org/pdf/2302.02384
is_fresh is interesting way of saying no alias
havoc useful?
https://www.cprover.org/cprover-manual/api/
Swap
%%file /tmp/swap.c
#include <stddef.h>
/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a,int *b);
void swap(int *a,int *b)
__CPROVER_requires( __CPROVER_is_fresh(b, sizeof(*b)) && __CPROVER_is_fresh(a, sizeof(*a)) && sizeof(*a) == sizeof(*b) &&
a != NULL && b != NULL)
__CPROVER_assigns(*a)
__CPROVER_assigns(*b)
{
__CPROVER_assume( __CPROVER_is_fresh(b, sizeof(*b)) && __CPROVER_is_fresh(a, sizeof(*a)) && sizeof(*a) == sizeof(*b) &&
a != NULL && b != NULL);
int tmp = *a ;
*a = *b ;
*b = tmp ;
return ;
}
Overwriting /tmp/swap.c
! cbmc /tmp/swap.c --function swap
CBMC version 6.7.1 (cbmc-6.7.1) 64-bit x86_64 linux
Type-checking swap
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is UNSATISFIABLE
** Results:
/tmp/swap.c function swap
[2m[swap.no-body.__CPROVER_is_fresh] [0mline 16 no body for callee __CPROVER_is_fresh: [31mFAILURE[0m
[2m[swap.pointer_dereference.1] [0mline 18 dereference failure: pointer NULL in *a: [32mSUCCESS[0m
[2m[swap.pointer_dereference.2] [0mline 18 dereference failure: pointer invalid in *a: [32mSUCCESS[0m
[2m[swap.pointer_dereference.3] [0mline 18 dereference failure: deallocated dynamic object in *a: [32mSUCCESS[0m
[2m[swap.pointer_dereference.4] [0mline 18 dereference failure: dead object in *a: [32mSUCCESS[0m
[2m[swap.pointer_dereference.5] [0mline 18 dereference failure: pointer outside object bounds in *a: [32mSUCCESS[0m
[2m[swap.pointer_dereference.6] [0mline 18 dereference failure: invalid integer address in *a: [32mSUCCESS[0m
[2m[swap.pointer_dereference.7] [0mline 19 dereference failure: pointer NULL in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.8] [0mline 19 dereference failure: pointer invalid in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.9] [0mline 19 dereference failure: deallocated dynamic object in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.10] [0mline 19 dereference failure: dead object in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.11] [0mline 19 dereference failure: pointer outside object bounds in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.12] [0mline 19 dereference failure: invalid integer address in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.13] [0mline 20 dereference failure: pointer NULL in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.14] [0mline 20 dereference failure: pointer invalid in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.15] [0mline 20 dereference failure: deallocated dynamic object in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.16] [0mline 20 dereference failure: dead object in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.17] [0mline 20 dereference failure: pointer outside object bounds in *b: [32mSUCCESS[0m
[2m[swap.pointer_dereference.18] [0mline 20 dereference failure: invalid integer address in *b: [32mSUCCESS[0m
** 1 of 19 failed (2 iterations)
VERIFICATION FAILED
! frama-c -wp -wp-verbose 0 -wp-rte /tmp/swap.c -then -report
[kernel] Parsing /tmp/swap.c (with preprocessing)
[rte:annot] annotating function swap
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'swap'
--------------------------------------------------------------------------------
[ Valid ] Post-condition 'A'
by Wp.typed.
[ Valid ] Post-condition 'B'
by Wp.typed.
[ Valid ] Exit-condition (generated)
by Unreachable Annotations.
[ Valid ] Termination-condition (generated)
by Trivial Termination.
[ Valid ] Assigns (file /tmp/swap.c, line 5)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file /tmp/swap.c, line 11)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file /tmp/swap.c, line 12)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file /tmp/swap.c, line 12)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file /tmp/swap.c, line 13)
by Wp.typed.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
10 Completely validated
10 Total
--------------------------------------------------------------------------------
! gcc -c -O1 -S /tmp/swap.c -o /tmp/swap.s && cat /tmp/swap.s
.file "swap.c"
.text
.globl swap
.type swap, @function
swap:
.LFB0:
.cfi_startproc
endbr64
movl (%rdi), %eax
movl (%rsi), %edx
movl %edx, (%rdi)
movl %eax, (%rsi)
ret
.cfi_endproc
.LFE0:
.size swap, .-swap
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
Maybe allowing global assumes would be useful for declaring intermediate constants? global asserts also? This is kind of too nice.
I would also like to see the ghost assignments in the trace
%%file /tmp/swap2.s
.include "/tmp/knuckle.s"
kd_prelude "(declare-const olda (_ BitVec 32))"
kd_prelude "(declare-const oldb (_ BitVec 32))"
kd_prelude "(declare-const gap (_ BitVec 64))"
#kd_prelude "(define-const mybv16 (_ bv16 64))" # seems to thrash bv16 notation
#kd_prelude "(define-fun has_gap ((x (_ BitVec 64)) (y (_ BitVec 64)) (g (_ BitVec 64))) (or (bvule (bvadd x y) g) "
#kd_prelude "(define-fun bvgap ((x (_ BitVec 64)) (y (_ BitVec 64)) (g (_ BitVec 64))) (distinct x (bvadd x 1) (bvadd x 2) (bvadd x 3) y (bvadd y 1) (bvadd y 2) (bvadd y 3))"
.globl swap
.type swap, @function
kd_entry swap "(and (= RDI (_ bv16 64)) (bvuge RSI (_ bv32 64)))"
#kd_entry swap "(and (bvule gap (_ (= (bvadd))"
.LFB0:
kd_assign save_olda olda "(select ram32 RDI)"
kd_assign save_oldb oldb "(select ram32 RSI)"
.cfi_startproc
endbr64
movl (%rdi), %eax
movl (%rsi), %edx
movl %edx, (%rdi)
movl %eax, (%rsi)
kd_exit myexit "(and (= (select ram32 RSI) olda) (= (select ram32 RDI) oldb))"
ret
.cfi_endproc
Overwriting /tmp/swap2.s
! python3 -m kdrag.contrib.pcode /tmp/swap2.s
Processing /tmp/swap2.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing SpecStmt: Assign(label='save_olda', addr=4194304, name='olda', expr=ram32[RDI])
Executing SpecStmt: Assign(label='save_oldb', addr=4194304, name='oldb', expr=ram32[RSI])
Executing 0x400000/4: ENDBR64 at (4194304, 0) PCODE IMARK ram[400000:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 0) PCODE IMARK ram[400004:2]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 1) PCODE unique[de00:4] = *[ram]RDI
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 2) PCODE EAX = unique[de00:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 3) PCODE RAX = zext(EAX)
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 0) PCODE IMARK ram[400006:2]
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 1) PCODE unique[de00:4] = *[ram]RSI
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 2) PCODE EDX = unique[de00:4]
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 3) PCODE RDX = zext(EDX)
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 0) PCODE IMARK ram[400008:2]
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 1) PCODE unique[6a80:4] = EDX
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 2) PCODE *[ram]RDI = unique[6a80:4]
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 0) PCODE IMARK ram[40000a:2]
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 1) PCODE unique[6a80:4] = EAX
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 2) PCODE *[ram]RSI = unique[6a80:4]
Executing SpecStmt: Exit(myexit, 0x40000c, And(ram32[RSI] == olda, ram32[RDI] == oldb))
Checking verification conditions...
[✅] Exit(myexit, 0x40000c, And(ram32[RSI] == olda, ram32[RDI] == oldb))
✅✅✅✅ All 1 verification conditions passed! ✅✅✅✅
! gcc -c /tmp/swap2.s -o /tmp/swap2.o
/tmp/swap2.s: Assembler messages:
/tmp/swap2.s:1: Error: can't open /tmp/knuckle.s for reading: No such file or directory
/tmp/swap2.s:2: Error: no such instruction: `kd_prelude "(declare-const olda (_ BitVec 32))"'
/tmp/swap2.s:3: Error: no such instruction: `kd_prelude "(declare-const oldb (_ BitVec 32))"'
/tmp/swap2.s:7: Error: no such instruction: `kd_entry swap "true"'
/tmp/swap2.s:9: Error: no such instruction: `kd_assign olda "(select ram32 RDI)"'
/tmp/swap2.s:10: Error: no such instruction: `kd_assign oldb "(select ram32 RSI)"'
/tmp/swap2.s:17: Error: no such instruction: `kd_exit myexit "(and (= (select ram32 RSI) olda)) (= (select ram32 RDI) oldb))"'
copy1
%%file /tmp/copy1.c
void copy1(int *src, int *dst){
*dst = *src;
return;
}
Overwriting /tmp/copy1.c
! gcc -c -O1 -S /tmp/copy1.c -o /tmp/copy1.s && cat /tmp/copy1.s
.file "copy1.c"
.text
.globl copy1
.type copy1, @function
copy1:
.LFB0:
.cfi_startproc
endbr64
movl (%rdi), %eax
movl %eax, (%rsi)
ret
.cfi_endproc
.LFE0:
.size copy1, .-copy1
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
%%file /tmp/copy1.s
.include "/tmp/knuckle.s"
.text
.globl copy1
.type copy1, @function
# Property fails if you comment this out. RDI and RSI cannot alias.
kd_entry copy1 "(distinct (bvadd RDI (_ bv1 64)) (bvadd RDI (_ bv2 64)) (bvadd RDI (_ bv3 64)) RSI (bvadd RSI (_ bv1 64)) (bvadd RSI (_ bv2 64)) (bvadd RSI (_ bv3 64)))"
.LFB0:
.cfi_startproc
endbr64
movl (%rdi), %eax
movl %eax, (%rsi)
kd_exit myexit "(= (select ram32 RSI) (select ram32 RDI))"
ret
.cfi_endproc
Overwriting /tmp/copy1.s
! python3 -m kdrag.contrib.pcode /tmp/copy1.s
Processing /tmp/copy1.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing 0x400000/4: ENDBR64 at (4194304, 0) PCODE IMARK ram[400000:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 0) PCODE IMARK ram[400004:2]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 1) PCODE unique[de00:4] = *[ram]RDI
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 2) PCODE EAX = unique[de00:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 3) PCODE RAX = zext(EAX)
Executing 0x400006/2: MOV dword ptr [RSI],EAX at (4194310, 0) PCODE IMARK ram[400006:2]
Executing 0x400006/2: MOV dword ptr [RSI],EAX at (4194310, 1) PCODE unique[6a80:4] = EAX
Executing 0x400006/2: MOV dword ptr [RSI],EAX at (4194310, 2) PCODE *[ram]RSI = unique[6a80:4]
Executing SpecStmt: Exit(myexit, 0x400008, ram32[RSI] == ram32[RDI])
Checking verification conditions...
[❌] Exit(myexit, 0x400008, ram32[RSI] == ram32[RDI])
---------------------------------------------
Trace:
Entry(copy1, 0x400000, Distinct(RDI + 1,
RDI + 2,
RDI + 3,
RSI,
RSI + 1,
RSI + 2,
RSI + 3))
0x400000/4: ENDBR64
0x400004/2: MOV EAX,dword ptr [RDI]
0x400006/2: MOV dword ptr [RSI],EAX
Exit(myexit, 0x400008, ram32[RSI] == ram32[RDI])
Countermodel:
{ram32[RSI]: 513,
ram32[RDI]: 512,
RSI: 144118647135587461,
RDI: 144118647135587464}
---------------------------------------------
❌❌❌❌ Some verification conditions failed. ❌❌❌❌
Memcopy
%%file /tmp/mymemcpy.c
#include <stddef.h>
void mymemcpy(int *dst, const int *src, size_t n) {
for (size_t i = 0; i < n; i++) {
dst[i] = src[i];
}
return;
}
Writing /tmp/mymemcpy.c
! gcc -c -O1 -S /tmp/mymemcpy.c -o /tmp/mymemcpy.s && cat /tmp/mymemcpy.s
.file "mymemcpy.c"
.text
.globl mymemcpy
.type mymemcpy, @function
mymemcpy:
.LFB0:
.cfi_startproc
endbr64
testq %rdx, %rdx
je .L1
movl $0, %eax
.L3:
movl (%rsi,%rax,4), %ecx
movl %ecx, (%rdi,%rax,4)
addq $1, %rax
cmpq %rax, %rdx
jne .L3
.L1:
ret
.cfi_endproc
.LFE0:
.size mymemcpy, .-mymemcpy
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
%%file /tmp/mymemcpy.s
.include "/tmp/knuckle.s"
kd_prelude "(declare-const offset (_ BitVec 64))"
.text
.globl mymemcpy
.type mymemcpy, @function
#kd_entry mymemcpy "(and (bvuge RDI (_ bv0 64)) (bvule RSI (_ bv128 64)))" # limit size
kd_entry mymemcpy "(and (= RDI (_ bv0 64)) (= RSI (_ bv1024 64)) (bvuge RDX (_ bv0 64)) (bvult RDX (_ bv32 64)))"
.LFB0:
.cfi_startproc
endbr64
testq %rdx, %rdx
je .L1
movl $0, %eax
.L3:
kd_cut mycut "(and (= RDI (_ bv0 64)) (= RSI (_ bv1024 64)) (bvuge RDX (_ bv0 64)) (bvult RDX (_ bv32 64)) (bvult RAX RDX) (forall ((offset (_ BitVec 64))) (=> (and (bvuge offset (_ bv0 64)) (bvult offset RAX)) (= (select ram32 (bvadd RDI (bvshl offset (_ bv2 64)))) (select ram32 (bvadd RSI (bvshl offset (_ bv2 64))))))))"
movl (%rsi,%rax,4), %ecx
movl %ecx, (%rdi,%rax,4)
addq $1, %rax
cmpq %rax, %rdx
jne .L3
.L1:
#kd_exit myexit "(forall ((offset (_ BitVec 64)) (= (select ram (bvadd RDI offset) (bvadd RSI offset)))"
#kd_exit myexit "(= (select ram RDI) (select ram RSI))"
#kd_exit myexit "(forall ((offset (_ BitVec 64))) (=> (and (bvuge offset (_ bv0 64)) (bvult offset RDX)) (= (select ram (bvadd RDI offset)) (select ram (bvadd RSI offset)))))"
kd_exit myexit "(=> (and (bvuge offset (_ bv0 64)) (bvult offset RDX)) (= (select ram32 (bvadd RDI (bvshl offset (_ bv2 64)))) (select ram32 (bvadd RSI (bvshl offset (_ bv2 64))))))"
#kd_exit myexit "(forall ((offset (_ BitVec 64)) true)"
ret
.cfi_endproc
Overwriting /tmp/mymemcpy.s
%%file /tmp/mymemcpy.s
.include "/tmp/knuckle.s"
kd_prelude "(define-const maxsize (_ BitVec 64) (_ bv64 64))"
kd_prelude "(define-const rsiaddr (_ BitVec 64) (_ bv1024 64))"
kd_prelude "(define-const rdiaddr (_ BitVec 64) (_ bv0 64))"
.text
.globl mymemcpy
.type mymemcpy, @function
kd_entry mymemcpy "(and (= RDI rdiaddr) (= RSI rsiaddr) (bvuge RDX (_ bv0 64)) (bvult RDX maxsize))"
.LFB0:
.cfi_startproc
endbr64
testq %rdx, %rdx
je .L1
movl $0, %eax
.L3:
# Loop invariant preserves stuff that is preserved and says that all memory up to offset RAX is copied
kd_cut mycut "(and (= RDI rdiaddr) (= RSI rsiaddr) (bvuge RDX (_ bv0 64)) (bvult RDX maxsize) (bvult RAX RDX) (forall ((offset (_ BitVec 64))) (=> (and (bvuge offset (_ bv0 64)) (bvult offset RAX)) (= (select ram32 (bvadd RDI (bvshl offset (_ bv2 64)))) (select ram32 (bvadd RSI (bvshl offset (_ bv2 64))))))))"
movl (%rsi,%rax,4), %ecx
movl %ecx, (%rdi,%rax,4)
addq $1, %rax
cmpq %rax, %rdx
jne .L3
.L1:
kd_prelude "(declare-const offset (_ BitVec 64))"
# everything up to RDX is copied
kd_exit myexit "(=> (and (bvuge offset (_ bv0 64)) (bvult offset RDX)) (= (select ram32 (bvadd RDI (bvshl offset (_ bv2 64)))) (select ram32 (bvadd RSI (bvshl offset (_ bv2 64))))))"
ret
.cfi_endproc
Overwriting /tmp/mymemcpy.s
! python3 -m kdrag.contrib.pcode /tmp/mymemcpy.s
Processing /tmp/mymemcpy.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing 0x400000/4: ENDBR64 at (4194304, 0) PCODE IMARK ram[400000:4]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 0) PCODE IMARK ram[40000e:3]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 1) PCODE unique[4900:8] = RAX * 0x4
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 2) PCODE unique[4a00:8] = RSI + unique[4900:8]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 3) PCODE unique[de00:4] = *[ram]unique[4a00:8]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 4) PCODE ECX = unique[de00:4]
Executing 0x40000e/3: MOV ECX,dword ptr [RSI + RAX*0x4] at (4194318, 5) PCODE RCX = zext(ECX)
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 0) PCODE IMARK ram[400011:3]
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 1) PCODE unique[4900:8] = RAX * 0x4
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 2) PCODE unique[4a00:8] = RDI + unique[4900:8]
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 3) PCODE unique[6a80:4] = ECX
Executing 0x400011/3: MOV dword ptr [RDI + RAX*0x4],ECX at (4194321, 4) PCODE *[ram]unique[4a00:8] = unique[6a80:4]
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 0) PCODE IMARK ram[400014:4]
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 1) PCODE CF = carry(RAX, 0x1)
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 2) PCODE OF = scarry(RAX, 0x1)
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 3) PCODE RAX = RAX + 0x1
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 4) PCODE SF = RAX s< 0x0
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 5) PCODE ZF = RAX == 0x0
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 6) PCODE unique[28080:8] = RAX & 0xff
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 7) PCODE unique[28100:1] = popcount(unique[28080:8])
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 8) PCODE unique[28180:1] = unique[28100:1] & 0x1
Executing 0x400014/4: ADD RAX,0x1 at (4194324, 9) PCODE PF = unique[28180:1] == 0x0
Executing 0x400018/3: CMP RDX,RAX at (4194328, 0) PCODE IMARK ram[400018:3]
Executing 0x400018/3: CMP RDX,RAX at (4194328, 1) PCODE unique[3af00:8] = RDX
Executing 0x400018/3: CMP RDX,RAX at (4194328, 2) PCODE CF = unique[3af00:8] < RAX
Executing 0x400018/3: CMP RDX,RAX at (4194328, 3) PCODE OF = sborrow(unique[3af00:8], RAX)
Executing 0x400018/3: CMP RDX,RAX at (4194328, 4) PCODE unique[3b000:8] = unique[3af00:8] - RAX
Executing 0x400018/3: CMP RDX,RAX at (4194328, 5) PCODE SF = unique[3b000:8] s< 0x0
Executing 0x400018/3: CMP RDX,RAX at (4194328, 6) PCODE ZF = unique[3b000:8] == 0x0
Executing 0x400018/3: CMP RDX,RAX at (4194328, 7) PCODE unique[28080:8] = unique[3b000:8] & 0xff
Executing 0x400018/3: CMP RDX,RAX at (4194328, 8) PCODE unique[28100:1] = popcount(unique[28080:8])
Executing 0x400018/3: CMP RDX,RAX at (4194328, 9) PCODE unique[28180:1] = unique[28100:1] & 0x1
Executing 0x400018/3: CMP RDX,RAX at (4194328, 10) PCODE PF = unique[28180:1] == 0x0
Executing 0x40001b/2: JNZ 0x40000e at (4194331, 0) PCODE IMARK ram[40001b:2]
Executing 0x40001b/2: JNZ 0x40000e at (4194331, 1) PCODE unique[e800:1] = !ZF
Executing 0x40001b/2: JNZ 0x40000e at (4194331, 2) PCODE if (unique[e800:1]) goto ram[40000e:8]
Executing SpecStmt: Cut(mycut, 0x40000e, And(RDI == 0,
RSI == 1024,
UGE(RDX, 0),
ULT(RDX, 64),
ULT(RAX, RDX),
ForAll(offset,
Implies(And(UGE(offset, 0), ULT(offset, RAX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))))
Executing SpecStmt: Exit(myexit, 0x40001d, Implies(And(UGE(offset, 0), ULT(offset, RDX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))
Executing 0x400004/3: TEST RDX,RDX at (4194308, 0) PCODE IMARK ram[400004:3]
Executing 0x400004/3: TEST RDX,RDX at (4194308, 1) PCODE CF = 0x0
Executing 0x400004/3: TEST RDX,RDX at (4194308, 2) PCODE OF = 0x0
Executing 0x400004/3: TEST RDX,RDX at (4194308, 3) PCODE unique[6c280:8] = RDX & RDX
Executing 0x400004/3: TEST RDX,RDX at (4194308, 4) PCODE SF = unique[6c280:8] s< 0x0
Executing 0x400004/3: TEST RDX,RDX at (4194308, 5) PCODE ZF = unique[6c280:8] == 0x0
Executing 0x400004/3: TEST RDX,RDX at (4194308, 6) PCODE unique[28080:8] = unique[6c280:8] & 0xff
Executing 0x400004/3: TEST RDX,RDX at (4194308, 7) PCODE unique[28100:1] = popcount(unique[28080:8])
Executing 0x400004/3: TEST RDX,RDX at (4194308, 8) PCODE unique[28180:1] = unique[28100:1] & 0x1
Executing 0x400004/3: TEST RDX,RDX at (4194308, 9) PCODE PF = unique[28180:1] == 0x0
Executing 0x400007/2: JZ 0x40001d at (4194311, 0) PCODE IMARK ram[400007:2]
Executing 0x400007/2: JZ 0x40001d at (4194311, 1) PCODE if (ZF) goto ram[40001d:8]
Executing 0x400009/5: MOV EAX,0x0 at (4194313, 0) PCODE IMARK ram[400009:5]
Executing 0x400009/5: MOV EAX,0x0 at (4194313, 1) PCODE RAX = 0x0
Executing SpecStmt: Cut(mycut, 0x40000e, And(RDI == 0,
RSI == 1024,
UGE(RDX, 0),
ULT(RDX, 64),
ULT(RAX, RDX),
ForAll(offset,
Implies(And(UGE(offset, 0), ULT(offset, RAX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))))
Executing SpecStmt: Exit(myexit, 0x40001d, Implies(And(UGE(offset, 0), ULT(offset, RDX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))
Checking verification conditions...
[✅] Exit(myexit, 0x40001d, Implies(And(UGE(offset, 0), ULT(offset, RDX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))
[✅] Cut(mycut, 0x40000e, And(RDI == 0,
RSI == 1024,
UGE(RDX, 0),
ULT(RDX, 64),
ULT(RAX, RDX),
ForAll(offset,
Implies(And(UGE(offset, 0), ULT(offset, RAX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))))
[✅] Exit(myexit, 0x40001d, Implies(And(UGE(offset, 0), ULT(offset, RDX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))
[✅] Cut(mycut, 0x40000e, And(RDI == 0,
RSI == 1024,
UGE(RDX, 0),
ULT(RDX, 64),
ULT(RAX, RDX),
ForAll(offset,
Implies(And(UGE(offset, 0), ULT(offset, RAX)),
ram32[RDI + (offset << 2)] ==
ram32[RSI + (offset << 2)]))))
✅✅✅✅ All 4 verification conditions passed! ✅✅✅✅
Doing simple BMC before attempting invariants is smart. Is there a way to keep both? It’d be nice to have starting state and ending state. It’d be nice to show state at each point.Also path conditions but this is harder Hard to parse what belongs to what
Reversing order of VC might be nice. We’re looking at bottom first right now
That it was kind of ok before I changed over to shifting is alarming. Only up to 32 bits is kind of hokey. It would be easy enough to just test this exhaustively
smtlib is painful and hard to read. Hmm. let helps. helper functions helps define-const is smart
frame conditions on loop do suck
I punted on aliasing by just pinning apart. Aliasing is a serious concern.
from kdrag.all import *
from kdrag.contrib.pcode.asmspec import assemble_and_gen_vcs
ctx, vcs = assemble_and_gen_vcs("/tmp/swap2.s")
vc = vcs[0]
print(str(smt.simplify(vc.vc(ctx).arg(1))))
Unexpected SP conflict
Executing SpecStmt: Assign(label='save_olda', addr=4194304, name='olda', expr=ram32[RDI])
Executing SpecStmt: Assign(label='save_oldb', addr=4194304, name='oldb', expr=ram32[RSI])
Executing 0x400000/4: ENDBR64 at (4194304, 0) PCODE IMARK ram[400000:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 0) PCODE IMARK ram[400004:2]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 1) PCODE unique[de00:4] = *[ram]RDI
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 2) PCODE EAX = unique[de00:4]
Executing 0x400004/2: MOV EAX,dword ptr [RDI] at (4194308, 3) PCODE RAX = zext(EAX)
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 0) PCODE IMARK ram[400006:2]
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 1) PCODE unique[de00:4] = *[ram]RSI
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 2) PCODE EDX = unique[de00:4]
Executing 0x400006/2: MOV EDX,dword ptr [RSI] at (4194310, 3) PCODE RDX = zext(EDX)
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 0) PCODE IMARK ram[400008:2]
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 1) PCODE unique[6a80:4] = EDX
Executing 0x400008/2: MOV dword ptr [RDI],EDX at (4194312, 2) PCODE *[ram]RDI = unique[6a80:4]
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 0) PCODE IMARK ram[40000a:2]
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 1) PCODE unique[6a80:4] = EAX
Executing 0x40000a/2: MOV dword ptr [RSI],EAX at (4194314, 2) PCODE *[ram]RSI = unique[6a80:4]
Executing SpecStmt: Exit(myexit, 0x40000c, And(ram32[RSI] == olda, ram32[RDI] == oldb))
And(Store(Store(Store(Store(Store(Store(Store(Store(ram(mem0),
RDI!539,
ram(mem0)[RSI!538]),
1 + RDI!539,
ram(mem0)[1 +
RSI!538]),
2 + RDI!539,
ram(mem0)[2 +
RSI!538]),
3 + RDI!539,
ram(mem0)[3 + RSI!538]),
RSI!538,
ram(mem0)[RDI!539]),
1 + RSI!538,
ram(mem0)[1 + RDI!539]),
2 + RSI!538,
ram(mem0)[2 + RDI!539]),
3 + RSI!538,
ram(mem0)[3 + RDI!539])[RDI!539] ==
ram(mem0)[RSI!538],
Store(Store(Store(Store(Store(Store(Store(Store(ram(mem0),
RDI!539,
ram(mem0)[RSI!538]),
1 + RDI!539,
ram(mem0)[1 +
RSI!538]),
2 + RDI!539,
ram(mem0)[2 +
RSI!538]),
3 + RDI!539,
ram(mem0)[3 + RSI!538]),
RSI!538,
ram(mem0)[RDI!539]),
1 + RSI!538,
ram(mem0)[1 + RDI!539]),
2 + RSI!538,
ram(mem0)[2 + RDI!539]),
3 + RSI!538,
ram(mem0)[3 + RDI!539])[1 + RDI!539] ==
ram(mem0)[1 + RSI!538],
Store(Store(Store(Store(Store(Store(Store(Store(ram(mem0),
RDI!539,
ram(mem0)[RSI!538]),
1 + RDI!539,
ram(mem0)[1 +
RSI!538]),
2 + RDI!539,
ram(mem0)[2 +
RSI!538]),
3 + RDI!539,
ram(mem0)[3 + RSI!538]),
RSI!538,
ram(mem0)[RDI!539]),
1 + RSI!538,
ram(mem0)[1 + RDI!539]),
2 + RSI!538,
ram(mem0)[2 + RDI!539]),
3 + RSI!538,
ram(mem0)[3 + RDI!539])[2 + RDI!539] ==
ram(mem0)[2 + RSI!538],
Store(Store(Store(Store(Store(Store(Store(Store(ram(mem0),
RDI!539,
ram(mem0)[RSI!538]),
1 + RDI!539,
ram(mem0)[1 +
RSI!538]),
2 + RDI!539,
ram(mem0)[2 +
RSI!538]),
3 + RDI!539,
ram(mem0)[3 + RSI!538]),
RSI!538,
ram(mem0)[RDI!539]),
1 + RSI!538,
ram(mem0)[1 + RDI!539]),
2 + RSI!538,
ram(mem0)[2 + RDI!539]),
3 + RSI!538,
ram(mem0)[3 + RDI!539])[3 + RDI!539] ==
ram(mem0)[3 + RSI!538])
Cleanup the verification condition. If we need to go manual, or debug, this is unacceptable.
kd_alias RAX kd_size “RAX” 4 # ? kd_object RAX 4 kd_separated kd_type RAX ctype
maybe ram32 is too cute. It is a weird construct. The different pieceso f the ram are aliased in an unpexected way (select32 ram RDI) (select16 ) (select8 )
smt.substitute(vc.vc(ctx).arg(1), (MemState.Const("mem0").mem.ram, smt.Lambda([addr], Select(ram64[addr], addr % 8, addr % 8 + 1)))
offset = 0
for name, vnode in ctx.vnodes.items():
if vnode.offset >= offset and len(name) < 4:
offset = vnode.offset + vnode.size
regfile = smt.FreshConst("regfile", smt.ArraySort(self.bits, self.bits))
ram = smt.FreshConsts( smt.ArraySort(self.bits, self.bits))
Sumn
%%file /tmp/sumn.c
#include <stdio.h>
#include <stdlib.h>
int sumn(int n) {
int sum = 0;
for (int i = 1; i <= n; i++) {
sum += i;
}
return sum;
}
Writing /tmp/sumn.c
! frama-c -eva /tmp/sumn.c
/bin/bash: line 1: framac: command not found
! gcc -c -O1 -S -o /tmp/sumn.s /tmp/sumn.c && cat /tmp/sumn.s
.file "sumn.c"
.text
.globl sumn
.type sumn, @function
sumn:
.LFB39:
.cfi_startproc
endbr64
testl %edi, %edi
jle .L4
addl $1, %edi
movl $1, %eax
movl $0, %edx
.L3:
addl %eax, %edx
addl $1, %eax
cmpl %edi, %eax
jne .L3
.L1:
movl %edx, %eax
ret
.L4:
movl $0, %edx
jmp .L1
.cfi_endproc
.LFE39:
.size sumn, .-sumn
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
%%file /tmp/sumarray.c
#include <stddef.h>
int sumarray(int *arr, size_t n) {
int sum = 0;
for (size_t i = 0; i < n; i++) {
sum += arr[i];
}
return sum;
}
Writing /tmp/sumarray.c
! frama-c
! gcc /tmp/sumarray.c -c -fverbose-asm -S -o /tmp/sumarray.s -O1 && cat /tmp/sumarray.s
.file "sumarray.c"
# GNU C17 (Ubuntu 13.3.0-6ubuntu2~24.04) version 13.3.0 (x86_64-linux-gnu)
# compiled by GNU C version 13.3.0, GMP version 6.3.0, MPFR version 4.2.1, MPC version 1.3.1, isl version isl-0.26-GMP
# GGC heuristics: --param ggc-min-expand=100 --param ggc-min-heapsize=131072
# options passed: -mtune=generic -march=x86-64 -O1 -fasynchronous-unwind-tables -fstack-protector-strong -fstack-clash-protection -fcf-protection
.text
.globl sumarray
.type sumarray, @function
sumarray:
.LFB0:
.cfi_startproc
endbr64
# /tmp/sumarray.c:4: for (size_t i = 0; i < n; i++) {
testq %rsi, %rsi # n
je .L4 #,
movq %rdi, %rax # arr, ivtmp.6
leaq (%rdi,%rsi,4), %rcx #, _19
# /tmp/sumarray.c:3: int sum = 0;
movl $0, %edx #, <retval>
.L3:
# /tmp/sumarray.c:5: sum += arr[i];
addl (%rax), %edx # MEM[(int *)_16], <retval>
# /tmp/sumarray.c:4: for (size_t i = 0; i < n; i++) {
addq $4, %rax #, ivtmp.6
cmpq %rcx, %rax # _19, ivtmp.6
jne .L3 #,
.L1:
# /tmp/sumarray.c:8: }
movl %edx, %eax # <retval>,
ret
.L4:
# /tmp/sumarray.c:3: int sum = 0;
movl $0, %edx #, <retval>
# /tmp/sumarray.c:7: return sum;
jmp .L1 #
.cfi_endproc
.LFE0:
.size sumarray, .-sumarray
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
%%file /tmp/copy.c
#include <stddef.h>
void mycopy(int *dest, const int *src, size_t n) {
for (size_t i = 0; i < n; i++) {
dest[i] = src[i];
}
}
Overwriting /tmp/copy.c
! gcc /tmp/copy.c -c -S -o /tmp/copy.s -O1 && cat /tmp/copy.s
.file "copy.c"
.text
.globl mycopy
.type mycopy, @function
mycopy:
.LFB0:
.cfi_startproc
endbr64
testq %rdx, %rdx
je .L1
movl $0, %eax
.L3:
movl (%rsi,%rax,4), %ecx
movl %ecx, (%rdi,%rax,4)
addq $1, %rax
cmpq %rax, %rdx
jne .L3
.L1:
ret
.cfi_endproc
.LFE0:
.size mycopy, .-mycopy
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
Better Countermodel
Maybe also print all ghost var or just add dummy conditions
kd_print “expr” kd_watch
Maybe suggest that some things may be aliasing. Suspicious looking numbers that are too close, or show up in selects.
%%file /tmp/mov42.s
.include "/tmp/knuckle.s"
.global _start
kd_entry _start "true"
movq $42, 8(%rsp)
kd_exit _start_end "(= (select ram (bvadd RSP (_ bv8 64))) (_ bv43 8))"
ret
Overwriting /tmp/mov42.s
! python3 -m kdrag.contrib.pcode /tmp/mov42.s
Processing /tmp/mov42.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing 0x400000/9: MOV qword ptr [RSP + 0x8],0x2a at (4194304, 0) PCODE IMARK ram[400000:9]
Executing 0x400000/9: MOV qword ptr [RSP + 0x8],0x2a at (4194304, 1) PCODE unique[4e00:8] = 0x8 + RSP
Executing 0x400000/9: MOV qword ptr [RSP + 0x8],0x2a at (4194304, 2) PCODE unique[6e80:8] = 0x2a
Executing 0x400000/9: MOV qword ptr [RSP + 0x8],0x2a at (4194304, 3) PCODE *[ram]unique[4e00:8] = unique[6e80:8]
Executing SpecStmt: Exit(_start_end, 0x400009, ram[RSP + 8] == 43)
Checking verification conditions...
[❌] Exit(_start_end, 0x400009, ram[RSP + 8] == 43)
---------------------------------------------
Trace:
Entry(_start, 0x400000, True)
0x400000/9: MOV qword ptr [RSP + 0x8],0x2a
Exit(_start_end, 0x400009, ram[RSP + 8] == 43)
Countermodel:
{ram[RSP + 8]: 42, RSP: 18446744073709551608}
---------------------------------------------
❌❌❌❌ Some verification conditions failed. ❌❌❌❌
32 bit
%%file /tmp/mov42.s
.include "/tmp/knuckle.s"
.text
.globl myfunc
kd_entry myfunc "true"
addi sp, sp, -4 # make room on the stack
li t0, 42 # t0 ← 42
sw t0, 0(sp) # [sp] = 42
kd_exit myfunc_end "(= (select ram32 sp) (_ bv42 32))"
ret
Overwriting /tmp/mov42.s
! python3 -m kdrag.contrib.pcode --help
Usage: python -m kdrag.contrib.pcode [OPTIONS] FILENAME
Simple program that greets NAME for a total of COUNT times.
Options:
--langid TEXT PCode language ID. Run `python3 -m pypcode --list` for
options
--asm TEXT Assembler to use. Default is 'as'.
--help Show this message and exit.
! python3 -m kdrag.contrib.pcode --langid="RISCV:LE:32:default" --asm /home/philip/Downloads/lowrisc-toolchain-gcc-rv32imcb-x86_64-20250710-1/bin/riscv32-unknown-elf-as /tmp/mov42.s
Processing /tmp/mov42.s with language ID RISCV:LE:32:default using assembler /home/philip/Downloads/lowrisc-toolchain-gcc-rv32imcb-x86_64-20250710-1/bin/riscv32-unknown-elf-as
Constructing Trace Fragments
Executing 0x400000/4: addi sp,sp,-0x4 at (4194304, 0) PCODE IMARK ram[400000:4]
Executing 0x400000/4: addi sp,sp,-0x4 at (4194304, 1) PCODE unique[580:4] = 0xfffffffc
Executing 0x400000/4: addi sp,sp,-0x4 at (4194304, 2) PCODE sp = sp + unique[580:4]
Executing 0x400004/4: li t0,0x2a at (4194308, 0) PCODE IMARK ram[400004:4]
Executing 0x400004/4: li t0,0x2a at (4194308, 1) PCODE unique[580:4] = 0x2a
Executing 0x400004/4: li t0,0x2a at (4194308, 2) PCODE t0 = unique[580:4]
Executing 0x400008/4: sw t0,0x0(sp) at (4194312, 0) PCODE IMARK ram[400008:4]
Executing 0x400008/4: sw t0,0x0(sp) at (4194312, 1) PCODE unique[600:4] = 0x0
Executing 0x400008/4: sw t0,0x0(sp) at (4194312, 2) PCODE unique[4180:4] = sp + unique[600:4]
Executing 0x400008/4: sw t0,0x0(sp) at (4194312, 3) PCODE *[ram]unique[4180:4] = t0
finish Exit(label='myfunc_end', addr=4194316, expr=ram32[sp] == 42) 0x40000c
[✅] VC(Entry(label='myfunc', addr=4194304, expr=True), ['0x400000', '0x400004', '0x400008'], Exit(label='myfunc_end', addr=4194316, expr=ram32[sp] == 42), {})
✅✅✅✅ All 1 verification conditions passed! ✅✅✅✅
from kdrag.contrib.pcode.asmspec import assemble_and_check
assemble_and_check("/tmp/mov42.s", langid="RISCV:LE:32:default", as_bin="riscv32-linux-gnu-as").successes
---------------------------------------------------------------------------
FileNotFoundError Traceback (most recent call last)
Cell In[8], line 2
1 from kdrag.contrib.pcode.asmspec import assemble_and_check
----> 2 assemble_and_check("/tmp/mov42.s", langid="RISCV:LE:32:default", as_bin="riscv32-linux-gnu-as").successes
File ~/Documents/python/knuckledragger/kdrag/contrib/pcode/asmspec.py:366, in assemble_and_check(filename, langid, as_bin)
363 def assemble_and_check(
364 filename: str, langid="x86:LE:64:default", as_bin="as"
365 ) -> Results:
--> 366 ctx, vcs = assemble_and_gen_vcs(filename, langid, as_bin)
367 res = Results()
368 for vc in vcs:
File ~/Documents/python/knuckledragger/kdrag/contrib/pcode/asmspec.py:357, in assemble_and_gen_vcs(filename, langid, as_bin)
355 f.write(kd_macro)
356 f.flush()
--> 357 subprocess.run([as_bin, filename, "-o", "/tmp/kdrag_temp.o"], check=True)
358 ctx = pcode.BinaryContext("/tmp/kdrag_temp.o", langid=langid)
359 spec = AsmSpec.of_file(filename, ctx)
File /usr/lib/python3.12/subprocess.py:548, in run(input, capture_output, timeout, check, *popenargs, **kwargs)
545 kwargs['stdout'] = PIPE
546 kwargs['stderr'] = PIPE
--> 548 with Popen(*popenargs, **kwargs) as process:
549 try:
550 stdout, stderr = process.communicate(input, timeout=timeout)
File /usr/lib/python3.12/subprocess.py:1026, in Popen.__init__(self, args, bufsize, executable, stdin, stdout, stderr, preexec_fn, close_fds, shell, cwd, env, universal_newlines, startupinfo, creationflags, restore_signals, start_new_session, pass_fds, user, group, extra_groups, encoding, errors, text, umask, pipesize, process_group)
1022 if self.text_mode:
1023 self.stderr = io.TextIOWrapper(self.stderr,
1024 encoding=encoding, errors=errors)
-> 1026 self._execute_child(args, executable, preexec_fn, close_fds,
1027 pass_fds, cwd, env,
1028 startupinfo, creationflags, shell,
1029 p2cread, p2cwrite,
1030 c2pread, c2pwrite,
1031 errread, errwrite,
1032 restore_signals,
1033 gid, gids, uid, umask,
1034 start_new_session, process_group)
1035 except:
1036 # Cleanup if the child failed starting.
1037 for f in filter(None, (self.stdin, self.stdout, self.stderr)):
File /usr/lib/python3.12/subprocess.py:1955, in Popen._execute_child(self, args, executable, preexec_fn, close_fds, pass_fds, cwd, env, startupinfo, creationflags, shell, p2cread, p2cwrite, c2pread, c2pwrite, errread, errwrite, restore_signals, gid, gids, uid, umask, start_new_session, process_group)
1953 err_msg = os.strerror(errno_num)
1954 if err_filename is not None:
-> 1955 raise child_exception_type(errno_num, err_msg, err_filename)
1956 else:
1957 raise child_exception_type(errno_num, err_msg)
FileNotFoundError: [Errno 2] No such file or directory: 'riscv32-linux-gnu-as'
import archinfo
info = archinfo.ArchPcode("RISCV:LE:32:default")
info.bits
32
Push pop
%%file /tmp/knuckle.s
# For injection of SMT commands, e.g., declare-const
.macro kd_prelude smt_command
.pushsection .asmspec,"a"
.ascii "kd_prelude \"\expr\"\n"
.popsection
.endm
.macro kd_always smt_bool
.pushsection .asmspec,"a"
.ascii "kd_always \"\expr\"\n"
.popsection
.endm
.macro kd_boolstmt kind label expr
.pushsection .asmspec,"a"
.ascii "\kind \label \"\expr\" \n"
.popsection
\label:
.endm
# symbolic execution start points and precondition
.macro kd_entry label smt_bool
kd_boolstmt "kd_entry" \label \smt_bool
.endm
# Assert properties
.macro kd_assert label smt_bool
kd_boolstmt "kd_assert" \label \smt_bool
.endm
.macro kd_assume label smt_bool
kd_boolstmt "kd_assume" \label \smt_bool
.endm
# symbolic execution end points and postcondition
.macro kd_exit label smt_bool
kd_boolstmt "kd_entry" \label \smt_bool
.endm
# invariant
.macro kd_cut label smt_bool
kd_boolstmt "kd_cut" \label \smt_bool
.endm
# For manipulation of executor ghost state. Often for saving values
.macro kd_assign label name value
.pushsection .asmspec,"a"
.ascii "kd_assign \"\expr\"\n"
.popsection
\label :
.endm
Overwriting /tmp/knuckle.s
%%file /tmp/test.s
.include "/tmp/knuckle.s"
.globl myfunc
.text
kd_entry myfunc "true"
kd_entry myfunc2 "true"
movq $42, %rax
kd_assert my_assert "(= RAX (_ bv42 64))"
kd_exit func_end "(= RAX (_ bv42 64))"
ret
Overwriting /tmp/test.s
! as /tmp/test.s -o /tmp/test.o && objdump -s /tmp/test.o
/tmp/test.o: file format elf64-x86-64
Contents of section .text:
0000 48c7c02a 000000c3 H..*....
Contents of section .asmspec:
0000 6b645f65 6e747279 206d7966 756e6320 kd_entry myfunc
0010 22747275 6522200a 6b645f65 6e747279 "true" .kd_entry
0020 206d7966 756e6332 20227472 75652220 myfunc2 "true"
0030 0a6b645f 61737365 7274206d 795f6173 .kd_assert my_as
0040 73657274 2022283d 52415820 285f2062 sert "(=RAX (_ b
0050 76343220 36342929 22200a6b 645f656e v42 64))" .kd_en
0060 74727920 66756e63 5f656e64 2022283d try func_end "(=
0070 52415820 285f2062 76343220 36342929 RAX (_ bv42 64))
0080 22200a " .
%%file /tmp/test.s
.include "/tmp/knuckle.s"
.globl myfunc
.text
kd_entry myfunc "true"
movq $42, %rax
kd_exit .Lfunc_end "(= RAX (_ bv42 64))"
ret
Overwriting /tmp/test.s
Local labels. Don’t pollute actual linking space. Ah, ok, I need to call the assembler with -L to support local labels
! python3 -m kdrag.contrib.pcode /tmp/test.s
Processing /tmp/test.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing 0x400000/7: MOV RAX,0x2a at (4194304, 0) PCODE IMARK ram[400000:7]
Executing 0x400000/7: MOV RAX,0x2a at (4194304, 1) PCODE RAX = 0x2a
Executing SpecStmt: Assert(my_assert, 0x400007, RAX == 42)
Executing SpecStmt: Exit(func_end, 0x400007, RAX == 42)
Checking verification conditions...
[✅] Assert(my_assert, 0x400007, RAX == 42)
[✅] Exit(func_end, 0x400007, RAX == 42)
✅✅✅✅ All 2 verification conditions passed! ✅✅✅✅
from kdrag.all import *
import kdrag.contrib.pcode as pcode
ctx = pcode.BinaryContext("/tmp/kdrag_temp.o")
sym = ctx.loader.find_symbol("")
Unexpected SP conflict
---------------------------------------------------------------------------
NameError Traceback (most recent call last)
Cell In[53], line 4
2 import kdrag.contrib.pcode as pcode
3 ctx = pcode.BinaryContext("/tmp/kdrag_temp.o")
----> 4 sym = ctx.loader.find_symbol(label)
NameError: name 'label' is not defined
! objdump -d /tmp/kdrag_temp.o
/tmp/kdrag_temp.o: file format elf64-x86-64
Disassembly of section .text:
0000000000000000 <.Lmyfunc>:
0: 48 c7 c0 2a 00 00 00 mov $0x2a,%rax
0000000000000007 <func_end>:
7: c3 ret
! python3 -m kdrag.contrib.pcode --help
Usage: python -m kdrag.contrib.pcode [OPTIONS] FILENAME
asmc - Assembly Checker A tool to check verification conditions for assembly
code using Ghidra PCode.
Example:
```/tmp/test.s
.include "/tmp/knuckle.s"
.globl myfunc
.text
kd_entry myfunc "true"
movq $42, %rax
kd_exit .Lfunc_end "(= RAX (_ bv42 64))"
ret
```
```
python3 -m kdrag.contrib.pcode /tmp/test.s
```
Options:
--langid TEXT PCode language ID. Run `python3 -m pypcode --list` for
options
--asm TEXT Assembler to use. Default is 'as'.
--print-macros Print annotation GAS macros. Give it a dummy filename
--help Show this message and exit.
inline asm
So yeah, it’s pretty hard to control where the inline asm might go. ABI boundaries are OK, maybe. If you need to actually constrain the compiler just to add these annotations, not so nice.
%%file /tmp/test.c
#include <stddef.h>
#include <stdint.h>
__asm__ (".include \"/tmp/knuckle.s\"");
uint64_t add42(uint64_t x) {
__asm__ volatile ("kd_entry myfun \"true\"");
uint64_t res = x + 42;
__asm__ volatile ("kd_exit myexit \"(= RAX (bvadd RDI (_ bv42 64)))\""
:
: "r"(res)
: );
return res;
}
Overwriting /tmp/test.c
! gcc -c -O1 -S /tmp/test.c -o /tmp/test.s && cat /tmp/test.s && as /tmp/test.s -o /tmp/test.o
.file "test.c"
.text
#APP
.include "/tmp/knuckle.s"
#NO_APP
.globl add42
.type add42, @function
add42:
.LFB0:
.cfi_startproc
endbr64
#APP
# 6 "/tmp/test.c" 1
kd_entry myfun "true"
# 0 "" 2
#NO_APP
leaq 42(%rdi), %rax
#APP
# 8 "/tmp/test.c" 1
kd_exit myexit "(= RAX (bvadd RDI (_ bv42 64)))"
# 0 "" 2
#NO_APP
ret
.cfi_endproc
.LFE0:
.size add42, .-add42
.ident "GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
.section .note.GNU-stack,"",@progbits
.section .note.gnu.property,"a"
.align 8
.long 1f - 0f
.long 4f - 1f
.long 5
0:
.string "GNU"
1:
.align 8
.long 0xc0000002
.long 3f - 2f
2:
.long 0x3
3:
.align 8
4:
! python3 -m kdrag.contrib.pcode /tmp/test.s
Processing /tmp/test.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing 0x400004/4: LEA RAX,[RDI + 0x2a] at (4194308, 0) PCODE IMARK ram[400004:4]
Executing 0x400004/4: LEA RAX,[RDI + 0x2a] at (4194308, 1) PCODE unique[4700:8] = RDI + 0x2a
Executing 0x400004/4: LEA RAX,[RDI + 0x2a] at (4194308, 2) PCODE RAX = unique[4700:8]
Executing SpecStmt: Exit(myexit, 0x400008, RAX == RDI + 42)
Checking verification conditions...
[✅] Exit(myexit, 0x400008, RAX == RDI + 42)
✅✅✅✅ All 1 verification conditions passed! ✅✅✅✅
External Spec File
pypcode supports an external SLA file describing the architecture. COuld be interesting for WASM, Cheri, describing mmio?
https://spinsel.dev/2020/06/17/ghidra-brainfuck-processor-1.html https://www.reddit.com/r/ghidra/comments/f5lk42/my_experience_writing_processor_modules/ https://github.com/nneonneo/ghidra-wasm-plugin https://github.com/rbran/sleigh-rs https://lib.rs/crates/tree-sitter-sleigh
asm school
https://github.com/FFmpeg/asm-lessons
arb and flint has handwritten stuff
https://blogs.gnome.org/rbultje/2017/07/14/writing-x86-simd-using-x86inc-asm/
s2n-bignum
https://github.com/awslabs/s2n-bignum/tree/main/arm/tutorial
“Note that symbolic simulator will discard the output of instructions if its inputs do not have their symbolic expressions defined in assumption. To list which instructions are discarded by the simulation tactic. set: arm_print_log := true;; This flag will also print helpful informations that are useful. “ Hmm. Is that useful?
%%file /tmp/simple.s
add x2, x1, x0
sub x2, x2, x1
Overwriting /tmp/simple.s
%%file /tmp/simple.s
.include "/tmp/knuckle.s"
.intel_syntax noprefix
.text
kd_prelude "(declare-const pc (_ BitVec 64))"
kd_prelude "(declare-const a (_ BitVec 64))"
kd_prelude "(declare-const b (_ BitVec 64))"
kd_entry myfunc "(and (= RAX a) (= RBX b) (= RIP pc))"
add rbx, rax
sub rbx, rax
kd_exit myfunc_end "(and (= RBX b) (= RIP (bvadd pc (_ bv6 64))))"
ret
Overwriting /tmp/simple.s
Hmm. Implicit RIP in semantics
! python3 -m kdrag.contrib.pcode /tmp/simple.s
Processing /tmp/simple.s with language ID x86:LE:64:default using assembler as
Constructing Trace Fragments...
Unexpected SP conflict
Executing 0x400000/3: ADD RBX,RAX at (4194304, 0) PCODE IMARK ram[400000:3]
Executing 0x400000/3: ADD RBX,RAX at (4194304, 1) PCODE CF = carry(RBX, RAX)
Executing 0x400000/3: ADD RBX,RAX at (4194304, 2) PCODE OF = scarry(RBX, RAX)
Executing 0x400000/3: ADD RBX,RAX at (4194304, 3) PCODE RBX = RBX + RAX
Executing 0x400000/3: ADD RBX,RAX at (4194304, 4) PCODE SF = RBX s< 0x0
Executing 0x400000/3: ADD RBX,RAX at (4194304, 5) PCODE ZF = RBX == 0x0
Executing 0x400000/3: ADD RBX,RAX at (4194304, 6) PCODE unique[28080:8] = RBX & 0xff
Executing 0x400000/3: ADD RBX,RAX at (4194304, 7) PCODE unique[28100:1] = popcount(unique[28080:8])
Executing 0x400000/3: ADD RBX,RAX at (4194304, 8) PCODE unique[28180:1] = unique[28100:1] & 0x1
Executing 0x400000/3: ADD RBX,RAX at (4194304, 9) PCODE PF = unique[28180:1] == 0x0
Executing 0x400003/3: SUB RBX,RAX at (4194307, 0) PCODE IMARK ram[400003:3]
Executing 0x400003/3: SUB RBX,RAX at (4194307, 1) PCODE CF = RBX < RAX
Executing 0x400003/3: SUB RBX,RAX at (4194307, 2) PCODE OF = sborrow(RBX, RAX)
Executing 0x400003/3: SUB RBX,RAX at (4194307, 3) PCODE RBX = RBX - RAX
Executing 0x400003/3: SUB RBX,RAX at (4194307, 4) PCODE SF = RBX s< 0x0
Executing 0x400003/3: SUB RBX,RAX at (4194307, 5) PCODE ZF = RBX == 0x0
Executing 0x400003/3: SUB RBX,RAX at (4194307, 6) PCODE unique[28080:8] = RBX & 0xff
Executing 0x400003/3: SUB RBX,RAX at (4194307, 7) PCODE unique[28100:1] = popcount(unique[28080:8])
Executing 0x400003/3: SUB RBX,RAX at (4194307, 8) PCODE unique[28180:1] = unique[28100:1] & 0x1
Executing 0x400003/3: SUB RBX,RAX at (4194307, 9) PCODE PF = unique[28180:1] == 0x0
Executing SpecStmt: Exit(myfunc_end, 0x400006, And(RBX == b, RIP == pc + 6))
Checking verification conditions...
[❌] Exit(myfunc_end, 0x400006, And(RBX == b, RIP == pc + 6))
---------------------------------------------
Trace:
Entry(myfunc, 0x400000, And(RAX == a, RBX == b, RIP == pc))
0x400000/3: ADD RBX,RAX
0x400003/3: SUB RBX,RAX
Exit(myfunc_end, 0x400006, And(RBX == b, RIP == pc + 6))
Countermodel:
{b: 0, pc: 0, RBX: 0, RIP: 0}
---------------------------------------------
❌❌❌❌ 1 verification conditions failed. ❌❌❌❌