From 1aee3b40f2b4d502163b105ecd7ea552dc343d14 Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Thu, 27 Apr 2023 23:01:25 +0200
Subject: [PATCH] Merge branch 'CI/FV/run-on-ACMR' into fv/ERC20Votes

---
 .github/workflows/formal-verification.yml | 14 ++++-
 certora/run.js                            | 64 ++++++++++++++++-------
 certora/specs/Ownable.spec                |  4 +-
 3 files changed, 61 insertions(+), 21 deletions(-)

diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml
index 29c02541c..833d02619 100644
--- a/.github/workflows/formal-verification.yml
+++ b/.github/workflows/formal-verification.yml
@@ -33,8 +33,20 @@ jobs:
     if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification')
     steps:
       - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
       - name: Set up environment
         uses: ./.github/actions/setup
+      - name: identify specs that need to be run
+        id: arguments
+        run: |
+          if [[ ${{ github.event_name }} = 'pull_request' ]];
+          then
+            RESULT=$(git diff ${{ github.event.pull_request.head.sha }}..${{ github.event.pull_request.base.sha }} --name-only certora/specs/*.spec | while IFS= read -r file; do [[ -f $file ]] && basename "${file%.spec}"; done)
+          else
+            RESULT='--all'
+          fi
+          echo "result=$RESULT" >> "$GITHUB_OUTPUT"
       - name: Install python
         uses: actions/setup-python@v4
         with:
@@ -55,6 +67,6 @@ jobs:
       - name: Verify specification
         run: |
           make -C certora apply
-          node certora/run.js >> "$GITHUB_STEP_SUMMARY"
+          node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY"
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/certora/run.js b/certora/run.js
index f3234c1a3..2dc7d0181 100644
--- a/certora/run.js
+++ b/certora/run.js
@@ -1,37 +1,65 @@
 #!/usr/bin/env node
 
 // USAGE:
-//    node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...]
+//    node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH]
 // EXAMPLES:
+//    node certora/run.js --all
 //    node certora/run.js AccessControl
 //    node certora/run.js AccessControlHarness:AccessControl
 
-const MAX_PARALLEL = 4;
-
-let specs = require(__dirname + '/specs.json');
-
 const proc = require('child_process');
 const { PassThrough } = require('stream');
 const events = require('events');
-const limit = require('p-limit')(MAX_PARALLEL);
 
-let [, , request = '', ...extraOptions] = process.argv;
-if (request.startsWith('-')) {
-  extraOptions.unshift(request);
-  request = '';
+const argv = require('yargs')
+  .env('')
+  .options({
+    all: {
+      alias: 'a',
+      type: 'boolean',
+    },
+    spec: {
+      alias: 's',
+      type: 'string',
+      default: __dirname + '/specs.json',
+    },
+    parallel: {
+      alias: 'p',
+      type: 'number',
+      default: 4,
+    },
+    options: {
+      alias: 'o',
+      type: 'array',
+      default: [],
+    },
+  }).argv;
+
+function match(entry, request) {
+  const [reqSpec, reqContract] = request.split(':').reverse();
+  return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract);
 }
 
-if (request) {
-  const [reqSpec, reqContract] = request.split(':').reverse();
-  specs = Object.values(specs).filter(s => reqSpec === s.spec && (!reqContract || reqContract === s.contract));
-  if (specs.length === 0) {
-    console.error(`Error: Requested spec '${request}' not found in specs.json`);
-    process.exit(1);
+const specs = require(argv.spec).filter(s => argv.all || argv._.some(r => match(s, r)));
+const limit = require('p-limit')(argv.parallel);
+
+if (argv._.length == 0 && !argv.all) {
+  console.error(`Warning: No specs requested. Did you forgot to toggle '--all'?`);
+}
+
+for (const r of argv._) {
+  if (!specs.some(s => match(s, r))) {
+    console.error(`Error: Requested spec '${r}' not found in ${argv.spec}`);
+    process.exitCode = 1;
   }
 }
 
-for (const { spec, contract, files, options = [] } of Object.values(specs)) {
-  limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]);
+if (process.exitCode) {
+  process.exit(process.exitCode);
+}
+
+for (const { spec, contract, files, options = [] } of specs) {
+  limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]);
 }
 
 // Run certora, aggregate the output and print it at the end
diff --git a/certora/specs/Ownable.spec b/certora/specs/Ownable.spec
index 48bd84d13..4fdfeb09c 100644
--- a/certora/specs/Ownable.spec
+++ b/certora/specs/Ownable.spec
@@ -62,10 +62,10 @@ rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
 │ Rule: ownership can only change in specific ways                                                                    │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e, method f) {
+rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
     address oldCurrent = owner();
 
-    calldataarg args;
+    method f; calldataarg args;
     f(e, args);
 
     address newCurrent = owner();