Commit 38dd0000 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Remane readonly to mark_readonly and More defensive macros

parent a8666eb0
......@@ -238,9 +238,9 @@ let mk_delete_stmt vi =
mk_call ~loc (mk_api_name "delete_block") [ Cil.evar ~loc vi ]
| _ -> mk_call ~loc (mk_api_name "delete_block") [ Cil.mkAddrOfVi vi ]
let mk_readonly vi =
let mk_mark_readonly vi =
let loc = vi.vdecl in
mk_call ~loc (mk_api_name "readonly") [ Cil.evar ~loc vi ]
mk_call ~loc (mk_api_name "mark_readonly") [ Cil.evar ~loc vi ]
(* ************************************************************************** *)
(** {2 Other stuff} *)
......
......@@ -73,7 +73,7 @@ val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
val mk_delete_stmt: varinfo -> stmt
val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
val mk_initialize: loc:location -> lval -> stmt
val mk_readonly: varinfo -> stmt
val mk_mark_readonly: varinfo -> stmt
(* ************************************************************************** *)
(** {2 Other stuff} *)
......
......@@ -154,7 +154,7 @@ static void full_init (void * ptr) {
}
/* mark a block as read-only */
static void readonly(void * ptr) {
static void mark_readonly(void * ptr) {
bt_block * tmp;
if (ptr == NULL)
return;
......@@ -212,11 +212,21 @@ static size_t block_length(void* ptr) {
return tmp->size;
}
static int allocated(void* ptr, size_t size, void *ptr_base) {
bt_block * blk = bt_find(ptr);
bt_block * blk_base = bt_find(ptr_base);
if (blk == NULL || blk_base == NULL || blk->ptr != blk_base->ptr)
return false;
return (blk->size - ((size_t)ptr - blk->ptr) >= size);
}
/* return whether the size bytes of ptr are readable/writable */
static int valid(void* ptr, size_t size, void *ptr_base) {
/* Many similarities with allocated (so far at least), but it is better
* to use this tandalone definition, otherwise the block needs to be looked
* up twice */
bt_block * blk = bt_find(ptr);
bt_block * blk_base = bt_find(ptr_base);
if (blk == NULL || blk_base == NULL || blk->ptr != blk_base->ptr)
return false;
return (blk->size - ((size_t)ptr - blk->ptr) >= size && !blk->is_readonly);
......@@ -224,12 +234,7 @@ static int valid(void* ptr, size_t size, void *ptr_base) {
/* return whether the size bytes of ptr are readable */
static int valid_read(void* ptr, size_t size, void *ptr_base) {
bt_block * blk = bt_find(ptr);
bt_block * blk_base = bt_find(ptr_base);
if (blk == NULL || blk_base == NULL || blk->ptr != blk_base->ptr)
return false;
return (blk->size - ((size_t)ptr - blk->ptr) >= size);
return allocated(ptr, size, ptr_base);
}
/* return the base address of the block containing ptr */
......@@ -396,7 +401,7 @@ static int bittree_posix_memalign(void **memptr, size_t alignment, size_t size)
return -1;
/* Make sure that the first argument to posix memalign is indeed allocated */
vassert(valid(memptr, sizeof(void*), memptr),
vassert(allocated((void*)memptr, sizeof(void*), (void*)memptr),
"\\invalid memptr in posix_memalign", NULL);
int res = native_posix_memalign(memptr, alignment, size);
......@@ -595,7 +600,7 @@ public_alias(valid)
public_alias(block_length)
public_alias(initialized)
public_alias(freeable)
public_alias(readonly)
public_alias(mark_readonly)
/* Block initialization */
public_alias(initialize)
public_alias(full_init)
......
......@@ -112,7 +112,7 @@ void __e_acsl_full_init(void * ptr)
/*! \brief Mark a memory block which start address is given by \p ptr as
* read-only. */
/*@ assigns \nothing; */
void __e_acsl_readonly(void * ptr)
void __e_acsl_mark_readonly(void * ptr)
__attribute__((FC_BUILTIN));
/* ****************** */
......
......@@ -69,8 +69,8 @@ static void full_init(void * ptr) {
initialize(ptr, block_length(ptr));
}
static void readonly(void * ptr) {
mark_readonly((uintptr_t)ptr, block_length(ptr));
static void mark_readonly(void * ptr) {
mark_readonly_region((uintptr_t)ptr, block_length(ptr));
}
/* ****************** */
......@@ -102,6 +102,13 @@ static int valid_read(void * ptr, size_t size, void *ptr_base) {
return 0;
}
/** \brief Return 1 if a given memory location is read-only and 0 otherwise */
static int readonly (void *ptr) {
uintptr_t addr = (uintptr_t)ptr;
DVALIDATE_ALLOCATED(addr, 1, addr);
return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
}
/*! NB: The implementation for this function can also be specified via
* \p base_addr macro that will eventually call ::TRY_SEGMENT. The following
* implementation is preferred for performance reasons. */
......@@ -199,8 +206,8 @@ public_alias(valid_read)
public_alias(valid)
public_alias(initialized)
public_alias(freeable)
public_alias(readonly)
/* Block initialization */
public_alias(mark_readonly)
public_alias(initialize)
public_alias(full_init)
/* Memory state initialization */
......
......@@ -352,16 +352,23 @@ static void validate_memory_layout() {
DVASSERT(zeroed_out((void *)_addr, _size), \
"Block [%a, %a+%lu] not nullified", _addr, _addr, _size)
/* Assert that memory block [_addr, _addr + _size] is allocated */
# define DVALIDATE_ALLOCATED(_addr, _size, _base) \
DVASSERT(allocated((uintptr_t)_addr, _size, (uintptr_t)_base), \
"Operation on unallocated block [%a + %lu] with base %lu\n ", \
_addr, _size, _base)
/* Assert that memory block [_addr, _addr + _size] is allocated
* and can be written to */
# define DVALIDATE_RW_ACCESS(_addr, _size) \
DVASSERT(valid((void*)_addr, _size,(void*)_addr), \
"Operation on unallocated block [%a + %lu]\n ", _addr, _size)
# define DVALIDATE_RW_ACCESS(_addr, _size) { \
DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_addr); \
DVASSERT(!readonly((void*)_addr), \
"Unexpected readonly address: %lu\n", _addr) \
}
/* Assert that memory block [_addr, _addr + _size] is allocated */
# define DVALIDATE_RO_ACCESS(_addr, _size) \
DVASSERT(valid_read((void*)_addr, _size, (void*)_addr), \
"Operation on unallocated block [%a + %lu]\n ", _addr, _size)
DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_addr)
#else
/*! \cond exclude from doxygen */
......@@ -382,6 +389,7 @@ static void validate_memory_layout() {
# define DVALIDATE_HEAP_FREE
# define DVALIDATE_RO_ACCESS
# define DVALIDATE_RW_ACCESS
# define DVALIDATE_ALLOCATED
/*! \endcond */
#endif
/* }}} */
......@@ -708,7 +716,7 @@ static void initialize_static_region(uintptr_t addr, long size) {
* NOTE: This function has many similarities with ::initialize_static_region
* The functionality, however is preferred to be kept separate
* because the ::mark_readonly should operate only on the global shadow. */
static void mark_readonly (uintptr_t addr, long size) {
static void mark_readonly_region (uintptr_t addr, long size) {
/* Since read-only blocks can only be stored in the globals segments (e.g.,
* TEXT), this function required ptr carry a global address. */
DASSERT(IS_ON_GLOBAL(addr));
......
......@@ -204,7 +204,7 @@ class e_acsl_visitor prj generate = object (self)
Cil.mkStmtOneInstr ~valid_sid:true (Set(Cil.var vi, e, loc))
:: Misc.mk_store_stmt ~str_size vi
:: Misc.mk_full_init_stmt ~addr:false vi
:: Misc.mk_readonly vi
:: Misc.mk_mark_readonly vi
:: stmts)
stmts
in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment