[phix33]

Recover imported names and terminal calls in PPC32 PIC code. With GCC and GNU PowerPC binutils:

mkdir -p tmp/ppc32-pic
printf '%s\n' 'extern void __stack_chk_fail(void), extra(void);' \
  'void refs(void) { __stack_chk_fail(); }' \
  'int check(void) { extra(); return 7; }' > tmp/ppc32-pic/calls.c
powerpc-linux-gnu-gcc -O1 -fPIC -msecure-plt -c tmp/ppc32-pic/calls.c -o tmp/ppc32-pic/calls.o
powerpc-linux-gnu-gcc -shared -msecure-plt tmp/ppc32-pic/calls.o -o tmp/ppc32-pic/calls.so
kuna decompile tmp/ppc32-pic/calls.so refs --mode fast

void refs(void)
{
  sub_590();
  return;
}

Adding --option ppc32picimports on names __stack_chk_fail and removes the final return. With abi, check also changes from sub_5c0(); return 7; to extra(); return 7;.

Implementation

• on proves terminal calls in their caller context; returning imports invalidate later slot reads. abi enables broader stub naming under documented compiler and ABI assumptions, including that application code leaves GOT slots intact.
• Keep recovery default-off. The CLI applies the mode before loading; changing to or from abi in the console requires reload. Recovered xrefs include instruction text.
• Decode unwind bounds in the ELF byte order and retain stubs covered by shared unwind records using indexed overlap checks.

Tests

Both byte orders cover counted branches, slot overwrites, callbacks, xrefs and unaligned stores; the overlapping-store regression fails before the fix. A large synthetic unwind image checks scaling. Focused tests, parity, spec and catalog checks pass. The full workspace retains nine pre-existing failures.

[mahaloz]

[AUTOMATED] The proof is sound in everything we built (4,700+ recovered names checked against linker relocations, 0 wrong), but it never fires on a normally linked image. Repro, the body's example linked through the compiler driver:

powerpc-linux-gnu-gcc -shared -msecure-plt -Wl,--strip-all tmp/ppc32-pic/check.o -o tmp/ppc32-pic/check-gcc.so
kuna decompile tmp/ppc32-pic/check-gcc.so check --mode fast --option ppc32picimports on   # still sub_620();

crtbeginS.o calls through CTR, and one uncertified caller withdraws every contract in the image. The same happens when any function has add/cmpw/crxor before its return, calls a static helper, or passes a stack address to an import. Result: 0 names on all 10 PPC32 sysroot libraries (libstdc++ has 2,951 r30 stubs), on gcc-linked .so/PIE builds, and on Lua.

Tracking the exact registers each unhandled instruction writes doesn't move any of those off 0. Scoping a failure to the stubs its caller reaches would, but needs an argument for why an uncertified transfer cannot enter other stubs. Could you make recovery reach compiled images (e.g. scoped failure under stated ABI assumptions, local-call summaries, calls through GOT-loaded import pointers) before this lands?

I pushed two commits: a per-image cache of the proof plus a linear lazy-resolver scan (option-on load of an 8,201-import image 2.9x -> 1.2x of option-off; a crafted 16,000-resolver image 47 s -> 0.06 s), the option-off GNU assertion restored, and docs stating the current reach.

[mahaloz]

[AUTOMATED] I extended the proof (pushed adc6411f9) so it names imports in images linked through the compiler driver, and merged main. It is still sound against the linker. Repro: the body's example linked with the start files, using GCC 13.3 and binutils 2.42.

printf '%s\n' 'extern void __stack_chk_fail(void), other(void), another(void), extra(void);' \
  'void refs(void) { other(); another(); extra(); __stack_chk_fail(); }' \
  'int check(void) { extra(); return 7; }' |
  powerpc-linux-gnu-gcc -O1 -fPIC -msecure-plt -fno-asynchronous-unwind-tables -x c -c - -o check.o
powerpc-linux-gnu-gcc -shared -msecure-plt -Wl,--secure-plt check.o -o check-gcc.so
kuna decompile check-gcc.so check --mode fast --option ppc32picimports on

Before this push the call printed as sub_620();. It now prints as extra(); return 7;. A 5 KB build of the same image is committed as decompiler/crates/kuna-cli/tests/fixtures/ppc32-pic-driver.so, with its provenance. tests/stages/kuna-ppc32picimports-driver.xml checks all six stubs with the option off and on.

What changed

• Scoped failure. A caller the proof cannot certify now withdraws only the stubs its own code reaches, instead of every name in the image. This holds because the linker writes a PIC stub's address only into branch fields. No relocation gives that address to data or to address arithmetic. So a return address, function pointer or jump-table target never holds a stub address, and an uncertified jump cannot enter some other stub.
  • Every case where that could fail stays unnamed: a stub that a data word, relocation, symbol, the entry, a landing pad, an interior branch or a computed-and-stored address points into.
• Per-function proof. Each function entry is walked once with symbolic registers. The walk tracks each nonvolatile register's stack save word, the LR spill and the back chain. It also reads loads from the GOT, the code and read-only data.
• Calls.
  • Calls to imports and calls through registers keep r1, r2 and r13-r31, as the SysV calling convention guarantees.
  • A call to local code keeps only what that function's own proven summary says it restores. Summaries start from the strongest claim and weaken to a fixed point, which stays sound for recursion.
  • Straight-line helpers such as _savegpr_N/_restgpr_N run in place.
• Jump tables and landing pads.
  • Jump tables are followed; a cmplwi the branch passed, or the index mask, bounds the table.
  • LSDA landing pads are entered from the calls in their call-site range.
• Exact edge cases. bcl 20,31 reads the PC; it is not a call. Flow stops after:
  • ABI no-return imports (named by their own proven slot);
  • unconditional traps;
  • the exit syscalls;
  • a call that is the last instruction of its FDE range or sized symbol.
• Spec. docs/spec/01-program-prep.md now spells out the soundness argument: the seven assumptions it rests on, and the checks behind each one.

Results (raw proof output, before demangling)

• Lua, C and C++ builds: 58 builds as .so and PIE, at O0, O1, O2, O3 and Os, with fPIC and fpic, with and without unwind tables, each stripped and unstripped. Of the stubs the linker's --emit-relocs call relocations name, 122,440 of 122,528 are named, 0 wrong.
• 10 PPC32 sysroot libraries: 3,906 of 3,931 r30 stubs are named, with 0 disagreements against an independent r30 decoder.
  • libstdc++: 2,942 of 2,951
  • libasan: 349 of 352
  • libubsan: 230 of 231
  • libgomp: 218 of 219
  • libc: 12 of 19 (its remaining callers go through setcontext/__sigsetjmp-style assembly).
  • libasan and libubsan keep the linker's stub labels: 210 match, 0 wrong.
• Hand-written adversarial assembly: cases that change r30 between calls or on one path stay unnamed. Cases that move r30 on purpose are named after the slot the call actually loads at runtime, not after the linker's label.

Default. It stays off. With the loader gate forced on, the datatests (675/675) and the stage tests still match their baselines exactly. But with it on, listing a PPC32 PIC image's functions takes 1.1x to 1.7x as long (Lua .so 1.17x, libstdc++ 1.33x, libc 1.49x). A single-function decompile of a large library takes up to about 3x as long (libc perror: 0.16 s to 0.54 s). Both are well over the 5% budget. Other formats, and the off path, are unchanged.

[phix33]

Oops, sorry I was working on this. I'll rebase and see if any of my updates help - things slow here as many other tasks running!! 😀

[mahaloz]

[AUTOMATED] @phix33, before you rebase: we pushed fa8de6f8a to your branch. It is a merge of current main, plus fixes for 7 hand-written-assembly shapes that made the proof name a stub after a slot its runtime caller doesn't load:

• a return past the return address;
• a tail branch with a stale LR;
• stwcx./stwbrx counted as saves;
• saves below SP and the 4(r1) word;
• a jump-table entry that points at a stub;
• a returning call at the end of its scope;
• a return address stored to memory.

It also fixes a crafted 6 KB .so that made the option-on load use 2.1 GB. Repros are in tests/ppc32_imports.rs (ppc32_pic_paths_the_walk_cannot_follow_withhold_the_stub).

Results after the fixes:

• 58 gcc-linked configs still name 122,440 stubs, with 0 wrong against --emit-relocs.
• The sysroot libraries name 3,903 stubs.
• With the option off, output is byte-identical to main and costs nothing.

One case is still open, and the spec now states it as part of assumption (5). A callee stores a return address it received in r0, and another function later jumps there with its own r30. In the repro below, kuna decompile stash-one.so c --option ppc32picimports on prints ccc();, but h runs that call with r30-4, which selects bbb's slot.

The cheap rule would be to give up whenever a return address sits in a register at a local call. It costs 38% of libstdc++'s names and 88% of Lua -O1's. Could the walk instead give volatile registers symbolic entry values, so a callee that stores an incoming register is seen as leaking whatever its caller passed?

powerpc-linux-gnu-gcc -shared -msecure-plt -Wl,--secure-plt stash-one.s -o stash-one.so

stash-one.s

	.macro PRO l
	stwu 1,-32(1)
	mflr 0
	bcl 20,31,\l
\l:	stw 30,24(1)
	mflr 30
	addis 30,30,.LCTOC1-\l@ha
	stw 0,36(1)
	addi 30,30,.LCTOC1-\l@l
	.endm
	.macro EPI
	lwz 0,36(1)
	lwz 30,24(1)
	addi 1,1,32
	mtlr 0
	blr
	.endm
	.section ".got2","aw"
.LCTOC1 = .+32768
	.long 0
	.section ".bss"
	.align 2
saved_ra: .long 0
	.text
	.globl refs, c, h
	.type refs,@function
	.type c,@function
	.type h,@function
refs:	PRO .L0
	bl aaa+32768@plt
	bl bbb+32768@plt
	bl ddd+32768@plt
	EPI
c:	PRO .L1
	bl a              # a's return address (c+0x24) reaches stash in r0
	bl ccc+32768@plt  # named ccc; h re-enters here with r30-4
	EPI
a:	PRO .L2
	bl stash
	EPI
stash:	mflr 11           # store the caller's r0 for h
	bcl 20,31,.L3
.L3:	mflr 12
	mtlr 11
	addis 12,12,saved_ra-.L3@ha
	stw 0,saved_ra-.L3@l(12)
	cmpwi 3,0
	beq 1f
1:	blr
h:	PRO .L4
	bcl 20,31,.L5
.L5:	mflr 12
	addis 12,12,saved_ra-.L5@ha
	lwz 9,saved_ra-.L5@l(12)
	addi 30,30,-4
	mtctr 9
	bctr