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 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

// 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 std::str::FromStr;
use crate::ir::*;
use crate::lexer::LexError;
use crate::ir_lexer::Tok;
use crate::bitvector::BV;
use crate::zencode;

grammar<'input, B> where B: BV;

pub Val: Val<B> = {
    "()" => Val::Unit,
    "true" => Val::Bool(true),
    "false" => Val::Bool(false),
    <n:Nat> => Val::I128(i128::from_str(&n).unwrap()),
    "-" <n:Nat> => Val::I128(- i128::from_str(&n).unwrap()),
    <hex:Hex> => {
        Val::Bits(B::from_str(&hex)
                      .unwrap_or_else(|| panic!("Unable to parse bitvector literal {}", hex)))
    },
    <bin:Bin> => {
        Val::Bits(B::from_str(&bin)
                      .unwrap_or_else(|| panic!("Unable to parse bitvector literal {}", bin)))
    },
}

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

pub Assign: (Loc<String>, Val<B>) = {
    <loc:Loc> "=" <v:Val> => (loc, v),
}

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

Id: String = <id:"identifier"> => zencode::encode(id);
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>),
        "()" => Tok::Unit,
        "," => Tok::Comma,
        "-" => Tok::Minus,
        "=" => Tok::Eq,
        "{" => Tok::Lbrace,
        "}" => Tok::Rbrace,
        "true" => Tok::True,
        "false" => Tok::False,
        "." => Tok::Dot,
    }
}