Merge pull request #1200 from smowton/feature/throw-arithmetic-exception

Throw on divide-by-zero

Author: smowton

regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class

@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            int i=0;
+            int j=10/i;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java

@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring

regression/cbmc-java/ArithmeticException1/test.desc

@@ -0,0 +1,12 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            long denom=0;
+            long num=10;
+            long j=num/denom;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class

@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring

regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java

@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            int i=0;
+            int j=10%i;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArithmeticException2/test.desc

@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring

regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class

@@ -0,0 +1,12 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+          long denom=0;
+          long num=10;
+          long result=num%denom;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java

@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring

regression/cbmc-java/ArithmeticException3/test.desc

@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            double i=0;
+            double j=10/i;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class

@@ -0,0 +1,8 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java

@@ -0,0 +1,10 @@
+public class ArithmeticExceptionTest {
+    public static void  main(int denom) {
+        try {
+            int j=10/denom;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArithmeticException4/test.desc

@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring

regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.class

@@ -1052,6 +1052,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
        i_it->statement=="checkcast" ||
        i_it->statement=="newarray" ||
        i_it->statement=="anewarray" ||
+       i_it->statement=="idiv" ||
+       i_it->statement=="ldiv" ||
+       i_it->statement=="irem" ||
+       i_it->statement=="lrem" ||
        i_it->statement==patternt("?astore") ||
        i_it->statement==patternt("?aload") ||
        i_it->statement=="invokestatic" ||

regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java

@@ -57,6 +57,10 @@ class java_bytecode_instrumentt:public messaget
     const exprt &idx,
     const source_locationt &original_loc);
 
+  codet check_arithmetic_exception(
+    const exprt &denominator,
+    const source_locationt &original_loc);
+
   codet check_null_dereference(
     const exprt &expr,
     const source_locationt &original_loc,
@@ -132,6 +136,30 @@ codet java_bytecode_instrumentt::throw_exception(
   return if_code;
 }
 
+
+/// Checks whether there is a division by zero
+/// and throws ArithmeticException if necessary.
+/// Exceptions are thrown when the `throw_runtime_exceptions`
+/// flag is set.
+/// \return Based on the value of the flag `throw_runtime_exceptions`,
+/// it returns code that either throws an ArithmeticException
+/// or is a skip
+codet java_bytecode_instrumentt::check_arithmetic_exception(
+  const exprt &denominator,
+  const source_locationt &original_loc)
+{
+  const constant_exprt &zero=from_integer(0, denominator.type());
+  const binary_relation_exprt equal_zero(denominator, ID_equal, zero);
+
+  if(throw_runtime_exceptions)
+    return throw_exception(
+      equal_zero,
+      original_loc,
+      "java.lang.ArithmeticException");
+
+  return code_skipt();
+}
+
 /// Checks whether the array access array_struct[idx] is out-of-bounds,
 /// and throws ArrayIndexOutofBoundsException/generates an assertion
 /// if necessary; Exceptions are thrown when the `throw_runtime_exceptions`
@@ -463,6 +491,14 @@ codet java_bytecode_instrumentt::instrument_expr(
         expr.op0(),
         expr.source_location());
   }
+  else if((expr.id()==ID_div || expr.id()==ID_mod) &&
+          expr.type().id()==ID_signedbv)
+  {
+    // check division by zero (for integer types only)
+    return check_arithmetic_exception(
+      expr.op1(),
+      expr.source_location());
+  }
   else if(expr.id()==ID_member &&
           expr.get_bool(ID_java_member_access))
   {