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

use btor2rs::op::{TriOp, TriOpType};
use syn::Expr;

use crate::translate::btor2::{node::bi::create_bit_and, util::create_rnid_expr, Error};

use super::{bi::create_bit_or, uni::create_bit_not, NodeTranslator};

impl NodeTranslator<'_> {
    pub fn tri_op_expr(&mut self, op: &TriOp) -> Result<(syn::Expr, Vec<syn::Stmt>), Error> {
        let a_length = self.get_nid_bitvec(op.a.nid())?.length.get();

        let a_expr = create_rnid_expr(op.a);
        let b_expr = create_rnid_expr(op.b);
        let c_expr = create_rnid_expr(op.c);
        match op.ty {
            TriOpType::Ite => {
                // a = condition, b = then, c = else
                // to avoid control flow, convert condition to bitmask

                let result_sort = self.get_bitvec(op.sid)?;
                let result_length = result_sort.length.get();

                let (condition_mask, mut stmts) =
                    self.create_sext(a_expr.clone(), a_length, result_length)?;
                let (not_condition_mask, not_condition_stmts) =
                    self.create_sext(create_bit_not(a_expr), a_length, result_length)?;

                stmts.extend(not_condition_stmts);

                let then_result: Expr = create_bit_and(condition_mask, b_expr);
                let else_result: Expr = create_bit_and(not_condition_mask, c_expr);
                Ok((create_bit_or(then_result, else_result), stmts))
            }
            TriOpType::Write => {
                // a = array, b = index, c = element to be stored
                Err(Error::NotImplemented(op.ty.to_string()))
            }
        }
    }
}