From 519a1dc746a116ba8fed05d1999c4802db2ab5ea Mon Sep 17 00:00:00 2001
From: Nils Fitinghoff <nils.fitinghoff@grepit.se>
Date: Sun, 28 Apr 2019 12:02:09 +0200
Subject: [PATCH] improve abort identification in KLEE output
KLEE reports the line that called `ll::abort()`. The previous
solution called a safe `abort()` which in turn called `ll::abort`. This
meant that every abort was reported as originating in this library.
This replaces the safe `abort()` function with a macro `kabort!()`. The
behavior differs in that `kabort!()` expands to nothing when not in KLEE
mode, while `abort()` expanded to a panic.
The macro causes the call to `ll::abort()` to happen directly from user
code from KLEE's point of view.
---
klee-examples/examples/modify.rs | 2 +-
klee-examples/src/peripheral.rs | 2 +-
klee-examples/src/register.rs | 2 +-
src/lib.rs | 32 ++++++++++++++------------------
4 files changed, 17 insertions(+), 21 deletions(-)
diff --git a/klee-examples/examples/modify.rs b/klee-examples/examples/modify.rs
index 6febd18..eb22811 100644
--- a/klee-examples/examples/modify.rs
+++ b/klee-examples/examples/modify.rs
@@ -22,6 +22,6 @@ fn main() {
}
if rw.read() == 0 {
- klee::abort(); // we directly call the intrinsic abort
+ klee::kabort!(); // we directly call the intrinsic abort
}
}
diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
index e281cd8..8d0bc89 100644
--- a/klee-examples/src/peripheral.rs
+++ b/klee-examples/src/peripheral.rs
@@ -18,7 +18,7 @@ fn main() {
}
if dwt.ctrl.read() == 0 {
if dwt.ctrl.read() == 0 {
- klee::abort();
+ klee::kabort!();
};
};
}
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
index 8024b4e..a5f247c 100644
--- a/klee-examples/src/register.rs
+++ b/klee-examples/src/register.rs
@@ -51,7 +51,7 @@ fn main() {
if rw.read() == 0 {
if rw.read() == 0 {
- klee::abort();
+ klee::kabort!();
}
}
}
diff --git a/src/lib.rs b/src/lib.rs
index 2cc7fe1..91976ba 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -16,15 +16,13 @@ use core::ffi::c_void;
#[doc(hidden)]
pub use cstr_core::CStr;
-#[cfg(feature = "klee-analysis")]
-#[inline(always)]
-pub fn abort() -> ! {
- unsafe { ll::abort() }
-}
-
-#[cfg(not(feature = "klee-analysis"))]
-pub fn abort() -> ! {
- panic!(); // leads to the defined panic handler
+/// Aborts the path in KLEE mode, does nothing otherwise
+#[macro_export]
+macro_rules! kabort {
+ () => {
+ #[cfg(feature = "klee-analysis")]
+ unsafe { $crate::ll::abort() };
+ };
}
#[cfg(feature = "klee-analysis")]
@@ -60,18 +58,16 @@ macro_rules! ksymbol {
};
}
-#[cfg(feature = "klee-analysis")]
+/// If in KLEE mode, the assertion is made.
+/// Otherwise, this is does nothing.
#[macro_export]
macro_rules! kassert {
($e:expr) => {
- if !$e {
- $crate::abort();
+ #[cfg(feature = "klee-analysis")]
+ {
+ if !$e {
+ $crate::kabort!();
+ }
}
};
}
-
-#[cfg(not(feature = "klee-analysis"))]
-#[macro_export]
-macro_rules! kassert {
- ($e:expr) => {};
-}
--
GitLab