bulwahn · OzanAlpay · Jul 6, 2018 · Jul 4, 2018 · Jul 4, 2018 · Jul 4, 2018
diff --git a/Documentation/InferAnalyseScriptManual.md b/Documentation/InferAnalyseScriptManual.md
@@ -0,0 +1,79 @@
+## Infer Analyse Script ##
+In this document you can find how to use [analyse-kernel.sh](../scripts/analyse-kernel.sh), in order to run different infer versions(0.13.1, 0.14.0, 0.15.0) on various kernel versions(v4.15, v4.16) with using kernel-configurations(defconfig, maximalyesconfig)  
+
+## Test System Configuration ##
+**Operating-System:** Ubuntu 16.04.4 LTS 64-bit  
+**Docker-Version:** Docker version 18.03.0-ce, build 0520e24
+### Prerequirements ###
+To be able to run ```analyse-kernel.sh``` on your system successfully, please follow these steps:
+- Clone this repo  
+- Install Docker [Tutorial](https://www.digitalocean.com/community/tutorials/how-to-install-and-use-docker-on-ubuntu-16-04)  
+- Complete Setup instructions [Setup](Setup.md)  
+- Build Dockerfiles that required for Infer run: ```cd scripts && build-infer-docker.sh```  
+
+Now you are ready to use ```analyse-kernel.sh```, to understand how to use it and parameter explanations please follow next section.  
+
+
+## Analyse-Kernel.sh Parameters ##
+### Mandatory Parameters ###
+**Kernel Repository Parameter ( -r ):**  
+Possible values are torvalds, stable and next.  
+Example:  
+```./analyse-kernel.sh -r stable```  
+
+**Kernel Configuration Parameter ( -c ):**   
+You can either pass a string or a file path for this parameter  
+We already prepared a maximalyesconfig for Linux-Kernel v4.16 that compiles with clang  
+You can find it in ```/scripts/files/v416/maximalyesconfig```  
+Examples:  
+```./analyse-kernel.sh -c defconfig```  
+```./analyse-kernel.sh -c files/v416/maximalyesconfig```  
+
+### Optional Parameters ###
+
+**Compiler Parameter ( -cc ):**  
+You can pass compiler parameter that will be used for infer capture and infer analyze phases:  
+Possible values:  
+Default value: ```clang```  
+Example:  
+```./analyse-kernel.sh -cc clang-6.0```  
+
+! Be sure that your selected compiler is included in Dockerfile, You may need to modify and build your dockerfiles again, if you select a currently unsupported parameter !  
+
+**Infer Version Parameter (-infer-version):**  
+You can select an infer version, in order to use it for infer capture an infer analyze phases:  
+Possible values: 0.13.1, 0.14.0, 0.15.0  
+Default value: 0.14.0  
+Example:  
+```./analyse-kernel.sh -infer-version 0.15.0```  
+
+**Inferconfig File Path Parameter (-i):**  
+Since there are some problems about running Infer on Linux-Kernel, we need different inferconfig files to avoid crashes.  
+We also prepared some inferconfig files according to infer-version and kernel-configuration.  
+You can find them in ```scripts/files/{infer-version-number}```  
+Default value: -  
+Examples:  
+```./analyse-kernel.sh -i files/infer0131/inferconfig```  
+```./analyse-kernel.sh -i files/infer0150/infermaximalyesconfig```  
+
+**Analysis File Configuration (--analysisconfig):**  
+Instead of passing this parameters from command-line, you can provide a custom ```analysisconfig``` as a parameter, and ```./analyse-kernel.sh``` will read that file and set parameters according to file content.  
+You can find an example analysisconfig at ```scripts/files/analysisconfig```  
+!This method is not tested very well, so there may some problems if you use an analysisconfig!  
+Default value: -  
+Example:  
+```./analyse-kernel.sh --analysisconfig files/analysisconfig```  
+
+**Dont Run Analyze Parameter (--no-analyze):**  
+Infer Analyze needs a lot of time and computing power. If you don't want to run infer analyze after infer capture finishes, you can call this script with passing --no-analyze as an parameter  
+Dfeault value: -  
+Example:  
+```./analyse-kernel.sh --no-analyze```  
+
+## Notes ##
+To understand why we blacklisted some files or want to know how to build infer from source etc, please see:[Infer-On-Linux-Kernel-Documentation](InferOnLinuxKernel.md)  
+
+
+
+
+
diff --git a/Documentation/InferOnLinuxKernel.md b/Documentation/InferOnLinuxKernel.md
@@ -0,0 +1,139 @@
+# Installing Infer #
+We need to compile and install infer from source code , in order to be able to hack it later. 
+You can find facebook/infer's source code [here](https://github.com/facebook/infer) or you can use following command: 
+```git clone https://github.com/facebook/infer.git```
+## My current setup ##
+**Host OS:** Ubuntu 64-bit 16.04  
+**Kernel Version To Be Checked with Infer:** Linux 4.15 Stable  
+**Kernel Compilation Configuration:** defconfig  
+**Infer fork with HEAD commit:** 4799fb6b8226("[racerd] skeleton for testing access path stability")  
+**Clang:** clang version 3.8.0-2ubuntu4 (tags/RELEASE_380/final)  
+
+## Prerequisites ##
+You can find latest prerequisites for your operating system for building infer [here](https://github.com/facebook/infer/blob/master/INSTALL.md).
+
+## Dependency Problems I have encountered during Compilation ##
+Even though I have installed this prerequisites, I had some problems with:
+- sqlite3.4.3.2 ```opam depext sqlite3.4.3.2```
+- camlzip.1.0.7 ```opam depext camlzip.1.07```
+- cmake ```sudo apt-get install cmake```
+
+## Compile Infer ##
+After cloning infer to your computer, and installing all required files. You can start compiling with infer with ```./build_infer.sh``` command.
+
+## Install Infer ##
+After infer build finished, you can install it with using ```make install``` command. Now you are able to run infer from your command line.
+
+## Packages Needed to build Linux Kernel ##
+You need some extra packages, to become able to compile linux 4.15 from source code. In my case they were:  
+- libelf-dev ```sudo apt-get install libelf-dev```  
+- libssl-dev ```sudo apt-get install libssl-dev```
+
+## Prepare to Run Infer on Linux Kernel ##
+
+Now you can :
+- Compile Linux 4.15 without getting any errors
+- Call infer via command line
+
+To use infer with linux-kernel, first you must capture Linux 4.15 source code with ```infer capture -- make``` command , and then analyse infer-out folder with ```infer analyse```. However with current setup Infer can't capture Linux 4.15 source code. To be able to get an output you need to make some modifications. I explained required modifications below, with two solutions for each of them.
+
+## Modify Infer to mark problematic directories blacklisted ##
+First of all, we need to mark some linux directories as blacklisted, to avoid compilation errors during ```infer capture``` phase.
+To do this you have two options and I prefer second option.
+
+### Modify Infer source code ###
+You can directly modify your infer fork, and mark directories as blacklisted with help of [patch](../scripts/files/0001-Blacklist-files-from-infer-source-code.patch), please don't forget to modify file paths which passed as parameter before applying it.
+
+### Add an inferconfig file ###
+
+Thanks to [@Evan Zhao](https://github.com/Tacinight) we have much simplier and flexible way to solve this problem. You can create an ```.inferconfig``` file in linux-kernel root directory and then mark problematics directories as blacklisted as following: (Please do not forget replace file paths with absolute paths.)
+You can do it via execute ```echo $PWD``` in linux-stable root directory. Then delete first ``` \ ``` and replace ```[linux-stable-absolute-path]```'s with rest of string.
+Example :  
+```"home/ozan/linux-stable/stable/linux-stable/mm"```  
+
+```
+{
+"skip-analysis-in-path": 
+[
+"[linux-stable-absolute-path]/arch/x86/entry/vdso",
+"[linux-stable-absolute-path]/arch/x86/kernel", 
+"[linux-stable-absolute-path]/arch/x86/mm", 
+"[linux-stable-absolute-path]/arch/x86/boot", 
+"[linux-stable-absolute-path]/drivers/acpi", 
+"[linux-stable-absolute-path]/fs", 
+"[linux-stable-absolute-path]/kernel/bpf", 
+"[linux-stable-absolute-path]/mm", 
+"[linux-stable-absolute-path]/net/mac80211"
+]
+}
+```
+You can find why you should these files into the blacklist; and if you dont them, add what kind of error they create at : [Blacklisted-Files-Explanations](../infer/Documentation/BlacklistExplanation) folder.
+
+
+## Set default CC to clang for linux-kernel compilation ##
+
+After that, we need to set clang as a default compiler when we start infer capture phase with ```infer capture -- make``` command.  Otherwise Linux Makefiles uses gcc flags, and since infer compiles with clang, we need clang compiler flags for a successfull compilation.
+For this issue again we have two different solutions, and I prefer second one.
+
+### GCC Hack ###
+It is a serious hack, which may breaks your other builds. Basically we just point ```gcc``` command to clang compiler. If you want to use this method I strongly encourage you to take a backup.
+
+- Open terminal
+- ```cd /usr/bin```
+- ```sudo ln -sf clang gcc```
+
+### Patch file for Linux ###
+
+Another way is applying [this patch](../scripts/files/0001-Set-default-CC-to-Clang-from-Makefile.patch), to top of linux 4.15. After that you won't have any problems about compiler flags.
+
+## Run Infer on Linux Kernel ##
+
+After all this configurations, you are ready to compile linux kernel with infer:
+
+- Go to Linux-kernel root directory.
+- ```make clean && make defconfig```
+- ```infer capture -- make```
+After ```infer capture -- make``` completed you can observe infer creates a directory named infer-out. So now we should execute```infer analyze``` command and get output from infer-out folder. But it may take a lot of time and need huge computing power.
+- Again from linux-kernel root directory,
+- Execute ```infer analyze```
+- Look for results with ```cat /infer-out/bugs.txt```
+## Common problems ##
+
+### Base_64.S problem ###
+after executing ```infer capture -- make``` command if you get error messages as:
+``` <instantiation>:4:8: error: expected absolute expression
+ .skip -(((144f-143f)-(141b-140b)) > 0) * ((144f-143f)-(141b-140b)),0x90
+       ^
+<instantiation>:4:8: error: expected absolute expression
+ .skip -(((144f-143f)-(141b-140b)) > 0) * ((144f-143f)-(141b-140b)),0x90
+       ^
+<instantiation>:4:8: error: expected absolute expression
+ .skip -(((144f-143f)-(141b-140b)) > 0) * ((144f-143f)-(141b-140b)),0x90
+       ^
+```
+during compilation of base64.S file, that means linux makefile still using wrong flags during compilation, I suggest you to look at **Set default CC to clang for linux-kernel compilation** section again. To avoid that kind of errors, Makefiles adds different compiler flags according to selected compiler. For example in this case we need -no-integrated-as flag to avoid using clang's integrated assembler.
+### objcopy: 'arch/x86/entry/vdso/vdso64.so.dbg': No such file problem ###
+If you get  
+```
+arch/x86/entry/vdso/vclock_gettime.o: In function `__vdso_time':
+vclock_gettime.c:(.text+0x667): undefined reference to `memcpy'
+arch/x86/entry/vdso/vclock_gettime.o: In function `gtod_read_begin':
+vclock_gettime.c:(.text+0x734): undefined reference to `memcpy'
+Error: the following clang command did not run successfully:
+```  
+error during ```infer capture``` phase, you should re-do mark problematic directories blacklisted step. Maybe you can check if your directory paths are written correctly. Please not that directories shouldn't start with ``` \ ```  
+**Invalid:**  
+```"/home/ozan/linux-stable/stable/linux-stable/mm"```    
+**Valid:**  
+```"home/ozan/linux-stable/stable/linux-stable/mm"```  
+
+
+## Using Docker for Kernel-Analysis with Infer ##
+
+You can do all this process , with using Docker. It is the most basic and straightforward way to run infer on Linux Kernel.
+To do this, please follow the instructions below.
+- Clone repository ```git clone https://github.com/bulwahn/linux-kernel-analysis.git```
+- Follow [Setup](Setup.md) instructions, clone at least linux-stable to your computer and be sure that you set```KERNEL_SRC_BASE```
+- Go to scripts directory ```cd ~/linux-kernel-analysis/scripts```
+- Run ```./build_infer_docker.sh``` and build docker file.
+- Run ```./analyse_kernel.sh```, That script completes all required steps that described above, then will run ```infer capture -- make``` on linux-kernel. You can call it with various parameters. Please see detailed instructions about ```analyse_kernel.sh``` script at (manual-for-infer-analyse-script)[InferAnalyseScriptManual.md]
diff --git a/docker/infer-0.13.1/Dockerfile b/docker/infer-0.13.1/Dockerfile
@@ -0,0 +1,51 @@
+FROM debian:stretch-slim
+
+LABEL maintainer "Ozan Alpay <ozanalpay@yandex.com.tr>"
+
+# mkdir the man/man1 directory due to Debian bug #863199
+RUN apt-get update && \
+    mkdir -p /usr/share/man/man1 && \
+    apt-get install --yes --no-install-recommends \
+      autoconf \
+      automake \
+      bc \
+      bison \
+      bsdmainutils \
+      ca-certificates \
+      cmake \
+      clang \
+      curl \
+      flex \
+      git \
+      gnupg \
+      libc6-dev \
+      libelf-dev \
+      libsqlite3-dev \
+      libssl-dev \
+      make \
+      opam \
+      pkg-config \
+      python2.7 \
+      wget \
+      zlib1g-dev && \
+    rm -rf /var/lib/apt/lists/*
+
+# Download the latest Infer release
+RUN INFER_VERSION=v0.13.1; \
+    cd /opt && \
+    curl -sL \
+      https://github.com/facebook/infer/releases/download/${INFER_VERSION}/infer-linux64-${INFER_VERSION}.tar.xz | \
+    tar xJ && \
+    rm -f /infer && \
+    ln -s ${PWD}/infer-linux64-$INFER_VERSION /infer && \
+	ln -s ${PWD}/infer-linux64-$INFER_VERSION/infer/bin/infer /usr/local/bin/infer
+
+# Compile Infer
+RUN OCAML_VERSION=4.05.0+flambda; \
+    cd /infer && ./build-infer.sh clang --opam-switch $OCAML_VERSION && rm -rf /root/.opam
+
+# Install Infer
+ENV INFER_HOME /infer/infer
+ENV PATH ${INFER_HOME}/bin:${PATH}
+
+
diff --git a/docker/infer-0.14.0/Dockerfile b/docker/infer-0.14.0/Dockerfile
@@ -0,0 +1,48 @@
+FROM debian:stretch-slim
+
+LABEL maintainer "Ozan Alpay <ozanalpay@yandex.com.tr>"
+
+# mkdir the man/man1 directory due to Debian bug #863199
+RUN apt-get update && \
+    mkdir -p /usr/share/man/man1 && \
+    apt-get install --yes --no-install-recommends \
+      autoconf \
+      automake \
+      bc \
+      bison \
+      bsdmainutils \
+      ca-certificates \
+      cmake \
+      clang \
+      curl \
+      flex \
+      git \
+      gnupg \
+      libc6-dev \
+      libelf-dev \
+      libsqlite3-dev \
+      libssl-dev \
+      make \
+      opam \
+      pkg-config \
+      python2.7 \
+      wget \
+      zlib1g-dev && \
+    rm -rf /var/lib/apt/lists/*
+# Download the latest Infer release
+RUN INFER_VERSION=v0.14.0; \
+    cd /opt && \
+    curl -sL \
+      https://github.com/facebook/infer/releases/download/${INFER_VERSION}/infer-linux64-${INFER_VERSION}.tar.xz | \
+    tar xJ && \
+    rm -f /infer && \
+    ln -s ${PWD}/infer-linux64-$INFER_VERSION /infer && \
+	ln -s ${PWD}/infer-linux64-$INFER_VERSION/infer/bin/infer /usr/local/bin/infer
+
+# Compile Infer
+RUN OCAML_VERSION=4.06.1+flambda; \
+    cd /infer && ./build-infer.sh clang --opam-switch $OCAML_VERSION && rm -rf /root/.opam
+
+# Install Infer
+ENV INFER_HOME /infer/infer
+ENV PATH ${INFER_HOME}/bin:${PATH}
diff --git a/docker/infer-0.15.0/Dockerfile b/docker/infer-0.15.0/Dockerfile
@@ -0,0 +1,46 @@
+FROM debian:stretch-slim
+
+LABEL maintainer "Ozan Alpay <ozanalpay@yandex.com.tr>"
+
+# mkdir the man/man1 directory due to Debian bug #863199
+RUN apt-get update && \
+    mkdir -p /usr/share/man/man1 && \
+    apt-get install --yes --no-install-recommends \
+      autoconf \
+      automake \
+      bc \
+      bison \
+      bsdmainutils \
+      ca-certificates \
+      cmake \
+      clang \
+      curl \
+      flex \
+      git \
+      gnupg \
+      libc6-dev \
+      libelf-dev \
+      libsqlite3-dev \
+      libssl-dev \
+      make \
+      opam \
+      pkg-config \
+      python2.7 \
+      wget \
+      zlib1g-dev && \
+rm -rf /var/lib/apt/lists/*
+
+# Download the latest Infer release
+RUN INFER_VERSION=v0.15.0; \
+    cd /opt && \
+    curl -sL \
+      https://github.com/facebook/infer/releases/download/${INFER_VERSION}/infer-linux64-${INFER_VERSION}.tar.xz | \
+    tar xJ && \
+    rm -f /infer && \
+    ln -s ${PWD}/infer-linux64-$INFER_VERSION /infer
+
+
+# Install Infer
+ENV INFER_HOME /infer/infer
+ENV PATH ${INFER_HOME}/bin:${PATH}
+RUN ln -s /infer/bin/infer /usr/local/bin/infer