Merge remote-tracking branch 'origin/main' into georgy/simplify-impli…

…cation
runtimeverification · Jul 28, 2023 · 49c4e83 · 49c4e83
2 parents f2d5974 + 8735476
commit 49c4e83
Show file tree

Hide file tree

Showing 31 changed files with 413 additions and 113 deletions.
diff --git a/cabal.project.freeze b/cabal.project.freeze
@@ -1,5 +1,6 @@
 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,
@@ -45,6 +46,10 @@ constraints: any.Cabal ==3.6.3.0,
              byteslice +avoid-rawmemchr,
              any.bytesmith ==0.3.9.1,
              any.bytestring ==0.11.4.0,
+             any.bz2 ==1.0.1.0,
+             bz2 -cross +with-bzlib,
+             any.c2hs ==0.28.8,
+             c2hs +base3 -regression,
              any.cabal-doctest ==1.0.9,
              any.call-stack ==0.4.0,
              any.case-insensitive ==1.2.1.0,

diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs
@@ -28,15 +28,10 @@ import Network.JSONRPC
 import Kore.JsonRpc.Types
 import Kore.Syntax.Json.Types hiding (Left, Right)
 
-diffJson :: FilePath -> FilePath -> IO DiffResult
-diffJson korefile1 korefile2 = do
-    contents1 <-
-        decodeKoreRpc <$> BS.readFile korefile1
-    contents2 <-
-        decodeKoreRpc <$> BS.readFile korefile2
-
-    pure $ case (contents1, contents2) of
-        (_, _)
+diffJson :: BS.ByteString -> BS.ByteString -> DiffResult
+diffJson file1 file2 =
+    case (decodeKoreRpc file1, decodeKoreRpc file2) of
+        (contents1, contents2)
             | contents1 == contents2 ->
                 Identical $ rpcTypeOf contents1
         (NotRpcJson lines1, NotRpcJson lines2) -> do
@@ -96,22 +91,25 @@ decodeKoreRpc input =
         req <- Json.decode @Request input
         parser <- parseParams req.getReqMethod
         parseMaybe parser req.getReqParams
-    rpcResponse = fmap RpcResponse $ do
+    rpcResponse = do
         resp <- Json.decode @Response input
-        foldl1
-            (<|>)
-            [ Execute <$> parseMaybe (Json.parseJSON @ExecuteResult) resp.getResult
-            , Implies <$> parseMaybe (Json.parseJSON @ImpliesResult) resp.getResult
-            , Simplify <$> parseMaybe (Json.parseJSON @SimplifyResult) resp.getResult
-            , AddModule <$> parseMaybe (Json.parseJSON @()) resp.getResult
-            , GetModel <$> parseMaybe (Json.parseJSON @GetModelResult) resp.getResult
-            ]
+        case resp of
+            ResponseError{} -> extractError resp.getError
+            OrphanError{} -> extractError resp.getError
+            Response{} ->
+                fmap RpcResponse . try $
+                    [ Execute <$> parseMaybe (Json.parseJSON @ExecuteResult) resp.getResult
+                    , Implies <$> parseMaybe (Json.parseJSON @ImpliesResult) resp.getResult
+                    , Simplify <$> parseMaybe (Json.parseJSON @SimplifyResult) resp.getResult
+                    , AddModule <$> parseMaybe (Json.parseJSON @()) resp.getResult
+                    , GetModel <$> parseMaybe (Json.parseJSON @GetModelResult) resp.getResult
+                    ]
     rpcError =
-        Json.decode @ErrorObj input
-            >>= \case
-                ErrorObj msg code mbData ->
-                    pure $ RpcError msg code mbData
-                ErrorVal{} -> fail "arbitrary json can be an ErrorVal"
+        Json.decode @ErrorObj input >>= extractError
+    extractError = \case
+        ErrorObj msg code mbData ->
+            pure $ RpcError msg code mbData
+        ErrorVal{} -> fail "arbitrary json can be an ErrorVal"
     koreJson =
         RpcKoreJson <$> Json.decode @KoreJson input
     unknown =
@@ -137,6 +135,7 @@ instance ToJSON KoreRpcJson where
                 Execute r -> toJSON r
                 Implies r -> toJSON r
                 Simplify r -> toJSON r
+                SimplifyImplies r -> toJSON r
                 AddModule r -> toJSON r
                 GetModel r -> toJSON r
                 Cancel -> toJSON ()
@@ -181,6 +180,7 @@ rpcTypeOf = \case
         Execute _ -> ExecuteM
         Implies _ -> ImpliesM
         Simplify _ -> SimplifyM
+        SimplifyImplies _ -> SimplifyImpliesM
         AddModule _ -> AddModuleM
         GetModel _ -> GetModelM
         Cancel -> error "Cancel"

diff --git a/package.yaml b/package.yaml
@@ -125,16 +125,20 @@ executables:
       - aeson-pretty
       - base
       - bytestring
+      - bz2
       - clock
       - directory
       - extra
+      - filepath
       - hs-backend-booster
       - network
       - network-run
       - optparse-applicative
       - process
+      - tar
       - text
       - vector
+      - zlib
     ghc-options:
       - -rtsopts
   parsetest:

diff --git a/test/jsonrpc-examples/add-module.error.response b/test/jsonrpc-examples/add-module.error.response
@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":4,"error":{"code":2,"data":{"context":null,"error":"FOUNDRY-MAIN-DEPENDS-MODULE: Duplicate module"},"message":"Could not verify pattern"}}
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
diff --git a/...mples/expected/add-module.error.response@depth-limit.spaghetti-formatted.execute.response b/...mples/expected/add-module.error.response@depth-limit.spaghetti-formatted.execute.response
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/foundry-proof.implies.request: ImpliesM request
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/foundry-proof.simplify.request: SimplifyM request
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/foundry-proof2.simplify.request: SimplifyM request
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/not-json.error: non-JSON file
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/params.random.json: unknown object
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/state-a.kore.json: Kore term
diff --git a/...jsonrpc-examples/expected/[email protected] b/...jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/state-a.spaghetti-formatted.kore.json: Kore term
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/state-a.unformatted.execute.request: ExecuteM request
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/terminal.execute.response: ExecuteM response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/add-module.error.response: error response
+  * File test/jsonrpc-examples/with-logging.simplify.response: SimplifyM response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/...mples/expected/depth-limit.spaghetti-formatted.execute.response@add-module.error.response b/...mples/expected/depth-limit.spaghetti-formatted.execute.response@add-module.error.response
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/foundry-proof.implies.request: ImpliesM request
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/foundry-proof.simplify.request: SimplifyM request
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/foundry-proof2.simplify.request: SimplifyM request
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/not-json.error: non-JSON file
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/params.random.json: unknown object
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/state-a.kore.json: Kore term
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/...jsonrpc-examples/expected/[email protected] b/...jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/state-a.spaghetti-formatted.kore.json: Kore term
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/state-a.unformatted.execute.request: ExecuteM request
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/terminal.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/test/jsonrpc-examples/expected/[email protected] b/test/jsonrpc-examples/expected/[email protected]
@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/with-logging.simplify.response: SimplifyM response
+  * File test/jsonrpc-examples/add-module.error.response: error response
diff --git a/tools/kore-json-differ/Main.hs b/tools/kore-json-differ/Main.hs
@@ -31,9 +31,11 @@ main = do
         _
             | "--help" `elem` args ->
                 putStrLn usage
-        [x, y] -> do
-            result <- diffJson x y
-            BS.putStrLn $ renderResult x y result
+        [file1, file2] -> do
+            x <- BS.readFile file1
+            y <- BS.readFile file2
+            let result = diffJson x y
+            BS.putStrLn $ renderResult file1 file2 result
             exitWith $ if isIdentical result then ExitSuccess else ExitFailure 1
         _other -> do
             putStrLn $ "ERROR: program requires exactly two arguments.\n\n" <> usage