Bvsmod results inconsistent with IDIV instruction

[smpcpp]

Triton/src/libtriton/ast/ast.cpp

Line 1561 in 2ea88a6

this->eval = (static_cast<triton::uint512>((((op1Signed % op2Signed) + op2Signed) % op2Signed)) & this->getBitvectorMask());

The BvsmodNode is used to produce the semantics for an x86 IDIV instruction but it doesn't always give the same results.
This was changed from the basic modulus in 52aae9e but I couldn't see why.

Example:

BA FFFFFFFF | mov edx,FFFFFFFF |  
B8 59E4ADBD | mov eax,BDADE459 |  
B9 E8030000 | mov ecx,3E8 |  
F7F9 | idiv ecx |  

Emulating in triton produces a remainder EDX = 0x2c9
Running locally produces EDX = 0xfffffee1

Changing back to

this->eval = (static_cast<triton::uint512>((op1Signed % op2Signed)) & this->getBitvectorMask());

produces the correct remainder.

[smpcpp]

Maybe the solution is replacing the bvsmod node with bvsrem in idiv_s semantics
I see now you changed from bvsrem to bvsmod in a1ea273 but there wasn't a referenced issue.

[JonathanSalwan]

Sorry for the delay, can you provide a unit test of this behaviour ?

[GhostInCell]

Encountered with same issue. Here is a short example:

import z3 #4.13.0.0
from triton import * #1.0.0rc3

ctx = TritonContext(ARCH.X86_64)
astCtx = ctx.getAstContext()

a = astCtx.bvsmod(astCtx.bv(96, 8), astCtx.bv(-77, 8))
b = z3.simplify(z3.IntVal(96) % z3.IntVal(-77))

#assert(198 == 19)
assert(a.evaluate() == b.as_long())