[Abstract Domains iii]: Resolve constant aliases

src/config.ts

@@ -7,6 +7,16 @@ import { getParentDirectory } from './util/files';
 import Joi from 'joi';
 import type { BuiltInDefinitions } from './dataflow/environments/built-in-config';
 
+
+export enum VariableResolve {
+	/** Don't resolve constants at all */
+	Disabled = 'disabled',
+	/** Use alias tracking to resolve */
+	Alias = 'alias',
+	/** Only resolve directly assigned builtin constants */
+	Builtin = 'builtin'
+}
+
 export interface FlowrConfigOptions extends MergeableRecord {
 	/**
 	 * Whether source calls should be ignored, causing {@link processSourceCall}'s behavior to be skipped
@@ -29,6 +39,14 @@ export interface FlowrConfigOptions extends MergeableRecord {
 			}
 		}
 	}
+	/** How to resolve constants, constraints, cells, ... */
+	readonly solver: {
+		/**
+		 * How to resolve variables and their values
+		 */
+		readonly variables: VariableResolve
+	}
+
 }
 
 export const defaultConfigOptions: FlowrConfigOptions = {
@@ -41,6 +59,9 @@ export const defaultConfigOptions: FlowrConfigOptions = {
 				definitions:  []
 			}
 		}
+	},
+	solver: {
+		variables: VariableResolve.Alias
 	}
 };
 
@@ -54,7 +75,10 @@ export const flowrConfigFileSchema = Joi.object({
 				definitions:  Joi.array().items(Joi.object()).optional().description('The definitions to load/overwrite.')
 			}).optional().description('Do you want to overwrite (parts) of the builtin definition?')
 		}).optional().description('Semantics regarding the handlings of the environment.')
-	}).description('Configure language semantics and how flowR handles them.')
+	}).description('Configure language semantics and how flowR handles them.'),
+	solver: Joi.object({
+		variables: Joi.string().valid(...Object.values(VariableResolve)).description('How to resolve variables and their values.')
+	}).description('How to resolve constants, constraints, cells, ...')
 }).description('The configuration file format for flowR.');
 
 // we don't load from a config file at all by default unless setConfigFile is called

src/dataflow/environments/identifier.ts

@@ -99,8 +99,12 @@ export interface IdentifierReference {
  */
 interface InGraphIdentifierDefinition extends IdentifierReference {
 	readonly type:      InGraphReferenceType
-	/** The assignment (or whatever, like `assign` function call) node which ultimately defined this identifier */
+	/**
+	 * The assignment node which ultimately defined this identifier
+	 * (the arrow operator for e.g. `x <- 3`, or `assign` call in `assign("x", 3)`)
+	 */
 	readonly definedAt: NodeId
+	readonly value?:    NodeId[]
 }
 
 /**

src/dataflow/environments/resolve-by-name.ts

@@ -2,9 +2,16 @@ import type { IEnvironment, REnvironmentInformation } from './environment';
 import { BuiltInEnvironment } from './environment';
 import { Ternary } from '../../util/logic';
 import type { Identifier, IdentifierDefinition } from './identifier';
-import { isReferenceType , ReferenceType } from './identifier';
+import { isReferenceType, ReferenceType } from './identifier';
 import { happensInEveryBranch } from '../info';
 import type { BuiltInIdentifierConstant } from './built-in';
+import type { NodeId } from '../../r-bridge/lang-4.x/ast/model/processing/node-id';
+import { recoverName } from '../../r-bridge/lang-4.x/ast/model/processing/node-id';
+import { VertexType } from '../graph/vertex';
+import type { DataflowGraph } from '../graph/graph';
+import { getConfig, VariableResolve } from '../../config';
+import { assertUnreachable } from '../../util/assert';
+
 
 const FunctionTargetTypes = ReferenceType.Function | ReferenceType.BuiltInFunction | ReferenceType.Unknown | ReferenceType.Argument | ReferenceType.Parameter;
 const VariableTargetTypes = ReferenceType.Variable | ReferenceType.Parameter | ReferenceType.Argument | ReferenceType.Unknown;
@@ -85,23 +92,125 @@ export function resolvesToBuiltInConstant(name: Identifier | undefined, environm
 	}
 }
 
-export interface ResolveResult<T = unknown> {
-	value: T,
-	from:  ReferenceType
-}
-
-export function resolveToConstants(name: Identifier | undefined, environment: REnvironmentInformation): ResolveResult[] | undefined {
+export function resolveToConstants(name: Identifier | undefined, environment: REnvironmentInformation): unknown[] | undefined {
 	if(name === undefined) {
 		return undefined;
 	}
 
 	const definitions = resolveByName(name, environment, ReferenceType.Constant);
-	if(definitions === undefined) {
+
+	return definitions?.map(def => (def as BuiltInIdentifierConstant).value);
+}
+
+type AliasHandler = (s: NodeId, d: DataflowGraph, e: REnvironmentInformation) => NodeId[] | undefined;
+
+const AliasHandler = {
+	[VertexType.Value]:              (sourceId: NodeId) => [sourceId],
+	[VertexType.Use]:                getUseAlias,
+	[VertexType.FunctionCall]:       () => undefined,
+	[VertexType.FunctionDefinition]: () => undefined,
+	[VertexType.VariableDefinition]: () => undefined
+} as const satisfies Record<VertexType, AliasHandler>;
+
+function getUseAlias(sourceId: NodeId, dataflow: DataflowGraph, environment: REnvironmentInformation): NodeId[] | undefined {
+	const definitions: NodeId[] = [];
+
+	// Source is Symbol -> resolve definitions of symbol
+	const identifier = recoverName(sourceId, dataflow.idMap);
+	if(identifier === undefined) {
+		return undefined;
+	}
+
+	const defs = resolveByName(identifier, environment);
+	if(defs === undefined) {
+		return undefined;
+	}
+
+	for(const def of defs) {
+		// If one definition is not constant (or a variable aliasing a constant)
+		// we can't say for sure what value the source has
+		if(def.type === ReferenceType.Variable) {
+			if(def.value === undefined) {
+				return undefined;
+			}
+			definitions.push(...def.value);
+		} else if(def.type === ReferenceType.Constant || def.type === ReferenceType.BuiltInConstant) {
+			definitions.push(def.nodeId);
+		} else {
+			return undefined;
+		}
+	}
+
+	return definitions;
+}
+
+export function getAliases(sourceIds: readonly NodeId[], dataflow: DataflowGraph, environment: REnvironmentInformation): NodeId[] | undefined {
+	const definitions: Set<NodeId> = new Set<NodeId>();
+
+	for(const sourceId of sourceIds) {
+		const info = dataflow.getVertex(sourceId);
+		if(info === undefined) {
+			return undefined;
+		}
+
+		const defs = AliasHandler[info.tag](sourceId, dataflow, environment);
+		for(const def of defs ?? []) {
+			definitions.add(def);
+		}
+	}
+
+	return [...definitions];
+}
+
+export function resolveToValues(identifier: Identifier | undefined, environment: REnvironmentInformation, graph: DataflowGraph): unknown[] | undefined {
+	if(identifier === undefined) {
+		return undefined;
+	}
+
+	const defs = resolveByName(identifier, environment);
+	if(defs === undefined) {
+		return undefined;
+	}
+
+	const values: unknown[] = [];
+	for(const def of defs) {
+		if(def.type === ReferenceType.BuiltInConstant) {
+			values.push(def.value);
+		} else if(def.type === ReferenceType.BuiltInFunction) {
+			// Tracked in #1207
+		} else if(def.value !== undefined) {
+			/* if there is at least one location for which we have no idea, we have to give up for now! */
+			if(def.value.length === 0) {
+				return undefined;
+			}
+			for(const id of def.value) {
+				const value = graph.idMap?.get(id)?.content;
+				if(value !== undefined) {
+					values.push(value);
+				}
+			}
+		}
+	}
+
+	if(values.length == 0) {
 		return undefined;
 	}
 
-	return definitions.map<ResolveResult>(def => ({
-		value: (def as BuiltInIdentifierConstant).value,
-		from:  def.type
-	}));
+	return values;
+}
+
+/**
+ * Convenience function using the variable resolver as specified within the configuration file
+ * In the future we may want to have this set once at the start of the analysis
+ */
+export function resolveValueOfVariable(identifier: Identifier | undefined, environment: REnvironmentInformation, graph: DataflowGraph): unknown[] | undefined {
+	const resolve = getConfig().solver.variables;
+
+	switch(resolve) {
+		case VariableResolve.Alias: return resolveToValues(identifier, environment, graph);
+		case VariableResolve.Builtin: return resolveToConstants(identifier, environment);
+		case VariableResolve.Disabled: return [];
+		default: assertUnreachable(resolve);
+	}
 }
+

src/dataflow/internal/process/functions/call/built-in/built-in-assignment.ts

@@ -14,7 +14,7 @@ import type { Base, Location, RNode } from '../../../../../../r-bridge/lang-4.x/
 import type { RSymbol } from '../../../../../../r-bridge/lang-4.x/ast/model/nodes/r-symbol';
 import { RType } from '../../../../../../r-bridge/lang-4.x/ast/model/type';
 import type { RFunctionArgument } from '../../../../../../r-bridge/lang-4.x/ast/model/nodes/r-function-call';
-import type { NodeId } from '../../../../../../r-bridge/lang-4.x/ast/model/processing/node-id';
+import { type NodeId } from '../../../../../../r-bridge/lang-4.x/ast/model/processing/node-id';
 import { dataflowLogger } from '../../../../../logger';
 import type {
 	IdentifierDefinition,
@@ -32,6 +32,7 @@ import { EdgeType } from '../../../../../graph/edge';
 import type { ForceArguments } from '../common';
 import type { REnvironmentInformation } from '../../../../../environments/environment';
 import type { DataflowGraph } from '../../../../../graph/graph';
+import { getAliases } from '../../../../../environments/resolve-by-name';
 
 function toReplacementSymbol<OtherInfo>(target: RNodeWithParent<OtherInfo & ParentInformation> & Base<OtherInfo> & Location, prefix: string, superAssignment: boolean): RSymbol<OtherInfo & ParentInformation> {
 	return {
@@ -161,12 +162,16 @@ function extractSourceAndTarget<OtherInfo>(args: readonly RFunctionArgument<Othe
 	return { source, target };
 }
 
-function produceWrittenNodes<OtherInfo>(rootId: NodeId, target: DataflowInformation, referenceType: InGraphReferenceType, data: DataflowProcessorInformation<OtherInfo>, makeMaybe: boolean): IdentifierDefinition[] {
+/**
+ * Promotes the ingoing/unknown references of target (an assignment) to defitions   
+ */
+function produceWrittenNodes<OtherInfo>(rootId: NodeId, target: DataflowInformation, referenceType: InGraphReferenceType, data: DataflowProcessorInformation<OtherInfo>, makeMaybe: boolean, value: NodeId[] | undefined): IdentifierDefinition[] {
 	return [...target.in, ...target.unknownReferences].map(ref => ({
 		...ref,
 		type:                referenceType,
 		definedAt:           rootId,
-		controlDependencies: data.controlDependencies ?? (makeMaybe ? [] : undefined)
+		controlDependencies: data.controlDependencies ?? (makeMaybe ? [] : undefined),
+		value:               value
 	}));
 }
 
@@ -292,7 +297,8 @@ function processAssignmentToSymbol<OtherInfo>({
 }: AssignmentToSymbolParameters<OtherInfo>): DataflowInformation {
 	const referenceType = checkTargetReferenceType(source, sourceArg);
 
-	const writeNodes = produceWrittenNodes(rootId, targetArg, referenceType, data, makeMaybe ?? false);
+	const aliases = getAliases([source.info.id], information.graph, information.environment);
+	const writeNodes = produceWrittenNodes(rootId, targetArg, referenceType, data, makeMaybe ?? false, aliases);
 
 	if(writeNodes.length !== 1 && log.settings.minLevel <= LogLevel.Warn) {
 		log.warn(`Unexpected write number in assignment: ${JSON.stringify(writeNodes)}`);

src/dataflow/internal/process/functions/call/built-in/built-in-if-then-else.ts

@@ -10,7 +10,7 @@ import type { ParentInformation } from '../../../../../../r-bridge/lang-4.x/ast/
 import type { RFunctionArgument } from '../../../../../../r-bridge/lang-4.x/ast/model/nodes/r-function-call';
 import type { NodeId } from '../../../../../../r-bridge/lang-4.x/ast/model/processing/node-id';
 import { dataflowLogger } from '../../../../../logger';
-import { resolveToConstants } from '../../../../../environments/resolve-by-name';
+import { resolveValueOfVariable } from '../../../../../environments/resolve-by-name';
 import { EdgeType } from '../../../../../graph/edge';
 import { appendEnvironment } from '../../../../../environments/append';
 import type { IdentifierReference } from '../../../../../environments/identifier';
@@ -52,9 +52,9 @@ export function processIfThenElse<OtherInfo>(
 
 	// we should defer this to the abstract interpretation
 
-	const definitions = resolveToConstants(condArg?.lexeme, data.environment);
-	const conditionIsAlwaysFalse = definitions?.every(d => d.value === false) ?? false;
-	const conditionIsAlwaysTrue  = definitions?.every(d => d.value === true) ?? false;
+	const values = resolveValueOfVariable(condArg?.lexeme, data.environment, cond.graph);
+	const conditionIsAlwaysFalse = values?.every(d => d === false) ?? false;
+	const conditionIsAlwaysTrue  = values?.every(d => d === true) ?? false;
 
 	if(!conditionIsAlwaysFalse) {
 		then = processDataflowFor(thenArg, data);

src/documentation/print-interface-wiki.ts

@@ -13,7 +13,7 @@ import { DockerName } from './doc-util/doc-docker';
 import { documentReplSession, printReplHelpAsMarkdownTable } from './doc-util/doc-repl';
 import { printDfGraphForCode } from './doc-util/doc-dfg';
 import type { FlowrConfigOptions } from '../config';
-import { flowrConfigFileSchema } from '../config';
+import { flowrConfigFileSchema, VariableResolve } from '../config';
 import { describeSchema } from '../util/schema';
 import { markdownFormatter } from '../util/ansi';
 import { defaultConfigFile } from '../cli/flowr-main-options';
@@ -179,6 +179,7 @@ The following summarizes the configuration options:
 - \`semantics\`: allows to configure the way _flowR_ handles R, although we currently only support \`semantics/environment/overwriteBuiltIns\`. 
   You may use this to overwrite _flowR_'s handling of built-in function and even completely clear the preset definitions shipped with flowR. 
   See [Configure BuiltIn Semantics](#configure-builtin-semantics) for more information.
+- \`solver\`: allows to configure how _flowR_ resolves variables and their values (currently we support: ${Object.values(VariableResolve).map(v => `\`${v}\``).join(', ')}).
 
 So you can configure _flowR_ by adding a file like the following:
 
@@ -198,6 +199,9 @@ ${codeBlock('json', JSON.stringify(
 						]
 					}
 				}
+			},
+			solver: {
+				variables: VariableResolve.Alias
 			}
 		} satisfies FlowrConfigOptions,
 		null, 2))
@@ -245,7 +249,7 @@ _flowR_ can be used as a [module](${FlowrNpmRef}) and offers several main classe
 ### Using the \`${RShell.name}\` to Interact with R
 
 The \`${RShell.name}\` class allows to interface with the \`R\` ecosystem installed on the host system.
-For now there are no (real) alternatives, although we plan on providing more flexible drop-in replacements.
+For now, there are no (real) alternatives, although we plan on providing more flexible drop-in replacements.
 
 > [!IMPORTANT]
 > Each \`${RShell.name}\` controls a new instance of the R interpreter, make sure to call \`${RShell.name}::${shell.close.name}()\` when you’re done.

test/functionality/dataflow/environments/resolve.test.ts

@@ -94,7 +94,7 @@ describe('Resolve', () => {
 				['NA',    null],
 			])("Identifier '%s' should always resolve to %s", (identifier, wantedValue) => {
 				const defs = resolveToConstants(identifier, defaultEnv());
-				const all = defs?.every(d => d.value === wantedValue) ?? false;
+				const all = defs?.every(d => d === wantedValue) ?? false;
 				assert.isTrue(all, 'should be true');
 			});
 
@@ -105,8 +105,8 @@ describe('Resolve', () => {
 				['FALSE', false, defaultEnv().defineInEnv({ name: 'FALSE', nodeId: 0, definedAt: 1, type: ReferenceType.Constant, controlDependencies: [{ id: 42, when: true }] })]
 			])("Identifier '%s' should maybe resolve to %s", (identifier, wantedValue, environment) => {
 				const defs = resolveToConstants(identifier, environment);
-				const some = defs?.some(d => d.value === wantedValue) ?? false;
-				const all = defs?.every(d => d.value === wantedValue) ?? false;
+				const some = defs?.some(d => d === wantedValue) ?? false;
+				const all = defs?.every(d => d === wantedValue) ?? false;
 				assert.isTrue(some, 'some should be True');
 				assert.isFalse(all, 'all should be False');
 			});
@@ -120,7 +120,7 @@ describe('Resolve', () => {
 				['FALSE',     false,     defaultEnv().defineInEnv({ name: 'FALSE', nodeId: 0, definedAt: 1, type: ReferenceType.Constant, controlDependencies: [{ id: 42, when: true }, { id: 42, when: false }] })]
 			])("Identifier '%s' should never resolve to %s", (identifier, wantedValue, environment) => {
 				const defs = resolveToConstants(identifier, environment);
-				const result = defs?.every(p => p.value === wantedValue) ?? false;
+				const result = defs?.every(p => p === wantedValue) ?? false;
 				assert.isFalse(result, 'result should be False');
 			});
 		});

test/functionality/slicing/static-program-slices/alias-tracking.test.ts

@@ -0,0 +1,35 @@
+import { withShell } from '../../_helper/shell';
+import { describe, expect, test } from 'vitest';
+import { PipelineExecutor } from '../../../../src/core/pipeline-executor';
+import { DEFAULT_DATAFLOW_PIPELINE } from '../../../../src/core/steps/pipeline/default-pipelines';
+import { requestFromInput } from '../../../../src/r-bridge/retriever';
+import { resolveToValues } from '../../../../src/dataflow/environments/resolve-by-name';
+import type { Identifier } from '../../../../src/dataflow/environments/identifier';
+import type { RShell } from '../../../../src/r-bridge/shell';
+import { numVal } from '../../_helper/ast-builder';
+
+async function runPipeline(code: string, shell: RShell) {
+	return await new PipelineExecutor(DEFAULT_DATAFLOW_PIPELINE, {
+		shell:   shell,
+		request: requestFromInput(code)
+	}).allRemainingSteps();
+}
+
+describe.sequential('Alias Tracking', withShell(shell => {
+	test.each([
+		['x <- TRUE; print(x);', 'x', [true]],
+		['x <- TRUE; y <- x; print(y);', 'y', [true]],
+		['x <- 42; y <- x; print(y);', 'y', [numVal(42)]],
+		['x <- TRUE; y <- FALSE; z <- x; z <- y; print(z);', 'z', [false]],
+		['x <- TRUE; y <- FALSE; if(x) { y <- TRUE; }; print(y);', 'y', [true]],
+		['x <- TRUE; while(x) { if(runif(1)) { x <- FALSE } }', 'x', [true, false]],
+		['k <- 4; if(u) { x <- 2; } else { x <- 3; }; y <- x; print(y);', 'y', [numVal(2), numVal(3)]],
+		['f <- function(a = u) { if(k) { u <- 1; } else { u <- 2; }; print(a); }; f();', 'a', undefined], // Note: This should result in a in [1,2] in the future
+		['x <- 1; while(x < 10) { if(runif(1)) x <- x + 1 }', 'x', undefined]
+	])('%s should resolve %s to %o', async(code, identifier, expectedValues) => {
+		const result = await runPipeline(code, shell);
+		const values = resolveToValues(identifier as Identifier, result.dataflow.environment, result.dataflow.graph);
+		expect(values).toEqual(expectedValues);
+	});
+}));
+