Merge pull request #358 from GaloisInc/dm/testing-scripts2

Add simple scripting interface to support batch-mode interaction
GaloisInc · Feb 6, 2024 · 5d3d284 · 5d3d284
2 parents 189f3d5 + d223ec5
commit 5d3d284
Show file tree

Hide file tree

Showing 30 changed files with 1,129 additions and 664 deletions.
diff --git a/.env b/.env
@@ -1 +1,2 @@
-export HACKATHON_NOV_2023=$(git rev-parse --show-toplevel)/../Hackathon_November_23
+export HACKATHON_NOV_2023=$(git rev-parse --show-toplevel)/../Hackathon_November_23
+export CHALLENGE_DIR=$(git rev-parse --show-toplevel)/../Challenge-Problems
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -68,6 +68,7 @@ jobs:
         git submodule update --init
         cp cabal.project.dist cabal.project
 
+
     - name: Installing the freeze file
       run: mv cabal.GHC-${{ matrix.ghc }}.freeze cabal.project.freeze
 
@@ -98,12 +99,22 @@ jobs:
       run: |
         sudo apt update
         sudo apt install -y software-properties-common apt-transport-https ca-certificates wget
-        sudo apt install -y curl zlibc zlib1g zlib1g-dev git zip \
+        sudo apt install -y bsdiff curl zlibc zlib1g zlib1g-dev git zip \
           libgmp3-dev build-essential libtinfo-dev autoconf automake gperf cmake locales \
           python3-distutils python-setuptools antlr3 libantlr3c-dev libtool libtool-bin libboost-all-dev python3-pip libfftw3-dev
         sudo locale-gen en_US.UTF-8
         sudo pip3 install toml
 
+    - name: Checkout Challenge Problems
+      env:
+        GITLAB_TOKEN: ${{ secrets.GITLAB_TOKEN }}
+        GITLAB_USER: ${{ env.GITLAB_USER }}
+      run: |
+        export CHALLENGE_DIR=${HOME}/programtargets
+        git clone --depth=1 https://${GITLAB_USER}:${GITLAB_TOKEN}@gitlab-ext.galois.com/pate/programtargets.git ${CHALLENGE_DIR}
+        cd tests
+        make extras
+
     - name: Build pate
       run: |
         cabal configure pkg:pate --write-ghc-environment-files=always --enable-tests -j --allow-newer=base
@@ -117,7 +128,6 @@ jobs:
         YICES_VERSION: "2.6.2"
         CVC4_VERSION: "4.1.8"
 
-
     - name: Test
       if: runner.os == 'Linux'
       run: |

diff --git a/.gitignore b/.gitignore
@@ -19,3 +19,5 @@ dist-profile/
 *.log
 *.hi
 /tools/pate/Main
+/tests/aarch32/scripted/challenge10.original.exe
+/tests/aarch32/scripted/challenge10.patched.exe
diff --git a/demos/may-2023/challenge10/Makefile b/demos/may-2023/challenge10/Makefile
@@ -23,6 +23,7 @@ run: challenge10.patched.exe
 		-r AllowEqRescopeFailure \
 		-s transport_handler \
 		--save-macaw-cfgs CFGs \
+		--script challenge10.pate \
         ${EXTRA_FLAGS}
 
 run_json: EXTRA_FLAGS = --json-toplevel

diff --git a/pate.cabal b/pate.cabal
@@ -26,6 +26,7 @@ common shared
   build-depends:       base >= 4.10 && < 5,
                        aeson >= 2,
                        async >= 2.2 && < 2.3,
+                       ansi-terminal >= 0.7 && <= 1.0,
                        bv-sized >= 1 && < 1.1,
                        bytestring >= 0.9 && < 0.12,
                        containers >= 0.5 && < 0.7,
@@ -79,7 +80,8 @@ common shared
                        time >= 1 && < 2,
                        vector >= 0.10 && < 0.13,
                        th-utilities >= 0.2 && < 0.3,
-                       hashable >= 1.3.5
+                       hashable >= 1.3.5,
+                       optparse-applicative
 
   default-language:    Haskell2010
   ghc-options:         -Wall -Wcompat
@@ -99,6 +101,7 @@ library
                        Pate.Binary,
                        Pate.Block,
                        Pate.Config,
+                       Pate.CLI,
                        Pate.Discovery,
                        Pate.Discovery.PLT,
                        Pate.Discovery.ParsedFunctions
@@ -132,6 +135,7 @@ library
                        Pate.Hints.JSON,
                        Pate.Hints.DWARF,
                        Pate.IOReplay,
+                       Pate.JSONReport,
                        Pate.Location,
                        Pate.Monad,
                        Pate.Monad.Context,
@@ -152,6 +156,7 @@ library
                        Pate.Register.Traversal,
                        Pate.Solver,
                        Pate.SymbolTable,
+                       Pate.Script,
                        Pate.Timeout,
                        Pate.TraceTree,
                        Pate.ExprMappable,
@@ -195,10 +200,12 @@ common shared-test
                  filepath,
                  filemanip,
                  lens,
+                 split,
                  lumberjack,
                  macaw-base,
                  macaw-loader,
                  macaw-symbolic,
+                 optparse-applicative,
                  crucible,
                  crucible-llvm,
                  mtl,
@@ -356,7 +363,6 @@ library pate-base
                        Pate.PPC,
                        Pate.AArch32,
                        Pate.ArchLoader,
-                       JSONReport,
                        Output
   hs-source-dirs:      tools/pate tools arch