Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

saw-remote-api: Out-of-date documentation in "Crucible setup values" section #1091

Closed
RyanGlScott opened this issue Feb 24, 2021 · 0 comments · Fixed by #1092
Closed

saw-remote-api: Out-of-date documentation in "Crucible setup values" section #1091

RyanGlScott opened this issue Feb 24, 2021 · 0 comments · Fixed by #1092
Labels
documentation Issues involving documentation subsystem: saw-remote-api Issues related to the SAW server and its RPC bindings

Comments

@RyanGlScott
Copy link
Contributor

Currently, the Crucible setup values section of the SAW remote API documentation lists the following values that the setup value tag can be:

  • saved
  • null value
  • Cryptol
  • array value
  • field lvalue
  • element lvalue
  • global initializer
  • global lvalue

This doesn't quite agree with what's in the current implementation of saw-remote-api, however:

instance FromJSON SetupValTag where
parseJSON =
withText "tag for setup value" $
\case
"named" -> pure TagNamedValue
"null" -> pure TagNullValue
"Cryptol" -> pure TagCryptol
"array" -> pure TagArrayValue
"struct" -> pure TagStructValue
"field" -> pure TagFieldLValue
"element lvalue" -> pure TagElemLValue
"global initializer" -> pure TagGlobalInit
"global lvalue" -> pure TagGlobalLValue
_ -> empty
instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where
parseJSON v = fromObject v
where
fromObject = withObject "saved value or Cryptol expression" $ \o ->
o .: "setup value" >>=
\case
TagNamedValue -> NamedValue <$> o .: "name"
TagNullValue -> pure NullValue
TagCryptol -> CryptolExpr <$> o .: "expression"
TagArrayValue -> ArrayValue <$> o .: "elements"
TagStructValue -> StructValue <$> o .: "fields"
TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field"
TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index"
TagGlobalInit -> GlobalInitializer <$> o .: "name"
TagGlobalLValue -> GlobalLValue <$> o .: "name"

In particular:

  • The implementation uses named, instead of saved as in the documentation.
  • The implementation uses null and array, instead of null value and array value as in the documentation.
  • The implementation uses field, instead of field lvalue as in the documentation.
  • The implementation has a struct tag that isn't mentioned in the documentation at all.

We should sync the documentation with respect to the current state of the implementation.

@RyanGlScott RyanGlScott added documentation Issues involving documentation subsystem: saw-remote-api Issues related to the SAW server and its RPC bindings labels Feb 24, 2021
@mergify mergify bot closed this as completed in #1092 Feb 25, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Issues involving documentation subsystem: saw-remote-api Issues related to the SAW server and its RPC bindings
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant