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.

Sign up for GitHub

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

Jump to bottom

Run crucible-jvm tests on CI #634

Open
RyanGlScott opened this issue Feb 2, 2021 · 2 comments
Open

Run crucible-jvm tests on CI #634

RyanGlScott opened this issue Feb 2, 2021 · 2 comments
Labels
CI crux jvm testing

Comments

@RyanGlScott
Copy link
Contributor

Currently, the tests.sh script associated with crucible-jvm is not run on CI, which leaves it susceptible to bitrotting. Indeed, it's not surprising that's it isn't ran on CI at the moment, as it hardcodes the location of rt.jar:

crucible/crucible-jvm/tests/test.sh

Line 3 in 91236c3

RTJAR=/Library/Java/JavaVirtualMachines/jdk1.8.0_171.jdk/Contents/Home/jre/lib/rt.jar

We should fix this and make sure that CI is capable of running this.
@RyanGlScott
Copy link
Contributor Author

RyanGlScott commented Feb 2, 2021 •
edited
Loading

It looks like the ashes test suite under crucible-jvm/tests/ashes (which also leverages crucible-jvm) isn't ran on CI either.

@RyanGlScott
Copy link
Contributor Author

Getting ashes to work at all (let alone on CI) will likely be more challenging, as it doesn't appear to mesh well with how Crux currently dumps information to the terminal:

$ ./runAshes.hs 
kaffeRegressionSuite/benchmarks/str                        Unexpect Fail
Expected:
12abcd34567890
Got:
[Crux] Checking "Str.java"
12abcd78345678
[Crux] Simulation complete.
[Crux] All goals discharged through internal simplification.
[Crux] Overall status: Valid.
initializeClass java/lang/String  (start)
initializeClass java/lang/Object  (start)
special java/lang/Object/<clinit>
initializeClass java/lang/Object  (finish)
special java/lang/String/<clinit>
initializeClass java/lang/String  (finish)
new ClassName "java/lang/StringBuffer" (start)
new ClassName "java/lang/StringBuffer" (finish)
initializeClass java/lang/StringBuffer  (start)
initializeClass java/lang/AbstractStringBuilder  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/AbstractStringBuilder  (finish)
special java/lang/StringBuffer/<clinit>
initializeClass java/lang/StringBuffer  (finish)
initializeClass java/lang/String  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/String  (finish)
invoke: java/lang/StringBuffer/insert
finish invoke:java/lang/StringBuffer/insert
initializeClass java/lang/System  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
Initializing System.out static field
Finished initializing System.out
Initializing System.err static field
Finished initializing System.err
initializeClass java/lang/System  (finish)
invoke: java/io/PrintStream/println
finish invoke:java/io/PrintStream/println
invoke: java/lang/String/length
finish invoke:java/lang/String/length
initializeClass java/lang/AbstractStringBuilder  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/AbstractStringBuilder  (finish)
invoke: java/lang/StringBuffer/append
finish invoke:java/lang/StringBuffer/append
getfield "java/lang/String.value"
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
putfield "java/lang/AbstractStringBuilder.value"
putfield "java/lang/StringBuffer.toStringCache"
initializeClass java/lang/AbstractStringBuilder  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/AbstractStringBuilder  (finish)
invoke: java/lang/String/length
finish invoke:java/lang/String/length
getfield "java/lang/AbstractStringBuilder.count"
initializeClass java/lang/AbstractStringBuilder  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/AbstractStringBuilder  (finish)
getfield "java/lang/AbstractStringBuilder.value"
getfield "java/lang/AbstractStringBuilder.count"
invoke: java/lang/String/getChars
finish invoke:java/lang/String/getChars
getfield "java/lang/AbstractStringBuilder.count"
putfield "java/lang/AbstractStringBuilder.count"
initializeClass java/lang/AbstractStringBuilder  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/AbstractStringBuilder  (finish)
getfield "java/lang/AbstractStringBuilder.value"
getfield "java/lang/AbstractStringBuilder.value"
initializeClass java/lang/AbstractStringBuilder  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/AbstractStringBuilder  (finish)
initializeClass java/util/Arrays  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
special java/lang/Arrays/<clinit>
initializeClass java/util/Arrays  (finish)
putfield "java/lang/AbstractStringBuilder.value"
getfield "java/lang/String.value"
getfield "java/lang/String.value"
invoke static: java/lang/System/arraycopy
new ClassName "java/lang/StringIndexOutOfBoundsException" (start)
new ClassName "java/lang/StringIndexOutOfBoundsException" (finish)
initializeClass java/lang/StringIndexOutOfBoundsException  (start)
initializeClass java/lang/IndexOutOfBoundsException  (start)
initializeClass java/lang/RuntimeException  (start)
initializeClass java/lang/Exception  (start)
initializeClass java/lang/Throwable  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/String  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/String  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Throwable  (finish)
initializeClass java/lang/Exception  (finish)
initializeClass java/lang/RuntimeException  (finish)
initializeClass java/lang/IndexOutOfBoundsException  (finish)
initializeClass java/lang/StringIndexOutOfBoundsException  (finish)
new ClassName "java/lang/StringIndexOutOfBoundsException" (start)
new ClassName "java/lang/StringIndexOutOfBoundsException" (finish)
initializeClass java/lang/StringIndexOutOfBoundsException  (start)
initializeClass java/lang/IndexOutOfBoundsException  (start)
initializeClass java/lang/RuntimeException  (start)
initializeClass java/lang/Exception  (start)
initializeClass java/lang/Throwable  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Throwable  (finish)
initializeClass java/lang/Exception  (finish)
initializeClass java/lang/RuntimeException  (finish)
initializeClass java/lang/IndexOutOfBoundsException  (finish)
initializeClass java/lang/StringIndexOutOfBoundsException  (finish)
new ClassName "java/lang/StringIndexOutOfBoundsException" (start)
new ClassName "java/lang/StringIndexOutOfBoundsException" (finish)
initializeClass java/lang/StringIndexOutOfBoundsException  (start)
initializeClass java/lang/IndexOutOfBoundsException  (start)
initializeClass java/lang/RuntimeException  (start)
initializeClass java/lang/Exception  (start)
initializeClass java/lang/Throwable  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Throwable  (finish)
initializeClass java/lang/Exception  (finish)
initializeClass java/lang/RuntimeException  (finish)
initializeClass java/lang/IndexOutOfBoundsException  (finish)
initializeClass java/lang/StringIndexOutOfBoundsException  (finish)
putfield "java/lang/StringBuffer.toStringCache"
initializeClass java/lang/AbstractStringBuilder  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/AbstractStringBuilder  (finish)
new ClassName "java/lang/StringIndexOutOfBoundsException" (start)
new ClassName "java/lang/StringIndexOutOfBoundsException" (finish)
initializeClass java/lang/StringIndexOutOfBoundsException  (start)
initializeClass java/lang/IndexOutOfBoundsException  (start)
initializeClass java/lang/RuntimeException  (start)
initializeClass java/lang/Exception  (start)
initializeClass java/lang/Throwable  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/Throwable  (finish)
initializeClass java/lang/Exception  (finish)
initializeClass java/lang/RuntimeException  (finish)
initializeClass java/lang/IndexOutOfBoundsException  (finish)
initializeClass java/lang/StringIndexOutOfBoundsException  (finish)
invoke: java/lang/AbstractStringBuilder/length
finish invoke:java/lang/AbstractStringBuilder/length
invoke: java/lang/String/length
finish invoke:java/lang/String/length
getfield "java/lang/AbstractStringBuilder.count"
initializeClass java/lang/AbstractStringBuilder  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/AbstractStringBuilder  (finish)
getfield "java/lang/AbstractStringBuilder.value"
getfield "java/lang/AbstractStringBuilder.value"
getfield "java/lang/AbstractStringBuilder.count"
invoke static: java/lang/System/arraycopy
getfield "java/lang/AbstractStringBuilder.value"
invoke: java/lang/String/getChars
finish invoke:java/lang/String/getChars
getfield "java/lang/AbstractStringBuilder.count"
putfield "java/lang/AbstractStringBuilder.count"
initializeClass java/lang/String  (start)
initializeClass java/lang/Object  (start)
initializeClass java/lang/Object  (finish)
initializeClass java/lang/String  (finish)
getfield "java/lang/StringBuffer.count"
getfield "java/lang/String.value"
getfield "java/lang/String.value"
invoke static: java/lang/System/arraycopy
Exit code = ExitSuccess
Failed

If I change the verbosity from 2 to 0, it instead fails with:

$ ./runAshes.hs   
kaffeRegressionSuite/benchmarks/str                        Unexpect Fail
Expected:
12abcd34567890
Got:
12abcd78345678
[Crux] All goals discharged through internal simplification.
[Crux] Overall status: Valid.
Exit code = ExitSuccess
Failed

@RyanGlScott RyanGlScott mentioned this issue Feb 2, 2021
Merged
RyanGlScott added a commit that referenced this issue Feb 3, 2021
@RyanGlScott
crucible-jvm: Add --java-bin-dirs
bd2ed44 
This mirrors a similar recent change introduced to SAW in
GaloisInc/saw-script#1030.

While I was in town, I updated the two `crucible-jvm`–related test suites
to use the `PATH` instead of the `-j` flag. I can't exactly confirm via CI
if these changes work (see #634), but they appear to do the right thing
locally.

Fixes #633.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this issue Feb 5, 2021
@RyanGlScott
WIP: Support JDK 9 or later
d6eae5e 
This allows SAW to deal with JDK 9 or later, which packages its standard
library not in a JAR file, but in a JIMAGE file. This leverages `crucible-jvm`
changes from GaloisInc/crucible#634.

This fixes #861.

Other things:

* I removed the dependency on the `xdg-basedir`, as it was unused. This
  dependency was likely added quite some time ago, and it appears that
  `saw-script` switched over to using XDG-related functionality from the
  `directory` library since then. I opted to use `directory` to find the
  `.cache` directory as well, so I have made that clear in the `.cabal` file.

* The `biJavaCodebase :: Codebase` field of `BuiltinContext` is completely
  unused, which I noticed when making changes to the `Codebase` type. Let's
  just remove it. This fixes #1003.
@RyanGlScott RyanGlScott mentioned this issue Feb 5, 2021
Merged
RyanGlScott added a commit to GaloisInc/saw-script that referenced this issue Feb 5, 2021
@RyanGlScott
WIP: Support JDK 9 or later
30c9bb9 
This allows SAW to deal with JDK 9 or later, which packages its standard
library not in a JAR file, but in a JIMAGE file. This leverages `crucible-jvm`
changes from GaloisInc/crucible#634.

This fixes #861.

Other things:

* I removed the dependency on the `xdg-basedir`, as it was unused. This
  dependency was likely added quite some time ago, and it appears that
  `saw-script` switched over to using XDG-related functionality from the
  `directory` library since then. I opted to use `directory` to find the
  `.cache` directory as well, so I have made that clear in the `.cabal` file.

* The `biJavaCodebase :: Codebase` field of `BuiltinContext` is completely
  unused, which I noticed when making changes to the `Codebase` type. Let's
  just remove it.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this issue Feb 5, 2021
@RyanGlScott
WIP: Support JDK 9 or later
b21344b 
This allows SAW to deal with JDK 9 or later, which packages its standard
library not in a JAR file, but in a JIMAGE file. This leverages `crucible-jvm`
changes from GaloisInc/crucible#634.

This fixes #861.

Other things:

* I removed the dependency on the `xdg-basedir`, as it was unused. This
  dependency was likely added quite some time ago, and it appears that
  `saw-script` switched over to using XDG-related functionality from the
  `directory` library since then. I opted to use `directory` to find the
  `.cache` directory as well, so I have made that clear in the `.cabal` file.

* The `biJavaCodebase :: Codebase` field of `BuiltinContext` is completely
  unused, which I noticed when making changes to the `Codebase` type. Let's
  just remove it.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this issue Feb 5, 2021
@RyanGlScott
WIP: Support JDK 9 or later
decacf0 
This allows SAW to deal with JDK 9 or later, which packages its standard
library not in a JAR file, but in a JIMAGE file. This leverages `crucible-jvm`
changes from GaloisInc/crucible#634.

This fixes #861.

Other things:

* I removed the dependency on the `xdg-basedir`, as it was unused. This
  dependency was likely added quite some time ago, and it appears that
  `saw-script` switched over to using XDG-related functionality from the
  `directory` library since then. I opted to use `directory` to find the
  `.cache` directory as well, so I have made that clear in the `.cabal` file.

* The `biJavaCodebase :: Codebase` field of `BuiltinContext` is completely
  unused, which I noticed when making changes to the `Codebase` type. Let's
  just remove it.
@atomb atomb self-assigned this Mar 12, 2021
@atomb atomb added the CI label Apr 9, 2021
@atomb atomb added this to the Crux 0.5 milestone May 21, 2021
@RyanGlScott RyanGlScott mentioned this issue Sep 7, 2021
Open
@atomb atomb removed this from the Crux 0.5 milestone Sep 14, 2021
@atomb atomb removed their assignment Oct 19, 2021
@RyanGlScott RyanGlScott mentioned this issue Oct 29, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
CI crux jvm testing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@atomb @RyanGlScott