Peter Goodman

This is probably the cause: https://github.com/lifting-bits/remill/blob/269e61a601a399229d8d8deb8fc00cb4def69038/lib/Arch/X86/Semantics/BINARY.cpp#L246-L256

We should really have a one-argument form of `__remill_undefined_8` that takes in a concrete value.

It looks like with the P4 core, IMUL started preserving some of the flags: https://www.sandpile.org/x86/flags.htm

@m4xw can you provide an example binary that manifests the issue described here: https://github.com/lifting-bits/remill/blob/bbb3fa58017f4aae628619b4153d2b7ed612d94d/lib/BC/PcodeCFG.cpp#L125 Also, it would help if you had a screenshot from ghidra showing the relevant assembly +...

Here's where we implement it for aarch64: https://github.com/lifting-bits/remill/blob/master/lib/Arch/AArch64/Semantics/BINARY.cpp#L140-L151 For x86, I think we explicitly detect signed underflow, though it adds a bunch of complexity to the semantics: https://github.com/lifting-bits/remill/blob/master/lib/Arch/X86/Semantics/BINARY.cpp#L488-L489 Also the...

Ah interesting! @regehr had previously done a bit of translation validation with remill (through [anvill](https://github.com/lifting-bits/anvill)) and alive2 with [opt-fuzz](https://github.com/regehr/opt-fuzz). I believe they eventually switched to their own custom AArch64 binary...

@Toizi This is excellent!

The code checks `hasNUsesOrMore(1)` on calls and loads. This surprises me; why are those conditional on at least one use at all? Is there some logic somewhere that is able...

Is there a way to encode the partial order relation as Z3 expressions? That is, could `load`s be somehow turned into uninterpreted function calls that return a tuple, where one...

Define a new LLVM function with prototype roughly ``` ptr __ptr(ptr, ptr) ``` Transform loads as follows: ```llvm %x = load %y ``` Into: ```llvm %MEMORY = alloca ptr ......