Remove uses of mkTypedTerm

src/SAWScript/Builtins.hs

@@ -57,6 +57,8 @@ import Verifier.SAW.Grammar (parseSAWTerm)
 import Verifier.SAW.ExternalFormat
 import Verifier.SAW.FiniteValue
   ( FiniteType(..), readFiniteValue
+  , FirstOrderType(..)
+  , firstOrderTypeOf
   , FirstOrderValue(..)
   , toFirstOrderValue, scFirstOrderValue
   )
@@ -267,7 +269,11 @@ readAIGPrim f = do
   et <- io $ readAIG proxy opts sc f
   case et of
     Left err -> fail $ "Reading AIG failed: " ++ err
-    Right t -> io $ mkTypedTerm sc t
+    Right (inLen, outLen, t) -> pure $ TypedTerm schema t
+      where
+        t1 = C.tWord (C.tNum inLen)
+        t2 = C.tWord (C.tNum outLen)
+        schema = C.tMono (C.tFun t1 t2)
 
 replacePrim :: TypedTerm -> TypedTerm -> TypedTerm -> TopLevel TypedTerm
 replacePrim pat replace t = do
@@ -1034,6 +1040,23 @@ toValueCase prim =
   SV.VLambda $ \v2 ->
   prim (SV.fromValue b) v1 v2
 
+cryptolTypeOfFirstOrderType :: FirstOrderType -> C.Type
+cryptolTypeOfFirstOrderType fot =
+  case fot of
+    FOTBit -> C.tBit
+    FOTInt -> C.tInteger
+    FOTVec n t -> C.tSeq (C.tNum n) (cryptolTypeOfFirstOrderType t)
+    FOTTuple ts -> C.tTuple (map cryptolTypeOfFirstOrderType ts)
+    FOTArray a b ->
+      C.tArray
+      (cryptolTypeOfFirstOrderType a)
+      (cryptolTypeOfFirstOrderType b)
+    FOTRec m ->
+      C.tRec $
+      C.recordFromFields $
+      [ (C.packIdent l, cryptolTypeOfFirstOrderType t)
+      | (l, t) <- Map.assocs m ]
+
 caseProofResultPrim :: SV.ProofResult
                     -> SV.Value -> SV.Value
                     -> TopLevel SV.Value
@@ -1045,7 +1068,9 @@ caseProofResultPrim pr vValid vInvalid = do
       let fvs = map snd pairs
       ts <- io $ mapM (scFirstOrderValue sc) fvs
       t <- io $ scTuple sc ts
-      tt <- io $ mkTypedTerm sc t
+      let fot = firstOrderTypeOf (FOVTuple fvs)
+      let cty = cryptolTypeOfFirstOrderType fot
+      let tt = TypedTerm (C.tMono cty) t
       SV.applyValue vInvalid (SV.toValue tt)
 
 caseSatResultPrim :: SV.SatResult
@@ -1059,7 +1084,9 @@ caseSatResultPrim sr vUnsat vSat = do
       let fvs = map snd pairs
       ts <- io $ mapM (scFirstOrderValue sc) fvs
       t <- io $ scTuple sc ts
-      tt <- io $ mkTypedTerm sc t
+      let fot = firstOrderTypeOf (FOVTuple fvs)
+      let cty = cryptolTypeOfFirstOrderType fot
+      let tt = TypedTerm (C.tMono cty) t
       SV.applyValue vSat (SV.toValue tt)
 
 envCmd :: TopLevel ()

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs

@@ -54,6 +54,9 @@ import qualified Lang.Crucible.Simulator.RegMap        as Crucible
 import qualified Lang.Crucible.Simulator.OverrideSim   as Crucible
 import qualified Lang.Crucible.Analysis.Postdom        as Crucible
 
+-- cryptol
+import qualified Cryptol.TypeCheck.Type as Cryptol
+
 -- crucible/what4
 import qualified What4.Expr as W4
 import qualified What4.Config as W4
@@ -62,13 +65,15 @@ import qualified What4.Solver.Yices as Yices
 
 -- saw-core
 import Verifier.SAW.SharedTerm(Term, SharedContext, mkSharedContext, scImplies, scAbstractExts)
-import Verifier.SAW.TypedTerm(TypedTerm, mkTypedTerm)
+
+-- cryptol-verifier
+import Verifier.SAW.TypedTerm(TypedTerm(..))
 
 -- saw-script
 import SAWScript.Builtins(fixPos)
 import SAWScript.Value
 import SAWScript.Options(Options,simVerbose)
-import SAWScript.Crucible.LLVM.Builtins (setupArg, setupArgs, getGlobalPair, runCFG)
+import SAWScript.Crucible.LLVM.Builtins (setupArg, setupArgs, getGlobalPair, runCFG, baseCryptolType)
 
 -- jvm-verifier
 import qualified Language.JVM.Common as J
@@ -164,13 +169,20 @@ crucible_java_extract bic opts c mname = do
           case res of
             Crucible.FinishedResult _ pr -> do
               gp <- getGlobalPair opts pr
-              t <- Crucible.asSymExpr
-                   (gp^.Crucible.gpValue)
-                   (CrucibleSAW.toSC sym)
-                   (fail $ unwords ["Unexpected return type:",
-                                    show (Crucible.regType (gp^.Crucible.gpValue))])
-              t' <- scAbstractExts sc (toList ecs) t
-              mkTypedTerm sc t'
+              let regval = gp^.Crucible.gpValue
+              let regty = Crucible.regType regval
+              let failure = fail $ unwords ["Unexpected return type:", show regty]
+              t <- Crucible.asSymExpr regval (CrucibleSAW.toSC sym) failure
+              cty <-
+                case Crucible.asBaseType regty of
+                  Crucible.NotBaseType -> failure
+                  Crucible.AsBaseType bt ->
+                    case baseCryptolType bt of
+                      Nothing -> failure
+                      Just cty -> return cty
+              t' <- scAbstractExts sc (map snd (toList ecs)) t
+              let cty' = foldr Cryptol.tFun cty (map fst (toList ecs))
+              return $ TypedTerm (Cryptol.tMono cty') t'
             Crucible.AbortedResult _ _ar -> do
               fail $ unlines [ "Symbolic execution failed." ]
             Crucible.TimeoutResult _cxt -> do

src/SAWScript/Crucible/JVM/Override.hs

@@ -384,8 +384,8 @@ refreshTerms sc ss =
   where
     freshenTerm tt =
       case asExtCns (ttTerm tt) of
-        Just ec -> do new <- liftIO (mkTypedTerm sc =<< scFreshGlobal sc (ecName ec) (ecType ec))
-                      return (termId (ttTerm tt), ttTerm new)
+        Just ec -> do new <- liftIO (scFreshGlobal sc (ecName ec) (ecType ec))
+                      return (termId (ttTerm tt), new)
         Nothing -> error "refreshTerms: not a variable"
 
 ------------------------------------------------------------------------

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -62,6 +62,7 @@ module SAWScript.Crucible.LLVM.Builtins
     , setupArgs
     , getGlobalPair
     , runCFG
+    , baseCryptolType
 
     , displayVerifExceptionOpts
     , findDecl
@@ -155,6 +156,8 @@ import Verifier.SAW.FiniteValue (ppFirstOrderValue)
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.TypedAST
 import Verifier.SAW.Recognizer
+
+-- cryptol-verifier
 import Verifier.SAW.TypedTerm
 
 -- saw-script
@@ -1269,44 +1272,75 @@ setupLLVMCrucibleContext bic opts lm action =
 
 --------------------------------------------------------------------------------
 
+baseCryptolType :: Crucible.BaseTypeRepr tp -> Maybe Cryptol.Type
+baseCryptolType bt =
+  case bt of
+    Crucible.BaseBoolRepr -> pure $ Cryptol.tBit
+    Crucible.BaseBVRepr w -> pure $ Cryptol.tWord (Cryptol.tNum (natValue w))
+    Crucible.BaseNatRepr  -> Nothing
+    Crucible.BaseIntegerRepr -> pure $ Cryptol.tInteger
+    Crucible.BaseArrayRepr indexTypes range ->
+      do ts <- baseCryptolTypes indexTypes
+         t <- baseCryptolType range
+         pure $ foldr Cryptol.tFun t ts
+    Crucible.BaseFloatRepr _ -> Nothing
+    Crucible.BaseStringRepr _ -> Nothing
+    Crucible.BaseComplexRepr  -> Nothing
+    Crucible.BaseRealRepr     -> Nothing
+    Crucible.BaseStructRepr ts ->
+      Cryptol.tTuple <$> baseCryptolTypes ts
+  where
+    baseCryptolTypes :: Ctx.Assignment Crucible.BaseTypeRepr args -> Maybe [Cryptol.Type]
+    baseCryptolTypes Ctx.Empty = pure []
+    baseCryptolTypes (xs Ctx.:> x) =
+      do ts <- baseCryptolTypes xs
+         t <- baseCryptolType x
+         pure (ts ++ [t])
+
 setupArg ::
   forall tp.
   SharedContext ->
   Sym ->
-  IORef (Seq (ExtCns Term)) ->
+  IORef (Seq (Cryptol.Type, ExtCns Term)) ->
   Crucible.TypeRepr tp ->
   IO (Crucible.RegEntry Sym tp)
 setupArg sc sym ecRef tp =
   case (Crucible.asBaseType tp, tp) of
     (Crucible.AsBaseType btp, _) ->
-      do sc_tp <- CrucibleSAW.baseSCType sym sc btp
-         t     <- freshGlobal sc_tp
+      do cty <-
+           case baseCryptolType btp of
+             Just cty -> pure cty
+             Nothing ->
+               fail $ unwords ["Unsupported type for Crucible extraction:", show btp]
+         sc_tp <- CrucibleSAW.baseSCType sym sc btp
+         t     <- freshGlobal cty sc_tp
          elt   <- CrucibleSAW.bindSAWTerm sym btp t
          return (Crucible.RegEntry tp elt)
 
     (Crucible.NotBaseType, Crucible.LLVMPointerRepr w) ->
-      do sc_tp <- scBitvector sc (natValue w)
-         t     <- freshGlobal sc_tp
+      do let cty = Cryptol.tWord (Cryptol.tNum (natValue w))
+         sc_tp <- scBitvector sc (natValue w)
+         t     <- freshGlobal cty sc_tp
          elt   <- CrucibleSAW.bindSAWTerm sym (Crucible.BaseBVRepr w) t
          elt'  <- Crucible.llvmPointer_bv sym elt
          return (Crucible.RegEntry tp elt')
 
     (Crucible.NotBaseType, _) ->
       fail $ unwords ["Crucible extraction currently only supports Crucible base types", show tp]
   where
-    freshGlobal sc_tp =
+    freshGlobal cty sc_tp =
       do i     <- scFreshGlobalVar sc
          ecs   <- readIORef ecRef
          let len = Seq.length ecs
          let ec = EC i ("arg_"++show len) sc_tp
-         writeIORef ecRef (ecs Seq.|> ec)
+         writeIORef ecRef (ecs Seq.|> (cty, ec))
          scFlatTermF sc (ExtCns ec)
 
 setupArgs ::
   SharedContext ->
   Sym ->
   Crucible.FnHandle init ret ->
-  IO (Seq (ExtCns Term), Crucible.RegMap Sym init)
+  IO (Seq (Cryptol.Type, ExtCns Term), Crucible.RegMap Sym init)
 setupArgs sc sym fn =
   do ecRef  <- newIORef Seq.empty
      regmap <- Crucible.RegMap <$> Ctx.traverseFC (setupArg sc sym ecRef) (Crucible.handleArgTypes fn)
@@ -1357,15 +1391,21 @@ extractFromLLVMCFG opts sc cc (Crucible.AnyCFG cfg) =
             let regv = gp^.Crucible.gpValue
                 rt = Crucible.regType regv
                 rv = Crucible.regValue regv
-            t <-
+            (cty, t) <-
               case rt of
-                Crucible.LLVMPointerRepr _ ->
+                Crucible.LLVMPointerRepr w ->
                   do bv <- Crucible.projectLLVM_bv sym rv
-                     CrucibleSAW.toSC sym bv
-                Crucible.BVRepr _ -> CrucibleSAW.toSC sym rv
+                     t <- CrucibleSAW.toSC sym bv
+                     let cty = Cryptol.tWord (Cryptol.tNum (natValue w))
+                     return (cty, t)
+                Crucible.BVRepr w ->
+                  do t <- CrucibleSAW.toSC sym rv
+                     let cty = Cryptol.tWord (Cryptol.tNum (natValue w))
+                     return (cty, t)
                 _ -> fail $ unwords ["Unexpected return type:", show rt]
-            t' <- scAbstractExts sc (toList ecs) t
-            mkTypedTerm sc t'
+            t' <- scAbstractExts sc (map snd (toList ecs)) t
+            let cty' = foldr Cryptol.tFun cty (map fst (toList ecs))
+            return $ TypedTerm (Cryptol.tMono cty') t'
        Crucible.AbortedResult _ ar ->
          do let resultDoc = ppAbortedResult cc ar
             fail $ unlines [ "Symbolic execution failed."

src/SAWScript/ImportAIG.hs

@@ -178,21 +178,20 @@ loadAIG p f = do
       Left e -> return (Left (show (e :: IOException)))
       Right ntk -> return $ Right ntk
 
+-- | The return tuple consists of (input bits, output bits, term).
 readAIG :: (AIG.IsAIG l g) =>
            AIG.Proxy l g
         -> Options
         -> SharedContext
         -> FilePath
-        -> IO (Either String Term)
+        -> IO (Either String (Int, Int, Term))
 readAIG proxy opts sc f =
   withReadAiger proxy f $ \(AIG.Network ntk outputLits) -> do
-    inputs <- AIG.inputCount ntk
-    inLen <- scNat sc (fromIntegral inputs)
-    outLen <- scNat sc (fromIntegral (length outputLits))
-    boolType <- scBoolType sc
-    inType <- scVecType sc inLen boolType
-    outType <- scVecType sc outLen boolType
-    runExceptT $
+    inLen <- AIG.inputCount ntk
+    let outLen = length outputLits
+    inType <- scBitvector sc (fromIntegral inLen)
+    outType <- scBitvector sc (fromIntegral outLen)
+    fmap (fmap (\t -> (inLen, outLen, t))) $ runExceptT $
       translateNetwork opts sc ntk outputLits [("x", inType)] outType
 
 -- | Check that the input and output counts of the given

src/SAWScript/JavaBuiltins.hs

@@ -34,7 +34,7 @@ import Verifier.Java.Codebase hiding (lookupClass)
 import Verifier.Java.Simulator as JSS hiding (lookupClass)
 import Verifier.Java.SAWBackend
 
-import Verifier.SAW.Cryptol (exportFirstOrderValue)
+import Verifier.SAW.Cryptol (importType, emptyEnv, exportFirstOrderValue)
 import Verifier.SAW.Recognizer
 import Verifier.SAW.FiniteValue (FirstOrderValue)
 import Verifier.SAW.SCTypeCheck hiding (TypedTerm)
@@ -367,9 +367,8 @@ checkCompatibleType
   -> JavaActualType
   -> Cryptol.Schema
   -> JavaSetup ()
-checkCompatibleType sc msg aty schema = do
-  cty <- liftIO $ cryptolTypeOfActual sc aty
-  case cty of
+checkCompatibleType _sc msg aty schema =
+  case cryptolTypeOfActual aty of
     Nothing ->
       throwJava $ "Type is not translatable: " ++ show aty ++ " (" ++ msg ++ ")"
     Just lt -> do
@@ -457,9 +456,13 @@ javaVar bic _ name t = do
     _ -> return ()
   modifySpec (specAddVarDecl expr aty)
   let sc = biSharedContext bic
-  liftIO $ do
-    Just lty <- narrowTypeOfActual sc aty
-    scJavaValue sc lty name >>= mkTypedTerm sc
+  case cryptolTypeOfActual aty of
+    Nothing -> throwJava $ "Unsupported type for `java_var`: " ++ show aty
+    Just cty ->
+      liftIO $
+      do lty <- importType sc emptyEnv cty
+         v <- scJavaValue sc lty name
+         return $ TypedTerm (Cryptol.tMono cty) v
 
 javaMayAlias :: [String] -> JavaSetup ()
 javaMayAlias exprs = do

src/SAWScript/JavaExpr.hs

@@ -266,37 +266,34 @@ javaTypeToActual tp
   | JSS.isPrimitiveType tp = Just (PrimitiveType tp)
   | otherwise = Nothing
 
-narrowTypeOfActual :: SharedContext -> JavaActualType
-                  -> IO (Maybe Term)
-narrowTypeOfActual _ (ClassInstance _) = return Nothing
-narrowTypeOfActual sc (ArrayInstance l tp) = do
-  case javaTypeToActual tp of
-    Just at -> do
-      melTy <- narrowTypeOfActual sc  at
-      case melTy of
-        Just elTy -> do
-          lTm <- scNat sc (fromIntegral l)
-          Just <$> scVecType sc lTm elTy
-        Nothing -> return Nothing
+narrowTypeOfActual :: SharedContext -> JavaActualType -> IO (Maybe Term)
+narrowTypeOfActual sc at =
+  case cryptolTypeOfActual at of
     Nothing -> return Nothing
-narrowTypeOfActual sc (PrimitiveType JSS.BooleanType) =
-  Just <$> scBoolType sc
-narrowTypeOfActual sc (PrimitiveType JSS.ByteType) =
-  Just <$> scBitvector sc 8
-narrowTypeOfActual sc (PrimitiveType JSS.CharType) =
-  Just <$> scBitvector sc 16
-narrowTypeOfActual sc (PrimitiveType JSS.ShortType) =
-  Just <$> scBitvector sc 16
-narrowTypeOfActual sc (PrimitiveType JSS.IntType) =
-  Just <$> scBitvector sc 32
-narrowTypeOfActual sc (PrimitiveType JSS.LongType) =
-  Just <$> scBitvector sc 64
-narrowTypeOfActual _ _ = return Nothing
-
-cryptolTypeOfActual :: SharedContext -> JavaActualType -> IO (Maybe Cryptol.Type)
-cryptolTypeOfActual sc ty = do
-  mnty <- narrowTypeOfActual sc ty
-  maybe (return Nothing) (\nty -> Just <$> scCryptolType sc nty) mnty
+    Just cty ->
+      do t <- importType sc emptyEnv cty
+         return (Just t)
+
+cryptolTypeOfActual :: JavaActualType -> Maybe Cryptol.Type
+cryptolTypeOfActual ty =
+  case ty of
+    ClassInstance _ -> Nothing
+    ArrayInstance l tp ->
+      do at <- javaTypeToActual tp
+         ct <- cryptolTypeOfActual at
+         Just (Cryptol.tSeq (Cryptol.tNum l) ct)
+    PrimitiveType pt ->
+      case pt of
+        JSS.BooleanType -> Just $ Cryptol.tBit
+        JSS.ByteType    -> Just $ Cryptol.tWord (Cryptol.tNum (8 :: Integer))
+        JSS.CharType    -> Just $ Cryptol.tWord (Cryptol.tNum (16 :: Integer))
+        JSS.ShortType   -> Just $ Cryptol.tWord (Cryptol.tNum (16 :: Integer))
+        JSS.IntType     -> Just $ Cryptol.tWord (Cryptol.tNum (32 :: Integer))
+        JSS.LongType    -> Just $ Cryptol.tWord (Cryptol.tNum (64 :: Integer))
+        JSS.ArrayType _ -> Nothing
+        JSS.ClassType _ -> Nothing
+        JSS.DoubleType  -> Nothing
+        JSS.FloatType   -> Nothing
 
 ppActualType :: JavaActualType -> String
 ppActualType (ClassInstance x) = JSS.slashesToDots (JSS.unClassName (JSS.className x))