diff options
| -rw-r--r-- | runtime/Sanitizer/README.md | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/runtime/Sanitizer/README.md b/runtime/Sanitizer/README.md new file mode 100644 index 00000000..3071ba71 --- /dev/null +++ b/runtime/Sanitizer/README.md @@ -0,0 +1,74 @@ +# KLEE UBSan runtime + +## Introduction + +KLEE UBSan runtime is a tailored runtime +of [UndefinedBehaviorSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) to meet KLEE needs. For +certain reasons, not all [checks](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html#available-checks) and +diagnostics are supported in there. + +## Usage + +Use `clang++` to compile and link your program with sanitizer flags. Make sure to use `clang++` (not `ld`) as a +linker, so that your executable is linked with proper UBSan runtime libraries. You can use `clang` instead of `clang++` +if you’re compiling/linking C code. + +For compiling/linking with **all** available checks to catch **both** undefined behaviour and unintentional issues, just +add one of the following options: + +* Short exclusive form + * `-fsanitize=undefined,float-divide-by-zero,unsigned-integer-overflow,implicit-conversion,nullability -fno-sanitize=local-bounds,function,vptr` +* Verbose inclusive form + * LLVM 11 and lower + * `-fsanitize=alignment,bool,builtin,array-bounds,enum,float-cast-overflow,float-divide-by-zero,implicit-unsigned-integer-truncation,implicit-signed-integer-truncation,implicit-integer-sign-change,integer-divide-by-zero,nonnull-attribute,null,nullability-arg,nullability-assign,nullability-return,object-size,pointer-overflow,return,returns-nonnull-attribute,shift,signed-integer-overflow,unreachable,unsigned-integer-overflow,vla-bound` + * LLVM 12 and higher + * `-fsanitize=alignment,bool,builtin,array-bounds,enum,float-cast-overflow,float-divide-by-zero,implicit-unsigned-integer-truncation,implicit-signed-integer-truncation,implicit-integer-sign-change,integer-divide-by-zero,nonnull-attribute,null,nullability-arg,nullability-assign,nullability-return,object-size,pointer-overflow,return,returns-nonnull-attribute,shift,unsigned-shift-base,signed-integer-overflow,unreachable,unsigned-integer-overflow,vla-bound` + +For compiling/linking with **all** available checks to catch **only** undefined behaviour, just add +the following option: + +* `-fsanitize=undefined -fno-sanitize=local-bounds,function,vptr` + +## Available checks + +Available checks for KLEE as are: + +* `-fsanitize=alignment` +* `-fsanitize=bool` +* `-fsanitize=builtin` +* `-fsanitize=array-bounds` +* `-fsanitize=enum` +* `-fsanitize=float-cast-overflow` +* `-fsanitize=float-divide-by-zero` +* `-fsanitize=implicit-unsigned-integer-truncation` +* `-fsanitize=implicit-signed-integer-truncation` +* `-fsanitize=implicit-integer-sign-change` +* `-fsanitize=integer-divide-by-zero` +* `-fsanitize=nonnull-attribute` +* `-fsanitize=null` +* `-fsanitize=nullability-arg` +* `-fsanitize=nullability-assign` +* `-fsanitize=nullability-return` +* `-fsanitize=object-size` +* `-fsanitize=pointer-overflow` +* `-fsanitize=return` +* `-fsanitize=returns-nonnull-attribute` +* `-fsanitize=shift` +* `-fsanitize=unsigned-shift-base` +* `-fsanitize=signed-integer-overflow` +* `-fsanitize=unreachable` +* `-fsanitize=unsigned-integer-overflow` +* `-fsanitize=vla-bound` + +## Unavailable checks + +Also, note some unavailable checks as are: + +* `-fsanitize=local-bounds` +* `-fsanitize=function` +* `-fsanitize=objc-cast` +* `-fsanitize=vptr` + +## Additional Configuration + +Additional configuration via UBSan options and environment variables may not work as expected, so use with care. \ No newline at end of file |