diff --git a/regression/cbmc/Local_out_of_scope4/main.c b/regression/cbmc/Local_out_of_scope4/main.c new file mode 100644 index 00000000000..4117a283b4d --- /dev/null +++ b/regression/cbmc/Local_out_of_scope4/main.c @@ -0,0 +1,15 @@ +int main() +{ + int *p = 0; + + for(int i = 0; i < 3; ++i) + { + { + int x = 42; + p = &x; + *p = 1; + } + } + + return 0; +} diff --git a/regression/cbmc/Local_out_of_scope4/test.desc b/regression/cbmc/Local_out_of_scope4/test.desc new file mode 100644 index 00000000000..39c491ba8bb --- /dev/null +++ b/regression/cbmc/Local_out_of_scope4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Memory_leak_abort/main.c b/regression/cbmc/Memory_leak_abort/main.c new file mode 100644 index 00000000000..2db9de9621b --- /dev/null +++ b/regression/cbmc/Memory_leak_abort/main.c @@ -0,0 +1,18 @@ +#include + +extern void __VERIFIER_error() __attribute__((__noreturn__)); + +int main() +{ + int *p = malloc(sizeof(int)); + if(*p == 0) + abort(); + if(*p == 1) + exit(1); + if(*p == 2) + _Exit(1); + if(*p == 3) + __VERIFIER_error(); + free(p); + return 0; +} diff --git a/regression/cbmc/Memory_leak_abort/test.desc b/regression/cbmc/Memory_leak_abort/test.desc new file mode 100644 index 00000000000..778831b5ce3 --- /dev/null +++ b/regression/cbmc/Memory_leak_abort/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--memory-leak-check --no-assertions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +_Exit\.memory-leak\.1.*FAILURE +__CPROVER__start\.memory-leak\.1.*SUCCESS +abort\.memory-leak\.1.*FAILURE +exit\.memory-leak\.1.*FAILURE +main\.memory-leak\.1.*FAILURE +-- +main\.assertion\.1.*FAILURE +^warning: ignoring diff --git a/regression/cbmc/alloca1/main.c b/regression/cbmc/alloca1/main.c new file mode 100644 index 00000000000..bc30d7624a1 --- /dev/null +++ b/regression/cbmc/alloca1/main.c @@ -0,0 +1,8 @@ +#include + +int main() +{ + int *p = alloca(sizeof(int)); + *p = 42; + free(p); +} diff --git a/regression/cbmc/alloca1/test.desc b/regression/cbmc/alloca1/test.desc new file mode 100644 index 00000000000..66fa40a9537 --- /dev/null +++ b/regression/cbmc/alloca1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +free called for stack-allocated object: FAILURE$ +^\*\* 1 of 12 failed +-- +^warning: ignoring diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc index cb22eaba5d0..5203bd00210 100644 --- a/regression/cbmc/graphml_witness1/test.desc +++ b/regression/cbmc/graphml_witness1/test.desc @@ -7,34 +7,21 @@ main.c - - path - - - false - false false - - false - false - - 0 - - @@ -45,7 +32,6 @@ main.c C - true @@ -68,10 +54,6 @@ main.c true - - main.c - 31 - -- diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index a4a79f28ab1..f7de54ad46b 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index 6a28820a4b0..47aea19e28b 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-instrument/print_global_state_size1/main.c b/regression/goto-instrument/print_global_state_size1/main.c index 68f16e02519..08f28f20724 100644 --- a/regression/goto-instrument/print_global_state_size1/main.c +++ b/regression/goto-instrument/print_global_state_size1/main.c @@ -3,7 +3,7 @@ uint32_t some_global_var; int8_t other_global_var; -int main(int argc, char *argv[]) +int main() { return 0; } diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index c47cd9128e7..b7c6fc1e7ba 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -53,6 +53,7 @@ rm Malloc23/test.desc rm Malloc24/test.desc rm Memory_leak1/test.desc rm Memory_leak2/test.desc +rm Memory_leak_abort/test.desc rm Multi_Dimensional_Array1/test.desc rm Multi_Dimensional_Array2/test.desc rm Multi_Dimensional_Array3/test.desc diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index ce6f07672a3..ffdff96f7be 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -103,6 +103,7 @@ class goto_checkt void bounds_check(const index_exprt &, const guardt &); void div_by_zero_check(const div_exprt &, const guardt &); + void memory_leak_check(const irep_idt &function_id); void mod_by_zero_check(const mod_exprt &, const guardt &); void undefined_shift_check(const shift_exprt &, const guardt &); void pointer_rel_check(const exprt &, const guardt &); @@ -1515,6 +1516,30 @@ void goto_checkt::rw_ok_check(exprt &expr) } } +void goto_checkt::memory_leak_check(const irep_idt &function_id) +{ + const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak"); + const symbol_exprt leak_expr = leak.symbol_expr(); + + // add self-assignment to get helpful counterexample output + goto_programt::targett t = new_code.add_instruction(); + t->make_assignment(); + t->code = code_assignt(leak_expr, leak_expr); + + source_locationt source_location; + source_location.set_function(function_id); + + equal_exprt eq(leak_expr, null_pointer_exprt(to_pointer_type(leak.type))); + + add_guarded_claim( + eq, + "dynamically allocated memory never freed", + "memory-leak", + source_location, + eq, + guardt()); +} + void goto_checkt::goto_check( goto_functiont &goto_function, const irep_idt &_mode) @@ -1678,6 +1703,16 @@ void goto_checkt::goto_check( } else if(i.is_assume()) { + // These are further 'exit points' of the program + const exprt simplified_guard = simplify_expr(i.guard, ns); + if( + enable_memory_leak_check && simplified_guard.is_false() && + (i.function == "abort" || i.function == "exit" || + i.function == "_Exit" || + (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort"))) + { + memory_leak_check(i.function); + } if(!enable_assumptions) { i.make_skip(); @@ -1711,32 +1746,41 @@ void goto_checkt::goto_check( } } } - else if(i.is_end_function()) + else if(i.is_decl()) { - if(i.function==goto_functionst::entry_point() && - enable_memory_leak_check) + if(enable_pointer_check) { - const symbolt &leak=ns.lookup(CPROVER_PREFIX "memory_leak"); - const symbol_exprt leak_expr=leak.symbol_expr(); - - // add self-assignment to get helpful counterexample output - goto_programt::targett t=new_code.add_instruction(); - t->make_assignment(); - t->code=code_assignt(leak_expr, leak_expr); - - source_locationt source_location; - source_location.set_function(i.function); + assert(i.code.operands().size()==1); + const symbol_exprt &variable=to_symbol_expr(i.code.op0()); - equal_exprt eq( - leak_expr, - null_pointer_exprt(to_pointer_type(leak.type))); - add_guarded_claim( - eq, - "dynamically allocated memory never freed", - "memory-leak", - source_location, - eq, - guardt()); + // is it dirty? + if(local_bitvector_analysis->dirty(variable)) + { + // reset the dead marker + goto_programt::targett t=new_code.add_instruction(ASSIGN); + exprt address_of_expr=address_of_exprt(variable); + exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + if(!base_type_eq(lhs.type(), address_of_expr.type(), ns)) + address_of_expr.make_typecast(lhs.type()); + exprt rhs= + if_exprt( + equal_exprt(lhs, address_of_expr), + null_pointer_exprt(to_pointer_type(address_of_expr.type())), + lhs, + lhs.type()); + t->source_location=i.source_location; + t->code=code_assignt(lhs, rhs); + t->code.add_source_location()=i.source_location; + } + } + } + else if(i.is_end_function()) + { + if( + i.function == goto_functionst::entry_point() && + enable_memory_leak_check) + { + memory_leak_check(i.function); } } diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index b22dafa554e..99102773d75 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -136,6 +136,12 @@ void ansi_c_internal_additions(std::string &code) CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited[" CPROVER_PREFIX "constant_infinity_uint];\n" "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n" + CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys[" + CPROVER_PREFIX "constant_infinity_uint];\n" + CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors[" + CPROVER_PREFIX "constant_infinity_uint])(void *);\n" + CPROVER_PREFIX "thread_local unsigned long " + CPROVER_PREFIX "next_thread_key = 0;\n" "extern unsigned char " CPROVER_PREFIX "memory[" CPROVER_PREFIX "constant_infinity_uint];\n" @@ -148,6 +154,7 @@ void ansi_c_internal_additions(std::string &code) "const void *" CPROVER_PREFIX "memory_leak=0;\n" "void *" CPROVER_PREFIX "allocate(" CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n" + "const void *" CPROVER_PREFIX "alloca_object = 0;\n" // this is ANSI-C "extern " CPROVER_PREFIX "thread_local const char __func__[" diff --git a/src/ansi-c/c_typecheck_argc_argv.cpp b/src/ansi-c/c_typecheck_argc_argv.cpp index dfc752c8e19..7ff32a4810d 100644 --- a/src/ansi-c/c_typecheck_argc_argv.cpp +++ b/src/ansi-c/c_typecheck_argc_argv.cpp @@ -42,6 +42,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol) argc_symbol.type=op0.type(); argc_symbol.is_static_lifetime=true; argc_symbol.is_lvalue=true; + argc_symbol.value = side_effect_expr_nondett(op0.type()); if(argc_symbol.type.id()!=ID_signedbv && argc_symbol.type.id()!=ID_unsignedbv) @@ -81,6 +82,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol) argv_symbol.type=argv_type; argv_symbol.is_static_lifetime=true; argv_symbol.is_lvalue=true; + argv_symbol.value = side_effect_expr_nondett(argv_type); symbolt *argv_new_symbol; move_symbol(argv_symbol, argv_new_symbol); @@ -99,6 +101,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol) envp_size_symbol.name="envp_size'"; envp_size_symbol.type=op0.type(); // same type as argc! envp_size_symbol.is_static_lifetime=true; + envp_size_symbol.value = side_effect_expr_nondett(op0.type()); move_symbol(envp_size_symbol, envp_new_size_symbol); if(envp_symbol.type.id()!=ID_pointer) @@ -113,6 +116,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol) envp_symbol.type.id(ID_array); envp_symbol.type.add(ID_size).swap(size_expr); + envp_symbol.value = side_effect_expr_nondett(envp_symbol.type); symbolt *envp_new_symbol; move_symbol(envp_symbol, envp_new_symbol); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 4080b8a6d81..e8deeb74c8e 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -39,7 +39,8 @@ expr2c_configurationt expr2c_configurationt::default_configuration true, true, "TRUE", - "FALSE" + "FALSE", + "NULL" }; expr2c_configurationt expr2c_configurationt::clean_configuration @@ -48,6 +49,7 @@ expr2c_configurationt expr2c_configurationt::clean_configuration false, false, "1", + "0", "0" }; @@ -715,6 +717,7 @@ std::string expr2ct::convert_struct_type( if(tag!="") dest+=" "+id2string(tag); +#if 0 if(inc_struct_body) { dest+=" {"; @@ -737,6 +740,7 @@ std::string expr2ct::convert_struct_type( dest+=" }"; } +#endif dest+=declarator; @@ -1970,14 +1974,14 @@ std::string expr2ct::convert_constant( { if(value==ID_NULL) { - dest="NULL"; + dest = configuration.null_pointer_string; if(type.subtype().id()!=ID_empty) dest="(("+convert(type)+")"+dest+")"; } else if(value==std::string(value.size(), '0') && config.ansi_c.NULL_is_zero) { - dest="NULL"; + dest = configuration.null_pointer_string; if(type.subtype().id()!=ID_empty) dest="(("+convert(type)+")"+dest+")"; } diff --git a/src/ansi-c/expr2c.h b/src/ansi-c/expr2c.h index 3689c5478bb..818f82737e7 100644 --- a/src/ansi-c/expr2c.h +++ b/src/ansi-c/expr2c.h @@ -36,17 +36,22 @@ struct expr2c_configurationt final /// This is the string that will be printed for the false boolean expression std::string false_string; + /// This is the string that will be printed for null pointers + std::string null_pointer_string; + expr2c_configurationt( const bool include_struct_padding_components, const bool print_struct_body_in_type, const bool include_array_size, std::string true_string, - std::string false_string) + std::string false_string, + const std::string &null_pointer_string) : include_struct_padding_components(include_struct_padding_components), print_struct_body_in_type(print_struct_body_in_type), include_array_size(include_array_size), true_string(std::move(true_string)), - false_string(std::move(false_string)) + false_string(std::move(false_string)), + null_pointer_string(null_pointer_string) { } diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 97194052a54..e8c25a4a009 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -293,10 +293,23 @@ inline int pthread_mutex_destroy(pthread_mutex_t *mutex) extern __CPROVER_bool __CPROVER_threads_exited[]; extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; +extern __CPROVER_thread_local const void* __CPROVER_thread_keys[]; +extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void*); +extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; + inline void pthread_exit(void *value_ptr) { __CPROVER_HIDE:; if(value_ptr!=0) (void)*(char*)value_ptr; +#if 0 + for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) + { + const void *key = __CPROVER_thread_keys[i]; + __CPROVER_thread_keys[i] = 0; + if(__CPROVER_thread_key_dtors[i] && key) + __CPROVER_thread_key_dtors[i](key); + } +#endif __CPROVER_threads_exited[__CPROVER_thread_id]=1; __CPROVER_assume(0); } @@ -522,6 +535,44 @@ extern __CPROVER_bool __CPROVER_threads_exited[]; extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; extern unsigned long __CPROVER_next_thread_id; +extern __CPROVER_thread_local const void* __CPROVER_thread_keys[]; +extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void*); +extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; + +inline void __spawned_thread( + unsigned long this_thread_id, + // void (**thread_key_dtors)(void*), + unsigned long next_thread_key, + void * (*start_routine)(void *), + void *arg) +{ + __CPROVER_HIDE:; + __CPROVER_thread_id = this_thread_id; + __CPROVER_next_thread_key = next_thread_key; +#if 0 + for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) + __CPROVER_thread_key_dtors[i] = thread_key_dtors[i]; +#endif + #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS + // Clear all locked mutexes; locking must happen in same thread. + __CPROVER_clear_must(0, "mutex-locked"); + __CPROVER_clear_may(0, "mutex-locked"); + #endif + start_routine(arg); + __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", + "WWcumul", "RRcumul", "RWcumul", "WRcumul"); +#if 0 + for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) + { + const void *key = __CPROVER_thread_keys[i]; + __CPROVER_thread_keys[i] = 0; + if(__CPROVER_thread_key_dtors[i] && key) + __CPROVER_thread_key_dtors[i](key); + } +#endif + __CPROVER_threads_exited[this_thread_id] = 1; +} + inline int pthread_create( pthread_t *thread, // must not be null const pthread_attr_t *attr, // may be null @@ -543,17 +594,16 @@ inline int pthread_create( if(attr) (void)*attr; + unsigned long next_thread_key = __CPROVER_next_thread_key; + // void (**thread_key_dtors)(void*) = __CPROVER_thread_key_dtors; + __CPROVER_ASYNC_1: - __CPROVER_thread_id=this_thread_id, - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS - // Clear all locked mutexes; locking must happen in same thread. - __CPROVER_clear_must(0, "mutex-locked"), - __CPROVER_clear_may(0, "mutex-locked"), - #endif - start_routine(arg), - __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", - "WWcumul", "RRcumul", "RWcumul", "WRcumul"), - __CPROVER_threads_exited[this_thread_id]=1; + __spawned_thread( + this_thread_id, + // thread_key_dtors, + next_thread_key, + start_routine, + arg); return 0; } @@ -634,8 +684,8 @@ inline int pthread_cond_wait( #endif __CPROVER_atomic_begin(); - __CPROVER_assume(*((unsigned *)cond)); - (*((unsigned *)cond))--; + if(*((unsigned *)cond)) + (*((unsigned *)cond))--; __CPROVER_atomic_end(); return 0; // we never fail @@ -807,3 +857,71 @@ inline int pthread_barrier_wait(pthread_barrier_t *barrier) return result; } #endif + +/* FUNCTION: pthread_key_create */ + +#ifndef __CPROVER_PTHREAD_H_INCLUDED +#include +#define __CPROVER_PTHREAD_H_INCLUDED +#endif + +extern __CPROVER_thread_local const void* __CPROVER_thread_keys[]; +extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void*); +extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; + +inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void*)) +{ + __CPROVER_HIDE:; + __CPROVER_thread_keys[__CPROVER_next_thread_key] = 0; + // __CPROVER_thread_key_dtors[__CPROVER_next_thread_key] = destructor; + __CPROVER_precondition(destructor == 0, "destructors are not yet supported"); + *key = __CPROVER_next_thread_key++; + return 0; +} + +/* FUNCTION: pthread_key_delete */ + +#ifndef __CPROVER_PTHREAD_H_INCLUDED +#include +#define __CPROVER_PTHREAD_H_INCLUDED +#endif + +extern __CPROVER_thread_local const void* __CPROVER_thread_keys[]; + +inline int pthread_key_delete(pthread_key_t key) +{ + __CPROVER_HIDE:; + __CPROVER_thread_keys[key] = 0; + return 0; +} + +/* FUNCTION: pthread_getspecific */ + +#ifndef __CPROVER_PTHREAD_H_INCLUDED +#include +#define __CPROVER_PTHREAD_H_INCLUDED +#endif + +extern __CPROVER_thread_local const void* __CPROVER_thread_keys[]; + +inline void* pthread_getspecific(pthread_key_t key) +{ + __CPROVER_HIDE:; + return (void *)__CPROVER_thread_keys[key]; +} + +/* FUNCTION: pthread_setspecific */ + +#ifndef __CPROVER_PTHREAD_H_INCLUDED +#include +#define __CPROVER_PTHREAD_H_INCLUDED +#endif + +extern __CPROVER_thread_local const void* __CPROVER_thread_keys[]; + +inline int pthread_setspecific(pthread_key_t key, const void *value) +{ + __CPROVER_HIDE:; + __CPROVER_thread_keys[key] = value; + return 0; +} diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 7f72651a18f..39739733553 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -128,6 +128,7 @@ inline void *malloc(__CPROVER_size_t malloc_size) /* FUNCTION: __builtin_alloca */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +extern void *__CPROVER_alloca_object; inline void *__builtin_alloca(__CPROVER_size_t alloca_size) { @@ -144,14 +145,31 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size) __CPROVER_malloc_size=record_malloc?alloca_size:__CPROVER_malloc_size; __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array; + // record alloca to detect invalid free + __CPROVER_bool record_alloca = __VERIFIER_nondet___CPROVER_bool(); + __CPROVER_alloca_object = record_alloca ? res : __CPROVER_alloca_object; + return res; } +/* FUNCTION: alloca */ + +#undef alloca + +void *__builtin_alloca(__CPROVER_size_t alloca_size); + +inline void *alloca(__CPROVER_size_t alloca_size) +{ + __CPROVER_HIDE:; + return __builtin_alloca(alloca_size); +} + /* FUNCTION: free */ #undef free __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +extern void *__CPROVER_alloca_object; inline void free(void *ptr) { @@ -173,6 +191,11 @@ inline void free(void *ptr) !__CPROVER_malloc_is_new_array, "free called for new[] object"); + // catch people who try to use free(...) with alloca + __CPROVER_precondition( + ptr == 0 || __CPROVER_alloca_object != ptr, + "free called for stack-allocated object"); + if(ptr!=0) { // non-deterministically record as deallocated diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index f62f0880a25..b1a376f455d 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -72,6 +72,16 @@ void cpp_internal_additions(std::ostream &out) << CPROVER_PREFIX "threads_exited[__CPROVER::constant_infinity_uint];" << '\n'; out << "unsigned long " CPROVER_PREFIX "next_thread_id = 0;" << '\n'; + // TODO: thread_local is still broken + out << "void* " + << CPROVER_PREFIX "thread_keys[__CPROVER::constant_infinity_uint];" + << '\n'; + // TODO: thread_local is still broken + out << "void (*" + << CPROVER_PREFIX "thread_key_dtors[__CPROVER::constant_infinity_uint])" + << "(void *);" << '\n'; + // TODO: thread_local is still broken + out << "unsigned long " CPROVER_PREFIX "next_thread_key = 0;" << '\n'; out << "extern unsigned char " << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n'; @@ -85,6 +95,7 @@ void cpp_internal_additions(std::ostream &out) out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n'; out << "void *" CPROVER_PREFIX "allocate(" << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n'; + out << "const void *" CPROVER_PREFIX "alloca_object = 0;" << '\n'; // auxiliaries for new/delete out << "void *__new(__CPROVER::size_t);" << '\n'; diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index a638c1d094e..c6f9100d22b 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -711,6 +711,7 @@ void goto_convertt::do_function_call_symbol( // are being checked goto_programt::targett a=dest.add_instruction(ASSUME); a->guard=false_exprt(); + a->labels.push_back("__VERIFIER_abort"); a->source_location=function.source_location(); a->source_location.set("user-provided", true); } diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index b1821cfde78..106265cc7aa 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -9,19 +9,38 @@ Author: Daniel Kroening /// \file /// Witnesses for Traces and Proofs +#include + #include "graphml_witness.h" #include #include #include #include +#include #include #include +#include +#include #include +#include + +#include #include "goto_program.h" +static std::string expr_to_string( + const namespacet &ns, + const irep_idt &id, + const exprt &expr) +{ + if(get_mode_from_identifier(ns, id) == ID_C) + return expr2c(expr, ns, expr2c_configurationt::clean_configuration); + else + return from_expr(ns, id, expr); +} + void graphml_witnesst::remove_l0_l1(exprt &expr) { if(expr.id()==ID_symbol) @@ -52,9 +71,38 @@ std::string graphml_witnesst::convert_assign_rec( const irep_idt &identifier, const code_assignt &assign) { + static std::unordered_map, std::string> cache; + { + const auto cit = cache.find({identifier.get_no(), &assign.read()}); + if(cit != cache.end()) + return cit->second; + } + std::string result; - if(assign.rhs().id()==ID_array) + if(assign.rhs().id()=="array-list") + { + const array_typet &type= + to_array_type(ns.follow(assign.rhs().type())); + + const auto ops=assign.rhs().operands(); + DATA_INVARIANT( + ops.size()%2==0, + "array-list has odd number of operands"); + + for(size_t listidx=0; listidx!=ops.size(); listidx+=2) + { + index_exprt index( + assign.lhs(), + ops[listidx], + type.subtype()); + if(!result.empty()) + result+=' '; + result+= + convert_assign_rec(identifier, code_assignt(index, ops[listidx+1])); + } + } + else if(assign.rhs().id()==ID_array) { const array_typet &type= to_array_type(ns.follow(assign.rhs().type())); @@ -130,13 +178,17 @@ std::string graphml_witnesst::convert_assign_rec( exprt clean_rhs=assign.rhs(); remove_l0_l1(clean_rhs); - std::string lhs=from_expr(ns, identifier, assign.lhs()); - if(lhs.find('$')!=std::string::npos) + exprt clean_lhs=assign.lhs(); + remove_l0_l1(clean_lhs); + std::string lhs=expr_to_string(ns, identifier, clean_lhs); + if(lhs.find("#return_value")!=std::string::npos || + (lhs.find('$')!=std::string::npos && + lhs.find("return_value___VERIFIER_nondet_")==0U)) lhs="\\result"; - result=lhs+" = "+from_expr(ns, identifier, clean_rhs)+";"; + result=lhs+" = "+expr_to_string(ns, identifier, clean_rhs)+";"; } - + cache.insert({{identifier.get_no(), &assign.read()}, result}); return result; } @@ -170,22 +222,86 @@ static bool filter_out( source_location.get_file().empty() || source_location.is_built_in() || source_location.get_line().empty()) + { + const irep_idt id=source_location.get_function(); + if(!(has_prefix(id2string(id), CPROVER_PREFIX) && it->is_assert())) + return true; + } + + return false; +} + +static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix){ + if(expr.id()==ID_symbol && + has_prefix(id2string(to_symbol_expr(expr).get_identifier()), prefix)) + { return true; + } + forall_operands(it, expr) + { + if(contains_symbol_prefix(*it, prefix)) + return true; + } return false; } /// counterexample witness void graphml_witnesst::operator()(const goto_tracet &goto_trace) { + unsigned int max_thread_idx=0U; + bool trace_has_violation=false; + for(goto_tracet::stepst::const_iterator it=goto_trace.steps.begin(); + it!=goto_trace.steps.end(); + ++it) + { + if(it->thread_nr>max_thread_idx) + max_thread_idx=it->thread_nr; + if(it->type==goto_trace_stept::typet::ASSERT && !it->cond_value) + trace_has_violation=true; + } + graphml.key_values["sourcecodelang"]="C"; const graphmlt::node_indext sink=graphml.add_node(); graphml[sink].node_name="sink"; - graphml[sink].thread_nr=0; graphml[sink].is_violation=false; graphml[sink].has_invariant=false; + if(max_thread_idx > 0U && trace_has_violation) + { + std::vector nodes; + + for(unsigned int i=0U; i<=max_thread_idx+1U; ++i) + { + nodes.push_back(graphml.add_node()); + graphml[nodes.back()].node_name="N" + std::to_string(i); + graphml[nodes.back()].is_violation=(i==max_thread_idx+1U) ? true : false; + graphml[nodes.back()].has_invariant=false; + } + + for(auto it=nodes.cbegin(); std::next(it)!=nodes.cend(); ++it) + { + xmlt edge("edge"); + edge.set_attribute("source", graphml[*it].node_name); + edge.set_attribute("target", graphml[*std::next(it)].node_name); + const auto thread_id=std::distance(nodes.cbegin(), it); + xmlt &data=edge.new_element("data"); + data.set_attribute("key", "createThread"); + data.data=std::to_string(thread_id); + if(thread_id==0) + { + xmlt &data=edge.new_element("data"); + data.set_attribute("key", "enterFunction"); + data.data="main"; + } + graphml[*std::next(it)].in[*it].xml_node=edge; + graphml[*it].out[*std::next(it)].xml_node=edge; + } + + return; + } + // step numbers start at 1 std::vector step_to_node(goto_trace.steps.size()+1, 0); @@ -224,14 +340,16 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr); graphml[node].file=source_location.get_file(); graphml[node].line=source_location.get_line(); - graphml[node].thread_nr=it->thread_nr; graphml[node].is_violation= it->type==goto_trace_stept::typet::ASSERT && !it->cond_value; + graphml[node].has_invariant=false; step_to_node[it->step_nr]=node; } + std::size_t thread_id=0; + // build edges for(goto_tracet::stepst::const_iterator it=goto_trace.steps.begin(); @@ -240,7 +358,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) { const std::size_t from=step_to_node[it->step_nr]; - if(from==sink) + // no outgoing edges from sinks or violation nodes + if(from==sink || graphml[from].is_violation) { ++it; continue; @@ -263,6 +382,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) case goto_trace_stept::typet::ASSIGNMENT: case goto_trace_stept::typet::ASSERT: case goto_trace_stept::typet::GOTO: + case goto_trace_stept::typet::SPAWN: { xmlt edge("edge"); edge.set_attribute("source", graphml[from].node_name); @@ -276,51 +396,55 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) xmlt &data_l=edge.new_element("data"); data_l.set_attribute("key", "startline"); data_l.data=id2string(graphml[from].line); + + xmlt &data_t=edge.new_element("data"); + data_t.set_attribute("key", "threadId"); + data_t.data=std::to_string(it->thread_nr); } if(it->type==goto_trace_stept::typet::ASSIGNMENT && it->full_lhs_value.is_not_nil() && - it->full_lhs.is_not_nil()) + it->full_lhs.is_not_nil() && + it->full_lhs.id() == ID_symbol) { - xmlt &val=edge.new_element("data"); - val.set_attribute("key", "assumption"); - val.data = from_expr(ns, it->function, it->full_lhs) + " = " + - from_expr(ns, it->function, it->full_lhs_value) + ";"; - - xmlt &val_s=edge.new_element("data"); - val_s.set_attribute("key", "assumption.scope"); - val_s.data=id2string(it->pc->source_location.get_function()); + const symbol_exprt &lhs_symbol = to_symbol_expr(it->full_lhs); + if(id2string(lhs_symbol.get_identifier()) + .find("pthread_create::thread")!=std::string::npos) + { + xmlt &data_t=edge.new_element("data"); + data_t.set_attribute("key", "createThread"); + data_t.data=std::to_string(++thread_id); + } + else if( + id2string(lhs_symbol.get_identifier()) + .find("#return_value")==std::string::npos && + !contains_symbol_prefix( + it->full_lhs_value, "symex_dynamic::dynamic_object") && + !contains_symbol_prefix( + it->full_lhs, "symex_dynamic::dynamic_object") && + id2string(lhs_symbol.get_identifier()) + .find("thread")==std::string::npos && + id2string(lhs_symbol.get_identifier()) + .find("mutex")==std::string::npos && + (!it->full_lhs_value.is_constant() || + !it->full_lhs_value.has_operands() || + !has_prefix(id2string(it->full_lhs_value.op0().get(ID_value)), + "INVALID-"))) + { + xmlt &val=edge.new_element("data"); + val.set_attribute("key", "assumption"); + code_assignt assign(it->full_lhs, it->full_lhs_value); + irep_idt identifier=lhs_symbol.get_identifier(); + val.data=convert_assign_rec(identifier, assign); + + xmlt &val_s=edge.new_element("data"); + val_s.set_attribute("key", "assumption.scope"); + val_s.data=id2string(it->pc->source_location.get_function()); + } } else if(it->type==goto_trace_stept::typet::GOTO && it->pc->is_goto()) { - xmlt &val=edge.new_element("data"); - val.set_attribute("key", "sourcecode"); - const std::string cond = from_expr(ns, it->function, it->cond_expr); - const std::string neg_cond = - from_expr(ns, it->function, not_exprt(it->cond_expr)); - val.data="["+(it->cond_value ? cond : neg_cond)+"]"; - - #if 0 - xmlt edge2("edge"); - edge2.set_attribute("source", graphml[from].node_name); - edge2.set_attribute("target", graphml[sink].node_name); - - xmlt &data_f2=edge2.new_element("data"); - data_f2.set_attribute("key", "originfile"); - data_f2.data=id2string(graphml[from].file); - - xmlt &data_l2=edge2.new_element("data"); - data_l2.set_attribute("key", "startline"); - data_l2.data=id2string(graphml[from].line); - - xmlt &val2=edge2.new_element("data"); - val2.set_attribute("key", "sourcecode"); - val2.data="["+(it->cond_value ? neg_cond : cond)+"]"; - - graphml[sink].in[from].xml_node=edge2; - graphml[from].out[sink].xml_node=edge2; - #endif } graphml[to].in[from].xml_node=edge; @@ -337,7 +461,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) case goto_trace_stept::typet::OUTPUT: case goto_trace_stept::typet::SHARED_READ: case goto_trace_stept::typet::SHARED_WRITE: - case goto_trace_stept::typet::SPAWN: case goto_trace_stept::typet::MEMORY_BARRIER: case goto_trace_stept::typet::ATOMIC_BEGIN: case goto_trace_stept::typet::ATOMIC_END: @@ -359,7 +482,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) const graphmlt::node_indext sink=graphml.add_node(); graphml[sink].node_name="sink"; - graphml[sink].thread_nr=0; graphml[sink].is_violation=false; graphml[sink].has_invariant=false; @@ -405,7 +527,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) std::to_string(step_nr); graphml[node].file=source_location.get_file(); graphml[node].line=source_location.get_line(); - graphml[node].thread_nr=it->source.thread_nr; graphml[node].is_violation=false; graphml[node].has_invariant=false; @@ -446,6 +567,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) case goto_trace_stept::typet::ASSIGNMENT: case goto_trace_stept::typet::ASSERT: case goto_trace_stept::typet::GOTO: + case goto_trace_stept::typet::SPAWN: { xmlt edge("edge"); edge.set_attribute("source", graphml[from].node_name); @@ -474,15 +596,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) graphml[to].invariant_scope= id2string(it->source.pc->source_location.get_function()); } - else if(it->is_goto() && - it->source.pc->is_goto()) - { - xmlt &val=edge.new_element("data"); - val.set_attribute("key", "sourcecode"); - const std::string cond = - from_expr(ns, it->source.function, it->cond_expr); - val.data="["+cond+"]"; - } graphml[to].in[from].xml_node=edge; graphml[from].out[to].xml_node=edge; @@ -498,7 +611,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) case goto_trace_stept::typet::OUTPUT: case goto_trace_stept::typet::SHARED_READ: case goto_trace_stept::typet::SHARED_WRITE: - case goto_trace_stept::typet::SPAWN: case goto_trace_stept::typet::MEMORY_BARRIER: case goto_trace_stept::typet::ATOMIC_BEGIN: case goto_trace_stept::typet::ATOMIC_END: diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 125042ff065..56de8162d42 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -38,6 +38,7 @@ goto_symex_statet::goto_symex_statet() goto_symex_statet::~goto_symex_statet()=default; +#if 0 /// write to a variable static bool check_renaming(const exprt &expr); @@ -120,10 +121,11 @@ static bool check_renaming(const exprt &expr) return false; } +#endif static void assert_l1_renaming(const exprt &expr) { - #if 1 + #if 0 if(check_renaming_l1(expr)) { std::cerr << expr.pretty() << '\n'; @@ -136,7 +138,7 @@ static void assert_l1_renaming(const exprt &expr) static void assert_l2_renaming(const exprt &expr) { - #if 1 + #if 0 if(check_renaming(expr)) { std::cerr << expr.pretty() << '\n'; diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 03a2819b3e2..bb49c557e4b 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -218,17 +218,6 @@ void goto_symext::symex_assign_symbol( guardt &guard, assignment_typet assignment_type) { - // do not assign to L1 objects that have gone out of scope -- - // pointer dereferencing may yield such objects; parameters do not - // have an L2 entry set up beforehand either, so exempt them from - // this check (all other L1 objects should have seen a declaration) - const symbolt *s; - if(!ns.lookup(lhs.get_object_name(), s) && - !s->is_parameter && - !lhs.get_level_1().empty() && - state.level2.current_count(lhs.get_identifier())==0) - return; - exprt ssa_rhs=rhs; // put assignment guard into the rhs diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 85d144ad6f1..f062ba553a7 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -184,18 +184,20 @@ void goto_symext::symex_allocate( exprt rhs; + symbol_exprt v=value_symbol.symbol_expr(); + v.add("#dynamic_guard", state.guard); + if(object_type.id()==ID_array) { - const auto &array_type = to_array_type(object_type); + const auto &array_type = to_array_type(value_symbol.type); index_exprt index_expr(array_type.subtype()); - index_expr.array()=value_symbol.symbol_expr(); + index_expr.array() = v; index_expr.index()=from_integer(0, index_type()); rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype())); } else { - rhs=address_of_exprt( - value_symbol.symbol_expr(), pointer_type(value_symbol.type)); + rhs = address_of_exprt(v, pointer_type(value_symbol.type)); } if(rhs.type()!=lhs.type()) diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index ff2caf9cb4a..8b39b2610f4 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -66,11 +66,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) state.propagation.erase(l1_identifier); // L2 renaming - // inlining may yield multiple declarations of the same identifier - // within the same L1 context - if(state.level2.current_names.find(l1_identifier)== - state.level2.current_names.end()) - state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0); + state.level2.current_names.insert( + std::make_pair(l1_identifier, std::make_pair(ssa, 0))); state.level2.increase_counter(l1_identifier); const bool record_events=state.record_events; state.record_events=false; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index ec7f61a3f43..d2524cfc111 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -452,17 +452,23 @@ void goto_symext::phi_function( // 1. Either guard is false, so we can't follow that branch. // 2. Either identifier is of generation zero, and so hasn't been // initialized and therefor an invalid target. - if(dest_state.guard.is_false()) - rhs=goto_state_rhs; - else if(goto_state.guard.is_false()) - rhs=dest_state_rhs; - else if(goto_state.level2_current_count(l1_identifier) == 0) + if( + dest_state.guard.is_false() || + dest_state.level2.current_count(l1_identifier) == 0) { - rhs = dest_state_rhs; + if(goto_state.level2_current_count(l1_identifier) == 0) + continue; + + rhs = goto_state_rhs; } - else if(dest_state.level2.current_count(l1_identifier) == 0) + else if( + goto_state.guard.is_false() || + goto_state.level2_current_count(l1_identifier) == 0) { - rhs = goto_state_rhs; + if(dest_state.level2.current_count(l1_identifier) == 0) + continue; + + rhs = dest_state_rhs; } else { diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index b9bb0828e64..5120dfafd0e 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -63,16 +63,13 @@ void static_lifetime_init( continue; // special values - if(identifier==CPROVER_PREFIX "constant_infinity_uint" || - identifier==CPROVER_PREFIX "memory" || - identifier=="__func__" || - identifier=="__FUNCTION__" || - identifier=="__PRETTY_FUNCTION__" || - identifier=="argc'" || - identifier=="argv'" || - identifier=="envp'" || - identifier=="envp_size'") + if( + identifier == CPROVER_PREFIX "constant_infinity_uint" || + identifier == CPROVER_PREFIX "memory" || identifier == "__func__" || + identifier == "__FUNCTION__" || identifier == "__PRETTY_FUNCTION__") + { continue; + } // just for linking if(has_prefix(id, CPROVER_PREFIX "architecture_")) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 791c06475b1..7236621b7bf 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -12,7 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include +#include +#include +#include literalt bv_pointerst::convert_rest(const exprt &expr) { @@ -25,24 +29,15 @@ literalt bv_pointerst::convert_rest(const exprt &expr) if(operands.size()==1 && operands[0].type().id()==ID_pointer) { - const bvt &bv=convert_bv(operands[0]); - - if(!bv.empty()) - { - bvt invalid_bv; - encode(pointer_logic.get_invalid_object(), invalid_bv); - - bvt equal_invalid_bv; - equal_invalid_bv.resize(object_bits); + // we postpone + literalt l=prop.new_variable(); - for(std::size_t i=0; i( + ssa.get_original_expr().find("#dynamic_guard")); + + if(guard.is_nil()) + continue; + + const bvt &guard_bv=convert_bv(guard); + assert(guard_bv.size()==1); + literalt l_guard=guard_bv[0]; + + disj.push_back(prop.land(!l_guard, l1)); + } + + // compare object part to max object number + bvt bv; + encode(number, bv); + + bv.erase(bv.begin(), bv.begin()+offset_bits); + assert(bv.size()==saved_bv.size()); + + disj.push_back( + bv_utils.rel(saved_bv, ID_ge, bv, bv_utilst::representationt::UNSIGNED)); + + assert(postponed.bv.size()==1); + literalt l=postponed.bv.front(); + prop.l_set_to(prop.lequal(prop.lor(disj), l), true); + } else UNREACHABLE; } diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 1819f13a299..32b250edbdf 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "string2int.h" #include "string_utils.h" +#include #include #include diff --git a/src/util/irep.cpp b/src/util/irep.cpp index b403ea96550..31d07351b17 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -153,8 +153,8 @@ void irept::nonrecursive_destructor(dt *old_data) if(d->ref_count==0) { stack.reserve(stack.size()+ - d->named_sub.size()+ - d->comments.size()+ + std::distance(d->named_sub.begin(), d->named_sub.end()) + + std::distance(d->comments.begin(), d->comments.end()) + d->sub.size()); for(named_subt::iterator @@ -275,7 +275,11 @@ void irept::remove(const irep_namet &name) named_subt::iterator it=named_subt_lower_bound(s, name); if(it!=s.end() && it->first==name) - s.erase(it); + { + named_subt::iterator before = s.before_begin(); + while(std::next(before) != it) ++before; + s.erase_after(before); + } #else s.erase(name); #endif @@ -312,7 +316,11 @@ irept &irept::add(const irep_namet &name) if(it==s.end() || it->first!=name) - it=s.insert(it, std::make_pair(name, irept())); + { + named_subt::iterator before = s.before_begin(); + while(std::next(before) != it) ++before; + it = s.emplace_after(before, name, irept()); + } return it->second; #else @@ -330,7 +338,11 @@ irept &irept::add(const irep_namet &name, const irept &irep) if(it==s.end() || it->first!=name) - it=s.insert(it, std::make_pair(name, irep)); + { + named_subt::iterator before = s.before_begin(); + while(std::next(before) != it) ++before; + it = s.emplace_after(before, name, irep); + } else it->second=irep; @@ -393,10 +405,20 @@ bool irept::full_eq(const irept &other) const const irept::named_subt &i1_comments=get_comments(); const irept::named_subt &i2_comments=other.get_comments(); +#ifdef SUB_IS_LIST + if( + i1_sub.size() != i2_sub.size() || + std::distance(i1_named_sub.begin(), i1_named_sub.end()) != + std::distance(i2_named_sub.begin(), i2_named_sub.end()) || + std::distance(i1_comments.begin(), i1_comments.end()) != + std::distance(i2_comments.begin(), i2_comments.end())) + return false; +#else if(i1_sub.size()!=i2_sub.size() || i1_named_sub.size()!=i2_named_sub.size() || i1_comments.size()!=i2_comments.size()) return false; +#endif for(std::size_t i=0; ii_n_size) @@ -591,7 +620,13 @@ std::size_t irept::hash() const result=hash_combine(result, it->second.hash()); } - result=hash_finalize(result, named_sub.size()+sub.size()); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(named_sub.begin(), named_sub.end()); +#else + const std::size_t named_sub_size = named_sub.size(); +#endif + result = hash_finalize(result, named_sub_size + sub.size()); #ifdef HASH_CODE read().hash_code=result; @@ -624,9 +659,16 @@ std::size_t irept::full_hash() const result=hash_combine(result, it->second.full_hash()); } - result=hash_finalize( - result, - named_sub.size()+sub.size()+comments.size()); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(named_sub.begin(), named_sub.end()); + const std::size_t comments_size = + std::distance(comments.begin(), comments.end()); +#else + const std::size_t named_sub_size = named_sub.size(); + const std::size_t comments_size = comments.size(); +#endif + result = hash_finalize(result, named_sub_size + sub.size() + comments_size); return result; } diff --git a/src/util/irep.h b/src/util/irep.h index 706fb60db26..3398ddfb947 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -18,12 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "irep_ids.h" #define SHARING -// #define HASH_CODE +#define HASH_CODE #define USE_MOVE -// #define SUB_IS_LIST +#define SUB_IS_LIST #ifdef SUB_IS_LIST -#include +#include #else #include #endif @@ -164,7 +164,7 @@ class irept // memory and increase efficiency. #ifdef SUB_IS_LIST - typedef std::list > named_subt; + typedef std::forward_list > named_subt; #else typedef std::map named_subt; #endif diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp index dc79d098670..b49ef2b105d 100644 --- a/src/util/irep_hash_container.cpp +++ b/src/util/irep_hash_container.cpp @@ -51,9 +51,16 @@ void irep_hash_container_baset::pack( const irept::named_subt &named_sub=irep.get_named_sub(); const irept::named_subt &comments=irep.get_comments(); - packed.reserve( - 1+1+sub.size()+named_sub.size()*2+ - (full?comments.size()*2:0)); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(named_sub.begin(), named_sub.end()); + const std::size_t comments_size = full ? + std::distance(comments.begin(), comments.end()) : 0; +#else + const std::size_t named_sub_size = named_sub.size(); + const std::size_t comments_size = full ? comments.size() : 0; +#endif + packed.reserve(1 + 1 + sub.size() + named_sub_size * 2 + comments_size * 2); packed.push_back(irep_id_hash()(irep.id())); @@ -61,7 +68,7 @@ void irep_hash_container_baset::pack( forall_irep(it, sub) packed.push_back(number(*it)); - packed.push_back(named_sub.size()); + packed.push_back(named_sub_size); forall_named_irep(it, named_sub) { packed.push_back(irep_id_hash()(it->first)); // id @@ -70,7 +77,7 @@ void irep_hash_container_baset::pack( if(full) { - packed.push_back(comments.size()); + packed.push_back(comments_size); forall_named_irep(it, comments) { packed.push_back(irep_id_hash()(it->first)); // id diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp index 6f223d0c7f6..35904def2fa 100644 --- a/src/util/lispirep.cpp +++ b/src/util/lispirep.cpp @@ -46,9 +46,17 @@ void irep2lisp(const irept &src, lispexprt &dest) dest.value=""; dest.type=lispexprt::List; - dest.reserve(2+2*src.get_sub().size() - +2*src.get_named_sub().size() - +2*src.get_comments().size()); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(src.get_named_sub().begin(), src.get_named_sub().end()); + const std::size_t comments_size = + std::distance(src.get_comments().begin(), src.get_comments().end()); +#else + const std::size_t named_sub_size = src.get_named_sub().size(); + const std::size_t comments_size = src.get_comments().size(); +#endif + dest.reserve( + 2 + 2 * src.get_sub().size() + 2 * named_sub_size + 2 * comments_size); lispexprt id; id.type=lispexprt::String; diff --git a/src/util/merge_irep.cpp b/src/util/merge_irep.cpp index 02e04b461e5..a82846dd006 100644 --- a/src/util/merge_irep.cpp +++ b/src/util/merge_irep.cpp @@ -28,7 +28,13 @@ std::size_t to_be_merged_irept::hash() const result, static_cast(it->second).hash()); } - result=hash_finalize(result, named_sub.size()+sub.size()); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(named_sub.begin(), named_sub.end()); +#else + const std::size_t named_sub_size = named_sub.size(); +#endif + result = hash_finalize(result, named_sub_size + sub.size()); return result; } @@ -44,9 +50,16 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const const irept::named_subt &o_named_sub=other.get_named_sub(); if(sub.size()!=o_sub.size()) - return true; + return false; +#ifdef SUB_IS_LIST + if( + std::distance(named_sub.begin(), named_sub.end()) != + std::distance(o_named_sub.begin(), o_named_sub.end())) + return false; +#else if(named_sub.size()!=o_named_sub.size()) - return true; + return false; +#endif { irept::subt::const_iterator s_it=sub.begin(); @@ -95,13 +108,19 @@ const merged_irept &merged_irepst::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); +#ifdef SUB_IS_LIST + irept::named_subt::iterator before = dest_named_sub.before_begin(); +#endif forall_named_irep(it, src_named_sub) + { #ifdef SUB_IS_LIST - dest_named_sub.push_back( - std::make_pair(it->first, merged(it->second))); // recursive call + dest_named_sub.emplace_after( + before, it->first, merged(it->second)); // recursive call + ++before; #else dest_named_sub[it->first]=merged(it->second); // recursive call #endif + } std::pair result= to_be_merged_irep_store.insert(to_be_merged_irept(new_irep)); @@ -140,24 +159,36 @@ const irept &merge_irept::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); +#ifdef SUB_IS_LIST + irept::named_subt::iterator before = dest_named_sub.before_begin(); +#endif forall_named_irep(it, src_named_sub) + { #ifdef SUB_IS_LIST - dest_named_sub.push_back( - std::make_pair(it->first, merged(it->second))); // recursive call + dest_named_sub.emplace_after( + before, it->first, merged(it->second)); // recursive call + ++before; #else dest_named_sub[it->first]=merged(it->second); // recursive call #endif + } const irept::named_subt &src_comments=irep.get_comments(); irept::named_subt &dest_comments=new_irep.get_comments(); +#ifdef SUB_IS_LIST + before = dest_comments.before_begin(); +#endif forall_named_irep(it, src_comments) + { #ifdef SUB_IS_LIST - dest_comments.push_back( - std::make_pair(it->first, merged(it->second))); // recursive call + dest_comments.emplace_after( + before, it->first, merged(it->second)); // recursive call + ++before; #else dest_comments[it->first]=merged(it->second); // recursive call #endif + } return *irep_store.insert(new_irep).first; } @@ -188,24 +219,36 @@ const irept &merge_full_irept::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); +#ifdef SUB_IS_LIST + irept::named_subt::iterator before = dest_named_sub.before_begin(); +#endif forall_named_irep(it, src_named_sub) + { #ifdef SUB_IS_LIST - dest_named_sub.push_back( - std::make_pair(it->first, merged(it->second))); // recursive call + dest_named_sub.emplace_after( + before, it->first, merged(it->second)); // recursive call + ++before; #else dest_named_sub[it->first]=merged(it->second); // recursive call #endif + } const irept::named_subt &src_comments=irep.get_comments(); irept::named_subt &dest_comments=new_irep.get_comments(); +#ifdef SUB_IS_LIST + before = dest_comments.before_begin(); +#endif forall_named_irep(it, src_comments) + { #ifdef SUB_IS_LIST - dest_comments.push_back( - std::make_pair(it->first, merged(it->second))); // recursive call + dest_comments.emplace_after( + before, it->first, merged(it->second)); // recursive call + ++before; #else dest_comments[it->first]=merged(it->second); // recursive call #endif + } return *irep_store.insert(new_irep).first; } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 3be87c69f00..9716c550d0f 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2127,7 +2127,7 @@ bool simplify_exprt::simplify_node(exprt &expr) bool result=true; - result=sort_and_join(expr) && result; + result = sort_and_join(expr, false) && result; if(expr.id()==ID_typecast) result=simplify_typecast(expr) && result; diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index 53b2f38f7e1..83e086e6959 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -119,7 +119,7 @@ static const struct saj_tablet &sort_and_join( return saj_table[i]; } -bool sort_and_join(exprt &expr) +bool sort_and_join(exprt &expr, bool do_sort) { bool result=true; @@ -158,8 +158,9 @@ bool sort_and_join(exprt &expr) } // sort it + if(do_sort) + result = sort_operands(new_ops) && result; - result=sort_operands(new_ops) && result; expr.operands().swap(new_ops); return result; diff --git a/src/util/simplify_utils.h b/src/util/simplify_utils.h index 33e294f4e96..6f0af7865b9 100644 --- a/src/util/simplify_utils.h +++ b/src/util/simplify_utils.h @@ -14,6 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com bool sort_operands(exprt::operandst &operands); -bool sort_and_join(exprt &expr); +bool sort_and_join(exprt &expr, bool do_sort=true); #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H diff --git a/src/util/std_pair_hash.h b/src/util/std_pair_hash.h new file mode 100644 index 00000000000..33ea4635004 --- /dev/null +++ b/src/util/std_pair_hash.h @@ -0,0 +1,35 @@ +/*******************************************************************\ + +Module: util/std_pair_hash + +Author: Marek Trtik, marek.trtik@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_STD_PAIR_HASH_H +#define CPROVER_UTIL_STD_PAIR_HASH_H + +#include + +template +inline void hash_combine(std::size_t & seed, const T & v) +{ + std::hash hasher; + seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2); +} + +namespace std +{ + template struct hash > + { + inline size_t operator()(const pair & v) const + { + size_t seed = 0; + ::hash_combine(seed, v.first); + ::hash_combine(seed, v.second); + return seed; + } + }; +} + +#endif diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 17dc6fd9577..4b780b9df8c 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -54,7 +54,6 @@ static bool build_graph_rec( node.node_name=node_name; node.is_violation=false; node.has_invariant=false; - node.thread_nr=0; for(xmlt::elementst::const_iterator e_it=xml.elements.begin(); @@ -66,8 +65,6 @@ static bool build_graph_rec( if(e_it->get_attribute("key")=="violation" && e_it->data=="true") node.is_violation=e_it->data=="true"; - else if(e_it->get_attribute("key")=="threadNumber") - node.thread_nr=safe_string2unsigned(e_it->data); else if(e_it->get_attribute("key")=="entry" && e_it->data=="true") entrynode=node_name; @@ -255,33 +252,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.set_attribute("id", "invariant.scope"); } - // - // path - // - { - xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "nodeType"); - key.set_attribute("attr.type", "string"); - key.set_attribute("for", "node"); - key.set_attribute("id", "nodetype"); - - key.new_element("default").data="path"; - } - - // - // false - // - { - xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "isFrontierNode"); - key.set_attribute("attr.type", "boolean"); - key.set_attribute("for", "node"); - key.set_attribute("id", "frontier"); - - key.new_element("default").data="false"; - } - // // false @@ -336,14 +306,39 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.new_element("default").data="false"; } + // + // false + // + { + xmlt &key=graphml.new_element("key"); + key.set_attribute("attr.name", "cyclehead"); + key.set_attribute("attr.type", "boolean"); + key.set_attribute("for", "edge"); + key.set_attribute("id", "cyclehead"); + + key.new_element("default").data="false"; + } + // - // TODO: format for multi-threaded programs not defined yet { xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "threadNumber"); + key.set_attribute("attr.name", "threadId"); key.set_attribute("attr.type", "int"); - key.set_attribute("for", "node"); - key.set_attribute("id", "thread"); + key.set_attribute("for", "edge"); + key.set_attribute("id", "threadId"); + + key.new_element("default").data="0"; + } + + // + { + xmlt &key=graphml.new_element("key"); + key.set_attribute("attr.name", "createThread"); + key.set_attribute("attr.type", "int"); + key.set_attribute("for", "edge"); + key.set_attribute("id", "createThread"); key.new_element("default").data="0"; } @@ -408,15 +403,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.set_attribute("id", "producer"); } - // - { - xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "sourcecode"); - key.set_attribute("attr.type", "string"); - key.set_attribute("for", "edge"); - key.set_attribute("id", "sourcecode"); - } - // { xmlt &key=graphml.new_element("key"); @@ -525,13 +511,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os) entry_done=true; } - if(n.thread_nr!=0) - { - xmlt &entry=node.new_element("data"); - entry.set_attribute("key", "threadNumber"); - entry.data=std::to_string(n.thread_nr); - } - // // true // diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h index f86dac5648e..cbdcd122828 100644 --- a/src/xmllang/graphml.h +++ b/src/xmllang/graphml.h @@ -32,7 +32,6 @@ struct xml_graph_nodet:public graph_nodet std::string node_name; irep_idt file; irep_idt line; - unsigned thread_nr; bool is_violation; bool has_invariant; std::string invariant; diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp index ea97126f19e..50f7a4e7556 100644 --- a/unit/util/irep.cpp +++ b/unit/util/irep.cpp @@ -141,11 +141,15 @@ SCENARIO("irept_memory", "[core][utils][irept]") irept irep2("second_irep"); irep.add("a_new_element", irep2); REQUIRE(irep.find("a_new_element").id() == "second_irep"); - REQUIRE(irep.get_named_sub().size() == 1); + std::size_t named_sub_size = std::distance( + irep.get_named_sub().begin(), irep.get_named_sub().end()); + REQUIRE(named_sub_size == 1); irep.add("#a_comment", irep2); REQUIRE(irep.find("#a_comment").id() == "second_irep"); - REQUIRE(irep.get_comments().size() == 1); + std::size_t comments_size = + std::distance(irep.get_comments().begin(), irep.get_comments().end()); + REQUIRE(comments_size == 1); irept bak(irep); irep.remove("no_such_id"); @@ -159,19 +163,29 @@ SCENARIO("irept_memory", "[core][utils][irept]") irep.move_to_named_sub("another_entry", irep2); REQUIRE(irep.get_sub().size() == 1); - REQUIRE(irep.get_named_sub().size() == 1); - REQUIRE(irep.get_comments().size() == 1); + named_sub_size = std::distance( + irep.get_named_sub().begin(), irep.get_named_sub().end()); + REQUIRE(named_sub_size == 1); + comments_size = + std::distance(irep.get_comments().begin(), irep.get_comments().end()); + REQUIRE(comments_size == 1); irept irep3; irep.move_to_named_sub("#a_comment", irep3); REQUIRE(irep.find("#a_comment").id().empty()); REQUIRE(irep.get_sub().size() == 1); - REQUIRE(irep.get_named_sub().size() == 1); - REQUIRE(irep.get_comments().size() == 1); + named_sub_size = std::distance( + irep.get_named_sub().begin(), irep.get_named_sub().end()); + REQUIRE(named_sub_size == 1); + comments_size = + std::distance(irep.get_comments().begin(), irep.get_comments().end()); + REQUIRE(comments_size == 1); irept irep4; irep.move_to_named_sub("#another_comment", irep4); - REQUIRE(irep.get_comments().size() == 2); + comments_size = + std::distance(irep.get_comments().begin(), irep.get_comments().end()); + REQUIRE(comments_size == 2); } THEN("Setting and getting works")