diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..a7a4484 --- /dev/null +++ b/Dockerfile @@ -0,0 +1,3 @@ +FROM framac/frama-c:dev +COPY entrypoint.sh /entrypoint.sh +ENTRYPOINT ["/entrypoint.sh"] diff --git a/README.md b/README.md new file mode 100644 index 0000000..6a9b240 --- /dev/null +++ b/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 .eva`, + where `` 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 `` 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 `` 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 !** diff --git a/action.yml b/action.yml new file mode 100644 index 0000000..005b6b1 --- /dev/null +++ b/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 }} diff --git a/actions-tab.png b/actions-tab.png new file mode 100644 index 0000000..d1bc187 Binary files /dev/null and b/actions-tab.png differ diff --git a/entrypoint.sh b/entrypoint.sh new file mode 100755 index 0000000..b75c2ec --- /dev/null +++ b/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" diff --git a/workflow-example.yml b/workflow-example.yml new file mode 100644 index 0000000..a877a86 --- /dev/null +++ b/workflow-example.yml @@ -0,0 +1,28 @@ +# replace 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: '.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/.sarif