monster-rs 0.4.1

Monster is a symbolic execution engine for 64-bit RISC-U code
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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127

use super::{
    Assignment, BVOperator, BitVector, Formula, SmtSolver, Solver, SolverError,
    Symbol::{Constant, Input, Operator},
    SymbolId,
};
use boolector_solver::{
    option::{BtorOption, ModelGen, OutputFileFormat},
    Btor, SolverResult, BV,
};
use std::{collections::HashMap, rc::Rc};

pub struct Boolector {}

impl Boolector {
    pub fn new() -> Self {
        Self {}
    }
}

impl Default for Boolector {
    fn default() -> Self {
        Self::new()
    }
}

impl SmtSolver for Boolector {
    fn smt_options() -> &'static str {
        "(set-option :incremental true)\n(set-option :produce-models true)\n"
    }
}

impl Solver for Boolector {
    fn name() -> &'static str {
        "Boolector"
    }

    fn solve_impl<F: Formula>(&self, formula: &F) -> Result<Option<Assignment>, SolverError> {
        let solver = Rc::new(Btor::new());
        solver.set_opt(BtorOption::ModelGen(ModelGen::All));
        solver.set_opt(BtorOption::Incremental(true));
        solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2));

        let mut bvs = HashMap::new();
        let bv = traverse(formula, formula.root(), &solver, &mut bvs);
        bv.slice(0, 0).assert();

        match solver.sat() {
            SolverResult::Sat => {
                let assignments = formula
                    .symbol_ids()
                    .filter_map(|i| {
                        bvs.get(&i).map(|bv| {
                            (
                                i,
                                BitVector(
                                    bv.get_a_solution()
                                        .as_u64()
                                        .expect("BV always fits in 64 bits for our machine"),
                                ),
                            )
                        })
                    })
                    .collect();

                Ok(Some(assignments))
            }
            SolverResult::Unsat => Ok(None),
            SolverResult::Unknown => Err(SolverError::SatUnknown),
        }
    }
}

fn traverse<'a, F: Formula>(
    formula: &F,
    sym: SymbolId,
    solver: &'a Rc<Btor>,
    bvs: &mut HashMap<SymbolId, BV<Rc<Btor>>>,
) -> BV<Rc<Btor>> {
    let bv =
        match &formula[sym] {
            Operator(op) => match formula.operands(sym) {
                (lhs, Some(rhs)) => match op {
                    BVOperator::Add => traverse(formula, lhs, solver, bvs)
                        .add(&traverse(formula, rhs, solver, bvs)),
                    BVOperator::Sub => traverse(formula, lhs, solver, bvs)
                        .sub(&traverse(formula, rhs, solver, bvs)),
                    BVOperator::Mul => traverse(formula, lhs, solver, bvs)
                        .mul(&traverse(formula, rhs, solver, bvs)),
                    BVOperator::Equals => traverse(formula, lhs, solver, bvs)
                        ._eq(&traverse(formula, rhs, solver, bvs))
                        .uext(63),
                    BVOperator::BitwiseAnd => traverse(formula, lhs, solver, bvs)
                        .and(&traverse(formula, rhs, solver, bvs)),
                    BVOperator::Divu => traverse(formula, lhs, solver, bvs)
                        .udiv(&traverse(formula, rhs, solver, bvs)),
                    BVOperator::Remu => traverse(formula, lhs, solver, bvs)
                        .urem(&traverse(formula, rhs, solver, bvs)),
                    BVOperator::Sltu => traverse(formula, lhs, solver, bvs)
                        .ult(&traverse(formula, rhs, solver, bvs))
                        .uext(63),
                    i => unreachable!("binary operator: {:?}", i),
                },
                (lhs, None) => match op {
                    BVOperator::Not => traverse(formula, lhs, solver, bvs)
                        ._eq(&BV::from_u64(solver.clone(), 0, 64))
                        .uext(63),
                    i => unreachable!("unary operator: {:?}", i),
                },
            },
            Input(name) => {
                if let Some(value) = bvs.get(&sym) {
                    value.clone()
                } else {
                    // input names are not unique in the formula, but symbol-ids are unique
                    BV::new(
                        solver.clone(),
                        64,
                        Some(format!("x{}: {}", sym, name).as_str()),
                    )
                }
            }
            Constant(c) => BV::from_u64(solver.clone(), (*c).0, 64),
        };

    bvs.insert(sym, bv.clone());
    bv
}