diff --git a/Cargo.toml b/Cargo.toml index fe1ac0f..8887b8f 100644 --- a/Cargo.toml +++ b/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"] } diff --git a/inputs/const_array_example.btor b/inputs/const_array_example.btor new file mode 100644 index 0000000..5e188f5 --- /dev/null +++ b/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 + diff --git a/src/btor2/mod.rs b/src/btor2/mod.rs index 2ea035f..22b6354 100644 --- a/src/btor2/mod.rs +++ b/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}; diff --git a/src/btor2/parse.rs b/src/btor2/parse.rs index 1a38004..426f250 100644 --- a/src/btor2/parse.rs +++ b/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(); diff --git a/src/btor2/witness.rs b/src/btor2/witness.rs index 5d56dc7..996b431 100644 --- a/src/btor2/witness.rs +++ b/src/btor2/witness.rs @@ -2,4 +2,164 @@ // released under BSD 3-Clause License // author: Kevin Laeufer -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 = std::io::Result; + +pub fn parse_witness(input: &mut impl BufRead) -> Result { + let witnesses = parse_witnesses(input, 1)?; + Ok(witnesses.into_iter().next().unwrap()) +} + +pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result> { + 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, 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) { + 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()) + } +} diff --git a/src/mc/mod.rs b/src/mc/mod.rs index ba97079..0b46e9e 100644 --- a/src/mc/mod.rs +++ b/src/mc/mod.rs @@ -2,3 +2,5 @@ // released under BSD 3-Clause License // author: Kevin Laeufer mod state; + +pub use state::{State, Value, ValueRef, Witness}; diff --git a/src/mc/state.rs b/src/mc/state.rs index d45a0d2..81cb0ff 100644 --- a/src/mc/state.rs +++ b/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, + pub inputs: Vec, + /// Index of all safety properties (bad state predicates) that are violated by this witness. + pub failed_safety: Vec, } 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, longs: Vec, @@ -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)] diff --git a/tests/btor2_witness_tests.rs b/tests/btor2_witness_tests.rs new file mode 100644 index 0000000..0f17ec8 --- /dev/null +++ b/tests/btor2_witness_tests.rs @@ -0,0 +1,216 @@ +// Copyright 2023 The Regents of the University of California +// released under BSD 3-Clause License +// author: Kevin Laeufer + +use libpatron::btor2; + +#[test] +fn test_no_state_witness() { + let _wit = btor2::parse_witness(&mut NO_STATE.as_bytes()).unwrap(); +} + +#[test] +fn test_fsm_witness() { + let _wit = btor2::parse_witness(&mut FSM.as_bytes()).unwrap(); +} + +#[test] +fn test_const_array_example_witness() { + let _wit = btor2::parse_witness(&mut CONST_ARRAY_EXAMPLE.as_bytes()).unwrap(); +} + +#[test] +fn test_multiple_witnesses() { + let _wit = btor2::parse_witness(&mut MULTIPLE.as_bytes()).unwrap(); + let _wits = btor2::parse_witnesses(&mut MULTIPLE.as_bytes(), 30).unwrap(); +} + +const NO_STATE: &str = r#" +sat +b0 +@0 +0 0 reset@0 +1 11111011 a@0 +2 00000101 b@0 +. + +"#; + +const FSM: &str = r#" +sat +b0 +#0 +0 00 state#0 +@0 +0 1 reset@0 +1 1 in@0 +@1 +0 0 reset@1 +1 1 in@1 +. + +"#; + +/// Witness obtained by running `btormc const_array_example.btor` +const CONST_ARRAY_EXAMPLE: &str = r#" +sat +b0 +#0 +0 11111 addr#0 +1 11111111111111111111111111111111 data#0 +2 [11111] 11111111111111111111111111111110 mem@0 +4 11111 a#0 +@0 +. +"#; + +const MULTIPLE: &str = r#" +sat +b0 +#0 +0 0 state0#0 +2 0 state2#0 +3 0 state3#0 +4 0 state4#0 +6 1 state6#0 +7 0 state7#0 +8 0 state8#0 +9 0 state9#0 +10 0 state10#0 +11 0 state11#0 +12 1 state12#0 +@0 +0 0 clock@0 +1 1 in@0 +2 1 reset@0 +#1 +8 0 state8#1 +9 0 state9#1 +10 0 state10#1 +11 0 state11#1 +12 0 state12#1 +@1 +0 0 clock@1 +1 0 in@1 +2 0 reset@1 +#2 +8 0 state8#2 +9 0 state9#2 +10 0 state10#2 +11 0 state11#2 +12 0 state12#2 +@2 +0 0 clock@2 +1 0 in@2 +2 0 reset@2 +. +sat +b1 +#0 +0 0 state0#0 +2 0 state2#0 +3 0 state3#0 +4 0 state4#0 +6 1 state6#0 +7 0 state7#0 +8 0 state8#0 +9 0 state9#0 +10 0 state10#0 +11 0 state11#0 +12 1 state12#0 +@0 +0 0 clock@0 +1 1 in@0 +2 1 reset@0 +#1 +8 0 state8#1 +9 0 state9#1 +10 0 state10#1 +11 0 state11#1 +12 0 state12#1 +@1 +0 0 clock@1 +1 1 in@1 +2 0 reset@1 +#2 +8 0 state8#2 +9 0 state9#2 +10 0 state10#2 +11 0 state11#2 +12 0 state12#2 +@2 +0 0 clock@2 +1 0 in@2 +2 0 reset@2 +#3 +8 0 state8#3 +9 0 state9#3 +10 0 state10#3 +11 0 state11#3 +12 0 state12#3 +@3 +0 0 clock@3 +1 0 in@3 +2 0 reset@3 +. +sat +b2 +#0 +0 0 state0#0 +2 0 state2#0 +3 0 state3#0 +4 0 state4#0 +6 1 state6#0 +7 0 state7#0 +8 0 state8#0 +9 0 state9#0 +10 0 state10#0 +11 0 state11#0 +12 1 state12#0 +@0 +0 0 clock@0 +1 1 in@0 +2 1 reset@0 +#1 +8 0 state8#1 +9 0 state9#1 +10 0 state10#1 +11 0 state11#1 +12 0 state12#1 +@1 +0 0 clock@1 +1 1 in@1 +2 0 reset@1 +#2 +8 0 state8#2 +9 0 state9#2 +10 0 state10#2 +11 0 state11#2 +12 1 state12#2 +@2 +0 0 clock@2 +1 1 in@2 +2 0 reset@2 +#3 +8 0 state8#3 +9 0 state9#3 +10 0 state10#3 +11 0 state11#3 +12 0 state12#3 +@3 +0 0 clock@3 +1 0 in@3 +2 0 reset@3 +#4 +8 0 state8#4 +9 0 state9#4 +10 0 state10#4 +11 0 state11#4 +12 0 state12#4 +@4 +0 0 clock@4 +1 0 in@4 +2 0 reset@4 +. + +"#;