Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/abstract-interpretation/absint-condition-semantics.ts
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,8 @@ export function createConditionApplier<StateDomain extends AnyStateDomain<AnyAbs
[Identifier.make('('), unaryConditionSemanticsGuard(applyConditionSemantics), unaryConditionSemanticsGuard(applyNegatedConditionSemantics)],
[Identifier.make('||'), binaryConditionSemanticsGuard(orConditionSemantics), binaryConditionSemanticsGuard(negatedOrConditionSemantics)],
[Identifier.make('&&'), binaryConditionSemanticsGuard(andConditionSemantics), binaryConditionSemanticsGuard(negatedAndConditionSemantics)],
[Identifier.make('|'), binaryConditionSemanticsGuard(orConditionSemantics), binaryConditionSemanticsGuard(negatedOrConditionSemantics)],
[Identifier.make('&'), binaryConditionSemanticsGuard(andConditionSemantics), binaryConditionSemanticsGuard(negatedAndConditionSemantics)],
] as const satisfies ConditionSemanticsMapperInfo<StateDomain, Visitor>[];

function orConditionSemantics(leftNodeId: NodeId, rightNodeId: NodeId, state: StateDomain, visitor: Visitor, dfg: DataflowGraph): StateDomain {
Expand Down
4 changes: 3 additions & 1 deletion src/abstract-interpretation/absint-visitor.ts
Original file line number Diff line number Diff line change
Expand Up @@ -287,8 +287,10 @@ export abstract class AbstractInterpretationVisitor<StateDomain extends AnyState

if(value !== undefined) {
this.currentState.set(target, value);
this.trace.set(target, this.currentState);
} else {
this.currentState.remove(target);
}
this.trace.set(target, this.currentState);
}

protected override onReplacementCall({ target }: { call: DataflowGraphVertexFunctionCall, target?: NodeId, source?: NodeId }): void {
Expand Down
227 changes: 227 additions & 0 deletions src/abstract-interpretation/benchmarking.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,227 @@
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 { 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 { 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 <file-to-analyze> <output-folder>');
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() {

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this function would be more readable if you split parts of it into separate functions :)

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()
Comment thread
schuler-henry marked this conversation as resolved.
.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,
Comment thread
schuler-henry marked this conversation as resolved.
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,
Comment thread
schuler-henry marked this conversation as resolved.
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);

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

if you filter on the ast type you have to be more careful wrt. symbols that resolve to numeric constants (which you miss this way), like NA etc. or pi

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What woud be ur suggested solution?

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you could resolve the value with alias tracking and then check on the unpacked value in case of symbols etc. but generally I'd argue this is fine 1) you do not support pi etc. yourself right now 2) the other counts are very low 3) you do not care about NA(integer) do you?

It was more a comment of something that should be noted wrt. statements made on the result.

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay 😄


const functionCalls = dfg.verticesOfType(VertexType.FunctionCall).toArray();
Comment thread
schuler-henry marked this conversation as resolved.
const supportedExpressionFunctionCalls = functionCalls.filter(([_, dfgCall]) =>

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe it would also be interesting to filter these supported function calls for those calls for which you inferred anything?

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();

Comment thread
schuler-henry marked this conversation as resolved.
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,
Comment thread
schuler-henry marked this conversation as resolved.
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,
Comment thread
schuler-henry marked this conversation as resolved.
baselineInMs: baselineEnd - baselineStart,
astInMs: dfgStart - astStart,
dfgInMs: cfgStart - dfgStart,
cfgInMs: cfgEnd - cfgStart,
intervalAnalysisInMs: intervalEnd - intervalStart,
intervalResultGatheringInMs: intervalResultEnd - intervalResultStart,
Comment thread
schuler-henry marked this conversation as resolved.
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));
}();

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, for comprehensibility, giving this function a name (e.g. main or so) and calling it by name would be better

2 changes: 1 addition & 1 deletion src/abstract-interpretation/interval/eval.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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", ' +
Expand Down
34 changes: 22 additions & 12 deletions src/abstract-interpretation/interval/expression-semantics.ts
Original file line number Diff line number Diff line change
Expand Up @@ -194,6 +194,10 @@ function unaryExprFnSemantics<StateDomain extends AnyStateDomain<AnyAbstractDoma
return (args: readonly FunctionArgument[], visitor: IntervalExpressionSemanticsVisitor<StateDomain>, 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);
}

Expand Down Expand Up @@ -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 {
Expand All @@ -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<StateDomain extends AnyStateDomain<AnyAbstractDomain>>(args: readonly FunctionArgument[], visitor: IntervalExpressionSemanticsVisitor<StateDomain>, significantFigures: number | undefined): IntervalDomain | undefined {
Expand Down Expand Up @@ -767,7 +777,7 @@ function intervalRunif<StateDomain extends AnyStateDomain<AnyAbstractDomain>>(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();
Expand Down
Loading