Action: parse, run Eva, display alarm count + coverage, build SARIF r…

…eport

Dockerfile

@@ -0,0 +1,3 @@
+FROM framac/frama-c:dev
+COPY entrypoint.sh /entrypoint.sh
+ENTRYPOINT ["/entrypoint.sh"]

README.md

@@ -0,0 +1,119 @@
+# Frama-C/Eva: sound analysis of possible runtime errors
+
+The open-source [Frama-C](http://frama-c.com/) platform performs sound analyses
+of C code bases based on different techniques.
+
+This Github action uses the [Eva plug-in](http://frama-c.com/value.html)
+for a mostly automatic analysis of runtime errors.
+Its purpose is to extensively list all possible undefined behaviors in the code.
+
+Note that, unlike many syntactic analyzers, Frama-C's deep semantic analysis
+requires a considerable amount of information concerning the code and the
+underlying architecture to give best results. Also, unlike *bug finders*,
+which do not guarantee to be exhaustive, Frama-C intends to list *all* possible
+issues in the code.
+
+This action intends to help users already familiar with the platform to
+automatically setup their C code bases so that Frama-C will run after each
+commit.
+
+If you are not familiar with the Frama-C platform, consider reading the
+[Eva User Manual and Tutorial](http://frama-c.com/download/frama-c-eva-manual.pdf).
+
+In technical terms, this action uses a
+[Docker image of Frama-C](https://hub.docker.com/r/framac/frama-c/tags)
+to parse and analyze a code base with Eva. After the analysis, it produces a
+[SARIF](https://www.oasis-open.org/committees/tc_home.php?wg_abbrev=sarif)
+report as artifact.
+
+## Inputs
+
+### `fc-dir`
+
+Directory containing the Frama-C makefile. Default: `.frama-c`.
+
+### `fc-makefile`
+
+Name of the Makefile for Frama-C. Must be inside `fc-dir`.
+Default: `GNUmakefile`.
+
+### `eva-target`
+
+**Required** Name of the Eva target in the Makefile. Default: `main.eva`.
+
+## Outputs
+
+### `alarm-count`
+
+Number of alarms reported by Eva.
+
+### `coverage`
+
+Eva coverage estimation (%).
+
+## Installation and usage
+
+### Setting up the workflow on a C repository
+
+#### With Frama-C 22 (or newer) installed
+
+1. In the base directory of your C repository, run
+   `frama-c-script make-template` to interactively fill an analysis
+   template. It will be created in `.frama-c/GNUmakefile`.
+
+2. Run the analysis, to make sure it works: `make <target>.eva`,
+   where `<target>` is the name you chose when filling the template.
+   If necessary, you can adjust `.frama-c/GNUmakefile` to fine-tune the
+   analysis.
+
+3. Copy the [workflow-example.yml](workflow-example.yml) file to your
+   `.github/workflows/main.yml`, replacing `<target>` with the name you chose
+   in step 1.
+
+4. Commit the changes to your project, and push them to Github.
+
+#### Without Frama-C installed (possible, but harder to setup if you never used Frama-C in your project)
+
+1. Create a `.frama-c` directory in the root of your Github clone.
+
+2. Copy a template Makefile from [here](https://git.frama-c.com/pub/frama-c/-/blob/master/share/analysis-scripts/template.mk) and put it in `.frama-c`.
+   You should name it `GNUmakefile`.
+
+3. Open the Makefile and replace `main.eva` with an appropriate name
+   (e.g. `monocypher.eva`).
+   Also rename `main.parse` accordingly (e.g. `monocypher.parse`) and
+   add the list of sources, *relative to the `.frama-c` directory*
+   (e.g. `monocypher.parse: ../file1.c ../file2.c ...`).
+
+4. (Optional) If necessary, add preprocessing flags in `CPPFLAGS`.
+   If you are familiar with Frama-C/Eva, you can also edit `EVAFLAGS` to
+   improve precision, add stubs, etc.
+
+5. Copy the [workflow-example.yml](workflow-example.yml) file to your
+   `.github/workflows/main.yml`, replacing `<target>` with the name you chose
+   in step 3.
+
+6. Commit the changes to your project, and push them to Github.
+
+### Viewing the results
+
+You should see an Actions tab in your project, with the Frama-C/Eva workflow,
+as in the image below.
+
+![Actions tab and workflows](actions-tab.png)
+
+After each push to `master`, Github will run the workflow.
+
+If the action runs successfully, an artifact (report.sarif) will be available
+for the run. You can open it using a SARIF viewer, such as Microsoft's
+[VSCode plug-in](https://marketplace.visualstudio.com/items?itemName=MS-SarifVSCode.sarif-viewer).
+
+You can also click on `run_eva`, in the left tab, to see a text log of the
+entire run.
+
+### Practical example
+
+A practical example of usage of this action is available at the following repository:
+https://github.com/maroneze/Monocypher
+
+**Have fun with Frama-C !**

action.yml

@@ -0,0 +1,31 @@
+# action.yml
+name: 'Frama-C-Eva'
+description: 'Sound analysis of C code with the open-source platform Frama-C: exhaustively list possible runtime errors'
+branding:
+  icon: 'facebook'
+  color: 'orange'
+inputs:
+  fc-dir:
+    description: 'Directory containing the Frama-C makefile (default: .frama-c)'
+    required: false
+    default: '.frama-c'
+  fc-makefile:
+    description: 'Makefile for Frama-C (must be inside [fc-dir])'
+    required: false
+    default: 'GNUmakefile'
+  eva-target:
+    description: 'Name of the Eva target in the makefile'
+    required: true
+    default: 'main.eva'
+outputs:
+  alarm-count:
+    description: 'Number of alarms reported by Eva'
+  coverage:
+    description: 'Eva coverage estimation (%)'
+runs:
+  using: 'docker'
+  image: 'Dockerfile'
+  args:
+    - ${{ inputs.fc-dir }}
+    - ${{ inputs.fc-makefile }}
+    - ${{ inputs.eva-target }}

entrypoint.sh

@@ -0,0 +1,44 @@
+#!/bin/bash -e
+
+echo "Frama-C/Eva action entrypoint, displaying environment information"
+echo "PWD=$PWD"
+
+if [ $# -ne 3 ]; then
+    echo "error: expected 3 arguments: fc-dir, fc-makefile and eva-target"
+    exit 1
+fi
+
+fc_dir="$1"
+fc_makefile="$2"
+target="${3%.eva}"
+
+if [ ! -f "$fc_dir/$fc_makefile" ]; then
+    echo "error: file not found: $fc_dir/$fc_makefile"
+    exit 1
+fi
+
+eval $(opam env)
+
+echo "Parsing files: running target ${target}.parse"
+
+# '-B' ensures that existing/versioned files will not prevent a rebuild
+make -B -C "$fc_dir" -f "$fc_makefile" "${target}.parse"
+
+echo "Running Eva: running target ${target}.eva"
+
+make -C "$fc_dir" -f "$fc_makefile" "${target}.eva"
+
+# output Eva summary
+cd "$fc_dir"
+summary=$(mktemp eva_summary_XXX.log)
+sed -n -e '/====== ANALYSIS SUMMARY ======/,/\[metrics\] Eva coverage statistics/{/\[metrics\] Eva coverage statistics/!p}' "${target}.eva/eva.log" > $summary
+
+alarm_count=$(wc -l "${target}.eva/alarms.csv" | cut -d' ' -f1)
+coverage=$(grep "Coverage estimation" "${target}.eva/metrics.log" | cut -d'=' -f2)
+
+echo "::set-output name=alarm-count::$alarm_count"
+echo "::set-output name=coverage::$coverage"
+
+# Produce SARIF report
+
+frama-c -load "${target}.eva"/framac.sav -mdr-gen sarif -mdr-no-print-libc -mdr-out "${target}.sarif"

workflow-example.yml

@@ -0,0 +1,28 @@
+# replace <target> with the target name in your GNUmakefile
+
+name: Frama-C-Eva-SARIF
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+jobs:
+  run_eva:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v2
+    - name: Run Frama-C/Eva
+      id: eva
+      uses: Frama-C/github-action-eva-sarif@v1
+      with:
+        eva-target: '<target>.eva'
+    - name: Alarm count
+      run: echo "Eva reported ${{ steps.eva.outputs.alarm-count }}"
+    - name: Eva coverage estimation
+      run: echo "Eva coverage estimation:${{ steps.eva.outputs.coverage }}"
+    - uses: actions/upload-artifact@v2
+      with:
+        name: report.sarif
+        path: ${{ github.workspace }}/.frama-c/<target>.sarif