diff --git a/examples/assume.rs b/examples/assume.rs
index 429372d3d11abcb1c6db9b477c2596724afae407..9727a3e1c8d7b6205faddaa27ec03ef39d5aea9a 100644
--- a/examples/assume.rs
+++ b/examples/assume.rs
@@ -8,23 +8,23 @@ extern crate panic_abort;
#[no_mangle]
fn main() {
- let mut a: u32 = 0;
- let mut b: u32 = 0;
+ let mut a: u32 = 0;
+ let mut b: u32 = 0;
- klee::ksymbol!(&mut a, "a");
- klee::ksymbol!(&mut b, "b");
+ klee::ksymbol!(&mut a, "a");
+ klee::ksymbol!(&mut b, "b");
- let mut c = 0;
- if a > 10 {
- c += 1;
- }
- // klee::kassume(b > 0);
- let v = a + b;
+ let mut c = 0;
+ if a > 10 {
+ c += 1;
+ }
+ // klee::kassume(b > 0);
+ let v = a + b;
- unsafe {
- core::ptr::read_volatile(&a);
- core::ptr::read_volatile(&b);
- core::ptr::read_volatile(&v);
- core::ptr::read_volatile(&c);
- }
+ unsafe {
+ core::ptr::read_volatile(&a);
+ core::ptr::read_volatile(&b);
+ core::ptr::read_volatile(&v);
+ core::ptr::read_volatile(&c);
+ }
}
diff --git a/examples/concurrent.rs b/examples/concurrent.rs
index 1552def793c75002b0d5783206926a504140d1b9..000bcab7a94c4ee04dc5f339794c4a3f7c1835ae 100644
--- a/examples/concurrent.rs
+++ b/examples/concurrent.rs
@@ -11,24 +11,24 @@ use volatile_register::{RO, RW, WO};
#[no_mangle]
fn main() {
- let rw: RW<u32> = unsafe { core::mem::uninitialized() };
- let ro: RO<u32> = unsafe { core::mem::uninitialized() };
- let wo: WO<u32> = unsafe { core::mem::uninitialized() };
+ let rw: RW<u32> = unsafe { core::mem::uninitialized() };
+ let ro: RO<u32> = unsafe { core::mem::uninitialized() };
+ let wo: WO<u32> = unsafe { core::mem::uninitialized() };
- unsafe { wo.write(2) };
+ unsafe { wo.write(2) };
+ if rw.read() == 0 {
+ unsafe {
+ rw.write(0);
+ }
if rw.read() == 0 {
- unsafe {
- rw.write(0);
- }
- if rw.read() == 0 {
- panic!();
- }
+ panic!();
}
+ }
+ if ro.read() == 0 {
if ro.read() == 0 {
- if ro.read() == 0 {
- panic!();
- }
+ panic!();
}
+ }
}
diff --git a/examples/eq.rs b/examples/eq.rs
index a881738d0cda0d7333d0a572b54b25425c3f4118..59600a57a92b97974bb95470e0231a5ff2220662 100644
--- a/examples/eq.rs
+++ b/examples/eq.rs
@@ -136,7 +136,11 @@ fn main() {
}
}
-fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
+fn periodic(
+ STATE: &mut State,
+ TIMEOUT_CNTR: &mut u32,
+ data: &Data,
+) {
*STATE = match STATE {
S8000 => match (data.a, data.b) {
(F, F) => S8001,
@@ -163,8 +167,12 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
_ => {
*TIMEOUT_CNTR -= 1;
match (data.a, data.b) {
- (F, _) => S8001,
- (_, T) => S8000,
+ (F, F) => S8001,
+ (F, T) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8014
+ }
+ (T, T) => S8000,
_ => S8004,
}
}
@@ -174,8 +182,12 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
_ => {
*TIMEOUT_CNTR -= 1;
match (data.a, data.b) {
- (_, F) => S8001,
- (T, _) => S8000,
+ (F, F) => S8001,
+ (T, F) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8004
+ }
+ (T, T) => S8000,
_ => S8014,
}
}
diff --git a/examples/model.rs b/examples/model.rs
index 66fcab18fb956dc7d21d9273a0edf900280581b9..141e9d7cf4b0da172b58f74418e52f5e361b8feb 100644
--- a/examples/model.rs
+++ b/examples/model.rs
@@ -10,35 +10,38 @@ extern crate volatile_register;
use volatile_register::RW;
struct Device<'a> {
- ptr: &'a RW<u32>,
+ ptr: &'a RW<u32>,
}
// HW model.
// The register holds values 0..31
impl<'a> Device<'a> {
- pub fn read(&self) -> u32 {
- let v = self.ptr.read();
- klee::kassume(v < 32);
- v
- }
- pub unsafe fn write(&self, v: u32) {
- klee::kassert!(v < 32);
- let v = self.ptr.write(v);
- }
+ pub fn read(&self) -> u32 {
+ let v = self.ptr.read();
+ klee::kassume(v < 32);
+ v
+ }
+ pub unsafe fn write(
+ &self,
+ v: u32,
+ ) {
+ klee::kassert!(v < 32);
+ let v = self.ptr.write(v);
+ }
}
#[no_mangle]
fn main() {
- let reg = unsafe { core::mem::uninitialized() };
- let device = Device { ptr: ® };
+ let reg = unsafe { core::mem::uninitialized() };
+ let device = Device { ptr: ® };
- let v = device.read();
- if v > 5 {
- unsafe {
- device.write(v - 1);
- }
- if device.read() == v - 1 {
- panic!();
- }
+ let v = device.read();
+ if v > 5 {
+ unsafe {
+ device.write(v - 1);
+ }
+ if device.read() == v - 1 {
+ panic!();
}
+ }
}
diff --git a/examples/model2.rs b/examples/model2.rs
index 9cc479c4e999e399273a1e75ff1205234c5ab746..b3842f029c6bfdb1d1508162c1e0736f34e8b604 100644
--- a/examples/model2.rs
+++ b/examples/model2.rs
@@ -14,15 +14,18 @@ use volatile_register::RW;
struct RegA(RW<u32>);
impl RegA {
- pub fn read(&self) -> u32 {
- let v = self.0.read();
- klee::kassume(v < 32);
- v
- }
- pub unsafe fn write(&self, v: u32) {
- klee::kassert!(v < 32);
- let v = self.0.write(v);
- }
+ pub fn read(&self) -> u32 {
+ let v = self.0.read();
+ klee::kassume(v < 32);
+ v
+ }
+ pub unsafe fn write(
+ &self,
+ v: u32,
+ ) {
+ klee::kassert!(v < 32);
+ let v = self.0.write(v);
+ }
}
// model RegB
@@ -31,40 +34,43 @@ struct RegB(RW<u32>);
static mut STATE: u32 = 0; // reset value
impl RegB {
- pub fn read(&self) -> u32 {
- unsafe {
- STATE += 1;
- STATE
- }
- }
- pub unsafe fn write(&self, v: u32) {
- STATE = v;
+ pub fn read(&self) -> u32 {
+ unsafe {
+ STATE += 1;
+ STATE
}
+ }
+ pub unsafe fn write(
+ &self,
+ v: u32,
+ ) {
+ STATE = v;
+ }
}
#[no_mangle]
fn main() {
- let reg_a: RegA = unsafe { core::mem::uninitialized() };
- let reg_b: RegB = unsafe { core::mem::uninitialized() };
+ let reg_a: RegA = unsafe { core::mem::uninitialized() };
+ let reg_b: RegB = unsafe { core::mem::uninitialized() };
- unsafe {
- reg_b.write(0);
- }
+ unsafe {
+ reg_b.write(0);
+ }
- let t1 = reg_b.read();
- let t2 = reg_b.read();
+ let t1 = reg_b.read();
+ let t2 = reg_b.read();
- let diff = 100 / (t2 - t1);
+ let diff = 100 / (t2 - t1);
- klee::kassert!(t2 > t1);
+ klee::kassert!(t2 > t1);
- let v = reg_a.read();
- if v > 5 {
- unsafe {
- reg_a.write(v - 1);
- }
- if reg_a.read() == v - 1 {
- panic!();
- }
+ let v = reg_a.read();
+ if v > 5 {
+ unsafe {
+ reg_a.write(v - 1);
+ }
+ if reg_a.read() == v - 1 {
+ panic!();
}
+ }
}
diff --git a/examples/model3.rs b/examples/model3.rs
index 39182dd369062109eee63603cfa929db7621178c..ddea1f081d88a5e8c39fde53a4f4fbbb08f38701 100644
--- a/examples/model3.rs
+++ b/examples/model3.rs
@@ -16,41 +16,44 @@ struct RegC(RW<u32>);
static mut OLD_STATE: u32 = 0; // reset value
impl RegC {
- pub fn read(&self) -> u32 {
- let v = self.0.read();
- unsafe {
- // klee::kassume(v - 0xFFFF_FFFC > 0);
- // klee::kassume(v - OLD_STATE > 0);
- // klee::kassert!(v > OLD_STATE);
- klee::kassume(v > OLD_STATE);
-
- OLD_STATE = v;
- }
- v
- }
- pub unsafe fn write(&self, v: u32) {
- OLD_STATE = v;
+ pub fn read(&self) -> u32 {
+ let v = self.0.read();
+ unsafe {
+ // klee::kassume(v - 0xFFFF_FFFC > 0);
+ // klee::kassume(v - OLD_STATE > 0);
+ // klee::kassert!(v > OLD_STATE);
+ klee::kassume(v > OLD_STATE);
+
+ OLD_STATE = v;
}
+ v
+ }
+ pub unsafe fn write(
+ &self,
+ v: u32,
+ ) {
+ OLD_STATE = v;
+ }
}
#[no_mangle]
fn main() {
- let reg_c: RegC = unsafe { core::mem::uninitialized() };
- let mut init: u32 = unsafe { core::mem::uninitialized() };
- klee::ksymbol!(&mut init, "init");
- //klee::kassume(init < 0xFFFF_FFFC);
- //init = 0xFFFF_FFFD;
- unsafe {
- reg_c.write(init);
- }
-
- let t1 = reg_c.read();
- let t2 = reg_c.read();
- // let t3 = reg_c.read();
-
- // let diff = 100 / (t2 - t1);
-
- klee::kassert!(t2 > t1);
- //klee::kassert!(t3 > t2);
- //klee::kassert!(t3 > t1);
+ let reg_c: RegC = unsafe { core::mem::uninitialized() };
+ let mut init: u32 = unsafe { core::mem::uninitialized() };
+ klee::ksymbol!(&mut init, "init");
+ //klee::kassume(init < 0xFFFF_FFFC);
+ //init = 0xFFFF_FFFD;
+ unsafe {
+ reg_c.write(init);
+ }
+
+ let t1 = reg_c.read();
+ let t2 = reg_c.read();
+ // let t3 = reg_c.read();
+
+ // let diff = 100 / (t2 - t1);
+
+ klee::kassert!(t2 > t1);
+ //klee::kassert!(t3 > t2);
+ //klee::kassert!(t3 > t1);
}
diff --git a/examples/model4.rs b/examples/model4.rs
index 8e0b6cc0ef96ba26506d2470124b65fda4a0f76b..e1de24820c951f5ab69606845b191344afe0ad3f 100644
--- a/examples/model4.rs
+++ b/examples/model4.rs
@@ -16,33 +16,36 @@ struct RegC(RW<u32>);
static mut OLD_STATE: u32 = 0; // reset value, cannot be symbolic (awaiting const eval)
impl RegC {
- pub fn read(&self) -> u32 {
- let v = self.0.read(); // to get a symbolic value
- klee::kassume(v > 0); // to ensure that the value is positive
- unsafe {
- if (OLD_STATE as u64 + v as u64) < 0x1_0000_0000 {
- OLD_STATE += v
- }
- OLD_STATE
- }
- }
-
- pub unsafe fn write(&self, v: u32) {
- OLD_STATE = v;
+ pub fn read(&self) -> u32 {
+ let v = self.0.read(); // to get a symbolic value
+ klee::kassume(v > 0); // to ensure that the value is positive
+ unsafe {
+ if (OLD_STATE as u64 + v as u64) < 0x1_0000_0000 {
+ OLD_STATE += v
+ }
+ OLD_STATE
}
+ }
+
+ pub unsafe fn write(
+ &self,
+ v: u32,
+ ) {
+ OLD_STATE = v;
+ }
}
#[no_mangle]
fn main() {
- let reg_c: RegC = unsafe { core::mem::uninitialized() };
- let mut init: u32 = unsafe { core::mem::uninitialized() };
- klee::ksymbol!(&mut init, "init");
- unsafe {
- reg_c.write(init); // to ensure that the initial value is symbolic
- }
-
- let t1 = reg_c.read();
- // let t2 = reg_c.read();
- let c = 100 / (t1 - init);
- // klee::kassert!(t2 > t1);
+ let reg_c: RegC = unsafe { core::mem::uninitialized() };
+ let mut init: u32 = unsafe { core::mem::uninitialized() };
+ klee::ksymbol!(&mut init, "init");
+ unsafe {
+ reg_c.write(init); // to ensure that the initial value is symbolic
+ }
+
+ let t1 = reg_c.read();
+ // let t2 = reg_c.read();
+ let c = 100 / (t1 - init);
+ // klee::kassert!(t2 > t1);
}
diff --git a/rustfmt.toml b/rustfmt.toml
new file mode 100644
index 0000000000000000000000000000000000000000..1ddeb658d764278f694accb9ac0178ae0522e720
--- /dev/null
+++ b/rustfmt.toml
@@ -0,0 +1,2 @@
+tab_spaces = 2
+fn_args_density = "Vertical"
diff --git a/src/main.rs b/src/main.rs
index 1ee0085e4262e17e0b3946ddabda7dc40862afba..6f3432e1a3ea57d12b365415f45120f9a3fae4d0 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -5,78 +5,78 @@ use klee::{kassert, ksymbol};
#[no_mangle]
fn main() {
- let mut DATA: [Data; (DISCREPENCY + 1) as usize] = unsafe { core::mem::uninitialized() };
- ksymbol!(&mut DATA, "DATA");
+ let mut DATA: [Data; (DISCREPENCY + 1) as usize] = unsafe { core::mem::uninitialized() };
+ ksymbol!(&mut DATA, "DATA");
- let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
- ksymbol!(&mut TIMEOUT_CNTR, "TIMEOUT_CNTR");
+ let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+ ksymbol!(&mut TIMEOUT_CNTR, "TIMEOUT_CNTR");
- let mut STATE_HISTORY: [State; (DISCREPENCY + 1) as usize] =
- unsafe { core::mem::uninitialized() };
+ let mut STATE_HISTORY: [State; (DISCREPENCY + 1) as usize] =
+ unsafe { core::mem::uninitialized() };
- DATA[0] = Data { a: false, b: false };
- TIMEOUT_CNTR = 0;
- let mut STATE = S8001;
+ DATA[0] = Data { a: false, b: false };
+ TIMEOUT_CNTR = 0;
+ let mut STATE = S8001;
- for i in 0..(DISCREPENCY + 1) as usize {
- periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
+ for i in 0..(DISCREPENCY + 1) as usize {
+ periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
- // invariants
- // S8000 -> a & b
- if STATE == S8000 {
- kassert!(DATA[i].a & DATA[i].b);
- }
- // !a | !b -> ! S8000
- if !DATA[i].a | !DATA[i].b {
- kassert!(!(STATE == S8000));
- }
- // S8001 -> !a & !b
- if STATE == S8001 {
- kassert!(!DATA[i].a | !DATA[i].b);
- }
- // !a & !b -> S8001
- if !DATA[i].a & !DATA[i].b {
- kassert!(STATE == S8001);
- }
+ // invariants
+ // S8000 -> a & b
+ if STATE == S8000 {
+ kassert!(DATA[i].a & DATA[i].b);
+ }
+ // !a | !b -> ! S8000
+ if !DATA[i].a | !DATA[i].b {
+ kassert!(!(STATE == S8000));
+ }
+ // S8001 -> !a & !b
+ if STATE == S8001 {
+ kassert!(!DATA[i].a | !DATA[i].b);
+ }
+ // !a & !b -> S8001
+ if !DATA[i].a & !DATA[i].b {
+ kassert!(STATE == S8001);
+ }
- // error states implies timeout
- match STATE {
- C001 | C002 | C002 => kassert!(TIMEOUT_CNTR == 0),
- _ => {}
- }
+ // error states implies timeout
+ match STATE {
+ C001 | C002 | C002 => kassert!(TIMEOUT_CNTR == 0),
+ _ => {}
+ }
- if i > 0 {
- match STATE_HISTORY[i - 1] {
- C001 | C002 | C003 | S8005 => {
- kassert!(!(STATE == S8000));
- }
- _ => {
- if DATA[i].a & DATA[i].b {
- kassert!(STATE == S8000);
- }
- }
- }
+ if i > 0 {
+ match STATE_HISTORY[i - 1] {
+ C001 | C002 | C003 | S8005 => {
+ kassert!(!(STATE == S8000));
+ }
+ _ => {
+ if DATA[i].a & DATA[i].b {
+ kassert!(STATE == S8000);
+ }
}
- STATE_HISTORY[i] = STATE;
+ }
}
+ STATE_HISTORY[i] = STATE;
+ }
}
#[derive(Debug, Copy, Clone)]
pub struct Data {
- a: bool,
- b: bool,
+ a: bool,
+ b: bool,
}
#[derive(Debug, Copy, Clone, PartialEq)]
pub enum State {
- S8000,
- S8001,
- S8004,
- S8014,
- S8005,
- C001,
- C002,
- C003,
+ S8000,
+ S8001,
+ S8004,
+ S8014,
+ S8005,
+ C001,
+ C002,
+ C003,
}
use State::*;
@@ -85,73 +85,77 @@ const DISCREPENCY: u32 = 4;
const T: bool = true;
const F: bool = false;
-fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
- // we start directly in the init state S80001
- // static mut STATE: State = State::S8001;
- // static mut TIMEOUT_CNTR: u32 = 0;
-
- let data = DATA;
-
- *STATE = match STATE {
- S8000 => match (data.a, data.b) {
- (F, F) => S8001,
- (F, T) | (T, F) => {
- *TIMEOUT_CNTR = DISCREPENCY;
- S8005
- }
- (T, T) => S8000,
- },
- S8001 => match (data.a, data.b) {
- (F, F) => S8001,
- (F, T) => {
- *TIMEOUT_CNTR = DISCREPENCY;
- S8014
- }
- (T, F) => {
- *TIMEOUT_CNTR = DISCREPENCY;
- S8004
- }
- (T, T) => S8000,
+fn periodic(
+ STATE: &mut State,
+ TIMEOUT_CNTR: &mut u32,
+ DATA: &mut Data,
+) {
+ // we start directly in the init state S80001
+ // static mut STATE: State = State::S8001;
+ // static mut TIMEOUT_CNTR: u32 = 0;
+
+ let data = DATA;
+
+ *STATE = match STATE {
+ S8000 => match (data.a, data.b) {
+ (F, F) => S8001,
+ (F, T) | (T, F) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8005
+ }
+ (T, T) => S8000,
+ },
+ S8001 => match (data.a, data.b) {
+ (F, F) => S8001,
+ (F, T) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8014
+ }
+ (T, F) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8004
+ }
+ (T, T) => S8000,
+ },
+ S8004 => {
+ *TIMEOUT_CNTR -= 1;
+ match *TIMEOUT_CNTR {
+ 0 => C001,
+ _ => match (data.a, data.b) {
+ (F, _) => S8001,
+ (_, T) => S8000,
+ _ => S8004,
},
- S8004 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C001,
- _ => match (data.a, data.b) {
- (F, _) => S8001,
- (_, T) => S8000,
- _ => S8004,
- },
- }
- }
- S8014 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C002,
- _ => match (data.a, data.b) {
- (_, F) => S8001,
- (T, _) => S8000,
- _ => S8014,
- },
- }
- }
- S8005 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C003,
- _ => match (data.a, data.b) {
- (F, F) => S8001,
- _ => S8005,
- },
- }
- }
- C001 | C002 => match (data.a, data.b) {
- (F, F) => S8001,
- _ => *STATE,
+ }
+ }
+ S8014 => {
+ *TIMEOUT_CNTR -= 1;
+ match *TIMEOUT_CNTR {
+ 0 => C002,
+ _ => match (data.a, data.b) {
+ (_, F) => S8001,
+ (T, _) => S8000,
+ _ => S8014,
},
- C003 => match (data.a, data.b) {
- (F, F) => S8001,
- _ => C003,
+ }
+ }
+ S8005 => {
+ *TIMEOUT_CNTR -= 1;
+ match *TIMEOUT_CNTR {
+ 0 => C003,
+ _ => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => S8005,
},
- };
+ }
+ }
+ C001 | C002 => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => *STATE,
+ },
+ C003 => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => C003,
+ },
+ };
}