From 9f9f6c0b1388714c914d64d1c86658bc84746e98 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 Sep 2024 12:50:56 +0000 Subject: [PATCH] Deprecate make_and in favour of conjunction(expr, expr) `make_and` does not necessarily produce an `and_exprt`, so its name is misleading. We already have `conjunction(exprt::operandst)`, and will now have a variant thereof that takes exactly two operands. --- regression/cbmc-cover/mcdc8/test.desc | 8 ++++---- src/goto-symex/symex_assign.cpp | 3 +-- src/solvers/prop/bdd_expr.cpp | 4 ++-- src/util/expr_util.cpp | 20 +------------------- src/util/expr_util.h | 1 + src/util/std_expr.cpp | 25 +++++++++++++++++++++++++ src/util/std_expr.h | 5 +++++ 7 files changed, 39 insertions(+), 27 deletions(-) diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc index 5c5bee9eaed..de6becf4ae6 100644 --- a/regression/cbmc-cover/mcdc8/test.desc +++ b/regression/cbmc-cover/mcdc8/test.desc @@ -3,10 +3,10 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && a != FALSE && !\(b != FALSE\).* SATISFIED$ -^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && !\(a != FALSE\) && b != FALSE.* SATISFIED$ -^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$ -^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition '!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$ +^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition 'a != FALSE && !\(b != FALSE\) && c != FALSE: SATISFIED$ +^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition 'a != FALSE && !\(b != FALSE\) && !\(c != FALSE\): SATISFIED$ +^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition '!\(a != FALSE\) && b != FALSE && c != FALSE: SATISFIED$ +^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition '!\(a != FALSE\) && !\(b != FALSE\) && c != FALSE: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index c829e4b1d8c..2e0f7053e9b 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_assign.h" #include -#include #include #include @@ -238,7 +237,7 @@ void symex_assignt::assign_non_struct_symbol( : assignment_type; target.assignment( - make_and(state.guard.as_expr(), conjunction(guard)), + conjunction(state.guard.as_expr(), conjunction(guard)), l2_lhs, l2_full_lhs, get_original_name(l2_full_lhs), diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index f900c90f765..cbb5ee60cc6 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -138,7 +138,7 @@ exprt bdd_exprt::as_expr( if(r.else_branch().is_complement()) // else is false { exprt then_case = as_expr(r.then_branch(), cache); - return make_and(n_expr, then_case); + return conjunction(n_expr, then_case); } exprt then_case = as_expr(r.then_branch(), cache); return make_or(not_exprt(n_expr), then_case); @@ -149,7 +149,7 @@ exprt bdd_exprt::as_expr( if(r.then_branch().is_complement()) // then is false { exprt else_case = as_expr(r.else_branch(), cache); - return make_and(not_exprt(n_expr), else_case); + return conjunction(not_exprt(n_expr), else_case); } exprt else_case = as_expr(r.else_branch(), cache); return make_or(n_expr, else_case); diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index e272918c364..2b65b858e19 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -346,25 +346,7 @@ constant_exprt make_boolean_expr(bool value) exprt make_and(exprt a, exprt b) { - PRECONDITION(a.is_boolean() && b.is_boolean()); - if(b.is_constant()) - { - if(b.get(ID_value) == ID_false) - return false_exprt{}; - return a; - } - if(a.is_constant()) - { - if(a.get(ID_value) == ID_false) - return false_exprt{}; - return b; - } - if(b.id() == ID_and) - { - b.add_to_operands(std::move(a)); - return b; - } - return and_exprt{std::move(a), std::move(b)}; + return conjunction(a, b); } bool is_null_pointer(const constant_exprt &expr) diff --git a/src/util/expr_util.h b/src/util/expr_util.h index eefe6903f37..04ffb59a274 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -112,6 +112,7 @@ constant_exprt make_boolean_expr(bool); /// Conjunction of two expressions. If the second is already an `and_exprt` /// add to its operands instead of creating a new expression. If one is `true`, /// return the other expression. If one is `false` returns `false`. +DEPRECATED(SINCE(2024, 9, 10, "use conjunction(exprt, exprt) instead")) exprt make_and(exprt a, exprt b); /// Returns true if \p expr has a pointer type and a value NULL; it also returns diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 1da4141bd14..b52dfca7ab4 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -80,12 +80,37 @@ exprt disjunction(const exprt::operandst &op) } } +exprt conjunction(exprt a, exprt b) +{ + PRECONDITION(a.is_boolean() && b.is_boolean()); + if(b.is_constant()) + { + if(to_constant_expr(b).is_false()) + return false_exprt{}; + return a; + } + if(a.is_constant()) + { + if(to_constant_expr(a).is_false()) + return false_exprt{}; + return b; + } + if(b.id() == ID_and) + { + b.add_to_operands(std::move(a)); + return b; + } + return and_exprt{std::move(a), std::move(b)}; +} + exprt conjunction(const exprt::operandst &op) { if(op.empty()) return true_exprt(); else if(op.size()==1) return op.front(); + else if(op.size() == 2) + return conjunction(op[0], op[1]); else { return and_exprt(exprt::operandst(op)); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index e27e5b5f1e9..771fef67b0e 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2152,6 +2152,11 @@ class and_exprt:public multi_ary_exprt exprt conjunction(const exprt::operandst &); +/// Conjunction of two expressions. If the second is already an `and_exprt` +/// add to its operands instead of creating a new expression. If one is `true`, +/// return the other expression. If one is `false` returns `false`. +exprt conjunction(exprt a, exprt b); + template <> inline bool can_cast_expr(const exprt &base) {