[eacsl] Complete ensuresec example with run scripts

src/plugins/e-acsl/examples/ensuresec/.gitignore

+build/

src/plugins/e-acsl/examples/ensuresec/Makefile

+OUT:=$(dir $(abspath $(lastword $(MAKEFILE_LIST))))build
+DEPS:=Makefile ensuresec_ee.c json_assert.c
+EACSL_CC:=e-acsl-gcc.sh -c --concurrency --external-assert json_assert.c ensuresec_ee.c
+MKDIR:=mkdir -p
+
+EE_ID:=EnsuresecEE
+EE_TOOL_ID:=EnsuresecEE_EACSL
+
+$(OUT)/ensuresec_ee.e-acsl: $(DEPS)
+	$(MKDIR) $(OUT)
+	$(EACSL_CC) -o $(OUT)/ensuresec_ee.frama.c -O $(OUT)/ensuresec_ee
+
+$(OUT)/ensuresec_ee_pall.e-acsl: $(DEPS)
+	$(MKDIR) $(OUT)
+	$(EACSL_CC) -e -DE_ACSL_DEBUG_ASSERT -o $(OUT)/ensuresec_ee_pall.frama.c -O $(OUT)/ensuresec_ee_pall
+
+$(OUT)/ensuresec_ee_debug.e-acsl: $(DEPS)
+	$(MKDIR) $(OUT)
+	$(EACSL_CC) -e -DE_ACSL_DEBUG_ASSERT --rt-debug -o $(OUT)/ensuresec_ee_debug.frama.c -O $(OUT)/ensuresec_ee_debug
+
+compile: $(OUT)/ensuresec_ee.e-acsl
+compile_print_all: $(OUT)/ensuresec_ee_pall.e-acsl
+compile_debug: $(OUT)/ensuresec_ee_debug.e-acsl
+
+run: $(OUT)/ensuresec_ee.e-acsl
+	ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee.json" $(OUT)/ensuresec_ee.e-acsl
+
+run_print_all: $(OUT)/ensuresec_ee_pall.e-acsl
+	ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee_pall.json" $(OUT)/ensuresec_ee_pall.e-acsl
+
+run_debug: $(OUT)/ensuresec_ee_debug.e-acsl
+	ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee_debug.json" $(OUT)/ensuresec_ee_debug.e-acsl
+
+all: run run_print_all run_debug
+
+clean:
+	rm -rf $(OUT)

src/plugins/e-acsl/examples/ensuresec/README.md

+# Ensuresec
+
+This folder illustrates the developments done for the European H2020 project
+Ensuresec.
+
+## Files
+
+### `Makefile`
+
+The makefile in the folder provides some targets to test the ensuresec
+developments:
+
+- `compile` (default): Compile `ensuresec_ee.c` with the external assert
+  implementation in `json_assert.c`.
+- `compile_print_all`: Same as `compile` but every assertion (valid or invalid)
+  will be printed to the output.
+- `compile_debug`: Same as `compile_print_all` but in debug mode.
+- `run`: run the output of the `compile` step.
+- `run_print_all`: run the output of the `compile_print_all` step.
+- `run_debug`: run the output of the `compile_debug` step.
+
+### `json_assert.c`
+
+The file `json_assert.c` contains an external `__e_acsl_assert()` implementation
+that will print assertion violations to a json file.
+
+The following environment variables must be defined when using this
+implementation:
+
+- `ENSURESEC_EE_ID`: Ensuresec e-commerce ecosystem id
+- `ENSURESEC_EE_TOOL_ID`: Ensuresec e-commerce ecosystem tool id
+- `ENSURESEC_OUTPUT_FILE`: json output file
+
+### `ensuresec_ee.c`
+
+Multithread program serving as an exemple Ensuresec e-commerce ecosystem
+program. The program contains `check` assertions that will be violated during
+its execution without halting the program.

src/plugins/e-acsl/examples/ensuresec/ensuresec_ee.c

+// Get default definitions and macros, e.g. pthread_rwlock_t
+#ifndef _DEFAULT_SOURCE
+#  define _DEFAULT_SOURCE 1
+#endif
+
+#include <assert.h>
+#include <errno.h>
+#include <pthread.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+// Number of writers and readers created
+#define SIZE 10
+
+// Mutex protecting the calls to `rand()`
+static pthread_mutex_t rand_mutex;
+
+// Data array
+static int *values[SIZE];
+
+// Synchronization array: if `written[idx] == 1` then `values[idx]` has been written to.
+static int written[SIZE] = {0};
+
+// Read-write lock protecting the accesses to `written`
+static pthread_rwlock_t locks[SIZE];
+
+// Thread-safe version of `rand()` that returns a random value between `min`
+// and `max`.
+/*@ requires 0 <= min < max <= RAND_MAX;
+  @ ensures min <= \result <= max; */
+static int ensuresec_rand(int min, int max) {
+  pthread_mutex_lock(&rand_mutex);
+  int value = rand();
+  pthread_mutex_unlock(&rand_mutex);
+  return (double)value * (max - min) / RAND_MAX + min;
+}
+
+/*@ requires \let idx = *(int*)arg; 0 <= idx < SIZE; */
+static void *write_value(void *arg) {
+  int idx = *(int *)arg;
+  pthread_rwlock_t *lock = &locks[idx];
+
+  // Acquire a read lock so that the specification can check `writte[idx]` and
+  // `values[idx]`.
+  pthread_rwlock_rdlock(lock);
+
+  /*@ requires written[idx] == 0;
+    @ ensures written[idx] == 1;
+    @ ensures \valid_read(values[idx]) && \initialized(values[idx]); */
+  {
+    // Long computation
+    int duration = ensuresec_rand(1, 5);
+    sleep(duration);
+
+    // No data race since each thread will access its own index and
+    // `read_value()` will not read this index until we update `written[idx]`.
+    values[idx] = malloc(sizeof(int));
+    *values[idx] = idx + duration;
+
+    // Now we want to update `written[idx]` so we need to acquire the lock for
+    // this index in writing mode
+    pthread_rwlock_unlock(lock);
+    pthread_rwlock_wrlock(lock);
+    written[idx] = 1;
+  }
+
+  pthread_rwlock_unlock(lock);
+  return NULL;
+}
+
+/*@ requires \let idx = *(int*)arg; 0 <= idx < SIZE; */
+static void *read_value(void *arg) {
+  int idx = *(int *)arg;
+  pthread_rwlock_t *lock = &locks[idx];
+
+  // Long computation
+  int duration = ensuresec_rand(0, 3);
+  sleep(duration);
+
+  // Check `written[idx]` while the value is 0
+  int idx_written;
+  do {
+    pthread_rwlock_rdlock(lock);
+    idx_written = written[idx];
+    // Unlock and sleep a bit between each check to let `write_value()` some
+    // time to change the value of `written[idx]`
+    pthread_rwlock_unlock(lock);
+    usleep(100);
+  } while (!idx_written);
+
+  // Acquire a read lock so that the specification can check `writte[idx]` and
+  // `values[idx]`.
+  pthread_rwlock_rdlock(lock);
+  /*@ requires written[idx] == 1;
+    @ requires \valid_read(values[idx]) && \initialized(values[idx]); */
+  {
+    int value = *values[idx];
+    free(values[idx]);
+
+    // Non-critical assertion that will sometimes fail and raise an alert
+    //@ check (value - idx) > duration;
+  }
+  pthread_rwlock_unlock(lock);
+
+  return NULL;
+}
+
+int main() {
+  pthread_t writers[SIZE];
+  pthread_t readers[SIZE];
+  int args[SIZE];
+
+  // Initialize rand seed
+  srand(time(NULL));
+
+  // Initialize locks
+  int res = pthread_mutex_init(&rand_mutex, NULL);
+  assert(res == 0);
+  for (int i = 0; i < SIZE; ++i) {
+    res = pthread_rwlock_init(&locks[i], NULL);
+    assert(res == 0);
+  }
+
+  // Create all threads
+  for (int i = 0; i < SIZE; ++i) {
+    args[i] = i;
+    pthread_create(&writers[i], NULL, write_value, &args[i]);
+    pthread_create(&readers[i], NULL, read_value, &args[i]);
+  }
+
+  // Wait for completion
+  for (int i = 0; i < SIZE; ++i) {
+    pthread_join(writers[i], NULL);
+    pthread_join(readers[i], NULL);
+  }
+
+  return 0;
+}