Make it possible to build simple programs with divinecc, isolated from system libraries.

.gitignore

@@ -44,3 +44,10 @@ bin/
 Network Trash Folder
 Temporary Items
 .apdisk
+
+# misc
+*.o
+*.bc
+*.swp
+*.swo
+*~

CMakeLists.txt

@@ -1,6 +1,7 @@
 cmake_minimum_required(VERSION 2.8.5)
+set(CMAKE_C_COMPILER "clang")
+set(CMAKE_CXX_COMPILER "clang++")
 project(VFS)
-set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -ggdb3 -std=c++11")
-set(CMAKE_CXX "clang++")
+set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -ggdb3 -std=c++11 -DVFS_STANDALONE")
 
 add_executable(fs _glue.cpp fs.cpp fs-dummyEntrypoint.cpp fs-manager.cpp fs-memory.cpp main.cpp)

Makefile

@@ -0,0 +1,27 @@
+
+CPPS=fs.cpp fs-dummyEntrypoint.cpp fs-manager.cpp fs-memory.cpp main.cpp dvuser.cpp
+# $(wildcard *.cpp)
+PWD=$(shell pwd)
+NATIVEO=native/sys.o
+DIVINE ?= /home/xstill/DiVinE/next
+
+all : fs
+
+fs : $(CPPS:.cpp=.o) libdivinert.o $(NATIVEO)
+	ld $^ -o $@
+
+libdivinert.o :
+	divinecc --libraries-only --disable-vfs --standalone
+	clang++ -c $(@:.o=.bc) -g
+
+%.o : %.cpp
+	divinecc --standalone --dont-link --disable-vfs $< -std=c++11 -I$(PWD) -I$(DIVINE)/bricks -g
+	clang++ -c $(<:.cpp=.bc) -g
+
+clean :
+	rm -rf $(CPPS:.cpp=.bc) $(CPPS:.cpp=.o) mmap.o libdivinert.bc libdivinert.o fs
+
+native/sys.o : native/sys.c
+	clang -c $< -o $@ --sysroot=/try-to-avoid-using-system-includes -Inative -g
+
+.PHONY : clean all

_glue.cpp

@@ -1,6 +1,8 @@
 extern "C" {
 extern void abort();
-void __divine_problem( int, const char * ) noexcept {}
+void __divine_problem( int, const char * ) noexcept {
+    abort();
+}
 void __divine_interrupt_mask() noexcept {}
 void __divine_interrupt_unmask() noexcept {}
 void __divine_assert( int value ) noexcept {

divine.h

@@ -1,8 +1,15 @@
 #ifndef __DIVINE_USR_H
 #define __DIVINE_USR_H
 
+#if defined __cplusplus
+#define __ASSERT_VOID_CAST static_cast< void >
+#else
+#define __ASSERT_VOID_CAST (void)
+#endif
+
 #undef assert
-#define assert( x ) __divine_assert( !!(x) )
+#define assert( x ) ((x) ? __ASSERT_VOID_CAST(0) : __divine_problem( 2, #x ))
+#define assume( x ) __divine_assume( !!(x) )
 
 #define AP( x ) __divine_ap( x )
 #define LTL( name, x ) extern const char * const __divine_LTL_ ## name = #x;
@@ -21,12 +28,14 @@ extern "C" {
 int __divine_new_thread( void (*entry)(void *), void *arg ) NOTHROW;
 int __divine_get_tid( void ) NOTHROW;
 
-void __divine_interrupt_mask( void ) NOTHROW;
+// returns previous state of the mask (0 = not masked before, 1 = masked before)
+int __divine_interrupt_mask( void ) NOTHROW;
 void __divine_interrupt_unmask( void ) NOTHROW;
-void __divine_interrupt( void ) NOTHROW;
+void __divine_interrupt( void ) NOTHROW __attribute__((deprecated));
 
 void __divine_assert( int value ) NOTHROW;
 void __divine_ap( int id ) NOTHROW;
+void __divine_assume( int value ) NOTHROW;
 
 void __divine_problem( int type, const char *data ) NOTHROW;
 
@@ -58,6 +67,7 @@ int __divine_choice( int n, ... ) NOTHROW;
 void *__divine_malloc( unsigned long size ) NOTHROW;
 void __divine_free( void *ptr ) NOTHROW;
 int __divine_heap_object_size( void *ptr ) NOTHROW;
+int __divine_is_private( void *ptr ) NOTHROW;
 
 /*
  * Copy memory. Doing a per-byte copy would destroy pointer maps, hence you are

dvuser.cpp

@@ -0,0 +1,171 @@
+#include <divine.h>
+#include <divine/problem.h>
+#include <atomic>
+#include <errno.h>
+
+extern "C" void *__mmap_anon( size_t len );
+extern "C" void __native_putErrStr( const char *, size_t );
+extern "C" void __native_putStr( const char *, size_t );
+extern "C" _Noreturn void __exit( int );
+
+extern "C" void _init();
+extern "C" void exit( int );
+extern "C" int main();
+extern "C" void __native_start() {
+//    _init();
+    exit( main() );
+}
+
+extern "C" void _Unwind_Resume() { }
+extern "C" void clock_gettime() { }
+
+extern "C" _Noreturn void __die( const char *msg, size_t size ) {
+    __native_putErrStr( msg, size );
+    int *null = nullptr;
+    null[0] = 42;
+    for ( ;; ) { }
+}
+
+#define DIESTR( str ) __die( str, sizeof( str ) - 1 )
+#define DIE( str ) __die( str, strlen( str ) )
+#define PUTESTR( str ) __native_putErrStr( str, sizeof( str ) - 1 )
+
+struct AllocInfo {
+    void *begin = nullptr;
+    void *end = nullptr;
+};
+
+struct AllocBlock {
+    AllocInfo info[4096 / sizeof( AllocInfo ) - sizeof( void * )];
+    AllocBlock *next = nullptr;
+};
+
+AllocBlock __allocRoot;
+
+struct Working {
+    char *block = nullptr;
+    size_t size = 0;
+};
+
+Working __working;
+
+template< typename T, typename R >
+T roundUp( T val, R _radix ) {
+    const T radix = _radix;
+    return val % radix == 0 ? val : (val / radix + 1) * radix;
+}
+
+char *__get_block( size_t size ) noexcept {
+    if ( __working.block && __working.size >= size ) {
+        char *block = __working.block;
+        __working.block += size;
+        __working.size -= size;
+        return block;
+    }
+    const auto asz = roundUp( size, 4096 );
+    char *block = static_cast< char * >( __mmap_anon( asz ) );
+    if ( asz - size > __working.size ) {
+        __working.block = block + size;
+        __working.size = asz - size;
+    }
+    return block;
+}
+
+void *__divine_malloc( size_t size ) noexcept {
+    char *block = __get_block( size );
+    AllocInfo bi;
+    bi.begin = block;
+    bi.end = block + size;
+
+    AllocBlock *meta = &__allocRoot;
+    AllocBlock *last = nullptr;
+    while ( meta ) {
+        for ( auto &i : meta->info ) {
+            if ( !i.begin ) {
+                i = bi;
+                return block;
+            }
+        }
+        last = meta;
+        meta = meta->next;
+    }
+    last->next = reinterpret_cast< AllocBlock * >( __mmap_anon( sizeof( AllocBlock ) ) );
+    last->next->info[0] = bi;
+    return block;
+}
+
+void __divine_free( void *ptr ) noexcept {
+}
+int __divine_heap_object_size( void *ptr ) noexcept {
+    AllocBlock *meta = &__allocRoot;
+    while ( meta )
+        for ( auto &i : meta->info )
+            if ( i.begin <= ptr && ptr < i.end )
+                return size_t( i.end ) - size_t( i.begin );
+    DIESTR( "__divine_heap_object_size called on pointer which is not on heap" );
+}
+int __divine_is_private( void * ) noexcept { return false; }
+
+void __divine_assume( int x ) noexcept {
+    if ( !x )
+        __exit( 1 );
+}
+_Noreturn void __divine_problem( int p, const char *msg ) noexcept {
+    switch ( p ) {
+        #define PROBLEM(x) case x: PUTESTR( "DIVINE problem: " #x "\n" ); break;
+        #include <divine/problem.def>
+        #undef PROBLEM
+    }
+    DIESTR( "__divine_problem called, terminating\n" );
+}
+void __divine_assert( int x ) noexcept {
+    if ( !x )
+        __divine_problem( Assert, nullptr );
+}
+void __divine_ap( int id ) noexcept { }
+
+int __divine_new_thread( void (*entry)(void *), void *arg ) noexcept {
+    DIESTR( "Threading not yet supported" );
+}
+int __divine_get_tid() noexcept { return 0; }
+
+void *__divine_va_start( void ) noexcept {
+    DIESTR( "va_args are not yet supported" );
+}
+
+int __divine_choice( int, ... ) noexcept { return 0; }
+
+void *__divine_memcpy( void *_dest, void *_src, size_t count ) noexcept {
+    char *dest = static_cast< char * >( _dest );
+    char *src = static_cast< char * >( _src );
+    while ( count > 0 ) {
+        *dest++ = *src++;
+        --count;
+    }
+    return _dest;
+}
+
+void __divine_unwind( int, ... ) noexcept {
+    DIESTR( "Exceptions are not yet supported" );
+}
+
+_DivineLP_Info *__divine_landingpad( int frameid ) noexcept {
+    DIESTR( "Exceptions are not yet supported" );
+}
+
+std::atomic< int > __interruptMask = ATOMIC_VAR_INIT( -1 );
+
+void __divine_interrupt() noexcept { }
+int __divine_interrupt_mask() noexcept {
+    int expected = -1;
+    int tid = __divine_get_tid();
+    while ( !__interruptMask.compare_exchange_weak( expected, tid ) ) {
+        if ( expected == tid )
+            return 1;
+        expected = -1;
+    }
+    return 0;
+}
+void __divine_interrupt_unmask() noexcept {
+    __interruptMask = -1;
+}

fs-utils.h

@@ -22,7 +22,7 @@
 
 #define FS_CHOICE_GOAL              0
 
-#ifdef __divine__
+#if defined( __divine__ ) || defined( __divinecc__ )
 # include <divine.h>
 # include <divine/problem.h>
 

fs.cpp

@@ -678,7 +678,7 @@ int fchmod( int fd, mode_t mode ) {
         return -1;
     }
 }
-#if defined(__divine__)
+#if defined(__divine__) || defined( __divinecc__ )
 int alphasort( const struct dirent **a, const struct dirent **b ) {
     return std::strcoll( (*a)->d_name, (*b)->d_name );
 }