isla-lib 0.2.0

Isla is a symbolic execution engine for Sail instruction set architecture specifications. This crate implements the core symbolic execution engine as a library.
Documentation
// BSD 2-Clause License
//
// Copyright (c) 2019, 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 std::str::FromStr;
use crate::ir::*;
use crate::lexer::LexError;
use crate::ir_lexer::Tok;
use crate::bitvector::{BV, b64::B64};

grammar<'input, B>;

pub Ty: Ty<String> = {
    "%i" => Ty::I128,
    "%i" <n:Nat> => {
        let sz = u32::from_str(&n).unwrap();
        if sz == 64 {
            Ty::I64
        } else {
            panic!("Unsupported integer size {}", sz)
        }
    },
    "%bv" => Ty::AnyBits,
    "%bv" <n:Nat> => Ty::Bits(u32::from_str(&n).unwrap()),
    "%unit" => Ty::Unit,
    "%bool" => Ty::Bool,
    "%bit" => Ty::Bit,
    "%string" => Ty::String,
    "%real" => Ty::Real,
    "%enum" <id:Id> => Ty::Enum(id),
    "%struct" <id:Id> => Ty::Struct(id),
    "%union" <id:Id> => Ty::Union(id),
    "%vec" "(" <ty:Ty> ")" => Ty::Vector(Box::new(ty)),
    "%fvec" "(" <n:Nat> "," <ty:Ty> ")" => Ty::FixedVector(u32::from_str(&n).unwrap(), Box::new(ty)),
    "%list" "(" <ty:Ty> ")" => Ty::List(Box::new(ty)),
    "&" "(" <ty:Ty> ")" => Ty::Ref(Box::new(ty)),
};

pub Loc: Loc<String> = {
    <id:Id> => Loc::Id(id),
    <l:Loc> "." <field:Id> => Loc::Field(Box::new(l), field),
    <l:Loc> "*" => Loc::Addr(Box::new(l)),
}

pub Op: Op = {
    "@not" => Op::Not,
    "@or" => Op::Or,
    "@and" => Op::And,
    "@eq" => Op::Eq,
    "@neq" => Op::Neq,
    "@slice" "::<" <n:Nat> ">" => Op::Slice(u32::from_str(&n).unwrap()),
    "@set_slice" => Op::SetSlice,
    "@signed" "::<" <n:Nat> ">" => Op::Signed(u32::from_str(&n).unwrap()),
    "@unsigned" "::<" <n:Nat> ">" => Op::Unsigned(u32::from_str(&n).unwrap()),
    "@zero_extend" "::<" <n:Nat> ">" => Op::ZeroExtend(u32::from_str(&n).unwrap()),
    "@bvnot" => Op::Bvnot,
    "@bvor" => Op::Bvor,
    "@bvxor" => Op::Bvxor,
    "@bvand" => Op::Bvand,
    "@bvadd" => Op::Bvadd,
    "@bvsub" => Op::Bvsub,
    "@bvaccess" => Op::Bvaccess,
    "@concat" => Op::Concat,
    "@lteq" => Op::Lteq,
    "@lt" => Op::Lt,
    "@gteq" => Op::Gteq,
    "@gt" => Op::Gt,
    "@hd" => Op::Head,
    "@tl" => Op::Tail,
    "@iadd" => Op::Add,
    "@isub" => Op::Sub,
}

pub Exp: Exp<String> = {
    <id:Id> => Exp::Id(id),
    "true" => Exp::Bool(true),
    "false" => Exp::Bool(false),
    "bitzero" => Exp::Bits(B64::new(0, 1)),
    "bitone" => Exp::Bits(B64::new(1, 1)),
    "()" => Exp::Unit,
    "undefined" ":" <ty:Ty> => Exp::Undefined(ty),
    <n:Nat> => Exp::I64(i64::from_str(&n).unwrap()),
    "-" <n:Nat> => Exp::I64(- i64::from_str(&n).unwrap()),
    <n:Nat> ":" "%i" <sz:Nat> => {
        let sz = u32::from_str(&sz).unwrap();
        if sz == 64 {
            Exp::I64(i64::from_str(&n).unwrap())
        } else if sz == 128 {
            Exp::I128(i128::from_str(&n).unwrap())
        } else {
            panic!("Cannot parse integer size {}", sz)
        }
    },
    "-" <n:Nat> ":" "%i" <sz:Nat> => {
        let sz = u32::from_str(&sz).unwrap();
        if sz == 64 {
            Exp::I64(- i64::from_str(&n).unwrap())
        } else if sz == 128 {
            Exp::I128(- i128::from_str(&n).unwrap())
        } else {
            panic!("Cannot parse integer size {}", sz)
        }
    },
    <s:String> => Exp::String(s),
    "emptybitvec" => Exp::Bits(B64::zeros(0)),
    <hex:Hex> => {
        Exp::Bits(B64::from_str(&hex).expect("Unable to parse bitvector literal"))
    },
    <bin:Bin> => {
        Exp::Bits(B64::from_str(&bin).expect("Unable to parse bitvector literal"))
    },
    "&" <id:Id> => Exp::Ref(id),
    "struct" <id:Id> "{" <fields:Comma<Fexp>> "}" => Exp::Struct(id, fields),
    <e:Exp> "is" <id:Id> => Exp::Kind(id, Box::new(e)),
    <e:Exp> "as" <id:Id> => Exp::Unwrap(id, Box::new(e)),
    <e:Exp> "." <id:Id> => Exp::Field(Box::new(e), id),
    <op:Op> "(" <es:Comma<Exp>> ")" => Exp::Call(op, es)
}

pub Instr: Instr<String, B> = {
    <id:Id> ":" <ty:Ty> => Instr::Decl(id, ty),
    <id:Id> ":" <ty:Ty> "=" <e:Exp> => Instr::Init(id, ty, e),
    "jump" <e:Exp> "goto" <n:Nat> "`" <s:String> => Instr::Jump(e, usize::from_str(&n).unwrap(), s),
    "goto" <n:Nat> => Instr::Goto(usize::from_str(&n).unwrap()),
    <l:Loc> "=" <e:Exp> => Instr::Copy(l, e),
    "mono" <id:Id> => Instr::Monomorphize(id),
    <l:Loc> "=" <id:Id> "(" <es:Comma<Exp>> ")" => Instr::Call(l, false, id, es),
    <l:Loc> "=" "$" <id:Id> "(" <es:Comma<Exp>> ")" => Instr::Call(l, true, id, es),
    "failure" => Instr::Failure,
    "arbitrary" => Instr::Arbitrary,
    "end" => Instr::End,
}

pub Def: Def<String, B> = {
    "register" <id:Id> ":" <ty:Ty> =>
        Def::Register(id, ty),
    "let" "(" <ids:Comma<Arg>> ")" "{" <instrs:Semi<Instr>> "}" =>
        Def::Let(ids, instrs),
    "enum" <id:Id> "{" <ids:Comma<Id>> "}" =>
        Def::Enum(id, ids),
    "struct" <id:Id> "{" <ids:Comma<Arg>> "}" =>
        Def::Struct(id, ids),
    "union" <id:Id> "{" <ids:Comma<Arg>> "}" =>
        Def::Union(id, ids),
    "val" <id:Id> ":" "(" <tys:Comma<Ty>> ")" "->" <ty:Ty> =>
        Def::Val(id, tys, ty),
    "val" <id:Id> "=" <ext:String> ":" "(" <tys:Comma<Ty>> ")" "->" <ty:Ty> =>
        Def::Extern(id, ext, tys, ty),
    "fn" <id:Id> "(" <ids:Comma<Id>> ")" "{" <instrs:Semi<Instr>> "}" =>
        Def::Fn(id, ids, instrs),
}

pub Ir: Vec<Def<String, B>> = {
    <ds:Def*> => ds
}

Arg: (String, Ty<String>) = {
    <id:Id> ":" <ty:Ty> => (id, ty)
}

Fexp: (String, Exp<String>) = {
    <id:Id> "=" <e:Exp> => (id, e)
}

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

Semi<T>: Vec<T> = {
    <v:(<T> ";")*> <e:T> ";"? => {
        let mut v = v;
        v.push(e);
        v
    }
};

Id: String = <id:"identifier"> => id.to_string();
Nat: String = <nat:"natural"> => nat.to_string();
String: String = <s:"string"> => s.to_string();
Hex: String = <b:"hex"> => b.to_string();
Bin: String = <b:"bin"> => b.to_string();

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

    enum Tok<'input> {
        "identifier" => Tok::Id(<&'input str>),
        "natural" => Tok::Nat(<&'input str>),
        "string" => Tok::String(<&'input str>),
        "hex" => Tok::Hex(<&'input str>),
        "bin" => Tok::Bin(<&'input str>),
        "%i" => Tok::TyI,
        "%bv" => Tok::TyBv,
        "%unit" => Tok::TyUnit,
        "%bool" => Tok::TyBool,
        "%bit" => Tok::TyBit,
        "%string" => Tok::TyString,
        "%real" => Tok::TyReal,
        "%enum" => Tok::TyEnum,
        "%struct" => Tok::TyStruct,
        "%union" => Tok::TyUnion,
        "%vec" => Tok::TyVec,
        "%fvec" => Tok::TyFVec,
        "%list" => Tok::TyList,
        "`" => Tok::Backtick,
        "&" => Tok::Amp,
        "." => Tok::Dot,
        "," => Tok::Comma,
        ";" => Tok::Semi,
        "*" => Tok::Star,
        "-" => Tok::Minus,
        ":" => Tok::Colon,
        "=" => Tok::Eq,
        "$" => Tok::Dollar,
        "(" => Tok::Lparen,
        ")" => Tok::Rparen,
        "{" => Tok::Lbrace,
        "}" => Tok::Rbrace,
        "@not" => Tok::OpNot,
        "@or" => Tok::OpOr,
        "@and" => Tok::OpAnd,
        "@eq" => Tok::OpEq,
        "@neq" => Tok::OpNeq,
        "@slice" => Tok::OpSlice,
        "@set_slice" => Tok::OpSetSlice,
        "@concat" => Tok::OpConcat,
        "@signed" => Tok::OpSigned,
        "@unsigned" => Tok::OpUnsigned,
        "@zero_extend" => Tok::OpZeroExtend,
        "@bvnot" => Tok::OpBvnot,
        "@bvor" => Tok::OpBvor,
        "@bvxor" => Tok::OpBvxor,
        "@bvand" => Tok::OpBvand,
        "@bvadd" => Tok::OpBvadd,
        "@bvsub" => Tok::OpBvsub,
        "@bvaccess" => Tok::OpBvaccess,
        "@lteq" => Tok::OpLteq,
        "@lt" => Tok::OpLt,
        "@gteq" => Tok::OpGteq,
        "@gt" => Tok::OpGt,
        "@hd" => Tok::OpHead,
        "@tl" => Tok::OpTail,
        "@iadd" => Tok::OpAdd,
        "@isub" => Tok::OpSub,
        "bitzero" => Tok::Bitzero,
        "bitone" => Tok::Bitone,
        "::<" => Tok::TurboFish,
        ">" => Tok::Gt,
        "()" => Tok::Unit,
        "->" => Tok::Arrow,
        "struct" => Tok::Struct,
        "enum" => Tok::Enum,
        "union" => Tok::Union,
        "is" => Tok::Is,
        "as" => Tok::As,
        "goto" => Tok::Goto,
        "jump" => Tok::Jump,
        "mono" => Tok::Mono,
        "failure" => Tok::Failure,
        "arbitrary" => Tok::Arbitrary,
        "undefined" => Tok::Undefined,
        "end" => Tok::End,
        "register" => Tok::Register,
        "fn" => Tok::Fn,
        "let" => Tok::Let,
        "val" => Tok::Val,
        "true" => Tok::True,
        "false" => Tok::False,
        "emptybitvec" => Tok::EmptyBitvec,
    }
}