Rule merger: bug fix and better error messages

kore/src/Kore/Exec.hs

@@ -10,7 +10,6 @@ Expose concrete execution as a library
 -}
 module Kore.Exec
     ( exec
-    , extractRules
     , mergeAllRules
     , mergeRulesConsecutiveBatches
     , search
@@ -27,19 +26,27 @@ import Control.Concurrent.MVar
 import Control.DeepSeq
     ( deepseq
     )
-import Control.Error
-    ( note
-    )
 import qualified Control.Lens as Lens
 import Control.Monad
     ( (>=>)
     )
 import Control.Monad.Catch
     ( MonadMask
     )
+import Control.Monad.Trans.Except
+    ( ExceptT
+    , runExceptT
+    , throwE
+    )
 import Data.Coerce
     ( coerce
     )
+import Data.Generics.Product
+    ( field
+    )
+import Data.Generics.Wrapped
+    ( _Unwrapped
+    )
 import qualified Data.Map.Strict as Map
 import Data.Text
     ( Text
@@ -95,6 +102,10 @@ import Kore.Internal.TermLike
 import Kore.Log.ErrorRewriteLoop
     ( errorRewriteLoop
     )
+import Kore.Log.ErrorRuleMergeDuplicate
+    ( errorRuleMergeDuplicateIds
+    , errorRuleMergeDuplicateLabels
+    )
 import Kore.Log.InfoExecDepth
 import Kore.Log.KoreLogOptions
     ( KoreLogOptions (..)
@@ -211,7 +222,7 @@ exec
     -> smt (ExitCode, TermLike VariableName)
 exec breadthLimit verifiedModule strategy initialTerm =
     evalSimplifier verifiedModule' $ do
-        initialized <- initialize verifiedModule
+        initialized <- initializeAndSimplify verifiedModule
         let Initialized { rewriteRules } = initialized
         finals <-
             getFinalConfigsOf $ do
@@ -344,7 +355,7 @@ search
 search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
   =
     evalSimplifier verifiedModule $ do
-        initialized <- initialize verifiedModule
+        initialized <- initializeAndSimplify verifiedModule
         let Initialized { rewriteRules } = initialized
         simplifiedPatterns <-
             Pattern.simplify SideCondition.top
@@ -495,7 +506,7 @@ boundedModelCheck
     -> smt (Bounded.CheckResult (TermLike VariableName))
 boundedModelCheck breadthLimit depthLimit definitionModule specModule searchOrder =
     evalSimplifier definitionModule $ do
-        initialized <- initialize definitionModule
+        initialized <- initializeAndSimplify definitionModule
         let Initialized { rewriteRules } = initialized
             specClaims = extractImplicationClaims specModule
         assertSomeClaims specClaims
@@ -560,85 +571,68 @@ mergeRules
     -- ^ The list of rules to merge
     -> smt (Either Text [RewriteRule VariableName])
 mergeRules ruleMerger verifiedModule ruleNames =
-    evalSimplifier verifiedModule $ do
-        initialized <- initialize verifiedModule
+    evalSimplifier verifiedModule $ runExceptT $ do
+        initialized <- initializeWithoutSimplification verifiedModule
         let Initialized { rewriteRules } = initialized
-
-        let nonEmptyRules :: Either Text (NonEmpty (RewriteRule VariableName))
-            nonEmptyRules = do
-                let rewriteRules' = unRewritingRule <$> rewriteRules
-                rules <- extractRules rewriteRules' ruleNames
-                case rules of
-                    [] -> Left "Empty rule list."
-                    (r : rs) -> Right (r :| rs)
-
-        case nonEmptyRules of
-            (Left left) -> return (Left left)
-            (Right rules) -> Right <$> ruleMerger rules
-
-extractRules
-    :: [RewriteRule VariableName]
+            rewriteRules' = unRewritingRule <$> rewriteRules
+        rules <- extractAndSimplifyRules rewriteRules' ruleNames
+        lift $ ruleMerger rules
+
+extractAndSimplifyRules
+    :: forall m
+    .  MonadSimplify m
+    => [RewriteRule VariableName]
     -> [Text]
-    -> Either Text [RewriteRule VariableName]
-extractRules rules = foldr addExtractRule (Right [])
-  where
-    addExtractRule
-        :: Text
-        -> Either Text [RewriteRule VariableName]
-        -> Either Text [RewriteRule VariableName]
-    addExtractRule ruleName processedRules =
-        (:) <$> extractRule ruleName <*> processedRules
-
-    maybeRuleUniqueId :: RewriteRule VariableName -> Maybe Text
-    maybeRuleUniqueId
-        (RewriteRule RulePattern
-            { attributes = Attribute.Axiom
-                { uniqueId = Attribute.UniqueId maybeName }
-            }
-        )
-      =
-        maybeName
-
-    maybeRuleLabel :: RewriteRule VariableName -> Maybe Text
-    maybeRuleLabel
-        (RewriteRule RulePattern
-            { attributes = Attribute.Axiom
-                { label = Attribute.Label maybeName }
-            }
-        )
-      =
-        maybeName
-
-    idRules :: [RewriteRule VariableName] -> [(Text, RewriteRule VariableName)]
-    idRules = mapMaybe namedRule
-      where
-        namedRule rule = do
-            name <- maybeRuleUniqueId rule
-            return (name, rule)
-
-    labelRules :: [RewriteRule VariableName] -> [(Text, RewriteRule VariableName)]
-    labelRules = mapMaybe namedRule
-      where
-        namedRule rule = do
-            name <- maybeRuleLabel rule
-            return (name, rule)
-
-    rulesByName :: Map.Map Text (RewriteRule VariableName)
-    rulesByName = Map.union
-        (Map.fromListWith
-            (const $ const $ error "duplicate rule")
-            (idRules rules)
-        )
-        (Map.fromListWith
-            (const $ const $ error "duplicate rule")
-            (labelRules rules)
-        )
+    -> ExceptT Text m (NonEmpty (RewriteRule VariableName))
+extractAndSimplifyRules rules names = do
+    let rulesById = mapMaybe ruleById rules
+        rulesByLabel = mapMaybe ruleByLabel rules
+    whenDuplicate errorRuleMergeDuplicateIds rulesById
+    whenDuplicate errorRuleMergeDuplicateLabels rulesByLabel
+    let ruleRegistry = Map.fromList (rulesById <> rulesByLabel)
+    extractedRules <-
+        traverse (extractRule ruleRegistry >=> simplifyRuleLhs) names
+        & fmap (>>= toList)
+    case extractedRules of
+        [] -> throwE "Empty rule list."
+        (r : rs) -> return (r :| rs)
 
-    extractRule :: Text -> Either Text (RewriteRule VariableName)
-    extractRule ruleName =
-        note
-            ("Rule not found: '" <> ruleName <> "'.")
-            (Map.lookup ruleName rulesByName)
+  where
+    ruleById = ruleByName (field @"uniqueId")
+
+    ruleByLabel = ruleByName (field @"label")
+
+    ruleByName lens rule = do
+        name <-
+            Lens.view
+                (_Unwrapped . field @"attributes" . lens . _Unwrapped)
+                rule
+        return (name, rule)
+
+    extractRule registry ruleName =
+        maybe
+            (throwE $ "Rule not found: '" <> ruleName <> "'.")
+            return
+            (Map.lookup ruleName registry)
+
+    whenDuplicate logError withNames = do
+        let duplicateNames =
+                findCollisions . mkMapWithCollisions $ withNames
+        unless (null duplicateNames) (logError duplicateNames)
+
+mkMapWithCollisions
+    :: Ord key
+    => [(key, val)]
+    -> Map.Map key [val]
+mkMapWithCollisions pairs =
+    Map.fromListWith (<>)
+    $ (fmap . fmap) pure pairs
+
+findCollisions :: Map.Map key [val] -> Map.Map key [val]
+findCollisions = filter (not . isSingleton)
+  where
+    isSingleton [_] = True
+    isSingleton _ = False
 
 assertSingleClaim :: Monad m => [claim] -> m ()
 assertSingleClaim claims =
@@ -667,13 +661,28 @@ simplifySomeClaim rule = do
     claim' <- Rule.simplifyClaimPattern claim
     return $ Lens.set lensClaimPattern claim' rule
 
+initializeAndSimplify
+    :: MonadSimplify simplifier
+    => VerifiedModule StepperAttributes
+    -> simplifier Initialized
+initializeAndSimplify verifiedModule =
+    initialize (simplifyRuleLhs >=> Logic.scatter) verifiedModule
+
+initializeWithoutSimplification
+    :: MonadSimplify simplifier
+    => VerifiedModule StepperAttributes
+    -> simplifier Initialized
+initializeWithoutSimplification verifiedModule =
+    initialize return verifiedModule
+
 -- | Collect various rules and simplifiers in preparation to execute.
 initialize
     :: forall simplifier
     .  MonadSimplify simplifier
-    => VerifiedModule StepperAttributes
+    => (RewriteRule VariableName -> LogicT simplifier (RewriteRule VariableName))
+    -> VerifiedModule StepperAttributes
     -> simplifier Initialized
-initialize verifiedModule = do
+initialize simplificationProcedure verifiedModule = do
     rewriteRules <-
         Logic.observeAllT $ do
             rule <- Logic.scatter (extractRewriteAxioms verifiedModule)
@@ -684,7 +693,7 @@ initialize verifiedModule = do
         :: RewriteRule VariableName
         -> LogicT simplifier (RewriteRule RewritingVariableName)
     initializeRule rule = do
-        simplRule <- simplifyRuleLhs rule >>= Logic.scatter
+        simplRule <- simplificationProcedure rule
         when (lhsEqualsRhs $ getRewriteRule simplRule)
             (errorRewriteLoop simplRule)
         let renamedRule = mkRewritingRule simplRule
@@ -712,7 +721,7 @@ initializeProver
     -> Maybe (VerifiedModule StepperAttributes)
     -> simplifier InitializedProver
 initializeProver definitionModule specModule maybeTrustedModule = do
-    initialized <- initialize definitionModule
+    initialized <- initializeAndSimplify definitionModule
     tools <- Simplifier.askMetadataTools
     let Initialized { rewriteRules } = initialized
         changedSpecClaims :: [MaybeChanged SomeClaim]

kore/src/Kore/Log/ErrorRuleMergeDuplicate.hs

@@ -0,0 +1,127 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Log.ErrorRuleMergeDuplicate
+    ( ErrorRuleMergeDuplicateIds
+    , errorRuleMergeDuplicateIds
+    , ErrorRuleMergeDuplicateLabels
+    , errorRuleMergeDuplicateLabels
+    ) where
+
+import Prelude.Kore
+
+import Control.Exception
+    ( Exception (..)
+    , throw
+    )
+import qualified Control.Lens as Lens
+import Data.Generics.Product
+    ( field
+    )
+import Data.Generics.Wrapped
+    ( _Unwrapped
+    )
+import Data.Map.Strict
+    ( Map
+    )
+import qualified Data.Map.Strict as Map
+import Data.Text
+    ( Text
+    )
+import qualified Generics.SOP as SOP
+import qualified GHC.Generics as GHC
+
+import Kore.Attribute.SourceLocation
+    ( SourceLocation (..)
+    )
+import Kore.Internal.TermLike
+    ( VariableName
+    )
+import Kore.Step.RulePattern
+    ( RewriteRule (..)
+    )
+import Log
+import Pretty
+    ( Pretty (..)
+    )
+import qualified Pretty
+
+newtype ErrorRuleMergeDuplicateIds =
+    ErrorRuleMergeDuplicateIds
+        { unErrorRuleMergeDuplicateIds :: Map Text [SourceLocation]
+        }
+    deriving (Show)
+    deriving (GHC.Generic)
+    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
+
+instance Exception ErrorRuleMergeDuplicateIds where
+    toException = toException . SomeEntry
+    fromException exn =
+        fromException exn >>= fromEntry
+
+instance Entry ErrorRuleMergeDuplicateIds where
+    entrySeverity _ = Error
+    helpDoc _ =
+        "error thrown during rule merging when\
+        \ multiple rules have the same id"
+
+instance Pretty ErrorRuleMergeDuplicateIds where
+    pretty (ErrorRuleMergeDuplicateIds duplicateIds) =
+        prettyErrorText "id" duplicateIds
+
+newtype ErrorRuleMergeDuplicateLabels =
+    ErrorRuleMergeDuplicateLabels
+        { unErrorRuleMergeDuplicateLabels :: Map Text [SourceLocation]
+        }
+    deriving (Show)
+    deriving (GHC.Generic)
+    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
+
+instance Exception ErrorRuleMergeDuplicateLabels where
+    toException = toException . SomeEntry
+    fromException exn =
+        fromException exn >>= fromEntry
+
+instance Entry ErrorRuleMergeDuplicateLabels where
+    entrySeverity _ = Error
+    helpDoc _ =
+        "error thrown during rule merging when\
+        \ multiple rules have the same label"
+
+instance Pretty ErrorRuleMergeDuplicateLabels where
+    pretty (ErrorRuleMergeDuplicateLabels duplicateLabels) =
+        prettyErrorText "label" duplicateLabels
+
+errorRuleMergeDuplicateIds :: Map Text [RewriteRule VariableName] -> a
+errorRuleMergeDuplicateIds (getLocations -> duplicateIds) =
+    throw (ErrorRuleMergeDuplicateIds duplicateIds)
+
+errorRuleMergeDuplicateLabels :: Map Text [RewriteRule VariableName] -> a
+errorRuleMergeDuplicateLabels (getLocations -> duplicateLabels) =
+    throw (ErrorRuleMergeDuplicateLabels duplicateLabels)
+
+prettyErrorText :: Text -> Map Text [SourceLocation] -> Pretty.Doc ann
+prettyErrorText type' = Map.foldMapWithKey accum
+  where
+    accum name locations =
+        Pretty.vsep
+            $ ["The rules at the following locations:"]
+            <> fmap (Pretty.indent 4 . pretty) locations
+            <> [ Pretty.indent 2 duplicateNameType
+               , Pretty.indent 4 (pretty name)
+               ]
+    duplicateNameType =
+        Pretty.hsep ["all have the following", pretty type', ":"]
+
+getLocations :: Map Text [RewriteRule VariableName] -> Map Text [SourceLocation]
+getLocations =
+    (fmap . fmap)
+        ( Lens.view
+            ( _Unwrapped
+            . field @"attributes"
+            . field @"sourceLocation"
+            )
+        )