Merge pull request #1075 from rnbguy/grpc-client-via-reflection

Use gRPC reflection to retrieve CmdExecutor file

CHANGELOG.md

@@ -17,6 +17,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - The behavior of `oneOf` has changed, existing seed values for `quint test`
   can exhibit different behavior than before (#1060)
+- `APALACHE_DIST` no longer needed to run `quint verify` (#1075)
 - Record field labels that include `::` are now illegal and raise a syntax error
   (#1086)
 

quint/apalache-dist-tests.md

@@ -58,10 +58,27 @@ APALACHE_DIST=_build/corrupt-dist-test quint verify ../examples/language-feature
 error: Apalache distribution is corrupted. Could not extract proto file from apalache.jar.
 ```
 
-### Inability to connect to the server produces an errer
+### Inability to connect to the server produces an errer (`APALACHE_DIST` unset)
 
-We now assume a correctly configured installation of Apalache, but expect that the
-server it not already running.
+We now do not set `APALACHE_DIST`, which will try to load the proto file
+dynamically, using gRPC reflection, but expect that the server is not already
+running.
+
+<!-- !test in server not running -->
+```
+quint verify ../examples/language-features/booleans.qnt
+```
+
+<!-- !test exit 1 -->
+<!-- !test err server not running -->
+```
+error: Failed to obtain a connection to Apalache after 5 seconds.
+```
+
+### Inability to connect to the server produces an errer (`APALACHE_DIST` set)
+
+We now assume a correctly configured installation of Apalache in
+`APALACHE_DIST`, but expect that the server is not already running.
 
 See https://github.com/informalsystems/quint/issues/823 for plans to manage the
 server, making this error case all but impossible.

quint/apalache-tests.md

@@ -14,7 +14,7 @@ apalache-mc server
 This requirement will be removed with https://github.com/informalsystems/quint/issues/823
 
 <!-- !test program
-APALACHE_DIST=_build/apalache bash -
+bash -
 -->
 
 ## Configuration errors
@@ -45,6 +45,11 @@ Contains an import + const instantiation.
 quint verify --invariant=Postcondition --main=BinSearch10 ../examples/classic/sequential/BinSearch/BinSearch.qnt
 ```
 
+<!-- !test check can check BinSearch10.qnt using APALACHE_DIST -->
+```
+APALACHE_DIST=_build/apalache quint verify --invariant=Postcondition --main=BinSearch10 ../examples/classic/sequential/BinSearch/BinSearch.qnt
+```
+
 ### Default `step` and `init` operators are found
 
 <!-- !test check can find default operator names -->

quint/package.json

@@ -67,7 +67,7 @@
     "yargs": "^17.2.1"
   },
   "scripts": {
-    "compile": "genversion -e src/version.ts && tsc && copyfiles -u 1 ./src/builtin.qnt ./dist/src/",
+    "compile": "genversion -e src/version.ts && tsc && copyfiles -u 1 ./src/reflection.proto ./src/builtin.qnt ./dist/src/",
     "prepare": "rm -rf ./dist && npm run compile && chmod +x ./dist/src/cli.js",
     "test": "mocha --reporter-option maxDiffSize=0 -r ts-node/register test/*.test.ts test/**/*.test.ts",
     "coverage": "nyc npm run test",

quint/src/quintVerifier.ts

@@ -22,10 +22,14 @@ import fs from 'fs'
 import os from 'os'
 import * as grpc from '@grpc/grpc-js'
 import * as proto from '@grpc/proto-loader'
+import * as protobufDescriptor from 'protobufjs/ext/descriptor'
 import { setTimeout } from 'timers/promises'
 import { promisify } from 'util'
 import { ItfTrace } from './itf'
 
+import type { Buffer } from 'buffer'
+import type { PackageDefinition as ProtoPackageDefinition } from '@grpc/proto-loader'
+
 const APALACHE_SERVER_URI = 'localhost:8822'
 // These will be addressed as we work out the packaging for apalche
 // See https://github.com/informalsystems/quint/issues/701
@@ -133,8 +137,6 @@ type CmdExecutor = {
 
 // The refined interface to the CmdExecutor we produce from the generated interface
 type AsyncCmdExecutor = {
-  // Reference to the distribution lets us start the server if needed
-  dist: ApalacheDist
   run: (req: RunRequest) => Promise<RunResponse>
   ping: () => Promise<void>
 }
@@ -152,14 +154,8 @@ function err<A>(explanation: string, errors: ErrorMessage[] = [], traces?: ItfTr
 }
 
 function findApalacheDistribution(): VerifyResult<ApalacheDist> {
-  if (!process.env.APALACHE_DIST) {
-    // TODO: fetch release if APALACHE_DIST is not configured
-    // See https://github.com/informalsystems/quint/issues/701
-    return err('APALACHE_DIST enviroment variable is not set.')
-  }
-
-  const dist = path.isAbsolute(process.env.APALACHE_DIST)
-    ? process.env.APALACHE_DIST
+  const dist = path.isAbsolute(process.env.APALACHE_DIST!)
+    ? process.env.APALACHE_DIST!
     : path.join(process.cwd(), process.env.APALACHE_DIST!)
 
   if (!fs.existsSync(dist)) {
@@ -192,7 +188,7 @@ const grpcStubOptions = {
   oneofs: true,
 }
 
-function loadGrpcClient(dist: ApalacheDist): VerifyResult<AsyncCmdExecutor> {
+function loadProtoDefViaDistribution(dist: ApalacheDist): VerifyResult<ProtoPackageDefinition> {
   const jarUtilitiyIsInstalled = spawnSync('jar', ['--version']).status === 0
   if (!jarUtilitiyIsInstalled) {
     return err('The `jar` utility must be installed')
@@ -213,45 +209,113 @@ function loadGrpcClient(dist: ApalacheDist): VerifyResult<AsyncCmdExecutor> {
   // We have the proto file loaded, so we can delete the tmp dir
   fs.rmSync(tmpDir, { recursive: true, force: true })
 
+  return right(protoDef)
+}
+
+async function loadProtoDefViaReflection(): Promise<VerifyResult<ProtoPackageDefinition>> {
+  // Types of the gRPC interface.
+  type ServerReflectionRequest = { file_containing_symbol: string }
+  type ServerReflectionResponseSuccess = {
+    file_descriptor_response: {
+      file_descriptor_proto: Buffer[]
+    }
+  }
+  type ServerReflectionResponseFailure = {
+    error_response: {
+      error_code: number
+      error_message: string
+    }
+  }
+  type ServerReflectionResponse = ServerReflectionResponseSuccess | ServerReflectionResponseFailure
+  type ServerReflectionService = {
+    new (url: string, creds: grpc.ChannelCredentials): ServerReflectionService
+    ServerReflectionInfo: () => grpc.ClientDuplexStream<ServerReflectionRequest, ServerReflectionResponse>
+  }
+  type ServerReflectionPkg = {
+    grpc: { reflection: { v1alpha: { ServerReflection: ServerReflectionService } } }
+  }
+
+  // Obtain a reflection service client
+  const protoPath = require.resolve('./reflection.proto')
+  const packageDefinition = proto.loadSync(protoPath, grpcStubOptions)
+  const reflectionProtoDescriptor = grpc.loadPackageDefinition(packageDefinition) as unknown as ServerReflectionPkg
+  const serverReflectionService = reflectionProtoDescriptor.grpc.reflection.v1alpha.ServerReflection
+  const reflectionClient = new serverReflectionService(APALACHE_SERVER_URI, grpc.credentials.createInsecure())
+
+  // Query reflection endpoint (retry if server is unreachable)
+  return retryWithTimeout(
+    () =>
+      new Promise<ServerReflectionResponse>((resolve, reject) => {
+        const call = reflectionClient.ServerReflectionInfo()
+        call.on('data', (r: ServerReflectionResponse) => {
+          call.end()
+          resolve(r)
+        })
+        call.on('error', (e: grpc.StatusObject) => reject(e))
+
+        call.write({ file_containing_symbol: 'shai.cmdExecutor.CmdExecutor' })
+      })
+  ).then(response =>
+    // Construct a proto definition of the reflection response.
+    response.chain((protoDefResponse: ServerReflectionResponse) => {
+      if ('error_response' in protoDefResponse) {
+        return err(
+          `Apalache gRPC endpoint is corrupted. Could not extract proto file: ${protoDefResponse.error_response.error_message}`
+        )
+      }
+
+      // Decode reflection response to FileDescriptorProto
+      let fileDescriptorProtos = protoDefResponse.file_descriptor_response.file_descriptor_proto.map(
+        bytes => protobufDescriptor.FileDescriptorProto.decode(bytes) as protobufDescriptor.IFileDescriptorProto
+      )
+
+      // Use proto-loader to load the FileDescriptorProto wrapped in a FileDescriptorSet
+      return right(proto.loadFileDescriptorSetFromObject({ file: fileDescriptorProtos }, grpcStubOptions))
+    })
+  )
+}
+
+function loadGrpcClient(protoDef: ProtoPackageDefinition): VerifyResult<AsyncCmdExecutor> {
   const protoDescriptor = grpc.loadPackageDefinition(protoDef)
   // The cast thru `unkown` lets us convince the type system of anything
   // See https://basarat.gitbook.io/typescript/type-system/type-assertion#double-assertion
   const pkg = protoDescriptor.shai as unknown as ShaiPkg
   const stub = new pkg.cmdExecutor.CmdExecutor(APALACHE_SERVER_URI, grpc.credentials.createInsecure())
   const impl: AsyncCmdExecutor = {
-    dist,
     run: promisify((data: RunRequest, cb: AsyncCallBack<any>) => stub.run(data, cb)),
     ping: promisify((cb: AsyncCallBack<void>) => stub.ping({}, cb)),
   }
   return right(impl)
 }
 
-// Try to connect to the server repeatedly, in .5 second intervals
-async function tryToConnect(grpcApi: AsyncCmdExecutor): Promise<VerifyResult<void>> {
-  try {
-    return await grpcApi.ping().then(right)
-  } catch {
-    // Wait .5 secs before retry
-    await setTimeout(500)
-    return tryToConnect(grpcApi)
+// Retry a function repeatedly, in .5 second intervals, until it does not throw.
+async function retry<T>(f: () => Promise<T>): Promise<T> {
+  for (;;) {
+    // avoid linter error on while(true): https://github.com/eslint/eslint/issues/5477
+    try {
+      return await f()
+    } catch {
+      // Wait .5 secs before retry
+      await setTimeout(500)
+    }
   }
 }
 
+// Call `f` repeatedly until its promise resolves, in .5 second intervals, for up to 5 seconds.
+// Returns right(T) on success, or a left(VerifyError) on timeout.
+async function retryWithTimeout<T>(f: () => Promise<T>): Promise<VerifyResult<T>> {
+  const delayMS = 5000
+  return Promise.race([
+    retry(f).then(right),
+    setTimeout(delayMS, err<T>(`Failed to obtain a connection to Apalache after ${delayMS / 1000} seconds.`)),
+  ])
+}
+
 // Try to establish a connection to the Apalache server
 //
 // A successful connection procudes an `Apalache` object.
 async function connect(cmdExecutor: AsyncCmdExecutor): Promise<VerifyResult<Apalache>> {
-  // TODO Start server of it's not already running
-  // See https://github.com/informalsystems/quint/issues/823
-  const delayMS = 5000
-  const response = await Promise.race([
-    tryToConnect(cmdExecutor),
-    setTimeout(delayMS, err(`Failed to obtain a connection to Apalache after ${delayMS / 1000} seconds.`)),
-  ])
-  // We received a response in time, so we have a valid connection to the server
-  return response.map(_pong => {
-    return apalache(cmdExecutor)
-  })
+  return retryWithTimeout(() => cmdExecutor.ping()).then(response => response.map(_ => apalache(cmdExecutor)))
 }
 
 /**
@@ -263,6 +327,12 @@ async function connect(cmdExecutor: AsyncCmdExecutor): Promise<VerifyResult<Apal
  * @returns right(void) if verification succeeds, or left(err) explaining the failure
  */
 export async function verify(config: any): Promise<VerifyResult<void>> {
-  const connectionResult = await findApalacheDistribution().chain(loadGrpcClient).asyncChain(connect)
+  // Attempt to load proto definition:
+  // - if APALACHE_DIST is set, from the Apalache distribution
+  // - otherwise, via gRPC reflection
+  const protoDefResult = process.env.APALACHE_DIST
+    ? findApalacheDistribution().chain(dist => loadProtoDefViaDistribution(dist))
+    : await loadProtoDefViaReflection()
+  const connectionResult = await protoDefResult.chain(loadGrpcClient).asyncChain(connect)
   return connectionResult.asyncChain(conn => conn.check(config))
 }