isla-cat 0.2.0

Isla is a symbolic execution engine for Sail instruction set architecture specifications. This crate implements a SMT translator for subset of the cat language used by herd7 to specify relaxed memory models.
Documentation
// BSD 2-Clause License
//
// Copyright (c) 2020 Alasdair Armstrong
//
// All rights reserved.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are
// met:
//
// 1. Redistributions of source code must retain the above copyright
// notice, this list of conditions and the following disclaimer.
//
// 2. Redistributions in binary form must reproduce the above copyright
// notice, this list of conditions and the following disclaimer in the
// documentation and/or other materials provided with the distribution.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
// HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

use crate::cat::*;
use crate::cat_lexer::{LexError, Tok};

grammar<'input>;

AtomicExp: Exp<()> = {
    "0" => Exp::Empty(()),
    <id:Id> => Exp::Id(id, ()),
    "{" "}" => Exp::Empty(()),
    "(" <x:Exp> ")" => x,
    "[" <x:Exp> "]" => Exp::Identity(Box::new(x)),
}

Exp0: Exp<()> = {
    <x:AtomicExp> => x,
    <f:Id> <x:AtomicExp> => Exp::App(f, Box::new(x), ()),
    "~" <x:AtomicExp> => Exp::Compl(Box::new(x), ()),
    <x:AtomicExp> "?" => Exp::IdentityUnion(Box::new(x)),
    <x:AtomicExp> "^-1" => Exp::Inverse(Box::new(x)),
}

Exp1: Exp<()> = {
    <x:Exp0> => x,
    <x:Exp0> "*" <y:Exp0> => Exp::Cartesian(Box::new(x), Box::new(y)),
}

Exp2: Exp<()> = {
    <x:Exp1> => x,
    <x:Exp2> "\\" <y:Exp1> => Exp::Diff(Box::new(x), Box::new(y), ()),
}

Exp3: Exp<()> = {
    <x:Exp2> => x,
    <x:Exp2> "&" <y:Exp3> => Exp::Inter(Box::new(x), Box::new(y), ()),
}

Exp4: Exp<()> = {
    <x:Exp3> => x,
    <x:Exp3> ";" <y:Exp4> => Exp::Seq(Box::new(x), Box::new(y)),
}

Exp5: Exp<()> = {
    <x:Exp4> => x,
    //<x:Exp4> "++" <y:Exp5> => Exp::Add(Box::new(x), Box::new(y), ()),
}

Exp6: Exp<()> = {
    <x:Exp5> => x,
    <x:Exp5> "|" <y:Exp6> => Exp::Union(Box::new(x), Box::new(y), ()),
}

Exp: Exp<()> = {
    <x:Exp6> => x,
    "let" <id:Id> "=" <x:Exp> "in" <y:Exp> => Exp::Let(id, Box::new(x), Box::new(y), ()),
    "try" <x:Exp> "with" <y:Exp> => Exp::TryWith(Box::new(x), Box::new(y), ()),
}

Check: Check = {
    "acyclic" => Check::Acyclic,
    "irreflexive" => Check::Irreflexive,
    "empty" => Check::Empty,
    "~" "acyclic" => Check::NonAcyclic,
    "~" "irreflexive" => Check::NonIrreflexive,
    "~" "empty" => Check::NonEmpty,
}

Binding: (String, Exp<()>) = {
    <name:Id> "=" <exp:Exp> => (name, exp)
}

Bindings: (u8, Vec<(String, Exp<()>)>) = {
    <name:Id> "=" <exp:Exp> "^+" => (0, vec![(name, exp)]),
    <name:Id> "=" <exp:Exp> "^*" => (1, vec![(name, exp)]),
    <mut v:(<Binding> "and")*> <b:Binding> => {
        v.push(b);
        (3, v)
    }
}

Def: Def<()> = {
    "let" <b:Bindings> => 
        match b {
            (0, mut b) => {
                let (name, exp) = b.remove(0);
                Def::TClosure(name, exp)
            }
            (1, mut b) => {
                let (name, exp) = b.remove(0);
                Def::RTClosure(name, exp)
            }
            (_, b) => Def::Let(b)
        },

    "let" <name:Id> "(" <param:Id> ")" "=" <exp:Exp> => Def::Fn(name, vec![(param, ())], exp),

    "flag" <c:Check> <exp:Exp> "as" <tag:Id> => Def::Flag(c, exp, tag),

    <c:Check> <exp:Exp>               => Def::Check(c, exp, None),
    <c:Check> <exp:Exp> "as" <tag:Id> => Def::Check(c, exp, Some(tag)),

    "show" <names:Comma<Id>> => Def::Show(names),
    "show" <exp:Exp> "as" <name:Id> => Def::ShowAs(exp, name),
    "unshow" <names:Comma<Id>> => Def::Unshow(names),

    "set" <name:Id> => Def::Set(name),
    "relation" <name:Id> => Def::Relation(name),
}

ParseDef: ParseDef = {
    "include" <file:String> => ParseDef::Include(file),
    <def:Def> => ParseDef::Def(def),
}

pub Cat: ParseCat = {
                 <defs:ParseDef*> => ParseCat { tag: "".to_string(), defs },
    <tag:String> <defs:ParseDef*> => ParseCat { tag, defs },
    <tag:Id>     <defs:ParseDef*> => ParseCat { tag, defs },
}

Id: String = <id:"id"> => id.to_string();
String: String = <string:"string"> => string.to_string();

Comma<T>: Vec<T> = {
    <mut v:(<T> ",")*> <e:T> => {
        v.push(e);
        v
    }
};

extern {
    type Location = usize;
    type Error = LexError;

    enum Tok<'input> {
        "id" => Tok::Id(<&'input str>),
        "string" => Tok::String(<&'input str>),
        "in" => Tok::In,
        "include" => Tok::Include,
        "as" => Tok::As,
        "acyclic" => Tok::Acyclic,
        "flag" => Tok::Flag,
        "irreflexive" => Tok::Irreflexive,
        "empty" => Tok::Empty,
        "let" => Tok::Let,
        "rec" => Tok::Rec,
        "and" => Tok::And,
        "try" => Tok::Try,
        "with" => Tok::With,
        "show" => Tok::Show,
        "unshow" => Tok::Unshow,
        "transitive" => Tok::Transitive,
        "reflexive" => Tok::Reflexive,
        "set" => Tok::Set,
        "relation" => Tok::Relation,
        "^-1" => Tok::Inverse,
        "^+" => Tok::HatPlus,
        "^*" => Tok::HatStar,
        "0" => Tok::Zero,
        "," => Tok::Comma,
        "=" => Tok::Eq,
        "~" => Tok::Tilde,
        "|" => Tok::Bar,
        "&" => Tok::Amp,
        "++" => Tok::PlusPlus,
        ";" => Tok::SemiColon,
        "\\" => Tok::Backslash,
        "+" => Tok::Plus,
        "*" => Tok::Star,
        "?" => Tok::Question,
        "{" => Tok::Lbrace,
        "}" => Tok::Rbrace,
        "(" => Tok::Lparen,
        ")" => Tok::Rparen,
        "[" => Tok::Lsquare,
        "]" => Tok::Rsquare,
    }
}