Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
C
cargo-klee
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Mark Hakansson
cargo-klee
Commits
6568c3fc
Commit
6568c3fc
authored
5 years ago
by
Per
Browse files
Options
Downloads
Patches
Plain Diff
examples updated
parent
b196a57b
No related branches found
No related tags found
No related merge requests found
Changes
2
Show whitespace changes
Inline
Side-by-side
Showing
2 changed files
klee-examples/src/peripheral.rs
+105
-6
105 additions, 6 deletions
klee-examples/src/peripheral.rs
klee-examples/src/register.rs
+92
-42
92 additions, 42 deletions
klee-examples/src/register.rs
with
197 additions
and
48 deletions
klee-examples/src/peripheral.rs
+
105
−
6
View file @
6568c3fc
// > cargo klee --bin peripheral -r -k -g -v --release
// ...
// KLEE: done: total instructions = 33
// KLEE: done: completed paths = 1
// KLEE: done: generated tests = 1
//
// The example, has just one path, leading up to an abort.
// The reason is that the progam unconditionally will panic, as
// taking the peripheral is only only allowed once (for soundness).
// (Internally this in tracked by a state variable.)
//
// This is very good news, that KLEE will detect the error at compile time.
//
// Let's remove the error to see if the example code is correct.
// (comment out the second `take`)
//
// > cargo klee --bin peripheral -r -k -g -v --release
//
// KLEE: ERROR: src/peripheral.rs:104: divide by zero
// KLEE: NOTE: now ignoring this error at this location
//
// KLEE: done: total instructions = 85
// KLEE: done: completed paths = 2
// KLEE: done: generated tests = 2
//
//(gdb) shell ls klee-last
// assembly.ll info messages.txt run.istats run.stats test000001.div.err test000001.kquery test000001.ktest test000002.ktest warnings.txt
//
// So we see that test000001.ktest was causing a division error,
// the other test case passed
//
// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
// (gdb) run
// ...
// Program received signal SIGFPE, Arithmetic exception.
// 0x00005555555551b0 in main () at src/peripheral.rs:104
// 104 let some_time_quota = unchecked_div(a, c - b);
//
// Let's look at the actual test
// (gdb) shell ktest-tool klee-last/test000001.ktest
// ktest file : 'klee-last/test000001.ktest'
// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/peripheral-d1d6043ca4c81fef.ll']
// num objects: 5
// object 0: name: 'PRIMASK'
// object 0: size: 4
// object 0: data: b'\x00\x00\x00\x00'
// object 0: hex : 0x00000000
// object 0: int : 0
// object 0: uint: 0
// object 0: text: ....
// object 1: name: 'vcell'
// object 1: size: 4
// object 1: data: b'\x00\x00\x00\x00'
// object 1: hex : 0x00000000
// object 1: int : 0
// object 1: uint: 0
// object 1: text: ....
// object 2: name: 'vcell'
// object 2: size: 4
// object 2: data: b'\x00\x00\x00\x00'
// object 2: hex : 0x00000000
// object 2: int : 0
// object 2: uint: 0
// object 2: text: ....
// object 3: name: 'vcell'
// object 3: size: 4
// object 3: data: b'\x00\x00\x00\x00'
// object 3: hex : 0x00000000
// object 3: int : 0
// object 3: uint: 0
// object 3: text: ....
// object 4: name: 'vcell'
// object 4: size: 4
// object 4: data: b'\x00\x00\x00\x00'
// object 4: hex : 0x00000000
// object 4: int : 0
// object 4: uint: 0
// object 4: text: ....
//
// In order to analyze hardware dependent code, hardware access are treated
// as a new symbolic value. In `cortex-m` we give symbolic names to core peripherals.
// The svd2rust generated PAC is currently given the symbolic name `vcell`. This
// might in the future change to giving the address to the register instead.
//
// A breakdown of the example:
// Behind the scenes the PRIMASK register is accessed, and given concrete value.
// This access is along the happy path towards the error, so any value would
// suffice (in this case 0x00000000 was selected by KLEE).
//
// The first `vcell` access: was done when enabling the cycle counter.
// The rest of accesses stem from reading `a`, `b`, and `c`.
// Critical here is that KLEE spots that `(c - b) = 0`, leading up to a division
// by zero error (satisfied by `c` and `b` set to 0x00000000)
//
// Notice here, that this error is spotted EVEN while we are telling
// Rust to use the primitive (intrinsic) division for performance.
//
#![feature(core_intrinsics)]
// we use intrinsic division
#![no_std]
#![no_std]
#![no_main]
#![no_main]
...
@@ -8,17 +106,18 @@ extern crate cortex_m;
...
@@ -8,17 +106,18 @@ extern crate cortex_m;
use
cortex_m
::
peripheral
::
Peripherals
;
use
cortex_m
::
peripheral
::
Peripherals
;
use
core
::{
intrinsics
::
unchecked_div
,
ptr
::
read_volatile
};
#[no_mangle]
#[no_mangle]
fn
main
()
{
fn
main
()
{
let
peripherals
=
Peripherals
::
take
()
.unwrap
();
let
peripherals
=
Peripherals
::
take
()
.unwrap
();
let
mut
dwt
=
peripherals
.DWT
;
let
mut
dwt
=
peripherals
.DWT
;
dwt
.enable_cycle_counter
();
dwt
.enable_cycle_counter
();
let
a
=
dwt
.cyccnt
.read
();
let
b
=
dwt
.cyccnt
.read
();
let
c
=
dwt
.cyccnt
.read
();
unsafe
{
unsafe
{
dwt
.ctrl
.write
(
0
);
let
some_time_quota
=
unchecked_div
(
a
,
c
-
b
);
read_volatile
(
&
some_time_quota
);
// prevent optization
}
}
if
dwt
.ctrl
.read
()
==
0
{
if
dwt
.ctrl
.read
()
==
0
{
klee
::
kabort!
();
};
};
}
}
This diff is collapsed.
Click to expand it.
klee-examples/src/register.rs
+
92
−
42
View file @
6568c3fc
//! showcase volatile register
// showcase volatile register
//!
// This is the underlying abstraction to all register accesses using the
//! $ cargo klee --bin register -r -g -k
// embedded Rust ecosystem.
//! ...
//
//! Reading symbols from register.replay...done.
// When analyzed by KLEE, we make the return value symbolic, thus each access
//!
// givs a new unique symbol. Even if we write a value to it, the next read
//! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
// will still be treated as a new symbol. That might be overly pessimistic
//! (gdb) run
// but is a safe approximation for the worst case behavior of the hardware.
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/release/deps/main2.replay
//
//! [Inferior 1 (process 25074) exited with code 01]
// > cargo klee --bin register --release
//!
// ...
//! (gdb) set env KTEST_FILE=klee-last/test000003.ktest
// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.2/src/lib.rs:49: abort failure
//! (gdb) run
// KLEE: NOTE: now ignoring this error at this location
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/release/deps/main2.replay
//! rust_begin_unwind (_info=0x7fffffffd678)
// KLEE: done: total instructions = 33
//! at /home/pln/.cargo/git/checkouts/cargo-klee-8f30fda3bd23bb30/68dc73d/src/lang_items.rs:66
// KLEE: done: completed paths = 3
//! unsafe { intrinsics::abort() }
// KLEE: done: generated tests = 3
//! (gdb) backtrace
//
//! #0 rust_begin_unwind (_info=0x7fffffffd678)
// > ls target/release/deps/klee-last/
//! at /home/pln/.cargo/git/checkouts/cargo-klee-8f30fda3bd23bb30/68dc73d/src/lang_items.rs:6
// assembly.ll info messages.txt run.istats run.stats test000001.ktest test000002.ktest test000003.abort.err test000003.kquery test000003.ktest warnings.txt
//! #1 0x000055555555531c in core::panicking::panic_fmt () at src/libcore/panicking.rs:95
//
//! #2 0x000055555555539b in core::panicking::panic () at src/libcore/panicking.rs:59
// We see that KLEE spoted the test3 hits unreachable (and thus panics)
//! #3 0x00005555555552a6 in main () at src/main2.rs:54
//
//! (gdb) q
// Let's look at the test cases separately:
//! A debugging session is active.
//
//!
// test1 passed:
//! Inferior 1 [process 25893] will be killed.
// ktest-tool target/release/deps/klee-last/test000001.ktest
//! $ ktest-tool --write-int target/debug/deps/klee-last/test000003.ktest
// ktest file : 'target/release/deps/klee-last/test000001.ktest'
//! ktest file : 'target/debug/deps/klee-last/test000003.ktest'
// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
//! args : ['/home/pln/rust/cargo-klee/klee-examples/target/debug/deps/main2-2a0fc03ce12ab528.ll']
// num objects: 1
//! num objects: 2
// object 0: name: 'vcell'
//! object 0: name: b'register'
// object 0: size: 4
//! object 0: size: 4
// object 0: data: b'\x00\x00\x00\x00'
//! object 0: data: 0
// object 0: hex : 0x00000000
//! object 1: name: b'register'
// object 0: int : 0
//! object 1: size: 4
// object 0: uint: 0
//! object 1: data: 0
// object 0: text: ....
// If the first read of the register is not 1 then we are ok.
//
// The second test also passed.
// ktest-tool target/release/deps/klee-last/test000002.ktest
// ktest file : 'target/release/deps/klee-last/test000002.ktest'
// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
// num objects: 2
// object 0: name: 'vcell'
// object 0: size: 4
// object 0: data: b'\x01\x00\x00\x00'
// object 0: hex : 0x01000000
// object 0: int : 1
// object 0: uint: 1
// object 0: text: ....
// object 1: name: 'vcell'
// object 1: size: 4
// object 1: data: b'\x00\x00\x00\x00'
// object 1: hex : 0x00000000
// object 1: int : 0
// object 1: uint: 0
// object 1: text: ....
// Here we are saved by the second reading of the register NOT giving
// returning 2.
//
// The third test gives the error.
// ktest-tool target/release/deps/klee-last/test000003.ktest
// ktest file : 'target/release/deps/klee-last/test000003.ktest'
// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
// num objects: 2
// object 0: name: 'vcell'
// object 0: size: 4
// object 0: data: b'\x01\x00\x00\x00'
// object 0: hex : 0x01000000
// object 0: int : 1
// object 0: uint: 1
// object 0: text: ....
// object 1: name: 'vcell'
// object 1: size: 4
// object 1: data: b'\x02\x00\x00\x00'
// object 1: hex : 0x02000000
// object 1: int : 2
// object 1: uint: 2
// object 1: text: ....
//
// The first read gives 1, the second 2, and we hit unreacable.
#![no_std]
#![no_std]
#![no_main]
#![no_main]
...
@@ -43,15 +88,20 @@ extern crate klee;
...
@@ -43,15 +88,20 @@ extern crate klee;
extern
crate
panic_abort
;
extern
crate
panic_abort
;
extern
crate
volatile_register
;
extern
crate
volatile_register
;
use
volatile_register
::
R
O
;
use
volatile_register
::
R
W
;
#[no_mangle]
#[no_mangle]
fn
main
()
{
fn
main
()
{
let
rw
:
RO
<
u32
>
=
unsafe
{
core
::
mem
::
uninitialized
()
};
// we emulate a read/write hardware register (rw)
let
rw
:
RW
<
u32
>
=
unsafe
{
core
::
mem
::
MaybeUninit
::
uninit
()
.assume_init
()
};
if
rw
.read
()
==
0
{
// reading will render a symbolic value of type u32
if
rw
.read
()
==
0
{
if
rw
.read
()
==
1
{
klee
::
kabort!
();
// we emulate a write to the hardware register
unsafe
{
rw
.write
(
0
)
};
// this read is still treated as a new symbolic value of type u32
if
rw
.read
()
==
2
{
unreachable!
();
}
}
}
}
}
}
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment