Skip to content

Commit 5892a0e

Browse files
ana-pantilieana-pantilie
authored
Rule merger: bug fix and better error messages (#2230)
* Add ErrorRuleMergeDuplicateId * Add ErrorRuleMergeDuplicateLabel * mergeRules: WIP clean-up * extractRules: WIP add assertion that ids are unique * Revert "extractRules: WIP add assertion that ids are unique" This reverts commit 4a4ce1b. * extractRules: refactor and add errors * Revert "extractRules: refactor and add errors" This reverts commit 048126b. * Revert "Revert "extractRules: WIP add assertion that ids are unique"" This reverts commit 86b8bd1. * mergeRules: simplify after selecting rules + WIP clean-up * ErrorRuleMergeDuplicate: clean-up * Clean-up
1 parent 015cdb8 commit 5892a0e

File tree

3 files changed

+229
-87
lines changed

3 files changed

+229
-87
lines changed

‎kore/src/Kore/Exec.hs

Lines changed: 96 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ Expose concrete execution as a library
1010
-}
1111
module Kore.Exec
1212
( exec
13-
, extractRules
1413
, mergeAllRules
1514
, mergeRulesConsecutiveBatches
1615
, search
@@ -27,19 +26,27 @@ import Control.Concurrent.MVar
2726
import Control.DeepSeq
2827
( deepseq
2928
)
30-
import Control.Error
31-
( note
32-
)
3329
import qualified Control.Lens as Lens
3430
import Control.Monad
3531
( (>=>)
3632
)
3733
import Control.Monad.Catch
3834
( MonadMask
3935
)
36+
import Control.Monad.Trans.Except
37+
( ExceptT
38+
, runExceptT
39+
, throwE
40+
)
4041
import Data.Coerce
4142
( coerce
4243
)
44+
import Data.Generics.Product
45+
( field
46+
)
47+
import Data.Generics.Wrapped
48+
( _Unwrapped
49+
)
4350
import qualified Data.Map.Strict as Map
4451
import Data.Text
4552
( Text
@@ -95,6 +102,10 @@ import Kore.Internal.TermLike
95102
import Kore.Log.ErrorRewriteLoop
96103
( errorRewriteLoop
97104
)
105+
import Kore.Log.ErrorRuleMergeDuplicate
106+
( errorRuleMergeDuplicateIds
107+
, errorRuleMergeDuplicateLabels
108+
)
98109
import Kore.Log.InfoExecDepth
99110
import Kore.Log.KoreLogOptions
100111
( KoreLogOptions (..)
@@ -211,7 +222,7 @@ exec
211222
-> smt (ExitCode, TermLike VariableName)
212223
exec breadthLimit verifiedModule strategy initialTerm =
213224
evalSimplifier verifiedModule' $ do
214-
initialized <- initialize verifiedModule
225+
initialized <- initializeAndSimplify verifiedModule
215226
let Initialized { rewriteRules } = initialized
216227
finals <-
217228
getFinalConfigsOf $ do
@@ -344,7 +355,7 @@ search
344355
search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
345356
=
346357
evalSimplifier verifiedModule $ do
347-
initialized <- initialize verifiedModule
358+
initialized <- initializeAndSimplify verifiedModule
348359
let Initialized { rewriteRules } = initialized
349360
simplifiedPatterns <-
350361
Pattern.simplify SideCondition.top
@@ -495,7 +506,7 @@ boundedModelCheck
495506
-> smt (Bounded.CheckResult (TermLike VariableName))
496507
boundedModelCheck breadthLimit depthLimit definitionModule specModule searchOrder =
497508
evalSimplifier definitionModule $ do
498-
initialized <- initialize definitionModule
509+
initialized <- initializeAndSimplify definitionModule
499510
let Initialized { rewriteRules } = initialized
500511
specClaims = extractImplicationClaims specModule
501512
assertSomeClaims specClaims
@@ -560,85 +571,68 @@ mergeRules
560571
-- ^ The list of rules to merge
561572
-> smt (Either Text [RewriteRule VariableName])
562573
mergeRules ruleMerger verifiedModule ruleNames =
563-
evalSimplifier verifiedModule $ do
564-
initialized <- initialize verifiedModule
574+
evalSimplifier verifiedModule $ runExceptT $ do
575+
initialized <- initializeWithoutSimplification verifiedModule
565576
let Initialized { rewriteRules } = initialized
566-
567-
let nonEmptyRules :: Either Text (NonEmpty (RewriteRule VariableName))
568-
nonEmptyRules = do
569-
let rewriteRules' = unRewritingRule <$> rewriteRules
570-
rules <- extractRules rewriteRules' ruleNames
571-
case rules of
572-
[] -> Left "Empty rule list."
573-
(r : rs) -> Right (r :| rs)
574-
575-
case nonEmptyRules of
576-
(Left left) -> return (Left left)
577-
(Right rules) -> Right <$> ruleMerger rules
578-
579-
extractRules
580-
:: [RewriteRule VariableName]
577+
rewriteRules' = unRewritingRule <$> rewriteRules
578+
rules <- extractAndSimplifyRules rewriteRules' ruleNames
579+
lift $ ruleMerger rules
580+
581+
extractAndSimplifyRules
582+
:: forall m
583+
. MonadSimplify m
584+
=> [RewriteRule VariableName]
581585
-> [Text]
582-
-> Either Text [RewriteRule VariableName]
583-
extractRules rules = foldr addExtractRule (Right [])
584-
where
585-
addExtractRule
586-
:: Text
587-
-> Either Text [RewriteRule VariableName]
588-
-> Either Text [RewriteRule VariableName]
589-
addExtractRule ruleName processedRules =
590-
(:) <$> extractRule ruleName <*> processedRules
591-
592-
maybeRuleUniqueId :: RewriteRule VariableName -> Maybe Text
593-
maybeRuleUniqueId
594-
(RewriteRule RulePattern
595-
{ attributes = Attribute.Axiom
596-
{ uniqueId = Attribute.UniqueId maybeName }
597-
}
598-
)
599-
=
600-
maybeName
601-
602-
maybeRuleLabel :: RewriteRule VariableName -> Maybe Text
603-
maybeRuleLabel
604-
(RewriteRule RulePattern
605-
{ attributes = Attribute.Axiom
606-
{ label = Attribute.Label maybeName }
607-
}
608-
)
609-
=
610-
maybeName
611-
612-
idRules :: [RewriteRule VariableName] -> [(Text, RewriteRule VariableName)]
613-
idRules = mapMaybe namedRule
614-
where
615-
namedRule rule = do
616-
name <- maybeRuleUniqueId rule
617-
return (name, rule)
618-
619-
labelRules :: [RewriteRule VariableName] -> [(Text, RewriteRule VariableName)]
620-
labelRules = mapMaybe namedRule
621-
where
622-
namedRule rule = do
623-
name <- maybeRuleLabel rule
624-
return (name, rule)
625-
626-
rulesByName :: Map.Map Text (RewriteRule VariableName)
627-
rulesByName = Map.union
628-
(Map.fromListWith
629-
(const $ const $ error "duplicate rule")
630-
(idRules rules)
631-
)
632-
(Map.fromListWith
633-
(const $ const $ error "duplicate rule")
634-
(labelRules rules)
635-
)
586+
-> ExceptT Text m (NonEmpty (RewriteRule VariableName))
587+
extractAndSimplifyRules rules names = do
588+
let rulesById = mapMaybe ruleById rules
589+
rulesByLabel = mapMaybe ruleByLabel rules
590+
whenDuplicate errorRuleMergeDuplicateIds rulesById
591+
whenDuplicate errorRuleMergeDuplicateLabels rulesByLabel
592+
let ruleRegistry = Map.fromList (rulesById <> rulesByLabel)
593+
extractedRules <-
594+
traverse (extractRule ruleRegistry >=> simplifyRuleLhs) names
595+
& fmap (>>= toList)
596+
case extractedRules of
597+
[] -> throwE "Empty rule list."
598+
(r : rs) -> return (r :| rs)
636599

637-
extractRule :: Text -> Either Text (RewriteRule VariableName)
638-
extractRule ruleName =
639-
note
640-
("Rule not found: '" <> ruleName <> "'.")
641-
(Map.lookup ruleName rulesByName)
600+
where
601+
ruleById = ruleByName (field @"uniqueId")
602+
603+
ruleByLabel = ruleByName (field @"label")
604+
605+
ruleByName lens rule = do
606+
name <-
607+
Lens.view
608+
(_Unwrapped . field @"attributes" . lens . _Unwrapped)
609+
rule
610+
return (name, rule)
611+
612+
extractRule registry ruleName =
613+
maybe
614+
(throwE $ "Rule not found: '" <> ruleName <> "'.")
615+
return
616+
(Map.lookup ruleName registry)
617+
618+
whenDuplicate logError withNames = do
619+
let duplicateNames =
620+
findCollisions . mkMapWithCollisions $ withNames
621+
unless (null duplicateNames) (logError duplicateNames)
622+
623+
mkMapWithCollisions
624+
:: Ord key
625+
=> [(key, val)]
626+
-> Map.Map key [val]
627+
mkMapWithCollisions pairs =
628+
Map.fromListWith (<>)
629+
$ (fmap . fmap) pure pairs
630+
631+
findCollisions :: Map.Map key [val] -> Map.Map key [val]
632+
findCollisions = filter (not . isSingleton)
633+
where
634+
isSingleton [_] = True
635+
isSingleton _ = False
642636

643637
assertSingleClaim :: Monad m => [claim] -> m ()
644638
assertSingleClaim claims =
@@ -667,13 +661,28 @@ simplifySomeClaim rule = do
667661
claim' <- Rule.simplifyClaimPattern claim
668662
return $ Lens.set lensClaimPattern claim' rule
669663

664+
initializeAndSimplify
665+
:: MonadSimplify simplifier
666+
=> VerifiedModule StepperAttributes
667+
-> simplifier Initialized
668+
initializeAndSimplify verifiedModule =
669+
initialize (simplifyRuleLhs >=> Logic.scatter) verifiedModule
670+
671+
initializeWithoutSimplification
672+
:: MonadSimplify simplifier
673+
=> VerifiedModule StepperAttributes
674+
-> simplifier Initialized
675+
initializeWithoutSimplification verifiedModule =
676+
initialize return verifiedModule
677+
670678
-- | Collect various rules and simplifiers in preparation to execute.
671679
initialize
672680
:: forall simplifier
673681
. MonadSimplify simplifier
674-
=> VerifiedModule StepperAttributes
682+
=> (RewriteRule VariableName -> LogicT simplifier (RewriteRule VariableName))
683+
-> VerifiedModule StepperAttributes
675684
-> simplifier Initialized
676-
initialize verifiedModule = do
685+
initialize simplificationProcedure verifiedModule = do
677686
rewriteRules <-
678687
Logic.observeAllT $ do
679688
rule <- Logic.scatter (extractRewriteAxioms verifiedModule)
@@ -684,7 +693,7 @@ initialize verifiedModule = do
684693
:: RewriteRule VariableName
685694
-> LogicT simplifier (RewriteRule RewritingVariableName)
686695
initializeRule rule = do
687-
simplRule <- simplifyRuleLhs rule >>= Logic.scatter
696+
simplRule <- simplificationProcedure rule
688697
when (lhsEqualsRhs $ getRewriteRule simplRule)
689698
(errorRewriteLoop simplRule)
690699
let renamedRule = mkRewritingRule simplRule
@@ -712,7 +721,7 @@ initializeProver
712721
-> Maybe (VerifiedModule StepperAttributes)
713722
-> simplifier InitializedProver
714723
initializeProver definitionModule specModule maybeTrustedModule = do
715-
initialized <- initialize definitionModule
724+
initialized <- initializeAndSimplify definitionModule
716725
tools <- Simplifier.askMetadataTools
717726
let Initialized { rewriteRules } = initialized
718727
changedSpecClaims :: [MaybeChanged SomeClaim]

‎kore/src/Kore/Log/ErrorRuleMergeDuplicate.hs

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2020
3+
License : NCSA
4+
5+
-}
6+
7+
module Kore.Log.ErrorRuleMergeDuplicate
8+
( ErrorRuleMergeDuplicateIds
9+
, errorRuleMergeDuplicateIds
10+
, ErrorRuleMergeDuplicateLabels
11+
, errorRuleMergeDuplicateLabels
12+
) where
13+
14+
import Prelude.Kore
15+
16+
import Control.Exception
17+
( Exception (..)
18+
, throw
19+
)
20+
import qualified Control.Lens as Lens
21+
import Data.Generics.Product
22+
( field
23+
)
24+
import Data.Generics.Wrapped
25+
( _Unwrapped
26+
)
27+
import Data.Map.Strict
28+
( Map
29+
)
30+
import qualified Data.Map.Strict as Map
31+
import Data.Text
32+
( Text
33+
)
34+
import qualified Generics.SOP as SOP
35+
import qualified GHC.Generics as GHC
36+
37+
import Kore.Attribute.SourceLocation
38+
( SourceLocation (..)
39+
)
40+
import Kore.Internal.TermLike
41+
( VariableName
42+
)
43+
import Kore.Step.RulePattern
44+
( RewriteRule (..)
45+
)
46+
import Log
47+
import Pretty
48+
( Pretty (..)
49+
)
50+
import qualified Pretty
51+
52+
newtype ErrorRuleMergeDuplicateIds =
53+
ErrorRuleMergeDuplicateIds
54+
{ unErrorRuleMergeDuplicateIds :: Map Text [SourceLocation]
55+
}
56+
deriving (Show)
57+
deriving (GHC.Generic)
58+
deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
59+
60+
instance Exception ErrorRuleMergeDuplicateIds where
61+
toException = toException . SomeEntry
62+
fromException exn =
63+
fromException exn >>= fromEntry
64+
65+
instance Entry ErrorRuleMergeDuplicateIds where
66+
entrySeverity _ = Error
67+
helpDoc _ =
68+
"error thrown during rule merging when\
69+
\ multiple rules have the same id"
70+
71+
instance Pretty ErrorRuleMergeDuplicateIds where
72+
pretty (ErrorRuleMergeDuplicateIds duplicateIds) =
73+
prettyErrorText "id" duplicateIds
74+
75+
newtype ErrorRuleMergeDuplicateLabels =
76+
ErrorRuleMergeDuplicateLabels
77+
{ unErrorRuleMergeDuplicateLabels :: Map Text [SourceLocation]
78+
}
79+
deriving (Show)
80+
deriving (GHC.Generic)
81+
deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
82+
83+
instance Exception ErrorRuleMergeDuplicateLabels where
84+
toException = toException . SomeEntry
85+
fromException exn =
86+
fromException exn >>= fromEntry
87+
88+
instance Entry ErrorRuleMergeDuplicateLabels where
89+
entrySeverity _ = Error
90+
helpDoc _ =
91+
"error thrown during rule merging when\
92+
\ multiple rules have the same label"
93+
94+
instance Pretty ErrorRuleMergeDuplicateLabels where
95+
pretty (ErrorRuleMergeDuplicateLabels duplicateLabels) =
96+
prettyErrorText "label" duplicateLabels
97+
98+
errorRuleMergeDuplicateIds :: Map Text [RewriteRule VariableName] -> a
99+
errorRuleMergeDuplicateIds (getLocations -> duplicateIds) =
100+
throw (ErrorRuleMergeDuplicateIds duplicateIds)
101+
102+
errorRuleMergeDuplicateLabels :: Map Text [RewriteRule VariableName] -> a
103+
errorRuleMergeDuplicateLabels (getLocations -> duplicateLabels) =
104+
throw (ErrorRuleMergeDuplicateLabels duplicateLabels)
105+
106+
prettyErrorText :: Text -> Map Text [SourceLocation] -> Pretty.Doc ann
107+
prettyErrorText type' = Map.foldMapWithKey accum
108+
where
109+
accum name locations =
110+
Pretty.vsep
111+
$ ["The rules at the following locations:"]
112+
<> fmap (Pretty.indent 4 . pretty) locations
113+
<> [ Pretty.indent 2 duplicateNameType
114+
, Pretty.indent 4 (pretty name)
115+
]
116+
duplicateNameType =
117+
Pretty.hsep ["all have the following", pretty type', ":"]
118+
119+
getLocations :: Map Text [RewriteRule VariableName] -> Map Text [SourceLocation]
120+
getLocations =
121+
(fmap . fmap)
122+
( Lens.view
123+
( _Unwrapped
124+
. field @"attributes"
125+
. field @"sourceLocation"
126+
)
127+
)

0 commit comments

Comments
 (0)