Add cases handling cond_exprt wherever symex or value-set currently handles if_exprt

Author: smowton

src/goto-symex/build_goto_trace.cpp

@@ -89,6 +89,37 @@ static exprt build_full_lhs_rec(
     else
       return std::move(tmp2);
   }
+  else if(id == ID_cond)
+  {
+    const auto &original_cond_expr = to_cond_expr(src_original);
+    const auto &ssa_cond_expr = to_cond_expr(src_ssa);
+    cond_exprt result(
+      {}, src_original.type(), original_cond_expr.is_exclusive());
+    for(std::size_t i = 0; i < original_cond_expr.get_n_cases(); ++i)
+    {
+      exprt condition =
+        decision_procedure.get(to_cond_expr(src_ssa).condition(i));
+      if(condition.is_false())
+        continue;
+
+      exprt value = build_full_lhs_rec(
+        decision_procedure,
+        ns,
+        original_cond_expr.value(i),
+        ssa_cond_expr.value(i));
+
+      if(
+        condition.is_true() &&
+        (result.get_n_cases() == 0 || result.is_exclusive()))
+      {
+        return value;
+      }
+
+      result.add_case(condition, value);
+    }
+
+    return std::move(result);
+  }
   else if(id==ID_typecast)
   {
     typecast_exprt tmp=to_typecast_expr(src_original);

src/goto-symex/goto_symex_state.cpp

@@ -579,6 +579,16 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
 
       if_expr.type()=if_expr.true_case().type();
     }
+    else if(expr.id() == ID_cond)
+    {
+      cond_exprt &cond_expr = to_cond_expr(expr);
+      for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      {
+        cond_expr.condition(i) =
+          rename<level>(std::move(cond_expr.condition(i)), ns).get();
+        rename_address<level>(cond_expr.value(i), ns);
+      }
+    }
     else if(expr.id()==ID_member)
     {
       member_exprt &member_expr=to_member_expr(expr);

src/goto-symex/symex_dereference.cpp

@@ -123,6 +123,18 @@ exprt goto_symext::address_arithmetic(
 
     result=if_expr;
   }
+  else if(expr.id() == ID_cond)
+  {
+    cond_exprt cond_expr = to_cond_expr(expr);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+    {
+      dereference_rec(cond_expr.condition(i), state, false);
+      cond_expr.value(i) =
+        address_arithmetic(cond_expr.value(i), state, keep_array);
+    }
+
+    result = std::move(cond_expr);
+  }
   else if(expr.id()==ID_symbol ||
           expr.id()==ID_string_constant ||
           expr.id()==ID_label ||

src/goto-symex/symex_other.cpp

@@ -55,6 +55,21 @@ void goto_symext::havoc_rec(
     guard_f.add(not_exprt(if_expr.cond()));
     havoc_rec(state, guard_f, if_expr.false_case());
   }
+  else if(dest.id() == ID_cond)
+  {
+    const auto &cond_expr = to_cond_expr(dest);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+    {
+      guardt guard = state.guard;
+      if(!cond_expr.is_exclusive())
+      {
+        for(std::size_t j = 0; j < i; ++j)
+          guard.add(not_exprt(cond_expr.condition(j)));
+      }
+      guard.add(cond_expr.condition(i));
+      havoc_rec(state, guard, cond_expr.value(i));
+    }
+  }
   else if(dest.id()==ID_typecast)
   {
     havoc_rec(state, guard, to_typecast_expr(dest).op());

src/pointer-analysis/value_set.cpp

@@ -1175,6 +1175,12 @@ void value_sett::get_reference_set_rec(
     get_reference_set_rec(expr.op2(), dest, ns);
     return;
   }
+  else if(expr.id() == ID_cond)
+  {
+    const auto &cond_expr = to_cond_expr(expr);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      get_reference_set_rec(cond_expr.value(i), dest, ns);
+  }
 
   insert(dest, exprt(ID_unknown, expr.type()));
 }

src/pointer-analysis/value_set_dereference.cpp

@@ -36,14 +36,21 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
     throw "dereference expected pointer type, but got "+
           pointer.type().pretty();
 
-  // we may get ifs due to recursive calls
+  // we may get ifs or conds due to recursive calls
   if(pointer.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(pointer);
     exprt true_case = dereference(if_expr.true_case());
     exprt false_case = dereference(if_expr.false_case());
     return if_exprt(if_expr.cond(), true_case, false_case);
   }
+  else if(pointer.id() == ID_cond)
+  {
+    cond_exprt result = to_cond_expr(pointer);
+    for(std::size_t i = 0; i < result.get_n_cases(); ++i)
+      result.value(i) = dereference(result.value(i));
+    return std::move(result);
+  }
 
   // type of the object
   const typet &type=pointer.type().subtype();