isla-cat 🐱

isla-cat is a Rust library for converting the cat files used by herd to describe hardware relaxed memory models into a form suitable for use with SMT solvers such as Z3 and CVC4.

It also contains a small binary cat2smt which translates such cat files on the command line.

Documentation for the cat language can be found here.

Licensing

The .cat files in the catlib subdirectory are licensed under the CeCILL-B license from herd.

The .cat files in the tests directory are likewise licensed under the CeCILL-B license, except aarch64.cat which is under a 3-clause BSD license from ARM Ltd.

Limitations

cat has some features which are not easy (or even possible at all) to translate into SMT. Roughly-speaking, this supports the fragment of cat that defines sets and relations over events. More formally the fragment of cat we support is defined by the grammar:

expr ::= 0
       | id
       | expr? | expr^-1
       | ~expr
       | [expr]
       | expr | expr
       | expr ; expr | expr \ expr | expr & expr | expr * expr
       | expr expr
       | let id = expr in expr
       | ( expr )

binding ::= id = expr

closure_binding ::= id = expr^+
                  | id = expr^*

id ::= [a-zA-Z_][0-9a-z_.-]*

def ::= let binding { and binding }
      | let closure_binding
      | let funbinding
      | include string
      | show expr as id
      | show id {, id }
      | unshow id {, id }
      | [ flag ] check expr [ as id ]

funbinding ::= id ( id ) = expr

check ::= checkname | ~checkname

checkname ::= acyclic | irreflexive | empty