Exception exit support #91

markro49 · 2017-07-17T14:38:02Z

I have completed an upstream merge of Philipp Hirch's changes to add exception exit ppts to chicory output files. I think there might be a little more common code in chicory/Instrument and dcomp/DCIstrument that can be merged, but that can wait until latter.

markro49 · 2017-07-17T14:43:29Z

Should have mentioned that this subsumes #56. That pull request will be deleted/closed as part of this work.

…nto exception-exit-support

Still need upstream merge and doc changes.

markro49 · 2017-07-28T17:24:57Z

still need to update doc files

fix another blank at end of line in txt-jaif output

markro49 · 2017-08-02T02:31:03Z

As we discussed, I have completed this work and it is ready for review.

mernst · 2017-08-03T18:29:11Z

A few high-level questions:

foo():::ENTER is the point at the entry to procedure foo(). The invariants at that point are the preconditions for the foo() method, properties that are always true when the procedure is invoked.

Are these normal preconditions or overall preconditions?

Is there a way to determine exceptional preconditions for a given :::EXCEPTION program point?
A user may want to know, what are the preconditions (the properties upon entry to the routine) that lead to this particular exception.

The Daikon manual (section 5.2) doesn't mention EXCEPTIONUNCAUGHT program points, but it should.

mernst · 2018-07-31T00:25:18Z

doc/daikon.texinfo

-points.  Typically, @code{orig()} variables do not appear in the trace,
-but are automatically created by Daikon when it matches up
-@code{:::ENTER} and @code{:::EXIT@var{nn}} program points.
+of @code{x}).  These variables appear only at @code{:::EXIT} and


Please don't refill paragraphs (that is, don't remove line breaks). It makes the diffs bigger and harder to read.

mernst

Here are some initial comments. Could you address these, and then I will do another round of code review?

One comment is that there seem to be some changes that are not directly related to handling exceptional exits. It would be nice to separate those into a second pull request, so that I can review the two pull requests separately.
Thanks!

mernst · 2018-08-01T15:51:39Z

java/daikon/chicory/DaikonWriter.java

+   * @return the exception name suffix for Daikon
+   */
+  private static String exceptionSuffix(int lineNum) {
+    return lineNum < 0


Could this be lineNum == -1? That seems clearer to me.

mernst · 2018-08-01T16:08:40Z

java/daikon/PptTopLevel.java

@@ -4405,6 +4405,19 @@ public boolean is_exit() {
    }
  }

+  // UNDONE: this doesn't look right


Does "UNDONE" mean "TODO"? I think the "UNDONE" comments should be clarified or removed, throughout.

mernst · 2018-08-01T16:11:38Z

java/daikon/chicory/Instrument.java

@@ -388,7 +407,7 @@ private InstructionList call_initNotify(
   * Instrument all the methods in a class. For each method, add instrumentation code at the entry
   * and at each return from the method. In addition, changes each return statement to first place
   * the value being returned into a local and then return. This allows us to work around the JDI
-   * deficiency of not being able to query return values.
+   * deficiency of not being able to query return values. (We now instrument throws as well.)


Please don't write comments like this. Years from now, people won't know when this comment was written or why it is relevant. Please describe the code, not the code's history.

mernst · 2018-08-01T16:17:12Z

java/daikon/chicory/Instrument.java

-   * (return__$trace2_val) and then do the return. Also, calls Runtime.exit() immediately before the
-   * return.
+   * If this is a return instruction, generate new il to assign the result to a local variable
+   * (return__$trace2_val) and then call Runtime.exit(). This il wil be inserted immediately before


This is confusing. It's not java.lang.Runtime.exit(), nor daikon.Runtime. I think it's what is in runtime_classname. Clarifying that would be helpful.

mernst · 2018-08-01T16:21:38Z

java/daikon/Chicory.java

@@ -130,6 +130,9 @@
  @Option("Number of calls after which sampling will begin")
  public static int sample_start = 0;

+  @Option("Enable remote debug")


Please add a Javadoc comment, explaining what this does or how to use it.

This was added and used by Philipp Hirch. I do not know how to use it. Should I comment out or just delete?

This is not a new change -- it already existed, and he just moved it to be a command-line option.

I see that now and presumably his changes made it work (better?). I get the jist of what this does and I think all the debug arguments are just magic. I will write up something.

mernst · 2018-08-01T16:27:44Z

java/daikon/VarInfo.java

+        if (!name().contains("exception")) {
+          return ("\\result");
+        } else {
+          return ("Exception");


Don't use unnecessary parentheses around return statement values.

mernst · 2018-08-01T16:28:53Z

tests/chicory-tests/option-tests/README

@@ -1,3 +1,5 @@
 This directory tests Chicory command-line options.
 Each test runs Chicory and Daikon on the StackAr program, but each test
 uses a different set of command-line options.
+
+The test suite has been augmented to cover the addition of exception exit ppts.


Delete this. It isn't helpful in the code -- it's just a code review comment, and as such it doesn't belong in the code.

mernst · 2018-08-01T16:31:49Z

tests/daikon-tests/BinaryTree/BinaryTree.txt-merge-esc.goal

  /*@ requires \typeof(x) == \type(DataStructures.MyInteger); */
  /*@ modifies this.root; */
  /*@ ensures this.root != null; */
+  /*@ ensures \old(x) != null; */


This is an odd change. I find the original line clearer and more intuitive than the new one.
Do you understand the cause of this change in output? What would it take to restore the behavior?

Sorry, I do not understand the cause of this change.

OK, we need to understand this before we merge the change.

mernst · 2018-08-01T16:33:59Z

tests/daikon-tests/purity/purity.txt-jml.goal

@@ -3,10 +3,10 @@ misc.Purity:::OBJECT
    Variables: this this.value this.shift this.heavy this.list1 this.list1[] this.list1[].getClass().getName() this.list2 this.list2[] this.list2[].getClass().getName() this.list2.getClass().getName() this.getValue() this.getShift() this.isHeavy() this.getNum() this.getNum().getClass().getName() this.getJWrap() this.scale(this.value) this.scale(this.shift) this.scale(this.getValue()) this.scale(this.getShift()) this.sum(this.getNum()) this.sum(this.getJWrap()) this.retrieve(this.list1) this.retrieve(this.list2) size(this.list1[]) size(this.list1[])-1 size(this.list2[]) size(this.list2[])-1 this.list1[this.value] this.list1[this.value-1] this.list1[this.value..] this.list1[this.value+1..] this.list1[0..this.value] this.list1[0..this.value-1] this.list2[this.value] this.list2[this.value-1] this.list2[this.value..] this.list2[this.value+1..] this.list2[0..this.value] this.list2[0..this.value-1] this.list1[this.shift] this.list1[this.shift-1] this.list1[this.shift..] this.list1[this.shift+1..] this.list1[0..this.shift] this.list1[0..this.shift-1] this.list2[this.shift] this.list2[this.shift-1] this.list2[this.shift..] this.list2[this.shift+1..] this.list2[0..this.shift] this.list2[0..this.shift-1] this.list1[this.getValue()] this.list1[this.getValue()-1] this.list1[this.getValue()..] this.list1[this.getValue()+1..] this.list1[0..this.getValue()] this.list1[0..this.getValue()-1] this.list1[this.getShift()] this.list1[this.getShift()-1] this.list1[this.getShift()..] this.list1[this.getShift()+1..] this.list1[0..this.getShift()] this.list1[0..this.getShift()-1] this.list1[this.scale(this.value)] this.list1[this.scale(this.value)-1] this.list1[this.scale(this.value)..] this.list1[this.scale(this.value)+1..] this.list1[0..this.scale(this.value)] this.list1[0..this.scale(this.value)-1] this.list1[this.scale(this.shift)] this.list1[this.scale(this.shift)-1] this.list1[this.scale(this.shift)..] this.list1[this.scale(this.shift)+1..] this.list1[0..this.scale(this.shift)] this.list1[0..this.scale(this.shift)-1] this.list1[this.scale(this.getValue())] this.list1[this.scale(this.getValue())-1] this.list1[this.scale(this.getValue())..] this.list1[this.scale(this.getValue())+1..] this.list1[0..this.scale(this.getValue())] this.list1[0..this.scale(this.getValue())-1] this.list1[this.scale(this.getShift())] this.list1[this.scale(this.getShift())-1] this.list1[this.scale(this.getShift())..] this.list1[this.scale(this.getShift())+1..] this.list1[0..this.scale(this.getShift())] this.list1[0..this.scale(this.getShift())-1] this.list1[this.sum(this.getNum())] this.list1[this.sum(this.getNum())-1] this.list1[this.sum(this.getNum())..] this.list1[this.sum(this.getNum())+1..] this.list1[0..this.sum(this.getNum())] this.list1[0..this.sum(this.getNum())-1] this.list1[this.sum(this.getJWrap())] this.list1[this.sum(this.getJWrap())-1] this.list1[this.sum(this.getJWrap())..] this.list1[this.sum(this.getJWrap())+1..] this.list1[0..this.sum(this.getJWrap())] this.list1[0..this.sum(this.getJWrap())-1] this.list1[this.retrieve(this.list1)] this.list1[this.retrieve(this.list1)-1] this.list1[this.retrieve(this.list1)..] this.list1[this.retrieve(this.list1)+1..] this.list1[0..this.retrieve(this.list1)] this.list1[0..this.retrieve(this.list1)-1] this.list1[this.retrieve(this.list2)] this.list1[this.retrieve(this.list2)-1] this.list1[this.retrieve(this.list2)..] this.list1[this.retrieve(this.list2)+1..] this.list1[0..this.retrieve(this.list2)] this.list1[0..this.retrieve(this.list2)-1] this.list2[this.getValue()] this.list2[this.getValue()-1] this.list2[this.getValue()..] this.list2[this.getValue()+1..] this.list2[0..this.getValue()] this.list2[0..this.getValue()-1] this.list2[this.getShift()] this.list2[this.getShift()-1] this.list2[this.getShift()..] this.list2[this.getShift()+1..] this.list2[0..this.getShift()] this.list2[0..this.getShift()-1] this.list2[this.scale(this.value)] this.list2[this.scale(this.value)-1] this.list2[this.scale(this.value)..] this.list2[this.scale(this.value)+1..] this.list2[0..this.scale(this.value)] this.list2[0..this.scale(this.value)-1] this.list2[this.scale(this.shift)] this.list2[this.scale(this.shift)-1] this.list2[this.scale(this.shift)..] this.list2[this.scale(this.shift)+1..] this.list2[0..this.scale(this.shift)] this.list2[0..this.scale(this.shift)-1] this.list2[this.scale(this.getValue())] this.list2[this.scale(this.getValue())-1] this.list2[this.scale(this.getValue())..] this.list2[this.scale(this.getValue())+1..] this.list2[0..this.scale(this.getValue())] this.list2[0..this.scale(this.getValue())-1] this.list2[this.scale(this.getShift())] this.list2[this.scale(this.getShift())-1] this.list2[this.scale(this.getShift())..] this.list2[this.scale(this.getShift())+1..] this.list2[0..this.scale(this.getShift())] this.list2[0..this.scale(this.getShift())-1] this.list2[this.sum(this.getNum())] this.list2[this.sum(this.getNum())-1] this.list2[this.sum(this.getNum())..] this.list2[this.sum(this.getNum())+1..] this.list2[0..this.sum(this.getNum())] this.list2[0..this.sum(this.getNum())-1] this.list2[this.sum(this.getJWrap())] this.list2[this.sum(this.getJWrap())-1] this.list2[this.sum(this.getJWrap())..] this.list2[this.sum(this.getJWrap())+1..] this.list2[0..this.sum(this.getJWrap())] this.list2[0..this.sum(this.getJWrap())-1] this.list2[this.retrieve(this.list1)] this.list2[this.retrieve(this.list1)-1] this.list2[this.retrieve(this.list1)..] this.list2[this.retrieve(this.list1)+1..] this.list2[0..this.retrieve(this.list1)] this.list2[0..this.retrieve(this.list1)-1] this.list2[this.retrieve(this.list2)] this.list2[this.retrieve(this.list2)-1] this.list2[this.retrieve(this.list2)..] this.list2[this.retrieve(this.list2)+1..] this.list2[0..this.retrieve(this.list2)] this.list2[0..this.retrieve(this.list2)-1]
 this.value == this.getValue()
 this.shift == this.getShift()
-this.shift == this.retrieve()
-this.shift == this.retrieve()
+this.shift == this.retrieve(this.list1)


What caused this change? If it's correct, was this a bug fix unrelated to the exceptional exit support, but in the same pull request? Or was it caused by a previously-committed change, but the goal files were not regenerated since then?

Looking at the history of this goal file, it appears this is a new change. I do not know what caused it.

mernst · 2018-08-01T16:37:22Z

tests/daikon-tests/Makefile

@@ -41,12 +41,12 @@ everything-%: quick-% nonquick-%
 	@echo ${HR}
 quick-%: SQD-% polycalc-% special-cases-% siemens-%
 	@echo ${HR}
-nonquick-%: dsaa-% mapquick-% javautil-% 6170-% large-% new-%
+nonquick-%: dsaa-% mapquick-% javautil-% 6170-% large-% new-% newRar-%


Is this name from the username of the author of the commit? Please use a better name, or eliminate it (and update line 69 below).

mernst · 2018-08-01T18:18:14Z

The build is failing, which indicates I broke something. Sorry about that. I'll look into it this evening.

…nto exception-exit-support

markro49 added 4 commits July 11, 2017 08:05

Philipp Hirch's changes to support exception exits from methods.

dece759

fix a couple of typos

64f2bd3

missed a new goal file

bdb64d0

a little source clean up

91fe6e5

mernst and others added 9 commits July 17, 2017 15:32

Merge github.com:codespecs/daikon into exception-exit-support

e839f68

Add changelog entry [ci skip]

57e3338

clean up after code review

85bda2f

Merge branch 'exception-exit-support' of github.com:markro49/daikon i…

832a572

…nto exception-exit-support

Merge branch 'master' into exception-exit-support

4d26244

Merge branch 'master' into exception-exit-support

32b43ff

Check point changes in response to pull request review.

809c7a3

Still need upstream merge and doc changes.

Merge branch 'master' into exception-exit-support

e9def80

javadoc fix; update new exception goal files

d982c93

markro49 added 4 commits July 31, 2017 07:20

Merge branch 'master' into exception-exit-support

c344ace

update docs to reflect new ppt names and relationships

49eb2d7

remove exception-handling switch; make it the default

a5bef21

fix another blank at end of line in txt-jaif output

update java7 goal files

491ff39

markro49 added 4 commits August 28, 2017 11:06

Merge branch 'master' into exception-exit-support

f4d90c4

Merge branch 'master' into exception-exit-support

c35be22

update goal files due to String EqualityComparison change.

907f505

Merge branch 'master' into exception-exit-support

9477798

mernst mentioned this pull request Jul 30, 2018

Feature exception handling #56

Open

Merge branch 'master' into exception-exit-support

a60986d

mernst reviewed Jul 31, 2018

View reviewed changes

markro49 and others added 2 commits July 31, 2018 07:14

undo refilling of paragraphs

251de7d

Merge ../daikon into exception-exit-support

bb75d9b

mernst added 3 commits August 1, 2018 08:34

Tweak changelog

cfa8943

Changes from code review

feb20e5

Documentation improvements

e8cc02e

mernst requested changes Aug 1, 2018

View reviewed changes

mernst and others added 16 commits August 1, 2018 11:50

Fix cross-reference

8c461ec

Merge branch 'master' into exception-exit-support

29c06b6

merge branch master; address most of comments from mernst

bce5892

Merge branch 'exception-exit-support' of github.com:markro49/daikon i…

82061a1

…nto exception-exit-support

Merge branch 'master' into exception-exit-support

e7f147d

add missing javadoc documentation

2ec156a

Remove unused variables

51ed8c4

Merge ../daikon-branch-master into exception-exit-support

5662498

Merge ../daikon-branch-master into exception-exit-support

f3e6bdc

Merge branch 'master' into exception-exit-support

a6879b7

fix Require Java 8 merge error

118ebb0

Merge ../daikon-branch-master into exception-exit-support

1101880

Small changes

a5d33eb

Merge ../daikon-branch-master into exception-exit-support

133f01f

add missing CLASSPATH changes

177c11a

Merge ../daikon-branch-master into exception-exit-support

d28c06f

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Exception exit support #91

Exception exit support #91

markro49 commented Jul 17, 2017

markro49 commented Jul 17, 2017

markro49 commented Jul 28, 2017

markro49 commented Aug 2, 2017

mernst commented Aug 3, 2017

mernst Jul 31, 2018

mernst left a comment

mernst Aug 1, 2018

mernst Aug 1, 2018

mernst Aug 1, 2018

mernst Aug 1, 2018

mernst Aug 1, 2018

markro49 Aug 7, 2018

mernst Aug 7, 2018

markro49 Aug 7, 2018

mernst Aug 1, 2018

mernst Aug 1, 2018

mernst Aug 1, 2018

markro49 Aug 7, 2018

mernst Aug 7, 2018

mernst Aug 1, 2018

markro49 Aug 7, 2018

mernst Aug 1, 2018

mernst commented Aug 1, 2018

Exception exit support #91

Are you sure you want to change the base?

Exception exit support #91

Conversation

markro49 commented Jul 17, 2017

markro49 commented Jul 17, 2017

markro49 commented Jul 28, 2017

markro49 commented Aug 2, 2017

mernst commented Aug 3, 2017

Choose a reason for hiding this comment

mernst 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

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

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

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

Choose a reason for hiding this comment

mernst commented Aug 1, 2018