Eliminate compilation warnings

.travis.yml

@@ -39,7 +39,10 @@ script:
   # `libabc.a` is built in by `cabal configure`, not by `cabal build`.
   # caching `dist-newstyle` means it must be manually built each time
   - (pushd deps/abcBridge && scripts/build-abc.sh X86_64 Linux --init && popd)
-  - cabal new-build -j saw jss
+  # Ideally, we'd like to pass --ghc-options=-Werror to cabal build.
+  # However, this currently enables -Werror for all dependencies as well.
+  # See: https://github.com/haskell/cabal/issues/3883
+  - cabal new-build --project-file=cabal.project.ci -j saw jss
   - cp `cabal new-exec --verbose=silent -- sh -c 'which saw'` bin
   - cp `cabal new-exec --verbose=silent -- sh -c 'which jss'` bin
 

cabal.project.ci

@@ -0,0 +1,33 @@
+packages:
+    saw-script.cabal
+    deps/llvm-pretty
+    deps/llvm-pretty-bc-parser
+    deps/jvm-parser
+    deps/aig
+    deps/abcBridge
+    deps/cryptol
+    deps/saw-core
+    deps/saw-core-aig
+    deps/saw-core-sbv
+    deps/saw-core-what4
+    deps/cryptol-verifier
+    deps/jvm-verifier
+    deps/what4/what4
+    deps/what4/what4-abc
+    deps/crucible/crucible
+    deps/crucible/crucible-jvm
+    deps/crucible/crucible-llvm
+    deps/crucible/crucible-saw
+    deps/crucible/crux
+    deps/parameterized-utils
+    deps/flexdis86
+    deps/flexdis86/binary-symbols
+    deps/macaw/base
+    deps/macaw/symbolic
+    deps/macaw/x86
+    deps/macaw/x86_symbolic
+    deps/elf-edit
+    deps/dwarf
+
+package saw-script
+  ghc-options: -Werror

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -46,7 +46,6 @@ import           Data.Foldable (for_)
 import           Data.Function
 import           Data.IORef
 import           Data.List
-import           Data.Monoid ((<>))
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Set (Set)

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -201,6 +201,8 @@ resolveSAWTerm cc tp tm =
       fail "resolveSAWTerm: unsupported record type"
     Cryptol.TVFun _ _ ->
       fail "resolveSAWTerm: unsupported function type"
+    Cryptol.TVAbstract _ _ ->
+      fail "resolveSAWTerm: unsupported abstract type"
   where
     sym = cc^.jccBackend
 
@@ -265,6 +267,7 @@ toJVMType tp =
     Cryptol.TVTuple _tps -> Nothing
     Cryptol.TVRec _flds -> Nothing
     Cryptol.TVFun _ _ -> Nothing
+    Cryptol.TVAbstract _ _ -> Nothing
 
 equalValsPred ::
   JVMCrucibleContext ->

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -103,7 +103,6 @@ import           Control.Lens
 import           Control.Monad (when)
 import           Data.Functor.Compose (Compose(..))
 import           Data.IORef
-import           Data.Monoid ((<>))
 import           Data.Type.Equality (TestEquality(..))
 import qualified Text.LLVM.AST as L
 import qualified Text.LLVM.PP as L

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -412,6 +412,8 @@ resolveSAWTerm cc tp tm =
         fail "resolveSAWTerm: unimplemented record type (FIXME)"
       Cryptol.TVFun _ _ ->
         fail "resolveSAWTerm: invalid function type"
+      Cryptol.TVAbstract _ _ ->
+        fail "resolveSAWTerm: invalid abstract type"
   where
     sym = cc^.ccBackend
     dl = Crucible.llvmDataLayout (ccTypeCtx cc)
@@ -455,6 +457,7 @@ toLLVMType dl tp =
       return (Crucible.StructType si)
     Cryptol.TVRec _flds -> Left (NotYetSupported "record")
     Cryptol.TVFun _ _ -> Left (Impossible "function")
+    Cryptol.TVAbstract _ _ -> Left (Impossible "abstract")
 
 toLLVMStorageType ::
   forall w .

src/SAWScript/Interpreter.hs

@@ -44,8 +44,6 @@ import System.Directory (getCurrentDirectory, setCurrentDirectory, canonicalizeP
 import System.FilePath (takeDirectory)
 import System.Process (readProcess)
 
-import qualified Text.LLVM.AST as L
-
 import qualified SAWScript.AST as SS
 import qualified SAWScript.Position as SS
 import SAWScript.AST (Located(..),Import(..))

src/SAWScript/Value.hs

@@ -84,7 +84,6 @@ import Verifier.SAW.TypedTerm
 
 import qualified Verifier.SAW.Simulator.Concrete as Concrete
 import qualified Cryptol.Eval as C
-import qualified Cryptol.Eval.Value as C
 import qualified Cryptol.Eval.Concrete.Value as C
 import Verifier.SAW.Cryptol (exportValueWithSchema)
 import qualified Cryptol.TypeCheck.AST as Cryptol (Schema)

src/SAWScript/X86Spec.hs

@@ -424,6 +424,8 @@ locRepr l =
         M.BVTypeRepr w -> LLVMPointerRepr w
         M.BoolTypeRepr -> BoolRepr
         M.TupleTypeRepr {} -> error $ "[locRepr] Unexpected tuple register"
+        M.FloatTypeRepr {} -> error $ "[locRepr] Unexpected float register"
+        M.VecTypeRepr {} -> error $ "[locRepr] Unexpected vector register"
 
 --------------------------------------------------------------------------------