Move is_{true,false,zero,one} from exprt to constant_exprt

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(

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

@@ -69,7 +69,8 @@
 
 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 @@
     {
       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)

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());

src/analyses/custom_bitvector_analysis.cpp

@@ -530,7 +530,7 @@
 
       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;
@@ -814,12 +814,12 @@
       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 @@
         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)

src/analyses/goto_rw.cpp

@@ -116,17 +116,17 @@
   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 @@
   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 @@
     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(

src/analyses/guard_bdd.cpp

@@ -44,7 +44,7 @@
   }
   else
   {
-    if(expr.is_false())
+    if(expr.is_constant() && to_constant_expr(expr).is_false())
     {
       return boolean_negate(as_expr());
     }

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

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);

src/analyses/interval_analysis.cpp

@@ -46,7 +46,10 @@
     {
       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 @@
     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);
     }
 

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();
     }
   }

src/analyses/invariant_set.cpp

@@ -394,14 +394,17 @@
     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 @@
   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 @@
   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)
   {

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();

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)
       {

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)));

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -275,7 +275,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();
@@ -579,10 +579,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();
 }
@@ -640,7 +640,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();
   }
@@ -833,7 +833,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))
     {