diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class new file mode 100644 index 00000000000..3ad4e6ebe86 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class differ 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 diff --git a/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class new file mode 100644 index 00000000000..3ac62d1ede5 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..0c83bf9a409 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java @@ -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; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException2/test.desc b/regression/cbmc-java/ArithmeticException2/test.desc new file mode 100644 index 00000000000..00820d86c6e --- /dev/null +++ b/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 9 function.*: FAILURE$ +^VERIFICATION FAILED +-- +^warning: ignoring diff --git a/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class new file mode 100644 index 00000000000..21c451e02f3 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..dfe7b031288 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException3/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/ArithmeticException3/test.desc b/regression/cbmc-java/ArithmeticException3/test.desc new file mode 100644 index 00000000000..e8f7c941fd4 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException3/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 diff --git a/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class new file mode 100644 index 00000000000..a4723d1d652 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..1e811e417f8 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java @@ -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; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException4/test.desc b/regression/cbmc-java/ArithmeticException4/test.desc new file mode 100644 index 00000000000..00820d86c6e --- /dev/null +++ b/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 9 function.*: FAILURE$ +^VERIFICATION FAILED +-- +^warning: ignoring diff --git a/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.class new file mode 100644 index 00000000000..813391d04af Binary files /dev/null and b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..d32299a427f --- /dev/null +++ b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java @@ -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; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException5/test.desc b/regression/cbmc-java/ArithmeticException5/test.desc new file mode 100644 index 00000000000..d57ec32a9a9 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException5/test.desc @@ -0,0 +1,8 @@ +CORE +ArithmeticExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class new file mode 100644 index 00000000000..fdcb29ad252 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..281f868b3e6 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException6/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; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException6/test.desc b/regression/cbmc-java/ArithmeticException6/test.desc new file mode 100644 index 00000000000..8cab5f69869 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException6/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 diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 3cb2cc2861d..91ba790ab8d 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1051,6 +1051,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" || diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 79b89eebe60..8e56439346b 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, @@ -133,6 +137,30 @@ 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) +{ + 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` @@ -464,6 +492,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)) {