-
Notifications
You must be signed in to change notification settings - Fork 136
/
Configuration.txt
114 lines (79 loc) · 5.14 KB
/
Configuration.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
Configuration options
SymCC is configured at two different stages:
1. At compile time, you decide which features to enable, which mainly affects
compilation time and the set of dependencies. This is done via arguments to
CMake.
2. When you run programs that have been compiled with SymCC, the environment
variables control various aspects of the execution and analysis.
We list all available options for each stage in turn.
Compile-time options
Each of these is passed to CMake with "-D" when configuring the build:
- QSYM_BACKEND=ON/OFF (default OFF): Compile either the QSYM backend or our
simple Z3 wrapper (see docs/Backends.txt for details). Note that binaries
produced by the SymCC compiler are backend-agnostic; you can use
LD_LIBRARY_PATH to switch between backends per execution.
- TARGET_32BIT=ON/OFF (default OFF): Enable support for 32-bit compilation on
64-bit hosts. This will essentially make the compiler switch "-m32" work as
expected; see docs/32-bit.txt for details.
- LLVM_DIR/LLVM_32BIT_DIR (default empty): Hints for the build system to find
LLVM if it's in a non-standard location.
- Z3_DIR/Z3_32BIT_DIR (default empty): Hints for the build system to find Z3 if
it's in a non-standard location.
- Z3_TRUST_SYSTEM_VERSION (default OFF): Trust that the system provides a
suitable version of Z3 if the corresponding CMake module can't be found. Use
this with Linux distributions that don't package the CMake module but still
ship an otherwise usable development setup (e.g., Fedora before F33). Note
that we can't check the Z3 version for compatibility in this case, so prepare
for compiler errors if the system-wide installation of Z3 is too old.
Run-time options
"Run time" refers to the time when you run programs compiled with SymCC, not
when you run SymCC itself. In other words, these are settings that you can
change on every execution of an instrumented program. They are specified via
environment variables.
- SYMCC_NO_SYMBOLIC_INPUT=0/1 (default 0): When set to 1, input is never marked
as symbolic; in other words, instrumented programs will run just like their
uninstrumented counterparts.
- SYMCC_OUTPUT_DIR (default "/tmp/output"): This is the directory where SymCC
will store new inputs (QSYM backend only). If you prefer to handle them
programmatically, make your program call symcc_set_test_case_handler; the
handler will be called instead of the default handler each time the backend
generates a new input.
- SYMCC_INPUT_FILE (default empty): When empty, SymCC treats data read from
standard input as symbolic; when set to a file name, any data read from that
file is considered symbolic. Ignored if SYMCC_NO_SYMBOLIC_INPUT is set to 1.
- SYMCC_MEMORY_INPUT=0/1 (default 0): When set to 1, expect the program under
test to communicate symbolic inputs with one or more calls to
symcc_make_symbolic. Can't be combined with SYMCC_INPUT_FILE. Ignored if
SYMCC_NO_SYMBOLIC_INPUT is set to 1.
- SYMCC_LOG_FILE (default empty): When set to a file name, SymCC creates the
file (or overwrites any existing file!) and uses it to log backend activity
including solver output (simple backend only).
- SYMCC_ENABLE_LINEARIZATION=0/1 (default 0): Enable QSYM's basic-block pruning,
a call-stack-aware strategy to reduce solver queries when executing code
repeatedly (QSYM backend only). See the QSYM paper for details; highly
recommended for fuzzing and enabled automatically by the fuzzing helper.
- SYMCC_AFL_COVERAGE_MAP (default empty): When set to the file name of an
AFL-style coverage map, load the map before executing the target program and
use it to skip solver queries for paths that have already been covered (QSYM
backend only). The map is updated in place, so beware of races when running
multiple instances of SymCC! The fuzzing helper uses this to remember the
state of exploration across multiple executions of the target program.
Warning: This setting has a misleading name - while the format of the map
follows (classic) AFL, the variable isn't meant to point at a map file that
AFL uses too!
(Most people should stop reading here.)
Advanced options
There is actually a third category of options: when compiling with SymCC, you
can specify the location of its various components via environment variables.
This is not necessary in most cases because the build system makes sure that all
components know about each other; however, in some advanced setups you may need
to move files around after building them, and in that case, you can use the
variables documented below to communicate the new locations:
- SYMCC_RUNTIME_DIR and SYMCC_RUNTIME32_DIR: The directory that contains the
run-time support library (i.e., libSymRuntime.so).
- SYMCC_PASS_DIR: The directory containing the compiler pass (i.e.,
libSymbolize.so).
- SYMCC_CLANG and SYMCC_CLANGPP: The clang and clang++ binaries to use during
compilation. Be very careful with this one: if the version of the compiler you
specify here doesn't match the one you built SymCC against, you'll most likely
get linker errors.