Program "dies" after calling ctx.getModel

[Z4ee]

Hello, I encountered a problem while processing sample3.vmp.trace in attack_vmp.py. Attack_vmp "dies" after calling the ctx.getModel function in detecting_vjmp. There is no error information, and I cannot determine what exactly the problem is.

Here is the code that causes the problem:

def detecting_vjmp(execid, ctx, inst, vbraddr, vbrflag):
    ...
    if inst.isSymbolized() and inst.getType() == OPCODE.X86.POPFQ:
        cf = ctx.getRegisterAst(ctx.registers.cf)
        if len(ast.search(cf, AST_NODE.VARIABLE)) == 2:
            model, status, _ = ctx.getModel(cf != cf.evaluate(), status=True)
            ...

After this call, the program simply "dies" without outputting any errors. I added debug messages before and after the call, and they point to this section of code as the problematic area. The problem likely occurs inside the ctx.getModel call.

Can you help me understand why this is happening and how to solve this problem? I would appreciate any help!

Thank you!

[JonathanSalwan]

I've never got this issue. If an error happens during the getModel processing, an exception is raised and you should see it. I think at this step, the best way to understand what is going on is to attach a debugger.

[JonathanSalwan]

Btw, when you say "die", what the program does? it exits or it's more like a infinity loop? Because, if it's looks like an infinity loop, it could probably means that the getModel is searching for a model.

[Z4ee]

Yes, under "die" I mean exits

> attack_vmp.py --trace1 sample3.vmp.trace --symsize 1
- [+] Replaying the VMP trace
- [+] Symbolize inputs
- > c:\users\icant\desktop\tr\old\attack_vmp.py(69)detecting_vjmp()
-      68                 ipdb.set_trace()
- ---> 69                 model, status, _ = ctx.getModel(cf != cf.evaluate(), status=True)
-      70                 if status == SOLVER_STATE.SAT:

- ipdb> s

> ...

after ipdb->step, attack_vmp.py exits

(I'm not very good at debugging python code)

[Z4ee]

I think the issue might be related to using incorrect versions of the dependencies. Could you please let me know the versions of the following libraries that you use or recommend for Triton:

1. LLVM
2. Capstone
3. Python
4. Z3

Currently, I have the following versions of the libraries installed:

1. LLVM -> 15
2. Capstone -> 4.0.2
3. Python -> 3.10
4. Z3 -> 4.12.1

By knowing the recommended versions, I will be able to configure my development environment accordingly and possibly resolve the issues I'm experiencing. Thank you for your time and assistance.

[JonathanSalwan]

1. LLVM -> 15
2. Capstone -> 4.0.2
3. Python -> 3.10
4. Z3 -> 4.12.1

They are all valid. If you want, you can upgrade to Capstone 5.x but it will not fix your issue.

However, as the issue is related to getModel, maybe using the Bitwuzla solver might help you? Once Bitwuzla installed, you have to recompile Triton using the cmake variable: -DBITWUZLA_INTERFACE=ON. Then, in your python script, you can switch from a solver to another like this:

ctx = TritonContext(...)

ctx.setSolver(SOLVER.BITWUZLA) # will use Bitwuzla as a solver
ctx.setSolver(SOLVER.Z3) # will use Z3 as a solver

[Z4ee]

Hi, I wanted to let you know that I managed to resolve the issue I previously reported with processing sample3.vmp.trace in attack_vmp.py. It turned out that there might have been conflicts between some libraries on my system.

After performing a clean installation of Windows, the problem disappeared. It seems that the issue was related to my specific setup and not with Triton itself. I apologize for any confusion this may have caused.

Thank you for your assistance and suggestions earlier. Keep up the great work on Triton!

Best regards.