From 13dfd5abf748459da2ea7a59cceeaccab903ff59 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Tue, 1 Mar 2016 13:29:44 +0000
Subject: [PATCH] make_binary is not safe to use when types are mixed

Removed use of make_binary in pointer contexts, as pointer arithmetic
yields expressions that include pointer and non-pointer type operands,
with the overall expression type being that of the pointer.
---
 src/analyses/local_bitvector_analysis.cpp |  4 +++-
 src/analyses/local_may_alias.cpp          |  4 ++--
 src/pointer-analysis/dereference.cpp      | 14 ++++++++++----
 src/util/expr_util.cpp                    |  6 ++++++
 4 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 43cb5c1d360..3fc0d10bb09 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -253,7 +253,9 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
   {
     if(rhs.operands().size()>=3)
     {
-      return get_rec(make_binary(rhs), loc_info_src);
+      assert(rhs.op0().type().id()==ID_pointer);
+      return get_rec(rhs.op0(), loc_info_src) |
+             flagst::mk_uses_offset();
     }
     else if(rhs.operands().size()==2)
     {
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 53d089b9544..ffaefe73667 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/std_code.h>
-#include <util/expr_util.h>
 
 #include <ansi-c/c_types.h>
 #include <langapi/language_util.h>
@@ -309,7 +308,8 @@ void local_may_aliast::get_rec(
   {
     if(rhs.operands().size()>=3)
     {
-      get_rec(dest, make_binary(rhs), loc_info_src);
+      assert(rhs.op0().type().id()==ID_pointer);
+      get_rec(dest, rhs.op0(), loc_info_src);
     }
     else if(rhs.operands().size()==2)
     {
diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index b21313f85bf..bd9db73dfb4 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/src/pointer-analysis/dereference.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #endif
 
 #include <util/std_expr.h>
-#include <util/expr_util.h>
 #include <util/byte_operators.h>
 #include <util/pointer_offset_size.h>
 #include <util/base_type.h>
@@ -279,11 +278,18 @@ exprt dereferencet::dereference_plus(
   const exprt &offset,
   const typet &type)
 {
+  exprt pointer=expr.op0();
+  exprt integer=expr.op1();
+
+  // need not be binary
   if(expr.operands().size()>2)
-    return dereference_rec(make_binary(expr), offset, type);
+  {
+    assert(expr.op0().type().id()==ID_pointer);
 
-  // binary
-  exprt pointer=expr.op0(), integer=expr.op1();
+    exprt::operandst plus_ops(
+      ++expr.operands().begin(), expr.operands().end());
+    integer.operands().swap(plus_ops);
+  }
 
   if(ns.follow(integer.type()).id()==ID_pointer)
     std::swap(pointer, integer);
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index f5abbc06c28..d5a28e4f5fa 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -55,13 +55,19 @@ exprt make_binary(const exprt &expr)
   if(operands.size()<=2)
     return expr;
 
+  // types must be identical for make_binary to be safe to use
+  const typet &type=expr.type();
+
   exprt previous=operands.front();
+  assert(previous.type()==type);
 
   for(exprt::operandst::const_iterator
       it=++operands.begin();
       it!=operands.end();
       ++it)
   {
+    assert(it->type()==type);
+
     exprt tmp=expr;
     tmp.operands().clear();
     tmp.operands().resize(2);