Merge upstream

.clang-format

@@ -0,0 +1,192 @@
+---
+Language:        Cpp
+# BasedOnStyle:  LLVM
+AccessModifierOffset: -2
+AlignAfterOpenBracket: Align
+AlignArrayOfStructures: None
+AlignConsecutiveMacros: None
+AlignConsecutiveAssignments: None
+AlignConsecutiveBitFields: None
+AlignConsecutiveDeclarations: None
+AlignEscapedNewlines: Right
+AlignOperands:   Align
+AlignTrailingComments: true
+AllowAllArgumentsOnNextLine: true
+AllowAllParametersOfDeclarationOnNextLine: true
+AllowShortEnumsOnASingleLine: true
+AllowShortBlocksOnASingleLine: Never
+AllowShortCaseLabelsOnASingleLine: false
+AllowShortFunctionsOnASingleLine: All
+AllowShortLambdasOnASingleLine: All
+AllowShortIfStatementsOnASingleLine: Never
+AllowShortLoopsOnASingleLine: false
+AlwaysBreakAfterDefinitionReturnType: None
+AlwaysBreakAfterReturnType: None
+AlwaysBreakBeforeMultilineStrings: false
+AlwaysBreakTemplateDeclarations: MultiLine
+AttributeMacros:
+  - __capability
+BinPackArguments: true
+BinPackParameters: true
+BraceWrapping:
+  AfterCaseLabel:  false
+  AfterClass:      false
+  AfterControlStatement: Never
+  AfterEnum:       false
+  AfterFunction:   false
+  AfterNamespace:  false
+  AfterObjCDeclaration: false
+  AfterStruct:     false
+  AfterUnion:      false
+  AfterExternBlock: false
+  BeforeCatch:     false
+  BeforeElse:      false
+  BeforeLambdaBody: false
+  BeforeWhile:     false
+  IndentBraces:    false
+  SplitEmptyFunction: true
+  SplitEmptyRecord: true
+  SplitEmptyNamespace: true
+BreakBeforeBinaryOperators: None
+BreakBeforeConceptDeclarations: true
+BreakBeforeBraces: Attach
+BreakBeforeInheritanceComma: false
+BreakInheritanceList: BeforeColon
+BreakBeforeTernaryOperators: true
+BreakConstructorInitializersBeforeComma: false
+BreakConstructorInitializers: BeforeColon
+BreakAfterJavaFieldAnnotations: false
+BreakStringLiterals: true
+ColumnLimit:     80
+CommentPragmas:  '^ IWYU pragma:'
+QualifierAlignment: Leave
+CompactNamespaces: false
+ConstructorInitializerIndentWidth: 4
+ContinuationIndentWidth: 4
+Cpp11BracedListStyle: true
+DeriveLineEnding: true
+DerivePointerAlignment: false
+DisableFormat:   false
+EmptyLineAfterAccessModifier: Never
+EmptyLineBeforeAccessModifier: LogicalBlock
+ExperimentalAutoDetectBinPacking: false
+PackConstructorInitializers: BinPack
+BasedOnStyle:    ''
+ConstructorInitializerAllOnOneLineOrOnePerLine: false
+AllowAllConstructorInitializersOnNextLine: true
+FixNamespaceComments: true
+ForEachMacros:
+  - foreach
+  - Q_FOREACH
+  - BOOST_FOREACH
+IfMacros:
+  - KJ_IF_MAYBE
+IncludeBlocks:   Preserve
+IncludeCategories:
+  - Regex:           '^"(llvm|llvm-c|clang|clang-c)/'
+    Priority:        2
+    SortPriority:    0
+    CaseSensitive:   false
+  - Regex:           '^(<|"(gtest|gmock|isl|json)/)'
+    Priority:        3
+    SortPriority:    0
+    CaseSensitive:   false
+  - Regex:           '.*'
+    Priority:        1
+    SortPriority:    0
+    CaseSensitive:   false
+IncludeIsMainRegex: '(Test)?$'
+IncludeIsMainSourceRegex: ''
+IndentAccessModifiers: false
+IndentCaseLabels: false
+IndentCaseBlocks: false
+IndentGotoLabels: true
+IndentPPDirectives: None
+IndentExternBlock: AfterExternBlock
+IndentRequires:  false
+IndentWidth:     2
+IndentWrappedFunctionNames: false
+InsertTrailingCommas: None
+JavaScriptQuotes: Leave
+JavaScriptWrapImports: true
+KeepEmptyLinesAtTheStartOfBlocks: true
+LambdaBodyIndentation: Signature
+MacroBlockBegin: ''
+MacroBlockEnd:   ''
+MaxEmptyLinesToKeep: 1
+NamespaceIndentation: None
+ObjCBinPackProtocolList: Auto
+ObjCBlockIndentWidth: 2
+ObjCBreakBeforeNestedBlockParam: true
+ObjCSpaceAfterProperty: false
+ObjCSpaceBeforeProtocolList: true
+PenaltyBreakAssignment: 2
+PenaltyBreakBeforeFirstCallParameter: 19
+PenaltyBreakComment: 300
+PenaltyBreakFirstLessLess: 120
+PenaltyBreakOpenParenthesis: 0
+PenaltyBreakString: 1000
+PenaltyBreakTemplateDeclaration: 10
+PenaltyExcessCharacter: 1000000
+PenaltyReturnTypeOnItsOwnLine: 60
+PenaltyIndentedWhitespace: 0
+PointerAlignment: Right
+PPIndentWidth:   -1
+ReferenceAlignment: Pointer
+ReflowComments:  true
+RemoveBracesLLVM: false
+SeparateDefinitionBlocks: Leave
+ShortNamespaceLines: 1
+SortIncludes:    CaseSensitive
+SortJavaStaticImport: Before
+SortUsingDeclarations: true
+SpaceAfterCStyleCast: false
+SpaceAfterLogicalNot: false
+SpaceAfterTemplateKeyword: true
+SpaceBeforeAssignmentOperators: true
+SpaceBeforeCaseColon: false
+SpaceBeforeCpp11BracedList: false
+SpaceBeforeCtorInitializerColon: true
+SpaceBeforeInheritanceColon: true
+SpaceBeforeParens: ControlStatements
+SpaceBeforeParensOptions:
+  AfterControlStatements: true
+  AfterForeachMacros: true
+  AfterFunctionDefinitionName: false
+  AfterFunctionDeclarationName: false
+  AfterIfMacros:   true
+  AfterOverloadedOperator: false
+  BeforeNonEmptyParentheses: false
+SpaceAroundPointerQualifiers: Default
+SpaceBeforeRangeBasedForLoopColon: true
+SpaceInEmptyBlock: false
+SpaceInEmptyParentheses: false
+SpacesBeforeTrailingComments: 1
+SpacesInAngles:  Never
+SpacesInConditionalStatement: false
+SpacesInContainerLiterals: true
+SpacesInCStyleCastParentheses: false
+SpacesInLineCommentPrefix:
+  Minimum:         1
+  Maximum:         -1
+SpacesInParentheses: false
+SpacesInSquareBrackets: false
+SpaceBeforeSquareBrackets: false
+BitFieldColonSpacing: Both
+Standard:        Latest
+StatementAttributeLikeMacros:
+  - Q_EMIT
+StatementMacros:
+  - Q_UNUSED
+  - QT_REQUIRE_VERSION
+TabWidth:        8
+UseCRLF:         false
+UseTab:          Never
+WhitespaceSensitiveMacros:
+  - STRINGIZE
+  - PP_STRINGIZE
+  - BOOST_PP_STRINGIZE
+  - NS_SWIFT_NAME
+  - CF_SWIFT_NAME
+...
+

.github/workflows/run_tests.yml

@@ -1,5 +1,5 @@
 name: Compile and test SymCC
-on: [push, pull_request]
+on: [pull_request]
 jobs:
   build_and_test_symcc:
     runs-on: ubuntu-20.04
@@ -15,3 +15,29 @@ jobs:
         run: docker build --target builder_qsym  -t symcc .
       - name: Creation of the final SymCC docker image with Qsym backend and libcxx
         run: docker build  -t symcc .
+  llvm_compatibility:
+    runs-on: ubuntu-22.04
+    strategy:
+      matrix:
+        llvm_version: [11, 12, 13, 14]
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: true
+      - name: Install dependencies
+        run: |
+          sudo apt-get install -y \
+            llvm-${{ matrix.llvm_version }}-dev \
+            libz3-dev \
+            python2
+      - name: Build SymCC with the QSYM backend
+        run: |
+          mkdir build
+          cd build
+          cmake \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DZ3_TRUST_SYSTEM_VERSION=ON \
+            -DQSYM_BACKEND=ON \
+            -DLLVM_DIR=/usr/lib/llvm-${{ matrix.llvm_version }}/cmake \
+            ..
+          make

CMakeLists.txt

@@ -79,8 +79,8 @@ find_package(LLVM REQUIRED CONFIG)
 message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}")
 message(STATUS "Using LLVMConfig.cmake from ${LLVM_DIR}")
 
-if (${LLVM_VERSION_MAJOR} LESS 8 OR ${LLVM_VERSION_MAJOR} GREATER 11)
-  message(WARNING "The software has been developed for LLVM 8 through 11; \
+if (${LLVM_VERSION_MAJOR} LESS 8 OR ${LLVM_VERSION_MAJOR} GREATER 15)
+  message(WARNING "The software has been developed for LLVM 8 through 15; \
 it is unlikely to work with other versions!")
 endif()
 
@@ -90,7 +90,7 @@ include_directories(SYSTEM ${LLVM_INCLUDE_DIRS})
 set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++17 \
 -Wredundant-decls -Wcast-align -Wmissing-include-dirs -Wswitch-default \
 -Wextra -Wall -Winvalid-pch -Wredundant-decls -Wformat=2 \
--Wmissing-format-attribute -Wformat-nonliteral -Werror")
+-Wmissing-format-attribute -Wformat-nonliteral -Werror -Wno-error=deprecated-declarations")
 
 # Mark nodelete to work around unload bug in upstream LLVM 5.0+
 set(CMAKE_MODULE_LINKER_FLAGS "${CMAKE_MODULE_LINKER_FLAGS} -Wl,-z,nodelete")
@@ -117,6 +117,12 @@ if (NOT CLANG_BINARY)
   message(FATAL_ERROR "Clang not found; please make sure that the version corresponding to your LLVM installation is available.")
 endif()
 
+if (${LLVM_VERSION_MAJOR} LESS 13)
+  set(CLANG_LOAD_PASS "-Xclang -load -Xclang ")
+else()
+  set(CLANG_LOAD_PASS "-fpass-plugin=")
+endif()
+
 configure_file("compiler/symcc.in" "symcc" @ONLY)
 configure_file("compiler/sym++.in" "sym++" @ONLY)
 

README.md

@@ -15,16 +15,18 @@ compiler inserts code that computes symbolic expressions for each value in the
 program. The actual computation happens through calls to the support library at
 run time.
 
-To build the pass and the support library, make sure that LLVM 8, 9, 10 or 11
-and Z3 version 4.5 or later, as well as a C++ compiler with support for C++17
-are installed. "lit" is also needed which is not always packaged with LLVM.
+To build the pass and the support library, install LLVM (any version between 8
+and 15) and Z3 (version 4.5 or later), as well as a C++ compiler with support
+for C++17. LLVM lit is only needed to run the tests; if it's not packaged with
+your LLVM, you can get it with `pip install lit`.
 
-Under Ubuntu groovy the following one liner should install all required
+Under Ubuntu Groovy the following one liner should install all required
 packages:
 
 ```
 sudo apt install -y git cargo clang-10 cmake g++ git libz3-dev llvm-10-dev llvm-10-tools ninja-build python2 python3-pip zlib1g-dev && sudo pip3 install lit
 ```
+
 Alternatively, see below for using the provided Dockerfile, or the file
 `util/quicktest.sh` for exact steps to perform under Ubuntu (or use with the
 provided Vagrant file).
@@ -180,6 +182,57 @@ every change to SymCC (which is, in principle the right thing to do), whereas in
 many cases it is sufficient to let the build system figure out what to rebuild
 (and recompile, e.g., libc++ only when necessary).
 
+## FAQ / BUGS / TODOs
+
+### Why is SymCC only exploring one path and not all paths?
+
+SymCC is currently a concolic executor it follows the concrete
+path. In theory, it would be possible to make it a forking executor
+see [issue #14](https://github.com/eurecom-s3/symcc/issues/14)
+
+### Why does SymCC not generate some test cases?
+
+There are multiple possible reasons:
+
+#### QSym backend performs pruning
+
+When built with the QSym backend exploration (e.g., loops) symcc is
+subject to path pruning, this is part of the optimizations that makes
+SymCC/QSym fast, it isn't sound. This is not a problem for using in
+hybrid fuzzing, but this may be a problem for other uses. See for
+example [issue #88](https://github.com/eurecom-s3/symcc/issues/88).
+
+When building with the simple backend the paths should be found. If
+the paths are not found with the simple backend this may be a bug (or
+possibly a limitation of the simple backend).
+
+#### Incomplete symbolic handing of functions, systems interactions.
+
+The current symbolic understanding of libc is incomplete. So when an
+unsupported libc function is called SymCC can't trace the computations
+that happen in the function.
+
+1. Adding the function to the [collection of wrapped libc
+   functions](https://github.com/eurecom-s3/symcc/blob/master/runtime/LibcWrappers.cpp)
+   and [register the
+   wrapper](https://github.com/eurecom-s3/symcc/blob/b29dc4db2803830ebf50798e72b336473a567655/compiler/Runtime.cpp#L159)
+   in the compiler.
+2. Build a fully instrumented libc.
+3. Cherry-pick individual libc functions from a libc implementation (e.g., musl) 
+
+See [issue #23](https://github.com/eurecom-s3/symcc/issues/23) for more details.
+
+
+### Rust support ?
+
+This would be possible to support RUST, see [issue
+#1](https://github.com/eurecom-s3/symcc/issues/1) for tracking this.
+
+### Bug reporting
+
+We appreciate bugs with test cases and steps to reproduce, PR with
+corresponding test cases. SymCC is currently understaffed, we hope to
+catch up and get back to active development at some point.
 
 ## Contact