Merge pull request #1078 from informalsystems/1054/record-arity-checks

Add arity checks for tuple and record operators

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
 

quint/src/types/constraintGenerator.ts

@@ -38,14 +38,47 @@ 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 = (
   _table: LookupTable,
   _constraint: Constraint
 ) => Either<Map<bigint, ErrorTree>, 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<Error, null> {
+  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<Error, TypeScheme> => {
-      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)
   }

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<Error, Constraint[]> {
-  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<Error, Constraint[]> {
-  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

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'
+    )
+  })
 })