From 66283a1722416bb31b3b835455bd0084424064ce Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 7 Jun 2019 09:58:35 -0700
Subject: [PATCH] update pipeline

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 azure-pipelines.yml                     | 33 ++++++++++++++++++++-----
 contrib/ci/scripts/build_z3_cmake.sh    |  7 ------
 scripts/azure-pipeline.vsts-vs2013.yaml | 15 -----------
 scripts/azure-pipeline.vsts-vs2017.yaml | 16 ------------
 4 files changed, 27 insertions(+), 44 deletions(-)
 delete mode 100644 scripts/azure-pipeline.vsts-vs2013.yaml
 delete mode 100644 scripts/azure-pipeline.vsts-vs2017.yaml

diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 9d63b8dd0..3d7b2fd6b 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -1,4 +1,9 @@
 
+variables:
+  cmakeStdArgs: '-DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "Ninja" ../'
+  asanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" {CFLAGS} -fsanitize=address -fno-omit-frame-pointer"'
+  ubsanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" CFLAGS="${CFLAGS} -fsanitize=undefined"'
+
 jobs:
 
 - job: "LinuxPythonDebug"
@@ -21,7 +26,10 @@ jobs:
     - script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2    
 
 
-# TBD: specify a matrix of options that are used in the cmake line.
+# TBD: 
+#   test python bindings
+#   build documentation
+#   Asan, ubsan, msan
 
 - job: "LinuxCMake"
   displayName: "Ubuntu build - cmake"
@@ -30,11 +38,20 @@ jobs:
   strategy:
     matrix:
       debugClang:
-        cmdLine: 'CC=clang CXX=clang++ cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -G "Ninja" ../'
+        cmdLine: 'CC=clang CXX=clang++ cmake $(cmakeStdArgs)'
+        runUnitTest: True
       releaseClang:
-        cmdLine: 'CC=clang CXX=clang++ cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DCMAKE_BUILD_TYPE=Release -G "Ninja" ../'
+        cmdLine: 'CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Release $(cmakeStdArgs)'
+        runUnitTest: True
       debugGcc:
-        cmdLine: 'CC=gcc CXX=g++ cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -G "Ninja" ../'
+        cmdLine: 'CC=gcc CXX=g++ cmake $(cmakeStdArgs)'
+        runUnitTest: True
+      gccX86:
+        cmdLine: 'CXXFLAGS="${CXXFLAGS} -m32" CFLAGS="${CFLAGS} -m32" CC=gcc-5 CXX=g++-5 cmake -DCMAKE_BUILD_TYPE=RelWithDebInfo $(cmakeStdArgs)'
+        runUnitTest: True
+      asan:
+        cmdLine: '$(asanEnv) cmake $(cmakeStdArgs)'
+        runUnitTest: False
   steps:
     - script: sudo apt-get install ninja-build
     - script: |
@@ -51,7 +68,6 @@ jobs:
         examples/cpp_example_build_dir/cpp_example
         examples/tptp_build_dir/z3_tptp5 -help
         examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt
-        # TBD: add python examples
         mkdir -p examples/java
         cp ../examples/java/JavaExample.java examples/java/
         javac examples/java/Javaexamplejava -classpath com.microsoft.z3.jar
@@ -59,6 +75,11 @@ jobs:
         java -cp .:examples/java:com.microsoft.z3.jar JavaExample
         ./test-z3 -a
         cd ..
+    - script: |
+         cd build
+         ./test-z3 -a
+         cd ..
+      condition: $(runUnitTest)
     - script: git clone https://github.com/z3prover/z3test z3test
     - script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2    
 
@@ -100,7 +121,7 @@ jobs:
     - script: |
         mkdir build
         cd build
-        CC=clang CXX=clang++ cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -G "Ninja" ../
+        CC=clang CXX=clang++ $(cmakeStdArgs)
         ninja
         ninja test-z3
         ninja c_example
diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh
index c1014d5d5..4333bb092 100755
--- a/contrib/ci/scripts/build_z3_cmake.sh
+++ b/contrib/ci/scripts/build_z3_cmake.sh
@@ -33,13 +33,6 @@ else
   ADDITIONAL_Z3_OPTS+=('-DBUILD_LIBZ3_SHARED=ON')
 fi
 
-# Use OpenMP?
-if [ "X${USE_OPENMP}" = "X1" ]; then
-  ADDITIONAL_Z3_OPTS+=('-DUSE_OPENMP=ON')
-else
-  ADDITIONAL_Z3_OPTS+=('-DUSE_OPENMP=OFF')
-fi
-
 # Use LibGMP?
 if [ "X${USE_LIBGMP}" = "X1" ]; then
   ADDITIONAL_Z3_OPTS+=('-DUSE_LIB_GMP=ON')
diff --git a/scripts/azure-pipeline.vsts-vs2013.yaml b/scripts/azure-pipeline.vsts-vs2013.yaml
deleted file mode 100644
index fa8d5451b..000000000
--- a/scripts/azure-pipeline.vsts-vs2013.yaml
+++ /dev/null
@@ -1,15 +0,0 @@
-pool:
-  name: Hosted
-  demands: Cmd
-
-steps:
-- task: DotNetCoreInstaller@0
-  displayName: 'Use .NET Core sdk 2.1'
-  inputs:
-    version: 2.1.300
-
-- task: BatchScript@1
-  displayName: 'scripts\vsts-vs2013.cmd'
-  inputs:
-    filename: 'scripts\vsts-vs2013.cmd'
-
diff --git a/scripts/azure-pipeline.vsts-vs2017.yaml b/scripts/azure-pipeline.vsts-vs2017.yaml
deleted file mode 100644
index 0feafbaf6..000000000
--- a/scripts/azure-pipeline.vsts-vs2017.yaml
+++ /dev/null
@@ -1,16 +0,0 @@
-pool:
-  name: Hosted
-  demands: Cmd
-
-steps:
-- task: DotNetCoreInstaller@0
-  displayName: 'Use .NET Core sdk 2.1'
-  inputs:
-    version: 2.1.300
-
-- task: BatchScript@1
-  displayName: 'scripts\vsts-vs2017.cmd'
-  inputs:
-    filename: 'scripts\vsts-vs2017.cmd'
-    arguments: 'x64'
-