diff --git a/src/abstract-interpretation/absint-condition-semantics.ts b/src/abstract-interpretation/absint-condition-semantics.ts index f6f4fb81912..681ab44c284 100644 --- a/src/abstract-interpretation/absint-condition-semantics.ts +++ b/src/abstract-interpretation/absint-condition-semantics.ts @@ -108,6 +108,8 @@ export function createConditionApplier[]; function orConditionSemantics(leftNodeId: NodeId, rightNodeId: NodeId, state: StateDomain, visitor: Visitor, dfg: DataflowGraph): StateDomain { diff --git a/src/abstract-interpretation/absint-visitor.ts b/src/abstract-interpretation/absint-visitor.ts index a8e37526000..e6357098da0 100644 --- a/src/abstract-interpretation/absint-visitor.ts +++ b/src/abstract-interpretation/absint-visitor.ts @@ -287,8 +287,10 @@ export abstract class AbstractInterpretationVisitor '); + process.exit(1); +} + +const [_, __, filePath, outputDirectory] = process.argv; + +interface FileMetadata { + fileName: string; + intervalResultFileName: string; + pentagonResultFileName: string; + loc: number; + cloc: number; + numOfDfgNodes: number; + numOfCfgNodes: number; + numOfConstants: number; + numOfRNumberConstants: number; + RNumberConstantNodeIds: NodeId[]; + numOfFunctionDefinitions: number; + numOfFunctionCalls: number; + numOfSupportedExpressionFunctionCalls: number; + SupportedExpressionFunctionCallNodeIds: NodeId[]; + numOfSupportedConditionFunctionCalls: number; + SupportedConditionFunctionCalls: NodeId[]; + numOfConditions: number; + numOfIfThenElse: number; + numOfWhile: number; + numOfStopIfNot: number; + numOfFnWithUnknownSideEffect: number; + linterDeadCodeIds: NodeId[]; + metadataGatheringInMs: number; + baselineInMs: number; + astInMs: number; + dfgInMs: number; + cfgInMs: number; + intervalAnalysisInMs: number; + intervalResultGatheringInMs: number; + pentagonAnalysisInMs: number; + pentagonResultGatheringInMs: number; +} + +interface InferredValue { + nodeId: NodeId; + inferredValue: string; + significantFigures: string; + sourceLocation: string; + lexeme: string; + dfgTag: VertexType | 'unknown'; +} + +void async function() { + fs.mkdirSync(outputDirectory, { recursive: true }); + const fileName = path.basename(filePath); + const fileNameWithoutEnding = path.parse(fileName).name; + const metadataOutputFile = fileNameWithoutEnding + '.json'; + const intervalResultFile = fileNameWithoutEnding + '-interval.json'; + const pentagonResultFile = fileNameWithoutEnding + '-pentagon.json'; + + const baselineStart = performance.now(); + const analyzer = await new FlowrAnalyzerBuilder() + .setEngine('tree-sitter') + .build(); + analyzer.addRequest(fileProtocol + filePath); + const astStart = performance.now(); + const ast = await analyzer.normalize(); + const dfgStart = performance.now(); + const dfg = (await analyzer.dataflow()).graph; + const cfgStart = performance.now(); + const cfg = await analyzer.controlflow(); + const cfgEnd = performance.now(); + const ctx = analyzer.context(); + const baselineEnd = performance.now(); + + const visitorContext: AbsintVisitorConfiguration = { normalizedAst: ast, dfg, controlFlow: cfg, ctx }; + + // Run Interval Analysis + const intervalVisitor = new NumericIntervalInferenceVisitor(visitorContext); + + const intervalStart = performance.now(); + intervalVisitor.start(); + const intervalEnd = performance.now(); + + const intervalResultStart = performance.now(); + const intervalResults: InferredValue[] = []; + for(const nodeId of intervalVisitor.getAbstractTrace().keys()) { + const value = intervalVisitor.getAbstractValue(nodeId); + if(value !== undefined) { + const node = ast.idMap.get(nodeId); + + intervalResults.push({ + nodeId: nodeId, + inferredValue: value.toString() ?? 'undefined', + significantFigures: value.significantFigures?.toString() ?? 'unknown', + sourceLocation: SourceRange.fromNode(node)?.toString() ?? 'unknown', + lexeme: node?.lexeme ?? 'unknown', + dfgTag: dfg.getVertex(nodeId)?.tag ?? 'unknown', + }); + } + } + const intervalResultEnd = performance.now(); + + // Dump Interval Results + const intervalPath = path.join(outputDirectory, intervalResultFile); + fs.rmSync(intervalPath, { recursive: true, force: true }); + superBigJsonStringify(intervalResults, '\n', (msg) => fs.appendFileSync(intervalPath, msg)); + + // Run Pentagon Analysis + const pentagonVisitor = new NumericPentagonInferenceVisitor(visitorContext); + + const pentagonStart = performance.now(); + pentagonVisitor.start(); + const pentagonEnd = performance.now(); + + const pentagonResultStart = performance.now(); + const pentagonResults: InferredValue[] = []; + for(const nodeId of pentagonVisitor.getAbstractTrace().keys()) { + const value = pentagonVisitor.getAbstractValue(nodeId); + if(value !== undefined) { + const node = ast.idMap.get(nodeId); + + pentagonResults.push({ + nodeId: nodeId, + inferredValue: value.toString() ?? 'undefined', + significantFigures: value.value.interval.significantFigures?.toString() ?? 'unknown', + sourceLocation: SourceRange.fromNode(node)?.toString() ?? 'unknown', + lexeme: node?.lexeme ?? 'unknown', + dfgTag: dfg.getVertex(nodeId)?.tag ?? 'unknown', + }); + } + } + const pentagonResultEnd = performance.now(); + + // Dump Pentagon Results + const pentagonPath = path.join(outputDirectory, pentagonResultFile); + fs.rmSync(pentagonPath, { recursive: true, force: true }); + superBigJsonStringify(pentagonResults, '\n', (msg) => fs.appendFileSync(pentagonPath, msg)); + + // Create File and Runtime Metadata + const metadataStart = performance.now(); + const constants = dfg.verticesOfType(VertexType.Value).toArray(); + const numberConstants = constants.filter(value => ast.idMap.get(value[0])?.type === RType.Number); + + const functionCalls = dfg.verticesOfType(VertexType.FunctionCall).toArray(); + const supportedExpressionFunctionCalls = functionCalls.filter(([_, dfgCall]) => + IntervalExpressionSemanticsMapper().find(([id]) => Identifier.matches(id, dfgCall.name)) !== undefined || + PentagonExpressionSemanticsMapper.find(([id]) => Identifier.matches(id, dfgCall.name)) !== undefined + ); + const supportedConditionFunctionCalls = functionCalls.filter(([_, dfgCall]) => + IntervalSemanticsMaper().find(([id]) => Identifier.matches(id, dfgCall.name)) !== undefined || + UpperBoundsSemanticsMapper().find(([id]) => Identifier.matches(id, dfgCall.name)) !== undefined || + ['&&', '!', '||', '&', '|'].some(id => Identifier.matches(id, dfgCall.name)) + ); + const conditions = functionCalls.filter(([_, dfgCall]) => + dfgCall.origin.includes(BuiltInProcName.IfThenElse) || dfgCall.origin.includes(BuiltInProcName.WhileLoop) || dfgCall.origin.includes(BuiltInProcName.StopIfNot) + ); + const functionsWithUnknownSideEffects = functionCalls.filter(([_, dfgCall]) => UnsupportedFunctions.isUnsupportedCall(dfgCall)); + + const deadCodeQueryResult = await analyzer.query([{ + type: 'linter', + rules: ['dead-code'] + }]); + const deadCodeResult = deadCodeQueryResult.linter.results['dead-code'] as LintingResultsSuccess<'dead-code'>; + const linterDeadNodes = deadCodeResult.results.reduce((acc: NodeId[], val) => acc.concat(val.involvedId ?? []), []); + + + const metadataEnd = performance.now(); + + const fileMetadata: FileMetadata = { + fileName: fileName, + intervalResultFileName: intervalResultFile, + pentagonResultFileName: pentagonResultFile, + loc: analyzer.inspectContext().files.getAllFiles()[0].content().toString().split('\n').length, + cloc: analyzer.inspectContext().files.getAllFiles()[0].content().toString().split('\n').filter(line => line.trim() !== '' && !line.trimStart().startsWith('#')).length, + numOfDfgNodes: dfg.vertices(true).toArray().length, + numOfCfgNodes: cfg.graph.vertices(false).size, + numOfConstants: constants.length, + numOfRNumberConstants: numberConstants.length, + RNumberConstantNodeIds: numberConstants.map(([node]) => node), + numOfFunctionDefinitions: dfg.verticesOfType(VertexType.FunctionDefinition).toArray().length, + numOfFunctionCalls: functionCalls.length, + numOfSupportedExpressionFunctionCalls: supportedExpressionFunctionCalls.length, + SupportedExpressionFunctionCallNodeIds: supportedExpressionFunctionCalls.map(([node]) => node), + numOfSupportedConditionFunctionCalls: supportedConditionFunctionCalls.length, + SupportedConditionFunctionCalls: supportedConditionFunctionCalls.map(([node]) => node), + numOfConditions: conditions.length, + numOfIfThenElse: functionCalls.filter(([_, dfgCall]) => dfgCall.origin.includes(BuiltInProcName.IfThenElse)).length, + numOfWhile: functionCalls.filter(([_, dfgCall]) => dfgCall.origin.includes(BuiltInProcName.WhileLoop)).length, + numOfStopIfNot: functionCalls.filter(([_, dfgCall]) => dfgCall.origin.includes(BuiltInProcName.StopIfNot)).length, + numOfFnWithUnknownSideEffect: functionsWithUnknownSideEffects.length, + linterDeadCodeIds: linterDeadNodes, + metadataGatheringInMs: metadataEnd - metadataStart, + baselineInMs: baselineEnd - baselineStart, + astInMs: dfgStart - astStart, + dfgInMs: cfgStart - dfgStart, + cfgInMs: cfgEnd - cfgStart, + intervalAnalysisInMs: intervalEnd - intervalStart, + intervalResultGatheringInMs: intervalResultEnd - intervalResultStart, + pentagonAnalysisInMs: pentagonEnd - pentagonStart, + pentagonResultGatheringInMs: pentagonResultEnd - pentagonResultStart + }; + + // Dump File and Runtime Metadata + const fileMetadataPath = path.join(outputDirectory, metadataOutputFile); + fs.rmSync(fileMetadataPath, { recursive: true, force: true }); + fs.writeFileSync(fileMetadataPath, JSON.stringify(fileMetadata, null, 2)); +}(); \ No newline at end of file diff --git a/src/abstract-interpretation/interval/eval.ts b/src/abstract-interpretation/interval/eval.ts index b28d2873c2a..2a9474a17ec 100644 --- a/src/abstract-interpretation/interval/eval.ts +++ b/src/abstract-interpretation/interval/eval.ts @@ -102,7 +102,7 @@ async function instrument(folder: string, workingDir: string, outputFolder: stri `tolower(as.character(is.numeric(${lhs}))), ` + `tolower(as.character(is.vector(${lhs}))), ` + `paste0(length(${lhs})), ` + - ((isNotUndefined(inferredValue) || isNotUndefined(inferredPentagonValue)) ? `paste0('"', ifelse(length(${lhs}) == 1, paste0(${lhs}), ""), ` : `paste0('"', ifelse(is.numeric(${lhs}) && length(${lhs}) == 1 , paste0(${lhs}), ""), '"'), `) + + ((isNotUndefined(inferredValue) || isNotUndefined(inferredPentagonValue)) ? `paste0('"', ifelse(length(${lhs}) == 1, paste0(${lhs}), ""), '"'), ` : `paste0('"', ifelse(is.numeric(${lhs}) && length(${lhs}) == 1 , paste0(${lhs}), ""), '"'), `) + `'"${inferredValue?.toString() ?? 'undefined'}"', ` + `'"${inferredPentagonValue?.toString() ?? 'undefined'}"',` + '"\\n", ' + diff --git a/src/abstract-interpretation/interval/expression-semantics.ts b/src/abstract-interpretation/interval/expression-semantics.ts index 2ed043189b5..b7054e12111 100644 --- a/src/abstract-interpretation/interval/expression-semantics.ts +++ b/src/abstract-interpretation/interval/expression-semantics.ts @@ -194,6 +194,10 @@ function unaryExprFnSemantics, significantFigures: number | undefined, info: ResolveInfo): IntervalDomain | undefined => { if(args.length !== 1) { numericInferenceLogger.warn('Called unary function with more/less than 1 argument, which is not supported.'); + if(args.length > 1) { + numericInferenceLogger.warn('Currently, calling unary methods in apply or tapply provides two arguments to the unary function (dfg has two reads edges) although only one is used, therefore overapproximate to top (undefined) to not underapproximate in these cases.'); + return undefined; + } return IntervalDomain.bottom(significantFigures); } @@ -509,11 +513,16 @@ function intervalAbs(arg: IntervalDomain | undefined): IntervalDomain | undefine } const [a, b] = arg.value; - const minMax = getMinMax([Math.abs(a), Math.abs(b)]); - if(isNotUndefined(minMax)) { - return arg.create([minMax.min, minMax.max]); + if(a >= 0) { + return arg.create(arg.value); + } else if(b <= 0) { + return arg.create([-b, -a]); } - return arg.top(); + // interval is positive and negative, so get the bigger of both absolute values as upper and 0 as lower bound + if(b > -a) { + return arg.create([0, b]); + } + return arg.create([0, -a]); } function intervalModulo(left: IntervalDomain | undefined, right: IntervalDomain | undefined): IntervalDomain | undefined { @@ -532,19 +541,20 @@ function intervalModulo(left: IntervalDomain | undefined, right: IntervalDomain return undefined; } if(a === b && c == d) { - return left.scalar(a % c, significantFigures); + let rResult = a % c; + // right decides the sign + if(c > 0 && rResult < 0 || c < 0 && rResult > 0) { + rResult += c; + } + return left.scalar(rResult, significantFigures); } // right decides the sign - // result is at most max of right value - const maxLeft = getMax([Math.abs(a), Math.abs(b)]) ?? 0; - const maxRight = getMax([Math.abs(c), Math.abs(d)]) ?? 0; - const maxModulo = maxLeft < maxRight ? maxLeft : maxRight; if(c > 0) { // result is positive - return left.create([0, maxModulo], significantFigures); + return left.create([0, d], significantFigures); } // result is negative - return left.create([-maxModulo, 0], significantFigures); + return left.create([c, 0], significantFigures); } function intervalLog>(args: readonly FunctionArgument[], visitor: IntervalExpressionSemanticsVisitor, significantFigures: number | undefined): IntervalDomain | undefined { @@ -767,7 +777,7 @@ function intervalRunif>(ar let [lmin, rmin] = [0, 0]; let [lmax, rmax] = [0, 0]; - // min and max default to 0 if not specified + // min and max default to 0 and 1 if not specified if(min !== 'unknown') { if(min?.value === Bottom) { return IntervalDomain.bottom(); diff --git a/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts b/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts index f61ea4b9661..30267054e41 100644 --- a/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts +++ b/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts @@ -1,6 +1,12 @@ import { IntervalDomain } from '../domains/interval-domain'; import type { NodeId } from '../../r-bridge/lang-4.x/ast/model/processing/node-id'; -import type { ConcreteState, StateDomainBottom, StateDomainLift, StateDomainTop } from '../domains/state-abstract-domain'; +import type { + ConcreteState, + StateDomainBottom, + StateDomainLift, + StateDomainTop, + StateDomainValue +} from '../domains/state-abstract-domain'; import { StateAbstractDomain } from '../domains/state-abstract-domain'; import { UpperBoundsValueDomain } from './upper-bounds/upper-bounds-value-domain'; import { Bottom, Top } from '../domains/lattice'; @@ -51,8 +57,122 @@ export class ClosedPentagonDomain extends StateAbstractDomain other.value.size) { + return false; + } + for(const [key, value] of this.value.entries()) { + const otherValue = other.get(key); + + // If right is not defined, then we have not visited that element on the right side yet, so its not leq + if(isUndefined(otherValue)) { + return false; + } + + // Leq is the case when for every element on the left holds that + // Interval of value leq interval of otherValue + // And upperbounds of left leq upper bounds of right (which equals right is subset of left) + + // If interval leq does not hold, then leq over all does not hold + if(!(value.value.interval.leq(otherValue.value.interval))) { + return false; + } + + // Early exit if the upper bounds of left and right side are equal, then leq is fine + if(value.value.upperBounds === otherValue.value.upperBounds) { + continue; + } + + // Since both are not equal, if right side is Bottom, then leq is also not satisfiable + if(otherValue.value.upperBounds.value === Bottom) { + return false; + } + + // At this point, left side could be bottom, right side has to be upper bounds + // Problem is, that the left side might have implicit upper bounds through intervals that are not explicit + // So for each upper bound on the right side, we must check if it is explicitly or implicitly present on the left + // If one is neither explicitly nor implicitly present, leq is not satisfiable and we return false + for(const rightUpperBound of otherValue.value.upperBounds.value.values()) { + // Is explicitly present on left side? => continue with next upper bound + if(value.value.upperBounds.has(rightUpperBound)) { + continue; + } + // Is implicitly present on left side? + const intervalA = value.value.interval; + const intervalB = this.value.get(rightUpperBound)?.value.interval; + + // If the right interval does not exist, or any of both are bottom, then the upper bound cannot be implicitly present + if(intervalB === undefined || intervalA.value === Bottom || intervalB.value === Bottom) { + return false; + } + + // It is implicitly present if intervalA <= intervalB and therefore the upper limit of A <= lower limit of B + if(intervalA.value[1] <= intervalB.value[0]) { + continue; + } + // The interval is not implicitly present, so leq is not satisfiable. + return false; + } + } + return true; + } + public override join(other: this): this { - return this.create(super.join(other).value); + if(this.value === Bottom){ + return this.create(other.value); + } else if(other.value === Bottom) { + return this.create(this.value); + } + const result = this.create(this.value) as this & StateAbstractDomain>; + + for(const [key, value] of other.value.entries()) { + const currValue = result.get(key); + + if(currValue === undefined) { + result.set(key, value); + } else { + const leftInterval = currValue.value.interval; + const rightInterval = value.value.interval; + const joinedInterval = leftInterval.join(rightInterval); + + const leftUpperBounds = currValue.value.upperBounds; + const rightUpperBounds = value.value.upperBounds; + // For the upper bounds part, we: + // 1. Join both upper bounds + const joinedUpperBounds = leftUpperBounds.join(rightUpperBounds); + // 2. Add all upper bounds of the left, that are implicitly present on the right + if(leftUpperBounds.isValue() && rightInterval.isValue()) { + for(const leftUpperBound of leftUpperBounds.value) { + const intervalA = rightInterval; + const intervalB = other.value.get(leftUpperBound)?.value.interval; + if(intervalB !== undefined && intervalB.isValue() && intervalA.value[1] <= intervalB.value[0]) { + // The upper bound is implicitly present on both sides + joinedUpperBounds.add(leftUpperBound); + } + } + } + // 3. Add all upper bounds of the right, that are implicitly present on the left + if(rightUpperBounds.isValue() && leftInterval.isValue()) { + for(const rightUpperBound of rightUpperBounds.value) { + const intervalA = leftInterval; + const intervalB = result.get(rightUpperBound)?.value.interval; + if(intervalB !== undefined && intervalB.isValue() && intervalA.value[1] <= intervalB.value[0]) { + // The upper bound is implicitly present on both sides + joinedUpperBounds.add(rightUpperBound); + } + } + } + + result.set(key, currValue.create({ interval: joinedInterval, upperBounds: joinedUpperBounds })); + } + } + return result; } public override meet(other: this): this { @@ -117,7 +237,7 @@ export class ClosedPentagonDomain extends StateAbstractDomain): StateDomainLift { + public static reduce(value: StateDomainLift): StateDomainLift { if(value === Bottom) { return Bottom; } @@ -127,31 +247,10 @@ export class ClosedPentagonDomain extends StateAbstractDomain(); - const removeBounds = new Set(); - for(const [otherKey, otherPentagon] of value.entries()) { - if(key === otherKey) { - continue; - } - const keyInterval = pentagon.value.interval; - const otherKeyInterval = otherPentagon.value.interval; - if(!pentagon.value.upperBounds.has(otherKey) && keyInterval.isValue() && otherKeyInterval.isValue() && keyInterval.value[1] <= otherKeyInterval.value[0]) { - newInferredBounds.add(otherKey); - } - } - + // If there is a self reference in the upper bounds, remove it if(pentagon.value.upperBounds.has(key)) { - removeBounds.add(key); - } - - if(newInferredBounds.size > 0 || removeBounds.size > 0) { const reducedPentagon = pentagon.create(pentagon.value); - for(const bound of newInferredBounds.values()) { - reducedPentagon.value.upperBounds.add(bound); - } - for(const bound of removeBounds.values()) { - reducedPentagon.value.upperBounds.remove(bound); - } + reducedPentagon.value.upperBounds.remove(key); (value as Map).set(key, reducedPentagon); } } diff --git a/src/abstract-interpretation/pentagon/expression-semantics.ts b/src/abstract-interpretation/pentagon/expression-semantics.ts index 33e56516ecf..a71cd0f589c 100644 --- a/src/abstract-interpretation/pentagon/expression-semantics.ts +++ b/src/abstract-interpretation/pentagon/expression-semantics.ts @@ -21,7 +21,7 @@ const numericInferenceLogger = log.getSubLogger({ name: 'numeric-pentagon-infere /** * Maps function/operator names to the semantic functions. */ -const PentagonExpressionSemanticsMapper = [ +export const PentagonExpressionSemanticsMapper = [ [Identifier.make('+'), unaryBinaryExprOpSemantics(pentagonUnaryIdentityOp, pentagonAddOp)], [Identifier.make('-'), unaryBinaryExprOpSemantics(pentagonNegativeOp, pentagonSubtractOp)] ] as const satisfies readonly PentagonSemanticsMapperInfo[]; diff --git a/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts b/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts index 02560f8ae02..1eed3d0c8c6 100644 --- a/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts +++ b/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts @@ -3,6 +3,7 @@ import type { AbsintVisitorConfiguration } from '../absint-visitor'; import { AbstractInterpretationVisitor } from '../absint-visitor'; import { ClosedPentagonValueDomain } from './closed-pentagon-value-domain'; import type { DataflowGraphVertexFunctionCall, DataflowGraphVertexValue } from '../../dataflow/graph/vertex'; +import { isFunctionCallVertex, isValueVertex } from '../../dataflow/graph/vertex'; import type { RNumber } from '../../r-bridge/lang-4.x/ast/model/nodes/r-number'; import type { ParentInformation } from '../../r-bridge/lang-4.x/ast/model/processing/decorate'; import { IntervalDomain } from '../domains/interval-domain'; @@ -18,6 +19,8 @@ import type { AnyAbstractDomain } from '../domains/abstract-domain'; import { log } from '../../util/log'; import type { ResolveInfo } from '../../dataflow/eval/resolve/alias-tracking'; import { VariableResolve } from '../../config'; +import { FunctionArgument } from '../../dataflow/graph/graph'; +import { Bottom } from '../domains/lattice'; const numericInferenceLogger = log.getSubLogger({ name: 'numeric-pentagon-inference' }); @@ -75,9 +78,66 @@ export class NumericPentagonInferenceVisitor extends AbstractInterpretationVisit this.currentState.set(sourceOrigin, sourcePentagon); this.currentState.set(target, targetPentagon); } + + // Remove information of all constants/expression results on the right hand side + this.currentState = this.removeConstantAndExpressionInfo(source); } } + /** + * Removes all inferred information for expressions and constants in the state, that are part of the provided nodeId. + * This is used for assignments, to remove any information on constants or expressions that are part of the source + * part of the assignment to reduce the number of inferred values for the following inference steps + * (as these information will not be referenced/required anymore, and will still be present in the traces of the + * respective node if queried). + * @param nodeId - The root node that contains the constant/expression infos to remove (should be source part of assignment). + * @param state - Optional state to modify, defaults to this.currentState. + * @private + */ + private removeConstantAndExpressionInfo(nodeId: NodeId, state?: ClosedPentagonDomain): ClosedPentagonDomain { + state ??= this.currentState; + const minifiedDomain = state.create(state.value); + + const removeConstant = (nodeId: NodeId, state: ClosedPentagonDomain): NodeId[] => { + // Remove information of all constants on the right hand side + const rhsVertex = this.config.dfg.getVertex(nodeId); + if(isValueVertex(rhsVertex)) { + state.remove(nodeId); + return [nodeId]; + } else if(isFunctionCallVertex(rhsVertex)) { + let removedNodeIds: NodeId[] = []; + for(const arg of rhsVertex.args.map(FunctionArgument.getReference).filter(isNotUndefined)) { + removedNodeIds = removedNodeIds.concat(removeConstant(arg, state)); + } + state.remove(nodeId); + removedNodeIds.push(nodeId); + return removedNodeIds; + } + return []; + }; + + const removedNodeIds = new Set(removeConstant(nodeId, minifiedDomain)); + + if(minifiedDomain.value !== Bottom && removedNodeIds.size > 0) { + for(const [key, pentagon] of minifiedDomain.value.entries()) { + if(pentagon.value.upperBounds.isValue()) { + const upperBoundsToRemove = pentagon.value.upperBounds.value.intersection(removedNodeIds); + if(upperBoundsToRemove.size > 0) { + const reducedPentagon = pentagon.create(pentagon.value); + for(const bound of upperBoundsToRemove.values()) { + reducedPentagon.value.upperBounds.remove(bound); + } + // Manually set the value as we do not want to trigger the reduction for every set, + // as we apply the reduction at the end. + (minifiedDomain.value as Map).set(key, reducedPentagon); + } + } + } + } + + return state.create(ClosedPentagonDomain.reduce(minifiedDomain.value)); + } + protected override onNumberConstant({ vertex, node }: { vertex: DataflowGraphVertexValue, node: RNumber }) { super.onNumberConstant({ vertex, node }); @@ -143,7 +203,7 @@ export class NumericPentagonInferenceVisitor extends AbstractInterpretationVisit // As we currently cannot describe that we have upper bounds-info but not know whether it is a numeric scalar value, we cannot infer upper-bounds values for non-numeric scalar values. return; } - pentagon.value.upperBounds = value; + pentagon.value.upperBounds = value.create(value.value); state.set(node, pentagon); } @@ -163,26 +223,24 @@ export class NumericPentagonInferenceVisitor extends AbstractInterpretationVisit } protected override applyConditionSemantics(state: ClosedPentagonDomain, conditionNodeId: NodeId, trueBranch: boolean): ClosedPentagonDomain { - const reducePentagon = (state: ClosedPentagonDomain) => state.create(state.value); - const { applyConditionSemantics: intervalPositiveSemantics, applyNegatedConditionSemantics: intervalNegativeSemantics } = getIntervalConditionSemantics(); const { applyConditionSemantics: upperBoundsPositiveSemantics, applyNegatedConditionSemantics: upperBoundsNegativeSemantics } = getUpperBoundsConditionSemantics(); const intervalSemantics = trueBranch ? intervalPositiveSemantics : intervalNegativeSemantics; const ubSemantics = trueBranch ? upperBoundsPositiveSemantics : upperBoundsNegativeSemantics; - return reducePentagon( - ubSemantics( + const conditionState = ubSemantics( + conditionNodeId, + intervalSemantics( conditionNodeId, - intervalSemantics( - conditionNodeId, - state, - this, - this.config.dfg - ), + state, this, this.config.dfg - ) + ), + this, + this.config.dfg ); + + return this.removeConstantAndExpressionInfo(conditionNodeId, conditionState); } } \ No newline at end of file diff --git a/src/project/plugins/project-discovery/flowr-analyzer-project-discovery-plugin.ts b/src/project/plugins/project-discovery/flowr-analyzer-project-discovery-plugin.ts index b2e6ef8498d..e236921d7b9 100644 --- a/src/project/plugins/project-discovery/flowr-analyzer-project-discovery-plugin.ts +++ b/src/project/plugins/project-discovery/flowr-analyzer-project-discovery-plugin.ts @@ -23,7 +23,7 @@ export abstract class FlowrAnalyzerProjectDiscoveryPlugin extends FlowrAnalyzerP } const discoverRSourcesRegex = /\.(r|rmd|ipynb|qmd|rnw)$/i; -const ignorePathsWith = /(\.git|\.svn|\.hg|renv|packrat|node_modules|__pycache__|\.Rproj\.user)/i; +const ignorePathsWith = /(\.git|\.svn|\.hg|rv|renv|packrat|node_modules|__pycache__|\.Rproj\.user)/i; const excludeRequestsForPaths = /vignettes?|tests?|revdep|inst|data/i; /** Configuration options for the {@link DefaultFlowrAnalyzerProjectDiscoveryPlugin}. */ diff --git a/test/functionality/abstract-interpretation/interval/inference.test.ts b/test/functionality/abstract-interpretation/interval/inference.test.ts index b3866de79e8..92c6cfd7d69 100644 --- a/test/functionality/abstract-interpretation/interval/inference.test.ts +++ b/test/functionality/abstract-interpretation/interval/inference.test.ts @@ -112,7 +112,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar(0) }], ['/', { domain: IntervalTests.scalar(0) }], ['^', { domain: IntervalTests.scalar(Number.POSITIVE_INFINITY) }], - ['%%', { domain: IntervalTests.scalar(0%(-5)) }], + ['%%', { domain: IntervalTests.scalar(0) }], ])], [['2', '5'], new Map([ ['+', { domain: IntervalTests.scalar(2+5) }], @@ -120,7 +120,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar(2*5) }], ['/', { domain: IntervalTests.scalar(2/5) }], ['^', { domain: IntervalTests.scalar(2**5) }], - ['%%', { domain: IntervalTests.scalar(2%5) }] + ['%%', { domain: IntervalTests.scalar(2) }] ])], [['384', '92'], new Map([ ['+', { domain: IntervalTests.scalar(384+92) }], @@ -128,7 +128,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar(384*92) }], ['/', { domain: IntervalTests.scalar(384/92) }], ['^', { domain: IntervalTests.scalar(384**92) }], - ['%%', { domain: IntervalTests.scalar(384%92) }] + ['%%', { domain: IntervalTests.scalar(16) }] ])], [['(-5)', '18'], new Map([ ['+', { domain: IntervalTests.scalar((-5)+18) }], @@ -136,7 +136,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar((-5)*18) }], ['/', { domain: IntervalTests.scalar((-5)/18) }], ['^', { domain: IntervalTests.scalar((-5)**18) }], - ['%%', { domain: IntervalTests.scalar((-5)%18) }] + ['%%', { domain: IntervalTests.scalar(13) }] ])], [['(-15)', '-2'], new Map([ ['+', { domain: IntervalTests.scalar((-15)+(-2)) }], @@ -144,7 +144,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar((-15)*(-2)) }], ['/', { domain: IntervalTests.scalar((-15)/(-2)) }], ['^', { domain: IntervalTests.scalar((-15)**(-2)) }], - ['%%', { domain: IntervalTests.scalar((-15)%(-2)) }] + ['%%', { domain: IntervalTests.scalar(-1) }] ])], [['2.7', '1.3'], new Map([ ['+', { domain: IntervalTests.scalar(2.7+1.3) }], @@ -152,7 +152,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar(2.7*1.3) }], ['/', { domain: IntervalTests.scalar(2.7/1.3) }], ['^', { domain: IntervalTests.scalar(2.7**1.3), matching: DomainMatchingType.Overapproximation }], - ['%%', { domain: IntervalTests.scalar(2.7%1.3) }] + ['%%', { domain: IntervalTests.scalar(0.1, 15) }] ])], [['2', '1.3'], new Map([ ['+', { domain: IntervalTests.scalar(2+1.3) }], @@ -160,7 +160,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar(2*1.3) }], ['/', { domain: IntervalTests.scalar(2/1.3) }], ['^', { domain: IntervalTests.scalar(2**1.3), matching: DomainMatchingType.Overapproximation }], - ['%%', { domain: IntervalTests.scalar(2%1.3) }] + ['%%', { domain: IntervalTests.scalar(0.7) }] ])], [['5', '-3'], new Map([ ['+', { domain: IntervalTests.scalar(5+(-3)) }], @@ -168,7 +168,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar(5*(-3)) }], ['/', { domain: IntervalTests.scalar(5/(-3), 16) }], ['^', { domain: IntervalTests.scalar(5**(-3)) }], - ['%%', { domain: IntervalTests.scalar(5%(-3)) }] + ['%%', { domain: IntervalTests.scalar(-1) }] ])], [['(-2)', '4'], new Map([ ['+', { domain: IntervalTests.scalar((-2)+4) }], @@ -176,7 +176,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar((-2)*4) }], ['/', { domain: IntervalTests.scalar((-2)/4) }], ['^', { domain: IntervalTests.scalar((-2)**4) }], - ['%%', { domain: IntervalTests.scalar((-2)%4) }] + ['%%', { domain: IntervalTests.scalar(2) }] ])], [['(-3)', '-6'], new Map([ ['+', { domain: IntervalTests.scalar((-3)+(-6)) }], @@ -184,7 +184,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar((-3)*(-6)) }], ['/', { domain: IntervalTests.scalar((-3)/(-6)) }], ['^', { domain: IntervalTests.scalar((-3)**(-6)) }], - ['%%', { domain: IntervalTests.scalar((-3)%(-6)) }] + ['%%', { domain: IntervalTests.scalar(-3) }] ])], [['1e10', '1e-5'], new Map([ ['+', { domain: IntervalTests.scalar(1e10+1e-5) }], @@ -192,7 +192,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.scalar(1e10*1e-5) }], ['/', { domain: IntervalTests.scalar(1e10/1e-5) }], ['^', { domain: IntervalTests.scalar(1e10**1e-5), matching: DomainMatchingType.Overapproximation }], - ['%%', { domain: IntervalTests.scalar(1e10%1e-5) }] + ['%%', { domain: IntervalTests.scalar(9.181909e-06, 5) }] ])], [['Inf', '0'], new Map([ ['+', { domain: IntervalTests.scalar(Infinity) }], @@ -312,7 +312,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.interval(-10, 20) }], ['/', { domain: IntervalTests.interval((-2)/5, 4/5) }], ['^', { domain: IntervalTests.interval((-2)**5, 4**5) }], - ['%%', { domain: IntervalTests.interval(0, 4) }] + ['%%', { domain: IntervalTests.interval(3, 4), matching: DomainMatchingType.Overapproximation }] ])], [['ifelse(c, 1, 4)', '5'], new Map([ ['+', { domain: IntervalTests.interval(6, 9) }], @@ -320,7 +320,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.interval(5, 20) }], ['/', { domain: IntervalTests.interval(1/5, 4/5) }], ['^', { domain: IntervalTests.interval(1, 4**5) }], - ['%%', { domain: IntervalTests.interval(0, 4) }] + ['%%', { domain: IntervalTests.interval(1, 4), matching: DomainMatchingType.Overapproximation }] ])], [['ifelse(c, -1, -4)', '5'], new Map([ ['+', { domain: IntervalTests.interval(1, 4) }], @@ -328,7 +328,7 @@ export const binaryOperatorSuccessTestCases: IntervalInferenceOperatorTestCase = ['*', { domain: IntervalTests.interval(-20, -5) }], ['/', { domain: IntervalTests.interval((-4)/5, (-1)/5) }], ['^', { domain: IntervalTests.interval((-4)**5, (-1)**5) }], - ['%%', { domain: IntervalTests.interval(0, 4) }] + ['%%', { domain: IntervalTests.interval(1, 4), matching: DomainMatchingType.Overapproximation }] ])] ] as const; @@ -343,7 +343,7 @@ export const lengthTestCases: [value: string, expected: IntervalSlicingCriterion ['"Hallo"', { domain: IntervalTests.interval(0, Infinity) }], ['TRUE', { domain: IntervalTests.interval(0, Infinity) }], ['NULL', { domain: IntervalTests.interval(0, Infinity) }], - ['1, 2', { domain: IntervalTests.bottom() }] + ['1, 2', { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }] ] as const; describe('Interval Inference', () => { @@ -390,6 +390,16 @@ describe('Interval Inference', () => { '1@x': { domain: IntervalTests.bottom() }, '2@y': { domain: IntervalTests.bottom() } }); + + testIntervalDomain(` + data <- data.frame (a = c (1, 3, 7, 12, 9), + b = c (4, 4, 6, 7, 8), + c = c (14, 15, 11, 10, 6)) + x <- apply(data, 1, length) + `, { + '1@data': { domain: IntervalTests.top() }, + '4@x': { domain: IntervalTests.top() } + }); }); describe('sum semantics', () => { @@ -433,10 +443,11 @@ describe('Interval Inference', () => { const testCases: [arguments: string[], expected: IntervalSlicingCriterionExpected][] = [ // Copy the test cases from below [[], { domain: IntervalTests.bottom() }], - [['1', '2'], { domain: IntervalTests.bottom() }], + [['1', '2'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['1'], { domain: IntervalTests.scalar(1) }], [['-1'], { domain: IntervalTests.scalar(1) }], - [['ifelse(c, -5, 2)'], { domain: IntervalTests.interval(2, 5) }], + [['ifelse(c, -5, 2)'], { domain: IntervalTests.interval(2, 5), matching: DomainMatchingType.Overapproximation }], + [['ifelse(c, -5, ifelse(c, 1, 2))'], { domain: IntervalTests.interval(1, 5), matching: DomainMatchingType.Overapproximation }], [['c(1,2,3)'], { domain: IntervalTests.top() }] ]; @@ -499,7 +510,7 @@ describe('Interval Inference', () => { describe('sign', () => { const testCases: [argument: string[], expected: IntervalSlicingCriterionExpected][] = [ [[], { domain: IntervalTests.bottom() }], - [['0.2851', '2'], { domain: IntervalTests.bottom() }], + [['0.2851', '2'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['0'], { domain: IntervalTests.scalar(0) }], [['-1'], { domain: IntervalTests.scalar(-1) }], [['4'], { domain: IntervalTests.scalar(1) }], @@ -522,7 +533,7 @@ describe('Interval Inference', () => { describe('sqrt', () => { const testCases: [argument: string[], expected: IntervalSlicingCriterionExpected][] = [ [[], { domain: IntervalTests.bottom() }], - [['0.2851', '2'], { domain: IntervalTests.bottom() }], + [['0.2851', '2'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['0'], { domain: IntervalTests.scalar(0) }], [['-1'], { domain: IntervalTests.top() }], [['4'], { domain: IntervalTests.scalar(2) }], @@ -626,7 +637,7 @@ describe('Interval Inference', () => { const testCases: [argument: string[], expected: IntervalSlicingCriterionExpected][] = [ [[], { domain: IntervalTests.bottom() }], [['Hallo'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], - [['2, 3'], { domain: IntervalTests.bottom() }], + [['2, 3'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['2'], { domain: IntervalTests.scalar(Math.sin(2)), matching: DomainMatchingType.Overapproximation }], [['0'], { domain: IntervalTests.scalar(Math.sin(0)), matching: DomainMatchingType.Overapproximation }], [['-1.5'], { domain: IntervalTests.scalar(Math.sin(-1)), matching: DomainMatchingType.Overapproximation }], @@ -648,7 +659,7 @@ describe('Interval Inference', () => { const testCases: [argument: string[], expected: IntervalSlicingCriterionExpected][] = [ [[], { domain: IntervalTests.bottom() }], [['Hallo'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], - [['2, 3'], { domain: IntervalTests.bottom() }], + [['2, 3'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['2'], { domain: IntervalTests.scalar(Math.cos(2)), matching: DomainMatchingType.Overapproximation }], [['0'], { domain: IntervalTests.scalar(Math.cos(0)), matching: DomainMatchingType.Overapproximation }], [['-1.5'], { domain: IntervalTests.scalar(Math.cos(-1)), matching: DomainMatchingType.Overapproximation }], @@ -670,8 +681,8 @@ describe('Interval Inference', () => { describe('nrow', () => { const testCases: [argument: string[], expected: IntervalSlicingCriterionExpected][] = [ [[], { domain: IntervalTests.bottom() }], - [['2, 3'], { domain: IntervalTests.bottom() }], - [['data.frame(), data.frame()'], { domain: IntervalTests.bottom() }], + [['2, 3'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], + [['data.frame(), data.frame()'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['2'], { domain: IntervalTests.top() }], [['data.frame(c(1,2,3), c(1,2))'], { domain: IntervalTests.scalar(3), matching: DomainMatchingType.Overapproximation }], [['data.frame(c(1), c(2,3), c(1,2,3,4))'], { domain: IntervalTests.scalar(4), matching: DomainMatchingType.Overapproximation }], @@ -702,8 +713,8 @@ describe('Interval Inference', () => { const testCases: [argument: string[], expected: IntervalSlicingCriterionExpected][] = [ [[], { domain: IntervalTests.bottom() }], [['Hallo'], { domain: IntervalTests.scalar(1), matching: DomainMatchingType.Overapproximation }], - [['2, 3'], { domain: IntervalTests.bottom() }], - [['data.frame(), data.frame()'], { domain: IntervalTests.bottom() }], + [['2, 3'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], + [['data.frame(), data.frame()'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['2'], { domain: IntervalTests.scalar(1) }], [['c(1,2,3)'], { domain: IntervalTests.scalar(3), matching: DomainMatchingType.Overapproximation }], [['data.frame(c(1,2,3), c(1,2))'], { domain: IntervalTests.scalar(3), matching: DomainMatchingType.Overapproximation }], @@ -722,8 +733,8 @@ describe('Interval Inference', () => { describe('ncol', () => { const testCases: [argument: string[], expected: IntervalSlicingCriterionExpected][] = [ [[], { domain: IntervalTests.bottom() }], - [['2, 3'], { domain: IntervalTests.bottom() }], - [['data.frame(), data.frame()'], { domain: IntervalTests.bottom() }], + [['2, 3'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], + [['data.frame(), data.frame()'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['2'], { domain: IntervalTests.top() }], [['data.frame(c(1,2,3), c(1,2))'], { domain: IntervalTests.scalar(2), matching: DomainMatchingType.Overapproximation }], [['data.frame(c(1), c(2,3), c(1,2,3,4))'], { domain: IntervalTests.scalar(3), matching: DomainMatchingType.Overapproximation }], @@ -754,8 +765,8 @@ describe('Interval Inference', () => { const testCases: [argument: string[], expected: IntervalSlicingCriterionExpected][] = [ [[], { domain: IntervalTests.bottom() }], [['Hallo'], { domain: IntervalTests.scalar(1), matching: DomainMatchingType.Overapproximation }], - [['2, 3'], { domain: IntervalTests.bottom() }], - [['data.frame(), data.frame()'], { domain: IntervalTests.bottom() }], + [['2, 3'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], + [['data.frame(), data.frame()'], { domain: IntervalTests.bottom(), matching: DomainMatchingType.Overapproximation }], [['2'], { domain: IntervalTests.scalar(1) }], [['c(1,2,3)'], { domain: IntervalTests.scalar(1), matching: DomainMatchingType.Overapproximation }], [['data.frame(c(1,2,3), c(1,2))'], { domain: IntervalTests.scalar(2), matching: DomainMatchingType.Overapproximation }], @@ -1418,4 +1429,33 @@ describe('Interval Inference', () => { '3@x': { domain: IntervalTests.interval(1, 4), matching: DomainMatchingType.Overapproximation }, }); }); + + describe('Joining two states where a variable is known in both states but undefined in only one leads to underapproximation', { fails: true }, () => { + testIntervalDomain(` + x <- "UNDEFINED" # Simply anything produces undefined + + if(x == 1) { + x # Applying the condition updates the origin of x to be [1, 1] + } else { + x # Applying the condition updates the origin of x to remain undefined + } + x # Joining both branches should result in undefined + `, { + '8@x': { domain: IntervalTests.top() }, + }); + }); + + describe('Fails to resolve correct origin when for loop overrides variable from before for-loop', { fails: true }, () => { + testIntervalDomain(` + i <- 111 + for (i in 1:20) { + if (i %% 10 == 0) { + i # should be reachable for i = 10 and i = 20, but currently always resolves i to 111 and therefore asserts unreachable + } + } + i + `, { + '4@i': { domain: IntervalTests.interval(10, 20), matching: DomainMatchingType.Overapproximation }, + }); + }); }); diff --git a/test/functionality/abstract-interpretation/interval/interval.ts b/test/functionality/abstract-interpretation/interval/interval.ts index 5e881017716..b4d0c7591be 100644 --- a/test/functionality/abstract-interpretation/interval/interval.ts +++ b/test/functionality/abstract-interpretation/interval/interval.ts @@ -110,7 +110,7 @@ export function testIntervalDomain(code: string, expected: IntervalTestExpected) } const errorContext = `expected inferred value ${inferredIntervalDomain?.toString()} to be ${criterionExpected.matching} - match for ${criterionExpected.domain?.toString()} in final state ${visitor.getEndState().toString()} for ${code.trim().replaceAll('\n', ' \\n ')}`; + match for ${criterionExpected.domain?.toString()} (${targetId}) in trace \n${visitor.getAbstractTrace().entries().map(([key, value]) => `${key} => ${value.toString()}`).toArray().join('\n')}\nin final state ${visitor.getEndState().toString()}\nfor: ${code.trim().replaceAll('\n', ' \\n ')}`; if(!isUndefined(inferredIntervalDomain) && !isUndefined(criterionExpected.domain)) { if(criterionExpected.matching === DomainMatchingType.Equal) { diff --git a/test/functionality/abstract-interpretation/pentagon/inference.test.ts b/test/functionality/abstract-interpretation/pentagon/inference.test.ts index e2b8339e3b4..64855b95eae 100644 --- a/test/functionality/abstract-interpretation/pentagon/inference.test.ts +++ b/test/functionality/abstract-interpretation/pentagon/inference.test.ts @@ -75,6 +75,8 @@ describe('Pentagon Inference', () => { describe('combined pentagon part', () => { describe('basic combined calculation', () => { + // For this example, we can only infer implicit upper bounds via the interval domain, which are not + // explicitly present in the upper bounds testPentagonDomain(` x <- 3 y <- -4 @@ -84,10 +86,10 @@ describe('Pentagon Inference', () => { invalid <- Inf * zero `, { '1@x': { interval: IntervalTests.scalar(3), upperBounds: UpperBoundsTests.top() }, - '2@y': { interval: IntervalTests.scalar(-4), upperBounds: UpperBoundsTests.bounds(['1@x']) }, - '3@z': { interval: IntervalTests.scalar(2.4), upperBounds: UpperBoundsTests.bounds(['1@x']), lowerBounds: UpperBoundsTests.bounds(['2@y']) }, - '4@result': { interval: IntervalTests.scalar(3*3-(-4)*2.4), upperBounds: UpperBoundsTests.top(), lowerBounds: UpperBoundsTests.bounds(['1@x']) }, - '5@zero': { interval: IntervalTests.scalar(0), upperBounds: UpperBoundsTests.bounds(['1@x', '3@z']), lowerBounds: UpperBoundsTests.bounds(['2@y']) }, + '2@y': { interval: IntervalTests.scalar(-4), upperBounds: UpperBoundsTests.top() }, + '3@z': { interval: IntervalTests.scalar(2.4), upperBounds: UpperBoundsTests.top() }, + '4@result': { interval: IntervalTests.scalar(3*3-(-4)*2.4), upperBounds: UpperBoundsTests.top() }, + '5@zero': { interval: IntervalTests.scalar(0), upperBounds: UpperBoundsTests.top() }, '6@invalid': { interval: IntervalTests.top(), upperBounds: UpperBoundsTests.top() } }); @@ -97,7 +99,7 @@ describe('Pentagon Inference', () => { z <- x + y `, { '1@x': { interval: IntervalTests.scalar(-Infinity), upperBounds: UpperBoundsTests.top() }, - '2@y': { interval: IntervalTests.scalar(4), upperBounds: UpperBoundsTests.top(), lowerBounds: UpperBoundsTests.bounds(['1@x']) }, + '2@y': { interval: IntervalTests.scalar(4), upperBounds: UpperBoundsTests.top() }, '3@z': { interval: IntervalTests.scalar(-Infinity), upperBounds: UpperBoundsTests.bounds(['3@y']), lowerBounds: UpperBoundsTests.bounds(['3@x']) }, }); }); diff --git a/test/functionality/abstract-interpretation/pentagon/thesis-example.test.ts b/test/functionality/abstract-interpretation/pentagon/thesis-example.test.ts index 820eaef0f5a..0b36e5d9d04 100644 --- a/test/functionality/abstract-interpretation/pentagon/thesis-example.test.ts +++ b/test/functionality/abstract-interpretation/pentagon/thesis-example.test.ts @@ -21,7 +21,7 @@ describe('Thesis example', () => { `, { '5@x': { interval: IntervalTests.interval(-Infinity, Infinity), upperBounds: UpperBoundsTests.top() }, '5@a': { interval: IntervalTests.interval(3.5, 4.5), upperBounds: UpperBoundsTests.top() }, - '6@b': { interval: IntervalTests.interval(2 * Math.log(3.5), 2 * Math.log(4.5)), upperBounds: UpperBoundsTests.bounds(['5@a']) }, + '6@b': { interval: IntervalTests.interval(2 * Math.log(3.5), 2 * Math.log(4.5)), upperBounds: UpperBoundsTests.top() }, '9@result': { interval: IntervalTests.bottom(), upperBounds: UpperBoundsTests.bounds(['8@b']) }, '11@result': { interval: IntervalTests.interval(2 * Math.log(3.5), 2 * Math.log(4.5)), upperBounds: UpperBoundsTests.bounds(['8@a', '8@b']) }, '13@result': { interval: IntervalTests.interval(2 * Math.log(3.5), 2 * Math.log(4.5)), upperBounds: UpperBoundsTests.bounds(['8@a', '8@b']), lowerBounds: UpperBoundsTests.bounds(['8@b'], ['8@a']) }, @@ -53,8 +53,8 @@ describe('Thesis example', () => { cat(result, low, high) `, { '3@result': { interval: IntervalTests.scalar(-1), upperBounds: UpperBoundsTests.top() }, - '4@low': { interval: IntervalTests.scalar(1), upperBounds: UpperBoundsTests.top(), lowerBounds: UpperBoundsTests.bounds(['3@result']) }, - '5@high': { interval: IntervalTests.interval(0, Infinity), upperBounds: UpperBoundsTests.top(), lowerBounds: UpperBoundsTests.bounds(['3@result']) }, + '4@low': { interval: IntervalTests.scalar(1), upperBounds: UpperBoundsTests.top(), lowerBounds: UpperBoundsTests.top() }, + '5@high': { interval: IntervalTests.interval(0, Infinity), upperBounds: UpperBoundsTests.top(), lowerBounds: UpperBoundsTests.top() }, '6@low': { interval: IntervalTests.interval(1, Infinity), intervalMatching: DomainMatchingType.Overapproximation, upperBounds: UpperBoundsTests.bounds(['6@high']), lowerBounds: UpperBoundsTests.bounds(['3@result']) }, '6@high': { interval: IntervalTests.interval(1, Infinity), intervalMatching: DomainMatchingType.Overapproximation, upperBounds: UpperBoundsTests.bounds(['3@result']), lowerBounds: UpperBoundsTests.bounds(['6@low']) }, '7@mid': { interval: IntervalTests.interval(1, Infinity), intervalMatching: DomainMatchingType.Overapproximation, upperBounds: UpperBoundsTests.top(), lowerBounds: UpperBoundsTests.bounds(['3@result']) },