diff --git a/.gitignore b/.gitignore index 115ca57475c..362978b3a23 100644 --- a/.gitignore +++ b/.gitignore @@ -19,6 +19,8 @@ src/.settings/* # Visual Studio Debug/* Release/* +#vi(m) +*.swp # compilation files *.lo @@ -65,6 +67,8 @@ jbmc/regression/**/tests-symex-driven-loading.log # files stored by editors *~ +.*.swp +.*.swo # libs downloaded by make [name]-download minisat*/ diff --git a/regression/ansi-c/code_contracts1/main.c b/regression/ansi-c/code_contracts1/main.c new file mode 100644 index 00000000000..b2c1a16a0c6 --- /dev/null +++ b/regression/ansi-c/code_contracts1/main.c @@ -0,0 +1,21 @@ +int foo() __CPROVER_ensures(__CPROVER_forall { + int i; + 1 == 1 +}) +{ + return 1; +} + +int bar() __CPROVER_ensures(__CPROVER_forall { + int i; + 1 == 1 +} && __CPROVER_return_value == 1) +{ + return 1; +} + +int main() +{ + foo(); + bar(); +} diff --git a/regression/ansi-c/code_contracts1/test.desc b/regression/ansi-c/code_contracts1/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/code_contracts1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/contracts/function_apply_01/test.desc b/regression/contracts/function_apply_01/test.desc index abc8686ad8e..4f37c84c808 100644 --- a/regression/contracts/function_apply_01/test.desc +++ b/regression/contracts/function_apply_01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --apply-code-contracts ^EXIT=0$ @@ -6,4 +6,3 @@ main.c ^VERIFICATION SUCCESSFUL$ -- -- -Applying code contracts currently also checks them. diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/function_check_01/test.desc +++ b/regression/contracts/function_check_01/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc index 20a7e46f099..3a3bc557bf7 100644 --- a/regression/contracts/function_check_04/test.desc +++ b/regression/contracts/function_check_04/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$ -^\[foo.1\] line 9 : FAILURE$ +^\[foo.1\] .* : FAILURE$ ^VERIFICATION FAILED$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/function_check_05/test.desc b/regression/contracts/function_check_05/test.desc index 77e210f10d8..7c82bf97f02 100644 --- a/regression/contracts/function_check_05/test.desc +++ b/regression/contracts/function_check_05/test.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE main.c --check-code-contracts -^\[main.assertion.1\] assertion y == 0: FAILURE$ -^\[main.assertion.2\] assertion z == 1: SUCCESS$ -^\[foo.1\] : SUCCESS$ -^VERIFICATION SUCCESSFUL$ +^\[main.assertion.1\] .* assertion y == 0: FAILURE$ +^\[main.assertion.2\] .* assertion z == 1: SUCCESS$ +^\[foo.1\] .* : SUCCESS$ +^VERIFICATION FAILED$ -- -- -Contract checking does not properly havoc function calls. diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c index b63364f4d57..10d79cf8190 100644 --- a/regression/contracts/function_check_mem_01/main.c +++ b/regression/contracts/function_check_mem_01/main.c @@ -33,7 +33,7 @@ void foo(bar *x) __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar))) { x->x += 1; - return + return; } int main() diff --git a/regression/contracts/function_check_mem_01/test.desc b/regression/contracts/function_check_mem_01/test.desc index b46799f781b..c45406ad744 100644 --- a/regression/contracts/function_check_mem_01/test.desc +++ b/regression/contracts/function_check_mem_01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --check-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/invar_check_01/test.desc +++ b/regression/contracts/invar_check_01/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/invar_check_02/test.desc +++ b/regression/contracts/invar_check_02/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/invar_check_03/test.desc +++ b/regression/contracts/invar_check_03/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc index f8abcf720a5..e5a66f2d71b 100644 --- a/regression/contracts/invar_check_04/test.desc +++ b/regression/contracts/invar_check_04/test.desc @@ -1,12 +1,11 @@ CORE main.c ---apply-code-contracts +--check-code-contracts +^EXIT=10$ +^SIGNAL=0$ ^\[main.1\] .* Loop invariant violated before entry: SUCCESS$ ^\[main.2\] .* Loop invariant not preserved: SUCCESS$ ^\[main.assertion.1\] .* assertion r == 0: FAILURE$ ^VERIFICATION FAILED$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/goto-instrument/expand-pointer-predicates1/main.c b/regression/goto-instrument/expand-pointer-predicates1/main.c new file mode 100644 index 00000000000..acf68d8fa87 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates1/main.c @@ -0,0 +1,7 @@ +int main() +{ + int *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x)); + *x = 1; + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates1/test.desc b/regression/goto-instrument/expand-pointer-predicates1/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates2/main.c b/regression/goto-instrument/expand-pointer-predicates2/main.c new file mode 100644 index 00000000000..8205fbd42e0 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates2/main.c @@ -0,0 +1,7 @@ +int main() +{ + int *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int))); + *x = 1; + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates2/test.desc b/regression/goto-instrument/expand-pointer-predicates2/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates3/main.c b/regression/goto-instrument/expand-pointer-predicates3/main.c new file mode 100644 index 00000000000..f4f7ce609dd --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates3/main.c @@ -0,0 +1,8 @@ +int main() +{ + int *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int))); + __CPROVER_assert( + __CPROVER_points_to_valid_memory(x, sizeof(int)), "Assert matches assume"); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates3/test.desc b/regression/goto-instrument/expand-pointer-predicates3/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates4/main.c b/regression/goto-instrument/expand-pointer-predicates4/main.c new file mode 100644 index 00000000000..a4c9c33cfa8 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates4/main.c @@ -0,0 +1,7 @@ +int main() +{ + int x; + int *y = &x; + __CPROVER_assert(__CPROVER_points_to_valid_memory(y), "Assert works on &"); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates4/test.desc b/regression/goto-instrument/expand-pointer-predicates4/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates5/main.c b/regression/goto-instrument/expand-pointer-predicates5/main.c new file mode 100644 index 00000000000..9e898c16e14 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates5/main.c @@ -0,0 +1,19 @@ +struct bar +{ + int w; + int x; + int y; + int z; +}; + +int main() +{ + struct bar s; + s.z = 5; + int *x_pointer = &(s.x); + __CPROVER_assert( + __CPROVER_points_to_valid_memory(x_pointer, 3 * sizeof(int)), + "Variable length assert"); + assert(x_pointer[2] == 5); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates5/test.desc b/regression/goto-instrument/expand-pointer-predicates5/test.desc new file mode 100644 index 00000000000..eca2be9cee2 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates5/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.assertion.1\] Variable length assert: SUCCESS$ +^\[main.assertion.2\] assertion x_pointer\[\(signed long( long)? int\)2\] == 5: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates6/main.c b/regression/goto-instrument/expand-pointer-predicates6/main.c new file mode 100644 index 00000000000..a8b4931a4b1 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates6/main.c @@ -0,0 +1,21 @@ +#include + +struct my_struct +{ + int *field1; + int *field2; +}; + +void example(struct my_struct *s) +{ + s->field2 = malloc(sizeof(*(s->field2))); +} + +int main() +{ + struct my_struct *s; + __CPROVER_assume(__CPROVER_points_to_valid_memory(s)); + example(s); + __CPROVER_assert(__CPROVER_points_to_valid_memory(s->field2), ""); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates6/test.desc b/regression/goto-instrument/expand-pointer-predicates6/test.desc new file mode 100644 index 00000000000..69d70b62e0f --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates6/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.assertion.1\] : SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates7/main.c b/regression/goto-instrument/expand-pointer-predicates7/main.c new file mode 100644 index 00000000000..5f18fb9fa1f --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates7/main.c @@ -0,0 +1,22 @@ +#include + +struct my_struct +{ + int *field; +}; + +void example(struct my_struct *s) +{ + __CPROVER_assume(__CPROVER_points_to_valid_memory(s)); + size_t size; + __CPROVER_assume(size == sizeof(*(s->field))); + __CPROVER_assume(__CPROVER_points_to_valid_memory(s->field, size)); + int read = *(s->field); +} + +int main() +{ + struct my_struct *s; + example(s); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates7/test.desc b/regression/goto-instrument/expand-pointer-predicates7/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates7/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates8/main.c b/regression/goto-instrument/expand-pointer-predicates8/main.c new file mode 100644 index 00000000000..766ea1525f9 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates8/main.c @@ -0,0 +1,16 @@ +#include + +int main() +{ + int *x; + int *y; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x, 2 * sizeof(int))); + __CPROVER_assume(__CPROVER_points_to_valid_memory(y, 2 * sizeof(int) - 1)); + (void)(x[0]); // Should succeed + (void)(x[1]); // Should succeed + (void)(x[2]); // Should fail + (void)(x[-1]); // Should fail + (void)(y[0]); // Should succeed + (void)(y[1]); // Should fail + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates8/test.desc b/regression/goto-instrument/expand-pointer-predicates8/test.desc new file mode 100644 index 00000000000..a15c074645c --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates8/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in x\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)2\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)-1\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in y\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)1\]: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates9/main.c b/regression/goto-instrument/expand-pointer-predicates9/main.c new file mode 100644 index 00000000000..bb80cf4c996 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates9/main.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + char *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x)); + (void)(*x); // Should succeed + (void)(*(x + 1)); // Should fail + (void)(*(x - 1)); // Should fail + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates9/test.desc b/regression/goto-instrument/expand-pointer-predicates9/test.desc new file mode 100644 index 00000000000..4a9a4bf26fc --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates9/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*x: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*\(x - \(signed long( long)? int\)1\): FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/regression/goto-instrument/slice19/test.desc b/regression/goto-instrument/slice19/test.desc index 03cff4a4fac..3793f7374e1 100644 --- a/regression/goto-instrument/slice19/test.desc +++ b/regression/goto-instrument/slice19/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --full-slice ^EXIT=0$ diff --git a/regression/goto-instrument/slice24/main.c b/regression/goto-instrument/slice24/main.c new file mode 100644 index 00000000000..6989dc105d5 --- /dev/null +++ b/regression/goto-instrument/slice24/main.c @@ -0,0 +1,20 @@ +#include +#include + +static void f(int *x) +{ + *x = 5; +} +static void g(int *x) +{ + assert(*x == 5); +} + +int main(int argc, char **argv) +{ + int *x = (int *)malloc(sizeof(int)); + f(x); + g(x); + + return 0; +} diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc new file mode 100644 index 00000000000..3906443eafc --- /dev/null +++ b/regression/goto-instrument/slice24/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--full-slice --add-library +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +Data dependencies across function calls are still not working correctly. diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index e84ba05cb18..07d70522331 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -174,7 +174,9 @@ void dep_graph_domaint::data_dependencies( { bool found=false; for(const auto &wr : w_range.second) + { for(const auto &r_range : r_ranges) + { if(!found && may_be_def_use_pair(wr.first, wr.second, r_range.first, r_range.second)) @@ -183,6 +185,8 @@ void dep_graph_domaint::data_dependencies( data_deps.insert(w_range.first); found=true; } + } + } } dep_graph.reaching_definitions()[to].clear_cache(it->first); diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index b2386f73f96..aee94eacffb 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -138,8 +138,6 @@ void rw_range_sett::get_objects_dereference( { const exprt &pointer=deref.pointer(); get_objects_rec(get_modet::READ, pointer); - if(mode!=get_modet::READ) - get_objects_rec(mode, pointer); } void rw_range_sett::get_objects_byte_extract( @@ -430,16 +428,18 @@ void rw_range_sett::get_objects_typecast( void rw_range_sett::get_objects_address_of(const exprt &object) { - if(object.id() == ID_string_constant || - object.id() == ID_label || - object.id() == ID_array || - object.id() == ID_null_object) + if( + object.id() == ID_symbol || object.id() == ID_string_constant || + object.id() == ID_label || object.id() == ID_array || + object.id() == ID_null_object) + { // constant, nothing to do return; - else if(object.id()==ID_symbol) - get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_dereference) + { get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_index) { const index_exprt &index=to_index_expr(object); @@ -543,6 +543,11 @@ void rw_range_sett::get_objects_rec( get_objects_array(mode, to_array_expr(expr), range_start, size); else if(expr.id()==ID_struct) get_objects_struct(mode, to_struct_expr(expr), range_start, size); + else if(expr.id() == ID_dynamic_object) + { + const auto obj_instance = to_dynamic_object_expr(expr).get_instance(); + add(mode, "goto_rw::dynamic_object-" + std::to_string(obj_instance), 0, -1); + } else if(expr.id()==ID_symbol) { const symbol_exprt &symbol=to_symbol_expr(expr); @@ -586,11 +591,6 @@ void rw_range_sett::get_objects_rec( { // dereferencing may yield some weird ones, ignore these } - else if(mode==get_modet::LHS_W) - { - forall_operands(it, expr) - get_objects_rec(mode, *it); - } else throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled"; } @@ -630,6 +630,8 @@ void rw_range_set_value_sett::get_objects_dereference( exprt object=deref; dereference(target, object, ns, value_sets); + PRECONDITION(object.is_not_nil()); + auto type_bits = pointer_offset_bits(object.type(), ns); range_spect new_size; diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index e60efc7daa0..1c3586cf6da 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -319,20 +319,17 @@ void rd_range_domaint::transform_assign( { const irep_idt &identifier=it->first; // ignore symex::invalid_object - const symbolt *symbol_ptr; - if(ns.lookup(identifier, symbol_ptr)) + const symbolt *symbol_ptr = nullptr; + bool not_found = ns.lookup(identifier, symbol_ptr); + if(not_found && has_prefix(id2string(identifier), "symex::invalid_object")) continue; - INVARIANT_STRUCTURED( - symbol_ptr!=nullptr, - nullptr_exceptiont, - "Symbol is in symbol table"); const range_domaint &ranges=rw_set.get_ranges(it); - if(is_must_alias && - (!rd.get_is_threaded()(from) || - (!symbol_ptr->is_shared() && - !rd.get_is_dirty()(identifier)))) + if( + is_must_alias && (!rd.get_is_threaded()(from) || + (symbol_ptr != nullptr && symbol_ptr->is_shared() && + !rd.get_is_dirty()(identifier)))) for(const auto &range : ranges) kill(identifier, range.first, range.second); diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 91466d3ed6c..1dcd025584c 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -743,11 +743,15 @@ void c_typecheck_baset::typecheck_declaration( typet ret_type=empty_typet(); if(new_symbol.type.id()==ID_code) ret_type=to_code_type(new_symbol.type).return_type(); - assert(parameter_map.empty()); if(ret_type.id()!=ID_empty) + { + DATA_INVARIANT( + parameter_map.empty(), "parameter map should be cleared"); parameter_map[CPROVER_PREFIX "return_value"] = ret_type; + } typecheck_spec_expr(contract, ID_C_spec_ensures); - parameter_map.clear(); + if(ret_type.id() != ID_empty) + parameter_map.clear(); if(contract.find(ID_C_spec_requires).is_not_nil()) new_symbol.type.add(ID_C_spec_requires)= diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b42818006aa..79ebce402ef 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -33,6 +33,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "anonymous_member.h" #include "padding.h" +bool is_lvalue(const exprt &expr); + void c_typecheck_baset::typecheck_expr(exprt &expr) { if(expr.id()==ID_already_typechecked) @@ -2128,6 +2130,58 @@ exprt c_typecheck_baset::do_special_functions( return same_object_expr; } + else if(identifier == CPROVER_PREFIX "points_to_valid_memory") + { + if(expr.arguments().size() != 2 && expr.arguments().size() != 1) + { + error().source_location = f_op.source_location(); + error() << "points_to_valid_memory expects one or two operands" << eom; + throw 0; + } + if(!is_lvalue(expr.arguments().front())) + { + error().source_location = f_op.source_location(); + error() << "ptr argument to points_to_valid_memory" + << " must be an lvalue" << eom; + throw 0; + } + + exprt same_object_expr; + if(expr.arguments().size() == 2) + { +// TODO: We should add some way to enforce that the second argument +// has a reasonable type (coercible to __CPROVER_size_t). +#if 0 + if(expr.arguments()[1].type() <[cannot be coerced to size_t]>) + { + err_location(f_op); + error() << "size argument to points_to_valid_memory" + << " must be coercible to size_t" << eom; + throw 0; + } +#endif + same_object_expr = + points_to_valid_memory(expr.arguments()[0], expr.arguments()[1]); + } + else if(expr.arguments().size() == 1) + { + PRECONDITION(expr.arguments()[0].type().id() == ID_pointer); + + const typet &base_type = expr.arguments()[0].type().subtype(); + exprt sizeof_expr = size_of_expr(base_type, *this); + sizeof_expr.add(ID_C_c_sizeof_type) = base_type; + + same_object_expr = + points_to_valid_memory(expr.arguments()[0], sizeof_expr); + } + else + { + UNREACHABLE; + } + same_object_expr.add_source_location() = source_location; + + return same_object_expr; + } else if(identifier==CPROVER_PREFIX "buffer_size") { if(expr.arguments().size()!=1) @@ -2184,7 +2238,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type()); + exprt dynamic_object_expr = exprt(ID_is_dynamic_object, expr.type()); dynamic_object_expr.operands()=expr.arguments(); dynamic_object_expr.add_source_location()=source_location; diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 14f282af610..a8fb4272163 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -6,6 +6,7 @@ void __CPROVER_havoc_object(void *); __CPROVER_bool __CPROVER_equal(); __CPROVER_bool __CPROVER_same_object(const void *, const void *); __CPROVER_bool __CPROVER_invalid_pointer(const void *); +__CPROVER_bool __CPROVER_points_to_valid_memory(const void *, ...); __CPROVER_bool __CPROVER_is_zero_string(const void *); __CPROVER_size_t __CPROVER_zero_string_length(const void *); __CPROVER_size_t __CPROVER_buffer_size(const void *); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 5b4ca270dd7..fba9dd763ba 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3474,6 +3474,9 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_good_pointer) return convert_function(src, "GOOD_POINTER", precedence=16); + else if(src.id() == ID_points_to_valid_memory) + return convert_function(src, "POINTS_TO_VALID_MEMORY", precedence = 16); + else if(src.id()==ID_object_size) return convert_function(src, "OBJECT_SIZE", precedence=16); @@ -3528,8 +3531,8 @@ std::string expr2ct::convert_with_precedence( return convert_function( src, CPROVER_PREFIX "invalid_pointer", precedence = 16); - else if(src.id()==ID_dynamic_object) - return convert_function(src, "DYNAMIC_OBJECT", precedence=16); + else if(src.id() == ID_is_dynamic_object) + return convert_function(src, "IS_DYNAMIC_OBJECT", precedence = 16); else if(src.id()=="is_zero_string") return convert_function(src, "IS_ZERO_STRING", precedence=16); diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index c2bb06a36d0..941c8fd35a6 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -32,6 +32,7 @@ SRC = accelerate/accelerate.cpp \ document_properties.cpp \ dot.cpp \ dump_c.cpp \ + expand_pointer_predicates.cpp \ full_slicer.cpp \ function.cpp \ function_modifies.cpp \ diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 98408f6accd..0b1af7d57a6 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -13,157 +13,116 @@ Date: February 2016 #include "code_contracts.h" +#include +#include +#include #include #include +#include #include #include -#include +#include #include +#include + #include "loop_utils.h" +enum class contract_opst +{ + APPLY, + CHECK +}; + class code_contractst { public: code_contractst( symbol_tablet &_symbol_table, - goto_functionst &_goto_functions): - ns(_symbol_table), + goto_functionst &_goto_functions) + : ns(_symbol_table), symbol_table(_symbol_table), - goto_functions(_goto_functions), - temporary_counter(0) + goto_functions(_goto_functions) { } - void operator()(); + void operator()(contract_opst op_type); protected: namespacet ns; symbol_tablet &symbol_table; goto_functionst &goto_functions; - unsigned temporary_counter; - - std::unordered_set summarized; + void apply_code_contracts(); + void check_code_contracts(); void code_contracts(goto_functionst::goto_functiont &goto_function); + /// Applies (but does not check) a function contract. This will assume that + /// the contract holds, and then use that assumption to remove the function + /// call located at target. + /// \param goto_program The goto program containing the target call site. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param target An iterator pointing to the function call to be removed. void apply_contract( goto_programt &goto_program, + value_setst &value_sets, goto_programt::targett target); - void add_contract_check( - const irep_idt &function, + /// Applies (but does not check) a loop invariant. This will assume that the + /// loop invariant is indeed an invariant, and then use that assumption to + /// remove the loop. + /// \param goto_function The goto function containing the target loop. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param loop_head An iterator pointing to the first instruction of the + /// target loop. + /// \param loop The loop being removed. + void apply_invariant( + goto_functionst::goto_functiont &goto_function, + value_setst &value_sets, + const goto_programt::targett loop_head, + const loopt &loop); + + /// Checks (but does not apply) a function contract. This will build a code + /// snippet to be inserted at dest which will check that the function contract + /// is satisfied. + /// \param function_id The id of the function being checked. + /// \param goto_function The goto_function object for the function + /// being checked. + /// \param dest An iterator pointing to the place to insert checking code. + void check_contract( + const irep_idt &function_id, + goto_functionst::goto_functiont &goto_function, goto_programt &dest); + /// Checks and applies a loop invariant This will replace the loop with a code + /// snippet (based on the loop) which will check that the loop invariant is + /// indeed an invariant, and then use that invariant in what follows. + /// \param goto_function The goto function containing the target loop. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param loop_head An iterator pointing to the first instruction of the + /// target loop. + /// \param loop The loop being removed. + void check_apply_invariant( + goto_functionst::goto_functiont &goto_function, + value_setst &value_sets, + const goto_programt::targett loop_head, + const loopt &loop); + const symbolt &new_tmp_symbol( const typet &type, const source_locationt &source_location); }; -static void check_apply_invariants( - goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, - const goto_programt::targett loop_head, - const loopt &loop) -{ - assert(!loop.empty()); - - // find the last back edge - goto_programt::targett loop_end=loop_head; - for(loopt::const_iterator - it=loop.begin(); - it!=loop.end(); - ++it) - if((*it)->is_goto() && - (*it)->get_target()==loop_head && - (*it)->location_number>loop_end->location_number) - loop_end=*it; - - // see whether we have an invariant - exprt invariant= - static_cast( - loop_end->guard.find(ID_C_spec_loop_invariant)); - if(invariant.is_nil()) - return; - - // change H: loop; E: ... - // to - // H: assert(invariant); - // havoc; - // assume(invariant); - // if(guard) goto E: - // loop; - // assert(invariant); - // assume(false); - // E: ... - - // find out what can get changed in the loop - modifiest modifies; - get_modifies(local_may_alias, loop, modifies); - - // build the havocking code - goto_programt havoc_code; - - // assert the invariant - { - goto_programt::targett a=havoc_code.add_instruction(ASSERT); - a->guard=invariant; - a->function=loop_head->function; - a->source_location=loop_head->source_location; - a->source_location.set_comment("Loop invariant violated before entry"); - } - - // havoc variables being written to - build_havoc_code(loop_head, modifies, havoc_code); - - // assume the invariant - { - goto_programt::targett assume=havoc_code.add_instruction(ASSUME); - assume->guard=invariant; - assume->function=loop_head->function; - assume->source_location=loop_head->source_location; - } - - // non-deterministically skip the loop if it is a do-while loop - if(!loop_head->is_goto()) - { - goto_programt::targett jump=havoc_code.add_instruction(GOTO); - jump->guard = - side_effect_expr_nondett(bool_typet(), loop_head->source_location); - jump->targets.push_back(loop_end); - jump->function=loop_head->function; - } - - // Now havoc at the loop head. Use insert_swap to - // preserve jumps to loop head. - goto_function.body.insert_before_swap(loop_head, havoc_code); - - // assert the invariant at the end of the loop body - { - goto_programt::instructiont a(ASSERT); - a.guard=invariant; - a.function=loop_end->function; - a.source_location=loop_end->source_location; - a.source_location.set_comment("Loop invariant not preserved"); - goto_function.body.insert_before_swap(loop_end, a); - ++loop_end; - } - - // change the back edge into assume(false) or assume(guard) - loop_end->targets.clear(); - loop_end->type=ASSUME; - if(loop_head->is_goto()) - loop_end->guard = false_exprt(); - else - loop_end->guard = boolean_negate(loop_end->guard); -} - void code_contractst::apply_contract( goto_programt &goto_program, + value_setst &value_sets, goto_programt::targett target) { const code_function_callt &call=to_code_function_call(target->code); @@ -176,14 +135,49 @@ void code_contractst::apply_contract( const symbolt &f_sym=ns.lookup(function); const code_typet &type=to_code_type(f_sym.type); - exprt requires= - static_cast(type.find(ID_C_spec_requires)); - exprt ensures= - static_cast(type.find(ID_C_spec_ensures)); + exprt requires = static_cast(type.find(ID_C_spec_requires)); + exprt ensures = static_cast(type.find(ID_C_spec_ensures)); - // is there a contract? if(ensures.is_nil()) - return; + { + // If there is no contract at all, we skip this function. + if(requires.is_nil()) + { + return; + } + else + { + // If there's no ensures but is a requires, treat it as ensures(true) + ensures = true_exprt(); + } + } + + // find out what can be written by the function + modifiest modifies; + + rw_range_set_value_sett rw_set(ns, value_sets); + goto_rw(goto_functions, function, rw_set); + forall_rw_range_set_w_objects(it, rw_set) + { + // Skip over local variables of the function being called, as well as + // variables not in the namespace (e.g. symex::invalid_object) + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + const std::string &name_string = id2string(symbol_ptr->name); + std::string scope_prefix(id2string(ns.lookup(function).name)); + scope_prefix += "::"; + + if(name_string.find(scope_prefix) == std::string::npos) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } + } + + // build the havocking code + goto_programt havoc_code; + build_havoc_code(target, modifies, havoc_code); // replace formal parameters by arguments, replace return replace_symbolt replace; @@ -212,6 +206,18 @@ void code_contractst::apply_contract( replace(requires); replace(ensures); + // Havoc the return value of the function call. + if(type.return_type() != empty_typet()) + { + const exprt &lhs = call.lhs(); + const exprt &rhs = side_effect_expr_nondett(call.lhs().type()); + target->make_assignment(code_assignt(lhs, rhs)); + } + else + { + target->make_skip(); + } + if(requires.is_not_nil()) { goto_programt::instructiont a(ASSERT); @@ -223,74 +229,145 @@ void code_contractst::apply_contract( ++target; } - target->make_assumption(ensures); + goto_program.destructive_insert(target, havoc_code); - summarized.insert(function); + { + goto_programt::targett a = goto_program.insert_after(target); + a->make_assumption(ensures); + a->function = target->function; + a->source_location = target->source_location; + } } -void code_contractst::code_contracts( - goto_functionst::goto_functiont &goto_function) +void code_contractst::apply_invariant( + goto_functionst::goto_functiont &goto_function, + value_setst &value_sets, + const goto_programt::targett loop_head, + const loopt &loop) { - local_may_aliast local_may_alias(goto_function); - natural_loops_mutablet natural_loops(goto_function.body); - - // iterate over the (natural) loops in the function - for(natural_loops_mutablet::loop_mapt::const_iterator - l_it=natural_loops.loop_map.begin(); - l_it!=natural_loops.loop_map.end(); - l_it++) - check_apply_invariants( - goto_function, - local_may_alias, - l_it->first, - l_it->second); - - // look at all function calls - Forall_goto_program_instructions(it, goto_function.body) - if(it->is_function_call()) - apply_contract(goto_function.body, it); -} + PRECONDITION(!loop.empty()); -const symbolt &code_contractst::new_tmp_symbol( - const typet &type, - const source_locationt &source_location) -{ - return get_fresh_aux_symbol( - type, - id2string(source_location.get_function()), - "tmp_cc", - source_location, - irep_idt(), - symbol_table); + // find the last back edge + goto_programt::targett loop_end = loop_head; + for(const goto_programt::targett &inst : loop) + { + if( + inst->is_goto() && inst->get_target() == loop_head && + inst->location_number > loop_end->location_number) + { + loop_end = inst; + } + } + + exprt invariant = + static_cast(loop_end->guard.find(ID_C_spec_loop_invariant)); + if(invariant.is_nil()) + { + return; + } + + // change H: loop; E: ... + // to + // H: assert(invariant); + // havoc; + // assume(invariant); + // assume(!guard); + // E: ... + + // find out what can get changed in the loop + modifiest modifies; + + rw_range_set_value_sett rw_set(ns, value_sets); + for(const goto_programt::targett &inst : loop) + { + goto_rw(inst, rw_set); + } + forall_rw_range_set_w_objects(it, rw_set) + { + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } + + // build the havocking code + goto_programt havoc_code; + + // assert the invariant + { + goto_programt::targett a = havoc_code.add_instruction(ASSERT); + a->guard = invariant; + a->function = loop_head->function; + a->source_location = loop_head->source_location; + a->source_location.set_comment("Loop invariant violated before entry"); + } + + // havoc variables that can be modified by the loop + build_havoc_code(loop_head, modifies, havoc_code); + + // assume the invariant + { + goto_programt::targett assume = havoc_code.add_instruction(ASSUME); + assume->guard = invariant; + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; + } + + // assume !guard + { + goto_programt::targett assume = havoc_code.add_instruction(ASSUME); + + if(loop_head->is_goto()) + assume->guard = loop_head->guard; + else + assume->guard = boolean_negate(loop_end->guard); + + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; + } + + // Clear out loop body + for(const goto_programt::targett &inst : loop) + { + inst->make_skip(); + } + + // Now havoc at the loop head. Use insert_before_swap to preserve jumps to + // loop head. + goto_function.body.insert_before_swap(loop_head, havoc_code); + + // Remove all the skips we created. + remove_skip(goto_function.body); } -void code_contractst::add_contract_check( - const irep_idt &function, +void code_contractst::check_contract( + const irep_idt &function_id, + goto_functionst::goto_functiont &goto_function, goto_programt &dest) { - assert(!dest.instructions.empty()); - - goto_functionst::function_mapt::iterator f_it= - goto_functions.function_map.find(function); - assert(f_it!=goto_functions.function_map.end()); + PRECONDITION(!dest.instructions.empty()); - const goto_functionst::goto_functiont &gf=f_it->second; + exprt requires = + static_cast(goto_function.type.find(ID_C_spec_requires)); + exprt ensures = + static_cast(goto_function.type.find(ID_C_spec_ensures)); - const exprt &requires= - static_cast(gf.type.find(ID_C_spec_requires)); - const exprt &ensures= - static_cast(gf.type.find(ID_C_spec_ensures)); - assert(ensures.is_not_nil()); + // Nothing to check if ensures is nil. + if(ensures.is_nil()) + { + return; + } - // build: - // if(nondet) + // We build the following checking code: + // if(nondet) goto end // decl ret // decl parameter1 ... // assume(requires) [optional] - // ret=function(parameter1, ...) + // ret = function(parameter1, ...) // assert(ensures) - // assume(false) - // skip: ... + // end: + // skip // build skip so that if(nondet) can refer to it goto_programt tmp_skip; @@ -302,57 +379,60 @@ void code_contractst::add_contract_check( // if(nondet) goto_programt::targett g=check.add_instruction(); - g->make_goto( - skip, side_effect_expr_nondett(bool_typet(), skip->source_location)); + g->make_goto(skip, side_effect_expr_nondett(bool_typet())); g->function=skip->function; g->source_location=skip->source_location; // prepare function call including all declarations - code_function_callt call(ns.lookup(function).symbol_expr()); + code_function_callt call; + call.function() = ns.lookup(function_id).symbol_expr(); replace_symbolt replace; // decl ret - if(gf.type.return_type()!=empty_typet()) + // TODO: Handle void functions + // void functions seem to be handled by goto-cc + if(goto_function.type.return_type() != empty_typet()) { goto_programt::targett d=check.add_instruction(DECL); d->function=skip->function; d->source_location=skip->source_location; - symbol_exprt r= - new_tmp_symbol(gf.type.return_type(), - d->source_location).symbol_expr(); + symbol_exprt r = + new_tmp_symbol(goto_function.type.return_type(), d->source_location) + .symbol_expr(); d->code=code_declt(r); call.lhs()=r; - symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); - replace.insert(ret_val, r); + symbol_exprt old( + "__CPROVER_return_value", goto_function.type.return_type()); + replace.insert(old, r); } // decl parameter1 ... - for(code_typet::parameterst::const_iterator - p_it=gf.type.parameters().begin(); - p_it!=gf.type.parameters().end(); - ++p_it) + for(const auto &p_it : goto_function.type.parameters()) { goto_programt::targett d=check.add_instruction(DECL); d->function=skip->function; d->source_location=skip->source_location; - symbol_exprt p= - new_tmp_symbol(p_it->type(), - d->source_location).symbol_expr(); + symbol_exprt p = + new_tmp_symbol(p_it.type(), d->source_location).symbol_expr(); d->code=code_declt(p); call.arguments().push_back(p); - if(!p_it->get_identifier().empty()) + if(!p_it.get_identifier().empty()) { - symbol_exprt cur_p(p_it->get_identifier(), p_it->type()); - replace.insert(cur_p, p); + symbol_exprt old(p_it.get_identifier(), p_it.type()); + replace.insert(old, p); } } + // rewrite any use of parameters + replace(requires); + replace(ensures); + // assume(requires) if(requires.is_not_nil()) { @@ -360,9 +440,6 @@ void code_contractst::add_contract_check( a->make_assumption(requires); a->function=skip->function; a->source_location=requires.source_location(); - - // rewrite any use of parameters - replace(a->guard); } // ret=function(parameter1, ...) @@ -377,39 +454,262 @@ void code_contractst::add_contract_check( a->function=skip->function; a->source_location=ensures.source_location(); - // rewrite any use of __CPROVER_return_value - replace(a->guard); - - // assume(false) - goto_programt::targett af=check.add_instruction(); - af->make_assumption(false_exprt()); - af->function=skip->function; - af->source_location=ensures.source_location(); - // prepend the new code to dest check.destructive_append(tmp_skip); dest.destructive_insert(dest.instructions.begin(), check); } -void code_contractst::operator()() +void code_contractst::check_apply_invariant( + goto_functionst::goto_functiont &goto_function, + value_setst &value_sets, + const goto_programt::targett loop_head, + const loopt &loop) { + PRECONDITION(!loop.empty()); + + // find the last back edge + goto_programt::targett loop_end = loop_head; + for(const goto_programt::targett &inst : loop) + if( + inst->is_goto() && inst->get_target() == loop_head && + inst->location_number > loop_end->location_number) + loop_end = inst; + + // see whether we have an invariant + exprt invariant = + static_cast(loop_end->guard.find(ID_C_spec_loop_invariant)); + if(invariant.is_nil()) + { + return; + } + + // change H: loop; E: ... + // to + // H: assert(invariant); + // havoc writes of loop; + // assume(invariant); + // loop (minus the ending goto); + // assert(invariant); + // assume(!guard) + // E: + // ... + + // find out what can get changed in the loop + modifiest modifies; + + rw_range_set_value_sett rw_set(ns, value_sets); + for(const goto_programt::targett &inst : loop) + { + goto_rw(inst, rw_set); + } + forall_rw_range_set_w_objects(it, rw_set) + { + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } + + // build the havocking code + goto_programt havoc_code; + + // assert the invariant + { + goto_programt::targett a = havoc_code.add_instruction(ASSERT); + a->guard = invariant; + a->function = loop_head->function; + a->source_location = loop_head->source_location; + a->source_location.set_comment("Loop invariant violated before entry"); + } + + // havoc variables that can be modified by the loop + build_havoc_code(loop_head, modifies, havoc_code); + + // assume the invariant + { + goto_programt::targett assume = havoc_code.add_instruction(ASSUME); + assume->guard = invariant; + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; + } + + // assert the invariant at the end of the loop body + { + goto_programt::instructiont a(ASSERT); + a.guard = invariant; + a.function = loop_end->function; + a.source_location = loop_end->source_location; + a.source_location.set_comment("Loop invariant not preserved"); + + goto_function.body.insert_before_swap(loop_end, a); + ++loop_end; + } + + // change the back edge into assume(!guard) + loop_end->targets.clear(); + loop_end->type = ASSUME; + if(loop_head->is_goto()) + { + loop_end->guard = loop_head->guard; + } + else + { + loop_end->guard = boolean_negate(loop_end->guard); + } + + // Now havoc at the loop head. Use insert_before_swap to preserve jumps to + // loop head. + goto_function.body.insert_before_swap(loop_head, havoc_code); +} + +const symbolt &code_contractst::new_tmp_symbol( + const typet &type, + const source_locationt &source_location) +{ + return get_fresh_aux_symbol( + type, + id2string(source_location.get_function()), + "tmp_cc", + source_location, + ID_C, + symbol_table); +} + +void code_contractst::apply_code_contracts() +{ + auto vs = util_make_unique(ns); + (*vs)(goto_functions); + std::unique_ptr value_sets = std::move(vs); + Forall_goto_functions(it, goto_functions) - code_contracts(it->second); + { + goto_functionst::goto_functiont &goto_function = it->second; + + natural_loops_mutablet natural_loops(goto_function.body); + + for(const auto &l_it : natural_loops.loop_map) + { + apply_invariant(goto_function, *value_sets, l_it.first, l_it.second); + } + + Forall_goto_program_instructions(it, goto_function.body) + { + if(it->is_function_call()) + { + apply_contract(goto_function.body, *value_sets, it); + } + } + } + + goto_functions.update(); +} + +void code_contractst::check_code_contracts() +{ + auto vs = util_make_unique(ns); + (*vs)(goto_functions); + std::unique_ptr value_sets = std::move(vs); goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); assert(i_it!=goto_functions.function_map.end()); + goto_programt &init_function = i_it->second.body; + + Forall_goto_functions(it, goto_functions) + { + goto_functionst::goto_functiont &goto_function = it->second; + + natural_loops_mutablet natural_loops(goto_function.body); + + for(const auto &l_it : natural_loops.loop_map) + { + check_apply_invariant( + goto_function, *value_sets, l_it.first, l_it.second); + } + + Forall_goto_program_instructions(it, goto_function.body) + { + if(it->is_function_call()) + { + apply_contract(goto_function.body, *value_sets, it); + } + } + } + + Forall_goto_functions(it, goto_functions) + { + check_contract(it->first, it->second, init_function); + } + + // Partially initialize state + goto_programt init_code; + + goto_programt::targett d = init_code.add_instruction(DECL); + d->function = i_it->first; + // TODO add source location + // d->source_location = + + symbol_exprt tmp_var = + new_tmp_symbol(void_typet(), d->source_location).symbol_expr(); + d->code = code_declt(tmp_var); + d->code.add_source_location() = d->source_location; + + { + const symbol_exprt &deallocated_expr = + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); + + goto_programt::targett a = init_code.add_instruction(ASSIGN); + a->function = i_it->first; + // TODO add source location + // a->source_location = + address_of_exprt rhs(tmp_var, to_pointer_type(deallocated_expr.type())); + a->code = code_assignt(deallocated_expr, rhs); + a->code.add_source_location() = a->source_location; + } + + { + const symbol_exprt &dead_expr = + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + + goto_programt::targett a = init_code.add_instruction(ASSIGN); + a->function = i_it->first; + // TODO add source location + // a->source_location = + address_of_exprt rhs(tmp_var, to_pointer_type(dead_expr.type())); + a->code = code_assignt(dead_expr, rhs); + a->code.add_source_location() = a->source_location; + } - for(const auto &contract : summarized) - add_contract_check(contract, i_it->second.body); + init_function.destructive_insert( + init_function.instructions.begin(), init_code); - // remove skips - remove_skip(i_it->second.body); + remove_skip(init_function); goto_functions.update(); } -void code_contracts(goto_modelt &goto_model) +void code_contractst::operator()(contract_opst op_type) +{ + switch(op_type) + { + case contract_opst::APPLY: + apply_code_contracts(); + break; + case contract_opst::CHECK: + check_code_contracts(); + break; + } +} + +void check_code_contracts(goto_modelt &goto_model) +{ + code_contractst(goto_model.symbol_table, goto_model.goto_functions)( + contract_opst::CHECK); +} + +void apply_code_contracts(goto_modelt &goto_model) { - code_contractst(goto_model.symbol_table, goto_model.goto_functions)(); + code_contractst(goto_model.symbol_table, goto_model.goto_functions)( + contract_opst::APPLY); } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index dc02902c142..87395007fff 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -16,6 +16,19 @@ Date: February 2016 class goto_modelt; -void code_contracts(goto_modelt &); +void apply_code_contracts(goto_modelt &); +void check_code_contracts(goto_modelt &); + +// clang-format off +#define HELP_APPLY_CODE_CONTRACTS \ + " --apply-code-contracts Assume (without checking) that the contracts used in code hold\n" \ + " This will use __CPROVER_requires, __CPROVER_ensures,\n" \ + " and __CPROVER_loop_invariant as assumptions in order to avoid\n" \ + " checking code that is assumed to satisfy a specification.\n" +#define HELP_CHECK_CODE_CONTRACTS \ + " --check-code-contracts Assume (with checking) that the contracts used in code hold.\n" \ + " This differs from --apply-code-contracts in that in addition to\n" \ + " assuming specifications, it checks that they are correct.\n" +// clang-format on #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H diff --git a/src/goto-instrument/expand_pointer_predicates.cpp b/src/goto-instrument/expand_pointer_predicates.cpp new file mode 100644 index 00000000000..248adc66260 --- /dev/null +++ b/src/goto-instrument/expand_pointer_predicates.cpp @@ -0,0 +1,215 @@ +/*******************************************************************\ + +Module: Expand pointer predicates in assertions/assumptions. + +Author: Klaas Pruiksma + +Date: June 2018 + +\*******************************************************************/ + +/// \file +/// Replace pointer predicates (e.g. __CPROVER_points_to_valid_memory) +/// in assumptions and assertions with suitable expressions and additional +/// instructions. + +#include "expand_pointer_predicates.h" + +#include + +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +class expand_pointer_predicatest +{ +public: + expand_pointer_predicatest( + symbol_tablet &_symbol_table, + goto_functionst &_goto_functions) + : ns(_symbol_table), + symbol_table(_symbol_table), + goto_functions(_goto_functions), + local_bitvector_analysis(nullptr) + { + } + + void operator()(); + +protected: + namespacet ns; + symbol_tablet &symbol_table; + goto_functionst &goto_functions; + local_bitvector_analysist *local_bitvector_analysis; + + void expand_pointer_predicates(); + + void expand_assumption( + goto_programt &program, + goto_programt::targett target, + exprt &assume_expr); + + void expand_assertion(exprt &assert_expr); + + const symbolt & + new_tmp_symbol(const typet &type, const source_locationt &source_location); +}; + +bool is_lvalue(const exprt &expr); + +void expand_pointer_predicatest::expand_pointer_predicates() +{ + Forall_goto_functions(f_it, goto_functions) + { + goto_functionst::goto_functiont &goto_function = f_it->second; + local_bitvector_analysist local_bitvector_analysis_obj(goto_function); + local_bitvector_analysis = &local_bitvector_analysis_obj; + Forall_goto_program_instructions(i_it, goto_function.body) + { + if(i_it->is_assert()) + { + expand_assertion(i_it->guard); + } + else if(i_it->is_assume()) + { + expand_assumption(goto_function.body, i_it, i_it->guard); + local_bitvector_analysis_obj = local_bitvector_analysist(goto_function); + local_bitvector_analysis = &local_bitvector_analysis_obj; + } + else + { + continue; + } + } + } +} + +void expand_pointer_predicatest::expand_assumption( + goto_programt &program, + goto_programt::targett target, + exprt &assume_expr) +{ + goto_programt assume_code; + for(depth_iteratort it = assume_expr.depth_begin(); + it != assume_expr.depth_end();) + { + if(it->id() == ID_points_to_valid_memory) + { + exprt &valid_memory_expr = it.mutate(); + exprt &pointer_expr = valid_memory_expr.op0(); + exprt size_expr = valid_memory_expr.op1(); + simplify(size_expr, ns); + + // This should be forced by typechecking. + INVARIANT( + pointer_expr.type().id() == ID_pointer && is_lvalue(pointer_expr), + "Invalid argument to valid_pointer."); + + local_bitvector_analysist::flagst flags = + local_bitvector_analysis->get(target, pointer_expr); + // Only create a new object if the pointer may be uninitialized. + if(flags.is_uninitialized() || flags.is_unknown()) + { + typet object_type = type_from_size(size_expr, ns); + + // Decl a new variable (which is therefore unconstrained) + goto_programt::targett d = assume_code.add_instruction(DECL); + d->function = target->function; + d->source_location = assume_expr.source_location(); + const symbol_exprt obj = + new_tmp_symbol(object_type, d->source_location).symbol_expr(); + d->code = code_declt(obj); + + exprt rhs; + if(object_type.id() == ID_array) + { + rhs = typecast_exprt( + address_of_exprt(index_exprt(obj, from_integer(0, index_type()))), + pointer_expr.type()); + } + else + { + rhs = address_of_exprt(obj); + } + + // Point the relevant pointer to the new object + goto_programt::targett a = assume_code.add_instruction(ASSIGN); + a->function = target->function; + a->source_location = assume_expr.source_location(); + a->code = code_assignt(pointer_expr, rhs); + a->code.add_source_location() = assume_expr.source_location(); + } + + // Because some uses of this occur before deallocated, dead, and malloc + // objects are initialized, we need to make some additional assumptions + // to clarify that our newly allocated object is not dead, deallocated, + // or outside the bounds of a malloc region. + + exprt check_expr = + points_to_valid_memory_def(pointer_expr, size_expr, ns); + valid_memory_expr.swap(check_expr); + it.next_sibling_or_parent(); + } + else + { + ++it; + } + } + + program.destructive_insert(target, assume_code); +} + +void expand_pointer_predicatest::expand_assertion(exprt &assert_expr) +{ + for(depth_iteratort it = assert_expr.depth_begin(); + it != assert_expr.depth_end();) + { + if(it->id() == ID_points_to_valid_memory) + { + // Build an expression that checks validity. + exprt &valid_memory_expr = it.mutate(); + exprt &pointer_expr = valid_memory_expr.op0(); + exprt &size_expr = valid_memory_expr.op1(); + + exprt check_expr = + points_to_valid_memory_def(pointer_expr, size_expr, ns); + valid_memory_expr.swap(check_expr); + it.next_sibling_or_parent(); + } + else + { + ++it; + } + } +} + +const symbolt &expand_pointer_predicatest::new_tmp_symbol( + const typet &type, + const source_locationt &source_location) +{ + return get_fresh_aux_symbol( + type, + id2string(source_location.get_function()), + "tmp_epp", + source_location, + ID_C, + symbol_table); +} + +void expand_pointer_predicatest::operator()() +{ + expand_pointer_predicates(); +} + +void expand_pointer_predicates(goto_modelt &goto_model) +{ + expand_pointer_predicatest( + goto_model.symbol_table, goto_model.goto_functions)(); +} diff --git a/src/goto-instrument/expand_pointer_predicates.h b/src/goto-instrument/expand_pointer_predicates.h new file mode 100644 index 00000000000..37d41d1023b --- /dev/null +++ b/src/goto-instrument/expand_pointer_predicates.h @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Expand pointer predicates in assertions/assumptions. + +Author: Klaas Pruiksma + +Date: June 2018 + +\*******************************************************************/ + +/// \file +/// Replace pointer predicates (e.g. __CPROVER_points_to_valid_memory) +/// in assumptions and assertions with suitable expressions and additional +/// instructions. + +#ifndef CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H +#define CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H + +class goto_modelt; + +void expand_pointer_predicates(goto_modelt &goto_model); + +#endif // CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index f4b29d43e02..989053e1862 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -76,6 +76,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "document_properties.h" #include "dot.h" #include "dump_c.h" +#include "expand_pointer_predicates.h" #include "full_slicer.h" #include "function.h" #include "havoc_loops.h" @@ -1072,11 +1073,22 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions.update(); } - // verify and set invariants and pre/post-condition pairs if(cmdline.isset("apply-code-contracts")) { status() << "Applying Code Contracts" << eom; - code_contracts(goto_model); + apply_code_contracts(goto_model); + } + + // verify and set invariants and pre/post-condition pairs + if(cmdline.isset("check-code-contracts")) + { + status() << "Checking Code Contracts" << eom; + check_code_contracts(goto_model); + } + + if(cmdline.isset("expand-pointer-predicates")) + { + expand_pointer_predicates(goto_model); } // replace function pointers, if explicitly requested @@ -1621,6 +1633,8 @@ void goto_instrument_parse_optionst::help() " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) " convert each call to an undefined function to assume(false)\n" + HELP_APPLY_CODE_CONTRACTS + HELP_CHECK_CODE_CONTRACTS HELP_REPLACE_FUNCTION_BODY "\n" "Loop transformations:\n" @@ -1669,6 +1683,7 @@ void goto_instrument_parse_optionst::help() " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) + " --expand-pointer-predicates Expands predicates about pointers (e.g. __CPROVER_points_to_valid_memory) into a form useable by CBMC\n" // NOLINT(*) HELP_REMOVE_CALLS_NO_BODY HELP_REMOVE_CONST_FUNCTION_POINTERS " --add-library add models of C library functions\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index a5179302446..bf27b38fcf6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -90,8 +90,9 @@ Author: Daniel Kroening, kroening@kroening.com "(interpreter)(show-reaching-definitions)" \ "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ - "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ - "(show-threaded)(list-calls-args)" \ + "(horn)(skip-loops):(apply-code-contracts)(check-code-contracts)" \ + "(expand-pointer-predicates)" \ + "(model-argc-argv):(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ OPT_AGGRESSIVE_SLICER \ diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index b9bdf010261..8b9f3f75913 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -21,27 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -inline static typet c_sizeof_type_rec(const exprt &expr) -{ - const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); - - if(!sizeof_type.is_nil()) - { - return static_cast(sizeof_type); - } - else if(expr.id()==ID_mult) - { - forall_operands(it, expr) - { - typet t=c_sizeof_type_rec(*it); - if(t.is_not_nil()) - return t; - } - } - - return nil_typet(); -} - void goto_symext::symex_allocate( statet &state, const exprt &lhs, @@ -69,62 +49,12 @@ void goto_symext::symex_allocate( } else { - exprt tmp_size=size; + exprt tmp_size = size; state.rename(tmp_size, ns); // to allow constant propagation - simplify(tmp_size, ns); - - // special treatment for sizeof(T)*x - { - typet tmp_type=c_sizeof_type_rec(tmp_size); - - if(tmp_type.is_not_nil()) - { - // Did the size get multiplied? - auto elem_size = pointer_offset_size(tmp_type, ns); - mp_integer alloc_size; - - if(!elem_size.has_value() || *elem_size==0) - { - } - else if(to_integer(tmp_size, alloc_size) && - tmp_size.id()==ID_mult && - tmp_size.operands().size()==2 && - (tmp_size.op0().is_constant() || - tmp_size.op1().is_constant())) - { - exprt s=tmp_size.op0(); - if(s.is_constant()) - { - s=tmp_size.op1(); - PRECONDITION(c_sizeof_type_rec(tmp_size.op0()) == tmp_type); - } - else - PRECONDITION(c_sizeof_type_rec(tmp_size.op1()) == tmp_type); - - object_type=array_typet(tmp_type, s); - } - else - { - if(alloc_size == *elem_size) - object_type=tmp_type; - else - { - mp_integer elements = alloc_size / (*elem_size); - - if(elements * (*elem_size) == alloc_size) - object_type=array_typet( - tmp_type, from_integer(elements, tmp_size.type())); - } - } - } - } - - if(object_type.is_nil()) - object_type=array_typet(unsigned_char_type(), tmp_size); + object_type = type_from_size(tmp_size, ns); // we introduce a fresh symbol for the size // to prevent any issues of the size getting ever changed - if(object_type.id()==ID_array && !to_array_type(object_type).size().is_constant()) { diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 7eb546f92aa..a658479f818 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -316,8 +316,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // this is also our guard result.pointer_guard = dynamic_object(pointer_expr); - // can't remove here, turn into *p - result.value=dereference_exprt(pointer_expr, dereference_type); + // TODO should this be object or root_object? + // TODO It's unclear whether this is a good approach to take --- it + // successfully ensures that every (non-null) dereference points to + // something, making the write set computation work correctly, but dynamic + // objects do not seem to be intended to be used in this way. + result.value = object; } else if(root_object.id()==ID_integer_address) { diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index b6cd92369d9..c52f06caadf 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -45,21 +45,21 @@ literalt bv_pointerst::convert_rest(const exprt &expr) } } } - else if(expr.id()==ID_dynamic_object) + else if(expr.id() == ID_is_dynamic_object) { - if(operands.size()==1 && - operands[0].type().id()==ID_pointer) - { - // we postpone - literalt l=prop.new_variable(); + DATA_INVARIANT( + operands.size() == 1 && operands[0].type().id() == ID_pointer, + std::string("is_dynamic_object_exprt should have one") + + "operand, which should have pointer type."); + // we postpone + literalt l = prop.new_variable(); - postponed_list.push_back(postponedt()); - postponed_list.back().op=convert_bv(operands[0]); - postponed_list.back().bv.push_back(l); - postponed_list.back().expr=expr; + postponed_list.push_back(postponedt()); + postponed_list.back().op = convert_bv(operands[0]); + postponed_list.back().bv.push_back(l); + postponed_list.back().expr = expr; - return l; - } + return l; } else if(expr.id()==ID_lt || expr.id()==ID_le || expr.id()==ID_gt || expr.id()==ID_ge) @@ -736,7 +736,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv) void bv_pointerst::do_postponed( const postponedt &postponed) { - if(postponed.expr.id()==ID_dynamic_object) + if(postponed.expr.id() == ID_is_dynamic_object) { const pointer_logict::objectst &objects= pointer_logic.objects; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 5966fb87fd3..f3cbbf67c72 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1399,7 +1399,7 @@ void smt2_convt::convert_expr(const exprt &expr) if(ext>0) out << ")"; // zero_extend } - else if(expr.id()==ID_dynamic_object) + else if(expr.id() == ID_is_dynamic_object) { convert_is_dynamic_object(expr); } diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index b94d1ae2e8a..22897defbbe 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -8,17 +8,101 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_util.h" -#include -#include - +#include "arith_tools.h" +#include "c_types.h" #include "expr.h" #include "expr_iterator.h" #include "fixedbv.h" #include "ieee_float.h" +#include "namespace.h" +#include "pointer_offset_size.h" +#include "simplify_expr.h" #include "std_expr.h" #include "symbol.h" -#include "namespace.h" -#include "arith_tools.h" +#include +#include + +inline static typet c_sizeof_type_rec(const exprt &expr) +{ + const irept &sizeof_type = expr.find(ID_C_c_sizeof_type); + + if(!sizeof_type.is_nil()) + { + return static_cast(sizeof_type); + } + else if(expr.id() == ID_mult) + { + forall_operands(it, expr) + { + typet t = c_sizeof_type_rec(*it); + if(t.is_not_nil()) + return t; + } + } + + return nil_typet(); +} + +typet type_from_size(const exprt &size, const namespacet &ns) +{ + exprt tmp_size = size; + simplify(tmp_size, ns); + typet tmp_type = c_sizeof_type_rec(tmp_size); + + // Default to char[size] if nothing better can be found. + typet result_type = array_typet(unsigned_char_type(), tmp_size); + + if(tmp_type.is_not_nil()) + { + // Did the size get multiplied? + optionalt elem_size = pointer_offset_size(tmp_type, ns); + mp_integer alloc_size; + + if(!elem_size || *elem_size < 0) + { + // If this occurs, then either tmp_type contains some type with invalid + // ID or tmp_type contains a bitvector of negative size. Neither of these + // should ever happen, and if one does, it suggests a failure in CBMC + // rather than a failure on the part of the user. + UNREACHABLE; + } + // Case for constant size (in case it is a multiple of the element size) + else if(!to_integer(tmp_size, alloc_size)) + { + if(alloc_size == *elem_size) + { + result_type = tmp_type; + } + else if((alloc_size / *elem_size) * (*elem_size) == alloc_size) + { + // Allocation size is a multiple of the element size + result_type = array_typet( + tmp_type, from_integer(alloc_size / *elem_size, tmp_size.type())); + } + } + // Special case for constant * sizeof + else if( + tmp_size.id() == ID_mult && tmp_size.operands().size() == 2 && + (tmp_size.op0().is_constant() || tmp_size.op1().is_constant())) + { + exprt s = tmp_size.op0(); + if(s.is_constant()) + { + s = tmp_size.op1(); + PRECONDITION(c_sizeof_type_rec(tmp_size.op0()) == tmp_type); + } + else + { + PRECONDITION(c_sizeof_type_rec(tmp_size.op1()) == tmp_type); + } + + result_type = array_typet(tmp_type, s); + } + } + + POSTCONDITION(result_type.is_not_nil()); + return result_type; +} bool is_lvalue(const exprt &expr) { @@ -33,6 +117,7 @@ bool is_lvalue(const exprt &expr) else return false; } + exprt make_binary(const exprt &expr) { const exprt::operandst &operands=expr.operands(); diff --git a/src/util/expr_util.h b/src/util/expr_util.h index bc0b5099071..122ca212029 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -30,6 +30,18 @@ class symbolt; class typet; class namespacet; +/// Creates a type with size (in bytes) equal to the size argument. +/// Makes use of sizeof() in the argument to avoid unnecessary use of byte +/// arrays. +/// \param size: An expression describing the size (in bytes) of the desired +/// type. +/// \param ns : A namespace for symbol type lookups. +/// \return A type with size given by the argument \a size. +/// If \a size is of the form n*sizeof(T) (or sizeof(T)*n), then this +/// type will be T[n]. If \a size is of the form sizeof(T), then this +/// type will be T. Otherwise, the type will be unsigned char[size]. +typet type_from_size(const exprt &size, const namespacet &ns); + /// Returns true iff the argument is (syntactically) an lvalue. bool is_lvalue(const exprt &expr); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index b6fd76a8855..10082ccaa63 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -219,6 +219,7 @@ IREP_ID_TWO(C_invalid_object, #invalid_object) IREP_ID_ONE(pointer_offset) IREP_ID_ONE(pointer_object) IREP_ID_TWO(invalid_pointer, invalid-pointer) +IREP_ID_ONE(points_to_valid_memory) IREP_ID_ONE(ieee_float_equal) IREP_ID_ONE(ieee_float_notequal) IREP_ID_ONE(isnan) @@ -448,6 +449,7 @@ IREP_ID_TWO(overflow_minus, overflow--) IREP_ID_TWO(overflow_mult, overflow-*) IREP_ID_TWO(overflow_unary_minus, overflow-unary-) IREP_ID_ONE(object_descriptor) +IREP_ID_ONE(is_dynamic_object) IREP_ID_ONE(dynamic_object) IREP_ID_TWO(C_dynamic, #dynamic) IREP_ID_ONE(object_size) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 93fb6f45c34..e08ded41a97 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "cprover_prefix.h" #include "namespace.h" #include "pointer_offset_size.h" +#include "simplify_expr.h" #include "std_expr.h" #include "symbol.h" @@ -70,7 +71,7 @@ exprt dynamic_size(const namespacet &ns) exprt dynamic_object(const exprt &pointer) { - exprt dynamic_expr(ID_dynamic_object, bool_typet()); + exprt dynamic_expr(ID_is_dynamic_object, bool_typet()); dynamic_expr.copy_to_operands(pointer); return dynamic_expr; } @@ -143,6 +144,47 @@ exprt invalid_pointer(const exprt &pointer) return unary_exprt(ID_invalid_pointer, pointer, bool_typet()); } +exprt points_to_valid_memory(const exprt &pointer, const exprt &size) +{ + return binary_exprt(pointer, ID_points_to_valid_memory, size, bool_typet()); +} + +exprt points_to_valid_memory_def( + const exprt &pointer, + const exprt &size, + const namespacet &ns) +{ + const not_exprt not_null(null_pointer(pointer)); + + const not_exprt not_deallocated(deallocated(pointer, ns)); + + const not_exprt not_dead(dead_object(pointer, ns)); + + const not_exprt not_invalid(invalid_pointer(pointer)); + + const or_exprt malloc_in_bounds( + not_exprt(malloc_object(pointer, ns)), + and_exprt( + not_exprt(dynamic_object_lower_bound(pointer, ns, nil_exprt())), + not_exprt(dynamic_object_upper_bound(pointer, ns, size)))); + + const or_exprt dynamic_in_bounds( + dynamic_object(pointer), + and_exprt( + not_exprt(object_lower_bound(pointer, ns, nil_exprt())), + not_exprt(object_upper_bound(pointer, ns, size)))); + + exprt check_expr = conjunction( + {not_null, + not_deallocated, + not_dead, + not_invalid, + malloc_in_bounds, + dynamic_in_bounds}); + + return simplify_expr(check_expr, ns); +} + exprt dynamic_object_lower_bound( const exprt &pointer, const namespacet &ns, diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index f83588df8fe..dfdfb63afe6 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -31,6 +31,11 @@ exprt null_object(const exprt &pointer); exprt null_pointer(const exprt &pointer); exprt integer_address(const exprt &pointer); exprt invalid_pointer(const exprt &pointer); +exprt points_to_valid_memory(const exprt &pointer, const exprt &size); +exprt points_to_valid_memory_def( + const exprt &pointer, + const exprt &size, + const namespacet &); exprt dynamic_object_lower_bound( const exprt &pointer, const namespacet &, diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 74a3cab7c93..97caf577944 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2152,8 +2152,8 @@ bool simplify_exprt::simplify_node(exprt &expr) result=simplify_byte_extract(to_byte_extract_expr(expr)) && result; else if(expr.id()==ID_pointer_object) result=simplify_pointer_object(expr) && result; - else if(expr.id()==ID_dynamic_object) - result=simplify_dynamic_object(expr) && result; + else if(expr.id() == ID_is_dynamic_object) + result = simplify_is_dynamic_object(expr) && result; else if(expr.id()==ID_invalid_pointer) result=simplify_invalid_pointer(expr) && result; else if(expr.id()==ID_object_size) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 5e192292666..3dd7d8601e1 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -96,7 +96,7 @@ class simplify_exprt bool simplify_pointer_object(exprt &expr); bool simplify_object_size(exprt &expr); bool simplify_dynamic_size(exprt &expr); - bool simplify_dynamic_object(exprt &expr); + bool simplify_is_dynamic_object(exprt &expr); bool simplify_invalid_pointer(exprt &expr); bool simplify_same_object(exprt &expr); bool simplify_good_pointer(exprt &expr); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index e45bf34891e..837dc31edb5 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1707,11 +1707,12 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) if(expr.op0().id()==ID_address_of && expr.op0().operands().size()==1) { - if(expr.op0().op0().id()==ID_symbol || - expr.op0().op0().id()==ID_dynamic_object || - expr.op0().op0().id()==ID_member || - expr.op0().op0().id()==ID_index || - expr.op0().op0().id()==ID_string_constant) + if( + expr.op0().op0().id() == ID_symbol || + expr.op0().op0().id() == ID_is_dynamic_object || + expr.op0().op0().id() == ID_member || + expr.op0().op0().id() == ID_index || + expr.op0().op0().id() == ID_string_constant) { expr=false_exprt(); return false; @@ -1723,11 +1724,12 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) expr.op0().op0().id()==ID_address_of && expr.op0().op0().operands().size()==1) { - if(expr.op0().op0().op0().id()==ID_symbol || - expr.op0().op0().op0().id()==ID_dynamic_object || - expr.op0().op0().op0().id()==ID_member || - expr.op0().op0().op0().id()==ID_index || - expr.op0().op0().op0().id()==ID_string_constant) + if( + expr.op0().op0().op0().id() == ID_symbol || + expr.op0().op0().op0().id() == ID_is_dynamic_object || + expr.op0().op0().op0().id() == ID_member || + expr.op0().op0().op0().id() == ID_index || + expr.op0().op0().op0().id() == ID_string_constant) { expr=false_exprt(); return false; diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index a5025f09b9b..97b77096b99 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -467,10 +467,10 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) if(op.id()==ID_address_of) { - if(op.operands().size()!=1 || - (op.op0().id()!=ID_symbol && - op.op0().id()!=ID_dynamic_object && - op.op0().id()!=ID_string_constant)) + if( + op.operands().size() != 1 || + (op.op0().id() != ID_symbol && op.op0().id() != ID_is_dynamic_object && + op.op0().id() != ID_string_constant)) return true; } else if(op.id()!=ID_constant || @@ -513,18 +513,20 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr) return result; } -bool simplify_exprt::simplify_dynamic_object(exprt &expr) +bool simplify_exprt::simplify_is_dynamic_object(exprt &expr) { - if(expr.operands().size()!=1) - return true; + DATA_INVARIANT( + expr.operands().size() == 1 && expr.op0().type().id() == ID_pointer, + std::string("is_dynamic_object_exprt should have one") + + "operand, which should have pointer type."); exprt &op=expr.op0(); if(op.id()==ID_if && op.operands().size()==3) { if_exprt if_expr=lift_if(expr, 0); - simplify_dynamic_object(if_expr.true_case()); - simplify_dynamic_object(if_expr.false_case()); + simplify_is_dynamic_object(if_expr.true_case()); + simplify_is_dynamic_object(if_expr.false_case()); simplify_if(if_expr); expr.swap(if_expr); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 525ffab6b5a..6e42cd98104 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2271,8 +2271,53 @@ inline void validate_expr(const dynamic_object_exprt &value) validate_operands(value, 2, "Dynamic object must have two operands"); } +/*! \brief Evaluates to true if the operand is a pointer to a dynamic object. +*/ +class is_dynamic_object_exprt : public unary_predicate_exprt +{ +public: + is_dynamic_object_exprt() : unary_predicate_exprt(ID_is_dynamic_object) + { + } + + explicit is_dynamic_object_exprt(const exprt &op) + : unary_predicate_exprt(ID_is_dynamic_object, op) + { + } +}; + +/*! \brief Cast a generic exprt to a \ref is_dynamic_object_exprt + * + * This is an unchecked conversion. \a expr must be known to be \ref + * is_dynamic_object_exprt. + * + * \param expr Source expression + * \return Object of type \ref is_dynamic_object_exprt + * + * \ingroup gr_std_expr +*/ +inline const is_dynamic_object_exprt & +to_is_dynamic_object_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_is_dynamic_object); + DATA_INVARIANT( + expr.operands().size() == 1, "is_dynamic_object must have one operand"); + return static_cast(expr); +} + +/*! \copydoc to_is_dynamic_object_expr(const exprt &) + * \ingroup gr_std_expr +*/ +inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_is_dynamic_object); + DATA_INVARIANT( + expr.operands().size() == 1, "is_dynamic_object must have one operand"); + return static_cast(expr); +} -/// \brief Semantic type conversion +/*! \brief semantic type conversion +*/ class typecast_exprt:public unary_exprt { public: