search

maude-lang / Maude

Language based on Rewriting Logic
GNU General Public License v2.0
78 stars 10 forks source link

Maude 3.2.1 test failure in Arch Linux #2

Closed felixonmars closed 1 year ago

felixonmars commented 2 years ago 
============================================
   Maude 3.2.1: tests/Misc/test-suite.log
============================================

# TOTAL: 35
# PASS:  34
# SKIP:  0
# XFAIL: 0
# FAIL:  1
# XPASS: 0
# ERROR: 0

.. contents:: :depth: 2

FAIL: fileTest
==============

Maude 3.1 in the same environment passes all tests (this particular test cause seems to be new in 3.2, though).

stevenmeker commented 2 years ago

Maude 3.2.1 passes this test under Ubuntu and I don't have an Arch Linux machine to hand. Can you provide the tests/Misc/fileTest.out file generated by this failing test?

felixonmars commented 2 years ago

Sure. Uploaded at: https://paste.xinu.at/6RL/

Looks like the test files are missing?

Also attaching a diff:

--- src/Maude-3.2.1/tests/Misc/fileTest.expected        2022-02-22 04:55:35.000000000 +0200
+++ src/Maude-3.2.1/tests/Misc/fileTest.out     2022-02-23 20:02:07.020720632 +0200
@@ -12,71 +12,73 @@
     "No such file or directory")
 ==========================================
 erewrite in FILE-TEST2 : run .
-rewrites: 2
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
-    "Bad size.")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST3 : run .
-rewrites: 2
-result Configuration: <> < me : myClass | none > gotChars(me, file(3), "***\n***\tTest file operations and error handling.\n***\n\nset show timing off .\n\nload file\n\nmod FILE-TEST1 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op badName : -> String .\nendm\n\nerew <> < me : myClass | none > openFile(fileManager, me, badName, \"r\") .\nerew <> < me : myClass | none > openFile(fileManager, me, \"/shouldNotExist\", \"r\") .\n\n\nmod FILE-TEST2 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op run : -> Configuration .\n  op badNat : -> Nat .\nvars O O2 F : Oid .\n\n  eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n  rl < O : myClass | none > openedFile(O, O2, F) =>\n     < O : myClass | none > getChars(F, O, badNat) .\nendm\n\nerew run .\n\n\nmod FILE-TEST3 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op run : -> Configuration .\nvars O O2 F : Oid .\n\n  eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n  rl < O : myClass | none > ")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST4 : run .
-rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
-    "Bad offset.")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST5 : run .
-rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
-    "Bad offset.")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST6 : run .
-rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
-    "Bad offset.")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST7 : run .
-rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
-    "Bad base.")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST8 : run .
-rewrites: 4
-result Configuration: <> < me : myClass | state(1) > gotChars(me, file(3), "T1 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op badName : -> String .\nendm\n\nerew ")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST9 : run .
-rewrites: 5
-result Configuration: <> < me : myClass | state(1) > positionGot(me, file(3),
-    200)
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST10 : run .
-rewrites: 2
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
-    "File not open for writing.")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST11 : run .
-rewrites: 2
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
-    "File not open for writing.")
+rewrites: 1
+result Configuration: <> < me : myClass | none > fileError(me, fileManager,
+    "No such file or directory")
 ==========================================
 erewrite in FILE-TEST12 : run .
 rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "File not open for reading.")
 ==========================================
 erewrite in FILE-TEST13 : run .
 rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "File not open for reading.")
 ==========================================
 erewrite in FILE-TEST14 : run .
 rewrites: 4
-result Configuration: <> < me : myClass | none > gotLine(me, file(3),
+result Configuration: <> < me : myClass | none > gotLine(me, file(6),
     "testing testing 1 2 3\n")
 ==========================================
 erewrite in FILE-TEST15 : run .
 rewrites: 5
-result Configuration: <> closedFile(me, file(3)) < me : myClass | none >
+result Configuration: <> closedFile(me, file(6)) < me : myClass | none >
 ==========================================
 erewrite in FILE-TEST15 : <> < me : myClass | none > removeFile(fileManager,
     me, "fileTest.tmp") .
stevenmeker commented 2 years ago

The errors arise because Maude cannot open the test file itself:

"../../../tests/Misc/fileTest.maude"

This is probably because the binary isn't where it expects to be relative to the test directory. Perhaps because Maude is being built in the source directory rather than a build subdirectory.

felixonmars commented 2 years ago

Thanks. I have tried to run the build in a build subdir. This particular test still fails, but with a different diff now:

--- src/Maude-3.2.1/tests/Misc/fileTest.expected        2022-02-22 04:55:35.000000000 +0200
+++ src/Maude-3.2.1/build/tests/Misc/fileTest.out       2022-02-23 22:53:43.405763431 +0200
@@ -13,70 +13,70 @@
 ==========================================
 erewrite in FILE-TEST2 : run .
 rewrites: 2
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "Bad size.")
 ==========================================
 erewrite in FILE-TEST3 : run .
 rewrites: 2
-result Configuration: <> < me : myClass | none > gotChars(me, file(3), "***\n***\tTest file operations and error handling.\n***\n\nset show timing off .\n\nload file\n\nmod FILE-TEST1 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op badName : -> String .\nendm\n\nerew <> < me : myClass | none > openFile(fileManager, me, badName, \"r\") .\nerew <> < me : myClass | none > openFile(fileManager, me, \"/shouldNotExist\", \"r\") .\n\n\nmod FILE-TEST2 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op run : -> Configuration .\n  op badNat : -> Nat .\nvars O O2 F : Oid .\n\n  eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n  rl < O : myClass | none > openedFile(O, O2, F) =>\n     < O : myClass | none > getChars(F, O, badNat) .\nendm\n\nerew run .\n\n\nmod FILE-TEST3 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op run : -> Configuration .\nvars O O2 F : Oid .\n\n  eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n  rl < O : myClass | none > ")
+result Configuration: <> < me : myClass | none > gotChars(me, file(6), "***\n***\tTest file operations and error handling.\n***\n\nset show timing off .\n\nload file\n\nmod FILE-TEST1 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op badName : -> String .\nendm\n\nerew <> < me : myClass | none > openFile(fileManager, me, badName, \"r\") .\nerew <> < me : myClass | none > openFile(fileManager, me, \"/shouldNotExist\", \"r\") .\n\n\nmod FILE-TEST2 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op run : -> Configuration .\n  op badNat : -> Nat .\nvars O O2 F : Oid .\n\n  eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n  rl < O : myClass | none > openedFile(O, O2, F) =>\n     < O : myClass | none > getChars(F, O, badNat) .\nendm\n\nerew run .\n\n\nmod FILE-TEST3 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op run : -> Configuration .\nvars O O2 F : Oid .\n\n  eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n  rl < O : myClass | none > ")
 ==========================================
 erewrite in FILE-TEST4 : run .
 rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "Bad offset.")
 ==========================================
 erewrite in FILE-TEST5 : run .
 rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "Bad offset.")
 ==========================================
 erewrite in FILE-TEST6 : run .
 rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "Bad offset.")
 ==========================================
 erewrite in FILE-TEST7 : run .
 rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "Bad base.")
 ==========================================
 erewrite in FILE-TEST8 : run .
 rewrites: 4
-result Configuration: <> < me : myClass | state(1) > gotChars(me, file(3), "T1 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op badName : -> String .\nendm\n\nerew ")
+result Configuration: <> < me : myClass | state(1) > gotChars(me, file(6), "T1 is\n  pr FILE .\n  op myClass : -> Cid .\n  ops me : -> Oid .\n  op badName : -> String .\nendm\n\nerew ")
 ==========================================
 erewrite in FILE-TEST9 : run .
 rewrites: 5
-result Configuration: <> < me : myClass | state(1) > positionGot(me, file(3),
+result Configuration: <> < me : myClass | state(1) > positionGot(me, file(6),
     200)
 ==========================================
 erewrite in FILE-TEST10 : run .
 rewrites: 2
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "File not open for writing.")
 ==========================================
 erewrite in FILE-TEST11 : run .
 rewrites: 2
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "File not open for writing.")
 ==========================================
 erewrite in FILE-TEST12 : run .
 rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "File not open for reading.")
 ==========================================
 erewrite in FILE-TEST13 : run .
 rewrites: 3
-result Configuration: <> < me : myClass | none > fileError(me, file(3),
+result Configuration: <> < me : myClass | none > fileError(me, file(6),
     "File not open for reading.")
 ==========================================
 erewrite in FILE-TEST14 : run .
 rewrites: 4
-result Configuration: <> < me : myClass | none > gotLine(me, file(3),
+result Configuration: <> < me : myClass | none > gotLine(me, file(6),
     "testing testing 1 2 3\n")
 ==========================================
 erewrite in FILE-TEST15 : run .
 rewrites: 5
-result Configuration: <> closedFile(me, file(3)) < me : myClass | none >
+result Configuration: <> closedFile(me, file(6)) < me : myClass | none >
 ==========================================
 erewrite in FILE-TEST15 : <> < me : myClass | none > removeFile(fileManager,
     me, "fileTest.tmp") .
stevenmeker commented 2 years ago

The only difference now is the file handle being returned by the OS for opening the file - 3 is expected but 6 is being returned. I thought it might be a bug in Maude, failing to clean up and release old file descriptors but it arises in FILE-TEST2, the first test that successfully opens a file, and the same descriptor is returned in all the other tests. This leads me to believe that Arch Linux returns file descriptors starting at 6 rather than 3 for opening files. Do you happen to know if it reserves descriptors 3, 4 and 5 in the same way that 0, 1 and 2 are reserved for standard I/O?

ningit commented 2 years ago

I can reproduce the issue in Arch, although with file(4) instead of file(3) or file(6) in my setting. The file descriptor 3 is occupied by /dev/tty, which has been opened in the static initialization function of the CLN library (a dependency of CVC4). It is used as an output stream for debugging (see here).

The problem does not appear when building with Yices2 instead of CVC4. If the particular file descriptor number does not matter and since it seems to depend on some uncontrollable environmental conditions, the following could be used

set print conceal on .
print conceal file .

and file(...) would be shown instead of that number. There is a patch for this test below.

Patch ```diff --- a/tests/Misc/fileTest.maude +++ b/tests/Misc/fileTest.maude @@ -3,6 +3,8 @@ *** set show timing off . +set print conceal on . +print conceal file . load file --- a/tests/Misc/fileTest.expected +++ b/tests/Misc/fileTest.expected @@ -13,70 +13,70 @@ ========================================== erewrite in FILE-TEST2 : run . rewrites: 2 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "Bad size.") ========================================== erewrite in FILE-TEST3 : run . rewrites: 2 -result Configuration: <> < me : myClass | none > gotChars(me, file(3), "***\n***\tTest file operations and error handling.\n***\n\nset show timing off .\n\nload file\n\nmod FILE-TEST1 is\n pr FILE .\n op myClass : -> Cid .\n ops me : -> Oid .\n op badName : -> String .\nendm\n\nerew <> < me : myClass | none > openFile(fileManager, me, badName, \"r\") .\nerew <> < me : myClass | none > openFile(fileManager, me, \"/shouldNotExist\", \"r\") .\n\n\nmod FILE-TEST2 is\n pr FILE .\n op myClass : -> Cid .\n ops me : -> Oid .\n op run : -> Configuration .\n op badNat : -> Nat .\nvars O O2 F : Oid .\n\n eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n rl < O : myClass | none > openedFile(O, O2, F) =>\n < O : myClass | none > getChars(F, O, badNat) .\nendm\n\nerew run .\n\n\nmod FILE-TEST3 is\n pr FILE .\n op myClass : -> Cid .\n ops me : -> Oid .\n op run : -> Configuration .\nvars O O2 F : Oid .\n\n eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n rl < O : myClass | none > ") +result Configuration: <> < me : myClass | none > gotChars(me, file(...), "***\n***\tTest file operations and error handling.\n***\n\nset show timing off .\nset print conceal on .\nprint conceal file .\n\nload file\n\nmod FILE-TEST1 is\n pr FILE .\n op myClass : -> Cid .\n ops me : -> Oid .\n op badName : -> String .\nendm\n\nerew <> < me : myClass | none > openFile(fileManager, me, badName, \"r\") .\nerew <> < me : myClass | none > openFile(fileManager, me, \"/shouldNotExist\", \"r\") .\n\n\nmod FILE-TEST2 is\n pr FILE .\n op myClass : -> Cid .\n ops me : -> Oid .\n op run : -> Configuration .\n op badNat : -> Nat .\nvars O O2 F : Oid .\n\n eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.maude\", \"r\") .\n\n rl < O : myClass | none > openedFile(O, O2, F) =>\n < O : myClass | none > getChars(F, O, badNat) .\nendm\n\nerew run .\n\n\nmod FILE-TEST3 is\n pr FILE .\n op myClass : -> Cid .\n ops me : -> Oid .\n op run : -> Configuration .\nvars O O2 F : Oid .\n\n eq run = <> < me : myClass | none > openFile(fileManager, me, \"../../../tests/Misc/fileTest.") ========================================== erewrite in FILE-TEST4 : run . rewrites: 3 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "Bad offset.") ========================================== erewrite in FILE-TEST5 : run . rewrites: 3 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "Bad offset.") ========================================== erewrite in FILE-TEST6 : run . rewrites: 3 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "Bad offset.") ========================================== erewrite in FILE-TEST7 : run . rewrites: 3 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "Bad base.") ========================================== erewrite in FILE-TEST8 : run . rewrites: 4 -result Configuration: <> < me : myClass | state(1) > gotChars(me, file(3), "T1 is\n pr FILE .\n op myClass : -> Cid .\n ops me : -> Oid .\n op badName : -> String .\nendm\n\nerew ") +result Configuration: <> < me : myClass | state(1) > gotChars(me, file(...), "rint conceal file .\n\nload file\n\nmod FILE-TEST1 is\n pr FILE .\n op myClass : -> Cid .\n ops me : -> ") ========================================== erewrite in FILE-TEST9 : run . rewrites: 5 -result Configuration: <> < me : myClass | state(1) > positionGot(me, file(3), +result Configuration: <> < me : myClass | state(1) > positionGot(me, file(...), 200) ========================================== erewrite in FILE-TEST10 : run . rewrites: 2 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "File not open for writing.") ========================================== erewrite in FILE-TEST11 : run . rewrites: 2 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "File not open for writing.") ========================================== erewrite in FILE-TEST12 : run . rewrites: 3 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "File not open for reading.") ========================================== erewrite in FILE-TEST13 : run . rewrites: 3 -result Configuration: <> < me : myClass | none > fileError(me, file(3), +result Configuration: <> < me : myClass | none > fileError(me, file(...), "File not open for reading.") ========================================== erewrite in FILE-TEST14 : run . rewrites: 4 -result Configuration: <> < me : myClass | none > gotLine(me, file(3), +result Configuration: <> < me : myClass | none > gotLine(me, file(...), "testing testing 1 2 3\n") ========================================== erewrite in FILE-TEST15 : run . rewrites: 5 -result Configuration: <> closedFile(me, file(3)) < me : myClass | none > +result Configuration: <> closedFile(me, file(...)) < me : myClass | none > ========================================== erewrite in FILE-TEST15 : <> < me : myClass | none > removeFile(fileManager, me, "fileTest.tmp") . ```
felixonmars commented 2 years ago

Ah, that makes a lot of sense. I have both CVC4 and Yices2 enabled.

peti commented 2 years ago

For what it's worth, I ran into the same test failure trying to update maude in NixOS. We are building the package with Yices enabled.

stevenmeker commented 1 year ago

The Mar 2 patch from ningit is now incorporated in Maude 3.2.2.

felixonmars commented 1 year ago

Thanks. Confirmed that it's fixed now in 3.2.2.