Fix pattern AndBool and friends that did not match the _andBool_ …

…symbol (#476)

Summary of changes:
* correct the pattern synonyms in `Booster.Pattern.Bool` by including
the `hook` attribute to the hooked symbols
- the absence of the attribute in i.e. `AndBool` pattern synonym caused
it to *not match* the `_andBool_` symbols from rules's requires clauses;
- that caused the conjunction splitting functions `splitAndBool` and
`splitBoolPredicates` to have no effect, potentially blocking rule
applications.
* add unit-tests for these pattern synonyms in
`Test.Booster.Pattern.Bool`
- the test internalize the symbols from surface KORE using the
quasi-quoter and test that the internalized symbols are indeed matched
by the pattern synonyms.
* change the hook name to be represented as `ByteString` (not `Text`)
- having both BS and Text causes issues when parsing symbols with both
hook and smt-hook attributes using the quasi-quoter
- that triggered the need to regenerate the responses in
`test-foundry-bug-report`

TODO:

- [x] run KEVM performance tests and post results
- [x] run Kontrol performance tests and post results

---------

Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

library/Booster/Builtin.hs

@@ -13,6 +13,7 @@ module Booster.Builtin (
 
 import Control.Monad
 import Control.Monad.Trans.Except
+import Data.ByteString.Char8 (ByteString)
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Text (Text)
@@ -27,19 +28,19 @@ import Booster.Prettyprinter
 -- partial (returning a Maybe type)
 type BuiltinFunction = [Term] -> Except Text (Maybe Term)
 
-hooks :: Map Text BuiltinFunction
+hooks :: Map ByteString BuiltinFunction
 hooks =
     Map.unions
         [ builtinsKEQUAL
         ]
 
 ------------------------------------------------------------
-(~~>) :: Text -> BuiltinFunction -> (Text, BuiltinFunction)
+(~~>) :: ByteString -> BuiltinFunction -> (ByteString, BuiltinFunction)
 (~~>) = (,)
 
 ------------------------------------------------------------
 -- KEQUAL hooks
-builtinsKEQUAL :: Map Text BuiltinFunction
+builtinsKEQUAL :: Map ByteString BuiltinFunction
 builtinsKEQUAL =
     Map.fromList
         [ "KEQUAL.ite" ~~> iteHook

library/Booster/Definition/Attributes/Base.hs

@@ -201,7 +201,7 @@ data SymbolAttributes = SymbolAttributes
     , hasEvaluators :: Flag "canBeEvaluated"
     , collectionMetadata :: Maybe KCollectionMetadata
     , smt :: Maybe SMTType
-    , hook :: Maybe Text
+    , hook :: Maybe ByteString
     }
     deriving stock (Eq, Ord, Show, Generic, Data, Lift)
     deriving anyclass (NFData, Hashable)

library/Booster/Definition/Attributes/Reader.hs

@@ -179,6 +179,9 @@ instance HasAttributes ParsedSymbol where
                         pure . Just . SMTLib $ encodeUtf8 txt
                     (Nothing, Nothing) ->
                         pure Nothing
+            hook = do
+                hooked <- attributes .:? "hook"
+                pure (encodeUtf8 <$> hooked)
 
         SymbolAttributes
             <$> symbolType
@@ -188,7 +191,7 @@ instance HasAttributes ParsedSymbol where
             <*> hasConcreteEvaluators
             <*> pure Nothing
             <*> smt
-            <*> (attributes .:? "hook")
+            <*> hook
 
 instance HasAttributes ParsedSort where
     type Attributes ParsedSort = SortAttributes

library/Booster/Pattern/ApplyEquations.hs

@@ -51,6 +51,7 @@ import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text, pack)
 import Data.Text qualified as Text
+import Data.Text.Encoding qualified as Text
 import Prettyprinter
 
 import Booster.Builtin as Builtin
@@ -541,7 +542,7 @@ applyAtTop pref term = do
                 | Just hook <- flip Map.lookup Builtin.hooks =<< sym.attributes.hook -> do
                     logOther (LevelOther "Simplify") $
                         "Calling hooked function "
-                            <> fromJust sym.attributes.hook
+                            <> (Text.decodeUtf8 $ fromJust sym.attributes.hook)
                             <> " for "
                             <> renderText (pretty term)
                     either (throw . InternalError) checkChanged

library/Booster/Pattern/Bool.hs

@@ -24,7 +24,6 @@ module Booster.Pattern.Bool (
 ) where
 
 import Data.ByteString.Char8 (ByteString)
-import Data.Text (Text)
 
 import Booster.Definition.Attributes.Base (
     SMTType (SMTHook),
@@ -52,20 +51,20 @@ import Booster.Pattern.Base (
 import Booster.Pattern.Util (isConcrete)
 import Booster.SMT.Base (SExpr (Atom), SMTId (..))
 
-pattern TotalFunctionWithSMT :: ByteString -> SymbolAttributes
-pattern TotalFunctionWithSMT hook =
+pattern HookedTotalFunction :: ByteString -> SymbolAttributes
+pattern HookedTotalFunction hook =
     SymbolAttributes
         TotalFunction
         IsNotIdem
         IsNotAssoc
         IsNotMacroOrAlias
         CanBeEvaluated
         Nothing
-        (Just (SMTHook (Atom (SMTId hook))))
         Nothing
+        (Just hook)
 
-pattern HookedFunctionWithSMT :: Text -> ByteString -> SymbolAttributes
-pattern HookedFunctionWithSMT hook smt =
+pattern HookedTotalFunctionWithSMT :: ByteString -> ByteString -> SymbolAttributes
+pattern HookedTotalFunctionWithSMT hook smt =
     SymbolAttributes
         TotalFunction
         IsNotIdem
@@ -84,7 +83,7 @@ pattern AndBool l r =
                 []
                 [SortBool, SortBool]
                 SortBool
-                (TotalFunctionWithSMT "and")
+                (HookedTotalFunctionWithSMT "BOOL.and" "and")
             )
         []
         [l, r]
@@ -97,7 +96,7 @@ pattern NotBool t =
                 []
                 [SortBool]
                 SortBool
-                (TotalFunctionWithSMT "not")
+                (HookedTotalFunctionWithSMT "BOOL.not" "not")
             )
         []
         [t]
@@ -110,7 +109,7 @@ pattern EqualsInt a b =
                 []
                 [SortInt, SortInt]
                 SortBool
-                (TotalFunctionWithSMT "=")
+                (HookedTotalFunctionWithSMT "INT.eq" "=")
             )
         []
         [a, b]
@@ -121,7 +120,7 @@ pattern EqualsBool a b =
                 []
                 [SortBool, SortBool]
                 SortBool
-                (TotalFunctionWithSMT "=")
+                (HookedTotalFunctionWithSMT "BOOL.eq" "=")
             )
         []
         [a, b]
@@ -132,7 +131,7 @@ pattern NEqualsInt a b =
                 []
                 [SortInt, SortInt]
                 SortBool
-                (TotalFunctionWithSMT "distinct")
+                (HookedTotalFunctionWithSMT "INT.ne" "distinct")
             )
         []
         [a, b]
@@ -143,7 +142,7 @@ pattern EqualsK a b =
                 []
                 [SortK, SortK]
                 SortBool
-                (HookedFunctionWithSMT "KEQUAL.eq" "=")
+                (HookedTotalFunctionWithSMT "KEQUAL.eq" "=")
             )
         []
         [a, b]
@@ -154,16 +153,7 @@ pattern SetIn a b =
                 []
                 [SortKItem, SortSet]
                 SortBool
-                ( SymbolAttributes
-                        TotalFunction
-                        IsNotIdem
-                        IsNotAssoc
-                        IsNotMacroOrAlias
-                        CanBeEvaluated
-                        Nothing
-                        Nothing
-                        Nothing
-                    )
+                (HookedTotalFunction "SET.in")
             )
         []
         [a, b]
@@ -174,7 +164,7 @@ pattern NEqualsK a b =
                 []
                 [SortK, SortK]
                 SortBool
-                (HookedFunctionWithSMT "KEQUAL.ne" "distinct")
+                (HookedTotalFunctionWithSMT "KEQUAL.ne" "distinct")
             )
         []
         [a, b]

package.yaml

@@ -207,3 +207,22 @@ tests:
       - process
       - text
       - transformers
+
+  predicates-integration:
+    source-dirs: test/predicates-integration
+    main: Main.hs
+    dependencies:
+      - base
+      - bytestring
+      - containers
+      - filepath
+      - tasty
+      - tasty-golden
+      - tasty-hunit
+      - tasty-test-reporter
+      - hspec-hedgehog
+      - hs-backend-booster
+      - kore-rpc-types
+      - process
+      - text
+      - transformers