Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
Lustrec - public version
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
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
LustreC
Lustrec - public version
Commits
a5dc55ca
Commit
a5dc55ca
authored
6 years ago
by
Pierre Loic Garoche
Browse files
Options
Downloads
Patches
Plain Diff
Restructuring code in SEAL
parent
82906771
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/tools/seal_utils.ml
+92
-81
92 additions, 81 deletions
src/tools/seal_utils.ml
with
92 additions
and
81 deletions
src/tools/seal_utils.ml
+
92
−
81
View file @
a5dc55ca
...
@@ -2,91 +2,102 @@ open Lustre_types
...
@@ -2,91 +2,102 @@ open Lustre_types
open
Utils
open
Utils
let
report
=
Log
.
report
~
plugin
:
"seal"
let
report
=
Log
.
report
~
plugin
:
"seal"
let
compute_sliced_vars
vars_to_keep
deps
nd
=
let
is_variable
vid
=
List
.
exists
(
fun
v
->
v
.
var_id
=
vid
)
nd
.
node_locals
in
let
find_variable
vid
=
List
.
find
(
fun
v
->
v
.
var_id
=
vid
)
nd
.
node_locals
in
(* Returns the vars required to compute v.
Memories are specifically identified. *)
let
coi_var
v
=
(******************************************************************************)
let
vname
=
v
.
var_id
in
(* Computing a slice of a node, selecting only some variables, based on *)
let
sliced_deps
=
(* their COI (cone of influence) *)
Causality
.
slice_graph
deps
vname
(******************************************************************************)
in
(* Format.eprintf "sliced graph for %a: %a@."
* Printers.pp_var v
* Causality.pp_dep_graph sliced_deps; *)
let
vset
,
memset
=
IdentDepGraph
.
fold_vertex
(
fun
vname
(
vset
,
memset
)
->
if
Causality
.
ExprDep
.
is_read_var
vname
then
let
vname'
=
String
.
sub
vname
1
(
-
1
+
String
.
length
vname
)
in
if
is_variable
vname'
then
ISet
.
add
vname'
vset
,
ISet
.
add
vname'
memset
else
vset
,
memset
else
ISet
.
add
vname
vset
,
memset
)
sliced_deps
(
ISet
.
singleton
vname
,
ISet
.
empty
)
in
report
~
level
:
3
(
fun
fmt
->
Format
.
fprintf
fmt
"COI of var %s: (%a // %a)@."
v
.
var_id
(
fprintf_list
~
sep
:
","
Format
.
pp_print_string
)
(
ISet
.
elements
vset
)
(
fprintf_list
~
sep
:
","
Format
.
pp_print_string
)
(
ISet
.
elements
memset
)
)
;
vset
,
memset
in
(*
Computes the variables required to compute
(*
Basic functions to search into nodes. Could be moved to corelang eventually *)
vl. Variables /seen/ do not need to
let
is_variable
nd
vid
=
be computed *)
List
.
exists
let
rec
coi_vars
vl
seen
=
(
fun
v
->
v
.
var_id
=
vid
)
List
.
fold_left
nd
.
node_locals
(
fun
accu
v
->
let
vset
,
memset
=
coi_var
v
in
let
find_variable
nd
vid
=
(* We handle the new mems
List
.
find
discovered in the coi *
)
(
fun
v
->
v
.
var_id
=
vid
)
let
memset
=
nd
.
node_locals
ISet
.
filter
(
fun
vid
->
(* Returns the vars required to compute v.
not
Memories are specifically identified. *)
(
List
.
exists
let
coi_var
deps
nd
v
=
(
fun
v
->
v
.
var_id
=
vid
)
let
vname
=
v
.
var_id
in
vl
let
sliced_deps
=
)
Causality
.
slice_graph
deps
vname
)
memset
in
in
(* Format.eprintf "sliced graph for %a: %a@."
let
memset_vars
=
*
Printers.pp_var v
ISet
.
fold
(
*
Causality.pp_dep_graph sliced_deps; *)
fun
vid
accu
->
let
vset
,
memset
=
(
find_variable
vid
)
::
accu
IdentDepGraph
.
fold_vertex
)
memset
[]
(
fun
vname
(
vset
,
memset
)
->
in
if
Causality
.
ExprDep
.
is_read_var
vname
let
vset'
=
then
coi_vars
memset_vars
(
vl
@
seen
)
let
vname'
=
String
.
sub
vname
1
(
-
1
+
String
.
length
vname
)
in
i
n
if
is_variable
nd
vname'
the
n
ISet
.
union
accu
(
ISet
.
union
vset
vset
'
)
ISet
.
add
vname'
vset
,
)
ISet
.
add
vname'
memset
ISet
.
empty
else
(
List
.
filter
vset
,
memset
(
fun
v
->
not
(
List
.
mem
v
seen
))
else
vl
ISet
.
add
vname
vset
,
memset
)
)
sliced_deps
(
ISet
.
singleton
vname
,
ISet
.
empty
)
in
in
ISet
.
elements
(
coi_vars
vars_to_keep
[]
)
report
~
level
:
3
(
fun
fmt
->
Format
.
fprintf
fmt
"COI of var %s: (%a // %a)@."
v
.
var_id
(
fprintf_list
~
sep
:
","
Format
.
pp_print_string
)
(
ISet
.
elements
vset
)
(
fprintf_list
~
sep
:
","
Format
.
pp_print_string
)
(
ISet
.
elements
memset
)
)
;
vset
,
memset
(* Computes the variables required to compute vl. Variables /seen/ do not need
to be computed *)
let
rec
coi_vars
deps
nd
vl
seen
=
let
coi_vars
=
coi_vars
deps
nd
in
List
.
fold_left
(
fun
accu
v
->
let
vset
,
memset
=
coi_var
deps
nd
v
in
(* We handle the new mems discovered in the coi *)
let
memset
=
ISet
.
filter
(
fun
vid
->
not
(
List
.
exists
(
fun
v
->
v
.
var_id
=
vid
)
vl
)
)
memset
in
let
memset_vars
=
ISet
.
fold
(
fun
vid
accu
->
(
find_variable
nd
vid
)
::
accu
)
memset
[]
in
let
vset'
=
coi_vars
memset_vars
(
vl
@
seen
)
in
ISet
.
union
accu
(
ISet
.
union
vset
vset'
)
)
ISet
.
empty
(
List
.
filter
(
fun
v
->
not
(
List
.
mem
v
seen
))
vl
)
(* compute the coi of vars_to_keeps in node nd *)
let
compute_sliced_vars
vars_to_keep
deps
nd
=
ISet
.
elements
(
coi_vars
deps
nd
vars_to_keep
[]
)
(* If existing outputs are included in vars_to_keep, just slice the content.
(* If existing outputs are included in vars_to_keep, just slice the content.
...
...
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