Merge pull request #2762 from GaloisInc/bh/term-var-types

Enforce consistent variable typing contexts for all SAWCore terms

Author: brianhuffman

otherTests/saw-core/Tests/Functor.hs

@@ -50,7 +50,7 @@ shared :: TermIndex -> TermF Term -> Term
 shared ix t = STApp {
     stAppIndex = ix,
     stAppHash = hash t,
-    stAppFreeVars = mempty,
+    stAppVarTypes = mempty,
     stAppTermF = t
  }
 

saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs

@@ -2,13 +2,12 @@
 -- backends.
 {-# Language DataKinds, TypeOperators, GADTs, TypeApplications #-}
 {-# Language ImplicitParams #-}
-module SAWCentral.Crucible.Common.ResolveSetupValue ( 
+module SAWCentral.Crucible.Common.ResolveSetupValue (
   resolveBoolTerm, resolveBoolTerm',
   resolveBitvectorTerm, resolveBitvectorTerm',
   ResolveRewrite(..),
   ) where
 
-import qualified Data.Map as Map
 import           Data.Set(Set)
 import qualified Data.BitVector.Sized as BV
 import           Data.Parameterized.Some (Some(..))
@@ -19,7 +18,6 @@ import qualified What4.Interface as W4
 
 
 import SAWCore.SharedTerm
-import SAWCore.Name
 import qualified SAWCore.Prim as Prim
 
 import qualified SAWCore.Simulator.Concrete as Concrete
@@ -32,7 +30,6 @@ import SAWCentral.Crucible.Common
 
 import SAWCentral.Proof (TheoremNonce)
 import SAWCore.Rewriter (Simpset, rewriteSharedTerm)
-import qualified CryptolSAWCore.Simpset as Cryptol
 import SAWCoreWhat4.What4(w4EvalAny, valueToSymExpr)
 
 import Cryptol.TypeCheck.Type (tIsBit, tIsSeq, tIsNum)
@@ -82,21 +79,13 @@ resolveTerm sym unint bt rr tm =
               _ -> fail "resolveTerm: expected `Bool` or bit-vector"
 
         | rrWhat4Eval rr ->
-          do -- Try to use rewrites to simplify the term
-            cryptol_ss <- Cryptol.mkCryptolSimpset @TheoremNonce sc
-            tm''       <- snd <$> rewriteSharedTerm sc cryptol_ss tm'
-            tm'''      <- basicRewrite sc tm''
-            if all isPreludeName (Map.elems (getConstantSet tm''')) then
-              do
-                (_, _, _, p) <- w4EvalAny sym st sc mempty unint tm'''
-                case valueToSymExpr p of
-                  Just (Some y)
-                    | Just Refl <- testEquality bt ty -> pure y
-                    | otherwise -> typeError (show ty)
-                    where ty = W4.exprType y
-                  _ -> fail ("resolveTerm: unexpected w4Eval result " ++ show p)
-              else
-                bindSAWTerm sym st bt tm'''
+          do (_, _, _, p) <- w4EvalAny sym st sc mempty unint tm'
+             case valueToSymExpr p of
+               Just (Some y)
+                 | Just Refl <- testEquality bt ty -> pure y
+                 | otherwise -> typeError (show ty)
+                 where ty = W4.exprType y
+               _ -> fail ("resolveTerm: unexpected w4Eval result " ++ show p)
 
           -- Just bind the term
         | otherwise -> bindSAWTerm sym st bt tm'
@@ -107,11 +96,6 @@ resolveTerm sym unint bt rr tm =
       Nothing -> pure
       Just ss -> \t -> snd <$> rewriteSharedTerm sc ss t
 
-  isPreludeName nm =
-    case nm of
-      ModuleIdentifier ident -> identModule ident == preludeName
-      _ -> False
-
   checkType sc =
     do
       schema <- ttType <$> mkTypedTerm sc tm
@@ -146,9 +130,8 @@ resolveBoolTerm sym unint = resolveBoolTerm' sym unint noResolveRewrite
 resolveBitvectorTerm' ::
   (1 W4.<= w) => Sym -> Set VarIndex -> W4.NatRepr w -> ResolveRewrite -> Term -> IO (W4.SymBV Sym w)
 resolveBitvectorTerm' sym unint w = resolveTerm sym unint (W4.BaseBVRepr w)
-                  
+
 -- 'resolveTerm' specialized to bit-vectors, without rewriting.
-resolveBitvectorTerm :: 
+resolveBitvectorTerm ::
   (1 W4.<= w) => Sym -> Set VarIndex -> W4.NatRepr w -> Term -> IO (W4.SymBV Sym w)
 resolveBitvectorTerm sym unint w = resolveBitvectorTerm' sym unint w noResolveRewrite
-

saw-central/src/SAWCentral/SolverCache.hs

@@ -79,6 +79,7 @@ import Control.Monad (when, forM_)
 import System.Timeout (timeout)
 
 import GHC.Generics (Generic)
+import qualified Data.IntMap as IntMap
 import Data.IORef (IORef, newIORef, modifyIORef, readIORef)
 import Data.Time.Clock (UTCTime, getCurrentTime)
 import Data.Tuple.Extra (first, firstM)
@@ -116,6 +117,7 @@ import SAWCore.Name (VarName(..))
 import SAWCore.SATQuery
 import SAWCore.ExternalFormat
 import SAWCore.SharedTerm
+import SAWCore.Term.Raw (varTypes)
 
 import SAWCentral.Options
 import SAWCentral.Proof
@@ -300,7 +302,8 @@ mkSolverCacheKey :: SharedContext -> SolverBackendVersions ->
                     [SolverBackendOption] -> SATQuery -> IO SolverCacheKey
 mkSolverCacheKey sc vs opts satq = do
   body <- satQueryAsPropTerm sc satq
-  satVars <- traverse (scFirstOrderType sc) (satVariables satq)
+  let mkVar x _fot = IntMap.lookup (vnIndex x) (varTypes body)
+  let satVars = Map.mapMaybeWithKey mkVar (satVariables satq)
   let vars = Map.toList satVars ++
              filter (\(x, _) -> vnIndex x `elem` satUninterp satq)
                     (getAllVars body)

saw-core/src/SAWCore/Rewriter.hs

@@ -719,9 +719,25 @@ rewriteSharedTerm sc ss t0 =
     rewriteAll STApp{ stAppIndex = tidx, stAppTermF = tf } =
         useCache ?cache tidx (traverseTF rewriteAll tf >>= scTermF sc >>= rewriteTop)
 
-    traverseTF :: forall b. (b -> IO b) -> TermF b -> IO (TermF b)
-    traverseTF _ tf@(Constant {}) = pure tf
-    traverseTF f tf = traverse f tf
+    traverseTF :: (Term -> IO Term) -> TermF Term -> IO (TermF Term)
+    traverseTF f tf =
+      case tf of
+        -- Maintain invariant that types on Lambda/Pi binders should
+        -- exactly match types on the bound variables in the body.
+        Variable {} -> pure tf
+        Lambda x t1 t2 ->
+          do t1' <- f t1
+             var <- scVariable sc x t1'
+             t2' <- scInstantiate sc (IntMap.singleton (vnIndex x) var) t2
+             t2'' <- f t2'
+             pure (Lambda x t1' t2'')
+        Pi x t1 t2 ->
+          do t1' <- f t1
+             var <- scVariable sc x t1'
+             t2' <- scInstantiate sc (IntMap.singleton (vnIndex x) var) t2
+             t2'' <- f t2'
+             pure (Pi x t1' t2'')
+        _ -> traverse f tf
 
     rewriteTop :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => Term -> IO Term
     rewriteTop t =

saw-core/src/SAWCore/SATQuery.hs

@@ -6,13 +6,16 @@ module SAWCore.SATQuery
 , satQueryAsPropTerm
 ) where
 
+import qualified Data.IntMap as IntMap
 import Data.Map (Map)
+import Data.Maybe (mapMaybe)
 import Data.Set (Set)
 import Data.Foldable (foldrM)
 
 import SAWCore.Name
 import SAWCore.FiniteValue
 import SAWCore.SharedTerm
+import SAWCore.Term.Raw (varTypes)
 
 -- | This datatype represents a satisfiability query that might
 --   be dispatched to a solver.  It carries a series of assertions
@@ -96,6 +99,7 @@ satQueryAsPropTerm sc satq =
   scTupleType sc =<< mapM assertAsPropTerm (satAsserts satq)
   where assertAsPropTerm (BoolAssert b) = scEqTrue sc b
         assertAsPropTerm (UniversalAssert vars hs g) =
-          do vars' <- traverse (traverse (scFirstOrderType sc)) vars
-             scPiList sc vars' =<<
-               scEqTrue sc =<< foldrM (scImplies sc) g hs
+          do body <- scEqTrue sc =<< foldrM (scImplies sc) g hs
+             let varType x = fmap ((,) x) $ IntMap.lookup (vnIndex x) (varTypes body)
+             let vars' = mapMaybe (varType . fst) vars
+             scPiList sc vars' body