From e715e86252bba5d8a2254e620360cf28e4937c0b Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 4 Jun 2024 23:07:38 -0500 Subject: [PATCH] Ignore cprover symbols in loop assigns inference --- src/goto-instrument/contracts/contracts.cpp | 3 +- .../dfcc_infer_loop_assigns.cpp | 3 +- .../contracts/instrument_spec_assigns.cpp | 8 +++ src/goto-instrument/contracts/utils.cpp | 17 +++++++ src/goto-instrument/contracts/utils.h | 8 +++ src/goto-instrument/loop_utils.cpp | 49 ++++++++++++++----- src/goto-instrument/loop_utils.h | 15 ++++++ 7 files changed, 90 insertions(+), 13 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index ca8189ff8465..3c3bba791dee 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -22,6 +22,7 @@ Date: February 2016 #include #include #include +#include #include #include @@ -218,7 +219,7 @@ void code_contractst::check_apply_loop_contracts( // and the inferred aliasing relation. try { - get_assigns(local_may_alias, loop, to_havoc); + infer_loop_assigns(local_may_alias, loop, to_havoc); // remove loop-local symbols from the inferred set cfg_info.erase_locals(to_havoc); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp index a0ed6b09afca..611b09ffbc56 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp @@ -13,6 +13,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include +#include #include #include "dfcc_root_object.h" @@ -53,7 +54,7 @@ assignst dfcc_infer_loop_assigns( { // infer assignst assigns; - get_assigns(local_may_alias, loop_instructions, assigns); + infer_loop_assigns(local_may_alias, loop_instructions, assigns); // compute locals std::unordered_set loop_locals; diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index e941c0732d39..5f975e4cbb78 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -19,6 +19,7 @@ Date: January 2022 #include #include #include +#include #include #include @@ -147,6 +148,13 @@ void instrument_spec_assignst::check_inclusion_assignment( const exprt &lhs, goto_programt &dest) const { + // Don't check assignable for CPROVER symbol + if( + lhs.id() == ID_symbol && + has_prefix(id2string(to_symbol_expr(lhs).get_identifier()), CPROVER_PREFIX)) + { + return; + } // create temporary car but do not track const auto car = create_car_expr(true_exprt{}, lhs); create_snapshot(car, dest); diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 2edd3b22a50d..2bb9ce77e9ab 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -18,6 +18,7 @@ Date: September 2021 #include #include #include +#include #include #include @@ -338,6 +339,22 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment) std::string::npos; } +void infer_loop_assigns( + const local_may_aliast &local_may_alias, + const loopt &loop, + assignst &assigns) +{ + // Assign targets should not include cprover symbols. + get_assigns(local_may_alias, loop, assigns, [](const exprt &e) { + if(e.id() == ID_symbol) + { + const auto &s = expr_try_dynamic_cast(e); + return has_prefix(id2string(s->get_identifier()), CPROVER_PREFIX); + } + return true; + }); +} + void widen_assigns(assignst &assigns, const namespacet &ns) { assignst result; diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index f7b7ac5e2850..0dd802bab186 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -16,7 +16,9 @@ Date: September 2021 #include #include +#include #include +#include #include @@ -214,6 +216,12 @@ irep_idt make_assigns_clause_replacement_tracking_comment( /// \ref make_assigns_clause_replacement_tracking_comment. bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment); +/// Infer loop assigns using alias analysis result `local_may_alias`. +void infer_loop_assigns( + const local_may_aliast &local_may_alias, + const loopt &loop, + assignst &assigns); + /// Widen expressions in \p assigns with the following strategy. /// If an expression is an array index or object dereference expression, /// with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant `i`, diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index 1384223e51f2..f05998a023ac 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -42,9 +42,24 @@ void get_assigns_lhs( const exprt &lhs, assignst &assigns) { - if(lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index) + get_assigns_lhs( + local_may_alias, t, lhs, assigns, [](const exprt &e) { return true; }); +} + +void get_assigns_lhs( + const local_may_aliast &local_may_alias, + goto_programt::const_targett t, + const exprt &lhs, + assignst &assigns, + std::function predicate) +{ + if( + (lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index) && + predicate(lhs)) + { assigns.insert(lhs); - else if(lhs.id()==ID_dereference) + } + else if(lhs.id() == ID_dereference) { const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer()); for(const auto &mod : local_may_alias.get(t, ptr.pointer)) @@ -54,15 +69,18 @@ void get_assigns_lhs( { continue; } + exprt to_insert; if(ptr.offset.is_nil()) - assigns.insert(dereference_exprt{typed_mod}); + to_insert = dereference_exprt{typed_mod}; else - assigns.insert(dereference_exprt{plus_exprt{typed_mod, ptr.offset}}); + to_insert = dereference_exprt{plus_exprt{typed_mod, ptr.offset}}; + if(predicate(to_insert)) + assigns.insert(std::move(to_insert)); } } - else if(lhs.id()==ID_if) + else if(lhs.id() == ID_if) { - const if_exprt &if_expr=to_if_expr(lhs); + const if_exprt &if_expr = to_if_expr(lhs); get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns); get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns); @@ -74,20 +92,29 @@ void get_assigns( const loopt &loop, assignst &assigns) { - for(loopt::const_iterator - i_it=loop.begin(); i_it!=loop.end(); i_it++) + get_assigns( + local_may_alias, loop, assigns, [](const exprt &e) { return true; }); +} + +void get_assigns( + const local_may_aliast &local_may_alias, + const loopt &loop, + assignst &assigns, + std::function predicate) +{ + for(loopt::const_iterator i_it = loop.begin(); i_it != loop.end(); i_it++) { - const goto_programt::instructiont &instruction=**i_it; + const goto_programt::instructiont &instruction = **i_it; if(instruction.is_assign()) { const exprt &lhs = instruction.assign_lhs(); - get_assigns_lhs(local_may_alias, *i_it, lhs, assigns); + get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate); } else if(instruction.is_function_call()) { const exprt &lhs = instruction.call_lhs(); - get_assigns_lhs(local_may_alias, *i_it, lhs, assigns); + get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate); } } } diff --git a/src/goto-instrument/loop_utils.h b/src/goto-instrument/loop_utils.h index dd5c0f9b9dcc..6838f662975f 100644 --- a/src/goto-instrument/loop_utils.h +++ b/src/goto-instrument/loop_utils.h @@ -24,12 +24,27 @@ void get_assigns( const loopt &loop, assignst &assigns); +/// get all assign targets that satisfy `predicate` within the loops. +void get_assigns( + const local_may_aliast &local_may_alias, + const loopt &loop, + assignst &assigns, + std::function predicate); + void get_assigns_lhs( const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns); +/// get all assign targets that satisfy `predicate` from `lhs`. +void get_assigns_lhs( + const local_may_aliast &local_may_alias, + goto_programt::const_targett t, + const exprt &lhs, + assignst &assigns, + std::function predicate); + goto_programt::targett get_loop_exit(const loopt &); #endif // CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H