Skip to content

[FEATURE REQUEST] Smashed sum abstract domain #23

@VincenzoArceri

Description

@VincenzoArceri

Description
The smashed sum abstract domain takes n > 2 abstract domains and compose them smashing their bottom elements and creating a new single bottom element. Top elements are not smashed but, to preserve the lattice structure, a new top element is introduced (that is greater than each top element of the underlying abstract domains). Least upper bound of two elements of such domain is top when elements come from different abstract domains composing the smashed sum, the least upper bound of the underlying domain otherwise. It is important to have such a way to compose domains especially when dealing with dynamic languages or analysis that handle values of different types.

Suggested implementation
The implementation should be an instance of SemanticDomain and should introduce singletons bottom and top elements. The implementation of the methods of SemanticDomain (e.g., assign, lub) should be similar to the Cartesian product one, except that we need to pay attention when we get non-bottom values from different abstract domains, in such a casa top should be returned.

Metadata

Metadata

Assignees

No one assigned

    Labels

    ❗ priority:p3Priority planning - level 3🎆 type:featureNew feature or request🔍 scope:analysisWork regarding abstract domains or fixpoint algorithms

    Type

    No type

    Projects

    Status

    Backlog

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions