Implement getExitCode (#499)

* exit{} attribute

* execGetExitCode, extracts an exit cell's contents, returns the corresponding exit code

* generalize mkSymbol_ over the returned symbol's pattern phantom type

* add execGetExitCode tests

* Add exit{} attribute tests

* rename attribute field

Co-Authored-By: njohnwalker <[email protected]>

* review

* New mkEqualityAxiom

* remove unused attribute exit{}

Author: Nick Walker

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

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 []

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

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 []