Merge branch 'master' into unification-refactor2

Author: emarzion

deps/k_release

@@ -1 +1 @@
-v5.1.14
+v5.1.25

docs/hooks.md

@@ -401,20 +401,29 @@ Convert an integer value to its base10 string representation.
 
 ~~~
     hooked-symbol int2string{}(Int{}) : String{}
-        [hook{}("STRING.string2int")]
+        [hook{}("STRING.int2string")]
 ~~~
 
 ### STRING.string2base
 
 Takes a string and a base and converts the string from `base` to its integer
 value.
-Currently only works for base 8, 10, and 16.
+Supports bases 2 to 36 inclusive.
 
 ~~~
     hooked-symbol string2base{}(String{}, Int{}) : Int{}
         [hook{}("STRING.string2base")]
 ~~~
 
+### STRING.base2string
+
+Convert an integer value to its base string representation.
+
+~~~
+    hooked-symbol base2string{}(/* value */ Int{}, /* base */ Int{}) : String{}
+        [hook{}("STRING.base2string")]
+~~~
+
 ### STRING.substr
 
 Substr takes a string and two indices (start and end) and returns the substring
@@ -989,3 +998,21 @@ using the provided value.
     hooked-symbol bytes2int{}(Bytes{}, Endianness{}, Signedness{}) : Int{}
         [hook{}("BYTES.bytes2int")]
 ~~~
+
+### BYTES.decodeBytes
+
+`BYTES.decodeBytes` supports `"UTF-8"`, `"UTF-16LE"`, `"UTF-16BE"`, `"UTF-32LE"`, and `"UTF-32BE"` as the first argument. If decoding UTF-8 and the input contains any invalid data then `bottom` is returned. If decoding UTF-16 or UTF-32 and the input contains any invalid data then an exception will be thrown.
+
+~~~
+    hooked-symbol decodeBytes{}(/* decoding */ String{}, /* contents */ Bytes{}) : String{}
+        [hook{}("BYTES.decodeBytes")]
+~~~
+
+### BYTES.encodeBytes
+
+`BYTES.encodeBytes` supports `"UTF-8"`, `"UTF-16LE"`, `"UTF-16BE"`, `"UTF-32LE"`, and `"UTF-32BE"` as the first argument.
+
+~~~
+    hooked-symbol encodeBytes{}(/* encoding */ String{}, /* contents */ String{}) : Bytes{}
+        [hook{}("BYTES.encodeBytes")]
+~~~

kore/app/exec/Main.hs

@@ -37,6 +37,9 @@ import qualified Data.Text.IO as Text (
  )
 import qualified GHC.Generics as GHC
 import GlobalMain
+import Kore.Attribute.Definition (
+    KFileLocations (..),
+ )
 import Kore.Attribute.Symbol as Attribute
 import Kore.BugReport
 import Kore.Exec
@@ -584,7 +587,7 @@ mainWithOptions execOptions = do
                         }
             writeOptionsAndKoreFiles tmpDir execOptions'
             e <-
-                mainDispatch execOptions' <* warnIfLowProductivity
+                mainDispatch execOptions'
                     & handle handleWithConfiguration
                     & handle handleSomeException
                     & runKoreLog tmpDir koreLogOptions
@@ -618,23 +621,34 @@ mainWithOptions execOptions = do
 
 -- | Dispatch the requested command, for example 'koreProve' or 'koreRun'.
 mainDispatch :: KoreExecOptions -> Main ExitCode
-mainDispatch execOptions
-    | Just proveOptions@KoreProveOptions{bmc} <- koreProveOptions =
-        if bmc
-            then koreBmc execOptions proveOptions
-            else koreProve execOptions proveOptions
-    | Just searchOptions <- koreSearchOptions =
-        koreSearch execOptions searchOptions
-    | Just mergeOptions <- koreMergeOptions =
-        koreMerge execOptions mergeOptions
-    | otherwise =
-        koreRun execOptions
+mainDispatch = warnProductivity . mainDispatchWorker
   where
-    KoreExecOptions{koreProveOptions} = execOptions
-    KoreExecOptions{koreSearchOptions} = execOptions
-    KoreExecOptions{koreMergeOptions} = execOptions
+    warnProductivity :: Main (KFileLocations, ExitCode) -> Main ExitCode
+    warnProductivity action = do
+        (kFileLocations, exitCode) <- action
+        warnIfLowProductivity kFileLocations
+        return exitCode
+    mainDispatchWorker :: KoreExecOptions -> Main (KFileLocations, ExitCode)
+    mainDispatchWorker execOptions
+        | Just proveOptions@KoreProveOptions{bmc} <- koreProveOptions =
+            if bmc
+                then koreBmc execOptions proveOptions
+                else koreProve execOptions proveOptions
+        | Just searchOptions <- koreSearchOptions =
+            koreSearch execOptions searchOptions
+        | Just mergeOptions <- koreMergeOptions =
+            koreMerge execOptions mergeOptions
+        | otherwise =
+            koreRun execOptions
+      where
+        KoreExecOptions{koreProveOptions} = execOptions
+        KoreExecOptions{koreSearchOptions} = execOptions
+        KoreExecOptions{koreMergeOptions} = execOptions
 
-koreSearch :: KoreExecOptions -> KoreSearchOptions -> Main ExitCode
+koreSearch ::
+    KoreExecOptions ->
+    KoreSearchOptions ->
+    Main (KFileLocations, ExitCode)
 koreSearch execOptions searchOptions = do
     let KoreExecOptions{definitionFileName} = execOptions
     definition <- loadDefinitions [definitionFileName]
@@ -648,13 +662,13 @@ koreSearch execOptions searchOptions = do
         execute execOptions mainModule $
             search depthLimit breadthLimit mainModule initial target config
     lift $ renderResult execOptions (unparse final)
-    return ExitSuccess
+    return (kFileLocations definition, ExitSuccess)
   where
     KoreSearchOptions{bound, searchType} = searchOptions
     config = Search.Config{bound, searchType}
     KoreExecOptions{breadthLimit, depthLimit} = execOptions
 
-koreRun :: KoreExecOptions -> Main ExitCode
+koreRun :: KoreExecOptions -> Main (KFileLocations, ExitCode)
 koreRun execOptions = do
     let KoreExecOptions{definitionFileName} = execOptions
     definition <- loadDefinitions [definitionFileName]
@@ -666,11 +680,14 @@ koreRun execOptions = do
         execute execOptions mainModule $
             exec depthLimit breadthLimit mainModule strategy initial
     lift $ renderResult execOptions (unparse final)
-    return exitCode
+    return (kFileLocations definition, exitCode)
   where
     KoreExecOptions{breadthLimit, depthLimit, strategy} = execOptions
 
-koreProve :: KoreExecOptions -> KoreProveOptions -> Main ExitCode
+koreProve ::
+    KoreExecOptions ->
+    KoreProveOptions ->
+    Main (KFileLocations, ExitCode)
 koreProve execOptions proveOptions = do
     let KoreExecOptions{definitionFileName} = execOptions
         KoreProveOptions{specFileName} = proveOptions
@@ -707,7 +724,7 @@ koreProve execOptions proveOptions = do
                 getRewritingPattern . getConfiguration . getStuckClaim
     lift $ for_ saveProofs $ saveProven specModule provenClaims
     lift $ renderResult execOptions (unparse final)
-    return exitCode
+    return (kFileLocations definition, exitCode)
   where
     failure pat = (ExitFailure 1, pat)
     success :: (ExitCode, TermLike VariableName)
@@ -768,7 +785,10 @@ koreProve execOptions proveOptions = do
                 , definitionModules = [provenModule]
                 }
 
-koreBmc :: KoreExecOptions -> KoreProveOptions -> Main ExitCode
+koreBmc ::
+    KoreExecOptions ->
+    KoreProveOptions ->
+    Main (KFileLocations, ExitCode)
 koreBmc execOptions proveOptions = do
     let KoreExecOptions{definitionFileName} = execOptions
         KoreProveOptions{specFileName} = proveOptions
@@ -794,12 +814,15 @@ koreBmc execOptions proveOptions = do
                 return success
             Bounded.Failed final -> return (failure final)
     lift $ renderResult execOptions (unparse final)
-    return exitCode
+    return (kFileLocations definition, exitCode)
   where
     failure pat = (ExitFailure 1, pat)
     success = (ExitSuccess, mkTop $ mkSortVariable "R")
 
-koreMerge :: KoreExecOptions -> KoreMergeOptions -> Main ExitCode
+koreMerge ::
+    KoreExecOptions ->
+    KoreMergeOptions ->
+    Main (KFileLocations, ExitCode)
 koreMerge execOptions mergeOptions = do
     let KoreExecOptions{definitionFileName} = execOptions
     definition <- loadDefinitions [definitionFileName]
@@ -816,12 +839,12 @@ koreMerge execOptions mergeOptions = do
     case eitherMergedRule of
         (Left err) -> do
             lift $ Text.hPutStrLn stderr err
-            return (ExitFailure 1)
+            return (kFileLocations definition, ExitFailure 1)
         (Right mergedRule) -> do
             let mergedRule' =
                     mergedRule <&> mapRuleVariables getRewritingVariable
             lift $ renderResult execOptions (vsep (map unparse mergedRule'))
-            return ExitSuccess
+            return (kFileLocations definition, ExitSuccess)
 
 loadRuleIds :: FilePath -> IO [Text]
 loadRuleIds fileName = do

kore/app/repl/Main.hs

@@ -215,7 +215,8 @@ mainWithOptions
                         let swapLogAction = swappableLogger mvarLogAction
                         flip runLoggerT swapLogAction $
                             runExceptionHandlers $ do
-                                definition <- loadDefinitions [definitionFileName, specFile]
+                                definition <-
+                                    loadDefinitions [definitionFileName, specFile]
                                 indexedModule <- loadModule mainModuleName definition
                                 specDefIndexedModule <- loadModule specModule definition
 
@@ -265,8 +266,10 @@ mainWithOptions
                                         outputFile
                                         mainModuleName
                                         koreLogOptions
+                                        (GlobalMain.kFileLocations definition)
 
                                 warnIfLowProductivity
+                                    (GlobalMain.kFileLocations definition)
                                 pure ExitSuccess
             exitWith exitCode
       where

kore/app/share/GlobalMain.hs

@@ -18,7 +18,7 @@ module GlobalMain (
     verifyDefinitionWithBase,
     mainParse,
     lookupMainModule,
-    LoadedDefinition,
+    LoadedDefinition (..),
     LoadedModule,
     loadDefinitions,
     loadModule,
@@ -34,6 +34,7 @@ import qualified Control.Lens as Lens
 import qualified Control.Monad as Monad
 import Data.List (
     intercalate,
+    nub,
  )
 import Data.Map.Strict (
     Map,
@@ -55,6 +56,13 @@ import Kore.ASTVerifier.DefinitionVerifier (
     verifyAndIndexDefinitionWithBase,
  )
 import Kore.ASTVerifier.PatternVerifier as PatternVerifier
+import Kore.Attribute.Definition (
+    KFileLocations (..),
+    parseKFileAttributes,
+ )
+import Kore.Attribute.SourceLocation (
+    notDefault,
+ )
 import qualified Kore.Attribute.Symbol as Attribute (
     Symbol,
  )
@@ -84,6 +92,7 @@ import Kore.Syntax
 import Kore.Syntax.Definition (
     ModuleName (..),
     ParsedDefinition,
+    definitionAttributes,
     getModuleNameForError,
  )
 import qualified Kore.Verified as Verified
@@ -473,18 +482,34 @@ mainParse parser fileName = do
 
 type LoadedModule = VerifiedModule Attribute.Symbol
 
-type LoadedDefinition = (Map ModuleName LoadedModule, Map Text AstLocation)
+data LoadedDefinition = LoadedDefinition
+    { indexedModules :: Map ModuleName LoadedModule
+    , definedNames :: Map Text AstLocation
+    , kFileLocations :: KFileLocations
+    }
 
 loadDefinitions :: [FilePath] -> Main LoadedDefinition
 loadDefinitions filePaths =
-    loadedDefinitions <&> sortClaims
+    do
+        loadedDefinitions & fmap sortClaims
   where
-    loadedDefinitions =
-        Monad.foldM verifyDefinitionWithBase mempty
-            =<< traverse parseDefinition filePaths
+    loadedDefinitions = do
+        parsedDefinitions <- traverse parseDefinition filePaths
+        let attributes = fmap definitionAttributes parsedDefinitions
+        sources <- traverse parseKFileAttributes attributes
+        let sources' = filter notDefault (nub sources)
+        (indexedModules, definedNames) <-
+            Monad.foldM verifyDefinitionWithBase mempty parsedDefinitions
+        return $
+            LoadedDefinition
+                indexedModules
+                definedNames
+                (KFileLocations sources')
 
     sortClaims :: LoadedDefinition -> LoadedDefinition
-    sortClaims = Lens._1 . Lens.traversed %~ sortModuleClaims
+    sortClaims def@LoadedDefinition{indexedModules} =
+        let indexedModules' = indexedModules & Lens.traversed %~ sortModuleClaims
+         in def{indexedModules = indexedModules'}
 
 loadModule :: ModuleName -> LoadedDefinition -> Main LoadedModule
-loadModule moduleName = lookupMainModule moduleName . fst
+loadModule moduleName = lookupMainModule moduleName . indexedModules

kore/kore.cabal

@@ -198,6 +198,7 @@ library
     Kore.Attribute.Axiom.Unit
     Kore.Attribute.Comm
     Kore.Attribute.Constructor
+    Kore.Attribute.Definition
     Kore.Attribute.Function
     Kore.Attribute.Functional
     Kore.Attribute.Hook
@@ -209,7 +210,6 @@ library
     Kore.Attribute.Overload
     Kore.Attribute.Owise
     Kore.Attribute.Parser
-    Kore.Attribute.Pattern
     Kore.Attribute.Pattern.ConstructorLike
     Kore.Attribute.Pattern.Created
     Kore.Attribute.Pattern.Defined
@@ -302,6 +302,7 @@ library
     Kore.Internal.ApplicationSorts
     Kore.Internal.Condition
     Kore.Internal.Conditional
+    Kore.Internal.From
     Kore.Internal.Inj
     Kore.Internal.InternalBool
     Kore.Internal.InternalBytes
@@ -676,6 +677,7 @@ test-suite kore-test
     Test.Kore.IndexedModule.SortGraph
     Test.Kore.Internal.ApplicationSorts
     Test.Kore.Internal.Condition
+    Test.Kore.Internal.From
     Test.Kore.Internal.Key
     Test.Kore.Internal.MultiAnd
     Test.Kore.Internal.OrCondition

kore/src/Kore/ASTVerifier/DefinitionVerifier.hs

@@ -100,7 +100,7 @@ verifyAndIndexDefinition builtinVerifiers definition = do
 {- |Verifies a `ParsedDefinition` against a preverified definition, consisting of
 map of indexed modules and a map of defined names.
 
-If verification is successfull, it returns the updated maps op indexed modules
+If verification is successfull, it returns the updated maps of indexed modules
 and defined names.
 -}
 verifyAndIndexDefinitionWithBase ::

kore/src/Kore/Attribute/Definition.hs

@@ -0,0 +1,36 @@
+{- |
+Copyright   : (c) Runtime Verification, 2021
+License     : NCSA
+-}
+module Kore.Attribute.Definition (
+    parseKFileAttributes,
+    KFileLocations (..),
+) where
+
+import Control.Monad.Catch (MonadThrow)
+import qualified Data.Default as Default
+import Data.Generics.Product (typed)
+import Kore.Attribute.Attributes (Attributes (..))
+import Kore.Attribute.Parser (ParseAttributes (..))
+import Kore.Attribute.SourceLocation (SourceLocation)
+import Kore.Error (printError)
+import Kore.Log.ErrorParse
+import Prelude.Kore
+
+{- | Location attribute for some of the K files used during execution, displayed
+by the 'WarnIfLowProductivity' warning.
+-}
+newtype KFileLocations = KFileLocations
+    {locations :: [SourceLocation]}
+    deriving stock (Show)
+
+parseKFileAttributes :: MonadThrow m => Attributes -> m SourceLocation
+parseKFileAttributes (Attributes attrs) =
+    case parser of
+        Left err -> errorParse $ printError err
+        Right sourceLocation ->
+            return sourceLocation
+  where
+    parser = foldlM (flip parseDefinitionLocation) Default.def attrs
+    parseDefinitionLocation source =
+        typed @SourceLocation (parseAttribute source)