Value-set dereference: use cond_exprt to avoid quadratic guards

src/pointer-analysis/value_set_dereference.cpp

@@ -107,12 +107,12 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
         may_fail=true;
   }
 
+  exprt failure_value;
+
   if(may_fail)
   {
     // first see if we have a "failed object" for this pointer
 
-    exprt failure_value;
-
     if(
       const symbolt *failed_symbol =
         dereference_callback.get_or_create_failed_symbol(pointer))
@@ -138,36 +138,61 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
       failure_value=symbol.symbol_expr();
       failure_value.set(ID_C_invalid_object, true);
     }
-
-    valuet value;
-    value.value=failure_value;
-    value.pointer_guard=true_exprt();
-    values.push_front(value);
   }
 
   // now build big case split, but we only do "good" objects
 
-  exprt value=nil_exprt();
-
-  for(std::list<valuet>::const_iterator
-      it=values.begin();
-      it!=values.end();
-      it++)
+  optionalt<exprt> value_without_condition;
+  cond_exprt cond({}, type, true);
+  for(const auto &alias_value : values)
   {
-    if(it->value.is_not_nil())
+    if(alias_value.value.is_not_nil())
     {
-      if(value.is_nil()) // first?
-        value=it->value;
+      if(alias_value.pointer_guard.is_false())
+      {
+        INVARIANT(
+          !value_without_condition.has_value(),
+          "can't discriminate between two different catch-all aliases");
+        value_without_condition = alias_value.value;
+      }
       else
-        value=if_exprt(it->pointer_guard, it->value, value);
+      {
+        cond.add_case(alias_value.pointer_guard, alias_value.value);
+        INVARIANT(
+          alias_value.value.type() == type,
+          "deref value types should match the pointer being derefd");
+      }
     }
   }
 
-  #if 0
-  std::cout << "R: " << format(value) << "\n\n";
-  #endif
+  // I'd like to put an invariant here that values without a pointer guard, such
+  // as integer_address, cannot co-occur with failed objects, but this isn't the
+  // case. There's no way to write a GOTO condition to discriminate between the
+  // two however, so purely by historical accident, the failed object takes
+  // precedence:
+
+  if(may_fail || value_without_condition.has_value())
+  {
+    // The cases must be disjoint, so add
+    // "!(p == &o1 || p == &o2 || p == &o3 || ...) => failure-value"
+    exprt::operandst other_case_conditions;
+    for(std::size_t i = 0; i < cond.get_n_cases(); ++i)
+      other_case_conditions.push_back(cond.condition(i));
+    cond.add_case(
+      not_exprt(disjunction(other_case_conditions)),
+      may_fail ? failure_value : *value_without_condition);
+  }
 
-  return value;
+#if 0
+  std::cout << "R: " << format(cond) << "\n\n";
+#endif
+
+  if(cond.get_n_cases() == 0)
+    return nil_exprt();
+  else if(cond.get_n_cases() == 1)
+    return cond.value(0);
+  else
+    return std::move(cond);
 }
 
 /// Check if the two types have matching number of ID_pointer levels, with

src/util/irep_ids.def

@@ -723,6 +723,7 @@ IREP_ID_ONE(to_member)
 IREP_ID_ONE(pointer_to_member)
 IREP_ID_ONE(tuple)
 IREP_ID_ONE(function_body)
+IREP_ID_ONE(exclusive)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/std_expr.h

@@ -4394,6 +4394,8 @@ inline popcount_exprt &to_popcount_expr(exprt &expr)
 /// this is a parametric version of an if-expression: it returns
 /// the value of the first case (using the ordering of the operands)
 /// whose condition evaluates to true.
+/// It can be exclusive, in which case the creator asserts that the conditions
+/// are mutually exclusive (i.e. they may be processed in any order).
 class cond_exprt : public multi_ary_exprt
 {
 public:
@@ -4402,9 +4404,11 @@ class cond_exprt : public multi_ary_exprt
   {
   }
 
-  cond_exprt(operandst _operands, typet _type)
+  cond_exprt(operandst _operands, typet _type, bool exclusive = false)
     : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
   {
+    if(exclusive)
+      set(ID_exclusive, true);
   }
 
   /// adds a case to a cond expression
@@ -4417,6 +4421,36 @@ class cond_exprt : public multi_ary_exprt
     operands().push_back(condition);
     operands().push_back(value);
   }
+
+  std::size_t get_n_cases() const
+  {
+    return operands().size() / 2;
+  }
+
+  const exprt &condition(std::size_t case_index) const
+  {
+    return operands().at(case_index * 2);
+  }
+
+  const exprt &value(std::size_t case_index) const
+  {
+    return operands().at((case_index * 2) + 1);
+  }
+
+  exprt &condition(std::size_t case_index)
+  {
+    return operands().at(case_index * 2);
+  }
+
+  exprt &value(std::size_t case_index)
+  {
+    return operands().at((case_index * 2) + 1);
+  }
+
+  bool is_exclusive() const
+  {
+    return get_bool(ID_exclusive);
+  }
 };
 
 template <>