patronus 0.35.0

Hardware bug-finding toolkit.
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

// Copyright 2023 The Regents of the University of California
// Copyright 2024 Cornell University
// released under BSD 3-Clause License
// author: Kevin Laeufer <laeufer@cornell.edu>

use baa::Value;

#[derive(Debug, Clone, Default)]
pub enum InitValue {
    BitVec(baa::BitVecValue),
    /// For arrays we store the array data + the entries that are relevant.
    Array(baa::ArrayValue, Vec<baa::BitVecValue>),
    /// No value available
    #[default]
    None,
}

impl TryFrom<InitValue> for Value {
    type Error = ();

    fn try_from(value: InitValue) -> Result<Self, Self::Error> {
        match value {
            InitValue::BitVec(v) => Ok(Value::BitVec(v)),
            InitValue::Array(v, _) => Ok(Value::Array(v)),
            InitValue::None => Err(()),
        }
    }
}

/// Contains the initial state and the inputs over `len` cycles.
#[derive(Debug, Default)]
pub struct Witness {
    /// The starting state. Contains an optional value for each state.
    pub init: Vec<InitValue>,
    /// Optional name for each init value.
    pub init_names: Vec<Option<String>>,
    /// The inputs over time. Each entry contains an optional value for each input.
    pub inputs: Vec<Vec<Option<Value>>>,
    /// Optional name for each input
    pub input_names: Vec<Option<String>>,
    /// Index of all safety properties (bad state predicates) that are violated by this witness.
    pub failed_safety: Vec<u32>,
}