Commit 13686b45 authored by Henrich Lauko's avatar Henrich Lauko

dios: Refactor rst common stuff.

parent 849568d0
#define STR_VALUE(arg) #arg
#define NAMESPACE_JOIN( a, b ) STR_VALUE(a.b)
#define CAT(a, ...) PRIMITIVE_CAT(a, __VA_ARGS__)
#define PRIMITIVE_CAT(a, ...) a ## __VA_ARGS__
#define RST_PROT( prot ) prot _ROOT _NOTHROW
#define PREF() CAT( __ , DOMAIN_NAME )
#define SUFF( name ) CAT( _ , name )
#define RET_PROT( ret, name, ... ) \
RST_PROT( ret PROT_NAME( name )(__VA_ARGS__) );
#define PROT( name, ... ) \
RET_PROT( DOMAIN_TYPE, name, __VA_ARGS__ )
#define PROT_NAME( name ) \
CAT( PREF(), SUFF( name ) )
#define BINARY_PROT( name ) \
PROT( name, DOMAIN_TYPE, DOMAIN_TYPE )
#define UNARY_PROT( name ) \
PROT( name, DOMAIN_TYPE )
#define CAST_PROT( name ) \
PROT( name, DOMAIN_TYPE, int bitwidth )
#define VAL_PROT( bitwidth ) \
RET_PROT( uint ##bitwidth ## _t, val ## _i ## bitwidth, )
#define ASSUME_PROT() \
PROT( assume, DOMAIN_TYPE val, DOMAIN_TYPE constraint, bool assume )
#define FREEZE_PROT() \
RET_PROT( void, freeze, DOMAIN_TYPE val, void * addr )
#define THAW_PROT() \
PROT( thaw, void * addr )
#define THAW_PROT_BV() \
PROT( thaw, void * addr, int bw )
#define CLEANUP_PROT() \
RET_PROT( void, cleanup, void )
#define STASH_PROT() \
RET_PROT( void, stash, DOMAIN_TYPE val )
#define UNSTASH_PROT() \
PROT( unstash )
#define LART_DOMAIN_SPEC( _tag ) \
__attribute__((annotate( NAMESPACE_JOIN(lart.abstract.domain.spec, _tag) )))
#define LART_DOMAIN_KIND( _kind ) \
__attribute__((annotate( NAMESPACE_JOIN(lart.abstract.domain.kind, _kind) )))
#include <rst/tristate.hpp>
typedef __dios::rst::abstract::Tristate __tristate;
extern "C" {
RET_PROT( __tristate , bool_to_tristate, DOMAIN_TYPE )
ASSUME_PROT()
FREEZE_PROT()
CLEANUP_PROT()
STASH_PROT()
UNSTASH_PROT()
}
......@@ -84,14 +84,14 @@ namespace abstract {
return reinterpret_cast< T >( reinterpret_cast< uintptr_t >( val ) + __tainted );
}
extern "C" bool __vm_test_taint_addr( bool (*tainted) ( bool, void * addr ), bool, void * addr ) noexcept;
extern "C" bool __vm_test_taint_addr( bool (*tainted) ( bool, void * addr ), bool, void * addr );
static bool tainted( void * addr )
{
return __vm_test_taint_addr( [] ( bool, void * ) { return true; }, false, addr );
}
extern "C" bool __vm_test_taint_byte( bool (*tainted) ( bool, char val ), bool, char val ) noexcept;
extern "C" bool __vm_test_taint_byte( bool (*tainted) ( bool, char val ), bool, char val );
static bool tainted( char val )
{
......
#pragma once
#include <cstdint>
#include <dios.h>
#include <util/array.hpp>
#include <rst/tristate.hpp>
#include <experimental/type_traits>
#define _NOTHROW __attribute__((__nothrow__))
#define _ROOT __attribute__((__annotate__("divine.link.always")))
#define _UNREACHABLE_F(...) do { \
__dios_trace_f( __VA_ARGS__ ); \
......@@ -19,26 +21,141 @@
_UNREACHABLE_F( __VA_ARGS__ );
#define _LART_INLINE \
__attribute__((__always_inline__, __flatten__))
__attribute__((__always_inline__, __flatten__)) __invisible
#define _LART_NOINLINE \
__attribute__((__noinline__))
#define _LART_INTERFACE \
__attribute__((__nothrow__, __noinline__, __flatten__)) \
__invisible extern "C"
__attribute__((__used__,__nothrow__, __noinline__, __flatten__)) __invisible
#define _LART_SCALAR __attribute__((__annotate__("lart.abstract.return.scalar")))
extern uint64_t __tainted;
extern "C" bool __vm_test_taint_addr( bool (*tainted) ( bool, void * addr ), bool, void * addr );
#define _LART_FN \
__attribute__((__nothrow__, __always_inline__, __flatten__)) __invisible \
extern "C" bool __vm_test_taint_byte( bool (*tainted) ( bool, char val ), bool, char val );
namespace __dios::rst::abstract {
template < typename T, int PT = _VM_PT_Heap >
using Array = __dios::Array< T, PT >;
template< typename It >
struct Range {
using iterator = It;
using const_iterator = It;
Range( It begin, It end ) noexcept : _begin( begin ), _end( end ) { }
Range( const Range & ) noexcept = default;
_LART_INLINE
iterator begin() const noexcept { return _begin; }
_LART_INLINE
iterator end() const noexcept { return _end; }
private:
It _begin, _end;
};
template< typename It >
_LART_INLINE
static Range< It > range( It begin, It end ) noexcept { return Range< It >( begin, end ); }
template< typename T >
struct Abstracted { };
using Bitwidth = int8_t;
} // namespace abstract
template< typename T >
_LART_INLINE static T taint() noexcept
{
static_assert( std::is_arithmetic_v< T > || std::is_pointer_v< T >,
"Cannot taint a non-arithmetic or non-pointer value." );
return static_cast< T >( __tainted );
}
template< typename T >
_LART_INLINE static T taint( T val ) noexcept
{
static_assert( std::is_arithmetic_v< T > || std::is_pointer_v< T >,
"Cannot taint a non-arithmetic or non-pointer value." );
if constexpr ( std::is_arithmetic_v< T > )
return val + static_cast< T >( __tainted );
else
return reinterpret_cast< T >( reinterpret_cast< uintptr_t >( val ) + __tainted );
}
_LART_INLINE static bool tainted( void * addr ) noexcept
{
return __vm_test_taint_addr( [] ( bool, void * ) { return true; }, false, addr );
}
_LART_INLINE static bool tainted( char val ) noexcept
{
return __vm_test_taint_byte( [] ( bool, char ) { return true; }, false, val );
}
template< typename T, _VM_PointerType PT = _VM_PT_Heap, typename ... Args >
_LART_INLINE T *__new( Args &&...args )
{
void *ptr = __vm_obj_make( sizeof( T ), PT );
new ( ptr ) T( std::forward< Args >( args )... );
return static_cast< T * >( ptr );
}
template< typename T >
_LART_INLINE static T * peek_object( void * addr ) noexcept
{
struct { uint32_t off = 0, obj; } ptr;
ptr.obj = __vm_peek( addr, _VM_ML_User );
T * obj;
memcpy( &obj, &ptr, sizeof( T * ) );
return obj;
}
template< typename T >
_LART_INLINE static void poke_object( T * obj, void * addr ) noexcept
{
struct { uint32_t off, obj; } ptr;
memcpy( &ptr, &obj, sizeof( T * ) );
__vm_poke( addr, _VM_ML_User, ptr.obj );
}
template< typename T >
_LART_INLINE T * object( T * ptr ) noexcept
{
return reinterpret_cast< T * >( reinterpret_cast< uintptr_t >( ptr ) & _VM_PM_Obj );
}
template< typename T >
_LART_INLINE uint32_t offset( T * ptr ) noexcept
{
return static_cast< uint32_t >( reinterpret_cast< uintptr_t >( ptr ) & _VM_PM_Off );
}
_LART_INLINE static uint64_t ignore_fault() noexcept
{
return __vm_ctl_flag( 0, _DiOS_CF_IgnoreFault );
}
_LART_INLINE static void restore_fault( uint64_t flags ) noexcept
{
if ( ( flags & _DiOS_CF_IgnoreFault ) == 0 )
__vm_ctl_flag( _DiOS_CF_IgnoreFault, 0 );
}
_LART_INLINE static bool marked( void * addr ) noexcept
{
return __dios_pointer_get_type( addr ) == _VM_PT_Marked;
}
_LART_INLINE static bool weak( void * addr ) noexcept
{
return __dios_pointer_get_type( addr ) == _VM_PT_Weak;
}
} // namespace __dios::rst::abstract
#include <rst/common-domain.def>
extern "C" {
#define OP( ret, name, ... ) \
RET_PROT( ret, name, __VA_ARGS__ );
LART_DOMAIN_SPEC( DOMAIN_NAME )
LART_DOMAIN_KIND( DOMAIN_KIND )
OP( DOMAIN_TYPE, lift, const void * addr, unsigned len );
OP( void, store, char val, DOMAIN_TYPE addr );
OP( char, load, DOMAIN_TYPE addr );
OP( DOMAIN_TYPE, gep, DOMAIN_TYPE addr, int64_t idx );
FREEZE_PROT()
THAW_PROT()
#undef OP
}
#include <rst/common-domain.def>
#define FCMP_PROT( name ) \
PROT( fcmp_ ## name, DOMAIN_TYPE, DOMAIN_TYPE )
#define FLOAT_VAL_PROT( type, bitwidth ) \
RET_PROT( type, val ## float ## bitwidth, )
extern "C" {
FLOAT_VAL_PROT( float , 32 )
FLOAT_VAL_PROT( double, 64 )
PROT( lift_float, int bitwidth, int argc, ... )
FCMP_PROT( false )
FCMP_PROT( oeq )
FCMP_PROT( ogt )
FCMP_PROT( oge )
FCMP_PROT( olt )
FCMP_PROT( ole )
FCMP_PROT( one )
FCMP_PROT( ord )
FCMP_PROT( uno )
FCMP_PROT( ueq )
FCMP_PROT( ugt )
FCMP_PROT( uge )
FCMP_PROT( ult )
FCMP_PROT( ule )
FCMP_PROT( une )
FCMP_PROT( true )
BINARY_PROT( fadd )
BINARY_PROT( fsub )
BINARY_PROT( fmul )
BINARY_PROT( fdiv )
BINARY_PROT( frem )
CAST_PROT( fptrunc )
CAST_PROT( fpext )
}
#undef FLOAT_VAL_PROT
#undef FCMP_PROT
#include <rst/common-domain.def>
#define ICMP_PROT( name ) \
PROT( icmp_ ## name, DOMAIN_TYPE, DOMAIN_TYPE )
extern "C" {
VAL_PROT( 8 )
VAL_PROT( 16 )
VAL_PROT( 32 )
VAL_PROT( 64 )
LART_DOMAIN_SPEC( DOMAIN_NAME )
LART_DOMAIN_KIND( DOMAIN_KIND )
PROT( lift, int bitwidth, int argc, ... )
BINARY_PROT( add )
BINARY_PROT( sub )
BINARY_PROT( mul )
BINARY_PROT( sdiv )
BINARY_PROT( udiv )
BINARY_PROT( urem )
BINARY_PROT( srem )
BINARY_PROT( and )
BINARY_PROT( or )
BINARY_PROT( xor )
BINARY_PROT( shl )
BINARY_PROT( lshr )
BINARY_PROT( ashr )
CAST_PROT( trunc )
CAST_PROT( zext )
CAST_PROT( sext )
UNARY_PROT( bitcast )
UNARY_PROT( ptrtoint )
ICMP_PROT( eq )
ICMP_PROT( ne )
ICMP_PROT( ugt )
ICMP_PROT( uge )
ICMP_PROT( ult )
ICMP_PROT( ule )
ICMP_PROT( sgt )
ICMP_PROT( sge )
ICMP_PROT( slt )
ICMP_PROT( sle )
THAW_PROT_BV()
}
#undef ICMP_PROT
#include <rst/common-domain.def>
#include <rst/content-domain.def>
extern "C" {
#define OP( ret, name, ... ) \
RET_PROT( ret, name, __VA_ARGS__ );
/* String manipulation */
OP( DOMAIN_TYPE, strcpy , DOMAIN_TYPE dest, const DOMAIN_TYPE src );
OP( DOMAIN_TYPE, strncpy, DOMAIN_TYPE dest, const DOMAIN_TYPE src, size_t count );
OP( DOMAIN_TYPE, strcat , DOMAIN_TYPE dest, const DOMAIN_TYPE src );
OP( DOMAIN_TYPE, strncat, DOMAIN_TYPE dest, const DOMAIN_TYPE src, size_t count );
OP( size_t , strxfrm, DOMAIN_TYPE dest, const DOMAIN_TYPE src, size_t count );
/* String examination */
OP( size_t , strlen , const DOMAIN_TYPE str );
OP( int , strcmp , const DOMAIN_TYPE lhs, const DOMAIN_TYPE rhs );
OP( int , strncmp, const DOMAIN_TYPE lhs, const DOMAIN_TYPE rhs, size_t count );
OP( int , strcoll, const DOMAIN_TYPE lhs, const DOMAIN_TYPE rhs );
OP( DOMAIN_TYPE, strchr , const DOMAIN_TYPE str, int ch );
OP( DOMAIN_TYPE, strrchr, const DOMAIN_TYPE str, int ch );
OP( size_t , strspn , const DOMAIN_TYPE dest, const DOMAIN_TYPE src );
OP( size_t , strcspn, const DOMAIN_TYPE dest, const DOMAIN_TYPE src );
OP( DOMAIN_TYPE, strpbrk, const DOMAIN_TYPE dest, const char * breakset );
OP( DOMAIN_TYPE, strstr , const DOMAIN_TYPE str, const char* substr );
OP( DOMAIN_TYPE, strtok , DOMAIN_TYPE str, const char * delim );
#undef OP
}
......@@ -3,7 +3,7 @@
#include <cstdio>
#include <dios/sys/kernel.hpp> // get_debug
#include <rst/common.h> // for weaken
#include <rst/common.hpp> // for weaken
#include <fcntl.h>
#include <dios.h>
#include <cstring>
......
#include <rst/common.h>
using namespace abstract;
#include <rst/common.hpp>
uint64_t __tainted = 0;
void * __tainted_ptr = nullptr;
// TODO call from abstraction init
__attribute__((constructor)) void __tainted_init()
{
__vm_poke( &__tainted, _VM_ML_Taints, 0xF );
......
#include <rst/lart.h>
#include <sys/task.h>
#include <rst/common.h>
#include <sys/divm.h>
#include <rst/common.hpp>
#include <string.h>
......
#include <rst/tristate.hpp>
#include <rst/common.h>
#include <rst/common.hpp>
using __tristate = __dios::rst::abstract::Tristate;
......
......@@ -9,7 +9,7 @@
#include <sys/vmutil.h>
#include <sys/cdefs.h>
#include <dios/sys/kernel.hpp> // get_debug
#include <rst/common.h>
#include <rst/common.hpp>
#define _WM_INLINE __attribute__((__always_inline__, __flatten__))
#define _WM_NOINLINE __attribute__((__noinline__))
......@@ -82,7 +82,7 @@ using ThreadMap = __dios::ArrayMap< __dios_task, T >;
template< typename T >
using Array = __dios::Array< T >;
using abstract::range;
using __dios::rst::abstract::range;
template< typename T >
_WM_INLINE
......
......@@ -19,7 +19,7 @@
#include <util/map.hpp>
#include <rst/common.h>
#include <rst/common.hpp>
namespace __dios {
......
......@@ -24,7 +24,7 @@
#include <dios.h>
#include <dios/sys/memory.hpp>
#include <dios/sys/stdlibwrap.hpp> // Queue
#include <rst/common.h>
#include <rst/common.hpp>
#include <sys/fault.h>
#include <sys/trace.h>
......
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