Z3 not working inside a DynamoRio client.

[0ca]

Hi,

I was trying to use Z3 inside a DR client in Windows. Some functions are working but it is crashing solving an expression. It is not a Z3 problem because the same code is working properly in a normal console project:

#include <iostream>
#include <z3++.h>

void testz3()
{
    std::stringstream   formula;
    z3::context ctx;
    z3::solver  solver(ctx);

    formula << "(declare-const x Int)";
    formula << "(assert (= x 4))";

    Z3_ast ast = Z3_parse_smtlib2_string(ctx, formula.str().c_str(), 0, 0, 0, 0, 0, 0);
    z3::expr eq(ctx, ast);
    solver.add(eq);
    printf("Before check\n");
    if (solver.check() == z3::sat)
        printf("SAT!\n");
    else
        printf("UNSAT!\n");
}

int main(int ac, const char **av)
{
    testz3();
    return 0;
}

The following code of the DR client is crashing in the instruction solver.check:

#include <dr_api.h>
#include <sstream>
#include <z3++.h>

void testz3()
{
    std::stringstream   formula;
    z3::context ctx;
    z3::solver  solver(ctx);

    formula << "(declare-const x Int)";
    formula << "(assert (= x 4))";

    Z3_ast ast = Z3_parse_smtlib2_string(ctx, formula.str().c_str(), 0, 0, 0, 0, 0, 0);
    z3::expr eq(ctx, ast);
    solver.add(eq);
    dr_printf("Before check\n");
    if (solver.check() == z3::sat)
        dr_printf("SAT!\n");
    else
        dr_printf("UNSAT!\n");
}

DR_EXPORT void dr_client_main(client_id_t id, int argc, const char *argv[])
{
    dr_enable_console_printing();
    testz3();
}

I guess that DynamoRio is interfering in the execution of the Z3 project, but I don't know where.

I attach the DR client log (loglevel 5):
Crackme.exe.0.2056.html.zip

And I attach the two projects with the Z3 console app and the DR client using Z3.
Z3_projects.zip

Could anyone test it?

[derekbruening]

What happens under DR debug build?

What is the callstack of the crash? See https://github.com/DynamoRIO/dynamorio/wiki/Debugging

[0ca]

I executed it with a DR debug build.

In the log I attached is possible to get the callstack but without symbols:

print_symbolic_address(0x0024b727)='[KERNELBASE.dll]'
print_symbolic_address(0x73d69339)='[MSVCR120.dll]'
print_symbolic_address(0x00a40983)='[libz3.dll]'
print_symbolic_address(0x00a41800)='[libz3.dll]'
print_symbolic_address(0x00a40a55)='[libz3.dll]'
print_symbolic_address(0x00a41534)='[libz3.dll]'
print_symbolic_address(0x00cf374b)='[libz3.dll]'
print_symbolic_address(0x00cf3772)='[libz3.dll]'
print_symbolic_address(0x00ceeffc)='[libz3.dll]'
print_symbolic_address(0x00cf3772)='[libz3.dll]'
print_symbolic_address(0x00ceeffc)='[libz3.dll]'
print_symbolic_address(0x00cf51c8)='[libz3.dll]'
print_symbolic_address(0x00cf539b)='[libz3.dll]'
print_symbolic_address(0x00c5783d)='[libz3.dll]'
print_symbolic_address(0x00c580fb)='[libz3.dll]'
print_symbolic_address(0x00c587d6)='[libz3.dll]'
print_symbolic_address(0x0085b8b6)='[libz3.dll]'
print_symbolic_address(0x0085bae0)='[libz3.dll]'
print_symbolic_address(0x10021806)='[RioTool.dll]'
print_symbolic_address(0x1002148e)='[RioTool.dll]'
print_symbolic_address(0x10010d9f)='[RioTool.dll]'
print_symbolic_address(0x100032f4)='[RioTool.dll]'
print_symbolic_address(0x60426fc8)='[dynamorio.dll]'
print_symbolic_address(0x60282b97)='[dynamorio.dll]'
print_symbolic_address(0x604d09f1)='[dynamorio.dll]'
print_symbolic_address(0x60569a28)='[dynamorio.dll]'

The kenelbase address is in the RaiseException function, the function in MSVCR120.dll is a wrapper to RaiseException, and the next one is libz3 raising an exception.

So the problem is Z3 is raising an exception when it is inside the DR private loader. But why?

It would be cool to be possible to disable the virtual heap, the private loader and all the different transparency artifacts to narrow down the issue. But as you told me here it doesn't seem to be an easy task, I would need to modify the options.c I don't feel very confident modifying that code.

I would appreciate any help to identify or solve the problem. Thank you!

[derekbruening]

Use windbg to attach and get the callstack at the crash point (where the msgbox is raised), getting symbols as shown on the wiki link pasted above.

With a private lib silently failing, debugging involves stepping through with windbg the private z3 code loaded by DR and comparing its execution to z3 code run natively in windbg. Here there is an actual crash, though, and that should be analyzed directly.

[netanel01]

Hi,
I used the exact same code that @0ca provided, I found out that the exception code is e06d7363 which is correspond to c++ exception code.
I run the Z3Test under windbg and it hit 2 times c++ exception here is the call stack:

00 0093ecac 1078e53e KERNELBASE!RaiseException+0x62
01 0093ecec 105b13f8 libz3!_CxxThrowException+0x5b [f:\dd\vctools\crt\crtw32\eh\throw.cpp @ 152]
02 0093ed04 105af715 libz3!is_non_qfbv_predicate::operator()+0xb8 [c:\...\z3\src\tactic\probe.cpp @ 295]
03 0093edd4 105b0bb4 libz3!for_each_expr_core<is_non_qfbv_predicate,ast_fast_mark<1>,0,0>+0x2b5 [c:\...\z3\src\ast\for_each_expr.h @ 77]
04 0093ee60 105b15b2 libz3!test<is_non_qfbv_predicate>+0x94 [c:\...\z3\src\tactic\goal.h @ 175]
05 0093ee84 105b99bb libz3!is_qfbv_probe::operator()+0x22 [c:\...\z3\src\tactic\probe.cpp @ 315]
06 0093eea4 105b8d63 libz3!cond_tactical::operator()+0x1b [c:\...\z3\src\tactic\tactical.cpp @ 1245]
07 0093f0b4 105ae76c libz3!and_then_tactical::operator()+0x293 [c:\...\z3\src\tactic\tactical.cpp @ 140]
08 0093f130 105ae379 libz3!exec+0x6c [c:\...\z3\src\tactic\tactic.cpp @ 168]
09 0093f1f4 10511915 libz3!check_sat+0x159 [c:\...\z3\src\tactic\tactic.cpp @ 190]
0a 0093f2a8 105134e6 libz3!tactic2solver::check_sat_core+0x275 [c:\...\z3\src\solver\tactic2solver.cpp @ 151]
0b 0093f2dc 10514616 libz3!solver_na2as::check_sat+0x66 [c:\...\z3\src\solver\solver_na2as.cpp @ 67]
0c 0093f324 10053d79 libz3!combined_solver::check_sat+0x206 [c:\...\z3\src\solver\combined_solver.cpp @ 258]
0d 0093f384 1005224f libz3!_solver_check+0x109 [c:\...\z3\src\api\api_solver.cpp @ 302]
0e 0093f3c4 003e6b8f libz3!Z3_solver_check+0x7f [c:\...\z3\src\api\api_solver.cpp @ 311]
0f 0093f4b8 003e9427 Z3Test!z3::solver::check+0x3f [c:\...\z3\src\api\c++\z3++.h @ 1877]
10 0093f6c0 003e9a02 Z3Test!testz3+0x1a7 [c:\...\z3test\z3test.cpp @ 18]
11 0093f794 003ea459 Z3Test!main+0x32 [c:\...\z3test\z3test.cpp @ 29]
12 0093f7e4 003ea64d Z3Test!__tmainCRTStartup+0x199 [f:\dd\vctools\crt\crtw32\dllstuff\crtexe.c @ 626]
13 0093f7ec 758a8484 Z3Test!mainCRTStartup+0xd [f:\dd\vctools\crt\crtw32\dllstuff\crtexe.c @ 466]
14 0093f800 7740305a KERNEL32!BaseThreadInitThunk+0x24
15 0093f848 7740302a ntdll!__RtlUserThreadStart+0x2f
16 0093f858 00000000 ntdll!_RtlUserThreadStart+0x1b

the addresses are aligned when running the client under drrun here is the call stack from the assert:

c:\...\DynamoRIO-Windows-7.0.0-RC1\bin32\drrun.exe -c RioTool.dll -- calc
Before check
Exception caught: e06d7363
<Application C:\Windows\SysWOW64\calc.exe (32256).  internal crash at PC 0x0c27ddc2.  Program aborted.
0xe06d7363 0x00000001 0x0c27ddc2 0x0c27ddc2 0x19930520 0x001ceebc
Base: 0x70be0000
Registers: eax=0x001cedd8 ebx=0x0420bb40 ecx=0x00000003 edx=0x00000000
        esi=0x108c7f4c edi=0x001ceebc esp=0x001cedd8 ebp=
version 7.0.0, build 1
-no_dynamic_options -client_lib 'C:\...\RioTool VS2013\Win32\dyn\RioTool.dll;0;' -code_api -probe_api -stack_size 56K -max_elide_jmp 0 -max_elide_call 0 -no_inline_ignored_syscalls -native_exec_default_list '' -no_native_exec_managed_code -no_indcall2direct -no_aslr_dr -pad_jmps_mark_no_trace
0x001cee30 0x1078e53e 
0x001cee70 0x105e0af5 _CxxThrowException(x,x)
0x001cef18 0x105deb3d 
0x001cef58 0x1058dff5 
0x001cefa4 0x1058e144 
0x001cf000 0x105b998d
0x001cf020 0x105b8c9e
0x001cf230 0x105ae76c exec(...)
0x001cf2ac 0x105ae379 check_sat(...)
0x001cf370 0x10511915
0x001cf424 0x105134e6
0x001cf458 0x10514616
0x001cf4a0 0x10053d79 _solver_check
0x001cf500 0x1005224f
0x001cf540 0x20002050>

I didn't understand one thing why when i run Z3Test with the following command it won't crash:
c:\...\DynamoRIO-Windows-7.0.0-RC1\bin32\drrun.exe -t drcov -- Z3Test.exe
But when running the client directly it crash as mentioned above:
c:\...\DynamoRIO-Windows-7.0.0-RC1\bin32\drrun.exe -c RioTool.dll -- calc
So i dig up the code and I understand that when intercept_exception is called it will lead to check_internal_exception which will "raise" the exception and won't let it try continue execution because it is "is_dynamo_address".
I don't know the reason for that maybe someone can shed some light?
Moreover, I got the feeling that it has something to do with: #1717 and that it wasn't fixed for win32

[derekbruening]

Trying to continue on an exception inside DR itself is not done because there are no SEH handlers (deliberately): SEH relies on user-mode code and DR wants to run as little of such code as possible, for transparency to avoid interacting with app state. Any handling it needs to do for its own try..except mechanisms is done directly via custom machinery.

To continue for a client exception for #1717 requires ensuring the state used by the SEH code is all properly separated from the app and ensuring an unhandled exception gets back to DR.