From 407914b652a0378fdff83f41f4631a1ee2ed73b2 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 19 May 2023 22:24:23 -0500 Subject: [PATCH] CONTRACTS: dfcc_is_cprover_symbol now uses allow lists The result of `dfcc_is_cprover_symbol` is used to skip frame conditon checks on symbols with special meaning. Before we were matching symbols based on their prefix, which would allow users to skip frame condition checks just by naming their symbols with these prefixes. We now use a closed allow list, and distinguish function symbolds form static var symbols. We add test that show that variables named with __CPROVER, __VERIFIER or nondet prefixes do not bypass frame condition checks. --- .../main.c | 23 +++ .../test.desc | 13 ++ .../main.c | 23 +++ .../test.desc | 14 ++ .../dynamic-frames/dfcc_cfg_info.cpp | 2 +- .../dynamic-frames/dfcc_instrument.cpp | 2 +- .../dynamic-frames/dfcc_is_cprover_symbol.cpp | 138 +++++++++++++++++- .../dynamic-frames/dfcc_is_cprover_symbol.h | 11 +- 8 files changed, 218 insertions(+), 8 deletions(-) create mode 100644 regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c create mode 100644 regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.desc create mode 100644 regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c create mode 100644 regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.desc diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c new file mode 100644 index 00000000000..2208c1b74c6 --- /dev/null +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c @@ -0,0 +1,23 @@ +void foo() +{ + int nondet_var; + int __VERIFIER_var; + int __CPROVER_var; + for(int i = 10; i > 0; i--) + // clang-format off + __CPROVER_assigns(i) + __CPROVER_loop_invariant(0 <= i && i <= 10) + __CPROVER_decreases(i) + // clang-format on + { + nondet_var = 0; + __VERIFIER_var = 0; + __CPROVER_var = 0; + } +} + +int main() +{ + foo(); + return 0; +} diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.desc b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.desc new file mode 100644 index 00000000000..ba74b6d3387 --- /dev/null +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--dfcc main --apply-loop-contracts +^\[foo.assigns.\d+\] line \d+ Check that nondet_var is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that __VERIFIER_var is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_var is assignable: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that program variables with special name prefixes +__CPROVER_, __VERIFIER, or nondet do not escape assigns clause checking. diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c new file mode 100644 index 00000000000..fa1b4a5b622 --- /dev/null +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c @@ -0,0 +1,23 @@ +void foo() +{ + int nondet_var; + int __VERIFIER_var; + int __CPROVER_var; + for(int i = 10; i > 0; i--) + // clang-format off + __CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var) + __CPROVER_loop_invariant(0 <= i && i <= 10) + __CPROVER_decreases(i) + // clang-format on + { + nondet_var = 0; + __VERIFIER_var = 0; + __CPROVER_var = 0; + } +} + +int main() +{ + foo(); + return 0; +} diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.desc b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.desc new file mode 100644 index 00000000000..214fb2a0aa1 --- /dev/null +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--dfcc main --apply-loop-contracts +^\[foo.assigns.\d+\] line \d+ Check that nondet_var is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that __VERIFIER_var is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_var is assignable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that when program variables names have special prefixes +__CPROVER_, __VERIFIER, or nondet, adding them to the write set makes them +assignable. diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 67857f71548..8e963d1c83d 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -794,7 +794,7 @@ static bool must_check_lhs_from_local_and_tracked( return true; } const auto &id = to_symbol_expr(expr).get_identifier(); - if(dfcc_is_cprover_symbol(id)) + if(dfcc_is_cprover_static_symbol(id)) { // Skip the check if we have a single cprover symbol as root object // cprover symbols are used for generic checks instrumentation and are diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index fe3bc6b1a19..44f13d014b4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -235,7 +235,7 @@ bool dfcc_instrumentt::is_internal_symbol(const irep_idt &id) const bool dfcc_instrumentt::do_not_instrument(const irep_idt &id) const { return !has_prefix(id2string(id), CPROVER_PREFIX "file_local") && - (dfcc_is_cprover_symbol(id) || is_internal_symbol(id)); + (dfcc_is_cprover_function_symbol(id) || is_internal_symbol(id)); } void dfcc_instrumentt::instrument_harness_function( diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp index 210aec5746c..24bce179189 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp @@ -14,9 +14,141 @@ Date: March 2023 #include #include -bool dfcc_is_cprover_symbol(const irep_idt &id) +#include + +static void +init_function_symbols(std::unordered_set &function_symbols) +{ + // the set of all CPROVER symbols that we know of + if(function_symbols.empty()) + { + function_symbols.insert(CPROVER_PREFIX "_start"); + function_symbols.insert(CPROVER_PREFIX "array_copy"); + function_symbols.insert(CPROVER_PREFIX "array_replace"); + function_symbols.insert(CPROVER_PREFIX "array_set"); + function_symbols.insert(CPROVER_PREFIX "assert"); + function_symbols.insert(CPROVER_PREFIX "assignable"); + function_symbols.insert(CPROVER_PREFIX "assume"); + function_symbols.insert(CPROVER_PREFIX "contracts_car_create"); + function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains"); + function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create"); + function_symbols.insert(CPROVER_PREFIX "contracts_car_set_insert"); + function_symbols.insert(CPROVER_PREFIX "contracts_car_set_remove"); + function_symbols.insert( + CPROVER_PREFIX "contracts_check_replace_ensures_was_freed_preconditions"); + function_symbols.insert(CPROVER_PREFIX "contracts_free"); + function_symbols.insert(CPROVER_PREFIX "contracts_is_freeable"); + function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh"); + function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated"); + function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated"); + function_symbols.insert(CPROVER_PREFIX "contracts_link_is_fresh"); + function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract"); + function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add"); + function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append"); + function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains_exact"); + function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains"); + function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_create_append"); + function_symbols.insert(CPROVER_PREFIX + "contracts_obj_set_create_indexed_by_object_id"); + function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release"); + function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove"); + function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc"); + function_symbols.insert(CPROVER_PREFIX "contracts_was_freed"); + function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_allocated"); + function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_decl"); + function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_freeable"); + function_symbols.insert( + CPROVER_PREFIX + "contracts_write_set_check_allocated_deallocated_is_empty"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_check_array_copy"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_check_array_replace"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_check_array_set"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_check_assignment"); + function_symbols.insert( + CPROVER_PREFIX "contracts_write_set_check_assigns_clause_inclusion"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_check_deallocate"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_check_frees_clause_inclusion"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_check_havoc_object"); + function_symbols.insert(CPROVER_PREFIX "contracts_write_set_create"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_deallocate_freeable"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_havoc_get_assignable_target"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_havoc_object_whole"); + function_symbols.insert(CPROVER_PREFIX "contracts_write_set_havoc_slice"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_insert_assignable"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_insert_object_from"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_insert_object_upto"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_insert_object_whole"); + function_symbols.insert(CPROVER_PREFIX "contracts_write_set_record_dead"); + function_symbols.insert(CPROVER_PREFIX + "contracts_write_set_record_deallocated"); + function_symbols.insert(CPROVER_PREFIX "contracts_write_set_release"); + function_symbols.insert(CPROVER_PREFIX "deallocate"); + function_symbols.insert(CPROVER_PREFIX "freeable"); + function_symbols.insert(CPROVER_PREFIX "havoc_object"); + function_symbols.insert(CPROVER_PREFIX "havoc_slice"); + function_symbols.insert(CPROVER_PREFIX "initialize"); + function_symbols.insert(CPROVER_PREFIX "is_freeable"); + function_symbols.insert(CPROVER_PREFIX "is_fresh"); + function_symbols.insert(CPROVER_PREFIX "obeys_contract"); + function_symbols.insert(CPROVER_PREFIX "object_from"); + function_symbols.insert(CPROVER_PREFIX "object_upto"); + function_symbols.insert(CPROVER_PREFIX "object_whole"); + function_symbols.insert(CPROVER_PREFIX "pointer_in_range_dfcc"); + function_symbols.insert(CPROVER_PREFIX "precondition"); + function_symbols.insert(CPROVER_PREFIX "printf"); + function_symbols.insert(CPROVER_PREFIX "was_freed"); + } +} + +static void init_static_symbols(std::unordered_set &static_symbols) +{ + if(static_symbols.empty()) + { + static_symbols.insert(CPROVER_PREFIX "dead_object"); + static_symbols.insert(CPROVER_PREFIX "deallocated"); + static_symbols.insert(CPROVER_PREFIX "fpu_control_word"); + static_symbols.insert(CPROVER_PREFIX "jsa_jump_buffer"); + static_symbols.insert(CPROVER_PREFIX "malloc_failure_mode_return_null"); + static_symbols.insert(CPROVER_PREFIX + "malloc_failure_mode_assert_then_assume"); + static_symbols.insert(CPROVER_PREFIX "malloc_is_new_array"); + static_symbols.insert(CPROVER_PREFIX "max_malloc_size"); + static_symbols.insert(CPROVER_PREFIX "memory_leak"); + static_symbols.insert(CPROVER_PREFIX "pipe_offset"); + static_symbols.insert(CPROVER_PREFIX "pipes"); + static_symbols.insert(CPROVER_PREFIX "rounding_mode"); + } +} + +bool dfcc_is_cprover_function_symbol(const irep_idt &id) { + std::unordered_set function_symbols; + init_function_symbols(function_symbols); std::string str = id2string(id); - return has_prefix(str, CPROVER_PREFIX) || has_prefix(str, "__VERIFIER") || - has_prefix(str, "nondet") || has_suffix(str, "$object"); + return function_symbols.find(id) != function_symbols.end() || + // nondet functions + has_prefix(str, "__VERIFIER") || has_prefix(str, "nondet"); +} + +bool dfcc_is_cprover_static_symbol(const irep_idt &id) +{ + std::unordered_set static_symbols; + init_static_symbols(static_symbols); + return static_symbols.find(id) != static_symbols.end() || + // auto objects from pointer derefs + has_suffix(id2string(id), "$object"); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h index 9b3d3699002..ce2b3eeb37a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h @@ -15,8 +15,13 @@ Date: March 2023 #include -/// \return True iff the id starts with CPROVER_PREFIX, `__VERIFIER`, `nondet` -/// or ends with `$object`. -bool dfcc_is_cprover_symbol(const irep_idt &id); +/// Returns `true` iff id is one of the known CPROVER functions or starts with +/// `__VERIFIER` or `nondet`. +bool dfcc_is_cprover_function_symbol(const irep_idt &id); + +/// Returns `true` iff the symbol is one of the known CPROVER static +/// instrumentation variables or ends with `$object` and represents an +/// auto-generated object following a pointer dereference. +bool dfcc_is_cprover_static_symbol(const irep_idt &id); #endif