Skip to content

TDacik/Astral

Repository files navigation

Astral

Astral is a solver for separation logic based on translation to SMT. Astral supports clasical separation logic as well as strong-separation logic (SSL), in particular, it supports several features that are not supported by other solvers such as limited support for magic wands and arbitrary mixing and nesting of boolean and spatial connectives (see supported fragment).

The solver is currently able to use two SMT backends – Z3 and cvc5.



Supported fragment

Let $x, y$ be variables. Atomic formulae are defined as follow:

Atomic formula Input syntax Semantics
$x = y$ (= x y) $s(x) = s(y)$ and $h = \emptyset$
$x \neq y$ (distinct x y) $s(x) \neq s(y)$ and $h = \emptyset$
$x \mapsto y$ (pto x y) $h = \lbrace s(x) \mapsto s(y) \rbrace$
$\mathsf{emp}$ emp $h = \emptyset$
$\mathsf{ls}$(x,y) (ls x y) $\mathsf{dom}(h) = \emptyset \land s(x) = s(y) \text{ or there exist } n \geq 1, \ell_0, ..., \ell_n \text{ such that } \mathsf{distinct}(\ell_0, ..., \ell_n)$ $\text{ and } h = \lbrace \ell_0 \mapsto \ell_1, ..., \ell_{n-1} \mapsto \ell_n \rbrace \text{ and } s(x) = \ell_0, s(y) = \ell_n$

Let $\phi, \psi$ be formulae.

Connective Input syntax Semantics
$\varphi \land \psi$ (and $\varphi$ $\psi$) $(s,h) \models \varphi \text{ and } (s,h) \models \psi$
$\varphi \lor \psi$ (or $\varphi$ $\psi$) $(s,h) \models \varphi \text{ or } (s,h) \models \psi$
$\varphi \land_\neg \psi$ (and $\varphi \text{ (not } \psi$)) $(s,h) \models \varphi \text{ and } (s,h) \not\models \psi$
$\varphi \ast \psi$ (sep $\phi$ $\psi$) $\exists h_1, h_2. h = h_1 \uplus^s h_2 \text{ and } (s,h_1) \models \varphi \text{ and } (s,h_2) \models \psi$
$\varphi -\kern-.46em{\circledast}$ $\psi$ (septraction $\phi$ $\psi$) $\exists h_1. (s,h_1) \models \varphi \text { and } h_1 \uplus^s h_2 \neq \bot \text{ and } (s,h_1 \uplus^s h_2) \models \psi$

Example input

A formula $x \mapsto y -\kern-.46em{\circledast}$ $\mathsf{ls}(x,y)$ can be represented as:

(declare-sort Loc 0)      ;; Declaration of location sort. Currently fixed to this form by Astral.
(declare-heap (Loc Loc))  ;; Declaration of heap sort. Currently fixed to this form by Astral.

;; Declaration of location variables
(declare-const x Loc)
(declare-const y Loc)

;; Input formula
(assert
  (septraction
    (pto x y)
    (ls x y)
  )
)

(check-sat)

Installation & Usage

After cloning the repository, run opam install . to install Astral. Then the solver can be run by the command astral formula.smt2.

Related Papers

Contact

If you have any questions, do not hesitate to contact the tool/method authors:

License

The tool is available under MIT license.

Acknowledgements

The development was supported by projects SNAPPY and AIDE of the Czech Science Foundation. The main author of the tool was supported by Brno Ph.D. Talent Scholarship funded by the Brno City Municipality.