Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
Symbolic Executor
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Iterations
Wiki
Requirements
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Locked files
Build
Pipelines
Jobs
Pipeline schedules
Test cases
Artifacts
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Code review analytics
Issue analytics
Insights
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Blockchains
UTXO Chains
Symbolic Executor
Commits
48b2590f
Commit
48b2590f
authored
2 years ago
by
vincent
Browse files
Options
Downloads
Patches
Plain Diff
Add utils to compute number of paths in a program
parent
01cb9c53
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
symbolic_execution/program/block/utils.py
+75
-0
75 additions, 0 deletions
symbolic_execution/program/block/utils.py
with
75 additions
and
0 deletions
symbolic_execution/program/block/utils.py
0 → 100644
+
75
−
0
View file @
48b2590f
from
..block.interfaces
import
IInstructionBlock
import
numpy
as
np
from
typing
import
List
def
build_adjacency_matrix
(
start_block
:
IInstructionBlock
):
"""
Build the adjacency matrix of a program.
"""
# attribute to every block a number
visited
=
{}
to_visit
=
{
start_block
}
# Populate the set of all blocks
while
to_visit
:
block
=
to_visit
.
pop
()
if
block
not
in
visited
:
# attribute to every block a number
visited
[
block
]
=
len
(
visited
)
for
child
in
block
.
children
:
if
child
not
in
visited
:
to_visit
.
add
(
child
)
# Because the starting block is not necessary the root, we need to parse the parents
for
parent
in
block
.
parents
:
if
parent
not
in
visited
:
to_visit
.
add
(
parent
)
adjacency_matrix
=
np
.
zeros
((
len
(
visited
),
len
(
visited
)))
for
block
,
src_id
in
visited
.
items
():
for
child
in
block
.
children
:
dest_id
=
visited
[
child
]
adjacency_matrix
[
src_id
][
dest_id
]
=
1
return
adjacency_matrix
def
find_orphan_nodes
(
adjacency_matrix
)
->
List
[
int
]:
"""
Find the nodes without parents.
"""
sums
=
adjacency_matrix
.
sum
(
axis
=
0
)
return
(
sums
==
0
).
nonzero
()[
0
]
def
find_single_nodes
(
adjacency_matrix
)
->
List
[
int
]:
"""
Find the nodes without children.
"""
sums
=
adjacency_matrix
.
sum
(
axis
=
1
)
return
(
sums
==
0
).
nonzero
()[
0
]
def
compute_path_count
(
start_block
:
IInstructionBlock
,
max_path_length
=
None
)
->
int
:
"""
Compute the number of paths from an entry point of the program to a final block.
"""
adjacency_matrix
=
build_adjacency_matrix
(
start_block
)
orphan_nodes
=
find_orphan_nodes
(
adjacency_matrix
)
single_nodes
=
find_single_nodes
(
adjacency_matrix
)
converged
=
False
path_count
=
0
path_length
=
1
path_count_matrix
=
adjacency_matrix
while
not
converged
and
(
max_path_length
is
None
or
path_length
<=
max_path_length
):
# count the number of the paths of length {path_length}
for
start
in
orphan_nodes
:
for
end
in
single_nodes
:
path_count
+=
path_count_matrix
[
start
][
end
]
length_plus_one_paths
=
np
.
matmul
(
path_count_matrix
,
adjacency_matrix
)
# Note these conditions do not ensure the function will ever halt. Set
# max_path_length to be sure of it.
if
np
.
array_equiv
(
length_plus_one_paths
,
path_count_matrix
)
or
not
np
.
any
(
length_plus_one_paths
):
converged
=
True
path_count_matrix
=
length_plus_one_paths
path_length
+=
1
return
int
(
path_count
)
\ No newline at end of file
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