From 02ffa6e9a0ddd8582616fe93e73d3f2a2689ab92 Mon Sep 17 00:00:00 2001
From: Cristina <cristina.david@gmail.com>
Date: Mon, 22 May 2017 19:48:39 +0100
Subject: [PATCH 1/2] Throw ArithmeticException whenever a division-by-zero is
 encountered

---
 .../java_bytecode_convert_method.cpp          |  1 +
 .../java_bytecode_instrument.cpp              | 37 +++++++++++++++++++
 2 files changed, 38 insertions(+)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 4ae7c72ed69..967b3cc239f 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1051,6 +1051,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
        i_it->statement=="checkcast" ||
        i_it->statement=="newarray" ||
        i_it->statement=="anewarray" ||
+       i_it->statement==patternt("?div") ||
        i_it->statement==patternt("?astore") ||
        i_it->statement==patternt("?aload") ||
        i_it->statement=="invokestatic" ||
diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp
index b41e1e73baf..35ea54e9cbd 100644
--- a/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/src/java_bytecode/java_bytecode_instrument.cpp
@@ -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,32 @@ codet java_bytecode_instrumentt::throw_exception(
   return init_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)
+{
+  symbolt exc_symbol;
+
+  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 +493,13 @@ codet java_bytecode_instrumentt::instrument_expr(
         expr.op0(),
         expr.source_location());
   }
+  else if(expr.id()==ID_div)
+  {
+    // check division by zero
+    return check_arithmetic_exception(
+      expr.op1(),
+      expr.source_location());
+  }
   else if(expr.id()==ID_member &&
           expr.get_bool(ID_java_member_access))
   {

From 61311213493cc7aba772d0e6423f5c5cfaf3d02f Mon Sep 17 00:00:00 2001
From: Cristina <cristina.david@gmail.com>
Date: Mon, 22 May 2017 20:51:54 +0100
Subject: [PATCH 2/2] Regression test for ArithmeticException

---
 .../ArithmeticExceptionTest.class                 | Bin 0 -> 818 bytes
 .../ArithmeticExceptionTest.java                  |  11 +++++++++++
 .../cbmc-java/ArithmeticException1/test.desc      |   9 +++++++++
 3 files changed, 20 insertions(+)
 create mode 100644 regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class
 create mode 100644 regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java
 create mode 100644 regression/cbmc-java/ArithmeticException1/test.desc

diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class
new file mode 100644
index 0000000000000000000000000000000000000000..3ad4e6ebe86e52587843990ffa9af01256fb2197
GIT binary patch
literal 818
zcmZuvPfrs;6#u>Mw%cwCmR6w@5Kz#<!CtsgjRY~#R6UfCfT!tpQU<nLGP^Zg{Th4$
z&S)ZuCVKZn8Q<H0C9#K{nfLbh=e;-c`_K2E0JgB{BadYdD+T1R>fw<OSK`M$*0Ap3
z38A{C;#k|n45Rp!iB&h$JpvsOaxD{?<ORWLY#b2W-C<7??zK&%-;V}eZTAICsI-TH
z3J;Vu65k}<<k-Z7`Sy-A$?-rZCfGX<^qKhV>p0nF!GSUnVYczHeWE_8W~icmvy)g8
z^|!^441aIfUY`eq<vXAWnxdy{pDn8s<OoxpL<Ohs)LB{|PlS+f1>sGHerGtcfqreI
zpT!CCQt~sYvV<Z^gr#xC6VN3T;1g<hK({mAvvz0+a}!wN;o)fs4Qvp~WAcaYi4GDT
z{W!H7@~!dgdO9{%_jYdOxyxk4KlsXyu*#R7=XXHmniRw*2PF0LI>k|wcj7&}c@4Va
zLk82l=F%kF@mZh@Kp8W<7f?Z!GeZ8%XovT@(<=K5;qyy=2VdY^p!fss;We_qu2QbY
z#)1^(I%|VpV1^aFv?Pzq$zz@|;<my#`F9@=m|JAdEap;`I%<p(1u!%7*2BUy6BqyW
kvX#PsnM&>(ybE~lC0yq#od5e0jVv;ym(u+b2N^v43vqX+?f?J)

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java
new file mode 100644
index 00000000000..7988e85700e
--- /dev/null
+++ b/regression/cbmc-java/ArithmeticException1/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;
+        }
+    }
+}
diff --git a/regression/cbmc-java/ArithmeticException1/test.desc b/regression/cbmc-java/ArithmeticException1/test.desc
new file mode 100644
index 00000000000..e8f7c941fd4
--- /dev/null
+++ b/regression/cbmc-java/ArithmeticException1/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