Daikon API

[Inga Egorova]

Hello.

I'm developing tool and I'd like to use Daikon to obtain invariants.

The best way to do it obviously is to use API, but documentation is pretty ambiguous and there are really only few examples on Github now.

Can you, please, if it's possible, provide an "schema" example how to get values for one specific invariant, say IntGreaterEqual?  

Thank you in advance.

[Michael Ernst]

I'm sorry you are having trouble.

We would like to help, but from your message, I am not sure what you are trying to do.

Could you please be more specific?  For example, is your goal to create a tool that internally runs Daikon and then obtains information about one invariant in Daikon's output?

Also, you said "documentation is pretty ambiguous".  Can you please say exactly what documentation you are having trouble with, and what is your specific confusion regarding it?

With more information, perhaps we can help you.

Mike

--
You received this message because you are subscribed to the Google Groups "Daikon discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to daikon-discus...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/daikon-discuss/e3c95021-14c2-4550-8ae8-93cb01d9c0a5%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Inga Egorova]

I'm trying to adapt Daikon to infer invariants, describing restrictions on values of Java classes field variables and method parameters in ENTER and EXIT ppt's.

It's necessary because I'm working on inference of formal rules of software libraries usage and model is planned to be based on invariants.

I've found API description for FileIO.Processor and tried to use: 

SimpleProcessor + PrintInvariants.print_all_ternary_invs(ppts);

but got nothing. Also I've tried to use: 

get_invariants(), instantiate_views_and_invariants().

And implemented subclass of CollectDataProcessor.

As a possible way to reach a result I also thought of either 

PptTopLevel.add_bottom_up() 

or 

ppt.get_or_instantiate_slice(..) + addInvariant(..),

but the last one seems too tricky.

Actually I need to be able to define very limited number of types of invariants (like "allow") and to get values (whether they were falsified or not).

I've started to read code of DaikonHelper though it seems probably to be not so helpful as I wish because it contains calls of internal functions/ usage of internal vars.

But finally after addition of 

setup_proto_invs(); 

it works! If I understand correctly that the only addition I need to choose desirable invariants is to add them to proto_invs list manually?

понедельник, 17 июня 2019 г., 19:23:32 UTC+3 пользователь Inga Egorova написал:

[Michael Ernst]

Thank you for the additional details.

I'm trying to adapt Daikon to infer invariants, describing restrictions on values of Java classes field variables and method parameters in ENTER and EXIT ppt's.

According to this description, you are trying to modify Daikon, not build a different tool that uses Daikon.  Is that correct?

Can you give an example of output that Daikon fails to produce, but which you want to produce?

I ask this because Daikon already does what you described:  it computes facts about values of Java classes field variables and method parameters in ENTER and EXIT ppt's.  Maybe there is a simpler solution for your problem.

 

Actually I need to be able to define very limited number of types of invariants (like "allow") and to get values (whether they were falsified or not).

Daikon has command-line arguments to enable/disable specific types of invariants.  Could you use those?

it works! If I understand correctly that the only addition I need to choose desirable invariants is to add them to proto_invs list manually?

I'm glad that works for you!  Without seeing your code I cannot be certain, but that seems like a reasonable approach.

However, the command-line arguments I mentioned above give the same effect, without needing to modify Daikon's source code.

Mike

[Inga Egorova]

According to this description, you are trying to modify Daikon, not build a different tool that uses Daikon.  Is that correct?

No, probably it wasn't the best way to describe my task. I need to use Daikon to get predicates to be able to generate class methods specifications based on results.

 

Can you give an example of output that Daikon fails to produce, but which you want to produce?

I want it to give me predicates for field variables & method parameters to describe possible invocations of methods. Like 'x<=2' and so on.

 

Daikon has command-line arguments to enable/disable specific types of invariants.  Could you use those?

Currently I'm trying to do the same programatically, but, unfortunately, it doesn't work. Could you, please, told me, what's wrong here:

https://github.com/Suntrie/daikonization/blob/0ec773adf14fc397129b69815da90903938522c9/src/main/java/predicatesGenerator/DaikonRunner.java#L141 ?

As I see, it's just a programmatic way to enable/disable specific predicates. Now, for test project https://github.com/Suntrie/jackson-example.git  there is an exception (with commented code included):

Exception in thread "main" java.lang.NullPointerException

at daikon.PptSlice.repCheck(PptSlice.java:301)

at daikon.PptTopLevel.repCheck(PptTopLevel.java:3322)

at daikon.DaikonSimple.instantiate_views_and_invariants(DaikonSimple.java:304)

at daikon.DaikonSimple$SimpleProcessor.add(DaikonSimple.java:601)

at daikon.DaikonSimple$SimpleProcessor.add(DaikonSimple.java:585)

at daikon.DaikonSimple$SimpleProcessor.process_sample(DaikonSimple.java:539)

at daikon.FileIO.read_data_trace_file(FileIO.java:1436)

at daikon.FileIO.read_data_trace_files(FileIO.java:964)

at predicatesGenerator.DaikonRunner.getInvariantsPptMap(DaikonRunner.java:145)

at predicatesGenerator.DaikonRunner.generateInvariantsPptMap(DaikonRunner.java:163)

at predicateMiningAPIFacade.Main.update_ppt_map(Main.java:72)

at predicateMiningAPIFacade.Main.main(Main.java:53)

Also there is another unclear exception. I can't find standard reasons to get this:

Chicory warning: ClassFile: org.apache.commons.math3.util.Precision - classfile version (49) is out of date and may not be processed correctly.
Unexpected exception encountered: java.lang.RuntimeException: Invalid StackMap offset 3java.lang.RuntimeException: Invalid StackMap offset 3
 at org.plumelib.bcelutil.StackMapUtils.modify_stack_maps_for_switches(StackMapUtils.java:363)
 at daikon.chicory.Instrument.instrument_all_methods(Instrument.java:517)
 at daikon.chicory.Instrument.transform(Instrument.java:204)
 at sun.instrument.TransformerManager.transform(TransformerManager.java:188)
 at sun.instrument.InstrumentationImpl.transform(InstrumentationImpl.java:428)
 at java.lang.ClassLoader.defineClass1(Native Method)
 at java.lang.ClassLoader.defineClass(ClassLoader.java:763)
 at java.security.SecureClassLoader.defineClass(SecureClassLoader.java:142)
 at java.net.URLClassLoader.defineClass(URLClassLoader.java:468)
 at java.net.URLClassLoader.access$100(URLClassLoader.java:74)
 at java.net.URLClassLoader$1.run(URLClassLoader.java:369)
 at java.net.URLClassLoader$1.run(URLClassLoader.java:363)
 at java.security.AccessController.doPrivileged(Native Method)
 at java.net.URLClassLoader.findClass(URLClassLoader.java:362)
 at java.lang.ClassLoader.loadClass(ClassLoader.java:424)
 at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:349)
 at java.lang.ClassLoader.loadClass(ClassLoader.java:357)
 at org.apache.commons.math3.stat.descriptive.rank.Percentile.removeAndSlice(Percentile.java:521)
 at org.apache.commons.math3.stat.descriptive.rank.Percentile.getWorkArray(Percentile.java:455)
 at org.apache.commons.math3.stat.descriptive.rank.Percentile.evaluate(Percentile.java:351)
 at org.apache.commons.math3.stat.descriptive.rank.Percentile.evaluate(Percentile.java:302)
 at org.apache.commons.math3.util.ResizableDoubleArray.compute(ResizableDoubleArray.java:949)
 at org.apache.commons.math3.stat.descriptive.DescriptiveStatistics.apply(DescriptiveStatistics.java:499)
 at org.apache.commons.math3.stat.descriptive.DescriptiveStatistics.getPercentile(DescriptiveStatistics.java:460)
 at com.journaldev.jackson.model.Address.squareOfToString(Address.java:52)
 at RegressionTest0.test24(RegressionTest0.java:352)
 at RegressionTestDriver.main(RegressionTestDriver.java:145)

Thank you for help.

[Inga Egorova]

A little addition: I just have managed to resolve my first problem (correction of order of invocations was required), but I still got exceptions from Chicory and any help would be appreciated.

понедельник, 17 июня 2019 г., 21:35:16 UTC+3 пользователь Michael Ernst написал:

[Michael Ernst]

I'm sorry you are still having trouble.
I have the same questions as in my response two months ago.
Without answers to those questions, we cannot help you.

Can you please give a complete program, the exact commands to run it and run Daikon (able to be cut-and-pasted into a Linux command shell), the exact output, and the output that you would like to see?

> Could you, please, told me, what's wrong here:
> https://github.com/Suntrie/daikonization/blob/0ec773adf14fc397129b69815da90903938522c9/src/main/java/predicatesGenerator/DaikonRunner.java#L141 ?

Well, the first problem is that it isn't documented. :-)
Without knowing what you are trying to do and what went wrong, I cannot speculate regarding what the solution might be.
But, it's more important to answer my question above.

> Chicory warning: ClassFile: org.apache.commons.math3.util.Precision - classfile version (49) is out of date and may not be processed correctly.

Your program uses an old classfile format that is missing information that Chicory uses during instrumentation.  Chicory might work properly, or it might not.  You can eliminate the warning by re-compiling your program, using a @code{-target} command-line argument for a more recent version of Java.  In your case, classfile version 49 corresponds to Java 5, which was released in 2004; Java 6 was released in 2006, and Java 8 was released in 2014.

> Unexpected exception encountered: java.lang.RuntimeException: Invalid StackMap offset 3java.lang.RuntimeException: Invalid StackMap offset 3

This indicates that either a .class file that was supplied to Chicory was malformed, or Chicory has a bug.

Mike

--

You received this message because you are subscribed to the Google Groups "Daikon discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to daikon-discus...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/daikon-discuss/5c14d62b-cb55-44d8-a17a-388c9a8ceab1%40googlegroups.com.