Merge branch 'master' into no-simplify-lhs

Author: emarzion

kore/CHANGELOG.md

@@ -14,6 +14,26 @@ All notable changes to this project will be documented in this file.
 
 ### Fixed
 
+## [0.39.0.0] - 2021-02-04
+
+### Added
+
+- `kore-parser` accepts the `--pattern` argument multiple times. It will
+  validate all the patterns with a single definition. (#2369)
+
+### Changed
+
+- `kore-exec --version` will report the version number and Git commit, but not
+  the build date. The build date was never reported correctly anyway. (#2370)
+
+### Fixed
+
+- The priority of equations is respected again. (#2366)
+- Terms are still equal if the backend has inferred that one is defined but not
+  the other. (#2372)
+- Uninterpreted functions appearing in the keys of maps and sets are handled
+  correctly. (#2323)
+
 ## [0.38.0.0] - 2021-01-24
 
 ### Added

kore/app/exec/Main.hs

@@ -118,14 +118,16 @@ import Kore.Log
     , SomeEntry (..)
     , WithLog
     , logEntry
-    , logWarning
     , parseKoreLogOptions
     , runKoreLog
     , unparseKoreLogOptions
     )
 import Kore.Log.ErrorException
     ( errorException
     )
+import Kore.Log.WarnBoundedModelChecker
+    ( warnBoundedModelChecker
+    )
 import Kore.Log.WarnIfLowProductivity
     ( warnIfLowProductivity
     )
@@ -770,8 +772,8 @@ koreBmc execOptions proveOptions = do
                 graphSearch
         case checkResult of
             Bounded.Proved -> return success
-            Bounded.Unknown -> do
-                logWarning "The pattern does not terminate within the bound."
+            Bounded.Unknown claim -> do
+                warnBoundedModelChecker claim
                 return success
             Bounded.Failed final -> return (failure final)
     lift $ renderResult execOptions (unparse final)

kore/kore.cabal

@@ -4,10 +4,10 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 1eb807e1a58c0a657f51fd08934c8a7e171988a07bcd9e0e4c098055595b6ac4
+-- hash: c7335f234ff802f2b2d42c8970fd41a6fa133676b9afa09d411e6222e1120d42
 
 name:           kore
-version:        0.38.0.0
+version:        0.39.0.0
 description:    Please see the [README](README.md) file.
 category:       Language
 homepage:       https://github.com/kframework/kore#readme
@@ -223,6 +223,7 @@ library
       Kore.Log.KoreLogOptions
       Kore.Log.Registry
       Kore.Log.SQLite
+      Kore.Log.WarnBoundedModelChecker
       Kore.Log.WarnFunctionWithoutEvaluators
       Kore.Log.WarnIfLowProductivity
       Kore.Log.WarnRetrySolverQuery

kore/package.yaml

@@ -1,5 +1,5 @@
 name:                kore
-version:             0.38.0.0
+version:             0.39.0.0
 github:              "kframework/kore"
 license:             NCSA
 license-file:        LICENSE

kore/src/Debug.hs

@@ -1,10 +1,10 @@
+{-# LANGUAGE UndecidableInstances #-}
+
 {- |
 Copyright   : (c) Runtime Verification, 2019
 License     : NCSA
 
  -}
-{-# LANGUAGE Strict               #-}
-{-# LANGUAGE UndecidableInstances #-}
 
 module Debug
     (
@@ -37,14 +37,6 @@ import Data.Hashable
     ( Hashed
     , unhashed
     )
-import Data.HashMap.Strict
-    ( HashMap
-    )
-import qualified Data.HashMap.Strict as HashMap
-import Data.HashSet
-    ( HashSet
-    )
-import qualified Data.HashSet as HashSet
 import Data.Int
 import Data.Map.Strict
     ( Map
@@ -340,21 +332,11 @@ instance (Debug k, Debug a) => Debug (Map.Map k a) where
         (parens (precOut >= 10) . Pretty.sep)
         ["Data.Map.Strict.fromList", debug (Map.toList as)]
 
-instance (Debug k, Debug a) => Debug (HashMap k a) where
-    debugPrec as precOut =
-        (parens (precOut >= 10) . Pretty.sep)
-        ["Data.HashMap.Strict.fromList", debug (HashMap.toList as)]
-
 instance Debug a => Debug (Set a) where
     debugPrec as precOut =
         (parens (precOut >= 10) . Pretty.sep)
         ["Data.Set.fromList", debug (Set.toList as)]
 
-instance Debug a => Debug (HashSet a) where
-    debugPrec as precOut =
-        (parens (precOut >= 10) . Pretty.sep)
-        ["Data.HashSet.fromList", debug (HashSet.toList as)]
-
 instance Debug a => Debug (Seq a) where
     debugPrec as precOut =
         (parens (precOut >= 10) . Pretty.sep)
@@ -610,16 +592,6 @@ instance
         wrapFromList diff' precOut =
             parens (precOut >= 10) $ "Data.Map.Strict.fromList" <+> diff' 10
 
-instance
-    ( Debug key, Debug value, Diff key, Diff value )
-    => Diff (HashMap key value)
-  where
-    diffPrec as bs =
-        fmap wrapFromList $ diffPrec (HashMap.toList as) (HashMap.toList bs)
-      where
-        wrapFromList diff' precOut =
-            parens (precOut >= 10) $ "Data.HashMap.Strict.fromList" <+> diff' 10
-
 instance (Debug a, Debug b, Diff a, Diff b) => Diff (a, b)
 
 instance (Debug a, Diff a) => Diff (Set a) where
@@ -629,13 +601,6 @@ instance (Debug a, Diff a) => Diff (Set a) where
         wrapFromList diff' precOut =
             parens (precOut >= 10) $ "Data.Set.fromList" <+> diff' 10
 
-instance (Debug a, Diff a) => Diff (HashSet a) where
-    diffPrec as bs =
-        fmap wrapFromList $ diffPrec (HashSet.toList as) (HashSet.toList bs)
-      where
-        wrapFromList diff' precOut =
-            parens (precOut >= 10) $ "Data.HashSet.fromList" <+> diff' 10
-
 instance Diff ExitCode
 
 instance (Debug a, Debug b, Diff a, Diff b) => Diff (Either a b)

kore/src/Kore/ASTVerifier/AttributesVerifier.hs

@@ -42,7 +42,7 @@ import Kore.AST.AstWithLocation
     ( locationFromAst
     )
 import qualified Kore.Attribute.Parser as Attribute.Parser
-import qualified Kore.Attribute.Symbol as Attribute
+import qualified Kore.Attribute.Symbol as Attribute.Symbol
 import Kore.Error
 import Kore.IndexedModule.IndexedModule
 import Kore.IndexedModule.Resolvers
@@ -149,7 +149,7 @@ verifyNoHookAttribute attributes = do
 
 verifyNoHookedSupersort
     :: MonadError (Error VerifyError) error
-    => IndexedModule Verified.Pattern Attribute.Symbol attrs
+    => IndexedModule Verified.Pattern Attribute.Symbol.Symbol attrs
     -> Attribute.Axiom SymbolOrAlias VariableName
     -> [Subsort.Subsort]
     -> error ()
@@ -176,7 +176,7 @@ verifyNoHookedSupersort indexedModule axiom subsorts = do
 verifyAxiomAttributes
     :: forall error attrs
     .  MonadError (Error VerifyError) error
-    => IndexedModule Verified.Pattern Attribute.Symbol attrs
+    => IndexedModule Verified.Pattern Attribute.Symbol.Symbol attrs
     -> Attribute.Axiom SymbolOrAlias VariableName
     -> error (Attribute.Axiom Internal.Symbol.Symbol VariableName)
 verifyAxiomAttributes indexedModule axiom = do
@@ -214,15 +214,15 @@ verifyAxiomAttributes indexedModule axiom = do
 verifySymbolAttributes
     :: forall error a
     .  MonadError (Error VerifyError) error
-    => IndexedModule Verified.Pattern Attribute.Symbol a
-    -> Attribute.Symbol
-    -> error Attribute.Symbol
+    => IndexedModule Verified.Pattern Attribute.Symbol.Symbol a
+    -> Attribute.Symbol.Symbol
+    -> error Attribute.Symbol.Symbol
 verifySymbolAttributes _ attrs = return attrs
 
 verifySortAttributes
     :: forall error a
     .  MonadError (Error VerifyError) error
-    => IndexedModule Verified.Pattern Attribute.Symbol a
-    -> Attribute.Symbol
-    -> error Attribute.Symbol
+    => IndexedModule Verified.Pattern Attribute.Symbol.Symbol a
+    -> Attribute.Symbol.Symbol
+    -> error Attribute.Symbol.Symbol
 verifySortAttributes _ attrs = return attrs

kore/src/Kore/ASTVerifier/DefinitionVerifier.hs

@@ -44,7 +44,7 @@ import Kore.ASTVerifier.ModuleVerifier
 import Kore.ASTVerifier.Verifier
 import qualified Kore.Attribute.Axiom as Attribute
 import Kore.Attribute.Parser as Attribute.Parser
-import qualified Kore.Attribute.Symbol as Attribute
+import qualified Kore.Attribute.Symbol as Attribute.Symbol
 import qualified Kore.Builtin as Builtin
 import Kore.Error
 import Kore.IndexedModule.IndexedModule
@@ -91,7 +91,7 @@ verifyAndIndexDefinition
     -> ParsedDefinition
     -> Either
         (Error VerifyError)
-        (Map.Map ModuleName (VerifiedModule Attribute.Symbol))
+        (Map.Map ModuleName (VerifiedModule Attribute.Symbol.Symbol))
 verifyAndIndexDefinition builtinVerifiers definition = do
     (indexedModules, _defaultNames) <-
         verifyAndIndexDefinitionWithBase
@@ -127,7 +127,7 @@ verifyAndIndexDefinitionWithBase
         implicitModule
             :: ImplicitIndexedModule
                 Verified.Pattern
-                Attribute.Symbol
+                Attribute.Symbol.Symbol
                 (Attribute.Axiom Internal.Symbol.Symbol VariableName)
         implicitModule = ImplicitIndexedModule implicitIndexedModule
         parsedModules = modulesByName (definitionModules definition)

kore/src/Kore/Attribute/Symbol.hs

@@ -83,6 +83,7 @@ import Kore.Attribute.Parser
 import Kore.Attribute.Smthook
 import Kore.Attribute.Smtlib
 import Kore.Attribute.SortInjection
+import Kore.Attribute.SourceLocation
 import Kore.Attribute.Symbol.Anywhere
 import Kore.Attribute.Symbol.Klabel
 import Kore.Attribute.Symbol.Memo
@@ -119,6 +120,8 @@ data Symbol =
     , klabel        :: !Klabel
     , symbolKywd    :: !SymbolKywd
     , noEvaluators  :: !NoEvaluators
+    , sourceLocation :: !SourceLocation
+    -- ^ Location in the original (source) file.
     }
     deriving (Eq, Ord, Show)
     deriving (GHC.Generic)
@@ -145,6 +148,7 @@ instance ParseAttributes Symbol where
         >=> typed @Klabel (parseAttribute attr)
         >=> typed @SymbolKywd (parseAttribute attr)
         >=> typed @NoEvaluators (parseAttribute attr)
+        >=> typed @SourceLocation (parseAttribute attr)
 
 instance From Symbol Attributes where
     from =
@@ -162,26 +166,28 @@ instance From Symbol Attributes where
             , from . klabel
             , from . symbolKywd
             , from . noEvaluators
+            , from . sourceLocation
             ]
 
 type StepperAttributes = Symbol
 
 defaultSymbolAttributes :: Symbol
 defaultSymbolAttributes =
     Symbol
-        { function      = def
-        , functional    = def
-        , constructor   = def
-        , injective     = def
-        , sortInjection = def
-        , anywhere      = def
-        , hook          = def
-        , smtlib        = def
-        , smthook       = def
-        , memo          = def
-        , klabel        = def
-        , symbolKywd    = def
-        , noEvaluators  = def
+        { function       = def
+        , functional     = def
+        , constructor    = def
+        , injective      = def
+        , sortInjection  = def
+        , anywhere       = def
+        , hook           = def
+        , smtlib         = def
+        , smthook        = def
+        , memo           = def
+        , klabel         = def
+        , symbolKywd     = def
+        , noEvaluators   = def
+        , sourceLocation = def
         }
 
 -- | See also: 'defaultSymbolAttributes'

kore/src/Kore/Attribute/Symbol/Klabel.hs

@@ -19,6 +19,7 @@ import qualified GHC.Generics as GHC
 
 import Kore.Attribute.Parser as Parser
 import Kore.Debug
+import Pretty
 
 -- | @Klabel@ represents the @klabel@ attribute for symbols.
 newtype Klabel = Klabel { getKlabel :: Maybe Text }
@@ -31,6 +32,10 @@ newtype Klabel = Klabel { getKlabel :: Maybe Text }
 instance Default Klabel where
     def = Klabel Nothing
 
+instance Pretty Klabel where
+    pretty (Klabel (Just text)) = pretty text
+    pretty (Klabel Nothing) = "<no label>"
+
 -- | Kore identifier representing the @klabel@ attribute symbol.
 klabelId :: Id
 klabelId = "klabel"