search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Z3 not working inside a DynamoRio client #458

Closed 0ca closed 8 years ago

0ca commented 8 years ago

Z3 is not working properly inside a DynamoRio client as I reported here: https://github.com/DynamoRIO/dynamorio/issues/1881

It seem that some of the Z3 functionality solving expressions are not working inside DynamoRio. It is not a Z3 bug, but maybe some Z3 developers can easily figure out where it is the problem.

Any help is appreciated ;)

wintersteiger commented 8 years ago

I have never heard of DynamoRio before, but it looks like it makes some sort of distinction between "natived" and "managed" code, and the options in the error message sound vaguely like "native" code support is disabled?

0ca commented 8 years ago

It is not exactly that. As it says here: http://dynamorio.org/docs/transparency.html

DynamoRIO must avoid interfering with the semantics of a program while it executes. Shifting execution from the original application code into a cache that occupies the application's own address space provides flexibility but complicates transparency. To achieve transparency, DynamoRIO cannot make any assumptions about a program's stack usage, heap usage, or any of its dependencies on the instruction set architecture or operating system. DynamoRIO's transparency restrictions necessarily apply to a client aswell. Contents:

So DynamoRio has its own DLL loader and its own heap. And I guess that in some point Z3 is doing something DynamoRio doesn't expect.

It is interesting the function Z3_parse_smtlib2_string is executed correctly. It is crashing in the solver.check function.

Do you have any idea about what kinds of "not tipical" actions is doing Z3 when it's solving a formula? Maybe highly use of the stack, use a custom heap manager or other atypical thing?

Thank you very much for your help. Z3+DynamoRio could be very useful for the people interested in Concolic Execution ;)

NikolajBjorner commented 8 years ago

Definitely relevant for fuzzing. Z3 has several custom heaps (small object allocators and also paged memory).

wintersteiger commented 8 years ago

+1 to what @NikolajBjorner said, those memory managers may definitely confuse some tools. Another "atypical" thing is that libz3.dll uses thread-local storage (see memory_manager.cpp), but I would have expected a different error message if that was the issue. (But then, Windows XP doesn't provide one either and just crashes...)

delcypher commented 8 years ago

@0ca it might be related to #436. In a x86_64 build of Z3 a method is used for allocating clauses that can break if the addresses returned by malloc() are not in a certain range. You could try running a 32-bit build of Z3 to see if the problem you have been observing still occurs.

0ca commented 8 years ago

Thanks everyone!

@delcypher the tests were done in Windows 7 32 bits.

NikolajBjorner commented 8 years ago

That clause allocation is run in the native sat solver so given the test program it is somewhat less likely to be on the path.

delcypher commented 8 years ago

@0ca

@delcypher the tests were done in Windows 7 32 bits.

Okay #436 is unrelated then.

NikolajBjorner commented 8 years ago

Should we put Rio to rest or is it still dynamic?