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
f9508a76
Commit
f9508a76
authored
Feb 25, 2018
by
Henrik Tjäder
Browse files
Options
Downloads
Patches
Plain Diff
Adapt the GDB-script to get the CYCCNT and Ceiling
parent
03894aa2
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
examples/resource.rs
+7
-9
7 additions, 9 deletions
examples/resource.rs
klee_stm_gdb.py
+149
-45
149 additions, 45 deletions
klee_stm_gdb.py
with
156 additions
and
54 deletions
examples/resource.rs
+
7
−
9
View file @
f9508a76
...
@@ -77,26 +77,19 @@ fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
...
@@ -77,26 +77,19 @@ fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
#[inline(never)]
#[inline(never)]
#[allow(dead_code)]
#[allow(dead_code)]
fn
init
(
_p
:
init
::
Peripherals
,
_r
:
init
::
Resources
)
{
fn
init
(
_p
:
init
::
Peripherals
,
_r
:
init
::
Resources
)
{
loop
{
loop
{}
rtfm
::
bkpt
();
}
}
}
extern
crate
cortex_m
;
extern
crate
cortex_m
;
use
cortex_m
::
register
::
basepri
;
use
cortex_m
::
register
::
basepri
;
// for wcet should be autogenerated...
// for wcet should be autogenerated...
#[inline(never)]
#[inline(never)]
#[no_mangle]
#[no_mangle]
fn
readbasepri
()
->
u8
{
fn
readbasepri
()
->
u8
{
cortex_m
::
register
::
basepri
::
read
()
cortex_m
::
register
::
basepri
::
read
()
}
}
// The idle loop.
//
// This runs after `init` and has a priority of 0. All tasks can preempt this
// function. This function can never return so it must contain some sort of
// endless loop.
#[inline(never)]
#[inline(never)]
#[allow(non_snake_case)]
#[allow(non_snake_case)]
#[no_mangle]
#[no_mangle]
...
@@ -118,6 +111,11 @@ fn stub_EXTI3() {
...
@@ -118,6 +111,11 @@ fn stub_EXTI3() {
}
}
}
}
// The idle loop.
//
// This runs after `init` and has a priority of 0. All tasks can preempt this
// function. This function can never return so it must contain some sort of
// endless loop.
#[inline(never)]
#[inline(never)]
fn
idle
()
->
!
{
fn
idle
()
->
!
{
readbasepri
();
readbasepri
();
...
...
This diff is collapsed.
Click to expand it.
klee_stm_gdb.py
+
149
−
45
View file @
f9508a76
...
@@ -16,7 +16,14 @@ file_index_current = 0
...
@@ -16,7 +16,14 @@ file_index_current = 0
object_index_current
=
0
object_index_current
=
0
tasks
=
[]
tasks
=
[]
task_to_test
=
-
1
task_to_test
=
0
task_name
=
""
# Name, Cyccnt, ceiling
outputdata
=
[]
init_done
=
0
"""
Max number of events guard
"""
"""
Max number of events guard
"""
object_index_max
=
100
object_index_max
=
100
...
@@ -112,22 +119,30 @@ class KTest:
...
@@ -112,22 +119,30 @@ class KTest:
self
.
programName
=
program_name
self
.
programName
=
program_name
class
MainBP
(
gdb
.
Breakpoint
):
def
do_continue
():
gdb
.
execute
(
"
continue
"
)
global
tasks
class
MainBP
(
gdb
.
Breakpoint
):
def
stop
(
self
):
def
stop
(
self
):
# print("##### breakpoint")
# print("##### breakpoint")
global
file_index_current
global
file_index_current
gdb
.
events
.
stop
.
connect
(
stop_event
)
global
outputdata
global
init_done
if
self
.
location
==
"
init
"
:
if
self
.
location
==
"
init
"
:
gdb
.
write
(
"
Breakpoint in init()
\n
"
)
# print("##### breakpoint init")
gdb
.
prompt_hook
=
prompt
gdb
.
post_event
(
posted_event_main
)
if
not
init_done
:
# gdb.execute('stop')
# gdb.prompt_hook = prompt
# gdb.execute('jump %r' % tasks[0])
init_done
=
1
gdb
.
post_event
(
posted_event_init
)
else
:
gdb
.
post_event
(
gather_data
)
elif
self
.
location
==
"
idle
"
:
elif
self
.
location
==
"
idle
"
:
# print("##### breakpoint idle")
"""
Idle loop is reached, now jump to the task specified
"""
Idle loop is reached, now jump to the task specified
in the
"
task
"
value in the ktest files.
in the
"
task
"
value in the ktest files.
...
@@ -135,42 +150,59 @@ class MainBP(gdb.Breakpoint):
...
@@ -135,42 +150,59 @@ class MainBP(gdb.Breakpoint):
then run all of the tasks.
then run all of the tasks.
"""
"""
gdb
.
write
(
"
Breakpoint in loop()
\n
"
)
gdb
.
prompt_hook
=
prompt
# print("Tasks: ", tasks)
# print("Name of task to test:", tasks[task_to_test])
if
not
task_to_test
==
-
1
:
gdb
.
write
(
'
Task to call: %s
\n
'
%
(
"
stub_
"
+
tasks
[
task_to_test
]))
gdb
.
execute
(
'
call %s
'
%
"
stub_
"
+
tasks
[
task_to_test
]
+
"
()
"
)
else
:
print
(
"
No task defined
"
)
"""
for task in tasks:
gdb.write(
'
Task: %r
\n
'
% task)
gdb.execute(
'
jump %r
'
% task)
"""
# gdb.write("Breakpoint in finish_execution\n")
# gdb.write("Breakpoint in finish_execution\n")
# gdb.write("Stopped before the main loop\n")
# gdb.write("Stopped before the main loop\n")
"""
Save the execution time and
"""
Save the execution time and
reload back to the main function.
reload back to the main function.
"""
"""
gdb
.
prompt_hook
=
prompt
gdb
.
prompt_hook
=
prompt
gdb
.
post_event
(
posted_event_finish_execution
)
#
gdb.post_event(posted_event_finish_execution)
"""
Needed to actually stop after the breakpoint
"""
"""
Needed to actually stop after the breakpoint
True: Return prompt
False: Continue?
"""
return
True
return
True
# return False
# Subscribing to the stop events
# Subscribing to the stop events
def
stop_event
(
evt
):
def
stop_event
(
evt
):
# print("#### stop event")
# print("#### stop event")
# print("evt %r" % evt)
# print("evt %r" % evt)
global
outputdata
global
task_name
tmp1
=
task_name
tmp2
=
gdb_cyccnt_read
()
"""
Get the current ceiling level, cast it to an integer
"""
try
:
tmp3
=
int
(
gdb
.
parse_and_eval
(
"
ceiling
"
).
cast
(
gdb
.
lookup_type
(
'
u8
'
)))
except
gdb
.
error
:
print
(
"
Returned from call to %s
"
%
task_name
)
"""
If there is no ceiling, it means we have returned to init
since every claim have ceiling
"""
gdb
.
events
.
stop
.
disconnect
(
stop_event
)
gdb
.
events
.
stop
.
disconnect
(
stop_event
)
print
(
"
Claims:
"
)
print
(
outputdata
)
gdb
.
execute
(
"
quit
"
)
print
(
"
CYCCNT: %s
\n
Ceiling: %s
"
%
(
tmp2
,
tmp3
))
outputdata
.
append
([
tmp1
,
tmp2
,
tmp3
])
"""
Prepare a prompt for do_continue()
"""
gdb
.
prompt_hook
=
prompt
do_continue
()
# Hooking the prompt:
# Hooking the prompt:
def
prompt
(
current
):
def
prompt
(
current
):
...
@@ -185,16 +217,68 @@ def prompt(current):
...
@@ -185,16 +217,68 @@ def prompt(current):
# gdb.execute("
# gdb.execute("
def
posted_event_init
():
"""
Called at the very beginning of execution
when the breakpoint at init() is hit
Loads each defined task
"""
"""
"""
Called wh
en t
he b
reakpoint
at main() is hit
Subscribe stop_ev
en
t
t
o B
reakpoint
notifications
"""
"""
gdb
.
events
.
stop
.
connect
(
stop_event
)
# print("Entering posted_event_init")
def
posted_event_main
():
global
tasks
# print("# main BP")
global
task_to_test
global
task_name
global
file_index_current
global
file_index_current
ktest_setdata
(
file_index_current
)
gdb
.
execute
(
"
continue
"
)
"""
Load the variable data
"""
# ktest_setdata(file_index_current)
"""
Prepare the cycle counter
"""
gdb_cyccnt_enable
()
gdb_cyccnt_reset
()
# ccount = gdb_cyccnt_read()
# print(ccount)
# print("Tasks: ", tasks)
# print("Name of task to test:", tasks[task_to_test])
if
not
task_to_test
==
-
1
:
gdb
.
write
(
'
Task to call: %s
\n
'
%
(
"
stub_
"
+
tasks
[
task_to_test
]
+
"
()
"
))
task_name
=
tasks
[
task_to_test
]
# gdb.prompt_hook = prompt
gdb
.
execute
(
'
call %s
'
%
"
stub_
"
+
tasks
[
task_to_test
]
+
"
()
"
)
print
(
"
Called stub
"
)
task_to_test
=
-
1
do_continue
()
else
:
# gdb.execute("mon mdw 0xe0001004")
# print(gdb_cyccnt_read())
print
(
"
Done else
"
)
print
(
"
In init!
"
)
# do_continue()
def
gather_data
():
global
outputdata
print
(
"
Finished everything
"
)
print
(
outputdata
)
gdb
.
execute
(
"
quit
"
)
def
posted_event_finish_execution
():
def
posted_event_finish_execution
():
...
@@ -315,7 +399,7 @@ def ktest_setdata(file_index):
...
@@ -315,7 +399,7 @@ def ktest_setdata(file_index):
print
(
'
object %4d: data: %r
'
%
print
(
'
object %4d: data: %r
'
%
(
i
,
obj_data
))
(
i
,
obj_data
))
# gdb.execute('whatis %r' % name.decode('UTF-8'))
# gdb.execute('whatis %r' % name.decode('UTF-8'))
gdb
.
execute
(
'
whatis %r
'
%
obj_data
)
#
gdb.execute('whatis %r' % obj_data)
gdb
.
execute
(
'
set variable %s = %r
'
%
gdb
.
execute
(
'
set variable %s = %r
'
%
(
name
.
decode
(
'
UTF-8
'
),
obj_data
))
(
name
.
decode
(
'
UTF-8
'
),
obj_data
))
# gdb.write('Variable %s is:' % name.decode('UTF-8'))
# gdb.write('Variable %s is:' % name.decode('UTF-8'))
...
@@ -332,13 +416,14 @@ def ktest_iterate():
...
@@ -332,13 +416,14 @@ def ktest_iterate():
curdir
=
os
.
getcwd
()
curdir
=
os
.
getcwd
()
print
(
curdir
)
print
(
curdir
)
"""
We have already entered the output folder
"""
"""
We have already entered the output folder
"""
rustoutputfolder
=
"
../target/x86_64-unknown-linux-gnu/
debug
/examples/
"
rustoutputfolder
=
"
../target/x86_64-unknown-linux-gnu/
release
/examples/
"
try
:
try
:
os
.
chdir
(
rustoutputfolder
)
os
.
chdir
(
rustoutputfolder
)
except
IOError
:
except
IOError
:
print
(
rustoutputfolder
+
"
not found. Need to run
\n
"
)
print
(
rustoutputfolder
+
"
not found. Need to run
\n
"
)
print
(
"
xargo build --example resource --features
\
print
(
"
xargo build
--release
--example resource --features
\
klee_mode --target x86_64-unknown-linux-gnu
"
)
klee_mode --target x86_64-unknown-linux-gnu
"
)
sys
.
exit
(
1
)
dirlist
=
next
(
os
.
walk
(
"
.
"
))[
1
]
dirlist
=
next
(
os
.
walk
(
"
.
"
))[
1
]
dirlist
.
sort
()
dirlist
.
sort
()
...
@@ -347,6 +432,7 @@ def ktest_iterate():
...
@@ -347,6 +432,7 @@ def ktest_iterate():
directory
=
dirlist
[
-
1
]
directory
=
dirlist
[
-
1
]
except
IOError
:
except
IOError
:
print
(
"
No KLEE output, need to run KLEE
"
)
print
(
"
No KLEE output, need to run KLEE
"
)
sys
.
exit
(
1
)
print
(
"
Using ktest-files from directory:
\n
"
+
rustoutputfolder
+
directory
)
print
(
"
Using ktest-files from directory:
\n
"
+
rustoutputfolder
+
directory
)
...
@@ -371,13 +457,15 @@ def tasklist_get():
...
@@ -371,13 +457,15 @@ def tasklist_get():
print
(
os
.
getcwd
())
print
(
os
.
getcwd
())
with
open
(
'
../klee/tasks.txt
'
)
as
fin
:
with
open
(
'
../klee/tasks.txt
'
)
as
fin
:
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
(
"
[]
\"
"
)
for
x
in
line
.
split
(
'
,
'
)]
def
klee_run
():
def
klee_run
():
"""
Stub for running KLEE on the LLVM IR
"""
PWD
=
os
.
getcwd
()
PWD
=
os
.
getcwd
()
user_id
=
subprocess
.
check_output
([
'
id
'
,
'
-u
'
]).
decode
()
user_id
=
subprocess
.
check_output
([
'
id
'
,
'
-u
'
]).
decode
()
group_id
=
subprocess
.
check_output
([
'
id
'
,
'
-g
'
]).
decode
()
group_id
=
subprocess
.
check_output
([
'
id
'
,
'
-g
'
]).
decode
()
...
@@ -407,6 +495,21 @@ def gdb_cyccnt_reset():
...
@@ -407,6 +495,21 @@ def gdb_cyccnt_reset():
gdb
.
execute
(
"
mon mww 0xe0001004 0
"
)
gdb
.
execute
(
"
mon mww 0xe0001004 0
"
)
def
gdb_cyccnt_read
():
# Read cycle counter
return
int
(
gdb
.
execute
(
"
mon mdw 0xe0001004
"
,
False
,
True
).
strip
(
'
\n
'
).
strip
(
'
0xe000012004:
'
).
strip
(
'
,
'
).
strip
(),
16
)
def
gdb_cyccnt_write
(
num
):
# Write to cycle counter
gdb
.
execute
(
'
mon mww 0xe0001004 %r
'
%
num
)
def
gdb_basepri_read
():
return
gdb
.
execute
(
"
readbasepri()
"
,
False
,
True
)
"""
Run KLEE on the generated files
"""
"""
Run KLEE on the generated files
"""
# print(klee_run())
# print(klee_run())
...
@@ -417,8 +520,8 @@ MainBP("init")
...
@@ -417,8 +520,8 @@ MainBP("init")
"""
Tell gdb-dashboard to hide
"""
"""
Tell gdb-dashboard to hide
"""
gdb
.
execute
(
"
dashboard -enabled off
"
)
#
gdb.execute("dashboard -enabled off")
gdb
.
execute
(
"
dashboard -output /dev/null
"
)
#
gdb.execute("dashboard -output /dev/null")
"""
Also break at the main-loop
"""
"""
Also break at the main-loop
"""
MainBP
(
"
idle
"
)
MainBP
(
"
idle
"
)
...
@@ -428,14 +531,15 @@ MainBP("idle")
...
@@ -428,14 +531,15 @@ MainBP("idle")
gdb
.
execute
(
"
set confirm off
"
)
gdb
.
execute
(
"
set confirm off
"
)
gdb
.
execute
(
"
set pagination off
"
)
gdb
.
execute
(
"
set pagination off
"
)
gdb
.
execute
(
"
set verbose off
"
)
gdb
.
execute
(
"
set verbose off
"
)
gdb
.
execute
(
"
set height 0
"
)
"""
Save all ktest files into an array
"""
"""
Save all ktest files into an array
"""
file_list
=
ktest_iterate
()
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
()
tasks
=
tasklist_get
()
print
(
tasks
)
print
(
tasks
)
"""
Run until the
main()
breakpoint
"""
"""
Run until the
next
breakpoint
"""
gdb
.
execute
(
"
c
"
)
gdb
.
execute
(
"
c
"
)
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