diff --git a/.vscode/tasks.json b/.vscode/tasks.json
index d03517591f05b8587880a0492d4051c58cf560a4..0c7cc26322b96403071ffe9fda0871aefc945de3 100644
--- a/.vscode/tasks.json
+++ b/.vscode/tasks.json
@@ -5,8 +5,8 @@
"tasks": [
{
"type": "shell",
- "label": "cargo +stable run --example example --features debug-fmt",
- "command": "cargo +stable run --example example --features debug-fmt",
+ "label": "cargo build",
+ "command": "cargo build",
"problemMatcher": [
"$rustc"
],
@@ -17,8 +17,8 @@
},
{
"type": "shell",
- "label": "cargo +nightly run --example example2 --features 'debug-fmt nightly'",
- "command": "cargo +nightly run --example example2 --features 'debug-fmt nightly'",
+ "label": "cargo build --all-features",
+ "command": "cargo build --all-features",
"problemMatcher": [
"$rustc"
],
@@ -26,6 +26,6 @@
"kind": "build",
"isDefault": true
}
- }
+ },
]
}
\ No newline at end of file
diff --git a/Cargo.toml b/Cargo.toml
index 769e7d7360b40869f55351668d648bba6e357320..e3180a2c1d782696b2207d452221c1230149f0b4 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -15,15 +15,8 @@ version = "0.3.0"
[dependencies]
vcell = "0.1.0"
-array-debug = { git = "https://gitlab.henriktjader.com/pln/array-debug", optional = true }
+klee = { path = "..", optional = true }
[features]
-debug-fmt = []
-nightly = ["array-debug"]
+klee-analysis = ["klee"]
-[[example]]
-name = "example"
-
-[[example]]
-name = "example2"
-required-features = ["nightly"]
diff --git a/README.md b/README.md
index 216967902047e6b54c722436da325fd66045409b..cea5352cfff135e03fea1962dd2ae7c0b73dafaf 100644
--- a/README.md
+++ b/README.md
@@ -5,90 +5,11 @@
> Volatile access to memory mapped hardware registers
-Adds debug to volatile register when compiled with `--features debug-fmt`.
-
-## Caveats
-
-Notice, the current implementation of `array-debug` (see `examples/example2.rs`) requires a nightly toolchain (`#![feature(unsize)]`). This is however an "opt-in", and needed to support `#[derive(Debug)]` for cases with (register) arrays larger than 32 elements.
-
-
-``` rust
-//! Example to show the use of `Debug` formatting for small register arrays
-//!
-//! > cargo +stable run --example example --features debug-fmt
-//!
-
-extern crate volatile_register;
-use std::mem;
-use volatile_register::{RW};
-
- #[repr(C)]
- #[derive(Debug)]
- pub struct Nvic {
- /// Interrupt Set-Enable
- pub iser: [RW<u32>; 8],
- reserved0: [u32; 24],
- /// Interrupt Clear-Enable
- pub icer: [RW<u32>; 8],
- reserved1: [u32; 24],
- // .. more registers ..
-}
-
-fn main() {
- let r : Nvic = unsafe {mem::uninitialized() };
- println!("{:?}", r);
-}
-```
-
-This will render an output of the form:
-
-``` txt
-Nvic { iser: [0xB618860, 0x7FFE, 0x20, 0x0, 0x0, 0x7F70, 0x30, 0x0], reserved0: [7, 0, 3, 0, 274354200, 22074, 31, 0, 80, 0, 4294967024, 4294967295, 0, 0, 3, 48, 0, 0, 0, 0, 91, 110, 0, 0], icer: [0x77, 0x7C, 0xFFFFFEF0,0xFFFFFFFF, 0xC3041AA0, 0x7F70, 0x20, 0x0], reserved1: [132352, 0, 3271845168, 32624, 274356992, 22074, 1, 0, 3272547558, 32624, 3269993280, 32624, 274357008, 22074, 3272638464, 32624, 252047400, 22074, 3269993088, 32624, 3270237052, 32624, 274356816, 22074] }
-```
-
-Registers will be formatted under `UpperHex`, notice in the example that arrays are of size less than 32, hence `Debug` of array (`[T; N]`) is implemented by default. Notice that the `reserved` fields falls back to the default integer formatting (as not wrapped by the `volatile-register` abstraction).
-
-For register arrays with more then 32 elements, `array-debug` provides a newtype over array, replicating the array behavior while providing `Debug`.
-
-``` rust
-//! Example to show the use of ¡Debug` formatting for big register arrays
-//!
-//! > cargo +nightly run --example example2 --features 'debug-fmt nightly'
-//!
-
-extern crate array_debug;
-extern crate volatile_register;
-
-use array_debug::ArrayDebug;
-use std::mem;
-use volatile_register::RW;
-
-#[repr(C)]
-#[derive(Debug)]
-pub struct Nvic {
- /// Interrupt Set-Enable
- pub iser: ArrayDebug<[RW<u32>; 38], RW<u32>>,
- reserved0: [u32; 24],
- /// Interrupt Clear-Enable
- pub icer: [RW<u32>; 8],
- reserved1: [u32; 24],
- // .. more registers ..
-}
-
-fn main() {
- let r: Nvic = unsafe { mem::uninitialized() };
- println!("{:?}", r);
-}
-```
-
-Rendering output of the form:
-
-``` text
-Nvic { iser: [0x3, 0x30, 0x0, 0x0, 0x0, 0x0, 0x5B, 0x6E, 0x0, 0x0, 0x77, 0x7C, 0x4C6DAEC0, 0x7F95, 0x1F, 0x0, 0x20, 0x0, 0x1, 0x0, 0xFFFFFEF0, 0xFFFFFFFF, 0x0, 0x0, 0x4C65C340, 0x7F95, 0x4C6E2967, 0x7F95, 0x20, 0x0, 0xD7FADB10, 0x7FFF, 0x20, 0x0, 0x0, 0x7F95, 0x30, 0x0], reserved0: [7, 0, 3, 0, 4060155928, 22095, 31, 0, 80, 0, 4294967024, 4294967295, 0, 0, 3, 48, 0, 0, 0, 0, 91, 110, 0, 0], icer: [0x77, 0x7C, 0xFFFFFEF0, 0xFFFFFFFF, 0x4C81BAA0, 0x7F95, 0x20, 0x0], reserved1: [132352, 0, 1283589424, 32661, 4060158720, 22095, 1, 0, 1284291814, 32661, 1281737536, 32661, 4060158736, 22095, 1284382720, 32661, 4038778920, 22095, 1281737344, 32661, 1281981308, 32661, 4060158544, 22095] }
-```
-
## [Documentation](https://docs.rs/crate/volatile-register)
+## Version 0.3.0
+KLEE support making register reads symbolic, enabled by the `klee-analysis` feature.
+
## License
Licensed under either of
diff --git a/src/lib.rs b/src/lib.rs
index c9394d218d8a5852a8f3fb5373d07e9dfee7b431..56680e2ae6ff5d8c19ae000bad5cfff421f4f765 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -26,12 +26,15 @@
//! ```
#![deny(missing_docs)]
+#![deny(warnings)]
#![no_std]
extern crate vcell;
-#[cfg(feature = "debug-fmt")]
-use core::fmt::{self, Debug, UpperHex};
+#[cfg(feature = "klee-analysis")]
+#[macro_use]
+extern crate klee;
+
use vcell::VolatileCell;
/// Read-Only register
@@ -39,19 +42,11 @@ pub struct RO<T>
where
T: Copy,
{
+ #[allow(unused)]
register: VolatileCell<T>,
}
-#[cfg(feature = "debug-fmt")]
-impl<T> fmt::Debug for RO<T>
-where
- T: Copy + Debug + UpperHex,
-{
- fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- write!(f, "{:#X}", self.read())
- }
-}
-
+#[cfg(not(feature = "klee-analysis"))]
impl<T> RO<T>
where
T: Copy,
@@ -63,13 +58,17 @@ where
}
}
-#[cfg(feature = "debug-fmt")]
-impl<T> fmt::Debug for RW<T>
+#[cfg(feature = "klee-analysis")]
+impl<T> RO<T>
where
- T: Copy + Debug + UpperHex,
+ T: Copy,
{
- fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- write!(f, "{:#X}", self.read())
+ /// Reads the symbolic value of the register
+ #[inline(always)]
+ pub fn read(&self) -> T {
+ let mut register: T = unsafe { core::mem::uninitialized() };
+ ksymbol!(&mut register, "register");
+ register
}
}
@@ -81,6 +80,7 @@ where
register: VolatileCell<T>,
}
+#[cfg(not(feature = "klee-analysis"))]
impl<T> RW<T>
where
T: Copy,
@@ -111,24 +111,49 @@ where
}
}
-/// Write-Only register
-pub struct WO<T>
+#[cfg(feature = "klee-analysis")]
+impl<T> RW<T>
where
T: Copy,
{
- register: VolatileCell<T>,
+ /// Performs a read-modify-write operation
+ ///
+ /// NOTE: `unsafe` to keep API consistent,
+ /// in `klee-analysis` the reading side effect is preserved
+ #[inline(always)]
+ pub unsafe fn modify<F>(&self, f: F)
+ where
+ F: FnOnce(T) -> T,
+ {
+ f(self.register.get());
+ }
+
+ /// Reads the symbolic value of the register
+ #[inline(always)]
+ pub fn read(&self) -> T {
+ let mut register: T = unsafe { core::mem::uninitialized() };
+ ksymbol!(&mut register, "register");
+ register
+ }
+
+ /// Writes a `value` into the register
+ ///
+ /// NOTE: `unsafe` to keep API consistent,
+ /// in `klee-analysis` writing has no side effect
+ #[inline(always)]
+ pub unsafe fn write(&self, _value: T) {}
}
-#[cfg(feature = "debug-fmt")]
-impl<T> fmt::Debug for WO<T>
+/// Write-Only register
+pub struct WO<T>
where
- T: Copy + Debug,
+ T: Copy,
{
- fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- write!(f, "- write only -") // TODO: perhaps self.register.get()
- }
+ #[allow(unused)]
+ register: VolatileCell<T>,
}
+#[cfg(not(feature = "klee-analysis"))]
impl<T> WO<T>
where
T: Copy,
@@ -141,3 +166,16 @@ where
self.register.set(value)
}
}
+
+#[cfg(feature = "klee-analysis")]
+impl<T> WO<T>
+where
+ T: Copy,
+{
+ /// Writes `value` into the register
+ ///
+ /// NOTE: `unsafe` to keep API consistent,
+ /// in `klee-analysis` writing has no side effect
+ #[inline(always)]
+ pub unsafe fn write(&self, _value: T) {}
+}