Merge branch 'main' into _update-deps/runtimeverification/haskell-bac…

…kend
runtimeverification · Oct 19, 2023 · 0fd3cb2 · 0fd3cb2
2 parents 630ca09 + 0cc3ef5
commit 0fd3cb2
Show file tree

Hide file tree

Showing 7 changed files with 41 additions and 65 deletions.
diff --git a/cabal.project.freeze b/cabal.project.freeze
@@ -1,6 +1,5 @@
 active-repositories: hackage.haskell.org:merge
 constraints: any.Cabal ==3.6.3.0,
-             any.Diff ==0.4.1,
              any.Glob ==0.10.2,
              any.HUnit ==1.6.2.0,
              any.OneTuple ==0.3.1,

diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-6.0.125
+6.0.146
diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs
@@ -21,8 +21,9 @@ import Data.Aeson.Types (parseMaybe)
 import Data.ByteString.Lazy.Char8 qualified as BS
 import Data.Maybe (fromMaybe)
 import Network.JSONRPC
-import System.IO (hFlush)
-import System.IO.Temp (withSystemTempFile)
+import System.Exit (ExitCode (..))
+import System.FilePath
+import System.IO.Extra (withTempDir)
 import System.IO.Unsafe (unsafePerformIO)
 import System.Process (readProcessWithExitCode)
 
@@ -201,17 +202,16 @@ rpcTypeOf = \case
         Cancel -> error "Cancel"
 
 -------------------------------------------------------------------
--- pretty diff output
--- Currently using a String-based module from the Diff package but
--- which should be rewritten to handle Text and Char8.ByteString
+-- doing the actual diff when output is requested
 
 renderDiff :: BS.ByteString -> BS.ByteString -> BS.ByteString
-renderDiff first second = unsafePerformIO $ do
-    withSystemTempFile "diff_file1.txt" $ \path1 handle1 -> do
-        withSystemTempFile "diff_file2.txt" $ \path2 handle2 -> do
-            BS.hPut handle1 first
-            BS.hPut handle2 second
-            hFlush handle1
-            hFlush handle2
-            (_, str, _) <- readProcessWithExitCode "diff" ["-w", path1, path2] ""
-            return $ BS.pack str
+renderDiff first second = unsafePerformIO . withTempDir $ \dir -> do
+    let path1 = dir </> "diff_file1.txt"
+        path2 = dir </> "diff_file2.txt"
+    BS.writeFile path1 first
+    BS.writeFile path2 second
+    (result, str, _) <- readProcessWithExitCode "diff" ["-w", path1, path2] ""
+    case result of
+        ExitSuccess -> error "Unexpected result: identical content"
+        ExitFailure 1 -> pure $ BS.pack str
+        ExitFailure n -> error $ "diff process exited with code " <> show n
diff --git a/library/Booster/Syntax/ParsedKore/Parser.y b/library/Booster/Syntax/ParsedKore/Parser.y
@@ -206,24 +206,8 @@ StringLiteral :: { Text }
 ApplicationPattern :: { KorePattern }
 		    : leftAssoc '{' '}' '(' ident SortsBrace NePatterns ')'
                       { mkAssoc True $5 $6 $7 }
-		    | leftAssoc '{' '}' '(' and SortsBrace NePatterns ')'
-                      { mkAssoc True $5 $6 $7 }
-		    | leftAssoc '{' '}' '(' or SortsBrace NePatterns ')'
-                      { mkAssoc True $5 $6 $7 }
-		    | leftAssoc '{' '}' '(' implies SortsBrace NePatterns ')'
-                      { mkAssoc True $5 $6 $7 }
-		    | leftAssoc '{' '}' '(' iff SortsBrace NePatterns ')'
-                      { mkAssoc True $5 $6 $7 }
                     | rightAssoc '{' '}' '(' ident SortsBrace NePatterns ')'
                       { mkAssoc False $5 $6 $7 }
-                    | rightAssoc '{' '}' '(' and SortsBrace NePatterns ')'
-                      { mkAssoc False $5 $6 $7 }
-                    | rightAssoc '{' '}' '(' or SortsBrace NePatterns ')'
-                      { mkAssoc False $5 $6 $7 }
-                    | rightAssoc '{' '}' '(' implies SortsBrace NePatterns ')'
-                      { mkAssoc False $5 $6 $7 }
-                    | rightAssoc '{' '}' '(' iff SortsBrace NePatterns ')'
-                      { mkAssoc False $5 $6 $7 }
                     | top '{' Sort '}' '(' ')'
                       { KJTop {sort = $3} }
                     | bottom '{' Sort '}' '(' ')'
@@ -419,11 +403,6 @@ the result. Namely, \\and, \\or, \\implies, and \\iff. Designed to be passed to
 foldl1' or foldr1.
 -}
 mkApply :: Token -> [Sort] -> KorePattern -> KorePattern -> KorePattern
-mkApply tok [sort] first second
-    | Token _ TokenAnd <- tok = KJAnd sort [first, second]
-    | Token _ TokenOr <- tok = KJOr sort [first, second]
-    | Token _ TokenImplies <- tok = KJImplies sort first second
-    | Token _ TokenIff <- tok = KJIff sort first second
 mkApply tok sorts@[_, _] first second
     | Token _ (TokenIdent _) <- tok = KJApp (mkId tok) sorts [first, second]
 mkApply other _ _ _ = error $ "mkApply: unsupported token " <> show other

diff --git a/package.yaml b/package.yaml
@@ -71,7 +71,6 @@ library:
   - containers
   - deepseq
   - deriving-aeson
-  - Diff
   - exceptions
   - extra
   - filepath
@@ -93,7 +92,6 @@ library:
   - stm-conduit
   - syb
   - template-haskell
-  - temporary
   - text
   - transformers
   - unix

diff --git a/test/rpc-integration/resources/diamond.kore b/test/rpc-integration/resources/diamond.kore
@@ -318,18 +318,18 @@ module TEST
   axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(K0:SortSet{}))) [functional{}()] // functional
   axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional
   axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'Tild'Int'Unds'{}(K0:SortInt{}))) [functional{}()] // functional
-  axiom{} \right-assoc{}(\or{SortKItem{}} (\exists{SortKItem{}} (Val:SortIntCellOpt{}, inj{SortIntCellOpt{}, SortKItem{}} (Val:SortIntCellOpt{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortKItem{}} (Val:SortIntCell{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortIntCellOpt{}} (LblnoIntCell{}(), \exists{SortIntCellOpt{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortIntCellOpt{}} (Val:SortIntCell{})), \bottom{SortIntCellOpt{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv)
-  axiom{} \right-assoc{}(\or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv)
-  axiom{} \right-assoc{}(\or{SortIntCell{}} (\exists{SortIntCell{}} (X0:SortInt{}, Lbl'-LT-'int'-GT-'{}(X0:SortInt{})), \bottom{SortIntCell{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv)
-  axiom{} \right-assoc{}(\or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortIntCell{}, \exists{SortGeneratedTopCell{}} (X2:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortIntCell{}, X2:SortGeneratedCounterCell{})))), \bottom{SortGeneratedTopCell{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortIntCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortIntCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv)
+  axiom{} \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortIntCellOpt{}, inj{SortIntCellOpt{}, SortKItem{}} (Val:SortIntCellOpt{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortKItem{}} (Val:SortIntCell{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortIntCellOpt{}} (LblnoIntCell{}(), \exists{SortIntCellOpt{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortIntCellOpt{}} (Val:SortIntCell{})), \bottom{SortIntCellOpt{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv)
+  axiom{} \or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv)
+  axiom{} \or{SortIntCell{}} (\exists{SortIntCell{}} (X0:SortInt{}, Lbl'-LT-'int'-GT-'{}(X0:SortInt{})), \bottom{SortIntCell{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv)
+  axiom{} \or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortIntCell{}, \exists{SortGeneratedTopCell{}} (X2:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortIntCell{}, X2:SortGeneratedCounterCell{})))), \bottom{SortGeneratedTopCell{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortIntCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortIntCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv)
 
 // rules
 // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1369,8,1369,102)), org.kframework.attributes.Source(Source(/nix/store/392hsax8839a1kk18xkx3cs4hvz3411w-k-6.0.87-3997d65c227fde4e67cedfca83a8a2d2436229e6-maven/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]