Source code for lyra.abstract_domains.usage.usage_domain

"""
Syntactic Usage Abstract Domain
===============================

Abstract domain to be used for **input data usage analysis** using syntactic variable dependencies.
A program variable can have value *U* (used), *S* (scoped), *W* (written), and *N* (not used).

:Authors: Caterina Urban and Simon Wehrli
"""
from collections import defaultdict
from copy import deepcopy
from typing import Dict, Type, Set

from lyra.abstract_domains.lattice import Lattice
from lyra.abstract_domains.stack import Stack
from lyra.abstract_domains.state import State
from lyra.abstract_domains.store import Store
from lyra.abstract_domains.usage.usage_lattice import UsageLattice
from lyra.core.expressions import VariableIdentifier, Expression, Subscription, Slicing
from lyra.core.types import LyraType
from lyra.core.utils import copy_docstring


[docs]class UsageStore(Store): """An element of a store mapping each program variable to its usage status. All program variables are *not used* by default. .. document private methods .. automethod:: UsageStore._less_equal .. automethod:: UsageStore._meet .. automethod:: UsageStore._join """ def __init__(self, variables, lattices: Dict[LyraType, Type[Lattice]]): """Map each program variable to its usage status. :param variables: set of program variables :param lattices: dictionary from variable types to the corresponding lattice types """ super().__init__(variables, lattices)
[docs] @copy_docstring(Store.is_bottom) def is_bottom(self) -> bool: """The current store is bottom if `all` of its variables map to a bottom element.""" return all(element.is_bottom() for element in self.store.values())
[docs] def increase(self) -> 'UsageStore': """Increase the nesting level. :return: current lattice element modified to reflect an increased nesting level The increase is performed point-wise for each variable. """ for var in self.store: self.store[var].increase() return self
[docs] def decrease(self, other: 'UsageStore') -> 'UsageStore': """Decrease the nesting level by combining lattice elements. :param other: other lattice element :return: current lattice element modified to reflect a decreased nesting level The decrease is performed point-wise for each variable. """ for var in self.store: self.store[var].decrease(other.store[var]) return self
[docs]class SimpleUsageStore(UsageStore): """An element of a store mapping each program variable to its usage status. All program variables are *not used* by default. .. note:: Program variables storing lists are abstracted via summarization. .. document private methods .. automethod:: SimpleUsageStore._less_equal .. automethod:: SimpleUsageStore._meet .. automethod:: SimpleUsageStore._join """ def __init__(self, variables: Set[VariableIdentifier]): """Map each program variable to its usage status. :param variables: set of program variables """ lattices = defaultdict(lambda: UsageLattice) super().__init__(variables, lattices)
[docs]class SimpleUsageState(Stack, State): """Input data usage analysis state. An element of the syntactic usage abstract domain. Stack of maps from each program variable to its usage status. The stack contains a single map by default. .. note:: Program variables storing lists are abstracted via summarization. .. document private methods .. automethod:: SimpleUsageState._assign .. automethod:: SimpleUsageState._assume .. automethod:: SimpleUsageState._output .. automethod:: SimpleUsageState._substitute """ def __init__(self, variables: Set[VariableIdentifier], precursory: State = None): super().__init__(SimpleUsageStore, {'variables': variables}) State.__init__(self, precursory)
[docs] @copy_docstring(Stack.push) def push(self): if self.is_bottom() or self.is_top(): return self self.stack.append(deepcopy(self.lattice).increase()) return self
[docs] @copy_docstring(Stack.pop) def pop(self): if self.is_bottom() or self.is_top(): return self current = self.stack.pop() self.lattice.decrease(current) return self
[docs] @copy_docstring(State._assign) def _assign(self, left: Expression, right: Expression): raise RuntimeError("Unexpected assignment in a backward analysis!")
[docs] @copy_docstring(State._assume) def _assume(self, condition: Expression) -> 'SimpleUsageState': effect = False # effect of the current nesting level on the outcome of the program for variable in self.lattice.variables: value = self.lattice.store[variable] if value.is_written() or value.is_top(): effect = True if effect: # the current nesting level has an effect on the outcome of the program for identifier in condition.ids(): self.lattice.store[identifier].top() return self
[docs] @copy_docstring(State.enter_if) def enter_if(self) -> 'SimpleUsageState': return self.push()
[docs] @copy_docstring(State.exit_if) def exit_if(self) -> 'SimpleUsageState': return self.pop()
[docs] @copy_docstring(State.enter_loop) def enter_loop(self) -> 'SimpleUsageState': return self.push()
[docs] @copy_docstring(State.exit_loop) def exit_loop(self) -> 'SimpleUsageState': return self.pop()
[docs] @copy_docstring(State._output) def _output(self, output: Expression) -> 'SimpleUsageState': for identifier in output.ids(): self.lattice.store[identifier].top() return self
[docs] @copy_docstring(State._substitute) def _substitute(self, left: Expression, right: Expression) -> 'SimpleUsageState': if isinstance(left, VariableIdentifier): if self.lattice.store[left].is_top() or self.lattice.store[left].is_scoped(): # the assigned variable is used or scoped self.lattice.store[left].written() for identifier in right.ids(): self.lattice.store[identifier].top() return self elif isinstance(left, Subscription) or isinstance(left, Slicing): target = left.target if self.lattice.store[target].is_top() or self.lattice.store[target].is_scoped(): # the assigned variable is used or scoped self.lattice.store[target].top() # summarization abstraction (join of U/S with W) for identifier in right.ids(): self.lattice.store[identifier].top() if isinstance(left, Subscription): ids = left.key.ids() else: # Slicing ids = left.lower.ids() | left.upper.ids() for identifier in ids: # make ids in subscript used self.lattice.store[identifier].top() return self error = f"Substitution for {left} is not yet implemented!" raise NotImplementedError(error)