Throw ArithmeticException whenever a division-by-zero is encountered #950

cristina-david · 2017-05-22T19:57:29Z

This is best merged after PR #912 which introduces the initial instrumentation for throwing runtime exceptions.

kroening · 2017-05-25T12:52:16Z

src/java_bytecode/java_bytecode_convert_method.cpp

+    exc_symbol.name="ArithmeticException";
+    exc_symbol.mode=ID_java;
+    exc_symbol.type=typet(ID_pointer, empty_typet());
+    symbol_table.add(exc_symbol);


Sure this shouldn't have some class type?

I'm now using a class stub. Soon, we should have a proper model so that we can capture the class hierarchy (for now, this wouldn't be caught by a handler for, say, RuntimeException).

kroening · 2017-05-25T12:53:52Z

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1933,6 +1979,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
    {
      assert(op.size()==2 && results.size()==1);
      results[0]=div_exprt(op[0], op[1]);
+      c=throw_arithmetic_exception(op[1], i_it->source_location);
    }


This doesn't seem to be the right place for this -- this should happen during conversion from program into goto-program.

I would think that this is a better place than the conversion to goto-program as the exception being thrown is language dependent. I assume we don't want to throw an exception for all input languages?

smowton

Suspect object-factory needs replacing with a real constructor

smowton · 2017-06-22T12:48:42Z

src/java_bytecode/java_bytecode_convert_method.cpp

+{
+  symbolt exc_symbol;
+
+  if(!symbol_table.has_symbol("java.lang.ArithmeticException"))


Factor with java_bytecode_convert_classt::generate_class_stub?

smowton · 2017-06-22T12:49:25Z

src/java_bytecode/java_bytecode_convert_method.cpp

+
+  code_blockt init_code;
+  // create the exception object
+  auto exc=object_factory(


Should we really nondet init it rather than calling a particular constructor?

smowton · 2017-06-22T12:50:22Z

src/java_bytecode/java_bytecode_convert_method.cpp

+
+\*******************************************************************/
+
+codet java_bytecode_convert_methodt::throw_arithmetic_exception(


Consider adding an annotation here and then moving this to your existing instrumentation pass

cristina-david · 2017-06-26T09:17:29Z

Once #1019 is merged, this PR will need some major changes as the instrumentation added here also needs to be refactored out of bytecode convert.

cristina-david · 2017-07-12T21:42:04Z

@smowton and @kroening This is now rebased and done outside java_bytecode_convert.

smowton · 2017-07-13T07:50:29Z

Tested this with test case:

public class test {
    public static void f(int a, float b, double c) {
        int x = 0;
        try {
            div(1, a);
        }
        catch(ArithmeticException e) {
            x++;
        }
        try {
            div(1, b);
        }
        catch(ArithmeticException e) {
            x++;
        }
        try {
            div(1, c);
        }
        catch(ArithmeticException e) {
            x++;
        }       
    }

    public static int div(int num, int denom) {
        return num / denom;
    }

    public static float div(float num, float denom) {
        return num / denom;
    }

    public static double div(double num, double denom) {
        return num / denom;
    }    
}

I found that the way of initialising the exception object meant it could get thrown without being initialised. Made a couple of improvements here: https://github.com/smowton/cbmc/commits/smowton/feature/exceptions_improved

smowton · 2017-07-13T08:16:27Z

Corresponding test-gen PR: https://github.com/diffblue/test-gen/pull/750

mgudemann · 2017-07-18T14:10:43Z

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") ||


only idiv and ldiv throw ArithmeticException, fdiv and ddiv do not. In addition irem and lrem throw, too.

mgudemann · 2017-07-18T14:12:46Z

src/java_bytecode/java_bytecode_instrument.cpp

+  const source_locationt &original_loc)
+{
+  symbolt exc_symbol;
+


as only integral div-by-zero throws, maybe add invariant for java_int_type or java_long_type

mgudemann · 2017-07-18T14:15:29Z

src/java_bytecode/java_bytecode_instrument.cpp

@@ -463,6 +493,13 @@ codet java_bytecode_instrumentt::instrument_expr(
        expr.op0(),
        expr.source_location());
  }
+  else if(expr.id()==ID_div)


needs ID_mod, too, ID_rem is for float/double, if I understood correctly

peterschrammel

@smowton, there are comments to address here.

smowton · 2017-07-25T14:48:25Z

I know, I'm currently working on resolving the remaining exception issues, which might subsume this in any event

cristina-david force-pushed the feature/throw-arithmetic-exception branch from f6f4064 to f74e4ba Compare May 22, 2017 20:18

kroening reviewed May 25, 2017

View reviewed changes

cristina-david force-pushed the feature/throw-arithmetic-exception branch 2 times, most recently from 3ef77a1 to 85dd6b5 Compare May 25, 2017 23:05

smowton suggested changes Jun 22, 2017

View reviewed changes

cristina-david force-pushed the feature/throw-arithmetic-exception branch from 85dd6b5 to dd811f1 Compare July 12, 2017 21:33

cristina-david added 2 commits July 12, 2017 22:35

Throw ArithmeticException whenever a division-by-zero is encountered

02ffa6e

Regression test for ArithmeticException

6131121

cristina-david force-pushed the feature/throw-arithmetic-exception branch from dd811f1 to 6131121 Compare July 12, 2017 21:36

peterschrammel requested review from mgudemann and peterschrammel July 13, 2017 19:20

mgudemann suggested changes Jul 18, 2017

View reviewed changes

peterschrammel assigned smowton Jul 20, 2017

peterschrammel reviewed Jul 25, 2017

View reviewed changes

smowton closed this Aug 3, 2017

smowton mentioned this pull request Aug 3, 2017

Throw on divide-by-zero #1200

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Throw ArithmeticException whenever a division-by-zero is encountered #950

Throw ArithmeticException whenever a division-by-zero is encountered #950

cristina-david commented May 22, 2017

kroening May 25, 2017

cristina-david May 25, 2017

kroening May 25, 2017

cristina-david May 25, 2017 •

edited

Loading

smowton left a comment

smowton Jun 22, 2017

smowton Jun 22, 2017

smowton Jun 22, 2017

cristina-david commented Jun 26, 2017

cristina-david commented Jul 12, 2017

smowton commented Jul 13, 2017

smowton commented Jul 13, 2017

mgudemann Jul 18, 2017

mgudemann Jul 18, 2017

mgudemann Jul 18, 2017

peterschrammel left a comment

smowton commented Jul 25, 2017


		\*******************************************************************/

		codet java_bytecode_convert_methodt::throw_arithmetic_exception(

Throw ArithmeticException whenever a division-by-zero is encountered #950

Throw ArithmeticException whenever a division-by-zero is encountered #950

Conversation

cristina-david commented May 22, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cristina-david May 25, 2017 • edited Loading

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cristina-david commented Jun 26, 2017

cristina-david commented Jul 12, 2017

smowton commented Jul 13, 2017

smowton commented Jul 13, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

smowton commented Jul 25, 2017

cristina-david May 25, 2017 •

edited

Loading