Merge branch 'master' into remove-sort-checks

Author: emarzion

.github/workflows/test.yml

@@ -4,7 +4,10 @@ on:
 jobs:
   nix:
     name: 'Nix'
-    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    runs-on: ${{ matrix.os }}
     steps:
       - name: Check out code
         uses: actions/[email protected]

kore/CHANGELOG.md

@@ -14,6 +14,18 @@ All notable changes to this project will be documented in this file.
 
 ### Fixed
 
+## [0.41.0.0] - 2021-03-05
+
+### Changed
+
+- Clauses in the side condition of a configuration are considered when
+  simplifying applying equations to other clauses in the side condition (#2393).
+
+### Fixed
+
+- Values of the `BYTES.Bytes` sort are unparsed in the correct 8-bit encoding
+  instead of the base-16 encoding. (#2411)
+
 ## [0.40.0.0] - 2021-02-17
 
 ### Fixed

kore/kore.cabal

@@ -4,10 +4,10 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 03c98e7a7113ac321409caf3539c3987574f8cb7fa4049e7fb285d8c462de491
+-- hash: 2702a5d875e9f185a4aedc5fdcafa951249ccd4ef5edab6f1e96689991c8f13f
 
 name:           kore
-version:        0.40.0.0
+version:        0.41.0.0
 description:    Please see the [README](README.md) file.
 category:       Language
 homepage:       https://github.com/kframework/kore#readme

kore/package.yaml

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

kore/src/Kore/Internal/Conditional.hs

@@ -90,7 +90,7 @@ quadratic complexity.
  -}
 data Conditional variable child =
     Conditional
-        { term :: child
+        { term :: !child
         , predicate :: !(Predicate variable)
         , substitution :: !(Substitution variable)
         }

kore/src/Kore/Reachability/Claim.hs

@@ -40,6 +40,7 @@ import Control.Lens
     ( Lens'
     )
 import qualified Control.Lens as Lens
+import qualified Control.Monad as Monad
 import Control.Monad.Catch
     ( Exception (..)
     , SomeException (..)
@@ -604,6 +605,7 @@ simplify' lensClaimPattern claim = do
 
     simplifyLeftHandSide =
         Lens.traverseOf (lensClaimPattern . field @"left") $ \config -> do
+            Monad.guard (not . isBottom . Conditional.term $ config)
             let definedConfig =
                     Pattern.andCondition (mkDefined <$> config)
                     $ from $ makeCeilPredicate (Conditional.term config)

kore/src/Kore/Repl.hs

@@ -16,6 +16,7 @@ import Prelude.Kore
 import Control.Concurrent.MVar
 import Control.Exception
     ( AsyncException (UserInterrupt)
+    , fromException
     )
 import qualified Control.Lens as Lens
 import Control.Monad
@@ -87,6 +88,9 @@ import Prof
     ( MonadProf
     )
 
+import Kore.Log.ErrorException
+    ( errorException
+    )
 import Kore.Unification.Procedure
     ( unificationProcedure
     )
@@ -276,9 +280,10 @@ runRepl
 
     catchEverything :: a -> m a -> m a
     catchEverything a =
-        Exception.handleAll $ \e -> liftIO $ do
-            putStrLn "Stepper evaluation errored."
-            print e
+        Exception.handleAll $ \e -> do
+            case fromException e of
+                Just (Log.SomeEntry entry) -> Log.logEntry entry
+                Nothing -> errorException e
             pure a
 
     replGreeting :: m ()

kore/src/Kore/Step/Axiom/Matcher.hs

@@ -176,6 +176,7 @@ matchOne
 matchOne pair =
     (   matchVariable    pair
     <|> matchEqualHeads  pair
+    <|> matchAnd         pair
     <|> matchExists      pair
     <|> matchForall      pair
     <|> matchApplication pair
@@ -443,6 +444,15 @@ matchDefined (Pair term1 term2)
   | Defined_ def2 <- term2 = push (Pair term1 def2)
   | otherwise = empty
 
+matchAnd
+    :: (MatchingVariable variable, MonadSimplify simplifier)
+    => Pair (TermLike variable)
+    -> MaybeT (MatcherT variable simplifier) ()
+matchAnd (Pair term1 term2)
+    | And_ _ conj1 conj2 <- term1 =
+        push (Pair conj1 term2) >> push (Pair conj2 term2)
+    | otherwise = empty
+
 -- * Implementation
 
 type MatchingVariable variable = InternalVariable variable

kore/test/Test/Kore/Reachability/Prove.hs

@@ -658,6 +658,21 @@ test_proveClaims =
         [ mkTest "OnePath" simpleOnePathClaim
         , mkTest "AllPath" simpleAllPathClaim
         ]
+    , testGroup "LHS is undefined" $
+        let mkTest name mkSimpleClaim =
+                testCase name $ do
+                    let claims = [mkSimpleClaim mkBottom_ Mock.a]
+                    actual <- proveClaims_
+                        Unlimited
+                        Unlimited
+                        []
+                        claims
+                        []
+                    assertEqual "Result is \\top" MultiAnd.top actual
+        in
+        [ mkTest "OnePath" simpleOnePathClaim
+        , mkTest "AllPath" simpleAllPathClaim
+        ]
     ]
 
 simpleAxiom

kore/test/Test/Kore/Step/Axiom/Matcher.hs

@@ -15,6 +15,7 @@ module Test.Kore.Step.Axiom.Matcher
     , test_matching_Exists
     , test_matching_Forall
     , test_matching_Equals
+    , test_matching_And
     , test_matcherOverloading
     , match
     , MatchResult
@@ -778,6 +779,32 @@ test_matching_Pair =
         [(inject xInt, mkElemVar zInt), (inject yInt, mkElemVar zInt)]
     ]
 
+test_matching_And :: [TestTree]
+test_matching_And =
+    [ matches        "and(x, x) matches x"
+        (mkAnd (mkElemVar xInt) (mkElemVar xInt))
+        (mkElemVar xInt)
+        []
+    , matches        "and(x, y) matches y"
+        (mkAnd (mkElemVar xInt) (mkElemVar yInt))
+        (mkElemVar yInt)
+        [(inject xInt, mkElemVar yInt)]
+    , matches        "and(y, x) matches y"
+        (mkAnd (mkElemVar yInt) (mkElemVar xInt))
+        (mkElemVar yInt)
+        [(inject xInt, mkElemVar yInt)]
+    , matches        "and(x, y) matches z"
+        (mkAnd (mkElemVar xInt) (mkElemVar yInt))
+        (mkElemVar zInt)
+        [(inject xInt, mkElemVar zInt), (inject yInt, mkElemVar zInt)]
+    , doesn'tMatch   "and(x, 1) does not match 2"
+        (mkAnd (mkElemVar xInt) (mkInt 1))
+        (mkInt 2)
+    , doesn'tMatch   "and(1, x) does not match 2"
+        (mkAnd (mkInt 1) (mkElemVar xInt))
+        (mkInt 2)
+    ]
+
 mkPair
     :: TermLike RewritingVariableName
     -> TermLike RewritingVariableName

nix/kore.nix.d/kore.nix

@@ -11,7 +11,7 @@
     flags = { release = false; threaded = true; };
     package = {
       specVersion = "2.2";
-      identifier = { name = "kore"; version = "0.40.0.0"; };
+      identifier = { name = "kore"; version = "0.41.0.0"; };
       license = "NCSA";
       copyright = "2018-2020 Runtime Verification Inc";
       maintainer = "[email protected]";

shell.nix

@@ -47,7 +47,7 @@ in
 shellFor {
   buildInputs =
     [
-      gnumake yq z3
+      gnumake z3
       hls-renamed
       ghcid hlint hpack stylish-haskell
       cabal-install stack