Add argo submodule and build

.github/ci.sh

@@ -10,7 +10,7 @@ mkdir -p "$BIN"
 is_exe() { [[ -x "$1/$2$EXT" ]] || command -v "$2" > /dev/null 2>&1; }
 
 extract_exe() {
-  exe="$(cabal v2-exec which "$1$EXT")"
+  exe="$(find dist-newstyle -type f -name "$1$EXT")"
   name="$(basename "$exe")"
   echo "Copying $name to $2"
   mkdir -p "$2"
@@ -38,9 +38,10 @@ retry() {
 }
 
 setup_dist_bins() {
-  is_exe "dist/bin" "saw" && is_exe "dist/bin" "jss" && return
+  is_exe "dist/bin" "saw" && is_exe "dist/bin" "jss" && is_exe "dist/bin" "saw-remote-api" && return
   extract_exe "saw" "dist/bin"
   extract_exe "jss" "dist/bin"
+  extract_exe "saw-remote-api" "dist/bin"
   export PATH=$PWD/dist/bin:$PATH
   echo "::add-path::$PWD/dist/bin"
   strip dist/bin/saw* || echo "Strip failed: Ignoring harmless error"
@@ -117,12 +118,12 @@ build() {
   ghc_ver="$(ghc --numeric-version)"
   cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
   cabal v2-update
-  cabal v2-configure -j2 --minimize-conflict-set
+  echo "allow-newer: all" >> cabal.project.local
   tee -a cabal.project > /dev/null < cabal.project.ci
-  if ! retry cabal v2-build "$@" saw jss && [[ "$RUNNER_OS" == "macOS" ]]; then
+  if ! retry cabal v2-build "$@" jss saw saw-remote-api && [[ "$RUNNER_OS" == "macOS" ]]; then
     echo "Working around a dylib issue on macos by removing the cache and trying again"
     cabal v2-clean
-    retry cabal v2-build "$@" saw jss
+    retry cabal v2-build "$@" jss saw saw-remote-api
   fi
 }
 
@@ -150,7 +151,6 @@ install_system_deps() {
 }
 
 test_dist() {
-  setup_dist_bins
   find_java
   pushd intTests
   for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_examples test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done
@@ -171,7 +171,6 @@ bundle_files() {
   cp deps/abcBridge/abc-build/copyright.txt dist/ABC_LICENSE
   cp LICENSE README.md dist/
   $IS_WIN || chmod +x dist/bin/*
-  rm -f "dist/bin/jss"
 
   cp doc/extcore.md dist/doc
   cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf

.github/workflows/build.yml

@@ -53,11 +53,17 @@ jobs:
           git submodule update --init
           git -C deps/abcBridge submodule update --init
 
+      - uses: actions/setup-python@v2
+        with:
+          python-version: '3.x'
+
+      - shell: bash
+        run: pip3 install virtualenv
+
       - uses: actions/setup-haskell@v1
         id: setup-haskell
         with:
           ghc-version: ${{ matrix.ghc }}
-          enable-stack: true
 
       - uses: actions/cache@v2
         name: Cache cabal store
@@ -82,6 +88,16 @@ jobs:
           CVC4_VERSION: "4.1.8"
           YICES_VERSION: "2.6.2"
 
+      - shell: bash
+        run: .github/ci.sh setup_dist_bins
+
+      - shell: bash
+        # TODO: change this once we can get these tests working in CI
+        continue-on-error: true
+        run: cabal v2-test saw-remote-api
+        env:
+          SAW_SERVER: ${GITHUB_WORKSPACE}/dist/bin/saw-remote-api
+
       - uses: actions/setup-java@v1
         with:
           java-version: "8"
@@ -93,8 +109,6 @@ jobs:
         continue-on-error: ${{ matrix.continue-on-error }}
         name: Integration Tests
         run: |
-          mkdir -p ~/.stack
-          echo "system-ghc: true" >> ~/.stack/config.yaml
           .github/ci.sh test_dist
 
       - if: >-

.gitmodules

@@ -49,3 +49,6 @@
 [submodule "deps/saw-core-coq"]
 	path = deps/saw-core-coq
 	url = https://github.com/GaloisInc/saw-core-coq.git
+[submodule "deps/argo"]
+	path = deps/argo
+	url = https://github.com/galoisinc/argo

cabal.project

@@ -1,5 +1,6 @@
 packages:
     saw-script.cabal
+    saw-remote-api
     deps/llvm-pretty
     deps/llvm-pretty-bc-parser
     deps/jvm-parser
@@ -29,3 +30,7 @@ packages:
     deps/macaw/x86_symbolic
     deps/elf-edit
     deps/dwarf
+    deps/argo/argo
+    deps/argo/tasty-script-exitcode
+    deps/argo/python
+    deps/cryptol/cryptol-remote-api

saw-remote-api/CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for saw-remote-api
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

saw-remote-api/LICENSE

@@ -0,0 +1,29 @@
+BSD 3-Clause License
+
+Copyright (c) 2019, Galois, Inc.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

saw-remote-api/Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

saw-remote-api/saw-remote-api.cabal

@@ -0,0 +1,112 @@
+cabal-version:       2.4
+-- Initial package description 'saw-remote-api.cabal' generated by 'cabal
+-- init'.  For further documentation, see
+-- http://haskell.org/cabal/users-guide/
+
+name:                saw-remote-api
+version:             0.1.0.0
+-- synopsis:
+-- description:
+-- bug-reports:
+license:             BSD-3-Clause
+license-file:        LICENSE
+author:              Kenny Foner
+maintainer:          [email protected]
+-- copyright:
+category:            Network
+extra-source-files:  CHANGELOG.md
+data-files:          test-scripts/*.py
+                     test-scripts/*.cry
+                     test-scripts/*.bc
+                     test-scripts/*.c
+
+common warnings
+  ghc-options:
+    -Weverything
+    -Wno-missing-exported-signatures
+    -Wno-missing-import-lists
+    -Wno-missed-specialisations
+    -Wno-all-missed-specialisations
+    -Wno-unsafe
+    -Wno-safe
+    -Wno-missing-local-signatures
+    -Wno-monomorphism-restriction
+    -Wno-implicit-prelude
+
+common deps
+  build-depends: base >=4.11.1.0 && <4.15,
+                 abcBridge,
+                 aeson,
+                 argo,
+                 bytestring,
+                 containers >= 0.6 && < 0.7,
+                 cryptol >= 2.8.1,
+                 cryptol-saw-core,
+                 crucible,
+                 crucible-jvm,
+                 cryptonite,
+                 cryptonite-conduit,
+                 directory,
+                 jvm-parser,
+                 jvm-verifier,
+                 lens,
+                 llvm-pretty,
+                 llvm-pretty-bc-parser,
+                 mtl,
+                 parameterized-utils,
+                 saw-core,
+                 saw-script,
+                 silently,
+                 text,
+                 vector >= 0.12 && < 0.13,
+                 cryptol-remote-api
+  default-language: Haskell2010
+
+library
+  import: deps, warnings
+  hs-source-dirs: src
+  exposed-modules: SAWServer,
+                   SAWServer.CryptolExpression,
+                   SAWServer.CryptolSetup,
+                   SAWServer.Data.Contract,
+                   SAWServer.Data.JVMType,
+                   SAWServer.Data.LLVMType,
+                   SAWServer.Data.SetupValue,
+                   SAWServer.Exceptions,
+                   SAWServer.JVMCrucibleSetup,
+                   SAWServer.JVMVerify,
+                   SAWServer.LLVMCrucibleSetup,
+                   SAWServer.LLVMVerify,
+                   SAWServer.NoParams,
+                   SAWServer.OK,
+                   SAWServer.ProofScript,
+                   SAWServer.SaveTerm,
+                   SAWServer.SetOption,
+                   SAWServer.Term,
+                   SAWServer.TopLevel,
+                   SAWServer.TrackFile,
+                   SAWServer.VerifyCommon
+
+executable saw-remote-api
+  import: deps, warnings
+  main-is:             Main.hs
+  build-depends:       saw-remote-api
+  -- other-modules:
+  -- other-extensions:
+  hs-source-dirs: saw-remote-api
+
+test-suite test-saw-remote-api
+  import:              deps, warnings
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             Test.hs
+  other-modules:       Paths_saw_remote_api
+  build-depends:       argo-python,
+                       cryptol-remote-api,
+                       filepath,
+                       process,
+                       quickcheck-instances,
+                       tasty,
+                       tasty-hunit,
+                       tasty-quickcheck,
+                       tasty-script-exitcode

saw-remote-api/saw-remote-api/Main.hs

@@ -0,0 +1,49 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main (main) where
+
+import qualified Data.Aeson as JSON
+import Data.Text (Text)
+
+import Argo
+import Argo.DefaultMain
+
+import SAWServer
+import SAWServer.CryptolSetup
+import SAWServer.JVMCrucibleSetup
+import SAWServer.JVMVerify
+import SAWServer.LLVMCrucibleSetup
+import SAWServer.LLVMVerify
+import SAWServer.ProofScript
+import SAWServer.SaveTerm
+import SAWServer.SetOption
+
+
+main :: IO ()
+main =
+  do theApp <- mkApp initialState sawMethods
+     defaultMain description theApp
+
+description :: String
+description =
+  "An RPC server for SAW."
+
+sawMethods :: [(Text, MethodType, JSON.Value -> Method SAWState JSON.Value)]
+sawMethods =
+  -- Cryptol
+  [ ("SAW/Cryptol/load module",  Command, method cryptolLoadModule)
+  , ("SAW/Cryptol/load file",    Command, method cryptolLoadFile)
+  , ("SAW/Cryptol/save term",    Command, method saveTerm)
+  -- JVM
+  , ("SAW/JVM/load class",       Command, method jvmLoadClass)
+  , ("SAW/JVM/verify",           Command, method jvmVerify)
+  , ("SAW/JVM/assume",           Command, method jvmAssume)
+  -- LLVM
+  , ("SAW/LLVM/load module",     Command, method llvmLoadModule)
+  , ("SAW/LLVM/verify",          Command, method llvmVerify)
+  , ("SAW/LLVM/verify x86",      Command, method llvmVerifyX86)
+  , ("SAW/LLVM/assume",          Command, method llvmAssume)
+  -- General
+  , ("SAW/make simpset",         Command, method makeSimpset)
+  , ("SAW/prove",                Command, method prove)
+  , ("SAW/set option",           Command, method setOption)
+  ]