The fork profile gives you a summary of all the locations in the system that forked. This helps debug sources of path explosion.
In order to obtain a fork profile, run the forkprofile subcommand as follows:
$ s2e new_project /home/users/coreutils-8.26/build/bin/cat -T @@ $ ... launch s2e and let it run for a while ... $ s2e forkprofile cat INFO: [symbols] Looking for debug information for /home/vitaly/s2e/env/projects/cat-symb/././cat INFO: [forkprofile] # The fork profile shows all the program counters where execution forked: INFO: [forkprofile] # process_pid module_path:address fork_count source_file:line_number (function_name) INFO: [forkprofile] 01309 cat:0x08049ade 143 /home/user/coreutils-8.26/src/cat.c:483 (cat) INFO: [forkprofile] 01309 cat:0x08049b0a 81 /home/user/coreutils-8.26/src/cat.c:488 (cat) INFO: [forkprofile] 01309 cat:0x08049981 73 /home/user/coreutils-8.26/src/cat.c:410 (cat)
The trace above shows that the cat module (which has a pid 1309) forked at three different program counters. The source information (if available) gives the source file, the line, and the function name where the forks occurred.
Using the fork profile to debug path explosion¶
- Spot locations that should not fork. For example, your program might write something to the console. This typically results in forks in the OS’s console driver. The source information will point to the responsible linux kernel driver, allowing you to quickly fix your bootstrap script (e.g., by redirecting output to /dev/null or a symbolic file).
- Identify library functions that can be optimized. You will immediately see if the program forks in functions such as strlen or atoi. These functions can be replaced with function models that eliminate forks altogether, although at the expense of generating more complex expressions.
- Identify sections of code that can benefit of state merging. Certain types of code sections are hard to model and can be instead surrounded by s2e_merge_group_begin() and s2e_merge_group_end() API calls, which will merge into one state the subtree in between these two calls.
Using the native fork profiler¶
This method is deprecated and may not work reliably (especially debug information).
Create a new project using s2e-env.
Start symbolic execution using
When analysis is done and the VM has shut down the
forkprofilermay be run.
./bin/forkprofiler -trace ./projects/<name</s2e-last/ExecutionTracer.dat -moddir /path/to/bin/dir
Running this command will produce a
forkprofiler.txtfile. This file will contain the list of function addresses where fork occurred.
If function names are required the
-moddiroption should be used. First mount the VM image as loop device.
mkdir /tmp/img-mount/ sudo mount -o loop,offset=1048576 ./images/s2e-linux-i386.raw.s2e /tmp/img-mount/
-moddirspecify path to the directory with analysed program. If you are using image created with
s2e-envthe program will be located in
/home/s2e/on the guest VM.
./bin/forkprofiler -trace ./projects/name/s2e-last/ExecutionTracer.dat -moddir /tmp/img-mount/home/s2e/
Once everything is done unmount the image.
sudo umount /tmp/img-mount/ rmdir /tmp/img-mount
If analysis is run on multiple cores each node will produce its own
ExecutionTracer.dat file in
./s2e-last/<node_number>/ExecutionTracer.dat. The following script may be used to process such cases. Save it in
the project folder and run,
#!/bin/bash MODDIR_PATH=/tmp/img-mount/home/s2e/ forkprofilerpath=../bin/forkprofiler path=`find $1/ -mindepth 1 -maxdepth 1 -type d | sort -V` cmd=$forkprofilerpath cmd="$cmd -moddir=$MODDIR_PATH " for d in $path; do tmppath=`readlink -f "$d/ExecutionTracer.dat"` cmd="$cmd -trace $tmppath " done echo $cmd $cmd
After running this script you will have a single forkprofiler.txt file as before.
- Directory containing the binary modules.
- The start address of kernel space.
- Store the fork profile into the given folder.
- -trace=<Input trace>
- Specify an execution trace file. These are available in
ModuleTracer(for debug information)