Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixes related to Gazer 2.0 #99

Open
wants to merge 24 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
cb82587
Refactor topological sorts into their own classes
sallaigy Dec 30, 2020
716c3de
Some refactoring for BMC backend
sallaigy Dec 30, 2020
89c01c4
Introduce classof_iterator to filter and cast polymorphic ranges
sallaigy Dec 31, 2020
2eed431
Remove NormalizeVerifierCalls pass, handle verifier function in Speci…
sallaigy Jan 16, 2021
cfcdc2b
Refactor Z3Solver
sallaigy Jan 18, 2021
0436b2f
Variables created through GazerContext can no longer have name collis…
sallaigy Jan 24, 2021
3e1448a
Add tests and small fixes in BoundedModelChecker
sallaigy Jan 24, 2021
99d5b51
Move CFA inlining algorithm out of BoundedModelChecker.cpp
sallaigy Jan 31, 2021
9cb6fdc
Refactor ExprWalker to use virtual methods instead of CRTP
sallaigy Feb 6, 2021
b1d8173
Small fixes and refactorings
sallaigy Mar 16, 2021
f9aca62
Rework CMake files
sallaigy Dec 26, 2020
45b2a23
Fix code smells flagged by SonarLint
sallaigy May 2, 2021
d0962d0
Remove unneeded files
sallaigy May 4, 2021
8e351c5
Add missing cases to ExprWalker and ExprRewrite
sallaigy May 11, 2021
8504317
Update Boost dependency to 1.74
sallaigy May 13, 2021
04ff7c9
Upgrade to LLVM 12
sallaigy May 29, 2021
8acd747
Disable failing portfolio tests
sallaigy Sep 25, 2021
c75dfc0
Mark some issues flagged by SonarLint
sallaigy Sep 25, 2021
9d9146e
Download Boost instead of relying on OS packages
sallaigy Sep 25, 2021
22baa3b
Move BoundedModelChecker back to the Verifier directory
sallaigy Sep 26, 2021
415e250
Fix some build warnings
sallaigy Sep 26, 2021
ea7734c
CFA variable iteration should return pointers
sallaigy Sep 27, 2021
8582926
GitHub actions experiment (#1)
sallaigy Oct 13, 2021
865b728
Change SonarCloud GH action scope
sallaigy Oct 29, 2021
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .clang-tidy
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,4 @@ Checks: '

HeaderFilterRegex: 'include/*.h'
AnalyzeTemporaryDtors: false
FormatStyle: none
FormatStyle: none
10 changes: 6 additions & 4 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -13,15 +13,17 @@ jobs:
run: sudo apt-get install build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil
- name: Set up some more dependencies
run: |
sudo apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost-all-dev
sudo apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime
sudo ln -sf /usr/bin/clang-9 /usr/bin/clang
sudo ln -s `which opt-9` /usr/bin/opt -f
sudo ln -s `which FileCheck-9` /usr/bin/FileCheck
sudo pip3 install lit
- name: Set up portfolio dependencies
run: sudo apt-get install perl libyaml-tiny-perl libproc-processtable-perl
- name: Build
run: cmake -DCMAKE_CXX_COMPILER=clang++-9 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On . && make
run: |
cmake -B build -DCMAKE_CXX_COMPILER=clang++-9 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On
cmake --build build/ -j2
- name: Get Theta
run: |
mkdir tools/gazer-theta/theta
Expand All @@ -32,6 +34,6 @@ jobs:
env:
THETA_VERSION: v2.10.0
- name: Run unit tests
run: make check-unit
run: cmake --build build --target check-unit
- name: Run functional tests
run: make check-functional
run: cmake --build build --target check-functional
64 changes: 64 additions & 0 deletions .github/workflows/sonarcloud.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
name: Run SonarCloud analysis

on: ['push', 'pull_request']

jobs:
build:
runs-on: ubuntu-20.04
env:
SONAR_SCANNER_VERSION: 4.6.1.2450
SONAR_SERVER_URL: "https://sonarcloud.io"
BUILD_WRAPPER_OUT_DIR: build_wrapper_output_directory
steps:
- uses: actions/checkout@v2
with:
fetch-depth: 0
- name: Update apt
run: sudo apt-get update
- name: Set up dependencies
run: sudo apt-get install build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil
- name: Set up some more dependencies
run: |
sudo apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime
sudo ln -sf /usr/bin/clang-9 /usr/bin/clang
sudo ln -s `which opt-9` /usr/bin/opt -f
- name: Cache SonarCloud packages and analysis
uses: actions/cache@v1
with:
path: ~/.sonar/cache
key: ${{ runner.os }}-sonar
restore-keys: ${{ runner.os }}-sonar
- name: Download and set up sonar-scanner
env:
SONAR_SCANNER_DOWNLOAD_URL: https://binaries.sonarsource.com/Distribution/sonar-scanner-cli/sonar-scanner-cli-${{ env.SONAR_SCANNER_VERSION }}-linux.zip
run: |
mkdir -p $HOME/.sonar
curl -sSLo $HOME/.sonar/sonar-scanner.zip ${{ env.SONAR_SCANNER_DOWNLOAD_URL }}
unzip -o $HOME/.sonar/sonar-scanner.zip -d $HOME/.sonar/
echo "$HOME/.sonar/sonar-scanner-${{ env.SONAR_SCANNER_VERSION }}-linux/bin" >> $GITHUB_PATH
- name: Download and set up build-wrapper
env:
BUILD_WRAPPER_DOWNLOAD_URL: ${{ env.SONAR_SERVER_URL }}/static/cpp/build-wrapper-linux-x86.zip
run: |
curl -sSLo $HOME/.sonar/build-wrapper-linux-x86.zip ${{ env.BUILD_WRAPPER_DOWNLOAD_URL }}
unzip -o $HOME/.sonar/build-wrapper-linux-x86.zip -d $HOME/.sonar/
echo "$HOME/.sonar/build-wrapper-linux-x86" >> $GITHUB_PATH
- name: Build
run: |
mkdir build
cmake -B build -DCMAKE_CXX_COMPILER=clang++-9 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Release -DCMAKE_EXPORT_COMPILE_COMMANDS=On -DGAZER_ENABLE_COVERAGE=On
build-wrapper-linux-x86-64 --out-dir ${{ env.BUILD_WRAPPER_OUT_DIR }} cmake --build build/
- name: Run unit tests
continue-on-error: true
run: |
cmake --build build --target check-unit
- name: Compile coverage reports
run: |
llvm-profdata-9 merge -sparse `find . -name "*.profraw"` -o coverage.profdata
llvm-cov-9 show -instr-profile=coverage.profdata $(for f in $(find ./build/src -name "libGazer*.so"); do echo -object $f; done) > llvm_cov_report.txt
- name: Run sonar-scanner
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}
run: |
sonar-scanner --define sonar.host.url="${{ env.SONAR_SERVER_URL }}" --define sonar.cfamily.build-wrapper-output="${{ env.BUILD_WRAPPER_OUT_DIR }}"
50 changes: 44 additions & 6 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
cmake_minimum_required(VERSION 3.8)
cmake_minimum_required(VERSION 3.13)
project(gazer)

# Set version information
Expand Down Expand Up @@ -43,7 +43,8 @@ if(GAZER_ENABLE_SANITIZER)
endif()
endif()

# Coverage
## Coverage
################################################################################
option(GAZER_ENABLE_COVERAGE "Enable code coverage" OFF)
if (GAZER_ENABLE_COVERAGE)
if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang")
Expand All @@ -58,19 +59,56 @@ if (GAZER_ENABLE_COVERAGE)
endif()

# Get LLVM
find_package(LLVM 9.0 REQUIRED CONFIG)
find_package(LLVM 12.0 REQUIRED CONFIG)
message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}")
message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}")

include_directories(${LLVM_INCLUDE_DIRS})
add_definitions(${LLVM_DEFINITIONS})
list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")

# If `GAZER_SHARED_LLVM` is on, we want to link against LLVM dynamically.
# If it is set to off, we want to map components to static library names
# and link against those.
option(GAZER_SHARED_LLVM "Link against shared libLLVM.so" OFF)

function(require_llvm_libraries outVar)
if (GAZER_SHARED_LLVM)
message(STATUS "Searching for shared libLLVM in ${LLVM_LIBRARY_DIR}")
find_library(
LLVM_LIBS
NAMES LLVM-9
PATHS ${LLVM_LIBRARY_DIRS}
NO_DEFAULT_PATH
)
message(STATUS "Found shared libLLVM in ${LLVM_LIBS}")
set(${outVar} ${LLVM_LIBS} PARENT_SCOPE)
else()
llvm_map_components_to_libnames(LLVM_LIBRARY_NAMES ${ARGN})
set(${outVar} ${LLVM_LIBRARY_NAMES} PARENT_SCOPE)
endif()
endfunction()

# Get boost
find_package(Boost 1.70 REQUIRED)
include_directories(${Boost_INCLUDE_DIR})
include(FetchContent)

FetchContent_Declare(
Boost
URL https://boostorg.jfrog.io/artifactory/main/release/1.76.0/source/boost_1_76_0.tar.bz2
URL_HASH SHA256=f0397ba6e982c4450f27bf32a2a83292aba035b827a5623a14636ea583318c41
)
FetchContent_GetProperties(Boost)

if(NOT Boost_POPULATED)
message(STATUS "Fetching Boost")
FetchContent_Populate(Boost)
message(STATUS "Fetching Boost - done")
endif()

message("Boost include directories are ${boost_SOURCE_DIR}")
add_definitions(-DBOOST_NO_RTTI -DBOOST_EXCEPTION_DISABLE -DBOOST_NO_EXCEPTIONS -DBOOST_NO_IOSTREAM)
include_directories(${boost_SOURCE_DIR})

add_definitions(-DBOOST_NO_RTTI -DBOOST_EXCEPTION_DISABLE -DBOOST_NO_EXCEPTIONS)

# Project directories
set(GAZER_INCLUDE_DIR "${CMAKE_CURRENT_LIST_DIR}/include")
Expand Down
13 changes: 7 additions & 6 deletions Dockerfile
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
FROM ubuntu:18.04
FROM ubuntu:20.04

ARG DEBIAN_FRONTEND=noninteractive
ENV TZ=Europe/Budapest
ENV THETA_VERSION v2.10.0

RUN apt-get update && \
Expand All @@ -10,11 +12,10 @@ RUN apt-get update && \

# fetch LLVM and other dependencies
RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && \
add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-9 main" && \
add-apt-repository "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-12 main" && \
apt-get update && \
add-apt-repository ppa:mhier/libboost-latest && \
apt-get update && \
apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost1.70-dev perl libyaml-tiny-perl
apt-get install -y clang-12 llvm-12-dev llvm-12-tools llvm-12-runtime perl libyaml-tiny-perl

# create a new user `user` with the password `user` and sudo rights
RUN useradd -m user && \
Expand All @@ -24,15 +25,15 @@ RUN useradd -m user && \

# (the portfolio uses clang)
RUN ln -sf /usr/bin/clang-9 /usr/bin/clang

USER user

ENV GAZER_DIR /home/user/gazer

ADD --chown=user:user . $GAZER_DIR

WORKDIR $GAZER_DIR
RUN cmake -DCMAKE_CXX_COMPILER=clang++-9 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On . && make
RUN cmake -DCMAKE_CXX_COMPILER=clang++-12 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On . && make

# download theta (and libs)
RUN mkdir $GAZER_DIR/tools/gazer-theta/theta && \
Expand Down
17 changes: 0 additions & 17 deletions cmake/GoogleTestDownload.cmake

This file was deleted.

1 change: 1 addition & 0 deletions doc/Developers.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
In addition to the standard cmake flags, Gazer builds may be configured with the following Gazer-specific flags:
* **GAZER_ENABLE_UNIT_TESTS:** Build Gazer unit tests. Defaults to ON.
* **GAZER_ENABLE_SANITIZER:** Enable the address and undefined behavior sanitizers. Defaults to OFF.
* **GAZER_SHARED_LLVM:** Link LLVM components dynamically (e.g. using `libLLVM.so`). Only recommended for debug builds, defaults to OFF.

## Test

Expand Down
22 changes: 11 additions & 11 deletions include/gazer/ADT/Graph.h
Original file line number Diff line number Diff line change
Expand Up @@ -125,8 +125,8 @@ class GraphEdge
template<class NodeTy, class EdgeTy>
class Graph
{
static_assert(std::is_base_of_v<GraphNode<NodeTy, EdgeTy>, NodeTy>, "");
static_assert(std::is_base_of_v<GraphEdge<NodeTy, EdgeTy>, EdgeTy>, "");
static_assert(std::is_base_of_v<GraphNode<NodeTy, EdgeTy>, NodeTy>);
static_assert(std::is_base_of_v<GraphEdge<NodeTy, EdgeTy>, EdgeTy>);

using NodeVectorTy = std::vector<std::unique_ptr<NodeTy>>;
using EdgeVectorTy = std::vector<std::unique_ptr<EdgeTy>>;
Expand All @@ -135,11 +135,11 @@ class Graph
using node_iterator = SmartPtrGetIterator<typename NodeVectorTy::iterator>;
using const_node_iterator = SmartPtrGetIterator<typename NodeVectorTy::const_iterator>;

node_iterator node_begin() { return mNodes.begin(); }
node_iterator node_end() { return mNodes.end(); }
node_iterator node_begin() { return node_iterator(mNodes.begin()); }
node_iterator node_end() { return node_iterator(mNodes.end()); }

const_node_iterator node_begin() const { return mNodes.begin(); }
const_node_iterator node_end() const { return mNodes.end(); }
const_node_iterator node_begin() const { return const_node_iterator(mNodes.begin()); }
const_node_iterator node_end() const { return const_node_iterator(mNodes.end()); }

llvm::iterator_range<node_iterator> nodes() {
return llvm::make_range(node_begin(), node_end());
Expand All @@ -151,11 +151,11 @@ class Graph
using edge_iterator = SmartPtrGetIterator<typename EdgeVectorTy::iterator>;
using const_edge_iterator = SmartPtrGetIterator<typename EdgeVectorTy::const_iterator>;

edge_iterator edge_begin() { return mEdges.begin(); }
edge_iterator edge_end() { return mEdges.end(); }
edge_iterator edge_begin() { return edge_iterator(mEdges.begin()); }
edge_iterator edge_end() { return edge_iterator(mEdges.end()); }

const_edge_iterator edge_begin() const { return mEdges.begin(); }
const_edge_iterator edge_end() const { return mEdges.end(); }
const_edge_iterator edge_begin() const { return const_edge_iterator(mEdges.begin()); }
const_edge_iterator edge_end() const { return const_edge_iterator(mEdges.end()); }
llvm::iterator_range<edge_iterator> edges() {
return llvm::make_range(edge_begin(), edge_end());
}
Expand Down Expand Up @@ -360,6 +360,6 @@ struct GraphTraits<Inverse<gazer::GraphNode<NodeTy, EdgeTy>*>>
}
};

} // namespace gazer
} // namespace llvm

#endif
Loading