tygus / suslik Goto Github PK
View Code? Open in Web Editor NEWSynthesis of Heap-Manipulating Programs from Separation Logic
License: Other
Synthesis of Heap-Manipulating Programs from Separation Logic
License: Other
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.
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
.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.