From 20c0c268a8c396da39b71005330dc8738ecc112c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 19 Jan 2021 13:29:22 -0800 Subject: [PATCH] Update submodules and adapt to GaloisInc/saw-core#119. The saw-core term AST has changed some uses of `String` to `Text`. --- deps/crucible | 2 +- deps/saw-core | 2 +- deps/saw-core-coq | 2 +- src/SAWScript/Builtins.hs | 7 ++++--- src/SAWScript/ImportAIG.hs | 6 ++++-- src/SAWScript/Prover/MRSolver.hs | 3 ++- src/SAWScript/Prover/RME.hs | 3 ++- src/SAWScript/Prover/SBV.hs | 3 ++- 8 files changed, 17 insertions(+), 11 deletions(-) diff --git a/deps/crucible b/deps/crucible index 12a1fba8b3..4d99990c51 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 12a1fba8b31073d8f7badd3718f8de03f7244d14 +Subproject commit 4d99990c5114e1b50d924a35d8f2765cb9647c15 diff --git a/deps/saw-core b/deps/saw-core index 943f03ce02..13995d82a2 160000 --- a/deps/saw-core +++ b/deps/saw-core @@ -1 +1 @@ -Subproject commit 943f03ce02c72c834d7c0b14a9d4476125cf433e +Subproject commit 13995d82a234b5cb79117354f965539103a21535 diff --git a/deps/saw-core-coq b/deps/saw-core-coq index f970f9763c..62490c887e 160000 --- a/deps/saw-core-coq +++ b/deps/saw-core-coq @@ -1 +1 @@ -Subproject commit f970f9763cbb942a93d388b4fa5a7cf6044bbff3 +Subproject commit 62490c887e9aaae49075180bce5d6c6edaebcc59 diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 9bd08a499a..f249d1e6d3 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -41,6 +41,7 @@ import qualified Data.Set as Set import Data.Maybe import Data.Time.Clock import Data.Typeable +import Data.Text (Text) import qualified Data.Text as Text import System.Directory import qualified System.Environment @@ -578,7 +579,7 @@ goal_apply (Theorem (Prop rule) _stats) = return ((), ProofState (newgoals ++ goals') concl stats timeout) applyFirst (asPiLists rule) where - asPiLists :: Term -> [([(String, Term)], Term)] + asPiLists :: Term -> [([(Text, Term)], Term)] asPiLists t = case asPi t of Nothing -> [([], t)] @@ -608,7 +609,7 @@ goal_intro s = case asPi (unProp (goalProp goal)) of Nothing -> fail "goal_intro failed: not a pi type" Just (nm, tp, body) -> - do let name = if null s then nm else s + do let name = if null s then Text.unpack nm else s sc <- SV.getSharedContext x <- io $ scFreshGlobal sc name tp tt <- io $ mkTypedTerm sc x @@ -983,7 +984,7 @@ w4AbcVerilog _unints sc _hashcons g = else do bits <- reverse <$> parseAigerCex cexText let goalArgs' = reverse goalArgs argTys = map snd goalArgs' - argNms = map fst goalArgs' + argNms = map (Text.unpack . fst) goalArgs' finiteArgTys <- traverse (asFiniteType sc) argTys case liftCexBB finiteArgTys bits of Left parseErr -> fail parseErr diff --git a/src/SAWScript/ImportAIG.hs b/src/SAWScript/ImportAIG.hs index 8970ce7cb0..84004d3dab 100644 --- a/src/SAWScript/ImportAIG.hs +++ b/src/SAWScript/ImportAIG.hs @@ -6,6 +6,7 @@ Maintainer : huffman Stability : provisional -} {-# LANGUAGE CPP #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} @@ -25,6 +26,7 @@ import Control.Exception import Control.Monad import Control.Monad.State.Strict import Control.Monad.Trans.Except +import Data.Text (Text) import qualified Data.Vector as V import Prettyprinter @@ -60,7 +62,7 @@ bitblastSharedTerm sc v (asBitvectorType -> Just w) = do modify (V.++ inputs) bitblastSharedTerm _ _ tp = throwTP $ show $ vcat - [ pretty "Could not parse AIG input type:" + [ "Could not parse AIG input type:" , indent 2 (ppTerm defaultPPOpts tp) ] @@ -149,7 +151,7 @@ translateNetwork :: AIG.IsAIG l g -> SharedContext -- ^ Context to build in term. -> g x -- ^ Network to bitblast -> [l x] -- ^ Outputs for network. - -> [(String, Term)] -- ^ Expected types + -> [(Text, Term)] -- ^ Expected types -> Term -- ^ Expected output type. -> ExceptT String IO Term translateNetwork opts sc ntk outputLits args resultType = do diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs index 2b72e8e80a..6519559bf3 100644 --- a/src/SAWScript/Prover/MRSolver.hs +++ b/src/SAWScript/Prover/MRSolver.hs @@ -13,6 +13,7 @@ import Control.Monad.Reader import Control.Monad.State import Control.Monad.Except import Data.Semigroup +import qualified Data.Text as Text import Prettyprinter @@ -612,7 +613,7 @@ askMRSolver sc smt_conf timeout t1 t2 = flip evalStateT init_st $ runExceptT $ do mrSolveEq (Type tp1) (Type tp2) let (pi_args, ret_tp) = asPiList tp1 - vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal x x_tp) pi_args + vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal (Text.unpack x) x_tp) pi_args case asCompMApp ret_tp of Just _ -> return () Nothing -> throwError (NotCompFunType tp1) diff --git a/src/SAWScript/Prover/RME.hs b/src/SAWScript/Prover/RME.hs index c628b25bd6..d2e003cb89 100644 --- a/src/SAWScript/Prover/RME.hs +++ b/src/SAWScript/Prover/RME.hs @@ -1,6 +1,7 @@ module SAWScript.Prover.RME where import qualified Data.Map as Map +import qualified Data.Text as Text import qualified Data.RME as RME @@ -25,7 +26,7 @@ proveRME sc goal = t <- bindAllExts sc t0 >>= rewriteEqs sc tp <- scWhnf sc =<< scTypeOf sc t let (args, _) = asPiList tp - argNames = map fst args + argNames = map (Text.unpack . fst) args RME.withBitBlastedPred sc Map.empty t $ \lit0 shapes -> let lit = RME.compl lit0 stats = solverStats "RME" (scSharedSize t0) diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs index e0b14df894..763aaa800f 100644 --- a/src/SAWScript/Prover/SBV.hs +++ b/src/SAWScript/Prover/SBV.hs @@ -11,6 +11,7 @@ import Data.Maybe import Data.Map ( Map ) import qualified Data.Map as Map import Data.Set ( Set ) +import qualified Data.Text as Text import qualified Data.Vector as V import Control.Monad @@ -65,7 +66,7 @@ proveUnintSBV conf unintSet timeout sc term = SBV.Satisfiable {} -> do let dict = SBV.getModelDictionary r - r' = getLabels labels dict argNames + r' = getLabels labels dict (map Text.unpack argNames) return (r', stats) SBV.SatExtField {} -> fail "Prover returned model in extension field"