From f7bb9487146af501f255b5a90d8c737a8c12c81c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sun, 17 May 2020 17:31:43 -0700 Subject: [PATCH 1/8] Remove unnecessary calls to `mkTypedTerm`. This is a step toward fixing #718. The use of mkTypedTerm is redundant in these cases in the SAWScript.Prover modules, as the computed schema in all cases is only used to check that the return type is Bool, and the prior calls to `propToPredicate` already ensure that. --- src/SAWScript/Prover/ABC.hs | 7 ++----- src/SAWScript/Prover/RME.hs | 5 +---- src/SAWScript/Prover/SBV.hs | 7 +------ src/SAWScript/Prover/What4.hs | 6 +----- 4 files changed, 5 insertions(+), 20 deletions(-) diff --git a/src/SAWScript/Prover/ABC.hs b/src/SAWScript/Prover/ABC.hs index 50e9820731..a7a8bad4d2 100644 --- a/src/SAWScript/Prover/ABC.hs +++ b/src/SAWScript/Prover/ABC.hs @@ -4,7 +4,6 @@ module SAWScript.Prover.ABC (proveABC) where import qualified Data.AIG as AIG import Verifier.SAW.SharedTerm -import Verifier.SAW.TypedTerm import Verifier.SAW.FiniteValue import qualified Verifier.SAW.Simulator.BitBlast as BBSim @@ -12,7 +11,7 @@ import SAWScript.Proof(Prop, propToPredicate) import SAWScript.Prover.SolverStats (SolverStats, solverStats) import SAWScript.Prover.Rewrite(rewriteEqs) import SAWScript.Prover.Util - (liftCexBB, bindAllExts, checkBooleanSchema) + (liftCexBB, bindAllExts) -- | Bit-blast a proposition and check its validity using ABC. proveABC :: @@ -23,9 +22,7 @@ proveABC :: IO (Maybe [(String, FirstOrderValue)], SolverStats) proveABC proxy sc goal = do t0 <- propToPredicate sc goal - TypedTerm schema t <- - (bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc) - checkBooleanSchema schema + t <- bindAllExts sc t0 >>= rewriteEqs sc BBSim.withBitBlastedPred proxy sc mempty t $ \be lit0 shapes -> do let lit = AIG.not lit0 diff --git a/src/SAWScript/Prover/RME.hs b/src/SAWScript/Prover/RME.hs index 6ee3f784e7..c4f8f0a5d5 100644 --- a/src/SAWScript/Prover/RME.hs +++ b/src/SAWScript/Prover/RME.hs @@ -7,7 +7,6 @@ import Verifier.SAW.FiniteValue import qualified Verifier.SAW.Simulator.RME as RME import qualified Verifier.SAW.Simulator.RME.Base as RME -import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm) import Verifier.SAW.Recognizer(asPiList) import SAWScript.Proof(Prop, propToPredicate) @@ -22,9 +21,7 @@ proveRME :: IO (Maybe [(String, FirstOrderValue)], SolverStats) proveRME sc goal = do t0 <- propToPredicate sc goal - TypedTerm schema t <- - bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc - checkBooleanSchema schema + t <- bindAllExts sc t0 >>= rewriteEqs sc tp <- scWhnf sc =<< scTypeOf sc t let (args, _) = asPiList tp argNames = map fst args diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs index 83dd7b8347..4b5095970e 100644 --- a/src/SAWScript/Prover/SBV.hs +++ b/src/SAWScript/Prover/SBV.hs @@ -20,14 +20,11 @@ import qualified Verifier.SAW.Simulator.SBV as SBVSim import Verifier.SAW.SharedTerm import Verifier.SAW.FiniteValue -import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm) import Verifier.SAW.Recognizer(asPi, asPiList) import SAWScript.Proof(Prop, propToPredicate) import SAWScript.Prover.SolverStats import SAWScript.Prover.Rewrite(rewriteEqs) -import SAWScript.Prover.Util(checkBooleanSchema) - -- | Bit-blast a proposition and check its validity using SBV. @@ -93,10 +90,8 @@ prepNegatedSBV sc unints goal = let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e)) exts <- filterM nonFun (getAllExts t0) - TypedTerm schema t' <- - scAbstractExts sc exts t0 >>= rewriteEqs sc >>= mkTypedTerm sc + t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc - checkBooleanSchema schema (labels, lit) <- SBVSim.sbvSolve sc mempty unints t' let lit' = liftM SBV.svNot lit return (t', labels, lit') diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs index 772ec75c54..1945a97e11 100644 --- a/src/SAWScript/Prover/What4.hs +++ b/src/SAWScript/Prover/What4.hs @@ -13,13 +13,11 @@ import Data.Maybe (catMaybes) import Verifier.SAW.SharedTerm import Verifier.SAW.FiniteValue -import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm) import Verifier.SAW.Recognizer(asPi) import SAWScript.Proof(Prop, propToPredicate) import SAWScript.Prover.Rewrite(rewriteEqs) import SAWScript.Prover.SolverStats -import SAWScript.Prover.Util import Data.Parameterized.Nonce @@ -119,10 +117,8 @@ prepWhat4 sym sc unints t0 = do let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e)) exts <- filterM nonFun (getAllExts t0) - TypedTerm schema t' <- - scAbstractExts sc exts t0 >>= rewriteEqs sc >>= mkTypedTerm sc + t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc - checkBooleanSchema schema (argNames, lit) <- W.w4Solve sym sc mempty unints t' return (t', argNames, lit) From 3747a88f39eddec4a0affba2bdd52cf279e97c6a Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 18 May 2020 22:09:29 -0700 Subject: [PATCH 2/8] Remove completely unnecessary call to `mkTypedTerm`. --- src/SAWScript/Crucible/JVM/Override.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 2ba7f68c29..3eabe4c398 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/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" ------------------------------------------------------------------------ From 1ecb24c0490ef2f2e92e5085f3b15c5c955702cd Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 18 May 2020 22:51:47 -0700 Subject: [PATCH 3/8] Reimplement some java-related code to avoid `mkTypedTerm`. --- src/SAWScript/JavaBuiltins.hs | 17 ++++++----- src/SAWScript/JavaExpr.hs | 57 +++++++++++++++++------------------ 2 files changed, 37 insertions(+), 37 deletions(-) diff --git a/src/SAWScript/JavaBuiltins.hs b/src/SAWScript/JavaBuiltins.hs index 72b1d0266f..ed8ad93791 100644 --- a/src/SAWScript/JavaBuiltins.hs +++ b/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 diff --git a/src/SAWScript/JavaExpr.hs b/src/SAWScript/JavaExpr.hs index bd3d04354d..e54bde2570 100644 --- a/src/SAWScript/JavaExpr.hs +++ b/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)) From 0686429bf37bf65b1fad6b655034afe3da3e9ee4 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 19 May 2020 10:51:25 -0700 Subject: [PATCH 4/8] Remove uses of `mkTypedTerm` in case{Proof,Sat}ResultPrim. --- src/SAWScript/Builtins.hs | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 3b274d7f69..08257eaf87 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -55,6 +55,8 @@ import Verifier.SAW.Grammar (parseSAWTerm) import Verifier.SAW.ExternalFormat import Verifier.SAW.FiniteValue ( FiniteType(..), readFiniteValue + , FirstOrderType(..) + , firstOrderTypeOf , FirstOrderValue(..) , toFirstOrderValue, scFirstOrderValue ) @@ -1020,6 +1022,18 @@ 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) + FOTRec m -> + C.tRec + [ (C.packIdent l, cryptolTypeOfFirstOrderType t) + | (l, t) <- Map.assocs m ] + caseProofResultPrim :: SV.ProofResult -> SV.Value -> SV.Value -> TopLevel SV.Value @@ -1031,7 +1045,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 @@ -1045,7 +1061,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 () From ea5fd43fc2c6b8d2c44c9503f5e9b42b32c2540c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 20 May 2020 14:19:14 -0700 Subject: [PATCH 5/8] Rewrite crucible llvm/jvm extract functions to avoid `mkTypedTerm`. --- src/SAWScript/Crucible/JVM/BuiltinsJVM.hs | 30 +++++++--- src/SAWScript/Crucible/LLVM/Builtins.hs | 68 ++++++++++++++++++----- 2 files changed, 75 insertions(+), 23 deletions(-) diff --git a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs index 09027c2552..67ed14fec2 100644 --- a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs +++ b/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(..), mkTypedTerm) -- 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 diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 65fdd31a7a..958f7624a6 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -59,6 +59,7 @@ module SAWScript.Crucible.LLVM.Builtins , setupArgs , getGlobalPair , runCFG + , baseCryptolType , displayVerifExceptionOpts , findDecl @@ -148,6 +149,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 @@ -1247,24 +1250,55 @@ 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') @@ -1272,19 +1306,19 @@ setupArg sc sym ecRef tp = (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) @@ -1335,15 +1369,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." From faadf2650da96ca6dc1950c19e615600ef0317d1 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 3 Aug 2020 15:15:02 -0700 Subject: [PATCH 6/8] Adapt to changes in `FirstOrderType` datatype from saw-core. This makes saw-script compile successfully again, after being broken by the most recent merge. --- src/SAWScript/Builtins.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 2afb017498..bc06f0647d 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1043,8 +1043,13 @@ cryptolTypeOfFirstOrderType fot = 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.tRec $ + C.recordFromFields $ [ (C.packIdent l, cryptolTypeOfFirstOrderType t) | (l, t) <- Map.assocs m ] From f3801fa84aa5d4f8869a41410efbe2625b2ec6ce Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 4 Aug 2020 12:57:01 -0700 Subject: [PATCH 7/8] Make `readAIG` return input and output bitwidths along with term. This lets us remove another use of `mkTypedTerm` from `readAIGPrim`. --- src/SAWScript/Builtins.hs | 6 +++++- src/SAWScript/ImportAIG.hs | 15 +++++++-------- 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index bc06f0647d..a231fed248 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -269,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 diff --git a/src/SAWScript/ImportAIG.hs b/src/SAWScript/ImportAIG.hs index 9889e9ece2..c8fa34d7d4 100644 --- a/src/SAWScript/ImportAIG.hs +++ b/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 From 99d15ff075d6542620e92e95d37ab0a78f58f8bf Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 4 Aug 2020 13:22:36 -0700 Subject: [PATCH 8/8] Remove unused import. --- src/SAWScript/Crucible/JVM/BuiltinsJVM.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs index 67ed14fec2..66de17aa9e 100644 --- a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs +++ b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs @@ -67,7 +67,7 @@ import qualified What4.Solver.Yices as Yices import Verifier.SAW.SharedTerm(Term, SharedContext, mkSharedContext, scImplies, scAbstractExts) -- cryptol-verifier -import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm) +import Verifier.SAW.TypedTerm(TypedTerm(..)) -- saw-script import SAWScript.Builtins(fixPos)