[klee-dev] How to handle 32bit bc file with 64bit klee

[Marek Chalupa]

Hi,

We had the same issue in our tool Symbiotic (
https://github.com/staticafi/symbiotic/) that can use KLEE internally.
This is what we had to do to make it somehow work (apart from compiling the
program with -m32):

1) compile 32-bit libraries (
https://github.com/staticafi/symbiotic/blob/master/scripts/build-klee.sh#L80)
and properly set-up the paths using KLEE_RUNTIME_LIBRARY_PATH
2) change the memory management of KLEE to allocate memory on lower
addresses (since KLEE uses pointers to memory allocated by the host system,
the address may be a number that does not fit into a 32-bit variable). I
think you can use the deterministic allocation feature in upstream KLEE to
solve this problem.

Cheers,
Marek

On Tue, Dec 15, 2020 at 3:19 PM JingXiaoni <jingxiaoni at icloud.com> wrote:

>
> Hi all,
> l have some problems
> on using klee,need your help .Thanks in advance
> My test target is 32bit app.Now I compile llvm and klee in x86_64, then
> add -m32 option on compile target object.
> For example:
> for bc file
> clang++ -m32 sample.cpp -c -o sample.bc
> for app
> clang++ -m32 sample.cpp -o sample -lkleeRuntest
> Now I have 2 issues
> 1. bc file compile is success.But when I use klee to generate test
> cases.There is a error info"LLVM ERROR:64-bit code requested on a subtarget
> that doesn't support it". I would like to make klee can handle 32bit
> bc.Then add option in CMakeList.txt with
> add_complie_option(--target=i386-pc-linux-gun).remake makefile and
> make,make has a warning that "cc1 plus:warning:command line option
> '-ftarget=i386-pc-linux-gun'is valid for Java but not for c++".Add Klee
> can’t work for 32 bit bc,too.
> So my question is how to add compile options in cmake or make file to make
> 64bit Klee can support 32bit bc file?
> 2.When I compile 32 bit app with Klee lib(libKleeRuntest),It shows can’t
> find this lib but when I compile 64bit app,there is no problem.Does it mean
> I need to compile a 32bit Klee to use it or is there some other way to set
> it up and it will work?
> Thanks for your help.
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed