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

Basic Structure for the Abstract Interpretation #397

Merged
merged 51 commits into from
Jan 26, 2024
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
8759589
feat: added an abstract interpretation (ai) step
LukasPietzschmann Oct 12, 2023
7c25938
feat-fix: forgot to add processor.ts
LukasPietzschmann Oct 12, 2023
a96f623
feat-fix: pass the correct arguments to the ai and slicing step
LukasPietzschmann Oct 12, 2023
954b547
feat: added the normalized ast as a parameter to the ai step
LukasPietzschmann Oct 12, 2023
87e328d
feat-fix: remove the explicitly included normalzsation step
LukasPietzschmann Oct 13, 2023
c3f0a99
refactor: remove normalized ast parameter from abstract interpretatio…
EagleoutIce Oct 13, 2023
2b1020c
git: Merge tag 'v1.2.0' into 378-basic-structure-for-the-abstract-int…
LukasPietzschmann Oct 16, 2023
91c029f
feat: added back the ast as an input for the ai processor
LukasPietzschmann Oct 16, 2023
2c6a555
Merge branch 'main' into 378-basic-structure-for-the-abstract-interpr…
LukasPietzschmann Oct 16, 2023
38077e8
feat, wip: borderline execution trace visitor for the cfg
EagleoutIce Nov 3, 2023
c75224d
feat, wip: only visit exit nodes after we have visited all of its suc…
EagleoutIce Nov 3, 2023
6739f2e
feat, wip: attributing vertex type in cfg
EagleoutIce Nov 3, 2023
71c4e2d
test-fix: adapting tests to new cfg vertex types
EagleoutIce Nov 3, 2023
5023dba
lint-fix: remove unused reference
EagleoutIce Nov 3, 2023
35b9620
Merge branch 'main' into 378-basic-structure-for-the-abstract-interpr…
EagleoutIce Nov 22, 2023
59561af
feat: Added basic structure for traversing the cfg
LukasPietzschmann Dec 6, 2023
1982f2e
feat: Added an interface specifying an interval
LukasPietzschmann Dec 7, 2023
934499a
feat: Narrowed down the node type of assignments
LukasPietzschmann Dec 7, 2023
14401a9
refactor: Intervals -> Domain
LukasPietzschmann Dec 7, 2023
302d19a
feat: If a dfg node reads from multiple sources, unify their domains
LukasPietzschmann Dec 7, 2023
2aab44a
refactor: fixed function names
LukasPietzschmann Dec 7, 2023
20fe13b
refactor: Refactored the unification of domains
LukasPietzschmann Dec 8, 2023
e397ecf
refactor: Domain is now a real class
LukasPietzschmann Dec 8, 2023
2929cae
refactor: Consistent naming scheme and no more .forEach
LukasPietzschmann Dec 8, 2023
7db9f76
feat-fix: don't use members before setting them lol
LukasPietzschmann Dec 9, 2023
7735735
feat: Exported functions, classes and interfaces
LukasPietzschmann Dec 9, 2023
aec40b9
test: Added AI test
LukasPietzschmann Dec 9, 2023
bfa5dca
feat-fix: Added additional flag for comparing intervals
LukasPietzschmann Dec 10, 2023
cc3bb71
refactor: replaced new Array() by the literal syntax []
LukasPietzschmann Dec 10, 2023
76a8242
test: Added tests for the unification of domains
LukasPietzschmann Dec 10, 2023
c3b19e4
refactor: Don't inherit Domain from a Set, make the intervals a member
LukasPietzschmann Dec 10, 2023
b316241
feat: Added interface AINode and a place to store them
LukasPietzschmann Jan 6, 2024
5002fdd
refactor: More sensible types and names
LukasPietzschmann Jan 6, 2024
6c8dd13
refactor: Merged BinOp and Assignment
LukasPietzschmann Jan 6, 2024
621ffef
feat: Added function for adding two domains
LukasPietzschmann Jan 6, 2024
1f439b0
refactor: Fixed formatting
LukasPietzschmann Jan 6, 2024
25ea6ec
feat: Implemented more handling code for bin ops
LukasPietzschmann Jan 6, 2024
b0db502
fix: Don't create Intervals using the literal syntax
LukasPietzschmann Jan 7, 2024
f187d45
fix: Typo
LukasPietzschmann Jan 8, 2024
3a73901
feat: We can now subtract one domain from another
LukasPietzschmann Jan 8, 2024
9b5e98e
refactor: Split into multiple files
LukasPietzschmann Jan 8, 2024
5ce85d9
feat: Added unifyIntervals as a helper
LukasPietzschmann Jan 8, 2024
5d57eef
feat: Check for interval overlaps, if an interval is added to a domain
LukasPietzschmann Jan 8, 2024
775863f
refactor: Code cleanup
LukasPietzschmann Jan 11, 2024
2d31117
refactor: Use the flowR logger
LukasPietzschmann Jan 11, 2024
e7a4e35
refactor: Add static factory methods to the Domain
LukasPietzschmann Jan 11, 2024
c57732e
refactor: Removed TODOs referencing more tests
LukasPietzschmann Jan 15, 2024
d9462d7
refactor: De-globalized the nodeMap
LukasPietzschmann Jan 15, 2024
af963b7
refactor: Replaced a guard with a warning
LukasPietzschmann Jan 22, 2024
7c68256
fix: Temporarily remove the call to `runAbstractInterpretation`
LukasPietzschmann Jan 23, 2024
dcf9eae
Merge branch 'main' into 378-basic-structure-for-the-abstract-interpr…
EagleoutIce Jan 26, 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
156 changes: 153 additions & 3 deletions src/abstract-interpretation/processor.ts
Original file line number Diff line number Diff line change
@@ -1,7 +1,157 @@
import { DataflowInformation } from '../dataflow/internal/info'
import { NormalizedAst } from '../r-bridge'
import {DataflowInformation} from '../dataflow/internal/info'
import {NodeId, NormalizedAst, ParentInformation, RBinaryOp, 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'

const constraintMap = new Map<NodeId, Constraints>()

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
}
}

interface IHandler<ValueType> {
name: string,
enter: () => void
exit: () => ValueType
next: (value: ValueType) => void
}

type Intervals = Set<{min: number, minInclusive: boolean, max: number, maxInclusive: boolean}>

LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved
interface Constraints {
node: NodeId,
intervals: Intervals,
debugMsg: string
}

function intervalFromNumber(n: number): Intervals {
return new Set([{min: n, minInclusive: true, max: n, maxInclusive: true}])
LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved
}

function getIntervalsOfDfgChild(node: NodeId, dfg: DataflowInformation): Intervals {
const dfgNode: [DataflowGraphVertexInfo, OutgoingEdges] | undefined = dfg.graph.get(node)
LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved
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)
if(ids.length === 0) {
return new Set()
}
guard(ids.length === 1, `Multiple reads-edges found for node ${node}`)
const id = ids[0]
LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved
const constraint = constraintMap.get(id)
guard(constraint !== undefined, `No constraint found for ID ${id}`)
return constraint.intervals
}

class Assignment implements IHandler<Constraints> {
private lhs: NodeId | undefined
private rhs: NodeId | undefined
private readonly node: RBinaryOp<ParentInformation>
name = 'Assignment'
LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved

constructor(node: RBinaryOp<ParentInformation>) {
this.node = node
}

enter(): void {
console.log(`Entered ${this.name} ${this.node.info.id}`)
}

exit(): Constraints {
console.log(`Exited ${this.name} ${this.node.info.id}`)
return {
node: this.lhs as NodeId,
intervals: new Set(), // TODO: check interval of the rhs
debugMsg: this.name
LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved
}
}

next(constraint: Constraints): void {
if(this.lhs === undefined) {
LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved
this.lhs = constraint.node
} else if(this.rhs === undefined){
this.rhs = constraint.node
}
console.log(`${this.name} received ${constraint.debugMsg}`)
}
}

class BinOp implements IHandler<Constraints> {
private readonly node: RBinaryOp<ParentInformation>

constructor(node: RBinaryOp<ParentInformation>) {
this.node = node
}

name = 'Bin Op'

enter(): void {
console.log(`Entered ${this.name}`)
}

exit(): Constraints {
console.log(`Exited ${this.name}`)
return {
node: this.node.info.id,
intervals: new Set(), // TODO: Check the operands constraints and see how the operation affects those
debugMsg: this.name
}
}

next(value: Constraints): void {
console.log(`${this.name} received ${value.debugMsg}`)
}
}

export function runAbstractInterpretation(ast: NormalizedAst, dfg: DataflowInformation): DataflowInformation {
console.log('hi from abstract interpretation')
const cfg = extractCFG(ast)
const operationStack = new Stack<IHandler<Constraints>>()
visitCfg(cfg, (node, _) => {
const astNode = ast.idMap.get(node.id)
// TODO: avoid if-else
if(astNode?.type === RType.BinaryOp) {
switch(astNode.flavor) {
case 'assignment': operationStack.push(new Assignment(astNode)).enter(); break
case 'arithmetic': operationStack.push(new BinOp(astNode)).enter; break
default: guard(false, `Unknown binary op ${astNode.flavor}`)
LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved
}
} else if(astNode?.type === RType.Symbol) {
operationStack.peek()?.next({
node: astNode.info.id,
LukasPietzschmann marked this conversation as resolved.
Show resolved Hide resolved
intervals: getIntervalsOfDfgChild(node.id, dfg),
debugMsg: 'Symbol'
})
} else if(astNode?.type === RType.Number){
const num = astNode.content.num
operationStack.peek()?.next({
node: astNode.info.id,
intervals: intervalFromNumber(num),
debugMsg: 'Number'
})
} else if(node.type === CfgVertexType.EndMarker) {
const operation = operationStack.pop()
if(operation === undefined) {
return
}
const operationResult = operation.exit()
guard(!constraintMap.has(operationResult.node), `No constraint for the given ID ${operationResult.node}`)
constraintMap.set(operationResult.node, operationResult)
operationStack.peek()?.next(operationResult)
} else {
guard(false, `Unknown node type ${node.type}`)
}
})
return dfg
}
15 changes: 5 additions & 10 deletions src/util/cfg/visitor.ts
Original file line number Diff line number Diff line change
Expand Up @@ -74,20 +74,15 @@ class ControlFlowGraphExecutionTraceVisitor {
return predecessors
}

// TODO: refactor join with single
private visitNodeArray(ids: NodeId[], cfg: ControlFlowInformation) {
const visited = new Set<NodeId>()
for(const id of ids) {
visit(cfg: ControlFlowInformation): void {
const visited = new Set<NodeId>
for(const id of cfg.entryPoints) {
const node = cfg.graph.vertices().get(id)
guard(node !== undefined, () => `Node with id ${id} not found`)
this.visitSingle(node, { parent: 'root', cfg, siblings: [...ids], visited })
guard(node !== undefined, `Node with id ${id} not present`)
this.visitSingle(node, {parent: 'root', cfg, siblings: [...cfg.entryPoints], visited})
}
}

visit(cfg: ControlFlowInformation): void {
this.visitNodeArray(cfg.entryPoints, cfg)
}

}

/**
Expand Down
Loading