Testing

Testing Policy

• All changes must be tested
• Tests must be run before pushing changes to the master branch

What this means

It is the responsibility of the person submitting a change for code review to adequately write tests for their change. Whether they use unit tests or ktest is up to them, however, certain types of code changes are not easily tested using ktest (e.g. error cases).

Sample unit tests

https://github.com/kframework/k/blob/master/java-backend/src/test/java/org/kframework/backend/java/builtins/BuiltinIOOperationsTest.java https://github.com/kframework/k/blob/master/kernel/src/test/java/org/kframework/krun/ioserver/filesystem/portable/PortableFileSystemTest.java

Sample end-to-end tests

https://github.com/kframework/k/tree/master/k-distribution/tests/regression/java-rewrite-engine/strings https://github.com/kframework/k/tree/master/k-distribution/tests/regression/java-rewrite-engine/set

Merging changes into master

It is your responsibility as a developer to make sure the test suite is run and all tests pass prior to a commit. This project is set up to automatically run mvn verify with Jenkins on pull requests, however it is ultimately your responsibility. If you merge a change that breaks master without code reviewing it first, you will be asked to provide a very clear explanation for why it happened, because code review is a simple expectation on all commits. If you do it a second time, your commit access will be revoked.

Jenkins use case

Suppose you are creating a pull request and you want to test your changes. This should happen automatically if you are a member of the kframework organization and you submit a pull request. Our Jenkins instance at http://office.runtimeverification.com:8080/rv-jenkins/job/k-framework-pull-requests/ will then update the status of the pull request to tell you whether the tests pass or fail. It will also automatically retest if you push new commits into the pull request. However, things do not always work completely as planned. Sometimes the Jenkins script has a bug, sometimes the plugin we use is buggy. Therefore, Jenkins exposes the following manual commands.

Jenkins Comment Interface

• Jenkins: test this please. Technically speaking you only need the string "Jenkins" followed by the string "test this please", so you could equally say Jenkins, test this please, Jenkins retest this please, etc. This command will kick off a build immediately. See section on Jenkins: ok to test for caveats.
• Jenkins: ok to test. Since we are essentially downloading someone else's code and running whatever it happens to tell us to run, it is important for security reasons that only approved users are able to run tests. As a result of this, Jenkins maintains a whitelist of all users who are allowed to run tests. If the user is not on the whitelist, the build will not automatically happen, and invoking Jenkins: test this please will do nothing. To fix this, an admin (in this case Dwight) has to run a command. The Jenkins: ok to test command will tell Jenkins that this pull request can be automatically retested. If I choose, I can also run Jenkins: add to whitelist to approve all changes by that author, or Jenkins: test this please to test only one commit of the pull request and require re-approval if the user pushes again.

WARNING: It came to my attention today that the Jenkins Github Pull Request plugin is not quite perfect in kicking off builds. It might not successfully kick off a build in all cases if several other builds are already queued up. In this case, wait until the queue has quieted down and then tell Jenkins to test it again.

Checkstyle

You can detect all checkstyle errors that the Jenkins build will generate by running mvn verify -DskipTests -DskipKTest.

Solving failed tests

Sometimes tests will fail when you merge into master. Assuming you have taken appropriate steps to test your change (i.e. run all tests before committing, and merging changes with the upstream if you expect conflicts), and assuming it has been code reviewed and I signed off on it having passed tests, you will not be blamed for this. However, regardless of whether blame falls on you for causing tests to fail in master, there are certain expectations you must perform if that occurs.

1. Determine whether the tests failed due to some kind of transient failure or because of your change. If you can demonstrate clearly that the failure has nothing to do with your change, rerun the test suite. If it passes, you are done. Otherwise, or if the tests failed due to your change, proceed to step 2.
2. Revert your change. This does not require a code review. If the first commit you want to revert has hash , and the last commit you want to revert has hash , run git revert <commit1>^..<commit2>. Note that this will not behave as you expect it to if you try to select a range of commits that are not ancestors of each other, for example if you try to select two commits that were parts of different branches without also selecting the revisions that merge these branches.
3. Push your revert upstream, once you have verified that it looks as you expect it to.
4. Cherry-pick your change back into your local repository with git cherry-pick <commit1>^..<commit2>.
5. Fix your change so that it passes all the tests (making sure to merge with upstream to ensure that you have considered any tests that might fail due to conflicts).
6. Submit your modified change as a pull request.

Failure to promptly follow steps 1-3 will put you on the same type of probation you would be put under for failing to code review your changes.