From deceb8236513398b6822d348e5cb608ecc520692 Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Mon, 11 Oct 2021 08:09:42 +0200 Subject: [PATCH 01/14] Update CBMC prerequisites --- lib/cbmc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/cbmc b/lib/cbmc index 1ecfc488..ddf6447b 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit 1ecfc4889b92942e8fb7158b105efd5aede0f363 +Subproject commit ddf6447b6e1e14e3ed9a564682d174d1a9aa5926 From 63188110008c2f30e4a6f495a8b86bf074256a83 Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Fri, 8 Oct 2021 07:43:16 +0200 Subject: [PATCH 02/14] Fix dynobj_instance_analysis The merge function needs to set has_values to unknown, otherwise the analysis fails to run. --- src/ssa/dynobj_instance_analysis.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ssa/dynobj_instance_analysis.cpp b/src/ssa/dynobj_instance_analysis.cpp index ca92b533..f0e9cae2 100644 --- a/src/ssa/dynobj_instance_analysis.cpp +++ b/src/ssa/dynobj_instance_analysis.cpp @@ -213,6 +213,7 @@ bool dynobj_instance_domaint::merge( trace_ptrt trace_to) { bool result=has_values.is_false() && !other.has_values.is_false(); + has_values=tvt::unknown(); for(auto &obj : other.must_alias_relations) { if(must_alias_relations.find(obj.first)==must_alias_relations.end()) From eff6f0fc01cc22338472fa8363f730dd35b50ec8 Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Fri, 8 Oct 2021 07:52:24 +0200 Subject: [PATCH 03/14] Workaround problem with GOTO targets If a single SKIP instruction is a target of both a forward and a backward GOTO, a malformed SSA is generated. This commit introduces a workaround that splits such GOTOs into two and redirects all backwards GOTOs to the second SKIP. This changes an SSA index in one test. --- .../precond_contextsensitive1/test.desc | 2 +- src/2ls/2ls_parse_options.cpp | 6 +++ src/2ls/2ls_parse_options.h | 1 + src/2ls/preprocessing_util.cpp | 48 +++++++++++++++++++ 4 files changed, 56 insertions(+), 1 deletion(-) diff --git a/regression/preconditions/precond_contextsensitive1/test.desc b/regression/preconditions/precond_contextsensitive1/test.desc index b7e6db72..ccfbfba6 100644 --- a/regression/preconditions/precond_contextsensitive1/test.desc +++ b/regression/preconditions/precond_contextsensitive1/test.desc @@ -3,4 +3,4 @@ main.c --context-sensitive --preconditions ^EXIT=5$ ^SIGNAL=0$ -^\[sign\]: sign#return_value#phi20 <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)sign#return_value#phi20\) <= 0 ==> x <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= 0$ +^\[sign\]: sign#return_value#phi21 <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)sign#return_value#phi21\) <= 0 ==> x <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= 0$ diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index be3e30fe..326237eb 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -1141,6 +1141,12 @@ bool twols_parse_optionst::process_goto_program( remove_dead_goto(goto_model); + // There's a bug in SSA creation that causes problems when a single SKIP + // instruction is a target of both a forward and a backward GOTO. + // This transformation fixes that by splitting such SKIPs into two. + // TODO: fix this properly in SSA, if possible. + fix_goto_targets(goto_model); + if(cmdline.isset("competition-mode")) { limit_array_bounds(goto_model); diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index c1d60ec2..1fbd95dd 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -197,6 +197,7 @@ class twols_parse_optionst: void handle_freed_ptr_compare(goto_modelt &goto_model); void assert_no_builtin_functions(goto_modelt &goto_model); void assert_no_atexit(goto_modelt &goto_model); + void fix_goto_targets(goto_modelt &goto_model); }; #endif diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index a281a710..062207c2 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -856,3 +856,51 @@ void twols_parse_optionst::assert_no_atexit(goto_modelt &goto_model) } } } + +/// Searches for SKIP instructions that are a target of both a forward and +/// a backward GOTO. Such instructions are split into 2 - the first one is +/// made the target of forward GOTOs and the second one is made the target of +/// backward GOTOs. +void twols_parse_optionst::fix_goto_targets(goto_modelt &goto_model) +{ + for (auto &f_it : goto_model.goto_functions.function_map) + { + Forall_goto_program_instructions(i_it, f_it.second.body) + { + if (i_it->incoming_edges.size() <= 1) + continue; + if (!i_it->is_skip()) + continue; + + bool has_backwards_goto = false; + bool has_forward_goto = false; + for (auto &incoming : i_it->incoming_edges) + { + if (incoming->location_number < i_it->location_number) + has_forward_goto = true; + if (incoming->location_number > i_it->location_number) + has_backwards_goto = true; + } + if (has_forward_goto && has_backwards_goto) + { + auto new_skip = f_it.second.body.insert_after( + i_it, + goto_programt::make_skip(i_it->source_location)); + + for (auto &incoming : i_it->incoming_edges) + { + if (incoming->location_number > i_it->location_number) + { + // Redirect backward GOTOs to the new skip + for (auto &target : incoming->targets) + { + if (target == i_it) + target = new_skip; + } + } + } + } + } + goto_model.goto_functions.update(); + } +} From c88cdd7ce482b436af241bbfa0b3806f0db7a03d Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Fri, 8 Oct 2021 15:24:56 +0200 Subject: [PATCH 04/14] SSA: drop conditional update of dynamic objects When assigning into a dereference, we allowed not to update the pointed dynamic object to simulate the fact that the dynamic object may be abstract (i.e. it may represent more concrete objects). This shouldn't be necessary anymore since we're using dynamic object instances, which should ensure soundness. --- src/ssa/local_ssa.cpp | 34 +--------------------------------- src/ssa/local_ssa.h | 17 ----------------- 2 files changed, 1 insertion(+), 50 deletions(-) diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index 151267c7..72d736a7 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -1110,40 +1110,8 @@ void local_SSAt::assign_rec( { const if_exprt &if_expr=to_if_expr(lhs); - exprt::operandst other_cond_conj; - if(if_expr.true_case().get_bool("#heap_access") && - if_expr.cond().id()==ID_equal) - { - const exprt heap_object=if_expr.true_case(); - const ssa_objectt ptr_object(to_equal_expr(if_expr.cond()).lhs(), ns); - if(ptr_object) - { - const irep_idt ptr_id=ptr_object.get_identifier(); - const exprt cond=read_rhs(if_expr.cond(), loc); - - for(const dyn_obj_assignt &do_assign : dyn_obj_assigns[heap_object]) - { - if(!alias_analysis[loc].aliases.same_set( - ptr_id, do_assign.pointer_id)) - { - other_cond_conj.push_back(do_assign.cond); - } - } - - dyn_obj_assigns[heap_object].emplace_back(ptr_id, cond); - } - } - - exprt cond=if_expr.cond(); - if(!other_cond_conj.empty()) - { - const exprt other_cond=or_exprt( - not_exprt(conjunction(other_cond_conj)), - name(guard_symbol(), OBJECT_SELECT, loc)); - cond=and_exprt(cond, other_cond); - } exprt orig_rhs=fresh_rhs ? name(ssa_objectt(rhs, ns), OUT, loc) : rhs; - exprt new_rhs=if_exprt(cond, orig_rhs, if_expr.true_case()); + exprt new_rhs=if_exprt(if_expr.cond(), orig_rhs, if_expr.true_case()); assign_rec( if_expr.true_case(), new_rhs, diff --git a/src/ssa/local_ssa.h b/src/ssa/local_ssa.h index 846350d8..6c5b1be7 100644 --- a/src/ssa/local_ssa.h +++ b/src/ssa/local_ssa.h @@ -51,7 +51,6 @@ class local_SSAt options, ssa_objects, ssa_value_ai), - alias_analysis(_function_identifier, _goto_function, ns), guard_map(_goto_function.body), function_identifier(_function_identifier), ssa_analysis(assignments), @@ -148,20 +147,6 @@ class local_SSAt // unknown heap objects var_sett unknown_objs; - // Maps members of dynamic object to a set of pointers used to access those - // objects when assigning them - class dyn_obj_assignt - { - public: - const irep_idt pointer_id; - const exprt cond; - - dyn_obj_assignt(const irep_idt &pointer_id, const exprt &cond): - pointer_id(pointer_id), cond(cond) {} - }; - typedef std::list dyn_obj_assignst; - std::map dyn_obj_assigns; - // Map dynamic object names to guards of their allocation std::map allocation_guards; @@ -239,8 +224,6 @@ class local_SSAt ssa_value_ait ssa_value_ai; assignmentst assignments; - may_alias_analysist alias_analysis; - // protected: guard_mapt guard_map; From 090c38de243d79730b89ae2e264227fc7d52aa79 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Mon, 11 Oct 2021 00:51:04 +0200 Subject: [PATCH 05/14] Correctly add allocation guards MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit In new CBMC, there is a case-split in the malloc function implementation for detecting malloc failures. This however resulted in SSA not being constructed correctly, since it expected the last definition of a symbol to be its allocation and not a phi node. Signed-off-by: František Nečas --- src/ssa/local_ssa.cpp | 42 +++++++++++++++++++++++++++++++++++------- src/ssa/local_ssa.h | 4 ++++ src/ssa/ssa_domain.h | 1 + 3 files changed, 40 insertions(+), 7 deletions(-) diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index 72d736a7..9010a9e2 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -883,17 +884,18 @@ exprt local_SSAt::read_rhs_rec(const exprt &expr, locationt loc) const { // If the last definition of an object is at its allocation, we can only use // the corresponding symbol if the object has truly been allocated - // (allocation guard holds). Otherwise we need to use the last definition - // before the allocation. + // (allocation guard holds). After the rebase to a newer version of CBMC, + // the last definition may also be a PHI node at the end of malloc ( + // which covers the case-split whether malloc can fail). + // Otherwise we need to use the last definition before the allocation. auto def_it=ssa_analysis[loc].def_map.find(object.get_identifier()); - if(def_it!=ssa_analysis[loc].def_map.end() && - def_it->second.def.kind==ssa_domaint::deft::ALLOCATION) + auto maybe_alloc_def=get_recent_object_alloc_def(loc, def_it); + if(maybe_alloc_def.has_value()) { - locationt alloc_loc=def_it->second.def.loc; return if_exprt( - read_rhs(def_it->second.def.guard, alloc_loc), + read_rhs(maybe_alloc_def->guard, maybe_alloc_def->loc), read_rhs(object, loc), - read_rhs(object, alloc_loc)); + read_rhs(object, maybe_alloc_def->loc)); } else return read_rhs(object, loc); @@ -904,6 +906,32 @@ exprt local_SSAt::read_rhs_rec(const exprt &expr, locationt loc) const } } +/// Checks whether the last definition of the object is its allocation and +/// if so, return the allocation def. Otherwise returns nullopt. +optionalt local_SSAt::get_recent_object_alloc_def( + locationt loc, + const ssa_domaint::def_mapt::const_iterator &def) const +{ + if(def==ssa_analysis[loc].def_map.end()) + return nullopt; + + if(def->second.def.is_allocation()) + return def->second.def; + + // Not a direct allocation, follow the split if it is a phi node and add + // guard if at least one of the branches is an allocation. + if(def->second.def.is_phi()) + { + const auto &phi_branches= + ssa_analysis[def->second.def.loc].phi_nodes.find(def->first); + if(phi_branches!=ssa_analysis[def->second.def.loc].phi_nodes.end()) + for(const auto &phi_branch : phi_branches->second) + if(phi_branch.second.is_allocation()) + return phi_branch.second; + } + return nullopt; +} + void local_SSAt::replace_side_effects_rec( exprt &expr, locationt loc, unsigned &counter) const { diff --git a/src/ssa/local_ssa.h b/src/ssa/local_ssa.h index 6c5b1be7..5f4d96d6 100644 --- a/src/ssa/local_ssa.h +++ b/src/ssa/local_ssa.h @@ -279,6 +279,10 @@ class local_SSAt void collect_custom_templates(); replace_mapt template_newvars; exprt template_last_newvar; + + optionalt get_recent_object_alloc_def( + locationt loc, + const ssa_domaint::def_mapt::const_iterator &def) const; }; std::list & operator << diff --git a/src/ssa/ssa_domain.h b/src/ssa/ssa_domain.h index a8f1088b..5fe41303 100644 --- a/src/ssa/ssa_domain.h +++ b/src/ssa/ssa_domain.h @@ -34,6 +34,7 @@ class ssa_domaint:public ai_domain_baset inline bool is_input() const { return kind==INPUT; } inline bool is_assignment() const { return kind==ASSIGNMENT; } inline bool is_phi() const { return kind==PHI; } + inline bool is_allocation() const { return kind==ALLOCATION; } }; friend inline bool operator==(const deft &a, const deft &b) From bc5b1daab7f84691a0b70da1e1a0734facccadfa Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Mon, 11 Oct 2021 11:17:35 +0200 Subject: [PATCH 06/14] Heap: improve obtaining pointed object from solver If the solver returns &(X.field) where field has offset 0, this is equivalent to &X. This commit handles the above situation in the heap domain so that the points-to relation to X is properly established in the domain value. --- src/domains/heap_domain.cpp | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/domains/heap_domain.cpp b/src/domains/heap_domain.cpp index d5b4b451..d04f3896 100644 --- a/src/domains/heap_domain.cpp +++ b/src/domains/heap_domain.cpp @@ -216,6 +216,8 @@ const exprt heap_domaint::get_points_to_dest( { // Value from the solver must be converted into an expression exprt ptr_value=value_to_ptr_exprt(solver_value); + if(ptr_value.id()==ID_typecast) + ptr_value=to_typecast_expr(ptr_value).op(); if((ptr_value.id()==ID_constant && to_constant_expr(ptr_value).get_value()==ID_NULL) || @@ -228,18 +230,30 @@ const exprt heap_domaint::get_points_to_dest( { // Template row pointer points to the heap (p = &obj) assert(ptr_value.id()==ID_address_of); - if(to_address_of_expr(ptr_value).object().id()!=ID_symbol) + exprt obj=to_address_of_expr(ptr_value).object(); + if(obj.id()==ID_member) + { + // &(X.field) where field has offset 0 is equal to &X + auto &member=to_member_expr(obj); + auto field=member.get_component_name(); + auto struct_type=ns.follow(member.compound().type()); + if(struct_type.id()==ID_struct && + to_struct_type(struct_type).component_number(field)==0) + { + obj=member.compound(); + } + } + if(obj.id()!=ID_symbol) { // If solver did not return address of a symbol, it is considered // as nondet value. return nil_exprt(); } - symbol_exprt obj=to_symbol_expr( - to_address_of_expr(ptr_value).object()); + symbol_exprt symbol_obj=to_symbol_expr(obj); - if(obj.type()!=templ_row_expr.type() && - ns.follow(templ_row_expr.type().subtype())!=ns.follow(obj.type())) + if(symbol_obj.type()!=templ_row_expr.type() && + ns.follow(templ_row_expr.type().subtype())!=ns.follow(symbol_obj.type())) { if(!is_cprover_symbol(templ_row_expr)) { @@ -249,7 +263,7 @@ const exprt heap_domaint::get_points_to_dest( } // Add equality p == &obj - return std::move(obj); + return std::move(symbol_obj); } else return nil_exprt(); From 646ac5d568467b5b7ba408519535365842d7a6dd Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Mon, 11 Oct 2021 12:36:57 +0200 Subject: [PATCH 07/14] Fix collection of free::record vars These are non-deterministic boolean variables used to control assignment to CPROVER-specific values during free. They used to be declared-only, now they are explicitly assigned a nondet value, which broke our code that searched for declarations only. Fixing this problem re-enables two true memsafety regression tests. --- regression/memsafety/built_from_end/test.desc | 31 +----------------- regression/memsafety/simple_true/test.desc | 32 +------------------ src/ssa/local_ssa.cpp | 6 ++-- 3 files changed, 5 insertions(+), 64 deletions(-) diff --git a/regression/memsafety/built_from_end/test.desc b/regression/memsafety/built_from_end/test.desc index c9a5cf96..a9c706a2 100644 --- a/regression/memsafety/built_from_end/test.desc +++ b/regression/memsafety/built_from_end/test.desc @@ -1,35 +1,6 @@ -KNOWNBUG +CORE main.c --heap --intervals --pointer-check --no-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ --- --- -CBMC 5.9 introduced changes to its implementation of some built-in functions, -the ones affecting this test are malloc and free. Malloc changes have been -already accounted for in 2LS codebase, however the control flow of free -is most likely causing problems in this test making one of the asserts fail: - -[main.pointer_dereference.27] dereference failure: deallocated dynamic object in *p: UNKNOWN - -This may be related to double free assertion, where GOTO changed from: - -... - IF !(__CPROVER_deallocated == ptr) THEN GOTO 6 - // 144 file line 18 function free - ASSERT 0 != 0 // double free - // 145 no location - ASSUME 0 != 0 - // 146 file line 29 function free - 6: _Bool record; -... - -to: - ASSERT ptr == NULL || __CPROVER_deallocated != ptr // double free - -Note the new ptr == NULL condition, this could be the root cause of -the problem. However further investigation is required -and will be done once the CBMC rebase is completed. According to the -C standard, free(NULL) is a valid construct (no operation) but 2LS doesn't -seem to handle this case correctly. diff --git a/regression/memsafety/simple_true/test.desc b/regression/memsafety/simple_true/test.desc index 8975589c..a9c706a2 100644 --- a/regression/memsafety/simple_true/test.desc +++ b/regression/memsafety/simple_true/test.desc @@ -1,36 +1,6 @@ -KNOWNBUG +CORE main.c --heap --intervals --pointer-check --no-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ --- --- -CBMC 5.9 introduced changes to its implementation of some built-in functions, -the ones affecting this test are malloc and free. Malloc changes have been -already accounted for in 2LS codebase, however the control flow of free -is most likely causing problems in this test making one of the asserts fail: - -[main.pointer_dereference.27] dereference failure: deallocated dynamic object in *p: UNKNOWN - -This may be related to double free assertion, where GOTO changed from: - -... - IF !(__CPROVER_deallocated == ptr) THEN GOTO 6 - // 144 file line 18 function free - ASSERT 0 != 0 // double free - // 145 no location - ASSUME 0 != 0 - // 146 file line 29 function free - 6: _Bool record; -... - -to: - ASSERT ptr == NULL || __CPROVER_deallocated != ptr // double free - -Note the new ptr == NULL condition, this could be the root cause of -the problem. However further investigation is required -and will be done once the CBMC rebase is completed. According to the -C standard, free(NULL) is a valid construct (no operation) but 2LS doesn't -seem to handle this case correctly. - diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index 9010a9e2..ff655a49 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -1541,10 +1541,10 @@ void local_SSAt::collect_allocation_guards( void local_SSAt::collect_record_frees(local_SSAt::locationt loc) { - if(loc->is_decl()) + if(loc->is_assign()) { - const code_declt &code_decl=code_declt{loc->decl_symbol()}; - const exprt &symbol=code_decl.symbol(); + const code_assignt &code_assign=to_code_assign(loc->get_code()); + const exprt &symbol=code_assign.lhs(); if(symbol.id()!=ID_symbol) return; From 25f05f59cfb22d096f91f6e38f81725d843ed0e0 Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Thu, 14 Oct 2021 08:03:15 +0200 Subject: [PATCH 08/14] malloc: fix getting malloc size After the rebase to new CBMC, constant propagation does not work in some cases. This is a problem for our malloc handling as we require to see: malloc_size = sizeof(...) This commit fixes the problem by recursively searching for the malloc size expression to handle cases like: size = sizeof(...) malloc_size = size Also adds a regression test for this case. --- regression/memsafety/double_free/main.c | 9 +++++ regression/memsafety/double_free/test.desc | 7 ++++ src/ssa/malloc_ssa.cpp | 42 +++++++++++++++++----- 3 files changed, 50 insertions(+), 8 deletions(-) create mode 100644 regression/memsafety/double_free/main.c create mode 100644 regression/memsafety/double_free/test.desc diff --git a/regression/memsafety/double_free/main.c b/regression/memsafety/double_free/main.c new file mode 100644 index 00000000..ee5589bd --- /dev/null +++ b/regression/memsafety/double_free/main.c @@ -0,0 +1,9 @@ +void *my_malloc(unsigned int size) { + return malloc(size); +} + +int main() { + void *a = my_malloc(sizeof(int)); + free(a); + free(a); +} diff --git a/regression/memsafety/double_free/test.desc b/regression/memsafety/double_free/test.desc new file mode 100644 index 00000000..7af3e2e0 --- /dev/null +++ b/regression/memsafety/double_free/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--pointer-check --inline +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +\[free.precondition.6\] free argument must be NULL or valid pointer: FAILURE diff --git a/src/ssa/malloc_ssa.cpp b/src/ssa/malloc_ssa.cpp index a46fc6b0..9a98afc8 100644 --- a/src/ssa/malloc_ssa.cpp +++ b/src/ssa/malloc_ssa.cpp @@ -289,6 +289,38 @@ static bool replace_malloc_rec( } } +/// Finds the latest assignment to lhs before location_number and: +/// - if the assignment rhs is a symbol, continues recursively +/// - otherwise returns the rhs +exprt get_malloc_size( + const exprt &lhs, + unsigned location_number, + const goto_functiont &goto_function) +{ + exprt result=nil_exprt(); + unsigned result_loc_num=0; + forall_goto_program_instructions(it, goto_function.body) + { + if(!it->is_assign()) + continue; + + if(lhs==it->assign_lhs()) + { + result=it->assign_rhs(); + if(result.id()==ID_typecast) + result=to_typecast_expr(result).op(); + result_loc_num=it->location_number; + } + + if(it->location_number==location_number) + break; + } + if(result.id()==ID_symbol) + return get_malloc_size(result, result_loc_num, goto_function); + + return result; +} + bool replace_malloc( goto_modelt &goto_model, const std::string &suffix, @@ -336,14 +368,8 @@ bool replace_malloc( function_copy.copy_from(f_it.second); constant_propagator_ait const_propagator(function_copy); const_propagator(f_it.first, function_copy, ns); - forall_goto_program_instructions(copy_i_it, function_copy.body) - { - if(copy_i_it->location_number==i_it->location_number) - { - assert(copy_i_it->is_assign()); - malloc_size=copy_i_it->get_assign().rhs(); - } - } + malloc_size=get_malloc_size( + i_it->assign_lhs(), i_it->location_number, function_copy); } } if(replace_malloc_rec(code_assign.rhs(), From 5a63242daebf183628d6433de938de7b9b17e6de Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Mon, 18 Oct 2021 08:39:21 +0200 Subject: [PATCH 09/14] Fix assert to limit array size CBMC has changed the representation of numerical values in constant_expr (at least for array sizes) - instead of base 2, it now uses base 16. We have to fix this in our assertion that limits the size of arrays in competition mode due to solver unsoundness that appears for arrays of size >=50000. --- src/2ls/preprocessing_util.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index 062207c2..5ed1e714 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -674,7 +674,7 @@ void twols_parse_optionst::limit_array_bounds(goto_modelt &goto_model) if(size_expr.id()==ID_constant) { int size=std::stoi( - id2string(to_constant_expr(size_expr).get_value()), nullptr, 2); + id2string(to_constant_expr(size_expr).get_value()), nullptr, 16); // @TODO temporary solution - there seems to be a bug in the solver assert(size<=50000); } From 2c45caf7fe97089447b7dac5f246a84266a11627 Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Mon, 18 Oct 2021 13:25:14 +0200 Subject: [PATCH 10/14] Disable unsupported operations in competition mode For now, we disable memcpy as it is implemented via a CBMC built-in operation that we do not support in 2LS, yet. --- src/ssa/local_ssa.cpp | 13 +++++++++++++ src/ssa/local_ssa.h | 3 +++ 2 files changed, 16 insertions(+) diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index ff655a49..0328ce1b 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -51,6 +51,9 @@ void local_SSAt::build_SSA() build_function_call(i_it); // build_unknown_objs(i_it); collect_record_frees(i_it); + + if (options.get_bool_option("competition-mode")) + disable_unsupported_instructions(i_it); } // collect custom templates in loop heads @@ -1644,3 +1647,13 @@ bool local_SSAt::can_reuse_symderef( return true; } + +void local_SSAt::disable_unsupported_instructions(locationt loc) +{ + if (loc->is_other()) + { + auto st = loc->get_code().get_statement(); + if(st=="array_copy" || st=="array_replace") + assert(false); + } +} diff --git a/src/ssa/local_ssa.h b/src/ssa/local_ssa.h index 5f4d96d6..268f1406 100644 --- a/src/ssa/local_ssa.h +++ b/src/ssa/local_ssa.h @@ -271,6 +271,9 @@ class local_SSAt void build_assertions(locationt loc); void build_unknown_objs(locationt loc); + // competition-mode specific checks + void disable_unsupported_instructions(locationt loc); + void collect_allocation_guards(const code_assignt &assign, locationt loc); void get_alloc_guard_rec(const exprt &expr, exprt old_guard); void collect_record_frees(locationt loc); From 11606bc50aad795880fdf19a935190416e4977e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Wed, 20 Oct 2021 11:13:55 +0200 Subject: [PATCH 11/14] Configure gcc preprocessing to fix linking MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: František Nečas --- src/2ls/2ls_parse_options.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index 326237eb..d8704d71 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include #include #include @@ -396,6 +397,14 @@ int twols_parse_optionst::doit() register_languages(); + // configure gcc, if required + if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC) + { + gcc_versiont gcc_version; + gcc_version.get("gcc"); + configure_gcc(gcc_version); + } + if(get_goto_program(options)) return 6; From 12cc730f96b5f7d6e8ea08d48ff4f043b89a3aa4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Sat, 23 Oct 2021 00:26:21 +0200 Subject: [PATCH 12/14] Correctly guard hoisted assertions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If there are multiple loops in the program, the assertions after the loops are reachable only if both of the loops exit their execution. Previously, exiting the first loop was sufficient due to the disjunction making the analysis unsound (producing incorrect true results in some cases, including SV-comp benchmarks). Signed-off-by: František Nečas --- regression/kiki/hard2_unwindbound5/main.c | 61 ++++++++++++++++++++ regression/kiki/hard2_unwindbound5/test.desc | 10 ++++ src/ssa/ssa_unwinder.cpp | 2 +- 3 files changed, 72 insertions(+), 1 deletion(-) create mode 100644 regression/kiki/hard2_unwindbound5/main.c create mode 100644 regression/kiki/hard2_unwindbound5/test.desc diff --git a/regression/kiki/hard2_unwindbound5/main.c b/regression/kiki/hard2_unwindbound5/main.c new file mode 100644 index 00000000..00b3177e --- /dev/null +++ b/regression/kiki/hard2_unwindbound5/main.c @@ -0,0 +1,61 @@ +/* + hardware integer division program, by Manna + returns q==A//B + */ + +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +void reach_error() { __assert_fail("0", "hard2.c", 8, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +extern void abort(void); +void assume_abort_if_not(int cond) { + if(!cond) {abort();} +} +void __VERIFIER_assert(int cond) { + if (!(cond)) { + ERROR: + {reach_error();} + } + return; +} + +int counter = 0; +int main() { + int A, B; + int r, d, p, q; + A = __VERIFIER_nondet_int(); + B = 1; + + r = A; + d = B; + p = 1; + q = 0; + + while (counter++<5) { + __VERIFIER_assert(q == 0); + __VERIFIER_assert(r == A); + __VERIFIER_assert(d == B * p); + if (!(r >= d)) break; + + d = 2 * d; + p = 2 * p; + } + + while (counter++<5) { + __VERIFIER_assert(A == q*B + r); + __VERIFIER_assert(d == B*p); + + if (!(p != 1)) break; + + d = d / 2; + p = p / 2; + if (r >= d) { + r = r - d; + q = q + p; + } + } + + __VERIFIER_assert(A == d*q + r); + __VERIFIER_assert(B == d); + return 0; +} diff --git a/regression/kiki/hard2_unwindbound5/test.desc b/regression/kiki/hard2_unwindbound5/test.desc new file mode 100644 index 00000000..de523f99 --- /dev/null +++ b/regression/kiki/hard2_unwindbound5/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--heap --values-refine --k-induction --competition-mode +^EXIT=10$ +^SIGNAL=0$ +^.*FAILURE$ +-- +-- +This is a past incorrect true benchmark from SV-comp which was caused by a bug +in SSA unwinder where the generated constraints made the analysis unsound. diff --git a/src/ssa/ssa_unwinder.cpp b/src/ssa/ssa_unwinder.cpp index 36c96ae9..de67420b 100644 --- a/src/ssa/ssa_unwinder.cpp +++ b/src/ssa/ssa_unwinder.cpp @@ -529,7 +529,7 @@ void ssa_local_unwindert::add_hoisted_assertions(loopt &loop, bool is_last) to_not_expr(it->first->guard).op().id()==ID_overflow_shl)) #endif { - exprt e=disjunction(it->second.exit_conditions); + exprt e=conjunction(it->second.exit_conditions); SSA.rename(e, loop.body_nodes.begin()->location); SSA.nodes.push_back( local_SSAt::nodet(it->first, SSA.nodes.end())); // add new node From 3f21ab96bc1aef8d0d4de1c297f40f558ecddc83 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Sat, 23 Oct 2021 10:57:49 +0200 Subject: [PATCH 13/14] Fix workaround for signed shl MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The format of the guard changed making the hack not work and causing incorrect true results in bitvector category in SV-comp due to the hoisted assertion being added. Fix this hack. Signed-off-by: František Nečas --- src/ssa/ssa_unwinder.cpp | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) diff --git a/src/ssa/ssa_unwinder.cpp b/src/ssa/ssa_unwinder.cpp index de67420b..bac7c8f1 100644 --- a/src/ssa/ssa_unwinder.cpp +++ b/src/ssa/ssa_unwinder.cpp @@ -515,6 +515,31 @@ equal_exprt ssa_local_unwindert::build_exit_merge( return equal_exprt(e, re); } + +/// Check whether the expression contains signed left shift. +/// This is a hack for SV-comp to disable hoisting assertions for this +/// operation. +bool has_overflow_shl(const exprt &expr) +{ + if(expr.id()==ID_shl) + { + binary_exprt shl=to_binary_expr(expr); + if(shl.op0().type().id()==ID_signedbv) + return true; + } + else + { + // Recursively go through the operands + if(!expr.has_operands()) + return false; + else + forall_operands(o_it, expr) + if(has_overflow_shl(*o_it)) + return true; + } + return false; +} + /// adds the assumptions for hoisted assertions for the current instance void ssa_local_unwindert::add_hoisted_assertions(loopt &loop, bool is_last) { @@ -525,8 +550,7 @@ void ssa_local_unwindert::add_hoisted_assertions(loopt &loop, bool is_last) if(!is_last // only add assumptions if we are not in %0 iteration && is_kinduction && !it->second.assertions.empty() #ifdef COMPETITION - && !(it->first->guard.id()==ID_not && - to_not_expr(it->first->guard).op().id()==ID_overflow_shl)) + && !has_overflow_shl(it->first->guard)) #endif { exprt e=conjunction(it->second.exit_conditions); From 9071c907f25b032d747c71b1320c8918e6238c3e Mon Sep 17 00:00:00 2001 From: Viktor Malik Date: Sun, 24 Oct 2021 12:20:51 +0200 Subject: [PATCH 14/14] Propagate #concrete for byte-array dynamic objs Byte arrays are produced when malloc(N) is used where N is an integer and not a sizeof operator. We still need to propagate the '#concrete' flag to make the memsafety analysis sound. --- src/ssa/malloc_ssa.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ssa/malloc_ssa.cpp b/src/ssa/malloc_ssa.cpp index 9a98afc8..05008f68 100644 --- a/src/ssa/malloc_ssa.cpp +++ b/src/ssa/malloc_ssa.cpp @@ -72,6 +72,8 @@ exprt create_dynamic_object( from_integer(0, index_type()), value_symbol.type.subtype()); object=index_expr; + if(is_concrete) + to_index_expr(object).array().set("#concrete", true); } else {