Merge pull request #2157 from GaloisInc/dholland-typechecker

Lower the boom on the mess in the saw-script typechecker

CHANGES.md

@@ -2,11 +2,23 @@
 
 ## New Features
 
+* Add a `:tenv` REPL command, which is like `:env` but prints the type
+  environment instead of the variable environment. `:t` is still short
+  for `:type`.
+
 * Add `mir_equal` and `jvm_equal` commands, which mirror the `llvm_equal`
   command for the MIR and JVM backends, respectively.
 
 ## Bug fixes
 
+* A number of SAWScript type checking problems have been fixed,
+including issue #2077.
+Some of these problems were partially mutually compensating; for
+example, in some cases nonexistent typedefs had been mishandled in
+ways that made them mostly work.
+Some previously accepted scripts and specs may be rejected and need
+(generally minor) adjustment.
+
 * Counterexamples including SMT arrays are now printed with the array
   contents instead of placeholder text.
 

intTests/test_type_errors/err002.log.good

@@ -0,0 +1,12 @@
+ Loading file "err002.saw"
+ err002.saw:5:44-5:57: Type mismatch.
+    Mismatch of type constructors. Expected: String but got ([])
+    internal:1:1-1:7: The type String arises from this type annotation
+    err002.saw:5:44-5:57: The type [LLVMType] arises from the type of this term
+
+    Expected: String
+    Found:    [LLVMType]
+
+    within "spec" (err002.saw:4:5-4:9)
+
+FAILED

intTests/test_type_errors/err002.saw

@@ -0,0 +1,8 @@
+// llvm_alias takes a string, pass it a list of types instead
+// (user meant to use llvm_struct_type and used llvm_struct,
+// which is a deprecated name for llvm_alias)
+let spec = do {
+   input <- llvm_fresh_var "x" (llvm_alias [llvm_int 32]);
+   llvm_execute_func [llvm_term input];
+};
+

intTests/test_type_errors/err003.log.good

@@ -0,0 +1,3 @@
+ Loading file "err003.saw"
+ err003.saw:3:16-3:27: Unbound type variable Nonexistent
+FAILED

intTests/test_type_errors/err003.saw

@@ -0,0 +1,8 @@
+
+let bar = do {
+   typedef t = Nonexistent;
+
+   let foo (a: t) = a;
+
+   return 0;
+};

intTests/test_type_errors/err004.log.good

@@ -0,0 +1,3 @@
+ Loading file "err004.saw"
+ err004.saw:2:13-2:24: Unbound type variable Nonexistent
+FAILED

intTests/test_type_errors/err004.saw

@@ -0,0 +1,4 @@
+
+typedef t = Nonexistent;
+
+let foo (a: t) = a;

intTests/test_type_errors/err005.log.good

@@ -0,0 +1,3 @@
+ Loading file "err005.saw"
+ err005.saw:1:30-1:31: Unbound type variable x
+FAILED

intTests/test_type_errors/err005.saw

@@ -0,0 +1 @@
+typedef x = { foo: Int, bar: x };

saw-remote-api/src/SAWServer.hs

@@ -246,8 +246,8 @@ initialState readFileFn =
                 }
          rw = TopLevelRW
                 { rwValues = mempty
-                , rwTypes = mempty
-                , rwTypedef = mempty
+                , rwValueTypes = mempty
+                , rwNamedTypes = mempty
                 , rwDocs = mempty
                 , rwCryptol = cenv
                 , rwMonadify = defaultMonEnv

saw/SAWScript/REPL/Command.hs

@@ -43,7 +43,7 @@ import Control.Monad (guard, void)
 
 import Data.Char (isSpace,isPunctuation,isSymbol)
 import Data.Function (on)
-import Data.List (intercalate)
+import Data.List (intercalate, nub)
 import System.FilePath((</>), isPathSeparator)
 import System.Directory(getHomeDirectory,getCurrentDirectory,setCurrentDirectory,doesDirectoryExist)
 import qualified Data.Map as Map
@@ -74,6 +74,7 @@ data Command
 -- | Command builder.
 data CommandDescr = CommandDescr
   { cName :: String
+  , cAliases :: [String]
   , cBody :: CommandBody
   , cHelp :: String
   }
@@ -94,39 +95,45 @@ data CommandBody
   | NoArg       (REPL ())
 
 
+-- | Convert the command list to a Trie, expanding aliases.
+makeCommands :: [CommandDescr] -> CommandMap
+makeCommands list  = foldl insert emptyTrie (concatMap expandAliases list)
+  where
+  insert m (name, d) = insertTrie name d m
+  expandAliases :: CommandDescr -> [(String, CommandDescr)]
+  expandAliases d = (cName d, d) : zip (cAliases d) (repeat d)
+
 -- | REPL command parsing.
 commands :: CommandMap
-commands  = foldl insert emptyTrie commandList
-  where
-  insert m d = insertTrie (cName d) d m
+commands = makeCommands commandList
 
 -- | Notebook command parsing.
 nbCommands :: CommandMap
-nbCommands  = foldl insert emptyTrie nbCommandList
-  where
-  insert m d = insertTrie (cName d) d m
+nbCommands = makeCommands nbCommandList
 
 -- | A subset of commands safe for Notebook execution
 nbCommandList :: [CommandDescr]
 nbCommandList  =
-  [ CommandDescr ":env"    (NoArg envCmd)
+  [ CommandDescr ":env"  []      (NoArg envCmd)
     "display the current sawscript environment"
-  , CommandDescr ":type"   (ExprArg typeOfCmd)
+  , CommandDescr ":tenv" []      (NoArg tenvCmd)
+    "display the current sawscript type environment"
+  , CommandDescr ":type" [":t"]  (ExprArg typeOfCmd)
     "check the type of an expression"
-  , CommandDescr ":?"      (ExprArg helpCmd)
+  , CommandDescr ":?"    []      (ExprArg helpCmd)
     "display a brief description about a built-in operator"
-  , CommandDescr ":help"   (ExprArg helpCmd)
+  , CommandDescr ":help" []      (ExprArg helpCmd)
     "display a brief description about a built-in operator"
   ]
 
 commandList :: [CommandDescr]
 commandList  =
   nbCommandList ++
-  [ CommandDescr ":quit"   (NoArg quitCmd)
+  [ CommandDescr ":quit" []   (NoArg quitCmd)
     "exit the REPL"
-  , CommandDescr ":cd" (FilenameArg cdCmd)
+  , CommandDescr ":cd"   []   (FilenameArg cdCmd)
     "set the current working directory"
-  , CommandDescr ":pwd" (NoArg pwdCmd)
+  , CommandDescr ":pwd"  []   (NoArg pwdCmd)
     "display the current working directory"
   ]
 
@@ -165,7 +172,7 @@ typeOfCmd str
          decl = SS.Decl pos (SS.PWild pos Nothing) Nothing expr
      rw <- getValueEnvironment
      ~(SS.Decl _pos _ (Just schema) _expr') <-
-       either failTypecheck return $ checkDecl (rwTypes rw) (rwTypedef rw) decl
+       either failTypecheck return $ checkDecl (rwValueTypes rw) (rwNamedTypes rw) decl
      io $ putStrLn $ SS.pShow schema
 
 quitCmd :: REPL ()
@@ -176,7 +183,12 @@ envCmd :: REPL ()
 envCmd = do
   env <- getValueEnvironment
   let showLName = SS.getVal
-  io $ sequence_ [ putStrLn (showLName x ++ " : " ++ SS.pShow v) | (x, v) <- Map.assocs (rwTypes env) ]
+  io $ sequence_ [ putStrLn (showLName x ++ " : " ++ SS.pShow v) | (x, v) <- Map.assocs (rwValueTypes env) ]
+
+tenvCmd :: REPL ()
+tenvCmd = do
+  env <- getValueEnvironment
+  io $ sequence_ [ putStrLn (a ++ " : " ++ SS.pShow t) | (a, t) <- Map.assocs (rwNamedTypes env) ]
 
 helpCmd :: String -> REPL ()
 helpCmd cmd
@@ -283,13 +295,20 @@ splitCommand txt =
 
     expr -> guard (not (null expr)) >> return (expr,[])
 
--- | Lookup a string in the command list.
+-- | Look up a string in a command list. If given a string that's both
+-- itself a command and a prefix of something else, choose that
+-- command; otherwise such commands are inaccessible. Also, deduplicate
+-- the list of results to avoid silliness with command aliases.
+findSomeCommand :: String -> CommandMap -> [CommandDescr]
+findSomeCommand str commandTable = nub $ lookupTrieWithExact str commandTable
+
+-- | Look up a string in the command list.
 findCommand :: String -> [CommandDescr]
-findCommand str = lookupTrie str commands
+findCommand str = findSomeCommand str commands
 
--- | Lookup a string in the notebook-safe command list.
+-- | Look up a string in the notebook-safe command list.
 findNbCommand :: String -> [CommandDescr]
-findNbCommand str = lookupTrie str nbCommands
+findNbCommand str = findSomeCommand str nbCommands
 
 -- | Parse a line as a command.
 parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command

saw/SAWScript/REPL/Trie.hs

@@ -41,6 +41,19 @@ lookupTrie key t@(Node mp _) = case key of
 
   [] -> leaves t
 
+-- | Return all matches with the given prefix. However, if an exact match
+-- exists, return just that match.
+lookupTrieWithExact :: String -> Trie a -> [a]
+lookupTrieWithExact key t@(Node mp mb) = case key of
+
+  c:cs -> case Map.lookup c mp of
+    Just m' -> lookupTrieWithExact cs m'
+    Nothing -> []
+
+  [] -> case mb of
+    Just b -> [b]
+    Nothing -> leaves t
+
 -- | Return all of the values from a Trie.
 leaves :: Trie a -> [a]
 leaves (Node mp mb) = maybeToList mb ++ concatMap leaves (Map.elems mp)

src/SAWScript/AST.hs

@@ -28,6 +28,7 @@ module SAWScript.AST
        , Type(..), TypeIndex
        , TyCon(..)
        , Schema(..)
+       , NamedType(..)
        , toLName
        , tMono, tForall, tTuple, tRecord, tArray, tFun
        , tString, tTerm, tType, tBool, tInt, tAIG, tCFG
@@ -164,15 +165,15 @@ instance Positioned Pattern where
   getPos (PTuple pos _) = pos
 
 data Stmt
-  = StmtBind     Pos Pattern (Maybe Type) Expr
+  = StmtBind     Pos Pattern Expr
   | StmtLet      Pos DeclGroup
   | StmtCode     Pos (Located String)
   | StmtImport   Pos Import
   | StmtTypedef  Pos (Located String) Type
   deriving Show
 
 instance Positioned Stmt where
-  getPos (StmtBind pos _ _ _)  = pos
+  getPos (StmtBind pos _ _)  = pos
   getPos (StmtLet pos _)       = pos
   getPos (StmtCode pos _)      = pos
   getPos (StmtImport pos _)    = pos
@@ -263,6 +264,13 @@ data TyCon
 data Schema = Forall [(Pos, Name)] Type
   deriving Show
 
+-- | The things a (named) TyVar can refer to by its name.
+--
+-- AbstractType is an opaque type whose only semantics are the
+-- operations available for it, if any. The name identifies it; the
+-- AbstractType constructor is a placeholder.
+data NamedType = ConcreteType Type | AbstractType
+
 -- }}}
 
 -- Pretty Printing {{{
@@ -332,9 +340,9 @@ instance Pretty Pattern where
 
 instance Pretty Stmt where
    pretty = \case
-      StmtBind _ (PWild _ _leftType) _rightType expr ->
+      StmtBind _ (PWild _ _ty) expr ->
          PP.pretty expr
-      StmtBind _ pat _rightType expr ->
+      StmtBind _ pat expr ->
          PP.pretty pat PP.<+> "<-" PP.<+> PP.align (PP.pretty expr)
       StmtLet _ (NonRecursive decl) ->
          "let" PP.<+> prettyDef decl
@@ -450,6 +458,11 @@ instance PrettyPrint Context where
     TopLevel     -> "TopLevel"
     CrucibleSetup-> "CrucibleSetup"
 
+instance PrettyPrint NamedType where
+  pretty par ty = case ty of
+    ConcreteType ty' -> pretty par ty'
+    AbstractType -> "<opaque>"
+
 replicateDoc :: Integer -> PP.Doc ann -> PP.Doc ann
 replicateDoc n d
   | n < 1 = PP.emptyDoc

src/SAWScript/AutoMatch.hs

@@ -374,17 +374,17 @@ processResults (TaggedSourceFile leftLang  leftFile) (TaggedSourceFile rightLang
          returning boundName . tell $
             case lang of
                Cryptol ->
-                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing
+                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing)
                      (SAWScript.Application triggerPos
                         (SAWScript.Var $ locate "cryptol_load")
                         (SAWScript.String triggerPos file))]
                LLVM ->
-                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing
+                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing)
                      (SAWScript.Application triggerPos
                         (SAWScript.Var $ locate "llvm_load_module")
                         (SAWScript.String triggerPos file))]
                JVM ->
-                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing
+                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing)
                      (SAWScript.Application triggerPos
                         (SAWScript.Var $ locate "java_load_class")
                         (SAWScript.String triggerPos $ dropExtension file))]
@@ -395,21 +395,21 @@ processResults (TaggedSourceFile leftLang  leftFile) (TaggedSourceFile rightLang
          returning boundName . tell $
             case lang of
                Cryptol ->
-                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing
+                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing)
                      (SAWScript.Application triggerPos
                         (SAWScript.Application triggerPos
                            (SAWScript.Var $ locate "cryptol_extract")
                            (SAWScript.Var loadedModule))
                         (SAWScript.String triggerPos function))]
                LLVM ->
-                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing
+                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing)
                      (SAWScript.Application triggerPos
                         (SAWScript.Application triggerPos
                            (SAWScript.Var $ locate "llvm_extract")
                            (SAWScript.Var loadedModule))
                         (SAWScript.String triggerPos function))]
                JVM ->
-                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing
+                  [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing)
                      (SAWScript.Application triggerPos
                         (SAWScript.Application triggerPos
                            (SAWScript.Var $ locate "jvm_extract")
@@ -426,7 +426,7 @@ processResults (TaggedSourceFile leftLang  leftFile) (TaggedSourceFile rightLang
                   name <- newNameWith (nameCenter (leftName ++ "_" ++ rightName))
                   return ((leftIndex, name), (rightIndex, name))
          returning theoremName . tell $
-            [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos theoremName Nothing) Nothing .
+            [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos theoremName Nothing) .
                 SAWScript.Code . locate .
                    show . Cryptol.ppPrec 0 .
                       cryptolAbstractNamesSAW leftArgs .
@@ -453,7 +453,7 @@ processResults (TaggedSourceFile leftLang  leftFile) (TaggedSourceFile rightLang
 
       prove :: SAWScript.LName -> ScriptWriter s tp ()
       prove theorem = tell $
-         [SAWScript.StmtBind triggerPos (SAWScript.PWild triggerPos Nothing) Nothing
+         [SAWScript.StmtBind triggerPos (SAWScript.PWild triggerPos Nothing)
              (SAWScript.Application triggerPos
                 (SAWScript.Application triggerPos
                    (SAWScript.Var $ locate "prove_print")
@@ -462,7 +462,7 @@ processResults (TaggedSourceFile leftLang  leftFile) (TaggedSourceFile rightLang
 
       printString :: String -> ScriptWriter s tp ()
       printString string = tell $
-         [SAWScript.StmtBind triggerPos (SAWScript.PWild triggerPos Nothing) Nothing
+         [SAWScript.StmtBind triggerPos (SAWScript.PWild triggerPos Nothing)
              (SAWScript.Application triggerPos
                 (SAWScript.Var $ locate "print")
                 (SAWScript.String triggerPos string))]

src/SAWScript/Builtins.hs

@@ -1774,7 +1774,7 @@ caseSatResultPrim sr vUnsat vSat = do
 
 envCmd :: TopLevel ()
 envCmd = do
-  m <- rwTypes <$> SV.getMergedEnv
+  m <- rwValueTypes <$> SV.getMergedEnv
   opts <- getOptions
   let showLName = getVal
   io $ sequence_ [ printOutLn opts Info (showLName x ++ " : " ++ pShow v) | (x, v) <- Map.assocs m ]