wip: witness parser

Cargo.toml

@@ -18,6 +18,7 @@ codespan-reporting = "0.11.1"
 fuzzy-matcher = "0.3.7"
 lazy_static = "1.4.0"
 num-bigint = "0.4.4"
+num-traits = "0.2.17"
 
 [dev-dependencies]
 clap =  { version = "4.4.8", features = ["derive"] }

inputs/const_array_example.btor

@@ -0,0 +1,36 @@
+1 sort bitvec 1
+5 sort bitvec 5
+23 sort bitvec 32
+
+; Symbolic Constant: addr
+121 state 5 addr
+122 next 5 121 121
+
+; Symbolic Constant: data
+123 state 23 data
+124 next 23 123 123
+
+; Symbolic Constant: mem
+125 sort array 5 23
+126 state 125 mem
+127 next 125 126 126
+
+; mem[addr := data]
+148 write 125 126 121 123
+
+; mem_n = mem[addr := data]
+155 state 125 mem_n
+156 init 125 155 148
+157 next 125 155 155
+
+; bad: mem_n[a] != mem[a]
+
+; Symbolic Constant: a
+200 state 5 a
+201 next 5 200 200
+
+210 read 23 126 200
+211 read 23 155 200
+212 neq 1 210 211
+213 bad 212
+

src/btor2/mod.rs

@@ -7,3 +7,4 @@ mod witness;
 
 pub use parse::{parse_file, parse_str};
 pub use serialize::{serialize, serialize_to_str};
+pub use witness::{parse_witness, parse_witnesses};

src/btor2/parse.rs

@@ -682,13 +682,13 @@ impl<'a> Parser<'a> {
 
 // Line Tokenizer
 #[derive(Default, Debug)]
-struct LineTokens<'a> {
-    tokens: SmallVec<[&'a str; 4]>,
-    comment: Option<&'a str>,
+pub(crate) struct LineTokens<'a> {
+    pub(crate) tokens: SmallVec<[&'a str; 4]>,
+    pub(crate) comment: Option<&'a str>,
 }
 
 const NO_TOKEN: usize = usize::MAX;
-fn tokenize_line(line: &str) -> LineTokens {
+pub(crate) fn tokenize_line(line: &str) -> LineTokens {
     if line.is_empty() {
         // special handling for empty lines
         return LineTokens::default();

src/btor2/witness.rs

@@ -2,4 +2,164 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <[email protected]>
 
-pub fn parse_witness() {}
+use crate::btor2::parse::tokenize_line;
+use crate::mc::{State, Value, Witness};
+use num_bigint::BigUint;
+use num_traits::Num;
+use std::io::BufRead;
+
+enum ParserState {
+    Start,
+    WaitForProp,
+    WaitForFrame,
+    ParsingStatesAt(u64),
+    ParsingInputsAt(u64),
+    Done,
+}
+
+type Result<T> = std::io::Result<T>;
+
+pub fn parse_witness(input: &mut impl BufRead) -> Result<Witness> {
+    let witnesses = parse_witnesses(input, 1)?;
+    Ok(witnesses.into_iter().next().unwrap())
+}
+
+pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result<Vec<Witness>> {
+    let mut state = ParserState::Start;
+    let mut out = Vec::with_capacity(1);
+    let mut wit = Witness::default();
+    let mut inputs = State::default();
+
+    let finish_witness = |out: &mut Vec<Witness>, wit: &mut Witness| {
+        out.push(std::mem::replace(wit, Witness::default()));
+        if out.len() >= parse_max {
+            ParserState::Done
+        } else {
+            ParserState::Start
+        }
+    };
+    let start_inputs = |line: &str, wit: &Witness| {
+        let at = u64::from_str_radix(&line[1..], 10).unwrap();
+        assert_eq!(at as usize, wit.inputs.len());
+        ParserState::ParsingInputsAt(at)
+    };
+    let finish_inputs = |wit: &mut Witness, inputs: &mut State| {
+        wit.inputs.push(std::mem::replace(inputs, State::default()));
+    };
+    let start_state = |line: &str| {
+        let at = u64::from_str_radix(&line[1..], 10).unwrap();
+        ParserState::ParsingStatesAt(at)
+    };
+
+    for line_res in input.lines() {
+        let full_line = line_res?;
+        let line = full_line.trim();
+        if line.is_empty() || line.starts_with(";") {
+            continue; // skip blank lines and comments
+        }
+
+        state = match state {
+            ParserState::Start => {
+                assert_eq!(
+                    line, "sat",
+                    "Expected witness header to be `sat`, not `{}`",
+                    line
+                );
+                ParserState::WaitForProp
+            }
+            ParserState::Done => break,
+            ParserState::WaitForProp => {
+                let tok = tokenize_line(line);
+                for token in tok.tokens {
+                    if token.starts_with("b") {
+                        let num = u32::from_str_radix(&token[1..], 10).unwrap();
+                        wit.failed_safety.push(num);
+                    } else if token.starts_with("j") {
+                        panic!("justice props are not supported");
+                    } else {
+                        panic!("unexpected property token: {}", token);
+                    }
+                }
+                ParserState::WaitForFrame
+            }
+            ParserState::WaitForFrame => {
+                if line.starts_with("@") {
+                    // no state initialization frame -> jump straight to inputs
+                    start_inputs(line, &wit)
+                } else {
+                    assert_eq!(line, "#0", "Expected initial state frame, not: {}", line);
+                    start_state(line)
+                }
+            }
+            ParserState::ParsingStatesAt(at) => {
+                if line == "." {
+                    let next = finish_witness(&mut out, &mut wit);
+                    if out.len() >= parse_max {
+                        break;
+                    }
+                    next
+                } else if line.starts_with("@") {
+                    start_inputs(line, &wit)
+                } else {
+                    let tok = tokenize_line(line);
+                    let (ii, _, data, index) = parse_assignment(&tok.tokens);
+                    println!("TODO: {ii} = {data:?}");
+                    // continue reading in state
+                    ParserState::ParsingStatesAt(at)
+                }
+            }
+            ParserState::ParsingInputsAt(at) => {
+                if line == "." {
+                    finish_inputs(&mut wit, &mut inputs);
+                    finish_witness(&mut out, &mut wit)
+                } else if line.starts_with("@") {
+                    finish_inputs(&mut wit, &mut inputs);
+                    start_inputs(line, &wit)
+                } else if line.starts_with("#") {
+                    finish_inputs(&mut wit, &mut inputs);
+                    start_state(line)
+                } else {
+                    let tok = tokenize_line(line);
+                    let (ii, _, data, index) = parse_assignment(&tok.tokens);
+                    println!("TODO: {ii} = {data:?}");
+                    // continue reading in inputs
+                    ParserState::ParsingInputsAt(at)
+                }
+            }
+        };
+    }
+
+    Ok(out)
+}
+
+fn parse_assignment<'a>(tokens: &'a [&'a str]) -> (u64, &'a str, Value, Option<Value>) {
+    let is_array = match tokens.len() {
+        3 => false, // its a bit vector
+        4 => true,
+        _ => panic!(
+            "Expected assignment to consist of 3-4 parts, not: {:?}",
+            tokens
+        ),
+    };
+    // index of the state or input
+    let index = u64::from_str_radix(tokens[0], 10).unwrap();
+    let name = *tokens.last().unwrap();
+    let (value, array_index) = if is_array {
+        let index_str = tokens[1];
+        assert!(index_str.starts_with("[") && index_str.ends_with("]"));
+        let array_index = parse_bit_vec(&index_str[1..index_str.len() - 1]);
+        (parse_bit_vec(tokens[2]), Some(array_index))
+    } else {
+        (parse_bit_vec(tokens[1]), None)
+    };
+    (index, name, value, array_index)
+}
+
+/// parses a string of 1s and 0s into a value.
+fn parse_bit_vec(value: &str) -> Value {
+    if value.len() <= 64 {
+        Value::Long(u64::from_str_radix(value, 2).unwrap())
+    } else {
+        Value::Big(BigUint::from_str_radix(value, 2).unwrap())
+    }
+}

src/mc/mod.rs

@@ -2,3 +2,5 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <[email protected]>
 mod state;
+
+pub use state::{State, Value, ValueRef, Witness};

src/mc/state.rs

@@ -6,11 +6,14 @@ use crate::ir::Type;
 use num_bigint::BigUint;
 
 /// 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.
-    init: State,
+    pub init: State,
     /// The inputs over time. Each entry contains an optional value for each input.
-    inputs: Vec<State>,
+    pub inputs: Vec<State>,
+    /// Index of all safety properties (bad state predicates) that are violated by this witness.
+    pub failed_safety: Vec<u32>,
 }
 
 impl Witness {
@@ -44,6 +47,7 @@ fn smt_tpe_to_storage_tpe(tpe: Type) -> StorageType {
 }
 
 /// Represents concrete values which can be updated, but state cannot be added once created.
+#[derive(Debug)]
 pub struct State {
     meta: Vec<StorageMetaData>,
     longs: Vec<u64>,
@@ -120,6 +124,10 @@ impl State {
             _ => panic!("Incompatible value for storage type: {:?}", meta.tpe),
         };
     }
+
+    pub fn is_empty(&self) -> bool {
+        self.meta.is_empty()
+    }
 }
 
 #[derive(Debug, PartialEq, Clone)]