From 9de08ae0e94517f6ff019f3be9af94e68686855d Mon Sep 17 00:00:00 2001 From: Henry Date: Thu, 21 May 2026 22:26:03 +0200 Subject: [PATCH 01/13] feat: first try to reduce ram - Remove unused inferred information for constant values and expression results after an assignment is complete/a condition has been processed. --- .../pentagon/closed-pentagon-domain.ts | 2 +- .../pentagon/numeric-pentagon-inference.ts | 72 +++++++++++++++---- 2 files changed, 61 insertions(+), 13 deletions(-) diff --git a/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts b/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts index f61ea4b9661..866fdadee18 100644 --- a/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts +++ b/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts @@ -117,7 +117,7 @@ export class ClosedPentagonDomain extends StateAbstractDomain): StateDomainLift { + public static reduce(value: StateDomainLift): StateDomainLift { if(value === Bottom) { return Bottom; } diff --git a/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts b/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts index e56e5c2aab2..da4a43fac28 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'; @@ -16,6 +17,8 @@ import { getUpperBoundsConditionSemantics } from './upper-bounds/upper-bounds-co import type { AnyStateDomain } from '../domains/state-domain-like'; import type { AnyAbstractDomain } from '../domains/abstract-domain'; import { log } from '../../util/log'; +import { FunctionArgument } from '../../dataflow/graph/graph'; +import { Bottom } from '../domains/lattice'; const numericInferenceLogger = log.getSubLogger({ name: 'numeric-pentagon-inference' }); @@ -73,9 +76,56 @@ export class NumericPentagonInferenceVisitor extends AbstractInterpretationVisit this.currentState.set(sourceOrigin, sourcePentagon); this.currentState.set(target, targetPentagon); } + + // Remove information of all constants on the right hand side + this.currentState = this.removeConstantAndExpressionInfo(source); } } + 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 }); @@ -140,7 +190,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); } @@ -160,26 +210,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 From 80f7255d8549008877db7f44f10aed75a2502445 Mon Sep 17 00:00:00 2001 From: Henry Date: Wed, 3 Jun 2026 15:31:29 +0200 Subject: [PATCH 02/13] feat: added benchmarking script --- src/abstract-interpretation/benchmarking.ts | 198 ++++++++++++++++++ .../pentagon/expression-semantics.ts | 2 +- 2 files changed, 199 insertions(+), 1 deletion(-) create mode 100644 src/abstract-interpretation/benchmarking.ts diff --git a/src/abstract-interpretation/benchmarking.ts b/src/abstract-interpretation/benchmarking.ts new file mode 100644 index 00000000000..1e1bc761781 --- /dev/null +++ b/src/abstract-interpretation/benchmarking.ts @@ -0,0 +1,198 @@ +import fs from 'node:fs'; +import type { NodeId } from '../r-bridge/lang-4.x/ast/model/processing/node-id'; +import { FlowrAnalyzerBuilder } from '../project/flowr-analyzer-builder'; +import { fileProtocol } from '../r-bridge/retriever'; +import { BuiltInProcName } from '../dataflow/environments/built-in-proc-name'; +import { VertexType } from '../dataflow/graph/vertex'; +import { RType } from '../r-bridge/lang-4.x/ast/model/type'; +import { IntervalExpressionSemanticsMapper } from './interval/expression-semantics'; +import { Identifier } from '../dataflow/environments/identifier'; +import { isNotUndefined, isUndefined } from '../util/assert'; +import { PentagonExpressionSemanticsMapper } from './pentagon/expression-semantics'; +import { IntervalSemanticsMaper } from './interval/condition-semantics'; +import { UpperBoundsSemanticsMapper } from './pentagon/upper-bounds/upper-bounds-condition-semantics'; +import { NumericIntervalInferenceVisitor } from './interval/numeric-interval-inference'; +import { SourceLocation } from '../util/range'; +import { NumericPentagonInferenceVisitor } from './pentagon/numeric-pentagon-inference'; +import path from 'path'; + +if(process.argv.length < 4) { + console.error('Usage: ts-node src/abstract-interpretation/benchmarking.ts '); + process.exit(1); +} + +const filePath = process.argv[2]; +const outputDirectory = process.argv[3]; + +interface FileMetadata { + fileName: string; + intervalResultFileName: string; + pentagonResultFileName: string; + loc: number; + numOfConstants: number; + numOfRNumberConstants: number; + RNumberConstantNodeIds: NodeId[]; + numOfFunctionCalls: number; + numOfSupportedExpressionFunctionCalls: number; + SupportedExpressionFunctionCallNodeIds: NodeId[]; + numOfSupportedConditionFunctionCalls: number; + SupportedConditionFunctionCalls: NodeId[]; + numOfConditions: number; + metadataGatheringInMs: number; + baselineInMs: number; + intervalAnalysisInMs: number; + intervalResultGatheringInMs: number; + pentagonAnalysisInMs: number; + pentagonResultGatheringInMs: number; +} + +interface InferredValue { + nodeId: NodeId; + inferredValue: string; + significantFigures: string; + sourceLocation: string; +} + +void async function() { + fs.mkdirSync(outputDirectory, { recursive: true }); + const fileName = filePath.split('/').reverse()[0]; + const metadataOutputFile = fileName.slice(0, -2) + '.csv'; + const intervalResultFile = fileName.slice(0, -2) + '-interval.csv'; + const pentagonResultFile = fileName.slice(0, -2) + '-pentagon.csv'; + + const baselineStart = performance.now(); + const analyzer = await new FlowrAnalyzerBuilder() + .setEngine('tree-sitter') + .build(); + analyzer.addRequest(fileProtocol + filePath); + const dfg = (await analyzer.dataflow()).graph; + const ast = await analyzer.normalize(); + + const visitorContext = { + normalizedAst: ast, + dfg: dfg, + controlFlow: await analyzer.controlflow(), + ctx: analyzer.inspectContext() + }; + const baselineEnd = performance.now(); + + // 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(isNotUndefined(value)) { + const node = ast.idMap.get(nodeId); + const location = node ? SourceLocation.fromNode(node) : undefined; + + intervalResults.push({ + nodeId: nodeId, + inferredValue: value?.toString() ?? 'undefined', + significantFigures: value?.significantFigures?.toString() ?? 'unknown', + sourceLocation: isUndefined(location) ? 'unknown' : SourceLocation.getRange(location).slice(0, 4).toString(), + }); + } + } + const intervalResultEnd = performance.now(); + + // Dump Interval Results + const intervalPath = path.join(outputDirectory, intervalResultFile); + if(fs.existsSync(intervalPath)) { + fs.rmSync(intervalPath, { recursive: true, force: true }); + } + fs.writeFileSync(intervalPath, ['nodeId', 'inferredValue', 'significantFigures', 'sourceLocation'].join(',') + '\n'); + for(const result of intervalResults) { + fs.appendFileSync(intervalPath, Object.values(result).map(value => '"' + value + '"').join(',') + '\n'); + } + + // 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(isNotUndefined(value)) { + const node = ast.idMap.get(nodeId); + const location = node ? SourceLocation.fromNode(node) : undefined; + + pentagonResults.push({ + nodeId: nodeId, + inferredValue: value?.toString() ?? 'undefined', + significantFigures: value?.value.interval.significantFigures?.toString() ?? 'unknown', + sourceLocation: isUndefined(location) ? 'unknown' : SourceLocation.getRange(location).slice(0, 4).toString(), + }); + } + } + const pentagonResultEnd = performance.now(); + + // Dump Pentagon Results + const pentagonPath = path.join(outputDirectory, pentagonResultFile); + if(fs.existsSync(pentagonPath)) { + fs.rmSync(pentagonPath, { recursive: true, force: true }); + } + fs.writeFileSync(pentagonPath, ['nodeId', 'inferredValue', 'significantFigures', 'sourceLocation'].join(',') + '\n'); + for(const result of pentagonResults) { + fs.appendFileSync(pentagonPath, Object.values(result).map(value => '"' + value + '"').join(',') + '\n'); + } + + // 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]) => + isNotUndefined(IntervalExpressionSemanticsMapper().find(([id]) => Identifier.matches(id, dfgCall.name))) || + isNotUndefined(PentagonExpressionSemanticsMapper.find(([id]) => Identifier.matches(id, dfgCall.name))) + ); + const supportedConditionFunctionCalls = functionCalls.filter(([_, dfgCall]) => + isNotUndefined(IntervalSemanticsMaper().find(([id]) => Identifier.matches(id, dfgCall.name))) || + isNotUndefined(UpperBoundsSemanticsMapper().find(([id]) => Identifier.matches(id, dfgCall.name))) || + ['&&', '!', '||'].some(id => Identifier.matches(id, dfgCall.name)) + ); + const conditions = functionCalls.filter(([_, dfgCall]) => + dfgCall.origin.includes(BuiltInProcName.IfThenElse) || dfgCall.origin.includes(BuiltInProcName.WhileLoop) + );//.map(([node, _]) => cfg.graph.ingoingEdges(node)?.keys().toArray()[0]); + const metadataEnd = performance.now(); + + const fileMetadata: FileMetadata = { + fileName: fileName, + intervalResultFileName: intervalResultFile, + pentagonResultFileName: pentagonResultFile, + loc: analyzer.inspectContext().files.getAllFiles()[0].content().toString().split('\n').length, + numOfConstants: constants.length, + numOfRNumberConstants: numberConstants.length, + RNumberConstantNodeIds: numberConstants.map(([node]) => node), + numOfFunctionCalls: functionCalls.length, + numOfSupportedExpressionFunctionCalls: supportedExpressionFunctionCalls.length, + SupportedExpressionFunctionCallNodeIds: supportedExpressionFunctionCalls.map(([node]) => node), + numOfSupportedConditionFunctionCalls: supportedConditionFunctionCalls.length, + SupportedConditionFunctionCalls: supportedConditionFunctionCalls.map(([node]) => node), + numOfConditions: conditions.length, + metadataGatheringInMs: metadataEnd - metadataStart, + baselineInMs: baselineEnd - baselineStart, + intervalAnalysisInMs: intervalEnd - intervalStart, + intervalResultGatheringInMs: intervalResultEnd - intervalResultStart, + pentagonAnalysisInMs: pentagonEnd - pentagonStart, + pentagonResultGatheringInMs: pentagonResultEnd - pentagonResultStart + }; + + // Dump File and Runtime Metadata + const fileMetadataPath = path.join(outputDirectory, metadataOutputFile); + if(fs.existsSync(fileMetadataPath)) { + fs.rmSync(fileMetadataPath, { recursive: true, force: true }); + } + fs.writeFileSync(fileMetadataPath, Object.keys(fileMetadata).join(',') + '\n' + + Object.values(fileMetadata).map(value => '"' + value + '"').join(',') + '\n'); +}(); \ No newline at end of file diff --git a/src/abstract-interpretation/pentagon/expression-semantics.ts b/src/abstract-interpretation/pentagon/expression-semantics.ts index e1131f31f16..7aae08ed72c 100644 --- a/src/abstract-interpretation/pentagon/expression-semantics.ts +++ b/src/abstract-interpretation/pentagon/expression-semantics.ts @@ -20,7 +20,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[]; From 6733f762b2a546dcfe28b66fe5d1aa3c10f25f90 Mon Sep 17 00:00:00 2001 From: Henry Date: Thu, 4 Jun 2026 13:06:42 +0200 Subject: [PATCH 03/13] feat: refined pentagon lattice operations from pentagon paper --- .../pentagon/closed-pentagon-domain.ts | 149 +++++++++++++++--- .../pentagon/inference.test.ts | 12 +- .../pentagon/thesis-example.test.ts | 4 +- 3 files changed, 133 insertions(+), 32 deletions(-) diff --git a/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts b/src/abstract-interpretation/pentagon/closed-pentagon-domain.ts index 866fdadee18..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 { @@ -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/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 cc6cc4b736f..5dae9b6cff0 100644 --- a/test/functionality/abstract-interpretation/pentagon/thesis-example.test.ts +++ b/test/functionality/abstract-interpretation/pentagon/thesis-example.test.ts @@ -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']) }, From 5edf6cd0a623a5166bc8d4774c5ceeb429d2beef Mon Sep 17 00:00:00 2001 From: Henry Date: Thu, 4 Jun 2026 15:33:50 +0200 Subject: [PATCH 04/13] feat-fix: first batch of pr fixes --- src/abstract-interpretation/benchmarking.ts | 83 +++++++++++---------- 1 file changed, 44 insertions(+), 39 deletions(-) diff --git a/src/abstract-interpretation/benchmarking.ts b/src/abstract-interpretation/benchmarking.ts index 1e1bc761781..9bf19af95d1 100644 --- a/src/abstract-interpretation/benchmarking.ts +++ b/src/abstract-interpretation/benchmarking.ts @@ -7,22 +7,21 @@ import { VertexType } from '../dataflow/graph/vertex'; import { RType } from '../r-bridge/lang-4.x/ast/model/type'; import { IntervalExpressionSemanticsMapper } from './interval/expression-semantics'; import { Identifier } from '../dataflow/environments/identifier'; -import { isNotUndefined, isUndefined } from '../util/assert'; import { PentagonExpressionSemanticsMapper } from './pentagon/expression-semantics'; import { IntervalSemanticsMaper } from './interval/condition-semantics'; import { UpperBoundsSemanticsMapper } from './pentagon/upper-bounds/upper-bounds-condition-semantics'; import { NumericIntervalInferenceVisitor } from './interval/numeric-interval-inference'; -import { SourceLocation } from '../util/range'; +import { SourceRange } from '../util/range'; import { NumericPentagonInferenceVisitor } from './pentagon/numeric-pentagon-inference'; import path from 'path'; +import type { AbsintVisitorConfiguration } from './absint-visitor'; if(process.argv.length < 4) { console.error('Usage: ts-node src/abstract-interpretation/benchmarking.ts '); process.exit(1); } -const filePath = process.argv[2]; -const outputDirectory = process.argv[3]; +const [_, __, filePath, outputDirectory] = process.argv; interface FileMetadata { fileName: string; @@ -40,6 +39,9 @@ interface FileMetadata { numOfConditions: number; metadataGatheringInMs: number; baselineInMs: number; + astInMs: number; + dfgInMs: number; + cfgInMs: number; intervalAnalysisInMs: number; intervalResultGatheringInMs: number; pentagonAnalysisInMs: number; @@ -51,31 +53,35 @@ interface InferredValue { inferredValue: string; significantFigures: string; sourceLocation: string; + lexeme: string; + dfgTag: VertexType | 'unknown'; } void async function() { fs.mkdirSync(outputDirectory, { recursive: true }); - const fileName = filePath.split('/').reverse()[0]; - const metadataOutputFile = fileName.slice(0, -2) + '.csv'; - const intervalResultFile = fileName.slice(0, -2) + '-interval.csv'; - const pentagonResultFile = fileName.slice(0, -2) + '-pentagon.csv'; + const fileName = path.basename(filePath); + const fileNameWithoutEnding = path.parse(fileName).name; + const metadataOutputFile = fileNameWithoutEnding + '.csv'; + const intervalResultFile = fileNameWithoutEnding + '-interval.csv'; + const pentagonResultFile = fileNameWithoutEnding + '-pentagon.csv'; const baselineStart = performance.now(); const analyzer = await new FlowrAnalyzerBuilder() .setEngine('tree-sitter') .build(); analyzer.addRequest(fileProtocol + filePath); - const dfg = (await analyzer.dataflow()).graph; + const astStart = performance.now(); const ast = await analyzer.normalize(); - - const visitorContext = { - normalizedAst: ast, - dfg: dfg, - controlFlow: await analyzer.controlflow(), - ctx: analyzer.inspectContext() - }; + 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); @@ -87,15 +93,16 @@ void async function() { const intervalResults: InferredValue[] = []; for(const nodeId of intervalVisitor.getAbstractTrace().keys()) { const value = intervalVisitor.getAbstractValue(nodeId); - if(isNotUndefined(value)) { + if(value !== undefined) { const node = ast.idMap.get(nodeId); - const location = node ? SourceLocation.fromNode(node) : undefined; intervalResults.push({ nodeId: nodeId, - inferredValue: value?.toString() ?? 'undefined', - significantFigures: value?.significantFigures?.toString() ?? 'unknown', - sourceLocation: isUndefined(location) ? 'unknown' : SourceLocation.getRange(location).slice(0, 4).toString(), + 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', }); } } @@ -103,9 +110,7 @@ void async function() { // Dump Interval Results const intervalPath = path.join(outputDirectory, intervalResultFile); - if(fs.existsSync(intervalPath)) { - fs.rmSync(intervalPath, { recursive: true, force: true }); - } + fs.rmSync(intervalPath, { recursive: true, force: true }); fs.writeFileSync(intervalPath, ['nodeId', 'inferredValue', 'significantFigures', 'sourceLocation'].join(',') + '\n'); for(const result of intervalResults) { fs.appendFileSync(intervalPath, Object.values(result).map(value => '"' + value + '"').join(',') + '\n'); @@ -122,15 +127,16 @@ void async function() { const pentagonResults: InferredValue[] = []; for(const nodeId of pentagonVisitor.getAbstractTrace().keys()) { const value = pentagonVisitor.getAbstractValue(nodeId); - if(isNotUndefined(value)) { + if(value !== undefined) { const node = ast.idMap.get(nodeId); - const location = node ? SourceLocation.fromNode(node) : undefined; pentagonResults.push({ nodeId: nodeId, - inferredValue: value?.toString() ?? 'undefined', - significantFigures: value?.value.interval.significantFigures?.toString() ?? 'unknown', - sourceLocation: isUndefined(location) ? 'unknown' : SourceLocation.getRange(location).slice(0, 4).toString(), + 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', }); } } @@ -138,9 +144,7 @@ void async function() { // Dump Pentagon Results const pentagonPath = path.join(outputDirectory, pentagonResultFile); - if(fs.existsSync(pentagonPath)) { - fs.rmSync(pentagonPath, { recursive: true, force: true }); - } + fs.rmSync(pentagonPath, { recursive: true, force: true }); fs.writeFileSync(pentagonPath, ['nodeId', 'inferredValue', 'significantFigures', 'sourceLocation'].join(',') + '\n'); for(const result of pentagonResults) { fs.appendFileSync(pentagonPath, Object.values(result).map(value => '"' + value + '"').join(',') + '\n'); @@ -153,12 +157,12 @@ void async function() { const functionCalls = dfg.verticesOfType(VertexType.FunctionCall).toArray(); const supportedExpressionFunctionCalls = functionCalls.filter(([_, dfgCall]) => - isNotUndefined(IntervalExpressionSemanticsMapper().find(([id]) => Identifier.matches(id, dfgCall.name))) || - isNotUndefined(PentagonExpressionSemanticsMapper.find(([id]) => Identifier.matches(id, dfgCall.name))) + IntervalExpressionSemanticsMapper().find(([id]) => Identifier.matches(id, dfgCall.name)) !== undefined || + PentagonExpressionSemanticsMapper.find(([id]) => Identifier.matches(id, dfgCall.name)) !== undefined ); const supportedConditionFunctionCalls = functionCalls.filter(([_, dfgCall]) => - isNotUndefined(IntervalSemanticsMaper().find(([id]) => Identifier.matches(id, dfgCall.name))) || - isNotUndefined(UpperBoundsSemanticsMapper().find(([id]) => Identifier.matches(id, dfgCall.name))) || + 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]) => @@ -182,6 +186,9 @@ void async function() { numOfConditions: conditions.length, metadataGatheringInMs: metadataEnd - metadataStart, baselineInMs: baselineEnd - baselineStart, + astInMs: dfgStart - astStart, + dfgInMs: cfgStart - dfgStart, + cfgInMs: cfgEnd - cfgStart, intervalAnalysisInMs: intervalEnd - intervalStart, intervalResultGatheringInMs: intervalResultEnd - intervalResultStart, pentagonAnalysisInMs: pentagonEnd - pentagonStart, @@ -190,9 +197,7 @@ void async function() { // Dump File and Runtime Metadata const fileMetadataPath = path.join(outputDirectory, metadataOutputFile); - if(fs.existsSync(fileMetadataPath)) { - fs.rmSync(fileMetadataPath, { recursive: true, force: true }); - } + fs.rmSync(fileMetadataPath, { recursive: true, force: true }); fs.writeFileSync(fileMetadataPath, Object.keys(fileMetadata).join(',') + '\n' + Object.values(fileMetadata).map(value => '"' + value + '"').join(',') + '\n'); }(); \ No newline at end of file From 8f07e16ad2f5f98cbdbd0a9d1422340a8750d744 Mon Sep 17 00:00:00 2001 From: Henry Date: Mon, 8 Jun 2026 15:19:35 +0200 Subject: [PATCH 05/13] feat: added more metadata --- src/abstract-interpretation/benchmarking.ts | 56 +++++++++++++++------ 1 file changed, 40 insertions(+), 16 deletions(-) diff --git a/src/abstract-interpretation/benchmarking.ts b/src/abstract-interpretation/benchmarking.ts index 9bf19af95d1..221d9d62fab 100644 --- a/src/abstract-interpretation/benchmarking.ts +++ b/src/abstract-interpretation/benchmarking.ts @@ -15,6 +15,9 @@ import { SourceRange } from '../util/range'; import { NumericPentagonInferenceVisitor } from './pentagon/numeric-pentagon-inference'; import path from 'path'; import type { AbsintVisitorConfiguration } from './absint-visitor'; +import { superBigJsonStringify } from '../util/json'; +import { UnsupportedFunctions } from './unsupported-functions'; +import type { LintingResultsSuccess } from '../linter/linter-format'; if(process.argv.length < 4) { console.error('Usage: ts-node src/abstract-interpretation/benchmarking.ts '); @@ -28,15 +31,24 @@ interface FileMetadata { 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; @@ -61,9 +73,9 @@ void async function() { fs.mkdirSync(outputDirectory, { recursive: true }); const fileName = path.basename(filePath); const fileNameWithoutEnding = path.parse(fileName).name; - const metadataOutputFile = fileNameWithoutEnding + '.csv'; - const intervalResultFile = fileNameWithoutEnding + '-interval.csv'; - const pentagonResultFile = fileNameWithoutEnding + '-pentagon.csv'; + const metadataOutputFile = fileNameWithoutEnding + '.json'; + const intervalResultFile = fileNameWithoutEnding + '-interval.json'; + const pentagonResultFile = fileNameWithoutEnding + '-pentagon.json'; const baselineStart = performance.now(); const analyzer = await new FlowrAnalyzerBuilder() @@ -111,10 +123,7 @@ void async function() { // Dump Interval Results const intervalPath = path.join(outputDirectory, intervalResultFile); fs.rmSync(intervalPath, { recursive: true, force: true }); - fs.writeFileSync(intervalPath, ['nodeId', 'inferredValue', 'significantFigures', 'sourceLocation'].join(',') + '\n'); - for(const result of intervalResults) { - fs.appendFileSync(intervalPath, Object.values(result).map(value => '"' + value + '"').join(',') + '\n'); - } + superBigJsonStringify(intervalResults, '\n', (msg) => fs.appendFileSync(intervalPath, msg)); // Run Pentagon Analysis const pentagonVisitor = new NumericPentagonInferenceVisitor(visitorContext); @@ -145,10 +154,7 @@ void async function() { // Dump Pentagon Results const pentagonPath = path.join(outputDirectory, pentagonResultFile); fs.rmSync(pentagonPath, { recursive: true, force: true }); - fs.writeFileSync(pentagonPath, ['nodeId', 'inferredValue', 'significantFigures', 'sourceLocation'].join(',') + '\n'); - for(const result of pentagonResults) { - fs.appendFileSync(pentagonPath, Object.values(result).map(value => '"' + value + '"').join(',') + '\n'); - } + superBigJsonStringify(pentagonResults, '\n', (msg) => fs.appendFileSync(pentagonPath, msg)); // Create File and Runtime Metadata const metadataStart = performance.now(); @@ -163,11 +169,21 @@ void async function() { 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)) + ['&&', '!', '||', '&', '|'].some(id => Identifier.matches(id, dfgCall.name)) ); const conditions = functionCalls.filter(([_, dfgCall]) => - dfgCall.origin.includes(BuiltInProcName.IfThenElse) || dfgCall.origin.includes(BuiltInProcName.WhileLoop) - );//.map(([node, _]) => cfg.graph.ingoingEdges(node)?.keys().toArray()[0]); + 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 = { @@ -175,15 +191,24 @@ void async function() { 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, @@ -198,6 +223,5 @@ void async function() { // Dump File and Runtime Metadata const fileMetadataPath = path.join(outputDirectory, metadataOutputFile); fs.rmSync(fileMetadataPath, { recursive: true, force: true }); - fs.writeFileSync(fileMetadataPath, Object.keys(fileMetadata).join(',') + '\n' + - Object.values(fileMetadata).map(value => '"' + value + '"').join(',') + '\n'); + fs.writeFileSync(fileMetadataPath, JSON.stringify(fileMetadata, null, 2)); }(); \ No newline at end of file From 32caeb00d8f231e200bd1acecbf21d7ce88021ae Mon Sep 17 00:00:00 2001 From: Henry Date: Mon, 8 Jun 2026 16:49:55 +0200 Subject: [PATCH 06/13] feat: added element wise and and or condition semantics --- src/abstract-interpretation/absint-condition-semantics.ts | 2 ++ 1 file changed, 2 insertions(+) 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 { From 4dd63528e7471a5d8f8c04fe544d68cef498d43d Mon Sep 17 00:00:00 2001 From: Henry Date: Tue, 9 Jun 2026 16:43:52 +0200 Subject: [PATCH 07/13] feat: fixed re-assignment problem in absint visitor --- src/abstract-interpretation/absint-visitor.ts | 4 +++- .../interval/inference.test.ts | 15 +++++++++++++++ .../abstract-interpretation/interval/interval.ts | 2 +- 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/src/abstract-interpretation/absint-visitor.ts b/src/abstract-interpretation/absint-visitor.ts index 5128402c6d0..e3be4ee1a5a 100644 --- a/src/abstract-interpretation/absint-visitor.ts +++ b/src/abstract-interpretation/absint-visitor.ts @@ -287,8 +287,10 @@ export abstract class AbstractInterpretationVisitor { '3@x': { domain: IntervalTests.interval(0, 1) }, }); }); + + 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() }, + }); + }); }); 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) { From e4fd7ded8c10d388cbe02c2892df420b5fc1b7aa Mon Sep 17 00:00:00 2001 From: Henry Date: Tue, 9 Jun 2026 17:30:43 +0200 Subject: [PATCH 08/13] refactor: added docstring for introduced method --- .../pentagon/numeric-pentagon-inference.ts | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts b/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts index da4a43fac28..06ff3511fcb 100644 --- a/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts +++ b/src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts @@ -77,11 +77,21 @@ export class NumericPentagonInferenceVisitor extends AbstractInterpretationVisit this.currentState.set(target, targetPentagon); } - // Remove information of all constants on the right hand side + // 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); From f8652045101681ee5998b8579da1c70a3dd2968c Mon Sep 17 00:00:00 2001 From: Henry <72646334+schuler-henry@users.noreply.github.com> Date: Wed, 10 Jun 2026 13:08:25 +0200 Subject: [PATCH 09/13] feat-fix: apply unary op gets two args When using apply or tapply, the unary function gets two reads edges to the other two provided argumetns. Therefore, when unary function is "called" with more than one arg not return bottom but overapproximate to top (undefined) to be sound. --- .../interval/expression-semantics.ts | 4 ++ .../interval/inference.test.ts | 52 ++++++++++++++----- 2 files changed, 42 insertions(+), 14 deletions(-) diff --git a/src/abstract-interpretation/interval/expression-semantics.ts b/src/abstract-interpretation/interval/expression-semantics.ts index 2ed043189b5..68efcb9c19f 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); } diff --git a/test/functionality/abstract-interpretation/interval/inference.test.ts b/test/functionality/abstract-interpretation/interval/inference.test.ts index c3475f79ab6..e198025c883 100644 --- a/test/functionality/abstract-interpretation/interval/inference.test.ts +++ b/test/functionality/abstract-interpretation/interval/inference.test.ts @@ -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,7 +443,7 @@ 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) }], @@ -499,7 +509,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 +532,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 +636,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 +658,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 +680,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 +712,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 +732,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 +764,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 }], @@ -1433,4 +1443,18 @@ describe('Interval Inference', () => { '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 }, + }); + }); }); From 141f0f244231116f50c74f6e068d01c631ef7186 Mon Sep 17 00:00:00 2001 From: Henry <72646334+schuler-henry@users.noreply.github.com> Date: Thu, 11 Jun 2026 23:25:09 +0200 Subject: [PATCH 10/13] feat-fix: fixed semantics for abs and modulo --- .../interval/expression-semantics.ts | 28 ++++++++++------- .../interval/inference.test.ts | 31 ++++++++++--------- 2 files changed, 33 insertions(+), 26 deletions(-) diff --git a/src/abstract-interpretation/interval/expression-semantics.ts b/src/abstract-interpretation/interval/expression-semantics.ts index 68efcb9c19f..2c567f8f7ed 100644 --- a/src/abstract-interpretation/interval/expression-semantics.ts +++ b/src/abstract-interpretation/interval/expression-semantics.ts @@ -513,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]); + } + // 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.top(); + return arg.create([0, -a]); } function intervalModulo(left: IntervalDomain | undefined, right: IntervalDomain | undefined): IntervalDomain | undefined { @@ -536,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 { diff --git a/test/functionality/abstract-interpretation/interval/inference.test.ts b/test/functionality/abstract-interpretation/interval/inference.test.ts index e198025c883..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; @@ -446,7 +446,8 @@ describe('Interval Inference', () => { [['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() }] ]; From 217f36244fcfeaa7b3865c802e552b5db9dec284 Mon Sep 17 00:00:00 2001 From: Henry <72646334+schuler-henry@users.noreply.github.com> Date: Thu, 25 Jun 2026 16:40:05 +0200 Subject: [PATCH 11/13] feat-fix: fixed bug in eval instrumentation and runif semantics --- src/abstract-interpretation/interval/eval.ts | 2 +- src/abstract-interpretation/interval/expression-semantics.ts | 4 ++-- .../flowr-analyzer-project-discovery-plugin.ts | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) 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 2c567f8f7ed..97cf5010947 100644 --- a/src/abstract-interpretation/interval/expression-semantics.ts +++ b/src/abstract-interpretation/interval/expression-semantics.ts @@ -776,8 +776,8 @@ function intervalRunif>(ar } let [lmin, rmin] = [0, 0]; - let [lmax, rmax] = [0, 0]; - // min and max default to 0 if not specified + let [lmax, rmax] = [1, 1]; + // 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/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}. */ From 125a4ec39f6e371ada818a3247e276abc81c59e1 Mon Sep 17 00:00:00 2001 From: Henry <72646334+schuler-henry@users.noreply.github.com> Date: Sun, 28 Jun 2026 13:19:49 +0200 Subject: [PATCH 12/13] feat-fix: adapted runif tests according to bug fix --- .../abstract-interpretation/interval/inference.test.ts | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/functionality/abstract-interpretation/interval/inference.test.ts b/test/functionality/abstract-interpretation/interval/inference.test.ts index 92c6cfd7d69..d2464997c5e 100644 --- a/test/functionality/abstract-interpretation/interval/inference.test.ts +++ b/test/functionality/abstract-interpretation/interval/inference.test.ts @@ -562,7 +562,8 @@ describe('Interval Inference', () => { [['0.2851', '2', '5'], { domain: IntervalTests.top() }], [['n=2, 3'], { domain: IntervalTests.top() }], [['4'], { domain: IntervalTests.top() }], - [['n=1, -3'], { domain: IntervalTests.interval(-3, 0) }], + [['n=1, -3'], { domain: IntervalTests.interval(-3, 1) }], + [['1'], { domain: IntervalTests.interval(0, 1) }], [['1', 'ifelse(c, -4.2, 2.5)', '4'], { domain: IntervalTests.interval(-4.2, 4) }], [['1', 'ifelse(c, -2, 3)', 'ifelse(c, 6, 7)'], { domain: IntervalTests.interval(-2, 7) }], [['1', 'max=3'], { domain: IntervalTests.interval(0, 3) }], From 7025ab358578d772890a01de2bab3948f1c8981a Mon Sep 17 00:00:00 2001 From: Henry <72646334+schuler-henry@users.noreply.github.com> Date: Wed, 1 Jul 2026 23:04:44 +0200 Subject: [PATCH 13/13] feat-fix: revert fix for runif semantics to get version of final eval --- src/abstract-interpretation/interval/expression-semantics.ts | 2 +- .../abstract-interpretation/interval/inference.test.ts | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/abstract-interpretation/interval/expression-semantics.ts b/src/abstract-interpretation/interval/expression-semantics.ts index 97cf5010947..b7054e12111 100644 --- a/src/abstract-interpretation/interval/expression-semantics.ts +++ b/src/abstract-interpretation/interval/expression-semantics.ts @@ -776,7 +776,7 @@ function intervalRunif>(ar } let [lmin, rmin] = [0, 0]; - let [lmax, rmax] = [1, 1]; + let [lmax, rmax] = [0, 0]; // min and max default to 0 and 1 if not specified if(min !== 'unknown') { if(min?.value === Bottom) { diff --git a/test/functionality/abstract-interpretation/interval/inference.test.ts b/test/functionality/abstract-interpretation/interval/inference.test.ts index d2464997c5e..92c6cfd7d69 100644 --- a/test/functionality/abstract-interpretation/interval/inference.test.ts +++ b/test/functionality/abstract-interpretation/interval/inference.test.ts @@ -562,8 +562,7 @@ describe('Interval Inference', () => { [['0.2851', '2', '5'], { domain: IntervalTests.top() }], [['n=2, 3'], { domain: IntervalTests.top() }], [['4'], { domain: IntervalTests.top() }], - [['n=1, -3'], { domain: IntervalTests.interval(-3, 1) }], - [['1'], { domain: IntervalTests.interval(0, 1) }], + [['n=1, -3'], { domain: IntervalTests.interval(-3, 0) }], [['1', 'ifelse(c, -4.2, 2.5)', '4'], { domain: IntervalTests.interval(-4.2, 4) }], [['1', 'ifelse(c, -2, 3)', 'ifelse(c, 6, 7)'], { domain: IntervalTests.interval(-2, 7) }], [['1', 'max=3'], { domain: IntervalTests.interval(0, 3) }],