Skip to content

Commit

Permalink
feat: error if divisor is zero (#644)
Browse files Browse the repository at this point in the history
Closes partially #543

### Summary of Changes

Show an error if we know that the divisor of a division is zero. Once
the partial evaluator gets fully implemented, this will work in more
cases.

---------

Co-authored-by: megalinter-bot <[email protected]>
  • Loading branch information
lars-reimann and megalinter-bot authored Oct 17, 2023
1 parent 8b076e7 commit 9af3b81
Show file tree
Hide file tree
Showing 5 changed files with 149 additions and 58 deletions.
54 changes: 30 additions & 24 deletions src/language/partialEvaluation/toConstantExpressionOrUndefined.ts
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ import {
SdsConstantBoolean,
SdsConstantExpression,
SdsConstantFloat,
SdsConstantInt,
SdsConstantNull,
SdsConstantString,
SdsIntermediateBlockLambda,
Expand Down Expand Up @@ -51,10 +52,10 @@ export const toConstantExpressionOrUndefined = (node: AstNode | undefined): SdsC
return undefined;
}

return toConstantExpressionOrNullImpl(node, new Map());
return toConstantExpressionOrUndefinedImpl(node, new Map());
};

const toConstantExpressionOrNullImpl = (
const toConstantExpressionOrUndefinedImpl = (
node: AstNode,
substitutions: ParameterSubstitutions,
): SdsConstantExpression | undefined => {
Expand Down Expand Up @@ -155,13 +156,16 @@ const simplifyExpressionLambda = (
};

const simplifyInfixOperation = (
_node: SdsInfixOperation,
_substitutions: ParameterSubstitutions,
node: SdsInfixOperation,
substitutions: ParameterSubstitutions,
): SdsConstantExpression | undefined => {
// // By design none of the operators are short-circuited
// val constantLeft = leftOperand.toConstantExpressionOrUndefined(substitutions) ?: return undefined
// val constantRight = rightOperand.toConstantExpressionOrUndefined(substitutions) ?: return undefined
//
// By design none of the operators are short-circuited
const constantLeft = toConstantExpressionOrUndefinedImpl(node.leftOperand, substitutions);
if (!constantLeft) return;

const constantRight = toConstantExpressionOrUndefinedImpl(node.rightOperand, substitutions);
if (!constantRight) return;

// return when (operator()) {
// Or -> simplifyLogicalOp(constantLeft, Boolean::or, constantRight)
// And -> simplifyLogicalOp(constantLeft, Boolean::and, constantRight)
Expand Down Expand Up @@ -282,30 +286,32 @@ const simplifyInfixOperation = (
// }

const simplifyPrefixOperation = (
_node: SdsPrefixOperation,
_substitutions: ParameterSubstitutions,
node: SdsPrefixOperation,
substitutions: ParameterSubstitutions,
): SdsConstantExpression | undefined => {
// val constantOperand = operand.toConstantExpressionOrUndefined(substitutions) ?: return undefined
//
// return when (operator()) {
// Not -> when (constantOperand) {
// is SdsConstantBoolean -> SdsConstantBoolean(!constantOperand.value)
// else -> undefined
// }
// PrefixMinus -> when (constantOperand) {
// is SdsConstantFloat -> SdsConstantFloat(-constantOperand.value)
// is SdsConstantInt -> SdsConstantInt(-constantOperand.value)
// else -> undefined
// }
// }
const constantOperand = toConstantExpressionOrUndefinedImpl(node.operand, substitutions);
if (!constantOperand) return;

if (node.operator === 'not') {
if (constantOperand instanceof SdsConstantBoolean) {
return new SdsConstantBoolean(!constantOperand.value);
}
} else if (node.operator === '-') {
if (constantOperand instanceof SdsConstantFloat) {
return new SdsConstantFloat(-constantOperand.value);
} else if (constantOperand instanceof SdsConstantInt) {
return new SdsConstantInt(-constantOperand.value);
}
}

return undefined;
};

const simplifyTemplateString = (
node: SdsTemplateString,
substitutions: ParameterSubstitutions,
): SdsConstantExpression | undefined => {
const constantExpressions = node.expressions.map((it) => toConstantExpressionOrNullImpl(it, substitutions));
const constantExpressions = node.expressions.map((it) => toConstantExpressionOrUndefinedImpl(it, substitutions));
if (constantExpressions.some((it) => it === undefined)) {
return undefined;
}
Expand Down
73 changes: 39 additions & 34 deletions src/language/typing/safe-ds-type-computer.ts
Original file line number Diff line number Diff line change
Expand Up @@ -91,14 +91,16 @@ export class SafeDsTypeComputer {
private readonly builtinClasses: SafeDsClasses;
private readonly nodeMapper: SafeDsNodeMapper;

private readonly typeCache: WorkspaceCache<string, Type>;
private readonly coreTypeCache: WorkspaceCache<string, Type>;
private readonly nodeTypeCache: WorkspaceCache<string, Type>;

constructor(services: SafeDsServices) {
this.astNodeLocator = services.workspace.AstNodeLocator;
this.builtinClasses = services.builtins.Classes;
this.nodeMapper = services.helpers.NodeMapper;

this.typeCache = new WorkspaceCache(services.shared);
this.coreTypeCache = new WorkspaceCache(services.shared);
this.nodeTypeCache = new WorkspaceCache(services.shared);
}

/**
Expand All @@ -112,7 +114,7 @@ export class SafeDsTypeComputer {
const documentUri = getDocument(node).uri.toString();
const nodePath = this.astNodeLocator.getAstNodePath(node);
const key = `${documentUri}~${nodePath}`;
return this.typeCache.get(key, () => this.doComputeType(node).unwrap());
return this.nodeTypeCache.get(key, () => this.doComputeType(node).unwrap());
}

// fun SdsAbstractObject.hasPrimitiveType(): Boolean {
Expand Down Expand Up @@ -257,21 +259,21 @@ export class SafeDsTypeComputer {
private computeTypeOfExpression(node: SdsExpression): Type {
// Terminal cases
if (isSdsBoolean(node)) {
return this.Boolean();
return this.Boolean;
} else if (isSdsFloat(node)) {
return this.Float();
return this.Float;
} else if (isSdsInt(node)) {
return this.Int();
return this.Int;
} else if (isSdsList(node)) {
return this.List();
return this.List;
} else if (isSdsMap(node)) {
return this.Map();
return this.Map;
} else if (isSdsNull(node)) {
return this.NothingOrNull();
return this.NothingOrNull;
} else if (isSdsString(node)) {
return this.String();
return this.String;
} else if (isSdsTemplateString(node)) {
return this.String();
return this.String;
}

// Recursive cases
Expand Down Expand Up @@ -304,21 +306,21 @@ export class SafeDsTypeComputer {
// Boolean operators
case 'or':
case 'and':
return this.Boolean();
return this.Boolean;

// Equality operators
case '==':
case '!=':
case '===':
case '!==':
return this.Boolean();
return this.Boolean;

// Comparison operators
case '<':
case '<=':
case '>=':
case '>':
return this.Boolean();
return this.Boolean;

// Arithmetic operators
case '+':
Expand All @@ -343,7 +345,7 @@ export class SafeDsTypeComputer {
} else if (isSdsPrefixOperation(node)) {
switch (node.operator) {
case 'not':
return this.Boolean();
return this.Boolean;
case '-':
return this.computeTypeOfArithmeticPrefixOperation(node);

Expand Down Expand Up @@ -378,7 +380,7 @@ export class SafeDsTypeComputer {

private computeTypeOfIndexedAccess(node: SdsIndexedAccess): Type {
const receiverType = this.computeType(node.receiver);
if (receiverType.equals(this.List()) || receiverType.equals(this.Map())) {
if (receiverType.equals(this.List) || receiverType.equals(this.Map)) {
return this.AnyOrNull();
} else {
return UnknownType;
Expand All @@ -389,10 +391,10 @@ export class SafeDsTypeComputer {
const leftOperandType = this.computeType(node.leftOperand);
const rightOperandType = this.computeType(node.rightOperand);

if (leftOperandType.equals(this.Int()) && rightOperandType.equals(this.Int())) {
return this.Int();
if (leftOperandType.equals(this.Int) && rightOperandType.equals(this.Int)) {
return this.Int;
} else {
return this.Float();
return this.Float;
}
}

Expand Down Expand Up @@ -426,10 +428,10 @@ export class SafeDsTypeComputer {
private computeTypeOfArithmeticPrefixOperation(node: SdsPrefixOperation): Type {
const leftOperandType = this.computeType(node.operand);

if (leftOperandType.equals(this.Int())) {
return this.Int();
if (leftOperandType.equals(this.Int)) {
return this.Int;
} else {
return this.Float();
return this.Float;
}
}

Expand Down Expand Up @@ -529,43 +531,46 @@ export class SafeDsTypeComputer {
// Builtin types
// -----------------------------------------------------------------------------------------------------------------

private AnyOrNull(): Type {
AnyOrNull(): Type {
return this.createCoreType(this.builtinClasses.Any, true);
}

private Boolean(): Type {
get Boolean(): Type {
return this.createCoreType(this.builtinClasses.Boolean);
}

private Float(): Type {
get Float(): Type {
return this.createCoreType(this.builtinClasses.Float);
}

private Int(): Type {
get Int(): Type {
return this.createCoreType(this.builtinClasses.Int);
}

private List(): Type {
get List(): Type {
return this.createCoreType(this.builtinClasses.List);
}

private Map(): Type {
get Map(): Type {
return this.createCoreType(this.builtinClasses.Map);
}

private NothingOrNull(): Type {
get NothingOrNull(): Type {
return this.createCoreType(this.builtinClasses.Nothing, true);
}

private String(): Type {
get String(): Type {
return this.createCoreType(this.builtinClasses.String);
}

private createCoreType(coreClass: SdsClass | undefined, isNullable: boolean = false): Type {
if (coreClass) {
return new ClassType(coreClass, isNullable);
} /* c8 ignore start */ else {
/* c8 ignore start */
if (!coreClass) {
return UnknownType;
} /* c8 ignore stop */
}
/* c8 ignore stop */

const key = `${coreClass.name}~${isNullable}`;
return this.coreTypeCache.get(key, () => new ClassType(coreClass, isNullable));
}
}
40 changes: 40 additions & 0 deletions src/language/validation/other/expressions/infixOperations.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
import { SdsInfixOperation } from '../../../generated/ast.js';
import { ValidationAcceptor } from 'langium';
import { SafeDsServices } from '../../../safe-ds-module.js';
import { toConstantExpressionOrUndefined } from '../../../partialEvaluation/toConstantExpressionOrUndefined.js';
import { SdsConstantFloat, SdsConstantInt } from '../../../partialEvaluation/model.js';
import { UnknownType } from '../../../typing/model.js';

export const CODE_INFIX_OPERATION_DIVISION_BY_ZERO = 'infix-operation/division-by-zero';

export const divisionDivisorMustNotBeZero = (services: SafeDsServices) => {
const typeComputer = services.types.TypeComputer;
const zeroInt = new SdsConstantInt(BigInt(0));
const zeroFloat = new SdsConstantFloat(0.0);
const minusZeroFloat = new SdsConstantFloat(-0.0);

return (node: SdsInfixOperation, accept: ValidationAcceptor): void => {
if (node.operator !== '/') {
return;
}

const dividendType = typeComputer.computeType(node.leftOperand);
if (
dividendType === UnknownType ||
(!dividendType.equals(typeComputer.Int) && !dividendType.equals(typeComputer.Float))
) {
return;
}

const divisorValue = toConstantExpressionOrUndefined(node.rightOperand);
if (
divisorValue &&
(divisorValue.equals(zeroInt) || divisorValue.equals(zeroFloat) || divisorValue.equals(minusZeroFloat))
) {
accept('error', 'Division by zero.', {
node,
code: CODE_INFIX_OPERATION_DIVISION_BY_ZERO,
});
}
};
};
2 changes: 2 additions & 0 deletions src/language/validation/safe-ds-validator.ts
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,7 @@ import {
import { classMustNotInheritItself, classMustOnlyInheritASingleClass } from './inheritance.js';
import { pythonNameShouldDifferFromSafeDsName } from './builtins/pythonName.js';
import { pythonModuleShouldDifferFromSafeDsPackage } from './builtins/pythonModule.js';
import { divisionDivisorMustNotBeZero } from './other/expressions/infixOperations.js';

/**
* Register custom validation checks.
Expand Down Expand Up @@ -166,6 +167,7 @@ export const registerValidationChecks = function (services: SafeDsServices) {
SdsImport: [importPackageMustExist(services), importPackageShouldNotBeEmpty(services)],
SdsImportedDeclaration: [importedDeclarationAliasShouldDifferFromDeclarationName],
SdsIndexedAccess: [indexedAccessesShouldBeUsedWithCaution],
SdsInfixOperation: [divisionDivisorMustNotBeZero(services)],
SdsLambda: [lambdaParametersMustNotBeAnnotated, lambdaParameterMustNotHaveConstModifier],
SdsMemberAccess: [
memberAccessMustBeNullSafeIfReceiverIsNullable(services),
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
package tests.validation.other.expressions.infixOperations.divisionByZero

pipeline test {
// $TEST$ error "Division by zero."
»1.0 / 0.0«;
// $TEST$ error "Division by zero."
»1.0 / -0.0«;
// $TEST$ no error "Division by zero."
»1.0 / 1.0«;

// $TEST$ error "Division by zero."
»1.0 / 0«;
// $TEST$ no error "Division by zero."
»1.0 / 1«;

// $TEST$ error "Division by zero."
»1 / 0.0«;
// $TEST$ error "Division by zero."
»1 / -0.0«;
// $TEST$ no error "Division by zero."
»1 / 1.0«;

// $TEST$ error "Division by zero."
»1 / 0«;
// $TEST$ no error "Division by zero."
»1 / 1«;

// $TEST$ no error "Division by zero."
»null / 0.0«;
// $TEST$ no error "Division by zero."
»null / -0.0«;
// $TEST$ no error "Division by zero."
»null / 1.0«;
// $TEST$ no error "Division by zero."
»null / 0«;
// $TEST$ no error "Division by zero."
»null / 1«;
}

0 comments on commit 9af3b81

Please sign in to comment.