Document, test, and fix --race-check instrumentation

doc/cprover-manual/properties.md

@@ -130,6 +130,7 @@ The goto-instrument program supports these checks:
 | `--undefined-shift-check`    |  add range checks for shift distances                |
 | `--nan-check`                |  add floating-point NaN checks                       |
 | `--uninitialized-check`      |  add checks for uninitialized locals (experimental)  |
+| `--race-check`               |  add data race checks for concurrent programs        |
 | `--error-label label`        |  check that given label is unreachable               |
 
 As all of these checks apply across the entire input program, we may wish to

doc/man/goto-instrument.1

@@ -249,7 +249,7 @@ add checks for uninitialized locals (experimental)
 add check that call stack size of non\-inlined functions never exceeds n
 .TP
 \fB\-\-race\-check\fR
-add floating\-point data race checks
+add data race checks for concurrent programs
 .SS "Semantic transformations:"
 .TP
 \fB\-\-nondet\-volatile\fR

regression/goto-instrument/race-check/conditional.c

@@ -0,0 +1,17 @@
+int shared;
+_Bool flag;
+
+void thread(void)
+{
+  if(flag)
+    shared = 1;
+}
+
+int main(void)
+{
+  flag = 1;
+__CPROVER_ASYNC_0:
+  thread();
+  shared = 2;
+  return 0;
+}

regression/goto-instrument/race-check/conditional.desc

@@ -0,0 +1,9 @@
+CORE
+conditional.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+W/W data race on shared
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/race-check/dirty-local-verification.desc

@@ -0,0 +1,14 @@
+// This test verifies that --race-check detects a W/W data race on a
+// dirty local variable (a local whose address is passed to another thread).
+// It is marked KNOWNBUG because CBMC's symex aborts with "pointer handling
+// for concurrency is unsound" when a pointer to a local variable is shared
+// between threads, preventing verification from completing.
+KNOWNBUG
+dirty-local.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+W/W data race on main::1::local
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/race-check/dirty-local.c

@@ -0,0 +1,13 @@
+void writer(int *p)
+{
+  *p = 42;
+}
+
+int main(void)
+{
+  int local = 0;
+__CPROVER_ASYNC_0:
+  writer(&local);
+  local = 1;
+  return 0;
+}

regression/goto-instrument/race-check/dirty-local.desc

@@ -0,0 +1,9 @@
+CORE
+dirty-local.c
+--race-check
+ASSIGN main::1::local\$w_guard := true
+W/W data race on main::1::local
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-instrument/race-check/function-call-arg.c

@@ -0,0 +1,19 @@
+int shared;
+
+void sink(int val)
+{
+  (void)val;
+}
+
+void writer(void)
+{
+  shared = 42;
+}
+
+int main(void)
+{
+__CPROVER_ASYNC_0:
+  writer();
+  sink(shared);
+  return 0;
+}

regression/goto-instrument/race-check/function-call-arg.desc

@@ -0,0 +1,9 @@
+CORE
+function-call-arg.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+R/W data race on shared
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/race-check/function-call-lhs.c

@@ -0,0 +1,19 @@
+int shared;
+
+int source(void)
+{
+  return 42;
+}
+
+void writer(void)
+{
+  shared = 1;
+}
+
+int main(void)
+{
+__CPROVER_ASYNC_0:
+  writer();
+  shared = source();
+  return 0;
+}

regression/goto-instrument/race-check/function-call-lhs.desc

@@ -0,0 +1,9 @@
+CORE
+function-call-lhs.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+W/W data race on shared
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/race-check/goto-guard.c

@@ -0,0 +1,16 @@
+int shared;
+
+void writer(void)
+{
+  shared = 42;
+}
+
+int main(void)
+{
+__CPROVER_ASYNC_0:
+  writer();
+  if(shared)
+  {
+  }
+  return 0;
+}

regression/goto-instrument/race-check/goto-guard.desc

@@ -0,0 +1,9 @@
+CORE
+goto-guard.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+R/W data race on shared
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/race-check/no-race-sequential.c

@@ -0,0 +1,8 @@
+int shared;
+
+int main(void)
+{
+  shared = 1;
+  shared = 2;
+  return 0;
+}

regression/goto-instrument/race-check/no-race-sequential.desc

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

regression/goto-instrument/race-check/no-race.c

@@ -0,0 +1,14 @@
+__CPROVER_thread_local int thread_local_var;
+
+void thread(void)
+{
+  thread_local_var = 1;
+}
+
+int main(void)
+{
+__CPROVER_ASYNC_0:
+  thread();
+  thread_local_var = 2;
+  return 0;
+}

regression/goto-instrument/race-check/no-race.desc

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

regression/goto-instrument/race-check/pointer.c

@@ -0,0 +1,14 @@
+int x;
+
+void thread(int *p)
+{
+  *p = 1;
+}
+
+int main(void)
+{
+__CPROVER_ASYNC_0:
+  thread(&x);
+  x = 2;
+  return 0;
+}

regression/goto-instrument/race-check/pointer.desc

@@ -0,0 +1,9 @@
+CORE
+pointer.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+data race on x
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/race-check/read-write.c

@@ -0,0 +1,15 @@
+int shared;
+
+void thread(void)
+{
+  shared = 1;
+}
+
+int main(void)
+{
+  int local;
+__CPROVER_ASYNC_0:
+  thread();
+  local = shared;
+  return 0;
+}

regression/goto-instrument/race-check/read-write.desc

@@ -0,0 +1,9 @@
+CORE
+read-write.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+R/W data race on shared
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/race-check/return-value.c

@@ -0,0 +1,20 @@
+int shared;
+
+int get_shared(void)
+{
+  return shared;
+}
+
+void writer(void)
+{
+  shared = 42;
+}
+
+int main(void)
+{
+  int local;
+__CPROVER_ASYNC_0:
+  writer();
+  local = get_shared();
+  return 0;
+}

regression/goto-instrument/race-check/return-value.desc

@@ -0,0 +1,9 @@
+CORE
+return-value.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+R/W data race on shared
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/race-check/write-write.c

@@ -0,0 +1,14 @@
+int shared;
+
+void thread(void)
+{
+  shared = 1;
+}
+
+int main(void)
+{
+__CPROVER_ASYNC_0:
+  thread();
+  shared = 2;
+  return 0;
+}

regression/goto-instrument/race-check/write-write.desc

@@ -0,0 +1,9 @@
+CORE
+write-write.c
+--race-check
+^EXIT=10$
+^SIGNAL=0$
+W/W data race on shared
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1940,7 +1940,7 @@ void goto_instrument_parse_optionst::help()
     HELP_UNINITIALIZED_CHECK
     " {y--stack-depth} {un} \t add check that call stack size of non-inlined"
     " functions never exceeds {un}\n"
-    " {y--race-check} \t add floating-point data race checks\n"
+    " {y--race-check} \t add data race checks for concurrent programs\n"
     "\n"
     "Semantic transformations:\n"
     HELP_NONDET_VOLATILE