# Potential Odin Improvements

This is a compilations of Odin's functionality that potentially needs improvements.

## General
1. ### Making use of imports (aliases)
While Odin supports two versions of import syntax (with and without explicit aliasing), they are not treated as actual imports (no code gets imported from other files). The only time the imported statements are checked against is when the analyzers encounter a token that they have no information of.

2. ### Support for parametrized objects
None of the analyzers even consider objects with void attributes objects.

3. ### Support for parametrized decoration
None of the analyzers make use of decorations that have parametres.
For instance, direct access defect will not be detected in the following:

[a] > parent
  a > state
[] > child
  parent memory > @
  [self] > method
    3.sub ((self.state.add 10).add 10) > @

4. ### Source mapping
Odin AST does not store the location of the term in the source code.

## Mutual Recursion
1. False positives occur in sources with dead code or base cases.

[] > test
  [] > base
    memory > x
    [self] > n
      x.write 0 > @
    [self] > m
      self.n self > @
  [] > derived
    base > @
    base.x > x
    [self] > n
      if. > @
        TRUE
        self.m self
        x.write (x.add 1)

https://github.com/Polystat/awesome-bugs/blob/master/tests/inheritance/mutual-recursion-with-if-branching3.yml

https://github.com/Polystat/awesome-bugs/blob/master/tests/inheritance/mutual-recursion-with-random-if-branching.yml

2. The program crashes with a stack overflow when encountering circular inheritance:

[] > a
  b > @

[] > b
  a > @

## State access

1. Some obscure ways to create state are not accounted for:

[] > a
  c1 > state
  c2 > c1
  cage > c2
[] > second_obj
  a > @
  [self] > func
    self.state > @

OR
(only plain state is detected as of now)

[] > base
  memory > plain_state
  [some_number] > inner_state
    some_number > n
    memory > m
    [] > very_inner_state
      [] > hidden_state
        m > @
    memory > inner_mem
    cage > inner_cage
[] > b
  base > @
  [self] > func
    (self.inner_state 3).very_inner_state.hidden_state > super_tmp
    self.inner_state.inner_cage > tmp
    seq > @
      self.plain_state.write 10
      self.inner_state.inner_mem

2. Shadowing of key words is not accounted for

[memory] > parent
  memory > state
[] > child
  parent > @
  [self] > method
    3.sub ((self.state.add 10).add 10) > @

## Logic extraction
1. Sometimes the princess solver crashes when extracting logic for
methods without arguments even though the formula is correct.

EO:

[] > base
  [self x] > util
    x > @
  [self] > n
    self.util self 10 > @

[] > derived
  base > @
  [self x] > util
    seq > @
      assert (x.less 10)
      x

SMT:

(define-fun properties-of-child-util ((var-child-x Int)) Bool (and true true))
(define-fun value-of-parent-util ((var-parent-x Int)) Int var-parent-x)
(define-fun properties-of-parent-util ((var-parent-x Int)) Bool (and true true))
(define-fun value-of-child-util ((var-child-x Int)) Int var-child-x)
(define-fun value-of-child-n () Int (value-of-child-util 10))
(define-fun properties-of-child-n () Bool (and (properties-of-child-util 10) true))
(define-fun properties-of-parent-n () Bool (and (properties-of-parent-util 10) true))
(define-fun value-of-parent-n () Int (value-of-parent-util 10))
(assert (=> (and (properties-of-parent-util 10) true) (and (properties-of-child-util 10) true)))

2. Current implementation makes it impossible to store boolean values in object fields. Only integer values are supported as of now.

3. No checks are performed on the contents of asserts in EO. As such, it is possible to assert an integer value, which would cause unanticipated behavior. For example, assert (3.add 5).

## Unjustified assumptions
1. Method pairs for inspection are formed by considering only direct descendants. For example, in case of an inheritance chain A -> B -> C only combinations (A,B) and (B,C) are examined. It would be ideal to examine all possible combinations. So, in the given example an additional pair (A,C) is to be examined.