lisa icon indicating copy to clipboard operation
lisa copied to clipboard

[FEATURE REQUEST] Smashed sum abstract domain

Open VincenzoArceri opened this issue 3 years ago • 0 comments

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.

VincenzoArceri avatar Dec 23 '20 00:12 VincenzoArceri