S2S: An Efficient Solver for Separation Logic

About S2S

S2S is an efficient and automatic decision procedure for problems in separation logic extended with string constraints. It can be used to prove the validity of both entailment and satisfiability of separation/string logic formulas.

Features

entailment and satisfiability problems of separation logic with

  • inductive predicates
  • integer arithmetic

    • satisfiability problems of string logic with

  • concatenation
  • regular memberships
  • length constraints

    • Download

    0.3.3 (March 2019 - tested on Ubuntu 14.04, Ubuntu 16.04 and Ubuntu 18.04).

    License: academic use only.

    Warranty information:

  • This version was dedicated to SL-COMP 2019. It is not an official release.
  • SL-COMP 2019 benchmarks in S2S grammar could be downloaded here.
  • The tool may contain bugs; use it with your own risks: "see it, send it, sorted".
  • New features are actively developed and updated.

    • Input Grammar (Updating)

    
program ::= (cell_definition  | inductive_definition  | command )*

cell_definition ::=
   'ddata' cell_name '{' (type ID;)* '}' '.'

inductive_definition ::=
   'pred' inductive_name'<'(variable:type)+ '>' '==' formula ('or' formula)* '.'

command ::=
  | 'checksat' formula.
  | 'checkent' formula '|-' formula '.'

formula ::=
  | heap_formula '&' pure_formula
  | '(' 'exists' variable '.' formula ')'

heap_formula ::=
  | 'emp'
  | variable '::' cell_name '<' expression* '>'
  | inductive_name '(' expression+ ')'
  | heap_formula '*' heap_formula

pure_formula ::=
  | 'true'
  | 'false'
  | exp '=' exp
  | exp '!=' exp
  | exp '>' exp
  | exp '>=' exp
  | exp '<' exp
  | exp '<=' exp
  | '!' pure_formula
  | pure_formula '&' pure_formula
  | pure_formula '|' pure_formula
  | '(' 'exists' variable '.' pure_formula ')'
  | '(' 'forall' variable '.' pure_formula ')'

exp ::=
  | integer
  | variable
  | char | word
  | null
  | '-' exp
  | expr '+' exp
  | exp '-' exp
  | integer '\*' exp

type ::=
  | 'int'
  | cell_name

variable ::= ID

cell_name ::= ID

inductive_name ::= ID

ID ::= [a-zA-Z_][a-zA-Z0-9_]*

integer ::= [0-9]+

    An example

    
ddata RefSll_t {
  RefSll_t next;
  int data;
}.

pred lsls< in:RefSll_t,dt1:int,len1:int,out:RefSll_t,dt2:int,len2:int > ==
 emp & in = out & dt1 = dt2 & len1 = len2
or (exists u,dt3,len3: in::RefSll_t * lsls(u,dt3,len3,out,dt2,len2) & dt1 < dt3+0 & len1 = len3+1).

checksat lsls(u_emp,d1,n1,z_emp,d2,n2) * z_emp::RefSll_t * lsls(y_emp,d3,n3,w_emp,d4,n4) & d1 != d2 & n3 = n4+3.

    Developers

  • Quang Loc Le

    • Contact

    lequangloc@gmail.com for bug report and discussion.

    Acknowledgments

  • Mihaela Sighireanu, the Chair, and the contributors of SL-COMP. At the early stage of the development, S2S was tested mainly by the bechmarks of SL-COMP 2018.