Skip to content

Commit

Permalink
resolve and reject on same execution tree
Browse files Browse the repository at this point in the history
  • Loading branch information
rnbguy committed Jul 26, 2023
1 parent ef2f296 commit 219458a
Showing 1 changed file with 20 additions and 4 deletions.
24 changes: 20 additions & 4 deletions quint/src/quintVerifier.ts
Original file line number Diff line number Diff line change
Expand Up @@ -225,26 +225,42 @@ async function loadProtoDefViaReflection(): Promise<VerifyResult<ProtoPackageDef
const serverReflectionService = reflectionProtoDescriptor.grpc.reflection.v1alpha.ServerReflection
const reflectionClient = new serverReflectionService(APALACHE_SERVER_URI, grpc.credentials.createInsecure())

const protoDefResponse: ServerReflectionResponse = await new Promise((resolve, reject) => {
const protoDefResponses: ServerReflectionResponse[] = await new Promise((resolve, reject) => {
// Query reflection endpoint
const call = reflectionClient.ServerReflectionInfo()
call.write({ file_containing_symbol: 'shai.cmdExecutor.CmdExecutor' })

let responses: ServerReflectionResponse[] = []

call.on('data', (reflectionResponse: ServerReflectionResponse) => {
responses.push(reflectionResponse)
call.cancel()
resolve(reflectionResponse)
})

call.on('error', (e: any) => {
// Ignore cancellation errors
if (e.code !== grpc.status.CANCELLED) {
if (e.code === grpc.status.CANCELLED) {
// Cancelled by us, so we have the response
resolve(responses)
} else {
// Ignore cancellation errors
// An error has occurred and the stream has been closed.
console.error(e)
reject(e)
}
})
})

if (protoDefResponses.length === 0) {
return err(`Apalache gRPC endpoint is corrupted. Could not extract proto file: no response from reflection service`)
} else if (protoDefResponses.length > 1) {
return err(
`Apalache gRPC endpoint is corrupted. Could not extract proto file: multiple responses from reflection service`
)
}

// We have a single response
const protoDefResponse = protoDefResponses[0]

if ('error_response' in protoDefResponse) {
return err(
`Apalache gRPC endpoint is corrupted. Could not extract proto file: ${protoDefResponse.error_response.error_message}`
Expand Down

0 comments on commit 219458a

Please sign in to comment.