Skip to content

Commit 563d082

Browse files
Dwight Guthgithub-actions
Dwight Guth
and
github-actions
authored
Use Data.Compact to serialize K definition at compilation time (#3017)
* deserialize compact region * serialize compact region * deepseq before compact * add compact dependency to kore.cabal * Format with fourmolu * fix lint errors * Materialize Nix expressions * allow kore-exec to use either deserialized or KORE definition * Format with fourmolu * Materialize Nix expressions * add error if serialized definition is older than executable * Format with fourmolu * Materialize Nix expressions * add comments * Format with fourmolu * Materialize Nix expressions * fix merge conflict Co-authored-by: github-actions <[email protected]>
1 parent a78dbbc commit 563d082

File tree

24 files changed

+592
-146
lines changed

24 files changed

+592
-146
lines changed

‎kore/app/exec/Main.hs‎

Lines changed: 88 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,16 @@ module Main (main) where
22

33
import Control.Lens qualified as Lens
44
import Control.Monad.Catch (
5-
MonadMask,
65
handle,
76
throwM,
87
)
98
import Control.Monad.Extra as Monad
9+
import Data.Compact (
10+
compactWithSharing,
11+
)
12+
import Data.Compact.Serialize (
13+
writeCompact,
14+
)
1015
import Data.Default (
1116
def,
1217
)
@@ -25,6 +30,9 @@ import Data.Set.Internal qualified as Set
2530
import Data.Text (
2631
unpack,
2732
)
33+
import Data.Time.Clock (
34+
UTCTime (..),
35+
)
2836
import GHC.Generics qualified as GHC
2937
import GlobalMain
3038
import Kore.Attribute.Definition (
@@ -53,8 +61,6 @@ import Kore.Internal.TermLike (
5361
)
5462
import Kore.Log (
5563
KoreLogOptions (..),
56-
LogMessage,
57-
WithLog,
5864
parseKoreLogOptions,
5965
runKoreLog,
6066
unparseKoreLogOptions,
@@ -72,6 +78,9 @@ import Kore.Log.WarnIfLowProductivity (
7278
import Kore.ModelChecker.Bounded qualified as Bounded (
7379
CheckResult (..),
7480
)
81+
import Kore.Options (
82+
enableDisableFlag,
83+
)
7584
import Kore.Parser.ParserUtils (
7685
readPositiveIntegral,
7786
)
@@ -128,7 +137,6 @@ import Options.Applicative qualified as Options
128137
import Options.Applicative.Help.Pretty qualified as OptPretty
129138
import Options.SMT (
130139
KoreSolverOptions (..),
131-
Solver (..),
132140
ensureSmtPreludeExists,
133141
parseKoreSolverOptions,
134142
unparseKoreSolverOptions,
@@ -140,13 +148,6 @@ import Pretty (
140148
hPutDoc,
141149
putDoc,
142150
)
143-
import Prof (
144-
MonadProf,
145-
)
146-
import SMT (
147-
MonadSMT,
148-
)
149-
import SMT qualified
150151
import Stats
151152
import System.Clock (
152153
Clock (Monotonic),
@@ -157,12 +158,16 @@ import System.Directory (
157158
copyFile,
158159
doesFileExist,
159160
emptyPermissions,
161+
getModificationTime,
160162
setOwnerExecutable,
161163
setOwnerReadable,
162164
setOwnerSearchable,
163165
setOwnerWritable,
164166
setPermissions,
165167
)
168+
import System.Environment (
169+
getExecutablePath,
170+
)
166171
import System.Exit (
167172
exitWith,
168173
)
@@ -280,6 +285,7 @@ data KoreExecOptions = KoreExecOptions
280285
, rtsStatistics :: !(Maybe FilePath)
281286
, bugReportOption :: !BugReportOption
282287
, maxCounterexamples :: Natural
288+
, serialize :: !Bool
283289
}
284290
deriving stock (GHC.Generic)
285291

@@ -324,6 +330,12 @@ parseKoreExecOptions startTime =
324330
<*> optional parseRtsStatistics
325331
<*> parseBugReportOption
326332
<*> parseMaxCounterexamples
333+
<*> enableDisableFlag
334+
"serialize"
335+
True
336+
False
337+
False
338+
"serialization of initialized definition to disk. [default: disabled]"
327339
parseMaxCounterexamples = counterexamples <|> pure 1
328340
where
329341
counterexamples =
@@ -441,6 +453,7 @@ koreExecSh
441453
rtsStatistics
442454
_
443455
maxCounterexamples
456+
_
444457
) =
445458
unlines $
446459
[ "#!/bin/sh"
@@ -540,19 +553,21 @@ envName = "KORE_EXEC_OPTS"
540553
main :: IO ()
541554
main = do
542555
startTime <- getTime Monotonic
556+
exePath <- getExecutablePath
557+
exeLastModifiedTime <- getModificationTime exePath
543558
options <-
544559
mainGlobal
545560
Main.exeName
546561
(Just envName)
547562
(parseKoreExecOptions startTime)
548563
parserInfoModifiers
549-
for_ (localOptions options) mainWithOptions
564+
for_ (localOptions options) $ mainWithOptions exeLastModifiedTime
550565

551566
{- | Use the parsed 'KoreExecOptions' to set up output and logging, then
552567
dispatch the requested command.
553568
-}
554-
mainWithOptions :: LocalOptions KoreExecOptions -> IO ()
555-
mainWithOptions LocalOptions{execOptions, simplifierx} = do
569+
mainWithOptions :: UTCTime -> LocalOptions KoreExecOptions -> IO ()
570+
mainWithOptions exeLastModifiedTime LocalOptions{execOptions, simplifierx} = do
556571
let KoreExecOptions{koreSolverOptions, bugReportOption, outputFileName} =
557572
execOptions
558573
ensureSmtPreludeExists koreSolverOptions
@@ -564,7 +579,7 @@ mainWithOptions LocalOptions{execOptions, simplifierx} = do
564579
}
565580
writeOptionsAndKoreFiles tmpDir execOptions'
566581
e <-
567-
mainDispatch LocalOptions{execOptions = execOptions', simplifierx}
582+
mainDispatch exeLastModifiedTime LocalOptions{execOptions = execOptions', simplifierx}
568583
& handle handleWithConfiguration
569584
& handle handleSomeException
570585
& runKoreLog
@@ -603,8 +618,8 @@ mainWithOptions LocalOptions{execOptions, simplifierx} = do
603618
throwM someException
604619

605620
-- | Dispatch the requested command, for example 'koreProve' or 'koreRun'.
606-
mainDispatch :: LocalOptions KoreExecOptions -> Main ExitCode
607-
mainDispatch = warnProductivity . mainDispatchWorker
621+
mainDispatch :: UTCTime -> LocalOptions KoreExecOptions -> Main ExitCode
622+
mainDispatch exeLastModifiedTime = warnProductivity . mainDispatchWorker
608623
where
609624
warnProductivity :: Main (KFileLocations, ExitCode) -> Main ExitCode
610625
warnProductivity action = do
@@ -620,59 +635,92 @@ mainDispatch = warnProductivity . mainDispatchWorker
620635
then koreBmc localOptions proveOptions
621636
else koreProve localOptions proveOptions
622637
| Just searchOptions <- koreSearchOptions =
623-
koreSearch localOptions searchOptions
638+
koreSearch exeLastModifiedTime localOptions searchOptions
639+
| True <- serialize =
640+
koreSerialize localOptions
624641
| otherwise =
625-
koreRun localOptions
642+
koreRun exeLastModifiedTime localOptions
626643
where
627644
KoreExecOptions{koreProveOptions} = execOptions
628645
KoreExecOptions{koreSearchOptions} = execOptions
646+
KoreExecOptions{serialize} = execOptions
629647

630648
koreSearch ::
649+
UTCTime ->
631650
LocalOptions KoreExecOptions ->
632651
KoreSearchOptions ->
633652
Main (KFileLocations, ExitCode)
634-
koreSearch LocalOptions{execOptions, simplifierx} searchOptions = do
653+
koreSearch exeLastModifiedTime LocalOptions{execOptions, simplifierx} searchOptions = do
635654
let KoreExecOptions{definitionFileName} = execOptions
636-
definition <- loadDefinitions [definitionFileName]
637655
let KoreExecOptions{mainModuleName} = execOptions
638-
mainModule <- loadModule mainModuleName definition
656+
let KoreExecOptions{koreSolverOptions} = execOptions
657+
SerializedDefinition{serializedModule, lemmas, locations} <-
658+
deserializeDefinition simplifierx koreSolverOptions definitionFileName mainModuleName exeLastModifiedTime
659+
let SerializedModule{verifiedModule, metadataTools} = serializedModule
639660
let KoreSearchOptions{searchFileName} = searchOptions
640-
target <- mainParseSearchPattern mainModule searchFileName
661+
target <- mainParseSearchPattern verifiedModule searchFileName
641662
let KoreExecOptions{patternFileName} = execOptions
642-
initial <- loadPattern mainModule patternFileName
663+
initial <- loadPattern verifiedModule patternFileName
643664
final <-
644-
execute execOptions mainModule $
665+
execute koreSolverOptions metadataTools lemmas $
645666
search
646667
simplifierx
647668
depthLimit
648669
breadthLimit
649-
mainModule
670+
serializedModule
650671
initial
651672
target
652673
config
653674
lift $ renderResult execOptions (unparse final)
654-
return (kFileLocations definition, ExitSuccess)
675+
return (locations, ExitSuccess)
655676
where
656677
KoreSearchOptions{bound, searchType} = searchOptions
657678
config = Search.Config{bound, searchType}
658679
KoreExecOptions{breadthLimit, depthLimit} = execOptions
659680

660-
koreRun :: LocalOptions KoreExecOptions -> Main (KFileLocations, ExitCode)
661-
koreRun LocalOptions{execOptions, simplifierx} = do
681+
koreRun :: UTCTime -> LocalOptions KoreExecOptions -> Main (KFileLocations, ExitCode)
682+
koreRun exeLastModifiedTime LocalOptions{execOptions, simplifierx} = do
662683
let KoreExecOptions{definitionFileName} = execOptions
663-
definition <- loadDefinitions [definitionFileName]
664684
let KoreExecOptions{mainModuleName} = execOptions
665-
mainModule <- loadModule mainModuleName definition
685+
let KoreExecOptions{koreSolverOptions} = execOptions
686+
SerializedDefinition{serializedModule, lemmas, locations} <-
687+
deserializeDefinition simplifierx koreSolverOptions definitionFileName mainModuleName exeLastModifiedTime
688+
let SerializedModule{verifiedModule, metadataTools} = serializedModule
666689
let KoreExecOptions{patternFileName} = execOptions
667-
initial <- loadPattern mainModule patternFileName
690+
initial <- loadPattern verifiedModule patternFileName
668691
(exitCode, final) <-
669-
execute execOptions mainModule $
670-
exec simplifierx depthLimit breadthLimit mainModule strategy initial
692+
execute koreSolverOptions metadataTools lemmas $
693+
exec
694+
simplifierx
695+
depthLimit
696+
breadthLimit
697+
serializedModule
698+
strategy
699+
initial
671700
lift $ renderResult execOptions (unparse final)
672-
return (kFileLocations definition, exitCode)
701+
return (locations, exitCode)
673702
where
674703
KoreExecOptions{breadthLimit, depthLimit, strategy} = execOptions
675704

705+
-- kore-exec --serialize calls this function in order to construct the definition to serialize
706+
-- and write it to the output file specified by the user. It is an error to not specify an output
707+
-- file as binary data cannot be displayed on the terminal. We put this functionality in the
708+
-- kore-exec binary because that's where most of the logic it needed in order to function already
709+
-- lived.
710+
koreSerialize :: LocalOptions KoreExecOptions -> Main (KFileLocations, ExitCode)
711+
koreSerialize LocalOptions{execOptions, simplifierx} = do
712+
let KoreExecOptions{definitionFileName} = execOptions
713+
let KoreExecOptions{mainModuleName} = execOptions
714+
let KoreExecOptions{outputFileName} = execOptions
715+
let KoreExecOptions{koreSolverOptions} = execOptions
716+
serializedDefinition@SerializedDefinition{locations} <- makeSerializedDefinition simplifierx koreSolverOptions definitionFileName mainModuleName
717+
case outputFileName of
718+
Nothing -> return (locations, ExitFailure 1)
719+
Just outputFile -> do
720+
compact <- compactWithSharing serializedDefinition & liftIO
721+
writeCompact outputFile compact & liftIO
722+
return (locations, ExitSuccess)
723+
676724
koreProve ::
677725
LocalOptions KoreExecOptions ->
678726
KoreProveOptions ->
@@ -689,7 +737,8 @@ koreProve LocalOptions{execOptions, simplifierx} proveOptions = do
689737
let KoreProveOptions{saveProofs} = proveOptions
690738
maybeAlreadyProvenModule <- loadProven definitionFileName saveProofs
691739
let KoreExecOptions{maxCounterexamples} = execOptions
692-
proveResult <- execute execOptions mainModule' $ do
740+
let KoreExecOptions{koreSolverOptions} = execOptions
741+
proveResult <- execute koreSolverOptions (MetadataTools.build mainModule) (getSMTLemmas mainModule) $ do
693742
let KoreExecOptions{breadthLimit, depthLimit} = execOptions
694743
KoreProveOptions{graphSearch, finalNodeType} = proveOptions
695744
prove
@@ -794,8 +843,9 @@ koreBmc LocalOptions{execOptions, simplifierx} proveOptions = do
794843
let KoreExecOptions{mainModuleName} = execOptions
795844
mainModule <- loadModule mainModuleName definition
796845
let KoreProveOptions{specMainModule} = proveOptions
846+
let KoreExecOptions{koreSolverOptions} = execOptions
797847
specModule <- loadModule specMainModule definition
798-
(exitCode, final) <- execute execOptions mainModule $ do
848+
(exitCode, final) <- execute koreSolverOptions (MetadataTools.build mainModule) (getSMTLemmas mainModule) $ do
799849
let KoreExecOptions{breadthLimit, depthLimit} = execOptions
800850
KoreProveOptions{graphSearch} = proveOptions
801851
checkResult <-
@@ -818,46 +868,7 @@ koreBmc LocalOptions{execOptions, simplifierx} proveOptions = do
818868
failure pat = (ExitFailure 1, pat)
819869
success = (ExitSuccess, mkTop $ mkSortVariable "R")
820870

821-
type MonadExecute exe =
822-
( MonadMask exe
823-
, MonadIO exe
824-
, MonadSMT exe
825-
, MonadProf exe
826-
, WithLog LogMessage exe
827-
)
828-
829-
-- | Run the worker in the context of the main module.
830-
execute ::
831-
forall r.
832-
KoreExecOptions ->
833-
-- | Main module
834-
LoadedModule ->
835-
-- | Worker
836-
(forall exe. MonadExecute exe => exe r) ->
837-
Main r
838-
execute options mainModule worker =
839-
clockSomethingIO "Executing" $
840-
case solver of
841-
Z3 -> withZ3
842-
None -> withoutSMT
843-
where
844-
withZ3 =
845-
SMT.runSMT
846-
config
847-
(declareSMTLemmas (MetadataTools.build mainModule) mainModule)
848-
worker
849-
withoutSMT = SMT.runNoSMT worker
850-
KoreSolverOptions{timeOut, rLimit, resetInterval, prelude, solver} =
851-
Lens.view (field @"koreSolverOptions") options
852-
config =
853-
SMT.defaultConfig
854-
{ SMT.timeOut = timeOut
855-
, SMT.rLimit = rLimit
856-
, SMT.resetInterval = resetInterval
857-
, SMT.prelude = prelude
858-
}
859-
860-
loadPattern :: LoadedModule -> Maybe FilePath -> Main (TermLike VariableName)
871+
loadPattern :: LoadedModuleSyntax -> Maybe FilePath -> Main (TermLike VariableName)
861872
loadPattern mainModule (Just fileName) =
862873
mainPatternParseAndVerify mainModule fileName
863874
loadPattern _ Nothing = error "Missing: --pattern PATTERN_FILE"

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import Kore.BugReport
88
import Kore.Exec (matchDisjunction)
99
import Kore.IndexedModule.IndexedModule (
1010
VerifiedModule,
11+
indexedModuleSyntax,
1112
)
1213
import Kore.Internal.Pattern (Pattern)
1314
import Kore.Internal.Pattern qualified as Pattern
@@ -146,7 +147,7 @@ koreMatchDisjunction :: LocalOptions KoreMatchDisjunctionOptions -> Main ExitCod
146147
koreMatchDisjunction LocalOptions{execOptions, simplifierx} = do
147148
definition <- loadDefinitions [definitionFileName]
148149
mainModule <- loadModule mainModuleName definition
149-
matchPattern <- mainParseMatchPattern mainModule matchFileName
150+
matchPattern <- mainParseMatchPattern (indexedModuleSyntax mainModule) matchFileName
150151
disjunctionPattern <-
151152
mainParseDisjunctionPattern mainModule disjunctionFileName
152153
final <-
@@ -178,7 +179,7 @@ mainParseDisjunctionPattern ::
178179
String ->
179180
Main [Pattern RewritingVariableName]
180181
mainParseDisjunctionPattern indexedModule patternFileName = do
181-
purePattern <- mainPatternParseAndVerify indexedModule patternFileName
182+
purePattern <- mainPatternParseAndVerify (indexedModuleSyntax indexedModule) patternFileName
182183
return $ parseDisjunction purePattern
183184
where
184185
parseDisjunction (Or_ _ term1 term2) =

‎kore/app/repl/Main.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,7 @@ mainWithOptions LocalOptions{execOptions, simplifierx} = do
243243
smtConfig
244244
( declareSMTLemmas
245245
(MetadataTools.build validatedDefinition)
246-
validatedDefinition
246+
(getSMTLemmas validatedDefinition)
247247
)
248248
$ proveWithRepl
249249
simplifierx

0 commit comments

Comments
 (0)