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

Bump submodules. #2011

Merged
merged 6 commits into from
Jan 17, 2024
Merged

Bump submodules. #2011

merged 6 commits into from
Jan 17, 2024

Conversation

andreistefanescu
Copy link
Contributor

No description provided.

deps/cryptol-specs Outdated Show resolved Hide resolved
heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs Outdated Show resolved Hide resolved
@RyanGlScott
Copy link
Contributor

Some integration tests are failing due to some files moving around a bit in GaloisInc/cryptol-specs#67, e.g.,

  test0001:                            [23:31:28.921] Loading file "/home/runner/work/saw-script/saw-script/intTests/test0001/javamd5test.saw"
[23:31:28.936] Stack trace:
Cryptol error:
Error:  can't find file: MD5.cry


FAIL (0.92s)
    intTests/IntegrationTest.hs:172:
    expected: ExitSuccess
     but got: ExitFailure 2
    Use -p '/test0001/' to rerun this test only.

That is likely failing since MD5.cry was moved to MD5.md, as it is now a literate Cryptol file. Similarly for the other failures. My hope is that these errors are easily fixed by changing some import lines.

@@ -1,3 +1,4 @@
import "../../deps/cryptol-specs/Common/GF28.cry";
Copy link
Contributor Author

Choose a reason for hiding this comment

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

@RyanGlScott @qsctr is this expected? This is the error without the explicit import:

Cryptol error:
Error:  Could not find module Common::GF28
Searched paths:
    ../../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block
    /home/runner/work/saw-script/saw-script/dist/lib
    /home/runner/work/saw-script/saw-script/examples/aes
    /home/runner/work/saw-script/saw-script/intTests/.cryptol
    /home/runner/work/saw-script/saw-script/dist/share/cryptol
Set the CRYPTOLPATH environment variable to search more directories

it seems that the issue is that Common::GF28 is relative to Primitive::Symmetric::Cipher::Block::AES, not absolute, I'm not sure

Copy link
Contributor

Choose a reason for hiding this comment

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

GaloisInc/cryptol-specs#67 moved the location of Common::GF28 within the cryptol-specs repo. Previously, it was located at Primitive/Symmetric/Cipher/Block/AES/GF28.cry, so the import "../../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block/AES.cry" line would be enough to find it. After GaloisInc/cryptol-specs#67, however, Common::GF28 is now located at Common/GF28.cry (it is now used by other things in cryptol-specs besides AES), so you have to explicitly indicate this.

@andreistefanescu
Copy link
Contributor Author

I'm splitting the cryptol-specs bump, as it causes a timeout in intTests/test0001/javamd5test.saw.

@andreistefanescu andreistefanescu merged commit 0a8fdf5 into master Jan 17, 2024
38 checks passed
@andreistefanescu andreistefanescu deleted the bump-submodules branch January 17, 2024 19:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants