Skip to content

Commit edcd219

Browse files
ana-pantilieana-pantilie
authored
Fix breadth limit bug; implementation for prove (#1931)
1 parent 3f55037 commit edcd219

File tree

15 files changed

+367
-102
lines changed

15 files changed

+367
-102
lines changed

‎kore/app/exec/Main.hs

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -89,11 +89,11 @@ import Kore.IndexedModule.IndexedModule
8989
import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
9090
( build
9191
)
92+
import qualified Kore.Internal.OrPattern as OrPattern
9293
import Kore.Internal.Pattern
9394
( Conditional (..)
9495
, Pattern
9596
)
96-
import qualified Kore.Internal.Pattern as Pattern
9797
import Kore.Internal.Predicate
9898
( makePredicate
9999
)
@@ -678,12 +678,15 @@ koreProve execOptions proveOptions = do
678678
maybeAlreadyProvenModule
679679

680680
(exitCode, final) <- case proveResult of
681-
Left Stuck { stuckPattern, provenClaims } -> do
681+
Left Stuck { stuckPatterns, provenClaims } -> do
682682
maybe
683683
(return ())
684684
(lift . saveProven specModule provenClaims)
685685
saveProofs
686-
return (failure $ Pattern.toTermLike stuckPattern)
686+
stuckPatterns
687+
& OrPattern.toTermLike
688+
& failure
689+
& return
687690
Right () -> return success
688691

689692
lift $ renderResult execOptions (unparse final)

‎kore/src/Kore/Exec.hs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -224,7 +224,10 @@ exec breadthLimit verifiedModule strategy initialTerm =
224224
let
225225
updateQueue = \as ->
226226
Strategy.unfoldDepthFirst as
227-
>=> lift . Strategy.applyBreadthLimit breadthLimit
227+
>=> lift
228+
. Strategy.applyBreadthLimit
229+
breadthLimit
230+
dropStrategy
228231
transit instr config =
229232
Strategy.transitionRule transitionRule instr config
230233
& runTransitionT
@@ -238,6 +241,7 @@ exec breadthLimit verifiedModule strategy initialTerm =
238241
let finalTerm = forceSort initialSort $ Pattern.toTermLike finalConfig
239242
return (exitCode, finalTerm)
240243
where
244+
dropStrategy = snd
241245
-- Get the first final configuration of an execution graph.
242246
getFinalConfigOf = takeFirstResult >=> orElseBottom
243247
where

‎kore/src/Kore/Step/Strategy.hs

Lines changed: 7 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -451,8 +451,6 @@ See also: 'pickLongest', 'pickFinal', 'pickOne', 'pickStar', 'pickPlus'
451451
constructExecutionGraph
452452
:: forall m config rule instr
453453
. (MonadProfiler m, MonadThrow m)
454-
=> Show instr
455-
=> Typeable instr
456454
=> Limit Natural
457455
-> (instr -> config -> TransitionT rule m config)
458456
-> [instr]
@@ -464,10 +462,11 @@ constructExecutionGraph breadthLimit transit instrs0 searchOrder0 config0 =
464462
& flip State.execStateT execGraph
465463
where
466464
execGraph = emptyExecutionGraph config0
465+
dropStrategy = snd
467466

468467
mkQueue = \as ->
469468
unfoldSearchOrder searchOrder0 as
470-
>=> applyBreadthLimit breadthLimit
469+
>=> applyBreadthLimit breadthLimit dropStrategy
471470
>=> profileQueueLength
472471

473472
profileQueueLength queue = do
@@ -546,14 +545,15 @@ unfoldSearchOrder DepthFirst = unfoldDepthFirst
546545
unfoldSearchOrder BreadthFirst = unfoldBreadthFirst
547546

548547
applyBreadthLimit
549-
:: Exception (LimitExceeded a)
548+
:: Exception (LimitExceeded b)
550549
=> MonadThrow m
551550
=> Limit Natural
551+
-> (a -> b)
552552
-> Seq a
553553
-> m (Seq a)
554-
applyBreadthLimit breadthLimit as
555-
| _ Seq.:<| as' <- as, exceedsLimit as' =
556-
Exception.throwM (LimitExceeded as)
554+
applyBreadthLimit breadthLimit transf as
555+
| exceedsLimit as =
556+
Exception.throwM (LimitExceeded (transf <$> as))
557557
| otherwise = pure as
558558
where
559559
exceedsLimit = not . withinLimit breadthLimit . fromIntegral . Seq.length
@@ -637,8 +637,6 @@ See also: 'pickLongest', 'pickFinal', 'pickOne', 'pickStar', 'pickPlus'
637637
runStrategy
638638
:: forall m prim rule config
639639
. (MonadProfiler m, MonadThrow m)
640-
=> Show prim
641-
=> Typeable prim
642640
=> Limit Natural
643641
-> (prim -> config -> TransitionT rule m config)
644642
-- ^ Primitive strategy rule
@@ -653,8 +651,6 @@ runStrategy breadthLimit applyPrim instrs0 config0 =
653651
runStrategyWithSearchOrder
654652
:: forall m prim rule config
655653
. (MonadProfiler m, MonadThrow m)
656-
=> Show prim
657-
=> Typeable prim
658654
=> Limit Natural
659655
-> (prim -> config -> TransitionT rule m config)
660656
-- ^ Primitive strategy rule

‎kore/src/Kore/Strategies/Verification.hs

Lines changed: 34 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ import qualified Control.Monad as Monad
2929
)
3030
import Control.Monad.Catch
3131
( MonadCatch
32+
, handle
3233
)
3334
import Control.Monad.Except
3435
( ExceptT
@@ -52,6 +53,10 @@ import Data.Limit
5253
)
5354
import qualified Data.Limit as Limit
5455
import Kore.Debug
56+
import Kore.Internal.OrPattern
57+
( OrPattern
58+
)
59+
import qualified Kore.Internal.OrPattern as OrPattern
5560
import Kore.Internal.Pattern
5661
( Pattern
5762
)
@@ -92,7 +97,10 @@ import qualified Logic
9297
-- TODO (thomas.tuegel): (Pattern VariableName) should be ReachabilityRule.
9398
type CommonProofState = ProofState.ProofState (Pattern VariableName)
9499

95-
commonProofStateTransformer :: ProofStateTransformer (Pattern VariableName) (Pattern VariableName)
100+
commonProofStateTransformer
101+
:: ProofStateTransformer
102+
(Pattern VariableName)
103+
(Pattern VariableName)
96104
commonProofStateTransformer =
97105
ProofStateTransformer
98106
{ goalTransformer = id
@@ -108,7 +116,7 @@ The action may throw an exception if the proof fails; the exception is a single
108116
@'Pattern' 'VariableName'@, the first unprovable configuration.
109117
110118
-}
111-
type Verifier m = ExceptT (Pattern VariableName) m
119+
type Verifier m = ExceptT (OrPattern VariableName) m
112120

113121
{- | Verifies a set of claims. When it verifies a certain claim, after the
114122
first step, it also uses the claims as axioms (i.e. it does coinductive proofs).
@@ -121,7 +129,7 @@ If the verification succeeds, it returns ().
121129
-}
122130
data Stuck =
123131
Stuck
124-
{ stuckPattern :: !(Pattern VariableName)
132+
{ stuckPatterns :: !(OrPattern VariableName)
125133
, provenClaims :: ![ReachabilityRule]
126134
}
127135
deriving (Eq, GHC.Generic, Show)
@@ -204,8 +212,8 @@ verifyHelper breadthLimit searchOrder claims axioms (ToProve toProve) =
204212
verifyClaim breadthLimit searchOrder claims axioms unprovenClaim
205213
return (claim : provenClaims)
206214
where
207-
wrapStuckPattern :: Pattern VariableName -> Stuck
208-
wrapStuckPattern stuckPattern = Stuck { stuckPattern, provenClaims }
215+
wrapStuckPattern :: OrPattern VariableName -> Stuck
216+
wrapStuckPattern stuckPatterns = Stuck { stuckPatterns, provenClaims }
209217

210218
verifyClaim
211219
:: forall simplifier
@@ -215,7 +223,7 @@ verifyClaim
215223
-> AllClaims ReachabilityRule
216224
-> Axioms ReachabilityRule
217225
-> (ReachabilityRule, Limit Natural)
218-
-> ExceptT (Pattern VariableName) simplifier ()
226+
-> ExceptT (OrPattern VariableName) simplifier ()
219227
verifyClaim
220228
breadthLimit
221229
searchOrder
@@ -230,19 +238,31 @@ verifyClaim
230238
strategy goal claims axioms
231239
& Foldable.toList
232240
& Limit.takeWithin depthLimit
233-
Strategy.leavesM
234-
updateQueue
235-
(Strategy.unfoldTransition transit)
236-
(limitedStrategy, startPattern)
237-
& fmap discardStrategy
238-
& throwUnproven
241+
handle
242+
handleLimitExceeded
243+
$ Strategy.leavesM
244+
updateQueue
245+
(Strategy.unfoldTransition transit)
246+
(limitedStrategy, startPattern)
247+
& fmap discardStrategy
248+
& throwUnproven
239249
where
240250
destination = getDestination goal
241251
discardStrategy = snd
242252

253+
handleLimitExceeded
254+
:: Strategy.LimitExceeded CommonProofState
255+
-> ExceptT (OrPattern VariableName) simplifier ()
256+
handleLimitExceeded (Strategy.LimitExceeded patterns) =
257+
Monad.Except.throwError
258+
. OrPattern.fromPatterns
259+
$ fmap
260+
(ProofState.proofState commonProofStateTransformer)
261+
patterns
262+
243263
updateQueue = \as ->
244264
Strategy.unfoldSearchOrder searchOrder as
245-
>=> lift . Strategy.applyBreadthLimit breadthLimit
265+
>=> lift . Strategy.applyBreadthLimit breadthLimit snd
246266
>=> profileQueueLength
247267

248268
profileQueueLength queue = do
@@ -263,7 +283,7 @@ verifyClaim
263283
-> Verifier simplifier ()
264284
throwUnprovenOrElse proofState acts = do
265285
ProofState.extractUnproven proofState
266-
& Foldable.traverse_ Monad.Except.throwError
286+
& Foldable.traverse_ (Monad.Except.throwError . OrPattern.fromPattern)
267287
acts
268288

269289
transit instr config =

‎kore/test/Test/Kore/Exec.hs

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -55,10 +55,8 @@ import Kore.Internal.Predicate
5555
)
5656
import Kore.Internal.TermLike
5757
import qualified Kore.Internal.TermLike as TermLike
58-
import Kore.Rewriting.RewritingVariable
5958
import Kore.Step
60-
( Prim (..)
61-
, priorityAllStrategy
59+
( priorityAllStrategy
6260
, priorityAnyStrategy
6361
)
6462
import Kore.Step.Rule
@@ -74,7 +72,6 @@ import Kore.Step.Search
7472
import qualified Kore.Step.Search as Search
7573
import Kore.Step.Strategy
7674
( LimitExceeded (..)
77-
, Strategy (..)
7875
)
7976
import Kore.Syntax.Definition hiding
8077
( Symbol
@@ -227,7 +224,7 @@ test_searchExceedingBreadthLimit =
227224

228225
assertion searchType =
229226
catch (shouldExceedBreadthLimit searchType)
230-
$ \(_ :: LimitExceeded ([Strategy (Prim (RewriteRule RewritingVariableName))], Graph.Node)) ->
227+
$ \(_ :: LimitExceeded Graph.Node) ->
231228
pure ()
232229

233230
shouldExceedBreadthLimit :: SearchType -> IO ()

‎kore/test/Test/Kore/Strategies/AllPath/Verification.hs

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,13 @@ import Data.Limit
1414
)
1515

1616
import qualified Kore.Attribute.Axiom as Attribute
17+
import qualified Kore.Internal.OrPattern as OrPattern
1718
import Kore.Internal.Pattern
1819
( Conditional (Conditional)
1920
)
2021
import Kore.Internal.Pattern as Conditional
2122
( Conditional (..)
2223
)
23-
import Kore.Internal.Pattern as Pattern
2424
import Kore.Internal.Predicate
2525
( makeEqualsPredicate
2626
, makeNotPredicate
@@ -67,7 +67,7 @@ test_allPathVerification =
6767
[ simpleClaim Mock.a Mock.b ]
6868
[]
6969
assertEqual ""
70-
(Left $ Pattern.fromTermLike Mock.a)
70+
(Left $ OrPattern.fromTermLike Mock.a)
7171
actual
7272
-- TODO(Ana): this should be uncommented if we decide
7373
-- that the destination doesn't need to be
@@ -133,7 +133,7 @@ test_allPathVerification =
133133
[ simpleClaim Mock.a Mock.b ]
134134
[]
135135
assertEqual ""
136-
(Left $ Pattern.fromTermLike Mock.c)
136+
(Left $ OrPattern.fromTermLike Mock.c)
137137
actual
138138
, testCase "Verifies one claim with branching" $ do
139139
-- Axiom: constr11(a) => b
@@ -169,7 +169,8 @@ test_allPathVerification =
169169
[simpleClaim (Mock.functionalConstr10 (mkElemVar Mock.x)) Mock.b]
170170
[]
171171
assertEqual ""
172-
(Left Conditional
172+
( Left . OrPattern.fromPattern
173+
$ Conditional
173174
{ term = Mock.functionalConstr11 (mkElemVar Mock.x)
174175
, predicate =
175176
makeNotPredicate
@@ -221,7 +222,7 @@ test_allPathVerification =
221222
]
222223
[]
223224
assertEqual ""
224-
(Left $ Pattern.fromTermLike Mock.c)
225+
(Left $ OrPattern.fromTermLike Mock.c)
225226
actual
226227
, testCase "fails second of two claims" $ do
227228
-- Axiom: a => b
@@ -242,7 +243,7 @@ test_allPathVerification =
242243
]
243244
[]
244245
assertEqual ""
245-
(Left $ Pattern.fromTermLike Mock.e)
246+
(Left $ OrPattern.fromTermLike Mock.e)
246247
actual
247248
, testCase "second proves first but fails" $ do
248249
-- Axiom: a => b
@@ -261,7 +262,7 @@ test_allPathVerification =
261262
]
262263
[]
263264
assertEqual ""
264-
(Left $ Pattern.fromTermLike Mock.b)
265+
(Left $ OrPattern.fromTermLike Mock.b)
265266
actual
266267
, testCase "first proves second but fails" $ do
267268
-- Axiom: a => b
@@ -280,7 +281,7 @@ test_allPathVerification =
280281
]
281282
[]
282283
assertEqual ""
283-
(Left $ Pattern.fromTermLike Mock.b)
284+
(Left $ OrPattern.fromTermLike Mock.b)
284285
actual
285286
, testCase "trusted first proves second" $ do
286287
-- Axiom: a => b
@@ -323,7 +324,7 @@ test_allPathVerification =
323324
]
324325
[]
325326
assertEqual ""
326-
(Left $ Pattern.fromTermLike Mock.e)
327+
(Left $ OrPattern.fromTermLike Mock.e)
327328
actual
328329
, testCase "Priority: should get stuck because of second axiom" $ do
329330
-- Axioms:
@@ -343,7 +344,7 @@ test_allPathVerification =
343344
]
344345
[]
345346
assertEqual ""
346-
(Left $ Pattern.fromTermLike Mock.c)
347+
(Left $ OrPattern.fromTermLike Mock.c)
347348
actual
348349
, testCase "Priority: should succeed, prefering axiom with priority 1" $ do
349350
-- Axioms:

‎kore/test/Test/Kore/Strategies/Common.hs

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ import Numeric.Natural
1717
( Natural
1818
)
1919

20-
import Kore.Internal.Pattern
21-
( Pattern
20+
import Kore.Internal.OrPattern
21+
( OrPattern
2222
)
2323
import Kore.Internal.TermLike
2424
import Kore.Rewriting.RewritingVariable
@@ -59,7 +59,7 @@ runVerificationToPattern
5959
-> [Rule ReachabilityRule]
6060
-> [ReachabilityRule]
6161
-> [ReachabilityRule]
62-
-> IO (Either (Pattern VariableName) ())
62+
-> IO (Either (OrPattern VariableName) ())
6363
runVerificationToPattern breadthLimit depthLimit axioms claims alreadyProven =
6464
do
6565
stuck <- runVerification
@@ -70,7 +70,8 @@ runVerificationToPattern breadthLimit depthLimit axioms claims alreadyProven =
7070
alreadyProven
7171
return (toPattern stuck)
7272
where
73-
toPattern = Bifunctor.first stuckPattern
73+
toPattern =
74+
Bifunctor.first stuckPatterns
7475

7576
runVerification
7677
:: Limit Natural

0 commit comments

Comments
 (0)