Skip to content

Commit 96c6f44

Browse files
ana-pantiliegithub-actionsrv-jenkins
authored
Add --simplifierx CL switch for all simplifier-using tools (#2941)
* Add --simplifierx CL switch for all simplifier-using tools * Format with fourmolu * Add experimental switch to simplifier environment * Add method in MonadSimplify for getting value of switch * Format with fourmolu * Fix compilation errors in other tools * Format with fourmolu * WIP: add test-simplifierx targets to Makefile * Fix test-k-simplifiers target * Bring back accidentally reverted changes * Review: fix typo Co-authored-by: github-actions <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent 2418087 commit 96c6f44

File tree

20 files changed

+488
-279
lines changed

20 files changed

+488
-279
lines changed

‎Makefile‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
include include.mk
22

33
.PHONY: all kore clean docs haddock \
4-
test test-kore test-k \
4+
test test-kore test-k test-k-simplifierx test-simplifierx \
55
kore-exec kore-repl kore-parser kore-check-functions \
66
kore-format kore-match-disjunction kore-prof
77

@@ -56,6 +56,9 @@ coverage_report: test-kore
5656
test-k:
5757
$(MAKE) -C test test
5858

59+
test-k-simplifierx:
60+
$(MAKE) -C test test-simplifierx
61+
5962
clean:
6063
$(STACK) clean --full
6164
$(STACK_HADDOCK) clean --full

‎kore/Makefile‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,15 @@ ghcid-repl:
4949
ghcid-match:
5050
$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-match-disjunction --work-dir .stack-work-ghci"
5151

52+
ghcid-check-func:
53+
$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-check-functions --work-dir .stack-work-ghci"
54+
55+
ghcid-parser:
56+
$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-parser --work-dir .stack-work-ghci"
57+
58+
ghcid-format:
59+
$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-format --work-dir .stack-work-ghci"
60+
5261
# TODO(Vladimir): remove 'hyperlink-source' when we upgrade from lts-12.10 (8.4.3)
5362
hoogle-gen:
5463
$(stack) haddock --work-dir .stack-work-hoogle; $(stack) hoogle generate --rebuild --work-dir .stack-work-hoogle -- --local

‎kore/app/check-functions/Main.hs‎

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ import Control.Monad.Catch (
1616
)
1717
import GlobalMain (
1818
ExeName (..),
19+
LocalOptions (..),
1920
loadDefinitions,
2021
loadModule,
2122
localOptions,
@@ -50,7 +51,6 @@ import Kore.Options (
5051
progDesc,
5152
str,
5253
)
53-
import Kore.Simplify.Data (evalSimplifier)
5454
import Kore.Syntax.Module (
5555
ModuleName,
5656
)
@@ -127,19 +127,27 @@ main = do
127127
checkerInfoModifiers
128128
mapM_ mainWithOptions $ localOptions options
129129

130-
mainWithOptions :: KoreCheckerOptions -> IO ()
131-
mainWithOptions opts =
132-
withBugReport exeName (bugReportOption opts) (koreCheckFunctions opts)
130+
mainWithOptions :: LocalOptions KoreCheckerOptions -> IO ()
131+
mainWithOptions localOptions@LocalOptions{execOptions} =
132+
withBugReport
133+
exeName
134+
(bugReportOption execOptions)
135+
(koreCheckFunctions localOptions)
133136
>>= exitWith
134137

135-
koreCheckFunctions :: KoreCheckerOptions -> FilePath -> IO ExitCode
136-
koreCheckFunctions opts tmpDir =
138+
koreCheckFunctions :: LocalOptions KoreCheckerOptions -> FilePath -> IO ExitCode
139+
koreCheckFunctions LocalOptions{execOptions, simplifierx} tmpDir =
137140
do
138-
definitions <- loadDefinitions [fileName opts]
139-
loadedModule <- loadModule (mainModuleName opts) definitions
140-
checkFunctions loadedModule
141-
& evalSimplifier loadedModule
141+
definitions <- loadDefinitions [fileName]
142+
loadedModule <- loadModule mainModuleName definitions
143+
checkFunctions simplifierx loadedModule
142144
& SMT.runSMT defaultConfig (pure ())
143145
return ExitSuccess
144146
& handle handleSomeException
145-
& runKoreLog tmpDir (koreLogOptions opts)
147+
& runKoreLog tmpDir koreLogOptions
148+
where
149+
KoreCheckerOptions
150+
{ fileName
151+
, mainModuleName
152+
, koreLogOptions
153+
} = execOptions

‎kore/app/exec/Main.hs‎

Lines changed: 42 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -574,9 +574,10 @@ main = do
574574
{- | Use the parsed 'KoreExecOptions' to set up output and logging, then
575575
dispatch the requested command.
576576
-}
577-
mainWithOptions :: KoreExecOptions -> IO ()
578-
mainWithOptions execOptions = do
579-
let KoreExecOptions{koreSolverOptions, bugReportOption, outputFileName} = execOptions
577+
mainWithOptions :: LocalOptions KoreExecOptions -> IO ()
578+
mainWithOptions LocalOptions{execOptions, simplifierx} = do
579+
let KoreExecOptions{koreSolverOptions, bugReportOption, outputFileName} =
580+
execOptions
580581
ensureSmtPreludeExists koreSolverOptions
581582
exitCode <-
582583
withBugReport Main.exeName bugReportOption $ \tmpDir -> do
@@ -586,7 +587,7 @@ mainWithOptions execOptions = do
586587
}
587588
writeOptionsAndKoreFiles tmpDir execOptions'
588589
e <-
589-
mainDispatch execOptions'
590+
mainDispatch LocalOptions{execOptions = execOptions', simplifierx}
590591
& handle handleWithConfiguration
591592
& handle handleSomeException
592593
& runKoreLog tmpDir koreLogOptions
@@ -612,36 +613,38 @@ mainWithOptions execOptions = do
612613
throwM someException
613614

614615
-- | Dispatch the requested command, for example 'koreProve' or 'koreRun'.
615-
mainDispatch :: KoreExecOptions -> Main ExitCode
616+
mainDispatch :: LocalOptions KoreExecOptions -> Main ExitCode
616617
mainDispatch = warnProductivity . mainDispatchWorker
617618
where
618619
warnProductivity :: Main (KFileLocations, ExitCode) -> Main ExitCode
619620
warnProductivity action = do
620621
(kFileLocations, exitCode) <- action
621622
warnIfLowProductivity kFileLocations
622623
return exitCode
623-
mainDispatchWorker :: KoreExecOptions -> Main (KFileLocations, ExitCode)
624-
mainDispatchWorker execOptions
624+
mainDispatchWorker ::
625+
LocalOptions KoreExecOptions ->
626+
Main (KFileLocations, ExitCode)
627+
mainDispatchWorker localOptions@LocalOptions{execOptions}
625628
| Just proveOptions@KoreProveOptions{bmc} <- koreProveOptions =
626629
if bmc
627-
then koreBmc execOptions proveOptions
628-
else koreProve execOptions proveOptions
630+
then koreBmc localOptions proveOptions
631+
else koreProve localOptions proveOptions
629632
| Just searchOptions <- koreSearchOptions =
630-
koreSearch execOptions searchOptions
633+
koreSearch localOptions searchOptions
631634
| Just mergeOptions <- koreMergeOptions =
632-
koreMerge execOptions mergeOptions
635+
koreMerge localOptions mergeOptions
633636
| otherwise =
634-
koreRun execOptions
637+
koreRun localOptions
635638
where
636639
KoreExecOptions{koreProveOptions} = execOptions
637640
KoreExecOptions{koreSearchOptions} = execOptions
638641
KoreExecOptions{koreMergeOptions} = execOptions
639642

640643
koreSearch ::
641-
KoreExecOptions ->
644+
LocalOptions KoreExecOptions ->
642645
KoreSearchOptions ->
643646
Main (KFileLocations, ExitCode)
644-
koreSearch execOptions searchOptions = do
647+
koreSearch LocalOptions{execOptions, simplifierx} searchOptions = do
645648
let KoreExecOptions{definitionFileName} = execOptions
646649
definition <- loadDefinitions [definitionFileName]
647650
let KoreExecOptions{mainModuleName} = execOptions
@@ -652,16 +655,23 @@ koreSearch execOptions searchOptions = do
652655
initial <- loadPattern mainModule patternFileName
653656
final <-
654657
execute execOptions mainModule $
655-
search depthLimit breadthLimit mainModule initial target config
658+
search
659+
simplifierx
660+
depthLimit
661+
breadthLimit
662+
mainModule
663+
initial
664+
target
665+
config
656666
lift $ renderResult execOptions (unparse final)
657667
return (kFileLocations definition, ExitSuccess)
658668
where
659669
KoreSearchOptions{bound, searchType} = searchOptions
660670
config = Search.Config{bound, searchType}
661671
KoreExecOptions{breadthLimit, depthLimit} = execOptions
662672

663-
koreRun :: KoreExecOptions -> Main (KFileLocations, ExitCode)
664-
koreRun execOptions = do
673+
koreRun :: LocalOptions KoreExecOptions -> Main (KFileLocations, ExitCode)
674+
koreRun LocalOptions{execOptions, simplifierx} = do
665675
let KoreExecOptions{definitionFileName} = execOptions
666676
definition <- loadDefinitions [definitionFileName]
667677
let KoreExecOptions{mainModuleName} = execOptions
@@ -670,17 +680,17 @@ koreRun execOptions = do
670680
initial <- loadPattern mainModule patternFileName
671681
(exitCode, final) <-
672682
execute execOptions mainModule $
673-
exec depthLimit breadthLimit mainModule strategy initial
683+
exec simplifierx depthLimit breadthLimit mainModule strategy initial
674684
lift $ renderResult execOptions (unparse final)
675685
return (kFileLocations definition, exitCode)
676686
where
677687
KoreExecOptions{breadthLimit, depthLimit, strategy} = execOptions
678688

679689
koreProve ::
680-
KoreExecOptions ->
690+
LocalOptions KoreExecOptions ->
681691
KoreProveOptions ->
682692
Main (KFileLocations, ExitCode)
683-
koreProve execOptions proveOptions = do
693+
koreProve LocalOptions{execOptions, simplifierx} proveOptions = do
684694
let KoreExecOptions{definitionFileName} = execOptions
685695
KoreProveOptions{specFileName} = proveOptions
686696
definition <- loadDefinitions [definitionFileName, specFileName]
@@ -696,6 +706,7 @@ koreProve execOptions proveOptions = do
696706
let KoreExecOptions{breadthLimit, depthLimit} = execOptions
697707
KoreProveOptions{graphSearch} = proveOptions
698708
prove
709+
simplifierx
699710
graphSearch
700711
breadthLimit
701712
depthLimit
@@ -785,10 +796,10 @@ koreProve execOptions proveOptions = do
785796
}
786797

787798
koreBmc ::
788-
KoreExecOptions ->
799+
LocalOptions KoreExecOptions ->
789800
KoreProveOptions ->
790801
Main (KFileLocations, ExitCode)
791-
koreBmc execOptions proveOptions = do
802+
koreBmc LocalOptions{execOptions, simplifierx} proveOptions = do
792803
let KoreExecOptions{definitionFileName} = execOptions
793804
KoreProveOptions{specFileName} = proveOptions
794805
definition <- loadDefinitions [definitionFileName, specFileName]
@@ -801,6 +812,7 @@ koreBmc execOptions proveOptions = do
801812
KoreProveOptions{graphSearch} = proveOptions
802813
checkResult <-
803814
boundedModelCheck
815+
simplifierx
804816
breadthLimit
805817
depthLimit
806818
mainModule
@@ -819,10 +831,10 @@ koreBmc execOptions proveOptions = do
819831
success = (ExitSuccess, mkTop $ mkSortVariable "R")
820832

821833
koreMerge ::
822-
KoreExecOptions ->
834+
LocalOptions KoreExecOptions ->
823835
KoreMergeOptions ->
824836
Main (KFileLocations, ExitCode)
825-
koreMerge execOptions mergeOptions = do
837+
koreMerge LocalOptions{execOptions, simplifierx} mergeOptions = do
826838
let KoreExecOptions{definitionFileName} = execOptions
827839
definition <- loadDefinitions [definitionFileName]
828840
let KoreExecOptions{mainModuleName} = execOptions
@@ -833,8 +845,12 @@ koreMerge execOptions mergeOptions = do
833845
eitherMergedRule <- execute execOptions mainModule $
834846
case maybeBatchSize of
835847
Just batchSize ->
836-
mergeRulesConsecutiveBatches batchSize mainModule ruleIds
837-
Nothing -> mergeAllRules mainModule ruleIds
848+
mergeRulesConsecutiveBatches
849+
simplifierx
850+
batchSize
851+
mainModule
852+
ruleIds
853+
Nothing -> mergeAllRules simplifierx mainModule ruleIds
838854
case eitherMergedRule of
839855
(Left err) -> do
840856
lift $ Text.hPutStrLn stderr err

‎kore/app/format/Main.hs‎

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -52,30 +52,30 @@ infoMod =
5252
<> header "kore-format - parse and render Kore definitions"
5353

5454
main :: IO ()
55-
main =
56-
do
57-
options <-
58-
mainGlobal
59-
(ExeName "kore-format")
60-
Nothing -- environment variable name for extra arguments
61-
commandLine
62-
infoMod
63-
case localOptions options of
64-
Nothing ->
65-
{- Global options were parsed, but local options were not.
66-
Exit gracefully. -}
67-
return ()
68-
Just KoreFormatOptions{fileName, width} ->
69-
do
70-
defn <- readKoreOrDie fileName
71-
let layoutOptions =
72-
defaultLayoutOptions
73-
{ layoutPageWidth =
74-
if width > 0
75-
then AvailablePerLine width 1.0
76-
else Unbounded
77-
}
78-
renderIO stdout (layoutPretty layoutOptions $ unparse defn)
55+
main = do
56+
options <-
57+
mainGlobal
58+
(ExeName "kore-format")
59+
Nothing -- environment variable name for extra arguments
60+
commandLine
61+
infoMod
62+
for_ (localOptions options) mainWorker
63+
where
64+
mainWorker
65+
LocalOptions
66+
{ execOptions =
67+
KoreFormatOptions{fileName, width}
68+
} =
69+
do
70+
defn <- readKoreOrDie fileName
71+
let layoutOptions =
72+
defaultLayoutOptions
73+
{ layoutPageWidth =
74+
if width > 0
75+
then AvailablePerLine width 1.0
76+
else Unbounded
77+
}
78+
renderIO stdout (layoutPretty layoutOptions $ unparse defn)
7979

8080
-- | Read a 'KoreDefinition' from the given file name or signal an error.
8181
readKoreOrDie :: FilePath -> IO ParsedDefinition

‎kore/app/match-disjunction/Main.hs‎

Lines changed: 16 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ import Options.Applicative (
4444
)
4545
import Prelude.Kore
4646
import Pretty
47+
import SMT (runNoSMT)
4748
import System.Clock (
4849
Clock (..),
4950
TimeSpec,
@@ -130,30 +131,35 @@ main = do
130131
parserInfoModifiers
131132
for_ (localOptions options) mainWithOptions
132133

133-
mainWithOptions :: KoreMatchDisjunctionOptions -> IO ()
134-
mainWithOptions options = do
134+
mainWithOptions :: LocalOptions KoreMatchDisjunctionOptions -> IO ()
135+
mainWithOptions localOptions@LocalOptions{execOptions} = do
135136
exitCode <-
136137
withBugReport exeName bugReportOption $ \tmpDir ->
137-
koreMatchDisjunction options
138+
koreMatchDisjunction localOptions
138139
& runKoreLog tmpDir koreLogOptions
139140
exitWith exitCode
140141
where
141-
KoreMatchDisjunctionOptions{bugReportOption} = options
142-
KoreMatchDisjunctionOptions{koreLogOptions} = options
142+
KoreMatchDisjunctionOptions{bugReportOption} = execOptions
143+
KoreMatchDisjunctionOptions{koreLogOptions} = execOptions
143144

144-
koreMatchDisjunction :: KoreMatchDisjunctionOptions -> Main ExitCode
145-
koreMatchDisjunction options = do
145+
koreMatchDisjunction :: LocalOptions KoreMatchDisjunctionOptions -> Main ExitCode
146+
koreMatchDisjunction LocalOptions{execOptions, simplifierx} = do
146147
definition <- loadDefinitions [definitionFileName]
147148
mainModule <- loadModule mainModuleName definition
148149
matchPattern <- mainParseMatchPattern mainModule matchFileName
149150
disjunctionPattern <-
150151
mainParseDisjunctionPattern mainModule disjunctionFileName
151152
final <-
152153
clockSomethingIO "Executing" $
153-
matchDisjunction mainModule matchPattern disjunctionPattern
154+
runNoSMT $
155+
matchDisjunction
156+
simplifierx
157+
mainModule
158+
matchPattern
159+
disjunctionPattern
154160
lift $
155161
renderResult
156-
options
162+
execOptions
157163
(unparse final)
158164
return ExitSuccess
159165
where
@@ -165,7 +171,7 @@ koreMatchDisjunction options = do
165171
, disjunctionFileName
166172
, matchFileName
167173
, mainModuleName
168-
} = options
174+
} = execOptions
169175

170176
mainParseDisjunctionPattern ::
171177
VerifiedModule StepperAttributes ->

0 commit comments

Comments
 (0)