nishanttotla / masters-thesis Goto Github PK

Should it be a tuple of (Pred, Pattern), or just a Pattern to keep things simple?

Positive examples (+) presented to the user are those that must be part of any pattern the user provides for a given node. Negative examples (-) must not be. Also, 1_D and 0_D are the universal and empty heaps, respectively.

What we have so far:

Consider a node [n] and the path from [root] to [ERR] that passes through [n].

[root] --> [n] --> [ERR]

Suppose [n] is currently annotated with S. Now consider the following algorithm

C := candidate (obtained from user or somewhere)

if S ⊨ C then do nothing
else
  h_1 := some heap in the set S\C
  return (h_1, +)

Here we're obviously trusting that S is a good candidate at [n], and that C needs to be expanded to cover that. Why should that be? The original IMPACT algorithm simply finds the Interpolant along the path, not having to worry about all these things.

The following part is unclear, it is relevant to generating negative examples.

  S = Post*(True, [root], [n])
  S_2 = Post*(C, [n], [ERR])
  since S ⊨ C
  if ∃ h ∈ C s.t. Post*(h, [n], [ERR]) is not entailed by all invariants labeled on the path [n] to [ERR] then return (h, -)

No idea how to actually find the h that is required above. The idea here is that if a heap h is such that it's strongest post transform up to a certain successor node [m] isn't actually part of the pattern candidate currently assigned to [m], then either h shouldn't be part of the pattern at [n], or the pattern at [m] is too strong. It's not clear which should be updated. We could either provide h as a negative example for [n] or a positive example for [m]. This is a tricky interplay and perhaps both possibilities need to be explored. Maybe a top level algorithm is needed, that somehow explores all cases by presenting them to the user. We could leave this discussion out of the scope of the initial draft of the paper, and revisit it later.

Also consider the following

  if ∃ h ∈ C s.t. Post*(h, [n], [ERR]) ≠ 0_D, then return (h, -)

The reasoning being that a concrete heap h that after passing through the path from [n] to [ERR] does not actually result in the empty heap must not be part of the candidate at that node [n]. Given that this Post* is a well-defined operation, only dependent on the program itself, it doesn't matter what candidates the nodes along the path are actually labeled with. So if this is the case, then we're absolutely sure (alluding to the discussion above) that h as a positive example for [m] makes more sense. It might still not end up being right, but still helps make a choice.

Not sure what is up. Here's the code for it.

% Transfer functions for each instruction.
\begin{figure*}
  \centering
  \begin{gather*}
    % Allocation:
    \inference[ALLOC]
    %
    { n \notin N & N' = \add{n}{N} \\
      %
      V' = \upd{V}{\cc{h}}{n}
      & F' = F[ \{ (n, f) \mapsto \nil \}_{f \in \fields} ]
    }
    %
    { \langle (C, V, F), \code{h \assign \alloc()} \rangle \step
      %
      (N', V', F')
    } \rulebuffer
    % Copy:
    \inference[COPY]
    %
    {  V' = \upd{V}{\cc{g}}{V(\cc{h})}
    }
    %
    { \langle (C, V, F), \code{g \assign h} \rangle \step
      %
      (C, V', F)
    } \\[\rowspace]
    % Load:
    \inference[LOAD]
    { V' = \upd{V}{\code{p}}{F(V(\code{q}), \code{f})}
    }
    %
    { \langle (C, V, F), \code{p \assign q \select f} \rangle \step
      %
      (C, V', F)
    } \rulebuffer
    % Store:
    \inference[STORE]
    { F' = \upd{F}{(\cc{p}, \cc{f})}{V(\cc{q})}
    }
    { \langle (C, V, F), \code{p \select f \assign q } \rangle
      \step
      %
      (C, V, F')
    }
  \end{gather*}
  \caption{Inference rules that define $\heapstep$, the transition
    relation over heaps and heap updates.}
  \label{fig:semantics}
\end{figure*}

In a single path, at a given program location, there is absolutely no reason to have more than one possible heap in a single vertex of the unwinding. We should ideally look at all the positive/negative examples for a given program location, not a point in the unwinding. The formalism needs a little tweaking.

This needs to be described clearly