From d9978b4d7549e349bb4c75c970f2d3572062a2ec Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sun, 19 Mar 2023 23:31:30 -0500 Subject: [PATCH 1/2] Don't error out when alias analysis fails during loop assigns inference --- regression/contracts/loop_assigns-fail/test.desc | 7 ++++--- src/goto-instrument/loop_utils.cpp | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/regression/contracts/loop_assigns-fail/test.desc b/regression/contracts/loop_assigns-fail/test.desc index b1f4751987d..38480d617d7 100644 --- a/regression/contracts/loop_assigns-fail/test.desc +++ b/regression/contracts/loop_assigns-fail/test.desc @@ -1,10 +1,11 @@ CORE main.c --apply-loop-contracts -activate-multi-line-match -Failed to infer variables being modified by the loop at file main.c line \d+ function main\.\nPlease specify an assigns clause\.\nReason:\nAlias analysis returned UNKNOWN! -^EXIT=6$ +^EXIT=10$ ^SIGNAL=0$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ +^VERIFICATION FAILED$ -- -- This test (taken from #6021) shows the need for assigns clauses on loops. diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index d60f22316fb..1384223e51f 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -52,7 +52,7 @@ void get_assigns_lhs( const typecast_exprt typed_mod{mod, ptr.pointer.type()}; if(mod.id() == ID_unknown) { - throw analysis_exceptiont("Alias analysis returned UNKNOWN!"); + continue; } if(ptr.offset.is_nil()) assigns.insert(dereference_exprt{typed_mod}); From c5bebfa1c964ffc9834f9705cd8386f72f864a5c Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sun, 19 Mar 2023 23:35:31 -0500 Subject: [PATCH 2/2] Use local alias analysis in loop assigns synthesis --- ...enumerative_loop_contracts_synthesizer.cpp | 25 ++++++++++++++++--- .../enumerative_loop_contracts_synthesizer.h | 5 +++- 2 files changed, 25 insertions(+), 5 deletions(-) diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index d7e5afcebea..206dcef40df 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -19,8 +19,12 @@ Author: Qinheping Hu #include #include +#include #include +#include +#include #include +#include #include "cegis_verifier.h" #include "expr_enumerator.h" @@ -82,17 +86,21 @@ void enumerative_loop_contracts_synthesizert::init_candidates() { for(auto &function_p : goto_model.goto_functions.function_map) { - natural_loopst natural_loops; + natural_loops_mutablet natural_loops; natural_loops(function_p.second.body); + // TODO: use global may alias instead. + local_may_aliast local_may_alias(function_p.second); + // Initialize invariants for unannotated loops as true for(const auto &loop_head_and_content : natural_loops.loop_map) { goto_programt::const_targett loop_end = - get_loop_end_from_loop_head_and_content( + get_loop_end_from_loop_head_and_content_mutable( loop_head_and_content.first, loop_head_and_content.second); loop_idt new_id(function_p.first, loop_end->loop_number); + loop_cfg_infot cfg_info(function_p.second, loop_head_and_content.second); log.debug() << "Initialize candidates for the loop at " << loop_end->source_location() << messaget::eom; @@ -116,6 +124,17 @@ void enumerative_loop_contracts_synthesizert::init_candidates() if(loop_end->condition().find(ID_C_spec_assigns).is_nil()) { assigns_map[new_id] = {}; + + // Infer loop assigns using alias analysis. + get_assigns( + local_may_alias, loop_head_and_content.second, assigns_map[new_id]); + + // remove loop-local symbols from the inferred set + cfg_info.erase_locals(assigns_map[new_id]); + + // If the set contains pairs (i, a[i]), + // we widen them to (i, __CPROVER_POINTER_OBJECT(a)) + widen_assigns(assigns_map[new_id], ns); } } } @@ -127,7 +146,6 @@ void enumerative_loop_contracts_synthesizert::synthesize_assigns( const exprt &checked_pointer, const std::list cause_loop_ids) { - namespacet ns(goto_model.symbol_table); auto new_assign = checked_pointer; // Add the new assigns target to the most-inner loop that doesn't contain @@ -242,7 +260,6 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause( // | StartBool <= StartBool | StartBool < StartBool // Start -> Start + Start | terminal_symbols // where a0, and a1 are symbol expressions. - namespacet ns(goto_model.symbol_table); enumerator_factoryt factory = enumerator_factoryt(ns); recursive_enumerator_placeholdert start_bool_ph(factory, "StartBool", ns); recursive_enumerator_placeholdert start_ph(factory, "Start", ns); diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h index e97081f787a..49636dfca3e 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h @@ -31,7 +31,8 @@ class enumerative_loop_contracts_synthesizert enumerative_loop_contracts_synthesizert( goto_modelt &goto_model, messaget &log) - : loop_contracts_synthesizer_baset(goto_model, log) + : loop_contracts_synthesizer_baset(goto_model, log), + ns(goto_model.symbol_table) { } @@ -45,6 +46,8 @@ class enumerative_loop_contracts_synthesizert return assigns_map; } + namespacet ns; + private: /// Initialize invariants as true for all unannotated loops. void init_candidates();