Skip to content

Commit 87c3bcf

Browse files
schuler-henryschuler-henry
committed
refactor: updated naming, assured condition semantics on state copy
1 parent f9bc0e9 commit 87c3bcf

File tree

3 files changed

+80
-90
lines changed

3 files changed

+80
-90
lines changed

‎src/abstract-interpretation/absint-visitor.ts‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ import { EmptyArgument } from '../r-bridge/lang-4.x/ast/model/nodes/r-function-c
1616
import type { NormalizedAst, ParentInformation } from '../r-bridge/lang-4.x/ast/model/processing/decorate';
1717
import type { NodeId } from '../r-bridge/lang-4.x/ast/model/processing/node-id';
1818
import { RType } from '../r-bridge/lang-4.x/ast/model/type';
19-
import { guard, isNotUndefined } from '../util/assert';
19+
import { guard, isNotUndefined, isUndefined } from '../util/assert';
2020
import { AbstractDomain, type AnyAbstractDomain } from './domains/abstract-domain';
2121
import type { StateAbstractDomain } from './domains/state-abstract-domain';
2222
import { MutableStateAbstractDomain } from './domains/state-abstract-domain';
@@ -321,15 +321,17 @@ export abstract class AbstractInterpretationVisitor<Domain extends AnyAbstractDo
321321
protected getPredecessorDomains(vertex: CfgVertex): MutableStateAbstractDomain<Domain>[] {
322322
return this.getPredecessorNodes(CfgVertex.getId(vertex))
323323
.map(pred => {
324+
const predState = this.trace.get(pred.id);
324325
const cfdEdge = pred.edges.find(CfgEdge.isControlDependency);
325326
if(isNotUndefined(cfdEdge)) {
326327
const branchType = CfgEdge.getWhen(cfdEdge);
327328
if(isNotUndefined(branchType)) {
328-
// Apply Condition Semantics
329-
return this.applyConditionSemantics(pred.id, branchType === RTrue);
329+
// Apply Condition Semantics to copy of predecessor state, as we do not want to modify the trace
330+
const copiedState = isUndefined(predState) ? undefined : predState.create(predState.value);
331+
return this.applyConditionSemantics(copiedState, pred.id, branchType === RTrue);
330332
}
331333
}
332-
return this.trace.get(pred.id);
334+
return predState;
333335
}).filter(isNotUndefined);
334336
}
335337

@@ -383,8 +385,8 @@ export abstract class AbstractInterpretationVisitor<Domain extends AnyAbstractDo
383385
return (this.visited.get(CfgVertex.getId(wideningPoint)) ?? 0) >= this.config.ctx.config.abstractInterpretation.wideningThreshold;
384386
}
385387

386-
protected applyConditionSemantics(conditionNodeId: NodeId, _trueBranch: boolean): MutableStateAbstractDomain<Domain> | undefined {
387-
return this.trace.get(conditionNodeId) ?? this._currentState.bottom();
388+
protected applyConditionSemantics(state: MutableStateAbstractDomain<Domain> | undefined, _conditionNodeId: NodeId, _trueBranch: boolean): MutableStateAbstractDomain<Domain> | undefined {
389+
return state;
388390
}
389391

390392
protected abstract getBottomValue(): Domain;

‎src/abstract-interpretation/interval/condition-semantics.ts‎

Lines changed: 69 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -14,34 +14,34 @@ import { FloatingPointComparison } from '../../util/floating-point';
1414
const IntervalConditionSemanticsMapper = [
1515
[Identifier.make('!'), unaryOpSemantics(applyNegatedIntervalConditionSemantics), unaryOpSemantics(applyIntervalConditionSemantics)],
1616
[Identifier.make('('), unaryOpSemantics(applyIntervalConditionSemantics), unaryOpSemantics(applyNegatedIntervalConditionSemantics)],
17-
[Identifier.make('=='), binaryOpSemantics(defaultEqualsOp), binaryOpSemantics(defaultNotEqualsOp)],
18-
[Identifier.make('!='), binaryOpSemantics(defaultNotEqualsOp), binaryOpSemantics(defaultEqualsOp)],
19-
[Identifier.make('>'), binaryOpSemantics(defaultGreaterOp), binaryOpSemantics(defaultLessEqualOp)],
20-
[Identifier.make('>='), binaryOpSemantics(defaultGreaterEqualOp), binaryOpSemantics(defaultLessOp)],
21-
[Identifier.make('<'), binaryOpSemantics(defaultLessOp), binaryOpSemantics(defaultGreaterEqualOp)],
22-
[Identifier.make('<='), binaryOpSemantics(defaultLessEqualOp), binaryOpSemantics(defaultGreaterOp)],
23-
[Identifier.make('is.na'), unaryOpSemantics(defaultIsNaFn), unaryOpSemantics(defaultNegatedIsNaFn)]
17+
[Identifier.make('=='), binaryOpSemantics(intervalEqualsOp), binaryOpSemantics(intervalNotEqualsOp)],
18+
[Identifier.make('!='), binaryOpSemantics(intervalNotEqualsOp), binaryOpSemantics(intervalEqualsOp)],
19+
[Identifier.make('>'), binaryOpSemantics(intervalGreaterOp), binaryOpSemantics(intervalLessEqualOp)],
20+
[Identifier.make('>='), binaryOpSemantics(intervalGreaterEqualOp), binaryOpSemantics(intervalLessOp)],
21+
[Identifier.make('<'), binaryOpSemantics(intervalLessOp), binaryOpSemantics(intervalGreaterEqualOp)],
22+
[Identifier.make('<='), binaryOpSemantics(intervalLessEqualOp), binaryOpSemantics(intervalGreaterOp)],
23+
[Identifier.make('is.na'), unaryOpSemantics(intervalIsNaFn), unaryOpSemantics(intervalNegatedIsNaFn)]
2424
] as const satisfies IntervalConditionSemanticsMapperInfo[];
2525

2626
type IntervalConditionSemanticsMapperInfo = [identifier: Identifier, semantics: NAryFnSemantics, negatedSemantics: NAryFnSemantics];
2727

28-
type UnaryOpSemantics = (argNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => MutableStateAbstractDomain<IntervalDomain> | undefined;
28+
type UnaryOpSemantics = (argNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => MutableStateAbstractDomain<IntervalDomain> | undefined;
2929

30-
type BinaryOpSemantics = (leftNodeId: NodeId, rightNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => MutableStateAbstractDomain<IntervalDomain> | undefined;
30+
type BinaryOpSemantics = (leftNodeId: NodeId, rightNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => MutableStateAbstractDomain<IntervalDomain> | undefined;
3131

32-
type NAryFnSemantics = (argNodeIds: readonly (NodeId | undefined)[], currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => MutableStateAbstractDomain<IntervalDomain> | undefined;
32+
type NAryFnSemantics = (argNodeIds: readonly (NodeId | undefined)[], state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => MutableStateAbstractDomain<IntervalDomain> | undefined;
3333

3434
/**
3535
* Applies the abstract condition semantics of the provided function with respect to the interval domain to the provided args.
3636
* @param argNodeId - The node id representing the condition to which the semantics should be applied.
37-
* @param currentState - The current state before applying the semantics, which can be used to determine the resulting state after applying the semantics.
37+
* @param state - The state before applying the semantics, which can be used to determine the resulting state after applying the semantics.
3838
* @param visitor - The numeric inference visitor performing the analysis used to resolve argument intervals.
3939
* @param dfg - The dataflow graph containing the vertex and its arguments.
4040
* @returns The filtered state after applying the semantics.
4141
*/
42-
export function applyIntervalConditionSemantics(argNodeId: NodeId | undefined, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph): MutableStateAbstractDomain<IntervalDomain> | undefined {
42+
export function applyIntervalConditionSemantics(argNodeId: NodeId | undefined, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph): MutableStateAbstractDomain<IntervalDomain> | undefined {
4343
if(isUndefined(argNodeId)) {
44-
return currentState;
44+
return state;
4545
}
4646

4747
const vertex = dfg.getVertex(argNodeId);
@@ -50,7 +50,7 @@ export function applyIntervalConditionSemantics(argNodeId: NodeId | undefined, c
5050

5151
if(isNotUndefined(match)) {
5252
const [_, semantics] = match;
53-
return semantics(vertex.args.map(FunctionArgument.getReference), currentState, visitor, dfg);
53+
return semantics(vertex.args.map(FunctionArgument.getReference), state, visitor, dfg);
5454
}
5555
}
5656

@@ -63,30 +63,26 @@ export function applyIntervalConditionSemantics(argNodeId: NodeId | undefined, c
6363
// evaluating an expression and evaluating a condition, we can just apply the semantics for evaluating an expression
6464
// in this case.
6565
if(argState?.isValue() && argState.value[0] == 0 && argState.value[1] == 0) {
66-
// Map every variable in state to bottom (fix until state-domain rework)
67-
if(isNotUndefined(currentState)) {
68-
// for(const entry of currentState.value.entries()) {
69-
// currentState.set(entry[0], entry[1].bottom());
70-
// }
71-
return currentState.bottom();
66+
if(isNotUndefined(state)) {
67+
return state.bottom();
7268
}
7369
return new MutableStateAbstractDomain(new Map(), true);
7470
}
7571

76-
return currentState;
72+
return state;
7773
}
7874

7975
/**
8076
* Applies the negated abstract condition semantics of the provided function with respect to the interval domain to the provided args.
8177
* @param argNodeId - The node id representing the condition to which the negated semantics should be applied.
82-
* @param currentState - The current state before applying the semantics, which can be used to determine the resulting state after applying the semantics.
78+
* @param state - The state before applying the semantics, which can be used to determine the resulting state after applying the semantics.
8379
* @param visitor - The numeric inference visitor performing the analysis used to resolve argument intervals.
8480
* @param dfg - The dataflow graph containing the vertex and its arguments.
8581
* @returns The filtered state after applying the negated semantics.
8682
*/
87-
export function applyNegatedIntervalConditionSemantics(argNodeId: NodeId | undefined, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph): MutableStateAbstractDomain<IntervalDomain> | undefined {
83+
export function applyNegatedIntervalConditionSemantics(argNodeId: NodeId | undefined, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph): MutableStateAbstractDomain<IntervalDomain> | undefined {
8884
if(isUndefined(argNodeId)) {
89-
return currentState;
85+
return state;
9086
}
9187

9288
const vertex = dfg.getVertex(argNodeId);
@@ -95,7 +91,7 @@ export function applyNegatedIntervalConditionSemantics(argNodeId: NodeId | undef
9591

9692
if(isNotUndefined(match)) {
9793
const [, , negatedSemantics] = match;
98-
return negatedSemantics(vertex.args.map(FunctionArgument.getReference), currentState, visitor, dfg);
94+
return negatedSemantics(vertex.args.map(FunctionArgument.getReference), state, visitor, dfg);
9995
}
10096
}
10197

@@ -108,94 +104,90 @@ export function applyNegatedIntervalConditionSemantics(argNodeId: NodeId | undef
108104
// evaluating a negated expression and evaluating a negated condition, we can just apply the semantics for
109105
// evaluating a negated expression in this case.
110106
if(argState?.isValue() && (0 < argState.value[0] || argState.value[1] < 0)) {
111-
// (fix until state-domain rework)
112-
if(isNotUndefined(currentState)) {
113-
// for(const entry of currentState.value.entries()) {
114-
// currentState.set(entry[0], entry[1].bottom());
115-
// }
116-
return currentState.bottom();
107+
if(isNotUndefined(state)) {
108+
return state.bottom();
117109
}
118110
return new MutableStateAbstractDomain(new Map(), true);
119111
}
120112

121-
return currentState;
113+
return state;
122114
}
123115

124116
function unaryOpSemantics(unaryOperatorSemantics: UnaryOpSemantics): NAryFnSemantics {
125-
return (argNodeIds: readonly (NodeId | undefined)[], currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => {
117+
return (argNodeIds: readonly (NodeId | undefined)[], state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => {
126118
if(argNodeIds.length !== 1 || isUndefined(argNodeIds[0])) {
127-
return currentState;
119+
return state;
128120
}
129-
return unaryOperatorSemantics(argNodeIds[0], currentState, visitor, dfg);
121+
return unaryOperatorSemantics(argNodeIds[0], state, visitor, dfg);
130122
};
131123
}
132124

133125
function binaryOpSemantics(binaryOperatorSemantics: BinaryOpSemantics): NAryFnSemantics {
134-
return (argNodeIds: readonly (NodeId | undefined)[], currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => {
126+
return (argNodeIds: readonly (NodeId | undefined)[], state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor, dfg: DataflowGraph) => {
135127
if(argNodeIds.length !== 2 || isUndefined(argNodeIds[0]) || isUndefined(argNodeIds[1])) {
136-
return currentState;
128+
return state;
137129
}
138130

139-
return binaryOperatorSemantics(argNodeIds[0], argNodeIds[1], currentState, visitor, dfg);
131+
return binaryOperatorSemantics(argNodeIds[0], argNodeIds[1], state, visitor, dfg);
140132
};
141133
}
142134

143-
function defaultEqualsOp(leftNodeId: NodeId, rightNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
144-
const leftValue = visitor.getAbstractValue(leftNodeId, currentState);
145-
const rightValue = visitor.getAbstractValue(rightNodeId, currentState);
135+
function intervalEqualsOp(leftNodeId: NodeId, rightNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
136+
const leftValue = visitor.getAbstractValue(leftNodeId, state);
137+
const rightValue = visitor.getAbstractValue(rightNodeId, state);
146138

147139
const meet = AbstractDomain.meetAll([leftValue, rightValue].filter(isNotUndefined));
148140

149141
if(meet.isBottom()) {
150-
if(isNotUndefined(currentState)) {
151-
return currentState.bottom();
142+
if(isNotUndefined(state)) {
143+
return state.bottom();
152144
}
153145
return new MutableStateAbstractDomain(new Map(), true);
154146
}
155147

156-
if(isUndefined(currentState)) {
157-
currentState = new MutableStateAbstractDomain(new Map());
148+
if(isUndefined(state)) {
149+
state = new MutableStateAbstractDomain(new Map());
158150
}
159151

160152
visitor.getVariableOrigins(leftNodeId).forEach(originNodeId => {
161-
currentState.set(originNodeId, meet);
153+
state.set(originNodeId, meet);
162154
});
163155
visitor.getVariableOrigins(rightNodeId).forEach(originNodeId => {
164-
currentState.set(originNodeId, meet);
156+
state.set(originNodeId, meet);
165157
});
166158

167-
return currentState;
159+
return state;
168160
}
169161

170-
function defaultNotEqualsOp(leftNodeId: NodeId, rightNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor): MutableStateAbstractDomain<IntervalDomain> | undefined {
171-
const leftValue = visitor.getAbstractValue(leftNodeId, currentState);
172-
const rightValue = visitor.getAbstractValue(rightNodeId, currentState);
162+
function intervalNotEqualsOp(leftNodeId: NodeId, rightNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor): MutableStateAbstractDomain<IntervalDomain> | undefined {
163+
const leftValue = visitor.getAbstractValue(leftNodeId, state);
164+
const rightValue = visitor.getAbstractValue(rightNodeId, state);
173165

174166
if(isNotUndefined(leftValue) && leftValue.isValue() && isNotUndefined(rightValue) && rightValue.isValue()) {
175167
const [a, b] = leftValue.value;
176168
const [c, d] = rightValue.value;
177169

178170
if(a == b && c == d && leftValue?.equals(rightValue)) {
179-
if(isNotUndefined(currentState)) {
180-
return currentState.bottom();
171+
if(isNotUndefined(state)) {
172+
return state.bottom();
181173
}
182174
return new MutableStateAbstractDomain(new Map(), true);
183175
}
184176
}
185177

186-
return currentState;
178+
return state;
187179
}
188180

189-
function defaultGreaterOp(leftNodeId: NodeId, rightNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
190-
if(isUndefined(currentState)) {
191-
return currentState;
181+
function intervalGreaterOp(leftNodeId: NodeId, rightNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
182+
if(isUndefined(state)) {
183+
return state;
192184
}
193185

194-
const leftValue = visitor.getAbstractValue(leftNodeId, currentState);
195-
const rightValue = visitor.getAbstractValue(rightNodeId, currentState);
186+
const leftValue = visitor.getAbstractValue(leftNodeId, state);
187+
const rightValue = visitor.getAbstractValue(rightNodeId, state);
196188

197189
if(isUndefined(leftValue) || isUndefined(rightValue)) {
198-
return currentState;
190+
return state;
199191
}
200192

201193
if(leftValue.isValue() && rightValue.isValue()) {
@@ -205,24 +197,24 @@ function defaultGreaterOp(leftNodeId: NodeId, rightNodeId: NodeId, currentState:
205197
if(c < b || FloatingPointComparison.isNearlyLess(c, b, leftValue.significantFigures) != Ternary.Never) {
206198
const maxAC = a < c ? c : a;
207199
visitor.getVariableOrigins(leftNodeId).forEach(originNodeId => {
208-
currentState.set(originNodeId, leftValue.create([maxAC, b]));
200+
state.set(originNodeId, leftValue.create([maxAC, b]));
209201
});
210202
const minBD = b < d ? b : d;
211203
visitor.getVariableOrigins(rightNodeId).forEach(originNodeId => {
212-
currentState.set(originNodeId, rightValue.create([c, minBD]));
204+
state.set(originNodeId, rightValue.create([c, minBD]));
213205
});
214-
return currentState;
206+
return state;
215207
}
216208
}
217209

218-
return currentState.bottom();
210+
return state.bottom();
219211
}
220212

221-
function defaultLessOp(leftNodeId: NodeId, rightNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
222-
return defaultGreaterOp(rightNodeId, leftNodeId, currentState, visitor);
213+
function intervalLessOp(leftNodeId: NodeId, rightNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
214+
return intervalGreaterOp(rightNodeId, leftNodeId, state, visitor);
223215
}
224216

225-
function defaultGreaterEqualOp(leftNodeId: NodeId, rightNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
217+
function intervalGreaterEqualOp(leftNodeId: NodeId, rightNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
226218
if(isUndefined(currentState)) {
227219
return currentState;
228220
}
@@ -254,24 +246,24 @@ function defaultGreaterEqualOp(leftNodeId: NodeId, rightNodeId: NodeId, currentS
254246
return currentState.bottom();
255247
}
256248

257-
function defaultLessEqualOp(leftNodeId: NodeId, rightNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
258-
return defaultGreaterEqualOp(rightNodeId, leftNodeId, currentState, visitor);
249+
function intervalLessEqualOp(leftNodeId: NodeId, rightNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
250+
return intervalGreaterEqualOp(rightNodeId, leftNodeId, state, visitor);
259251
}
260252

261-
function defaultIsNaFn(argNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
262-
if(isUndefined(currentState)) {
263-
return currentState;
253+
function intervalIsNaFn(argNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined, visitor: NumericInferenceVisitor) {
254+
if(isUndefined(state)) {
255+
return state;
264256
}
265257

266-
const argValue = visitor.getAbstractValue(argNodeId, currentState);
258+
const argValue = visitor.getAbstractValue(argNodeId, state);
267259

268260
if(isUndefined(argValue)) {
269-
return currentState;
261+
return state;
270262
}
271263

272-
return currentState.bottom();
264+
return state.bottom();
273265
}
274266

275-
function defaultNegatedIsNaFn(argNodeId: NodeId, currentState: MutableStateAbstractDomain<IntervalDomain> | undefined) {
276-
return currentState;
267+
function intervalNegatedIsNaFn(argNodeId: NodeId, state: MutableStateAbstractDomain<IntervalDomain> | undefined) {
268+
return state;
277269
}

0 commit comments

Comments
 (0)