Throw ArithmeticException whenever a division-by-zero is encountered by cristina-david · Pull Request #950 · diffblue/cbmc

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

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

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

Factor with java_bytecode_convert_classt::generate_class_stub?

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

src/java_bytecode/java_bytecode_convert_method.cpp

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

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

       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

        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

Conversation

cristina-david commented May 22, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cristina-david May 25, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cristina-david commented Jun 26, 2017

Uh oh!

cristina-david commented Jul 12, 2017

Uh oh!

smowton commented Jul 13, 2017

Uh oh!

smowton commented Jul 13, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Jul 25, 2017

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

cristina-david May 25, 2017 •

edited

Loading