diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index cfa4ae9af3..620c1a17e0 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -351,7 +351,8 @@ mainWithOptions case searchParameters of Nothing -> do pat <- exec indexedModule strategy' purePattern - return (ExitSuccess, pat) + exitCode <- execGetExitCode indexedModule strategy' pat + return (exitCode, pat) Just (searchPattern, searchConfig) -> do pat <- search diff --git a/kore/src/Kore/AST/Valid.hs b/kore/src/Kore/AST/Valid.hs index 5e46852a88..e98a7eafe9 100644 --- a/kore/src/Kore/AST/Valid.hs +++ b/kore/src/Kore/AST/Valid.hs @@ -422,7 +422,7 @@ applySymbol , valid ~ Valid (variable level) level , pattern' ~ PurePattern level domain variable valid ) - => SentenceSymbol level pattern' + => SentenceSymbol level pattern'' -- ^ 'Symbol' declaration -> [Sort level] -- ^ 'Symbol' sort parameters @@ -477,7 +477,7 @@ applySymbol_ , valid ~ Valid (variable level) level , pattern' ~ PurePattern level domain variable valid ) - => SentenceSymbol level pattern' + => SentenceSymbol level pattern'' -> [pattern'] -> pattern' applySymbol_ sentence = applySymbol sentence [] diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index c4f930bdcf..94892bbdc5 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -10,6 +10,7 @@ Expose concrete execution as a library -} module Kore.Exec ( exec + , execGetExitCode , search , prove , proveWithRepl @@ -22,19 +23,25 @@ import Control.Monad.Trans.Except ( runExceptT ) import qualified Data.Bifunctor as Bifunctor import qualified Data.Map.Strict as Map +import System.Exit + ( ExitCode (..) ) import Data.Limit ( Limit (..) ) import Kore.AST.Common +import Kore.AST.Identifier import Kore.AST.MetaOrObject ( Object (..) ) import Kore.AST.Valid import qualified Kore.Attribute.Axiom as Attribute import qualified Kore.Builtin as Builtin +import qualified Kore.Domain.Builtin as Domain import Kore.IndexedModule.IndexedModule ( VerifiedModule ) import Kore.IndexedModule.MetadataTools ( MetadataTools (..), extractMetadataTools ) +import Kore.IndexedModule.Resolvers + ( resolveSymbol ) import qualified Kore.Logger as Log import Kore.OnePath.Verification ( Axiom (Axiom), Claim (Claim), defaultStrategy, verify ) @@ -134,6 +141,29 @@ exec indexedModule strategy purePattern = do where Valid { patternSort } = extract purePattern +-- | Project the value of the exit cell, if it is present. +execGetExitCode + :: VerifiedModule StepperAttributes Attribute.Axiom + -- ^ The main module + -> ([Rewrite] -> [Strategy (Prim Rewrite)]) + -- ^ The strategy to use for execution; see examples in "Kore.Step.Step" + -> CommonStepPattern Object + -- ^ The final pattern (top cell) to extract the exit code + -> Simplifier ExitCode +execGetExitCode indexedModule strategy' purePattern = + case resolveSymbol indexedModule $ noLocationId "LblgetExitCode" of + Left _ -> return ExitSuccess + Right (_, exitCodeSymbol) -> do + exitCodePattern <- exec indexedModule strategy' + $ applySymbol_ exitCodeSymbol [purePattern] + case exitCodePattern of + DV_ _ (Domain.BuiltinInt (Domain.InternalInt _ 0)) -> + return ExitSuccess + DV_ _ (Domain.BuiltinInt (Domain.InternalInt _ exit)) -> + return $ ExitFailure $ fromInteger exit + _ -> + return $ ExitFailure 111 + -- | Symbolic search search :: VerifiedModule StepperAttributes Attribute.Axiom diff --git a/kore/test/Test/Kore/Exec.hs b/kore/test/Test/Kore/Exec.hs index db5026ce5f..e7da10ec0e 100644 --- a/kore/test/Test/Kore/Exec.hs +++ b/kore/test/Test/Kore/Exec.hs @@ -1,12 +1,13 @@ module Test.Kore.Exec ( test_exec , test_search + , test_execGetExitCode ) where import Test.Tasty ( TestTree, testGroup ) import Test.Tasty.HUnit - ( testCase ) + ( assertEqual, testCase ) import Control.Applicative ( liftA2 ) @@ -19,6 +20,8 @@ import Data.Set import qualified Data.Set as Set import Data.Text ( Text ) +import System.Exit + ( ExitCode (..) ) import Kore.AST.Kore import Kore.AST.Sentence @@ -29,7 +32,9 @@ import Kore.ASTVerifier.DefinitionVerifier import qualified Kore.Attribute.Axiom as Attribute import Kore.Attribute.Constructor import Kore.Attribute.Functional +import Kore.Attribute.Hook import qualified Kore.Builtin as Builtin +import qualified Kore.Builtin.Int as Int import Kore.Exec import Kore.IndexedModule.IndexedModule ( VerifiedModule ) @@ -280,3 +285,87 @@ applyToNoArgs sort name = , symbolOrAliasParams = [] } [] + +test_execGetExitCode :: TestTree +test_execGetExitCode = + testGroup "execGetExitCode" + [ makeTestCase "No getExitCode symbol => ExitSuccess" + testModuleNoSymbol 42 ExitSuccess + , makeTestCase "No getExitCode simplification axiom => ExitFailure 111" + testModuleNoAxiom 42 $ ExitFailure 111 + , makeTestCase "Exit cell contains 0 => ExitSuccess" + testModuleSuccessfulSimplification 0 ExitSuccess + , makeTestCase "Exit cell contains 42 => ExitFailure 42" + testModuleSuccessfulSimplification 42 $ ExitFailure 42 + ] + where + unlimited :: Limit Integer + unlimited = Unlimited + + makeTestCase name testModule inputInteger expectedCode = + testCase name + $ actual testModule inputInteger >>= assertEqual "" expectedCode + + actual testModule exitCode = + SMT.runSMT SMT.defaultConfig + $ evalSimplifier emptyLogger + $ execGetExitCode + (verifiedMyModule testModule) + (Limit.replicate unlimited . anyRewrite) + $ Int.asInternal myIntSort exitCode + + -- Module with no getExitCode symbol + testModuleNoSymbol = Module + { moduleName = ModuleName "MY-MODULE" + , moduleSentences = [] + , moduleAttributes = Attributes [] + } + -- simplification of the exit code pattern will not produce an integer + -- (no axiom present for the symbol) + testModuleNoAxiom = Module + { moduleName = ModuleName "MY-MODULE" + , moduleSentences = + [ asSentence intSortDecl + , asSentence getExitCodeDecl + ] + , moduleAttributes = Attributes [] + } + -- simplification succeeds + testModuleSuccessfulSimplification = Module + { moduleName = ModuleName "MY-MODULE" + , moduleSentences = + [ asSentence intSortDecl + , asSentence getExitCodeDecl + , mockGetExitCodeAxiom + ] + , moduleAttributes = Attributes [] + } + + myIntSortId = testId "Int" + + myIntSort = SortActualSort $ SortActual myIntSortId [] + + intSortDecl :: VerifiedKoreSentenceSort Object + intSortDecl = SentenceSort + { sentenceSortName = myIntSortId + , sentenceSortParameters = [] + , sentenceSortAttributes = Attributes [hookAttribute Int.sort] + } + + getExitCodeId = testId "LblgetExitCode" + + getExitCodeDecl :: VerifiedKoreSentenceSymbol Object + getExitCodeDecl = + ( mkSymbol_ getExitCodeId [myIntSort] myIntSort ) + { sentenceSymbolAttributes = Attributes [functionalAttribute] } + + mockGetExitCodeAxiom = + mkEqualityAxiom + (mkApp myIntSort getExitCodeSym [mkVar v]) (mkVar v) Nothing + where + v = Variable + { variableName = testId "V" + , variableCounter = mempty + , variableSort = myIntSort + } + getExitCodeSym = SymbolOrAlias getExitCodeId []