Merge pull request diffblue#519 from diffblue/smowton/merge/20180730

SEC-562: Smowton/merge/20180730

Author: smowton

cbmc/.gitignore

@@ -112,10 +112,10 @@ src/clobber/clobber
 src/clobber/clobber.exe
 src/big-int/test-bigint
 src/big-int/test-bigint.exe
-jbmc/src/jbmc/janalyzer
-jbmc/src/jbmc/janalyzer.exe
-jbmc/src/jbmc/jdiff
-jbmc/src/jbmc/jdiff.exe
+jbmc/src/janalyzer/janalyzer
+jbmc/src/janalyzer/janalyzer.exe
+jbmc/src/jdiff/jdiff
+jbmc/src/jdiff/jdiff.exe
 jbmc/src/jbmc/jbmc
 jbmc/src/jbmc/jbmc.exe
 

cbmc/.travis.yml

@@ -57,6 +57,7 @@ jobs:
           packages:
             - cmake
             - google-cloud-sdk
+            - graphviz
       cache:
         directories:
           - ${TRAVIS_BUILD_DIR}/doxygen/build/bin
@@ -101,7 +102,6 @@ jobs:
             - g++-5
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -136,7 +136,6 @@ jobs:
             - libwww-perl
             - g++-5
             - libubsan0
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -165,7 +164,6 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -194,7 +192,6 @@ jobs:
             - g++-5
             - libstdc++-5-dev
             - libubsan0
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -220,7 +217,6 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-5
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -246,7 +242,6 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-7
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-7 bin/gcc
@@ -278,7 +273,6 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         # Use gcc/g++ 5 for tests, as Clang doesn't work yet

cbmc/CODEOWNERS

@@ -3,58 +3,58 @@
 
 # These files should rarely change
 
-src/big-int/ @kroening
-src/ansi-c/ @kroening @tautschnig
-src/assembler/ @kroening @tautschnig
-src/goto-cc/ @kroening @tautschnig
-src/linking/ @kroening @tautschnig
-src/memory-models/ @kroening @tautschnig
-src/goto-symex/ @kroening @tautschnig @peterschrammel
-src/json/ @kroening @tautschnig @peterschrammel
-src/langapi/ @kroening @tautschnig @peterschrammel
-src/xmllang/ @kroening @tautschnig @peterschrammel
-src/nonstd/ @smowton @peterschrammel
-src/solvers/cvc @martin-cs @kroening
-src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
-src/solvers/floatbv @martin-cs @kroening
-src/solvers/miniBDD @tautschnig @kroening
-src/solvers/prop @martin-cs @kroening @tautschnig @peterschrammel
-src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
-src/solvers/smt2 @martin-cs @tautschnig @peterschrammel
-jbmc/src/miniz/ @smowton @mgudemann @peterschrammel
+/src/big-int/ @kroening
+/src/ansi-c/ @kroening @tautschnig
+/src/assembler/ @kroening @tautschnig
+/src/goto-cc/ @kroening @tautschnig
+/src/linking/ @kroening @tautschnig
+/src/memory-models/ @kroening @tautschnig
+/src/goto-symex/ @kroening @tautschnig @peterschrammel
+/src/json/ @kroening @tautschnig @peterschrammel
+/src/langapi/ @kroening @tautschnig @peterschrammel
+/src/xmllang/ @kroening @tautschnig @peterschrammel
+/src/nonstd/ @smowton @peterschrammel
+/src/solvers/cvc @martin-cs @kroening
+/src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
+/src/solvers/floatbv @martin-cs @kroening
+/src/solvers/miniBDD @tautschnig @kroening
+/src/solvers/prop @martin-cs @kroening @tautschnig @peterschrammel
+/src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
+/src/solvers/smt2 @martin-cs @tautschnig @peterschrammel
+/jbmc/src/miniz/ @smowton @mgudemann @peterschrammel
 
 
 # These files change frequently and changes are high-risk
 
-src/cbmc/ @smowton @kroening @tautschnig @peterschrammel
-src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
-src/util/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
-src/solvers/refinement @martin-cs @romainbrenguier @peterschrammel
-jbmc/src/java_bytecode/ @smowton @mgudemann @thk123 @cristina-david @cesaro @pkesseli @NathanJPhillips @peterschrammel
-src/analyses/ @martin-cs @peterschrammel @chrisr-diffblue @thk123 @smowton
-src/pointer-analysis/ @martin-cs @peterschrammel @chrisr-diffblue @smowton
+/src/cbmc/ @smowton @kroening @tautschnig @peterschrammel
+/src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
+/src/util/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
+/src/solvers/refinement @martin-cs @romainbrenguier @peterschrammel
+/jbmc/src/java_bytecode/ @smowton @mgudemann @thk123 @cristina-david @cesaro @pkesseli @NathanJPhillips @peterschrammel
+/src/analyses/ @martin-cs @peterschrammel @chrisr-diffblue @thk123 @smowton
+/src/pointer-analysis/ @martin-cs @peterschrammel @chrisr-diffblue @smowton
 
 
 # These files change frequently and changes are medium-risk
 
-src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
-src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
-src/goto-diff/ @tautschnig @peterschrammel
-jbmc/src/jbmc/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
-jbmc/src/janalyzer/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
-jbmc/src/jdiff/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
-src/cpp/ @kroening @tautschnig @peterschrammel
+/src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
+/src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
+/src/goto-diff/ @tautschnig @peterschrammel
+/jbmc/src/jbmc/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+/jbmc/src/janalyzer/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+/jbmc/src/jdiff/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+/src/cpp/ @kroening @tautschnig @peterschrammel
 
 
 # These files change frequently and changes are low-risk
 
-src/util/irep_ids.def @diffblue/cbmc-developers
+/src/util/irep_ids.def
 
-unit/ @diffblue/cbmc-developers
-regression/ @diffblue/cbmc-developers
-jbmc/unit/ @diffblue/cbmc-developers
-jbmc/regression/ @diffblue/cbmc-developers
+/unit/
+/regression/
+/jbmc/unit/
+/jbmc/regression/
 
-scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
-.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
-appveyor.yml @diffblue/devops @thk123 @forejtv @peterschrammel
+/scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
+/.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
+/appveyor.yml @diffblue/devops @thk123 @forejtv @peterschrammel

cbmc/CODING_STANDARD.md

@@ -197,6 +197,12 @@ Formatting is enforced using clang-format. For more information about this, see
   which safely manages the pointer. As such, `new` should only be used in
   constructors, and `delete` in destructors. Never use `malloc` or `free`.
 
+# CProver conventions
+- Avoid if at all possible using irept methods like `get(ID_name)`, instead cast
+  to a derived type (e.g. `class_typet`) and use the wrapper method `get_name`
+- Use `can_cast_type`/`can_cast_expr` instead of directly checking the `id()`
+  of an `irept`.
+
 # Architecture-specific code
 - Avoid if possible.
 - Use `__LINUX__`, `__MACH__`, and `_WIN32` to distinguish the architectures.

cbmc/COMPILING.md

@@ -29,6 +29,11 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
    Note that you need g++ version 5.0 or newer.
 
+   On Amazon Linux and similar distributions, do as root:
+   ```
+   yum install gcc72-c++ flex bison perl-libwww-perl patch
+   ```
+
    To compile JBMC, you additionally need the JDK and the java-models-library.
    For the JDK, on Debian-like distributions, do as root:
    ```
@@ -66,7 +71,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
 5. To compile JBMC, do
    ```
-   make -C jbmc/src java-models-library-download
+   make -C jbmc/src setup-submodules
    make -C jbmc/src
    ```
 
@@ -92,7 +97,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
 4. To compile JBMC, type
    ```
-   gmake -C jbmc/src java-models-library-download
+   gmake -C jbmc/src setup-submodules
    gmake -C jbmc/src
    ```
 
@@ -118,7 +123,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
 4. To compile JBMC, do
    ```
-   gmake -C jbmc/src java-models-library-download
+   gmake -C jbmc/src setup-submodules
    gmake -C jbmc/src
    ```
 
@@ -144,7 +149,7 @@ Follow these instructions:
    ```
 4. To compile JBMC, do
    ```
-   make -C jbmc/src java-models-library-download
+   make -C jbmc/src setup-submodules
    make -C jbmc/src
    ```
 
@@ -185,9 +190,9 @@ Follow these instructions:
    make -C src DOWNLOADER=wget minisat2-download
    make -C src
    ```
-5. To compile JMBC, open the Cygwin shell and type
+5. To compile JBMC, open the Cygwin shell and type
    ```
-   make -C jbmc/src java-models-library-download
+   make -C jbmc/src setup-submodules
    make -C jbmc/src
    ```
 
@@ -240,7 +245,11 @@ require manual modification of build files.
 2. Navigate to the *top level* folder of the project. This is different from
    the Makefile build, which requires you to navigate to the `src` directory
    first.
-3. Generate build files with CMake:
+3. Update git submodules:
+   ```
+   git submodule update --init
+   ```
+4. Generate build files with CMake:
    ```
    cmake -H. -Bbuild
    ```
@@ -264,7 +273,7 @@ require manual modification of build files.
    Finally, to enable building universal binaries on macOS, you can pass the
    flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
    the build will just be for the architecture of your machine.
-4. Run the build:
+5. Run the build:
    ```
    cmake --build build
    ```

cbmc/appveyor.yml

@@ -84,7 +84,6 @@ test_script:
     rmdir /s /q jbmc\VarLengthArrayTrace1
     rmdir /s /q jbmc\classpath1
     rmdir /s /q jbmc\jar-file3
-    rmdir /s /q jbmc\tableswitch2
     cd ../..
 
     make -C jbmc/regression test BUILD_ENV=MSVC

cbmc/buildspec-windows.yml

@@ -20,7 +20,7 @@ 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 -j4 -C jbmc/src setup-submodules" && bash -c "make -j4 -C jbmc/src BUILD_ENV=MSVC" '
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/unit all BUILD_ENV=MSVC ; exit 0" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/unit all BUILD_ENV=MSVC" '
 
   post_build:
     commands:
@@ -45,6 +45,11 @@ phases:
         Remove-Item goto-instrument\slice08 -Force -Recurse
         Remove-Item goto-analyzer/constant_propagation_nondet_rounding_mode -Force -Recurse
         cd ..
+        cd jbmc/regression
+        Remove-Item jbmc\VarLengthArrayTrace1 -Force -Recurse
+        Remove-Item jbmc\classpath1 -Force -Recurse
+        Remove-Item jbmc\jar-file3 -Force -Recurse
+        cd ../..
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
@@ -56,11 +61,11 @@ 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 jbmc/regression test BUILD_ENV=MSVC ; exit 0" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/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 jbmc/unit test BUILD_ENV=MSVC ; exit 0" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC" '
 
 artifacts:
   files:

cbmc/jbmc/README.md

@@ -27,10 +27,16 @@ JBMC compiles CBMC as part of its build process and as such has all the pre-requ
 Compilation
 ===========
 
-To compile you need to run the command:
+Before compilation, run the commands:
+
+```bash
+make -C src DOWNLOADER=wget minisat2-download
+make -C jbmc/src setup-submodules
+```
+
+Then compile using:
 
 ```bash
-make -C jbmc/src java-models-library-download
 make -C jbmc/src
 ```
 

cbmc/jbmc/regression/jbmc-cover/generics/test.desc

@@ -7,5 +7,3 @@ file AbstractTest.java line 18 .* SATISFIED
 file AbstractTest.java line 19 .* SATISFIED
 file AbstractTest.java line 20 .* SATISFIED
 file AbstractTest.java line 21 .* SATISFIED
-
-

cbmc/jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test.java line 8 .* SUCCESS$

cbmc/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc

@@ -1,12 +1,12 @@
 CORE
 Test.class
---function Test.testme
+--no-refine-strings --function Test.testme
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 type mismatch
 --
 Before cbmc#2472 this would assume that StringBuilder's direct parent was
-java.lang.Object, causing a type mismatch when --refine-strings was not in use
+java.lang.Object, causing a type mismatch when --no-refine-strings was in use
 (which at the time would assume that parent-child relationship)

cbmc/jbmc/regression/jbmc-strings/RegexMatches01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexMatches01.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

cbmc/jbmc/regression/jbmc-strings/RegexMatches02/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexMatches02.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

cbmc/jbmc/regression/jbmc-strings/RegexSubstitution01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution01.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

cbmc/jbmc/regression/jbmc-strings/RegexSubstitution02/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$