Add 'testsuite/' from commit '08c392e35ee6a55784bff6ccb077e069f12feda7'

git-subtree-dir: testsuite
git-subtree-mainline: f413377
git-subtree-split: 08c392e

testsuite/.gitignore

@@ -0,0 +1,8 @@
+windows32*
+windows64*
+linux64*
+linux32*
+cgc32*
+bin/*
+*.o
+

testsuite/LICENSE

@@ -0,0 +1,19 @@
+Copyright (c) 2019 Cyberhaven
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

testsuite/README.rst

@@ -0,0 +1,45 @@
+=============
+S2E Testsuite
+=============
+
+This repository contains the S2E testsuite. It has a collection of programs that help test various aspects of the S2E
+engine. They also serve as a reference for various S2E tutorials.
+
+A test is comprised of a program binary and a script that sets up an S2E analysis project, runs it, and then checks that
+the results are as expected.
+
+Please refer to the S2E documentation for details on how to run and extend the testsuite.
+The information below only gives a quick summary.
+
+
+Building and running the testsuite
+==================================
+
+.. code-block:: bash
+
+    # Switch to the root of the S2E environment created with s2e-env init
+    cd $S2EENV
+
+    # List the available tests
+    s2e testsuite list
+
+    # Compile the testsuite and generate projects for all tests.
+    # It is possible to specify individual tests.
+    s2e testsuite generate [test1, test2, ...]
+
+    # Run the testsuite
+    s2e testsuite run
+
+
+Creating tests
+==============
+
+This can be done in a few simple steps:
+
+1. Create a subdirectory named after the test.
+
+2. Create a makefile. It must have an ``all`` target that builds the binaries
+
+3. Create a ``config.yml`` file that describes the tests.
+
+4. Create a ``run-tests.tpl`` script that launches the test project and checks the output after S2E terminates.

testsuite/basic0-singlepath/Makefile

@@ -0,0 +1,46 @@
+# Copyright (c) 2019, Cyberhaven
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+TARGET=basic0-singlepath
+SOURCE=main.c
+
+GCC_LINUX=gcc
+GCC_WINDOWS64=x86_64-w64-mingw32-gcc
+GCC_WINDOWS32=i686-w64-mingw32-gcc
+
+CFLAGS:=$(CFLAGS) -O3 -g -Wall -std=c99
+
+linux64-$(TARGET): $(SOURCE)
+	$(GCC_LINUX) -m64 $(CFLAGS) -o "$@" "$^"
+
+linux32-$(TARGET): $(SOURCE)
+	$(GCC_LINUX) -m32 $(CFLAGS) -o "$@" "$^"
+
+windows64-$(TARGET).exe: $(SOURCE)
+	$(GCC_WINDOWS64) -m64 $(CFLAGS) -o "$@" "$^"
+
+windows32-$(TARGET).exe: $(SOURCE)
+	$(GCC_WINDOWS32) -m32 $(CFLAGS) -o "$@" "$^"
+
+TARGETS=linux64-$(TARGET) linux32-$(TARGET) windows64-$(TARGET).exe windows32-$(TARGET).exe
+
+all: $(TARGETS)
+clean:
+	rm -f $(TARGETS)

testsuite/basic0-singlepath/config.yml

@@ -0,0 +1,7 @@
+test:
+    description: "This is a smoke test that checks that guest images can load and run programs"
+    targets:
+        - windows32-basic0-singlepath.exe
+        - windows64-basic0-singlepath.exe
+        - linux32-basic0-singlepath
+        - linux64-basic0-singlepath

testsuite/basic0-singlepath/main.c

@@ -0,0 +1,27 @@
+// Copyright (c) 2019, Cyberhaven
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy
+// of this software and associated documentation files (the "Software"), to deal
+// in the Software without restriction, including without limitation the rights
+// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// copies of the Software, and to permit persons to whom the Software is
+// furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in all
+// copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+// SOFTWARE.
+
+#include <s2e/s2e.h>
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+    s2e_printf("All good");
+    return 0;
+}

testsuite/basic0-singlepath/run-tests.tpl

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+{% include 'common-run.sh.tpl' %}
+
+s2e run -n {{ project_name }}
+
+grep -q "All good" $S2E_LAST/debug.txt
+
+check_coverage {{project_name}} 100

testsuite/basic1-twopaths/Makefile

@@ -0,0 +1,46 @@
+# Copyright (c) 2019, Cyberhaven
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+TARGET=basic1-twopaths
+SOURCE=main.c
+
+GCC_LINUX=gcc
+GCC_WINDOWS64=x86_64-w64-mingw32-gcc
+GCC_WINDOWS32=i686-w64-mingw32-gcc
+
+CFLAGS:=-O3 -g -Wall -std=c99 $(CFLAGS)
+
+linux64-$(TARGET): $(SOURCE)
+	$(GCC_LINUX) -m64 $(CFLAGS) -o "$@" "$^"
+
+linux32-$(TARGET): $(SOURCE)
+	$(GCC_LINUX) -m32 $(CFLAGS) -o "$@" "$^"
+
+windows64-$(TARGET).exe: $(SOURCE)
+	$(GCC_WINDOWS64) -m64 $(CFLAGS) -o "$@" "$^"
+
+windows32-$(TARGET).exe: $(SOURCE)
+	$(GCC_WINDOWS32) -m32 $(CFLAGS) -o "$@" "$^"
+
+TARGETS=linux64-$(TARGET) linux32-$(TARGET) windows64-$(TARGET).exe windows32-$(TARGET).exe
+
+all: $(TARGETS)
+clean:
+	rm -f $(TARGETS)

testsuite/basic1-twopaths/config.yml

@@ -0,0 +1,14 @@
+test:
+    description: "Checks that basic symbolic execution works by forking two paths"
+
+    target_arguments:
+        - "@@"
+
+    targets:
+        - windows64-basic1-twopaths.exe
+        - windows32-basic1-twopaths.exe
+        - linux32-basic1-twopaths
+        - linux64-basic1-twopaths
+
+    build-options:
+        post-project-generation-script: fix-config.sh

testsuite/basic1-twopaths/fix-config.sh

@@ -0,0 +1,13 @@
+#!/bin/sh
+set -e
+
+echo "Patching s2e-config.lua..."
+
+PROJECT_NAME="$(basename $PROJECT_DIR)"
+
+if echo $PROJECT_NAME | grep -q windows; then
+cat << EOF >> $PROJECT_DIR/s2e-config.lua
+
+add_plugin("LibraryCallMonitor")
+EOF
+fi

testsuite/basic1-twopaths/main.c

@@ -0,0 +1,60 @@
+// Copyright (c) 2019, Cyberhaven
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy
+// of this software and associated documentation files (the "Software"), to deal
+// in the Software without restriction, including without limitation the rights
+// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// copies of the Software, and to permit persons to whom the Software is
+// furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in all
+// copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+// SOFTWARE.
+
+#include <s2e/s2e.h>
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+    int ret = 0;
+    FILE *fp = NULL;
+    int value = 0;
+
+    if (argc != 2) {
+        fprintf(stderr, "Usage: %s input_file\n", argv[0]);
+        ret = 1;
+        goto err;
+    }
+
+    fp = fopen(argv[1], "rb");
+    if (!fp) {
+        fprintf(stderr, "Could not open %s\n", argv[1]);
+        ret = 2;
+        goto err;
+    }
+
+    if (fread(&value, sizeof(value), 1, fp) != 1) {
+        fprintf(stderr, "Could not read value from file\n");
+        ret = 3;
+        goto err;
+    }
+
+    if (value == 1) {
+        s2e_printf("Value is 1\n");
+    } else {
+        s2e_printf("Value is not 1\n");
+    }
+
+err:
+    if (fp) {
+        fclose(fp);
+    }
+
+    return ret;
+}

testsuite/basic1-twopaths/run-tests.tpl

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+{% include 'common-run.sh.tpl' %}
+
+s2e run -n {{ project_name }}
+
+echo === Checking that program forked
+grep -q "Value is 1" $S2E_LAST/debug.txt
+grep -q "Value is not 1" $S2E_LAST/debug.txt
+
+{% if 'windows' in project_name %}
+echo === Checking that LibraryCallMonitor works properly
+grep -q "called ntdll.dll!RtlEnterCriticalSection" $S2E_LAST/debug.txt
+{% endif %}
+
+check_coverage {{project_name}} 60
+
+s2e forkprofile {{ project_name }} > $S2E_LAST/forkprofile.txt
+grep -q -i main.c $S2E_LAST/forkprofile.txt

testsuite/basic2-maze/Makefile

@@ -0,0 +1,46 @@
+# Copyright (c) 2019, Cyberhaven
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+TARGET=basic2-maze
+SOURCE=maze.c
+
+GCC_LINUX=gcc
+GCC_WINDOWS64=x86_64-w64-mingw32-gcc
+GCC_WINDOWS32=i686-w64-mingw32-gcc
+
+CFLAGS:=-O3 -g -Wall -std=c99 $(CFLAGS)
+
+linux64-$(TARGET): $(SOURCE)
+	$(GCC_LINUX) -m64 $(CFLAGS) -o "$@" "$^"
+
+linux32-$(TARGET): $(SOURCE)
+	$(GCC_LINUX) -m32 $(CFLAGS) -o "$@" "$^"
+
+windows64-$(TARGET).exe: $(SOURCE)
+	$(GCC_WINDOWS64) -m64 $(CFLAGS) -o "$@" "$^"
+
+windows32-$(TARGET).exe: $(SOURCE)
+	$(GCC_WINDOWS32) -m32 $(CFLAGS) -o "$@" "$^"
+
+TARGETS=linux64-$(TARGET) linux32-$(TARGET) windows64-$(TARGET).exe windows32-$(TARGET).exe
+
+all: $(TARGETS)
+clean:
+	rm -f $(TARGETS)

testsuite/basic2-maze/config.yml

@@ -0,0 +1,11 @@
+test:
+    description: "Maze demo that demonstrates more complex symbex with many states"
+
+    targets:
+        - windows64-basic2-maze.exe
+        - windows32-basic2-maze.exe
+        - linux32-basic2-maze
+        - linux64-basic2-maze
+
+    build-options:
+        post-project-generation-script: fix-config.sh

testsuite/basic2-maze/fix-config.sh

@@ -0,0 +1,10 @@
+#!/bin/sh
+set -e
+
+echo "Patching s2e-config.lua..."
+
+# Frequent state switching slows down large guests, increase batch time to avoid that
+sed -i 's/batchTime = 5/batchTime = 5000/g' $PROJECT_DIR/s2e-config.lua
+
+# Make sed worked
+grep -q "batchTime = 5000" $PROJECT_DIR/s2e-config.lua