diff --git a/CHANGELOG.md b/CHANGELOG.md index 3e5ff3765..58b96bdb4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,6 +33,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 server (#1074) - Fix a problem where some definitions would have to be exported from the main module in order for the REPL and the simulator to load them (#1039 and #1051) +- Invalid arities when applying record and tuple operator no longer cause a crash (#1054) ### Security diff --git a/quint/src/types/constraintGenerator.ts b/quint/src/types/constraintGenerator.ts index 0ed55e92a..d2786e6db 100644 --- a/quint/src/types/constraintGenerator.ts +++ b/quint/src/types/constraintGenerator.ts @@ -38,7 +38,14 @@ import { getSignatures } from './builtinSignatures' import { Constraint, Signature, TypeScheme, toScheme } from './base' import { Substitutions, applySubstitution, compose } from './substitutions' import { LookupTable } from '../names/base' -import { specialConstraints } from './specialConstraints' +import { + fieldConstraints, + fieldNamesConstraints, + itemConstraints, + recordConstructorConstraints, + tupleConstructorConstraints, + withConstraints, +} from './specialConstraints' import { FreshVarGenerator } from '../FreshVarGenerator' export type SolvingFunctionType = ( @@ -46,6 +53,32 @@ export type SolvingFunctionType = ( _constraint: Constraint ) => Either, Substitutions> +// `validateArity(opName, args, pred, msg)` is `right(null)` if +// if `pred(args.length) === true`, and otherwise `left(err)`, where `err` +// is constructed using the given `opName` and `msg`. +// +// `msg` should contain a textual description of the expected argument +// length, e.g., ("1", "2", "even number of", ...). +// +// Use this for operators that cannot be typed in the Quint type system. +function validateArity( + opcode: string, + args: [QuintEx, QuintType][], + pred: (arity: number) => Boolean, + msg: String +): Either { + if (!pred(args.length)) { + return left( + buildErrorLeaf( + `Checking arity for application of ${opcode}`, + `Operator expects ${msg} arguments but was given ${args.length}` + ) + ) + } else { + return right(null) + } +} + // A visitor that collects types and constraints for a module's expressions export class ConstraintGeneratorVisitor implements IRVisitor { // Inject dependency to allow manipulation in unit tests @@ -152,31 +185,47 @@ export class ConstraintGeneratorVisitor implements IRVisitor { }) ) - const result = argsResult.chain((results): Either => { - const signature = this.typeForName(e.opcode, e.id, e.args.length) - const a: QuintType = { kind: 'var', name: this.freshVarGenerator.freshVar('t') } - const special = specialConstraints(e.opcode, e.id, results, a) - - const constraints = special.chain(cs => { - // Check if there is a special case defined for the operator - if (cs.length > 0) { - // If yes, use the special constraints - return right(cs) - } else { - // Otherwise, define a constraint over the signature - return signature.map(t1 => { - const t2: QuintType = { kind: 'oper', args: results.map(r => r[1]), res: a } - const c: Constraint = { kind: 'eq', types: [t1, t2], sourceId: e.id } - return [c] - }) + // We want `definedSignature` computed before the fresh variable `a` so that the + // numbering of ther fresh variables stays in order, with `a`, used for return types, + // bearing the highest number. + const definedSignature = this.typeForName(e.opcode, e.id, e.args.length) + const a: QuintType = { kind: 'var', name: this.freshVarGenerator.freshVar('t') } + const result = argsResult + .chain(results => { + switch (e.opcode) { + // Record operators + case 'Rec': + return validateArity(e.opcode, results, l => l % 2 === 0, 'even number of').chain(() => + recordConstructorConstraints(e.id, results, a) + ) + case 'field': + return validateArity(e.opcode, results, l => l === 2, '2').chain(() => fieldConstraints(e.id, results, a)) + case 'fieldNames': + return validateArity(e.opcode, results, l => l === 1, '1').chain(() => + fieldNamesConstraints(e.id, results, a) + ) + case 'with': + return validateArity(e.opcode, results, l => l === 3, '3').chain(() => withConstraints(e.id, results, a)) + // Tuple operators + case 'Tup': + return validateArity(e.opcode, results, l => l > 0, 'at least one').chain(() => + tupleConstructorConstraints(e.id, results, a) + ) + case 'item': + return validateArity(e.opcode, results, l => l === 2, '2').chain(() => itemConstraints(e.id, results, a)) + // Otherwise it's a standard operator with a definition in the context + default: + return definedSignature.map(t1 => { + const t2: QuintType = { kind: 'oper', args: results.map(r => r[1]), res: a } + const c: Constraint = { kind: 'eq', types: [t1, t2], sourceId: e.id } + return [c] + }) } }) - - return constraints.map(cs => { + .map(cs => { this.constraints.push(...cs) return toScheme(a) }) - }) this.addToResults(e.id, result) } diff --git a/quint/src/types/specialConstraints.ts b/quint/src/types/specialConstraints.ts index 756b41065..9699dc7b2 100644 --- a/quint/src/types/specialConstraints.ts +++ b/quint/src/types/specialConstraints.ts @@ -5,7 +5,8 @@ * --------------------------------------------------------------------------------- */ /** - * Special constraint cases for Quint types, including record and tuple related operators + * Special constraint cases for Quint operators that we are not able to type in our system, + * including record and tuple related operators * * @author Gabriela Moreira * @@ -20,48 +21,11 @@ import { QuintType, QuintVarType } from '../quintTypes' import { Constraint } from './base' import { chunk, times } from 'lodash' -/* - * Generate constraints for operators for which signatures cannot be expressed as normal signatures - * - * @param opcode The name of the operator - * @param id The id of the component for which constraints are being generated - * @param args The arguments to the operator and their respective types - * @param resultTypeVar A fresh type variable for the result type - * - * @returns Either an error or a list of constraints - */ -export function specialConstraints( - opcode: string, - id: bigint, - args: [QuintEx, QuintType][], - resultTypeVar: QuintVarType -): Either { - switch (opcode) { - // Record operators - case 'Rec': - return recordConstructorConstraints(id, args, resultTypeVar) - case 'field': - return fieldConstraints(id, args, resultTypeVar) - case 'fieldNames': - return fieldNamesConstraints(id, args, resultTypeVar) - case 'with': - return withConstraints(id, args, resultTypeVar) - // Tuple operators - case 'Tup': - return tupleConstructorConstraints(id, args, resultTypeVar) - case 'item': - return itemConstraints(id, args, resultTypeVar) - default: - return right([]) - } -} - -function recordConstructorConstraints( +export function recordConstructorConstraints( id: bigint, args: [QuintEx, QuintType][], resultTypeVar: QuintVarType ): Either { - const constraints: Constraint[] = [] // A record constructor has the normal form Rec('field1', value1, 'field2', value2, ...) // So we iterate over the arguments in pairs (chunks of size 2) // @@ -82,13 +46,12 @@ function recordConstructorConstraints( return mergeInMany(fields).map(fs => { const t: QuintType = { kind: 'rec', fields: { kind: 'row', fields: fs, other: { kind: 'empty' } } } - const c: Constraint = { kind: 'eq', types: [t, resultTypeVar], sourceId: id } - constraints.push(c) - return constraints + const constraint: Constraint = { kind: 'eq', types: [t, resultTypeVar], sourceId: id } + return [constraint] }) } -function fieldConstraints( +export function fieldConstraints( id: bigint, args: [QuintEx, QuintType][], resultTypeVar: QuintVarType @@ -119,7 +82,7 @@ function fieldConstraints( return right([constraint]) } -function fieldNamesConstraints( +export function fieldNamesConstraints( id: bigint, args: [QuintEx, QuintType][], resultTypeVar: QuintVarType @@ -134,7 +97,7 @@ function fieldNamesConstraints( return right([c1, c2]) } -function withConstraints( +export function withConstraints( id: bigint, args: [QuintEx, QuintType][], resultTypeVar: QuintVarType @@ -166,7 +129,7 @@ function withConstraints( return right([c1, c2]) } -function tupleConstructorConstraints( +export function tupleConstructorConstraints( id: bigint, args: [QuintEx, QuintType][], resultTypeVar: QuintVarType @@ -180,7 +143,7 @@ function tupleConstructorConstraints( return right([c]) } -function itemConstraints( +export function itemConstraints( id: bigint, args: [QuintEx, QuintType][], resultTypeVar: QuintVarType diff --git a/quint/test/types/constraintGenerator.test.ts b/quint/test/types/constraintGenerator.test.ts index 4528370a6..62be3c0ce 100644 --- a/quint/test/types/constraintGenerator.test.ts +++ b/quint/test/types/constraintGenerator.test.ts @@ -115,4 +115,66 @@ describe('ConstraintGeneratorVisitor', () => { assert.sameDeepMembers(Array.from(errors.values()), [error]) }) + + function testArityError(def: string, location: string, message: string) { + const defs = [def] + + const solvingFunction: SolvingFunctionType = (_: LookupTable, _c: Constraint) => right([]) + + const visitor = visitModuleWithDefs(defs, solvingFunction) + const [errors, _types] = visitor.getResult() + + const [error] = Array.from(errors.values())[0].children + + assert.equal(error.location, location, 'unexpected error location') + assert.equal(error.message, message, 'unexpected error message') + } + + it('catches invalid arity on Rec operator', () => { + testArityError( + 'val x = Rec("a")', + 'Checking arity for application of Rec', + 'Operator expects even number of arguments but was given 1' + ) + }) + + it('catches invalid arity on field operator', () => { + testArityError( + 'val x = Rec("a", 1).field()', + 'Checking arity for application of field', + 'Operator expects 2 arguments but was given 1' + ) + }) + + it('catches invalid arity on fieldNames operator', () => { + testArityError( + 'val x = Rec("a", 1).fieldNames(1)', + 'Checking arity for application of fieldNames', + 'Operator expects 1 arguments but was given 2' + ) + }) + + it('catches invalid arity on with operator', () => { + testArityError( + 'val x = Rec("a", 1).with("a", 1, 2)', + 'Checking arity for application of with', + 'Operator expects 3 arguments but was given 4' + ) + }) + + it('catches invalid arity on Tup operator', () => { + testArityError( + 'val x = Tup()', + 'Checking arity for application of Tup', + 'Operator expects at least one arguments but was given 0' + ) + }) + + it('catches invalid arity on item operator', () => { + testArityError( + 'val x = (0, 1).item()', + 'Checking arity for application of item', + 'Operator expects 2 arguments but was given 1' + ) + }) })