diff --git a/saw-core-what4/saw-core-what4.cabal b/saw-core-what4/saw-core-what4.cabal index 717ee17f65..b7504e73ba 100644 --- a/saw-core-what4/saw-core-what4.cabal +++ b/saw-core-what4/saw-core-what4.cabal @@ -22,7 +22,6 @@ library mtl, saw-core, what4, - crucible-saw, panic, text, transformers, @@ -35,4 +34,6 @@ library Verifier.SAW.Simulator.What4.FirstOrder Verifier.SAW.Simulator.What4.PosNat Verifier.SAW.Simulator.What4.Panic + Verifier.SAW.Simulator.What4.ReturnTrip + GHC-options: -Wall -Werror diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 4a3da7e971..f1a8d492ac 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -78,8 +78,6 @@ import qualified Control.Exception as X import Control.Monad.State as ST import Numeric.Natural (Natural) -import Data.Reflection (Given(..), give) - -- saw-core import qualified Verifier.SAW.Recognizer as R import qualified Verifier.SAW.Simulator as Sim @@ -106,13 +104,11 @@ import qualified Data.Parameterized.Map as MapF import Data.Parameterized.Context (Assignment) import Data.Parameterized.Some --- crucible-saw -import qualified Lang.Crucible.Backend.SAWCore as CS - -- saw-core-what4 import Verifier.SAW.Simulator.What4.PosNat import Verifier.SAW.Simulator.What4.FirstOrder import Verifier.SAW.Simulator.What4.Panic +import Verifier.SAW.Simulator.What4.ReturnTrip --------------------------------------------------------------------- -- empty datatype to index (open) type families @@ -141,7 +137,7 @@ type instance Extra (What4 sym) = What4Extra sym type SValue sym = Value (What4 sym) -- Constraint -type Sym sym = (Given sym, IsSymExprBuilder sym) +type Sym sym = IsSymExprBuilder sym --------------------------------------------------------------------- @@ -156,10 +152,9 @@ instance Show (What4Extra sym) where -- Basic primitive table for What4 data -- -prims :: forall sym. (Sym sym) => - Prims.BasePrims (What4 sym) -prims = - let sym :: sym = given in +prims :: forall sym. + Sym sym => sym -> Prims.BasePrims (What4 sym) +prims sym = Prims.BasePrims { Prims.bpAsBool = W.asConstantPred -- Bitvectors @@ -174,7 +169,7 @@ prims = , Prims.bpMuxBool = W.itePred sym , Prims.bpMuxWord = SW.bvIte sym , Prims.bpMuxInt = W.intIte sym - , Prims.bpMuxExtra = muxWhat4Extra + , Prims.bpMuxExtra = muxWhat4Extra sym -- Booleans , Prims.bpTrue = W.truePred sym , Prims.bpFalse = W.falsePred sym @@ -243,21 +238,21 @@ prims = } -constMap :: forall sym. (Sym sym) => Map Ident (SValue sym) -constMap = - Map.union (Prims.constMap prims) $ +constMap :: forall sym. Sym sym => sym -> Map Ident (SValue sym) +constMap sym = + Map.union (Prims.constMap (prims sym)) $ Map.fromList [ -- Shifts - ("Prelude.bvShl" , bvShLOp) - , ("Prelude.bvShr" , bvShROp) - , ("Prelude.bvSShr", bvSShROp) + ("Prelude.bvShl" , bvShLOp sym) + , ("Prelude.bvShr" , bvShROp sym) + , ("Prelude.bvSShr", bvSShROp sym) -- Integers - , ("Prelude.intToNat", intToNatOp) - , ("Prelude.natToInt", natToIntOp) - , ("Prelude.intToBv" , intToBvOp) - , ("Prelude.bvToInt" , bvToIntOp) - , ("Prelude.sbvToInt", sbvToIntOp) + , ("Prelude.intToNat", intToNatOp sym) + , ("Prelude.natToInt", natToIntOp sym) + , ("Prelude.intToBv" , intToBvOp sym) + , ("Prelude.bvToInt" , bvToIntOp sym) + , ("Prelude.sbvToInt", sbvToIntOp sym) -- Integers mod n , ("Prelude.toIntMod" , toIntModOp) , ("Prelude.fromIntMod", fromIntModOp sym) @@ -268,11 +263,10 @@ constMap = , ("Prelude.intModNeg" , intModUnOp sym W.intNeg) -- Streams , ("Prelude.MkStream", mkStreamOp) - , ("Prelude.streamGet", streamGetOp) + , ("Prelude.streamGet", streamGetOp sym) -- Misc - , ("Prelude.expByNat", Prims.expByNatOp prims) + , ("Prelude.expByNat", Prims.expByNatOp (prims sym)) ] - where sym = given :: sym ----------------------------------------------------------------------- -- Implementation of constMap primitives @@ -287,19 +281,19 @@ toBool :: SValue sym -> IO (SBool sym) toBool (VBool b) = return b toBool x = fail $ unwords ["Verifier.SAW.Simulator.What4.toBool", show x] -toWord :: forall sym. (Sym sym) => - SValue sym -> IO (SWord sym) -toWord (VWord w) = return w -toWord (VVector vv) = do +toWord :: forall sym. + Sym sym => sym -> SValue sym -> IO (SWord sym) +toWord _ (VWord w) = return w +toWord sym (VVector vv) = do -- vec :: Vector (SBool sym)) vec1 <- T.traverse force vv vec2 <- T.traverse toBool vec1 - SW.bvPackBE (given :: sym) vec2 -toWord x = fail $ unwords ["Verifier.SAW.Simulator.What4.toWord", show x] + SW.bvPackBE sym vec2 +toWord _ x = fail $ unwords ["Verifier.SAW.Simulator.What4.toWord", show x] -wordFun :: (Sym sym) => - (SWord sym -> IO (SValue sym)) -> SValue sym -wordFun f = strictFun (\x -> f =<< toWord x) +wordFun :: + Sym sym => sym -> (SWord sym -> IO (SValue sym)) -> SValue sym +wordFun sym f = strictFun (\x -> f =<< toWord sym x) valueToSymExpr :: SValue sym -> Maybe (Some (W.SymExpr sym)) valueToSymExpr = \case @@ -327,43 +321,43 @@ symExprToValue tp expr = case tp of -- primitive intToNat : Integer -> Nat; -- intToNat x == max 0 x -intToNatOp :: forall sym. Sym sym => SValue sym -intToNatOp = +intToNatOp :: forall sym. Sym sym => sym -> SValue sym +intToNatOp sym = Prims.intFun "intToNat" $ \i -> case W.asInteger i of Just i' | 0 <= i' -> pure (VNat (fromInteger i')) | otherwise -> pure (VNat 0) Nothing -> - do z <- W.intLit (given :: sym) 0 - pneg <- W.intLt (given :: sym) i z - i' <- W.intIte (given :: sym) pneg z i + do z <- W.intLit sym 0 + pneg <- W.intLt sym i z + i' <- W.intIte sym pneg z i pure (VToNat (VInt i')) -- primitive natToInt :: Nat -> Integer; -natToIntOp :: forall sym. (Sym sym) => SValue sym -natToIntOp = +natToIntOp :: forall sym. Sym sym => sym -> SValue sym +natToIntOp sym = Prims.natFun' "natToInt" $ \n -> - VInt <$> W.intLit (given :: sym) (toInteger n) + VInt <$> W.intLit sym (toInteger n) -- interpret bitvector as unsigned integer -- primitive bvToInt : (n : Nat) -> Vec n Bool -> Integer; -bvToIntOp :: forall sym. (Sym sym) => SValue sym -bvToIntOp = constFun $ wordFun $ \(v :: SWord sym) -> do - VInt <$> SW.bvToInteger (given :: sym) v +bvToIntOp :: forall sym. Sym sym => sym -> SValue sym +bvToIntOp sym = constFun $ wordFun sym $ \v -> + VInt <$> SW.bvToInteger sym v -- interpret bitvector as signed integer -- primitive sbvToInt : (n : Nat) -> Vec n Bool -> Integer; -sbvToIntOp :: forall sym. (Sym sym) => SValue sym -sbvToIntOp = constFun $ wordFun $ \v -> do - VInt <$> SW.sbvToInteger (given :: sym) v +sbvToIntOp :: forall sym. Sym sym => sym -> SValue sym +sbvToIntOp sym = constFun $ wordFun sym $ \v -> + VInt <$> SW.sbvToInteger sym v -- primitive intToBv : (n : Nat) -> Integer -> Vec n Bool; -intToBvOp :: forall sym. (Sym sym) => SValue sym -intToBvOp = +intToBvOp :: forall sym. Sym sym => sym -> SValue sym +intToBvOp sym = Prims.natFun' "intToBv n" $ \n -> return $ Prims.intFun "intToBv x" $ \(x :: SymInteger sym) -> - VWord <$> SW.integerToBV (given :: sym) x n + VWord <$> SW.integerToBV sym x n -- @@ -402,34 +396,34 @@ liftRotate sym f w i = -- | op : (n : Nat) -> Vec n Bool -> Nat -> Vec n Bool -bvShiftOp :: (Sym sym) => +bvShiftOp :: Sym sym => sym -> (SWord sym -> SWord sym -> IO (SWord sym)) -> (SWord sym -> Integer -> IO (SWord sym)) -> SValue sym -bvShiftOp bvOp natOp = +bvShiftOp sym bvOp natOp = constFun $ -- additional argument? the size? - wordFun $ \x -> -- word to shift + wordFun sym $ \x -> -- word to shift return $ strictFun $ \y -> -- amount to shift as a nat case y of VNat i -> VWord <$> natOp x j where j = toInteger i `min` SW.bvWidth x - VToNat v -> VWord <$> (bvOp x =<< toWord v) + VToNat v -> VWord <$> (bvOp x =<< toWord sym v) _ -> error $ unwords ["Verifier.SAW.Simulator.What4.bvShiftOp", show y] -- bvShl : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool; -bvShLOp :: forall sym. (Sym sym) => SValue sym -bvShLOp = bvShiftOp (SW.bvShl given) - (liftShift given (SW.bvShl given)) +bvShLOp :: forall sym. Sym sym => sym -> SValue sym +bvShLOp sym = bvShiftOp sym (SW.bvShl sym) + (liftShift sym (SW.bvShl sym)) -- bvShR : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool; -bvShROp :: forall sym. (Sym sym) => SValue sym -bvShROp = bvShiftOp (SW.bvLshr given) - (liftShift given (SW.bvLshr given)) +bvShROp :: forall sym. Sym sym => sym -> SValue sym +bvShROp sym = bvShiftOp sym (SW.bvLshr sym) + (liftShift sym (SW.bvLshr sym)) -- bvSShR : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool; -bvSShROp :: forall sym. (Sym sym) => SValue sym -bvSShROp = bvShiftOp (SW.bvAshr given) - (liftShift given (SW.bvAshr given)) +bvSShROp :: forall sym. Sym sym => sym -> SValue sym +bvSShROp sym = bvShiftOp sym (SW.bvAshr sym) + (liftShift sym (SW.bvAshr sym)) bvForall :: W.IsSymExprBuilder sym => sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym) @@ -519,15 +513,15 @@ mkStreamOp = return $ VExtra (SStream (\n -> apply f (ready (VNat n))) r) -- streamGet :: (a :: sort 0) -> Stream a -> Nat -> a; -streamGetOp :: forall sym. (IsExpr (SymExpr sym), Sym sym) => SValue sym -streamGetOp = +streamGetOp :: forall sym. Sym sym => sym -> SValue sym +streamGetOp sym = constFun $ strictFun $ \xs -> return $ strictFun $ \case VNat n -> lookupSStream xs n VToNat w -> - do ilv <- toWord w - selectV (lazyMux @sym muxBVal) ((2 ^ SW.bvWidth ilv) - 1) (lookupSStream xs) ilv + do ilv <- toWord sym w + selectV sym (lazyMux @sym (muxBVal sym)) ((2 ^ SW.bvWidth ilv) - 1) (lookupSStream xs) ilv v -> Prims.panic "streamGetOp" ["Expected Nat value", show v] lookupSStream :: SValue sym -> Natural -> IO (SValue sym) @@ -541,17 +535,16 @@ lookupSStream (VExtra (SStream f r)) n = do lookupSStream _ _ = fail "expected Stream" -muxBVal :: forall sym. (Sym sym) => - SBool sym -> SValue sym -> SValue sym -> IO (SValue sym) -muxBVal = Prims.muxValue prims +muxBVal :: forall sym. Sym sym => + sym -> SBool sym -> SValue sym -> SValue sym -> IO (SValue sym) +muxBVal sym = Prims.muxValue (prims sym) -muxWhat4Extra :: - forall sym. (Sym sym) => - SBool sym -> What4Extra sym -> What4Extra sym -> IO (What4Extra sym) -muxWhat4Extra c x y = +muxWhat4Extra :: forall sym. Sym sym => + sym -> SBool sym -> What4Extra sym -> What4Extra sym -> IO (What4Extra sym) +muxWhat4Extra sym c x y = do let f i = do xi <- lookupSStream (VExtra x) i yi <- lookupSStream (VExtra y) i - muxBVal c xi yi + muxBVal sym c xi yi r <- newIORef Map.empty return (SStream f r) @@ -570,9 +563,11 @@ lazyMux muxFn c tm fm = -- selectV merger maxValue valueFn index returns valueFn v when index has value v -- if index is greater than maxValue, it returns valueFn maxValue. Use the ite op from merger. -selectV :: forall sym b. Sym sym => +selectV :: forall sym b. + Sym sym => + sym -> (SBool sym -> IO b -> IO b -> IO b) -> Natural -> (Natural -> IO b) -> SWord sym -> IO b -selectV merger maxValue valueFn vx = +selectV sym merger maxValue valueFn vx = case SW.bvAsUnsignedInteger vx of Just i -> valueFn (fromInteger i :: Natural) Nothing -> impl (swBvWidth vx) 0 @@ -581,7 +576,7 @@ selectV merger maxValue valueFn vx = impl _ x | x > maxValue || x < 0 = valueFn maxValue impl 0 y = valueFn y impl i y = do - p <- SW.bvAtBE (given :: sym) vx (toInteger j) + p <- SW.bvAtBE sym vx (toInteger j) merger p (impl j (y `setBit` j)) (impl j y) where j = i - 1 instance Show (SArray sym) where @@ -659,22 +654,22 @@ arrayEq sym lhs_arr rhs_arr -- a symbolic value w4SolveBasic :: - forall sym. (Given sym, IsSymExprBuilder sym) => + forall sym. IsSymExprBuilder sym => + sym -> SharedContext -> Map Ident (SValue sym) {- ^ additional primitives -} -> IORef (SymFnCache sym) {- ^ cache for uninterpreted function symbols -} -> Set VarIndex {- ^ 'unints' Constants in this list are kept uninterpreted -} -> Term {- ^ term to simulate -} -> IO (SValue sym) -w4SolveBasic sc addlPrims ref unintSet t = +w4SolveBasic sym sc addlPrims ref unintSet t = do m <- scGetModuleMap sc - let sym = given :: sym let extcns (EC ix nm ty) = parseUninterpreted sym ref (mkUnintApp (Text.unpack (toShortName nm) ++ "_" ++ show ix)) ty let uninterpreted ec | Set.member (ecVarIndex ec) unintSet = Just (extcns ec) | otherwise = Nothing - cfg <- Sim.evalGlobal m (constMap `Map.union` addlPrims) extcns uninterpreted + cfg <- Sim.evalGlobal m (constMap sym `Map.union` addlPrims) extcns uninterpreted Sim.evalSharedTerm cfg t @@ -869,9 +864,9 @@ w4SolveAny :: forall sym. (IsSymExprBuilder sym) => sym -> SharedContext -> Map Ident (SValue sym) -> Set VarIndex -> Term -> IO ([String], ([Maybe (Labeler sym)], SValue sym)) -w4SolveAny sym sc ps unintSet t = give sym $ do +w4SolveAny sym sc ps unintSet t = do ref <- newIORef Map.empty - let eval = w4SolveBasic sc ps ref unintSet + let eval = w4SolveBasic sym sc ps ref unintSet ty <- eval =<< scTypeOf sc t -- get the names of the arguments to the function @@ -884,7 +879,7 @@ w4SolveAny sym sc ps unintSet t = give sym $ do -- construct symbolic expressions for the variables vars' <- flip evalStateT 0 $ - sequence (zipWith (newVarsForType ref) argTs (argNames ++ moreNames)) + sequence (zipWith (newVarsForType sym ref) argTs (argNames ++ moreNames)) -- symbolically evaluate bval <- eval t @@ -970,29 +965,29 @@ mkConstant sym name ty = W.freshConstant sym (W.safeSymbol name) ty -- | Generate a new variable from a given BaseType -freshVar :: forall sym ty. (IsSymExprBuilder sym, Given sym) => - BaseTypeRepr ty -> String -> IO (TypedExpr sym) -freshVar ty str = - do c <- mkConstant (given :: sym) str ty +freshVar :: forall sym ty. IsSymExprBuilder sym => + sym -> BaseTypeRepr ty -> String -> IO (TypedExpr sym) +freshVar sym ty str = + do c <- mkConstant sym str ty return (TypedExpr ty c) nextId :: StateT Int IO String nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s)) -newVarsForType :: forall sym. (Given sym, IsSymExprBuilder sym) => +newVarsForType :: forall sym. IsSymExprBuilder sym => + sym -> IORef (SymFnCache sym) -> TValue (What4 sym) -> String -> StateT Int IO (Maybe (Labeler sym), SValue sym) -newVarsForType ref v nm = +newVarsForType sym ref v nm = case vAsFirstOrderType v of Just fot -> do - do (te,sv) <- newVarFOT fot + do (te,sv) <- newVarFOT sym fot return (Just te, sv) Nothing -> do sv <- lift $ parseUninterpreted sym ref (mkUnintApp nm) v return (Nothing, sv) - where sym = given :: sym myfun ::(Map FieldName (Labeler sym, SValue sym)) -> (Map FieldName (Labeler sym), Map FieldName (SValue sym)) myfun = fmap fst A.&&& fmap snd @@ -1005,35 +1000,35 @@ data Labeler sym | RecLabel (Map FieldName (Labeler sym)) -newVarFOT :: forall sym. (IsSymExprBuilder sym, Given sym) => - FirstOrderType -> StateT Int IO (Labeler sym, SValue sym) +newVarFOT :: forall sym. IsSymExprBuilder sym => + sym -> FirstOrderType -> StateT Int IO (Labeler sym, SValue sym) -newVarFOT (FOTTuple ts) = do - (labels,vals) <- V.unzip <$> traverse newVarFOT (V.fromList ts) +newVarFOT sym (FOTTuple ts) = do + (labels,vals) <- V.unzip <$> traverse (newVarFOT sym) (V.fromList ts) args <- traverse (return . ready) (V.toList vals) return (TupleLabel labels, vTuple args) -newVarFOT (FOTVec n tp) +newVarFOT sym (FOTVec n tp) | tp /= FOTBit - = do (labels,vals) <- V.unzip <$> V.replicateM (fromIntegral n) (newVarFOT tp) + = do (labels,vals) <- V.unzip <$> V.replicateM (fromIntegral n) (newVarFOT sym tp) args <- traverse @Vector @(StateT Int IO) (return . ready) vals return (VecLabel labels, VVector args) -newVarFOT (FOTRec tm) - = do (labels, vals) <- myfun <$> traverse newVarFOT tm +newVarFOT sym (FOTRec tm) + = do (labels, vals) <- myfun <$> traverse (newVarFOT sym) tm args <- traverse (return . ready) (vals :: (Map FieldName (SValue sym))) return (RecLabel labels, vRecord args) -newVarFOT (FOTIntMod n) +newVarFOT sym (FOTIntMod n) = do nm <- nextId let r = BaseIntegerRepr - si <- lift $ mkConstant (given :: sym) nm r + si <- lift $ mkConstant sym nm r return (IntModLabel n si, VIntMod n si) -newVarFOT fot +newVarFOT sym fot | Some r <- fotToBaseType fot = do nm <- nextId - te <- lift $ freshVar r nm + te <- lift $ freshVar sym r nm sv <- lift $ typedToSValue te return (BaseLabel te, sv) @@ -1071,14 +1066,16 @@ getLabelValues f = -- | Simplify a saw-core term by evaluating it through the saw backend -- of what4. w4EvalAny :: - forall n solver fs. - CS.SAWCoreBackend n solver fs -> SharedContext -> - 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 unintSet t = + forall n st fs. + B.ExprBuilder n st fs -> + SAWCoreState n -> + SharedContext -> + Map Ident (SValue (B.ExprBuilder n st fs)) -> Set VarIndex -> Term -> + IO ([String], ([Maybe (Labeler (B.ExprBuilder n st fs))], SValue (B.ExprBuilder n st fs))) +w4EvalAny sym st sc ps unintSet t = do modmap <- scGetModuleMap sc ref <- newIORef Map.empty - let eval = w4EvalBasic sym sc modmap ps ref unintSet + let eval = w4EvalBasic sym st sc modmap ps ref unintSet ty <- eval =<< scTypeOf sc t -- get the names of the arguments to the function @@ -1091,9 +1088,8 @@ w4EvalAny sym sc ps unintSet t = -- construct symbolic expressions for the variables vars' <- - give sym $ flip evalStateT 0 $ - sequence (zipWith (newVarsForType ref) argTs argNames) + sequence (zipWith (newVarsForType sym ref) argTs argNames) -- symbolically evaluate bval <- eval t @@ -1106,12 +1102,14 @@ w4EvalAny sym sc ps unintSet t = return (argNames, (bvs, bval')) w4Eval :: - forall n solver fs. - CS.SAWCoreBackend n solver fs -> SharedContext -> - 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 uintSet t = - do (argNames, (bvs, bval)) <- w4EvalAny sym sc ps uintSet t + forall n st fs. + B.ExprBuilder n st fs -> + SAWCoreState n -> + SharedContext -> + Map Ident (SValue (B.ExprBuilder n st fs)) -> Set VarIndex -> Term -> + IO ([String], ([Maybe (Labeler (B.ExprBuilder n st fs))], SBool (B.ExprBuilder n st fs))) +w4Eval sym st sc ps uintSet t = + do (argNames, (bvs, bval)) <- w4EvalAny sym st sc ps uintSet t case bval of VBool b -> return (argNames, (bvs, b)) _ -> fail $ "w4Eval: non-boolean result type. " ++ show bval @@ -1119,24 +1117,25 @@ w4Eval sym sc ps uintSet t = -- | Simplify a saw-core term by evaluating it through the saw backend -- of what4. w4EvalBasic :: - forall n solver fs. - CS.SAWCoreBackend n solver fs -> + forall n st fs. + B.ExprBuilder n st fs -> + SAWCoreState n -> SharedContext -> ModuleMap -> - Map Ident (SValue (CS.SAWCoreBackend n solver fs)) {- ^ additional primitives -} -> - IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) {- ^ cache for uninterpreted function symbols -} -> + Map Ident (SValue (B.ExprBuilder n st fs)) {- ^ additional primitives -} -> + IORef (SymFnCache (B.ExprBuilder n st fs)) {- ^ cache for uninterpreted function symbols -} -> 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 unintSet t = + IO (SValue (B.ExprBuilder n st fs)) +w4EvalBasic sym st 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 + parseUninterpretedSAW sym st sc ref trm (mkUnintApp (Text.unpack (toShortName nm) ++ "_" ++ show ix)) ty let uninterpreted tf ec | Set.member (ecVarIndex ec) unintSet = Just (extcns tf ec) | otherwise = Nothing - cfg <- Sim.evalGlobal' m (give sym constMap `Map.union` addlPrims) extcns uninterpreted + cfg <- Sim.evalGlobal' m (constMap sym `Map.union` addlPrims) extcns uninterpreted Sim.evalSharedTerm cfg t @@ -1146,24 +1145,25 @@ w4EvalBasic sym sc m addlPrims ref unintSet t = -- 'NameInfo' if it encounters a constant value with an 'ExtCns' -- that is not accepted by the filter. w4SimulatorEval :: - forall n solver fs. - CS.SAWCoreBackend n solver fs -> + forall n st fs. + B.ExprBuilder n st fs -> + SAWCoreState n -> SharedContext -> ModuleMap -> - Map Ident (SValue (CS.SAWCoreBackend n solver fs)) {- ^ additional primitives -} -> - IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) {- ^ cache for uninterpreted function symbols -} -> - (ExtCns (TValue (What4 (CS.SAWCoreBackend n solver fs))) -> Bool) + Map Ident (SValue (B.ExprBuilder n st fs)) {- ^ additional primitives -} -> + IORef (SymFnCache (B.ExprBuilder n st fs)) {- ^ cache for uninterpreted function symbols -} -> + (ExtCns (TValue (What4 (B.ExprBuilder n st fs))) -> Bool) {- ^ Filter for constant values. True means unfold, false means halt evaluation. -} -> Term {- ^ term to simulate -} -> - IO (Either NameInfo (SValue (CS.SAWCoreBackend n solver fs))) -w4SimulatorEval sym sc m addlPrims ref constantFilter t = + IO (Either NameInfo (SValue (B.ExprBuilder n st fs))) +w4SimulatorEval sym st sc m addlPrims ref constantFilter 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 + parseUninterpretedSAW sym st sc ref trm (mkUnintApp (Text.unpack (toShortName nm) ++ "_" ++ show ix)) ty let uninterpreted _tf ec = if constantFilter ec then Nothing else Just (X.throwIO (NeutralTermEx (ecName ec))) res <- X.try $ do - cfg <- Sim.evalGlobal' m (give sym constMap `Map.union` addlPrims) extcns uninterpreted + cfg <- Sim.evalGlobal' m (constMap sym `Map.union` addlPrims) extcns uninterpreted Sim.evalSharedTerm cfg t case res of Left (NeutralTermEx nmi) -> pure (Left nmi) @@ -1178,15 +1178,16 @@ instance X.Exception NeutralTermException -- the local variables have the corresponding types from the -- 'Assignment'. parseUninterpretedSAW :: - forall n solver fs. - CS.SAWCoreBackend n solver fs -> + forall n st fs. + B.ExprBuilder n st fs -> + SAWCoreState n -> SharedContext -> - IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) -> + IORef (SymFnCache (B.ExprBuilder n st fs)) -> ArgTerm {- ^ representation of function applied to arguments -} -> - UnintApp (SymExpr (CS.SAWCoreBackend n solver fs)) -> - TValue (What4 (CS.SAWCoreBackend n solver fs)) {- ^ return type -} -> - IO (SValue (CS.SAWCoreBackend n solver fs)) -parseUninterpretedSAW sym sc ref trm app ty = + UnintApp (SymExpr (B.ExprBuilder n st fs)) -> + TValue (What4 (B.ExprBuilder n st fs)) {- ^ return type -} -> + IO (SValue (B.ExprBuilder n st fs)) +parseUninterpretedSAW sym st sc ref trm app ty = case ty of VPiType t1 f -> return $ @@ -1195,13 +1196,13 @@ parseUninterpretedSAW sym sc ref trm app ty = arg <- mkArgTerm sc t1 x let trm' = ArgTermApply trm arg t2 <- f (ready x) - parseUninterpretedSAW sym sc ref trm' app' t2 + parseUninterpretedSAW sym st sc ref trm' app' t2 VBoolType - -> VBool <$> mkUninterpretedSAW sym ref trm app BaseBoolRepr + -> VBool <$> mkUninterpretedSAW sym st ref trm app BaseBoolRepr VIntType - -> VInt <$> mkUninterpretedSAW sym ref trm app BaseIntegerRepr + -> VInt <$> mkUninterpretedSAW sym st ref trm app BaseIntegerRepr -- 0 width bitvector is a constant VVecType 0 VBoolType @@ -1209,14 +1210,14 @@ parseUninterpretedSAW sym sc ref trm app ty = VVecType n VBoolType | Just (Some (PosNat w)) <- somePosNat n - -> (VWord . DBV) <$> mkUninterpretedSAW sym ref trm app (BaseBVRepr w) + -> (VWord . DBV) <$> mkUninterpretedSAW sym st ref trm app (BaseBVRepr w) VVecType n ety | n >= 0 -> do ety' <- termOfTValue sc ety let mkElem i = do let trm' = ArgTermAt n ety' trm i let app' = suffixUnintApp ("_a" ++ show i) app - parseUninterpretedSAW sym sc ref trm' app' ety + parseUninterpretedSAW sym st sc ref trm' app' ety xs <- traverse mkElem (genericTake n [0 ..]) return (VVector (V.fromList (map ready xs))) @@ -1224,7 +1225,7 @@ parseUninterpretedSAW sym sc ref trm app ty = | Just (Some idx_repr) <- valueAsBaseType ity , Just (Some elm_repr) <- valueAsBaseType ety -> (VArray . SArray) <$> - mkUninterpretedSAW sym ref trm app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr) + mkUninterpretedSAW sym st ref trm app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr) VUnitType -> return VUnit @@ -1232,22 +1233,24 @@ parseUninterpretedSAW sym sc ref trm app ty = VPairType ty1 ty2 -> do let trm1 = ArgTermPairLeft trm let trm2 = ArgTermPairRight trm - x1 <- parseUninterpretedSAW sym sc ref trm1 (suffixUnintApp "_L" app) ty1 - x2 <- parseUninterpretedSAW sym sc ref trm2 (suffixUnintApp "_R" app) ty2 + x1 <- parseUninterpretedSAW sym st sc ref trm1 (suffixUnintApp "_L" app) ty1 + x2 <- parseUninterpretedSAW sym st sc ref trm2 (suffixUnintApp "_R" app) ty2 return (VPair (ready x1) (ready x2)) _ -> fail $ "could not create uninterpreted symbol of type " ++ show ty mkUninterpretedSAW :: - forall n solver fs t. - CS.SAWCoreBackend n solver fs -> IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) -> + forall n st fs t. + B.ExprBuilder n st fs -> + SAWCoreState n -> + IORef (SymFnCache (B.ExprBuilder n st fs)) -> ArgTerm -> - UnintApp (SymExpr (CS.SAWCoreBackend n solver fs)) -> + UnintApp (SymExpr (B.ExprBuilder n st fs)) -> BaseTypeRepr t -> - IO (SymExpr (CS.SAWCoreBackend n solver fs) t) -mkUninterpretedSAW sym ref trm (UnintApp nm args tys) ret = + IO (SymExpr (B.ExprBuilder n st fs) t) +mkUninterpretedSAW sym st ref trm (UnintApp nm args tys) ret = do fn <- mkSymFn sym ref nm tys ret - CS.sawRegisterSymFunInterp sym fn (reconstructArgTerm trm) + sawRegisterSymFunInterp st fn (reconstructArgTerm trm) W.applySymFn sym fn args -- | An 'ArgTerm' is a description of how to reassemble a saw-core diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs new file mode 100644 index 0000000000..49ae4dd9b3 --- /dev/null +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs @@ -0,0 +1,1035 @@ +----------------------------------------------------------------------- +-- | +-- Module : Verifier.SAW.Simulator.What4.ReturnTrip +-- Description : Translation from What4 back to SawCore +-- Copyright : (c) Galois, Inc 2014-2021 +-- License : BSD3 +-- Maintainer : Rob Dockins +-- Stability : provisional +------------------------------------------------------------------------ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ViewPatterns #-} + +module Verifier.SAW.Simulator.What4.ReturnTrip + ( newSAWCoreState + , SAWCoreState(..) + , SAWExpr(..) + , baseSCType + , bindSAWTerm + , toSC + , sawCreateVar + , sawRegisterSymFunInterp + , getInputs + ) where + +import Control.Lens +import Control.Monad +import qualified Data.BitVector.Sized as BV +import Data.IORef +import Data.List (elemIndex) +import Data.IntMap (IntMap) +import qualified Data.IntMap as IntMap +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Map ( Map ) +import qualified Data.Map as Map +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Nonce +import Data.Parameterized.Some +import Data.Parameterized.TraversableFC +import Data.Ratio +import Data.Sequence (Seq) +import qualified Data.Sequence as Seq +import Data.Word(Word64) +import qualified Data.Text as Text + +import Numeric.Natural + +import What4.BaseTypes +import What4.Interface +import qualified What4.Expr.ArrayUpdateMap as AUM +import qualified What4.Expr.Builder as B +import qualified What4.Expr.BoolMap as BM +import qualified What4.Expr.WeightedSum as WSum +import qualified What4.SemiRing as B +import What4.Symbol + +import qualified Verifier.SAW.SharedTerm as SC +import qualified Verifier.SAW.TypedAST as SC +import Verifier.SAW.Utils (panic) + +data SAWCoreState n + = SAWCoreState + { saw_ctx :: SC.SharedContext -- ^ the main SAWCore datastructure for building shared terms + , saw_inputs :: IORef (Seq (SC.ExtCns SC.Term )) + -- ^ a record of all the symbolic input variables created so far, + -- in the order they were created + + , saw_symMap :: IORef (Map Word64 (SC.SharedContext -> [SC.Term] -> IO SC.Term)) + -- ^ What to do with uninterpreted functions. + -- The key is the "indexValue" of the "symFunId" for the function + + , saw_elt_cache :: B.IdxCache n SAWExpr + -- ^ cache mapping a What4 variable nonce to its corresponding SAWCore term. + + , saw_elt_cache_r :: IORef (IntMap (Some (B.Expr n))) + -- ^ reverse cache mapping a SAWCore TermIndex to its corresponding What4 variable. + -- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between + -- SAWCore terms and What4 variables. + + } + +newSAWCoreState :: + SC.SharedContext -> + IO (SAWCoreState n) +newSAWCoreState sc = + do inpr <- newIORef Seq.empty + ch <- B.newIdxCache + ch_r <- newIORef IntMap.empty + mr <- newIORef Map.empty + return SAWCoreState + { saw_ctx = sc + , saw_inputs = inpr + , saw_symMap = mr + , saw_elt_cache = ch + , saw_elt_cache_r = ch_r + } + +data SAWExpr (bt :: BaseType) where + SAWExpr :: !SC.Term -> SAWExpr bt + + -- This is a term that represents an integer, but has an + -- implicit integer-to-real conversion. + IntToRealSAWExpr :: !(SAWExpr BaseIntegerType) -> SAWExpr BaseRealType + -- This is a SAWCore term that represents a natural number, but has an + -- implicit nat-to-integer conversion. + NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType + +getInputs :: SAWCoreState n -> IO (Seq (SC.ExtCns SC.Term)) +getInputs st = readIORef (saw_inputs st) + +baseSCType :: + sym -> + SC.SharedContext -> + BaseTypeRepr tp -> + IO SC.Term +baseSCType sym sc bt = + case bt of + BaseBoolRepr -> SC.scBoolType sc + BaseBVRepr w -> SC.scBitvector sc $ fromIntegral (natValue w) + BaseNatRepr -> SC.scNatType sc + BaseIntegerRepr -> SC.scIntegerType sc + BaseArrayRepr indexTypes range + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + SC.scArrayType sc sc_idx_type sc_elm_type + | otherwise -> + unsupported sym "SAW backend does not support multidimensional Arrays: baseSCType" + BaseFloatRepr _ -> + unsupported sym "SAW backend does not support IEEE-754 floating point values: baseSCType" + BaseStringRepr _ -> + unsupported sym "SAW backend does not support string values: baseSCType" + BaseComplexRepr -> + unsupported sym "SAW backend does not support complex values: baseSCType" + BaseRealRepr -> + unsupported sym "SAW backend does not support real values: baseSCType" + BaseStructRepr ts -> + SC.scTupleType sc =<< baseSCTypes ts + where + baseSCTypes :: Ctx.Assignment BaseTypeRepr args -> IO [SC.Term] + baseSCTypes Ctx.Empty = return [] + baseSCTypes (xs Ctx.:> x) = + do ts <- baseSCTypes xs + t <- baseSCType sym sc x + return (ts ++ [t]) + +-- | Create a new symbolic variable. +sawCreateVar :: SAWCoreState n + -> String -- ^ the name of the variable + -> SC.Term + -> IO SC.Term +sawCreateVar st nm tp = do + let sc = saw_ctx st + ec <- SC.scFreshEC sc nm tp + t <- SC.scFlatTermF sc (SC.ExtCns ec) + modifyIORef (saw_inputs st) (\xs -> xs Seq.|> ec) + return t + +bindSAWTerm :: + B.ExprBuilder n st fs -> + SAWCoreState n -> + BaseTypeRepr bt -> + SC.Term -> + IO (B.Expr n bt) +bindSAWTerm sym st bt t = do + ch_r <- readIORef $ saw_elt_cache_r st + let midx = + case t of + SC.STApp { SC.stAppIndex = idx } -> Just idx + SC.Unshared _ -> Nothing + case midx >>= flip IntMap.lookup ch_r of + Just (Some var) -> do + Just Refl <- return $ testEquality bt (B.exprType var) + return var + Nothing -> do + sbVar@(B.BoundVarExpr bv) <- freshConstant sym emptySymbol bt + B.insertIdxValue (saw_elt_cache st) (B.bvarId bv) (SAWExpr t) + case midx of + Just i -> modifyIORef' (saw_elt_cache_r st) $ IntMap.insert i (Some sbVar) + Nothing -> pure () + return sbVar + +-- | Register an interpretation for a symbolic function. This is not +-- used during simulation, but rather, when we translate Crucible +-- values back into SAW. The interpretation function takes a list of +-- arguments in regular (left-to-right) order. +sawRegisterSymFunInterp :: + SAWCoreState n -> + B.ExprSymFn n (B.Expr n) args ret -> + (SC.SharedContext -> [SC.Term] -> IO SC.Term) -> + IO () +sawRegisterSymFunInterp st f i = + modifyIORef (saw_symMap st) (Map.insert (indexValue (B.symFnId f)) i) + +toSC :: B.ExprBuilder n st fs -> SAWCoreState n -> B.Expr n tp -> IO SC.Term +toSC sym st elt = evaluateExpr sym st (saw_ctx st) (saw_elt_cache st) elt + + +-- | Create a Real SAWELT value from a Rational. +-- +-- This fails on non-integer expressions. +scRealLit :: + sym -> + SC.SharedContext -> + Rational -> + IO (SAWExpr BaseRealType) +scRealLit sym sc r + | denominator r /= 1 = + unsupported sym "SAW backend does not support real values" + | r >= 0 = + IntToRealSAWExpr . NatToIntSAWExpr . SAWExpr <$> SC.scNat sc (fromInteger (numerator r)) + | otherwise = + IntToRealSAWExpr <$> scIntLit sc (numerator r) + +-- | Create a SAWCore term with type 'Integer' from a Haskell Integer. +scIntLit :: SC.SharedContext -> Integer -> IO (SAWExpr BaseIntegerType) +scIntLit sc i + | i >= 0 = + SAWExpr <$> (SC.scNatToInt sc =<< SC.scNat sc (fromInteger i)) + | otherwise = + SAWExpr <$> (SC.scIntNeg sc =<< SC.scNatToInt sc =<< SC.scNat sc (fromInteger (negate i))) + +-- | Create a SAWCore term with type 'Nat' from a Haskell Nat. +scNatLit :: SC.SharedContext -> Natural -> IO (SAWExpr BaseNatType) +scNatLit sc n = SAWExpr <$> SC.scNat sc n + +scBvLit :: SC.SharedContext -> NatRepr w -> BV.BV w -> IO (SAWExpr (BaseBVType w)) +scBvLit sc w bv = SAWExpr <$> SC.scBvConst sc (natValue w) (BV.asUnsigned bv) + + +scRealCmpop :: + (SC.SharedContext -> SAWExpr BaseIntegerType -> SAWExpr BaseIntegerType -> IO (SAWExpr BaseBoolType)) -> + sym -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealCmpop intOp _ sc (IntToRealSAWExpr x) (IntToRealSAWExpr y) = + intOp sc x y +scRealCmpop _ sym _ _ _ = + unsupported sym "SAW backend does not support real values" + +scRealBinop :: + (SC.SharedContext -> SAWExpr BaseIntegerType -> SAWExpr BaseIntegerType -> IO (SAWExpr BaseIntegerType)) -> + sym -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scRealBinop intOp _ sc (IntToRealSAWExpr x) (IntToRealSAWExpr y) = + IntToRealSAWExpr <$> intOp sc x y +scRealBinop _ sym _ _ _ = + unsupported sym "SAW backend does not support real values" + + +scIntBinop :: + (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseNatType)) + {- ^ operation on naturals -} -> + (SC.SharedContext -> SC.Term -> SC.Term -> IO SC.Term) {- ^ operation on integers -} -> + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseIntegerType) +scIntBinop natOp _intOp sc (NatToIntSAWExpr x) (NatToIntSAWExpr y) = + NatToIntSAWExpr <$> natOp sc x y +scIntBinop _natOp intOp sc (NatToIntSAWExpr (SAWExpr x)) (SAWExpr y) = + SAWExpr <$> join (intOp sc <$> SC.scNatToInt sc x <*> pure y) +scIntBinop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = + SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) +scIntBinop _natOp intOp sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> intOp sc x y + +scIntCmpop :: + (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseBoolType)) + {- ^ operation on naturals -} -> + (SC.SharedContext -> SC.Term -> SC.Term -> IO SC.Term) {- ^ operation on integers -} -> + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseBoolType) +scIntCmpop natOp _intOp sc (NatToIntSAWExpr x) (NatToIntSAWExpr y) = + natOp sc x y +scIntCmpop _natOp intOp sc (NatToIntSAWExpr (SAWExpr x)) (SAWExpr y) = + SAWExpr <$> join (intOp sc <$> SC.scNatToInt sc x <*> pure y) +scIntCmpop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = + SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) +scIntCmpop _natOp intOp sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> intOp sc x y + +scAddReal :: + sym -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scAddReal = scRealBinop scAddInt + +scAddInt :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scAddInt = scIntBinop scAddNat SC.scIntAdd + +scAddNat :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scAddNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scAddNat sc x y + + +scMulReal :: + sym -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scMulReal = scRealBinop scMulInt + +scMulInt :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scMulInt = scIntBinop scMulNat SC.scIntMul + +scMulNat :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scMulNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scMulNat sc x y + +scIteReal :: + sym -> + SC.SharedContext -> + SC.Term -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scIteReal sym sc p = scRealBinop (\sc' -> scIteInt sc' p) sym sc + +scIteInt :: SC.SharedContext + -> SC.Term + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scIteInt sc p = scIntBinop + (\sc' -> scIteNat sc' p) + (\sc' x y -> SC.scIntegerType sc >>= \tp -> SC.scIte sc' tp p x y) + sc + +scIteNat :: SC.SharedContext + -> SC.Term + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scIteNat sc p (SAWExpr x) (SAWExpr y) = + SAWExpr <$> (SC.scNatType sc >>= \tp -> SC.scIte sc tp p x y) + +scIte :: + sym -> + SC.SharedContext -> + BaseTypeRepr tp -> + SAWExpr BaseBoolType -> + SAWExpr tp -> + SAWExpr tp -> + IO (SAWExpr tp) +scIte sym sc tp (SAWExpr p) x y = + case tp of + BaseRealRepr -> scIteReal sym sc p x y + BaseNatRepr -> scIteNat sc p x y + BaseIntegerRepr -> scIteInt sc p x y + _ -> + do tp' <- baseSCType sym sc tp + x' <- termOfSAWExpr sym sc x + y' <- termOfSAWExpr sym sc y + SAWExpr <$> SC.scIte sc tp' p x' y' + + +scRealEq :: + sym -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealEq = scRealCmpop scIntEq + +scIntEq :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseBoolType) +scIntEq = scIntCmpop scNatEq SC.scIntEq + +scNatEq :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseBoolType) +scNatEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scEqualNat sc x y + +scBoolEq :: + SC.SharedContext -> + SAWExpr BaseBoolType -> + SAWExpr BaseBoolType -> + IO (SAWExpr BaseBoolType) +scBoolEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scBoolEq sc x y + +scEq :: + sym -> + SC.SharedContext -> + BaseTypeRepr tp -> + SAWExpr tp -> + SAWExpr tp -> + IO (SAWExpr BaseBoolType) +scEq sym sc tp x y = + case tp of + BaseBoolRepr -> scBoolEq sc x y + BaseRealRepr -> scRealEq sym sc x y + BaseNatRepr -> scNatEq sc x y + BaseIntegerRepr -> scIntEq sc x y + BaseBVRepr w -> + do let SAWExpr x' = x + let SAWExpr y' = y + w' <- SC.scNat sc $ fromIntegral (natValue w) + SAWExpr <$> SC.scBvEq sc w' x' y' + _ -> unsupported sym ("SAW backend: equality comparison on unsupported type:" ++ show tp) + + +scRealLe, scRealLt :: + sym -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealLe = scRealCmpop scIntLe +scRealLt = scRealCmpop scIntLt + +scIntLe, scIntLt :: + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseBoolType) +scIntLe = scIntCmpop scNatLe SC.scIntLe +scIntLt = scIntCmpop scNatLt SC.scIntLt + +scNatLe, scNatLt :: + SC.SharedContext -> + SAWExpr BaseNatType -> + SAWExpr BaseNatType -> + IO (SAWExpr BaseBoolType) +scNatLe sc (SAWExpr x) (SAWExpr y) = + do lt <- SC.scLtNat sc x y + eq <- SC.scEqualNat sc x y + SAWExpr <$> SC.scOr sc lt eq +scNatLt sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> SC.scLtNat sc x y + +scBvAdd :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvAdd sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvAdd sc n x y + +scBvNot :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvNot sc w (SAWExpr x) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvNot sc n x + +scBvMul :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvMul sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvMul sc n x y + +scBvAnd :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvAnd sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvAnd sc n x y + +scBvXor :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvXor sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvXor sc n x y + +termOfSAWExpr :: + sym -> + SC.SharedContext -> + SAWExpr tp -> IO SC.Term +termOfSAWExpr sym sc expr = + case expr of + SAWExpr t -> return t + NatToIntSAWExpr (SAWExpr t) -> SC.scNatToInt sc t + IntToRealSAWExpr _ + -> unsupported sym "SAW backend does not support real values" + +applyExprSymFn :: + forall n st fs args ret. + B.ExprBuilder n st fs -> + SAWCoreState n -> + SC.SharedContext -> + B.ExprSymFn n (B.Expr n) args ret -> + Ctx.Assignment SAWExpr args -> + IO (SAWExpr ret) +applyExprSymFn sym st sc fn args = + do mp <- readIORef (saw_symMap st) + mk <- + case Map.lookup (indexValue (B.symFnId fn)) mp of + Nothing -> panic "SAWCore.applyExprSymFn" + [ "Unknown symbolic function." + , "*** Name: " ++ show fn + ] + Just mk -> return mk + ts <- evaluateAsgn args + SAWExpr <$> mk sc (reverse ts) + where + evaluateAsgn :: Ctx.Assignment SAWExpr args' -> IO [SC.Term] + evaluateAsgn Ctx.Empty = return [] + evaluateAsgn (xs Ctx.:> x) = + do vs <- evaluateAsgn xs + v <- termOfSAWExpr sym sc x + return (v : vs) + +{- | Declare that we don't support something or other. +This aborts the current path of execution, and adds a proof +obligation to ensure that we won't get there. +These proof obligations are all tagged with "Unsupported", so that +users of the library can choose if they will try to discharge them, +fail in some other way, or just ignore them. -} +unsupported :: {- OnlineSolver solver => -} sym -> String -> IO a +unsupported _sym x = fail ("Unsupported " <> x) -- TODO, something better here.... + + +evaluateExpr :: forall n st tp fs. + B.ExprBuilder n st fs-> + SAWCoreState n -> + SC.SharedContext -> + B.IdxCache n SAWExpr -> + B.Expr n tp -> + IO SC.Term +evaluateExpr sym st sc cache = f [] + where + -- Evaluate the element, and expect the result to have the same type. + f :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO SC.Term + f env elt = termOfSAWExpr sym sc =<< eval env elt + + eval :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') + eval env elt = B.idxCacheEval cache elt (go env elt) + + realFail :: IO a + realFail = unsupported sym "SAW backend does not support real values" + + cplxFail :: IO a + cplxFail = unsupported sym "SAW backend does not support complex values" + + floatFail :: IO a + floatFail = unsupported sym "SAW backend does not support floating-point values" + + stringFail :: IO a + stringFail = unsupported sym "SAW backend does not support string values" + + unimplemented :: String -> IO a + unimplemented x = unsupported sym $ "SAW backend: not implemented: " ++ x + + go :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') + + go _ (B.BoolExpr b _) = SAWExpr <$> SC.scBool sc b + + go _ (B.SemiRingLiteral sr x _) = + case sr of + B.SemiRingNatRepr -> scNatLit sc x + B.SemiRingBVRepr _ w -> scBvLit sc w x + B.SemiRingIntegerRepr -> scIntLit sc x + B.SemiRingRealRepr -> scRealLit sym sc x + + go _ (B.StringExpr{}) = + unsupported sym "SAW backend does not support string values" + + go env (B.BoundVarExpr bv) = + case B.bvarKind bv of + B.UninterpVarKind -> do + tp <- baseSCType sym sc (B.bvarType bv) + SAWExpr <$> sawCreateVar st nm tp + where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv + B.LatchVarKind -> + unsupported sym "SAW backend does not support latch variables" + B.QuantifierVarKind -> do + case elemIndex (Just $ B.bvarName bv) env of + Nothing -> unsupported sym $ "unbound quantifier variable " <> nm + Just idx -> SAWExpr <$> SC.scLocalVar sc idx + where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv + + go env (B.NonceAppExpr p) = + case B.nonceExprApp p of + B.Annotation _tpr _n x -> + eval env x + + B.Forall bvar body -> + case B.bvarType bvar of + BaseBVRepr wrepr -> do + w <- SC.scNat sc $ natValue wrepr + ty <- SC.scVecType sc w =<< SC.scBoolType sc + SAWExpr <$> + (SC.scBvForall sc w + =<< SC.scLambda sc nm ty =<< f (Just (B.bvarName bvar):env) body) + where nm = solverSymbolAsText $ B.bvarName bvar + _ -> unsupported sym "SAW backend only supports universal quantifiers over bitvectors" + B.Exists{} -> + unsupported sym "SAW backend does not support existential quantifiers" + B.ArrayFromFn{} -> unimplemented "ArrayFromFn" + B.MapOverArrays{} -> unimplemented "MapOverArrays" + B.ArrayTrueOnEntries{} -> unimplemented "ArrayTrueOnEntries" + B.FnApp fn asgn -> + do args <- traverseFC (eval env) asgn + applyExprSymFn sym st sc fn args + + go env a0@(B.AppExpr a) = + let nyi = unsupported sym $ + "Expression form not yet implemented in SAWCore backend:\n" + ++ show a0 + in + case B.appExprApp a of + B.BaseIte bt _ c xe ye -> join (scIte sym sc bt <$> eval env c <*> eval env xe <*> eval env ye) + B.BaseEq bt xe ye -> join (scEq sym sc bt <$> eval env xe <*> eval env ye) + + B.SemiRingLe sr xe ye -> + case sr of + B.OrderedSemiRingRealRepr -> join (scRealLe sym sc <$> eval env xe <*> eval env ye) + B.OrderedSemiRingIntegerRepr -> join (scIntLe sc <$> eval env xe <*> eval env ye) + B.OrderedSemiRingNatRepr -> join (scNatLe sc <$> eval env xe <*> eval env ye) + + B.NotPred x -> + goNeg env x + + B.ConjPred xs -> + case BM.viewBoolMap xs of + BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc True + BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc False + BM.BoolMapTerms (t:|ts) -> + let pol (x,BM.Positive) = f env x + pol (x,BM.Negative) = termOfSAWExpr sym sc =<< goNeg env x + in SAWExpr <$> join (foldM (SC.scAnd sc) <$> pol t <*> mapM pol ts) + + B.SemiRingProd pd -> + case WSum.prodRepr pd of + B.SemiRingRealRepr -> + do pd' <- WSum.prodEvalM (scMulReal sym sc) (eval env) pd + maybe (scRealLit sym sc 1) return pd' + B.SemiRingIntegerRepr -> + do pd' <- WSum.prodEvalM (scMulInt sc) (eval env) pd + maybe (scIntLit sc 1) return pd' + B.SemiRingNatRepr -> + do pd' <- WSum.prodEvalM (scMulNat sc) (eval env) pd + maybe (scNatLit sc 1) return pd' + B.SemiRingBVRepr B.BVArithRepr w -> + do n <- SC.scNat sc (natValue w) + pd' <- WSum.prodEvalM (SC.scBvMul sc n) (f env) pd + maybe (scBvLit sc w (BV.one w)) (return . SAWExpr) pd' + B.SemiRingBVRepr B.BVBitsRepr w -> + do n <- SC.scNat sc (natValue w) + pd' <- WSum.prodEvalM (SC.scBvAnd sc n) (f env) pd + maybe (scBvLit sc w (BV.maxUnsigned w)) (return . SAWExpr) pd' + + B.SemiRingSum ss -> + case WSum.sumRepr ss of + B.SemiRingRealRepr -> WSum.evalM add smul (scRealLit sym sc) ss + where add x y = scAddReal sym sc x y + smul 1 e = eval env e + smul sm e = join $ scMulReal sym sc <$> scRealLit sym sc sm <*> eval env e + B.SemiRingIntegerRepr -> WSum.evalM add smul (scIntLit sc) ss + where add x y = scAddInt sc x y + smul 1 e = eval env e + smul sm e = join $ scMulInt sc <$> scIntLit sc sm <*> eval env e + B.SemiRingNatRepr -> WSum.evalM add smul (scNatLit sc) ss + where add x y = scAddNat sc x y + smul 1 e = eval env e + smul sm e = join $ scMulNat sc <$> scNatLit sc sm <*> eval env e + B.SemiRingBVRepr B.BVArithRepr w -> WSum.evalM add smul (scBvLit sc w) ss + where add x y = scBvAdd sc w x y + smul (BV.BV 1) e = eval env e + smul sm e = join (scBvMul sc w <$> scBvLit sc w sm <*> eval env e) + B.SemiRingBVRepr B.BVBitsRepr w + | ss^.WSum.sumOffset == one -> scBvNot sc w =<< bitwise_eval (ss & WSum.sumOffset .~ BV.zero w) + | otherwise -> bitwise_eval ss + + where one = BV.maxUnsigned w + bitwise_eval = WSum.evalM add smul (scBvLit sc w) + add x y = scBvXor sc w x y + smul sm e + | sm == one = eval env e + | otherwise = join (scBvAnd sc w <$> scBvLit sc w sm <*> eval env e) + + B.RealIsInteger{} -> unsupported sym "SAW backend does not support real values" + + B.BVOrBits w bs -> + do n <- SC.scNat sc (natValue w) + bs' <- traverse (f env) (B.bvOrToList bs) + case bs' of + [] -> scBvLit sc w (BV.zero w) + x:xs -> SAWExpr <$> foldM (SC.scBvOr sc n) x xs + + B.BVFill w p -> + do bit <- SC.scBoolType sc + n <- SC.scNat sc (natValue w) + x <- f env p + SAWExpr <$> SC.scGlobalApply sc (SC.mkIdent SC.preludeName "replicate") [n, bit, x] + + B.BVTestBit i bv -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth bv)) + bit <- SC.scBoolType sc + -- NB, SAWCore's `scAt` is big endian + let j = natValue (bvWidth bv) - i - 1 + join (SC.scAt sc w bit <$> f env bv <*> SC.scNat sc j) + + B.BVSlt x y -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvSLt sc w <$> f env x <*> f env y) + B.BVUlt x y -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvULt sc w <$> f env x <*> f env y) + + B.BVUnaryTerm{} -> unsupported sym "SAW backend does not support the unary bitvector representation" + + B.BVUdiv _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvUDiv sc n <$> f env x <*> f env y) + B.BVUrem _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvURem sc n <$> f env x <*> f env y) + B.BVSdiv _ x y -> fmap SAWExpr $ do + -- NB: bvSDiv applies 'Succ' to its width argument, so we + -- need to subtract 1 to make the types match. + n <- SC.scNat sc (natValue (bvWidth x) - 1) + join (SC.scBvSDiv sc n <$> f env x <*> f env y) + B.BVSrem _ x y -> fmap SAWExpr $ do + -- NB: bvSDiv applies 'Succ' to its width argument, so we + -- need to subtract 1 to make the types match. + n <- SC.scNat sc (natValue (bvWidth x) - 1) + join (SC.scBvSRem sc n <$> f env x <*> f env y) + B.BVShl _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + n <- SC.scNat sc w + join (SC.scBvShl sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVLshr _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + n <- SC.scNat sc w + join (SC.scBvShr sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVAshr _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + -- NB: bvSShr applies a `Succ` to its width argument, so we subtract + -- 1 here to make things match up. + n <- SC.scNat sc (w - 1) + join (SC.scBvSShr sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVRol w x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue w) + bit <- SC.scBoolType sc + x' <- f env x + y' <- SC.scBvToNat sc (natValue w) =<< f env y + SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateL") [n,bit,x',y'] + B.BVRor w x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue w) + bit <- SC.scBoolType sc + x' <- f env x + y' <- SC.scBvToNat sc (natValue w) =<< f env y + SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateR") [n,bit,x',y'] + B.BVConcat _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + m <- SC.scNat sc (natValue (bvWidth y)) + t <- SC.scBoolType sc + join (SC.scAppend sc t n m <$> f env x <*> f env y) + B.BVSelect start num x -> fmap SAWExpr $ do + i <- SC.scNat sc (natValue (bvWidth x) - natValue num - natValue start) + n <- SC.scNat sc (natValue num) + o <- SC.scNat sc (natValue start) + t <- SC.scBoolType sc + x' <- f env x + SC.scSlice sc t i n o x' + B.BVZext w' x -> fmap SAWExpr $ do + let w = bvWidth x + n <- SC.scNat sc (natValue w) + m <- SC.scNat sc (natValue w' - natValue w) + x' <- f env x + SC.scBvUExt sc m n x' + B.BVSext w' x -> fmap SAWExpr $ do + let w = bvWidth x + -- NB: width - 1 to make SAWCore types work out + n <- SC.scNat sc (natValue w - 1) + m <- SC.scNat sc (natValue w' - natValue w) + x' <- f env x + SC.scBvSExt sc m n x' + B.BVPopcount w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvPopcount sc n x' + B.BVCountLeadingZeros w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvCountLeadingZeros sc n x' + B.BVCountTrailingZeros w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvCountTrailingZeros sc n x' + + -- Note: SAWCore supports only unidimensional arrays. As a result, What4 multidimensional + -- arrays cannot be translated to SAWCore. + B.ArrayMap indexTypes range updates arr + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + SAWExpr <$> foldM + (\sc_acc_arr (Ctx.Empty Ctx.:> idx_lit, elm) -> + do sc_idx <- f env =<< indexLit sym idx_lit + sc_elm <- f env elm + SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_acc_arr sc_idx sc_elm) + sc_arr + (AUM.toList updates) + | otherwise -> unimplemented "multidimensional ArrayMap" + + B.ConstantArray indexTypes range v + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_elm <- f env v + SAWExpr <$> SC.scArrayConstant sc sc_idx_type sc_elm_type sc_elm + | otherwise -> unimplemented "multidimensional ConstantArray" + + B.SelectArray range arr indexTerms + | Ctx.Empty Ctx.:> idx <- indexTerms + , idx_type <- exprType idx -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + sc_idx <- f env idx + SAWExpr <$> SC.scArrayLookup sc sc_idx_type sc_elm_type sc_arr sc_idx + | otherwise -> unimplemented "multidimensional SelectArray" + + B.UpdateArray range indexTypes arr indexTerms v + | Ctx.Empty Ctx.:> idx_type <- indexTypes + , Ctx.Empty Ctx.:> idx <- indexTerms -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + sc_idx <- f env idx + sc_elm <- f env v + SAWExpr <$> SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_arr sc_idx sc_elm + | otherwise -> unimplemented "multidimensional UpdateArray" + + B.NatToInteger x -> NatToIntSAWExpr <$> eval env x + B.IntegerToNat x -> + eval env x >>= \case + NatToIntSAWExpr z -> return z + SAWExpr z -> SAWExpr <$> (SC.scIntToNat sc z) + + B.NatDiv x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scDivNat sc x' y' + + B.NatMod x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scModNat sc x' y' + + B.IntDiv x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scIntDiv sc x' y' + B.IntMod x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scIntMod sc x' y' + B.IntAbs x -> + eval env x >>= \case + NatToIntSAWExpr z -> return (NatToIntSAWExpr z) + SAWExpr z -> SAWExpr <$> (SC.scIntAbs sc z) + + B.IntDivisible x 0 -> + do x' <- f env x + SAWExpr <$> (SC.scIntEq sc x' =<< SC.scIntegerConst sc 0) + B.IntDivisible x k -> + do x' <- f env x + k' <- SC.scIntegerConst sc (toInteger k) + z <- SC.scIntMod sc x' k' + SAWExpr <$> (SC.scIntEq sc z =<< SC.scIntegerConst sc 0) + + B.BVToNat x -> + let n = natValue (bvWidth x) in + SAWExpr <$> (SC.scBvToNat sc n =<< f env x) + + B.IntegerToBV x w -> + do n <- SC.scNat sc (natValue w) + SAWExpr <$> (SC.scIntToBv sc n =<< f env x) + + B.BVToInteger x -> + do n <- SC.scNat sc (natValue (bvWidth x)) + SAWExpr <$> (SC.scBvToInt sc n =<< f env x) + + B.SBVToInteger x -> + do n <- SC.scNat sc (natValue (bvWidth x)) + SAWExpr <$> (SC.scSbvToInt sc n =<< f env x) + + -- Proper support for real and complex numbers will require additional + -- work on the SAWCore side + B.IntegerToReal x -> IntToRealSAWExpr . SAWExpr <$> f env x + B.RealToInteger x -> + eval env x >>= \case + IntToRealSAWExpr x' -> return x' + _ -> realFail + + ------------------------------------------------------------------------ + -- Floating point operations + + B.FloatPZero{} -> floatFail + B.FloatNZero{} -> floatFail + B.FloatNaN{} -> floatFail + B.FloatPInf{} -> floatFail + B.FloatNInf{} -> floatFail + B.FloatNeg{} -> floatFail + B.FloatAbs{} -> floatFail + B.FloatSqrt{} -> floatFail + B.FloatAdd{} -> floatFail + B.FloatSub{} -> floatFail + B.FloatMul{} -> floatFail + B.FloatDiv{} -> floatFail + B.FloatRem{} -> floatFail + B.FloatMin{} -> floatFail + B.FloatMax{} -> floatFail + B.FloatFMA{} -> floatFail + B.FloatFpEq{} -> floatFail + B.FloatFpNe{} -> floatFail + B.FloatLe{} -> floatFail + B.FloatLt{} -> floatFail + B.FloatIsNaN{} -> floatFail + B.FloatIsInf{} -> floatFail + B.FloatIsZero{} -> floatFail + B.FloatIsPos{} -> floatFail + B.FloatIsNeg{} -> floatFail + B.FloatIsSubnorm{} -> floatFail + B.FloatIsNorm{} -> floatFail + B.FloatCast{} -> floatFail + B.FloatRound{} -> floatFail + B.FloatFromBinary{} -> floatFail + B.BVToFloat{} -> floatFail + B.SBVToFloat{} -> floatFail + B.RealToFloat{} -> floatFail + B.FloatToBV{} -> floatFail + B.FloatToSBV{} -> floatFail + B.FloatToReal{} -> floatFail + B.FloatToBinary{} -> floatFail + + B.RoundReal{} -> realFail + B.RoundEvenReal{} -> realFail + B.FloorReal{} -> realFail + B.CeilReal{} -> realFail + B.RealDiv{} -> realFail + B.RealSqrt{} -> realFail + B.Pi{} -> realFail + B.RealSin{} -> realFail + B.RealCos{} -> realFail + B.RealSinh{} -> realFail + B.RealCosh{} -> realFail + B.RealExp{} -> realFail + B.RealLog{} -> realFail + B.RealATan2{} -> realFail + + B.Cplx{} -> cplxFail + B.RealPart{} -> cplxFail + B.ImagPart{} -> cplxFail + + B.StringLength{} -> stringFail + B.StringAppend{} -> stringFail + B.StringContains{} -> stringFail + B.StringIsPrefixOf{} -> stringFail + B.StringIsSuffixOf{} -> stringFail + B.StringIndexOf{} -> stringFail + B.StringSubstring{} -> stringFail + + B.StructCtor{} -> nyi -- FIXME + B.StructField{} -> nyi -- FIXME + + -- returns the logical negation of the result of 'go' + -- negations are pushed inside conjunctions and less-than-or-equal + goNeg :: [Maybe SolverSymbol] -> B.Expr n BaseBoolType -> IO (SAWExpr BaseBoolType) + goNeg env expr = + case expr of + -- negation of (x /\ y) becomes (~x \/ ~y) + B.AppExpr (B.appExprApp -> B.ConjPred xs) -> + case BM.viewBoolMap xs of + BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc False + BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc True + BM.BoolMapTerms (t:|ts) -> + let pol (x, BM.Positive) = termOfSAWExpr sym sc =<< goNegAtom env x + pol (x, BM.Negative) = f env x + in SAWExpr <$> join (foldM (SC.scOr sc) <$> pol t <*> mapM pol ts) + _ -> goNegAtom env expr + + -- returns the logical negation of the result of 'go' + -- negations are pushed inside less-than-or-equal + goNegAtom :: [Maybe SolverSymbol] -> B.Expr n BaseBoolType -> IO (SAWExpr BaseBoolType) + goNegAtom env expr = + case expr of + -- negation of (x <= y) becomes (y < x) + B.AppExpr (B.appExprApp -> B.SemiRingLe sr xe ye) -> + case sr of + B.OrderedSemiRingRealRepr -> join (scRealLt sym sc <$> eval env ye <*> eval env xe) + B.OrderedSemiRingIntegerRepr -> join (scIntLt sc <$> eval env ye <*> eval env xe) + B.OrderedSemiRingNatRepr -> join (scNatLt sc <$> eval env ye <*> eval env xe) + _ -> SAWExpr <$> (SC.scNot sc =<< f env expr) + diff --git a/saw-core/saw-core.cabal b/saw-core/saw-core.cabal index 90761dc410..acdd17ec2a 100644 --- a/saw-core/saw-core.cabal +++ b/saw-core/saw-core.cabal @@ -91,9 +91,10 @@ library Verifier.SAW.Unique Verifier.SAW.UntypedAST Verifier.SAW.Change + Verifier.SAW.Utils other-modules: Verifier.SAW.UnionFind - Verifier.SAW.Utils + GHC-options: -Wall -Werror -Wcompat if impl(ghc == 8.0.1) ghc-options: -Wno-redundant-constraints