Merge branch 'eurecom-s3:master' into main

.clang-format

@@ -1,192 +1,3 @@
 ---
-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
+BasedOnStyle: LLVM
 ...
-

.github/workflows/run_tests.yml

@@ -42,3 +42,37 @@ jobs:
             -DLLVM_DIR=/usr/lib/llvm-${{ matrix.llvm_version }}/cmake \
             ..
           make
+  llvm_compatibility_latest_llvm:
+    runs-on: ubuntu-22.04
+    strategy:
+      matrix:
+        llvm_version: [16, 17]
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: true
+      - name: Add LLVM project deb repository
+        uses: myci-actions/add-deb-repo@11
+        with:
+          repo: deb http://apt.llvm.org/jammy/ llvm-toolchain-jammy-${{ matrix.llvm_version }} main
+          repo-name: llvm
+          update: false
+          keys-asc: https://apt.llvm.org/llvm-snapshot.gpg.key
+      - name: Install dependencies
+        run: |
+          sudo apt-get update
+          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

@@ -82,8 +82,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 16)
-  message(WARNING "The software has been developed for LLVM 8 through 16; \
+if (${LLVM_VERSION_MAJOR} LESS 8 OR ${LLVM_VERSION_MAJOR} GREATER 17)
+  message(WARNING "The software has been developed for LLVM 8 through 17; \
 it is unlikely to work with other versions!")
 endif()
 

Dockerfile

@@ -15,19 +15,19 @@
 #
 # The base image
 #
-FROM ubuntu:20.04 AS builder
+FROM ubuntu:22.04 AS builder
 
 # Install dependencies
 RUN apt-get update \
     && DEBIAN_FRONTEND=noninteractive apt-get install -y \
         cargo \
-        clang-10 \
+        clang-15 \
         cmake \
         g++ \
         git \
         libz3-dev \
-        llvm-10-dev \
-        llvm-10-tools \
+        llvm-15-dev \
+        llvm-15-tools \
         ninja-build \
         python2 \
         python3-pip \
@@ -42,7 +42,7 @@ RUN git clone -b v2.56b https://github.com/google/AFL.git afl \
 
 # Download the LLVM sources already so that we don't need to get them again when
 # SymCC changes
-RUN git clone -b llvmorg-10.0.1 --depth 1 https://github.com/llvm/llvm-project.git /llvm_source
+RUN git clone -b llvmorg-15.0.0 --depth 1 https://github.com/llvm/llvm-project.git /llvm_source
 
 # Build a version of SymCC with the simple backend to compile libc++
 COPY . /symcc_source
@@ -105,14 +105,14 @@ RUN cmake -G Ninja \
 #
 # The final image
 #
-FROM ubuntu:20.04
+FROM ubuntu:22.04
 
 RUN apt-get update \
     && DEBIAN_FRONTEND=noninteractive apt-get install -y \
         build-essential \
-        clang-10 \
+        clang-15 \
         g++ \
-        libllvm10 \
+        libllvm15 \
         zlib1g \
         sudo \
     && rm -rf /var/lib/apt/lists/* \
@@ -127,8 +127,8 @@ COPY --from=builder_qsym /afl /afl
 
 ENV PATH /symcc_build:$PATH
 ENV AFL_PATH /afl
-ENV AFL_CC clang-10
-ENV AFL_CXX clang++-10
+ENV AFL_CC clang-15
+ENV AFL_CXX clang++-15
 ENV SYMCC_LIBCXX_PATH=/libcxx_symcc_install
 
 USER ubuntu

README.md

@@ -9,14 +9,14 @@ of PRs, we will try to merge them when possible.
 
 # SymCC: efficient compiler-based symbolic execution
 
-SymCC is a compiler wrapper which embeds symbolic execution into the program
+SymCC is a compiler pass which embeds symbolic execution into the program
 during compilation, and an associated run-time support library. In essence, the
 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, install LLVM (any version between 8
-and 16) and Z3 (version 4.5 or later), as well as a C++ compiler with support
+and 17) 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`.
 

compiler/Main.cpp

@@ -13,7 +13,9 @@
 // SymCC. If not, see <https://www.gnu.org/licenses/>.
 
 #include <llvm/IR/LegacyPassManager.h>
+#if LLVM_VERSION_MAJOR <= 15
 #include <llvm/Transforms/IPO/PassManagerBuilder.h>
+#endif
 #include <llvm/Transforms/Scalar.h>
 #include <llvm/Transforms/Scalar/Scalarizer.h>
 

docs/32-bit.txt

@@ -26,12 +26,12 @@ install the 32-bit version of Z3 in your system.
 Once the dependencies for 32-bit SymCC are available (as well as the 64-bit
 dependencies mentioned in the main README), configure and build SymCC as usual
 but add "-DTARGET_32BIT=ON" to the CMake invocation. If the build system doesn't
-find your 32-bit versions of LLVM and Z3, specify their locations with
+find your 32-bit versions of LLVM and Z3, and specify their locations with
 "-DLLVM_32BIT_DIR=/some/path" and "-DZ3_32BIT_DIR=/some/other/path",
 respectively - analogously to how you would hint at the 64-bit versions.
 
 The resulting "symcc" and "sym++" scripts work like regular SymCC, but they
-additionally understand the "-m32" switch, which tells clang to build 32-bit
+additionally understand the "-m32" switch, which tells Clang to build 32-bit
 artifacts. If you build anything with "-m32", SymCC will make sure that the
 32-bit version of the symbolic backend is linked to it instead of the 64-bit
 variant that would normally be used. Note that, in order to compile C++ code

docs/Backends.txt

@@ -13,7 +13,7 @@ used. Also, we always link against "libSymRuntime.so", so the choice of backend
 is deferred until run time. From the target program's point of view, the only
 requirement on a backend is that it be a shared library with the expected name
 that implements the interface defined in runtime/RuntimeCommon.h (with type
-"SymExpr" defined to be something of pointer width).
+"SymExpr" is defined to be something of pointer width).
 
 Depending on the build option QSYM_BACKEND we build either our own backend or
 parts of QSYM (which are pulled in via a git submodule) and a small translation

docs/Concreteness.txt

@@ -18,9 +18,9 @@ There are two stages at which data can be identified as concrete:
 
 If we detect in the compiler pass that a value is a compile-time constant (case
 1 above), we do not emit code for symbolic handling at all. However, for any
-other type of data we need to generate code that handles the case of it being
+other type of data, we need to generate code that handles the case of it being
 symbolic at run time. Concretely (no pun intended), we mark concrete values at
-run time by setting its corresponding symbolic expression in shadow memory to
+run time by setting their corresponding symbolic expression in shadow memory to
 null. This makes it very cheap to check concreteness during execution: just run
 a null check on the symbolic expression.