tygus / suslik Goto Github PK

Implement a specification for de-allocating/copying a list of lists of integers.

Synthesize it if given a hint about a specification of the corresponding auxiliary function that for simple lists of ints.

Depends on issue #12.

As an example, consider the list_copy specification:

{ r :-> x ** lseg(x, S) }
  void listcopy(loc r)
{ r :-> y ** lseg(x, S) ** lseg(y, S) }

It would be nice to be able to state something like

{ r :-> x ** [lseg(x, S)] }

in the precondition to indicate that this lseg is not to be unfolded during the synthesis. In the future, the syntax may be enhanced with fractional permissions.

This issue is about AST/parsing only. It does not cover the semantics of read-only permissions.

• Should rely on the unification machinery

When running suslik <example.syn> -r true, a trace is shown.

The successful subderivations of the synthesiser correspond to the trees. It would be good to have this tree captured as a byproduct of the synthesis, so it could be independently rendered in a format that can be checked by a third-party tool, such as HIP/SLEEK.

This issue is about the design of the derivation tree data type and a serialisation format for it.

Seems specific to the Open rule. When SuSLik succeeds on one branch (and adds the trace of this branch), the other branch (assuming the branch number is 2) is to be added to Worklist. However, it is possible that other expansion is successful, then makes the Open.0 a ghost node.

UnificationRules.SubstRight appears twice within callAbductionRules: in Line 100 and Line 117.

Is this intentional?

Depends on issue #10 and takes the similar example into the account.

This should beneficial for all examples implementing traversals and manipulations.

Given the following example (with dll defined as in the examples):

{ [x, 3] ** x :-> v ** (x + 1) :-> 0 ** (x + 2) :-> r ** dll(r, a, s) }
void helper (loc r)
{ dll(x, b, {v} ++ s) }

When run with -c 2 SuSLik outputs:

void helper (loc r) {
  if (r == 0) {
  } else {
    let y = *(r + 1);
    *(r + 2) = y;
    *(r + 1) = 0;
    helper(y);
    helper(r);
  }
}

Which, when called with r != 0 will recursively call itself with the same argument forever.
I tried to explore the tree in the online IDE, but am not familiar enough with the rules to figure out why the second recursive call was allowed. Possibly an issue in SuSLik or Cyclist, I'm not sure.

Implement a predicate for skip-list and basic operations on it.

A good example is given in this paper:
https://www.irif.fr/~sighirea/spen/FIT-TR-2014-01.pdf

At the moment, synthesis can take "hints" about auxiliary functions, which can be used for synthesing the main one. For instance, this is a specification for tree flattening that takes an auxiliary function:

{ lseg(x1, s1) ** lseg(x2, s2) ** ret :-> x2 }
void lseg_append (loc x1, loc ret)
{ s =i s1 ++ s2 ; lseg(y, s) ** ret :-> y }

{ z :-> x ** tree(x, s) }
void flatten(loc z)
{ z :-> y ** lseg(y, s) }

Even though lseg_append can be synthesized by suslik as a standalone function, it doesn't happen here.

This issue it about extending synthesizer to support "chained" synthesis with auxiliary functions. In this example, it would first synthesize lseg_append and then, using it flatten.