From 72d3074a440b1eaa9eb24bc663d314ab49df9eb5 Mon Sep 17 00:00:00 2001
From: 0152la <al2510@imperial.ac.uk>
Date: Thu, 29 Jul 2021 19:29:49 +0100
Subject: [PATCH] Add Ubuntu CMake Coverage CI step (#5442)

Adds an extra step to CI jobs which executes the Z3 test suite with
coverage enabled, and additionally executed coverage-enhancing tests
added to z3test.
---
 azure-pipelines.yml                    | 25 +++++++++++++++++++++++++
 scripts/test-regressions-coverage.yaml |  4 ++++
 2 files changed, 29 insertions(+)
 create mode 100644 scripts/test-regressions-coverage.yaml

diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 1735f2337..3db84ce71 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -5,6 +5,7 @@ variables:
   cmakeNet: '-DZ3_BUILD_DOTNET_BINDINGS=True'
   cmakePy:  '-DZ3_BUILD_PYTHON_BINDINGS=True'
   cmakeStdArgs: '-DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../'
+  cmakeCovArgs: '-DCMAKE_INSTALL_PREFIX=./install -G "Ninja" ../'
   asanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"'
   ubsanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" CFLAGS="${CFLAGS} -fsanitize=undefined"'
   msanEnv: 'CC=clang LDFLAGS="-L../libcxx/libcxx_msan/lib -lc++abi -Wl,-rpath=../libcxx/libcxx_msan/lib" CXX=clang++ CXXFLAGS="${CXXFLAGS} -stdlib=libc++ -fsanitize-memory-track-origins -fsanitize=memory -fPIE -fno-omit-frame-pointer -g -O2" CFLAGS="${CFLAGS} -stdlib=libc -fsanitize=memory -fsanitize-memory-track-origins -fno-omit-frame-pointer -g -O2"'
@@ -150,6 +151,30 @@ jobs:
     - ${{if eq(variables['runTests'], 'True')}}:
       - template: scripts/test-regressions.yml
 
+ 
+- job: "Ubuntu16CMakeCoverage"
+  displayName: "Ubuntu build - cmake w/ coverage"
+  pool:
+    vmImage: "ubuntu-latest"
+  steps:
+    - script: sudo apt-get install ninja-build 
+    - script: |
+        set -e
+        mkdir build
+        cd build
+        CXXFLAGS=--coverage LDFLAGS=-lgcov CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Debug $(cmakeCovArgs)
+        ninja
+        ninja test-z3
+        ninja install
+        cd ..
+    - script: |
+         cd build
+         ./test-z3 -a
+         cd ..
+    - template: scripts/test-examples-cmake.yml
+    - template: scripts/test-regressions-coverage.yml
+         
+
 - job: "WindowsLatest"
   displayName: "Windows"
   pool: 
diff --git a/scripts/test-regressions-coverage.yaml b/scripts/test-regressions-coverage.yaml
new file mode 100644
index 000000000..363ea2c19
--- /dev/null
+++ b/scripts/test-regressions-coverage.yaml
@@ -0,0 +1,4 @@
+steps:
+- script: git clone https://github.com/z3prover/z3test z3test
+- script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2    
+- script: python z3test/scripts/test_coverage_tests.py build/install z3test/coverage/cpp