[ 0:01] compiling /home/xrockai/src/divine/nightly/test/libcxx/div-extra/atomic-interface.cpp [ 0:01] compiling /dios/lib/config/seqklee.bc [ 0:02] setting up pass: functionmeta, options = [ 0:04] setting up pass: fuse-ctors, options = [ 0:04] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.20/_klee_out" [ 0:08] KLEE: Using Z3 solver backend [ 0:08] WARNING: this target does not support the llvm.stacksave intrinsic. [ 0:09] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-unknown-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf' [ 0:09] [ 0:09] KLEE: WARNING: undefined reference to function: __dios_tainted_init [ 0:16] KLEE: WARNING: undefined reference to function: klee_free [ 0:16] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:16] about to __boot:0 [ 0:16] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 0:16] about to run the scheduler:0 [ 0:16] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5 [ 0:16] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init [ 0:16] KLEE: NOTE: now ignoring this error at this location [ 0:16] KLEE: ERROR: EXITING ON ERROR: [ 0:16] Error: failed external call: __dios_tainted_init [ 0:16] File: /dios/libc/sys/start.cpp [ 0:16] Line: 87 [ 0:16] assembly.ll line: 164257 [ 0:16] Stack: [ 0:16] #000164257 in __dios_start (l=0, argc=1, argv=94209219616776, envp=94209219635208) at /dios/libc/sys/start.cpp:87 [ 0:16] #100140266 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:16] #200172505 in klee_boot (argc=1, argv=94209183934528) at /dios/arch/klee/boot.c:41 [ 0:16] [ 0:16] [ 0:16] 1 /* TAGS: min c++ */ [ 0:16] 2 #include [ 0:16] 3 #include [ 0:16] 4 #include [ 0:16] 5 [ 0:16] 6 #define OPERATOR( T ) \ [ 0:16] 7 friend bool operator==( T a, T b ) { \ [ 0:16] 8 return a.x == b.x; \ [ 0:16] 9 } [ 0:16] 10 [ 0:16] 11 template< typename T > [ 0:16] 12 struct Def { [ 0:16] 13 T operator()() { return T(); } [ 0:16] 14 }; [ 0:16] 15 [ 0:16] 16 template< typename T > [ 0:16] 17 struct Def< T * > { [ 0:16] 18 T *operator()() { return nullptr; } [ 0:16] 19 }; [ 0:16] 20 [ 0:16] 21 template< typename T > [ 0:16] 22 T def() { return Def< T >()(); } [ 0:16] 23 [ 0:16] 24 template< typename T > [ 0:16] 25 struct Conv { [ 0:16] 26 using R = T; [ 0:16] 27 T operator()( int i ) { return i; } [ 0:16] 28 }; [ 0:16] 29 [ 0:16] 30 template< typename T > [ 0:16] 31 struct Conv< T * > { [ 0:16] 32 using R = std::ptrdiff_t; [ 0:16] 33 R operator()( int i ) { return i; } [ 0:16] 34 }; [ 0:16] 35 [ 0:16] 36 template< typename T > [ 0:16] 37 auto conv( int i ) -> typename Conv< T >::R { [ 0:16] 38 return Conv< T >()( i ); [ 0:16] 39 } [ 0:16] 40 [ 0:16] 41 struct St8 { [ 0:16] 42 char x; [ 0:16] 43 [ 0:16] 44 OPERATOR( St8 ) [ 0:16] 45 }; [ 0:16] 46 [ 0:16] 47 struct St16 { [ 0:16] 48 int16_t x; [ 0:16] 49 [ 0:16] 50 OPERATOR( St16 ) [ 0:16] 51 }; [ 0:16] 52 [ 0:16] 53 struct St32 { [ 0:16] 54 int32_t x; [ 0:16] 55 [ 0:16] 56 OPERATOR( St32 ) [ 0:16] 57 }; [ 0:16] 58 [ 0:16] 59 struct St64 { [ 0:16] 60 int64_t x; [ 0:16] 61 [ 0:16] 62 OPERATOR( St64 ) [ 0:16] 63 }; [ 0:16] 64 [ 0:16] 65 struct Large { [ 0:16] 66 int64_t x; [ 0:16] 67 int64_t y[ 15 ]; [ 0:16] 68 [ 0:16] 69 OPERATOR( Large ) [ 0:16] 70 }; [ 0:16] 71 [ 0:16] 72 template< typename T > [ 0:16] 73 void genericIT() { [ 0:16] 74 std::atomic< T > defcon; [ 0:16] 75 std::atomic< T > initcon{ def< T >() }; [ 0:16] 76 std::atomic< T > macroinit = ATOMIC_VAR_INIT( def< T >() ); [ 0:16] 77 std::atomic< T > braceinit = { def< T >() }; [ 0:16] 78 [ 0:16] 79 defcon = def< T >(); [ 0:16] 80 assert( defcon.is_lock_free() ); [ 0:16] 81 assert( std::atomic_is_lock_free( &defcon ) ); [ 0:16] 82 [ 0:16] 83 std::atomic_init( &initcon, def< T >() ); [ 0:16] 84 [ 0:16] 85 defcon.store( def< T >() ); [ 0:16] 86 assert( defcon.load() == def< T >() ); [ 0:16] 87 assert( defcon == def< T >() ); [ 0:16] 88 assert( defcon.exchange( def< T >() ) == def< T >() ); [ 0:16] 89 [ 0:16] 90 T t{}; [ 0:16] 91 assert( defcon.compare_exchange_strong( t, def< T >() ) ); [ 0:16] 92 defcon.compare_exchange_weak( t, def< T >() ); [ 0:16] 93 [ 0:16] 94 std::atomic< T > *ptr = &defcon; [ 0:16] 95 std::atomic_store( ptr, def< T >() ); [ 0:16] 96 std::atomic_store_explicit( ptr, def< T >(), std::memory_order_seq_cst ); [ 0:16] 97 [ 0:16] 98 assert( std::atomic_load( ptr ) == def< T >() ); [ 0:16] 99 assert( std::atomic_load_explicit( ptr, std::memory_order_seq_cst ) == def< T >() ); [ 0:16] 100 [ 0:16] 101 assert( std::atomic_exchange( ptr, def< T >() ) == def< T >() ); [ 0:16] 102 assert( std::atomic_exchange_explicit( ptr, def< T >(), std::memory_order_seq_cst ) == def< T >() ); [ 0:16] 103 [ 0:16] 104 assert( std::atomic_compare_exchange_strong( ptr, &t, def< T >() ) ); [ 0:16] 105 assert( std::atomic_compare_exchange_strong_explicit( ptr, &t, def< T >(), [ 0:16] 106 std::memory_order_seq_cst, std::memory_order_seq_cst ) ); [ 0:16] 107 std::atomic_compare_exchange_weak( ptr, &t, def< T >() ); [ 0:16] 108 std::atomic_compare_exchange_weak_explicit( ptr, &t, def< T >(), [ 0:16] 109 std::memory_order_seq_cst, std::memory_order_seq_cst ); [ 0:16] 110 } [ 0:16] 111 [ 0:16] 112 template< typename T > [ 0:16] 113 void ptrIT() { [ 0:16] 114 genericIT< T >(); [ 0:16] 115 [ 0:16] 116 std::atomic< T > at( 0 ); [ 0:16] 117 const T p = at; [ 0:16] 118 [ 0:16] 119 assert( at.fetch_add( 1 ) == p ); [ 0:16] 120 assert( at == p + 1 ); [ 0:16] 121 assert( ++at == p + 2 ); [ 0:16] 122 assert( at == p + 2 ); [ 0:16] 123 assert( at++ == p + 2 ); [ 0:16] 124 assert( at == p + 3 ); [ 0:16] 125 assert( ( at += 2 ) == p + 5 ); [ 0:16] 126 assert( at == p + 5 ); [ 0:16] 127 [ 0:16] 128 assert( at.fetch_sub( 2 ) == p + 5 ); [ 0:16] 129 assert( at == p + 3 ); [ 0:16] 130 assert( --at == p + 2 ); [ 0:16] 131 assert( at == p + 2 ); [ 0:16] 132 assert( at-- == p + 2 ); [ 0:16] 133 assert( at == p + 1 ); [ 0:16] 134 assert( ( at -= 1 ) == 0 ); [ 0:16] 135 assert( at == 0 ); [ 0:16] 136 [ 0:16] 137 at += 10; [ 0:16] 138 assert( ( at = p ) == p ); [ 0:16] 139 } [ 0:16] 140 [ 0:16] 141 template< typename T > [ 0:16] 142 void integralIT() { [ 0:16] 143 ptrIT< T >(); [ 0:16] 144 [ 0:16] 145 std::atomic< T > at( 42 ); [ 0:16] 146 T t = 42; [ 0:16] 147 [ 0:16] 148 assert( std::atomic_fetch_add( &at, conv< T >( 10 ) ) == t ); [ 0:16] 149 assert( at == t + 10 ); [ 0:16] 150 assert( std::atomic_fetch_add_explicit( &at, T( 10 ), std::memory_order_seq_cst ) == t + 10 ); [ 0:16] 151 assert( at == t + 20 ); [ 0:16] 152 [ 0:16] 153 assert( std::atomic_fetch_sub( &at, T( 10 ) ) == t + 20 ); [ 0:16] 154 assert( at == t + 10 ); [ 0:16] 155 assert( std::atomic_fetch_sub_explicit( &at, T( 10 ), std::memory_order_seq_cst ) == t + 10 ); [ 0:16] 156 assert( at == t ); [ 0:16] 157 [ 0:16] 158 at.exchange( 0xff ); [ 0:16] 159 t = 0xff; [ 0:16] 160 [ 0:16] 161 assert( at.fetch_and( 0x0f ) == t ); [ 0:16] 162 assert( at == ( t &= 0x0f ) ); [ 0:16] 163 assert( at.fetch_and( 0x01, std::memory_order_seq_cst ) == t ); [ 0:16] 164 assert( at == ( t &= 0x01 ) ); [ 0:16] 165 [ 0:16] 166 assert( t == T( 0x01 ) ); [ 0:16] 167 [ 0:16] 168 assert( at.fetch_or( 0x0f ) == t ); [ 0:16] 169 assert( at == ( t |= 0x0f ) ); [ 0:16] 170 assert( at.fetch_or( 0xff, std::memory_order_seq_cst ) == t ); [ 0:16] 171 assert( at == ( t |= 0xff ) ); [ 0:16] 172 [ 0:16] 173 assert( t == T( 0xff ) ); [ 0:16] 174 [ 0:16] 175 assert( at.fetch_xor( 0xf0 ) == t ); [ 0:16] 176 assert( at == ( t ^= 0xf0 ) ); [ 0:16] 177 assert( at.fetch_xor( 0xff, std::memory_order_seq_cst ) == t ); [ 0:16] 178 assert( at == ( t ^= 0xff ) ); [ 0:16] 179 [ 0:16] 180 assert( t == T( 0xf0 ) ); [ 0:16] 181 [ 0:16] 182 assert( at.compare_exchange_strong( t, 0xff ) ); [ 0:16] 183 [ 0:16] 184 std::atomic< T > at2{ T( at ) }; [ 0:16] 185 [ 0:16] 186 assert( at.fetch_and( 0x0f ) == std::atomic_fetch_and( &at2, T( 0x0f ) ) ); [ 0:16] 187 assert( at.fetch_and( 0x01 ) == std::atomic_fetch_and_explicit( &at2, T( 0x01 ), std::memory_order_seq_cst ) ); [ 0:16] 188 [ 0:16] 189 assert( at.fetch_or( 0x0f ) == std::atomic_fetch_or( &at2, T( 0x0f ) ) ); [ 0:16] 190 assert( at.fetch_or( 0xff ) == std::atomic_fetch_or_explicit( &at2, T( 0xff ), std::memory_order_seq_cst ) ); [ 0:16] 191 [ 0:16] 192 assert( at.fetch_xor( 0xf0 ) == std::atomic_fetch_xor( &at2, T( 0xf0 ) ) ); [ 0:16] 193 assert( at.fetch_xor( 0xff ) == std::atomic_fetch_xor_explicit( &at2, T( 0xff ), std::memory_order_seq_cst ) ); [ 0:16] 194 [ 0:16] 195 while ( !at.compare_exchange_weak( t, 0xff ) ) { } [ 0:16] 196 while ( !std::atomic_compare_exchange_weak( &at2, &t, T( 0xff ) ) ) { } [ 0:16] 197 t = 0xff; [ 0:16] 198 [ 0:16] 199 assert( ( at &= 0x0f ) == ( t &= 0x0f ) ); [ 0:16] 200 assert( ( at |= 0x71 ) == ( t |= 0x71 ) ); [ 0:16] 201 assert( ( at ^= 0xf0 ) == ( t ^= 0xf0 ) ); [ 0:16] 202 } [ 0:16] 203 [ 0:16] 204 std::atomic_flag fstatic = ATOMIC_FLAG_INIT; [ 0:16] 205 [ 0:16] 206 void atomicFlagIT() { [ 0:16] 207 std::atomic_flag f = ATOMIC_FLAG_INIT; [ 0:16] 208 [ 0:16] 209 assert( !f.test_and_set() ); [ 0:16] 210 assert( f.test_and_set() ); [ 0:16] 211 f.clear(); [ 0:16] 212 assert( !f.test_and_set( std::memory_order_seq_cst ) ); [ 0:16] 213 f.clear( std::memory_order_seq_cst ); [ 0:16] 214 [ 0:16] 215 assert( !std::atomic_flag_test_and_set( &f ) ); [ 0:16] 216 assert( std::atomic_flag_test_and_set_explicit( &f, std::memory_order_seq_cst ) ); [ 0:16] 217 std::atomic_flag_clear( &f ); [ 0:16] 218 assert( !std::atomic_flag_test_and_set( &f ) ); [ 0:16] 219 std::atomic_flag_clear_explicit( &f, std::memory_order_seq_cst ); [ 0:16] 220 assert( !std::atomic_flag_test_and_set( &f ) ); [ 0:16] 221 } [ 0:16] 222 [ 0:16] 223 int main( void ) { [ 0:16] 224 [ 0:16] 225 atomicFlagIT(); [ 0:16] 226 genericIT< bool >(); [ 0:16] 227 [ 0:16] 228 integralIT< char >(); [ 0:16] 229 integralIT< int16_t >(); [ 0:16] 230 integralIT< int32_t >(); [ 0:16] 231 integralIT< int64_t >(); [ 0:16] 232 [ 0:16] 233 integralIT< unsigned char >(); [ 0:16] 234 integralIT< uint16_t >(); [ 0:16] 235 integralIT< uint32_t >(); [ 0:16] 236 integralIT< uint64_t >(); [ 0:16] 237 [ 0:16] 238 genericIT< St8 >(); [ 0:16] 239 genericIT< St16 >(); [ 0:16] 240 genericIT< St32 >(); [ 0:16] 241 genericIT< St64 >(); [ 0:16] 242 [ 0:16] 243 ptrIT< bool * >(); [ 0:16] 244 ptrIT< char * >(); [ 0:16] 245 ptrIT< int16_t * >(); [ 0:16] 246 ptrIT< int32_t * >(); [ 0:16] 247 ptrIT< int64_t * >(); [ 0:16] 248 [ 0:16] 249 ptrIT< St8 * >(); [ 0:16] 250 ptrIT< St16 * >(); [ 0:16] 251 ptrIT< St32 * >(); [ 0:16] 252 ptrIT< St64 * >(); [ 0:16] 253 [ 0:16] 254 ptrIT< Large * >(); [ 0:16] 255 } [ 0:16] # no errors were expected but one was found anyway