Skip to content
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

Abstract interpretation staging #825

Draft
wants to merge 72 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
72 commits
Select commit Hold shift + click to select a range
3efc72e
feat-fix: some AINodes had the wrong id
LukasPietzschmann Feb 22, 2024
5b187bd
feat: added conditional handler file
LukasPietzschmann Feb 22, 2024
ec43e10
feat: the cfg now contains entry and exit nodes for expr. lists
LukasPietzschmann Mar 8, 2024
f1c89ef
feat: differentiate between expression and node ID in AINode
LukasPietzschmann Mar 8, 2024
ad57a96
feat: changed how we store a bunch of domains
LukasPietzschmann Mar 28, 2024
08fb172
fixup! feat: changed how we store a bunch of domains
LukasPietzschmann Mar 28, 2024
07ed85a
feat: added exprlist handler
LukasPietzschmann Mar 28, 2024
59bb280
refactor: binOpOperators return a AINodeStore
LukasPietzschmann Mar 28, 2024
a617074
wip: added narrowDomain stub
LukasPietzschmann Mar 28, 2024
9fdd9d0
feat: implemented comparison operators
LukasPietzschmann Mar 28, 2024
cd7171d
feat: the conditiona handler's condition has to be an AINodeStore
LukasPietzschmann Mar 28, 2024
2becfea
feat-fix: fixed two bugs related to intervals
LukasPietzschmann Apr 15, 2024
fd9df2b
wip: implemented most of narrowDomain
LukasPietzschmann Apr 15, 2024
94193c4
refactor: restructured narrowDomain a bit
LukasPietzschmann Apr 16, 2024
04a12d8
feat-fix: fixed overlapIntervals for non overlapping intervals
LukasPietzschmann Apr 16, 2024
6fbe5ab
feat-fix: differentiate between overlapping and touching intervals
LukasPietzschmann Apr 16, 2024
6dd10cb
feat: narrowDomain now handles narrowing to exclusive bounds
LukasPietzschmann Apr 16, 2024
3f0849f
refactor: simplify comparison operator handler
LukasPietzschmann Apr 16, 2024
28f4046
refactor: added comments and renamed push to register
LukasPietzschmann Apr 24, 2024
8a8fa68
feat-fix: added flag to indicate when register should overwrite
LukasPietzschmann Apr 24, 2024
e1e32a5
feat: intervals like [T, T) or (T, T] are considered empty
LukasPietzschmann May 5, 2024
e587d5d
feat: add isBottom method to Domain class
LukasPietzschmann May 5, 2024
d1fde55
feat: added isSingleton method to Interval class
LukasPietzschmann May 5, 2024
f5b821c
feat: added dfg to all handlers
LukasPietzschmann May 7, 2024
c7ec544
feat: conditionals assign the narrowed domain to the correct node
LukasPietzschmann May 7, 2024
9278390
feat: handler::next can now also return new domains
LukasPietzschmann May 7, 2024
2ff9e4c
feat: add domains to the operationStack
LukasPietzschmann May 7, 2024
6b71910
feat: added better control on how to insert AINodes into the store
LukasPietzschmann May 11, 2024
0956802
feat: every handler now owns its domains
LukasPietzschmann May 11, 2024
e4da4c3
refactor: formatting
LukasPietzschmann May 11, 2024
9bfc404
feat: multiple changes; I was too lazy to separate them
LukasPietzschmann May 15, 2024
4dd6450
refactor: swapped Nop with ExprList since they behave identically
LukasPietzschmann May 15, 2024
06d704d
feat: don't throw, if we haven't yet calculated a domain for a dfg child
LukasPietzschmann May 15, 2024
1f6c2ab
feat: comparisons generate additional Domains for the else-case
LukasPietzschmann May 15, 2024
bad230e
feat: the conditional handler now uses the -else domains
LukasPietzschmann May 15, 2024
4e46327
refactor: intervals are now bottom instead of empty
LukasPietzschmann May 15, 2024
7096ff1
feat: added the notion of top domains
LukasPietzschmann May 15, 2024
0cbb41a
feat: comparisons now generate a third domain for the whole expr
LukasPietzschmann May 15, 2024
21348b0
feat: recognize paths that cannot be taken in conditionals
LukasPietzschmann May 15, 2024
de339e4
feat-fix: add comparison domains to conditional domains
LukasPietzschmann May 16, 2024
4c93b55
feat-fix: store comparison domain with the cleaned id
LukasPietzschmann May 16, 2024
ddcd60a
feat-fix: wrong narrowing of the right hand side of a comparison
LukasPietzschmann May 16, 2024
3f92648
refactor: removed fixme 'cause I fixed it :^)
LukasPietzschmann May 16, 2024
710255f
refactor: added tsdoc comments and removed unneeded method
LukasPietzschmann May 16, 2024
2ea665f
feat: conditionals now work (at least for simple examples)
LukasPietzschmann May 19, 2024
a82c7d2
refactor: removed unused setter
LukasPietzschmann May 19, 2024
e6d3add
refactor: promote AINode to class
LukasPietzschmann May 21, 2024
67871b6
refactor: easier way to partially modify an AINode
LukasPietzschmann May 21, 2024
36a1218
feat: create domain for RLogical
LukasPietzschmann May 21, 2024
e2714bb
refactor: use AINode constructor
LukasPietzschmann May 26, 2024
8e78bbd
Start work on supporting conditionals (let's start with if-else) (#706)
LukasPietzschmann May 26, 2024
1e22c3d
Merge tag 'v2.0.1' into abstract-interpretation-staging
LukasPietzschmann May 28, 2024
a4023d0
feat-fix: adapted AI impl to v2.0.1
LukasPietzschmann May 28, 2024
52437c8
feat: handle string and number node-ids correctly
LukasPietzschmann May 29, 2024
92d5c5a
feat: added domain generation to the dataflow step
LukasPietzschmann Jun 6, 2024
1c76879
feat: propagate domain of rhs to lhs in assignements
LukasPietzschmann Jun 6, 2024
8892c75
feat: generate domain for symbols
LukasPietzschmann Jun 6, 2024
7de6f5b
feat: generate domains for numbers and logicals
LukasPietzschmann Jun 6, 2024
09f7f50
feat: propagate domains through arguments
LukasPietzschmann Jun 6, 2024
5f24188
refactor: fixed imports and removed logs
LukasPietzschmann Jun 6, 2024
e80b1f7
feat: added domain calculation for + and -
LukasPietzschmann Jun 6, 2024
8e529b9
feat: added domain calculation for comparisons
LukasPietzschmann Jun 6, 2024
d3a9a50
feat: use ai to determine if a path in an if-else is not taken
LukasPietzschmann Jun 6, 2024
33120a3
feat: hacked together narrowing propagation
LukasPietzschmann Jun 7, 2024
f8fc753
feat-fix: fixed interval toJSON
LukasPietzschmann Jun 7, 2024
cebd411
feat: added ability to update a vertex inside the dfg
LukasPietzschmann Jun 7, 2024
a6229dd
feat-fix: fixed type
LukasPietzschmann Jun 7, 2024
e0e0551
test: compare vertex domains in tests
LukasPietzschmann Jun 7, 2024
cd2198e
test: added two simple tests
LukasPietzschmann Jun 7, 2024
11fec38
refactor: removed implemented todo
LukasPietzschmann Jun 7, 2024
1c867d9
feat: "abstracted" away truthy and falsy domains
LukasPietzschmann Jun 7, 2024
4b9c134
feat: added ai for && and ||
LukasPietzschmann Jun 7, 2024
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
247 changes: 226 additions & 21 deletions src/abstract-interpretation/domain.ts
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
import { assertUnreachable, guard } from '../util/assert'
import type { Identifier } from '../dataflow/environments/identifier'

interface IntervalBound {
readonly value: number,
Expand All @@ -8,25 +9,76 @@ interface IntervalBound {
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`)
}

static top(): Interval {
return new Interval(
{ value: Number.NEGATIVE_INFINITY, inclusive: false },
{ value: Number.POSITIVE_INFINITY, inclusive: false }
)
}

toString(): string {
if(this.isBottom()) {
return '∅'
}
if(this.isSingleton()) {
return this.min.value.toString()
}
return `${this.min.inclusive ? '[' : '('}${this.min.value}, ${this.max.value}${this.max.inclusive ? ']' : ')'}`
}

equals(other: Interval): boolean {
return this.min.value === other.min.value && this.min.inclusive === other.min.inclusive &&
this.max.value === other.max.value && this.max.inclusive === other.max.inclusive

}

/** An interval is considered empty if it's of the form [T, T) or (T, T] */
isBottom(): boolean {
return this.min.value === this.max.value && !(this.min.inclusive && this.max.inclusive)
}

/** An interval is considered singleton if it's of the form [T, T] */
isSingleton(): boolean {
return this.min.value === this.max.value && this.min.inclusive && this.max.inclusive
}

/** An interval is considered top if it's of the form (-∞, ∞) */
isTop(): boolean {
return this.min.value === Number.NEGATIVE_INFINITY && this.max.value === Number.POSITIVE_INFINITY
}

toJSON(): object {
return {
__type: 'Interval',
min: this.min,
max: this.max
}
}

static revive(data: object): Interval {
// @ts-expect-error I'm too lazy to define the proper type for the JSON object
// eslint-disable-next-line @typescript-eslint/no-unsafe-argument
return new Interval(data.min, data.max)
}
}

export class Domain {
private readonly _intervals: Set<Interval>

private constructor(intervals: Interval[] = []) {
this._intervals = new Set(unifyOverlappingIntervals(intervals))
this._intervals = new Set(unifyOverlappingIntervals(intervals).filter(interval => !interval.isBottom()))
}

static bottom(): Domain {
return new Domain()
}

static top(): Domain {
return new Domain([Interval.top()])
}

static fromIntervals(intervals: Interval[] | Set<Interval>): Domain {
return new Domain(Array.from(intervals))
}
Expand All @@ -38,26 +90,79 @@ export class Domain {
)])
}

static truthy(): Domain {
return Domain.fromScalar(1)
}

static falsy(): Domain {
return this.bottom()
}

isBottom(): boolean {
return this.intervals.size === 0
}

// FIXME: better notion of true/false in a domain
isTop(): boolean {
return this.intervals.size === 1 && Array.from(this.intervals)[0].isTop()
}

isTruthy(): boolean {
return !this.isBottom()
}

isFalsy(): boolean {
return this.isBottom()
}

get intervals(): Set<Interval> {
return this._intervals
}

private set intervals(intervals: Interval[]) {
this._intervals.clear()
for(const interval of intervals) {
this._intervals.add(interval)
toString(): string {
if(this.isBottom()) {
return '⊥'
} else if(this.isTop()) {
return '⊤'
} else {
return `{${Array.from(this.intervals).join(', ')}}`
}
}

addInterval(interval: Interval): void {
this.intervals = unifyOverlappingIntervals([...this.intervals, interval])
equals(other: Domain): boolean {
if(this.isBottom()) {
return other.isBottom()
}
if(this.isTop()) {
return other.isTop()
}
return this.intervals.size === other.intervals.size &&
Array.from(this.intervals).every(interval => Array.from(other.intervals).some(otherInterval => interval.equals(otherInterval)))
}

toString(): string {
return `{${Array.from(this.intervals).join(', ')}}`
toJSON(): object {
return {
__type: 'Domain',
intervals: Array.from(this.intervals)
}
}

static revive(data: object): Domain {
// @ts-expect-error I'm too lazy to define the proper type for the JSON object
// eslint-disable-next-line @typescript-eslint/no-unsafe-argument
return Domain.fromIntervals(data.intervals)
}
}

export interface Narrowing {
readonly positive: Omit<AiInfo, 'narrowings'>,
readonly negative: Omit<AiInfo, 'narrowings'>
}

export class AiInfo {
constructor(readonly id: Identifier, public domain: Domain, readonly narrowings: Narrowing[] = []) { }
}

const enum CompareType {
/** If qual, the bound that's inclusive is the smaller one */
Min,
Expand Down Expand Up @@ -90,23 +195,40 @@ function compareIntervalsByTheirMaximum(interval1: Interval, interval2: Interval
return compareIntervals(CompareType.Max, interval1.max, interval2.max)
}

export function doIntervalsOverlap(interval1: Interval, interval2: Interval): boolean {
export const enum OverlapKind {
Overlap = 0,
Touch = 1,
}

export function doIntervalsOverlap(interval1: Interval, interval2: Interval, kind: OverlapKind = OverlapKind.Overlap): boolean {
const diff1 = compareIntervals(CompareType.IgnoreInclusivity, interval1.max, interval2.min)
const diff2 = compareIntervals(CompareType.IgnoreInclusivity, interval2.max, interval1.min)

let doIntervalsOverlap = true
let doIntervalsTouch = true

// 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
doIntervalsOverlap = false
doIntervalsTouch = false
// If their bounds have the same value, they overlap if both are inclusive
// and touch if only one is inclusive
} else if(diff1 === 0) {
doIntervalsOverlap = interval1.max.inclusive && interval2.min.inclusive
doIntervalsTouch = interval1.max.inclusive !== interval2.min.inclusive
} else if(diff2 === 0) {
doIntervalsOverlap = interval2.max.inclusive && interval1.min.inclusive
doIntervalsTouch = interval2.max.inclusive !== interval1.min.inclusive
}

return true
switch(kind) {
case OverlapKind.Overlap:
return doIntervalsOverlap
case OverlapKind.Touch:
return doIntervalsTouch
default:
return doIntervalsOverlap && doIntervalsTouch
}
}

export function unifyDomains(domains: Domain[]): Domain {
Expand All @@ -123,7 +245,7 @@ export function unifyOverlappingIntervals(intervals: Interval[]): Interval[] {
const unifiedIntervals: Interval[] = []
let currentInterval = sortedIntervals[0]
for(const nextInterval of sortedIntervals) {
if(doIntervalsOverlap(currentInterval, nextInterval)) {
if(doIntervalsOverlap(currentInterval, nextInterval, OverlapKind.Touch | OverlapKind.Overlap)) {
const intervalWithEarlierStart = compareIntervalsByTheirMinimum(currentInterval, nextInterval) < 0 ? currentInterval : nextInterval
const intervalWithLaterEnd = compareIntervalsByTheirMaximum(currentInterval, nextInterval) > 0 ? currentInterval : nextInterval
currentInterval = new Interval(intervalWithEarlierStart.min, intervalWithLaterEnd.max)
Expand Down Expand Up @@ -166,4 +288,87 @@ export function subtractDomains(domain1: Domain, domain2: Domain): Domain {
}
}
return Domain.fromIntervals(intervals)
}

export const enum NarrowKind {
Equal = 1,
Smaller = 2,
Greater = 4
}

interface IntervalOverlap {
smaller: Interval | undefined,
intersection: Interval | undefined,
larger: Interval | undefined
}

function flipInclusiveness(intervalBound: IntervalBound): IntervalBound {
return { value: intervalBound.value, inclusive: !intervalBound.inclusive }
}

export function overlapIntervals(interval1: Interval, interval2: Interval): IntervalOverlap {
const diffMin = compareIntervalsByTheirMinimum(interval1, interval2)
const diffMax = compareIntervalsByTheirMaximum(interval1, interval2)

if(!doIntervalsOverlap(interval1, interval2)) {
if(diffMin < 0) {
return { smaller: interval1, intersection: undefined, larger: undefined }
} else if(diffMin > 0) {
return { smaller: undefined, intersection: undefined, larger: interval1 }
} else {
guard(false, 'Their lower bounds cannot be the same as they do not overlap')
}
}

const intersectionStart = diffMin > 0 ? interval1.min : interval2.min
const intersectionEnd = diffMax < 0 ? interval1.max : interval2.max
const intersection = new Interval(intersectionStart, intersectionEnd)

const smallerOverhang = diffMin < 0 ? new Interval(interval1.min, flipInclusiveness(intersectionStart)) : undefined
const greaterOverhang = diffMax > 0 ? new Interval(flipInclusiveness(intersectionEnd), interval1.max) : undefined

return {
smaller: smallerOverhang,
intersection: intersection,
larger: greaterOverhang
}
}

export function narrowDomain(baseDomain: Domain, boundDomain: Domain, narrowKind: NarrowKind): Domain {
const isSmaller = (narrowKind & NarrowKind.Smaller) !== 0
const isGreater = (narrowKind & NarrowKind.Greater) !== 0
const isEqual = (narrowKind & NarrowKind.Equal) !== 0

guard(!(isGreater && isSmaller), 'Greater and Smaller cannot be combined')

let getNarrowedIntervals: (overlap: IntervalOverlap, bound: Interval) => (Interval | undefined)[]
if(isGreater) {
getNarrowedIntervals = ({ intersection, larger }, bound) => {
if(!isEqual && intersection !== undefined && compareIntervalsByTheirMinimum(intersection, bound) === 0) {
intersection = new Interval({ value: intersection.min.value, inclusive: false }, intersection.max)
}
return [intersection, larger]
}
} else if(isSmaller) {
getNarrowedIntervals = ({ smaller, intersection }, bound) => {
if(!isEqual && intersection !== undefined && compareIntervalsByTheirMaximum(intersection, bound) === 0) {
intersection = new Interval(intersection.min, { value: intersection.max.value, inclusive: false })
}
return [intersection, smaller]
}
} else {
guard(false, 'Either isGreater or isSmaller must be set')
}

const narrowedIntervals: (Interval | undefined)[] = []
for(const baseInterval of baseDomain.intervals) {
for(const boundInterval of boundDomain.intervals) {
const overlap = overlapIntervals(baseInterval, boundInterval)
console.log(`Prompt: ${baseInterval.toString()} ${isSmaller ? '<' : ''}${isGreater ? '>' : ''}${isEqual ? '=' : ''} ${boundInterval.toString()}`)
console.log(`Overlap: ${(overlap.smaller ?? 'none').toString()} ${(overlap.intersection ?? 'none').toString()} ${(overlap.larger ?? 'none').toString()}`)
narrowedIntervals.push(...getNarrowedIntervals(overlap, boundInterval))
}
}

return Domain.fromIntervals(narrowedIntervals.filter(interval => interval !== undefined).map(interval => interval as Interval))
}
44 changes: 0 additions & 44 deletions src/abstract-interpretation/handler/binop/binop.ts

This file was deleted.

26 changes: 0 additions & 26 deletions src/abstract-interpretation/handler/binop/operators.ts

This file was deleted.

Loading
Loading