Making the instrumented clinit_wrapper function thread-safe

.clang-format

@@ -84,7 +84,7 @@ NamespaceIndentation: None
 PenaltyBreakString: 10000
 PointerAlignment: Right
 ReflowComments: 'false'
-SortIncludes: 'false'
+SortIncludes: 'true'
 SpaceAfterCStyleCast: 'false'
 SpaceBeforeAssignmentOperators: 'true'
 SpaceBeforeParens: Never

.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:

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/Struct_ptrmember1/main.c

@@ -0,0 +1,10 @@
+struct some_struct
+{
+  int some_field;
+} array[10];
+
+int main()
+{
+  array[0].some_field=1;
+  array->some_field=1;
+}

regression/ansi-c/Struct_ptrmember1/test.desc

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

regression/ansi-c/gcc_attributes11/main.c

@@ -0,0 +1,18 @@
+#ifdef __GNUC__
+// example extracted from SV-COMP's ldv-linux-3.4-simple/
+// 32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640
+static int __attribute__((__section__(".init.text")))
+__attribute__((no_instrument_function)) dp83640_init(void)
+{
+  return 0;
+}
+int init_module(void) __attribute__((alias("dp83640_init")));
+#endif
+
+int main()
+{
+#ifdef __GNUC__
+  dp83640_init();
+#endif
+  return 0;
+}

regression/ansi-c/gcc_attributes11/test.desc

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

regression/ansi-c/gcc_attributes9/main.c

@@ -11,11 +11,23 @@ const char* __attribute__((section("s"))) __attribute__((weak)) bar();
 volatile int __attribute__((__section__(".init.data1"))) txt_heap_base1;
 volatile int __attribute__((__section__(".init.data3"))) txt_heap_base, __attribute__((__section__(".init.data4"))) txt_heap_size;
 
+int __attribute__((__section__(".init.text"))) __attribute__((__cold__))
+__alloc_bootmem_huge_page(void *h);
+int __attribute__((__section__(".init.text"))) __attribute__((__cold__))
+alloc_bootmem_huge_page(void *h);
+int alloc_bootmem_huge_page(void *h)
+  __attribute__((weak, alias("__alloc_bootmem_huge_page")));
+int __alloc_bootmem_huge_page(void *h)
+{
+  return 1;
+}
 #endif
 
 int main()
 {
 #ifdef __GNUC__
+  int r = alloc_bootmem_huge_page(0);
+
   static int __attribute__((section(".data.unlikely"))) __warned;
   __warned=1;
   return __warned;

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/assertion_error_constructors/AssertionIssue.java

@@ -0,0 +1,13 @@
+public class AssertionIssue {
+
+    public static void throwAssertion() {
+        throw new AssertionError("Something went terribly wrong.", new ThrowableAssertion());
+    }
+
+    public static class ThrowableAssertion extends Throwable {
+        @Override
+        public String getMessage() {
+            return "How did we get here?";
+        }
+    }
+}

regression/cbmc-java/assertion_error_constructors/test.desc

@@ -0,0 +1,8 @@
+CORE
+AssertionIssue.class
+--function AssertionIssue.throwAssertion
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java

@@ -0,0 +1,7 @@
+public class TestClass {
+  public static void f(int y) {
+    float[][] a1 = new float[y][3];
+    int j = 0;
+    a1[j][0] = 34.5f;
+  }
+}

regression/cbmc-java/dynamic-multi-dimensional-array/test.desc

@@ -0,0 +1,10 @@
+CORE
+TestClass.class
+--function TestClass.f --cover location --unwind 2
+Source GOTO statement: .*
+(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows)
+^EXIT=6$
+--
+--
+The exception thrown in this test is the symptom of a bug; the purpose of this
+test is the validate the output of that exception

regression/cbmc-java/static_init1/test1.desc

@@ -0,0 +1,8 @@
+CORE
+static_init.class
+--function static_init.main --java-threading
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/static_init2/test1.desc

@@ -0,0 +1,8 @@
+CORE
+static_init.class
+--function static_init.main --java-threading
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/static_init_order/test3.desc

@@ -0,0 +1,7 @@
+CORE
+static_init_order.class
+--function static_init_order.test1 --trace --java-threading
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc-java/static_init_order/test4.desc

@@ -0,0 +1,7 @@
+CORE
+static_init_order.class
+--function static_init_order.test2 --java-threading
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

regression/cbmc-java/virtual7/test.desc

@@ -3,6 +3,6 @@ test.class
 --show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
-IF.*"java::C".*THEN GOTO
-IF.*"java::D".*THEN GOTO
+IF.*"java::B".*THEN GOTO
+IF.*"java::E".*THEN GOTO
 IF.*"java::A".*THEN GOTO

regression/cbmc/Bitfields3/main.c

@@ -0,0 +1,53 @@
+#include <stdlib.h>
+#include <assert.h>
+
+#pragma pack(1)
+struct A
+{
+  unsigned char a;
+  unsigned char b : 2;
+  unsigned char c : 2;
+  unsigned char d;
+};
+
+struct B
+{
+  unsigned char a;
+  unsigned char b : 2;
+  unsigned char c;
+  unsigned char d : 2;
+};
+
+struct C
+{
+  unsigned char a;
+  unsigned char b : 4;
+  unsigned char c : 4;
+  unsigned char d;
+};
+#pragma pack()
+
+int main(void)
+{
+  assert(sizeof(struct A) == 3);
+  struct A *p = malloc(3);
+  assert((unsigned char *)p + 2 == &(p->d));
+  p->c = 3;
+  if(p->c != 3)
+  {
+    free(p);
+  }
+  free(p);
+
+  assert(sizeof(struct B) == 4);
+  struct B *pb = malloc(4);
+  assert((unsigned char *)pb + 2 == &(pb->c));
+  free(pb);
+
+  assert(sizeof(struct C) == 3);
+  struct C *pc = malloc(3);
+  assert((unsigned char *)pc + 2 == &(pc->d));
+  free(pc);
+
+  return 0;
+}

regression/cbmc/Bitfields3/test.desc

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

regression/jbmc-strings/char_escape/Test.java

@@ -0,0 +1,19 @@
+public class Test {
+
+    public static boolean test(char c1, char c2, char c3, char c4, char c5, char c6, char c7, char c8) {
+        StringBuilder sb = new StringBuilder("");
+        sb.append(c1);
+        sb.append(c2);
+        sb.append(c3);
+        sb.append(c4);
+        sb.append(c5);
+        sb.append(c6);
+        sb.append(c7);
+        sb.append(c8);
+        if (sb.toString().equals("\b\t\n\f\r\"\'\\"))
+            return true;
+        if (!sb.toString().equals("\b\t\n\f\r\"\'\\"))
+            return false;
+        return true;
+    }
+}

regression/jbmc-strings/char_escape/test.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --function Test.test --cover location --trace --json-ui
+^EXIT=0$
+^SIGNAL=0$
+20 of 23 covered \(87.0%\)|30 of 44 covered \(68.2%\)

regression/jbmc-strings/long_string/Test.java

@@ -30,7 +30,9 @@ public static void checkAbort(String s, String t) {
         String u = s.concat(t);
 
         // Filter out
-        if(u.length() < 67_108_864)
+        // 67_108_864 corresponds to the maximum length for which the solver
+        // will concretize the string.
+        if(u.length() <= 67_108_864)
             return;
         if(CProverString.charAt(u, 2_000_000) != 'b')
             return;

regression/jbmc-strings/long_string/test_abort.desc

@@ -1,9 +1,10 @@
 CORE
 Test.class
---refine-strings --function Test.checkAbort
-^EXIT=6$
+--refine-strings --function Test.checkAbort --trace
+^EXIT=10$
 ^SIGNAL=0$
+dynamic_object[0-9]*=\(assignment removed\)
 --
 --
-This tests should abort, because concretizing a string of the required
-length may take to much memory.
+This tests that the object does not appear in the trace, because concretizing
+a string of the required length may take too much memory.