Pentagon as value product#2465
Pentagon as value product#2465schuler-henry wants to merge 4 commits into2451-interval-pentagon-ai-pentagon-inference-visitorfrom
Conversation
Implemented closed pentagon domain as state domain of a closed-pentagon value domain that combines the interval value domain with a set domain representing the upper bounds.
|
|
||
| public static top<Domain extends AnyAbstractDomain>(domain: Domain): StateAbstractDomain<Domain, StateDomainTop> { | ||
| return new StateAbstractDomain(new Map<NodeId, never>(), domain); | ||
| public static top<Domain extends AnyAbstractDomain, T extends StateAbstractDomain<Domain, StateDomainLift<Domain>>>(this: new (value: StateDomainTop, domain: Domain) => T, domain: Domain): T { |
There was a problem hiding this comment.
Maybe a more readable name for T, e.g. StateDomain?
| public static top<Domain extends AnyAbstractDomain, T extends StateAbstractDomain<Domain, StateDomainLift<Domain>>>(this: new (value: StateDomainTop, domain: Domain) => T, domain: Domain): T { | |
| public static top<Domain extends AnyAbstractDomain, StateDomain extends StateAbstractDomain<Domain>>(this: new (value: StateDomainTop, domain: Domain) => StateDomain, domain: Domain): StateDomain { |
| return new ClosedPentagonDomain({ interval: StateAbstractDomain.top(IntervalDomain.top()), upperBounds: UpperBoundsDomain.top() }); | ||
| public override create(value: StateDomainLift<ClosedPentagonValueDomain>): this; | ||
| public override create(value: StateDomainLift<ClosedPentagonValueDomain>): ClosedPentagonDomain { | ||
| return new ClosedPentagonDomain(value, ClosedPentagonValueDomain.top()); |
There was a problem hiding this comment.
| return new ClosedPentagonDomain(value, ClosedPentagonValueDomain.top()); | |
| return new ClosedPentagonDomain(value, this.domain); |
| if(this._value !== Bottom) { | ||
| const valueWithoutNodeItself = value.create(value.value); | ||
| valueWithoutNodeItself.value.upperBounds.remove(node); | ||
| (this._value as Map<NodeId, ClosedPentagonValueDomain>).set(node, valueWithoutNodeItself); |
There was a problem hiding this comment.
Maybe super.set(node, valueWithoutNodeItself)?
| public static bottom(): ClosedPentagonDomain { | ||
| return new ClosedPentagonDomain({ interval: StateAbstractDomain.bottom(IntervalDomain.bottom()), upperBounds: UpperBoundsDomain.bottom() }); | ||
| public override set(node: NodeId, value: ClosedPentagonValueDomain) { | ||
| if(this._value !== Bottom) { |
There was a problem hiding this comment.
If possible, prefer to use the getter this._value if you don't need to modify it
| if(this._value !== Bottom) { | |
| if(this.value !== Bottom) { |
| const valueWithoutNodeItself = value.create(value.value); | ||
| valueWithoutNodeItself.value.upperBounds.remove(node); |
There was a problem hiding this comment.
Can't you just put this directly into the reduction ClosedPentagonDomain.reduce so that you do not have to do this separately. If not, I would at least outsource this into a helper function
| public override narrow(_other: this): this { | ||
| throw new Error('Not Implemented'); | ||
| } |
There was a problem hiding this comment.
I would at least call super.narrow so that we do not have to adapt this code when narrowing is supported later
| public override join(other: this): this { | ||
| return this.create(super.join(other).value); | ||
| } | ||
|
|
||
| public override meet(other: this): this { | ||
| return this.create(super.meet(other).value); | ||
| } | ||
|
|
||
| public override widen(other: this): this { | ||
| return this.create(super.widen(other).value); | ||
| } |
There was a problem hiding this comment.
This is currently a bit inefficient, as we call create two times every time we are joining two states which copies the whole mapping
| public override concretize(_limit: number): ReadonlySet<ConcreteState<ClosedPentagonValueDomain>> | typeof Top { | ||
| if(this.value === Bottom) { | ||
| return new Set(); | ||
| } | ||
| return Top; | ||
| } |
There was a problem hiding this comment.
Do you really need to override this?
|
|
||
| (value.upperBounds.value as Map<NodeId, ReadonlySet<NodeId>>).set(key, newUpperBounds); | ||
| public override isTop(): this is this & StateAbstractDomain<ClosedPentagonValueDomain, StateDomainTop> { | ||
| return this.value !== Bottom && this.value.values().every(pentagon => pentagon.value.interval.isTop() && pentagon.value.upperBounds.isTop()); |
There was a problem hiding this comment.
I am not sure if this is the correct Top representation here.
Because, if you have a node for which you inferred Top in the inferval/upper bounds domain, you at least inferred that it is a number.
This contains more information than an empty map where you have no information about any node.
I think you don't need to override the isTop check here (your implementation of this.top is also the same as for the state domain)
| return this.value !== Bottom && this.value.values().every(pentagon => pentagon.value.interval.isTop() && pentagon.value.upperBounds.isTop()); | ||
| } | ||
|
|
||
| public static reduce(value: StateDomainLift<ClosedPentagonValueDomain>): StateDomainLift<ClosedPentagonValueDomain> { |
There was a problem hiding this comment.
Does this need to be public?
| } | ||
|
|
||
| public static top(): ClosedPentagonValueDomain { | ||
| return new ClosedPentagonValueDomain({ interval: IntervalDomain.top(), upperBounds: UpperBoundsValueDomain.top() as UpperBoundsValueDomain }); |
There was a problem hiding this comment.
Bottom carries them but top does not yet carry the sign-figures
Replaced the visitor call with a callback that resolves the interval for a node id to make the function mapper visitor independent to be reused in the pentagon semantics.
3 participants
No description provided.