Skip to content

Commit

Permalink
Concurrent kore-rpc strikes back (#3708)
Browse files Browse the repository at this point in the history 
This is a revert of the revert of
#3704. Needs
to be merged in sync with
runtimeverification/hs-backend-booster#427 and
also a change to `pyk` to handle the new modules IDs.

---------

Co-authored-by: Sam Balco <[email protected]>
Co-authored-by: github-actions <[email protected]>
  • Loading branch information
@geo2a @goodlyrottenapple
3 people authored Jan 24, 2024
1 parent d9fa6ae commit de63565
Show file tree
Hide file tree
Showing 9 changed files with 157 additions and 57 deletions.
2 changes: 1 addition & 1 deletion cabal.project.freeze
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ constraints: any.Cabal ==3.6.3.0,
any.json-rpc ==1.0.4,
any.junit-xml ==0.1.0.2,
any.kan-extensions ==5.2.5,
kore -threaded,
kore +threaded,
any.lens ==5.1.1,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libyaml ==0.1.2,
Expand Down
40 changes: 36 additions & 4 deletions docs/2022-07-18-JSON-RPC-Server-API.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -469,6 +469,11 @@ Same as for execute

## Add-module

* Allows extending the current rule-set of the RPC server by sending textual KORE definition of a module to the server.
* The server computes the SHA256 hash of the unparsed module string and saves the internalised module under this key, returning this ID in the response
* The optional `name-as-id` parameter allows the user to refer to the module by the name as well as the hashed ID.
* The IDs and original names are not disjoint for ease of implementation. the `m` pre-pended to the hash is necessary to make the name a valid kore identifier.

### Request

```json
Expand All @@ -477,12 +482,14 @@ Same as for execute
"id": 1,
"method": "add-module",
"params": {
"module": "module MODULE-NAME endmodule []"
"module": "module MODULE-NAME endmodule []",
"name-as-id": true
}
}
```

* `module` is a module represented in textual KORE format. The module may import modules that have been loaded or added earlier.
* `module` is a module represented in textual KORE format. The module may import modules that have been loaded or added earlier
* `name-as-id` is an optional argument which adds the module to the module map under the module name as well as the its ID.

### Error Response:

Expand All @@ -501,6 +508,23 @@ If the textual KORE in `module` is syntactically wrong, the response will use th
}
```

If two dfferent modules with the same name and `name-as-id: true` are sent, the second request will fail with a `Duplicate module name` error

```json
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"code": 8,
"message": "Duplicate module name"
}
}
```

However, if the modules are sent twice with `name-as-id: false` or without `name-as-id`, the second request will succeed.
THe request will also succeed in case the same module is sent multiple times, irrespective of the value of `name-as-id`.


Other errors, for instance, using an unknown sort or symbol, will be reported with the error code
`Could not verify pattern` and a more specific error message in the `data` field.

Expand All @@ -513,12 +537,12 @@ Responds with the name of the added module if successful.
"jsonrpc": "2.0",
"id": 1,
"result": {
"module": "MODULE-NAME"
"module": "`m<sha256_of_given_module>"
}
}
```

Module `MODULE-NAME` can now be used in subsequent requests to the server by passing `"module": "MODULE-NAME"`.
The module ID `m<sha256_of_given_module>` can now be used in subsequent requests to the server by passing `"module": "m<sha256_of_given_module>"`.

## Get-model

Expand Down Expand Up @@ -715,3 +739,11 @@ Error returned when the SMT solver crashes or is unable to discharge a goal.
## 7 Multiple states

The two errors above indicate that the execute endpoint ended up in an erroneous/inconsistent state and the returned error message is should be included in the bug report.

# 8 Invalid module

The module could not be parsed or is invalid (e.g. contains new symbols)

# 9 Duplicate module name

A module with the same name is already loaded on the server
2 changes: 2 additions & 0 deletions kore-rpc-types/src/Kore/JsonRpc/Error.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ data JsonRpcBackendError
| SmtSolverError
| Aborted
| MultipleStates
| InvalidModule
| DuplicateModuleName
deriving stock (Enum, Show)

backendError :: ToJSON a => JsonRpcBackendError -> a -> ErrorObj
Expand Down
3 changes: 2 additions & 1 deletion kore-rpc-types/src/Kore/JsonRpc/Types.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,11 +76,12 @@ data SimplifyRequest = SimplifyRequest

data AddModuleRequest = AddModuleRequest
{ _module :: Text
, nameAsId :: !(Maybe Bool)
}
deriving stock (Generic, Show, Eq)
deriving
(FromJSON, ToJSON)
via CustomJSON '[FieldLabelModifier '[StripPrefix "_"]] AddModuleRequest
via CustomJSON '[FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] AddModuleRequest

data GetModelRequest = GetModelRequest
{ state :: KoreJson
Expand Down
4 changes: 2 additions & 2 deletions kore/src/Kore/IndexedModule/IndexedModule.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ data IndexedModuleSyntax pat declAtts = IndexedModuleSyntax
!(Set.Set Id)
-- ^ set of hooked identifiers
}
deriving stock (Generic, Show, Functor, Foldable, Traversable)
deriving stock (Generic, Show, Eq, Functor, Foldable, Traversable)

-- TODO (thomas.tuegel): Consider splitting IndexedModule into separate sort,
-- symbol, and axiom indices.
Expand All @@ -157,7 +157,7 @@ data IndexedModule pat declAtts axiomAtts = IndexedModule
-- ^ map from builtin domain (symbol and sort) identifiers to the hooked
-- identifiers
}
deriving stock (Generic, Show, Functor, Foldable, Traversable)
deriving stock (Generic, Show, Eq, Functor, Foldable, Traversable)

recursiveIndexedModuleSortDescriptions ::
forall pat declAtts axiomAtts.
Expand Down
151 changes: 104 additions & 47 deletions kore/src/Kore/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,10 @@ module Kore.JsonRpc (
) where

import Control.Concurrent.MVar qualified as MVar
import Control.Monad.Except (runExceptT)
import Control.Monad.Except (MonadError (throwError), liftEither, runExceptT, withExceptT)
import Control.Monad.Logger (runLoggingT)
import Control.Monad.Trans.Except (catchE)
import Crypto.Hash (SHA256 (..), hashWith)
import Data.Aeson.Types (ToJSON (..))
import Data.Coerce (coerce)
import Data.Conduit.Network (serverSettings)
Expand All @@ -23,7 +25,9 @@ import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Sequence as Seq (Seq, empty)
import Data.Set qualified as Set
import Data.String (fromString)
import Data.Text (Text)
import Data.Text.Encoding (encodeUtf8)
import GlobalMain (
LoadedDefinition (..),
SerializedDefinition (..),
Expand Down Expand Up @@ -461,54 +465,107 @@ respond serverState moduleName runSMT =
OrPattern.toTermLike sort result
, logs = allLogs
}
AddModule AddModuleRequest{_module} ->
case parseKoreModule "<add-module>" _module of
Left err -> pure $ Left $ backendError CouldNotParsePattern err
Right parsedModule@Module{moduleName = name} -> do
LoadedDefinition{indexedModules, definedNames, kFileLocations} <-
liftIO $ loadedDefinition <$> MVar.readMVar serverState
let verified =
verifyAndIndexDefinitionWithBase
(indexedModules, definedNames)
Builtin.koreVerifiers
(Definition (def @Attributes) [parsedModule])
case verified of
Left err -> pure $ Left $ backendError CouldNotVerifyPattern err
Right (indexedModules', definedNames') ->
case Map.lookup (coerce name) indexedModules' of
Nothing -> pure $ Left $ backendError CouldNotFindModule name
Just mainModule -> do
let metadataTools = MetadataTools.build mainModule
lemmas = getSMTLemmas mainModule
serializedModule' <-
liftIO
. runSMT metadataTools lemmas
$ Exec.makeSerializedModule mainModule
internedTextCache <- liftIO $ readIORef globalInternedTextCache

liftIO . MVar.modifyMVar_ serverState $
\ServerState{serializedModules} -> do
let serializedDefinition =
SerializedDefinition
{ serializedModule = serializedModule'
, locations = kFileLocations
, internedTextCache
, lemmas
}
loadedDefinition =
LoadedDefinition
{ indexedModules = indexedModules'
, definedNames = definedNames'
, kFileLocations
}
pure
ServerState
{ serializedModules =
Map.insert (coerce name) serializedDefinition serializedModules
, loadedDefinition
AddModule AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do
let nameAsId = fromMaybe False nameAsId'
parsedModule@Module{moduleName = name} <-
withExceptT (backendError InvalidModule) $
liftEither $
parseKoreModule "<add-module>" _module
st@ServerState
{ serializedModules
, loadedDefinition = LoadedDefinition{indexedModules, definedNames, kFileLocations}
} <-
liftIO $ MVar.takeMVar serverState
let moduleHash = ModuleName . fromString . ('m' :) . show . hashWith SHA256 $ encodeUtf8 _module

-- put the original state back if we fail at any point
flip catchE (\e -> liftIO (MVar.putMVar serverState st) >> throwError e) $ do
when nameAsId $
case (Map.lookup (coerce name) indexedModules, Map.lookup (coerce moduleHash) indexedModules) of
(Just{}, Nothing) ->
-- another module with the same name already exists
throwError $ backendError DuplicateModuleName name
(Just nmMod, Just idMod)
| nmMod /= idMod ->
-- this module has previously been added and different
-- module with the same name also already exists
throwError $ backendError DuplicateModuleName name
| otherwise ->
-- this module has previously been added with name-as-id: true
-- we can allow this, since the contents of the named module
-- are the same
pure ()
_ -> pure ()

case (Map.lookup (coerce moduleHash) indexedModules, Map.lookup (coerce moduleHash) serializedModules) of
(Just foundIdxModule, Just foundSerModule) -> do
liftIO $
MVar.putMVar serverState $
if nameAsId
then -- the module already exists, but re-adding with name because name-as-id is true

ServerState
{ serializedModules =
Map.insert (coerce name) foundSerModule serializedModules
, loadedDefinition =
LoadedDefinition
{ indexedModules = Map.insert (coerce name) foundIdxModule indexedModules
, definedNames
, kFileLocations
}
}
else -- the module already exists so we don't need to add it again
st
pure . AddModule $ AddModuleResult (getModuleName moduleHash)
_ -> do
(newIndexedModules, newDefinedNames) <-
withExceptT (backendError InvalidModule) $
liftEither $
verifyAndIndexDefinitionWithBase
(indexedModules, definedNames)
Builtin.koreVerifiers
(Definition (def @Attributes) [parsedModule{moduleName = moduleHash}])

newModule <-
liftEither $
maybe (Left $ backendError CouldNotFindModule moduleHash) Right $
Map.lookup (coerce moduleHash) newIndexedModules

let metadataTools = MetadataTools.build newModule
lemmas = getSMTLemmas newModule
serializedModule <-
liftIO
. runSMT metadataTools lemmas
$ Exec.makeSerializedModule newModule
internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache

let serializedDefinition =
SerializedDefinition
{ serializedModule = serializedModule
, locations = kFileLocations
, internedTextCache = internedTextCacheHash
, lemmas = lemmas
}
newSerializedModules =
Map.fromList $
if nameAsId
then [(coerce moduleHash, serializedDefinition), (coerce name, serializedDefinition)]
else [(coerce moduleHash, serializedDefinition)]
loadedDefinition =
LoadedDefinition
{ indexedModules = (if nameAsId then Map.insert (coerce name) newModule else id) newIndexedModules
, definedNames = newDefinedNames
, kFileLocations
}

liftIO . MVar.putMVar serverState $
ServerState
{ serializedModules =
serializedModules `Map.union` newSerializedModules
, loadedDefinition
}

pure . Right . AddModule $ AddModuleResult (getModuleName name)
pure . AddModule $ AddModuleResult (getModuleName moduleHash)
GetModel GetModelRequest{state, _module} ->
withMainModule (coerce _module) $ \serializedModule lemmas ->
case verifyIn serializedModule state of
Expand Down
Loading

0 comments on commit de63565

Please sign in to comment.