SLING is a tool for dynamically inferring separation logic sepcifications. The input is traces so SLING can work with different programming languages. We have tested on C, C , Java and Python.
The default setting of SLING works with C or C . It uses LLDB to obtain traces and Python to infer seperation logic invariants based on the traces. SLING has been tested using the following setup:
- Ubuntu 16.04
- Python 2.7
- LLDB 3.8
Follow the following steps to setup SLING:
- Install Python and LLDB:
sudo apt install python python-pip lldb lldb-3.8-dev gcc - Install required Python libs:
pip install lark-parser z3-solver - Link LLDB libs in case of version conflict(when SLING couldn't obtain any traces):
cd /usr/lib/llvm-3.8/lib/python2.7/site-packages/lldb/ sudo ln -sf ../../../liblldb.so.1 _lldb.so sudo ln -sf ../../../libLLVM-3.6.0.so.1 libLLVM-3.6.0.so.1 sudo ln -sf ../../../libLLVM-3.6.0.so.1 libLLVM-3.6.so.1 export PYTHONPATH='/usr/lib/llvm-3.6/lib/python2.7/site-packages'
Given a program PATH/TO/sling/simple_example/sll/append.c:
SNnode * sll_append(SNnode * x1, SNnode * x2)
{
//pre
if (x1 == NULL) {
//post
return x2;
} else {
SNnode * tmp = sll_append(x1->next, x2);
x1->next = tmp;
//post
return x1;
}
}
The predicate defination(templates) PATH/TO/sling/simple_example/sll/defn.sl:
pred ll(x) := emp & x=nil
\/ (exists v, y. x->node{v, y} * ll(y));
Run the following command under PATH/TO/sling/src directory to call SLING to infer its invariants for a size 5 input:
./run.sh 5 PATH/TO/sling/simple_example/sll/defn.sl PATH/TO/sling/simple_example/sll/append.c
SLING then outputs the inferred precondition and postcondition for append.c:
dynsl.py:299 - Precondition at location 8:
dynsl.py:307 - ll(x2) * ll(x1)
dynsl.py:309 - ==============================
dynsl.py:312 - Postcondition at location 10:
dynsl.py:320 - ll(x2) & x2 = res
dynsl.py:322 - ==============================
dynsl.py:312 - Postcondition at location 15:
dynsl.py:320 - ll(x2) * x1:node->node{fv0, tmp}
dynsl.py:322 - ==============================
The dll concat motivating example in the paper is in the PAHT/TO/sling/simple_example/dll/concat.c:
DLNode* dll_concat(DLNode* a, DLNode* b)
{
//pre
if (a == NULL) {
//post
return b;
} else {
DLNode* tmp = dll_concat(a->next, b);
a->next = tmp;
if (tmp) tmp->prev = a;
//post
return a;
}
}
With the following predicate defination PATH/TO/sling/simple_example/dll/defn.sl:
pred dll(hd, p, tl, n) := hd=n & tl=p
\/ (exists d, x. hd->node{d, x, p} * dll(x, hd, tl, n));
Run the following command in PATH/TO/sling/src directory:
./run.sh 5 PATH/TO/sling/simple_example/dll/defn.sl PATH/TO/sling/simple_example/dll/concat.c
SLING infers the following results:
dynsl.py:299 - Precondition at location 7:
dynsl.py:307 - dll(b, nil, fv2, nil) * dll(a, fv1, fv0, nil)
dynsl.py:307 - dll(b, nil, fv2, nil) * dll(a, nil, fv1, fv0)
dynsl.py:307 - dll(b, nil, fv0, nil) * dll(a, nil, nil, a)
dynsl.py:309 - ==============================
dynsl.py:312 - Postcondition at location 9:
dynsl.py:320 - dll(b, nil, fv0, nil) & a = nil & b = res
dynsl.py:322 - ==============================
dynsl.py:312 - Postcondition at location 15:
dynsl.py:320 - dll(a, fv2, a, tmp) * dll(b, fv1, tmp, fv0) * dll(tmp, b, b, tmp) & a = res
dynsl.py:320 - dll(a, fv4, a, tmp) * dll(b, fv3, tmp, fv2) * dll(tmp, fv1, fv0, b) & a = res
dynsl.py:320 - dll(a, fv3, a, tmp) * dll(b, tmp, fv2, fv1) * dll(tmp, a, fv0, b) & a = res
dynsl.py:320 - dll(a, fv2, a, tmp) * dll(b, fv1, fv0, nil) * dll(tmp, b, b, tmp) & a = res
dynsl.py:320 - dll(a, fv4, a, tmp) * dll(b, fv3, fv2, nil) * dll(tmp, fv1, fv0, b) & a = res
dynsl.py:320 - dll(a, nil, fv3, fv2) * dll(b, fv1, tmp, fv0) * dll(tmp, b, b, tmp) & a = res
dynsl.py:320 - dll(a, nil, fv5, fv4) * dll(b, fv3, tmp, fv2) * dll(tmp, fv1, fv0, b) & a = res
dynsl.py:320 - dll(a, nil, fv4, fv3) * dll(b, tmp, fv2, fv1) * dll(tmp, a, fv0, b) & a = res
dynsl.py:320 - dll(a, nil, fv3, fv2) * dll(b, fv1, fv0, nil) * dll(tmp, b, b, tmp) & a = res
dynsl.py:320 - dll(a, nil, fv5, fv4) * dll(b, fv3, fv2, nil) * dll(tmp, fv1, fv0, b) & a = res
For information and experiment about PLDI19 artifect evaluation, please refer to the PLDI19_AE directory.