207 test tarball runner + tweak rpc client logging

flake.nix

@@ -8,14 +8,18 @@
     haskell-nix.follows = "haskell-backend/haskell-nix";
     nixpkgs.follows = "haskell-backend/haskell-nix/nixpkgs-unstable";
 
+    blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/da834be67f6c0aff11140ddfc0b04561494c14b8";
+    blockchain-k-plugin.inputs.flake-utils.follows = "k-framework/flake-utils";
+    blockchain-k-plugin.inputs.nixpkgs.follows = "k-framework/nixpkgs";
+
     flake-compat = {
       url = "github:edolstra/flake-compat";
       flake = false;
     };
   };
 
   outputs =
-    { self, nixpkgs, haskell-nix, k-framework, haskell-backend, ... }@inputs:
+    { self, nixpkgs, haskell-nix, k-framework, haskell-backend, blockchain-k-plugin, ... }@inputs:
     let
       inherit (nixpkgs) lib;
       perSystem = lib.genAttrs nixpkgs.lib.systems.flakeExposed;
@@ -214,6 +218,7 @@
                 packages."hs-backend-booster:exe:kore-rpc-booster";
               rpc-client = packages."hs-backend-booster:exe:rpc-client";
               inherit (k-framework.packages.${system}) k;
+              blockchain-k-plugin = blockchain-k-plugin.defaultPackage.${system};
             };
         });
 

package.yaml

@@ -131,6 +131,7 @@ executables:
       - extra
       - filepath
       - hs-backend-booster
+      - monad-logger
       - network
       - network-run
       - optparse-applicative

test/rpc-integration/default.nix

@@ -1,4 +1,4 @@
-{ stdenv, coreutils, lib, kore-rpc-booster, rpc-client, git, k }:
+{ stdenv, coreutils, lib, kore-rpc-booster, rpc-client, git, k, blockchain-k-plugin, openssl, procps }:
 
 let
   mkIntegrationTest =
@@ -16,7 +16,8 @@ let
           export ${f}
         '') buildFlags}
         export SERVER=${kore-rpc-booster}/bin/kore-rpc-booster
-        export CLIENT=${rpc-client}/bin/rpc-client
+        export CLIENT="${rpc-client}/bin/rpc-client -l debug"
+        export PLUGIN_DIR=${blockchain-k-plugin}
 
         patchShebangs runDirectoryTest.sh
         ./runDirectoryTest.sh test-${name} --time ${
@@ -46,4 +47,5 @@ in {
   simplify = mkIntegrationTest { name = "simplify"; };
   get-model = mkIntegrationTest { name = "get-model"; };
   issue212 = mkIntegrationTest { name = "issue212"; };
+  foundry-bug-report.tar.gz = mkIntegrationTest { name = "foundry-bug-report.tar.gz"; nativeBuildInputs = [ k openssl procps ]; };
 }

test/rpc-integration/resources/foundry-bug-report.tar.gz.kompile

@@ -0,0 +1,48 @@
+set -eux
+
+SCRIPT_DIR=$(dirname $0)
+PLUGIN_DIR=${PLUGIN_DIR:-""}
+NIX_LIBS=${NIX_LIBS:-""}
+
+
+if [ -z "$PLUGIN_DIR" ]; then
+    echo "PLUGIN_DIR required to link in a crypto plugin dependency"
+    exit 1
+else
+    for lib in libff libcryptopp libsecp256k1; do
+        LIBFILE=$(find ${PLUGIN_DIR} -name "${lib}.a" | head -1)
+        [ -z "$LIBFILE" ] && (echo "[Error] Unable to locate ${lib}.a"; exit 1)
+        PLUGIN_LIBS+="$LIBFILE "
+        PLUGIN_INCLUDE+="-I$(dirname $LIBFILE)/../include "
+    done
+    #PLUGIN_CPP=$(find ${PLUGIN_DIR}/plugin-c -name "*.cpp")
+    PLUGIN_CPP="${PLUGIN_DIR}/include/plugin-c/blake2.cpp ${PLUGIN_DIR}/include/plugin-c/crypto.cpp ${PLUGIN_DIR}/include/plugin-c/plugin_util.cpp"
+fi
+
+NAME=$(basename ${0%.tar.gz.kompile})
+NAMETGZ=$(basename ${0%.kompile})
+
+# unpack definition.kore and llvm_definition from tarball
+# into a directory named after the tarball
+cd $SCRIPT_DIR
+mkdir -p $NAME
+tar xzf ../test-$NAMETGZ -C $NAME definition.kore llvm_definition/
+
+# provide definition
+cp $NAME/definition.kore ${NAMETGZ}.kore
+
+# kompile llvm-definition to interpreter
+
+case "$OSTYPE" in
+  linux*)   LPROCPS="-lprocps" ;;
+  *)        LPROCPS="" ;;
+esac
+
+llvm-kompile $NAME/llvm_definition/definition.kore $NAME/llvm_definition/dt c -- \
+             -fPIC -std=c++17 -o interpreter \
+             $PLUGIN_LIBS $PLUGIN_INCLUDE $PLUGIN_CPP \
+             -lcrypto -lssl $LPROCPS
+mv interpreter.* $NAMETGZ.dylib
+
+# remove temporary artefacts
+rm -r $NAME

test/rpc-integration/runDirectoryTest.sh

@@ -44,7 +44,7 @@ dylib=resources/${dir#test-}.dylib
 echo "Running tests from $dir with definition $kore"
 
 # make sure directory and kore file exist
-[ ! -d "./$dir" ] && exit 1
+[ ! -e "./$dir" ] && exit 1
 if [ ! -f "./$kore" ]; then
   [ ! -f "./$kompile" ] && exit 2
   cd resources
@@ -68,20 +68,25 @@ server_pid=$!
 trap 'kill -2 ${server_pid}; popd' ERR EXIT
 echo "Server PID ${server_pid}"
 
-sleep 2
+sleep 5
 
-for test in $( ls $dir/state-*.{execute,send,simplify,add-module,get-model} 2>/dev/null ); do
-    tmp=${test#$dir/state-}
-    testname=${tmp%.*}
-    # determine send mode from suffix
-    mode=${test##*.}
-    printf "########## Test: %10s %20s\n" "$mode" "$testname #######"
-    if [ -f "$dir/params-${testname}.json" ]; then
-        params="--param-file $dir/params-${testname}.json"
-    else
-        params=""
-    fi
-    # call rpc-client
-    echo "$client $mode $test $params --expect $dir/response-${testname}.json $*"
-    $client $mode $test $params --expect $dir/response-${testname}.json $*
-done
+if [ -d $dir ]; then
+    for test in $( ls $dir/state-*.{execute,send,simplify,add-module,get-model} 2>/dev/null ); do
+        tmp=${test#$dir/state-}
+        testname=${tmp%.*}
+        # determine send mode from suffix
+        mode=${test##*.}
+        printf "########## Test: %10s %20s\n" "$mode" "$testname #######"
+        if [ -f "$dir/params-${testname}.json" ]; then
+            params="--param-file $dir/params-${testname}.json"
+        else
+            params=""
+        fi
+        # call rpc-client
+        echo "$client $mode $test $params --expect $dir/response-${testname}.json $*"
+        $client $mode $test $params --expect $dir/response-${testname}.json $*
+    done
+else
+    echo "$dir is a file, running a tarball test"
+    $client run-tarball $dir
+fi