Skip to content

Commit fd8775c

Browse files
dopamanegithub-actionsana-pantilierv-jenkins
authored
Check function definitions tool (#2710)
* add kore-check-functions cabal executable and Main stub * Materialize Nix expressions * draft kore-check-functions command line options * traverse module sentences * drafting function check for a sentence * use isFunctionPattern * cleanup equation pattern match * typechecks, used #2697 as loose template with extractEquations function * log error, use ExitFailure 3 to denote kore-check-function failure * WIP draft check functions test group * add license and copyright * ExitFailure 3 * add verifiedMyModule * Materialize Nix expressions * fixing test errors * move checkFunctions from Main to Kore.CheckFunctions * Materialize Nix expressions * first test typecheck * WIP testing failure * debugging unit test * use toTermLikeOld * debug tests * cleanup and typecheck * Format with fourmolu * debug too many arguments exception * Fix unit test for failing case * Format with fourmolu * Materialize Nix expressions * hlint * move checkFunctions into Kore.Exec * Materialize Nix expressions * move test_checkFunctions from Test.Kore.CheckFunctions into Test.Kore.Exec * Materialize Nix expressions * cleanup and add docs * add notes on test case * capitalization Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> * create new log type, cleanup checkFunctions * Format with fourmolu * Remove comment * Materialize Nix expressions * Make linter happy * cleanup checkFunctions, use filter Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: ana-pantilie <ana.pantilie95@gmail.com> Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>
1 parent 6394bf2 commit fd8775c

File tree

6 files changed

+360
-2
lines changed

6 files changed

+360
-2
lines changed

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

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2021
3+
License : BSD-3-Clause
4+
-}
5+
module Main (main) where
6+
7+
import GlobalMain (
8+
ExeName (..),
9+
Main,
10+
loadDefinitions,
11+
loadModule,
12+
localOptions,
13+
mainGlobal,
14+
parseModuleName,
15+
)
16+
import Kore.BugReport (
17+
BugReportOption,
18+
ExitCode,
19+
parseBugReportOption,
20+
withBugReport,
21+
)
22+
import Kore.Exec (
23+
checkFunctions,
24+
)
25+
import Kore.Log (
26+
KoreLogOptions,
27+
parseKoreLogOptions,
28+
runKoreLog,
29+
)
30+
import Kore.Options (
31+
InfoMod,
32+
Parser,
33+
argument,
34+
fullDesc,
35+
header,
36+
help,
37+
metavar,
38+
progDesc,
39+
str,
40+
)
41+
import Kore.Syntax.Module (
42+
ModuleName,
43+
)
44+
import Prelude.Kore
45+
import System.Clock (
46+
Clock (Monotonic),
47+
TimeSpec,
48+
getTime,
49+
)
50+
import System.Exit (
51+
exitWith,
52+
)
53+
54+
exeName :: ExeName
55+
exeName = ExeName "kore-check-functions"
56+
57+
-- | Modifiers for the command line parser description
58+
checkerInfoModifiers :: InfoMod options
59+
checkerInfoModifiers =
60+
fullDesc
61+
<> progDesc
62+
"Checks function definitions in FILE and verifies that for every \
63+
\equation in a function definition, the right-hand side of the \
64+
\equation is a function pattern."
65+
<> header "kore-check-functions - a tool to check function definitions"
66+
67+
data KoreCheckerOptions = KoreCheckerOptions
68+
{ -- | Name for a file containing function definitions to verify.
69+
fileName :: !FilePath
70+
, -- | Name of the main module in the definition
71+
mainModuleName :: !ModuleName
72+
, bugReportOption :: !BugReportOption
73+
, koreLogOptions :: !KoreLogOptions
74+
}
75+
76+
parseKoreCheckerOptions :: TimeSpec -> Parser KoreCheckerOptions
77+
parseKoreCheckerOptions startTime =
78+
KoreCheckerOptions
79+
<$> argument
80+
str
81+
( metavar "FILE"
82+
<> help "Kore source file to check."
83+
)
84+
<*> parseMainModuleName
85+
<*> parseBugReportOption
86+
<*> parseKoreLogOptions exeName startTime
87+
where
88+
parseMainModuleName =
89+
parseModuleName
90+
"MODULE"
91+
"module"
92+
"The name of the main module in the Kore definition."
93+
94+
main :: IO ()
95+
main = do
96+
startTime <- getTime Monotonic
97+
options <-
98+
mainGlobal
99+
exeName
100+
Nothing -- environment variable name for extra arguments
101+
(parseKoreCheckerOptions startTime)
102+
checkerInfoModifiers
103+
mapM_ mainWithOptions $ localOptions options
104+
105+
mainWithOptions :: KoreCheckerOptions -> IO ()
106+
mainWithOptions opts = do
107+
exitCode <-
108+
withBugReport exeName (bugReportOption opts) $ \tmpDir ->
109+
koreCheckFunctions opts
110+
& runKoreLog tmpDir (koreLogOptions opts)
111+
exitWith exitCode
112+
113+
koreCheckFunctions :: KoreCheckerOptions -> Main ExitCode
114+
koreCheckFunctions opts =
115+
loadDefinitions [fileName opts]
116+
>>= loadModule (mainModuleName opts)
117+
>>= checkFunctions

‎kore/kore.cabal‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -331,6 +331,7 @@ library
331331
Kore.Log.DebugUnifyBottom
332332
Kore.Log.ErrorBottomTotalFunction
333333
Kore.Log.ErrorDecidePredicateUnknown
334+
Kore.Log.ErrorEquationRightFunction
334335
Kore.Log.ErrorException
335336
Kore.Log.ErrorParse
336337
Kore.Log.ErrorRewriteLoop
@@ -597,6 +598,13 @@ executable kore-match-disjunction
597598
hs-source-dirs: app/match-disjunction
598599
build-depends: transformers >= 0.5
599600

601+
executable kore-check-functions
602+
import: haskell
603+
import: exe
604+
import: global-main
605+
main-is: Main.hs
606+
hs-source-dirs: app/check-functions
607+
600608
test-suite kore-test
601609
import: haskell
602610
import: library

‎kore/src/Kore/Exec.hs‎

Lines changed: 37 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ module Kore.Exec (
1717
proveWithRepl,
1818
boundedModelCheck,
1919
matchDisjunction,
20+
checkFunctions,
2021
Rewrite,
2122
Equality,
2223
) where
@@ -30,6 +31,7 @@ import Control.Error (
3031
)
3132
import qualified Control.Lens as Lens
3233
import Control.Monad (
34+
join,
3335
(>=>),
3436
)
3537
import Control.Monad.Catch (
@@ -66,6 +68,8 @@ import qualified Kore.Attribute.Symbol as Attribute
6668
import qualified Kore.Builtin as Builtin
6769
import Kore.Equation (
6870
Equation,
71+
extractEquations,
72+
right,
6973
)
7074
import Kore.IndexedModule.IndexedModule (
7175
VerifiedModule,
@@ -95,6 +99,9 @@ import Kore.Internal.Predicate (
9599
import qualified Kore.Internal.Predicate as Predicate
96100
import qualified Kore.Internal.SideCondition as SideCondition
97101
import Kore.Internal.TermLike
102+
import Kore.Log.ErrorEquationRightFunction (
103+
errorEquationRightFunction,
104+
)
98105
import Kore.Log.ErrorRewriteLoop (
99106
errorRewriteLoop,
100107
)
@@ -603,6 +610,34 @@ matchDisjunction mainModule matchPattern disjunctionPattern =
603610
sort = Pattern.patternSort matchPattern
604611
match = Search.matchWith SideCondition.top
605612

613+
{- | Ensure that for every equation in a function definition, the right-hand
614+
- side of the equation is a function pattern. 'checkFunctions' first extracts
615+
- equations from a verified module to a list of equations. Then it checks that
616+
- each equation in the list is a function pattern. 'filter' the equations that
617+
- fail the check, and pass the list to 'checkResults'. If there were no bad
618+
- equations, 'checkResults' returns 'ExitSuccess'. Otherwise, 'checkResults'
619+
- logs an error message for each bad equation before returning
620+
- @'ExitFailure' 3@.
621+
- See 'checkEquation',
622+
- 'Kore.Equation.Registry.extractEquations',
623+
- 'Kore.Internal.TermLike.isFunctionPattern',
624+
- and 'Kore.Log.ErrorEquationRightFunction.errorEquationRightFunction'.
625+
-}
626+
checkFunctions ::
627+
MonadLog m =>
628+
-- | The main module
629+
VerifiedModule StepperAttributes ->
630+
m ExitCode
631+
checkFunctions verifiedModule =
632+
checkResults $ filter (not . isFunctionPattern . right) equations
633+
where
634+
equations = join $ Map.elems $ extractEquations verifiedModule
635+
-- if any equations fail the check, log the equations and
636+
-- the entire function returns ExitFailure 3.
637+
checkResults [] = return ExitSuccess
638+
checkResults eqns =
639+
mapM_ errorEquationRightFunction eqns $> ExitFailure 3
640+
606641
-- | Rule merging
607642
mergeAllRules ::
608643
( MonadLog smt
@@ -698,10 +733,10 @@ extractAndSimplifyRules rules names = do
698733
return
699734
(Map.lookup ruleName registry)
700735

701-
whenDuplicate logError withNames = do
736+
whenDuplicate logErr withNames = do
702737
let duplicateNames =
703738
findCollisions . mkMapWithCollisions $ withNames
704-
unless (null duplicateNames) (logError duplicateNames)
739+
unless (null duplicateNames) (logErr duplicateNames)
705740

706741
mkMapWithCollisions ::
707742
Ord key =>

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

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
{- |
2+
Copyright : (c) Runtime Verification 2021
3+
License : BSD-3-Clause
4+
-}
5+
module Kore.Log.ErrorEquationRightFunction (
6+
ErrorEquationRightFunction (..),
7+
errorEquationRightFunction,
8+
) where
9+
10+
import Control.Monad.Catch (
11+
Exception (..),
12+
)
13+
import qualified GHC.Generics as GHC
14+
import qualified Generics.SOP as SOP
15+
import Kore.Equation.Equation (
16+
Equation,
17+
)
18+
import Kore.Internal.TermLike (
19+
VariableName,
20+
)
21+
import Log (
22+
Entry (..),
23+
MonadLog,
24+
Severity (Error),
25+
SomeEntry (SomeEntry),
26+
logError,
27+
)
28+
import Prelude.Kore
29+
import Pretty (
30+
Pretty,
31+
indent,
32+
layoutOneLine,
33+
pretty,
34+
renderText,
35+
vsep,
36+
)
37+
import SQL (
38+
Table,
39+
)
40+
41+
-- | Error when RHS of equation is not a function pattern.
42+
newtype ErrorEquationRightFunction = ErrorEquationRightFunction
43+
{ equation :: Equation VariableName
44+
}
45+
deriving stock (Show, GHC.Generic)
46+
47+
instance SOP.Generic ErrorEquationRightFunction
48+
49+
instance SOP.HasDatatypeInfo ErrorEquationRightFunction
50+
51+
instance Pretty ErrorEquationRightFunction where
52+
pretty ErrorEquationRightFunction{equation} =
53+
vsep
54+
[ "Checking equation"
55+
, indent 4 $ pretty equation
56+
, "right-hand side is not a function pattern."
57+
]
58+
59+
instance Exception ErrorEquationRightFunction where
60+
toException = toException . SomeEntry
61+
fromException exn =
62+
fromException exn >>= fromEntry
63+
64+
instance Entry ErrorEquationRightFunction where
65+
entrySeverity _ = Error
66+
helpDoc _ = "errors raised when right-hand side of equation is not a function pattern"
67+
68+
instance SQL.Table ErrorEquationRightFunction
69+
70+
-- | Error when RHS of equation is not a function pattern.
71+
errorEquationRightFunction ::
72+
MonadLog m =>
73+
Equation VariableName ->
74+
m ()
75+
errorEquationRightFunction =
76+
logError . renderText . layoutOneLine . pretty . ErrorEquationRightFunction

0 commit comments

Comments
 (0)