Skip to content
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.

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

Feature exception handling #56

Open
wants to merge 23 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
[![Build Status](https://travis-ci.org/rarworld/daikon.svg?branch=FeatureExceptionHandling)](https://travis-ci.org/rarworld/daikon)

This is the distribution of a fork of the Daikon invariant detector,
based on Daikon version 5.3.3, released May 2, 2016.
Daikon version 5.3.3.1_rar, released Mai 24, 2016

If you are working with a Daikon distribution downloaded from the Daikon
website, then most everything is setup and ready to go. See the 'doc'
subdirectory for additional information, including installation instructions.
You should start out with the file:
doc/index.html
The documentation also appears on the Daikon homepage:
http://plse.cs.washington.edu/daikon/

If you are working with source cloned from the source code repository
https://github.com/codespecs/daikon, then please review the file
README.source.
45 changes: 28 additions & 17 deletions doc/daikon.texinfo
Original file line number Diff line number Diff line change
Expand Up @@ -2357,11 +2357,11 @@ Static variables of a class have names of the form
@cindex pre-state variables
@code{orig(x)} refers to the value of variable @code{x} upon
entry to a procedure (because the procedure body might modify the value
of @code{x}). These variables appear only at @code{:::EXIT} program
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.
@xref{orig variable example}.
of @code{x}). These variables appear only at @code{:::EXIT} and
@code{:::THROWCOMBINED} program points. Typically, @code{orig()}
Copy link
Member

Choose a reason for hiding this comment

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

Request: please do not re-fill paragraphs. When you refill a paragraph, it changes many lines in the diff, making it hard to determine what real changes you made. It doesn't matter if the .texinfo file (which will be processed by Texinfo to make the manual) doesn't have perfectly filled paragraphs, because only developers will read it -- and those developers will care more that the diffs are small and easy to read.

Could you please un-fill the paragraphs that you reformatted?

variables do not appear in the trace, but are automatically created by
Daikon when it matches up @code{:::ENTER} and @code{:::EXIT@var{nn}} or
@code{:::THROW@var{nn}} program points. @xref{orig variable example}.

This variable prints as @code{orig} when using Daikon output format
(@pxref{Invariant syntax}), but may print differently in other formats
Expand Down Expand Up @@ -4010,6 +4010,15 @@ command-line argument is given.
The size is specified in the same manner as the
@option{--Xmx} switch to @command{java}; for example: @option{--heap-size=2048m}.

@item --exception-handling
By default, Chicory only traces the call of an exception
(@code{throw new Exception();}) which leads to an exit of the method.
With the @code{--exception-handling} parameter, Chicory will catch all
uncaught Exceptions (thrown and delagted) in the methods and produce a
valid Dataflow hierarchy and trace. To realize it, Chicory encapsulate
every method-block with an try-catch-block, which catches the delegated
exceptions.

@end table


Expand Down Expand Up @@ -7996,19 +8005,20 @@ answer is 0, but you believe that there are samples in the file you are
feeding to Daikon.

Using the normal dataflow hierarchy, Daikon explicitly processes
@code{:::EXIT} program points only. Other program points, such as
@code{:::ENTER} program points, are processed indirectly when their
corresponding @code{:::EXIT} points are encountered.
(You can disable this behavior with the
@code{:::EXIT} and @code{:::THROWCOMBINED} program points only. Other
program points, such as @code{:::ENTER} program points, are processed
indirectly when their corresponding @code{:::EXIT} points are
encountered. (You can disable this behavior with the
@option{--nohierarchy} switch to Daikon;
see @ref{Options to control invariant detection}.)
If no @code{:::EXIT} program points are present (perhaps every
execution threw an exception, you filtered out all the
@code{:::EXIT} program points, or the data trace is obtained from
spreadsheet data instead of from a program execution),
then Daikon will not process any of the other program points, such as
the @code{:::ENTER} program points. You can make Daikon print information
about unmatched procedure entries
If no @code{:::EXIT}/@code{:::THROWCOMBINED} program points are present
(perhaps every execution threw an exception which aren't traced
(@code{-- exception-handling}), you filtered out
all the @code{:::EXIT}/@code{:::THROWCOMBINED} program points, or the
data trace is obtained from spreadsheet data instead of from a
program execution), then Daikon will not process any of the other
program points, such as the @code{:::ENTER} program points. You can
make Daikon print information about unmatched procedure entries
via the @samp{daikon.FileIO.unmatched_procedure_entries_quiet}
configuration option (@pxref{General configuration options}).

Expand Down Expand Up @@ -9156,6 +9166,7 @@ Florian Gross,
Philip Guo,
Melissa Hao,
Michael Harder,
Philipp Hirch,
Dieter von Holten,
Greg Jay,
Josh Kataoka,
Expand Down Expand Up @@ -9185,7 +9196,7 @@ Matthew Tschantz,
Iuliu Vasilescu,
Chen Xiao,
Tao Xie,
Jeff Yuan.
Jeff Yuan
}

@nospellcheck{Craig Kaplan} carved the Daikon logo.
Expand Down
16 changes: 10 additions & 6 deletions doc/developer.texinfo
Original file line number Diff line number Diff line change
Expand Up @@ -1305,14 +1305,15 @@ a dataflow hierarchy.

@itemize
@item
A program point that represents the @code{ENTRY} or @code{EXIT} of a
static method will have a @code{parent} record that points to the
@code{CLASS} program point for the containing class.
A program point that represents the @code{ENTRY}, @code{THROWCOMBINED}
or @code{EXIT} of a static method will have a @code{parent} record that
points to the @code{CLASS} program point for the containing class.

@item
A program point that represents the @code{ENTRY} or @code{EXIT} of a
non-static (instance) method will have a @code{parent} record that points to the
@code{OBJECT} program point for the containing object.
A program point that represents the @code{ENTRY}, @code{THROWCOMBINED}
or @code{EXIT} of a non-static (instance) method will have a
@code{parent} record that points to the @code{OBJECT} program point for
the containing object.

@item
A program point that represents a @code{CLASS}
Expand Down Expand Up @@ -3181,6 +3182,9 @@ The following patterns are for the @code{enter}, @code{subexit},
@example
<fully qualified class name>.<method/function name>(<argument types>):::ENTER
<fully qualified class name>.<method/function name>(<argument types>):::EXIT<id>
<fully qualified class name>.<method/function name>(<argument types>):::THROWS
<fully qualified class name>.<method/function name>(<argument types>):::THROW<id>
<fully qualified class name>.<method/function name>(<argument types>):::THROWCOMBINED
<fully qualified class name>:::CLASS
<fully qualified class name>:::OBJECT
@end example
Expand Down
11 changes: 10 additions & 1 deletion java/daikon/AnnotateNullable.java
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,8 @@ public static void main(String[] args) throws IOException {
// static method can be identified because it will not have the OBJECT
// point as a parent.
for (PptTopLevel ppt : ppts.pptIterable()) {
if (!ppt.is_combined_exit() || !is_static_method(ppt)) continue;
if (!ppt.is_combined_exit() || !ppt.is_combined_exception() || !is_static_method(ppt))
continue;

String name = ppt.name().replaceFirst("[(].*$", "");
int lastdot = name.lastIndexOf('.');
Expand Down Expand Up @@ -424,6 +425,14 @@ public static String jvm_signature(PptTopLevel ppt) {
"signature") // application invariant: returnVar.type.toString() is a binary name (if returnVar is non-null), because we are processing a Java program
String returnType =
returnVar == null ? "V" : UtilMDE.binaryNameToFieldDescriptor(returnVar.type.toString());
// Or an throw point
Copy link
Member

Choose a reason for hiding this comment

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

Nit: "an throw" should be "a throw".

if (returnVar == null) {
returnVar = ppt.find_var_by_name("exception");
returnType =
returnVar == null
? "V"
: "V throws " + UtilMDE.binaryNameToFieldDescriptor(returnVar.type.toString());
}

return method + UtilMDE.arglistToJvm(java_args) + returnType;
}
Expand Down
18 changes: 14 additions & 4 deletions java/daikon/Chicory.java
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,12 @@ public class Chicory {
@Option("Number of calls after which sampling will begin")
public static int sample_start = 0;

@Option("Should Exception Handling be taken care of?")
Copy link
Member

Choose a reason for hiding this comment

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

Please make the documentation of this option more explicit. "taken care of" won't be clear to readers.

public static boolean exception_handling = false;

@Option("Enable remote debug")
public static boolean remote_debug = false;

/**
* Daikon port number. Daikon writes this to stdout when it is started
* in online mode.
Expand All @@ -138,8 +144,6 @@ public class Chicory {
/** flag to use if we want to turn on the static initialization checks **/
public static final boolean checkStaticInit = true;

private static final boolean RemoteDebug = false;

/** Flag to initiate a purity analysis and use results to create add vars **/
private static boolean purityAnalysis = false;

Expand Down Expand Up @@ -338,9 +342,10 @@ void start_target(String premain_args, String[] target_args) {
List<String> cmdlist = new ArrayList<String>();
cmdlist.add("java");

if (RemoteDebug) {
if (remote_debug) {
//-Xdebug -Xrunjdwp:server=y,transport=dt_socket,address=4142,suspend=n
cmdlist.add("-Xdebug -Xrunjdwp:server=n,transport=dt_socket,address=8000,suspend=y");
cmdlist.add("-agentlib:jdwp=transport=dt_socket,server=y,address=8000,suspend=y");
//cmdlist.add("-Xdebug -Xrunjdwp:server=n,transport=dt_socket,address=8000,suspend=y");
//cmdlist.add("-Xdebug -Xnoagent -Xrunjdwp:transport=dt_socket,server=n,suspend=n,address=8000 -Djava.compiler=NONE");
}

Expand Down Expand Up @@ -465,6 +470,11 @@ public void runDaikon() {
dtrace_file);
}

if (remote_debug) {
cmdstr =
cmdstr.replace(
"java", "java -agentlib:jdwp=transport=dt_socket,server=y,address=8001,suspend=y");
}
//System.out.println("daikon command is " + daikon_cmd);
//System.out.println("daikon command cmdstr " + cmdstr);

Expand Down
11 changes: 8 additions & 3 deletions java/daikon/Daikon.java
Original file line number Diff line number Diff line change
Expand Up @@ -1628,7 +1628,12 @@ public static void create_combined_exits(PptMap ppts) {

PptTopLevel exitnn_ppt = ppt;
PptName exitnn_name = exitnn_ppt.ppt_name;
PptName exit_name = ppt.ppt_name.makeExit();
PptName exit_name;
if (!exitnn_name.isThrowPoint()) {
exit_name = ppt.ppt_name.makeExit();
} else {
exit_name = ppt.ppt_name.makeThrowExit();
}
PptTopLevel exit_ppt = exit_ppts.get(exit_name);

if (debugInit.isLoggable(Level.FINE)) {
Expand Down Expand Up @@ -1715,7 +1720,7 @@ static List<Invariant> filter_invs(List<Invariant> invs) {
* Does nothing if exit_ppt is not an EXIT/EXITnn.
*/
private static void create_orig_vars(PptTopLevel exit_ppt, PptMap ppts) {
if (!exit_ppt.ppt_name.isExitPoint()) {
if (!exit_ppt.ppt_name.isExitPoint() && !exit_ppt.ppt_name.isExceptionPoint()) {
if (VarInfo.assertionsEnabled()) {
for (VarInfo vi : exit_ppt.var_infos) {
try {
Expand Down Expand Up @@ -2295,8 +2300,8 @@ public static void setupEquality(PptTopLevel ppt) {
// named program points such as :::POINT (used by convertcsv.pl)
// will be treated as leaves.
if (p.ppt_name.isCombinedExitPoint()
|| p.ppt_name.isCombinedThrowPoint()
|| p.ppt_name.isEnterPoint()
|| p.ppt_name.isThrowsPoint()
|| p.ppt_name.isObjectInstanceSynthetic()
|| p.ppt_name.isClassStaticSynthetic()) {
return;
Expand Down
16 changes: 13 additions & 3 deletions java/daikon/FileIO.java
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,12 @@ private FileIO() {
// a number may follow it.
public static final String exit_suffix = "EXIT";
public static final String exit_tag = ppt_tag_separator + exit_suffix;
public static final String throw_suffix = "THROW";
public static final String throw_tag = ppt_tag_separator + throw_suffix;
public static final String throws_suffix = "THROWS";
public static final String throws_tag = ppt_tag_separator + throws_suffix;
public static final String exception_suffix = "THROWSCOMBINED";
public static final String exception_tag = ppt_tag_separator + exception_suffix;
public static final String object_suffix = "OBJECT";
public static final String object_tag = ppt_tag_separator + object_suffix;
public static final String class_static_suffix = "CLASS";
Expand Down Expand Up @@ -1041,8 +1045,8 @@ private static void warn_if_hierarchy_mismatch(PptMap all_ppts) {
for (PptTopLevel ppt_top_level : all_ppts.ppt_all_iterable()) {
boolean is_program_point =
(ppt_top_level.ppt_name.isExitPoint()
|| ppt_top_level.ppt_name.isExceptionPoint()
|| ppt_top_level.ppt_name.isEnterPoint()
|| ppt_top_level.ppt_name.isThrowsPoint()
|| ppt_top_level.ppt_name.isObjectInstanceSynthetic()
|| ppt_top_level.ppt_name.isClassStaticSynthetic()
|| ppt_top_level.ppt_name.isGlobalPoint());
Expand Down Expand Up @@ -1773,9 +1777,9 @@ public static void process_sample(
// and :::CLASS program points. This scheme ensures that arbitrarly
// named program points such as :::POINT (used by convertcsv.pl)
// will be treated as leaves.
// Throws is a LEAF now, like Exit_nn
Copy link
Member

Choose a reason for hiding this comment

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

"now" isn't necessary. Why is "LEAF" capitalized?
This line seems contradictory with line 1776.


if (ppt.ppt_name.isEnterPoint()
|| ppt.ppt_name.isThrowsPoint()
|| ppt.ppt_name.isObjectInstanceSynthetic()
|| ppt.ppt_name.isClassStaticSynthetic()
|| ppt.ppt_name.isGlobalPoint()) {
Expand All @@ -1787,6 +1791,12 @@ public static void process_sample(
throw new RuntimeException(
"Bad program point name " + ppt.name + " is a combined exit point name");
}

if (ppt.ppt_name.isExceptionPoint() && ppt.ppt_name.isCombinedThrowPoint()) {
Copy link
Member

Choose a reason for hiding this comment

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

The lack of parallelism between the names "isExceptionPoint()" and "isCombinedThrowPoint()" is confusing. Please use the same term, either "Exception" or "Throw", in both.

// not Daikon.TerminationMessage; caller has more info (e.g., filename)
throw new RuntimeException(
"Bad program point name " + ppt.name + " is a combined exception point name");
}
}

// Add derived variables
Expand Down Expand Up @@ -2224,7 +2234,7 @@ public static boolean compute_orig_variables(
return false;
}

if (ppt.ppt_name.isExitPoint() || ppt.ppt_name.isThrowsPoint()) {
if (ppt.ppt_name.isExitPoint() || ppt.ppt_name.isExceptionPoint()) {
Invocation invoc;
// Set invoc
{
Expand Down
16 changes: 11 additions & 5 deletions java/daikon/MergeInvariants.java
Original file line number Diff line number Diff line change
Expand Up @@ -271,12 +271,12 @@ public static void mainHelper(String[] args)
debugProgress.fine("Building hierarchy between leaves of the maps");
for (PptTopLevel ppt : merge_ppts.pptIterable()) {

// Skip everything that is not a final exit point
if (!ppt.ppt_name.isExitPoint()) {
// Skip everything that is not a final exit or exception point
if (!ppt.ppt_name.isExitPoint() && !ppt.ppt_name.isExceptionPoint()) {
assert ppt.children.size() > 0 : ppt;
continue;
}
if (ppt.ppt_name.isCombinedExitPoint()) {
if (ppt.ppt_name.isCombinedExitPoint() || ppt.ppt_name.isCombinedThrowPoint()) {
assert ppt.children.size() > 0 : ppt;
continue;
}
Expand Down Expand Up @@ -383,8 +383,14 @@ public static void mainHelper(String[] args)
// Remove the PptRelation links so that when the file is written
// out it only includes the new information
for (PptTopLevel ppt : merge_ppts.pptIterable()) {
if (!ppt.ppt_name.isExitPoint()) continue;
if (ppt.ppt_name.isCombinedExitPoint()) continue;

if (!ppt.ppt_name.isExitPoint() && !ppt.ppt_name.isExceptionPoint()) {
continue;
}
if (ppt.ppt_name.isCombinedExitPoint() || ppt.ppt_name.isCombinedThrowPoint()) {
continue;
}

ppt.children.clear();
for (PptConditional cond : ppt.cond_iterable()) {
cond.children.clear();
Expand Down
Loading