Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
cristina-david wants to merge 2 commits into from
Closed

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

cristina-david wants to merge 2 commits into from

Conversation

@cristina-david
Copy link
Collaborator

@cristina-david cristina-david commented May 22, 2017

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

@cristina-david cristina-david force-pushed the feature/throw-arithmetic-exception branch from f6f4064 to f74e4ba Compare May 22, 2017 20:18
kroening
kroening reviewed May 25, 2017
View reviewed changes
src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

@kroening kroening May 25, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure this shouldn't have some class type?

Copy link
Collaborator Author

@cristina-david cristina-david May 25, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
kroening reviewed May 25, 2017
View reviewed changes
src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

@kroening kroening May 25, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@cristina-david cristina-david May 25, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

@cristina-david 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
smowton suggested changes Jun 22, 2017
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suspect object-factory needs replacing with a real constructor

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Contributor

@smowton smowton Jun 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Factor with java_bytecode_convert_classt::generate_class_stub?

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Contributor

@smowton smowton Jun 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Contributor

@smowton smowton Jun 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@cristina-david
Copy link
Collaborator Author

cristina-david commented Jun 26, 2017

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 cristina-david force-pushed the feature/throw-arithmetic-exception branch from 85dd6b5 to dd811f1 Compare July 12, 2017 21:33
@cristina-david cristina-david force-pushed the feature/throw-arithmetic-exception branch from dd811f1 to 6131121 Compare July 12, 2017 21:36
@cristina-david
Copy link
Collaborator Author

cristina-david commented Jul 12, 2017

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

@smowton
Copy link
Contributor

smowton commented Jul 13, 2017

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
Copy link
Contributor

smowton commented Jul 13, 2017

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

mgudemann
mgudemann suggested changes Jul 18, 2017
View reviewed changes
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") ||
Copy link
Contributor

@mgudemann mgudemann Jul 18, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

src/java_bytecode/java_bytecode_instrument.cpp
const source_locationt &original_loc)
{
symbolt exc_symbol;

Copy link
Contributor

@mgudemann mgudemann Jul 18, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

src/java_bytecode/java_bytecode_instrument.cpp
expr.op0(),
expr.source_location());
}
else if(expr.id()==ID_div)
Copy link
Contributor

@mgudemann mgudemann Jul 18, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

peterschrammel
peterschrammel reviewed Jul 25, 2017
View reviewed changes
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@smowton, there are comments to address here.

@smowton
Copy link
Contributor

smowton commented Jul 25, 2017

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

@smowton smowton closed this Aug 3, 2017
@smowton smowton mentioned this pull request Aug 3, 2017
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kroening kroening kroening left review comments

@peterschrammel peterschrammel peterschrammel left review comments

+2 more reviewers

@smowton smowton smowton requested changes

@mgudemann mgudemann mgudemann requested changes

Reviewers whose approvals may not affect merge requirements

Assignees

@smowton smowton

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@cristina-david @smowton @kroening @mgudemann @peterschrammel