Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
C
cortex-m-rtfm-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
Model registry
Operate
Environments
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
KLEE
cortex-m-rtfm-klee
Commits
d88a15fb
Commit
d88a15fb
authored
Mar 8, 2017
by
Jorge Aparicio
Browse files
Options
Downloads
Patches
Plain Diff
adapt to changes in cortex-m, verify the input of the `priority` function
parent
e56f8156
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
Cargo.toml
+1
-1
1 addition, 1 deletion
Cargo.toml
src/lib.rs
+62
-104
62 additions, 104 deletions
src/lib.rs
with
63 additions
and
105 deletions
Cargo.toml
+
1
−
1
View file @
d88a15fb
...
@@ -4,5 +4,5 @@ version = "0.1.0"
...
@@ -4,5 +4,5 @@ version = "0.1.0"
authors
=
[
"Jorge Aparicio <japaricious@gmail.com>"
]
authors
=
[
"Jorge Aparicio <japaricious@gmail.com>"
]
[dependencies.cortex-m]
[dependencies.cortex-m]
branch
=
"
svd2rust
"
branch
=
"
ng
"
git
=
"https://github.com/japaric/cortex-m"
git
=
"https://github.com/japaric/cortex-m"
This diff is collapsed.
Click to expand it.
src/lib.rs
+
62
−
104
View file @
d88a15fb
...
@@ -2,6 +2,8 @@
...
@@ -2,6 +2,8 @@
//!
//!
//! NOTE ARMv6-M is not supported at the moment.
//! NOTE ARMv6-M is not supported at the moment.
#![deny(missing_docs)]
#![deny(warnings)]
#![feature(asm)]
#![feature(asm)]
#![feature(const_fn)]
#![feature(const_fn)]
#![no_std]
#![no_std]
...
@@ -12,146 +14,95 @@ const PRIORITY_BITS: u8 = 4;
...
@@ -12,146 +14,95 @@ const PRIORITY_BITS: u8 = 4;
extern
crate
cortex_m
;
extern
crate
cortex_m
;
use
cortex_m
::
interrupt
::
CsToken
;
use
cortex_m
::
interrupt
::
CsCtxt
;
use
cortex_m
::
peripheral
::
Peripheral
;
use
cortex_m
::
register
::{
basepri
,
basepri_max
};
use
cortex_m
::
register
::{
basepri
,
basepri_max
};
use
core
::
cell
::
UnsafeCell
;
use
core
::
cell
::
UnsafeCell
;
use
core
::
marker
::
PhantomData
;
// XXX
why is this needed
?
// XXX
Do we need memory / instruction / compiler barriers here
?
#[inline(always)]
#[inline(always)]
fn
compiler_barrier
()
{
unsafe
fn
claim
<
T
,
R
,
F
>
(
f
:
F
,
res
:
*
const
T
,
ceiling
:
u8
)
->
R
unsafe
{
where
F
:
FnOnce
(
&
T
)
->
R
asm!
(
""
{
:
let
old_basepri
=
basepri
::
read
();
:
basepri_max
::
write
(
ceiling
);
:
"memory"
let
ret
=
f
(
&*
res
);
:
"volatile"
)
basepri
::
write
(
old_basepri
);
}
ret
}
// XXX why is this needed?
#[inline(always)]
fn
memory_barrier
()
{
unsafe
{
asm!
(
"dsb
isb"
:
:
:
"memory"
:
"volatile"
)
}
}
}
pub
struct
Peripheral
<
T
>
/// A peripheral as a resource
pub
struct
ResourceP
<
T
>
where
T
:
'static
where
T
:
'static
{
{
_ty
:
PhantomData
<&
'static
mut
T
>
,
peripheral
:
Peripheral
<
T
>
,
address
:
usize
,
// NOTE NVIC-style priority ceiling
ceiling
:
u8
,
ceiling
:
u8
,
}
}
impl
<
T
>
Peripheral
<
T
>
{
impl
<
T
>
ResourceP
<
T
>
{
pub
const
unsafe
fn
new
(
address
:
usize
,
ceiling
:
u8
)
->
Self
{
/// Wraps a `peripheral` into a `Resource`
Peripheral
{
///
_ty
:
PhantomData
,
/// NOTE `ceiling` must be in the range `[1, 15]` (inclusive)
address
:
address
,
///
ceiling
:
ceiling
,
/// # Unsafety
///
/// - Do not create two resources that point to the same peripheral
pub
const
unsafe
fn
new
(
p
:
Peripheral
<
T
>
,
ceiling
:
u8
)
->
Self
{
ResourceP
{
peripheral
:
p
,
// NOTE elements 1 and 2 of the tuple are a poor man's const context
// range checker
ceiling
:
(
priority
(
ceiling
),
ceiling
-
1
,
ceiling
+
240
)
.0
,
}
}
}
}
pub
fn
claim
<
F
,
R
>
(
&
self
,
f
:
F
)
->
R
/// Claims the resource, blocking tasks with priority lower than `ceiling`
pub
fn
claim
<
R
,
F
>
(
&
'static
self
,
f
:
F
)
->
R
where
F
:
FnOnce
(
&
T
)
->
R
where
F
:
FnOnce
(
&
T
)
->
R
{
{
unsafe
{
unsafe
{
claim
(
f
,
self
.peripheral
.get
(),
self
.ceiling
)
}
let
old_basepri
=
basepri
::
read
();
basepri_max
::
write
(
priority
(
self
.ceiling
));
memory_barrier
();
let
ret
=
f
(
&*
(
self
.address
as
*
const
T
));
compiler_barrier
();
basepri
::
write
(
old_basepri
);
ret
}
}
}
pub
fn
claim_mut
<
F
,
R
>
(
&
self
,
f
:
F
)
->
R
/// Borrows the resource for the duration of a critical section
where
F
:
FnOnce
(
&
mut
T
)
->
R
pub
fn
borrow
<
'a
>
(
&
'static
self
,
_ctxt
:
&
'a
CsCtxt
)
->
&
'a
T
{
{
unsafe
{
&*
self
.peripheral
.get
()
}
unsafe
{
let
old_basepri
=
basepri
::
read
();
basepri_max
::
write
(
priority
(
self
.ceiling
));
memory_barrier
();
let
ret
=
f
(
&
mut
*
(
self
.address
as
*
mut
T
));
compiler_barrier
();
basepri
::
write
(
old_basepri
);
ret
}
}
}
}
pub
fn
take
<
'a
>
(
&
self
,
_token
:
&
'a
CsToken
)
->
&
'a
T
{
unsafe
impl
<
T
>
Sync
for
ResourceP
<
T
>
{}
unsafe
{
&*
(
self
.address
as
*
const
T
)
}
}
pub
fn
take_mut
<
'a
>
(
&
self
,
_token
:
&
'a
CsToken
)
->
&
'a
mut
T
{
unsafe
{
&
mut
*
(
self
.address
as
*
mut
T
)
}
}
}
/// A resource
pub
struct
Resource
<
T
>
{
pub
struct
Resource
<
T
>
{
// NOTE NVIC-style priority ceiling
ceiling
:
u8
,
ceiling
:
u8
,
data
:
UnsafeCell
<
T
>
,
data
:
UnsafeCell
<
T
>
,
}
}
impl
<
T
>
Resource
<
T
>
{
impl
<
T
>
Resource
<
T
>
{
/// Initializes a resource
///
/// NOTE `ceiling` must be in the range `[1, 15]`
pub
const
fn
new
(
data
:
T
,
ceiling
:
u8
)
->
Self
{
pub
const
fn
new
(
data
:
T
,
ceiling
:
u8
)
->
Self
{
Resource
{
Resource
{
ceiling
:
ceiling
,
// NOTE elements 1 and 2 of the tuple are a poor man's const context
// range checker
ceiling
:
(
priority
(
ceiling
),
ceiling
-
1
,
ceiling
+
240
)
.0
,
data
:
UnsafeCell
::
new
(
data
),
data
:
UnsafeCell
::
new
(
data
),
}
}
}
}
pub
fn
claim
<
F
,
R
>
(
&
self
,
f
:
F
)
->
R
/// Claims the resource, blocking tasks with priority lower than `ceiling`
pub
fn
claim
<
F
,
R
>
(
&
'static
self
,
f
:
F
)
->
R
where
F
:
FnOnce
(
&
T
)
->
R
where
F
:
FnOnce
(
&
T
)
->
R
{
{
unsafe
{
unsafe
{
claim
(
f
,
self
.data
.get
(),
self
.ceiling
)
}
let
old_basepri
=
basepri
::
read
();
basepri_max
::
write
(
priority
(
self
.ceiling
));
memory_barrier
();
let
ret
=
f
(
&*
self
.data
.get
());
compiler_barrier
();
basepri
::
write
(
old_basepri
);
ret
}
}
pub
fn
claim_mut
<
F
,
R
>
(
&
self
,
f
:
F
)
->
R
where
F
:
FnOnce
(
&
mut
T
)
->
R
{
unsafe
{
let
old_basepri
=
basepri
::
read
();
basepri_max
::
write
(
priority
(
self
.ceiling
));
memory_barrier
();
let
ret
=
f
(
&
mut
*
self
.data
.get
());
compiler_barrier
();
basepri
::
write
(
old_basepri
);
ret
}
}
}
pub
fn
take
<
'a
>
(
&
self
,
_token
:
&
'a
CsToken
)
->
&
'a
T
{
/// Borrows the resource for the duration of a critical section
unsafe
{
pub
fn
borrow
<
'cs
>
(
&
self
,
_ctxt
:
&
'cs
CsCtxt
)
->
&
'cs
T
{
&*
self
.data
.get
()
unsafe
{
&*
self
.data
.get
()
}
}
}
pub
fn
take_mut
<
'a
>
(
&
self
,
_token
:
&
'a
CsToken
)
->
&
'a
mut
T
{
unsafe
{
&
mut
*
self
.data
.get
()
}
}
}
}
}
...
@@ -164,7 +115,14 @@ unsafe impl<T> Sync for Resource<T> {}
...
@@ -164,7 +115,14 @@ unsafe impl<T> Sync for Resource<T> {}
/// With NVIC priorities, `32` has LOWER priority than `16`. (Also, NVIC
/// With NVIC priorities, `32` has LOWER priority than `16`. (Also, NVIC
/// priorities encode the actual priority in the highest bits of a byte so
/// priorities encode the actual priority in the highest bits of a byte so
/// priorities like `1` and `2` aren't actually different)
/// priorities like `1` and `2` aren't actually different)
// TODO review the handling of extreme values
///
/// NOTE `logical` must be in the range `[1, 15]` (inclusive)
pub
const
fn
priority
(
logical
:
u8
)
->
u8
{
pub
const
fn
priority
(
logical
:
u8
)
->
u8
{
((
1
<<
PRIORITY_BITS
)
-
logical
)
<<
(
8
-
PRIORITY_BITS
)
// NOTE elements 1 and 2 of the tuple are a poor man's const context range
// checker
(((
1
<<
PRIORITY_BITS
)
-
logical
)
<<
(
8
-
PRIORITY_BITS
),
logical
-
1
,
logical
+
240
)
.0
}
}
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