diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 9675e9a9c31..8b249aafb63 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1087,8 +1087,12 @@ void java_object_factoryt::gen_nondet_init(
else
{
exprt within_bounds = interval.make_contains_expr(expr);
- if(!within_bounds.is_true())
+ if(
+ !within_bounds.is_constant() ||
+ !to_constant_expr(within_bounds).is_true())
+ {
assignments.add(code_assumet(std::move(within_bounds)));
+ }
}
if(
diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
index ae9f2272db1..ab49dc15896 100644
--- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
+++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
@@ -69,7 +69,8 @@ static bool is_call_to(
static bool is_assume_false(goto_programt::const_targett inst)
{
- return inst->is_assume() && inst->condition().is_false();
+ return inst->is_assume() && inst->condition().is_constant() &&
+ to_constant_expr(inst->condition()).is_false();
}
/// Interpret `program`, resolving classid comparisons assuming any actual
@@ -90,17 +91,20 @@ static goto_programt::const_targett interpret_classid_comparison(
{
exprt guard = pc->condition();
guard = resolve_classid_test(guard, actual_class_id, ns);
- if(guard.is_true())
+ if(!guard.is_constant())
+ {
+ // Can't resolve the test, so exit here:
+ return pc;
+ }
+ else if(to_constant_expr(guard).is_true())
{
REQUIRE(pc->targets.begin() != pc->targets.end());
pc = *(pc->targets.begin());
}
- else if(guard.is_false())
- ++pc;
else
{
- // Can't resolve the test, so exit here:
- return pc;
+ CHECK_RETURN(to_constant_expr(guard).is_false());
+ ++pc;
}
}
else if(pc->type() == SKIP)
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 80b9c778a45..e0e2efbd816 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -183,8 +183,8 @@ void constant_propagator_domaint::transform(
else
g = not_exprt(from->condition());
partial_evaluate(values, g, ns);
- if(g.is_false())
- values.set_to_bottom();
+ if(g.is_constant() && to_constant_expr(g).is_false())
+ values.set_to_bottom();
else
two_way_propagate_rec(g, ns, cp);
}
@@ -376,7 +376,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
// x != FALSE ==> x == TRUE
- if(rhs.is_zero() || rhs.is_false())
+ if(to_constant_expr(rhs).is_zero() || to_constant_expr(rhs).is_false())
rhs = from_integer(1, rhs.type());
else
rhs = from_integer(0, rhs.type());
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 7687ee51e5c..7efe922c09d 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -349,7 +349,7 @@ void custom_bitvector_domaint::transform(
{
if(
lhs.is_constant() &&
- is_null_pointer(to_constant_expr(lhs))) // NULL means all
+ to_constant_expr(lhs).is_null_pointer()) // NULL means all
{
if(mode==modet::CLEAR_MAY)
{
@@ -478,7 +478,7 @@ void custom_bitvector_domaint::transform(
{
if(
lhs.is_constant() &&
- is_null_pointer(to_constant_expr(lhs))) // NULL means all
+ to_constant_expr(lhs).is_null_pointer()) // NULL means all
{
if(mode==modet::CLEAR_MAY)
{
@@ -530,7 +530,7 @@ void custom_bitvector_domaint::transform(
const exprt result2 = simplify_expr(eval(guard, cba), ns);
- if(result2.is_false())
+ if(result2.is_constant() && to_constant_expr(result2).is_false())
make_bottom();
}
break;
@@ -716,7 +716,7 @@ exprt custom_bitvector_domaint::eval(
if(
pointer.is_constant() &&
- is_null_pointer(to_constant_expr(pointer))) // NULL means all
+ to_constant_expr(pointer).is_null_pointer()) // NULL means all
{
if(src.id() == ID_get_may)
{
@@ -814,12 +814,12 @@ void custom_bitvector_analysist::check(
if(use_xml)
{
out << "<result status=\"";
- if(result.is_true())
+ if(!result.is_constant())
+ out << "UNKNOWN";
+ else if(to_constant_expr(result).is_true())
out << "SUCCESS";
- else if(result.is_false())
- out << "FAILURE";
else
- out << "UNKNOWN";
+ out << "FAILURE";
out << "\">\n";
out << xml(i_it->source_location());
out << "<description>"
@@ -838,12 +838,12 @@ void custom_bitvector_analysist::check(
out << '\n';
}
- if(result.is_true())
+ if(!result.is_constant())
+ unknown++;
+ else if(to_constant_expr(result).is_true())
pass++;
- else if(result.is_false())
- fail++;
else
- unknown++;
+ fail++;
}
if(!use_xml)
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index a47497dddc4..55605acf716 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -116,17 +116,17 @@ void rw_range_sett::get_objects_if(
const range_spect &range_start,
const range_spect &size)
{
- if(if_expr.cond().is_false())
- get_objects_rec(mode, if_expr.false_case(), range_start, size);
- else if(if_expr.cond().is_true())
- get_objects_rec(mode, if_expr.true_case(), range_start, size);
- else
+ if(!if_expr.cond().is_constant())
{
get_objects_rec(get_modet::READ, if_expr.cond());
get_objects_rec(mode, if_expr.false_case(), range_start, size);
get_objects_rec(mode, if_expr.true_case(), range_start, size);
}
+ else if(to_constant_expr(if_expr.cond()).is_false())
+ get_objects_rec(mode, if_expr.false_case(), range_start, size);
+ else
+ get_objects_rec(mode, if_expr.true_case(), range_start, size);
}
void rw_range_sett::get_objects_dereference(
@@ -735,11 +735,7 @@ void rw_guarded_range_set_value_sett::get_objects_if(
const range_spect &range_start,
const range_spect &size)
{
- if(if_expr.cond().is_false())
- get_objects_rec(mode, if_expr.false_case(), range_start, size);
- else if(if_expr.cond().is_true())
- get_objects_rec(mode, if_expr.true_case(), range_start, size);
- else
+ if(!if_expr.cond().is_constant())
{
get_objects_rec(get_modet::READ, if_expr.cond());
@@ -753,6 +749,10 @@ void rw_guarded_range_set_value_sett::get_objects_if(
get_objects_rec(mode, if_expr.true_case(), range_start, size);
guard = std::move(copy);
}
+ else if(to_constant_expr(if_expr.cond()).is_false())
+ get_objects_rec(mode, if_expr.false_case(), range_start, size);
+ else
+ get_objects_rec(mode, if_expr.true_case(), range_start, size);
}
void rw_guarded_range_set_value_sett::add(
diff --git a/src/analyses/guard_bdd.cpp b/src/analyses/guard_bdd.cpp
index 1e69cb65a1a..55131d7b9da 100644
--- a/src/analyses/guard_bdd.cpp
+++ b/src/analyses/guard_bdd.cpp
@@ -44,7 +44,7 @@ exprt guard_bddt::guard_expr(exprt expr) const
}
else
{
- if(expr.is_false())
+ if(expr.is_constant() && to_constant_expr(expr).is_false())
{
return boolean_negate(as_expr());
}
diff --git a/src/analyses/guard_expr.cpp b/src/analyses/guard_expr.cpp
index b44e4e726fe..94ee1371dc7 100644
--- a/src/analyses/guard_expr.cpp
+++ b/src/analyses/guard_expr.cpp
@@ -24,7 +24,7 @@ exprt guard_exprt::guard_expr(exprt expr) const
}
else
{
- if(expr.is_false())
+ if(expr.is_constant() && to_constant_expr(expr).is_false())
{
return boolean_negate(as_expr());
}
@@ -39,9 +39,10 @@ void guard_exprt::add(const exprt &expr)
{
PRECONDITION(expr.is_boolean());
- if(is_false() || expr.is_true())
+ if(is_false() || (expr.is_constant() && to_constant_expr(expr).is_true()))
return;
- else if(is_true() || expr.is_false())
+ else if(
+ is_true() || (expr.is_constant() && to_constant_expr(expr).is_false()))
{
this->expr = expr;
@@ -198,7 +199,9 @@ guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2)
if(tmp != and_expr1)
{
- if(and_expr1.is_true() || and_expr2.is_true())
+ if(
+ (and_expr1.is_constant() && to_constant_expr(and_expr1).is_true()) ||
+ (and_expr2.is_constant() && to_constant_expr(and_expr2).is_true()))
{
}
else
diff --git a/src/analyses/guard_expr.h b/src/analyses/guard_expr.h
index ea5d227eee7..3d89ee1d6d0 100644
--- a/src/analyses/guard_expr.h
+++ b/src/analyses/guard_expr.h
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
#ifndef CPROVER_ANALYSES_GUARD_EXPR_H
#define CPROVER_ANALYSES_GUARD_EXPR_H
-#include <util/expr.h>
+#include <util/std_expr.h>
/// This is unused by this implementation of guards, but can be used by other
/// implementations of the same interface.
@@ -59,12 +59,12 @@ class guard_exprt
bool is_true() const
{
- return expr.is_true();
+ return expr.is_constant() && to_constant_expr(expr).is_true();
}
bool is_false() const
{
- return expr.is_false();
+ return expr.is_constant() && to_constant_expr(expr).is_false();
}
friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);
diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp
index f9cc3cf1906..755904f19bb 100644
--- a/src/analyses/interval_analysis.cpp
+++ b/src/analyses/interval_analysis.cpp
@@ -46,7 +46,10 @@ void instrument_intervals(
{
goto_programt::const_targett previous = std::prev(i_it);
- if(previous->is_goto() && !previous->condition().is_true())
+ if(
+ previous->is_goto() &&
+ (!previous->condition().is_constant() ||
+ !to_constant_expr(previous->condition()).is_true()))
{
// we follow a branch, instrument
}
@@ -69,7 +72,7 @@ void instrument_intervals(
for(const auto &symbol_expr : symbols)
{
exprt tmp=d.make_expression(symbol_expr);
- if(!tmp.is_true())
+ if(!tmp.is_constant() || !to_constant_expr(tmp).is_true())
assertion.push_back(tmp);
}
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 4594a4d2e94..8c15050968a 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -501,7 +501,8 @@ bool interval_domaint::ai_simplify(
// of when condition is true
if(!a.join(d)) // If d (this) is included in a...
{ // Then the condition is always true
- unchanged=condition.is_true();
+ unchanged =
+ condition.is_constant() && to_constant_expr(condition).is_true();
condition = true_exprt();
}
}
@@ -514,7 +515,8 @@ bool interval_domaint::ai_simplify(
d.assume(not_exprt(condition), ns); // Restrict to when condition is false
if(d.is_bottom()) // If there there are none...
{ // Then the condition is always true
- unchanged=condition.is_true();
+ unchanged =
+ condition.is_constant() && to_constant_expr(condition).is_true();
condition = true_exprt();
}
}
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index 49c3c8b2324..a8bc6086ea0 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -121,7 +121,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
if(expr.is_constant())
{
// NULL?
- if(is_null_pointer(to_constant_expr(expr)))
+ if(to_constant_expr(expr).is_null_pointer())
return "0";
const auto i = numeric_cast<mp_integer>(expr);
@@ -394,14 +394,17 @@ void invariant_sett::strengthen_rec(const exprt &expr)
return;
}
- if(expr.is_true())
- {
- // do nothing, it's useless
- }
- else if(expr.is_false())
+ if(expr.is_constant())
{
- // wow, that's strong
- make_false();
+ if(to_constant_expr(expr).is_true())
+ {
+ // do nothing, it's useless
+ }
+ else
+ {
+ // wow, that's strong
+ make_false();
+ }
}
else if(expr.id()==ID_not)
{
@@ -596,7 +599,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
if(is_false) // can't get any stronger
return tvt(true);
- if(expr.is_true())
+ if(expr.is_constant() && to_constant_expr(expr).is_true())
return tvt(true);
else if(expr.id()==ID_not)
{
@@ -701,15 +704,18 @@ void invariant_sett::nnf(exprt &expr, bool negate)
if(!expr.is_boolean())
throw "nnf: non-Boolean expression";
- if(expr.is_true())
- {
- if(negate)
- expr=false_exprt();
- }
- else if(expr.is_false())
+ if(expr.is_constant())
{
- if(negate)
- expr=true_exprt();
+ if(to_constant_expr(expr).is_true())
+ {
+ if(negate)
+ expr = false_exprt();
+ }
+ else
+ {
+ if(negate)
+ expr = true_exprt();
+ }
}
else if(expr.id()==ID_not)
{
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 59d0e110f23..e7f8e89a937 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -115,7 +115,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
{
if(rhs.is_constant())
{
- if(rhs.is_zero())
+ if(to_constant_expr(rhs).is_zero())
return flagst::mk_null();
else
return flagst::mk_integer_address();
diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp
index 60bcabb783f..f7645461b85 100644
--- a/src/analyses/local_cfg.cpp
+++ b/src/analyses/local_cfg.cpp
@@ -35,8 +35,12 @@ void local_cfgt::build(const goto_programt &goto_program)
switch(instruction.type())
{
case GOTO:
- if(!instruction.condition().is_true())
+ if(
+ !instruction.condition().is_constant() ||
+ !to_constant_expr(instruction.condition()).is_true())
+ {
node.successors.push_back(loc_nr+1);
+ }
for(const auto &target : instruction.targets)
{
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index d55b5d57293..f5249308af8 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -171,7 +171,7 @@ void local_may_aliast::get_rec(
{
if(rhs.is_constant())
{
- if(rhs.is_zero())
+ if(to_constant_expr(rhs).is_zero())
dest.insert(objects.number(exprt(ID_null_object)));
else
dest.insert(objects.number(exprt(ID_integer_address_object)));
diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp
index 4eedf918105..461b8fe59ff 100644
--- a/src/analyses/variable-sensitivity/abstract_environment.cpp
+++ b/src/analyses/variable-sensitivity/abstract_environment.cpp
@@ -269,7 +269,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
// Should be of the right type
INVARIANT(assumption.is_boolean(), "simplification preserves type");
- if(assumption.is_false())
+ if(assumption.is_constant() && to_constant_expr(assumption).is_false())
{
bool currently_bottom = is_bottom();
make_bottom();
@@ -573,10 +573,10 @@ static auto inverse_operations =
static exprt invert_result(const exprt &result)
{
- if(!result.is_boolean())
+ if(!result.is_boolean() || !result.is_constant())
return result;
- if(result.is_true())
+ if(to_constant_expr(result).is_true())
return false_exprt();
return true_exprt();
}
@@ -634,7 +634,7 @@ exprt assume_and(
for(auto const &operand : and_expr.operands())
{
auto result = env.do_assume(operand, ns);
- if(result.is_false())
+ if(result.is_constant() && to_constant_expr(result).is_false())
return result;
nil |= result.is_nil();
}
@@ -827,7 +827,7 @@ exprt assume_less_than(
auto reduced_le_expr =
binary_relation_exprt(left_lower, expr.id(), right_upper);
auto result = env.eval(reduced_le_expr, ns)->to_constant();
- if(result.is_true())
+ if(result.is_constant() && to_constant_expr(result).is_true())
{
if(is_assignable(operands.lhs))
{
diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp
index 2b339a3f5f3..e2e47a79cec 100644
--- a/src/analyses/variable-sensitivity/abstract_value_object.cpp
+++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp
@@ -664,8 +664,10 @@ class value_set_evaluator
for(const auto &v : condition)
{
auto expr = v->to_constant();
- all_true = all_true && expr.is_true();
- all_false = all_false && expr.is_false();
+ all_true =
+ all_true && expr.is_constant() && to_constant_expr(expr).is_true();
+ all_false =
+ all_false && expr.is_constant() && to_constant_expr(expr).is_false();
}
auto indeterminate = !all_true && !all_false;
diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp
index 1d766adf82a..0db1689bcd2 100644
--- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp
@@ -426,7 +426,7 @@ exprt full_array_abstract_objectt::to_predicate_internal(
auto index = index_exprt(name, ii);
auto field_expr = field.second->to_predicate(index);
- if(!field_expr.is_true())
+ if(!field_expr.is_constant() || !to_constant_expr(field_expr).is_true())
all_predicates.push_back(field_expr);
}
diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
index ab1ae403d46..5158a773472 100644
--- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
@@ -312,7 +312,7 @@ exprt full_struct_abstract_objectt::to_predicate_internal(
member_exprt(name, compound_type.get_component(field.first));
auto field_expr = field.second->to_predicate(field_name);
- if(!field_expr.is_true())
+ if(!field_expr.is_constant() || !to_constant_expr(field_expr).is_true())
all_predicates.push_back(field_expr);
}
diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp
index 51f738c5109..2a23434e576 100644
--- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp
+++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp
@@ -45,8 +45,9 @@ class interval_index_ranget : public index_range_implementationt
{
index = next;
next = next_element(next, ns);
- return simplify_expr(binary_predicate_exprt(index, ID_le, upper), ns)
- .is_true();
+ auto simp_expr =
+ simplify_expr(binary_predicate_exprt(index, ID_le, upper), ns);
+ return simp_expr.is_constant() && to_constant_expr(simp_expr).is_true();
}
index_range_implementation_ptrt reset() const override
@@ -239,11 +240,15 @@ bool new_interval_is_top(const constant_interval_exprt &e)
if(e.is_top())
return true;
- if(e.get_lower().is_false() && e.get_upper().is_true())
+ if(!e.get_lower().is_constant() || !e.get_upper().is_constant())
+ return false;
+
+ const constant_exprt &lower = to_constant_expr(e.get_lower());
+ const constant_exprt &upper = to_constant_expr(e.get_upper());
+
+ if(lower.is_false() && upper.is_true())
return true;
- if(
- e.type().id() == ID_c_bool && e.get_lower().is_zero() &&
- e.get_upper().is_one())
+ if(e.type().id() == ID_c_bool && lower.is_zero() && upper.is_one())
return true;
return false;
diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp
index 5357fc3046a..5df5e2b2921 100644
--- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp
@@ -441,11 +441,13 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
set,
[](const abstract_value_objectt &value) {
auto c = value.to_constant();
- return c.is_false() || (c.id() == ID_min_value);
+ return (c.is_constant() && to_constant_expr(c).is_false()) ||
+ (c.id() == ID_min_value);
},
[](const abstract_value_objectt &value) {
auto c = value.to_constant();
- return c.is_true() || (c.id() == ID_max_value);
+ return (c.is_constant() && to_constant_expr(c).is_true()) ||
+ (c.id() == ID_max_value);
});
}
@@ -455,11 +457,13 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
set,
[](const abstract_value_objectt &value) {
auto c = value.to_constant();
- return c.is_zero() || (c.id() == ID_min_value);
+ return (c.is_constant() && to_constant_expr(c).is_zero()) ||
+ (c.id() == ID_min_value);
},
[](const abstract_value_objectt &value) {
auto c = value.to_constant();
- return c.is_one() || (c.id() == ID_max_value);
+ return (c.is_constant() && to_constant_expr(c).is_one()) ||
+ (c.id() == ID_max_value);
});
}
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 873e857af8f..c978690da82 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -565,11 +565,11 @@ void c_typecastt::implicit_typecast_followed(
{
// special case: 0 == NULL
- if(simplify_expr(expr, ns).is_zero() && (
- src_type.id()==ID_unsignedbv ||
- src_type.id()==ID_signedbv ||
- src_type.id()==ID_natural ||
- src_type.id()==ID_integer))
+ auto simp_expr = simplify_expr(expr, ns);
+ if(
+ simp_expr.is_constant() && to_constant_expr(simp_expr).is_zero() &&
+ (src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
+ src_type.id() == ID_natural || src_type.id() == ID_integer))
{
expr = null_pointer_exprt{to_pointer_type(orig_dest_type)};
return; // ok
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index f11e08f7e14..b101d364a3b 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -312,7 +312,9 @@ static bool is_instantiation_of_flexible_array(
return old_array_type.element_type() == new_array_type.element_type() &&
old_array_type.get_bool(ID_C_flexible_array_member) &&
new_array_type.get_bool(ID_C_flexible_array_member) &&
- (old_array_type.size().is_nil() || old_array_type.size().is_zero());
+ (old_array_type.size().is_nil() ||
+ (old_array_type.size().is_constant() &&
+ to_constant_expr(old_array_type.size()).is_zero()));
}
void c_typecheck_baset::typecheck_redefinition_non_type(
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 6e348392845..d10db37a819 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -113,7 +113,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
implicit_typecast_bool(code.op0());
make_constant(code.op0());
- if(code.op0().is_false())
+ if(code.op0().is_constant() && to_constant_expr(code.op0()).is_false())
{
// failed
error().source_location = code.find_source_location();
@@ -948,7 +948,7 @@ void c_typecheck_baset::typecheck_conditional_targets(
auto &condition = conditional_target_group.condition();
typecheck_spec_condition(condition);
- if(condition.is_true())
+ if(condition.is_constant() && to_constant_expr(condition).is_true())
{
// if the condition is trivially true,
// simplify expr and expose the bare expressions
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 5e398ab2698..fa77f0ef433 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -258,7 +258,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
subtypes[1].remove(ID_C_volatile);
subtypes[1].remove(ID_C_restricted);
- expr = make_boolean_expr(gcc_types_compatible_p(subtypes[0], subtypes[1]));
+ expr = constant_exprt{gcc_types_compatible_p(subtypes[0], subtypes[1])};
expr.add_source_location()=source_location;
}
else if(expr.id()==ID_clang_builtin_convertvector)
@@ -1435,18 +1435,24 @@ void c_typecheck_baset::typecheck_expr_rel(
else
{
// pointer and zero
- if(type0.id()==ID_pointer &&
- simplify_expr(op1, *this).is_zero())
+ if(type0.id() == ID_pointer)
{
- op1 = null_pointer_exprt{to_pointer_type(type0)};
- return;
+ auto simp_op1 = simplify_expr(op1, *this);
+ if(simp_op1.is_constant() && to_constant_expr(simp_op1).is_zero())
+ {
+ op1 = null_pointer_exprt{to_pointer_type(type0)};
+ return;
+ }
}
- if(type1.id()==ID_pointer &&
- simplify_expr(op0, *this).is_zero())
+ if(type1.id() == ID_pointer)
{
- op0 = null_pointer_exprt{to_pointer_type(type1)};
- return;
+ auto simp_op0 = simplify_expr(op0, *this);
+ if(simp_op0.is_constant() && to_constant_expr(simp_op0).is_zero())
+ {
+ op0 = null_pointer_exprt{to_pointer_type(type1)};
+ return;
+ }
}
// pointer and integer
@@ -1672,13 +1678,13 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
// (at least that's how GCC behaves)
if(
to_pointer_type(operands[1].type()).base_type().id() == ID_empty &&
- tmp1.is_constant() && is_null_pointer(to_constant_expr(tmp1)))
+ tmp1.is_constant() && to_constant_expr(tmp1).is_null_pointer())
{
implicit_typecast(operands[1], operands[2].type());
}
else if(
to_pointer_type(operands[2].type()).base_type().id() == ID_empty &&
- tmp2.is_constant() && is_null_pointer(to_constant_expr(tmp2)))
+ tmp2.is_constant() && to_constant_expr(tmp2).is_null_pointer())
{
implicit_typecast(operands[2], operands[1].type());
}
@@ -3583,9 +3589,9 @@ exprt c_typecheck_baset::do_special_functions(
mp_integer arg1;
- if(expr.arguments()[1].is_true())
+ if(to_constant_expr(expr.arguments()[1]).is_true())
arg1=1;
- else if(expr.arguments()[1].is_false())
+ else if(to_constant_expr(expr.arguments()[1]).is_false())
arg1=0;
else if(to_integer(to_constant_expr(expr.arguments()[1]), arg1))
{
@@ -3627,7 +3633,7 @@ exprt c_typecheck_baset::do_special_functions(
typecast_exprt::conditional_cast(expr.arguments()[0], bool_typet());
make_constant(arg0);
- if(arg0.is_true())
+ if(to_constant_expr(arg0).is_true())
return expr.arguments()[1];
else
return expr.arguments()[2];
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index e17d59966c7..8d49ba2eead 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -405,8 +405,10 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
if(index>=dest->operands().size())
{
if(
- type.id() == ID_array && (to_array_type(type).size().is_zero() ||
- to_array_type(type).size().is_nil()))
+ type.id() == ID_array &&
+ ((to_array_type(type).size().is_constant() &&
+ to_constant_expr(to_array_type(type).size()).is_zero()) ||
+ to_array_type(type).size().is_nil()))
{
const typet &element_type = to_array_type(type).element_type();
@@ -673,10 +675,11 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
// in case of a variable-length array consume all remaining
// initializer elements
- if(vla_permitted &&
- dest_type.id()==ID_array &&
- (to_array_type(dest_type).size().is_zero() ||
- to_array_type(dest_type).size().is_nil()))
+ if(
+ vla_permitted && dest_type.id() == ID_array &&
+ ((to_array_type(dest_type).size().is_constant() &&
+ to_constant_expr(to_array_type(dest_type).size()).is_zero()) ||
+ to_array_type(dest_type).size().is_nil()))
{
value.id(ID_initializer_list);
value.operands().clear();
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 02e50709308..43a1a2f3a8e 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1069,12 +1069,12 @@ void c_typecheck_baset::typecheck_compound_body(
assertion = typecast_exprt(assertion, bool_typet());
make_constant(assertion);
- if(assertion.is_false())
+ if(to_constant_expr(assertion).is_false())
{
throw errort().with_location(it->source_location())
<< "failed _Static_assert";
}
- else if(!assertion.is_true())
+ else if(!to_constant_expr(assertion).is_true())
{
// should warn/complain
}
@@ -1243,9 +1243,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
typecheck_expr(tmp_v);
add_rounding_mode(tmp_v);
simplify(tmp_v, *this);
- if(tmp_v.is_true())
+ if(tmp_v.is_constant() && to_constant_expr(tmp_v).is_true())
value=1;
- else if(tmp_v.is_false())
+ else if(tmp_v.is_constant() && to_constant_expr(tmp_v).is_false())
value=0;
else if(
tmp_v.is_constant() && !to_integer(to_constant_expr(tmp_v), value))
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 3257a74f270..b7042177813 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1268,7 +1268,8 @@ std::string expr2ct::convert_complex(
unsigned precedence)
{
if(
- src.operands().size() == 2 && to_binary_expr(src).op0().is_zero() &&
+ src.operands().size() == 2 && to_binary_expr(src).op0().is_constant() &&
+ to_constant_expr(to_binary_expr(src).op0()).is_zero() &&
to_binary_expr(src).op1().is_constant())
{
// This is believed to be gcc only; check if this is sensible
@@ -1983,7 +1984,7 @@ std::string expr2ct::convert_constant(
}
else if(type.id()==ID_pointer)
{
- if(is_null_pointer(src))
+ if(src.is_null_pointer())
{
if(configuration.use_library_macros)
dest = "NULL";
@@ -3531,7 +3532,7 @@ std::string expr2ct::convert_conditional_target_group(const exprt &src)
std::string dest;
unsigned p;
const auto &cond = src.operands().front();
- if(!cond.is_true())
+ if(!cond.is_constant() || !to_constant_expr(cond).is_true())
{
dest += convert_with_precedence(cond, p);
dest += ": ";
@@ -3751,8 +3752,12 @@ std::string expr2ct::convert_with_precedence(
if(object.id() == ID_label)
return "&&" + object.get_string(ID_identifier);
- else if(object.id() == ID_index && to_index_expr(object).index().is_zero())
+ else if(
+ object.id() == ID_index && to_index_expr(object).index().is_constant() &&
+ to_constant_expr(to_index_expr(object).index()).is_zero())
+ {
return convert(to_index_expr(object).array());
+ }
else if(to_pointer_type(src.type()).base_type().id() == ID_code)
return convert_unary(to_unary_expr(src), "", precedence = 15);
else
diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp
index bf864fcdb1e..89575f0ee29 100644
--- a/src/ansi-c/goto-conversion/builtin_functions.cpp
+++ b/src/ansi-c/goto-conversion/builtin_functions.cpp
@@ -606,7 +606,8 @@ exprt make_va_list(const exprt &expr)
}
while(result.type().id() == ID_array &&
- to_array_type(result.type()).size().is_one())
+ to_array_type(result.type()).size().is_constant() &&
+ to_constant_expr(to_array_type(result.type()).size()).is_one())
{
result = index_exprt{result, from_integer(0, c_index_type())};
}
diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp
index f829ebeda7e..0fde03f8899 100644
--- a/src/ansi-c/goto-conversion/goto_check_c.cpp
+++ b/src/ansi-c/goto-conversion/goto_check_c.cpp
@@ -1685,7 +1685,8 @@ void goto_check_ct::bounds_check_index(
}
else if(
expr.array().id() == ID_member &&
- (size.is_zero() || array_type.get_bool(ID_C_flexible_array_member)))
+ ((size.is_constant() && to_constant_expr(size).is_zero()) ||
+ array_type.get_bool(ID_C_flexible_array_member)))
{
// a variable sized struct member
//
@@ -1766,8 +1767,12 @@ void goto_check_ct::add_guarded_property(
enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
// throw away trivial properties?
- if(!retain_trivial && simplified_expr.is_true())
+ if(
+ !retain_trivial && simplified_expr.is_constant() &&
+ to_constant_expr(simplified_expr).is_true())
+ {
return;
+ }
// add the guard
exprt guarded_expr = guard(simplified_expr);
@@ -2245,7 +2250,8 @@ void goto_check_ct::goto_check(
// These are further 'exit points' of the program
const exprt simplified_guard = simplify_expr(i.condition(), ns);
if(
- enable_memory_cleanup_check && simplified_guard.is_false() &&
+ enable_memory_cleanup_check && simplified_guard.is_constant() &&
+ to_constant_expr(simplified_guard).is_false() &&
(function_identifier == "abort" || function_identifier == "exit" ||
function_identifier == "_Exit" ||
(i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
index c015c1fe414..1193f7eb6c9 100644
--- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp
+++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
@@ -114,13 +114,15 @@ void goto_convertt::rewrite_boolean(exprt &expr)
"' must be Boolean, but got ",
irep_pretty_diagnosticst{expr});
+ const source_locationt source_location = expr.find_source_location();
+
// re-write "a ==> b" into a?b:1
if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
{
expr = if_exprt{
std::move(implies->lhs()),
std::move(implies->rhs()),
- true_exprt{},
+ true_exprt{}.with_source_location(source_location),
bool_typet{}};
return;
}
@@ -135,6 +137,8 @@ void goto_convertt::rewrite_boolean(exprt &expr)
else // ID_or
tmp = false_exprt();
+ tmp.add_source_location() = source_location;
+
exprt::operandst &ops = expr.operands();
// start with last one
@@ -146,17 +150,21 @@ void goto_convertt::rewrite_boolean(exprt &expr)
DATA_INVARIANT_WITH_DIAGNOSTICS(
op.is_boolean(),
"boolean operators must have only boolean operands",
- expr.find_source_location());
+ source_location);
if(expr.id() == ID_and)
{
- if_exprt if_e(op, tmp, false_exprt());
+ exprt if_e =
+ if_exprt{op, tmp, false_exprt{}.with_source_location(source_location)}
+ .with_source_location(source_location);
tmp.swap(if_e);
continue;
}
if(expr.id() == ID_or)
{
- if_exprt if_e(op, true_exprt(), tmp);
+ exprt if_e =
+ if_exprt{op, true_exprt{}.with_source_location(source_location), tmp}
+ .with_source_location(source_location);
tmp.swap(if_e);
continue;
}
@@ -220,13 +228,13 @@ goto_convertt::clean_expr_resultt goto_convertt::clean_expr(
{
exprt tmp_cond=if_expr.cond();
simplify(tmp_cond, ns);
- if(tmp_cond.is_true())
+ if(tmp_cond.is_constant() && to_constant_expr(tmp_cond).is_true())
{
clean_expr(if_expr.true_case(), dest, result_is_used);
expr=if_expr.true_case();
return;
}
- else if(tmp_cond.is_false())
+ else if(tmp_cond.is_constant() && to_constant_expr(tmp_cond).is_false())
{
clean_expr(if_expr.false_case(), dest, result_is_used);
expr=if_expr.false_case();
diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp
index f07ed0f424c..45992b93505 100644
--- a/src/ansi-c/goto-conversion/goto_convert.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert.cpp
@@ -419,7 +419,9 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
if(
it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
- !it_goto_y->condition().is_true() || it_goto_y->is_target())
+ !it_goto_y->condition().is_constant() ||
+ !to_constant_expr(it_goto_y->condition()).is_true() ||
+ it_goto_y->is_target())
{
continue;
}
@@ -700,7 +702,7 @@ void goto_convertt::convert(
typecast_exprt::conditional_cast(code.op0(), bool_typet());
simplify(assertion, ns);
INVARIANT_WITH_DIAGNOSTICS(
- !assertion.is_false(),
+ !assertion.is_constant() || !to_constant_expr(assertion).is_false(),
"static assertion " + id2string(get_string_constant(code.op1())),
code.op0().find_source_location());
}
@@ -743,7 +745,8 @@ void goto_convertt::convert_block(
// in a prior break/continue/return already, don't create dead code
if(
!dest.empty() && dest.instructions.back().is_goto() &&
- dest.instructions.back().condition().is_true())
+ dest.instructions.back().condition().is_constant() &&
+ to_constant_expr(dest.instructions.back().condition()).is_true())
{
// don't do destructors when we are unreachable
}
@@ -1774,7 +1777,8 @@ void goto_convertt::generate_ifthenelse(
// do guarded assertions directly
if(
is_size_one(true_case) && true_case.instructions.back().is_assert() &&
- true_case.instructions.back().condition().is_false() &&
+ true_case.instructions.back().condition().is_constant() &&
+ to_constant_expr(true_case.instructions.back().condition()).is_false() &&
true_case.instructions.back().labels.empty())
{
// The above conjunction deliberately excludes the instance
@@ -1792,7 +1796,8 @@ void goto_convertt::generate_ifthenelse(
// similarly, do guarded assertions directly
if(
is_size_one(false_case) && false_case.instructions.back().is_assert() &&
- false_case.instructions.back().condition().is_false() &&
+ false_case.instructions.back().condition().is_constant() &&
+ to_constant_expr(false_case.instructions.back().condition()).is_false() &&
false_case.instructions.back().labels.empty())
{
// The above conjunction deliberately excludes the instance
@@ -1812,7 +1817,11 @@ void goto_convertt::generate_ifthenelse(
if(
is_empty(false_case) && true_case.instructions.size() == 2 &&
true_case.instructions.front().is_assert() &&
- simplify_expr(true_case.instructions.front().condition(), ns).is_false() &&
+ simplify_expr(true_case.instructions.front().condition(), ns)
+ .is_constant() &&
+ to_constant_expr(
+ simplify_expr(true_case.instructions.front().condition(), ns))
+ .is_false() &&
true_case.instructions.front().labels.empty() &&
true_case.instructions.back().is_other() &&
true_case.instructions.back().get_other().get_statement() ==
diff --git a/src/ansi-c/goto-conversion/goto_convert_functions.cpp b/src/ansi-c/goto-conversion/goto_convert_functions.cpp
index 07a3c3713e1..8fa454f27ed 100644
--- a/src/ansi-c/goto-conversion/goto_convert_functions.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert_functions.cpp
@@ -96,8 +96,11 @@ void goto_convert_functionst::add_return(
// see if we have an unconditional goto at the end
if(!f.body.instructions.empty() &&
f.body.instructions.back().is_goto() &&
- f.body.instructions.back().guard.is_true())
+ f.body.instructions.back().guard.is_constant() &&
+ to_constant_expr(f.body.instructions.back().guard).is_true())
+ {
return;
+ }
#else
if(!f.body.instructions.empty())
@@ -108,7 +111,10 @@ void goto_convert_functionst::add_return(
while(true)
{
// unconditional goto, say from while(1)?
- if(last_instruction->is_goto() && last_instruction->condition().is_true())
+ if(
+ last_instruction->is_goto() &&
+ last_instruction->condition().is_constant() &&
+ to_constant_expr(last_instruction->condition()).is_true())
{
return;
}
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 59e320f7112..79e20d89187 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -1558,7 +1558,8 @@ pragma_packed:
{
init($$);
if(!PARSER.pragma_pack.empty() &&
- PARSER.pragma_pack.back().is_one())
+ PARSER.pragma_pack.back().is_constant() &&
+ to_constant_expr(PARSER.pragma_pack.back()).is_one())
set($$, ID_packed);
}
;
@@ -1762,7 +1763,8 @@ member_declaring_list:
if(parser_stack($2).id() != ID_struct &&
parser_stack($2).id() != ID_union &&
!PARSER.pragma_pack.empty() &&
- !PARSER.pragma_pack.back().is_zero())
+ (!PARSER.pragma_pack.back().is_constant() ||
+ !to_constant_expr(PARSER.pragma_pack.back()).is_zero()))
{
// communicate #pragma pack(n) alignment constraints by
// by both setting packing AND alignment for individual struct/union
diff --git a/src/ansi-c/printf_formatter.cpp b/src/ansi-c/printf_formatter.cpp
index 7ad8c06667c..d6a4dc741d3 100644
--- a/src/ansi-c/printf_formatter.cpp
+++ b/src/ansi-c/printf_formatter.cpp
@@ -215,7 +215,8 @@ void printf_formattert::process_format(std::ostream &out)
expr_try_dynamic_cast<index_exprt>(address_of->object()))
{
if(
- index_expr->index().is_zero() &&
+ index_expr->index().is_constant() &&
+ to_constant_expr(index_expr->index()).is_zero() &&
index_expr->array().id() == ID_string_constant)
{
out << format_constant(index_expr->array());
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
index 4328428b326..618bb1a09b4 100644
--- a/src/cpp/cpp_instantiate_template.cpp
+++ b/src/cpp/cpp_instantiate_template.cpp
@@ -67,9 +67,9 @@ std::string cpp_typecheckt::template_suffix(
// this must be a constant, which includes true/false
mp_integer i;
- if(e.is_true())
+ if(to_constant_expr(e).is_true())
i=1;
- else if(e.is_false())
+ else if(to_constant_expr(e).is_false())
i=0;
else if(to_integer(to_constant_expr(e), i))
{
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 41ec14ef5c2..af842155704 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -465,8 +465,10 @@ bool cpp_typecheckt::standard_conversion_pointer(
return false;
// integer 0 to NULL pointer conversion?
- if(simplify_expr(expr, *this).is_zero() &&
- expr.type().id()!=ID_pointer)
+ auto simp_expr = simplify_expr(expr, *this);
+ if(
+ simp_expr.is_constant() && to_constant_expr(simp_expr).is_zero() &&
+ expr.type().id() != ID_pointer)
{
new_expr=expr;
new_expr.set(ID_value, ID_NULL);
@@ -603,7 +605,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
if(expr.get_bool(ID_C_lvalue))
return false;
- if(expr.is_constant() && is_null_pointer(to_constant_expr(expr)))
+ if(expr.is_constant() && to_constant_expr(expr).is_null_pointer())
{
new_expr = typecast_exprt::conditional_cast(expr, type);
return true;
@@ -1857,7 +1859,8 @@ bool cpp_typecheckt::reinterpret_typecast(
type.id() == ID_pointer && !is_reference(type))
{
// integer to pointer
- if(simplify_expr(e, *this).is_zero())
+ auto simp_e = simplify_expr(e, *this);
+ if(simp_e.is_constant() && to_constant_expr(simp_e).is_zero())
{
// NULL
new_expr=e;
diff --git a/src/cpp/cpp_typecheck_method_bodies.cpp b/src/cpp/cpp_typecheck_method_bodies.cpp
index e8389d721be..13279619d45 100644
--- a/src/cpp/cpp_typecheck_method_bodies.cpp
+++ b/src/cpp/cpp_typecheck_method_bodies.cpp
@@ -39,10 +39,16 @@ void cpp_typecheckt::typecheck_method_bodies()
#ifdef DEBUG
std::cout << "convert_method_body: " << method_symbol.name << '\n';
std::cout << " is_not_nil: " << body.is_not_nil() << '\n';
- std::cout << " !is_zero: " << (!body.is_zero()) << '\n';
+ std::cout << " !is_zero: "
+ << (!body.is_constant() || !to_constant_expr(body).is_zero())
+ << '\n';
#endif
- if(body.is_not_nil() && !body.is_zero())
+ if(
+ body.is_not_nil() &&
+ (!body.is_constant() || !to_constant_expr(body).is_zero()))
+ {
convert_function(method_symbol);
+ }
}
old_instantiation_stack.swap(instantiation_stack);
diff --git a/src/cpp/cpp_typecheck_static_assert.cpp b/src/cpp/cpp_typecheck_static_assert.cpp
index a792c010355..394bd2dbe81 100644
--- a/src/cpp/cpp_typecheck_static_assert.cpp
+++ b/src/cpp/cpp_typecheck_static_assert.cpp
@@ -21,7 +21,7 @@ void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert)
implicit_typecast_bool(cpp_static_assert.op0());
make_constant(cpp_static_assert.op0());
- if(cpp_static_assert.op0().is_false())
+ if(to_constant_expr(cpp_static_assert.op0()).is_false())
{
// failed
error().source_location=cpp_static_assert.source_location();
diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp
index 8cb9e7b46a3..9197306f0b1 100644
--- a/src/cprover/bv_pointers_wide.cpp
+++ b/src/cprover/bv_pointers_wide.cpp
@@ -387,7 +387,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
{
const constant_exprt &c = to_constant_expr(expr);
- if(is_null_pointer(c))
+ if(c.is_null_pointer())
return encode(pointer_logic.get_null_object(), type);
else
{
diff --git a/src/cprover/inductiveness.cpp b/src/cprover/inductiveness.cpp
index 6f4484fae12..ee116d8c715 100644
--- a/src/cprover/inductiveness.cpp
+++ b/src/cprover/inductiveness.cpp
@@ -36,7 +36,7 @@ bool is_subsumed(
bool verbose,
const namespacet &ns)
{
- if(b.is_true())
+ if(b.is_constant() && to_constant_expr(b).is_true())
return true; // anything subsumes 'true'
if(a1.find(false_exprt()) != a1.end())
@@ -161,7 +161,7 @@ inductiveness_resultt inductiveness_check(
<< frame_ref.index << consolet::reset << ' ';
// trivially true?
- if(invariant.is_true())
+ if(invariant.is_constant() && to_constant_expr(invariant).is_true())
{
if(solver_options.verbose)
std::cout << "trivial\n";
diff --git a/src/cprover/instrument_contracts.cpp b/src/cprover/instrument_contracts.cpp
index 88dc0f22ef0..69baa005b5a 100644
--- a/src/cprover/instrument_contracts.cpp
+++ b/src/cprover/instrument_contracts.cpp
@@ -110,12 +110,14 @@ exprt assigns_match(const exprt &assigns, const exprt &lhs)
if(lhs.id() == ID_member)
{
- if(assigns_match(assigns, to_member_expr(lhs).struct_op()).is_true())
+ exprt struct_op = assigns_match(assigns, to_member_expr(lhs).struct_op());
+ if(struct_op.is_constant() && to_constant_expr(struct_op).is_true())
return true_exprt();
}
else if(lhs.id() == ID_index)
{
- if(assigns_match(assigns, to_index_expr(lhs).array()).is_true())
+ exprt array = assigns_match(assigns, to_index_expr(lhs).array());
+ if(array.is_constant() && to_constant_expr(array).is_true())
return true_exprt();
}
@@ -169,7 +171,7 @@ static exprt make_assigns_assertion(
auto match = assigns_match(a, lhs);
// trivial?
- if(match.is_true())
+ if(match.is_constant() && to_constant_expr(match).is_true())
return true_exprt();
disjuncts.push_back(std::move(match));
diff --git a/src/cprover/may_alias.cpp b/src/cprover/may_alias.cpp
index 046fbbcd84c..55e1fedfbab 100644
--- a/src/cprover/may_alias.cpp
+++ b/src/cprover/may_alias.cpp
@@ -179,8 +179,12 @@ same_address(const exprt &a, const exprt &b, const namespacet &ns)
CHECK_RETURN(base_same_address.has_value());
- if(base_same_address->is_false())
+ if(
+ base_same_address->is_constant() &&
+ to_constant_expr(*base_same_address).is_false())
+ {
return false_expr;
+ }
else
{
return and_exprt(
diff --git a/src/cprover/simplify_state_expr.cpp b/src/cprover/simplify_state_expr.cpp
index d11f031a8b5..146d4d8806e 100644
--- a/src/cprover/simplify_state_expr.cpp
+++ b/src/cprover/simplify_state_expr.cpp
@@ -73,7 +73,7 @@ exprt simplify_evaluate_update(
if(may_alias.has_value())
{
// 'simple' case
- if(may_alias->is_true())
+ if(may_alias->is_constant() && to_constant_expr(*may_alias).is_true())
{
// The object is known to be the same.
// (ς[A:=V])(A) --> V
@@ -83,7 +83,7 @@ exprt simplify_evaluate_update(
address_taken,
ns);
}
- else if(may_alias->is_false())
+ else if(may_alias->is_constant() && to_constant_expr(*may_alias).is_false())
{
// The object is known to be different.
// (ς[❝x❞:=V])(❝y❞) --> ς(❝y❞)
@@ -444,7 +444,7 @@ exprt simplify_writeable_object_expr(
else
{
const auto &symbol = ns.lookup(identifier);
- return make_boolean_expr(!symbol.type.get_bool(ID_C_constant));
+ return constant_exprt{!symbol.type.get_bool(ID_C_constant)};
}
}
@@ -680,7 +680,9 @@ exprt simplify_is_cstring_expr(
auto may_alias =
::may_alias(pointer, update_state_expr.address(), address_taken, ns);
- if(may_alias.has_value() && may_alias->is_false())
+ if(
+ may_alias.has_value() && may_alias->is_constant() &&
+ to_constant_expr(*may_alias).is_false())
{
// different objects
// cstring(s[x:=v], p) --> cstring(s, p)
@@ -690,7 +692,9 @@ exprt simplify_is_cstring_expr(
// maybe the same
// Are we writing zero?
- if(update_state_expr.new_value().is_zero())
+ if(
+ update_state_expr.new_value().is_constant() &&
+ to_constant_expr(update_state_expr.new_value()).is_zero())
{
// cstring(s[p:=0], q) --> if p alias q then true else cstring(s, q)
auto same_object = ::same_object(pointer, update_state_expr.address());
@@ -776,7 +780,9 @@ exprt simplify_cstrlen_expr(
auto may_be_same_object = ::may_be_same_object(
pointer, update_state_expr.address(), address_taken, ns);
- if(may_be_same_object.is_false())
+ if(
+ may_be_same_object.is_constant() &&
+ to_constant_expr(may_be_same_object).is_false())
{
// different objects
// cstrlen(s[x:=v], p) --> cstrlen(s, p)
diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp
index 56ef744c049..3d4e18e87f3 100644
--- a/src/cprover/state_encoding.cpp
+++ b/src/cprover/state_encoding.cpp
@@ -134,7 +134,9 @@ std::vector<symbol_exprt> state_encodingt::incoming_symbols(loct loc) const
// conditional jump from loc_in to loc?
if(
- loc_in->is_goto() && !loc_in->condition().is_true() &&
+ loc_in->is_goto() &&
+ (!loc_in->condition().is_constant() ||
+ !to_constant_expr(loc_in->condition()).is_true()) &&
loc != std::next(loc_in))
{
suffix = "T";
@@ -617,7 +619,9 @@ void state_encodingt::setup_incoming(const goto_functiont &goto_function)
forall_goto_program_instructions(it, goto_function.body)
{
auto next = std::next(it);
- if(it->is_goto() && it->condition().is_true())
+ if(
+ it->is_goto() && it->condition().is_constant() &&
+ to_constant_expr(it->condition()).is_true())
{
}
else if(next != goto_function.body.instructions.end())
@@ -1013,7 +1017,7 @@ void state_encodingt::encode(
// We produce ∅ when the 'other' branch is taken. Get the condition.
const auto &condition = loc->condition();
- if(condition.is_true())
+ if(condition.is_constant() && to_constant_expr(condition).is_true())
{
dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
}
diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp
index 9e9282f6de7..5d535a6e9a7 100644
--- a/src/goto-analyzer/static_verifier.cpp
+++ b/src/goto-analyzer/static_verifier.cpp
@@ -92,11 +92,11 @@ check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
}
domain.ai_simplify(e, ns);
- if(e.is_true())
+ if(e.is_constant() && to_constant_expr(e).is_true())
{
return ai_verifier_statust::TRUE;
}
- else if(e.is_false())
+ else if(e.is_constant() && to_constant_expr(e).is_false())
{
return ai_verifier_statust::FALSE_IF_REACHABLE;
}
diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp
index 55726c91e2b..d6960b84e2e 100644
--- a/src/goto-analyzer/taint_analysis.cpp
+++ b/src/goto-analyzer/taint_analysis.cpp
@@ -343,7 +343,8 @@ bool taint_analysist::operator()(
continue;
exprt result = custom_bitvector_analysis.eval(i_it->condition(), i_it);
- if(simplify_expr(std::move(result), ns).is_true())
+ exprt simp_result = simplify_expr(std::move(result), ns);
+ if(simp_result.is_constant() && to_constant_expr(simp_result).is_true())
continue;
if(first)
diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index 6e31d312d77..79dd9e58232 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -57,7 +57,9 @@ ssa_step_matches_failing_property(const irep_idt &property_id)
symex_target_equationt::SSA_stepst::const_iterator step,
const decision_proceduret &decision_procedure) {
return step->is_assert() && step->property_id == property_id &&
- decision_procedure.get(step->cond_handle).is_false();
+ decision_procedure.get(step->cond_handle).is_constant() &&
+ to_constant_expr(decision_procedure.get(step->cond_handle))
+ .is_false();
};
}
@@ -250,8 +252,10 @@ void update_properties_status_from_symex_target_equation(
// Don't update status of properties that are constant 'false';
// we wouldn't have traces for them.
- const auto status = step.cond_expr.is_true() ? property_statust::PASS
- : property_statust::UNKNOWN;
+ const auto status = (step.cond_expr.is_constant() &&
+ to_constant_expr(step.cond_expr).is_true())
+ ? property_statust::PASS
+ : property_statust::UNKNOWN;
auto emplace_result = properties.emplace(
property_id, property_infot{step.source.pc, step.comment, status});
diff --git a/src/goto-checker/counterexample_beautification.cpp b/src/goto-checker/counterexample_beautification.cpp
index 34bc7b0c191..4a15b2726bc 100644
--- a/src/goto-checker/counterexample_beautification.cpp
+++ b/src/goto-checker/counterexample_beautification.cpp
@@ -37,7 +37,8 @@ void counterexample_beautificationt::get_minimization_list(
it->is_assignment() &&
it->assignment_type == symex_targett::assignment_typet::STATE)
{
- if(!prop_conv.get(it->guard_handle).is_false())
+ exprt v = prop_conv.get(it->guard_handle);
+ if(!v.is_constant() || !to_constant_expr(v).is_false())
{
const typet &type = it->ssa_lhs.type();
@@ -75,9 +76,14 @@ counterexample_beautificationt::get_failed_property(
it != equation.SSA_steps.end();
it++)
{
+ if(!it->is_assert())
+ continue;
+
+ exprt g = prop_conv.get(it->guard_handle);
+ exprt c = prop_conv.get(it->cond_handle);
if(
- it->is_assert() && prop_conv.get(it->guard_handle).is_true() &&
- prop_conv.get(it->cond_handle).is_false())
+ g.is_constant() && to_constant_expr(g).is_true() && c.is_constant() &&
+ to_constant_expr(c).is_false())
{
return it;
}
diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp
index 7e70100657c..3c4407bd3b1 100644
--- a/src/goto-checker/goto_symex_fault_localizer.cpp
+++ b/src/goto-checker/goto_symex_fault_localizer.cpp
@@ -108,11 +108,12 @@ void goto_symex_fault_localizert::update_scores(
for(auto &l : localization_points)
{
auto &score = l.second->second;
- if(solver.get(l.first).is_true())
+ exprt v = solver.get(l.first);
+ if(v.is_constant() && to_constant_expr(v).is_true())
{
score++;
}
- else if(solver.get(l.first).is_false() && score > 0)
+ else if(v.is_constant() && to_constant_expr(v).is_false() && score > 0)
{
score--;
}
diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp
index 7dcc0fe1c40..1c10d3709c4 100644
--- a/src/goto-checker/goto_symex_property_decider.cpp
+++ b/src/goto-checker/goto_symex_property_decider.cpp
@@ -90,7 +90,8 @@ void goto_symex_property_decidert::add_constraint_from_goals(
{
if(
select_property(goal_pair.first) &&
- !goal_pair.second.condition.is_false())
+ (!goal_pair.second.condition.is_constant() ||
+ !to_constant_expr(goal_pair.second.condition).is_false()))
{
disjuncts.push_back(goal_pair.second.condition);
}
@@ -142,10 +143,9 @@ void goto_symex_property_decidert::update_properties_status_from_goals(
for(auto &goal_pair : goal_map)
{
auto &status = properties.at(goal_pair.first).status;
+ exprt v = solver->decision_procedure().get(goal_pair.second.condition);
if(
- solver->decision_procedure()
- .get(goal_pair.second.condition)
- .is_true() &&
+ v.is_constant() && to_constant_expr(v).is_true() &&
status != property_statust::FAIL)
{
status |= property_statust::FAIL;
diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
index 56bd0c198d6..66f5b954161 100644
--- a/src/goto-checker/symex_bmc.cpp
+++ b/src/goto-checker/symex_bmc.cpp
@@ -57,19 +57,21 @@ void symex_bmct::symex_step(
const goto_programt::const_targett cur_pc = state.source.pc;
const guardt cur_guard = state.guard;
- if(
- !state.guard.is_false() && state.source.pc->is_assume() &&
- simplify_expr(state.source.pc->condition(), ns).is_false())
+ if(!state.guard.is_false() && state.source.pc->is_assume())
{
- log.statistics() << "aborting path on assume(false) at "
- << state.source.pc->source_location() << " thread "
- << state.source.thread_nr;
-
- const irep_idt &c = state.source.pc->source_location().get_comment();
- if(!c.empty())
- log.statistics() << ": " << c;
-
- log.statistics() << log.eom;
+ exprt simp_cond = simplify_expr(state.source.pc->condition(), ns);
+ if(simp_cond.is_constant() && to_constant_expr(simp_cond).is_false())
+ {
+ log.statistics() << "aborting path on assume(false) at "
+ << state.source.pc->source_location() << " thread "
+ << state.source.thread_nr;
+
+ const irep_idt &c = state.source.pc->source_location().get_comment();
+ if(!c.empty())
+ log.statistics() << ": " << c;
+
+ log.statistics() << log.eom;
+ }
}
goto_symext::symex_step(get_goto_function, state);
@@ -88,7 +90,8 @@ void symex_bmct::symex_step(
// sure the goto is considered covered
if(
cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
- cur_pc->condition().is_true())
+ cur_pc->condition().is_constant() &&
+ to_constant_expr(cur_pc->condition()).is_true())
symex_coverage.covered(cur_pc, cur_pc->get_target());
else if(!state.guard.is_false())
symex_coverage.covered(cur_pc, state.source.pc);
@@ -111,8 +114,11 @@ void symex_bmct::merge_goto(
// could the branch possibly be taken?
!prev_guard.is_false() && !state.guard.is_false() &&
// branches only, no single-successor goto
- !prev_pc->condition().is_true())
+ (!prev_pc->condition().is_constant() ||
+ !to_constant_expr(prev_pc->condition()).is_true()))
+ {
symex_coverage.covered(prev_pc, state.source.pc);
+ }
}
bool symex_bmct::should_stop_unwind(
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 9fbeaa5875b..aee698f102c 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -44,7 +44,8 @@ goto_programt::targett acceleratet::find_back_jump(
for(const auto &t : loop)
{
if(
- t->is_goto() && t->condition().is_true() && t->targets.size() == 1 &&
+ t->is_goto() && t->condition().is_constant() &&
+ to_constant_expr(t->condition()).is_true() && t->targets.size() == 1 &&
t->targets.front() == loop_header &&
t->location_number > back_jump->location_number)
{
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index a0a6dcd37ad..8506de77737 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -256,7 +256,10 @@ exprt acceleration_utilst::precondition(patht &path)
// Ignore.
}
- if(!r_it->guard.is_true() && !r_it->guard.is_nil())
+ if(
+ (!r_it->guard.is_constant() ||
+ !to_constant_expr(r_it->guard).is_true()) &&
+ !r_it->guard.is_nil())
{
// The guard isn't constant true, so we need to accumulate that too.
ret=implies_exprt(r_it->guard, ret);
diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp
index 43256e6fc1a..9bc9eac5058 100644
--- a/src/goto-instrument/accelerate/cone_of_influence.cpp
+++ b/src/goto-instrument/accelerate/cone_of_influence.cpp
@@ -89,7 +89,9 @@ void cone_of_influencet::get_succs(
if(rit->is_goto())
{
- if(!rit->condition().is_false())
+ if(
+ !rit->condition().is_constant() ||
+ !to_constant_expr(rit->condition()).is_false())
{
// Branch can be taken.
for(goto_programt::targetst::const_iterator t=rit->targets.begin();
@@ -102,14 +104,18 @@ void cone_of_influencet::get_succs(
}
}
- if(rit->condition().is_true())
+ if(
+ rit->condition().is_constant() &&
+ to_constant_expr(rit->condition()).is_true())
{
return;
}
}
else if(rit->is_assume() || rit->is_assert())
{
- if(rit->condition().is_false())
+ if(
+ rit->condition().is_constant() &&
+ to_constant_expr(rit->condition()).is_false())
{
return;
}
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index 954be5565e6..93cc2d8fe34 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -789,7 +789,9 @@ void disjunctive_polynomial_accelerationt::build_path(
for(const auto &succ : succs)
{
exprt &distinguisher=distinguishing_points[succ];
- bool taken=scratch_program.eval(distinguisher).is_true();
+ exprt distinguisher_eval = scratch_program.eval(distinguisher);
+ bool taken = distinguisher_eval.is_constant() &&
+ to_constant_expr(distinguisher_eval).is_true();
if(taken)
{
@@ -992,7 +994,8 @@ void disjunctive_polynomial_accelerationt::record_path(
it != distinguishers.end();
++it)
{
- path_val[*it]=program.eval(*it).is_true();
+ exprt eval = program.eval(*it);
+ path_val[*it] = eval.is_constant() && to_constant_expr(eval).is_true();
}
accelerated_paths.push_back(path_val);
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 41a88788c58..f6801faac96 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -785,7 +785,10 @@ exprt polynomial_acceleratort::precondition(patht &path)
// Ignore.
}
- if(!r_it->guard.is_true() && !r_it->guard.is_nil())
+ if(
+ (!r_it->guard.is_constant() ||
+ !to_constant_expr(r_it->guard).is_true()) &&
+ !r_it->guard.is_nil())
{
// The guard isn't constant true, so we need to accumulate that too.
ret=implies_exprt(r_it->guard, ret);
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index eb645a5a9b1..c63242295d4 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -136,7 +136,9 @@ void sat_path_enumeratort::build_path(
for(const auto &succ : succs)
{
exprt &distinguisher=distinguishing_points[succ];
- bool taken=scratch_program.eval(distinguisher).is_true();
+ exprt distinguisher_eval = scratch_program.eval(distinguisher);
+ bool taken = distinguisher_eval.is_constant() &&
+ to_constant_expr(distinguisher_eval).is_true();
if(taken)
{
@@ -335,7 +337,10 @@ void sat_path_enumeratort::record_path(scratch_programt &program)
distinguish_valuest path_val;
for(const auto &expr : distinguishers)
- path_val[expr]=program.eval(expr).is_true();
+ {
+ exprt eval = program.eval(expr);
+ path_val[expr] = eval.is_constant() && to_constant_expr(eval).is_true();
+ }
accelerated_paths.push_back(path_val);
}
diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp
index ddbc688aa47..a797cdb67ca 100644
--- a/src/goto-instrument/call_sequences.cpp
+++ b/src/goto-instrument/call_sequences.cpp
@@ -231,8 +231,12 @@ void check_call_sequencet::operator()()
{
goto_programt::const_targett t=e.pc->get_target();
- if(e.pc->condition().is_true())
+ if(
+ e.pc->condition().is_constant() &&
+ to_constant_expr(e.pc->condition()).is_true())
+ {
e.pc=t;
+ }
else
{
e.pc++;
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index f99d87e4477..a2a6000f004 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -375,7 +375,9 @@ void code_contractst::check_apply_loop_contracts(
}
// TODO: Fix loop contract handling for do/while loops.
- if(loop_end->is_goto() && !loop_end->condition().is_true())
+ if(
+ loop_end->is_goto() && (!loop_end->condition().is_constant() ||
+ !to_constant_expr(loop_end->condition()).is_true()))
{
log.error() << "Loop contracts are unsupported on do/while loops: "
<< loop_head_location << messaget::eom;
@@ -782,7 +784,7 @@ void code_contractst::apply_function_contract(
// Generate: assume(ensures)
for(auto &clause : instantiated_ensures_clauses)
{
- if(clause.is_false())
+ if(clause.is_constant() && to_constant_expr(clause).is_false())
{
throw invalid_input_exceptiont(
std::string("Attempt to assume false at ")
@@ -1353,7 +1355,9 @@ void code_contractst::add_contract_check(
{
auto instantiated_clause =
to_lambda_expr(clause).application(instantiation_values);
- if(instantiated_clause.is_false())
+ if(
+ instantiated_clause.is_constant() &&
+ to_constant_expr(instantiated_clause).is_false())
{
throw invalid_input_exceptiont(
std::string("Attempt to assume false at ")
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp
index 505ca6c6695..e797707edd6 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp
@@ -156,7 +156,10 @@ void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log)
// IF TRUE GOTO HEAD
// EXIT: SKIP
// ```
- if(latch->has_condition() && !latch->condition().is_true())
+ if(
+ latch->has_condition() &&
+ (!latch->condition().is_constant() ||
+ !to_constant_expr(latch->condition()).is_true()))
{
const source_locationt &loc = latch->source_location();
const auto &exit =
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
index 8a97ef48fd0..41ad34547a4 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
@@ -110,8 +110,8 @@ void dfcc_contract_clauses_codegent::encode_assignable_target_group(
new_vars = cleaner.clean(condition, dest, language_mode);
// Jump target if condition is false
- auto goto_instruction = dest.add(
- goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
+ auto goto_instruction = dest.add(goto_programt::make_incomplete_goto(
+ boolean_negate(condition), source_location));
for(const auto &target : group.targets())
encode_assignable_target(language_mode, target, dest);
@@ -169,7 +169,7 @@ void dfcc_contract_clauses_codegent::encode_assignable_target(
arguments.emplace_back(size.value());
// is_ptr_to_ptr
- arguments.emplace_back(make_boolean_expr(target.type().id() == ID_pointer));
+ arguments.emplace_back(constant_exprt{target.type().id() == ID_pointer});
dest.add(
goto_programt::make_function_call(code_function_call, source_location));
@@ -199,8 +199,8 @@ void dfcc_contract_clauses_codegent::encode_freeable_target_group(
new_vars = cleaner.clean(condition, dest, language_mode);
// Jump target if condition is false
- auto goto_instruction = dest.add(
- goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
+ auto goto_instruction = dest.add(goto_programt::make_incomplete_goto(
+ boolean_negate(condition), source_location));
for(const auto &target : group.targets())
encode_freeable_target(language_mode, target, dest);
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
index 45d83370521..fe4c425ee61 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
@@ -282,8 +282,8 @@ void dfcc_wrapper_programt::encode_requires_write_set()
addr_of_requires_write_set,
from_integer(0, size_type()),
from_integer(0, size_type()),
- make_boolean_expr(check_mode),
- make_boolean_expr(!check_mode),
+ constant_exprt{check_mode},
+ constant_exprt{!check_mode},
false_exprt(),
false_exprt(),
true_exprt(),
@@ -355,8 +355,8 @@ void dfcc_wrapper_programt::encode_ensures_write_set()
from_integer(0, size_type()),
false_exprt(),
false_exprt(),
- make_boolean_expr(!check_mode),
- make_boolean_expr(check_mode),
+ constant_exprt{!check_mode},
+ constant_exprt{check_mode},
true_exprt(),
true_exprt(),
wrapper_sl);
diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
index 346fbe6e78f..b820ce321f1 100644
--- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
+++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
@@ -68,7 +68,7 @@ void havoc_assigns_clause_targetst::havoc_if_valid(
skip_program.add(goto_programt::make_skip(source_location_no_checks));
dest.add(goto_programt::make_goto(
- skip_target, not_exprt{car.valid_var()}, source_location_no_checks));
+ skip_target, boolean_negate(car.valid_var()), source_location_no_checks));
if(car.havoc_method == car_havoc_methodt::HAVOC_OBJECT)
{
@@ -142,7 +142,7 @@ void havoc_assigns_clause_targetst::havoc_static_local(
skip_program.add(goto_programt::make_skip(source_location_no_checks));
dest.add(goto_programt::make_goto(
- skip_target, not_exprt{car.valid_var()}, source_location_no_checks));
+ skip_target, boolean_negate(car.valid_var()), source_location_no_checks));
const auto &target_type = car.target().type();
side_effect_expr_nondett nondet(target_type, source_location);
diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
index fc273e46259..e2a4fdb64b8 100644
--- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp
+++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
@@ -585,8 +585,10 @@ car_exprt instrument_spec_assignst::create_car_expr(
valid_var,
lower_bound_var,
upper_bound_var,
- is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN
- : car_havoc_methodt::HAVOC_SLICE};
+ (is_ptr_to_ptr.is_constant() &&
+ to_constant_expr(is_ptr_to_ptr).is_true())
+ ? car_havoc_methodt::NONDET_ASSIGN
+ : car_havoc_methodt::HAVOC_SLICE};
}
}
}
@@ -656,9 +658,9 @@ exprt instrument_spec_assignst::target_validity_expr(
// (or is NULL if we allow it explicitly).
// This assertion will be falsified whenever `start_address` is invalid or
// not of the right size (or is NULL if we do not allow it explicitly).
- auto result =
- or_exprt{not_exprt{car.condition()},
- w_ok_exprt{car.target_start_address(), car.target_size()}};
+ auto result = or_exprt{
+ boolean_negate(car.condition()),
+ w_ok_exprt{car.target_start_address(), car.target_size()}};
if(allow_null_target)
result.add_to_operands(null_object(car.target_start_address()));
@@ -685,7 +687,9 @@ void instrument_spec_assignst::target_validity_assertion(
std::string comment = "Check that ";
comment += from_expr(ns, "", car.target());
comment += " is valid";
- if(!car.condition().is_true())
+ if(
+ !car.condition().is_constant() ||
+ !to_constant_expr(car.condition()).is_true())
{
comment += " when ";
comment += from_expr(ns, "", car.condition());
@@ -719,8 +723,12 @@ void instrument_spec_assignst::inclusion_check_assertion(
std::string comment = "Check that ";
if(!is_assigns_clause_replacement_tracking_comment(orig_comment))
{
- if(!car.condition().is_true())
+ if(
+ !car.condition().is_constant() ||
+ !to_constant_expr(car.condition()).is_true())
+ {
comment += from_expr(ns, "", car.condition()) + ": ";
+ }
comment += from_expr(ns, "", car.target());
}
else
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
index a33319509b2..d64b2ed91d8 100644
--- a/src/goto-instrument/contracts/utils.cpp
+++ b/src/goto-instrument/contracts/utils.cpp
@@ -41,7 +41,9 @@ static void append_safe_havoc_code_for_expr(
// skip havocing only if all pointer derefs in the expression are valid
// (to avoid spurious pointer deref errors)
dest.add(goto_programt::make_goto(
- skip_target, not_exprt{all_dereferences_are_valid(expr, ns)}, location));
+ skip_target,
+ boolean_negate(all_dereferences_are_valid(expr, ns)),
+ location));
havoc_code_impl();
@@ -149,7 +151,9 @@ void havoc_assigns_targetst::append_havoc_code_for_expr(
{
const auto &ptr = funcall.arguments().at(0);
const auto &size = funcall.arguments().at(1);
- if(funcall.arguments().at(2).is_true())
+ if(
+ funcall.arguments().at(2).is_constant() &&
+ to_constant_expr(funcall.arguments().at(2)).is_true())
{
append_havoc_pointer_code(expr.source_location(), ptr, dest);
}
@@ -259,10 +263,14 @@ void simplify_gotos(goto_programt &goto_program, namespacet &ns)
{
for(auto &instruction : goto_program.instructions)
{
- if(
- instruction.is_goto() &&
- simplify_expr(instruction.condition(), ns).is_false())
+ if(!instruction.is_goto())
+ continue;
+
+ exprt simp_cond = simplify_expr(instruction.condition(), ns);
+ if(simp_cond.is_constant() && to_constant_expr(simp_cond).is_false())
+ {
instruction.turn_into_skip();
+ }
}
}
@@ -433,8 +441,8 @@ static void replace_history_parameter_rec(
// 2.2. Skip storing the history if the expression is invalid
auto goto_instruction = history.add(goto_programt::make_incomplete_goto(
- not_exprt{
- all_dereferences_are_valid(parameter, namespacet(symbol_table))},
+ boolean_negate(
+ all_dereferences_are_valid(parameter, namespacet(symbol_table))),
location));
// 2.3. Add an assignment such that the value pointed to by the new
diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp
index 36af6b16964..ef1e3f207dc 100644
--- a/src/goto-instrument/cover_basic_blocks.cpp
+++ b/src/goto-instrument/cover_basic_blocks.cpp
@@ -23,8 +23,11 @@ std::optional<std::size_t> cover_basic_blockst::continuation_of_block(
const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
if(
in_t->is_goto() && !in_t->is_backwards_goto() &&
- in_t->condition().is_true())
+ in_t->condition().is_constant() &&
+ to_constant_expr(in_t->condition()).is_true())
+ {
return block_map[in_t];
+ }
return {};
}
diff --git a/src/goto-instrument/cover_instrument_branch.cpp b/src/goto-instrument/cover_instrument_branch.cpp
index efec9d5409c..0619b96bb38 100644
--- a/src/goto-instrument/cover_instrument_branch.cpp
+++ b/src/goto-instrument/cover_instrument_branch.cpp
@@ -26,7 +26,8 @@ void cover_branch_instrumentert::instrument(
const bool is_function_entry_point =
i_it == goto_program.instructions.begin();
const bool is_conditional_goto =
- i_it->is_goto() && !i_it->condition().is_true();
+ i_it->is_goto() && (!i_it->condition().is_constant() ||
+ !to_constant_expr(i_it->condition()).is_true());
if(!is_function_entry_point && !is_conditional_goto)
return;
diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp
index 770a52a5f26..5c50d772d4e 100644
--- a/src/goto-instrument/dot.cpp
+++ b/src/goto-instrument/dot.cpp
@@ -108,8 +108,12 @@ void dott::write_dot_subgraph(
std::stringstream tmp;
if(it->is_goto())
{
- if(it->condition().is_true())
+ if(
+ it->condition().is_constant() &&
+ to_constant_expr(it->condition()).is_true())
+ {
tmp.str("Goto");
+ }
else
{
std::string t = from_expr(ns, function_id, it->condition());
@@ -320,14 +324,20 @@ void dott::find_next(
std::set<goto_programt::const_targett, goto_programt::target_less_than> &tres,
std::set<goto_programt::const_targett, goto_programt::target_less_than> &fres)
{
- if(it->is_goto() && !it->condition().is_false())
+ if(
+ it->is_goto() && (!it->condition().is_constant() ||
+ !to_constant_expr(it->condition()).is_false()))
{
for(const auto &target : it->targets)
tres.insert(target);
}
- if(it->is_goto() && it->condition().is_true())
+ if(
+ it->is_goto() && it->condition().is_constant() &&
+ to_constant_expr(it->condition()).is_true())
+ {
return;
+ }
goto_programt::const_targett next = it; next++;
if(next!=instructions.end())
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 8f6800b35b8..dc2ff6115e7 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -1399,7 +1399,7 @@ void dump_ct::cleanup_expr(exprt &expr)
}
// add a typecast for NULL
else if(
- u.op().is_constant() && is_null_pointer(to_constant_expr(u.op())) &&
+ u.op().is_constant() && to_constant_expr(u.op()).is_null_pointer() &&
to_pointer_type(u.op().type()).base_type().id() == ID_empty)
{
const struct_union_typet::componentt &comp=
@@ -1459,7 +1459,7 @@ void dump_ct::cleanup_expr(exprt &expr)
// add a typecast for NULL or 0
if(
argument.is_constant() &&
- is_null_pointer(to_constant_expr(argument)))
+ to_constant_expr(argument).is_null_pointer())
{
const typet &comp_type=
to_union_type(type).components().front().type();
@@ -1499,7 +1499,9 @@ void dump_ct::cleanup_expr(exprt &expr)
{
const byte_update_exprt &bu = to_byte_update_expr(expr);
- if(bu.op().id() == ID_union && bu.offset().is_zero())
+ if(
+ bu.op().id() == ID_union && bu.offset().is_constant() &&
+ to_constant_expr(bu.offset()).is_zero())
{
const union_exprt &union_expr = to_union_expr(bu.op());
const union_typet &union_type =
@@ -1537,7 +1539,7 @@ void dump_ct::cleanup_expr(exprt &expr)
to_side_effect_expr(bu.op()).get_statement() == ID_nondet &&
(bu.op().type().id() == ID_union ||
bu.op().type().id() == ID_union_tag) &&
- bu.offset().is_zero())
+ bu.offset().is_constant() && to_constant_expr(bu.offset()).is_zero())
{
const union_typet &union_type =
bu.op().type().id() == ID_union_tag
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index f8b8c8a6414..5e1d79dd2d7 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -281,9 +281,12 @@ void full_slicert::operator()(
else if(implicit(instruction))
add_to_queue(queue, instruction_node_index, instruction);
else if(
- (instruction->is_goto() && instruction->condition().is_true()) ||
+ (instruction->is_goto() && instruction->condition().is_constant() &&
+ to_constant_expr(instruction->condition()).is_true()) ||
instruction->is_throw())
+ {
jumps.push_back(instruction_node_index);
+ }
else if(instruction->is_decl())
{
const auto &s = instruction->decl_symbol();
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 94c3351236d..c733e926e23 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -311,7 +311,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
const exprt this_va_list_expr = target->assign_lhs();
const exprt &r = skip_typecast(target->assign_rhs());
- if(r.is_constant() && is_null_pointer(to_constant_expr(r)))
+ if(r.is_constant() && to_constant_expr(r).is_null_pointer())
{
code_function_callt f(
symbol_exprt("va_end", code_typet({}, empty_typet())),
@@ -550,8 +550,12 @@ goto_programt::const_targett goto_program2codet::convert_goto(
(upper_bound==goto_program.instructions.end() ||
upper_bound->location_number > loop_entry->second->location_number))
return convert_goto_while(target, loop_entry->second, dest);
- else if(!target->condition().is_true())
+ else if(
+ !target->condition().is_constant() ||
+ !to_constant_expr(target->condition()).is_true())
+ {
return convert_goto_switch(target, upper_bound, dest);
+ }
else if(!loop_last_stack.empty())
return convert_goto_break_continue(target, upper_bound, dest);
else
@@ -580,7 +584,9 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
w.cond() = not_exprt(target->condition());
simplify(w.cond(), ns);
}
- else if(target->condition().is_true())
+ else if(
+ target->condition().is_constant() &&
+ to_constant_expr(target->condition()).is_true())
{
target = convert_goto_goto(target, to_code_block(w.body()));
}
@@ -597,11 +603,15 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
loop_last_stack.pop_back();
convert_labels(loop_end, to_code_block(w.body()));
- if(loop_end->condition().is_false())
+ if(
+ loop_end->condition().is_constant() &&
+ to_constant_expr(loop_end->condition()).is_false())
{
to_code_block(w.body()).add(code_breakt());
}
- else if(!loop_end->condition().is_true())
+ else if(
+ !loop_end->condition().is_constant() ||
+ !to_constant_expr(loop_end->condition()).is_true())
{
code_ifthenelset i(not_exprt(loop_end->condition()), code_breakt());
simplify(i.cond(), ns);
@@ -624,15 +634,18 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
f.swap(w);
}
- else if(w.body().has_operands() &&
- w.cond().is_true())
+ else if(
+ w.body().has_operands() && w.cond().is_constant() &&
+ to_constant_expr(w.cond()).is_true())
{
const codet &back=to_code(w.body().operands().back());
- if(back.get_statement()==ID_break ||
- (back.get_statement()==ID_ifthenelse &&
- to_code_ifthenelse(back).cond().is_true() &&
- to_code_ifthenelse(back).then_case().get_statement()==ID_break))
+ if(
+ back.get_statement() == ID_break ||
+ (back.get_statement() == ID_ifthenelse &&
+ to_code_ifthenelse(back).cond().is_constant() &&
+ to_constant_expr(to_code_ifthenelse(back).cond()).is_true() &&
+ to_code_ifthenelse(back).then_case().get_statement() == ID_break))
{
w.body().operands().pop_back();
code_dowhilet d(false_exprt(), w.body());
@@ -667,7 +680,8 @@ goto_programt::const_targett goto_program2codet::get_cases(
{
if(
cases_it->is_goto() && !cases_it->is_backwards_goto() &&
- cases_it->condition().is_true())
+ cases_it->condition().is_constant() &&
+ to_constant_expr(cases_it->condition()).is_true())
{
default_target=cases_it->get_target();
@@ -834,7 +848,8 @@ bool goto_program2codet::remove_default(
next_case != goto_program.instructions.end() &&
next_case == default_target &&
(!it->case_last->is_goto() ||
- (it->case_last->condition().is_true() &&
+ (it->case_last->condition().is_constant() &&
+ to_constant_expr(it->case_last->condition()).is_true() &&
it->case_last->get_target() == default_target)))
{
// if there is no goto here, yet we got here, all others would
@@ -845,9 +860,12 @@ bool goto_program2codet::remove_default(
// jumps to default are ok
if(
- it->case_last->is_goto() && it->case_last->condition().is_true() &&
+ it->case_last->is_goto() && it->case_last->condition().is_constant() &&
+ to_constant_expr(it->case_last->condition()).is_true() &&
it->case_last->get_target() == default_target)
+ {
continue;
+ }
// fall-through is ok
if(!it->case_last->is_goto())
@@ -1059,7 +1077,8 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
has_else =
before_else->is_goto() &&
before_else->get_target()->location_number > end_if->location_number &&
- before_else->condition().is_true() &&
+ before_else->condition().is_constant() &&
+ to_constant_expr(before_else->condition()).is_true() &&
(upper_bound == goto_program.instructions.end() ||
upper_bound->location_number >=
before_else->get_target()->location_number);
@@ -1145,7 +1164,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
copy_source_location(target, i);
- if(i.cond().is_true())
+ if(i.cond().is_constant() && to_constant_expr(i.cond()).is_true())
dest.add(std::move(i.then_case()));
else
dest.add(std::move(i));
@@ -1169,7 +1188,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
copy_source_location(target, i);
- if(i.cond().is_true())
+ if(i.cond().is_constant() && to_constant_expr(i.cond()).is_true())
dest.add(std::move(i.then_case()));
else
dest.add(std::move(i));
@@ -1227,7 +1246,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto(
copy_source_location(target, i);
- if(i.cond().is_true())
+ if(i.cond().is_constant() && to_constant_expr(i.cond()).is_true())
dest.add(std::move(i.then_case()));
else
dest.add(std::move(i));
@@ -1292,7 +1311,9 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
// 2: code in existing thread
/* check the structure and compute the iterators */
DATA_INVARIANT(
- next->is_goto() && next->condition().is_true(), "START THREAD pattern");
+ next->is_goto() && next->condition().is_constant() &&
+ to_constant_expr(next->condition()).is_true(),
+ "START THREAD pattern");
DATA_INVARIANT(!next->is_backwards_goto(), "START THREAD pattern");
DATA_INVARIANT(
thread_start->location_number < next->get_target()->location_number,
@@ -1508,9 +1529,13 @@ void goto_program2codet::cleanup_code(
if(do_while.body().get_statement()==ID_skip)
do_while.set_statement(ID_while);
// do stmt while(false) is just stmt
- else if(do_while.cond().is_false() &&
- do_while.body().get_statement()!=ID_block)
+ else if(
+ do_while.cond().is_constant() &&
+ to_constant_expr(do_while.cond()).is_false() &&
+ do_while.body().get_statement() != ID_block)
+ {
code=do_while.body();
+ }
}
}
@@ -1692,13 +1717,15 @@ void goto_program2codet::cleanup_code_ifthenelse(
// assert(false) expands to if(true) assert(false), simplify again (and also
// simplify other cases)
if(
- cond.is_true() &&
+ cond.is_constant() && to_constant_expr(cond).is_true() &&
(i_t_e.else_case().is_nil() || !has_labels(i_t_e.else_case())))
{
codet tmp = i_t_e.then_case();
code.swap(tmp);
}
- else if(cond.is_false() && !has_labels(i_t_e.then_case()))
+ else if(
+ cond.is_constant() && to_constant_expr(cond).is_false() &&
+ !has_labels(i_t_e.then_case()))
{
if(i_t_e.else_case().is_nil())
code=code_skipt();
diff --git a/src/goto-instrument/horn_encoding.cpp b/src/goto-instrument/horn_encoding.cpp
index 4d316fe47bd..2b32d454170 100644
--- a/src/goto-instrument/horn_encoding.cpp
+++ b/src/goto-instrument/horn_encoding.cpp
@@ -428,7 +428,9 @@ std::vector<symbol_exprt> state_encodingt::incoming_symbols(loct loc) const
// conditional jump from loc_in to loc?
if(
- loc_in->is_goto() && !loc_in->condition().is_true() &&
+ loc_in->is_goto() &&
+ (!loc_in->condition().is_constant() ||
+ !to_constant_expr(loc_in->condition()).is_true()) &&
loc != std::next(loc_in))
{
suffix = "T";
@@ -688,7 +690,9 @@ void state_encodingt::setup_incoming(const goto_functiont &goto_function)
forall_goto_program_instructions(it, goto_function.body)
{
auto next = std::next(it);
- if(it->is_goto() && it->condition().is_true())
+ if(
+ it->is_goto() && it->condition().is_constant() &&
+ to_constant_expr(it->condition()).is_true())
{
}
else if(next != goto_function.body.instructions.end())
@@ -921,7 +925,7 @@ void state_encodingt::encode(
// We produce ∅ when the 'other' branch is taken. Get the condition.
const auto &condition = loc->condition();
- if(condition.is_true())
+ if(condition.is_constant() && to_constant_expr(condition).is_true())
{
dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
}
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index c52adcdd905..837ef835d54 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -141,7 +141,9 @@ void goto_unwindt::unwind(
exprt exit_cond = false_exprt(); // default is false
- if(!t->condition().is_true()) // cond in backedge
+ if(
+ !t->condition().is_constant() ||
+ !to_constant_expr(t->condition()).is_true()) // cond in backedge
{
exit_cond = boolean_negate(t->condition());
}
@@ -191,7 +193,9 @@ void goto_unwindt::unwind(
goto_programt::const_targett t_before=loop_exit;
t_before--;
- if(!t_before->is_goto() || !t_before->condition().is_true())
+ if(
+ !t_before->is_goto() || !t_before->condition().is_constant() ||
+ !to_constant_expr(t_before->condition()).is_true())
{
goto_programt::targett t_goto = goto_program.insert_before(
loop_exit,
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
index e271d761b19..6e152b5905c 100644
--- a/src/goto-programs/cfg.h
+++ b/src/goto-programs/cfg.h
@@ -320,7 +320,8 @@ void cfg_baset<T, P, I>::compute_edges_goto(
{
if(
next_PC != goto_program.instructions.end() &&
- !instruction.condition().is_true())
+ (!instruction.condition().is_constant() ||
+ !to_constant_expr(instruction.condition()).is_true()))
{
this->add_edge(entry, entry_map[next_PC]);
}
@@ -501,8 +502,12 @@ void cfg_baset<T, P, I>::compute_edges(
case ASSUME:
// false guard -> no successor
- if(instruction.condition().is_false())
+ if(
+ instruction.condition().is_constant() &&
+ to_constant_expr(instruction.condition()).is_false())
+ {
break;
+ }
case ASSIGN:
case ASSERT:
diff --git a/src/goto-programs/ensure_one_backedge_per_target.cpp b/src/goto-programs/ensure_one_backedge_per_target.cpp
index f9f3c2c6d1e..3bdc63bb9a4 100644
--- a/src/goto-programs/ensure_one_backedge_per_target.cpp
+++ b/src/goto-programs/ensure_one_backedge_per_target.cpp
@@ -57,7 +57,9 @@ bool ensure_one_backedge_per_target(
// If the last backedge is a conditional jump, add an extra unconditional
// backedge after it:
- if(!last_backedge->condition().is_true())
+ if(
+ !last_backedge->condition().is_constant() ||
+ !to_constant_expr(last_backedge->condition()).is_true())
{
auto new_goto =
goto_program.insert_after(last_backedge, goto_programt::make_goto(it));
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index db89fd0f4fd..46a418c656c 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -79,7 +79,7 @@ std::ostream &goto_programt::instructiont::output(std::ostream &out) const
case GOTO:
case INCOMPLETE_GOTO:
- if(!condition().is_true())
+ if(!condition().is_constant() || !to_constant_expr(condition()).is_true())
{
out << "IF " << format(condition()) << " THEN ";
}
@@ -525,7 +525,9 @@ std::string as_string(
return "(NO INSTRUCTION TYPE)";
case GOTO:
- if(!i.condition().is_true())
+ if(
+ !i.condition().is_constant() ||
+ !to_constant_expr(i.condition()).is_true())
{
result += "IF " + from_expr(ns, function, i.condition()) + " THEN ";
}
@@ -742,8 +744,14 @@ void goto_programt::copy_from(const goto_programt &src)
bool goto_programt::has_assertion() const
{
for(const auto &i : instructions)
- if(i.is_assert() && !i.condition().is_true())
+ {
+ if(
+ i.is_assert() && (!i.condition().is_constant() ||
+ !to_constant_expr(i.condition()).is_true()))
+ {
return true;
+ }
+ }
return false;
}
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index fa8eca15353..6a9a1e9c05b 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -1137,8 +1137,13 @@ std::list<Target> goto_programt::get_successors(
{
std::list<Target> successors(i.targets.begin(), i.targets.end());
- if(!i.condition().is_true() && next != instructions.end())
+ if(
+ (!i.condition().is_constant() ||
+ !to_constant_expr(i.condition()).is_true()) &&
+ next != instructions.end())
+ {
successors.push_back(next);
+ }
return successors;
}
@@ -1167,7 +1172,9 @@ std::list<Target> goto_programt::get_successors(
if(i.is_assume())
{
- return !i.condition().is_false() && next != instructions.end()
+ return (!i.condition().is_constant() ||
+ !to_constant_expr(i.condition()).is_false()) &&
+ next != instructions.end()
? std::list<Target>{next}
: std::list<Target>();
}
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index 0a7797af2d3..af722107ab8 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -229,7 +229,7 @@ std::string trace_numeric_value(
}
else if(type.id()==ID_bool)
{
- return expr.is_true()?"1":"0";
+ return to_constant_expr(expr).is_true() ? "1" : "0";
}
else if(type.id()==ID_integer)
{
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index e0aef679768..1c9dde5a659 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -238,8 +238,12 @@ static bool filter_out(
prev_it->pc->source_location() == it->pc->source_location())
return true;
- if(it->is_goto() && it->pc->condition().is_true())
+ if(
+ it->is_goto() && it->pc->condition().is_constant() &&
+ to_constant_expr(it->pc->condition()).is_true())
+ {
return true;
+ }
const source_locationt &source_location = it->pc->source_location();
@@ -546,7 +550,8 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
if(
it->hidden ||
(!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
- (it->is_goto() && it->source.pc->condition().is_true()) ||
+ (it->is_goto() && it->source.pc->condition().is_constant() &&
+ to_constant_expr(it->source.pc->condition()).is_true()) ||
source_location.is_nil() || source_location.is_built_in() ||
source_location.get_line().empty())
{
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index cdb413e351e..7c1997ce1f8 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -382,7 +382,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
}
else if(expr.is_boolean())
{
- return {expr.is_true()};
+ return {to_constant_expr(expr).is_true()};
}
else if(expr.type().id()==ID_string)
{
diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp
index 16139131b90..5b534131555 100644
--- a/src/goto-programs/json_expr.cpp
+++ b/src/goto-programs/json_expr.cpp
@@ -53,7 +53,7 @@ static exprt simplify_json_expr(const exprt &src)
}
else if(
object.id() == ID_index && to_index_expr(object).index().is_constant() &&
- to_constant_expr(to_index_expr(object).index()).value_is_zero_string())
+ to_constant_expr(to_index_expr(object).index()).is_zero())
{
// simplify expressions of the form &array[0]
return simplify_json_expr(to_index_expr(object).array());
@@ -288,8 +288,9 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
else if(type.id() == ID_bool)
{
result["name"] = json_stringt("boolean");
- result["binary"] = json_stringt(expr.is_true() ? "1" : "0");
- result["data"] = jsont::json_boolean(expr.is_true());
+ result["binary"] =
+ json_stringt(to_constant_expr(expr).is_true() ? "1" : "0");
+ result["data"] = jsont::json_boolean(to_constant_expr(expr).is_true());
}
else if(type.id() == ID_string)
{
diff --git a/src/goto-programs/pointer_arithmetic.cpp b/src/goto-programs/pointer_arithmetic.cpp
index 7c52e30fd85..64e0ea04efd 100644
--- a/src/goto-programs/pointer_arithmetic.cpp
+++ b/src/goto-programs/pointer_arithmetic.cpp
@@ -46,7 +46,9 @@ void pointer_arithmetict::read(const exprt &src)
{
const index_exprt &index_expr = to_index_expr(address_of_src.op());
- if(index_expr.index().is_zero())
+ if(
+ index_expr.index().is_constant() &&
+ to_constant_expr(index_expr.index()).is_zero())
make_pointer(address_of_src);
else
{
diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
index 043a3107184..4eff54dc30d 100644
--- a/src/goto-programs/remove_const_function_pointers.cpp
+++ b/src/goto-programs/remove_const_function_pointers.cpp
@@ -170,7 +170,7 @@ bool remove_const_function_pointerst::try_resolve_function_call(
}
else if(simplified_expr.is_constant())
{
- if(simplified_expr.is_zero())
+ if(to_constant_expr(simplified_expr).is_zero())
{
// We have the null pointer - no need to throw everything away
// but we don't add any functions either
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 7db4f3456b7..1be6140690e 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -236,11 +236,11 @@ static void fix_return_type(
exprt old_lhs=function_call.lhs();
function_call.lhs()=tmp_symbol_expr;
- dest.add(goto_programt::make_assignment(code_assignt(
+ dest.add(goto_programt::make_assignment(
old_lhs,
make_byte_extract(
tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()),
- source_location)));
+ source_location));
}
void remove_function_pointerst::remove_function_pointer(
diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp
index 8ca1aea3787..f227c547bb0 100644
--- a/src/goto-programs/remove_skip.cpp
+++ b/src/goto-programs/remove_skip.cpp
@@ -37,8 +37,12 @@ bool is_skip(
if(it->is_goto())
{
- if(it->condition().is_false())
+ if(
+ it->condition().is_constant() &&
+ to_constant_expr(it->condition()).is_false())
+ {
return true;
+ }
goto_programt::const_targett next_it = it;
next_it++;
@@ -48,7 +52,9 @@ bool is_skip(
// A branch to the next instruction is a skip
// We also require the guard to be 'true'
- return it->condition().is_true() && it->get_target() == next_it;
+ return it->condition().is_constant() &&
+ to_constant_expr(it->condition()).is_true() &&
+ it->get_target() == next_it;
}
if(it->is_other())
diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp
index 71b37ed0c54..9c35023a013 100644
--- a/src/goto-programs/rewrite_union.cpp
+++ b/src/goto-programs/rewrite_union.cpp
@@ -146,7 +146,9 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns)
for(const auto &comp : union_type.components())
{
- if(be.offset().is_zero() && be.type() == comp.type())
+ if(
+ be.offset().is_constant() &&
+ to_constant_expr(be.offset()).is_zero() && be.type() == comp.type())
{
expr = member_exprt{be.op(), comp.get_name(), be.type()};
return false;
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 5a00c5a7efb..9f86d746f76 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -910,7 +910,7 @@ bool string_abstractiont::build_array(const array_exprt &object,
exprt::operandst::const_iterator it=object.operands().begin();
for(mp_integer i = 0; i < *size; ++i, ++it)
- if(it->is_zero())
+ if(it->is_constant() && to_constant_expr(*it).is_zero())
return build_symbol_constant(i, *size, dest);
return true;
@@ -1194,7 +1194,7 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
rhsp = &(to_typecast_expr(*rhsp).op());
// we only care if the constant zero is assigned
- if(!rhsp->is_zero())
+ if(!rhsp->is_constant() || !to_constant_expr(*rhsp).is_zero())
return target;
// index into a character array
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
index fe2e8b94130..54a1aa984f3 100644
--- a/src/goto-programs/vcd_goto_trace.cpp
+++ b/src/goto-programs/vcd_goto_trace.cpp
@@ -131,15 +131,25 @@ void output_vcd(
// booleans are special in VCD
if(type.id() == ID_bool)
{
- if(step.full_lhs_value.is_true())
+ if(
+ step.full_lhs_value.is_constant() &&
+ to_constant_expr(step.full_lhs_value).is_true())
+ {
out << "1"
<< "V" << number << "\n";
- else if(step.full_lhs_value.is_false())
+ }
+ else if(
+ step.full_lhs_value.is_constant() &&
+ to_constant_expr(step.full_lhs_value).is_false())
+ {
out << "0"
<< "V" << number << "\n";
+ }
else
+ {
out << "x"
<< "V" << number << "\n";
+ }
}
else
{
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
index da90516dace..99616b91bd3 100644
--- a/src/goto-programs/xml_expr.cpp
+++ b/src/goto-programs/xml_expr.cpp
@@ -221,7 +221,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)
result.name = "pointer";
result.set_attribute(
"binary", integer2binary(bvrep2integer(value, width, false), width));
- if(is_null_pointer(constant_expr))
+ if(constant_expr.is_null_pointer())
result.data = "NULL";
}
else if(type.id() == ID_bool)
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 7e4013f5b6e..0ef1bf2bb98 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -84,9 +84,9 @@ static exprt build_full_lhs_rec(
exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond());
- if(tmp.is_true())
+ if(tmp.is_constant() && to_constant_expr(tmp).is_true())
return tmp2.true_case();
- else if(tmp.is_false())
+ else if(tmp.is_constant() && to_constant_expr(tmp).is_false())
return tmp2.false_case();
else
return std::move(tmp2);
@@ -241,7 +241,8 @@ void build_goto_trace(
const SSA_stept &SSA_step = *it;
- if(!decision_procedure.get(SSA_step.guard_handle).is_true())
+ exprt v = decision_procedure.get(SSA_step.guard_handle);
+ if(!v.is_constant() || !to_constant_expr(v).is_true())
continue;
if(it->is_constraint() ||
@@ -409,8 +410,9 @@ void build_goto_trace(
{
goto_trace_step.cond_expr = SSA_step.cond_expr;
+ exprt v = decision_procedure.get(SSA_step.cond_handle);
goto_trace_step.cond_value =
- decision_procedure.get(SSA_step.cond_handle).is_true();
+ v.is_constant() && to_constant_expr(v).is_true();
}
if(SSA_step.source.pc->is_assert() || SSA_step.source.pc->is_assume())
@@ -445,8 +447,11 @@ static bool is_failed_assertion_step(
symex_target_equationt::SSA_stepst::const_iterator step,
const decision_proceduret &decision_procedure)
{
- return step->is_assert() &&
- decision_procedure.get(step->cond_handle).is_false();
+ if(!step->is_assert())
+ return false;
+
+ exprt v = decision_procedure.get(step->cond_handle);
+ return v.is_constant() && to_constant_expr(v).is_false();
}
void build_goto_trace(
diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp
index fb8e382f437..8cbe0038a13 100644
--- a/src/goto-symex/goto_state.cpp
+++ b/src/goto-symex/goto_state.cpp
@@ -145,11 +145,7 @@ void goto_statet::apply_condition(
if(!is_ssa_expr(lhs) || !goto_symex_can_forward_propagatet(ns)(rhs))
return;
- if(rhs.is_true())
- apply_condition(equal_exprt{lhs, false_exprt{}}, previous_state, ns);
- else if(rhs.is_false())
- apply_condition(equal_exprt{lhs, true_exprt{}}, previous_state, ns);
- else
- UNREACHABLE;
+ PRECONDITION(rhs.is_constant());
+ apply_condition(equal_exprt{lhs, boolean_negate(rhs)}, previous_state, ns);
}
}
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 9ac435c89a4..ed295bc5d25 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -353,10 +353,18 @@ exprt goto_symex_statet::l2_rename_rvalues(exprt lvalue, const namespacet &ns)
// The condition is an rvalue:
auto &if_lvalue = to_if_expr(lvalue);
if_lvalue.cond() = rename(if_lvalue.cond(), ns);
- if(!if_lvalue.cond().is_false())
+ if(
+ !if_lvalue.cond().is_constant() ||
+ !to_constant_expr(if_lvalue.cond()).is_false())
+ {
if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns);
- if(!if_lvalue.cond().is_true())
+ }
+ if(
+ !if_lvalue.cond().is_constant() ||
+ !to_constant_expr(if_lvalue.cond()).is_true())
+ {
if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns);
+ }
}
else if(lvalue.id() == ID_complex_real)
{
@@ -450,8 +458,12 @@ bool goto_symex_statet::l2_thread_read_encoding(
}
guardt cond = read_guard;
- if(!no_write.op().is_false())
+ if(
+ !no_write.op().is_constant() ||
+ !to_constant_expr(no_write.op()).is_false())
+ {
cond |= guardt{no_write.op(), guard_manager};
+ }
// It is safe to perform constant propagation in case we have read or
// written this object within the atomic section. We must actually do this,
@@ -494,8 +506,12 @@ bool goto_symex_statet::l2_thread_read_encoding(
expr = std::move(ssa_l2);
a_s_read.second.push_back(guard);
- if(!no_write.op().is_false())
+ if(
+ !no_write.op().is_constant() ||
+ !to_constant_expr(no_write.op()).is_false())
+ {
a_s_read.second.back().add(no_write);
+ }
return true;
}
diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp
index bbf2cab2692..60cd377c9fc 100644
--- a/src/goto-symex/memory_model_sc.cpp
+++ b/src/goto-symex/memory_model_sc.cpp
@@ -302,7 +302,9 @@ void memory_model_sct::from_read(symex_target_equationt &equation)
exprt cond;
cond.make_nil();
- if(c_it->first.second==*w_prime && !ws1.is_false())
+ if(
+ c_it->first.second == *w_prime &&
+ (!ws1.is_constant() || !to_constant_expr(ws1).is_false()))
{
exprt fr=before(r, *w);
@@ -314,7 +316,9 @@ void memory_model_sct::from_read(symex_target_equationt &equation)
and_exprt(r->guard, (*w)->guard, ws1, rf),
fr);
}
- else if(c_it->first.second==*w && !ws2.is_false())
+ else if(
+ c_it->first.second == *w &&
+ (!ws2.is_constant() || !to_constant_expr(ws2).is_false()))
{
exprt fr=before(r, *w_prime);
diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp
index 54d6b58b677..68299e840d8 100644
--- a/src/goto-symex/memory_model_tso.cpp
+++ b/src/goto-symex/memory_model_tso.cpp
@@ -148,7 +148,7 @@ void memory_model_tsot::program_order(
simplify(cond, ns);
}
- if(!cond.is_false())
+ if(!cond.is_constant() || !to_constant_expr(cond).is_false())
{
if(ordering.is_nil())
ordering=partial_order_concurrencyt::before(
diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
index 9ff92da9824..4073549fbd3 100644
--- a/src/goto-symex/partial_order_concurrency.cpp
+++ b/src/goto-symex/partial_order_concurrency.cpp
@@ -51,9 +51,9 @@ void partial_order_concurrencyt::add_init_writes(
if(init_done.find(a)!=init_done.end())
continue;
- if(spawn_seen ||
- e_it->is_shared_read() ||
- !e_it->guard.is_true())
+ if(
+ spawn_seen || e_it->is_shared_read() || !e_it->guard.is_constant() ||
+ !to_constant_expr(e_it->guard).is_true())
{
init_steps.emplace_back(
e_it->source, goto_trace_stept::typet::SHARED_WRITE);
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 8b71f111674..74255afe4ff 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -62,7 +62,7 @@ void postcondition(
{
postconditiont postcondition(ns, value_set, *it, s);
postcondition.compute(dest);
- if(dest.is_false())
+ if(dest.is_constant() && to_constant_expr(dest).is_false())
return;
}
}
@@ -137,7 +137,7 @@ void postconditiont::strengthen(exprt &dest)
exprt equality =
get_original_name(equal_exprt{SSA_step.ssa_lhs, SSA_step.ssa_rhs});
- if(dest.is_true())
+ if(dest.is_constant() && to_constant_expr(dest).is_true())
dest.swap(equality);
else
dest=and_exprt(dest, equality);
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index 76fc7f48a83..5b0739510a9 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -70,7 +70,7 @@ void precondition(
{
preconditiont precondition(ns, value_sets, target, *it, s, message_handler);
precondition.compute(dest);
- if(dest.is_false())
+ if(dest.is_constant() && to_constant_expr(dest).is_false())
return;
}
}
diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp
index fe7b2005d53..1113bd9cfec 100644
--- a/src/goto-symex/shadow_memory.cpp
+++ b/src/goto-symex/shadow_memory.cpp
@@ -39,7 +39,8 @@ void shadow_memoryt::initialize_shadow_memory(
if(
field_pair.second.id() == ID_typecast &&
- to_typecast_expr(field_pair.second).op().is_zero())
+ to_typecast_expr(field_pair.second).op().is_constant() &&
+ to_constant_expr(to_typecast_expr(field_pair.second).op()).is_zero())
{
const auto zero_value =
zero_initializer(type, expr.source_location(), ns);
diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp
index b86a725b067..85a18973e27 100644
--- a/src/goto-symex/shadow_memory_util.cpp
+++ b/src/goto-symex/shadow_memory_util.cpp
@@ -319,9 +319,7 @@ bool contains_null_or_invalid(
const std::vector<exprt> &value_set,
const exprt &address)
{
- if(
- address.id() == ID_constant && address.type().id() == ID_pointer &&
- to_constant_expr(address).is_zero())
+ if(address.is_constant() && to_constant_expr(address).is_null_pointer())
{
for(const auto &e : value_set)
{
@@ -692,7 +690,8 @@ static void clean_string_constant(exprt &expr)
{
const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr);
if(
- index_expr && index_expr->index().is_zero() &&
+ index_expr && index_expr->index().is_constant() &&
+ to_constant_expr(index_expr->index()).is_zero() &&
can_cast_expr<string_constantt>(index_expr->array()))
{
expr = index_expr->array();
@@ -930,19 +929,21 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
const exprt base_cond = get_matched_base_cond(
shadowed_address.address, matched_base_address, ns, log);
shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
- if(base_cond.is_false())
+ if(base_cond.is_constant() && to_constant_expr(base_cond).is_false())
{
continue;
}
const exprt expr_cond =
get_matched_expr_cond(dereference.pointer, expr, ns, log);
- if(expr_cond.is_false())
+ if(expr_cond.is_constant() && to_constant_expr(expr_cond).is_false())
{
continue;
}
- if(base_cond.is_true() && expr_cond.is_true())
+ if(
+ base_cond.is_constant() && to_constant_expr(base_cond).is_true() &&
+ expr_cond.is_constant() && to_constant_expr(expr_cond).is_true())
{
#ifdef DEBUG_SHADOW_MEMORY
log.debug() << "exact match" << messaget::eom;
@@ -953,7 +954,7 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
break;
}
- if(base_cond.is_true())
+ if(base_cond.is_constant() && to_constant_expr(base_cond).is_true())
{
// No point looking at further shadow addresses
// as only one of them can match.
@@ -1097,19 +1098,21 @@ get_shadow_memory_for_matched_object(
const exprt base_cond = get_matched_base_cond(
shadowed_address.address, matched_base_address, ns, log);
shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
- if(base_cond.is_false())
+ if(base_cond.is_constant() && to_constant_expr(base_cond).is_false())
{
continue;
}
const exprt expr_cond =
get_matched_expr_cond(dereference.pointer, expr, ns, log);
- if(expr_cond.is_false())
+ if(expr_cond.is_constant() && to_constant_expr(expr_cond).is_false())
{
continue;
}
- if(base_cond.is_true() && expr_cond.is_true())
+ if(
+ base_cond.is_constant() && to_constant_expr(base_cond).is_true() &&
+ expr_cond.is_constant() && to_constant_expr(expr_cond).is_true())
{
log_shadow_memory_message(log, "exact match");
@@ -1119,7 +1122,7 @@ get_shadow_memory_for_matched_object(
break;
}
- if(base_cond.is_true())
+ if(base_cond.is_constant() && to_constant_expr(base_cond).is_true())
{
// No point looking at further shadow addresses
// as only one of them can match.
diff --git a/src/goto-symex/show_program.cpp b/src/goto-symex/show_program.cpp
index 13c409ea197..fc6fc205f9e 100644
--- a/src/goto-symex/show_program.cpp
+++ b/src/goto-symex/show_program.cpp
@@ -47,7 +47,7 @@ static void show_step(
std::cout << annotation << '(' << string_value << ')';
std::cout << '\n';
- if(!step.guard.is_true())
+ if(!step.guard.is_constant() || !to_constant_expr(step.guard).is_true())
{
const std::string guard_string = from_expr(ns, function_id, step.guard);
std::cout << std::string(std::to_string(count).size() + 3, ' ');
@@ -76,7 +76,8 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
show_step(ns, step, "ASSUME", count);
else if(step.is_constraint())
{
- PRECONDITION(step.guard.is_true());
+ PRECONDITION(
+ step.guard.is_constant() && to_constant_expr(step.guard).is_true());
show_step(ns, step, "CONSTRAINT", count);
}
else if(step.is_shared_read())
diff --git a/src/goto-symex/solver_hardness.cpp b/src/goto-symex/solver_hardness.cpp
index 95c8ea70033..eeeccffadfc 100644
--- a/src/goto-symex/solver_hardness.cpp
+++ b/src/goto-symex/solver_hardness.cpp
@@ -246,7 +246,9 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc)
case GOTO:
case INCOMPLETE_GOTO:
- if(!instruction.condition().is_true())
+ if(
+ !instruction.condition().is_constant() ||
+ !to_constant_expr(instruction.condition()).is_true())
{
out << "IF " << format(instruction.condition()) << " THEN ";
}
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index c829e4b1d8c..001fffff1a1 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -46,7 +46,10 @@ static bool is_string_constant_initialization(const exprt &rhs)
const auto &index =
expr_try_dynamic_cast<index_exprt>(address_of->object()))
{
- if(index->array().id() == ID_string_constant && index->index().is_zero())
+ if(
+ index->array().id() == ID_string_constant &&
+ index->index().is_constant() &&
+ to_constant_expr(index->index()).is_zero())
{
return true;
}
@@ -238,7 +241,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/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 9d3797a7247..0f672aeef32 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -172,7 +172,9 @@ void goto_symext::symex_allocate(
INVARIANT(
zero_init.is_constant(), "allocate expects constant as second argument");
- if(!zero_init.is_zero() && !zero_init.is_false())
+ if(
+ !to_constant_expr(zero_init).is_zero() &&
+ !to_constant_expr(zero_init).is_false())
{
const auto zero_value =
zero_initializer(*object_type, code.source_location(), ns);
@@ -317,7 +319,8 @@ static irep_idt get_string_argument_rec(const exprt &src)
if(
index_expr.array().id() == ID_string_constant &&
- index_expr.index().is_zero())
+ index_expr.index().is_constant() &&
+ to_constant_expr(index_expr.index()).is_zero())
{
const exprt &fmt_str = index_expr.array();
return to_string_constant(fmt_str).value();
@@ -358,8 +361,12 @@ static std::optional<exprt> get_va_args(const exprt::operandst &operands)
return {};
const index_exprt &index_expr = to_index_expr(object);
- if(!index_expr.index().is_zero())
+ if(
+ !index_expr.index().is_constant() ||
+ !to_constant_expr(index_expr.index()).is_zero())
+ {
return {};
+ }
else
return index_expr.array();
}
@@ -454,14 +461,13 @@ void goto_symext::symex_output(
PRECONDITION(code.operands().size() >= 2);
exprt id_arg = state.rename(code.op0(), ns).get();
- std::list<renamedt<exprt, L2>> args;
+ std::list<exprt> args;
for(std::size_t i=1; i<code.operands().size(); i++)
{
renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
- if(symex_config.simplify_opt)
- l2_arg.simplify(ns);
- args.emplace_back(l2_arg);
+ args.emplace_back(l2_arg.get());
+ do_simplify(args.back());
}
const irep_idt output_id=get_string_argument(id_arg, ns);
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 5c1ff7134a9..3389c04e037 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -82,7 +82,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
if(expr.type().id() == ID_empty)
return;
- if(!ode.offset().is_zero())
+ if(!ode.offset().is_constant() || !to_constant_expr(ode.offset()).is_zero())
{
if(expr.type().id() != ID_array)
{
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 25a61e2f74e..76e1159cb74 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -362,7 +362,9 @@ void goto_symext::dereference_rec(
}
else if(
expr.id() == ID_index && to_index_expr(expr).array().id() == ID_member &&
- to_array_type(to_index_expr(expr).array().type()).size().is_zero())
+ to_array_type(to_index_expr(expr).array().type()).size().is_constant() &&
+ to_constant_expr(to_array_type(to_index_expr(expr).array().type()).size())
+ .is_zero())
{
// This is an expression of the form x.a[i],
// where a is a zero-sized array. This gets
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 6fdf9f4ff5e..bc316977499 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -273,9 +273,11 @@ void goto_symext::symex_function_call_post_clean(
}
// read the arguments -- before the locality renaming
- const std::vector<renamedt<exprt, L2>> renamed_arguments =
+ const std::vector<exprt> renamed_arguments =
make_range(cleaned_arguments).map([&](const exprt &a) {
- return state.rename(a, ns);
+ exprt arg = state.rename(a, ns).get();
+ do_simplify(arg);
+ return arg;
});
// we hide the call if the caller and callee are both hidden
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 404f04fec72..7c1f76beaa6 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -91,7 +91,7 @@ static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
if(
skip_typecast(other_operand).id() != ID_address_of &&
- (!constant_expr || !is_null_pointer(*constant_expr)))
+ (!constant_expr || !constant_expr->is_null_pointer()))
{
return {};
}
@@ -139,13 +139,14 @@ static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
typecast_exprt::conditional_cast(value.pointer, other_operand.type()),
other_operand},
ns);
- if(test_equal.is_true())
+ auto constant_expr = expr_try_dynamic_cast<constant_exprt>(test_equal);
+ if(constant_expr && constant_expr->is_true())
{
constant_found = true;
// We can't break because we have to make sure we find any instances of
// ID_unknown or ID_invalid
}
- else if(!test_equal.is_false())
+ else if(!constant_expr)
{
// We can't conclude anything about the value-set
return {};
@@ -238,11 +239,10 @@ void goto_symext::symex_goto(statet &state)
renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
renamed_guard = try_evaluate_pointer_comparisons(
std::move(renamed_guard), state.value_set, language_mode, ns);
- if(symex_config.simplify_opt)
- renamed_guard.simplify(ns);
new_guard = renamed_guard.get();
+ do_simplify(new_guard);
- if(new_guard.is_false())
+ if(new_guard.is_constant() && to_constant_expr(new_guard).is_false())
{
target.location(state.guard.as_expr(), state.source);
@@ -251,7 +251,7 @@ void goto_symext::symex_goto(statet &state)
return; // nothing to do
}
- target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
+ target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
DATA_INVARIANT(
!instruction.targets.empty(), "goto should have at least one target");
@@ -275,11 +275,12 @@ void goto_symext::symex_goto(statet &state)
// while(cond);
(instruction.incoming_edges.size() == 1 &&
*instruction.incoming_edges.begin() == goto_target &&
- goto_target->is_goto() && new_guard.is_true())))
+ goto_target->is_goto() && new_guard.is_constant() &&
+ to_constant_expr(new_guard).is_true())))
{
// generate assume(false) or a suitable negation if this
// instruction is a conditional goto
- exprt negated_guard = not_exprt{new_guard};
+ exprt negated_guard = boolean_negate(new_guard);
do_simplify(negated_guard);
log.statistics() << "replacing self-loop at "
<< state.source.pc->source_location() << " by assume("
@@ -314,7 +315,7 @@ void goto_symext::symex_goto(statet &state)
return;
}
- if(new_guard.is_true())
+ if(new_guard.is_constant() && to_constant_expr(new_guard).is_true())
{
// we continue executing the loop
if(check_break(loop_id, unwind))
@@ -328,7 +329,8 @@ void goto_symext::symex_goto(statet &state)
// No point executing both branches of an unconditional goto.
if(
- new_guard.is_true() && // We have an unconditional goto, AND
+ new_guard.is_constant() && to_constant_expr(new_guard).is_true() &&
+ // We have an unconditional goto, AND
// either there are no reachable blocks between us and the target in the
// surrounding scope (because state.guard == true implies there is no path
// around this GOTO instruction)
@@ -355,7 +357,7 @@ void goto_symext::symex_goto(statet &state)
state_pc++;
// skip dead instructions
- if(new_guard.is_true())
+ if(new_guard.is_constant() && to_constant_expr(new_guard).is_true())
while(state_pc!=goto_target && !state_pc->is_target())
++state_pc;
@@ -442,7 +444,7 @@ void goto_symext::symex_goto(statet &state)
// On an unconditional GOTO we don't need our state, as it will be overwritten
// by merge_goto. Therefore we move it onto goto_state_list instead of copying
// as usual.
- if(new_guard.is_true())
+ if(new_guard.is_constant() && to_constant_expr(new_guard).is_true())
{
// The move here only moves goto_statet, the base class of goto_symex_statet
// and not the entire thing.
@@ -572,7 +574,9 @@ void goto_symext::symex_unreachable_goto(statet &state)
goto_state_list.emplace_back(state.source, std::move(new_state));
};
- if(instruction.condition().is_true())
+ if(
+ instruction.condition().is_constant() &&
+ to_constant_expr(instruction.condition()).is_true())
{
if(instruction.is_backwards_goto())
{
@@ -929,12 +933,7 @@ void goto_symext::loop_bound_exceeded(
{
const std::string loop_number = std::to_string(state.source.pc->loop_number);
- exprt negated_cond;
-
- if(guard.is_true())
- negated_cond=false_exprt();
- else
- negated_cond=not_exprt(guard);
+ exprt negated_cond = boolean_negate(guard);
if(symex_config.unwinding_assertions)
{
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index de1e7f1f388..9e19cbc99f7 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -186,7 +186,7 @@ void goto_symext::vcc(
state.total_vccs++;
path_segment_vccs++;
- if(condition.is_true())
+ if(condition.is_constant() && to_constant_expr(condition).is_true())
return;
const exprt guarded_condition = state.guard.guard_expr(condition);
@@ -218,10 +218,10 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
{
- if(cond.is_true())
+ if(cond.is_constant() && to_constant_expr(cond).is_true())
return;
- if(cond.is_false())
+ if(cond.is_constant() && to_constant_expr(cond).is_false())
state.reachable = false;
// we are willing to re-write some quantified expressions
@@ -855,11 +855,15 @@ void goto_symext::try_filter_value_sets(
do_simplify(modified_condition);
- if(jump_taken_value_set && modified_condition.is_false())
+ if(
+ jump_taken_value_set && modified_condition.is_constant() &&
+ to_constant_expr(modified_condition).is_false())
{
erase_from_jump_taken_value_set.insert(value_set_element);
}
- else if(jump_not_taken_value_set && modified_condition.is_true())
+ else if(
+ jump_not_taken_value_set && modified_condition.is_constant() &&
+ to_constant_expr(modified_condition).is_true())
{
erase_from_jump_not_taken_value_set.insert(value_set_element);
}
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
index 209bc6de49e..fc6bad23f66 100644
--- a/src/goto-symex/symex_target.h
+++ b/src/goto-symex/symex_target.h
@@ -158,7 +158,7 @@ class symex_targett
virtual void function_call(
const exprt &guard,
const irep_idt &function_id,
- const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
+ const std::vector<exprt> &ssa_function_arguments,
const sourcet &source,
bool hidden) = 0;
@@ -192,7 +192,7 @@ class symex_targett
const exprt &guard,
const sourcet &source,
const irep_idt &output_id,
- const std::list<renamedt<exprt, L2>> &args) = 0;
+ const std::list<exprt> &args) = 0;
/// Record formatted output.
/// \param guard: Precondition for writing to the output
@@ -251,7 +251,7 @@ class symex_targett
/// goto instruction
virtual void goto_instruction(
const exprt &guard,
- const renamedt<exprt, L2> &cond,
+ const exprt &cond,
const sourcet &source) = 0;
/// Record a _global_ constraint: there is no guard limiting its scope.
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 0bb35155e01..5e469e730d4 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -181,7 +181,7 @@ void symex_target_equationt::location(
void symex_target_equationt::function_call(
const exprt &guard,
const irep_idt &function_id,
- const std::vector<renamedt<exprt, L2>> &function_arguments,
+ const std::vector<exprt> &function_arguments,
const sourcet &source,
const bool hidden)
{
@@ -190,8 +190,7 @@ void symex_target_equationt::function_call(
SSA_step.guard = guard;
SSA_step.called_function = function_id;
- for(const auto &arg : function_arguments)
- SSA_step.ssa_function_arguments.emplace_back(arg.get());
+ SSA_step.ssa_function_arguments = function_arguments;
SSA_step.hidden = hidden;
merge_ireps(SSA_step);
@@ -217,14 +216,13 @@ void symex_target_equationt::output(
const exprt &guard,
const sourcet &source,
const irep_idt &output_id,
- const std::list<renamedt<exprt, L2>> &args)
+ const std::list<exprt> &args)
{
SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
SSA_stept &SSA_step=SSA_steps.back();
SSA_step.guard=guard;
- for(const auto &arg : args)
- SSA_step.io_args.emplace_back(arg.get());
+ SSA_step.io_args = args;
SSA_step.io_id=output_id;
merge_ireps(SSA_step);
@@ -299,14 +297,14 @@ void symex_target_equationt::assertion(
void symex_target_equationt::goto_instruction(
const exprt &guard,
- const renamedt<exprt, L2> &cond,
+ const exprt &cond,
const sourcet &source)
{
SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
SSA_stept &SSA_step=SSA_steps.back();
SSA_step.guard=guard;
- SSA_step.cond_expr = cond.get();
+ SSA_step.cond_expr = cond;
merge_ireps(SSA_step);
}
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index b10a922b113..ef2f1056a3c 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -82,7 +82,7 @@ class symex_target_equationt:public symex_targett
virtual void function_call(
const exprt &guard,
const irep_idt &function_id,
- const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
+ const std::vector<exprt> &ssa_function_arguments,
const sourcet &source,
bool hidden);
@@ -103,7 +103,7 @@ class symex_target_equationt:public symex_targett
const exprt &guard,
const sourcet &source,
const irep_idt &output_id,
- const std::list<renamedt<exprt, L2>> &args);
+ const std::list<exprt> &args);
/// \copydoc symex_targett::output_fmt()
virtual void output_fmt(
@@ -137,7 +137,7 @@ class symex_target_equationt:public symex_targett
/// \copydoc symex_targett::goto_instruction()
virtual void goto_instruction(
const exprt &guard,
- const renamedt<exprt, L2> &cond,
+ const exprt &cond,
const sourcet &source);
/// \copydoc symex_targett::constraint()
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
index dd32b5eec57..5c4e91ebfc9 100644
--- a/src/goto-synthesizer/cegis_verifier.cpp
+++ b/src/goto-synthesizer/cegis_verifier.cpp
@@ -71,7 +71,7 @@ get_checked_pointer_from_null_pointer_check(const exprt &violation)
// NULL == ptr
if(
can_cast_expr<constant_exprt>(lhs_pointer) &&
- is_null_pointer(*expr_try_dynamic_cast<constant_exprt>(lhs_pointer)))
+ expr_try_dynamic_cast<constant_exprt>(lhs_pointer)->is_null_pointer())
{
return rhs_pointer;
}
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 65fc1a8f4d4..b8f04a6838f 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -523,15 +523,18 @@ bool linkingt::adjust_object_type_rec(
const exprt &old_size=to_array_type(t1).size();
const exprt &new_size=to_array_type(t2).size();
- if((old_size.is_nil() && new_size.is_not_nil()) ||
- (old_size.is_zero() && new_size.is_not_nil()) ||
- info.old_symbol.is_weak)
+ if(
+ (old_size.is_nil() && new_size.is_not_nil()) ||
+ (old_size.is_constant() && to_constant_expr(old_size).is_zero() &&
+ new_size.is_not_nil()) ||
+ info.old_symbol.is_weak)
{
info.set_to_new=true; // store new type
}
- else if(new_size.is_nil() ||
- new_size.is_zero() ||
- info.new_symbol.is_weak)
+ else if(
+ new_size.is_nil() ||
+ (new_size.is_constant() && to_constant_expr(new_size).is_zero()) ||
+ info.new_symbol.is_weak)
{
// ok, we will use the old type
}
@@ -549,9 +552,8 @@ bool linkingt::adjust_object_type_rec(
return true;
}
- equal_exprt eq(old_size, new_size);
-
- if(!simplify_expr(eq, ns).is_true())
+ exprt maybe_eq = simplify_expr(equal_exprt{old_size, new_size}, ns);
+ if(!maybe_eq.is_constant() || !to_constant_expr(maybe_eq).is_true())
{
linking_diagnosticst diag{message_handler, ns};
diag.error(
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index fca7edf08d0..0a83b83700b 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -621,7 +621,7 @@ void value_sett::get_value_set_rec(
else if(expr.is_constant())
{
// check if NULL
- if(is_null_pointer(to_constant_expr(expr)))
+ if(to_constant_expr(expr).is_null_pointer())
{
insert(
dest,
@@ -656,7 +656,7 @@ void value_sett::get_value_set_rec(
{
// integer-to-something
- if(op.is_zero())
+ if(op.is_constant() && to_constant_expr(op).is_zero())
{
insert(dest, exprt(ID_null_object, empty_typet{}), mp_integer{0});
}
@@ -1398,7 +1398,7 @@ void value_sett::get_reference_set_rec(
offsett o = a_it->second;
const auto i = numeric_cast<mp_integer>(offset);
- if(offset.is_zero())
+ if(i.has_value() && i == 0)
{
}
else if(i.has_value() && o)
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 3af8d4b72b1..4499dd31450 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -486,7 +486,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
if(root_object.id() == ID_null_object)
{
- if(!o.offset().is_zero())
+ if(!o.offset().is_constant() || !to_constant_expr(o.offset()).is_zero())
return {};
valuet result;
@@ -572,7 +572,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
// something generic -- really has to be a symbol
address_of_exprt object_pointer(object);
- if(o.offset().is_zero())
+ if(o.offset().is_constant() && to_constant_expr(o.offset()).is_zero())
{
result.pointer_guard = equal_exprt(
typecast_exprt::conditional_cast(pointer_expr, object_pointer.type()),
@@ -588,7 +588,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
if(
dereference_type_compare(object_type, dereference_type, ns) &&
- o.offset().is_zero())
+ o.offset().is_constant() && to_constant_expr(o.offset()).is_zero())
{
// The simplest case: types match, and offset is zero!
// This is great, we are almost done.
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 5d595cccb4b..6fc272f6289 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -532,7 +532,7 @@ void value_set_fit::get_value_set_rec(
else if(expr.is_constant())
{
// check if NULL
- if(is_null_pointer(to_constant_expr(expr)))
+ if(to_constant_expr(expr).is_null_pointer())
{
insert(
dest,
@@ -924,7 +924,7 @@ void value_set_fit::get_reference_set_sharing_rec(
offsett o = object_entry.second;
const auto i = numeric_cast<mp_integer>(offset);
- if(offset.is_zero())
+ if(i.has_value() && i == 0)
{
}
else if(i.has_value() && offset_is_zero(o))
diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp
index 5ca7c77b243..4d27c497b88 100644
--- a/src/solvers/flattening/boolbv_quantifier.cpp
+++ b/src/solvers/flattening/boolbv_quantifier.cpp
@@ -174,7 +174,10 @@ static std::optional<exprt> eager_quantifier_instantiation(
const exprt where_simplified = simplify_expr(expr.where(), ns);
- if(where_simplified.is_true() || where_simplified.is_false())
+ if(
+ where_simplified.is_constant() &&
+ (to_constant_expr(where_simplified).is_true() ||
+ to_constant_expr(where_simplified).is_false()))
{
return where_simplified;
}
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index a022801df4b..f14954c253a 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -443,7 +443,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
{
const constant_exprt &c = to_constant_expr(expr);
- if(is_null_pointer(c))
+ if(c.is_null_pointer())
return encode(pointer_logic.get_null_object(), type);
else
{
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index c5b866d6104..2de32c82abb 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -129,7 +129,7 @@ exprt pointer_logict::pointer_expr(
const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
const address_of_exprt base(be.op());
- if(be.offset().is_zero())
+ if(be.offset().is_constant() && to_constant_expr(be.offset()).is_zero())
return typecast_exprt::conditional_cast(base, type);
const auto object_size = pointer_offset_size(be.op().type(), ns);
diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp
index f900c90f765..112d162911f 100644
--- a/src/solvers/prop/bdd_expr.cpp
+++ b/src/solvers/prop/bdd_expr.cpp
@@ -21,7 +21,10 @@ bddt bdd_exprt::from_expr_rec(const exprt &expr)
PRECONDITION(expr.is_boolean());
if(expr.is_constant())
- return expr.is_false() ? bdd_mgr.bdd_false() : bdd_mgr.bdd_true();
+ {
+ return to_constant_expr(expr).is_false() ? bdd_mgr.bdd_false()
+ : bdd_mgr.bdd_true();
+ }
else if(expr.id()==ID_not)
return from_expr_rec(to_not_expr(expr).op()).bdd_not();
else if(expr.id()==ID_and ||
@@ -138,7 +141,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 +152,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/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp
index b2782f7c5fe..76ff73dcab5 100644
--- a/src/solvers/prop/cover_goals.cpp
+++ b/src/solvers/prop/cover_goals.cpp
@@ -26,9 +26,12 @@ void cover_goalst::mark()
o->satisfying_assignment();
for(auto &g : goals)
- if(
- g.status == goalt::statust::UNKNOWN &&
- decision_procedure.get(g.condition).is_true())
+ {
+ if(g.status != goalt::statust::UNKNOWN)
+ continue;
+
+ exprt v = decision_procedure.get(g.condition);
+ if(v.is_constant() && to_constant_expr(v).is_true())
{
g.status=goalt::statust::COVERED;
_number_covered++;
@@ -37,6 +40,7 @@ void cover_goalst::mark()
for(const auto &o : observers)
o->goal_covered(g);
}
+ }
}
/// Build clause
@@ -47,8 +51,14 @@ void cover_goalst::constraint()
// cover at least one unknown goal
for(const auto &g : goals)
- if(g.status == goalt::statust::UNKNOWN && !g.condition.is_false())
+ {
+ if(
+ g.status == goalt::statust::UNKNOWN &&
+ (!g.condition.is_constant() || !to_constant_expr(g.condition).is_false()))
+ {
disjuncts.push_back(g.condition);
+ }
+ }
// this is 'false' if there are no disjuncts
decision_procedure.set_to_true(disjunction(disjuncts));
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index 597f95c7067..36a65e1c10c 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -78,11 +78,11 @@ std::optional<bool> prop_conv_solvert::get_bool(const exprt &expr) const
{
// trivial cases
- if(expr.is_true())
+ if(expr.is_constant() && to_constant_expr(expr).is_true())
{
return true;
}
- else if(expr.is_false())
+ else if(expr.is_constant() && to_constant_expr(expr).is_false())
{
return false;
}
@@ -195,12 +195,12 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
if(expr.is_constant())
{
- if(expr.is_true())
+ if(to_constant_expr(expr).is_true())
return const_literal(true);
else
{
INVARIANT(
- expr.is_false(),
+ to_constant_expr(expr).is_false(),
"constant expression of type bool should be either true or false");
return const_literal(false);
}
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index b5c5366658c..d0945e247f9 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -273,7 +273,7 @@ static bool is_zero_width(const typet &type, const namespacet &ns)
}
else if(auto array_type = type_try_dynamic_cast<array_typet>(type))
{
- // we ignore array_type->size().is_zero() for now as there may be
+ // we ignore array_type->size() being zero for now as there may be
// out-of-bounds accesses that we need to model
return is_zero_width(array_type->element_type(), ns);
}
@@ -364,9 +364,9 @@ exprt smt2_convt::get(const exprt &expr) const
else if(expr.id() == ID_not)
{
auto op = get(to_not_expr(expr).op());
- if(op.is_true())
+ if(op.is_constant() && to_constant_expr(op).is_true())
return false_exprt();
- else if(op.is_false())
+ else if(op.is_constant() && to_constant_expr(op).is_false())
return true_exprt();
}
else if(
@@ -811,7 +811,7 @@ void smt2_convt::convert_address_of_rec(
const exprt &array = index_expr.array();
const exprt &index = index_expr.index();
- if(index.is_zero())
+ if(index.is_constant() && to_constant_expr(index).is_zero())
{
if(array.type().id()==ID_pointer)
convert_expr(array);
@@ -899,9 +899,9 @@ literalt smt2_convt::convert(const exprt &expr)
// Three cases where no new handle is needed.
- if(expr.is_true())
+ if(expr.is_constant() && to_constant_expr(expr).is_true())
return const_literal(true);
- else if(expr.is_false())
+ else if(expr.is_constant() && to_constant_expr(expr).is_false())
return const_literal(false);
else if(expr.id()==ID_literal)
return to_literal_expr(expr).get_literal();
@@ -3379,7 +3379,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
}
else if(expr_type.id()==ID_pointer)
{
- if(is_null_pointer(expr))
+ if(expr.is_null_pointer())
{
out << "(_ bv0 " << boolbv_width(expr_type)
<< ")";
diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index 551f58f073c..80dd9751ca5 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -60,9 +60,9 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
}
else if(expr_type.id() == ID_bool)
{
- if(expr.is_true())
+ if(to_constant_expr(expr).is_true())
out << "true";
- else if(expr.is_false())
+ else if(to_constant_expr(expr).is_false())
out << "false";
else
DATA_INVARIANT(false, "unknown Boolean constant");
diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index dc4efc6fb3d..919212ec8a8 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -329,7 +329,7 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
{
- if(is_null_pointer(constant_literal))
+ if(constant_literal.is_null_pointer())
{
const size_t bit_width =
type_checked_cast<pointer_typet>(constant_literal.type()).get_width();
diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp
index 689818c4aaf..2d7b0e62b0a 100644
--- a/src/solvers/strings/string_builtin_function.cpp
+++ b/src/solvers/strings/string_builtin_function.cpp
@@ -31,7 +31,7 @@ std::optional<std::vector<mp_integer>> eval_string(
const exprt cond = get_value(ite.cond());
if(!cond.is_constant())
return {};
- return cond.is_true()
+ return to_constant_expr(cond).is_true()
? eval_string(to_array_string_expr(ite.true_case()), get_value)
: eval_string(to_array_string_expr(ite.false_case()), get_value);
}
diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp
index 20ce1f8ab2a..8608a589461 100644
--- a/src/solvers/strings/string_format_builtin_function.cpp
+++ b/src/solvers/strings/string_format_builtin_function.cpp
@@ -596,8 +596,9 @@ string_constraintst string_format_builtin_functiont::constraints(
auto result_constraint_pair = add_axioms_for_format(
generator, result, format_string.value(), inputs, message_handler);
+ auto simp_expr = simplify_expr(result_constraint_pair.first, generator.ns);
INVARIANT(
- simplify_expr(result_constraint_pair.first, generator.ns).is_zero(),
+ simp_expr.is_constant() && to_constant_expr(simp_expr).is_zero(),
"add_axioms_for_format should return 0, meaning that formatting was"
"successful");
result_constraint_pair.second.existential.push_back(
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index e1980bed5f4..56624a4ca76 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -920,7 +920,7 @@ void string_refinementt::add_lemma(
simplify(simple_lemma, ns);
}
- if(simple_lemma.is_true())
+ if(simple_lemma.is_constant() && to_constant_expr(simple_lemma).is_true())
{
#if 0
log.debug() << "string_refinementt::add_lemma : tautology" << messaget::eom;
@@ -1843,9 +1843,9 @@ exprt string_refinementt::get(const exprt &expr) const
{
const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
const exprt cond = get(if_expr.cond());
- if(cond.is_true())
+ if(cond.is_constant() && to_constant_expr(cond).is_true())
current = std::cref(if_expr.true_case());
- else if(cond.is_false())
+ else if(cond.is_constant() && to_constant_expr(cond).is_false())
current = std::cref(if_expr.false_case());
else
UNREACHABLE;
@@ -2021,7 +2021,7 @@ static bool is_valid_string_constraint(
const exprt i = pair.second[j];
const equal_exprt equals(rep, i);
const exprt result = simplify_expr(equals, ns);
- if(result.is_false())
+ if(result.is_constant() && to_constant_expr(result).is_false())
{
stream << "Indices not equal: " << to_string(constraint)
<< ", str: " << format(pair.first) << messaget::eom;
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
index 4b14ec6ec7f..87babfb8b68 100644
--- a/src/util/arith_tools.cpp
+++ b/src/util/arith_tools.cpp
@@ -25,7 +25,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
if(type_id==ID_pointer)
{
- if(is_null_pointer(expr))
+ if(expr.is_null_pointer())
{
int_value=0;
return false;
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index bb9c814a496..88f269f90a8 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -26,14 +26,14 @@ Author: Daniel Kroening, kroening@kroening.com
/// \return True if is a Boolean constant representing `true`, false otherwise.
bool exprt::is_true() const
{
- return is_constant() && is_boolean() && get(ID_value) != ID_false;
+ return is_constant() && to_constant_expr(*this).is_true();
}
/// Return whether the expression is a constant representing `false`.
/// \return True if is a Boolean constant representing `false`, false otherwise.
bool exprt::is_false() const
{
- return is_constant() && is_boolean() && get(ID_value) == ID_false;
+ return is_constant() && to_constant_expr(*this).is_false();
}
/// Return whether the expression is a constant representing 0.
@@ -47,44 +47,9 @@ bool exprt::is_false() const
bool exprt::is_zero() const
{
if(is_constant())
- {
- const constant_exprt &constant=to_constant_expr(*this);
- const irep_idt &type_id=type().id_string();
-
- if(type_id==ID_integer || type_id==ID_natural)
- {
- return constant.value_is_zero_string();
- }
- else if(type_id==ID_rational)
- {
- rationalt rat_value;
- if(to_rational(*this, rat_value))
- CHECK_RETURN(false);
- return rat_value.is_zero();
- }
- else if(
- type_id == ID_unsignedbv || type_id == ID_signedbv ||
- type_id == ID_c_bool || type_id == ID_c_bit_field)
- {
- return constant.value_is_zero_string();
- }
- else if(type_id==ID_fixedbv)
- {
- if(fixedbvt(constant)==0)
- return true;
- }
- else if(type_id==ID_floatbv)
- {
- if(ieee_floatt(constant)==0)
- return true;
- }
- else if(type_id==ID_pointer)
- {
- return is_null_pointer(constant);
- }
- }
-
- return false;
+ return to_constant_expr(*this).is_zero();
+ else
+ return false;
}
/// Return whether the expression is a constant representing 1.
@@ -96,47 +61,9 @@ bool exprt::is_zero() const
bool exprt::is_one() const
{
if(is_constant())
- {
- const auto &constant_expr = to_constant_expr(*this);
- const irep_idt &type_id = type().id();
-
- if(type_id==ID_integer || type_id==ID_natural)
- {
- mp_integer int_value =
- string2integer(id2string(constant_expr.get_value()));
- if(int_value==1)
- return true;
- }
- else if(type_id==ID_rational)
- {
- rationalt rat_value;
- if(to_rational(*this, rat_value))
- CHECK_RETURN(false);
- return rat_value.is_one();
- }
- else if(
- type_id == ID_unsignedbv || type_id == ID_signedbv ||
- type_id == ID_c_bool || type_id == ID_c_bit_field)
- {
- const auto width = to_bitvector_type(type()).get_width();
- mp_integer int_value =
- bvrep2integer(id2string(constant_expr.get_value()), width, false);
- if(int_value==1)
- return true;
- }
- else if(type_id==ID_fixedbv)
- {
- if(fixedbvt(constant_expr) == 1)
- return true;
- }
- else if(type_id==ID_floatbv)
- {
- if(ieee_floatt(constant_expr) == 1)
- return true;
- }
- }
-
- return false;
+ return to_constant_expr(*this).is_one();
+ else
+ return false;
}
/// Get a \ref source_locationt from the expression or from its operands
diff --git a/src/util/expr.h b/src/util/expr.h
index 08e1d57a7e0..8327843c852 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
#define CPROVER_UTIL_EXPR_H
#include "as_const.h"
+#include "deprecate.h"
#include "type.h"
#include "validate_expressions.h"
#include "validate_types.h"
@@ -214,9 +215,13 @@ class exprt:public irept
return id() == ID_constant;
}
+ DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_true() instead"))
bool is_true() const;
+ DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_false() instead"))
bool is_false() const;
+ DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_zero() instead"))
bool is_zero() const;
+ DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_one() instead"))
bool is_one() const;
/// Return whether the expression represents a Boolean.
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index 3525b2804e1..e78ef7970b0 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -66,7 +66,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
exprt result;
if(init_expr.id() == ID_nondet)
result = side_effect_expr_nondett(type, source_location);
- else if(init_expr.is_zero())
+ else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
result = from_integer(0, type);
else
result = duplicate_per_byte(init_expr, type, ns);
@@ -80,7 +80,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
exprt result;
if(init_expr.id() == ID_nondet)
result = side_effect_expr_nondett(type, source_location);
- else if(init_expr.is_zero())
+ else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
result = constant_exprt(ID_0, type);
else
result = duplicate_per_byte(init_expr, type, ns);
@@ -94,7 +94,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
exprt result;
if(init_expr.id() == ID_nondet)
result = side_effect_expr_nondett(type, source_location);
- else if(init_expr.is_zero())
+ else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
{
const std::size_t width = to_bitvector_type(type).get_width();
std::string value(width, '0');
@@ -112,7 +112,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
exprt result;
if(init_expr.id() == ID_nondet)
result = side_effect_expr_nondett(type, source_location);
- else if(init_expr.is_zero())
+ else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
{
auto sub_zero = expr_initializer_rec(
to_complex_type(type).subtype(), source_location, init_expr);
@@ -287,7 +287,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
exprt result;
if(init_expr.id() == ID_nondet)
result = side_effect_expr_nondett(type, source_location);
- else if(init_expr.is_zero())
+ else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
result = constant_exprt(irep_idt(), type);
else
result = duplicate_per_byte(init_expr, type, ns);
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index 7e4739a7372..6727edaf0d0 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -68,33 +68,7 @@ exprt make_binary(const exprt &expr)
with_exprt make_with_expr(const update_exprt &src)
{
- const exprt::operandst &designator=src.designator();
- PRECONDITION(!designator.empty());
-
- with_exprt result{exprt{}, exprt{}, exprt{}};
- exprt *dest=&result;
-
- for(const auto &expr : designator)
- {
- with_exprt tmp{exprt{}, exprt{}, exprt{}};
-
- if(expr.id() == ID_index_designator)
- {
- tmp.where() = to_index_designator(expr).index();
- }
- else if(expr.id() == ID_member_designator)
- {
- // irep_idt component_name=
- // to_member_designator(*it).get_component_name();
- }
- else
- UNREACHABLE;
-
- *dest=tmp;
- dest=&to_with_expr(*dest).new_value();
- }
-
- return result;
+ return src.make_with_expr();
}
exprt is_not_zero(
@@ -128,12 +102,17 @@ exprt is_not_zero(
exprt boolean_negate(const exprt &src)
{
+ PRECONDITION(src.is_boolean());
+
if(src.id() == ID_not)
return to_not_expr(src).op();
- else if(src.is_true())
- return false_exprt();
- else if(src.is_false())
- return true_exprt();
+ else if(auto constant_expr = expr_try_dynamic_cast<constant_exprt>(src))
+ {
+ if(constant_expr->is_true())
+ return false_exprt{};
+ else
+ return true_exprt{};
+ }
else
return not_exprt(src);
}
@@ -338,51 +317,15 @@ bool can_forward_propagatet::is_constant_address_of(const exprt &expr) const
constant_exprt make_boolean_expr(bool value)
{
- if(value)
- return true_exprt();
- else
- return false_exprt();
+ return constant_exprt{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)
{
- if(expr.type().id() != ID_pointer)
- return false;
-
- if(expr.get_value() == ID_NULL)
- return true;
-
- // We used to support "0" (when NULL_is_zero), but really front-ends should
- // resolve this and generate ID_NULL instead.
-#if 0
- return config.ansi_c.NULL_is_zero && expr.value_is_zero_string();
-#else
- INVARIANT(
- !expr.value_is_zero_string() || !config.ansi_c.NULL_is_zero,
- "front-end should use ID_NULL");
- return false;
-#endif
+ return expr.is_null_pointer();
}
diff --git a/src/util/expr_util.h b/src/util/expr_util.h
index b423dcdd9fb..558c0bd9ac9 100644
--- a/src/util/expr_util.h
+++ b/src/util/expr_util.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
* \date Sun Jul 31 21:54:44 BST 2011
*/
+#include "deprecate.h"
#include "irep.h"
#include <functional>
@@ -40,6 +41,7 @@ bool is_assignable(const exprt &);
exprt make_binary(const exprt &);
/// converts an update expr into a (possibly nested) with expression
+DEPRECATED(SINCE(2024, 9, 10, "use update_exprt::make_with_expr() instead"))
with_exprt make_with_expr(const update_exprt &);
/// converts a scalar/float expression to C/C++ Booleans
@@ -106,16 +108,19 @@ class can_forward_propagatet
};
/// returns true_exprt if given true and false_exprt otherwise
+DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::constant_exprt(bool)"))
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
/// true when \p expr has value zero and NULL_is_zero is true; returns false in
/// all other cases.
+DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_null_pointer() instead"))
bool is_null_pointer(const constant_exprt &expr);
#endif // CPROVER_UTIL_EXPR_UTIL_H
diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp
index 822dff02a35..f41a666d595 100644
--- a/src/util/fixedbv.cpp
+++ b/src/util/fixedbv.cpp
@@ -126,11 +126,6 @@ fixedbvt &fixedbvt::operator/=(const fixedbvt &o)
return *this;
}
-bool fixedbvt::operator==(int i) const
-{
- return v==power(2, spec.get_fraction_bits())*i;
-}
-
std::string fixedbvt::format(
const format_spect &format_spec) const
{
diff --git a/src/util/fixedbv.h b/src/util/fixedbv.h
index bf37be62b7f..57e2a2b6263 100644
--- a/src/util/fixedbv.h
+++ b/src/util/fixedbv.h
@@ -66,8 +66,6 @@ class fixedbvt
std::string format(const format_spect &format_spec) const;
- bool operator==(int i) const;
-
bool is_zero() const
{
return v==0;
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index 582edeaa093..bd9b2f70e3c 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -194,7 +194,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
return os << ieee_floatt(src);
else if(type == ID_pointer)
{
- if(is_null_pointer(src))
+ if(src.is_null_pointer())
return os << ID_NULL;
else if(
src.get_value() == "INVALID" || src.get_value().starts_with("INVALID-"))
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 1fee65294a2..29c1771a4b0 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -1024,13 +1024,6 @@ bool ieee_floatt::ieee_equal(const ieee_floatt &other) const
return *this==other;
}
-bool ieee_floatt::operator==(int i) const
-{
- ieee_floatt other(spec);
- other.from_integer(i);
- return *this==other;
-}
-
bool ieee_floatt::operator!=(const ieee_floatt &other) const
{
return !(*this==other);
diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h
index 788975ba040..74bb2a8316a 100644
--- a/src/util/ieee_float.h
+++ b/src/util/ieee_float.h
@@ -133,13 +133,6 @@ class ieee_floatt
ieee_float_spect spec;
- explicit ieee_floatt(const ieee_float_spect &_spec):
- rounding_mode(ROUND_TO_EVEN),
- spec(_spec), sign_flag(false), exponent(0), fraction(0),
- NaN_flag(false), infinity_flag(false)
- {
- }
-
explicit ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
: rounding_mode(__rounding_mode),
spec(std::move(__spec)),
@@ -151,21 +144,17 @@ class ieee_floatt
{
}
- explicit ieee_floatt(const floatbv_typet &type):
- rounding_mode(ROUND_TO_EVEN),
- spec(ieee_float_spect(type)),
- sign_flag(false),
- exponent(0),
- fraction(0),
- NaN_flag(false),
- infinity_flag(false)
+ explicit ieee_floatt(const ieee_float_spect &_spec)
+ : ieee_floatt(_spec, ROUND_TO_EVEN)
+ {
+ }
+
+ explicit ieee_floatt(const floatbv_typet &type)
+ : ieee_floatt(ieee_float_spect(type))
{
}
- ieee_floatt():
- rounding_mode(ROUND_TO_EVEN),
- sign_flag(false), exponent(0), fraction(0),
- NaN_flag(false), infinity_flag(false)
+ ieee_floatt() : ieee_floatt(ieee_float_spect{}, ROUND_TO_EVEN)
{
}
@@ -305,7 +294,6 @@ class ieee_floatt
// e.g., NAN==NAN
bool operator==(const ieee_floatt &other) const;
bool operator!=(const ieee_floatt &other) const;
- bool operator==(int i) const;
// these do IEEE equality, i.e., NAN!=NAN
bool ieee_equal(const ieee_floatt &other) const;
diff --git a/src/util/interval.cpp b/src/util/interval.cpp
index 48c6d49c609..b7ee86d0453 100644
--- a/src/util/interval.cpp
+++ b/src/util/interval.cpp
@@ -689,7 +689,7 @@ exprt constant_interval_exprt::generate_division_expression(
PRECONDITION(!is_zero(rhs));
- if(rhs.is_one())
+ if(rhs.is_constant() && to_constant_expr(rhs).is_one())
{
return lhs;
}
@@ -744,7 +744,7 @@ exprt constant_interval_exprt::generate_modulo_expression(
PRECONDITION(!is_zero(rhs));
- if(rhs.is_one())
+ if(rhs.is_constant() && to_constant_expr(rhs).is_one())
{
return lhs;
}
@@ -1269,7 +1269,7 @@ bool constant_interval_exprt::is_zero(const exprt &expr)
INVARIANT(!is_max(expr) && !is_min(expr), "We excluded those cases");
- if(expr.is_zero())
+ if(expr.is_constant() && to_constant_expr(expr).is_zero())
{
return true;
}
@@ -1351,7 +1351,8 @@ bool constant_interval_exprt::equal(const exprt &a, const exprt &b)
INVARIANT(!is_extreme(l, r), "We've excluded this before");
- return simplified_expr(equal_exprt(l, r)).is_true();
+ exprt simp_eq = simplified_expr(equal_exprt(l, r));
+ return simp_eq.is_constant() && to_constant_expr(simp_eq).is_true();
}
// TODO: Signed/unsigned comparisons.
@@ -1399,7 +1400,8 @@ bool constant_interval_exprt::less_than(const exprt &a, const exprt &b)
!is_extreme(l) && !is_extreme(r),
"We have excluded all of these cases in the code above");
- return simplified_expr(binary_relation_exprt(l, ID_lt, r)).is_true();
+ exprt simp_lt = simplified_expr(binary_relation_exprt(l, ID_lt, r));
+ return simp_lt.is_constant() && to_constant_expr(simp_lt).is_true();
}
bool constant_interval_exprt::greater_than(const exprt &a, const exprt &b)
@@ -1628,8 +1630,11 @@ constant_interval_exprt::typecast(const typet &type) const
{
if(is_boolean() && is_int(type))
{
- bool lower = !has_no_lower_bound() && get_lower().is_true();
- bool upper = has_no_upper_bound() || get_upper().is_true();
+ bool lower = !has_no_lower_bound() && get_lower().is_constant() &&
+ to_constant_expr(get_lower()).is_true();
+ bool upper =
+ has_no_upper_bound() ||
+ (get_upper().is_constant() && to_constant_expr(get_upper()).is_true());
INVARIANT(!lower || upper, "");
@@ -1875,7 +1880,9 @@ bool constant_interval_exprt::contains_zero() const
return false;
}
- if(get_lower().is_zero() || get_upper().is_zero())
+ if(
+ (get_lower().is_constant() && to_constant_expr(get_lower()).is_zero()) ||
+ (get_upper().is_constant() && to_constant_expr(get_upper()).is_zero()))
{
return true;
}
diff --git a/src/util/pointer_offset_sum.cpp b/src/util/pointer_offset_sum.cpp
index dc34d0eb0ce..238cd7d203e 100644
--- a/src/util/pointer_offset_sum.cpp
+++ b/src/util/pointer_offset_sum.cpp
@@ -19,9 +19,9 @@ exprt pointer_offset_sum(const exprt &a, const exprt &b)
return a;
else if(b.id() == ID_unknown)
return b;
- else if(a.is_zero())
+ else if(a.is_constant() && to_constant_expr(a).is_zero())
return b;
- else if(b.is_zero())
+ else if(b.is_constant() && to_constant_expr(b).is_zero())
return a;
return plus_exprt(a, typecast_exprt::conditional_cast(b, a.type()));
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 266de986ac4..26a036d0a25 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -105,7 +105,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
if(type.id()==ID_floatbv)
{
ieee_floatt value(to_constant_expr(expr.op()));
- return make_boolean_expr(value.get_sign());
+ return constant_exprt{value.get_sign()};
}
else if(type.id()==ID_signedbv ||
type.id()==ID_unsignedbv)
@@ -113,7 +113,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
const auto value = numeric_cast<mp_integer>(expr.op());
if(value.has_value())
{
- return make_boolean_expr(*value >= 0);
+ return constant_exprt{*value >= 0};
}
}
}
@@ -858,7 +858,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
if(
expr_type.id() == ID_pointer && expr.op().is_constant() &&
(to_constant_expr(expr.op()).get_value() == ID_NULL ||
- (expr.op().is_zero() && config.ansi_c.NULL_is_zero)))
+ (to_constant_expr(expr.op()).is_zero() && config.ansi_c.NULL_is_zero)))
{
exprt tmp = expr.op();
tmp.type()=expr.type();
@@ -904,9 +904,10 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
if(
(op_plus_expr.op0().id() == ID_typecast &&
- to_typecast_expr(op_plus_expr.op0()).op().is_zero()) ||
+ to_typecast_expr(op_plus_expr.op0()).op().is_constant() &&
+ to_constant_expr(to_typecast_expr(op_plus_expr.op0()).op()).is_zero()) ||
(op_plus_expr.op0().is_constant() &&
- is_null_pointer(to_constant_expr(op_plus_expr.op0()))))
+ to_constant_expr(op_plus_expr.op0()).is_null_pointer()))
{
auto sub_size =
pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
@@ -1032,7 +1033,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
if(expr_type_id==ID_bool)
{
- return make_boolean_expr(int_value != 0);
+ return constant_exprt{int_value != 0};
}
if(expr_type_id==ID_unsignedbv ||
@@ -1071,11 +1072,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
expr_type_id==ID_c_enum ||
expr_type_id==ID_c_bit_field)
{
- if(operand.is_true())
+ if(to_constant_expr(operand).is_true())
{
return from_integer(1, expr_type);
}
- else if(operand.is_false())
+ else if(to_constant_expr(operand).is_false())
{
return from_integer(0, expr_type);
}
@@ -1085,15 +1086,15 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
if(!c_enum_type.is_incomplete()) // possibly incomplete
{
- unsigned int_value = operand.is_true() ? 1u : 0u;
+ unsigned int_value = to_constant_expr(operand).is_true() ? 1u : 0u;
exprt tmp=from_integer(int_value, c_enum_type);
tmp.type()=expr_type; // we maintain the tag type
return std::move(tmp);
}
}
- else if(expr_type_id==ID_pointer &&
- operand.is_false() &&
- config.ansi_c.NULL_is_zero)
+ else if(
+ expr_type_id == ID_pointer && to_constant_expr(operand).is_false() &&
+ config.ansi_c.NULL_is_zero)
{
return null_pointer_exprt(to_pointer_type(expr_type));
}
@@ -1110,7 +1111,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
if(expr_type_id==ID_bool)
{
- return make_boolean_expr(int_value != 0);
+ return constant_exprt{int_value != 0};
}
if(expr_type_id==ID_c_bool)
@@ -2094,8 +2095,9 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
// byte update of full object is byte_extract(new value)
if(
- offset.is_zero() && val_size.has_value() && *val_size > 0 &&
- root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
+ offset.is_constant() && to_constant_expr(offset).is_zero() &&
+ val_size.has_value() && *val_size > 0 && root_size.has_value() &&
+ *root_size > 0 && *val_size >= *root_size)
{
byte_extract_exprt be(
matching_byte_extract_id,
@@ -2419,8 +2421,9 @@ simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr)
// When one operand is zero, an overflow can only occur for a subtraction from
// zero.
if(
- expr.op1().is_zero() ||
- (expr.op0().is_zero() && !can_cast_expr<minus_overflow_exprt>(expr)))
+ (expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero()) ||
+ (expr.op0().is_constant() && to_constant_expr(expr.op0()).is_zero() &&
+ !can_cast_expr<minus_overflow_exprt>(expr)))
{
return false_exprt{};
}
@@ -2428,7 +2431,8 @@ simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr)
// One is neutral element for multiplication
if(
can_cast_expr<mult_overflow_exprt>(expr) &&
- (expr.op0().is_one() || expr.op1().is_one()))
+ ((expr.op0().is_constant() && to_constant_expr(expr.op0()).is_one()) ||
+ (expr.op1().is_constant() && to_constant_expr(expr.op1()).is_one())))
{
return false_exprt{};
}
@@ -2489,7 +2493,7 @@ simplify_exprt::resultt<>
simplify_exprt::simplify_overflow_unary(const unary_overflow_exprt &expr)
{
// zero is a neutral element for all operations supported here
- if(expr.op().is_zero())
+ if(expr.op().is_constant() && to_constant_expr(expr.op()).is_zero())
return false_exprt{};
// catch some cases over mathematical types
@@ -2539,7 +2543,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
if(expr.id() == ID_overflow_result_unary_minus)
{
// zero is a neutral element
- if(expr.op0().is_zero())
+ if(expr.op0().is_constant() && to_constant_expr(expr.op0()).is_zero())
return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()};
// catch some cases over mathematical types
@@ -2590,7 +2594,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
{
// When one operand is zero, an overflow can only occur for a subtraction
// from zero.
- if(expr.op0().is_zero())
+ if(expr.op0().is_constant() && to_constant_expr(expr.op0()).is_zero())
{
if(
expr.id() == ID_overflow_result_plus ||
@@ -2604,7 +2608,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
{from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()};
}
}
- else if(expr.op1().is_zero())
+ else if(expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero())
{
if(
expr.id() == ID_overflow_result_plus ||
@@ -2623,10 +2627,14 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
// One is neutral element for multiplication
if(
expr.id() == ID_overflow_result_mult &&
- (expr.op0().is_one() || expr.op1().is_one()))
+ ((expr.op0().is_constant() && to_constant_expr(expr.op0()).is_one()) ||
+ (expr.op1().is_constant() && to_constant_expr(expr.op1()).is_one())))
{
return struct_exprt{
- {expr.op0().is_one() ? expr.op1() : expr.op0(), false_exprt{}},
+ {(expr.op0().is_constant() && to_constant_expr(expr.op0()).is_one())
+ ? expr.op1()
+ : expr.op0(),
+ false_exprt{}},
expr.type()};
}
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index 1a520182176..702819d6225 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -93,11 +93,15 @@ simplify_exprt::simplify_index(const index_exprt &expr)
exprt new_index_expr = simplify_index(
index_exprt(with_expr.old(), index, new_expr.type())); // recursive call
- if(equality_expr.is_true())
+ if(
+ equality_expr.is_constant() &&
+ to_constant_expr(equality_expr).is_true())
{
return with_expr.new_value();
}
- else if(equality_expr.is_false())
+ else if(
+ equality_expr.is_constant() &&
+ to_constant_expr(equality_expr).is_false())
{
return new_index_expr;
}
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 569c91ef837..6cf7d82e265 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -56,13 +56,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
bool erase;
- if(it->is_true())
+ if(it->is_constant() && to_constant_expr(*it).is_true())
{
erase=true;
negate=!negate;
}
else
- erase=it->is_false();
+ erase = it->is_constant() && to_constant_expr(*it).is_false();
if(erase)
{
@@ -75,7 +75,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
if(new_operands.empty())
{
- return make_boolean_expr(negate);
+ return constant_exprt{negate};
}
else if(new_operands.size() == 1)
{
@@ -110,8 +110,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
if(!it->is_boolean())
return unchanged(expr);
- bool is_true=it->is_true();
- bool is_false=it->is_false();
+ bool is_true = it->is_constant() && to_constant_expr(*it).is_true();
+ bool is_false = it->is_constant() && to_constant_expr(*it).is_false();
if(expr.id()==ID_and && is_false)
{
@@ -298,12 +298,12 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
op.id() == ID_not && op.is_boolean() &&
expr_set.find(to_not_expr(op).op()) != expr_set.end())
{
- return make_boolean_expr(expr.id() == ID_or);
+ return constant_exprt{expr.id() == ID_or};
}
if(new_operands.empty())
{
- return make_boolean_expr(expr.id() == ID_and);
+ return constant_exprt{expr.id() == ID_and};
}
else if(new_operands.size() == 1)
{
@@ -334,11 +334,11 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
{
return to_not_expr(op).op();
}
- else if(op.is_false())
+ else if(op.is_constant() && to_constant_expr(op).is_false())
{
return true_exprt();
}
- else if(op.is_true())
+ else if(op.is_constant() && to_constant_expr(op).is_true())
{
return false_exprt();
}
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index f7fdd2952b3..8f69dbaba88 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -27,7 +27,7 @@ simplify_exprt::simplify_isinf(const unary_exprt &expr)
if(expr.op().is_constant())
{
ieee_floatt value(to_constant_expr(expr.op()));
- return make_boolean_expr(value.is_infinity());
+ return constant_exprt{value.is_infinity()};
}
return unchanged(expr);
@@ -41,7 +41,7 @@ simplify_exprt::simplify_isnan(const unary_exprt &expr)
if(expr.op().is_constant())
{
ieee_floatt value(to_constant_expr(expr.op()));
- return make_boolean_expr(value.is_NaN());
+ return constant_exprt{value.is_NaN()};
}
return unchanged(expr);
@@ -55,7 +55,7 @@ simplify_exprt::simplify_isnormal(const unary_exprt &expr)
if(expr.op().is_constant())
{
ieee_floatt value(to_constant_expr(expr.op()));
- return make_boolean_expr(value.is_normal());
+ return constant_exprt{value.is_normal()};
}
return unchanged(expr);
@@ -116,7 +116,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
if(type.id()==ID_floatbv)
{
ieee_floatt value(to_constant_expr(expr.op0()));
- expr = make_boolean_expr(value.get_sign());
+ expr = constant_exprt{value.get_sign()};
return false;
}
else if(type.id()==ID_signedbv ||
@@ -125,7 +125,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
mp_integer value;
if(!to_integer(expr.op0(), value))
{
- expr = make_boolean_expr(value>=0);
+ expr = constant_exprt{value>=0};
return false;
}
}
@@ -325,8 +325,9 @@ simplify_exprt::simplify_floatbv_op(const ieee_float_op_exprt &expr)
}
// division by one? Exact for all rounding modes.
- if(expr.id()==ID_floatbv_div &&
- op1.is_constant() && op1.is_one())
+ if(
+ expr.id() == ID_floatbv_div && op1.is_constant() &&
+ to_constant_expr(op1).is_one())
{
return op0;
}
@@ -355,9 +356,9 @@ simplify_exprt::simplify_ieee_float_relation(const binary_relation_exprt &expr)
ieee_floatt f_rhs(to_constant_expr(expr.rhs()));
if(expr.id()==ID_ieee_float_notequal)
- return make_boolean_expr(f_lhs.ieee_not_equal(f_rhs));
+ return constant_exprt{f_lhs.ieee_not_equal(f_rhs)};
else if(expr.id()==ID_ieee_float_equal)
- return make_boolean_expr(f_lhs.ieee_equal(f_rhs));
+ return constant_exprt{f_lhs.ieee_equal(f_rhs)};
else
UNREACHABLE;
}
diff --git a/src/util/simplify_expr_if.cpp b/src/util/simplify_expr_if.cpp
index c951603af48..31188f7df39 100644
--- a/src/util/simplify_expr_if.cpp
+++ b/src/util/simplify_expr_if.cpp
@@ -250,8 +250,8 @@ simplify_exprt::simplify_if_preorder(const if_exprt &expr)
// 1 ? a : b -> a and 0 ? a : b -> b
if(r_cond.expr.is_constant())
{
- return changed(
- simplify_rec(r_cond.expr.is_true() ? truevalue : falsevalue));
+ return changed(simplify_rec(
+ to_constant_expr(r_cond.expr).is_true() ? truevalue : falsevalue));
}
if(do_simplify_if)
@@ -350,33 +350,39 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
{
// a?b:c <-> (a && b) || (!a && c)
- if(truevalue.is_true() && falsevalue.is_false())
+ if(
+ truevalue.is_constant() && to_constant_expr(truevalue).is_true() &&
+ falsevalue.is_constant() && to_constant_expr(falsevalue).is_false())
{
// a?1:0 <-> a
return cond;
}
- else if(truevalue.is_false() && falsevalue.is_true())
+ else if(
+ truevalue.is_constant() && to_constant_expr(truevalue).is_false() &&
+ falsevalue.is_constant() && to_constant_expr(falsevalue).is_true())
{
// a?0:1 <-> !a
return changed(simplify_not(not_exprt(cond)));
}
- else if(falsevalue.is_false())
+ else if(
+ falsevalue.is_constant() && to_constant_expr(falsevalue).is_false())
{
// a?b:0 <-> a AND b
return changed(simplify_boolean(and_exprt(cond, truevalue)));
}
- else if(falsevalue.is_true())
+ else if(
+ falsevalue.is_constant() && to_constant_expr(falsevalue).is_true())
{
// a?b:1 <-> !a OR b
return changed(
simplify_boolean(or_exprt(simplify_not(not_exprt(cond)), truevalue)));
}
- else if(truevalue.is_true())
+ else if(truevalue.is_constant() && to_constant_expr(truevalue).is_true())
{
// a?1:b <-> a||(!a && b) <-> a OR b
return changed(simplify_boolean(or_exprt(cond, falsevalue)));
}
- else if(truevalue.is_false())
+ else if(truevalue.is_constant() && to_constant_expr(truevalue).is_false())
{
// a?0:b <-> !a && b
return changed(simplify_boolean(
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 473f75bb450..5cbce879efa 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -189,8 +189,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr)
// if one of the operands is zero the result is zero
// note: not true on IEEE floating point arithmetic
- if(it->is_zero() &&
- it->type().id()!=ID_floatbv)
+ if(
+ it->is_constant() && to_constant_expr(*it).is_zero() &&
+ it->type().id() != ID_floatbv)
{
return from_integer(0, expr.type());
}
@@ -250,7 +251,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr)
else
{
// if the constant is a one and there are other factors
- if(constant_found && constant->is_one())
+ if(constant_found && to_constant_expr(*constant).is_one())
{
// just delete it
new_operands.erase(constant);
@@ -343,8 +344,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_div(const div_exprt &expr)
else if(expr_type.id()==ID_fixedbv)
{
// division by one?
- if(expr.op1().is_constant() &&
- expr.op1().is_one())
+ if(expr.op1().is_constant() && to_constant_expr(expr.op1()).is_one())
{
return expr.op0();
}
@@ -538,7 +538,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr)
it != new_operands.end();
/* no it++ */)
{
- if(is_number(it->type()) && it->is_zero())
+ if(
+ is_number(it->type()) && it->is_constant() &&
+ to_constant_expr(*it).is_zero())
{
it = new_operands.erase(it);
no_change = false;
@@ -619,7 +621,8 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
if(
offset_op0.is_constant() && offset_op1.is_constant() &&
object_size.has_value() && element_size.has_value() &&
- element_size->is_constant() && !element_size->is_zero() &&
+ element_size->is_constant() &&
+ !to_constant_expr(*element_size).is_zero() &&
numeric_cast_v<mp_integer>(to_constant_expr(offset_op0)) <=
*object_size &&
numeric_cast_v<mp_integer>(to_constant_expr(offset_op1)) <=
@@ -647,7 +650,7 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
if(
element_size.has_value() && element_size->is_constant() &&
- !element_size->is_zero())
+ !to_constant_expr(*element_size).is_zero())
{
return changed(simplify_rec(div_exprt{
minus_exprt{offset_op0, offset_op1},
@@ -675,7 +678,9 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
if(op.id() == ID_typecast && to_typecast_expr(op).op().is_boolean())
{
}
- else if(op.is_zero() || op.is_one())
+ else if(
+ op.is_constant() &&
+ (to_constant_expr(op).is_zero() || to_constant_expr(op).is_one()))
{
}
else
@@ -700,9 +705,9 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
{
if(it->id()==ID_typecast)
*it = to_typecast_expr(*it).op();
- else if(it->is_zero())
+ else if(it->is_constant() && to_constant_expr(*it).is_zero())
*it=false_exprt();
- else if(it->is_one())
+ else if(it->is_constant() && to_constant_expr(*it).is_one())
*it=true_exprt();
}
@@ -770,14 +775,16 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
for(exprt::operandst::iterator it = new_expr.operands().begin();
it != new_expr.operands().end();) // no it++
{
- if(it->is_zero() && new_expr.operands().size() > 1)
+ if(
+ it->is_constant() && to_constant_expr(*it).is_zero() &&
+ new_expr.operands().size() > 1)
{
it = new_expr.operands().erase(it);
no_change = false;
}
else if(
it->is_constant() && it->type().id() == ID_bv &&
- to_constant_expr(*it).value_is_zero_string() &&
+ *it == to_bv_type(it->type()).all_zeros_expr() &&
new_expr.operands().size() > 1)
{
it = new_expr.operands().erase(it);
@@ -859,7 +866,7 @@ simplify_exprt::simplify_extractbit(const extractbit_exprt &expr)
src_bit_width,
numeric_cast_v<std::size_t>(*index_converted_to_int));
- return make_boolean_expr(bit);
+ return constant_exprt{bit};
}
simplify_exprt::resultt<>
@@ -875,9 +882,11 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr)
Forall_operands(it, new_expr)
{
exprt &op=*it;
- if(op.is_true() || op.is_false())
+ if(
+ op.is_constant() &&
+ (to_constant_expr(op).is_true() || to_constant_expr(op).is_false()))
{
- const bool value = op.is_true();
+ const bool value = to_constant_expr(op).is_true();
op = from_integer(value, unsignedbv_typet(1));
no_change = false;
}
@@ -1452,7 +1461,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
}
equal = tmp0_const.is_zero() && tmp1_const.is_zero();
}
- return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
+ return constant_exprt{expr.id() == ID_equal ? equal : !equal};
}
if(tmp0.type().id() == ID_fixedbv)
@@ -1461,13 +1470,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
fixedbvt f1(tmp1_const);
if(expr.id() == ID_ge)
- return make_boolean_expr(f0 >= f1);
+ return constant_exprt{f0 >= f1};
else if(expr.id() == ID_le)
- return make_boolean_expr(f0 <= f1);
+ return constant_exprt{f0 <= f1};
else if(expr.id() == ID_gt)
- return make_boolean_expr(f0 > f1);
+ return constant_exprt{f0 > f1};
else if(expr.id() == ID_lt)
- return make_boolean_expr(f0 < f1);
+ return constant_exprt{f0 < f1};
else
UNREACHABLE;
}
@@ -1477,13 +1486,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
ieee_floatt f1(tmp1_const);
if(expr.id() == ID_ge)
- return make_boolean_expr(f0 >= f1);
+ return constant_exprt{f0 >= f1};
else if(expr.id() == ID_le)
- return make_boolean_expr(f0 <= f1);
+ return constant_exprt{f0 <= f1};
else if(expr.id() == ID_gt)
- return make_boolean_expr(f0 > f1);
+ return constant_exprt{f0 > f1};
else if(expr.id() == ID_lt)
- return make_boolean_expr(f0 < f1);
+ return constant_exprt{f0 < f1};
else
UNREACHABLE;
}
@@ -1498,13 +1507,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
return unchanged(expr);
if(expr.id() == ID_ge)
- return make_boolean_expr(r0 >= r1);
+ return constant_exprt{r0 >= r1};
else if(expr.id() == ID_le)
- return make_boolean_expr(r0 <= r1);
+ return constant_exprt{r0 <= r1};
else if(expr.id() == ID_gt)
- return make_boolean_expr(r0 > r1);
+ return constant_exprt{r0 > r1};
else if(expr.id() == ID_lt)
- return make_boolean_expr(r0 < r1);
+ return constant_exprt{r0 < r1};
else
UNREACHABLE;
}
@@ -1521,13 +1530,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
return unchanged(expr);
if(expr.id() == ID_ge)
- return make_boolean_expr(*v0 >= *v1);
+ return constant_exprt{*v0 >= *v1};
else if(expr.id() == ID_le)
- return make_boolean_expr(*v0 <= *v1);
+ return constant_exprt{*v0 <= *v1};
else if(expr.id() == ID_gt)
- return make_boolean_expr(*v0 > *v1);
+ return constant_exprt{*v0 > *v1};
else if(expr.id() == ID_lt)
- return make_boolean_expr(*v0 < *v1);
+ return constant_exprt{*v0 < *v1};
else
UNREACHABLE;
}
@@ -1537,9 +1546,10 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1)
{
// we can't eliminate zeros
if(
- op0.is_zero() || op1.is_zero() ||
- (op0.is_constant() && is_null_pointer(to_constant_expr(op0))) ||
- (op1.is_constant() && is_null_pointer(to_constant_expr(op1))))
+ (op0.is_constant() && to_constant_expr(op0).is_zero()) ||
+ (op1.is_constant() && to_constant_expr(op1).is_zero()) ||
+ (op0.is_constant() && to_constant_expr(op0).is_null_pointer()) ||
+ (op1.is_constant() && to_constant_expr(op1).is_null_pointer()))
{
return true;
}
@@ -1566,8 +1576,9 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1)
}
else if(op0==op1)
{
- if(!op0.is_zero() &&
- op0.type().id()!=ID_complex)
+ if(
+ (!op0.is_constant() || !to_constant_expr(op0).is_zero()) &&
+ op0.type().id() != ID_complex)
{
// elimination!
op0=from_integer(0, op0.type());
@@ -1625,7 +1636,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
std::move(offset), ID_lt, std::move(*object_size)})
.expr;
if(in_object_bounds.is_constant())
- return tvt{in_object_bounds.is_true()};
+ return tvt{to_constant_expr(in_object_bounds).is_true()};
}
return tvt::unknown();
@@ -1736,7 +1747,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
const constant_exprt &op1_constant = to_constant_expr(expr.op1());
- if(is_null_pointer(op1_constant))
+ if(op1_constant.is_null_pointer())
{
// the address of an object is never NULL
@@ -1799,8 +1810,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
exprt ptr = simplify_object(expr.op0()).expr;
// NULL + N == NULL is N == 0
- if(ptr.is_constant() && is_null_pointer(to_constant_expr(ptr)))
- return make_boolean_expr(offset.is_zero());
+ if(ptr.is_constant() && to_constant_expr(ptr).is_null_pointer())
+ return constant_exprt{to_constant_expr(offset).is_zero()};
// &x + N == NULL is false when the offset is in bounds
else if(auto address_of = expr_try_dynamic_cast<address_of_exprt>(ptr))
{
@@ -1887,7 +1898,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
// is the constant zero?
- if(expr.op1().is_zero())
+ if(expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero())
{
if(expr.id()==ID_ge &&
expr.op0().type().id()==ID_unsignedbv)
@@ -1976,13 +1987,17 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op();
// we re-write (TYPE)boolean == 0 -> !boolean
- if(expr.op1().is_zero() && expr.id()==ID_equal)
+ if(
+ expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero() &&
+ expr.id() == ID_equal)
{
return changed(simplify_not(not_exprt(lhs_typecast_op)));
}
// we re-write (TYPE)boolean != 0 -> boolean
- if(expr.op1().is_zero() && expr.id()==ID_notequal)
+ if(
+ expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero() &&
+ expr.id() == ID_notequal)
{
return lhs_typecast_op;
}
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 1511717dd94..92e1b3e8d7f 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -38,7 +38,7 @@ static bool is_dereference_integer_object(
{
const constant_exprt &constant = to_constant_expr(pointer);
- if(is_null_pointer(constant))
+ if(constant.is_null_pointer())
{
address=0;
return true;
@@ -218,11 +218,15 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
}
// condition is a constant?
- if(new_if_expr.cond().is_true())
+ if(
+ new_if_expr.cond().is_constant() &&
+ to_constant_expr(new_if_expr.cond()).is_true())
{
return new_if_expr.true_case();
}
- else if(new_if_expr.cond().is_false())
+ else if(
+ new_if_expr.cond().is_constant() &&
+ to_constant_expr(new_if_expr.cond()).is_false())
{
return new_if_expr.false_case();
}
@@ -246,7 +250,9 @@ simplify_exprt::simplify_address_of(const address_of_exprt &expr)
{
auto index_expr = to_index_expr(new_object.expr);
- if(!index_expr.index().is_zero())
+ if(
+ !index_expr.index().is_constant() ||
+ !to_constant_expr(index_expr.index()).is_zero())
{
// we normalize &a[i] to (&a[0])+i
exprt offset = index_expr.op1();
@@ -353,7 +359,7 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
{
if(op.type().id()==ID_pointer)
ptr_expr.push_back(op);
- else if(!op.is_zero())
+ else if(!op.is_constant() || !to_constant_expr(op).is_zero())
{
exprt tmp=op;
if(tmp.type()!=expr.type())
@@ -398,7 +404,7 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
{
const constant_exprt &c_ptr = to_constant_expr(ptr);
- if(is_null_pointer(c_ptr))
+ if(c_ptr.is_null_pointer())
{
return from_integer(0, expr.type());
}
@@ -424,7 +430,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
if(
tmp0_address_of.object().id() == ID_index &&
- to_index_expr(tmp0_address_of.object()).index().is_zero())
+ to_index_expr(tmp0_address_of.object()).index().is_constant() &&
+ to_constant_expr(to_index_expr(tmp0_address_of.object()).index()).is_zero())
{
tmp0_address_of =
address_of_exprt(to_index_expr(tmp0_address_of.object()).array());
@@ -438,7 +445,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
if(
tmp1_address_of.object().id() == ID_index &&
- to_index_expr(tmp1_address_of.object()).index().is_zero())
+ to_index_expr(tmp1_address_of.object()).index().is_constant() &&
+ to_constant_expr(to_index_expr(tmp1_address_of.object()).index()).is_zero())
{
tmp1 = address_of_exprt(to_index_expr(tmp1_address_of.object()).array());
}
@@ -451,7 +459,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
bool equal = to_symbol_expr(tmp0_object).get_identifier() ==
to_symbol_expr(tmp1_object).get_identifier();
- return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
+ return constant_exprt{expr.id() == ID_equal ? equal : !equal};
}
else if(
tmp0_object.id() == ID_dynamic_object &&
@@ -460,19 +468,19 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
bool equal = to_dynamic_object_expr(tmp0_object).get_instance() ==
to_dynamic_object_expr(tmp1_object).get_instance();
- return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
+ return constant_exprt{expr.id() == ID_equal ? equal : !equal};
}
else if(
(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
(tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
{
- return make_boolean_expr(expr.id() != ID_equal);
+ return constant_exprt{expr.id() != ID_equal};
}
else if(
tmp0_object.id() == ID_string_constant &&
tmp1_object.id() == ID_string_constant && tmp0_object == tmp1_object)
{
- return make_boolean_expr(expr.id() == ID_equal);
+ return constant_exprt{expr.id() == ID_equal};
}
return unchanged(expr);
@@ -500,7 +508,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_pointer_object(
return unchanged(expr);
}
}
- else if(!op.is_constant() || !op.is_zero())
+ else if(!op.is_constant() || !to_constant_expr(op).is_zero())
{
return unchanged(expr);
}
@@ -571,7 +579,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
}
// NULL is not dynamic
- if(op.is_constant() && is_null_pointer(to_constant_expr(op)))
+ if(op.is_constant() && to_constant_expr(op).is_null_pointer())
return false_exprt();
// &something depends on the something
@@ -584,8 +592,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
const irep_idt identifier = to_symbol_expr(op_object).get_identifier();
// this is for the benefit of symex
- return make_boolean_expr(
- identifier.starts_with(SYMEX_DYNAMIC_PREFIX "::"));
+ return constant_exprt{identifier.starts_with(SYMEX_DYNAMIC_PREFIX "::")};
}
else if(op_object.id() == ID_string_constant)
{
@@ -619,7 +626,7 @@ simplify_exprt::simplify_is_invalid_pointer(const unary_exprt &expr)
}
// NULL is not invalid
- if(op.is_constant() && is_null_pointer(to_constant_expr(op)))
+ if(op.is_constant() && to_constant_expr(op).is_null_pointer())
{
return false_exprt();
}
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 80b1961508c..9ad47c77688 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -172,7 +172,9 @@ simplify_exprt::simplify_member(const member_exprt &expr)
{
// rewrite byte_extract(X, 0).member to X
// if the type of X is that of the member
- if(byte_extract_expr.offset().is_zero())
+ if(
+ byte_extract_expr.offset().is_constant() &&
+ to_constant_expr(byte_extract_expr.offset()).is_zero())
{
const union_typet &union_type =
op.type().id() == ID_union_tag
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index 3b61acd4d08..624d43e3f22 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -439,7 +439,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
}
else if(type.id() == ID_pointer)
{
- if(config.ansi_c.NULL_is_zero && is_null_pointer(to_constant_expr(expr)))
+ if(config.ansi_c.NULL_is_zero && to_constant_expr(expr).is_null_pointer())
return std::string(to_bitvector_type(type).get_width(), '0');
else
return {};
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 50cb5684220..d1f57046ca6 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -8,19 +8,155 @@ Author: Daniel Kroening, kroening@kroening.com
#include "std_expr.h"
+#include "arith_tools.h"
+#include "config.h"
+#include "expr_util.h"
+#include "fixedbv.h"
+#include "ieee_float.h"
+#include "mathematical_types.h"
#include "namespace.h"
#include "pointer_expr.h"
#include "range.h"
+#include "rational.h"
+#include "rational_tools.h"
#include "substitute_symbols.h"
#include <map>
+constant_exprt::constant_exprt(bool value)
+ : constant_exprt(value ? ID_true : ID_false, bool_typet{})
+{
+}
+
bool constant_exprt::value_is_zero_string() const
{
const std::string val=id2string(get_value());
return val.find_first_not_of('0')==std::string::npos;
}
+bool constant_exprt::is_true() const
+{
+ return is_boolean() && get_value() != ID_false;
+}
+
+bool constant_exprt::is_false() const
+{
+ return is_boolean() && get_value() == ID_false;
+}
+
+bool constant_exprt::is_zero() const
+{
+ const irep_idt &type_id = type().id();
+
+ if(type_id == ID_integer)
+ {
+ return integer_typet{}.zero_expr() == *this;
+ }
+ else if(type_id == ID_natural)
+ {
+ return natural_typet{}.zero_expr() == *this;
+ }
+ else if(type_id == ID_real)
+ {
+ return real_typet{}.zero_expr() == *this;
+ }
+ else if(type_id == ID_rational)
+ {
+ rationalt rat_value;
+ if(to_rational(*this, rat_value))
+ CHECK_RETURN(false);
+ return rat_value.is_zero();
+ }
+ else if(
+ type_id == ID_unsignedbv || type_id == ID_signedbv ||
+ type_id == ID_c_bool || type_id == ID_c_bit_field)
+ {
+ return value_is_zero_string();
+ }
+ else if(type_id == ID_fixedbv)
+ {
+ return fixedbvt(*this).is_zero();
+ }
+ else if(type_id == ID_floatbv)
+ {
+ return ieee_floatt(*this).is_zero();
+ }
+ else if(type_id == ID_pointer)
+ {
+ return is_null_pointer();
+ }
+ else
+ return false;
+}
+
+bool constant_exprt::is_one() const
+{
+ const irep_idt &type_id = type().id();
+
+ if(type_id == ID_integer)
+ {
+ return integer_typet{}.one_expr() == *this;
+ }
+ else if(type_id == ID_natural)
+ {
+ return natural_typet{}.one_expr() == *this;
+ }
+ else if(type_id == ID_real)
+ {
+ return real_typet{}.one_expr() == *this;
+ }
+ else if(type_id == ID_rational)
+ {
+ rationalt rat_value;
+ if(to_rational(*this, rat_value))
+ CHECK_RETURN(false);
+ return rat_value.is_one();
+ }
+ else if(
+ type_id == ID_unsignedbv || type_id == ID_signedbv ||
+ type_id == ID_c_bool || type_id == ID_c_bit_field)
+ {
+ const auto width = to_bitvector_type(type()).get_width();
+ mp_integer int_value = bvrep2integer(id2string(get_value()), width, false);
+ return int_value == 1;
+ }
+ else if(type_id == ID_fixedbv)
+ {
+ fixedbv_spect spec{to_fixedbv_type(type())};
+ fixedbvt one{spec};
+ one.from_integer(1);
+ return one == fixedbvt{*this};
+ }
+ else if(type_id == ID_floatbv)
+ {
+ ieee_floatt one{to_floatbv_type(type())};
+ one.from_integer(1);
+ return one == ieee_floatt{*this};
+ }
+ else
+ return false;
+}
+
+bool constant_exprt::is_null_pointer() const
+{
+ if(type().id() != ID_pointer)
+ return false;
+
+ if(get_value() == ID_NULL)
+ return true;
+
+ // We used to support "0" (when NULL_is_zero), but really front-ends should
+ // resolve this and generate ID_NULL instead.
+#if 0
+ return config.ansi_c.NULL_is_zero && value_is_zero_string();
+#else
+ INVARIANT(
+ !value_is_zero_string() || !config.ansi_c.NULL_is_zero,
+ "front-end should use ID_NULL");
+ return false;
+#endif
+}
+
void constant_exprt::check(const exprt &expr, const validation_modet vm)
{
nullary_exprt::check(expr, vm);
@@ -63,12 +199,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));
@@ -174,6 +335,37 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
}
}
+with_exprt update_exprt::make_with_expr() const
+{
+ const exprt::operandst &designators = designator();
+ PRECONDITION(!designators.empty());
+
+ with_exprt result{exprt{}, exprt{}, exprt{}};
+ exprt *dest = &result;
+
+ for(const auto &expr : designators)
+ {
+ with_exprt tmp{exprt{}, exprt{}, exprt{}};
+
+ if(expr.id() == ID_index_designator)
+ {
+ tmp.where() = to_index_designator(expr).index();
+ }
+ else if(expr.id() == ID_member_designator)
+ {
+ // irep_idt component_name=
+ // to_member_designator(*it).get_component_name();
+ }
+ else
+ UNREACHABLE;
+
+ *dest = tmp;
+ dest = &to_with_expr(*dest).new_value();
+ }
+
+ return result;
+}
+
exprt binding_exprt::instantiate(const operandst &values) const
{
// number of values must match the number of bound variables
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 431de0bfa00..71006ee4050 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<and_exprt>(const exprt &base)
{
@@ -2698,6 +2703,9 @@ class update_exprt : public ternary_exprt
return op2();
}
+ /// converts an update expr into a (possibly nested) with expression
+ with_exprt make_with_expr() const;
+
static void check(
const exprt &expr,
const validation_modet vm = validation_modet::INVARIANT)
@@ -2992,6 +3000,9 @@ class constant_exprt : public nullary_exprt
set_value(_value);
}
+ /// returns true_exprt if given true and false_exprt otherwise
+ explicit constant_exprt(bool);
+
const irep_idt &get_value() const
{
return get(ID_value);
@@ -3002,7 +3013,36 @@ class constant_exprt : public nullary_exprt
set(ID_value, value);
}
- bool value_is_zero_string() const;
+ /// Return whether the expression is a constant representing `true`.
+ /// \return True if is a Boolean value representing `true`, false otherwise.
+ bool is_true() const;
+
+ /// Return whether the expression is a constant representing `false`.
+ /// \return True if is a Boolean constant representing `false`, false otherwise.
+ bool is_false() const;
+
+ /// Return whether the expression is a constant representing 0.
+ /// Will consider the following types: ID_integer, ID_natural, ID_rational,
+ /// ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv,
+ /// ID_floatbv, ID_pointer.<br>
+ /// For ID_pointer, returns true iff the value is a zero string or a null
+ /// pointer.
+ /// For everything not in the above list, return false.
+ /// \return True if has value 0, false otherwise.
+ bool is_zero() const;
+
+ /// Return whether the expression is a constant representing 1.
+ /// Will consider the following types: ID_integer, ID_natural, ID_rational,
+ /// ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv,
+ /// ID_floatbv.<br>
+ /// For all other types, return false.
+ /// \return True if has value 1, false otherwise.
+ bool is_one() const;
+
+ /// Returns true if \p expr has a pointer type and a value NULL; it also
+ /// returns true when \p expr has value zero and NULL_is_zero is true; returns
+ /// false in all other cases.
+ bool is_null_pointer() const;
static void check(
const exprt &expr,
@@ -3015,6 +3055,9 @@ class constant_exprt : public nullary_exprt
{
check(expr, vm);
}
+
+protected:
+ bool value_is_zero_string() const;
};
template <>
diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp
index dc21adae69e..de56f91a7a6 100644
--- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp
+++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp
@@ -803,7 +803,8 @@ void ASSUME_TRUE(
auto assumption = env.do_assume(expr, ns);
REQUIRE(assumption.id() != ID_nil);
REQUIRE(assumption.is_boolean());
- REQUIRE(assumption.is_true());
+ REQUIRE(assumption.is_constant());
+ REQUIRE(to_constant_expr(assumption).is_true());
}
}
@@ -817,7 +818,8 @@ void ASSUME_FALSE(
auto assumption = env.do_assume(expr, ns);
REQUIRE(assumption.id() != ID_nil);
REQUIRE(assumption.is_boolean());
- REQUIRE(assumption.is_false());
+ REQUIRE(assumption.is_constant());
+ REQUIRE(to_constant_expr(assumption).is_false());
}
}
diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp
index afd79a0e43c..7762afdc748 100644
--- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp
+++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp
@@ -34,7 +34,8 @@ static void ASSUME_TRUE(
REQUIRE(assumption.id() != ID_nil);
REQUIRE(assumption.is_boolean());
- REQUIRE(assumption.is_true());
+ REQUIRE(assumption.is_constant());
+ REQUIRE(to_constant_expr(assumption).is_true());
}
static void EXPECT_RESULT(
diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp
index 8e5d02395e6..7d76dd61fab 100644
--- a/unit/goto-symex/goto_symex_state.cpp
+++ b/unit/goto-symex/goto_symex_state.cpp
@@ -172,8 +172,7 @@ SCENARIO(
const symbol_exprt object_symbol =
to_symbol_expr(object_descriptor->object());
REQUIRE(object_symbol.get_identifier() == "int_value!0");
- REQUIRE(to_constant_expr(object_descriptor->offset())
- .value_is_zero_string());
+ REQUIRE(to_constant_expr(object_descriptor->offset()).is_zero());
}
THEN("The target equations are unchanged")
{
diff --git a/unit/goto-symex/shadow_memory_util.cpp b/unit/goto-symex/shadow_memory_util.cpp
index 3fec5ef0c4c..e6700c46545 100644
--- a/unit/goto-symex/shadow_memory_util.cpp
+++ b/unit/goto-symex/shadow_memory_util.cpp
@@ -263,7 +263,7 @@ exprt simplify_bit_or_exprt(const exprt &expr)
for(const auto &operand : or_expr->operands())
{
const exprt reduced = simplify_bit_or_exprt(operand);
- res |= reduced.is_true();
+ res |= reduced.is_constant() && to_constant_expr(reduced).is_true();
}
return from_integer(res, bool_typet{});
}
diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp
index 462708fb3b0..dccae7f5d16 100644
--- a/unit/util/expr.cpp
+++ b/unit/util/expr.cpp
@@ -20,7 +20,7 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
THEN("is_zero() should be false")
{
- REQUIRE_FALSE(bitfield3.is_zero());
+ REQUIRE_FALSE(to_constant_expr(bitfield3).is_zero());
}
}
GIVEN("An exprt representing a bitfield constant of 0")
@@ -30,7 +30,7 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
THEN("is_zero() should be true")
{
- REQUIRE(bitfield0.is_zero());
+ REQUIRE(to_constant_expr(bitfield0).is_zero());
}
}
}
diff --git a/unit/util/interval/get_extreme.cpp b/unit/util/interval/get_extreme.cpp
index 63c15d3f5d0..0c79efd58d9 100644
--- a/unit/util/interval/get_extreme.cpp
+++ b/unit/util/interval/get_extreme.cpp
@@ -41,7 +41,8 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]")
THEN("Require it is TRUE")
{
- REQUIRE(op1.is_true());
+ REQUIRE(op1.is_constant());
+ REQUIRE(to_constant_expr(op1).is_true());
REQUIRE(interval_eval);
}
}
@@ -55,7 +56,8 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]")
THEN("Require it is FALSE")
{
- REQUIRE(op1.is_false());
+ REQUIRE(op1.is_constant());
+ REQUIRE(to_constant_expr(op1).is_false());
REQUIRE_FALSE(interval_eval);
}
}
@@ -70,7 +72,8 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]")
THEN("Require it is TRUE")
{
- REQUIRE(op1.is_true());
+ REQUIRE(op1.is_constant());
+ REQUIRE(to_constant_expr(op1).is_true());
REQUIRE(interval_eval);
REQUIRE(constant_interval_exprt::equal(CEV(1), CEV(1)));
}
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 18a4f4b88c5..6aee7d9128f 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -246,7 +246,8 @@ TEST_CASE("Simplify pointer_object equality", "[core][util]")
exprt simp = simplify_expr(equal_exprt{p_o_void, p_o_int}, ns);
- REQUIRE(simp.is_true());
+ REQUIRE(simp.is_constant());
+ REQUIRE(to_constant_expr(simp).is_true());
}
TEST_CASE("Simplify cast from bool", "[core][util]")