-
Notifications
You must be signed in to change notification settings - Fork 12
Validity prototype #2470
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
Open
MaxAtoms
wants to merge
30
commits into
staging/validity-linting
Choose a base branch
from
validity-prototype
base: staging/validity-linting
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Validity prototype #2470
Changes from 6 commits
Commits
Show all changes
30 commits
Select commit
Hold shift + click to select a range
6310282
wip: very first taint impl
MaxAtoms 3bae296
wip: very first dsl draft
MaxAtoms 112f042
docs-fix: typo
MaxAtoms 2612746
wip: add a very crude demo of conditional taints
MaxAtoms e12fe67
wip: a bit of clean-up
MaxAtoms 5dd99c3
lint-fix: annotation
MaxAtoms 78bc93f
feat: generic testing framework for abstract interpretation inference
OliverGerstl 8ac2f43
wip: improve dsl and predefined analyses
MaxAtoms 38ea1de
feat: add taint analysis to analyzer
MaxAtoms 9ed75c3
feat: add taint analysis query
MaxAtoms 08638f5
feat: adapt data frame shape inference tests to new test framework
OliverGerstl e6ba49f
feat: add generic test function for value inference
OliverGerstl ebb641e
Merge remote-tracking branch 'origin/main' into validity-prototype
MaxAtoms b1c05a8
build-fix: get rid of type errors
MaxAtoms 717bab5
test: add test file
MaxAtoms 954e515
Merge remote-tracking branch 'origin/2471-provide-a-generic-testing-f…
MaxAtoms 9d141c3
build-fix: fix type
MaxAtoms f041d47
wip: draft of finite domain builder
MaxAtoms d51279e
feat-fix: leq of finite domain
MaxAtoms 1586168
wip: add basic finite domain tests
MaxAtoms 31b9135
wip: improved finite lattice
MaxAtoms 843bbd3
tests: add a first set of taint analysis test cases
MaxAtoms c05bfc0
Merge remote-tracking branch 'origin/main' into validity-prototype
MaxAtoms b21aca5
wip: attempt to add type safety to analysis names
MaxAtoms bebfc7c
tests-fix: fix concretize and abstract cases
MaxAtoms 1bd5e7c
refactor: some clean-up
MaxAtoms 26ff15b
refactor: use Identifier helper object
MaxAtoms c4eac44
feat: simplify finite lattice def
MaxAtoms 067f410
test-fix: add test call
MaxAtoms 2727f19
feat-fix: type safety for predefined taint analyses
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,43 @@ | ||
| import type { FlowrAnalyzer } from '../project/flowr-analyzer'; | ||
| import type { AnyAbstractDomain } from '../abstract-interpretation/domains/abstract-domain'; | ||
| import type { FnTaintMapper } from './function-mapper'; | ||
| import { TaintInferenceVisitor } from './taint-visitor'; | ||
| import type { StateAbstractDomain } from '../abstract-interpretation/domains/state-abstract-domain'; | ||
|
|
||
| export class TaintAnalysis<Domain extends AnyAbstractDomain> { | ||
| private readonly domain: Domain; | ||
| private readonly analyzer: FlowrAnalyzer; | ||
| private mapper: FnTaintMapper<Domain> = {}; | ||
| private msg: string | undefined; | ||
|
|
||
| constructor(domain: Domain, analyzer: FlowrAnalyzer) { | ||
| this.domain = domain; | ||
| this.analyzer = analyzer; | ||
| } | ||
|
|
||
| public through(fnMapping: FnTaintMapper<Domain>): this { | ||
| this.mapper = { ...this.mapper, ...fnMapping }; | ||
| return this; | ||
| } | ||
|
|
||
| public to(fnMapping: FnTaintMapper<Domain>): this { | ||
| this.mapper = { ...this.mapper, ...fnMapping }; | ||
| return this; | ||
| } | ||
|
|
||
| public report(msg: string): this { | ||
| this.msg = msg; | ||
| return this; | ||
| } | ||
|
|
||
| public async run(): Promise<StateAbstractDomain<Domain>> { | ||
| const visitor = new TaintInferenceVisitor(this.domain, this.mapper, { | ||
| controlFlow: await this.analyzer.controlflow(), | ||
| ctx: this.analyzer.inspectContext(), | ||
| dfg: (await this.analyzer.dataflow()).graph, | ||
| normalizedAst: await this.analyzer.normalize() | ||
| }); | ||
| visitor.start(); | ||
| return visitor.getEndState(); | ||
| } | ||
| } |
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,67 @@ | ||
| import type { RNode } from '../r-bridge/lang-4.x/ast/model/model'; | ||
| import type { ParentInformation } from '../r-bridge/lang-4.x/ast/model/processing/decorate'; | ||
| import { RType } from '../r-bridge/lang-4.x/ast/model/type'; | ||
| import { Identifier } from '../dataflow/environments/identifier'; | ||
| import type { AbstractDomainValue, AnyAbstractDomain } from '../abstract-interpretation/domains/abstract-domain'; | ||
| import { VariableResolve } from '../config'; | ||
| import { getFunctionArgument, getFunctionArguments } from '../abstract-interpretation/data-frame/mappers/arguments'; | ||
| import type { DataflowGraph } from '../dataflow/graph/graph'; | ||
| import type { ReadOnlyFlowrAnalyzerContext } from '../project/context/flowr-analyzer-context'; | ||
| import type { PotentiallyEmptyRArgument } from '../r-bridge/lang-4.x/ast/model/nodes/r-function-call'; | ||
|
|
||
| export type ResolvedTaint<Domain extends AnyAbstractDomain> = { condition: TaintCond<Domain>, argument: PotentiallyEmptyRArgument<ParentInformation> } | { taint: AbstractDomainValue<Domain> } | undefined; | ||
|
|
||
| /** | ||
| * | ||
| */ | ||
| export function mapFnCallToTaint<Domain extends AnyAbstractDomain>( | ||
| node: RNode<ParentInformation>, | ||
| mapper: FnTaintMapper<Domain>, | ||
| dfg: DataflowGraph, | ||
| ctx: ReadOnlyFlowrAnalyzerContext | ||
| ): ResolvedTaint<Domain> { | ||
| if(node.type !== RType.FunctionCall || !node.named) { | ||
| return; | ||
| } | ||
|
|
||
| const functionName = Identifier.getName(node.functionName.content); | ||
| const taint = mapper[functionName]?.taint; | ||
|
|
||
| if(isTaintCond(taint)) { | ||
| const resolveInfo = { graph: dfg, idMap: dfg.idMap, full: true, resolve: VariableResolve.Alias, ctx: ctx }; | ||
| const args = getFunctionArguments(node, dfg); | ||
| const arg = getFunctionArgument(args, { pos: taint.pos }, resolveInfo); | ||
| if(arg) { | ||
| return { condition: taint, argument: arg }; | ||
| } else { | ||
| return undefined; | ||
| } | ||
| } else if(taint) { | ||
| return { taint: taint }; | ||
| } else { | ||
| return undefined; | ||
| } | ||
| } | ||
|
|
||
| export interface FnTaintMapperInfo<Domain extends AnyAbstractDomain> { | ||
| readonly taint: TaintOrTaintCond<Domain>; | ||
| } | ||
|
|
||
| export type TaintOrTaintCond<Domain extends AnyAbstractDomain> = TaintCond<Domain> | AbstractDomainValue<Domain>; | ||
|
|
||
| export type FnTaintMapper<Domain extends AnyAbstractDomain> = Record<string, FnTaintMapperInfo<Domain>>; | ||
|
|
||
| export type TaintCond<Domain extends AnyAbstractDomain = AnyAbstractDomain> = { | ||
| pos: number; | ||
| cond: (inParam: AbstractDomainValue<Domain>) => AbstractDomainValue<Domain>; | ||
| }; | ||
|
|
||
| /** | ||
| * | ||
| */ | ||
| export function isTaintCond(value: unknown): value is TaintCond { | ||
| if(typeof value !== 'object' || value === null) { | ||
| return false; | ||
| } | ||
| return ['pos', 'cond' ].every(property => property in value); | ||
| } |
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,101 @@ | ||
| import { AbstractDomain } from '../abstract-interpretation/domains/abstract-domain'; | ||
| import { Bottom, Top } from '../abstract-interpretation/domains/lattice'; | ||
|
|
||
| export const Unscaled = Symbol('Unscaled'); | ||
| export const Scaled = Symbol('Scaled'); | ||
|
|
||
| type Lift = typeof Scaled | typeof Unscaled | typeof Top | typeof Bottom; | ||
|
|
||
| // TODO Builder pattern in the DSL for the definition of finite taint lattices | ||
| export class ScaleDomain<Value extends Lift = Lift> extends AbstractDomain<Lift, Lift, typeof Top, typeof Bottom, Value> { | ||
| public create(value: Lift): this; | ||
| public create(value: Lift): ScaleDomain { | ||
| return new ScaleDomain<Lift>(value); | ||
| } | ||
|
|
||
| public top(): this & ScaleDomain<typeof Top>; | ||
| public top(): ScaleDomain<typeof Top> { | ||
| return new ScaleDomain(Top); | ||
| } | ||
|
|
||
| public bottom(): this & ScaleDomain<typeof Bottom>; | ||
| public bottom(): ScaleDomain<typeof Bottom> { | ||
| return new ScaleDomain(Bottom); | ||
| } | ||
|
|
||
| public equals(other: this): boolean { | ||
| return this.value === other.value; | ||
| } | ||
|
|
||
| public leq(other: this): boolean { | ||
| return this.value === Bottom || other.value === Top ; | ||
| } | ||
|
|
||
| public join(other: this): this { | ||
| if(this.value === other.value) { | ||
| return this.create(this.value); | ||
| } | ||
|
|
||
| if(this.value === Bottom) { | ||
| return this.create(other.value); | ||
| } | ||
|
|
||
| if(other.value === Bottom) { | ||
| return this.create(this.value); | ||
| } | ||
|
|
||
| return this.create(Top); | ||
| } | ||
|
|
||
| public meet(other: this): this { | ||
| if(this.value === other.value) { | ||
| return this.create(this.value); | ||
| } | ||
|
|
||
| if(this.value === Top) { | ||
| return this.create(other.value); | ||
| } | ||
|
|
||
| if(other.value === Top) { | ||
| return this.create(this.value); | ||
| } | ||
|
|
||
| return this.create(Bottom); | ||
| } | ||
|
|
||
| public widen(other: this): this { | ||
| return this.join(other); // Using join for widening as the lattice is finite | ||
| } | ||
|
|
||
| public narrow(other: this): this { | ||
| return this.meet(other); // Using meet for narrowing as the lattice is finite | ||
| } | ||
|
|
||
| public concretize(_limit: number): typeof Top | ReadonlySet<Lift> { | ||
| throw new Error('Method not implemented.'); | ||
| } | ||
|
|
||
| public abstract(_concrete: typeof Top | ReadonlySet<Lift>): this { | ||
| throw new Error('Method not implemented.'); | ||
| } | ||
|
|
||
| public toJson(): unknown { | ||
| throw new Error('Method not implemented.'); | ||
| } | ||
|
|
||
| public toString(): string { | ||
| return this.value.toString(); | ||
| } | ||
|
|
||
| public isTop(): this is ScaleDomain<typeof Top> { | ||
| return this.value === Top; | ||
| } | ||
|
|
||
| public isBottom(): this is ScaleDomain<typeof Bottom> { | ||
| return this.value === Bottom; | ||
| } | ||
|
|
||
| public isValue(): this is ScaleDomain { | ||
| return this.value !== Top && this.value !== Bottom; | ||
| } | ||
| } | ||
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,25 @@ | ||
| import { Scaled, ScaleDomain, Unscaled } from './scale-domain'; | ||
| import { Bottom, Top } from '../abstract-interpretation/domains/lattice'; | ||
| import type { FlowrAnalyzer } from '../project/flowr-analyzer'; | ||
| import { TaintAnalysis } from './dsl'; | ||
|
|
||
| /** | ||
| * | ||
| */ | ||
| export async function runScaleAnalysis(analyzer: FlowrAnalyzer) { | ||
| return await new TaintAnalysis(new ScaleDomain(Top), analyzer) | ||
| .through({ | ||
| 'c': { taint: Unscaled }, | ||
| 'scale': { taint: Scaled }, | ||
| }) | ||
| .to({ | ||
| 'mean': { | ||
| taint: { | ||
| pos: 0, | ||
| cond: (taint) => taint == Scaled ? Bottom : taint | ||
| } | ||
| }, | ||
| }) | ||
| .report('Warning: Mean of scaled value is always zero') | ||
| .run(); | ||
| } |
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,55 @@ | ||
| import type { AbsintVisitorConfiguration } from '../abstract-interpretation/absint-visitor'; | ||
| import { AbstractInterpretationVisitor } from '../abstract-interpretation/absint-visitor'; | ||
| import type { DataflowGraphVertexFunctionCall } from '../dataflow/graph/vertex'; | ||
| import type { AnyAbstractDomain } from '../abstract-interpretation/domains/abstract-domain'; | ||
| import type { FnTaintMapper, ResolvedTaint } from './function-mapper'; | ||
| import { mapFnCallToTaint } from './function-mapper'; | ||
| import { EmptyArgument } 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'; | ||
|
|
||
| // TODO Evaluation of violations | ||
| // TODO Taints dependent on multiple input parameters | ||
| export class TaintInferenceVisitor<Domain extends AnyAbstractDomain> extends AbstractInterpretationVisitor<Domain> { | ||
| private readonly domain: Domain; | ||
| private readonly fnCallMapper: FnTaintMapper<Domain>; | ||
|
|
||
| constructor(domain: Domain, fnCallMapper: FnTaintMapper<Domain>, visitorConfig: AbsintVisitorConfiguration) { | ||
| super(visitorConfig, domain.top()); | ||
| this.domain = domain; | ||
| this.fnCallMapper = fnCallMapper; | ||
| } | ||
|
|
||
| protected override onFunctionCall({ call }: { call: DataflowGraphVertexFunctionCall }): void { | ||
| super.onFunctionCall({ call }); | ||
|
|
||
| const node = this.getNormalizedAst(call.id); | ||
|
|
||
| if(node === undefined) { | ||
| return; | ||
| } | ||
|
|
||
| const taint = mapFnCallToTaint(node, this.fnCallMapper, this.config.dfg, this.config.ctx); | ||
| this.applyFnCall(node.info.id, taint); | ||
| } | ||
|
|
||
| private applyFnCall(id: NodeId, taint: ResolvedTaint<Domain>) { | ||
| if(!taint) { | ||
| this.updateState(id, this.domain.top()); | ||
| } else if('taint' in taint) { | ||
| this.updateState(id, this.domain.create(taint.taint)); | ||
| } else { | ||
| if(taint.argument === EmptyArgument || !taint.argument.value?.info) { | ||
| this.updateState(id, this.domain.top()); | ||
| return; | ||
| } | ||
| const currentValue = this.getAbstractValue(taint.argument.value.info.id); | ||
| if(currentValue === undefined) { | ||
| this.updateState(id, this.domain.top()); | ||
| return; | ||
| } | ||
| // @ts-expect-error Ignore for now | ||
| const newValue = taint.condition.cond(currentValue.value); | ||
| this.updateState(id, this.domain.create(newValue)); | ||
| } | ||
| } | ||
| } |
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,21 @@ | ||
| import { FlowrAnalyzerBuilder } from '../project/flowr-analyzer-builder'; | ||
| import { runScaleAnalysis } from './scale-inference'; | ||
|
|
||
| async function main() { | ||
| const analyzer = await new FlowrAnalyzerBuilder() | ||
| .setEngine('tree-sitter') | ||
| .build(); | ||
|
|
||
| analyzer.addRequest(` | ||
| x <- c(1 , 2 , 3 , 4 , 5) | ||
| y <- c(2 , 3 , 4 , 5 , 6) | ||
| x <- scale(x) | ||
| y <- mean(x) | ||
| x > y | ||
| `.trim()); | ||
|
|
||
| const result = await runScaleAnalysis(analyzer); | ||
| console.log(result); | ||
| } | ||
|
|
||
| void main(); |
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Using the
AbstractInterpretationVisitorhas been fine so far. My biggest gripe is the need to define the type of concrete values and abstraction/concretization functions