From 10f39efaf1760d8e143df6b8a53eb6487479d72f Mon Sep 17 00:00:00 2001
From: Petr Rockai <me@mornfall.net>
Date: Mon, 13 Jan 2020 22:16:33 +0000
Subject: [PATCH] dios: Improve memory management in the KLEE port.
---
dios/arch/klee/glue.cpp | 17 +++++++++++------
1 file changed, 11 insertions(+), 6 deletions(-)
diff --git a/dios/arch/klee/glue.cpp b/dios/arch/klee/glue.cpp
index c6b1e2d38..dcdf288a0 100644
--- a/dios/arch/klee/glue.cpp
+++ b/dios/arch/klee/glue.cpp
@@ -24,16 +24,21 @@ extern "C" /* platform glue */
{
void *__vm_obj_make( int sz, int )
{
- uint8_t *mem = klee_malloc( 8196 );
- reinterpret_cast< int * >( mem )[0] = sz;
- return mem + sizeof( int );
+ int alloc = sz >= 4096 ? 2 * sz + 2 * sizeof( int ) : 4096 + 2 * sizeof( int );
+ uint8_t *mem = klee_malloc( alloc );
+ int *meta = reinterpret_cast< int * >( mem );
+ meta[ 0 ] = alloc;
+ meta[ 1 ] = sz;
+ return mem + 2 * sizeof( int );
}
- void __vm_obj_free( void *ptr ) { klee_free( static_cast< uint8_t * >( ptr ) - 4 ); }
+ void __vm_obj_free( void *ptr ) { klee_free( static_cast< uint8_t * >( ptr ) - 2 * sizeof( int ) ); }
void __vm_obj_resize( void *optr, int nsz )
{
- static_cast< int * >( optr )[ -1 ] = nsz;
- klee_assume( nsz <= 8192 );
+ int *meta = static_cast< int * >( optr );
+ meta[ -1 ] = nsz;
+ if ( meta[ -1 ] > meta[ -2 ] )
+ klee_abort();
}
int __vm_obj_size( const void *ptr )
--
GitLab