From 276a1bfcec218de2e4a88934fff9ffbf6dc354ad Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 22 Aug 2023 20:46:10 -0700 Subject: [PATCH 1/3] Add ogFromParam when importing Cryptol names --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 3deafd0a90..8c05177e85 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -72,7 +72,7 @@ import qualified Cryptol.Utils.Ident as C ( Ident, PrimIdent(..), mkIdent , prelPrim, floatPrim, arrayPrim, suiteBPrim, primeECPrim , ModName, modNameToText, identText, interactiveName - , ModPath(..), modPathSplit, ogModule, Namespace(NSValue) + , ModPath(..), modPathSplit, ogModule, ogFromParam, Namespace(NSValue) , modNameChunksText ) import qualified Cryptol.Utils.RecordMap as C @@ -1375,10 +1375,14 @@ importName cnm = let (topMod, nested) = C.modPathSplit (C.ogModule og) topChunks = C.modNameChunksText topMod modNms = topChunks ++ map C.identText nested + ifaceNms = case C.ogFromParam og of + Just i -> [C.identText i] + Nothing -> [] shortNm = C.identText (C.nameIdent cnm) - longNm = Text.intercalate "::" (modNms ++ [shortNm]) + nmParts = modNms ++ ifaceNms ++ [shortNm] + longNm = Text.intercalate "::" nmParts aliases = [shortNm, longNm] - uri = cryptolURI (modNms ++ [shortNm]) Nothing + uri = cryptolURI nmParts Nothing in pure (ImportedName uri aliases) -- | Currently this imports declaration groups by inlining all the From a69cae0f6b290724978dc1585ab586925a43c971 Mon Sep 17 00:00:00 2001 From: Bretton Date: Wed, 23 Aug 2023 14:54:09 -0700 Subject: [PATCH 2/3] Add integration test for #1892 --- intTests/test1892/A.cry | 3 +++ intTests/test1892/F.cry | 6 ++++++ intTests/test1892/I.cry | 3 +++ intTests/test1892/J.cry | 3 +++ intTests/test1892/M.cry | 1 + intTests/test1892/test.saw | 2 ++ intTests/test1892/test.sh | 3 +++ 7 files changed, 21 insertions(+) create mode 100644 intTests/test1892/A.cry create mode 100644 intTests/test1892/F.cry create mode 100644 intTests/test1892/I.cry create mode 100644 intTests/test1892/J.cry create mode 100644 intTests/test1892/M.cry create mode 100644 intTests/test1892/test.saw create mode 100755 intTests/test1892/test.sh diff --git a/intTests/test1892/A.cry b/intTests/test1892/A.cry new file mode 100644 index 0000000000..4f725bfab5 --- /dev/null +++ b/intTests/test1892/A.cry @@ -0,0 +1,3 @@ +interface module A where + +a : [8] diff --git a/intTests/test1892/F.cry b/intTests/test1892/F.cry new file mode 100644 index 0000000000..1c60d0db61 --- /dev/null +++ b/intTests/test1892/F.cry @@ -0,0 +1,6 @@ +module F where + +import interface A as X +import interface A as Y + +f = X::a + Y::a diff --git a/intTests/test1892/I.cry b/intTests/test1892/I.cry new file mode 100644 index 0000000000..145cfe0538 --- /dev/null +++ b/intTests/test1892/I.cry @@ -0,0 +1,3 @@ +module I where + +a = 1 diff --git a/intTests/test1892/J.cry b/intTests/test1892/J.cry new file mode 100644 index 0000000000..05e944b5f4 --- /dev/null +++ b/intTests/test1892/J.cry @@ -0,0 +1,3 @@ +module J where + +a = 2 diff --git a/intTests/test1892/M.cry b/intTests/test1892/M.cry new file mode 100644 index 0000000000..4c7c3de7dc --- /dev/null +++ b/intTests/test1892/M.cry @@ -0,0 +1 @@ +module M = F { X = I, Y = J } diff --git a/intTests/test1892/test.saw b/intTests/test1892/test.saw new file mode 100644 index 0000000000..28bf4b974d --- /dev/null +++ b/intTests/test1892/test.saw @@ -0,0 +1,2 @@ +import "M.cry"; +prove_print z3 {{ f == X::a + Y::a }}; diff --git a/intTests/test1892/test.sh b/intTests/test1892/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1892/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw From d2de4300ada02c2b6b79d10a260a6db294adfde8 Mon Sep 17 00:00:00 2001 From: Bretton Date: Wed, 23 Aug 2023 15:18:33 -0700 Subject: [PATCH 3/3] Add comment explaining ifaceNms in importName --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 8c05177e85..3bb2176ff6 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -1375,6 +1375,10 @@ importName cnm = let (topMod, nested) = C.modPathSplit (C.ogModule og) topChunks = C.modNameChunksText topMod modNms = topChunks ++ map C.identText nested + -- If the name came from a module parameter, add the module + -- parameter identifier to distinguish between names that have the + -- same identifier but come from different module parameters (see + -- #1892) ifaceNms = case C.ogFromParam og of Just i -> [C.identText i] Nothing -> []