Bvsmod results inconsistent with IDIV instruction

[smpcpp]

https://github.com/JonathanSalwan/Triton/blob/2ea88a6ba957afdd987a5bb4e80ee24ced60fb9d/src/libtriton/ast/ast.cpp#L1561 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 52aae9e8edabe7bb97118eb185541bc1f51cb2d4 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 a1ea2735dabf1fa74f2bee4b44d21a88dd52d09c 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())