machine-check-hw 0.7.1

System crate for machine-check for verification of BTOR2 files
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

use btor2rs::{node::Const, sort::Bitvec};
use syn::{parse_quote, Expr};

use crate::translate::btor2::Error;

use super::{uni::create_arith_neg_expr, NodeTranslator};

impl NodeTranslator<'_> {
    pub fn const_expr(&self, value: &Const) -> Result<Expr, Error> {
        let result_bitvec = self.get_bitvec(value.sid)?;

        // convert negation to negation of resulting bitvector
        let (negate, str) = if let Some(str) = value.value.strip_prefix('-') {
            (true, str)
        } else {
            (false, value.value.as_str())
        };

        let value = u64::from_str_radix(str, value.ty.clone() as u32)
            .map_err(|_| Error::InvalidConstant(String::from(str)))?;
        // create value and optionally negate it
        let mut value = create_value_expr(value, result_bitvec);
        if negate {
            value = create_arith_neg_expr(value, result_bitvec.length.get());
        }
        Ok(value)
    }
}

pub fn create_value_expr(value: u64, bitvec: &Bitvec) -> Expr {
    let bitvec_length = bitvec.length.get();
    parse_quote!(::machine_check::Bitvector::<#bitvec_length>::new(#value))
}

pub fn create_zero_expr(bitvec: &Bitvec) -> Expr {
    create_value_expr(0, bitvec)
}

pub fn create_one_expr(bitvec: &Bitvec) -> Expr {
    create_value_expr(1, bitvec)
}

pub fn create_minus_one_expr(bitvec: &Bitvec) -> Expr {
    create_arith_neg_expr(create_value_expr(1, bitvec), bitvec.length.get())
}