Error happen when implement learch on klee-2.3

[for-just-we]

Hi, author. I recently try to implement learch on klee-2.3 with LLVM 11.0.0. The python interpreter I use is a env in anaconda3. When I migrate learch code to klee-2.3 and run on coreutils samples. There are something strange happened.

When I use other strategies(including subpath-length-1 to 8), klee runs without any exception. But if I run ml strategy. Klee report error runtime/POSIX/fd.c:1007: external modified read-only object. It seems that klee could not process system call with machine learning strategy. I debug, and found that the calculating process for reward of a state operates normaly. So I have no idea how to fix, do you have any idea

[LostBenjamin]

Hi,

It seems to me that this error is because klee cannot model some object symbolically. This error happens for Learch likely because Learch visits some states that other strategies do not visit. You can try to confirm this by checking from which source line in the input program the error originates and if other strategies cover this line.

Let me know if this helps.

Best, Jingxuan

[for-just-we]

Hi,

It seems to me that this error is because klee cannot model some object symbolically. This error happens for Learch likely because Learch visits some states that other strategies do not visit. You can try to confirm this by checking from which source line in the input program the error originates and if other strategies cover this line.

Let me know if this helps.

Best, Jingxuan

I try to find problems by using the method of elimination. And I found that the problem seem to relate to Py_Initialize. I first change the code of MLSearcher into a simple RandomStateSearcher code. Then add python interpreter API to MLSearcher one by one. And after I add Py_Initialize. The error happened.

This error happen only when symbolic executing syscall instruction. If there are no system call in testing samples(such as samples for klee official), there are no need to use posix environment and thus no error happen.

It seems to me that the calling for python interpreter is confilict with posix runtime, I try to use libtorch instead of call python interpreter. But there are always compile error, I already build LLVM with RTTI and ExceptionHandler on.

By the way, even I call Py_finalize in MLSearcher constructor after Py_initialize, there are still error happen.

[LostBenjamin]

Can you send me the complete log produced by klee?

[for-just-we]

Can you send me the complete log produced by klee?

The example I use is -sym-arg Usage example, the output in command line is

KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: syscall(4, 94222717110000, 94222714618160) at runtime/POSIX/fd.c:544 12
KLEE: ERROR: runtime/POSIX/fd.c:544: external modified read-only object

And in klee-last dir, there is an extra file named test000001.external.err, the content is:

Error: external modified read-only object

File: runtime/POSIX/fd.c

Line: 544

assembly.ll line: 4156

State: 1

Stack: 
    #000004156 in __fd_stat (path=94222717110000, buf=94222714618160) at runtime/POSIX/fd.c:544
    #100002017 in stat64 (path=94222717110000, buf=94222714618160) at runtime/POSIX/fd_64.c:95
    #200001222 in klee_init_fds (n_files=0, file_length=0, stdin_length=10, sym_stdout_flag=0, save_all_writes_flag=0, max_failures=0) at runtime/POSIX/fd_init.c:119
    #300000788 in klee_init_env (argcPtr=94222717110472, argvPtr=94222717110496) at runtime/POSIX/klee_init_env.c:234
    #400001059 in main (argcPtr=3, argvPtr=94222716478144, envp=94222716478176) at runtime/POSIX/klee_init_env.c:244

The content of info file

klee -posix-runtime --feature-extract --search=ml --model-type=feedforward --model-path=xxxx/feedforward_3.pt --script-path=xxx/learchExp --py-path=xxx/anaconda3/envs/Learch password.bc -sym-stdin 10

PID: 4654

Using monotonic steady clock with 1/1000000000s resolution

Started: 2022-10-25 18:57:15

BEGIN searcher description

<MLSearcher></MLSearcher>

END searcher description

Finished: 2022-10-25 18:57:15

Elapsed: 00:00:00

LEE: done: explored paths = 1

KLEE: done: total queries = 0

KLEE: done: valid queries = 0

KLEE: done: invalid queries = 0

KLEE: done: query cex = 0

KLEE: done: total instructions = 2087

KLEE: done: completed paths = 0

KLEE: done: partially completed paths = 1

KLEE: done: generated tests = 1

[LostBenjamin]

From the log, it seems that klee with the Learch strategy cannot symbolically model some object on the first and the only path it explores. Not sure why it works for other strategies though. As I already suggested, you can check from which source line in the input program the error originates and if other strategies cover this line.

[for-just-we]

From the log, it seems that klee with the Learch strategy cannot symbolically model some object on the first and the only path it explores. Not sure why it works for other strategies though. As I already suggested, you can check from which source line in the input program the error originates and if other strategies cover this line.

Well, from my experiment, I presume that the error comes from system call like printf, because if I remove this line. There are no error. And if I remove Py_initialize in klee MLSearcher code, klee also run without error. So I presume current posix version to a extent comflict with python interpreter. But I don't know why. So I try to implement with libtorch instead of call python interpreter.