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
Samuel Karlsson
cortex-m-rtfm-klee
Commits
268a32f4
Commit
268a32f4
authored
7 years ago
by
Per Lindgren
Browse files
Options
Downloads
Patches
Plain Diff
exam fixes
parent
a234264d
No related branches found
No related tags found
No related merge requests found
Changes
4
Show whitespace changes
Inline
Side-by-side
Showing
4 changed files
examples/resource.rs
+1
-19
1 addition, 19 deletions
examples/resource.rs
gdb.py
+113
-29
113 additions, 29 deletions
gdb.py
macros/src/lib.rs
+2
-2
2 additions, 2 deletions
macros/src/lib.rs
macros/src/trans.rs
+2
-2
2 additions, 2 deletions
macros/src/trans.rs
with
118 additions
and
52 deletions
examples/resource.rs
+
1
−
19
View file @
268a32f4
...
@@ -11,7 +11,7 @@ extern crate stm32f413;
...
@@ -11,7 +11,7 @@ extern crate stm32f413;
#[macro_use]
#[macro_use]
extern
crate
klee
;
extern
crate
klee
;
use
klee
::
*
;
use
klee
::
*
;
use
rtfm
::{
bkpt_1
,
bkpt_2
,
bkpt_3
};
//
use rtfm::{bkpt_1, bkpt_2, bkpt_3};
// import the procedural macro
// import the procedural macro
use
rtfm
::{
app
,
Resource
,
Threshold
};
use
rtfm
::{
app
,
Resource
,
Threshold
};
...
@@ -70,22 +70,6 @@ fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
...
@@ -70,22 +70,6 @@ fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
});
});
}
}
#[inline(never)]
#[no_mangle]
fn
enter
()
{
unsafe
{
rtfm
::
bkpt_1
();
}
}
#[inline(never)]
#[no_mangle]
fn
exit
()
{
unsafe
{
rtfm
::
bkpt_2
();
}
}
#[allow(non_snake_case)]
#[allow(non_snake_case)]
fn
exti3
(
t
:
&
mut
Threshold
,
mut
r
:
EXTI3
::
Resources
)
{
fn
exti3
(
t
:
&
mut
Threshold
,
mut
r
:
EXTI3
::
Resources
)
{
r
.X
.claim_mut
(
t
,
|
x
,
_
|
{
r
.X
.claim_mut
(
t
,
|
x
,
_
|
{
...
@@ -99,8 +83,6 @@ fn init(_p: init::Peripherals, _r: init::Resources) {}
...
@@ -99,8 +83,6 @@ fn init(_p: init::Peripherals, _r: init::Resources) {}
#[inline(never)]
#[inline(never)]
#[allow(dead_code)]
#[allow(dead_code)]
#[allow(private_no_mangle_fns)]
#[no_mangle]
fn
idle
()
->
!
{
fn
idle
()
->
!
{
loop
{
loop
{
rtfm
::
nop
();
rtfm
::
nop
();
...
...
This diff is collapsed.
Click to expand it.
gdb.py
+
113
−
29
View file @
268a32f4
...
@@ -25,11 +25,15 @@ object_index_current = 0
...
@@ -25,11 +25,15 @@ object_index_current = 0
tasks
=
[]
tasks
=
[]
priorities
=
[]
task_to_test
=
0
task_to_test
=
0
task_name
=
""
task_name
=
""
# Name, Cyccnt, ceiling
priority
=
0
# [[ Test, Task, Cyccnt, priority/ceiling] Info]
outputdata
=
[]
outputdata
=
[]
"""
Max number of events guard
"""
"""
Max number of events guard
"""
...
@@ -39,6 +43,31 @@ object_index_max = 100
...
@@ -39,6 +43,31 @@ object_index_max = 100
original_pwd
=
os
.
getcwd
()
original_pwd
=
os
.
getcwd
()
def
gather_data
():
global
outputdata
global
file_index_current
global
file_list
global
init_done
"""
If not all ktest-files done yet, proceed
"""
if
file_index_current
<
len
(
file_list
):
file_index_current
+=
1
# print("Current file: %s" % file_list[file_index_current])
gdb
.
post_event
(
posted_event_init
)
else
:
print
(
"
Finished everything
"
)
print
(
outputdata
)
"""
... call your analysis here ...
"""
gdb
.
execute
(
"
quit
"
)
class
KTestError
(
Exception
):
class
KTestError
(
Exception
):
pass
pass
...
@@ -128,6 +157,7 @@ def stop_event(evt):
...
@@ -128,6 +157,7 @@ def stop_event(evt):
global
task_name
global
task_name
global
file_index_current
global
file_index_current
global
file_list
global
file_list
global
priority
file_name
=
file_list
[
file_index_current
].
split
(
'
/
'
)[
-
1
]
file_name
=
file_list
[
file_index_current
].
split
(
'
/
'
)[
-
1
]
...
@@ -167,7 +197,7 @@ def stop_event(evt):
...
@@ -167,7 +197,7 @@ def stop_event(evt):
gdb
.
post_event
(
posted_event_init
)
gdb
.
post_event
(
posted_event_init
)
outputdata
.
append
([
file_name
,
task_name
,
outputdata
.
append
([
file_name
,
task_name
,
gdb_cyccnt_read
(),
0
,
"
Finish
"
])
gdb_cyccnt_read
(),
priority
,
"
Finish
"
])
if
file_index_current
<
len
(
file_list
)
-
1
:
if
file_index_current
<
len
(
file_list
)
-
1
:
gather_data
()
gather_data
()
...
@@ -204,6 +234,8 @@ def posted_event_init():
...
@@ -204,6 +234,8 @@ def posted_event_init():
global
file_index_current
global
file_index_current
global
file_list
global
file_list
global
outputdata
global
outputdata
global
priority
global
priorities
"""
Load the variable data
"""
"""
Load the variable data
"""
ktest_setdata
(
file_index_current
)
ktest_setdata
(
file_index_current
)
...
@@ -226,9 +258,10 @@ def posted_event_init():
...
@@ -226,9 +258,10 @@ def posted_event_init():
file_name
=
file_list
[
file_index_current
].
split
(
'
/
'
)[
-
1
]
file_name
=
file_list
[
file_index_current
].
split
(
'
/
'
)[
-
1
]
task_name
=
tasks
[
task_to_test
]
task_name
=
tasks
[
task_to_test
]
priority
=
priorities
[
task_to_test
]
outputdata
.
append
([
file_name
,
task_name
,
outputdata
.
append
([
file_name
,
task_name
,
gdb_cyccnt_read
(),
0
,
"
Start
"
])
gdb_cyccnt_read
(),
priority
,
"
Start
"
])
gdb
.
write
(
'
Task to call: %s
\n
'
%
(
gdb
.
write
(
'
Task to call: %s
\n
'
%
(
tasks
[
task_to_test
]
+
"
()
"
))
tasks
[
task_to_test
]
+
"
()
"
))
...
@@ -377,7 +410,7 @@ def tasklist_get():
...
@@ -377,7 +410,7 @@ def tasklist_get():
for
line
in
fin
:
for
line
in
fin
:
# print(line)
# print(line)
if
not
line
==
"
// autogenerated file
\n
"
:
if
not
line
==
"
// autogenerated file
\n
"
:
return
[
x
.
strip
().
strip
(
"
[]
\"
"
)
for
x
in
line
.
split
(
'
,
'
)]
return
[
x
.
strip
().
strip
(
"
[]
\"
"
)
.
split
(
'
'
)
for
x
in
line
.
split
(
'
,
'
)]
"""
Run xargo for building
"""
"""
Run xargo for building
"""
...
@@ -520,11 +553,23 @@ file_list = ktest_iterate()
...
@@ -520,11 +553,23 @@ file_list = ktest_iterate()
print
(
file_list
)
print
(
file_list
)
"""
Get all the tasks to jump to
"""
"""
Get all the tasks to jump to
"""
tasks
=
tasklist_get
()
task_list
=
tasklist_get
()
print
(
"
task_list {}
"
.
format
(
task_list
))
"""
Split into tasks and priorities
"""
for
x
in
task_list
:
priorities
.
append
(
x
.
pop
())
tasks
.
append
(
x
.
pop
())
print
(
"
Available tasks:
"
)
print
(
"
Available tasks:
"
)
for
t
in
tasks
:
for
t
in
tasks
:
print
(
t
)
print
(
t
)
print
(
"
At priorities:
"
)
for
t
in
priorities
:
print
(
t
)
"""
Subscribe stop_event_ignore to Breakpoint notifications
"""
"""
Subscribe stop_event_ignore to Breakpoint notifications
"""
gdb
.
events
.
stop
.
connect
(
stop_event
)
gdb
.
events
.
stop
.
connect
(
stop_event
)
...
@@ -535,28 +580,67 @@ gdb.events.stop.connect(stop_event)
...
@@ -535,28 +580,67 @@ gdb.events.stop.connect(stop_event)
gdb
.
execute
(
"
continue
"
)
gdb
.
execute
(
"
continue
"
)
def
gather_data
():
global
outputdata
global
file_index_current
global
file_list
global
init_done
"""
If not all ktest-files done yet, proceed
"""
if
file_index_current
<
len
(
file_list
):
file_index_current
+=
1
# print("Current file: %s" % file_list[file_index_current])
gdb
.
post_event
(
posted_event_init
)
else
:
print
(
"
Finished everything
"
)
print
(
outputdata
)
"""
... call your analysis here ...
"""
gdb
.
execute
(
"
quit
"
)
# Home exam, response time analysis
# Home exam, response time analysis
#
# 1. run the example and study the output
# it generates `output data`, a list of list, something like:
# Claims:
# ['test000001.ktest', '', 22095438, 0, 'Finish'] Total time: 22095438
# ['test000002.ktest', 'EXTI2', 0, '3', 'Start']
# ['test000002.ktest', 'EXTI2', 11, '3', 'Finish'] Total time: 11
# ['test000003.ktest', 'EXTI2', 0, '3', 'Start']
# ['test000003.ktest', 'EXTI2', 11, '3', 'Finish'] Total time: 11
# ['test000004.ktest', 'EXTI3', 0, '2', 'Start']
# ['test000004.ktest', 'EXTI3', 7, '2', 'Finish'] Total time: 7
# ['test000005.ktest', 'EXTI1', 0, '1', 'Start']
# ['test000005.ktest', 'EXTI1', 15, 2, 'Enter']
# ['test000005.ktest', 'EXTI1', 19, 3, 'Enter']
# ['test000005.ktest', 'EXTI1', 28, 3, 'Exit'] Claim time: 9
# ['test000005.ktest', 'EXTI1', 29, 2, 'Exit'] Claim time: 14
# ['test000005.ktest', 'EXTI1', 32, '1', 'Finish'] Total time: 32
# ['test000006.ktest', 'EXTI1', 0, '1', 'Start']...
#
# first entry
# ['test000001.ktest', ....
# is our bogus test, not of interest for the analysis)
#
# next entries:
#['test000002.ktest', 'EXTI2', 0, 3, 'Start']
#['test000002.ktest', 'EXTI2', 11, 3, 'Finish'] Total time: 11
# amounts to the first real task
# broken down, the first measurement
# -'test000002.ktest' the ktest file
# -'EXTI2' the task
# -'0' the time stamp (start from zero)
# -'3' the threshold (priority 3)
# -'Start' the 'Start' event
#
# broken down, the second measurement
# -'test000002.ktest' the ktest file
# -'EXTI2' the task
# -'11' the time stamp (start from zero)
# -'3' the threshold (priority 3)
# -'Finish' the 'Start' event
#
# followed by
# Total time: 11
#
# let us look at the following measurements
#
# 'test000003.ktest'
# recall from the lab that we had two cases for EXTI2
# both with the same result
#
# 'test000004.ktest'
# recall from the lab that we had a singel test for EXTI3
#
# and finally
#
# 'test000005.ktest' and on ... for EXTI1
# here at prio 1, and after 15 cycles claim X, raising threshold to 2
# after 19 cycles we clam Y, raising treshold to 3
# after 28 cycles we exit the Y claim, threshold 3 *before unlock Y*
# after 29 cycles we exit the X claim, threshold 2 *before unlock X*
# and finally we finish at 34 clock cycles
#
# (recall we had some 38 in the lab, this is due mesuring)
This diff is collapsed.
Click to expand it.
macros/src/lib.rs
+
2
−
2
View file @
268a32f4
...
@@ -192,9 +192,9 @@ fn run(ts: TokenStream) -> Result<TokenStream> {
...
@@ -192,9 +192,9 @@ fn run(ts: TokenStream) -> Result<TokenStream> {
if
cfg!
(
feature
=
"klee_mode"
)
{
if
cfg!
(
feature
=
"klee_mode"
)
{
println!
(
"tasks"
);
println!
(
"tasks"
);
let
mut
tasks
=
Vec
::
new
();
let
mut
tasks
=
Vec
::
new
();
for
(
id
,
_
task
)
in
app
.tasks
{
for
(
id
,
task
)
in
app
.tasks
{
println!
(
"{}"
,
id
);
println!
(
"{}"
,
id
);
tasks
.push
(
format!
(
"{}"
,
id
));
tasks
.push
(
format!
(
"{}
{}
"
,
id
,
task
.priority
));
}
}
let
path
=
Path
::
new
(
"klee/tasks.txt"
);
let
path
=
Path
::
new
(
"klee/tasks.txt"
);
...
...
This diff is collapsed.
Click to expand it.
macros/src/trans.rs
+
2
−
2
View file @
268a32f4
...
@@ -709,7 +709,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
...
@@ -709,7 +709,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
// call the task
// call the task
unsafe
{
#
_tname
();
}
unsafe
{
#
_tname
();
}
// break for finish wcet measurement
// break for finish wcet measurement
unsafe
{
bkpt_3
();
}
unsafe
{
rtfm
::
bkpt_3
();
}
}
}
});
});
}
}
...
@@ -745,7 +745,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
...
@@ -745,7 +745,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
#[inline(never)]
#[inline(never)]
pub
fn
wcet_start
()
{
pub
fn
wcet_start
()
{
// break for starting wcet measurement
// break for starting wcet measurement
unsafe
{
bkpt_3
()
};
unsafe
{
rtfm
::
bkpt_3
()
};
// call each stub to avoind optimizing out
// call each stub to avoind optimizing out
#
(
#
stubs
)
*
#
(
#
stubs
)
*
}
}
...
...
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