From dc36a11c210843be9760d904de6cdafd169a9b20 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 30 Oct 2020 15:04:35 -0700 Subject: [PATCH] Have the What4 and SBV solver methods take the values to be held uninterpreted as a `Set VarIndex` instead of a `[String]`. This shifts the burden of resolving user-provided names closer to the front-end. --- .../src/Verifier/SAW/Simulator/SBV.hs | 24 ++++++------ .../src/Verifier/SAW/Simulator/What4.hs | 38 +++++++++---------- 2 files changed, 30 insertions(+), 32 deletions(-) diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index 1d5a7fe1e4..7f3c0a2d0c 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -47,6 +47,7 @@ import Data.Bits import Data.IORef import Data.Map (Map) import qualified Data.Map as Map +import Data.Set (Set) import qualified Data.Set as Set import qualified Data.Text as Text import Data.Vector (Vector) @@ -566,10 +567,9 @@ muxSbvExtra c x y = -- | Abstract constants with names in the list 'unints' are kept as -- uninterpreted constants; all others are unfolded. -sbvSolveBasic :: SharedContext -> Map Ident SValue -> [String] -> Term -> IO SValue -sbvSolveBasic sc addlPrims unints t = do +sbvSolveBasic :: SharedContext -> Map Ident SValue -> Set VarIndex -> Term -> IO SValue +sbvSolveBasic sc addlPrims unintSet t = do m <- scGetModuleMap sc - unintSet <- Set.fromList <$> mapM (\u -> fst <$> scResolveUnambiguous sc (Text.pack u)) unints let extcns (EC ix nm ty) = parseUninterpreted [] (Text.unpack (toShortName nm) ++ "#" ++ show ix) ty let uninterpreted ec @@ -663,11 +663,11 @@ vAsFirstOrderType v = sbvSolve :: SharedContext -> Map Ident SValue - -> [String] + -> Set VarIndex -> Term -> IO ([Maybe Labeler], Symbolic SBool) -sbvSolve sc addlPrims unints t = do - let eval = sbvSolveBasic sc addlPrims unints +sbvSolve sc addlPrims unintSet t = do + let eval = sbvSolveBasic sc addlPrims unintSet ty <- eval =<< scTypeOf sc t let lamNames = map fst (fst (R.asLambdaList t)) let varNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ] @@ -775,16 +775,16 @@ argTypes sc t = do sbvCodeGen_definition :: SharedContext -> Map Ident SValue - -> [String] + -> Set VarIndex -> Term -> (Natural -> Bool) -- ^ Allowed word sizes -> IO (SBVCodeGen (), [FirstOrderType], FirstOrderType) -sbvCodeGen_definition sc addlPrims unints t checkSz = do +sbvCodeGen_definition sc addlPrims unintSet t checkSz = do ty <- scTypeOf sc t (argTs,resTy) <- argTypes sc ty shapes <- traverse (asFirstOrderType sc) argTs resultShape <- asFirstOrderType sc resTy - bval <- sbvSolveBasic sc addlPrims unints t + bval <- sbvSolveBasic sc addlPrims unintSet t vars <- evalStateT (traverse (newCodeGenVars checkSz) shapes) 0 let codegen = do args <- traverse (fmap ready) vars @@ -863,14 +863,14 @@ sbvSetOutput _checkSz _ft _v _i = do sbvCodeGen :: SharedContext -> Map Ident SValue - -> [String] + -> Set VarIndex -> Maybe FilePath -> String -> Term -> IO () -sbvCodeGen sc addlPrims unints path fname t = do +sbvCodeGen sc addlPrims unintSet path fname t = do -- The SBV C code generator expects only these word sizes let checkSz n = n `elem` [8,16,32,64] - (codegen,_,_) <- sbvCodeGen_definition sc addlPrims unints t checkSz + (codegen,_,_) <- sbvCodeGen_definition sc addlPrims unintSet t checkSz compileToC path fname codegen diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index be9bdaa923..92bf499d14 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -61,6 +61,7 @@ import Data.IORef import Data.List (genericTake) import Data.Map (Map) import qualified Data.Map as Map +import Data.Set (Set) import qualified Data.Set as Set import qualified Data.Text as Text import Data.Vector (Vector) @@ -660,13 +661,11 @@ w4SolveBasic :: SharedContext -> Map Ident (SValue sym) {- ^ additional primitives -} -> IORef (SymFnCache sym) {- ^ cache for uninterpreted function symbols -} -> - [String] {- ^ 'unints' Constants in this list are kept uninterpreted -} -> + Set VarIndex {- ^ 'unints' Constants in this list are kept uninterpreted -} -> Term {- ^ term to simulate -} -> IO (SValue sym) -w4SolveBasic sc addlPrims ref unints t = +w4SolveBasic sc addlPrims ref unintSet t = do m <- scGetModuleMap sc - unintSet <- Set.fromList <$> mapM (\u -> fst <$> scResolveUnambiguous sc (Text.pack u)) unints - let sym = given :: sym let extcns (EC ix nm ty) = parseUninterpreted sym ref (mkUnintApp (Text.unpack (toShortName nm) ++ "_" ++ show ix)) ty @@ -857,11 +856,11 @@ applyUnintApp sym app0 v = w4SolveAny :: forall sym. (IsSymExprBuilder sym) => - sym -> SharedContext -> Map Ident (SValue sym) -> [String] -> Term -> + sym -> SharedContext -> Map Ident (SValue sym) -> Set VarIndex -> Term -> IO ([String], ([Maybe (Labeler sym)], SValue sym)) -w4SolveAny sym sc ps unints t = give sym $ do +w4SolveAny sym sc ps unintSet t = give sym $ do ref <- newIORef Map.empty - let eval = w4SolveBasic sc ps ref unints + let eval = w4SolveBasic sc ps ref unintSet ty <- eval =<< scTypeOf sc t -- get the names of the arguments to the function @@ -888,10 +887,10 @@ w4SolveAny sym sc ps unints t = give sym $ do w4Solve :: forall sym. (IsSymExprBuilder sym) => - sym -> SharedContext -> Map Ident (SValue sym) -> [String] -> Term -> + sym -> SharedContext -> Map Ident (SValue sym) -> Set VarIndex -> Term -> IO ([String], ([Maybe (Labeler sym)], SBool sym)) -w4Solve sym sc ps unints t = - do (argNames, (bvs, bval)) <- w4SolveAny sym sc ps unints t +w4Solve sym sc ps unintSet t = + do (argNames, (bvs, bval)) <- w4SolveAny sym sc ps unintSet t case bval of VBool b -> return (argNames, (bvs, b)) _ -> fail $ "w4Solve: non-boolean result type. " ++ show bval @@ -1063,12 +1062,12 @@ getLabelValues f = w4EvalAny :: forall n solver fs. CS.SAWCoreBackend n solver fs -> SharedContext -> - Map Ident (SValue (CS.SAWCoreBackend n solver fs)) -> [String] -> Term -> + Map Ident (SValue (CS.SAWCoreBackend n solver fs)) -> Set VarIndex -> Term -> IO ([String], ([Maybe (Labeler (CS.SAWCoreBackend n solver fs))], SValue (CS.SAWCoreBackend n solver fs))) -w4EvalAny sym sc ps unints t = +w4EvalAny sym sc ps unintSet t = do modmap <- scGetModuleMap sc ref <- newIORef Map.empty - let eval = w4EvalBasic sym sc modmap ps ref unints + let eval = w4EvalBasic sym sc modmap ps ref unintSet ty <- eval =<< scTypeOf sc t -- get the names of the arguments to the function @@ -1098,10 +1097,10 @@ w4EvalAny sym sc ps unints t = w4Eval :: forall n solver fs. CS.SAWCoreBackend n solver fs -> SharedContext -> - Map Ident (SValue (CS.SAWCoreBackend n solver fs)) -> [String] -> Term -> + Map Ident (SValue (CS.SAWCoreBackend n solver fs)) -> Set VarIndex -> Term -> IO ([String], ([Maybe (Labeler (CS.SAWCoreBackend n solver fs))], SBool (CS.SAWCoreBackend n solver fs))) -w4Eval sym sc ps uints t = - do (argNames, (bvs, bval)) <- w4EvalAny sym sc ps uints t +w4Eval sym sc ps uintSet t = + do (argNames, (bvs, bval)) <- w4EvalAny sym sc ps uintSet t case bval of VBool b -> return (argNames, (bvs, b)) _ -> fail $ "w4Eval: non-boolean result type. " ++ show bval @@ -1115,12 +1114,11 @@ w4EvalBasic :: ModuleMap -> Map Ident (SValue (CS.SAWCoreBackend n solver fs)) {- ^ additional primitives -} -> IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) {- ^ cache for uninterpreted function symbols -} -> - [String] {- ^ 'unints' Constants in this list are kept uninterpreted -} -> + Set VarIndex {- ^ 'unints' Constants in this list are kept uninterpreted -} -> Term {- ^ term to simulate -} -> IO (SValue (CS.SAWCoreBackend n solver fs)) -w4EvalBasic sym sc m addlPrims ref unints t = - do unintSet <- Set.fromList <$> mapM (\u -> fst <$> scResolveUnambiguous sc (Text.pack u)) unints - let extcns tf (EC ix nm ty) = +w4EvalBasic sym sc m addlPrims ref unintSet t = + do let extcns tf (EC ix nm ty) = do trm <- ArgTermConst <$> scTermF sc tf parseUninterpretedSAW sym sc ref trm (mkUnintApp (Text.unpack (toShortName nm) ++ "_" ++ show ix)) ty