Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
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
pub
frama-c
Commits
abe9a1a8
Commit
abe9a1a8
authored
8 years ago
by
Kostyantyn Vorobyov
Browse files
Options
Downloads
Patches
Plain Diff
Namespace changes as per changes of terminology of shadow techniques
parent
a689d374
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+43
-41
43 additions, 41 deletions
...acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
with
43 additions
and
41 deletions
src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+
43
−
41
View file @
abe9a1a8
...
@@ -65,7 +65,7 @@
...
@@ -65,7 +65,7 @@
* These remaining bytes reuse the shadow of [0,7]. */
* These remaining bytes reuse the shadow of [0,7]. */
#define LONG_BLOCK_BOUNDARY(_size) (_size - _size%LONG_BLOCK)
#define LONG_BLOCK_BOUNDARY(_size) (_size - _size%LONG_BLOCK)
/*! \brief
Short
shadow of a long block consists of a 8-byte segment + a
/*! \brief
Primary
shadow of a long block consists of a 8-byte segment + a
* remainder. For instance, a 18-byte block is represented by two 8-byte
* remainder. For instance, a 18-byte block is represented by two 8-byte
* segments + 2 bytes. Each byte of a segment stores an offset in the secondary
* segments + 2 bytes. Each byte of a segment stores an offset in the secondary
* shadow. The offsets for each such segment can be expressed using the
* shadow. The offsets for each such segment can be expressed using the
...
@@ -225,7 +225,7 @@ static int freeable(void *ptr);
...
@@ -225,7 +225,7 @@ static int freeable(void *ptr);
# define DVALIDATE_HEAP_ACCESS(_addr, _size) \
# define DVALIDATE_HEAP_ACCESS(_addr, _size) \
DVALIDATE_SHADOW_LAYOUT; \
DVALIDATE_SHADOW_LAYOUT; \
DVASSERT(IS_ON_HEAP(
(uintptr_t)
_addr), \
DVASSERT(IS_ON_HEAP(_addr), \
"Expected heap location: %a\n ", _addr); \
"Expected heap location: %a\n ", _addr); \
DVASSERT(heap_allocated((uintptr_t)_addr, _size), \
DVASSERT(heap_allocated((uintptr_t)_addr, _size), \
"Operation on unallocated heap block [%a + %lu]\n ", _addr, _size)
"Operation on unallocated heap block [%a + %lu]\n ", _addr, _size)
...
@@ -233,7 +233,7 @@ static int freeable(void *ptr);
...
@@ -233,7 +233,7 @@ static int freeable(void *ptr);
# define segstr(_global) ((_global) ? "global" : "stack")
# define segstr(_global) ((_global) ? "global" : "stack")
# define DVALIDATE_STATIC_ACCESS(_addr, _size, _global) \
# define DVALIDATE_STATIC_ACCESS(_addr, _size, _global) \
DVALIDATE_SHADOW_LAYOUT; \
DVALIDATE_SHADOW_LAYOUT; \
DVASSERT(IS_ON_STATIC(
(uintptr_t)
_addr, _global), \
DVASSERT(IS_ON_STATIC(_addr, _global), \
"Expected %s location: %a\n ", segstr(_global), _addr); \
"Expected %s location: %a\n ", segstr(_global), _addr); \
DVASSERT(static_allocated((uintptr_t)_addr, _size, _global), \
DVASSERT(static_allocated((uintptr_t)_addr, _size, _global), \
"Operation on unallocated %s block [%a + %lu]\n ", \
"Operation on unallocated %s block [%a + %lu]\n ", \
...
@@ -241,7 +241,7 @@ static int freeable(void *ptr);
...
@@ -241,7 +241,7 @@ static int freeable(void *ptr);
# define DVALIDATE_STATIC_LOCATION(_addr, _global) \
# define DVALIDATE_STATIC_LOCATION(_addr, _global) \
DVALIDATE_SHADOW_LAYOUT; \
DVALIDATE_SHADOW_LAYOUT; \
DVASSERT(IS_ON_STATIC(
(uintptr_t)
_addr, _global), \
DVASSERT(IS_ON_STATIC(_addr, _global), \
"Expected %s location: %a\n ", segstr(_global), _addr); \
"Expected %s location: %a\n ", segstr(_global), _addr); \
DVASSERT(static_allocated_one((uintptr_t)_addr, _global), \
DVASSERT(static_allocated_one((uintptr_t)_addr, _global), \
"Operation on unallocated %s block [%a]\n ", segstr(_global), _addr)
"Operation on unallocated %s block [%a]\n ", segstr(_global), _addr)
...
@@ -306,11 +306,11 @@ static uintptr_t predicate(uintptr_t addr, char p) {
...
@@ -306,11 +306,11 @@ static uintptr_t predicate(uintptr_t addr, char p) {
#define block_length(_addr) predicate((uintptr_t)_addr, 'L')
#define block_length(_addr) predicate((uintptr_t)_addr, 'L')
/*! \brief Return a base address of a memory block address `_addr` belongs to
/*! \brief Return a base address of a memory block address `_addr` belongs to
* \param uintptr_t _addr - a memory address */
* \param uintptr_t _addr - a memory address */
#define base_addr(_addr)
predicate((uintptr_t)_addr, 'B')
#define base_addr(_addr) predicate((uintptr_t)_addr, 'B')
/*! \brief Return a byte offset of a memory address given by `_addr` within
/*! \brief Return a byte offset of a memory address given by `_addr` within
* its block
* its block
* \param uintptr_t _addr - a memory address */
* \param uintptr_t _addr - a memory address */
#define offset(_addr)
predicate((uintptr_t)_addr, 'O')
#define offset(_addr) predicate((uintptr_t)_addr, 'O')
/* }}} */
/* }}} */
/* Static allocation {{{ */
/* Static allocation {{{ */
...
@@ -336,39 +336,39 @@ static const char short_offsets_base [] = { 0, 1, 2, 4, 7, 11, 16, 22, 29 };
...
@@ -336,39 +336,39 @@ static const char short_offsets_base [] = { 0, 1, 2, 4, 7, 11, 16, 22, 29 };
static
void
shadow_alloca
(
void
*
ptr
,
size_t
size
,
int
global
)
{
static
void
shadow_alloca
(
void
*
ptr
,
size_t
size
,
int
global
)
{
DVALIDATE_SHADOW_LAYOUT
;
DVALIDATE_SHADOW_LAYOUT
;
unsigned
char
*
short
_shadow
ed
=
unsigned
char
*
prim
_shadow
=
(
unsigned
char
*
)
PRIMARY_SHADOW
(
ptr
,
global
);
(
unsigned
char
*
)
PRIMARY_SHADOW
(
ptr
,
global
);
uint64_t
*
short
_shadow
ed
_alt
=
uint64_t
*
prim
_shadow_alt
=
(
uint64_t
*
)
PRIMARY_SHADOW
(
ptr
,
global
);
(
uint64_t
*
)
PRIMARY_SHADOW
(
ptr
,
global
);
unsigned
int
*
long
_shadow
ed
=
unsigned
int
*
sec
_shadow
=
(
unsigned
int
*
)
SECONDARY_SHADOW
(
ptr
,
global
);
(
unsigned
int
*
)
SECONDARY_SHADOW
(
ptr
,
global
);
/* Flip read-only bit for zero-size blocks. That is, physically it exists
/* Flip read-only bit for zero-size blocks. That is, physically it exists
* but one cannot write to it. Further, the flipped read-only bit will also
* but one cannot write to it. Further, the flipped read-only bit will also
* identify such block as allocated */
* identify such block as allocated */
if
(
!
size
)
if
(
!
size
)
setbit
(
READONLY_BIT
,
short
_shadow
ed
[
0
]);
setbit
(
READONLY_BIT
,
prim
_shadow
[
0
]);
unsigned
int
i
,
j
=
0
,
k
=
0
;
unsigned
int
i
,
j
=
0
,
k
=
0
;
if
(
IS_LONG_BLOCK
(
size
))
{
/* Long blocks */
if
(
IS_LONG_BLOCK
(
size
))
{
/* Long blocks */
int
boundary
=
LONG_BLOCK_BOUNDARY
(
size
);
int
boundary
=
LONG_BLOCK_BOUNDARY
(
size
);
for
(
i
=
0
;
i
<
boundary
;
i
+=
LONG_BLOCK
)
{
for
(
i
=
0
;
i
<
boundary
;
i
+=
LONG_BLOCK
)
{
/* Set
values for a long shadow
*/
/* Set
-up a secondary shadow segment
*/
long
_shadow
ed
[
j
++
]
=
size
;
sec
_shadow
[
j
++
]
=
size
;
long
_shadow
ed
[
j
++
]
=
i
;
sec
_shadow
[
j
++
]
=
i
;
/* Set
offsets in the short shadow
*/
/* Set
primary shadow offsets
*/
short
_shadow
ed
_alt
[
k
++
]
=
LONG_BLOCK_MASK
;
prim
_shadow_alt
[
k
++
]
=
LONG_BLOCK_MASK
;
}
}
/* Write out the remainder */
/* Write out the remainder */
for
(
i
=
boundary
;
i
<
size
;
i
++
)
{
for
(
i
=
boundary
;
i
<
size
;
i
++
)
{
unsigned
char
offset
=
i
%
LONG_BLOCK
+
LONG_BLOCK_INDEX_START
+
LONG_BLOCK
;
unsigned
char
offset
=
i
%
LONG_BLOCK
+
LONG_BLOCK_INDEX_START
+
LONG_BLOCK
;
short
_shadow
ed
[
i
]
=
(
offset
<<
2
);
prim
_shadow
[
i
]
=
(
offset
<<
2
);
}
}
}
else
{
/* Short blocks */
}
else
{
/* Short blocks */
for
(
i
=
0
;
i
<
size
;
i
++
)
{
for
(
i
=
0
;
i
<
size
;
i
++
)
{
unsigned
char
code
=
short_offsets_base
[
size
]
+
i
;
unsigned
char
code
=
short_offsets_base
[
size
]
+
i
;
short
_shadow
ed
[
i
]
=
(
code
<<
2
);
prim
_shadow
[
i
]
=
(
code
<<
2
);
}
}
}
}
}
}
...
@@ -409,18 +409,18 @@ static void static_shadow_freea(void *ptr, int global) {
...
@@ -409,18 +409,18 @@ static void static_shadow_freea(void *ptr, int global) {
* applied to a stack or global address. */
* applied to a stack or global address. */
static
int
static_allocated
(
uintptr_t
addr
,
long
size
,
int
global
)
{
static
int
static_allocated
(
uintptr_t
addr
,
long
size
,
int
global
)
{
DVALIDATE_SHADOW_LAYOUT
;
DVALIDATE_SHADOW_LAYOUT
;
unsigned
char
*
short
_shadow
ed
=
(
unsigned
char
*
)
PRIMARY_SHADOW
(
addr
,
global
);
unsigned
char
*
prim
_shadow
=
(
unsigned
char
*
)
PRIMARY_SHADOW
(
addr
,
global
);
/* Unless the address belongs to tracked allocation 0 is returned */
/* Unless the address belongs to tracked allocation 0 is returned */
if
(
short
_shadow
ed
[
0
])
{
if
(
prim
_shadow
[
0
])
{
unsigned
int
code
=
(
short
_shadow
ed
[
0
]
>>
2
);
unsigned
int
code
=
(
prim
_shadow
[
0
]
>>
2
);
unsigned
int
long_block
=
(
code
>=
LONG_BLOCK_INDEX_START
);
unsigned
int
long_block
=
(
code
>=
LONG_BLOCK_INDEX_START
);
size_t
length
,
offset
;
size_t
length
,
offset
;
if
(
long_block
)
{
if
(
long_block
)
{
offset
=
code
-
LONG_BLOCK_INDEX_START
;
offset
=
code
-
LONG_BLOCK_INDEX_START
;
unsigned
int
*
long
_shadow
ed
=
unsigned
int
*
sec
_shadow
=
(
unsigned
int
*
)
SECONDARY_SHADOW
(
addr
-
offset
,
global
)
;
(
unsigned
int
*
)
SECONDARY_SHADOW
(
addr
-
offset
,
global
)
;
length
=
long
_shadow
ed
[
0
];
length
=
sec
_shadow
[
0
];
offset
=
long
_shadow
ed
[
1
]
+
offset
;
offset
=
sec
_shadow
[
1
]
+
offset
;
}
else
{
}
else
{
offset
=
short_offsets
[
code
];
offset
=
short_offsets
[
code
];
length
=
short_lengths
[
code
];
length
=
short_lengths
[
code
];
...
@@ -490,23 +490,23 @@ static int static_initialized(uintptr_t addr, long size, int global) {
...
@@ -490,23 +490,23 @@ static int static_initialized(uintptr_t addr, long size, int global) {
* unspecified. */
* unspecified. */
static
uintptr_t
static_info
(
uintptr_t
addr
,
char
type
,
int
global
)
{
static
uintptr_t
static_info
(
uintptr_t
addr
,
char
type
,
int
global
)
{
DVALIDATE_STATIC_LOCATION
(
addr
,
global
);
DVALIDATE_STATIC_LOCATION
(
addr
,
global
);
unsigned
char
*
short
_shadow
ed
=
(
unsigned
char
*
)
PRIMARY_SHADOW
(
addr
,
global
);
unsigned
char
*
prim
_shadow
=
(
unsigned
char
*
)
PRIMARY_SHADOW
(
addr
,
global
);
/* Unless the address belongs to tracked allocation 0 is returned */
/* Unless the address belongs to tracked allocation 0 is returned */
if
(
short
_shadow
ed
[
0
])
{
if
(
prim
_shadow
[
0
])
{
unsigned
int
code
=
(
short
_shadow
ed
[
0
]
>>
2
);
unsigned
int
code
=
(
prim
_shadow
[
0
]
>>
2
);
unsigned
int
long_block
=
(
code
>=
LONG_BLOCK_INDEX_START
);
unsigned
int
long_block
=
(
code
>=
LONG_BLOCK_INDEX_START
);
if
(
long_block
)
{
if
(
long_block
)
{
unsigned
int
offset
=
code
-
LONG_BLOCK_INDEX_START
;
unsigned
int
offset
=
code
-
LONG_BLOCK_INDEX_START
;
unsigned
int
*
long
_shadow
ed
=
unsigned
int
*
sec
_shadow
=
(
unsigned
int
*
)
SECONDARY_SHADOW
(
addr
-
offset
,
global
)
;
(
unsigned
int
*
)
SECONDARY_SHADOW
(
addr
-
offset
,
global
)
;
switch
(
type
)
{
switch
(
type
)
{
case
'B'
:
/* Base address */
case
'B'
:
/* Base address */
return
addr
-
offset
-
long
_shadow
ed
[
1
];
return
addr
-
offset
-
sec
_shadow
[
1
];
case
'O'
:
/* Offset */
case
'O'
:
/* Offset */
return
long
_shadow
ed
[
1
]
+
offset
;
return
sec
_shadow
[
1
]
+
offset
;
case
'L'
:
/* Length */
case
'L'
:
/* Length */
return
long
_shadow
ed
[
0
];
return
sec
_shadow
[
0
];
default:
default:
DASSERT
(
0
&&
"Unknown static query type"
);
DASSERT
(
0
&&
"Unknown static query type"
);
}
}
...
@@ -1084,11 +1084,11 @@ static void initialize(void *ptr, size_t n) {
...
@@ -1084,11 +1084,11 @@ static void initialize(void *ptr, size_t n) {
* shadow */
* shadow */
static
void
printbyte
(
unsigned
char
c
,
char
buf
[])
{
static
void
printbyte
(
unsigned
char
c
,
char
buf
[])
{
if
(
c
>>
2
<
LONG_BLOCK_INDEX_START
)
{
if
(
c
>>
2
<
LONG_BLOCK_INDEX_START
)
{
sprintf
(
buf
,
"
SHORT
: I{%u} RO{%u} OF{%2u} => %u[%u]"
,
sprintf
(
buf
,
"
PRIMARY
: I{%u} RO{%u} OF{%2u} => %u[%u]"
,
checkbit
(
INIT_BIT
,
c
),
checkbit
(
READONLY_BIT
,
c
),
c
>>
2
,
checkbit
(
INIT_BIT
,
c
),
checkbit
(
READONLY_BIT
,
c
),
c
>>
2
,
short_lengths
[
c
>>
2
],
short_offsets
[
c
>>
2
]);
short_lengths
[
c
>>
2
],
short_offsets
[
c
>>
2
]);
}
else
{
}
else
{
sprintf
(
buf
,
"
LONG
: I{%u} RO{%u} OF{%u} => %4u"
,
sprintf
(
buf
,
"
SECONDARY
: I{%u} RO{%u} OF{%u} => %4u"
,
checkbit
(
INIT_BIT
,
c
),
checkbit
(
READONLY_BIT
,
c
),
checkbit
(
INIT_BIT
,
c
),
checkbit
(
READONLY_BIT
,
c
),
(
c
>>
2
),
(
c
>>
2
)
-
LONG_BLOCK_INDEX_START
);
(
c
>>
2
),
(
c
>>
2
)
-
LONG_BLOCK_INDEX_START
);
}
}
...
@@ -1097,27 +1097,27 @@ static void printbyte(unsigned char c, char buf[]) {
...
@@ -1097,27 +1097,27 @@ static void printbyte(unsigned char c, char buf[]) {
/*! \brief Print human-readable (well, ish) representation of a memory block
/*! \brief Print human-readable (well, ish) representation of a memory block
* using primary and secondary shadows. */
* using primary and secondary shadows. */
static
void
print_static_shadows
(
uintptr_t
addr
,
size_t
size
,
int
global
)
{
static
void
print_static_shadows
(
uintptr_t
addr
,
size_t
size
,
int
global
)
{
char
short
_buf
[
256
];
char
prim
_buf
[
256
];
char
long
_buf
[
256
];
char
sec
_buf
[
256
];
unsigned
char
*
short
_shadow
ed
=
(
unsigned
char
*
)
PRIMARY_SHADOW
(
addr
,
global
);
unsigned
char
*
prim
_shadow
=
(
unsigned
char
*
)
PRIMARY_SHADOW
(
addr
,
global
);
unsigned
int
*
long
_shadow
ed
=
(
unsigned
int
*
)
SECONDARY_SHADOW
(
addr
,
global
);
unsigned
int
*
sec
_shadow
=
(
unsigned
int
*
)
SECONDARY_SHADOW
(
addr
,
global
);
int
i
,
j
=
0
;
int
i
,
j
=
0
;
for
(
i
=
0
;
i
<
size
;
i
++
)
{
for
(
i
=
0
;
i
<
size
;
i
++
)
{
long
_buf
[
0
]
=
'\0'
;
sec
_buf
[
0
]
=
'\0'
;
printbyte
(
short
_shadow
ed
[
i
],
short
_buf
);
printbyte
(
prim
_shadow
[
i
],
prim
_buf
);
if
(
IS_LONG_BLOCK
(
size
)
&&
(
i
%
LONG_BLOCK
)
==
0
)
{
if
(
IS_LONG_BLOCK
(
size
)
&&
(
i
%
LONG_BLOCK
)
==
0
)
{
j
+=
2
;
j
+=
2
;
if
(
i
<
LONG_BLOCK_BOUNDARY
(
size
))
{
if
(
i
<
LONG_BLOCK_BOUNDARY
(
size
))
{
sprintf
(
long
_buf
,
" %a SZ{%u} OF{%u}"
,
sprintf
(
sec
_buf
,
" %a SZ{%u} OF{%u}"
,
&
long
_shadow
ed
[
j
],
long
_shadow
ed
[
j
-
2
],
long
_shadow
ed
[
j
-
1
]);
&
sec
_shadow
[
j
],
sec
_shadow
[
j
-
2
],
sec
_shadow
[
j
-
1
]);
}
}
if
(
i
)
{
if
(
i
)
{
DLOG
(
"---------------------------------------------
\n
"
);
DLOG
(
"---------------------------------------------
\n
"
);
}
}
}
}
DLOG
(
"| [%2d] %a | %s || %s
\n
"
,
i
,
&
short
_shadow
ed
[
i
],
short
_buf
,
long
_buf
);
DLOG
(
"| [%2d] %a | %s || %s
\n
"
,
i
,
&
prim
_shadow
[
i
],
prim
_buf
,
sec
_buf
);
}
}
}
}
...
@@ -1184,6 +1184,8 @@ static void which_segment(uintptr_t addr) {
...
@@ -1184,6 +1184,8 @@ static void which_segment(uintptr_t addr) {
loc
=
"heap"
;
loc
=
"heap"
;
else
if
(
IS_ON_GLOBAL
(
addr
))
else
if
(
IS_ON_GLOBAL
(
addr
))
loc
=
"global"
;
loc
=
"global"
;
else
if
(
IS_ON_TLS
(
addr
))
loc
=
"TLS"
;
else
else
loc
=
"untracked"
;
loc
=
"untracked"
;
DLOG
(
"Address: %a -> %s
\n
"
,
addr
,
loc
);
DLOG
(
"Address: %a -> %s
\n
"
,
addr
,
loc
);
...
...
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