forked from eurecom-s3/symcc
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathConfiguration.txt
72 lines (47 loc) · 3.01 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
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, 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.
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).
- 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.
- 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
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.