From 36ceb5670abb0e4c3ce2e994db8414b5597eccad Mon Sep 17 00:00:00 2001 From: Ranadeep Biswas Date: Mon, 24 Jul 2023 20:11:28 +0200 Subject: [PATCH 1/5] Extract Apalache proto files via grpc reflection Co-authored-by: Thomas Pani --- quint/package.json | 2 +- quint/src/quintVerifier.ts | 96 ++++++++++++++++++++++---- quint/src/reflection.proto | 136 +++++++++++++++++++++++++++++++++++++ 3 files changed, 220 insertions(+), 14 deletions(-) create mode 100644 quint/src/reflection.proto diff --git a/quint/package.json b/quint/package.json index af92c2ad4..f414e82ef 100644 --- a/quint/package.json +++ b/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", diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index becfe8db5..1aff103a5 100644 --- a/quint/src/quintVerifier.ts +++ b/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 ping: () => Promise } @@ -152,14 +154,8 @@ function err(explanation: string, errors: ErrorMessage[] = [], traces?: ItfTr } function findApalacheDistribution(): VerifyResult { - 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 { +function loadProtoDefViaDistribution(dist: ApalacheDist): VerifyResult { const jarUtilitiyIsInstalled = spawnSync('jar', ['--version']).status === 0 if (!jarUtilitiyIsInstalled) { return err('The `jar` utility must be installed') @@ -213,13 +209,81 @@ function loadGrpcClient(dist: ApalacheDist): VerifyResult { // 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> { + 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 + } + type ServerReflectionPkg = { + grpc: { reflection: { v1alpha: { ServerReflection: ServerReflectionService } } } + } + + // Obtain a reflection service client + // To load from HTTP: + // const protoJson = protobuf.parse(response.data, grpcStubOptions).root.toJSON() + // const packageDefinition = proto.fromJSON(protoJson, grpcStubOptions) + 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 + const response: VerifyResult = await new Promise( + (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(right) + .catch(e => err(`Apalache gRPC endpoint is corrupted. Error reading from streaming API: ${e.details}`)) + + return 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 { 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) => stub.run(data, cb)), ping: promisify((cb: AsyncCallBack) => stub.ping({}, cb)), } @@ -263,6 +327,12 @@ async function connect(cmdExecutor: AsyncCmdExecutor): Promise> { - 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)) } diff --git a/quint/src/reflection.proto b/quint/src/reflection.proto new file mode 100644 index 000000000..816852f82 --- /dev/null +++ b/quint/src/reflection.proto @@ -0,0 +1,136 @@ +// Copyright 2016 gRPC authors. +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// Service exported by server reflection + +syntax = "proto3"; + +package grpc.reflection.v1alpha; + +service ServerReflection { + // The reflection service is structured as a bidirectional stream, ensuring + // all related requests go to a single server. + rpc ServerReflectionInfo(stream ServerReflectionRequest) + returns (stream ServerReflectionResponse); +} + +// The message sent by the client when calling ServerReflectionInfo method. +message ServerReflectionRequest { + string host = 1; + // To use reflection service, the client should set one of the following + // fields in message_request. The server distinguishes requests by their + // defined field and then handles them using corresponding methods. + oneof message_request { + // Find a proto file by the file name. + string file_by_filename = 3; + + // Find the proto file that declares the given fully-qualified symbol name. + // This field should be a fully-qualified symbol name + // (e.g. .[.] or .). + string file_containing_symbol = 4; + + // Find the proto file which defines an extension extending the given + // message type with the given field number. + ExtensionRequest file_containing_extension = 5; + + // Finds the tag numbers used by all known extensions of the given message + // type, and appends them to ExtensionNumberResponse in an undefined order. + // Its corresponding method is best-effort: it's not guaranteed that the + // reflection service will implement this method, and it's not guaranteed + // that this method will provide all extensions. Returns + // StatusCode::UNIMPLEMENTED if it's not implemented. + // This field should be a fully-qualified type name. The format is + // . + string all_extension_numbers_of_type = 6; + + // List the full names of registered services. The content will not be + // checked. + string list_services = 7; + } +} + +// The type name and extension number sent by the client when requesting +// file_containing_extension. +message ExtensionRequest { + // Fully-qualified type name. The format should be . + string containing_type = 1; + int32 extension_number = 2; +} + +// The message sent by the server to answer ServerReflectionInfo method. +message ServerReflectionResponse { + string valid_host = 1; + ServerReflectionRequest original_request = 2; + // The server set one of the following fields accroding to the message_request + // in the request. + oneof message_response { + // This message is used to answer file_by_filename, file_containing_symbol, + // file_containing_extension requests with transitive dependencies. As + // the repeated label is not allowed in oneof fields, we use a + // FileDescriptorResponse message to encapsulate the repeated fields. + // The reflection service is allowed to avoid sending FileDescriptorProtos + // that were previously sent in response to earlier requests in the stream. + FileDescriptorResponse file_descriptor_response = 4; + + // This message is used to answer all_extension_numbers_of_type requst. + ExtensionNumberResponse all_extension_numbers_response = 5; + + // This message is used to answer list_services request. + ListServiceResponse list_services_response = 6; + + // This message is used when an error occurs. + ErrorResponse error_response = 7; + } +} + +// Serialized FileDescriptorProto messages sent by the server answering +// a file_by_filename, file_containing_symbol, or file_containing_extension +// request. +message FileDescriptorResponse { + // Serialized FileDescriptorProto messages. We avoid taking a dependency on + // descriptor.proto, which uses proto2 only features, by making them opaque + // bytes instead. + repeated bytes file_descriptor_proto = 1; +} + +// A list of extension numbers sent by the server answering +// all_extension_numbers_of_type request. +message ExtensionNumberResponse { + // Full name of the base type, including the package name. The format + // is . + string base_type_name = 1; + repeated int32 extension_number = 2; +} + +// A list of ServiceResponse sent by the server answering list_services request. +message ListServiceResponse { + // The information of each service may be expanded in the future, so we use + // ServiceResponse message to encapsulate it. + repeated ServiceResponse service = 1; +} + +// The information of a single service used by ListServiceResponse to answer +// list_services request. +message ServiceResponse { + // Full name of a registered service, including its package name. The format + // is . + string name = 1; +} + +// The error code and error message sent by the server when an error occurs. +message ErrorResponse { + // This field uses the error codes defined in grpc::StatusCode. + int32 error_code = 1; + string error_message = 2; +} From b335d25fe62596d2e91d3e4221d7bcb66a8897d9 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Tue, 1 Aug 2023 14:06:16 +0200 Subject: [PATCH 2/5] Add integration tests --- quint/apalache-dist-tests.md | 23 ++++++++++++++++++++--- quint/apalache-tests.md | 7 ++++++- 2 files changed, 26 insertions(+), 4 deletions(-) diff --git a/quint/apalache-dist-tests.md b/quint/apalache-dist-tests.md index 27d03c1b6..cc8438821 100644 --- a/quint/apalache-dist-tests.md +++ b/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. + + +``` +quint verify ../examples/language-features/booleans.qnt +``` + + + +``` +error: Apalache gRPC endpoint is corrupted. Error reading from streaming API: No connection established +``` + +### 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. diff --git a/quint/apalache-tests.md b/quint/apalache-tests.md index fb06c2e5b..74fdf41df 100644 --- a/quint/apalache-tests.md +++ b/quint/apalache-tests.md @@ -14,7 +14,7 @@ apalache-mc server This requirement will be removed with https://github.com/informalsystems/quint/issues/823 ## Configuration errors @@ -45,6 +45,11 @@ Contains an import + const instantiation. quint verify --invariant=Postcondition --main=BinSearch10 ../examples/classic/sequential/BinSearch/BinSearch.qnt ``` + +``` +APALACHE_DIST=_build/apalache quint verify --invariant=Postcondition --main=BinSearch10 ../examples/classic/sequential/BinSearch/BinSearch.qnt +``` + ### Default `step` and `init` operators are found From a836c3d76c680ad0022e08e55d50f3761d671e0b Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Tue, 1 Aug 2023 14:14:03 +0200 Subject: [PATCH 3/5] Update changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 58b96bdb4..d5f07c675 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - **Breaking**: the behavior of `oneOf` has changed, existing seed values for `quint test` can exhibit different behavior than before (#1060) - `quint run` produces a friendlier message when it meets a `const` (#1050) +- `APALACHE_DIST` no longer needed to run `quint verify` (#1075) ### Deprecated ### Removed From bc4041e12a4d9afc4419ac36a5a647c2a7123699 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Wed, 2 Aug 2023 09:54:47 +0200 Subject: [PATCH 4/5] Factor out retry functionality --- quint/src/quintVerifier.ts | 40 ++++++++++++++++++++------------------ 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index 1aff103a5..b6cbbebca 100644 --- a/quint/src/quintVerifier.ts +++ b/quint/src/quintVerifier.ts @@ -290,32 +290,34 @@ function loadGrpcClient(protoDef: ProtoPackageDefinition): VerifyResult> { - 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(f: () => Promise): Promise { + 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(f: () => Promise): Promise> { + const delayMS = 5000 + return Promise.race([ + retry(f).then(right), + setTimeout(delayMS, err(`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> { - // 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))) } /** From f9223ea9bad609f2c71404ed9b14d7c28766e8af Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Wed, 2 Aug 2023 09:54:59 +0200 Subject: [PATCH 5/5] Retry reflection end point --- quint/apalache-dist-tests.md | 2 +- quint/src/quintVerifier.ts | 58 +++++++++++++++++------------------- 2 files changed, 29 insertions(+), 31 deletions(-) diff --git a/quint/apalache-dist-tests.md b/quint/apalache-dist-tests.md index cc8438821..180692ca7 100644 --- a/quint/apalache-dist-tests.md +++ b/quint/apalache-dist-tests.md @@ -72,7 +72,7 @@ quint verify ../examples/language-features/booleans.qnt ``` -error: Apalache gRPC endpoint is corrupted. Error reading from streaming API: No connection established +error: Failed to obtain a connection to Apalache after 5 seconds. ``` ### Inability to connect to the server produces an errer (`APALACHE_DIST` set) diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index b6cbbebca..fa07dc617 100644 --- a/quint/src/quintVerifier.ts +++ b/quint/src/quintVerifier.ts @@ -213,6 +213,7 @@ function loadProtoDefViaDistribution(dist: ApalacheDist): VerifyResult> { + // Types of the gRPC interface. type ServerReflectionRequest = { file_containing_symbol: string } type ServerReflectionResponseSuccess = { file_descriptor_response: { @@ -235,46 +236,43 @@ async function loadProtoDefViaReflection(): Promise = await new Promise( - (resolve, reject) => { - const call = reflectionClient.ServerReflectionInfo() - call.on('data', (r: ServerReflectionResponse) => { - call.end() - resolve(r) + // Query reflection endpoint (retry if server is unreachable) + return retryWithTimeout( + () => + new Promise((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' }) }) - call.on('error', (e: grpc.StatusObject) => reject(e)) - - call.write({ file_containing_symbol: 'shai.cmdExecutor.CmdExecutor' }) - } - ) - .then(right) - .catch(e => err(`Apalache gRPC endpoint is corrupted. Error reading from streaming API: ${e.details}`)) + ).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}` + ) + } - return 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 ) - } - - // 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)) - }) + // Use proto-loader to load the FileDescriptorProto wrapped in a FileDescriptorSet + return right(proto.loadFileDescriptorSetFromObject({ file: fileDescriptorProtos }, grpcStubOptions)) + }) + ) } function loadGrpcClient(protoDef: ProtoPackageDefinition): VerifyResult {