Skip to content

Commit 91aa4f2

Browse files
andreiburdusattuegelrv-jenkins
authored
Make ErrorDecidePredicateUnknown an actual Error (#2086)
* Make ErrorDecidePredicateUnknown an actual Error * Draft fix one test * Fix more tests: they needed SMT * Fix two more tests: use runSMT * Unit tests pass * Cleanup and stylish * Remove checkImplicationNoSMT * Restore test name * Remove redundant lambda Co-authored-by: Thomas Tuegel <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent 96001e2 commit 91aa4f2

File tree

10 files changed

+70
-47
lines changed

10 files changed

+70
-47
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ instance Pretty ErrorBottomTotalFunction where
5353
instance Exception ErrorBottomTotalFunction where
5454
toException = toException . SomeEntry
5555
fromException exn =
56-
fromException exn >>= \entry -> fromEntry entry
56+
fromException exn >>= fromEntry
5757

5858
instance Entry ErrorBottomTotalFunction where
5959
entrySeverity _ = Error

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

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,11 @@ module Kore.Log.ErrorDecidePredicateUnknown
1111

1212
import Prelude.Kore
1313

14+
import Control.Exception
15+
( Exception (..)
16+
, throw
17+
)
18+
1419
import Kore.Internal.Predicate
1520
( Predicate
1621
)
@@ -29,6 +34,11 @@ newtype ErrorDecidePredicateUnknown =
2934
}
3035
deriving (Show)
3136

37+
instance Exception ErrorDecidePredicateUnknown where
38+
toException = toException . SomeEntry
39+
fromException exn =
40+
fromException exn >>= fromEntry
41+
3242
instance Pretty ErrorDecidePredicateUnknown where
3343
pretty ErrorDecidePredicateUnknown { predicates } =
3444
Pretty.vsep
@@ -46,11 +56,10 @@ instance Entry ErrorDecidePredicateUnknown where
4656
"errors raised when the solver cannot decide satisfiability of a formula"
4757

4858
errorDecidePredicateUnknown
49-
:: MonadLog log
50-
=> InternalVariable variable
59+
:: InternalVariable variable
5160
=> NonEmpty (Predicate variable)
5261
-> log ()
5362
errorDecidePredicateUnknown predicates' =
54-
logEntry ErrorDecidePredicateUnknown { predicates }
63+
throw ErrorDecidePredicateUnknown { predicates }
5564
where
5665
predicates = Predicate.mapVariables (pure toVariableName) <$> predicates'

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ data ErrorRewriteLoop =
4848
instance Exception ErrorRewriteLoop where
4949
toException = toException . SomeEntry
5050
fromException exn =
51-
fromException exn >>= \entry -> fromEntry entry
51+
fromException exn >>= fromEntry
5252

5353
instance Pretty ErrorRewriteLoop where
5454
pretty ErrorRewriteLoop { rule, errorCallStack } =

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ instance SOP.HasDatatypeInfo ErrorRewritesInstantiation
9090
instance Exception ErrorRewritesInstantiation where
9191
toException = toException . SomeEntry
9292
fromException exn =
93-
fromException exn >>= \entry -> fromEntry entry
93+
fromException exn >>= fromEntry
9494

9595
instance Entry ErrorRewritesInstantiation where
9696
entrySeverity _ = Error

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -652,7 +652,9 @@ checkImplication'
652652
-> m (CheckImplicationResult goal)
653653
checkImplication' lensRulePattern goal =
654654
goal
655-
& Lens.traverseOf lensRulePattern (Compose . checkImplicationWorker)
655+
& Lens.traverseOf
656+
lensRulePattern
657+
(Compose . checkImplicationWorker)
656658
& getCompose
657659

658660
assertFunctionLikeConfiguration

‎kore/test/Test/Kore/Step/RewriteStep.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1095,7 +1095,7 @@ applyRewriteRulesParallel initial rules =
10951095
Unification.unificationProcedure
10961096
(mkRewritingRule <$> rules)
10971097
(mkRewritingPattern $ simplifiedPattern initial)
1098-
& runSimplifierNoSMT Mock.env
1098+
& runSimplifier Mock.env
10991099

11001100
applyClaimsSequence
11011101
:: TestPattern
@@ -1109,7 +1109,7 @@ applyClaimsSequence initial claims =
11091109
Unification.unificationProcedure
11101110
(mkRewritingPattern $ simplifiedPattern initial)
11111111
claims
1112-
& runSimplifierNoSMT Mock.env
1112+
& runSimplifier Mock.env
11131113

11141114
checkResults
11151115
:: Step.UnifyingRuleVariable rule ~ RewritingVariableName

‎kore/test/Test/Kore/Step/Rule/Combine.hs‎

Lines changed: 17 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,7 @@ import Test.Kore
6767
import qualified Test.Kore.Step.MockSymbols as Mock
6868
import Test.SMT
6969
( runNoSMT
70+
, runSMT
7071
)
7172
import Test.Tasty.HUnit.Ext
7273

@@ -234,13 +235,13 @@ test_combineRules =
234235
[ testCase "One rule" $ do
235236
let expected = [Mock.a `rewritesTo` Mock.cf]
236237

237-
actual <- runMergeRules [ Mock.a `rewritesTo` Mock.cf ]
238+
actual <- runMergeRulesNoSMT [ Mock.a `rewritesTo` Mock.cf ]
238239

239240
assertEqual "" expected actual
240241
, testCase "Two rules" $ do
241242
let expected = [Mock.a `rewritesTo` Mock.cf]
242243

243-
actual <- runMergeRules
244+
actual <- runMergeRulesNoSMT
244245
[ Mock.a `rewritesTo` Mock.b
245246
, Mock.b `rewritesTo` Mock.cf
246247
]
@@ -267,7 +268,7 @@ test_combineRules =
267268
`rewritesTo` y
268269
]
269270

270-
actual <- runMergeRules
271+
actual <- runMergeRulesNoSMT
271272
[ Mock.functionalConstr10 x `rewritesTo` x
272273
, Mock.functionalConstr11 y `rewritesTo` y
273274
]
@@ -318,7 +319,7 @@ test_combineRules =
318319
`rewritesTo` x0
319320
]
320321

321-
actual <- runMergeRules
322+
actual <- runMergeRulesNoSMT
322323
[ Mock.functionalConstr10 x `rewritesTo` x
323324
, Mock.functionalConstr11 x `rewritesTo` x
324325
]
@@ -341,7 +342,7 @@ test_combineRulesGrouped =
341342
, testCase "Two rules" $ do
342343
let expected = [Mock.a `rewritesTo` Mock.cf]
343344

344-
actual <- runMergeRules
345+
actual <- runMergeRulesNoSMT
345346
[ Mock.a `rewritesTo` Mock.b
346347
, Mock.b `rewritesTo` Mock.cf
347348
]
@@ -354,7 +355,7 @@ test_combineRulesGrouped =
354355
`rewritesTo` z
355356
]
356357

357-
actual <- runMergeRules
358+
actual <- runMergeRulesNoSMT
358359
[ Mock.functionalConstr10 x `rewritesTo` x
359360
, Mock.functionalConstr11 y `rewritesTo` y
360361
, Mock.functionalConstr12 z `rewritesTo` z
@@ -379,11 +380,20 @@ applyAlias name aliasRight =
379380
}
380381
[]
381382

383+
runMergeRulesNoSMT
384+
:: [RewriteRule VariableName]
385+
-> IO [RewriteRule VariableName]
386+
runMergeRulesNoSMT (rule : rules) =
387+
runNoSMT
388+
$ runSimplifier Mock.env
389+
$ mergeRules (rule :| rules)
390+
runMergeRulesNoSMT [] = error "Unexpected empty list of rules."
391+
382392
runMergeRules
383393
:: [RewriteRule VariableName]
384394
-> IO [RewriteRule VariableName]
385395
runMergeRules (rule : rules) =
386-
runNoSMT
396+
runSMT (pure ())
387397
$ runSimplifier Mock.env
388398
$ mergeRules (rule :| rules)
389399
runMergeRules [] = error "Unexpected empty list of rules."

‎kore/test/Test/Kore/Step/Rule/Simplify.hs‎

Lines changed: 31 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,7 @@ import Test.Kore.Step.Rule.Common
9494
import qualified Test.Kore.Step.Rule.Common as Common
9595
import Test.SMT
9696
( runNoSMT
97+
, runSMT
9798
)
9899
import Test.Tasty.HUnit.Ext
99100

@@ -103,14 +104,14 @@ test_simplifyRule_RewriteRule =
103104
let rule = Mock.a `rewritesToWithSortRewriteRule` Mock.cf
104105
expected = [rule]
105106

106-
actual <- runSimplifyRule rule
107+
actual <- runSimplifyRuleNoSMT rule
107108

108109
assertEqual "" expected actual
109110

110111
, testCase "Simplify lhs term" $ do
111112
let expected = [Mock.a `rewritesToWithSortRewriteRule` Mock.cf]
112113

113-
actual <- runSimplifyRule
114+
actual <- runSimplifyRuleNoSMT
114115
( mkAnd Mock.a (mkEquals Mock.testSort Mock.a Mock.a)
115116
`rewritesToWithSortRewriteRule`
116117
Mock.cf
@@ -125,14 +126,14 @@ test_simplifyRule_RewriteRule =
125126
mkAnd Mock.cf (mkEquals Mock.testSort Mock.a Mock.a)
126127
expected = [rule]
127128

128-
actual <- runSimplifyRule rule
129+
actual <- runSimplifyRuleNoSMT rule
129130

130131
assertEqual "" expected actual
131132

132133
, testCase "Substitution in lhs term" $ do
133134
let expected = [Mock.a `rewritesToWithSortRewriteRule` Mock.f Mock.b]
134135

135-
actual <- runSimplifyRule
136+
actual <- runSimplifyRuleNoSMT
136137
( mkAnd Mock.a (mkEquals Mock.testSort Mock.b x)
137138
`rewritesToWithSortRewriteRule` Mock.f x
138139
)
@@ -146,7 +147,7 @@ test_simplifyRule_RewriteRule =
146147
Pair (Mock.cf, makeEqualsPredicate Mock.testSort Mock.b Mock.b)
147148
expected = [rule]
148149

149-
actual <- runSimplifyRule rule
150+
actual <- runSimplifyRuleNoSMT rule
150151

151152
assertEqual "" expected actual
152153

@@ -156,7 +157,7 @@ test_simplifyRule_RewriteRule =
156157
, Mock.b `rewritesToWithSortRewriteRule` Mock.cf
157158
]
158159

159-
actual <- runSimplifyRule
160+
actual <- runSimplifyRuleNoSMT
160161
( mkOr Mock.a Mock.b
161162
`rewritesToWithSortRewriteRule`
162163
Mock.cf
@@ -168,7 +169,7 @@ test_simplifyRule_RewriteRule =
168169
[ Mock.functional10 x `rewritesToWithSortRewriteRule` Mock.a
169170
]
170171

171-
actual <- runSimplifyRule
172+
actual <- runSimplifyRuleNoSMT
172173
( Pair (Mock.functional10 x, makeTruePredicate Mock.testSort)
173174
`rewritesToWithSortRewriteRule`
174175
Pair (Mock.a, makeTruePredicate Mock.testSort)
@@ -192,14 +193,14 @@ test_simplifyRule_OnePathRule =
192193
let rule = Mock.a `rewritesToWithSort` Mock.cf
193194
expected = [rule]
194195

195-
actual <- runSimplifyRule rule
196+
actual <- runSimplifyRuleNoSMT rule
196197

197198
assertEqual "" expected actual
198199

199200
, testCase "Simplify lhs term" $ do
200201
let expected = [Mock.a `rewritesToWithSort` Mock.cf]
201202

202-
actual <- runSimplifyRule
203+
actual <- runSimplifyRuleNoSMT
203204
( mkAnd Mock.a (mkEquals Mock.testSort Mock.a Mock.a)
204205
`rewritesToWithSort`
205206
Mock.cf
@@ -214,14 +215,14 @@ test_simplifyRule_OnePathRule =
214215
mkAnd Mock.cf (mkEquals Mock.testSort Mock.a Mock.a)
215216
expected = [rule]
216217

217-
actual <- runSimplifyRule rule
218+
actual <- runSimplifyRuleNoSMT rule
218219

219220
assertEqual "" expected actual
220221

221222
, testCase "Substitution in lhs term" $ do
222223
let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b]
223224

224-
actual <- runSimplifyRule
225+
actual <- runSimplifyRuleNoSMT
225226
( mkAnd Mock.a (mkEquals Mock.testSort Mock.b x)
226227
`rewritesToWithSort` Mock.f x
227228
)
@@ -231,7 +232,7 @@ test_simplifyRule_OnePathRule =
231232
, testCase "Simplifies requires predicate" $ do
232233
let expected = [Mock.a `rewritesToWithSort` Mock.cf]
233234

234-
actual <- runSimplifyRule
235+
actual <- runSimplifyRuleNoSMT
235236
( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b Mock.b)
236237
`rewritesToWithSort`
237238
Pair (Mock.cf, makeTruePredicate Mock.testSort)
@@ -246,14 +247,14 @@ test_simplifyRule_OnePathRule =
246247
Pair (Mock.cf, makeEqualsPredicate Mock.testSort Mock.b Mock.b)
247248
expected = [rule]
248249

249-
actual <- runSimplifyRule rule
250+
actual <- runSimplifyRuleNoSMT rule
250251

251252
assertEqual "" expected actual
252253

253254
, testCase "Substitution in requires predicate" $ do
254255
let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b]
255256

256-
actual <- runSimplifyRule
257+
actual <- runSimplifyRuleNoSMT
257258
( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b x)
258259
`rewritesToWithSort`
259260
Pair (Mock.f x, makeTruePredicate Mock.testSort)
@@ -267,7 +268,7 @@ test_simplifyRule_OnePathRule =
267268
, Mock.b `rewritesToWithSort` Mock.cf
268269
]
269270

270-
actual <- runSimplifyRule
271+
actual <- runSimplifyRuleNoSMT
271272
( mkOr Mock.a Mock.b
272273
`rewritesToWithSort`
273274
Mock.cf
@@ -294,7 +295,7 @@ test_simplifyRule_OnePathRule =
294295
[ Mock.functional10 x `rewritesToWithSort` Mock.a
295296
]
296297

297-
actual <- runSimplifyRule
298+
actual <- runSimplifyRuleNoSMT
298299
( Pair (Mock.functional10 x, makeTruePredicate Mock.testSort)
299300
`rewritesToWithSort`
300301
Pair (Mock.a, makeTruePredicate Mock.testSort)
@@ -303,7 +304,7 @@ test_simplifyRule_OnePathRule =
303304
assertEqual "" expected actual
304305
, testCase "Predicate simplification removes trivial claim" $ do
305306
let expected = []
306-
actual <- runSimplifyRule
307+
actual <- runSimplifyRuleNoSMT
307308
( Pair
308309
( Mock.b
309310
, makeAndPredicate
@@ -331,13 +332,24 @@ test_simplifyRule_OnePathRule =
331332

332333
x = mkElemVar Mock.x
333334

335+
runSimplifyRuleNoSMT
336+
:: SimplifyRuleLHS rule
337+
=> rule
338+
-> IO [rule]
339+
runSimplifyRuleNoSMT rule =
340+
fmap MultiAnd.extractPatterns
341+
$ runNoSMT
342+
$ runSimplifier Mock.env $ do
343+
SMT.All.declare Mock.smtDeclarations
344+
simplifyRuleLhs rule
345+
334346
runSimplifyRule
335347
:: SimplifyRuleLHS rule
336348
=> rule
337349
-> IO [rule]
338350
runSimplifyRule rule =
339351
fmap MultiAnd.extractPatterns
340-
$ runNoSMT
352+
$ runSMT (pure ())
341353
$ runSimplifier Mock.env $ do
342354
SMT.All.declare Mock.smtDeclarations
343355
simplifyRuleLhs rule
@@ -412,7 +424,7 @@ test_simplifyClaimRule =
412424
assertEqual "" expect (MultiAnd.extractPatterns actual)
413425
where
414426
run =
415-
runNoSMT
427+
runSMT (pure ())
416428
. runSimplifier env
417429
. flip runReaderT TestEnv
418430
{ replacements, input, requires = aEqualsb }

‎kore/test/Test/Kore/Step/SMT/Helpers.hs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -181,10 +181,9 @@ getSmtResult
181181
let
182182
smtResult :: SMT SMT.Result
183183
smtResult = do
184-
preludeAction
185184
sequence_ actions
186185
SMT.check
187-
runSMT (pure ()) smtResult
186+
runSMT preludeAction smtResult
188187

189188
assertSmtResult
190189
:: HasCallStack

0 commit comments

Comments
 (0)