Need to use Logical Compare feature of Daikon

58 views
Skip to first unread message

Tanzeem Bin Noor

unread,
Dec 3, 2014, 3:28:48 PM12/3/14
to daikon-...@googlegroups.com
Hi,

I need to use the Logical Compare feature of Daikon tool (8.1.8). As the manual mentions, it requires the Simplify tool. (http://www.hpl.hp.com/downloads/crl/jtk/). I've downloaded the tool, but failed to install that on both Scientific Linux 32 and 64 bit. Actually, It got relocation error while trying to install. After searching on the Google, I found that the relocation error occurs because of trying to install old apps (rpms) on new systems. The Simplify tool requires PM3 compiler and the Simplify README gives the link as

for required packages. But I think the packages listed in the above are old and the development is not active anymore. I wonder how could I setup this Simplify tool? Is there any way to use Logical Compare of Daikon without using Simplify? If anyone has already installed Simplify/used logical compare, could you please share the recipe? I'm really stuck here. 

Thanks in advance.  

Stephen McCamant

unread,
Dec 5, 2014, 3:01:15 PM12/5/14
to daikon-...@googlegroups.com
>>>>> "TBN" == Tanzeem Bin Noor <tanzee...@gmail.com> writes:

TBN> Hi,
TBN> I need to use the Logical Compare feature of Daikon tool
TBN> (8.1.8). As the manual mentions, it requires the Simplify tool. (
TBN> http://www.hpl.hp.com/downloads/crl/jtk/). I've downloaded the
TBN> tool, but failed to install that on both Scientific Linux 32 and
TBN> 64 bit. Actually, It got relocation error while trying to
TBN> install. After searching on the Google, I found that the
TBN> relocation error occurs because of trying to install old apps
TBN> (rpms) on new systems. The Simplify tool requires PM3 compiler
TBN> and the Simplify README gives the link as
TBN> http://www.inference.phy.cam.ac.uk/ear23/m3/

TBN> for required packages. But I think the packages listed in the
TBN> above are old and the development is not active anymore. I wonder
TBN> how could I setup this Simplify tool? Is there any way to use
TBN> Logical Compare of Daikon without using Simplify? If anyone has
TBN> already installed Simplify/used logical compare, could you please
TBN> share the recipe? I'm really stuck here.

I think you're right that Simplify and the Modula 3 language it was
written in are both pretty much unmaintained right now.

Another community that has been using Simplify is ESC/Java 2. The
ESC/Java 2 site provides a binary archive of Simplify versions at:

http://kindsoftware.com/products/opensource/archives/Simplify-1.5.5-13-06-07-binary.zip

The Linux binary included in that distribution is 32-bit and
statically linked, so I think it should work across a large variety of
Linux distributions: for instance I checked just now that it works
fine on my Ubuntu 12.04 64-bit workstation here.

If we were writing this functionality from scratch now, we'd probably
use a SMT-LIB2 compatible solver like Z3 or CVC4 instead of Simplify.
Z3 actually used to have some compatibility support for the Simplify
input format, but I believe that has itself been removed in recent
versions. Conceptually I don't think there would be any major
obstacles to converting this code to work with an SMT-LIB2 solver, but
there might need to be a significant amount of boilerplate code
written to output each different kind of invariant in SMT-LIB2 format.

Hope this helps,

-- Stephen

Tanzeem Bin Noor

unread,
Dec 7, 2014, 8:26:48 PM12/7/14
to daikon-...@googlegroups.com
Hi Stephen,

Thanks for your reply. According to your information, I've downloaded the binary .zip and extracted that. I found "Simplify-1.5.4.linux" in the extracted Simplify folder. Then, I added execute permission ( chmod u+x Simplify-1.5.4.linux). Next, if I type ./Simplify-1.5.4.linux , I get a blank prompt (>). If I put, suppose x=2 in the prompt I get the following
>    x=2
Counterexample:  context:    (AND      (NOT x)    )
1: Invalid. >    Counterexample:
  context:    (AND      (NOT =)    )
2: Invalid. >    Bad input: Predicate not an atom or list.

Is the Simplify is working properly here? Actually I didn't use Simplify before. So, I'm not sure regarding the output.

However, after exiting the prompt, if I write "java daikon.tools.compare.LogicalCompare 00.inv.gz 01.inv.gz" I get the following error

Could not utilize Simplify: daikon.simplify.SimplifyError: java.io.IOException: Cannot run program "Simplify": error=2, No such file or directory
Exception in thread "main" daikon.simplify.SimplifyError: Couldn't start Simplify

This error is already mentioned in the troubleshooting section of daikon manual; it means Simplify has not been installed properly. 

So, am I missing something while installing Simplify, like setting any PATH or other things? I just need the LogicalCompare feature working for now. Could you please give me some more suggestions so that I can fix this. I really appreciate your help.

Michael Ernst

unread,
Dec 8, 2014, 1:39:27 AM12/8/14
to daikon-discuss, Tanzeem Bin Noor
> Could not utilize Simplify: daikon.simplify.SimplifyError:
> java.io.IOException: Cannot run program "Simplify": error=2, No such
> file or directory
> Exception in thread "main" daikon.simplify.SimplifyError: Couldn't start
> Simplify
>
> This error is already mentioned in the troubleshooting section of daikon
> manual; it means Simplify has not been installed properly.
>
> So, am I missing something while installing Simplify, like setting any
> PATH or other things?

Yes, you need to put the Simplify executable on your path. Alternately,
you could set the simplify.path property to its absolute pathname.

-Mike

Tanzeem Bin Noor

unread,
Dec 8, 2014, 1:13:18 PM12/8/14
to daikon-...@googlegroups.com

I have set up the PATH environment variable to the folder locating Simplify-1.5.4.linux after extracting from http://kindsoftware.com/products/opensource/archives/Simplify-1.5.5-13-06-07-binary.zip . I've already given the executable permission to. But still I'm getting the same error. Do I need to install PM3 or CM3 compiler separately? I didn't do that. If I need to install these compilers then which version should I use?

I'm using a Linux machine with the daikon tool working and I'm using daikon on Java code. I just need the steps to install Simplify from scratch so that I can use the logicalCompare feature on Java code. As I said, the simplify README (link given the daikon manual) contains the link of obsolete packages and I'm getting relocation errors while following the instructions in the README. 

Thanks for considering my issue. I really appreciate any further help.      
 

Stephen McCamant

unread,
Dec 8, 2014, 4:35:15 PM12/8/14
to daikon-...@googlegroups.com
>>>>> "TBN" == Tanzeem Bin Noor <tanzee...@gmail.com> writes:

TBN> I have set up the PATH environment variable to the folder locating
TBN> Simplify-1.5.4.linux after extracting from
TBN> http://kindsoftware.com/products/opensource/archives/Simplify-1.5.5-13-06-07-binary.zip .
TBN> I've already given the executable permission to. But still I'm
TBN> getting the same error. Do I need to install PM3 or CM3 compiler
TBN> separately? I didn't do that. If I need to install these
TBN> compilers then which version should I use?

No, you shouldn't need to install a Modula 3 compiler; I expect doing
so would be a significant amount of work so you probably want to avoid
it if you can. (I believe I successfully bootstrapped PM3 and
recompiled Simplify back when I was doing a project with this code;
I'm sure I tried. But I wouldn't expect it to have gotten easier in
the interim.)

TBN> I'm using a Linux machine with the daikon tool working and I'm
TBN> using daikon on Java code. I just need the steps to *install
TBN> Simplify from scratch* so that I can use the logicalCompare
TBN> feature on Java code. As I said, the simplify README (link given
TBN> the daikon manual) contains the link of obsolete packages and I'm
TBN> getting relocation errors while following the instructions in the
TBN> README.

Okay. I think the context of your use makes sense to me. Probably the
reason you are finding that the documentation is suggesting an old
source for Simplify is that this feature of Daikon is not among the
more frequently used, and sometimes users manage to muddle through
with imperfect documentation and then do not bother to suggest an
improvement. However if we manage to resolve your issue, that will
probably suggest a way the documentation could be improved.

I think the best thing to push the discussion forward would be if you
could send the exact text of the error message (what you describe as a
"relocation error") you see when you try to run the Simplify binary
from the source I suggested. Probably the most common kind of error
one would expect to see in a situation like this is if the program
depends on a dynamically-linked library or a particular symbol within
that library that is not available on your system, and that might be
called a "relocation error": in that case the identity of the
library/symbol would be key for suggesting a workaround. However an
attribute of the binaries I suggested was that they are statically
linked, which is supposed to avoid any such problems.

Tanzeem Bin Noor

unread,
Dec 8, 2014, 6:07:49 PM12/8/14
to daikon-...@googlegroups.com, sm...@alum.mit.edu
Thanks again for the suggestion.

No, you shouldn't need to install a Modula 3 compiler; I expect doing
so would be a significant amount of work so you probably want to avoid
it if you can. (I believe I successfully bootstrapped PM3 and
recompiled Simplify back when I was doing a project with this code;
I'm sure I tried. But I wouldn't expect it to have gotten easier in
the interim.)

Good to know that the manual compiler installation is no need. So, I'm not going to consider the README in Simplify that says to install the compiler.  

TBN> I'm using a Linux machine with the daikon tool working and I'm
TBN> using daikon on Java code. I just need the steps to *install
TBN> Simplify from scratch* so that I can use the logicalCompare
TBN> feature on Java code. As I said, the simplify README (link given
TBN> the daikon manual) contains the link of obsolete packages and I'm
TBN> getting relocation errors while following the instructions in the
TBN> README.


I think the best thing to push the discussion forward would be if you
could send the exact text of the error message (what you describe as a
"relocation error") you see when you try to run the Simplify binary
from the source I suggested. 
 
The relocation error comes when I try to follow the README instructions, NOT when trying your suggested binary. So, the steps I followed:

1. In a fresh Scientific Linux 64 bit machine with daikon installed, extracted the binary .zip http://kindsoftware.com/products/opensource/archives/Simplify-1.5.5-13-06-07-binary.zip
2. Found "Simplify-1.5.4.linux", "Simplify-1.5.4.exe", "Simplify-1.5.4.macosx", "Simplify-1.5.4.solaris", "plugin.xml" and a "META-INF" directory containing "MANIFEST.MF" file.
3. Added execute permission ( chmod u+x Simplify-1.5.4.linux).
4. Added the extracted directory containing "Simplify-1.5.4.linux" to PATH environment variable using EXPORT command. 
5. Now, if I type ./Simplify-1.5.4.linux , I get a blank prompt (>). If I put, suppose x=2 in the prompt I get the following
>    x=2
Counterexample:  context:    (AND      (NOT x)    )
1: Invalid. >    Counterexample:
  context:    (AND      (NOT =)    )
2: Invalid. >    Bad input: Predicate not an atom or list.

Is the Simplify is working properly here, as it is showing the above output? As I never used Simplify before, I'm not sure regarding the output.


However, after exiting the prompt, if I write "java daikon.tools.compare.LogicalCompare 00.inv.gz 01.inv.gz" I get the following error

Could not utilize Simplify: daikon.simplify.SimplifyError: java.io.IOException: Cannot run program "Simplify": error=2, No such file or directory
Exception in thread "main" daikon.simplify.SimplifyError: Couldn't start Simplify

which indicates Simplify is not working properly. Is the link http://kindsoftware.com/products/opensource/archives/Simplify-1.5.5-13-06-07-binary.zip enough for the Simplify installation without any other set-up, just following the above steps? If so, then what am I still missing?

Thanks.
--Tanzeem 




Stephen McCamant

unread,
Dec 9, 2014, 11:55:14 AM12/9/14
to Tanzeem Bin Noor, daikon-...@googlegroups.com
>>>>> "TBN" == Tanzeem Bin Noor <tanzee...@gmail.com> writes:

...
TBN> 4. Added the extracted directory containing
TBN> "Simplify-1.5.4.linux" to PATH environment variable using
TBN> EXPORT command.

TBN> 5. Now, if I type ./Simplify-1.5.4.linux , I get a blank prompt (>). If I
TBN> put, suppose x=2 in the prompt I get the following
TBN > x=2
TBN> Counterexample: context: (AND (NOT x) )
TBN> 1: Invalid. > Counterexample:
TBN> context: (AND (NOT =) )
TBN> 2: Invalid. > Bad input: Predicate not an atom or list.

TBN> Is the Simplify is working properly here, as it is showing the
TBN> above output? As I never used Simplify before, I'm not sure
TBN> regarding the output.

This looks to me like it's running without any low-level difficulties,
yes. The syntax is S-expression based, so a few more plausible
examples you might try are:

(EQ (+ 2 2) 4)
(EQ (+ 2 2) 5)
(> (+ x 1) x)

TBN> However, after exiting the prompt, if I write "java
TBN> daikon.tools.compare.LogicalCompare 00.inv.gz 01.inv.gz" I get the
TBN> following error

TBN> Could not utilize Simplify: daikon.simplify.SimplifyError:
TBN> java.io.IOException: Cannot run program "Simplify": error=2, No
TBN> such file or directory
TBN> Exception in thread "main" daikon.simplify.SimplifyError:
TBN> Couldn't start Simplify

TBN> which indicates Simplify is not working properly. Is the link
TBN> http://kindsoftware.com/products/opensource/archives/Simplify-1.5.5-13-06-07-binary.zip
TBN> enough for the Simplify installation* without any other set-up,
TBN> just following the above steps*? If so, then what am I still
TBN> missing?

The next problem it sounds like you might be having is that Daikon is
expecting the Simplify binary to be named "Simplify", whereas the one
you're trying to use from that distribution is in a file named
"Simplify-1.5.4.linux". Try linking or renaming the file so that it
appears in your $PATH with the name just "Simplify".

Tanzeem Bin Noor

unread,
Dec 9, 2014, 12:36:47 PM12/9/14
to daikon-...@googlegroups.com, tanzee...@gmail.com, sm...@alum.mit.edu

This looks to me like it's running without any low-level difficulties,
yes. The syntax is S-expression based, so a few more plausible
examples you might try are:

  (EQ (+ 2 2) 4)
  (EQ (+ 2 2) 5)
  (> (+ x 1) x)

Great. Now it is showing valid for the first expression and invalid for the second. So, I think Simplify is working properly.

The next problem it sounds like you might be having is that Daikon is
expecting the Simplify binary to be named "Simplify", whereas the one
you're trying to use from that distribution is in a file named
"Simplify-1.5.4.linux". Try linking or renaming the file so that it
appears in your $PATH with the name just "Simplify".

Great again.  After renaming, the previous "Cannot run program "Simplify":" error is gone. But, now if I put the command
"java daikon.tools.compare.LogicalCompare 00.inv.gz 01.inv.gz"
I'm getting the following error:
Exception in thread "main" java.lang.RuntimeException: Could not find simplify/daikon-background.txt
    at daikon.simplify.SessionManager.proverBackground(SessionManager.java:111)
    at daikon.simplify.SessionManager.attemptProverStartup(SessionManager.java:158)
    at daikon.simplify.LemmaStack.startProver(LemmaStack.java:94)
    at daikon.simplify.LemmaStack.<init>(LemmaStack.java:113)
    at daikon.tools.compare.LogicalCompare.startProver(LogicalCompare.java:400)
    at daikon.tools.compare.LogicalCompare.mainHelper(LogicalCompare.java:752)
    at daikon.tools.compare.LogicalCompare.main(LogicalCompare.java:570)

Am I giving correct command here for daikon? Where should be the "daikon-background.txt"? Is it missing?

Thanks again for your kind consideration.
--Tanzeem

Michael Ernst

unread,
Dec 10, 2014, 2:40:44 AM12/10/14
to daikon-discuss, Tanzeem Bin Noor, Stephen McCamant
Tanzeem-

> if I put the command
> "java daikon.tools.compare.LogicalCompare 00.inv.gz 01.inv.gz"
> I'm getting the following error:
> Exception in thread "main" java.lang.RuntimeException: Could not find
> simplify/daikon-background.txt
> at
> daikon.simplify.SessionManager.proverBackground(SessionManager.java:111)
> at
> daikon.simplify.SessionManager.attemptProverStartup(SessionManager.java:158)
> at daikon.simplify.LemmaStack.startProver(LemmaStack.java:94)
> at daikon.simplify.LemmaStack.<init>(LemmaStack.java:113)
> at
> daikon.tools.compare.LogicalCompare.startProver(LogicalCompare.java:400)
> at
> daikon.tools.compare.LogicalCompare.mainHelper(LogicalCompare.java:752)
> at daikon.tools.compare.LogicalCompare.main(LogicalCompare.java:570)
>
> Am I giving correct command here for daikon? Where should be the
> "daikon-background.txt"? Is it missing?

The resource daikon/simplify/daikon-background.txt is supposed to be found
on your classpath. It is in daikon.jar. What is your classpath?

-Mike

Tanzeem Bin Noor

unread,
Dec 10, 2014, 12:42:08 PM12/10/14
to daikon-...@googlegroups.com, tanzee...@gmail.com, sm...@alum.mit.edu, mer...@cs.washington.edu
> if I put the command
> "java daikon.tools.compare.LogicalCompare 00.inv.gz 01.inv.gz"
> I'm getting the following error:
> Exception in thread "main" java.lang.RuntimeException: Could not find
> simplify/daikon-background.txt

> Am I giving correct command here for daikon? Where should be the
> "daikon-background.txt"? Is it missing?

The resource daikon/simplify/daikon-background.txt is supposed to be found
on your classpath.  It is in daikon.jar.  What is your classpath?

 Thanks for your reply. My $CLASSPATH is as follows: /opt/Daikon_Parent/daikon/daikon.jar:.:/usr/lib/jvm/java-1.7.0-openjdk-1.7.0.65.x86_64/jre/lib/rt.jar:/usr/lib/jvm/java-1.7.0-openjdk-1.7.0.65.x86_64/lib/tools.jar

As I'm able to run other daikon commands, e.g., java daikon.Daikon 00.dtrace.gz, java daokon.PrintInvariants 00.inv.gz, java daikon.MergeInvaiants 00.inv.gz 01.inv.gz, I think the CLASSPATH is OK. Isn't it?

I checked the daikon.jar and found the resource at daikon/simplify/daikon-background.txt, as you mentioned. According to the error message, is it looking for the resource at simplify/daikon-background.txt instead of daikon/simplify/daikon-background.txt?

Thanks again.
--Tanzeem

Michael Ernst

unread,
Dec 10, 2014, 11:43:11 PM12/10/14
to Tanzeem Bin Noor, daikon-discuss, Stephen McCamant
Tanzeem-

> According to the error message, is it looking for the resource at
> simplify/daikon-background.txt instead of
> daikon/simplify/daikon-background.txt?

The problem was a bit more pernicious than that. It's looking for the
resource at the correct place, but the error message was hard-coded and
incorrect. Furthermore, it doesn't necessarily look for the resource in
the hard-coded error message, and one of the ones it looks for was omitted
from daikon.jar.

I have updated the rules for making daikon.jar so that it includes all the
appropriate Simplify background files, and I have updated the error
message so that it indicates the actual resource if it was not found.
These fixes are pushed to the Daikon version control repository. They
will appear in the next release, but if you don't want to re-build Daikon
I can provide a daikon.jar file.

-Mike

Tanzeem Bin Noor

unread,
Dec 11, 2014, 12:10:06 AM12/11/14
to daikon-...@googlegroups.com, tanzee...@gmail.com, sm...@alum.mit.edu, mer...@cs.washington.edu
  
These fixes are pushed to the Daikon version control repository.  They
will appear in the next release, but if you don't want to re-build Daikon
I can provide a daikon.jar file.

Thanks Mike. It would be very helpful for me if you kindly provide me the fixed daikon.jar. Actually, I'm really stuck here for quite a long time. My research idea depends on this logical compare feature, if it works properly. So at first I need to be ensured regarding the output of this feature. 

I really appreciate your effort and kind consideration. 
--Tanzeem  


Tanzeem Bin Noor

unread,
Dec 11, 2014, 4:39:04 PM12/11/14
to daikon-...@googlegroups.com
I see my previous error "could not found the resource" is gone with the new daikon version, when I issue the logical compare command. However, I'm getting different errors for two different pair of invariant as follows.

Case 1: java daikon.tools.compare.LogicalCompare 00.inv.gz 01.inv.gz

Looking at simpleStack2Test.simpleStack2Test(java.lang.String):::ENTER
Invalid: arg0 has only one value
Invalid: arg0.toString == "testph1"
Exception in thread "main" java.lang.NullPointerException
at daikon.VarInfo.simplify_name(VarInfo.java:3209)
at daikon.VarInfo.simplify_name(VarInfo.java:3180)
at daikon.VarInfo.name_using(VarInfo.java:2933)
at daikon.inv.unary.string.OneOfString.format_simplify(OneOfString.java:409)
at daikon.inv.unary.string.OneOfString.format_using(OneOfString.java:230)
at daikon.simplify.InvariantLemma.<init>(InvariantLemma.java:17)
at daikon.simplify.InvariantLemma.makeLemmaAddOrig(InvariantLemma.java:65)
at daikon.tools.compare.LogicalCompare.translateAddOrig(LogicalCompare.java:215)
at daikon.tools.compare.LogicalCompare.comparePpts(LogicalCompare.java:490)
at daikon.tools.compare.LogicalCompare.mainHelper(LogicalCompare.java:798)
at daikon.tools.compare.LogicalCompare.main(LogicalCompare.java:574)


Case 2: java daikon.tools.compare.LogicalCompare 1.inv.gz 0.inv.gz

simpleStack2Test.testph1():::ENTER was used but not tested
Looking at simpleStack.isEmpty():::ENTER
Can't handle this.myArray[..] == orig(this.myArray[..]): format_simplify can't handle one of these sequences: this.myArray[..] == orig(this.myArray[..])
Can't handle this.myArray[..] == orig(this.myArray[..]): format_simplify can't handle one of these sequences: this.myArray[..] == orig(this.myArray[..])
For improved error reporting, try using --config_option daikon.simplify.LemmaStack.synchronous_errors=true
java.lang.Error: Simplify error: Bad input: Cannot use OR as a function symbol. on (OR)
at daikon.simplify.CmdCheck.apply(CmdCheck.java:65)
at daikon.simplify.SessionManager$Worker.run(SessionManager.java:198)
Exception in thread "main" daikon.simplify.SimplifyError: java.lang.Error: Simplify error: Bad input: Cannot use OR as a function symbol. on (OR)
at daikon.simplify.SessionManager.request(SessionManager.java:87)
at daikon.simplify.LemmaStack.checkString(LemmaStack.java:171)
at daikon.simplify.LemmaStack.checkForContradiction(LemmaStack.java:194)
at daikon.tools.compare.LogicalCompare.evaluateImplications(LogicalCompare.java:334)
at daikon.tools.compare.LogicalCompare.comparePpts(LogicalCompare.java:475)
at daikon.tools.compare.LogicalCompare.mainHelper(LogicalCompare.java:798)
at daikon.tools.compare.LogicalCompare.main(LogicalCompare.java:574)

I wonder, is there any problem regarding my trace files. Actually I've generated those from running junit and omitted the pattern for ^(org.| junit). But, the daikon.printInvariant, daikon.mergeInvariant commands work fine on these same invariant binaries.

Is daikon able to check (logicalCompare) any kind of invariants just as mine or is there any specific criteria for checking? What should be the outcome of logical compare? Is it kind of a boolean, i.e., whether one invariant holds the property of another invariant (those are to be checked by logical compare)?

Thanks.

Michael Ernst

unread,
Dec 12, 2014, 1:02:20 AM12/12/14
to daikon-discuss, Tanzeem Bin Noor
Tanzeem-

We cannot diagnose nor debug your problem without you including all the
files that are necessary to reproduce it. (In a private communication, I
asked you for the .dtrace files and for the exact commands you ran to
create the .inv files, but you have not included them.)

-Mike


> Subject: Re: Need to use Logical Compare feature of Daikon
> From: Tanzeem Bin Noor <tanzee...@gmail.com>
> To: daikon-...@googlegroups.com
> Date: Thu, 11 Dec 2014 13:39:04 -0800 (PST)
> --
> 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.
> For more options, visit https://groups.google.com/d/optout.

Tanzeem Bin Noor

unread,
Dec 12, 2014, 12:59:30 PM12/12/14
to daikon-...@googlegroups.com, tanzee...@gmail.com, mer...@cs.washington.edu


We cannot diagnose nor debug your problem without you including all the
files that are necessary to reproduce it.  (In a private communication, I
asked you for the .dtrace files and for the exact commands you ran to
create the .inv files, but you have not included them.)


Hi Mike,

Sorry about that. Just forgot to add the .dtrace files. Here, I've attached the corresponding .dtrace file. The steps to reproduce the errors are as follows:

1. gzip 0.dtrace ; gzip 1.dtrace ; gzip 00.dtrace ; gzip 01.dtrace ;  (This will generate 0.dtrace.gz ; 1.dtrace.gz; 00.dtrace.gz; 01.dtrace.gz; respectively)
2  java daikon.Daikon 0.dtrace.gz; java daikon.Daikon 1.dtrace.gz; java daikon.Daikon 00.dtrace.gz; java daikon.Daikon 01.dtrace.gz; (This will generate the corresponding .inv files, e.g., 0.inv.gz, 1.inv.gz, 00.inv.gz, 01.inv.gz)

3. java daikon.tools.compare.LogicalCompare 00.inv.gz 01.inv.gz

Error:

Looking at simpleStack2Test.simpleStack2Test(java.lang.String):::ENTER
Invalid: arg0 has only one value
Invalid: arg0.toString == "testph1"
Exception in thread "main" java.lang.NullPointerException
    at daikon.VarInfo.simplify_name(VarInfo.java:3209)
    at daikon.VarInfo.simplify_name(VarInfo.java:3180)
    at daikon.VarInfo.name_using(VarInfo.java:2933)
    at daikon.inv.unary.string.OneOfString.format_simplify(OneOfString.java:409)
    at daikon.inv.unary.string.OneOfString.format_using(OneOfString.java:230)
    at daikon.simplify.InvariantLemma.<init>(InvariantLemma.java:17)
    at daikon.simplify.InvariantLemma.makeLemmaAddOrig(InvariantLemma.java:65)
    at daikon.tools.compare.LogicalCompare.translateAddOrig(LogicalCompare.java:215)
    at daikon.tools.compare.LogicalCompare.comparePpts(LogicalCompare.java:490)
    at daikon.tools.compare.LogicalCompare.mainHelper(LogicalCompare.java:798)
    at daikon.tools.compare.LogicalCompare.main(LogicalCompare.java:574)

4. java daikon.tools.compare.LogicalCompare 1.inv.gz 0.inv.gz

Error:


simpleStack2Test.testph1():::ENTER was used but not tested
Looking at simpleStack.isEmpty():::ENTER
Can't handle this.myArray[..] == orig(this.myArray[..]): format_simplify can't handle one of these sequences: this.myArray[..] == orig(this.myArray[..])
Can't handle this.myArray[..] == orig(this.myArray[..]): format_simplify can't handle one of these sequences: this.myArray[..] == orig(this.myArray[..])
For improved error reporting, try using --config_option daikon.simplify.LemmaStack.synchronous_errors=true
java.lang.Error: Simplify error: Bad input: Cannot use OR as a function symbol. on (OR)
    at daikon.simplify.CmdCheck.apply(CmdCheck.java:65)
    at daikon.simplify.SessionManager$Worker.run(SessionManager.java:198)
Exception in thread "main" daikon.simplify.SimplifyError: java.lang.Error: Simplify error: Bad input: Cannot use OR as a function symbol. on (OR)
    at daikon.simplify.SessionManager.request(SessionManager.java:87)
    at daikon.simplify.LemmaStack.checkString(LemmaStack.java:171)
    at daikon.simplify.LemmaStack.checkForContradiction(LemmaStack.java:194)
    at daikon.tools.compare.LogicalCompare.evaluateImplications(LogicalCompare.java:334)
    at daikon.tools.compare.LogicalCompare.comparePpts(LogicalCompare.java:475)
    at daikon.tools.compare.LogicalCompare.mainHelper(LogicalCompare.java:798)
    at daikon.tools.compare.LogicalCompare.main(LogicalCompare.java:574)
 
This is to mention that I've generated the .dtrace files using daikon.Chicory and then kept only related program point along with their declarations and parents declaration if any. I can run "java daikon.PrintInvariant 0.inv.gz" and same as on other .inv files. Similarly, I can run "java daikon.MergeInvariants 0.inv.gz 1.inv.gz" and same as on other pair.

Is there any problem with the .dtrace file? I thought they are valid as they work fine on other commands (PrintInvariant, MergeInvariants).

Thanks.
--Tanzeem


 
00.dtrace
01.dtrace
0.dtrace
1.dtrace
Reply all
Reply to author
Forward
0 new messages