Merge pull request diffblue#410 from diffblue/smowton/merge/20180511

Smowton/merge/20180511

Author: smowton

cbmc/.gitignore

@@ -30,8 +30,10 @@ Release/*
 *.lib
 src/ansi-c/arm_builtin_headers.inc
 src/ansi-c/clang_builtin_headers.inc
+src/ansi-c/cprover_builtin_headers.inc
 src/ansi-c/cprover_library.inc
 src/ansi-c/cw_builtin_headers.inc
+src/ansi-c/gcc_builtin_headers_types.inc
 src/ansi-c/gcc_builtin_headers_alpha.inc
 src/ansi-c/gcc_builtin_headers_arm.inc
 src/ansi-c/gcc_builtin_headers_generic.inc
@@ -46,6 +48,7 @@ src/ansi-c/gcc_builtin_headers_tm.inc
 src/ansi-c/gcc_builtin_headers_mips.inc
 src/ansi-c/gcc_builtin_headers_power.inc
 src/ansi-c/gcc_builtin_headers_ubsan.inc
+src/ansi-c/windows_builtin_headers.inc
 src/java_bytecode/java_core_models.inc
 
 # regression/test files
@@ -105,8 +108,8 @@ src/goto-instrument/goto-instrument.exe
 src/jbmc/jbmc
 src/musketeer/musketeer
 src/musketeer/musketeer.exe
-src/solvers/smt2/smt2_solver
-src/solvers/smt2/smt2_solver.exe
+src/solvers/smt2_solver
+src/solvers/smt2_solver.exe
 src/symex/symex
 src/symex/symex.exe
 src/goto-diff/goto-diff

cbmc/.travis.yml

@@ -38,6 +38,13 @@ jobs:
       script: scripts/travis_lint.sh
       before_cache:
 
+    - &string-table-check
+      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="string-table"
+      install:
+      script: scripts/string_table_check.sh
+      before_cache:
+
     - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
       env: NAME="DOXYGEN-CHECK"
       addons:
@@ -280,3 +287,14 @@ script:
 
 before_cache:
   - ccache -s
+
+notifications:
+  webhooks:
+    urls:
+      - http://dashboard.diffblue.com/api/travis-webhooks
+    on_success: always
+    on_failure: always
+    on_start: never
+    on_cancel: never
+    on_error: always
+    

cbmc/CHANGELOG

@@ -4,6 +4,9 @@
   generate bodies for functions that don't have a body
   in the goto code. This supercedes the functionality
   of --undefined-function-is-assume-false
+* The --fixedbv command-line option has been removed
+  (it was marked deprecated in January 2017)
+
 
 5.8
 ===

cbmc/CODING_STANDARD.md

@@ -19,7 +19,10 @@ Formatting is enforced using clang-format. For more information about this, see
       - Nested function calls do not need to be broken up into separate lines
         even if the outer function call does.
 - If a method is bigger than 50 lines, break it into parts.
-- Put matching `{ }` into the same column.
+- Put matching `{ }` into the same column, except for initializer lists and
+  lambdas, where you should place `{` directly after the closing `)`. This is
+  to comply with clang-format, which doesn't support aligned curly braces in
+  these cases.
 - Spaces around binary operators (`=`, `+`, `==` ...)
 - Space after comma (parameter lists, argument lists, ...)
 - Space after colon inside `for`

cbmc/regression/ansi-c/float_constant1/main.c

@@ -10,6 +10,17 @@ STATIC_ASSERT(0X1.0P-95F == 2.524355e-29f);
 // nothing before the dot
 STATIC_ASSERT(0X.0p+1f == 0);
 
+// 32-bit, 64-bit and 128-bit constants, GCC proper only,
+// clang doesn't have it
+#if defined(__GNUC__) && !defined(__clang__)
+STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32)));
+STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64)));
+STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128)));
+STATIC_ASSERT(__builtin_types_compatible_p(_Float32x, __typeof(1.0f32x)));
+STATIC_ASSERT(__builtin_types_compatible_p(_Float64x, __typeof(1.0f64x)));
+STATIC_ASSERT(__builtin_types_compatible_p(_Float128x, __typeof(1.0f128x)));
+#endif
+
 #ifdef __GNUC__
 _Complex c;
 #endif

cbmc/regression/ansi-c/gcc_types_compatible_p1/main.c

@@ -97,6 +97,10 @@ STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed));
 
 #ifndef __clang__
 // clang doesn't have these
+STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float));
+STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double));
+STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float));
+STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double));

cbmc/regression/cbmc-concurrency/malloc2/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+#include <pthread.h>
+
+_Bool set_done;
+int *ptr;
+
+void *set_x(void *arg)
+{
+  *(int *)arg = 10;
+  set_done = 1;
+}
+
+int main(int argc, char *argv[])
+{
+  __CPROVER_assume(argc >= sizeof(int));
+  ptr = malloc(argc);
+  __CPROVER_ASYNC_1: set_x(ptr);
+  __CPROVER_assume(set_done);
+  assert(*ptr == 10);
+  return 0;
+}

cbmc/regression/cbmc-concurrency/malloc2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

cbmc/regression/cbmc-java-concurrency/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:jbmc>"
+)

cbmc/regression/cbmc-java-concurrency/Makefile

@@ -0,0 +1,32 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/jbmc/jbmc
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/jbmc/jbmc
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

cbmc/regression/cbmc-java-concurrency/explicit_thread_blocks/A.class

@@ -0,0 +1,61 @@
+import java.lang.Thread;
+import org.cprover.CProver;
+
+public class A
+{
+  static int x = 0;
+
+  // verification success
+  public void me()
+  {
+    x = 5;
+    CProver.startThread(333);
+    x = 10;
+    CProver.endThread(333);
+    assert(x == 5 || x == 10);
+  }
+
+  // verification failed
+  public void me2()
+  {
+    x = 5;
+    CProver.startThread(333);
+    x = 10;
+    CProver.endThread(333);
+    assert(x == 10);
+  }
+
+  // Known-bug, thread id mismatch, this should be detected by the conversation
+  // process. It is currently not and thus will result in an assertion violation
+  // during symbolic execution.
+  public void me3()
+  {
+    x = 5;
+    CProver.startThread(22333);
+    x = 10;
+    CProver.endThread(333);
+    assert(x == 10);
+  }
+
+  // Known-bug, see: https://github.com/diffblue/cbmc/issues/1630
+  public void me4()
+  {
+    int x2 = 10;
+    CProver.startThread(22333);
+    x = x2;
+    assert(x == 10);
+    CProver.endThread(333);
+  }
+
+  // Known-bug, symex cannot handle nested thread-blocks
+  public void me5()
+  {
+    CProver.startThread(333);
+    x = 5;
+    CProver.startThread(222);
+    x = 8;
+    CProver.endThread(222);
+    CProver.endThread(333);
+    assert(x == 5 || x == 0 || x == 8);
+  }
+}

cbmc/regression/cbmc-java-concurrency/explicit_thread_blocks/A.java

@@ -0,0 +1,7 @@
+CORE
+A.class
+--function "A.me:()V" --lazy-methods --java-threading
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL

cbmc/regression/cbmc-java-concurrency/explicit_thread_blocks/test.desc

@@ -0,0 +1,6 @@
+CORE
+A.class
+--function "A.me2:()V" --lazy-methods --java-threading
+
+^SIGNAL=0$
+^VERIFICATION FAILED

cbmc/regression/cbmc-java-concurrency/explicit_thread_blocks/test2.desc

@@ -0,0 +1,13 @@
+@interface FieldAnnotation {
+}
+
+public class Test {
+    @FieldAnnotation
+    public static double d;
+
+    public void check() {
+        double f = d;
+        assert(f == d);
+        assert(f != d);
+    }
+}

cbmc/regression/cbmc-java/annotations2/FieldAnnotation.class

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 10 .* SUCCESS
+assertion at file Test.java line 11 .* FAILURE
+--
+--

cbmc/regression/cbmc-java/annotations2/Test.class

@@ -0,0 +1,3 @@
+public class A {
+  public float a;
+}

cbmc/regression/cbmc-java/annotations2/Test.java

@@ -0,0 +1,17 @@
+public class FloatMultidim1 {
+  public float[][] f(int y) {
+    if (y > 0 && y < 5) {
+      float[][] a1 = new float[y][2];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[j][1] = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}

cbmc/regression/cbmc-java/annotations2/test.desc

@@ -0,0 +1,17 @@
+public class FloatMultidim2 {
+  public float[][] f(int y) {
+    if (y > 0 && y < 5) {
+      float[][] a1 = new float[2][y];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[1][j] = 1.0f;
+      return a1;
+    } else {
+      return new float[1][1];
+    }
+  }
+}

cbmc/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.class

@@ -0,0 +1,18 @@
+public class RefMultidim1 {
+  public A[][] f(int y) {
+    if (y > 0 && y < 5) {
+      A[][] a1 = new A[y][2];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[j][1] = new A();
+      a1[j][1].a = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}

cbmc/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java

@@ -0,0 +1,18 @@
+public class RefMultidim2 {
+  public A[][] f(int y) {
+    if (y > 0 && y < 5) {
+      A[][] a1 = new A[2][y];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[1][j] = new A();
+      a1[1][j].a = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}

cbmc/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.class

@@ -0,0 +1,8 @@
+public class RefMultidimConstsize {
+  public void f(int y) {
+    A[][] a1 = new A[2][2];
+    int j = 1;
+    a1[j][1] = new A();
+    a1[j][1].a = 1.0f;
+  }
+}

cbmc/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.java

@@ -0,0 +1,18 @@
+public class RefSingledim {
+  public A[] f(int y) {
+    if (y > 0 && y < 5) {
+      A[] a1 = new A[y];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[j] = new A();
+      a1[j].a = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}

cbmc/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.class

@@ -0,0 +1,12 @@
+KNOWNBUG
+FloatMultidim1.class
+--function FloatMultidim1.f --cover location --unwind 3
+\d+ of \d+ covered
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This crashes during symex, with error 'cannot unpack array of nonconst size'
+when trying to access the element of the array. Symex uses byte_extract_little
+_endian to access the element which does not get simplified (it seems the
+problem is that the types in the instruction do not match). TG-1121