Merge branch 'feature/basile/eacsl-ensuresec-api' into 'master'

[eacsl] Extend Ensuresec example with a wrapper script to push E-ACSL alerts to a web API

See merge request frama-c/frama-c!3571

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

 build/
+__pycache__/
+.env
\ No newline at end of file

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)
+JSON_OUTPUT_DIR=$(dir $(abspath $(lastword $(MAKEFILE_LIST))))json-output
+PUSH_ALERTS_DIR=$(dir $(abspath $(lastword $(MAKEFILE_LIST))))push-alerts
+
+compile:
+	make -C $(JSON_OUTPUT_DIR) compile
+
+run:
+	make -C $(JSON_OUTPUT_DIR) run
+
+launch_receiver:
+	FLASK_APP=$(PUSH_ALERTS_DIR)/receiver.py FLASK_ENV=development flask run
+
+run_wrapped: compile
+	$(PUSH_ALERTS_DIR)/wrapper.py \
+		--alert-url http://localhost:5000/alert \
+		--id EnsuresecEE \
+		--tool-id EnsuresecEE_EACSL \
+		$(JSON_OUTPUT_DIR)/build/ensuresec_ee.e-acsl
+
+run_wrapped_print_all:
+	make -C $(JSON_OUTPUT_DIR) compile_print_all
+	$(PUSH_ALERTS_DIR)/wrapper.py \
+		--alert-url http://localhost:5000/alert \
+		--id EnsuresecEE \
+		--tool-id EnsuresecEE_EACSL \
+		$(JSON_OUTPUT_DIR)/build/ensuresec_ee_pall.e-acsl

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

@@ -3,9 +3,33 @@
 This folder illustrates the developments done for the European H2020 project
 Ensuresec.
 
+## Usage
+
+The `Makefile` in the root folder provides targets to launch some tests.
+
+- `compile`: Compile the example in folder `json-output`;
+- `run`: Run the example in folder `json-output`;
+- `launch_receiver`: Launch the test server in folder `push-alerts`;
+- `run_wrapped`: Run the example in folder `json-output` wrapped with the script
+  in folder `push-alerts`. The test server must be launched before executing
+  this target.
+- `run_wrapped_print_all`: Same than
+
+When using `make run`, the alerts raised by the example are saved to a JSON file
+in `./json-output/build/ensuresec_ee.json`.
+
+To test pushing alerts to a web API, `make launch_receiver` should be run in a
+secondary terminal. Then `make run_wrapped` can be executed in the primary
+terminal and alerts raised by the example should be visible on the receiver. The
+target `run_wrapped_print_all` will also push valid assertions.
+
 ## Files
 
-### `Makefile`
+### Folder `json-output`
+
+Custom E-ACSL assert to output alerts in a JSON file.
+
+#### `Makefile`
 
 The makefile in the folder provides some targets to test the ensuresec
 developments:
@@ -19,7 +43,7 @@ developments:
 - `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`
+#### `json_assert.c`
 
 The file `json_assert.c` contains an external `__e_acsl_assert()` implementation
 that will print assertion violations to a json file.
@@ -31,8 +55,39 @@ implementation:
 - `ENSURESEC_EE_TOOL_ID`: Ensuresec e-commerce ecosystem tool id
 - `ENSURESEC_OUTPUT_FILE`: json output file
 
-### `ensuresec_ee.c`
+#### `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.
+
+### Folder `push-alerts`
+
+Example of wrapping script to push alerts emitted by the program in
+`json-output` to a specific URL.
+
+#### `wrapper.py`
+
+Wrapper for an E-ACSL monitored executable that will `POST` each raised alert to
+a specific URL. See `./wrapper.py -h` for how to use the script.
+
+Python dependencies:
+
+- `python-dotenv`
+- `python-ijson`
+- `python-requests`
+
+#### `.env-example`
+
+Example `.env` file with environment variables read by `wrapper.py`.
+
+#### `receiver.py`
+
+Test server that listen on URL `http://localhost:5000/alert` for JSON emitted by
+an E-ACSL monitored program and print received alerts to the console output.
+
+Run with `FLASK_APP=receiver.py FLASK_ENV=development flask run`
+
+Python dependencies:
+
+- `python-flask`

src/plugins/e-acsl/examples/ensuresec/json-output/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/ensuresec_ee.c → src/plugins/e-acsl/examples/ensuresec/json-output/ensuresec_ee.c

@@ -89,7 +89,7 @@ static void *read_value(void *arg) {
     usleep(100);
   } while (!idx_written);
 
-  // Acquire a read lock so that the specification can check `writte[idx]` and
+  // Acquire a read lock so that the specification can check `written[idx]` and
   // `values[idx]`.
   pthread_rwlock_rdlock(lock);
   /*@ requires written[idx] == 1;

src/plugins/e-acsl/examples/ensuresec/push-alerts/.env-example

+ENSURESEC_ALERT_URL="http://localhost:5000/alert"
+ENSURESEC_EE_ID="EnsuresecEE"
+ENSURESEC_EE_TOOL_ID="EnsuresecEE_EACSL"

src/plugins/e-acsl/examples/ensuresec/push-alerts/receiver.py

+# -*- coding: utf-8 -*-
+
+# Test server that listen on URL /alert for JSON emitted by a program monitored
+# by E-ACSL and print received alerts to the console output.
+# Run with `FLASK_APP=receiver.py FLASK_ENV=development flask run`
+
+from flask import Flask, request
+
+app = Flask(__name__)
+
+
+@app.post("/alert")
+def add_alert():
+    if request.is_json:
+        alert = request.get_json()
+        content = alert['alert']['data'][0]['jsonContent']
+        print(
+"""{file}: In function '{fct}'
+{file}:{line}: {kind} {verdict}:
+\t{name}{post_name}{predicate}"""
+              .format(
+                  file=content['location']['file'],
+                  fct=content['location']['function'],
+                  line=content['location']['line'],
+                  kind=content['kind'],
+                  verdict=content['verdict'],
+                  name=content['name'],
+                  post_name=":\n\t" if content['name'] else "",
+                  predicate=content['predicate']
+              ))
+        if content['values']:
+            print("\tWith values:")
+            for value in content['values']:
+                print("\t- {}: {}".format(value['name'], value['value']))
+        return {}, 201
+    return {"error": "Request must be JSON."}, 415

src/plugins/e-acsl/examples/ensuresec/push-alerts/wrapper.py

+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+
+# Wrapper for an E-ACSL monitored executable that will POST each raised alert
+# to a specific URL.
+
+import argparse
+import dotenv
+import ijson
+import os
+import requests
+import subprocess
+
+ALERT_URL = 'ENSURESEC_ALERT_URL'
+EE_ID = 'ENSURESEC_EE_ID'
+EE_TOOL_ID = 'ENSURESEC_EE_TOOL_ID'
+
+
+def check_config(value, name):
+    """Check if the given value is empty and exit with an error message if that
+    is the case."""
+    if not value:
+        print("The '{}' option should be provided and not empty.".format(name))
+        exit(1)
+
+
+@ijson.coroutine
+def send_alert(url):
+    """send_alert() is a coroutine that will process E-ACSL alerts as they are
+    emitted by the program. The JSON alerts are POST-ed to the given URL."""
+    while True:
+        alert = (yield)
+        r = requests.post(url, json=alert)
+        if not r.ok:
+            print("Error while sending alert: " + r.text)
+
+
+def main():
+    default = {
+        # Default empty values
+        ALERT_URL: '',
+        EE_ID: '',
+        EE_TOOL_ID: '',
+        # Read configuration from .env file if it exists
+        **dotenv.dotenv_values(".env"),
+        # Overwrite with environment variables
+        **os.environ
+    }
+
+    # Parse script arguments
+    parser = argparse.ArgumentParser(
+        description="Wrapper for an E-ACSL monitored executable that will POST \
+                     each raised alert to a specific URL.")
+    parser.add_argument(
+        'program',
+        help="E-ACSL program to launch and monitor.")
+    parser.add_argument(
+        'args',
+        help="Arguments for the E-ACSL program.",
+        nargs='*')
+    parser.add_argument(
+        '-u', '--alert-url',
+        help="URL where alerts raised by the E-ACSL program must be pushed, \
+              default to environment variable {}.".format(ALERT_URL),
+        metavar='url',
+        default=default[ALERT_URL],
+        dest='alert_url')
+    parser.add_argument(
+        '-i', '--id',
+        help="Ensuresec e-commerce ecosystem id, default to environment \
+              variable {}.".format(EE_ID),
+        metavar='id',
+        default=default[EE_ID],
+        dest='id')
+    parser.add_argument(
+        '-t', '--tool-id',
+        help="Ensuresec e-commerce ecosystem tool id, default to environment \
+              variable {}.".format(EE_TOOL_ID),
+        metavar="id",
+        default=default[EE_TOOL_ID],
+        dest='tool_id')
+    config = parser.parse_args()
+
+    # Check that all necessary configurations have been provided
+    check_config(config.alert_url, 'alert-url')
+    check_config(config.id, 'id')
+    check_config(config.tool_id, 'tool-id')
+
+    # Create an environment for the subprocess with the information either
+    # retrieved from the configuration or the script arguments, and setup
+    # JSON output to stdout
+    env = {'ENSURESEC_EE_ID': config.id,
+           'ENSURESEC_EE_TOOL_ID': config.tool_id,
+           'ENSURESEC_OUTPUT_FILE': '-'}
+    # Launch E-ACSL program as a subprocess
+    p = subprocess.Popen([config.program] + config.args, stdout=subprocess.PIPE,
+                         env=env)
+
+    # Parse output of E-ACSL program as it is produced and use a coroutine to
+    # process JSON objects
+    coro = ijson.items_coro(send_alert(config.alert_url), 'item')
+    for chunk in p.stdout:
+        coro.send(chunk)
+    coro.close()
+
+    # Wait for the end of E-ACSL program
+    p.wait()
+
+
+if __name__ == "__main__":
+    main()