diff --git a/.gitignore b/.gitignore
index ae02f99b6..c38769aec 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
*~
+.clangd/*
sv-benchmarks/*
*/CMakeFiles/
*/Makefile
diff --git a/.gitmodules b/.gitmodules
index af8cbec7f..81095e6b1 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,9 +1,9 @@
[submodule "utils/base_image_map2check"]
path = utils/base_image_map2check
url = https://github.com/hbgit/base_image_map2check.git
-[submodule "utils/dev-llvm_6.0"]
- path = utils/dev-llvm_6.0
- url = https://github.com/hbgit/dev-llvm_6.0.git
[submodule "utils/benchexecrun"]
path = utils/benchexecrun
url = https://github.com/hbgit/benchexecrun.git
+[submodule "utils/llvm-docker-dev"]
+ path = utils/llvm-docker-dev
+ url = https://github.com/hbgit/llvm-docker-dev.git
diff --git a/.travis.yml b/.travis.yml
index b9c6703de..26578aa1a 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -2,8 +2,7 @@ dist: xenial
language: cpp
env:
- global:
- # - secure: "JlVpGztPCTzPA/F3IpRRxwXTD1kj9hN/Kprd1+TA/tSpDjP/l7U/dHepolEBkXa8DjPXUz93d7UNeasJR+vVbB0qX3VuAeWdYcRqdlqVMLL01qg0N9lKhoC9gdlLJ5dvQ30bA6tV7znbF0SQa8p5612RfJ9CO+CyeUY48+8tUTzt7rLtjmeIzu7+nVScEUVJjrx2OblPeLdomejxv7tVYvWLa2/X515wE7HE8jkbuwFuTrdobcdcB+0JaGv+c9TG/fcZlZc/i6Eq70ImWtGza7OMaFrZn5QFcKfA3TywSpVk7x9a1pdghAfNm6ZA9xQwZrTc+ih4RoMTvrN/3UeWz9GZRZsT+e1n7QYrpeG8VQhwEMpFgOFptGClOJ8CtIN90/Kfuuob7/T7sigs6mmpzhhPrJpid3BwKtnwoctJieZlBUddQ6JX83nQOLDYDsU/1c/JZXvIME46fevp0CMBXyYff2hPBmJESn3k5TOHy5e7RasdqMo1t4mZ5AR1dXys2+JPgGxFm0mboRwKyQByQUOl+ZXXhfw57C9Kpxzwg6gpKSy46nfM2whnv+1tcErvuzUWvvwaQ4qV9uC9xQhRXYMARct313WIQ2ZTkxIaYPIqS3YQgbtpEEO0oNmgLr2fLxhgkaZTN++JmkzPa2uamKjCmc+oaDC8MYqwPFb7An0="
+ global:
- GIT_NAME: hbgit
- GIT_EMAIL: herberthb12@gmail.com
- TRAVIS_REPO_SLUG: hbgit/Map2Check
@@ -12,17 +11,16 @@ services:
- docker
before_script:
-- docker build -t hrocha/mapdevel --no-cache -f Dockerfile .
-- docker build -t hrocha/benchexecrun --no-cache -f utils/benchexecrun/Dockerfile
+- docker build -t herberthb/mapdevel:v7.4 --no-cache -f Dockerfile .
+- docker build -t herberthb/benchexecrun --no-cache -f utils/benchexecrun/Dockerfile
utils/benchexecrun/
script:
- docker run --rm -v $(pwd):/home/map2check/devel_tool/mygitclone:Z --user $(id -u):$(id
- -g) hrocha/mapdevel /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./make-release.sh;
- ./make-unit-test.sh"
+ -g) herberthb/mapdevel:v7.4 /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./make-release.sh;"
- "./make-regression-test.sh t"
- docker run --rm -v $(pwd):/home/map2check/devel_tool/mygitclone:Z --user $(id -u):$(id
- -g) hrocha/mapdevel /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./check_code_style.py
+ -g) herberthb/mapdevel:v7.4 /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./check_code_style.py
-t -c -p"
notifications:
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 56406e153..650e8f3cd 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -4,20 +4,12 @@ project(Map2Check)
set(Map2Check_VERSION_MAJOR 7)
set(Map2Check_VERSION_MINOR 0)
-option(USE_PREBUILT_CLANG "Download and Install pre-built clang" ON)
option(BUILD_DOC "Build documentation" OFF)
-option(SKIP_LIB_FUZZER "Don't build libFuzzer" OFF)
-option(SKIP_KLEE "Don't build KLEE" OFF)
-option(REGRESSION "Prepare Regression Tests" OFF)
+#option(REGRESSION "Prepare Regression Tests" OFF)
option(ENABLE_TEST "Build all tests" OFF)
set (CMAKE_CXX_STANDARD 11)
-# set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
-# set(CMAKE_EXE_LINKER_FLAGS "-Bstatic -static-libgcc -static-libstdc++")
-# include(cmake/ExternalDeps.cmake)
-
-
set(Map2Check_MODE "STATIC")
set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
set(CMAKE_EXE_LINKER_FLAGS "-Bstatic -static-libgcc -static-libstdc++")
@@ -25,30 +17,18 @@ set(CMAKE_EXE_LINKER_FLAGS "-Bstatic -static-libgcc -static-libstdc++")
include(cmake/FindClang.cmake)
include(cmake/FindBoost.cmake)
-if(NOT SKIP_LIB_FUZZER)
- include(cmake/FindLibFuzzer.cmake)
-endif()
-
-if(NOT SKIP_KLEE)
- include(cmake/FindZ3.cmake)
- include(cmake/FindMiniSat.cmake)
- include(cmake/FindSTP.cmake)
- include(cmake/FindKleeUCLibC.cmake)
- include(cmake/FindKlee.cmake)
-endif()
-
-if(REGRESSION)
- include(cmake/DownloadRegression.cmake)
-endif()
+#if(REGRESSION)
+# include(cmake/DownloadRegression.cmake)
+#endif()
include_directories(${PROJECT_SOURCE_DIR})
-if(ENABLE_TEST)
- enable_testing()
- include(cmake/FindGTest.cmake)
- message("Adding tests")
- add_subdirectory(tests)
-endif()
+#if(ENABLE_TEST)
+# enable_testing()
+# include(cmake/FindGTest.cmake)
+# message("Adding tests")
+# add_subdirectory(tests)
+#endif()
add_subdirectory(modules)
diff --git a/Dockerfile b/Dockerfile
index 45dd81b7d..3907462bf 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -4,15 +4,15 @@
# Usage:
#
# By gitclone https://github.com/hbgit/Map2Check:
-# $ docker build -t hrocha/mapdevel --no-cache -f Dockerfile .
-# $ docker run -it --name=mapdevel -v $(pwd):/home/map2check/devel_tool/mygitclone:Z --user $(id -u):$(id -g) hrocha/mapdevel /bin/bash
+# $ docker build -t herberthb/mapdevel --no-cache -f Dockerfile .
+# $ docker run -it --name=mapdevel -v $(pwd):/home/map2check/devel_tool/mygitclone:Z --user $(id -u):$(id -g) herberthb/mapdevel /bin/bash
#
# The docker user is "map2check" and the password is "map2check"
# Docker tips:
# You can check that the container still exists by running: $ docker ps -a
# You can restart the container by running: docker start -ai mapdevel
############################################################
-FROM herberthb/base-image-map2check:v2
+FROM herberthb/base-image-map2check:v8
# Metadata indicating an image maintainer.
MAINTAINER
@@ -51,22 +51,15 @@ WORKDIR /home/map2check/devel_tool/
RUN cd /home/map2check/devel_tool/
-RUN wget http://releases.llvm.org/6.0.0/clang+llvm-6.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz
-RUN tar xf clang+llvm-6.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz
-RUN mv clang+llvm-6.0.0-x86_64-linux-gnu-ubuntu-16.04 clang600
-RUN rm clang+llvm-6.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz
-
RUN sudo chown -R map2check:map2check .
VOLUME /home/map2check/devel_tool/
+
# Revoke password-less sudo and Set up sudo access for the ``map2check`` user so it
# requires a password
USER root
RUN mv /etc/sudoers.bak /etc/sudoers && \
echo 'map2check ALL=(root) ALL' >> /etc/sudoers
USER map2check
-# Configure git
-RUN git config --global user.email "map2check.tool@gmail.com"
-RUN git config --global user.name "Map2Check"
##################### INSTALLATION END #####################
diff --git a/README.md b/README.md
index a5c03f655..ed1dfd7d8 100644
--- a/README.md
+++ b/README.md
@@ -12,7 +12,7 @@ ___
Map2Check is a bug hunting tool that automatically generating and checking safety properties in C programs.
It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety.
The generation of the tests cases are based on assertions (safety properties) from the code instructions, adopting the
-[LLVM framework](http://llvm.org/) version 6.0, [LibFuzzer](https://llvm.org/docs/LibFuzzer.html), [KLEE](https://klee.github.io/) to generate input values to the test cases generated by Map2Check. Additionally, we have adopted [Crab-LLVM](https://github.com/seahorn/crab-llvm) tool to computes inductive invariants for LLVM-based languages.
+[LLVM framework](http://llvm.org/) version 8.0, [LibFuzzer](https://llvm.org/docs/LibFuzzer.html), [KLEE](https://klee.github.io/) to generate input values to the test cases generated by Map2Check. Additionally, we have adopted [Crab-LLVM](https://github.com/seahorn/crab-llvm) tool to computes inductive invariants for LLVM-based languages.
Extra documentation is available at https://map2check.github.io
@@ -23,7 +23,7 @@ ___
To use the Map2Check tool is necessary a Linux 64-bit OS system. In the linux OS, you should install the requirements, typing the commands:
``` bash
-$ sudo apt install python-minimal
+$ sudo apt install python2-minimal
$ sudo apt install libc6-dev
```
@@ -37,8 +37,8 @@ After that, you should type the following command:
``` bash
-$ unzip map2check-rc-v7.3-svcomp20.zip
-$ cd map2check-rc-v7.3-svcomp20
+$ unzip map2check-rc-v8.zip
+$ cd map2check-rc-v8-svcomp20
```
#### Running the tool
@@ -49,7 +49,7 @@ in the installation directory as follows:
``` bash
-$ ./map2check --memtrack svcomp_960521-1_false-valid-free.c
+$ ./map2check --memtrack code.c
```
In this case, --memtrack is the option to check for memory errors. For help and others tool options:
@@ -71,8 +71,8 @@ $ git clone https://github.com/hbgit/Map2Check.git
$ cd Map2Check
$ git submodule update --init --recursive
# Build docker image to compile Map2Check
-$ docker build -t hrocha/mapdevel --no-cache -f Dockerfile .
-$ docker run --rm -v $(pwd):/home/map2check/devel_tool/mygitclone:Z --user $(id -u):$(id -g) hrocha/mapdevel /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./make-release.sh; ./make-unit-test.sh"
+$ docker build -t herberthb/mapdevel --no-cache -f Dockerfile .
+$ docker run --rm -v $(pwd):/home/map2check/devel_tool/mygitclone:Z --user $(id -u):$(id -g) herberthb/mapdevel /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./make-release.sh;"
```
More details at https://map2check.github.io/docker.html
diff --git a/cmake/CMakeLists.txt.googletest b/cmake/CMakeLists.txt.googletest
index c6247af53..649e0a52e 100644
--- a/cmake/CMakeLists.txt.googletest
+++ b/cmake/CMakeLists.txt.googletest
@@ -1,11 +1,11 @@
-cmake_minimum_required(VERSION 2.8.2)
+cmake_minimum_required(VERSION 3.1.1)
project(googletest-download NONE)
include(ExternalProject)
ExternalProject_Add(googletest
GIT_REPOSITORY https://github.com/google/googletest.git
- GIT_TAG master
+ GIT_TAG release-1.10.0
SOURCE_DIR "${CMAKE_CURRENT_BINARY_DIR}/googletest-src"
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/googletest-build"
CONFIGURE_COMMAND ""
diff --git a/compile_commands.json b/compile_commands.json
new file mode 100644
index 000000000..866da1984
--- /dev/null
+++ b/compile_commands.json
@@ -0,0 +1,127 @@
+[
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DTrackBasicBlockPass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/TrackBasicBlockPass.dir/TrackBasicBlockPass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/TrackBasicBlockPass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/TrackBasicBlockPass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DMap2CheckLibrary_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/Map2CheckLibrary.dir/Map2CheckLibrary.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/Map2CheckLibrary.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/Map2CheckLibrary.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DOverflowPass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/OverflowPass.dir/OverflowPass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/OverflowPass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/OverflowPass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DMemoryTrackPass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/MemoryTrackPass.dir/MemoryTrackPass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/MemoryTrackPass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/MemoryTrackPass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DTargetPass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/TargetPass.dir/TargetPass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/TargetPass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/TargetPass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/DebugInfo.dir/DebugInfo.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/DebugInfo.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/DebugInfo.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DNonDetPass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/NonDetPass.dir/NonDetPass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/NonDetPass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/NonDetPass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DGenerateAutomataTruePass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/GenerateAutomataTruePass.dir/GenerateAutomataTruePass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/GenerateAutomataTruePass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/GenerateAutomataTruePass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DAssertPass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/AssertPass.dir/AssertPass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/AssertPass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/AssertPass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DLoopPredAssumePass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/LoopPredAssumePass.dir/LoopPredAssumePass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/LoopPredAssumePass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/LoopPredAssumePass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -DCheckNonDetFunctPass_EXPORTS -I../ -fPIC -I/usr/lib/llvm-8/include -std=c++11 -fno-exceptions -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -fno-rtti -std=gnu++11 -o modules/backend/pass/CMakeFiles/CheckNonDetFunctPass.dir/CheckNonDetFunctPass.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/CheckNonDetFunctPass.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/backend/pass/CheckNonDetFunctPass.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -std=gnu++11 -o modules/frontend/CMakeFiles/map2check.dir/map2check.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/map2check.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/map2check.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -std=gnu++11 -o modules/frontend/CMakeFiles/Caller.dir/caller.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/caller.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/caller.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -std=gnu++11 -o modules/frontend/utils/CMakeFiles/Tools.dir/tools.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/utils/tools.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/utils/tools.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -std=gnu++11 -o modules/frontend/utils/CMakeFiles/Log.dir/log.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/utils/log.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/utils/log.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -std=gnu++11 -o modules/frontend/utils/CMakeFiles/GenCryptoHash.dir/gen_crypto_hash.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/utils/gen_crypto_hash.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/utils/gen_crypto_hash.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -std=gnu++11 -o modules/frontend/counter_example/CMakeFiles/CounterExample.dir/counter_example.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/counter_example/counter_example.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/counter_example/counter_example.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -std=gnu++11 -o modules/frontend/witness/CMakeFiles/Edge.dir/edge.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/witness/edge.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/witness/edge.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -std=gnu++11 -o modules/frontend/witness/CMakeFiles/Witness.dir/witness.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/witness/witness.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/witness/witness.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -std=gnu++11 -o modules/frontend/witness/CMakeFiles/Graph.dir/graph.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/witness/graph.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/witness/graph.cpp"
+},
+
+{
+ "directory": "/home/hrocha/Documents/Projects/Map2Check/build",
+ "command": "/usr/lib/llvm-8/bin/clang++ -I../ -I/usr/lib/llvm-8/include -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -std=gnu++11 -o modules/frontend/witness/CMakeFiles/Node.dir/node.cpp.o -c /home/hrocha/Documents/Projects/Map2Check/modules/frontend/witness/node.cpp",
+ "file": "/home/hrocha/Documents/Projects/Map2Check/modules/frontend/witness/node.cpp"
+}
+]
\ No newline at end of file
diff --git a/make-regression-test.sh b/make-regression-test.sh
index fd4b9aca6..acf6284f4 100755
--- a/make-regression-test.sh
+++ b/make-regression-test.sh
@@ -54,7 +54,7 @@ echo "Adopting: $xml_doc_benchexec_name"
# Check if docker image is already build
# 1 - Build docker image available at https://github.com/hbgit/benchexecrun
-has_docker_img=`docker images | grep -c "hrocha/benchexecrun"`
+has_docker_img=`docker images | grep -c "herberthb/benchexecrun"`
if [ $has_docker_img -gt 0 ]; then
echo "Found benchexec image to run tests ..."
is_main_dir=`ls | grep -c "make-regression-test.sh"`
@@ -62,11 +62,11 @@ if [ $has_docker_img -gt 0 ]; then
if [ $is_main_dir -gt 0 ]; then
if [ $travis_flag -eq 0 ]; then
time docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw \
- -v $(pwd):/home/bench/benchexec_files:Z hrocha/benchexecrun \
+ -v $(pwd):/home/bench/benchexec_files:Z herberthb/benchexecrun \
/bin/bash -c "cd release; python3 -m benchexec.benchexec --no-container ../$xml_doc_benchexec_name"
else
time docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw \
- -v $(pwd):/home/bench/benchexec_files:Z hrocha/benchexecrun \
+ -v $(pwd):/home/bench/benchexec_files:Z herberthb/benchexecrun \
/bin/bash -c "cd release; python3 -m benchexec.benchexec --no-container ../tests/regression_test/xml_doc_benchexec/$xml_doc_benchexec_name"
fi
@@ -74,8 +74,10 @@ if [ $has_docker_img -gt 0 ]; then
# Analyzing the results
get_last_file_result=`ls -t release/results/*.txt | head -1`
get_total_test_cases=`tail -n 10 $get_last_file_result | grep -oEi "Statistics:(.[^Files]*)" | grep -oe "[0-9]*"`
- get_total_success=`tail -n 10 $get_last_file_result | grep -oEi "Score:(.[^(]*)" | grep -oe "[0-9]*"`
- percent_tests=$(( ($get_total_success*100)/$get_total_test_cases ))
+ get_total_success=`tail -n 8 $get_last_file_result | grep -oEi "correct: (.[^a-z]*)" | grep -oe "[0-9]*"`
+
+ percent_tests=$((($get_total_success*100)/$get_total_test_cases))
+ #percent_tests=10
if [ $travis_flag -eq 0 ]; then
if [ $percent_tests -lt 20 ]; then
diff --git a/make-release.sh b/make-release.sh
index 32f9ba138..90e04d988 100755
--- a/make-release.sh
+++ b/make-release.sh
@@ -1,6 +1,5 @@
#!/bin/sh
-export LLVM_DIR_BASE=/llvm/release/llvm600
-export LLVM_VERSION=6.0.0
+export LLVM_VERSION=8.0.0
export_svcomp=true
@@ -18,29 +17,21 @@ echo ""
cd build
-export LLVM_DIR=$LLVM_DIR_BASE/lib/cmake/llvm
-export CXX=$LLVM_DIR_BASE/bin/clang++
-export CC=$LLVM_DIR_BASE/bin/clang
-cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON -DCMAKE_INSTALL_PREFIX=../release/
+export LLVM_DIR=/usr/lib/llvm-8/lib/cmake/llvm/
+export CXX=/usr/bin/clang++-8
+export CC=/usr/bin/clang-8
+cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DCMAKE_INSTALL_PREFIX=../release/
ninja
ninja install
-if [ ! -d "/home/map2check/devel_tool/clang600" ]; then
- CURRENT_DIR=`pwd`
- cd /home/map2check/devel_tool/
- wget http://releases.llvm.org/6.0.0/clang+llvm-6.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz
- tar xf clang+llvm-6.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz
- mv clang+llvm-6.0.0-x86_64-linux-gnu-ubuntu-16.04 clang600
- rm clang+llvm-6.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz
- cd $CURRENT_DIR
-fi
-
cd ../release
mkdir -p ./include
-cp -r /home/map2check/devel_tool/clang600/lib/clang/$LLVM_VERSION/include/* ./include
-cp -r /home/map2check/devel_tool/clang600/lib/clang ./lib
+
+cp -r /usr/include/clang/8/include/* ./include
+mkdir -p ./lib/clang
+cp -r /usr/lib/llvm-8/lib/clang/8.0.1 ./lib/clang/
# Copying external libraries and binaries
cp /usr/bin/ld ./bin
@@ -57,11 +48,17 @@ cp /usr/lib/gcc/x86_64-linux-gnu/5/crt* ./lib/
cp /usr/lib/x86_64-linux-gnu/crt* ./lib
cp /lib/x86_64-linux-gnu/librt.so.1 ./lib/librt.so
cp /usr/lib/x86_64-linux-gnu/libgomp.so.1 ./lib/
+cp /lib/x86_64-linux-gnu/ld-2.27.so ./lib/
+
+# Supporting LLVM 8
+cp /usr/lib/x86_64-linux-gnu/libLLVM-8.so.1 ./lib/
+cp /usr/lib/x86_64-linux-gnu/libffi.so.6.0.4 ./lib/libffi.so.6
+cp /lib/x86_64-linux-gnu/libtinfo.so.5.9 ./lib/libtinfo.so.5
echo ""
echo "Copying external tools"
# LibFuzzer
-cp /deps/install/fuzzer/libFuzzer.a ./lib
+cp /usr/lib/llvm-8/lib/libFuzzer.a ./lib
# Z3
if [ ! -d "./z3" ]; then
@@ -70,7 +67,10 @@ if [ ! -d "./z3" ]; then
fi
# Klee and klee_uclib
-cp -r /deps/install/klee/* .
+cp -r /deps/install/klee/bin/* ./bin/
+cp -r /deps/install/klee/include/* ./include/
+cp -r /deps/install/klee/lib/* ./lib/
+
# metasmt
echo "> Copying metaSMT deps ..."
@@ -82,63 +82,49 @@ cp -r /deps/src/metaSMT/deps/lingeling-ayv-86bf266-140429/lib/liblingeling.so li
cp -r /deps/src/metaSMT/deps/yices-2.5.1/lib/libyices.so.2.5.1 lib/
cp -r /deps/src/metaSMT/deps/yices-2.5.1/lib/libyices.so.2.5 lib/
cp -r /deps/src/metaSMT/deps/yices-2.5.1/lib/libyices.so lib/
+# minisat
cp -r /deps/src/metaSMT/deps/minisat-git/lib/libminisat.a lib/
cp -r /deps/src/metaSMT/deps/minisat-git/lib/libminisat.so lib/
cp -r /deps/src/metaSMT/deps/minisat-git/lib/libminisat.so.2 lib/
cp -r /deps/src/metaSMT/deps/minisat-git/lib/libminisat.so.2.1.0 lib/
-# minisat
-# stp
-
# Crab
if [ ! -d "./bin/crabllvm" ]; then
- cp -r /deps/install/crab ./bin
+ cp -r /deps/install/crab ./bin/
mv ./bin/crab ./bin/crabllvm
fi
echo "> Crab-LLVM replacing PATH"
-sed -i '54s/\"PATH\"/\"CLANG_PATH\"/' ./bin/crabllvm/bin/crabllvm.py
+sed -i '54s/\"PATH\"/\"CLANG_PATH\"/' ./bin/crabllvm/bin/clam.py
cp /usr/lib/x86_64-linux-gnu/libbfd-* ./bin/crabllvm/lib/
cp /usr/lib/x86_64-linux-gnu/libgomp.so.1 ./bin/crabllvm/lib/
cp /usr/lib/x86_64-linux-gnu/libstdc++* ./bin/crabllvm/lib/
-cp ./lib/libz3.so ./bin/crabllvm/lib/
+# cp ./lib/libz3.so ./bin/crabllvm/lib/
+
../utils/cp_utils_file.sh
-# #echo ""
+
if [ "$export_svcomp" = true ] ; then
echo ""
echo "Cleaning for SVCOMP"
rm -rf ./z3/include
- rm -rf ./z3/lib/python2.7
+ #rm -rf ./z3/lib/python2.7
rm -rf ./z3/lib
- rm -rf ./lib/python2.7
- rm -rf ./lib/clang/6.0.0/include
+ #rm -rf ./lib/python2.7
+ #rm -rf ./lib/clang/6.0.0/include
rm -rf ./moduleBenchExec
rm ./bin/kleaver
rm -rf ./bin/crabllvm/ldd
- rm ./bin/crabllvm/lib/libz3.so
- #ln -s ./z3/lib/libz3.so ./bin/crabllvm/lib/libz3.so
+ rm ./bin/crabllvm/lib/libz3.so
cd bin/crabllvm/lib/
ln -s ../../../lib/libz3.so .
- cd ../../../ # go back to release
- #rm ./lib/libz3.so
+ cd ../../../ # go back to release
fi
-#echo ""
-#echo "Generating archive ..."
-#if [ ! -d "map2check" ]; then
-# mkdir map2check
-#else
- #rm -rf map2check
- #mkdir map2check
-#fi
-#cp -r release/* map2check/
-#7z a map2check.zip map2check
-#rm -rf map2check
-#echo ""
+
echo ""
diff --git a/make-unit-test.sh b/make-unit-test.sh
index ca7064484..c851c5f14 100755
--- a/make-unit-test.sh
+++ b/make-unit-test.sh
@@ -1,6 +1,5 @@
#!/bin/sh
-export LLVM_DIR_BASE=/llvm/release/llvm600
-export LLVM_VERSION=6.0.0
+export LLVM_VERSION=8.0.0
if [ ! -d "build" ]; then
mkdir build
fi
@@ -13,9 +12,9 @@ echo ""
cd build
-export LLVM_DIR=$LLVM_DIR_BASE/lib/cmake/llvm
-export CXX=$LLVM_DIR_BASE/bin/clang++
-export CC=$LLVM_DIR_BASE/bin/clang
-cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON
+export LLVM_DIR=/usr/lib/llvm-8/lib/cmake/llvm/
+export CXX=/usr/bin/clang++-8
+export CC=/usr/bin/clang-8
+cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DENABLE_TEST=ON
ninja && ninja install && ctest
diff --git a/modules/backend/library/lib/NonDetGeneratorLibFuzzy.c b/modules/backend/library/lib/NonDetGeneratorLibFuzzy.c
index f4d9fdd97..7368417f0 100644
--- a/modules/backend/library/lib/NonDetGeneratorLibFuzzy.c
+++ b/modules/backend/library/lib/NonDetGeneratorLibFuzzy.c
@@ -34,7 +34,7 @@ void nondet_init() { nondet_log_init(); }
void nondet_destroy() { nondet_log_destroy(); }
-void nondet_cancel() { pthread_exit(NULL); }
+void nondet_cancel() { pthread_exit(NULL); } // TODO: checkout that
void nondet_assume(int expr) {
if (!expr) {
@@ -63,6 +63,7 @@ uint8_t get_next_input_from_fuzzer() {
int LLVMFuzzerTestOneInput(const uint8_t *Data, size_t Size) {
map2check_fuzzer_data = Data;
map2check_fuzzer_size = Size;
+
int prevType;
// int currentProccess = getpid();
// printf("Creating %d\n", currentProccess);
diff --git a/modules/backend/pass/CMakeLists.txt b/modules/backend/pass/CMakeLists.txt
index d96789e65..eadc63d2b 100755
--- a/modules/backend/pass/CMakeLists.txt
+++ b/modules/backend/pass/CMakeLists.txt
@@ -15,6 +15,8 @@ list(APPEND MAP2CHECK_PASS_LIB "GenerateAutomataTruePass")
list(APPEND MAP2CHECK_PASS_LIB "AssertPass")
list(APPEND MAP2CHECK_PASS_LIB "OverflowPass")
list(APPEND MAP2CHECK_PASS_LIB "LoopPredAssumePass")
+list(APPEND MAP2CHECK_PASS_LIB "CheckNonDetFunctPass")
+list(APPEND MAP2CHECK_PASS_LIB "InitVar2NonDetFunctPass")
diff --git a/modules/backend/pass/CheckNonDetFunctPass.cpp b/modules/backend/pass/CheckNonDetFunctPass.cpp
new file mode 100644
index 000000000..499dd66e6
--- /dev/null
+++ b/modules/backend/pass/CheckNonDetFunctPass.cpp
@@ -0,0 +1,41 @@
+/**
+ * Copyright (C) 2014 - 2020 Map2Check tool
+ * This file is part of the Map2Check tool, and is made available under
+ * the terms of the GNU General Public License version 2.
+ *
+ * LLVM -> NCSA
+ *
+ * SPDX-License-Identifier: (GPL-2.0 AND NCSA)
+ **/
+
+#include "CheckNonDetFunctPass.hpp"
+
+#include
+
+using llvm::dyn_cast;
+using llvm::RegisterPass;
+using llvm::errs;
+
+
+bool CheckNonDetFunctPass::runOnFunction(Function& F) {
+ // run on each basic block
+ for (auto &BB : F) {
+ // run on each instruction from the basic block
+ for (auto &I : BB) {
+ if (CallInst *callInst = dyn_cast(&I)) {
+ if (Function *calledFunct = callInst->getCalledFunction()) {
+ if (calledFunct->getName().startswith("__VERIFIER_nondet")) {
+ errs() << calledFunct->getName() << "\n";
+ }
+ }
+ }
+ }
+ }
+ // The IR was not modified
+ return false;
+}
+
+
+char CheckNonDetFunctPass::ID = 14;
+static RegisterPass X("check_nondet_functs",
+ "Identify nondet function using __VERIFIER_nondet_type() call");
diff --git a/modules/backend/pass/CheckNonDetFunctPass.hpp b/modules/backend/pass/CheckNonDetFunctPass.hpp
new file mode 100644
index 000000000..814ae7b64
--- /dev/null
+++ b/modules/backend/pass/CheckNonDetFunctPass.hpp
@@ -0,0 +1,43 @@
+/**
+ * Copyright (C) 2014 - 2020 Map2Check tool
+ * This file is part of the Map2Check tool, and is made available under
+ * the terms of the GNU General Public License version 2.
+ *
+ * LLVM -> NCSA
+ *
+ * SPDX-License-Identifier: (GPL-2.0 AND NCSA)
+ **/
+
+#ifndef MODULES_BACKEND_PASS_CHECKNONDETFUNCTPASS_HPP_
+
+
+#define MODULES_BACKEND_PASS_CHECKNONDETFUNCTPASS_HPP_
+
+
+#include
+#include
+#include
+#include
+#include
+
+#include
+#include