diff --git a/cryptol-saw-core/css/Main.hs b/cryptol-saw-core/css/Main.hs index 7dec5cc4..0517eb14 100644 --- a/cryptol-saw-core/css/Main.hs +++ b/cryptol-saw-core/css/Main.hs @@ -22,7 +22,7 @@ import Cryptol.Utils.Logger (quietLogger) import qualified Verifier.SAW.Cryptol as C import Verifier.SAW.SharedTerm import qualified Verifier.SAW.Cryptol.Prelude as C -import Verifier.SAW.CryptolEnv (schemaNoUser) +import Verifier.SAW.CryptolEnv (schemaNoUser, meSolverConfig) import qualified Data.ABC as ABC @@ -92,7 +92,7 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do modEnv <- CM.initialModuleEnv let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv (e,warn) <- - SMT.withSolver (CME.meSolverConfig modEnv) $ \s -> + SMT.withSolver (meSolverConfig modEnv) $ \s -> CM.loadModuleByPath inputModule (minp s) mapM_ (print . pp) warn case e of @@ -133,7 +133,7 @@ extractCryptol sc modEnv input = do Right x -> return x let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv (exprResult, exprWarnings) <- - SMT.withSolver (CME.meSolverConfig modEnv) $ \s -> + SMT.withSolver (meSolverConfig modEnv) $ \s -> CM.checkExpr pexpr (minp s) mapM_ (print . pp) exprWarnings ((_, expr, schema), _modEnv') <- diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 6a1487d8..6d081c51 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/cryptol-saw-core/saw/Cryptol.sawcore @@ -1208,22 +1208,37 @@ ecCat = -- Case for (TCNum m, TCInf) (\ (a:sort 0) -> streamAppend a m)); -ecSplitAt : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> - #(seq m a, seq n a); -ecSplitAt = +ecTake : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq m a; +ecTake = + Num_rec + (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq m a) + + (\ (m:Nat) -> + Num_rec + (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> Vec m a) + -- The case (TCNum m, TCNum n) + (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> take a m n xs) + -- The case (TCNum m, infinity) + (\ (a:sort 0) -> \ (xs: Stream a) -> streamTake a m xs)) + + (Num_rec + (\ (n:Num) -> (a:sort 0) -> seq (tcAdd TCInf n) a -> Stream a) + -- The case (TCInf, TCNum n) + (\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs) + -- The case (TCInf, TCInf) + (\ (a:sort 0) -> \ (xs:Stream a) -> xs)); + +ecDrop : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq n a; +ecDrop = finNumRec - (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> - #(seq m a, seq n a)) + (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq n a) (\ (m:Nat) -> Num_rec - (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> - #(Vec m a, seq n a)) + (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> seq n a) -- The case (TCNum n, TCNum m) - (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> - (take a m n xs, drop a m n xs)) + (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> drop a m n xs) -- The case (TCNum m, infinity) - (\ (a:sort 0) -> \ (xs: Stream a) -> - (streamTake a m xs, streamDrop a m xs))); + (\ (a:sort 0) -> \ (xs: Stream a) -> streamDrop a m xs)); ecJoin : (m n : Num) -> (a : sort 0) -> seq m (seq n a) -> seq (tcMul m n) a; ecJoin m = diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 2e293779..3eaf98ac 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -35,6 +35,8 @@ import Text.URI import qualified Cryptol.Eval.Type as TV import qualified Cryptol.Backend.Monad as V +import qualified Cryptol.Backend.SeqMap as V +import qualified Cryptol.Backend.WordValue as V import qualified Cryptol.Eval.Value as V import qualified Cryptol.Eval.Concrete as V import Cryptol.Eval.Type (evalValType) @@ -45,6 +47,7 @@ import qualified Cryptol.ModuleSystem.Name as C import qualified Cryptol.Utils.Ident as C ( Ident, PrimIdent(..), mkIdent, prelPrim, floatPrim, arrayPrim , ModName, modNameToText, identText, interactiveName + , ModPath(..), modPathSplit ) import qualified Cryptol.Utils.RecordMap as C import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf) @@ -740,7 +743,8 @@ prelPrims = -- -- Sequences primitives , ("#", flip scGlobalDef "Cryptol.ecCat") -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d - , ("splitAt", flip scGlobalDef "Cryptol.ecSplitAt") -- {a,b,c} (fin a) => [a+b] c -> ([a]c,[b]c) + , ("take", flip scGlobalDef "Cryptol.ecTake") -- {front, back, a} [front + back]a -> [front]a + , ("drop", flip scGlobalDef "Cryptol.ecDrop") -- {front, back, a} (fin front) => [front + back]a -> [back]a , ("join", flip scGlobalDef "Cryptol.ecJoin") -- {a,b,c} (fin b) => [a][b]c -> [a * b]c , ("split", flip scGlobalDef "Cryptol.ecSplit") -- {a,b,c} (fin b) => [a * b] c -> [a][b] c , ("reverse", flip scGlobalDef "Cryptol.ecReverse") -- {a,b} (fin a) => [a] b -> [a] b @@ -1231,18 +1235,20 @@ importName cnm = case C.nameInfo cnm of C.Parameter -> fail ("Cannot import non-top-level name: " ++ show cnm) C.Declared modNm _ - | modNm == C.interactiveName -> + | modNm == C.TopModule C.interactiveName -> let shortNm = C.identText (C.nameIdent cnm) aliases = [shortNm] uri = cryptolURI [shortNm] (Just (C.nameUnique cnm)) in pure (ImportedName uri aliases) | otherwise -> - let modNmTxt = C.modNameToText modNm - modNms = Text.splitOn "::" modNmTxt - shortNm = C.identText (C.nameIdent cnm) - aliases = [shortNm, modNmTxt <> "::" <> shortNm] - uri = cryptolURI (modNms ++ [shortNm]) Nothing + let (topMod, nested) = C.modPathSplit modNm + modNmTxt = C.modNameToText topMod + modNms = (Text.splitOn "::" modNmTxt) ++ map C.identText nested + shortNm = C.identText (C.nameIdent cnm) + longNm = Text.intercalate "::" ([modNmTxt] ++ map C.identText nested ++ [shortNm]) + aliases = [shortNm, longNm] + uri = cryptolURI (modNms ++ [shortNm]) Nothing in pure (ImportedName uri aliases) -- | Currently this imports declaration groups by inlining all the @@ -1639,22 +1645,22 @@ scCryptolEq sc x y = -- | Convert from SAWCore's Value type to Cryptol's, guided by the -- Cryptol type schema. -exportValueWithSchema :: C.Schema -> SC.CValue -> V.Value +exportValueWithSchema :: C.Schema -> SC.CValue -> V.Eval V.Value exportValueWithSchema (C.Forall [] [] ty) v = exportValue (evalValType mempty ty) v -exportValueWithSchema _ _ = V.VPoly mempty (error "exportValueWithSchema") +exportValueWithSchema _ _ = pure (V.VPoly mempty (error "exportValueWithSchema")) -- TODO: proper support for polymorphic values -exportValue :: TV.TValue -> SC.CValue -> V.Value +exportValue :: TV.TValue -> SC.CValue -> V.Eval V.Value exportValue ty v = case ty of TV.TVBit -> - V.VBit (SC.toBool v) + pure (V.VBit (SC.toBool v)) TV.TVInteger -> - V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer") + pure (V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer")) TV.TVIntMod _modulus -> - V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod") + pure (V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod")) TV.TVArray{} -> error $ "exportValue: (on array type " ++ show ty ++ ")" @@ -1666,28 +1672,29 @@ exportValue ty v = case ty of case v of SC.VWord w -> V.word V.Concrete (toInteger (width w)) (unsigned w) SC.VVector xs - | TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) (V.ready (V.LargeBitsVal (fromIntegral (Vector.length xs)) - (V.finiteSeqMap . map (V.ready . V.VBit . SC.toBool . SC.runIdentity . force) $ Fold.toList xs))) - | otherwise -> V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap $ - map (V.ready . exportValue e . SC.runIdentity . force) $ Vector.toList xs + | TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) <$> + V.bitmapWordVal V.Concrete (toInteger (Vector.length xs)) + (V.finiteSeqMap V.Concrete . map (V.ready . SC.toBool . SC.runIdentity . force) $ Fold.toList xs) + | otherwise -> pure . V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap V.Concrete $ + map (\x -> exportValue e (SC.runIdentity (force x))) (Vector.toList xs) _ -> error $ "exportValue (on seq type " ++ show ty ++ ")" -- infinite streams TV.TVStream e -> case v of - SC.VExtra (SC.CStream trie) -> V.VStream (V.IndexSeqMap $ \i -> V.ready $ exportValue e (IntTrie.apply trie i)) + SC.VExtra (SC.CStream trie) -> pure $ V.VStream (V.indexSeqMap $ \i -> exportValue e (IntTrie.apply trie i)) _ -> error $ "exportValue (on seq type " ++ show ty ++ ")" -- tuples - TV.TVTuple etys -> V.VTuple (exportTupleValue etys v) + TV.TVTuple etys -> pure $ V.VTuple $ exportTupleValue etys v -- records TV.TVRec fields -> - V.VRecord (C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v) + pure . V.VRecord . C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v -- functions TV.TVFun _aty _bty -> - V.VFun mempty (error "exportValue: TODO functions") + pure $ V.VFun mempty (error "exportValue: TODO functions") -- abstract types TV.TVAbstract{} -> @@ -1702,8 +1709,8 @@ exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value] exportTupleValue tys v = case (tys, v) of ([] , SC.VUnit ) -> [] - ([t] , _ ) -> [V.ready $ exportValue t v] - (t : ts, SC.VPair x y) -> (V.ready $ exportValue t (run x)) : exportTupleValue ts (run y) + ([t] , _ ) -> [exportValue t v] + (t : ts, SC.VPair x y) -> (exportValue t (run x)) : exportTupleValue ts (run y) _ -> error $ "exportValue: expected tuple" where run = SC.runIdentity . force @@ -1712,12 +1719,11 @@ exportRecordValue :: [(C.Ident, TV.TValue)] -> SC.CValue -> [(C.Ident, V.Eval V. exportRecordValue fields v = case (fields, v) of ([] , SC.VUnit ) -> [] - ([(n, t)] , _ ) -> [(n, V.ready $ exportValue t v)] - ((n, t) : ts, SC.VPair x y) -> - (n, V.ready $ exportValue t (run x)) : exportRecordValue ts (run y) + ([(n, t)] , _ ) -> [(n, exportValue t v)] + ((n, t) : ts, SC.VPair x y) -> (n, exportValue t (run x)) : exportRecordValue ts (run y) (_, SC.VRecordValue (alistAllFields (map (C.identText . fst) fields) -> Just ths)) -> - zipWith (\(n,t) x -> (n, V.ready $ exportValue t (run x))) fields ths + zipWith (\(n,t) x -> (n, exportValue t (run x))) fields ths _ -> error $ "exportValue: expected record" where run = SC.runIdentity . force @@ -1726,20 +1732,23 @@ fvAsBool :: FirstOrderValue -> Bool fvAsBool (FOVBit b) = b fvAsBool _ = error "fvAsBool: expected FOVBit value" -exportFirstOrderValue :: FirstOrderValue -> V.Value +exportFirstOrderValue :: FirstOrderValue -> V.Eval V.Value exportFirstOrderValue fv = case fv of - FOVBit b -> V.VBit b - FOVInt i -> V.VInteger i - FOVIntMod _ i -> V.VInteger i - FOVWord w x -> V.word V.Concrete (toInteger w) x + FOVBit b -> pure (V.VBit b) + FOVInt i -> pure (V.VInteger i) + FOVIntMod _ i -> pure (V.VInteger i) + FOVWord w x -> V.word V.Concrete (toInteger w) x FOVVec t vs - | t == FOTBit -> V.VWord len (V.ready (V.LargeBitsVal len (V.finiteSeqMap . map (V.ready . V.VBit . fvAsBool) $ vs))) - | otherwise -> V.VSeq len (V.finiteSeqMap (map (V.ready . exportFirstOrderValue) vs)) + | t == FOTBit -> V.VWord len <$> (V.bitmapWordVal V.Concrete len + (V.finiteSeqMap V.Concrete . map (V.ready . fvAsBool) $ vs)) + | otherwise -> pure (V.VSeq len (V.finiteSeqMap V.Concrete (map exportFirstOrderValue vs))) where len = toInteger (length vs) FOVArray{} -> error $ "exportFirstOrderValue: unsupported FOT Array" - FOVTuple vs -> V.VTuple (map (V.ready . exportFirstOrderValue) vs) - FOVRec vm -> V.VRecord $ C.recordFromFields [ (C.mkIdent n, V.ready $ exportFirstOrderValue v) | (n, v) <- Map.assocs vm ] + FOVTuple vs -> pure $ V.VTuple $ map exportFirstOrderValue vs + FOVRec vm -> + do let vm' = fmap exportFirstOrderValue vm + pure $ V.VRecord $ C.recordFromFields [ (C.mkIdent n, v) | (n, v) <- Map.assocs vm' ] importFirstOrderValue :: FirstOrderType -> V.Value -> IO FirstOrderValue importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0) @@ -1748,7 +1757,7 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0) go t v = case (t,v) of (FOTBit , V.VBit b) -> return (FOVBit b) (FOTInt , V.VInteger i) -> return (FOVInt i) - (FOTVec _ FOTBit, V.VWord w wv) -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete =<< wv) + (FOTVec _ FOTBit, V.VWord w wv) -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete wv) (FOTVec _ ty , V.VSeq len xs) -> FOVVec ty <$> traverse (go ty =<<) (V.enumerateSeqMap len xs) (FOTTuple tys , V.VTuple xs) -> FOVTuple <$> traverse (\(ty, x) -> go ty =<< x) (zip tys xs) (FOTRec fs , V.VRecord xs) -> diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 4d640ce7..5f3e0b9e 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -32,6 +32,7 @@ module Verifier.SAW.CryptolEnv , InputText(..) , lookupIn , resolveIdentifier + , meSolverConfig ) where @@ -152,7 +153,7 @@ nameMatcher xs = case modNameChunks (textToModName (pack xs)) of [] -> const False [x] -> (packIdent x ==) . MN.nameIdent - cs -> let m = MN.Declared (packModName (map pack (init cs))) MN.UserName + cs -> let m = MN.Declared (C.TopModule (packModName (map pack (init cs)))) MN.UserName i = packIdent (last cs) in \n -> MN.nameIdent n == i && MN.nameInfo n == m @@ -252,7 +253,7 @@ getNamingEnv env = eExtraNames env `MR.shadowing` nameEnv syms = case vis of OnlyPublic -> MI.ifPublic ifc PublicAndPrivate -> MI.ifPublic ifc `mappend` M.ifPrivate ifc - return $ MN.interpImport i syms + return $ MN.interpImportIface i syms getAllIfaceDecls :: ME.ModuleEnv -> M.IfaceDecls getAllIfaceDecls me = mconcat (map (both . ME.lmInterface) (ME.getLoadedModules (ME.meLoadedModules me))) @@ -363,13 +364,13 @@ loadCryptolModule sc env path = do newCryEnv <- C.importTopLevelDeclGroups sc oldCryEnv newDeclGroups newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv) - let names = MEx.eBinds (T.mExports m) -- :: Set T.Name + let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name let tm' = Map.filterWithKey (\k _ -> Set.member k names) $ Map.intersectionWith TypedTerm types newTermEnv let env' = env { eModuleEnv = modEnv'' , eTermEnv = newTermEnv } - let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.eTypes (T.mExports m))) (T.mTySyns m) + let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) (T.mTySyns m) return (CryptolModule sm' tm', env') bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv @@ -429,7 +430,7 @@ bindIdent ident env = (name, env') modEnv = eModuleEnv env supply = ME.meSupply modEnv fixity = Nothing - (name, supply') = MN.mkDeclared interactiveName MN.UserName ident fixity P.emptyRange supply + (name, supply') = MN.mkDeclared C.NSValue (C.TopModule interactiveName) MN.UserName ident fixity P.emptyRange supply modEnv' = modEnv { ME.meSupply = supply' } env' = env { eModuleEnv = modEnv' } @@ -466,6 +467,9 @@ bindInteger (ident, n) env = -------------------------------------------------------------------------------- +meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig +meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env) + resolveIdentifier :: (?fileReader :: FilePath -> IO ByteString) => CryptolEnv -> Text -> IO (Maybe T.Name) @@ -480,10 +484,10 @@ resolveIdentifier env nm = nameEnv = getNamingEnv env doResolve pnm = - SMT.withSolver (ME.meSolverConfig modEnv) $ \s -> + SMT.withSolver (meSolverConfig modEnv) $ \s -> do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv (res, _ws) <- MM.runModuleM (minp s) $ - MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm)) + MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar MR.NameUse pnm)) case res of Left _ -> pure Nothing Right (x,_) -> pure (Just x) @@ -544,18 +548,12 @@ parseDecls sc env input = do -- Convert from 'Decl' to 'TopDecl' so that types will be generalized let topdecls = [ P.Decl (P.TopLevel P.Public Nothing d) | d <- npdecls ] - -- Label each TopDecl with the "interactive" module for unique name generation - let (mdecls :: [MN.InModule (P.TopDecl P.PName)]) = map (MN.InModule interactiveName) topdecls - nameEnv1 <- MN.liftSupply (MN.namingEnv' mdecls) - -- Resolve names - let nameEnv = nameEnv1 `MR.shadowing` getNamingEnv env - (rdecls :: [P.TopDecl T.Name]) <- MM.interactive (MB.rename interactiveName nameEnv (traverse MR.rename topdecls)) + (_nenv, rdecls) <- MM.interactive (MB.rename interactiveName (getNamingEnv env) (MR.renameTopDecls interactiveName topdecls)) -- Create a Module to contain the declarations let rmodule = P.Module { P.mName = P.Located P.emptyRange interactiveName , P.mInstance = Nothing - , P.mImports = [] , P.mDecls = rdecls } @@ -623,7 +621,7 @@ declareName env mname input = do let modEnv = eModuleEnv env (cname, modEnv') <- liftModuleM modEnv $ MM.interactive $ - MN.liftSupply (MN.mkDeclared mname MN.UserName (P.getIdent pname) Nothing P.emptyRange) + MN.liftSupply (MN.mkDeclared C.NSValue (C.TopModule mname) MN.UserName (P.getIdent pname) Nothing P.emptyRange) let env' = env { eModuleEnv = modEnv' } return (cname, env') @@ -646,7 +644,7 @@ liftModuleM :: ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv) liftModuleM env m = do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader env - SMT.withSolver (ME.meSolverConfig env) $ \s -> + SMT.withSolver (meSolverConfig env) $ \s -> MM.runModuleM (minp s) m >>= moduleCmdResult defaultEvalOpts :: E.EvalOpts diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs index 0b4b216d..e166d024 100644 --- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs +++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs @@ -98,6 +98,8 @@ cryptolTypeOfFirstOrderType fot = FOTInt -> C.tInteger FOTIntMod n -> C.tIntMod (C.tNum n) FOTVec n t -> C.tSeq (C.tNum n) (cryptolTypeOfFirstOrderType t) + -- NB, special case, don't produce 1-tuples + FOTTuple [x] -> cryptolTypeOfFirstOrderType x FOTTuple ts -> C.tTuple (map cryptolTypeOfFirstOrderType ts) FOTArray a b -> C.tArray diff --git a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs index 9a2e742d..baf9bc76 100644 --- a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs +++ b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs @@ -18,7 +18,6 @@ Portability : non-portable (language extensions) module Verifier.SAW.Simulator.BitBlast ( BValue - , withBitBlastedPred , withBitBlastedTerm , withBitBlastedSATQuery ) where @@ -497,21 +496,7 @@ bitBlastTerm be sc addlPrims t = do shapes = argShapes ++ ecShapes return (bval', zip names shapes) --- | Bitblast a predicate and apply a function to the result. Supports --- @ExtCns@ subterms. -withBitBlastedPred :: AIG.IsAIG l g => AIG.Proxy l g -> - SharedContext -> - PrimMap l g -> - Term -> - (forall s. g s -> l s -> [(String, FiniteType)] -> IO a) -> IO a -withBitBlastedPred proxy sc addlPrims t c = AIG.withNewGraph proxy $ \be -> do - (bval, args) <- bitBlastTerm be sc addlPrims t - case bval of - VBool l -> c be l args - _ -> fail "Verifier.SAW.Simulator.BitBlast.bitBlast: non-boolean result type." - --- | Bitblast a term and apply a function to the result. Does not --- support @ExtCns@ subterms. +-- | Bitblast a term and apply a function to the result. withBitBlastedTerm :: AIG.IsAIG l g => AIG.Proxy l g -> SharedContext -> PrimMap l g -> diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index 947b57ec..d400089d 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -25,9 +25,7 @@ Stability : experimental Portability : non-portable (language extensions) -} module Verifier.SAW.Simulator.SBV - ( sbvSolve - , sbvSolveBasic - , sbvSATQuery + ( sbvSATQuery , SValue , Labeler(..) , sbvCodeGen_definition @@ -43,7 +41,6 @@ import Data.SBV.Dynamic import Verifier.SAW.Simulator.SBV.SWord import Control.Lens ((<&>)) -import qualified Control.Arrow as A import Data.Bits import Data.IORef @@ -632,42 +629,7 @@ mkUninterpreted :: Kind -> [SVal] -> String -> SVal mkUninterpreted k args nm = svUninterpreted k nm' Nothing args where nm' = "|" ++ nm ++ "|" -- enclose name to allow primes and other non-alphanum chars -asPredType :: TValue SBV -> IO [TValue SBV] -asPredType v = - case v of - VBoolType -> return [] - VPiType v1 f -> - do v2 <- f (error "asPredType: unsupported dependent SAW-Core type") - vs <- asPredType v2 - return (v1 : vs) - _ -> fail $ "non-boolean result type: " ++ show v - -vAsFirstOrderType :: TValue SBV -> Maybe FirstOrderType -vAsFirstOrderType v = - case v of - VBoolType - -> return FOTBit - VIntType - -> return FOTInt - VIntModType n - -> return (FOTIntMod n) - VVecType n v2 - -> FOTVec n <$> vAsFirstOrderType v2 - VUnitType - -> return (FOTTuple []) - VPairType v1 v2 - -> do t1 <- vAsFirstOrderType v1 - t2 <- vAsFirstOrderType v2 - case t2 of - FOTTuple ts -> return (FOTTuple (t1 : ts)) - _ -> return (FOTTuple [t1, t2]) - - VRecordType tps - -> (FOTRec <$> Map.fromList <$> - mapM (\(f,tp) -> (f,) <$> vAsFirstOrderType tp) tps) - _ -> Nothing - -sbvSATQuery :: SharedContext -> Map Ident SValue -> SATQuery -> IO ([Labeler], [Text.Text], Symbolic SBool) +sbvSATQuery :: SharedContext -> Map Ident SValue -> SATQuery -> IO ([Labeler], [ExtCns Term], Symbolic SBool) sbvSATQuery sc addlPrims query = do true <- liftIO (scBool sc True) t <- liftIO (foldM (scAnd sc) true (satAsserts query)) @@ -678,11 +640,9 @@ sbvSATQuery sc addlPrims query = flip evalStateT 0 $ unzip <$> mapM (newVars . snd) qvars - let varNames = map (toShortName . ecName . fst) qvars - m <- liftIO (scGetModuleMap sc) - return (labels, varNames, + return (labels, map fst qvars, do vars' <- sequence vars let varMap = Map.fromList (zip (map (ecVarIndex . fst) qvars) vars') @@ -703,29 +663,6 @@ sbvSATQuery sc addlPrims query = _ -> fail $ "sbvSATQuery: non-boolean result type. " ++ show bval ) -sbvSolve :: SharedContext - -> Map Ident SValue - -> Set VarIndex - -> Term - -> IO ([Maybe Labeler], Symbolic SBool) -sbvSolve sc addlPrims unintSet t = do - let eval = sbvSolveBasic sc addlPrims unintSet - ty <- eval =<< scTypeOf sc t - let lamNames = map (Text.unpack . fst) (fst (R.asLambdaList t)) - let varNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ] - let argNames = zipWith (++) varNames (map ("_" ++) lamNames ++ repeat "") - argTs <- asPredType (toTValue ty) - (labels, vars) <- - flip evalStateT 0 $ unzip <$> - sequence (zipWith newVarsForType argTs argNames) - bval <- eval t - let prd = do - bval' <- traverse (fmap ready) vars >>= (liftIO . applyAll bval) - case bval' of - VBool b -> return b - _ -> fail $ "sbvSolve: non-boolean result type. " ++ show bval' - return (labels, prd) - data Labeler = BoolLabel String | IntegerLabel String @@ -738,21 +675,8 @@ data Labeler nextId :: StateT Int IO String nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s)) ---unzipMap :: Map k (a, b) -> (Map k a, Map k b) ---unzipMap m = (fmap fst m, fmap snd m) - -myfun ::(Map FieldName (Labeler, Symbolic SValue)) -> (Map FieldName Labeler, Map FieldName (Symbolic SValue)) -myfun = fmap fst A.&&& fmap snd - -newVarsForType :: TValue SBV -> String -> StateT Int IO (Maybe Labeler, Symbolic SValue) -newVarsForType v nm = - case vAsFirstOrderType v of - Just fot -> - do (l, sv) <- newVars fot - return (Just l, sv) - Nothing -> - do sv <- lift $ parseUninterpreted [] nm v - return (Nothing, return sv) +unzipMap :: Map k (a, b) -> (Map k a, Map k b) +unzipMap m = (fmap fst m, fmap snd m) newVars :: FirstOrderType -> StateT Int IO (Labeler, Symbolic SValue) newVars FOTBit = nextId <&> \s-> (BoolLabel s, vBool <$> existsSBool s) @@ -770,20 +694,20 @@ newVars (FOTTuple ts) = do (labels, vals) <- V.unzip <$> traverse newVars (V.fromList ts) return (TupleLabel labels, vTuple <$> traverse (fmap ready) (V.toList vals)) newVars (FOTRec tm) = do - (labels, vals) <- myfun <$> (traverse newVars tm :: StateT Int IO (Map FieldName (Labeler, Symbolic SValue))) + (labels, vals) <- unzipMap <$> (traverse newVars tm :: StateT Int IO (Map FieldName (Labeler, Symbolic SValue))) return (RecLabel labels, vRecord <$> traverse (fmap ready) (vals :: (Map FieldName (Symbolic SValue)))) getLabels :: [Labeler] -> Map String CV -> - [String] -> Maybe [(String,FirstOrderValue)] + [ExtCns Term] -> Maybe [(ExtCns Term,FirstOrderValue)] -getLabels ls d argNames - | length argNames == length xs = Just (zip argNames xs) +getLabels ls d args + | length args == length xs = Just (zip args xs) | otherwise = error $ unwords [ "SBV SAT results do not match expected arguments " - , show argNames, show xs] + , show (map (toShortName . ecName) args), show xs] where xs = fmap getLabel ls diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index b01b453f..2c7426fb 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -40,7 +40,6 @@ module Verifier.SAW.Simulator.What4 ( w4Solve - , w4SolveBasic , SymFnCache , TypedExpr(..) , SValue @@ -867,11 +866,11 @@ w4Solve :: forall sym. sym -> SharedContext -> SATQuery -> - IO ([String], [FirstOrderType], [Labeler sym], SBool sym) + IO ([ExtCns Term], [FirstOrderType], [Labeler sym], SBool sym) w4Solve sym sc satq = do t <- satQueryAsTerm sc satq let varList = Map.toList (satVariables satq) - let argNames = map (Text.unpack . toShortName . ecName . fst) varList + let argNames = map fst varList let argTys = map snd varList vars <- evalStateT (traverse (traverse (newVarFOT sym)) varList) 0 let lbls = map (fst . snd) vars @@ -925,7 +924,7 @@ vAsFirstOrderType v = _ -> Nothing valueAsBaseType :: IsSymExprBuilder sym => TValue (What4 sym) -> Maybe (Some W.BaseTypeRepr) -valueAsBaseType v = fmap fotToBaseType $ vAsFirstOrderType v +valueAsBaseType v = fotToBaseType =<< vAsFirstOrderType v ------------------------------------------------------------------------------ @@ -974,6 +973,7 @@ myfun = fmap fst A.&&& fmap snd data Labeler sym = BaseLabel (TypedExpr sym) + | ZeroWidthBVLabel | IntModLabel Natural (SymInteger sym) | VecLabel (Vector (Labeler sym)) | TupleLabel (Vector (Labeler sym)) @@ -988,6 +988,9 @@ newVarFOT sym (FOTTuple ts) = do args <- traverse (return . ready) (V.toList vals) return (TupleLabel labels, vTuple args) +newVarFOT _sym (FOTVec 0 FOTBit) + = return (ZeroWidthBVLabel, VWord ZBV) + newVarFOT sym (FOTVec n tp) | tp /= FOTBit = do (labels,vals) <- V.unzip <$> V.replicateM (fromIntegral n) (newVarFOT sym tp) @@ -1006,17 +1009,18 @@ newVarFOT sym (FOTIntMod n) return (IntModLabel n si, VIntMod n si) newVarFOT sym fot - | Some r <- fotToBaseType fot + | Just (Some r) <- fotToBaseType fot = do nm <- nextId te <- lift $ freshVar sym r nm sv <- lift $ typedToSValue te return (BaseLabel te, sv) - + | otherwise + = fail ("Cannot create What4 variable of type: " ++ show fot) typedToSValue :: (IsExpr (SymExpr sym)) => TypedExpr sym -> IO (SValue sym) typedToSValue (TypedExpr ty expr) = - maybe (fail "Cannot handle") return $ symExprToValue ty expr + maybe (fail ("Cannot handle " ++ show ty)) return $ symExprToValue ty expr getLabelValues :: forall sym t. @@ -1033,6 +1037,7 @@ getLabelValues f = FOVRec <$> traverse (getLabelValues f) labels IntModLabel n x -> FOVIntMod n <$> groundEval f x + ZeroWidthBVLabel -> pure $ FOVWord 0 0 BaseLabel (TypedExpr ty bv) -> do gv <- groundEval f bv case (groundToFOV ty gv) of diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs index f8dcc4f9..bd010bba 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs @@ -43,36 +43,38 @@ import What4.Expr.GroundEval --------------------------------------------------------------------- -- | Convert a type expression from SAW-core to What4 -fotToBaseType :: FirstOrderType -> Some BaseTypeRepr +fotToBaseType :: FirstOrderType -> Maybe (Some BaseTypeRepr) fotToBaseType FOTBit - = Some BaseBoolRepr + = Just (Some BaseBoolRepr) fotToBaseType FOTInt - = Some BaseIntegerRepr + = Just (Some BaseIntegerRepr) fotToBaseType (FOTIntMod _n) - = Some BaseIntegerRepr + = Just (Some BaseIntegerRepr) fotToBaseType (FOTVec nat FOTBit) | Just (Some (PosNat nr)) <- somePosNat nat - = Some (BaseBVRepr nr) - | otherwise -- 0-width bit vector is 0 - = Some BaseIntegerRepr + = Just (Some (BaseBVRepr nr)) + | otherwise = Nothing + fotToBaseType (FOTVec nat fot) - | Some assn <- listToAssn (replicate (fromIntegral nat) fot) - = Some (BaseStructRepr assn) + | Just (Some assn) <- listToAssn (replicate (fromIntegral nat) fot) + = Just (Some (BaseStructRepr assn)) fotToBaseType (FOTArray fot1 fot2) - | Some ty1 <- fotToBaseType fot1 - , Some ty2 <- fotToBaseType fot2 - = Some $ BaseArrayRepr (Empty :> ty1) ty2 + | Just (Some ty1) <- fotToBaseType fot1 + , Just (Some ty2) <- fotToBaseType fot2 + = Just (Some (BaseArrayRepr (Empty :> ty1) ty2)) fotToBaseType (FOTTuple fots) - | Some assn <- listToAssn fots - = Some (BaseStructRepr assn) -fotToBaseType (FOTRec _) - = error "TODO: convert to What4 records ?!" + | Just (Some assn) <- listToAssn fots + = Just (Some (BaseStructRepr assn)) + +-- TODO: convert to What4 records ?! +fotToBaseType _ = Nothing -listToAssn :: [FirstOrderType] -> Some (Assignment BaseTypeRepr) -listToAssn [] = Some empty +listToAssn :: [FirstOrderType] -> Maybe (Some (Assignment BaseTypeRepr)) +listToAssn [] = Just (Some empty) listToAssn (fot:rest) = case (fotToBaseType fot, listToAssn rest) of - (Some bt, Some assn) -> Some $ extend assn bt + (Just (Some bt), Just (Some assn)) -> Just (Some (extend assn bt)) + _ -> Nothing --------------------------------------------------------------------- -- | Convert a type expression from What4 to SAW-core diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index 2b63fa84..84086c1e 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -642,7 +642,7 @@ and_triv2 (x : Bool) : Eq Bool (and (not x) x) False = -------------------------------------------------------------------------------- -- Converting Booleans to Propositions -EqTrue : Bool -> sort 1; +EqTrue : Bool -> Prop; EqTrue x = Eq Bool x True; TrueI : EqTrue True; diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index a4d086de..1680dc13 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -918,7 +918,13 @@ scTypeOf' sc env t0 = State.evalStateT (memo t0) Map.empty Pi _ tp rhs -> do ltp <- sort tp rtp <- toSort =<< lift (scTypeOf' sc (tp : env) rhs) - lift $ scSort sc (max ltp rtp) + + -- NOTE: the rule for type-checking Pi types is that (Pi x a b) is a Prop + -- when b is a Prop (this is a forall proposition), otherwise it is a + -- (Type (max (sortOf a) (sortOf b))) + let srt = if rtp == propSort then propSort else max ltp rtp + + lift $ scSort sc srt LocalVar i | i < length env -> lift $ incVars sc 0 (i + 1) (env !! i) | otherwise -> fail $ "Dangling bound variable: " ++ show (i - length env) diff --git a/saw-core/src/Verifier/SAW/Simulator/RME.hs b/saw-core/src/Verifier/SAW/Simulator/RME.hs index 09b45a4b..6b86e5f6 100644 --- a/saw-core/src/Verifier/SAW/Simulator/RME.hs +++ b/saw-core/src/Verifier/SAW/Simulator/RME.hs @@ -23,7 +23,6 @@ module Verifier.SAW.Simulator.RME , toBool , toWord , runIdentity - , withBitBlastedPred , withBitBlastedSATQuery ) where @@ -46,8 +45,7 @@ import qualified Verifier.SAW.Prim as Prim import qualified Verifier.SAW.Simulator as Sim import Verifier.SAW.Simulator.Value import qualified Verifier.SAW.Simulator.Prims as Prims -import Verifier.SAW.FiniteValue (FiniteType(..), asFiniteType, FirstOrderType, toFiniteType) -import qualified Verifier.SAW.Recognizer as R +import Verifier.SAW.FiniteValue (FiniteType(..), FirstOrderType, toFiniteType) import Verifier.SAW.SharedTerm import Verifier.SAW.TypedAST (ModuleMap) import Verifier.SAW.Utils (panic) @@ -397,31 +395,6 @@ bitBlastBasic m addlPrims ecMap t = runIdentity $ do (const Nothing) Sim.evalSharedTerm cfg t -asPredType :: SharedContext -> Term -> IO [Term] -asPredType sc t = do - t' <- scWhnf sc t - case t' of - (R.asPi -> Just (_, t1, t2)) -> (t1 :) <$> asPredType sc t2 - (R.asBoolType -> Just ()) -> return [] - _ -> panic "Verifier.SAW.Simulator.RME.asPredType" ["non-boolean result type:", showTerm t'] - -withBitBlastedPred :: - SharedContext -> - Map Ident RValue -> - Term -> - (RME -> [FiniteType] -> IO a) -> IO a -withBitBlastedPred sc addlPrims t c = do - ty <- scTypeOf sc t - argTs <- asPredType sc ty - shapes <- traverse (asFiniteType sc) argTs - modmap <- scGetModuleMap sc - let vars = evalState (traverse newVars' shapes) 0 - let bval = bitBlastBasic modmap addlPrims mempty t - let bval' = runIdentity $ applyAll bval vars - case bval' of - VBool anf -> c anf shapes - _ -> panic "Verifier.SAW.Simulator.RME.bitBlast" ["non-boolean result type."] - processVar :: (ExtCns Term, FirstOrderType) ->