"Fix" unit tests by ignoring rule predicate and substitution

Adapt test-3934-smt
runtimeverification · Oct 15, 2024 · 0935540 · 0935540
1 parent c97e13d
commit 0935540
Show file tree

Hide file tree

Showing 8 changed files with 13,085 additions and 60,451 deletions.
diff --git a/booster/test/rpc-integration/resources/3934-smt.kompile b/booster/test/rpc-integration/resources/3934-smt.kompile
@@ -2,7 +2,6 @@ set -eux
 
 SCRIPT_DIR=$(dirname $0)
 PLUGIN_DIR=${PLUGIN_DIR:-""}
-SECP=${SECP256K1_DIR:-/usr}
 
 
 if [ -z "$PLUGIN_DIR" ]; then
@@ -19,7 +18,6 @@ else
     PLUGIN_CPP="${PLUGIN_DIR}/include/plugin-c/crypto.cpp ${PLUGIN_DIR}/include/plugin-c/plugin_util.cpp"
 fi
 
-SECP_OPTS="-I${SECP}/include -L${SECP}/lib"
 
 NAME=$(basename ${0%.tar.gz.kompile})
 NAMETGZ=$(basename ${0%.kompile})
@@ -42,7 +40,7 @@ esac
 llvm-kompile 3934-smt.llvm.kore ./dt c -- \
              -fPIC -std=c++17 -o interpreter \
              $PLUGIN_LIBS $PLUGIN_INCLUDE $PLUGIN_CPP \
-             -lcrypto -lssl $LPROCPS ${SECP_OPTS}
+             -lcrypto -lssl $LPROCPS -lsecp256k1
 
 mv interpreter.* 3934-smt.dylib
 

diff --git a/booster/test/rpc-integration/resources/3934-smt.kore b/booster/test/rpc-integration/resources/3934-smt.kore
diff --git a/booster/test/rpc-integration/test-3934-smt/response-003.booster-dev b/booster/test/rpc-integration/test-3934-smt/response-003.booster-dev
diff --git a/booster/test/rpc-integration/test-3934-smt/response-005.booster-dev b/booster/test/rpc-integration/test-3934-smt/response-005.booster-dev
diff --git a/booster/test/rpc-integration/test-3934-smt/response-007.booster-dev b/booster/test/rpc-integration/test-3934-smt/response-007.booster-dev
diff --git a/booster/test/rpc-integration/test-3934-smt/response-008.booster-dev b/booster/test/rpc-integration/test-3934-smt/response-008.booster-dev
diff --git a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs
@@ -172,6 +172,12 @@ testConf = do
             , terminalLabels = []
             }
 
+ignoreRulePredicateAndSubst :: RewriteResult Pattern -> RewriteResult Pattern
+ignoreRulePredicateAndSubst =
+    \case
+        RewriteBranch pre posts -> RewriteBranch pre (NE.map (\(lbl, uid, p, _, _) -> (lbl, uid, p, Nothing, mempty)) posts)
+        other -> other
+
 ----------------------------------------
 errorCases
     , rewriteSuccess
@@ -244,7 +250,7 @@ rulePriority =
 
 runWith :: Term -> IO (Either (RewriteFailed "Rewrite") (RewriteResult Pattern))
 runWith t =
-    second fst <$> do
+    second (ignoreRulePredicateAndSubst . fst) <$> do
         conf <- testConf
         runNoLoggingT $ runRewriteT conf mempty (rewriteStep [] [] $ Pattern_ t)
 
@@ -260,7 +266,10 @@ branchesTo :: Term -> [(Text, Term)] -> IO ()
 t `branchesTo` ts =
     runWith t
         @?>>= Right
-            (RewriteBranch (Pattern_ t) $ NE.fromList $ map (\(lbl, t') -> (lbl, mockUniqueId, Pattern_ t')) ts)
+            ( RewriteBranch (Pattern_ t) $
+                NE.fromList $
+                    map (\(lbl, t') -> (lbl, mockUniqueId, Pattern_ t', Nothing, mempty)) ts
+            )
 
 failsWith :: Term -> RewriteFailed "Rewrite" -> IO ()
 failsWith t err =
@@ -276,7 +285,7 @@ runRewrite t = do
         runNoLoggingT $
             performRewrite conf $
                 Pattern_ t
-    pure (counter, fmap (.term) res)
+    pure (counter, fmap (.term) (ignoreRulePredicateAndSubst res))
 
 aborts :: RewriteFailed "Rewrite" -> Term -> IO ()
 aborts failure t = runRewrite t >>= (@?= (0, RewriteAborted failure t))
@@ -306,11 +315,15 @@ canRewrite =
                     ( "con1-f2"
                     , mockUniqueId
                     , [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |]
+                    , Nothing
+                    , mempty
                     )
                 branch2 =
                     ( "con1-f1'"
                     , mockUniqueId
                     , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}(    f1{}(   \dv{SomeSort{}}("somethingElse")                                   ) ), C:SortK{}) ) |]
+                    , Nothing
+                    , mempty
                     )
 
             rewrites
@@ -399,11 +412,15 @@ supportsDepthControl =
                     ( "con1-f2"
                     , mockUniqueId
                     , [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |]
+                    , Nothing
+                    , mempty
                     )
                 branch2 =
                     ( "con1-f1'"
                     , mockUniqueId
                     , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}(    f1{}(   \dv{SomeSort{}}("somethingElse")                                   ) ), C:SortK{}) ) |]
+                    , Nothing
+                    , mempty
                     )
 
             rewritesToDepth
@@ -419,7 +436,7 @@ supportsDepthControl =
         conf <- testConf
         (counter, _, res) <-
             runNoLoggingT $ performRewrite conf{mbMaxDepth = Just depth} $ Pattern_ t
-        (counter, fmap (.term) res) @?= (n, f t')
+        (counter, fmap (.term) (ignoreRulePredicateAndSubst res)) @?= (n, f t')
 
 supportsCutPoints :: TestTree
 supportsCutPoints =
@@ -452,11 +469,15 @@ supportsCutPoints =
                     ( "con1-f2"
                     , mockUniqueId
                     , [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |]
+                    , Nothing
+                    , mempty
                     )
                 branch2 =
                     ( "con1-f1'"
                     , mockUniqueId
                     , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}(    f1{}(   \dv{SomeSort{}}("somethingElse")                                   ) ), C:SortK{}) ) |]
+                    , Nothing
+                    , mempty
                     )
 
             rewritesToCutPoint
@@ -474,7 +495,7 @@ supportsCutPoints =
             runNoLoggingT $
                 performRewrite conf{cutLabels = [lbl]} $
                     Pattern_ t
-        (counter, fmap (.term) res) @?= (n, f t')
+        (counter, fmap (.term) (ignoreRulePredicateAndSubst res)) @?= (n, f t')
 
 supportsTerminalRules :: TestTree
 supportsTerminalRules =

diff --git a/scripts/booster-integration-tests.sh b/scripts/booster-integration-tests.sh
@@ -28,9 +28,6 @@ for dir in $(ls -d test-*); do
     name=${dir##test-}
     echo "Running $name..."
     case "$name" in
-        "3934-smt")
-	    continue
-            ;;
         "a-to-f" | "diamond")
             SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
             SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@
@@ -40,7 +37,7 @@ for dir in $(ls -d test-*); do
             SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@
             SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@
             ;;
-        "get-model" | "collectiontest" | "implies" | "implies2" | "implies-issue-3941" | "remainder-predicates" | "use-path-condition-in-equations" | "issue3764-vacuous-branch")
+        "get-model" | "collectiontest" | "implies" | "implies2" | "implies-issue-3941" | "remainder-predicates" | "use-path-condition-in-equations" | "issue3764-vacuous-branch" | "3934-smt")
             SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
             SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@
             ;;