From d24d7d78a8c3eddb48873401f665015768431d77 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 28 Jan 2019 12:22:44 +0000
Subject: [PATCH 1/2] Run CBMC regression tests with --paths lifo in CI

We were not regularly exercising this code outside unit tests, leading to
regressions on several tests. On my system, running this additional test takes
42 seconds, which is still better than users running into issues. (ctest -V -L
CORE -j8 takes an extra 10 seconds.)

Fixes: #3956
---
 .travis.yml                                         | 1 +
 buildspec-windows.yml                               | 4 ++++
 buildspec.yml                                       | 1 +
 regression/cbmc/CMakeLists.txt                      | 7 +++++++
 regression/cbmc/Makefile                            | 3 +++
 regression/cbmc/Multi_Dimensional_Array6/test.desc  | 2 +-
 regression/cbmc/address_space_size_limit1/test.desc | 2 +-
 regression/cbmc/array-tests/test.desc               | 2 +-
 8 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 3a89ddf1e71..db76e3f04ff 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -303,6 +303,7 @@ install:
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
+  - UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
   - scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
diff --git a/buildspec-windows.yml b/buildspec-windows.yml
index 8a7c248abc6..dc8c4561c61 100644
--- a/buildspec-windows.yml
+++ b/buildspec-windows.yml
@@ -40,6 +40,10 @@ phases:
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" '
 
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-paths-lifo BUILD_ENV=MSVC" '
+
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" '
diff --git a/buildspec.yml b/buildspec.yml
index e11d3fe33ca..e8a7a453e25 100644
--- a/buildspec.yml
+++ b/buildspec.yml
@@ -25,6 +25,7 @@ phases:
     commands:
       - make -C unit test
       - make -C regression test
+      - make -C regression/cbmc test-paths-lifo
       - scripts/delete_failing_smt2_solver_tests
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
index bb900107e38..954598f0b0f 100644
--- a/regression/cbmc/CMakeLists.txt
+++ b/regression/cbmc/CMakeLists.txt
@@ -1,3 +1,10 @@
 add_test_pl_tests(
     "$<TARGET_FILE:cbmc> --validate-goto-model" -X smt-backend
 )
+
+add_test_pl_profile(
+    "cbmc-paths-lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;-s;paths-lifo"
+    "CORE"
+)
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index 41cc877803e..8242ae26e44 100644
--- a/regression/cbmc/Makefile
+++ b/regression/cbmc/Makefile
@@ -6,6 +6,9 @@ test:
 test-cprover-smt2:
 	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
 
+test-paths-lifo:
+	@../test.pl -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
+
 tests.log: ../test.pl test
 
 show:
diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc
index 6a638d1e767..6694cf6e8b7 100644
--- a/regression/cbmc/Multi_Dimensional_Array6/test.desc
+++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
 main.c
 --unwind 3 --no-unwinding-assertions
 ^EXIT=10$
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
index 161958f9d5d..d68272d8db5 100644
--- a/regression/cbmc/address_space_size_limit1/test.desc
+++ b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects
diff --git a/regression/cbmc/array-tests/test.desc b/regression/cbmc/array-tests/test.desc
index 9efefbc7362..969d6de00f8 100644
--- a/regression/cbmc/array-tests/test.desc
+++ b/regression/cbmc/array-tests/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
 main.c
 
 ^EXIT=0$

From 0bda456a5ebc1cc421cafecb124bebe310f0dd3b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 5 Feb 2019 00:52:17 +0000
Subject: [PATCH 2/2] Decision procedure runtime may be very small

On Codebuild we have seen "1.5222e-05s" when running in path-based mode.
---
 regression/cbmc/Failing_Assert1/test.desc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/cbmc/Failing_Assert1/test.desc b/regression/cbmc/Failing_Assert1/test.desc
index eb20420afda..3acca2686a9 100644
--- a/regression/cbmc/Failing_Assert1/test.desc
+++ b/regression/cbmc/Failing_Assert1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^Runtime decision procedure: [0-9]+(\.[0-9]+)?s$
+^Runtime decision procedure: [0-9]+(\.[0-9]+(e-[0-9]+)?)?s$
 --
 ^warning: ignoring