Squashed 'cbmc/' changes from 31c47c2..20e7bca

20e7bca Merge pull request diffblue#2179 from cesaro/java-concurrency-support3
25e5820 Java concurrency regression tests
bc539b5 Adds support for concurrency in java programs
46849e9 Adding concurrency related methods to CProver.java
c817486 Merge pull request diffblue#2171 from thomasspriggs/json_tweaks
f3670e3 Expose `begin` and `end` methods of underlying `std::vector` in `json_arrayt`.
402bc56 Clang format updates.
2907ba9 Allow constructon of `json_stringt` from `irep_idt`.
ce674b5 Update constructor of `jsont` based on the copy and move idiom.
28117d2 Expose `emplace_back` method of underlying `std::vector` in `json_arrayt`.
a589a56 Supply `value_type` typedef in `json_arrayt` for STL algorithm usage.
1d0cd01 Merge pull request diffblue#2175 from diffblue/extract-goto-functiont
76d202a use goto_function.h when only goto_functiont is used
b9cd297 split out goto_functiont from goto_functions.h into separate file
784b6dd Merge pull request diffblue#2119 from svorenova/gs_tg1121_regression
1b6a939 Merge pull request diffblue#2169 from sonodtt/patch-1
faaacec Add dashboard webhooks to travis
7b0673e Merge pull request diffblue#2154 from diffblue/jar-file-cleanup
d069719 Merge pull request diffblue#1915 from karkhaz/kk-abstract-paths-worklist
aac16d5 Merge pull request diffblue#2159 from peterschrammel/clean-up-specc
d413dd8 Merge pull request diffblue#2123 from smowton/smowton/java-object-factory-zero-initializer
995a548 Merge pull request diffblue#2164 from tautschnig/cleanup-mp-arith
a4d1891 Merge pull request diffblue#2160 from diffblue/fix-java-constructor-pretty-name
b9db37d Merge pull request diffblue#2163 from tautschnig/fix-test
6b064b3 pretty name of constructors now uses empty declarator
b008bf3 add signature to method pretty names
a9bb35c strip package name from base_name of Java class symbols
7711933 Merge pull request diffblue#2162 from tautschnig/fix-format
7d91638 Merge pull request diffblue#2148 from diffblue/remove-fixedbv-option
7e09d5f Fix duplicate output of id in format()
033f4c5 Remove unnecessary (and inconsistent) return statement
90d59d8 Remove unused global constant
29763da Fix misleading comments: the required variant of numeric_cast does not exist
a2260bd remove the --fixedbv command-line option
78901ef fix in rounder in fixed-point arithmetic class
8414886 Remove SpecC support
88bbe32 Clean up references to php frontend
3f52c59 Clean up commented include
01685b6 Clean up references to SpecC frontend
916eb1f Unit tests for path exploration strategies
88db26f Merge pull request diffblue#2155 from tautschnig/mode-fixes
2fb3d2f Add missing mode
85aba52 Make new LIFO path exploration the default
feef069 Doxygen uses C++ parser for .h files
17951c8 Add path strategy chooser class
685937a Path exploration pushes both successors onto queue
2a86fb4 Bugfix: always print path exploration resume point
e823538 Symex paths saved onto abstract data structure
bbd4253 signal errors while getting file from JAR using optional
48f1af3 Merge pull request diffblue#2145 from cesaro/concurrency-support-for-clinit
8db6b22 Merge pull request diffblue#2139 from romainbrenguier/bugfix/annotations-as-comments
94bbbba Added new cmd option to jbmc, 'java-threading'
48914be Modifies the instrumented clinit_wrapper function
ce9f046 Merge pull request diffblue#2146 from diffblue/extra-float-types
46267b5 Merge pull request diffblue#2153 from diffblue/elaborate-format_expr
da940a9 Test for assignement of annotated field
9d94bf7 Make annotations comments in irep_idt
52e9737 new gcc floating-point type identifiers, Fixes: diffblue#2151
c6cbf7c Merge pull request diffblue#2147 from diffblue/fix-tempdir-buffer-overflow
957881c format now prints type expressions and the values of named sub-ireps
9609a52 simplify use of get_temporary_directory
5907f68 fix potential non-zero termination of a string buffer
41d7a45 Merge pull request diffblue#2129 from romainbrenguier/bugfix/generic_type_index
53bc892 Add invariant in java_generic_symbol_type
e3f240a Use get_name in generic_type_index
4a6ae9b Add java_types unit tests to Makefile
4c5144d Unit test for generic_type_index
8f0f780 Unit test for java_generic_symbol_type
41b3a6a Move java_generic_symbol_typet definitions to cpp
0afbe0f Unit test java_type_from_string and fix doc
b7c9ea1 Test for abstract class with two generic arguments
c141611 Fix generic_type_index
8127d4d Merge pull request diffblue#2141 from romainbrenguier/bugfix/goto-convert-mode
4948b70 Merge pull request diffblue#1712 from karkhaz/kk-flush-all
e0bc5fd Merge pull request diffblue#2143 from diffblue/missing-algorithm-include
fbed57e Add precondition ensuring mode is not empty
2ef91e7 Make mode an argument of goto-convert functions
2b4cd76 missing #include <algorithm> for std::find_if_not
7d11e85 Zero-initialize object factory structs
392c765 cleanup the includes in src/java_bytecode
1050637 fix a comment
c57439e missing const for parameter
227e83d Adding regression tests for multi-dimensional arrays
b8ffa5e Merge pull request diffblue#2135 from diffblue/solver-cleanout
0dc35fd Merge pull request diffblue#2136 from diffblue/unwind_module_cleanout
f6a92cc remove bmc_constraints
a2d9822 remove OpenSMT
218dc31 remove support for SMT1
e8aaf09 remove unused includes
b0f7476 remove do_unwind_module hook
4d75d3d Merge branch 'develop' of github.com:diffblue/cbmc into develop
60c03b3 whitespace fix
3ea32fe Merge pull request diffblue#2134 from peterschrammel/invalid-symbol-mode
b2a58c8 Assign mode to invalid objects
e4230c6 Merge pull request diffblue#2130 from romainbrenguier/bugfix/if-expr-mode
c6beb68 Merge pull request diffblue#2128 from tautschnig/include-cleanup
973b309 Merge pull request diffblue#2073 from tautschnig/reset-namespace
a6a825a Remove unused includes
b04122e Move definition of base_type_eqt to .cpp
104bc56 Use pointer_offset_bits instead of locally hacking up what it does anyway
99755fe Move asserts to invariants (and provide suitable includes)
3af3d72 Do not unnecessarily use C string functions
3c697da Add test where tmp_if_expr is introduced
746e337 Set mode of if_exprt introduced in preprocessing
73e0c0f Use C++ streams instead of C-style snprintf
d351a5d Use a single global INITIALIZE_FUNCTION macro instead of __CPROVER_initialize
9c03ca3 Use iosfwd instead of ostream where possible
6b8583d Merge pull request diffblue#2100 from tautschnig/string-table-cleanup
75caefa Merge pull request diffblue#2116 from peterschrammel/java-new-pass
6c90b35 Merge pull request diffblue#2052 from romainbrenguier/bugfix/default-axioms2#TG-2138
53dfa0a Merge pull request diffblue#2120 from diffblue/optional_optnr
8f7d9f0 use optional<size_t> instead of -1 in cmdlinet
a61d03f Remove java_bytecode deps from Makefiles
ce9f1fc Use remove_java_new
10d0042 more files to ignore
95ea29a Merge pull request diffblue#2115 from peterschrammel/language-mode-utils
ce11613 Factor out java new removal into separate pass
baa15f5 Add Makefile dependency for smt2_solver
bacfa27 Merge pull request diffblue#2114 from tautschnig/type-renaming
2bdaafc Add more doxygen to language.h and mode.h
74c2c3d Utility functions to get mode and language
b934aaf symex_dynamic::dynamic_object_size* are constants
ef83f93 array_size symbols: set mode and avoid redundant settings
8b20ebb Merge pull request diffblue#2112 from diffblue/address_of_byte_extract
66aa851 Merge pull request diffblue#2109 from LAJW/lajw/free-lambda-from-cpplint-oppression
7339638 Merge pull request diffblue#2111 from peterschrammel/bugfix/missing-java-modes
18cab61 Rephrase and justify curly brace alignment exceptions
6670703 Added an extension point for irep ids
38782bd Move enum idt to the single translation unit that actually requires it
e657da8 Fix Doxygen syntax
f79b453 Check that the string table does not include unused entries
61ca5df Remove unused entries from the string table
b2e4ca0 Use existing irep_idts instead of strings
2b819e6 Remove unused symbolt::{to,from}_irep
0b82ee2 allow address_of of byte_extract expressions
7747442 Associate dynamic objects with respective language mode
6438ee7 Bugfix: use proper language registration in unit tests
c274c15 Set mode in goto_convert auxiliary symbols
9a896f9 Replace asserts by invariants
78191ee Remove NOLINTs for lambdas.
692c4f3 Remove brace checking from cpplint
d344dd9 Update coding standard
b59a453 Move MAX_CONCRETE_STRING_SIZE definition to magic
05b924c Deprecate string-max-length option
132a26b Add tests showing the effect on string-max-length
0e8a863 Add test for generics array and strings
b83182f Get rid of string_max_length field
d726577 Make char_array_of_pointer return a reference
2154047 Get rid of default axioms for strings
1d4f26c Assign 0 to string length for null Java String
ff25fe2 Weaken invariant for nil exprt as model of array
56e7b37 Make get_array return nil for long strings
5fde05a Use string-max-length as default max input-length
b0c6528 Use boolbvt for getting counter examples
5b3a1a4 Remove unnecessary replace_expr
a630bb7 Correct bound in test with long string
e4cf694 Bugfix: Java symbol types must have mode ID_java
e158bb4 Bugfix: Java array symbols must have mode ID_java
d475abc Reset namespace after symbolic execution
1ef0f41 Add --flush option to flush all output

git-subtree-dir: cbmc
git-subtree-split: 20e7bca

Author: smowton

.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
@@ -104,8 +107,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

.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:
@@ -279,3 +286,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
+    

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
 ===

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`

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

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));

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;
+}

regression/cbmc-concurrency/malloc2/test.desc

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

regression/cbmc-java-concurrency/CMakeLists.txt

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

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)

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);
+  }
+}

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

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

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);
+    }
+}

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
+--
+--

regression/cbmc-java/annotations2/Test.class

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

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;
+    }
+  }
+}

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];
+    }
+  }
+}

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;
+    }
+  }
+}

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;
+    }
+  }
+}

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;
+  }
+}

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;
+    }
+  }
+}

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