From 1ed46d5269b5f9a0b3631b7cbb9c015e79ceeee1 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 26 Jun 2024 12:17:00 -0500 Subject: [PATCH 1/2] Add a test on which SMT2 fail with quantifers in nested loop contracts --- .../quantifiers-loop-fail/main.c | 27 +++++++++++++++++++ .../quantifiers-loop-fail/test.desc | 13 +++++++++ 2 files changed, 40 insertions(+) create mode 100644 regression/contracts-dfcc/quantifiers-loop-fail/main.c create mode 100644 regression/contracts-dfcc/quantifiers-loop-fail/test.desc diff --git a/regression/contracts-dfcc/quantifiers-loop-fail/main.c b/regression/contracts-dfcc/quantifiers-loop-fail/main.c new file mode 100644 index 00000000000..f44af096f58 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-fail/main.c @@ -0,0 +1,27 @@ +#include +#include + +#define N 16 + +void main() +{ + int a[N]; + a[10] = 0; + bool flag = true; + for(int j = 0; j < N; ++j) + __CPROVER_loop_invariant(j <= N) + { + for(int i = 0; i < N; ++i) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_whole(a)) + __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall { + int k; + (0 <= k && k <= N) ==> (k a[k] == 1) + }) + // clang-format on + { + a[i] = 1; + } + } + assert(a[10] == 1); +} diff --git a/regression/contracts-dfcc/quantifiers-loop-fail/test.desc b/regression/contracts-dfcc/quantifiers-loop-fail/test.desc new file mode 100644 index 00000000000..e54dd9ed35a --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-fail/test.desc @@ -0,0 +1,13 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts _ --smt2 +^EXIT=6$ +^SIGNAL=0$ +^SMT2 solver returned error message:$ +^.*\"line \d+ column \d+: unknown constant .*$ +^VERIFICATION ERROR$ +-- +^warning: ignoring +-- +This test case checks the handling of quantifiers in a nested loop's +loop contracts. From ab12de470f542e3b51eabfd5294eca13f4d3edd9 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 4 Jul 2024 22:15:35 -0500 Subject: [PATCH 2/2] Make sure free symbols are declared in SMT2_conv after quantifier rewriting A bound variable may shadow another free or bound variable. --- .../contracts-dfcc/quantifiers-loop-05/main.c | 34 +++++++++++++++++++ .../test.desc | 6 ++-- .../quantifiers-loop-fail/main.c | 27 --------------- src/solvers/smt2/smt2_conv.cpp | 34 +++++++++++++------ src/solvers/smt2/smt2_conv.h | 7 ++-- 5 files changed, 64 insertions(+), 44 deletions(-) create mode 100644 regression/contracts-dfcc/quantifiers-loop-05/main.c rename regression/contracts-dfcc/{quantifiers-loop-fail => quantifiers-loop-05}/test.desc (61%) delete mode 100644 regression/contracts-dfcc/quantifiers-loop-fail/main.c diff --git a/regression/contracts-dfcc/quantifiers-loop-05/main.c b/regression/contracts-dfcc/quantifiers-loop-05/main.c new file mode 100644 index 00000000000..b034b849559 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-05/main.c @@ -0,0 +1,34 @@ +#include +#include +#include + +#define N 16 + +void main() +{ + int a[N]; + a[10] = 0; + bool flag = true; + for(size_t j = 0; j < N; ++j) + // clang-format off + __CPROVER_assigns(j, __CPROVER_object_whole(a)) + __CPROVER_loop_invariant(j <= N) + __CPROVER_loop_invariant((j != 0) ==> __CPROVER_forall { + int k; + (0 <= k && k < N) ==> (a[k] == 1) + }) + // clang-format on + { + for(size_t i = 0; i < N; ++i) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_whole(a)) + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_loop_invariant(__CPROVER_forall { int k; k < i ==> a[k] == 1 }) + + // clang-format on + { + a[i] = 1; + } + } + assert(a[10] == 1); +} diff --git a/regression/contracts-dfcc/quantifiers-loop-fail/test.desc b/regression/contracts-dfcc/quantifiers-loop-05/test.desc similarity index 61% rename from regression/contracts-dfcc/quantifiers-loop-fail/test.desc rename to regression/contracts-dfcc/quantifiers-loop-05/test.desc index e54dd9ed35a..f6894dc7da1 100644 --- a/regression/contracts-dfcc/quantifiers-loop-fail/test.desc +++ b/regression/contracts-dfcc/quantifiers-loop-05/test.desc @@ -1,11 +1,9 @@ CORE dfcc-only main.c --dfcc main --apply-loop-contracts _ --smt2 -^EXIT=6$ +^EXIT=0$ ^SIGNAL=0$ -^SMT2 solver returned error message:$ -^.*\"line \d+ column \d+: unknown constant .*$ -^VERIFICATION ERROR$ +^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring -- diff --git a/regression/contracts-dfcc/quantifiers-loop-fail/main.c b/regression/contracts-dfcc/quantifiers-loop-fail/main.c deleted file mode 100644 index f44af096f58..00000000000 --- a/regression/contracts-dfcc/quantifiers-loop-fail/main.c +++ /dev/null @@ -1,27 +0,0 @@ -#include -#include - -#define N 16 - -void main() -{ - int a[N]; - a[10] = 0; - bool flag = true; - for(int j = 0; j < N; ++j) - __CPROVER_loop_invariant(j <= N) - { - for(int i = 0; i < N; ++i) - // clang-format off - __CPROVER_assigns(i, __CPROVER_object_whole(a)) - __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall { - int k; - (0 <= k && k <= N) ==> (k a[k] == 1) - }) - // clang-format on - { - a[i] = 1; - } - } - assert(a[10] == 1); -} diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index d132114cb22..6752b566b79 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -4721,11 +4721,11 @@ void smt2_convt::set_to(const exprt &expr, bool value) identifier_map.find(identifier) == identifier_map.end() && equal_expr.lhs() != equal_expr.rhs()) { - identifiert &id=identifier_map[identifier]; - CHECK_RETURN(id.type.is_nil()); + auto id_entry = identifier_map.insert( + {identifier, identifiert{equal_expr.lhs().type(), false}}); + CHECK_RETURN(id_entry.second); - id.type=equal_expr.lhs().type(); - find_symbols(id.type); + find_symbols(id_entry.first->second.type); exprt prepared_rhs = prepare_for_convert_expr(equal_expr.rhs()); std::string smt2_identifier=convert_identifier(identifier); @@ -4908,17 +4908,30 @@ void smt2_convt::find_symbols(const exprt &expr) if(expr.id() == ID_exists || expr.id() == ID_forall) { + std::unordered_map> shadowed_syms; + // do not declare the quantified symbol, but record // as 'bound symbol' const auto &q_expr = to_quantifier_expr(expr); for(const auto &symbol : q_expr.variables()) { const auto identifier = symbol.get_identifier(); - identifiert &id = identifier_map[identifier]; - id.type = symbol.type(); - id.is_bound = true; + auto id_entry = + identifier_map.insert({identifier, identifiert{symbol.type(), true}}); + shadowed_syms.insert( + {identifier, + id_entry.second ? std::nullopt + : std::optional{id_entry.first->second}}); } find_symbols(q_expr.where()); + for(const auto &[id, shadowed_val] : shadowed_syms) + { + auto previous_entry = identifier_map.find(id); + if(!shadowed_val.has_value()) + identifier_map.erase(previous_entry); + else + previous_entry->second = std::move(*shadowed_val); + } return; } @@ -4941,12 +4954,11 @@ void smt2_convt::find_symbols(const exprt &expr) identifier="nondet_"+ id2string(to_nondet_symbol_expr(expr).get_identifier()); - identifiert &id=identifier_map[identifier]; + auto id_entry = + identifier_map.insert({identifier, identifiert{expr.type(), false}}); - if(id.type.is_nil()) + if(id_entry.second) { - id.type=expr.type(); - std::string smt2_identifier=convert_identifier(identifier); smt2_identifiers.insert(smt2_identifier); diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 4a043824831..a0c0382e395 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -242,13 +242,16 @@ class smt2_convt : public stack_decision_proceduret // keeps track of all non-Boolean symbols and their value struct identifiert { + // We do not currently read any of the following members, but might do so in + // future. At this time, we just care about (not) having an entry in + // `identifier_map`. bool is_bound; typet type; exprt value; - identifiert() : is_bound(false) + identifiert(typet type, bool is_bound) + : is_bound(is_bound), type(std::move(type)) { - type.make_nil(); value.make_nil(); } };