Re: [klee-dev] fork() : creating child processes in KLEE's execution
Hi Prof. Cristian, Thanks for the clarification. Best Regards, Pansilu On Wed, Mar 9, 2022 at 9:53 PM Cristian Cadar wrote: > Hi, > > KLEE does not use the system call fork() to fork states. See > Executor::fork() in the code. > > Best, > Cristian > > On 23/02/2022 18:40, Pansilu Pitigalaarachchi wrote: > > Hi, > > > > I would like to check the possible scenarios where KLEE creates a child > > process. > > > > 1.My current understanding is that a 'state fork' performed at a branch > > condition will not result in a real forking of the KLEE process & does > > not invoke fork() syscall to create a child process of klee. i.e. the > > 'state forking' described in the original KLEE paper is a process where > > the objects in klee's memory are updated to create a new state. > > Can I check if this understanding is correct ? > > > > 2.In code, I encountered some cases where the fork() syscall is invoked. > > lib/Solver/MetaSMTSolver.cpp > > tools/klee-replay/file-creator.c > > tools/klee-replay/klee-replay.c etc > > Can I check if there are any cases where fork() syscall is issued to > > fork the klee process as a result of 'state forks' in symbolic execution > ? > > > > I went through the mailing list history and some literature/papers on > > klee, but cout not find a definite answer. I would really appreciate it > > if someone can help clarify. > > Thanks in advance. > > -- > > Pansilu Pitigalaarachchi > > > > > > ___ > > klee-dev mailing list > > klee-dev@imperial.ac.uk > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > ___ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > -- Pansilu Pitigalaarachchi ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] fork() : creating child processes in KLEE's execution
Hi, KLEE does not use the system call fork() to fork states. See Executor::fork() in the code. Best, Cristian On 23/02/2022 18:40, Pansilu Pitigalaarachchi wrote: Hi, I would like to check the possible scenarios where KLEE creates a child process. 1.My current understanding is that a 'state fork' performed at a branch condition will not result in a real forking of the KLEE process & does not invoke fork() syscall to create a child process of klee. i.e. the 'state forking' described in the original KLEE paper is a process where the objects in klee's memory are updated to create a new state. Can I check if this understanding is correct ? 2.In code, I encountered some cases where the fork() syscall is invoked. lib/Solver/MetaSMTSolver.cpp tools/klee-replay/file-creator.c tools/klee-replay/klee-replay.c etc Can I check if there are any cases where fork() syscall is issued to fork the klee process as a result of 'state forks' in symbolic execution ? I went through the mailing list history and some literature/papers on klee, but cout not find a definite answer. I would really appreciate it if someone can help clarify. Thanks in advance. -- Pansilu Pitigalaarachchi ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] fork() : creating child processes in KLEE's execution
Hi, I would like to check the possible scenarios where KLEE creates a child process. 1.My current understanding is that a 'state fork' performed at a branch condition will not result in a real forking of the KLEE process & does not invoke fork() syscall to create a child process of klee. i.e. the 'state forking' described in the original KLEE paper is a process where the objects in klee's memory are updated to create a new state. Can I check if this understanding is correct ? 2.In code, I encountered some cases where the fork() syscall is invoked. lib/Solver/MetaSMTSolver.cpp tools/klee-replay/file-creator.c tools/klee-replay/klee-replay.c etc Can I check if there are any cases where fork() syscall is issued to fork the klee process as a result of 'state forks' in symbolic execution ? I went through the mailing list history and some literature/papers on klee, but cout not find a definite answer. I would really appreciate it if someone can help clarify. Thanks in advance. -- Pansilu Pitigalaarachchi ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev