pointer-overflow-check: support >2 operands

Author: tautschnig

src/analyses/goto_check.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 
+#include <util/c_types.h>
+#include <util/invariant.h>
 #include <util/simplify_expr.h>
 #include <util/array_name.h>
 #include <util/ieee_float.h>
@@ -902,23 +904,57 @@ void goto_checkt::pointer_overflow_check(
   if(!enable_pointer_overflow_check)
     return;
 
-  if(expr.id()==ID_plus ||
-     expr.id()==ID_minus)
+  if(expr.id()!=ID_plus &&
+     expr.id()!=ID_minus)
+    return;
+
+  if(expr.operands().size()>2)
   {
-    if(expr.operands().size()==2)
+    // The overflow checks are binary!
+    // We break these up.
+
+    for(unsigned i=1; i<expr.operands().size(); i++)
     {
-      exprt overflow("overflow-"+expr.id_string(), bool_typet());
-      overflow.operands()=expr.operands();
+      exprt tmp;
 
-      add_guarded_claim(
-        not_exprt(overflow),
-        "pointer arithmetic overflow on "+expr.id_string(),
-        "overflow",
-        expr.find_source_location(),
-        expr,
-        guard);
+      if(i==1)
+        tmp=expr.op0();
+      else
+      {
+        tmp=expr;
+        tmp.operands().resize(i);
+      }
+
+      exprt tmp2=expr;
+      tmp2.operands().resize(2);
+      tmp2.op0()=tmp;
+      tmp2.op1()=expr.operands()[i];
+
+      pointer_overflow_check(tmp2, guard);
     }
   }
+  else
+  {
+    DATA_INVARIANT(
+      expr.operands().size() == 2,
+      "overflow-" + expr.id_string() + " takes 2 operands");
+
+    exprt overflow("overflow-"+expr.id_string(), bool_typet());
+    overflow.operands()=expr.operands();
+
+    // this is overflow over integers
+    overflow.op0().make_typecast(size_type());
+    if(overflow.op1().type()!=size_type())
+      overflow.op1().make_typecast(size_type());
+
+    add_guarded_claim(
+      not_exprt(overflow),
+      "pointer arithmetic overflow on "+expr.id_string(),
+      "overflow",
+      expr.find_source_location(),
+      expr,
+      guard);
+  }
 }
 
 void goto_checkt::pointer_validity_check(