From f04b00bfb1337d51284e9004ae5282d2b48867ef Mon Sep 17 00:00:00 2001 From: David Holland Date: Tue, 16 Sep 2025 21:23:44 -0400 Subject: [PATCH 1/2] Add two missing bits to SAWScript's Cryptol import syntax. - allow the word "submodule" (it is currently ignored, but that will likely change soon) - allow the import name to be qualified (as in "...as M::N") Add a test for the latter part. --- intTests/test2605/Foo.cry | 4 +++ intTests/test2605/test.saw | 3 +++ intTests/test2605/test.sh | 3 +++ .../test_sawscript_builtins/files.log.good | 4 +-- saw-central/src/SAWCentral/AST.hs | 3 ++- saw-script/src/SAWScript/Lexer.x | 2 +- saw-script/src/SAWScript/Parser.y | 26 +++++++++++++++++-- 7 files changed, 39 insertions(+), 6 deletions(-) create mode 100644 intTests/test2605/Foo.cry create mode 100644 intTests/test2605/test.saw create mode 100644 intTests/test2605/test.sh diff --git a/intTests/test2605/Foo.cry b/intTests/test2605/Foo.cry new file mode 100644 index 0000000000..3148fa08dd --- /dev/null +++ b/intTests/test2605/Foo.cry @@ -0,0 +1,4 @@ +module Foo where + +x : [8] +x = 3 diff --git a/intTests/test2605/test.saw b/intTests/test2605/test.saw new file mode 100644 index 0000000000..3fef512569 --- /dev/null +++ b/intTests/test2605/test.saw @@ -0,0 +1,3 @@ +import "Foo.cry" as Moo::Boo; + +let y = {{ Moo::Boo::x }}; diff --git a/intTests/test2605/test.sh b/intTests/test2605/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test2605/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/intTests/test_sawscript_builtins/files.log.good b/intTests/test_sawscript_builtins/files.log.good index 7fcbe665eb..21df77081e 100644 --- a/intTests/test_sawscript_builtins/files.log.good +++ b/intTests/test_sawscript_builtins/files.log.good @@ -4,8 +4,8 @@ [104, 101, 108, 108, 111, 10] dump_file_AST: Loading file "include/syntax.saw" -StmtImport include/syntax.saw:5:1-5:30 (Import {iModule = Left "Foo.cry", iAs = Just (ModName "Foo" NormalName), iSpec = Just (Only [Ident False NormalName "foo"]), iPos = include/syntax.saw:5:8-5:30}) -StmtImport include/syntax.saw:6:1-6:30 (Import {iModule = Left "Bar.cry", iAs = Nothing, iSpec = Just (Hiding [Ident False NormalName "bar"]), iPos = include/syntax.saw:6:8-6:30}) +StmtImport include/syntax.saw:5:1-5:30 (Import {iIsSubmodule = False, iModule = Left "Foo.cry", iAs = Just (ModName "Foo" NormalName), iSpec = Just (Only [Ident False NormalName "foo"]), iPos = include/syntax.saw:5:8-5:30}) +StmtImport include/syntax.saw:6:1-6:30 (Import {iIsSubmodule = False, iModule = Left "Bar.cry", iAs = Nothing, iSpec = Just (Hiding [Ident False NormalName "bar"]), iPos = include/syntax.saw:6:8-6:30}) StmtBind include/syntax.saw:8:1-8:4 (PWild include/syntax.saw:8:1-8:1 Nothing) (Int include/syntax.saw:8:1-8:4 123) StmtBind include/syntax.saw:9:1-9:16 (PVar include/syntax.saw:9:1-9:2 "a" (include/syntax.saw:9:1-9:2) Nothing) (Application include/syntax.saw:9:6-9:16 (Var "return" (include/syntax.saw:9:6-9:12)) (Int include/syntax.saw:9:13-9:16 456)) StmtLet include/syntax.saw:11:1-11:12 (NonRecursive (Decl {dPos = include/syntax.saw:11:5-11:12, dPat = PVar include/syntax.saw:11:5-11:6 "f" (include/syntax.saw:11:5-11:6) Nothing, dType = Nothing, dDef = Lambda include/syntax.saw:11:7-11:12 (Just "f") (PVar include/syntax.saw:11:7-11:8 "x" (include/syntax.saw:11:7-11:8) Nothing) (Var "x" (include/syntax.saw:11:11-11:12))})) diff --git a/saw-central/src/SAWCentral/AST.hs b/saw-central/src/SAWCentral/AST.hs index 7892767f37..2181dbd2a0 100644 --- a/saw-central/src/SAWCentral/AST.hs +++ b/saw-central/src/SAWCentral/AST.hs @@ -120,7 +120,8 @@ type LName = Located Name -- Expr Level {{{ data Import = Import - { iModule :: Either FilePath P.ModName + { iIsSubmodule :: Bool + , iModule :: Either FilePath P.ModName , iAs :: Maybe P.ModName , iSpec :: Maybe P.ImportSpec , iPos :: Pos diff --git a/saw-script/src/SAWScript/Lexer.x b/saw-script/src/SAWScript/Lexer.x index 845add6c76..d216a7d132 100644 --- a/saw-script/src/SAWScript/Lexer.x +++ b/saw-script/src/SAWScript/Lexer.x @@ -47,7 +47,7 @@ $idfirst = [$alpha \_] $idchar = [$alpha $digit $unidigit $unitick \' \_] $codechar = [$graphic $whitechar \n] -@reservedid = import|and|let|rec|in|do|if|then|else|as|hiding|typedef +@reservedid = import|submodule|and|let|rec|in|do|if|then|else|as|hiding|typedef |JavaSetup|LLVMSetup|MIRSetup|ProofScript|TopLevel|CrucibleSetup |Int|String|Term|Type|Bool|AIG|CFG |CrucibleMethodSpec|LLVMSpec|JVMMethodSpec|JVMSpec|MIRSpec diff --git a/saw-script/src/SAWScript/Parser.y b/saw-script/src/SAWScript/Parser.y index 01ddc13d63..d67afa2ecb 100644 --- a/saw-script/src/SAWScript/Parser.y +++ b/saw-script/src/SAWScript/Parser.y @@ -51,6 +51,7 @@ import Control.Exception %token 'import' { TReserved _ "import" } + 'submodule' { TReserved _ "submodule" } 'and' { TReserved _ "and" } 'as' { TReserved _ "as" } 'hiding' { TReserved _ "hiding" } @@ -89,6 +90,7 @@ import Control.Exception '{' { TPunct _ "{" } '}' { TPunct _ "}" } ':' { TPunct _ ":" } + '::' { TPunct _ "::" } ',' { TPunct _ "," } '.' { TPunct _ "." } '\\' { TPunct _ "\\" } @@ -134,11 +136,12 @@ StmtSemi :: { Stmt } : fst(Stmt, opt(';')) { $1 } Import :: { Import } - : string mbAs mbImportSpec { Import (Left (unpack $ tokStr $1)) (fst $2) (fst $3) (maxSpan [tokPos $1, snd $2, snd $3])} + : string mbAs mbImportSpec { buildImport False $1 $2 $3 } + | 'submodule' string mbAs mbImportSpec { buildImport True $2 $3 $4 } -- TODO: allow imports by module name instead of path mbAs :: { (Maybe P.ModName, Pos) } - : 'as' name { (Just (P.packModName [tokStr $2]), maxSpan [$1, $2]) } +: 'as' QName { (Just (P.packModName (fst $2)), maxSpan' $1 (snd $2)) } | {- empty -} { (Nothing, Unknown) } mbImportSpec :: { (Maybe P.ImportSpec, Pos) } @@ -271,6 +274,9 @@ Context :: { Type } FieldType :: { (Name, Type) } : name ':' Type { (tokStr $1, $3) } +QName :: { ([Text], Pos) } + : sepBy1(name, '::') { (map tokStr $1, maxSpan (map tokPos $1)) } + -- Parameterized productions, most come directly from the Happy manual. fst(p, q) : p q { $1 } snd(p, q) : p q { $2 } @@ -356,6 +362,22 @@ parseError toks = case toks of [] -> Left UnexpectedEOF t : _ -> Left (UnexpectedToken t) +-- | Cons up an import. +buildImport :: + Bool -> + Token Pos -> + (Maybe P.ModName, Pos) -> + (Maybe P.ImportSpec, Pos) -> + Import +buildImport issub modName (mbAsName, asPos) (mbSpec, specPos) = + Import { + iIsSubmodule = issub, + iModule = Left (unpack $ tokStr modName), + iAs = mbAsName, + iSpec = mbSpec, + iPos = maxSpan [tokPos modName, asPos, specPos] + } + -- | As seen by the parser, a "function name" is an arbitrary pattern. -- This is because we use the same syntax for function and value bindings: -- in "let (a, b) = e" the "(a, b)" can and should be an arbitrary pattern. From c3f765d7ede72b3c2f7926c95f3c446a138ebb19 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 17 Sep 2025 23:32:16 -0400 Subject: [PATCH 2/2] Bump CABAL_CACHE_VERSION to 12. The build failure seen earlier today is almost certainly cache corruption. Note that the 1.4 branch is using cache version 11; it's probably best to not try to share. --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index afa6a0caba..45f866dee8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,7 +25,7 @@ env: # version is changed but older .so files are cached, which can have various # effects (e.g. cabal complains it can't find a valid version of the "happy" # tool). - CABAL_CACHE_VERSION: 10 + CABAL_CACHE_VERSION: 12 CARGO_CACHE_VERSION: 1 SOLVER_CACHE_VERSION: 1