// -*- C++ -*- (c) 2019 Henrich Lauko #pragma once #ifdef BRICK_UNITTEST_REG #include DIVINE_RELAX_WARNINGS #include #include #include DIVINE_UNRELAX_WARNINGS #include #include #include #include #include #include #include #include #include #include #include namespace lart::t_abstract { using File = std::string; using Files = std::vector< File >; using SubstitutionPass = lart::abstract::SubstitutionPass; namespace rt = ::divine::rt; template< typename... Passes > auto test( std::unique_ptr< llvm::Module > m, Passes&&... passes ) { using namespace abstract; lart::Driver drv; drv.setup( CreateAbstractMetadata() , VPA() , Decast() , VPA() , StashingPass() , Syntactic() , LowerToBool() , std::forward< Passes >( passes )... ); drv.process( m.get() ); return m; } using namespace abstract; inline bool returns_abstract( llvm::Function * call ) { return meta::abstract::has( call->back().getTerminator() ); } struct TestBase { static const bool dont_link = false; static const bool verbose = false; const std::vector< std::string > flags = { "-std=c++14" }; std::shared_ptr< llvm::LLVMContext > _ctx; TestBase() : _ctx( new llvm::LLVMContext ) {} auto compile( const File & src ) { ::divine::rt::DiosCC c( { dont_link, verbose }, _ctx ); c.setupFS( [&]( auto yield ) { yield( "/main.cpp", src ); } ); c.link( c.compile( "/main.cpp", flags ) ); c.linkEntireArchive( "rst" ); return c.takeLinked(); } template< typename... Passes > auto test( const File & src, Passes&&... passes ) { return t_abstract::test( compile( src ), std::forward< Passes >( passes )... ); } template< typename... Passes > auto test_abstraction( const File & src, Passes&&... passes ) { return test( src, std::forward< Passes >( passes )... ); } template< typename... Passes > auto test_assume( const File & src, Passes&&... passes ) { return test_abstraction( src, AddAssumes(), std::forward< Passes >( passes )... ); } auto test_substitution( const File & src ) { return test_assume( src, SubstitutionPass(), CallInterrupt() ); } bool isVmInterupt( llvm::Function * fn ) { return fn->hasName() && fn->getName() == "__dios_suspend"; } const std::string annotation = "#define _SYM __attribute__((__annotate__(\"lart.abstract.sym\")))\n"; }; struct Abstraction : TestBase { TEST( simple ) { auto s = "int main() { return 0; }"; test_abstraction( annotation + s ); } TEST( create ) { auto s = R"(int main() { _SYM int abs; return 0; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT_EQ( meta::enumerate( *main ).size(), 3 ); } TEST( types ) { auto s = R"(int main() { _SYM short abs_s; _SYM int abs; _SYM long abs_l; return 0; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT_EQ( meta::enumerate( *main ).size(), 9 ); } TEST( binary_ops ) { auto s = R"(int main() { _SYM int abs; int a = abs + 42; int b = abs + a; return 0; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( m->getFunction( "lart.placeholder.abstract.binary.i32" ) ); } TEST( phi ) { auto s = R"(int main() { _SYM int x = 0; _SYM int y = 42; int z = x || y; return 0; })"; auto m = test_abstraction( annotation + s ); ASSERT( m->getFunction( "lart.placeholder.abstract.phi.i1" ) ); } TEST( call_simple ) { auto s = R"(int call( int arg ) { return arg; } int main() { _SYM int abs; int ret = call( abs ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4calli" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); } TEST( call_twice ) { auto s = R"(int call( int arg ) { return arg; } int main() { _SYM int abs; int ret = call( abs ); ret = call( ret ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4calli" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); } TEST( call_independent ) { auto s = R"(int call( int arg ) { return arg; } int main() { _SYM int abs; int ret = call( abs ); ret = call( 10 ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4calli" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); } TEST( call_two_args_mixed ) { auto s = R"(int call( int a, int b ) { return a + b; } int main() { _SYM int abs; int normal = 10; int ret = call( abs, normal ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4callii" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); } TEST( call_two_args_abstract ) { auto s = R"(int call( int a, int b ) { return a + b; } int main() { _SYM int a; _SYM int b; int ret = call( a, b ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4callii" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); } TEST( call_two_args_multiple_times ) { auto s = R"(int call( int a, int b ) { return a + b; } int main() { _SYM int a; _SYM int b; int ret, c = 0, d = 1; ret = call( a, b ); ret = call( a, c ); ret = call( c, d ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4callii" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); } TEST( call_two_times_from_different_source ) { auto s = R"(int call1( int x ) { return x; } int call2( int x ) { return call1( x ); } int main() { _SYM int x; call2( x ); call1( x ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call1 = m->getFunction( "_Z5call1i" ); ASSERT( meta::abstract::roots( call1 ) ); ASSERT( returns_abstract( call1 ) ); auto call2 = m->getFunction( "_Z5call2i" ); ASSERT( meta::abstract::roots( call2 ) ); ASSERT( returns_abstract( call2 ) ); } TEST( propagate_from_call_not_returning_abstract ) { auto s = R"(int call( int x ) { return 10; } int main() { _SYM int x; int ret = call( x ); ret = call( ret ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4calli" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( !returns_abstract( call ) ); } TEST( call_propagate_1 ) { auto s = R"(int call() { _SYM int x; return x; } int main() { int ret = call(); return 0; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); auto call = m->getFunction( "_Z4callv" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); } TEST( call_propagate_back_multiple_times ) { auto s = R"(int nondet() { _SYM int x; return x; } int add() { int x = nondet(); int y = nondet(); return x + y; } int main() { int x = add(); int y = add(); return 0; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); auto add = m->getFunction( "_Z3addv" ); ASSERT( meta::abstract::roots( add ) ); ASSERT( returns_abstract( add ) ); auto nondet = m->getFunction( "_Z6nondetv" ); ASSERT( meta::abstract::roots( nondet ) ); ASSERT( returns_abstract( nondet ) ); } TEST( call_propagate_deeper_1 ) { auto s = R"(int call2( int x ) { return x * x; } int call1() { _SYM int x; return x; } int main() { int ret = call1(); call2( ret ); return 0; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); auto call1 = m->getFunction( "_Z5call1v" ); ASSERT( meta::abstract::roots( call1 ) ); ASSERT( returns_abstract( call1 ) ); auto call2 = m->getFunction( "_Z5call2i" ); ASSERT( meta::abstract::roots( call2 ) ); ASSERT( returns_abstract( call2 ) ); } TEST( call_propagate_deeper_2 ) { auto s = R"( int call4( int x ) { return x; } int call3( int x ) { return x; } int call2( int x ) { return call3( x ) * call4( x ); } int call1() { _SYM int x; return x; } int main() { int ret = call1(); call2( ret ); return 0; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); auto call1 = m->getFunction( "_Z5call1v" ); ASSERT( meta::abstract::roots( call1 ) ); ASSERT( returns_abstract( call1 ) ); auto call2 = m->getFunction( "_Z5call2i" ); ASSERT( meta::abstract::roots( call2 ) ); ASSERT( returns_abstract( call2 ) ); auto call3 = m->getFunction( "_Z5call3i" ); ASSERT( meta::abstract::roots( call3 ) ); ASSERT( returns_abstract( call3 ) ); auto call4 = m->getFunction( "_Z5call4i" ); ASSERT( meta::abstract::roots( call4 ) ); ASSERT( returns_abstract( call4 ) ); } TEST( switch_test ) { auto s = R"(int main() { _SYM int x; int i = 0; switch( x ) { case 0: i = x; break; case 1: i = (-x); break; case 2: i = 42; break; } })"; auto m = test_abstraction( annotation + s ); ASSERT( m->getFunction( "lart.placeholder.abstract.freeze.i32" ) ); ASSERT( m->getFunction( "lart.placeholder.abstract.tobool.i1" ) ); } TEST( loop_test_1 ) { auto s = R"(int main() { _SYM int x; for ( int i = 0; i < x; ++i ) for ( int j = 0; j < x; ++j ) for ( int k = 0; k < x; ++k ) { _SYM int y = i * j *k; } })"; test_abstraction( annotation + s ); } TEST( loop_test_2 ) { auto s = R"(int main() { unsigned N = 1000; unsigned long long Q = 10000000000ULL; unsigned long long rem = 0; _SYM unsigned i; for (i = 1; i < N; i++) { unsigned long long r = 1; unsigned j; for (j = 0; j < i; j++) { r = (r * i) % Q; } rem = (rem + r) % Q; } return 0; })"; auto m = test_abstraction( annotation + s ); ASSERT( m->getFunction( "lart.placeholder.abstract.binary.i64" ) ); } TEST( recursion_direct ) { auto s = R"( int call( int x ) { if ( x < 100 ) return x; else return call( x - 1 ); } int main() { _SYM unsigned x; call( x ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4calli" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); ASSERT( m->getFunction( "lart.placeholder.abstract.binary.i32" ) ); } TEST( recursion_multiple_times ) { auto s = R"( void call( int x, int y ) { if ( x != y ) { int z = ( x + y ) / 2; call( x, z - 1 ); call( z + 1, y ); } } int main() { _SYM unsigned x; call( x, 100 ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4callii" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( !returns_abstract( call ) ); ASSERT( m->getFunction( "lart.placeholder.abstract.binary.i32" ) ); } TEST( recursion_without_abstract_return ) { auto s = R"( int call( int x, int y ) { if ( y == 0 || x == 0 ) return x; else return call(x - 1, y - 1); } int main() { _SYM unsigned x; call( 100, x ); return 0; })"; auto m = test_abstraction( annotation + s ); auto call = m->getFunction( "_Z4callii" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); ASSERT( m->getFunction( "lart.placeholder.abstract.binary.i32" ) ); } TEST( struct_simple ) { auto s = R"(struct S { int x; }; int main() { _SYM int x; S s; s.x = x; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); } TEST( struct_multiple_accesses ) { auto s = R"(struct S { int x; }; int main() { _SYM int x; S s; s.x = x; if ( s.x == 0 ) return 0; else return 1; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( m->getFunction( "lart.placeholder.abstract.cmp.i1" ) ); } TEST( struct_complex ) { auto s = R"(struct S { int x, y, z; }; int main() { _SYM int x; S s; s.y = x; return s.y; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); } TEST( struct_multiple_abstract_values ) { auto s = R"(struct S { int x, y, z; }; int main() { _SYM int x; _SYM int y; S s; s.x = x; s.y = y; s.z = 42; return s.x; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); } TEST( struct_nested_1 ) { auto s = R"(struct S { int x; }; struct T { S a; S b; }; int main() { _SYM int x; T t; t.a.x = x; return t.a.x; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); } TEST( struct_nested_2 ) { auto s = R"(struct S { int x; }; struct U { S s; }; struct V { U u; }; int main() { _SYM int x; V v; v.u.s.x = x; return v.u.s.x; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); } TEST( output_int_arg_1 ) { auto s = R"(void init( int * i ) { _SYM int v; *i = v; } int main() { int i; init( &i ); return i; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); auto init = m->getFunction( "_Z4initPi" ); ASSERT( meta::abstract::roots( init ) ); } TEST( output_int_arg_2 ) { auto s = R"(void init( int * i, int v ) { *i = v; } int main() { int i; _SYM int v; init( &i, v ); return i; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); auto init = m->getFunction( "_Z4initPii" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); ASSERT( meta::abstract::roots( init ) ); } TEST( output_int_arg_3 ) { auto s = R"( void init_impl( int * i ) { _SYM int v; *i = v; } void init( int * i ) { init_impl( i ); } int main() { int i; init( &i ); int v = i; return v; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); auto init = m->getFunction( "_Z4initPi" ); auto init_impl = m->getFunction( "_Z9init_implPi" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); ASSERT( meta::abstract::roots( init ) ); ASSERT( meta::abstract::roots( init_impl ) ); } TEST( output_int_arg_4 ) { auto s = R"( void init_impl( int * i, int v ) { *i = v; } void init( int * i ) { _SYM int v; init_impl( i, v ); } int main() { int i; init( &i ); return i; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); auto init = m->getFunction( "_Z4initPi" ); auto init_impl = m->getFunction( "_Z9init_implPii" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); ASSERT( meta::abstract::roots( init ) ); ASSERT( meta::abstract::roots( init_impl ) ); } TEST( output_struct_arg_1 ) { auto s = R"(struct Widget{ int i; }; void init( Widget * w ) { _SYM int v; w->i = v; } int main() { Widget w; init( &w ); return w.i; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); auto init = m->getFunction( "_Z4initP6Widget" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); ASSERT( meta::abstract::roots( init ) ); } TEST( output_struct_arg_2 ) { auto s = R"(struct Widget{ int i; }; void init( Widget * w ) { _SYM int v; w->i = v % 10; } bool check( Widget * w ) { return w->i < 10; } int main() { Widget w; init( &w ); return check( &w ); })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); auto init = m->getFunction( "_Z4initP6Widget" ); auto check = m->getFunction( "_Z5checkP6Widget" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); ASSERT( meta::abstract::roots( init ) ); ASSERT( meta::abstract::roots( check ) ); ASSERT( returns_abstract( check ) ); } TEST( output_struct_arg_3 ) { auto s = R"(struct Widget{ int i; }; struct Store{ Widget * w; }; void init( Widget * w ) { _SYM int v; w->i = v % 10; } void init( Store * s, Widget * w ) { s->w = w; } int main() { Store store; Widget w; init( &w ); init( &store, &w ); return store.w->i; })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); auto init = m->getFunction( "_Z4initP6Widget" ); auto init_store = m->getFunction( "_Z4initP5StoreP6Widget" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); ASSERT( meta::abstract::roots( init ) ); ASSERT( meta::abstract::roots( init_store ) ); } TEST( global_1 ) { auto s = R"(int g; int f() { return g; } int main() { _SYM int v; g = v; return f(); })"; auto m = test_abstraction( annotation + s ); auto main = m->getFunction( "main" ); auto f = m->getFunction( "_Z1fv" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); ASSERT( meta::abstract::roots( f ) ); ASSERT( returns_abstract( f ) ); } }; struct Assume : TestBase { TEST( simple ) { auto s = "int main() { return 0; }"; test_assume( annotation + s ); } TEST( tristate ) { auto s = R"(int main() { _SYM int x; if ( x > 0 ) return 42; else return 0; })"; test_assume( annotation + s ); } TEST( loop ) { auto s = R"(int main() { _SYM int abs; while( abs ) { ++abs; } return 0; })"; test_assume( annotation + s ); } }; struct Substitution : TestBase { TEST( simple ) { auto s = "int main() { return 0; }"; test_substitution( annotation + s ); } TEST( create ) { auto s = R"(int main() { _SYM int abs; return abs; })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); } TEST( types ) { auto s = R"(int main() { _SYM short abs_s; _SYM int abs; _SYM long abs_l; return 0; })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); } TEST( binary_ops ) { auto s = R"(int main() { _SYM int abs; int a = abs + 42; int b = abs + a; return 0; })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( m->getFunction( "__sym_lift" ) ); ASSERT( m->getFunction( "__sym_add" ) ); } TEST( tristate ) { auto s = R"(int main() { _SYM int x; if ( x > 0 ) return 42; else return 0; })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); } TEST( phi ) { auto s = R"(int main() { _SYM int x = 0; _SYM int y = 42; int z = x || y; return z; })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); ASSERT( returns_abstract( main ) ); } TEST( switch_test ) { auto s = R"(int main() { _SYM int x; int i = 0; switch( x ) { case 0: i = x; break; case 1: i = (-x); break; case 2: i = 42; break; } })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); } TEST( loop_1 ) { auto s = R"( int main() { _SYM int val; do { val++; } while(val % 6 != 0); })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); } TEST( loop_2 ) { auto s = R"(int main() { _SYM int x; for ( int i = 0; i < x; ++i ) for ( int j = 0; j < x; ++j ) for ( int k = 0; k < x; ++k ) { _SYM int y = i * j *k; } })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); } TEST( call_propagate_ones ) { auto s = R"(int call() { _SYM int x; return x; } int main() { int ret = call(); return 0; })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); auto call = m->getFunction( "_Z4callv" ); ASSERT( meta::abstract::roots( call ) ); ASSERT( returns_abstract( call ) ); } TEST( call_propagate_deeper_1 ) { auto s = R"(int call2( int x ) { return x * x; } int call1() { _SYM int x; return x; } int main() { int ret = call1(); call2( ret ); return 0; })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); auto call1 = m->getFunction( "_Z5call1v" ); ASSERT( meta::abstract::roots( call1 ) ); ASSERT( returns_abstract( call1 ) ); auto call2 = m->getFunction( "_Z5call2i" ); ASSERT( meta::abstract::roots( call2 ) ); ASSERT( returns_abstract( call2 ) ); } TEST( call_propagate_deeper_2 ) { auto s = R"( int call4( int x ) { return x; } int call3( int x ) { return x; } int call2( int x ) { return call3( x ) * call4( x ); } int call1() { _SYM int x; return x; } int main() { int ret = call1(); call2( ret ); return 0; })"; auto m = test_substitution( annotation + s ); auto main = m->getFunction( "main" ); ASSERT( meta::abstract::roots( main ) ); auto call1 = m->getFunction( "_Z5call1v" ); ASSERT( meta::abstract::roots( call1 ) ); ASSERT( returns_abstract( call1 ) ); auto call2 = m->getFunction( "_Z5call2i" ); ASSERT( meta::abstract::roots( call2 ) ); ASSERT( returns_abstract( call2 ) ); auto call3 = m->getFunction( "_Z5call3i" ); ASSERT( meta::abstract::roots( call3 ) ); ASSERT( returns_abstract( call3 ) ); auto call4 = m->getFunction( "_Z5call4i" ); ASSERT( meta::abstract::roots( call4 ) ); ASSERT( returns_abstract( call4 ) ); } TEST( call_undef_return ) { auto s = R"( bool is_zero( int v ) { return v == 0; } int main() { _SYM int input; return is_zero( input ); })"; test_substitution( annotation + s ); } }; } // namespace lart::t_abstract #endif