-
Notifications
You must be signed in to change notification settings - Fork 7
Basic Structure for the Abstract Interpretation #397
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
EagleoutIce
merged 51 commits into
main
from
378-basic-structure-for-the-abstract-interpretation
Jan 26, 2024
Merged
Changes from all commits
Commits
Show all changes
51 commits
Select commit
Hold shift + click to select a range
8759589
feat: added an abstract interpretation (ai) step
LukasPietzschmann 7c25938
feat-fix: forgot to add processor.ts
LukasPietzschmann a96f623
feat-fix: pass the correct arguments to the ai and slicing step
LukasPietzschmann 954b547
feat: added the normalized ast as a parameter to the ai step
LukasPietzschmann 87e328d
feat-fix: remove the explicitly included normalzsation step
LukasPietzschmann c3f0a99
refactor: remove normalized ast parameter from abstract interpretatio…
EagleoutIce 2b1020c
git: Merge tag 'v1.2.0' into 378-basic-structure-for-the-abstract-int…
LukasPietzschmann 91c029f
feat: added back the ast as an input for the ai processor
LukasPietzschmann 2c6a555
Merge branch 'main' into 378-basic-structure-for-the-abstract-interpr…
LukasPietzschmann 38077e8
feat, wip: borderline execution trace visitor for the cfg
EagleoutIce c75224d
feat, wip: only visit exit nodes after we have visited all of its suc…
EagleoutIce 6739f2e
feat, wip: attributing vertex type in cfg
EagleoutIce 71c4e2d
test-fix: adapting tests to new cfg vertex types
EagleoutIce 5023dba
lint-fix: remove unused reference
EagleoutIce 35b9620
Merge branch 'main' into 378-basic-structure-for-the-abstract-interpr…
EagleoutIce 59561af
feat: Added basic structure for traversing the cfg
LukasPietzschmann 1982f2e
feat: Added an interface specifying an interval
LukasPietzschmann 934499a
feat: Narrowed down the node type of assignments
LukasPietzschmann 14401a9
refactor: Intervals -> Domain
LukasPietzschmann 302d19a
feat: If a dfg node reads from multiple sources, unify their domains
LukasPietzschmann 2aab44a
refactor: fixed function names
LukasPietzschmann 20fe13b
refactor: Refactored the unification of domains
LukasPietzschmann e397ecf
refactor: Domain is now a real class
LukasPietzschmann 2929cae
refactor: Consistent naming scheme and no more .forEach
LukasPietzschmann 7db9f76
feat-fix: don't use members before setting them lol
LukasPietzschmann 7735735
feat: Exported functions, classes and interfaces
LukasPietzschmann aec40b9
test: Added AI test
LukasPietzschmann bfa5dca
feat-fix: Added additional flag for comparing intervals
LukasPietzschmann cc3bb71
refactor: replaced new Array() by the literal syntax []
LukasPietzschmann 76a8242
test: Added tests for the unification of domains
LukasPietzschmann c3b19e4
refactor: Don't inherit Domain from a Set, make the intervals a member
LukasPietzschmann b316241
feat: Added interface AINode and a place to store them
LukasPietzschmann 5002fdd
refactor: More sensible types and names
LukasPietzschmann 6c8dd13
refactor: Merged BinOp and Assignment
LukasPietzschmann 621ffef
feat: Added function for adding two domains
LukasPietzschmann 1f439b0
refactor: Fixed formatting
LukasPietzschmann 25ea6ec
feat: Implemented more handling code for bin ops
LukasPietzschmann b0db502
fix: Don't create Intervals using the literal syntax
LukasPietzschmann f187d45
fix: Typo
LukasPietzschmann 3a73901
feat: We can now subtract one domain from another
LukasPietzschmann 9b5e98e
refactor: Split into multiple files
LukasPietzschmann 5ce85d9
feat: Added unifyIntervals as a helper
LukasPietzschmann 5d57eef
feat: Check for interval overlaps, if an interval is added to a domain
LukasPietzschmann 775863f
refactor: Code cleanup
LukasPietzschmann 2d31117
refactor: Use the flowR logger
LukasPietzschmann e7a4e35
refactor: Add static factory methods to the Domain
LukasPietzschmann c57732e
refactor: Removed TODOs referencing more tests
LukasPietzschmann d9462d7
refactor: De-globalized the nodeMap
LukasPietzschmann af963b7
refactor: Replaced a guard with a warning
LukasPietzschmann 7c68256
fix: Temporarily remove the call to `runAbstractInterpretation`
LukasPietzschmann dcf9eae
Merge branch 'main' into 378-basic-structure-for-the-abstract-interpr…
EagleoutIce File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,169 @@ | ||
import {assertUnreachable, guard} from '../util/assert' | ||
|
||
interface IntervalBound { | ||
readonly value: number, | ||
readonly inclusive: boolean | ||
} | ||
|
||
export class Interval { | ||
constructor(readonly min: IntervalBound, readonly max: IntervalBound) { | ||
guard(min.value <= max.value, () => `The interval ${this.toString()} has a minimum that is greater than its maximum`) | ||
guard(min.value !== max.value || (min.inclusive === max.inclusive), `The bound ${min.value} cannot be in- and exclusive at the same time`) | ||
} | ||
|
||
toString(): string { | ||
return `${this.min.inclusive ? '[' : '('}${this.min.value}, ${this.max.value}${this.max.inclusive ? ']' : ')'}` | ||
} | ||
} | ||
|
||
export class Domain { | ||
private readonly _intervals: Set<Interval> | ||
|
||
private constructor(intervals: Interval[] = []) { | ||
this._intervals = new Set(unifyOverlappingIntervals(intervals)) | ||
} | ||
|
||
static bottom(): Domain { | ||
return new Domain() | ||
} | ||
|
||
static fromIntervals(intervals: Interval[] | Set<Interval>): Domain { | ||
return new Domain(Array.from(intervals)) | ||
} | ||
|
||
static fromScalar(n: number): Domain { | ||
return new Domain([new Interval( | ||
{value: n, inclusive: true}, | ||
{value: n, inclusive: true} | ||
)]) | ||
} | ||
|
||
get intervals(): Set<Interval> { | ||
return this._intervals | ||
} | ||
|
||
private set intervals(intervals: Interval[]) { | ||
this._intervals.clear() | ||
for(const interval of intervals) { | ||
this._intervals.add(interval) | ||
} | ||
} | ||
|
||
addInterval(interval: Interval): void { | ||
this.intervals = unifyOverlappingIntervals([...this.intervals, interval]) | ||
} | ||
|
||
toString(): string { | ||
return `{${Array.from(this.intervals).join(', ')}}` | ||
} | ||
} | ||
|
||
const enum CompareType { | ||
/** If qual, the bound that's inclusive is the smaller one */ | ||
Min, | ||
/** If equal, the bound that's inclusive is the greater one */ | ||
Max, | ||
/** Equality is only based on the "raw" values */ | ||
IgnoreInclusivity | ||
} | ||
|
||
function compareIntervals(compareType: CompareType, interval1: IntervalBound, interval2: IntervalBound): number { | ||
const diff = interval1.value - interval2.value | ||
if(diff !== 0 || compareType === CompareType.IgnoreInclusivity) { | ||
return diff | ||
} | ||
switch(compareType) { | ||
case CompareType.Min: | ||
return Number(!interval1.inclusive) - Number(!interval2.inclusive) | ||
case CompareType.Max: | ||
return Number(interval1.inclusive) - Number(interval2.inclusive) | ||
default: | ||
assertUnreachable(compareType) | ||
} | ||
} | ||
|
||
function compareIntervalsByTheirMinimum(interval1: Interval, interval2: Interval): number { | ||
return compareIntervals(CompareType.Min, interval1.min, interval2.min) | ||
} | ||
|
||
function compareIntervalsByTheirMaximum(interval1: Interval, interval2: Interval): number { | ||
return compareIntervals(CompareType.Max, interval1.max, interval2.max) | ||
} | ||
|
||
export function doIntervalsOverlap(interval1: Interval, interval2: Interval): boolean { | ||
const diff1 = compareIntervals(CompareType.IgnoreInclusivity, interval1.max, interval2.min) | ||
const diff2 = compareIntervals(CompareType.IgnoreInclusivity, interval2.max, interval1.min) | ||
|
||
// If one interval ends before the other starts, they don't overlap | ||
if(diff1 < 0 || diff2 < 0) { | ||
return false | ||
} | ||
// If their end and start are equal, they only overlap if both are inclusive | ||
if(diff1 === 0) { | ||
return interval1.max.inclusive && interval2.min.inclusive | ||
} | ||
if(diff2 === 0) { | ||
return interval2.max.inclusive && interval1.min.inclusive | ||
} | ||
|
||
return true | ||
} | ||
|
||
export function unifyDomains(domains: Domain[]): Domain { | ||
const unifiedIntervals = unifyOverlappingIntervals(domains.flatMap(domain => Array.from(domain.intervals))) | ||
return Domain.fromIntervals(unifiedIntervals) | ||
} | ||
|
||
export function unifyOverlappingIntervals(intervals: Interval[]): Interval[] { | ||
if(intervals.length === 0) { | ||
return [] | ||
} | ||
const sortedIntervals = intervals.sort(compareIntervalsByTheirMinimum) | ||
|
||
const unifiedIntervals: Interval[] = [] | ||
let currentInterval = sortedIntervals[0] | ||
for(const nextInterval of sortedIntervals) { | ||
if(doIntervalsOverlap(currentInterval, nextInterval)) { | ||
const intervalWithEarlierStart = compareIntervalsByTheirMinimum(currentInterval, nextInterval) < 0 ? currentInterval : nextInterval | ||
const intervalWithLaterEnd = compareIntervalsByTheirMaximum(currentInterval, nextInterval) > 0 ? currentInterval : nextInterval | ||
currentInterval = new Interval(intervalWithEarlierStart.min, intervalWithLaterEnd.max) | ||
} else { | ||
unifiedIntervals.push(currentInterval) | ||
currentInterval = nextInterval | ||
} | ||
} | ||
unifiedIntervals.push(currentInterval) | ||
return unifiedIntervals | ||
} | ||
|
||
export function addDomains(domain1: Domain, domain2: Domain): Domain { | ||
const intervals = new Set<Interval>() | ||
for(const interval1 of domain1.intervals) { | ||
LukasPietzschmann marked this conversation as resolved.
Show resolved
Hide resolved
|
||
for(const interval2 of domain2.intervals) { | ||
intervals.add(new Interval({ | ||
value: interval1.min.value + interval2.min.value, | ||
inclusive: interval1.min.inclusive && interval2.min.inclusive | ||
}, { | ||
value: interval1.max.value + interval2.max.value, | ||
inclusive: interval1.max.inclusive && interval2.max.inclusive | ||
})) | ||
} | ||
} | ||
return Domain.fromIntervals(intervals) | ||
} | ||
|
||
export function subtractDomains(domain1: Domain, domain2: Domain): Domain { | ||
const intervals = new Set<Interval>() | ||
for(const interval1 of domain1.intervals) { | ||
for(const interval2 of domain2.intervals) { | ||
intervals.add(new Interval({ | ||
value: interval1.min.value - interval2.max.value, | ||
inclusive: interval1.min.inclusive && interval2.max.inclusive | ||
}, { | ||
value: interval1.max.value - interval2.min.value, | ||
inclusive: interval1.max.inclusive && interval2.min.inclusive | ||
})) | ||
} | ||
} | ||
return Domain.fromIntervals(intervals) | ||
} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
import {Handler} from '../handler' | ||
import {aiLogger, AINode} from '../../processor' | ||
import {BinaryOperatorFlavor, ParentInformation, RBinaryOp} from '../../../r-bridge' | ||
import {guard} from '../../../util/assert' | ||
import {operators} from './operators' | ||
|
||
export type BinOpOperators = { | ||
LukasPietzschmann marked this conversation as resolved.
Show resolved
Hide resolved
|
||
[key in BinaryOperatorFlavor]: (lhs: AINode, rhs: AINode, node: RBinaryOp<ParentInformation>) => AINode | ||
} | ||
|
||
export class BinOp implements Handler<AINode> { | ||
lhs: AINode | undefined | ||
rhs: AINode | undefined | ||
|
||
constructor(readonly node: RBinaryOp<ParentInformation>) {} | ||
|
||
getName(): string { | ||
return `Bin Op (${this.node.flavor})` | ||
} | ||
|
||
enter(): void { | ||
aiLogger.trace(`Entered ${this.getName()}`) | ||
} | ||
|
||
exit(): AINode { | ||
aiLogger.trace(`Exited ${this.getName()}`) | ||
guard(this.lhs !== undefined, `No LHS found for assignment ${this.node.info.id}`) | ||
guard(this.rhs !== undefined, `No RHS found for assignment ${this.node.info.id}`) | ||
return operators[this.node.flavor](this.lhs, this.rhs, this.node) | ||
LukasPietzschmann marked this conversation as resolved.
Show resolved
Hide resolved
|
||
} | ||
|
||
next(node: AINode): void { | ||
aiLogger.trace(`${this.getName()} received`) | ||
if(this.lhs === undefined) { | ||
this.lhs = node | ||
} else if(this.rhs === undefined) { | ||
this.rhs = node | ||
} else { | ||
guard(false, `BinOp ${this.node.info.id} already has both LHS and RHS`) | ||
} | ||
} | ||
} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
import {guard} from '../../../util/assert' | ||
import {BinOpOperators} from './binop' | ||
import {addDomains, subtractDomains} from '../../domain' | ||
|
||
export const operators: BinOpOperators = { | ||
'assignment': (lhs, rhs, node) => { | ||
return { | ||
id: lhs.id, | ||
domain: rhs.domain, | ||
astNode: node.lhs, | ||
} | ||
}, | ||
'arithmetic': (lhs, rhs, node) => { | ||
switch(node.operator) { | ||
case '+': | ||
return { | ||
id: lhs.id, | ||
domain: addDomains(lhs.domain, rhs.domain), | ||
astNode: node, | ||
} | ||
case '-': | ||
return { | ||
id: lhs.id, | ||
domain: subtractDomains(lhs.domain, rhs.domain), | ||
astNode: node, | ||
} | ||
default: | ||
guard(false, `Unknown binary operator ${node.operator}`) | ||
} | ||
}, | ||
'logical': () => { | ||
guard(false, 'Not implemented yet') | ||
}, | ||
'model formula': () => { | ||
guard(false, 'Not implemented yet') | ||
}, | ||
'comparison': () => { | ||
guard(false, 'Not implemented yet') | ||
}, | ||
} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
export interface Handler<ValueType> { | ||
getName: () => string, | ||
enter: () => void | ||
exit: () => ValueType | ||
next: (value: ValueType) => void | ||
} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,83 @@ | ||
import {DataflowInformation} from '../dataflow/internal/info' | ||
import {NodeId, NormalizedAst, ParentInformation, RNodeWithParent, RType} from '../r-bridge' | ||
import {CfgVertexType, extractCFG} from '../util/cfg/cfg' | ||
import {visitCfg} from '../util/cfg/visitor' | ||
import {guard} from '../util/assert' | ||
import {DataflowGraphVertexInfo, EdgeType, OutgoingEdges} from '../dataflow' | ||
import {Handler} from './handler/handler' | ||
import {BinOp} from './handler/binop/binop' | ||
import {Domain, unifyDomains} from './domain' | ||
import {log} from '../util/log' | ||
|
||
export const aiLogger = log.getSubLogger({name: 'abstract-interpretation'}) | ||
|
||
export interface AINode { | ||
readonly id: NodeId | ||
readonly domain: Domain | ||
readonly astNode: RNodeWithParent<ParentInformation> | ||
} | ||
|
||
class Stack<ElementType> { | ||
private backingStore: ElementType[] = [] | ||
|
||
size(): number { return this.backingStore.length } | ||
peek(): ElementType | undefined { return this.backingStore[this.size() - 1] } | ||
pop(): ElementType | undefined { return this.backingStore.pop() } | ||
push(item: ElementType): ElementType { | ||
this.backingStore.push(item) | ||
return item | ||
} | ||
} | ||
|
||
function getDomainOfDfgChild(node: NodeId, dfg: DataflowInformation, nodeMap: Map<NodeId, AINode>): Domain { | ||
const dfgNode: [DataflowGraphVertexInfo, OutgoingEdges] | undefined = dfg.graph.get(node) | ||
guard(dfgNode !== undefined, `No DFG-Node found with ID ${node}`) | ||
const [_, children] = dfgNode | ||
const ids = Array.from(children.entries()) | ||
.filter(([_, edge]) => edge.types.has(EdgeType.Reads)) | ||
.map(([id, _]) => id) | ||
const domains: Domain[] = [] | ||
for(const id of ids) { | ||
const domain = nodeMap.get(id)?.domain | ||
guard(domain !== undefined, `No domain found for ID ${id}`) | ||
domains.push(domain) | ||
} | ||
return unifyDomains(domains) | ||
} | ||
|
||
export function runAbstractInterpretation(ast: NormalizedAst, dfg: DataflowInformation): DataflowInformation { | ||
const cfg = extractCFG(ast) | ||
const operationStack = new Stack<Handler<AINode>>() | ||
const nodeMap = new Map<NodeId, AINode>() | ||
visitCfg(cfg, (node, _) => { | ||
const astNode = ast.idMap.get(node.id) | ||
if(astNode?.type === RType.BinaryOp) { | ||
operationStack.push(new BinOp(astNode)).enter() | ||
} else if(astNode?.type === RType.Symbol) { | ||
operationStack.peek()?.next({ | ||
LukasPietzschmann marked this conversation as resolved.
Show resolved
Hide resolved
|
||
id: astNode.info.id, | ||
domain: getDomainOfDfgChild(node.id, dfg, nodeMap), | ||
astNode: astNode, | ||
}) | ||
} else if(astNode?.type === RType.Number){ | ||
const num = astNode.content.num | ||
operationStack.peek()?.next({ | ||
id: astNode.info.id, | ||
domain: Domain.fromScalar(num), | ||
astNode: astNode, | ||
}) | ||
} else if(node.type === CfgVertexType.EndMarker) { | ||
const operation = operationStack.pop() | ||
if(operation === undefined) { | ||
return | ||
} | ||
const operationResult = operation.exit() | ||
guard(!nodeMap.has(operationResult.id), `Domain for ID ${operationResult.id} already exists`) | ||
nodeMap.set(operationResult.id, operationResult) | ||
operationStack.peek()?.next(operationResult) | ||
} else { | ||
aiLogger.warn(`Unknown node type ${node.type}`) | ||
} | ||
}) | ||
return dfg | ||
} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.