From 41f7bc67bbae3cf5bde5602f0e40f9f297f12e4c Mon Sep 17 00:00:00 2001
From: Henrich Lauko <xlauko@mail.muni.cz>
Date: Thu, 10 Oct 2019 09:01:06 +0000
Subject: [PATCH] rst: Implement unit aggregate abstract domain.
---
dios/include/rst/domains.h | 2 ++
dios/include/rst/unit.hpp | 24 ++++++++++++++++++++++++
dios/rst/unit.cpp | 6 ++++++
3 files changed, 32 insertions(+)
diff --git a/dios/include/rst/domains.h b/dios/include/rst/domains.h
index 5d1c4bb96..8ff5d9f60 100644
--- a/dios/include/rst/domains.h
+++ b/dios/include/rst/domains.h
@@ -39,6 +39,8 @@ extern "C" {
float __unit_lift_float32( float );
double __unit_lift_float64( double );
+ void * __unit_aggregate();
+
char * __mstring_val( char * buff, unsigned buff_len );
uint8_t __constant_lift_i8( uint8_t c );
diff --git a/dios/include/rst/unit.hpp b/dios/include/rst/unit.hpp
index 91c24255f..88348a450 100644
--- a/dios/include/rst/unit.hpp
+++ b/dios/include/rst/unit.hpp
@@ -124,4 +124,28 @@ namespace __dios::rst::abstract {
#undef __bin
};
+
+ struct UnitAggregate : Base
+ {
+ using Ptr = void *;
+
+ template< typename T >
+ _LART_INTERFACE static Ptr lift_any( Abstracted< T > ) noexcept
+ {
+ return __new< UnitAggregate >();
+ }
+
+ _LART_INTERFACE
+ static Ptr op_load( Ptr /* address */ ) noexcept
+ {
+ return __new< Unit< PointerBase > >();
+ }
+
+ _LART_INTERFACE
+ static void op_store( Ptr /* value */, Ptr /* address */ ) noexcept { }
+
+ _LART_INTERFACE
+ static Ptr op_gep( Ptr address, Ptr /* offset */ ) noexcept { return address; }
+ };
+
} // namespace __dios::rst::abstract
diff --git a/dios/rst/unit.cpp b/dios/rst/unit.cpp
index 324438ba4..0e9879dd5 100644
--- a/dios/rst/unit.cpp
+++ b/dios/rst/unit.cpp
@@ -9,11 +9,14 @@ namespace __dios::rst::abstract {
template struct Unit< PointerBase >;
+ using Ptr = void *;
+
template< typename C >
_LART_INLINE C make_unit() noexcept
{
return make_abstract< C, Unit< PointerBase > >();
}
+
template< typename C >
_LART_INLINE C make_unit( C c ) noexcept
{
@@ -25,6 +28,9 @@ namespace __dios::rst::abstract {
_LART_SCALAR uint16_t __unit_val_i16() { return make_unit< uint16_t >(); }
_LART_SCALAR uint32_t __unit_val_i32() { return make_unit< uint32_t >(); }
_LART_SCALAR uint64_t __unit_val_i64() { return make_unit< uint64_t >(); }
+
+ _LART_AGGREGATE Ptr __unit_aggregate() { return make_abstract< Ptr, UnitAggregate >(); }
+
_LART_SCALAR float __unit_val_float32() { return make_unit< float >(); }
_LART_SCALAR double __unit_val_float64() { return make_unit< double >(); }
--
GitLab