Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
5cf9ae85
Commit
5cf9ae85
authored
Feb 14, 2020
by
Michele Alberti
Browse files
[kernel] Extract from Cil the visitor for const globals substitution into a new file.
parent
c2bc7ca5
Changes
7
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
5cf9ae85
...
...
@@ -565,6 +565,7 @@ KERNEL_CMO=\
src/kernel_internals/typing/rmtmps.cmo
\
src/kernel_internals/typing/oneret.cmo
\
src/kernel_internals/typing/frontc.cmo
\
src/kernel_internals/typing/substitute_const_globals.cmo
\
src/kernel_services/analysis/ordered_stmt.cmo
\
src/kernel_services/analysis/wto_statement.cmo
\
src/kernel_services/analysis/dataflows.cmo
\
...
...
headers/header_spec.txt
View file @
5cf9ae85
...
...
@@ -405,6 +405,8 @@ src/kernel_internals/typing/translate_lightweight.ml: CEA_INRIA_LGPL
src/kernel_internals/typing/translate_lightweight.mli: CEA_INRIA_LGPL
src/kernel_internals/typing/unroll_loops.ml: CEA_LGPL
src/kernel_internals/typing/unroll_loops.mli: CEA_LGPL
src/kernel_internals/typing/substitute_const_globals.ml: CEA_LGPL
src/kernel_internals/typing/substitute_const_globals.mli: CEA_LGPL
src/kernel_services/README.md: .ignore
src/kernel_services/abstract_interp/README.md: .ignore
src/kernel_services/abstract_interp/abstract_interp.ml: CEA_LGPL
...
...
src/kernel_internals/typing/substitute_const_globals.ml
0 → 100644
View file @
5cf9ae85
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2019 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* Syntactic substitution of globals, defined with the attribute 'const', with
respective initializers. *)
open
Cil_types
open
Cil_datatype
open
Cil
class
constGlobSubstVisitorClass
:
cilVisitor
=
object
inherit
nopCilVisitor
val
vi_to_init_opt
=
Varinfo
.
Hashtbl
.
create
7
(* Visit globals and register only the association between globals with attribute
'const' and respective initializers. *)
method
!
vglob
g
=
let
rec
is_arithmetic_type
=
function
|
TArray
(
typ
,
_
,
_
,
_
)
->
is_arithmetic_type
typ
|
TInt
_
|
TFloat
_
|
TEnum
_
->
true
|
_
->
false
in
match
g
with
|
GVar
(
vi
,
_
,
_
)
->
(* Register in [vi_to_init_opt] the association between [vi] and its
initializer [init_opt]. The latter is assumed to be an expression of
literal constants only, as the lvals originally appearing in it have
been substituted by the respective initializers in method [vexpr]. *)
let
register
=
function
|
GVar
(
vi
,
{
init
=
init_opt
}
,
_loc
)
as
g
->
Varinfo
.
Hashtbl
.
add
vi_to_init_opt
vi
init_opt
;
g
|
_
->
(* Cannot happen as we treat only [GVar _] cases in the outer
pattern matching. *)
assert
false
in
let
typ
=
unrollTypeDeep
vi
.
vtype
in
if
is_arithmetic_type
typ
&&
isConstType
typ
then
ChangeDoChildrenPost
([
g
]
,
List
.
map
register
)
else
DoChildren
|
_
->
DoChildren
(* Visit expressions and replace lvals, with a registered varinfo in
[vi_to_init_opt], with respective initializing constant expressions. *)
method
!
vexpr
e
=
match
e
.
enode
with
|
Lval
(
Var
vi
,
(
NoOffset
|
Index
_
as
offset
))
->
(* Support for variables and array, on arithmetic types only. *)
begin
match
Varinfo
.
Hashtbl
.
find
vi_to_init_opt
vi
with
|
None
->
(* Since [vi] is a global, we replace it with the zero expression,
i.e. the implicit initializer for such globals. *)
let
newexp
=
zero
~
loc
:
e
.
eloc
in
ChangeTo
newexp
|
Some
init
->
let
offset
=
constFoldOffset
true
offset
in
let
zero_exp
=
zero
~
loc
:
e
.
eloc
in
let
rec
find_replace
current_offset
current_init
current_newexp
=
match
current_init
with
|
SingleInit
si
->
if
Cil_datatype
.
OffsetStructEq
.
equal
offset
current_offset
then
new_exp
~
loc
:
e
.
eloc
si
.
enode
else
current_newexp
|
CompoundInit
(
ct
,
initl
)
->
(* We are dealing with an array: recursively [find_replace] among
its initializers. *)
foldLeftCompound
~
implicit
:
true
~
doinit
:
(
fun
coffset
cinit
_
acc
->
find_replace
(
addOffset
coffset
current_offset
)
cinit
acc
)
~
ct
~
initl
~
acc
:
current_newexp
in
let
newexp
=
find_replace
NoOffset
init
zero_exp
in
ChangeTo
newexp
|
exception
Not_found
->
DoChildren
end
|
_
->
DoChildren
end
let
constGlobSubstVisitor
=
new
constGlobSubstVisitorClass
src/kernel_internals/typing/substitute_const_globals.mli
0 → 100644
View file @
5cf9ae85
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2019 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(** A visitor that substitutes globals, defined with the attribute 'const', with
respective initializers. *)
val
constGlobSubstVisitor
:
Cil
.
cilVisitor
src/kernel_services/ast_queries/cil.ml
View file @
5cf9ae85
...
...
@@ -6305,86 +6305,6 @@ let foldLeftCompound
|
_
->
Kernel
.
fatal
~
current
:
true
"Type of Compound is not array or struct or union"
class
constGlobSubstVisitorClass
:
cilVisitor
=
object
inherit
nopCilVisitor
val
vi_to_init_opt
=
Varinfo
.
Hashtbl
.
create
7
(* Visit globals and register only the association between globals with attribute
'const' and respective initializers. *)
method
!
vglob
g
=
let
rec
is_arithmetic_type
=
function
|
TArray
(
typ
,
_
,
_
,
_
)
->
is_arithmetic_type
typ
|
TInt
_
|
TFloat
_
|
TEnum
_
->
true
|
_
->
false
in
match
g
with
|
GVar
(
vi
,
_
,
_
)
->
(* Register in [vi_to_init_opt] the association between [vi] and its
initializer [init_opt]. The latter is assumed to be an expression of
literal constants only, as the lvals originally appearing in it have
been substituted by the respective initializers in method [vexpr]. *)
let
register
=
function
|
GVar
(
vi
,
{
init
=
init_opt
}
,
_loc
)
as
g
->
Varinfo
.
Hashtbl
.
add
vi_to_init_opt
vi
init_opt
;
g
|
_
->
(* Cannot happen as we treat only [GVar _] cases in the outer
pattern matching. *)
assert
false
in
let
typ
=
unrollTypeDeep
vi
.
vtype
in
if
is_arithmetic_type
typ
&&
isConstType
typ
then
ChangeDoChildrenPost
([
g
]
,
List
.
map
register
)
else
DoChildren
|
_
->
DoChildren
(* Visit expressions and replace lvals, with a registered varinfo in
[vi_to_init_opt], with respective initializing constant expressions. *)
method
!
vexpr
e
=
match
e
.
enode
with
|
Lval
(
Var
vi
,
(
NoOffset
|
Index
_
as
offset
))
->
(* Support for variables and array, on arithmetic types only. *)
begin
match
Varinfo
.
Hashtbl
.
find
vi_to_init_opt
vi
with
|
None
->
(* Since [vi] is a global, we replace it with the zero expression,
i.e. the implicit initializer for such globals. *)
let
newexp
=
zero
~
loc
:
e
.
eloc
in
ChangeTo
newexp
|
Some
init
->
let
offset
=
constFoldOffset
true
offset
in
let
zero_exp
=
zero
~
loc
:
e
.
eloc
in
let
rec
find_replace
current_offset
current_init
current_newexp
=
match
current_init
with
|
SingleInit
si
->
if
Cil_datatype
.
OffsetStructEq
.
equal
offset
current_offset
then
new_exp
~
loc
:
e
.
eloc
si
.
enode
else
current_newexp
|
CompoundInit
(
ct
,
initl
)
->
(* We are dealing with an array: recursively [find_replace] among
its initializers. *)
foldLeftCompound
~
implicit
:
true
~
doinit
:
(
fun
coffset
cinit
_
acc
->
find_replace
(
addOffset
coffset
current_offset
)
cinit
acc
)
~
ct
~
initl
~
acc
:
current_newexp
in
let
newexp
=
find_replace
NoOffset
init
zero_exp
in
ChangeTo
newexp
|
exception
Not_found
->
DoChildren
end
|
_
->
DoChildren
end
let
constGlobSubstVisitor
=
new
constGlobSubstVisitorClass
let
has_flexible_array_member
t
=
let
is_flexible_array
t
=
match
unrollType
t
with
...
...
src/kernel_services/ast_queries/cil.mli
View file @
5cf9ae85
...
...
@@ -893,6 +893,10 @@ val constFoldTermNodeAtTop: term_node -> term_node
and [alignof]. *)
val
constFoldTerm
:
bool
->
term
->
term
(** Do constant folding on a {!Cil_types.offset}. If the second argument is true
then will also compute compiler-dependent expressions such as [sizeof]. *)
val
constFoldOffset
:
bool
->
offset
->
offset
(** Do constant folding on a binary operation. The bulk of the work done by
[constFold] is done here. If the second argument is true then
will also compute compiler-dependent expressions such as [sizeof]. *)
...
...
@@ -1971,10 +1975,6 @@ val is_skip: stmtkind -> bool
machine specific simplifications to be done, or not. *)
val
constFoldVisitor
:
bool
->
cilVisitor
(** A visitor that substitutes globals, defined with the attribute 'const', by
their constant initializing expressions. *)
val
constGlobSubstVisitor
:
cilVisitor
(* ************************************************************************* *)
(** {2 Debugging support} *)
(* ************************************************************************* *)
...
...
src/kernel_services/ast_queries/file.ml
View file @
5cf9ae85
...
...
@@ -1105,7 +1105,10 @@ let () =
let
constglobfold
=
register_code_transformation_category
"constglobfold"
in
let
syntactic_const_globals_substitution
ast
=
if
Kernel
.
Constfold
.
get
()
then
Cil
.
visitCilFileSameGlobals
Cil
.
constGlobSubstVisitor
ast
then
Cil
.
visitCilFileSameGlobals
Substitute_const_globals
.
constGlobSubstVisitor
ast
in
add_code_transformation_before_cleanup
~
deps
:
[
(
module
Kernel
.
Constfold
:
Parameter_sig
.
S
)
]
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment