diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 60be46e8..ca7c216e 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -1367,6 +1367,7 @@ asCryptolTypeValue v = case v of SC.VBoolType -> return C.tBit SC.VIntType -> return C.tInteger + SC.VIntModType n -> return (C.tIntMod (C.tNum n)) SC.VArrayType v1 v2 -> do t1 <- asCryptolTypeValue v1 t2 <- asCryptolTypeValue v2 @@ -1461,7 +1462,7 @@ exportValue ty v = case ty of V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer") TV.TVIntMod _modulus -> - V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer") + V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod") TV.TVArray{} -> error $ "exportValue: (on array type " ++ show ty ++ ")" @@ -1533,6 +1534,7 @@ 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 FOVVec t vs | t == FOTBit -> V.VWord len (V.ready (V.LargeBitsVal len (V.finiteSeqMap V.Concrete . map (V.ready . V.VBit . fvAsBool) $ vs))) diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs index 4a92aee2..276244e6 100644 --- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs +++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs @@ -96,6 +96,7 @@ cryptolTypeOfFirstOrderType fot = case fot of FOTBit -> C.tBit FOTInt -> C.tInteger + FOTIntMod n -> C.tIntMod (C.tNum n) FOTVec n t -> C.tSeq (C.tNum n) (cryptolTypeOfFirstOrderType t) FOTTuple ts -> C.tTuple (map cryptolTypeOfFirstOrderType ts) FOTArray a b -> diff --git a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs index 7b11c20d..24f393b4 100644 --- a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs +++ b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs @@ -269,9 +269,8 @@ beConstMap be = , ("Prelude.bvToInt" , bvToIntOp be) , ("Prelude.sbvToInt", sbvToIntOp be) -- Integers mod n - , ("Prelude.IntMod" , constFun (TValue VIntType)) , ("Prelude.toIntMod" , toIntModOp) - , ("Prelude.fromIntMod", constFun (VFun force)) + , ("Prelude.fromIntMod", fromIntModOp) , ("Prelude.intModEq" , intModEqOp be) , ("Prelude.intModAdd" , intModBinOp (+)) , ("Prelude.intModSub" , intModBinOp (-)) @@ -353,27 +352,33 @@ toIntModOp :: BValue l toIntModOp = Prims.natFun $ \n -> return $ Prims.intFun "toIntModOp" $ \x -> return $ - VInt (x `mod` toInteger n) + VIntMod n (x `mod` toInteger n) + +fromIntModOp :: BValue l +fromIntModOp = + constFun $ + Prims.intModFun "fromIntModOp" $ \x -> return $ + VInt x intModEqOp :: AIG.IsAIG l g => g s -> BValue (l s) intModEqOp be = constFun $ - Prims.intFun "intModEqOp" $ \x -> return $ - Prims.intFun "intModEqOp" $ \y -> return $ + Prims.intModFun "intModEqOp" $ \x -> return $ + Prims.intModFun "intModEqOp" $ \y -> return $ VBool (AIG.constant be (x == y)) intModBinOp :: (Integer -> Integer -> Integer) -> BValue l intModBinOp f = Prims.natFun $ \n -> return $ - Prims.intFun "intModBinOp x" $ \x -> return $ - Prims.intFun "intModBinOp y" $ \y -> return $ - VInt (f x y `mod` toInteger n) + Prims.intModFun "intModBinOp x" $ \x -> return $ + Prims.intModFun "intModBinOp y" $ \y -> return $ + VIntMod n (f x y `mod` toInteger n) intModUnOp :: (Integer -> Integer) -> BValue l intModUnOp f = Prims.natFun $ \n -> return $ - Prims.intFun "intModUnOp" $ \x -> return $ - VInt (f x `mod` toInteger n) + Prims.intModFun "intModUnOp" $ \x -> return $ + VIntMod n (f x `mod` toInteger n) ---------------------------------------- diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index c51dc3ce..2c7943f9 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -196,8 +196,7 @@ constMap = , ("Prelude.bvToInt" , bvToIntOp) , ("Prelude.sbvToInt", sbvToIntOp) -- Integers mod n - , ("Prelude.IntMod" , constFun (TValue VIntType)) - , ("Prelude.toIntMod" , constFun (VFun force)) + , ("Prelude.toIntMod" , toIntModOp) , ("Prelude.fromIntMod", fromIntModOp) , ("Prelude.intModEq" , intModEqOp) , ("Prelude.intModAdd" , intModBinOp svPlus) @@ -262,6 +261,8 @@ flattenSValue v = do return (concat xss, concat ss) VBool sb -> return ([sb], "") VInt si -> return ([si], "") + VIntMod 0 si -> return ([si], "") + VIntMod n si -> return ([svRem si (svInteger KUnbounded (toInteger n))], "") VWord sw -> return (if intSizeOf sw > 0 then [sw] else [], "") VCtorApp i (V.toList->ts) -> do (xss, ss) <- unzip <$> traverse (force >=> flattenSValue) ts return (concat xss, "_" ++ identName i ++ concat ss) @@ -434,6 +435,12 @@ svShiftR b x i = svIte b (svNot (svShiftRight (svNot x) i)) (svShiftRight x i) ------------------------------------------------------------ -- Integers mod n +toIntModOp :: SValue +toIntModOp = + Prims.natFun' "toIntMod" $ \n -> pure $ + Prims.intFun "toIntMod" $ \x -> pure $ + VIntMod n x + fromIntModOp :: SValue fromIntModOp = Prims.natFun $ \n -> return $ @@ -443,23 +450,23 @@ fromIntModOp = intModEqOp :: SValue intModEqOp = Prims.natFun $ \n -> return $ - Prims.intFun "intModEqOp" $ \x -> return $ - Prims.intFun "intModEqOp" $ \y -> return $ + Prims.intModFun "intModEqOp" $ \x -> return $ + Prims.intModFun "intModEqOp" $ \y -> return $ let modulus = literalSInteger (toInteger n) in VBool (svEqual (svRem (svMinus x y) modulus) (literalSInteger 0)) intModBinOp :: (SInteger -> SInteger -> SInteger) -> SValue intModBinOp f = Prims.natFun $ \n -> return $ - Prims.intFun "intModBinOp x" $ \x -> return $ - Prims.intFun "intModBinOp y" $ \y -> return $ - VInt (normalizeIntMod n (f x y)) + Prims.intModFun "intModBinOp x" $ \x -> return $ + Prims.intModFun "intModBinOp y" $ \y -> return $ + VIntMod n (normalizeIntMod n (f x y)) intModUnOp :: (SInteger -> SInteger) -> SValue intModUnOp f = Prims.natFun $ \n -> return $ Prims.intFun "intModUnOp" $ \x -> return $ - VInt (normalizeIntMod n (f x)) + VIntMod n (normalizeIntMod n (f x)) normalizeIntMod :: Natural -> SInteger -> SInteger normalizeIntMod n x = @@ -584,6 +591,9 @@ parseUninterpreted cws nm ty = VIntType -> return $ vInteger $ mkUninterpreted KUnbounded cws nm + VIntModType n + -> return $ VIntMod n $ mkUninterpreted KUnbounded cws nm + (VVecType n VBoolType) -> return $ vWord $ mkUninterpreted (KBounded False (fromIntegral n)) cws nm @@ -630,6 +640,8 @@ vAsFirstOrderType v = -> return FOTBit VIntType -> return FOTInt + VIntModType n + -> return (FOTIntMod n) VVecType n v2 -> FOTVec n <$> vAsFirstOrderType v2 VUnitType @@ -701,6 +713,7 @@ newVarsForType v nm = newVars :: FirstOrderType -> StateT Int IO (Labeler, Symbolic SValue) newVars FOTBit = nextId <&> \s-> (BoolLabel s, vBool <$> existsSBool s) newVars FOTInt = nextId <&> \s-> (IntegerLabel s, vInteger <$> existsSInteger s) +newVars (FOTIntMod n) = nextId <&> \s-> (IntegerLabel s, VIntMod n <$> existsSInteger s) newVars (FOTVec n FOTBit) = if n == 0 then nextId <&> \s-> (WordLabel s, return (vWord (literalSWord 0 0))) @@ -722,6 +735,7 @@ newVars (FOTRec tm) = do newCodeGenVars :: (Natural -> Bool) -> FirstOrderType -> StateT Int IO (SBVCodeGen SValue) newCodeGenVars _checkSz FOTBit = nextId <&> \s -> (vBool <$> svCgInput KBool s) newCodeGenVars _checkSz FOTInt = nextId <&> \s -> (vInteger <$> svCgInput KUnbounded s) +newCodeGenVars _checkSz (FOTIntMod _) = nextId <&> \s -> (vInteger <$> svCgInput KUnbounded s) newCodeGenVars checkSz (FOTVec n FOTBit) | n == 0 = nextId <&> \_ -> return (vWord (literalSWord 0 0)) | checkSz n = nextId <&> \s -> vWord <$> cgInputSWord s (fromIntegral n) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index f2c3d63c..b9759c3e 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -49,6 +49,7 @@ module Verifier.SAW.Simulator.What4 , w4Eval , w4EvalAny , w4EvalBasic + , getLabelValues ) where @@ -80,9 +81,11 @@ import qualified Verifier.SAW.Simulator.Prims as Prims import Verifier.SAW.SharedTerm import Verifier.SAW.Simulator.Value import Verifier.SAW.TypedAST (FieldName, ModuleMap, identName) -import Verifier.SAW.FiniteValue (FirstOrderType(..)) +import Verifier.SAW.FiniteValue (FirstOrderType(..), FirstOrderValue(..)) -- what4 +import qualified What4.Expr.Builder as B +import What4.Expr.GroundEval import What4.Interface(SymExpr,Pred,SymInteger, IsExpr, IsExprBuilder,IsSymExprBuilder) import qualified What4.Interface as W @@ -250,8 +253,7 @@ constMap = , ("Prelude.bvToInt" , bvToIntOp) , ("Prelude.sbvToInt", sbvToIntOp) -- Integers mod n - , ("Prelude.IntMod" , constFun (TValue VIntType)) - , ("Prelude.toIntMod" , constFun (VFun force)) + , ("Prelude.toIntMod" , toIntModOp) , ("Prelude.fromIntMod", fromIntModOp sym) , ("Prelude.intModEq" , intModEqOp sym) , ("Prelude.intModAdd" , intModBinOp sym W.intAdd) @@ -455,17 +457,23 @@ intMax sym i1 i2 = do ------------------------------------------------------------ -- Integers mod n +toIntModOp :: SValue sym +toIntModOp = + Prims.natFun' "toIntMod" $ \n -> pure $ + Prims.intFun "toIntMod" $ \x -> pure $ + VIntMod n x + fromIntModOp :: IsExprBuilder sym => sym -> SValue sym fromIntModOp sym = Prims.natFun $ \n -> return $ Prims.intFun "fromIntModOp" $ \x -> - VInt <$> (W.intMod sym x =<< W.intLit sym (toInteger n)) + VIntMod n <$> (W.intMod sym x =<< W.intLit sym (toInteger n)) intModEqOp :: IsExprBuilder sym => sym -> SValue sym intModEqOp sym = Prims.natFun $ \n -> return $ - Prims.intFun "intModEqOp" $ \x -> return $ - Prims.intFun "intModEqOp" $ \y -> + Prims.intModFun "intModEqOp" $ \x -> return $ + Prims.intModFun "intModEqOp" $ \y -> do modulus <- W.intLit sym (toInteger n) d <- W.intSub sym x y r <- W.intMod sym d modulus @@ -477,17 +485,17 @@ intModBinOp :: (sym -> SInt sym -> SInt sym -> IO (SInt sym)) -> SValue sym intModBinOp sym f = Prims.natFun $ \n -> return $ - Prims.intFun "intModBinOp x" $ \x -> return $ - Prims.intFun "intModBinOp y" $ \y -> - VInt <$> (normalizeIntMod sym n =<< f sym x y) + Prims.intModFun "intModBinOp x" $ \x -> return $ + Prims.intModFun "intModBinOp y" $ \y -> + VIntMod n <$> (normalizeIntMod sym n =<< f sym x y) intModUnOp :: IsExprBuilder sym => sym -> (sym -> SInt sym -> IO (SInt sym)) -> SValue sym intModUnOp sym f = Prims.natFun $ \n -> return $ - Prims.intFun "intModUnOp" $ \x -> - VInt <$> (normalizeIntMod sym n =<< f sym x) + Prims.intModFun "intModUnOp" $ \x -> + VIntMod n <$> (normalizeIntMod sym n =<< f sym x) normalizeIntMod :: IsExprBuilder sym => sym -> Natural -> SInt sym -> IO (SInt sym) normalizeIntMod sym n x = @@ -723,7 +731,7 @@ parseUninterpreted sym ref app ty = VPiType _ f -> return $ strictFun $ \x -> do - app' <- applyUnintApp app x + app' <- applyUnintApp sym app x t2 <- f (ready x) parseUninterpreted sym ref app' t2 @@ -733,6 +741,9 @@ parseUninterpreted sym ref app ty = VIntType -> VInt <$> mkUninterpreted sym ref app BaseIntegerRepr + VIntModType n + -> VIntMod n <$> mkUninterpreted sym ref app BaseIntegerRepr + -- 0 width bitvector is a constant VVecType 0 VBoolType -> return $ VWord ZBV @@ -807,23 +818,29 @@ extendUnintApp (UnintApp nm xs tys) x ty = -- encode them as suffixes on the function name of the 'UnintApp'. applyUnintApp :: forall sym. + (W.IsExprBuilder sym) => + sym -> UnintApp (SymExpr sym) -> SValue sym -> IO (UnintApp (SymExpr sym)) -applyUnintApp app0 v = +applyUnintApp sym app0 v = case v of VUnit -> return app0 - VPair x y -> do app1 <- applyUnintApp app0 =<< force x - app2 <- applyUnintApp app1 =<< force y + VPair x y -> do app1 <- applyUnintApp sym app0 =<< force x + app2 <- applyUnintApp sym app1 =<< force y return app2 - VRecordValue elems -> foldM applyUnintApp app0 =<< traverse (force . snd) elems - VVector xv -> foldM applyUnintApp app0 =<< traverse force xv + VRecordValue elems -> foldM (applyUnintApp sym) app0 =<< traverse (force . snd) elems + VVector xv -> foldM (applyUnintApp sym) app0 =<< traverse force xv VBool sb -> return (extendUnintApp app0 sb BaseBoolRepr) VInt si -> return (extendUnintApp app0 si BaseIntegerRepr) + VIntMod 0 si -> return (extendUnintApp app0 si BaseIntegerRepr) + VIntMod n si -> do n' <- W.intLit sym (toInteger n) + si' <- W.intMod sym si n' + return (extendUnintApp app0 si' BaseIntegerRepr) VWord (DBV sw) -> return (extendUnintApp app0 sw (W.exprType sw)) VArray (SArray sa) -> return (extendUnintApp app0 sa (W.exprType sa)) VWord ZBV -> return app0 - VCtorApp i xv -> foldM applyUnintApp app' =<< traverse force xv + VCtorApp i xv -> foldM (applyUnintApp sym) app' =<< traverse force xv where app' = suffixUnintApp ("_" ++ identName i) app0 VNat n -> return (suffixUnintApp ("_" ++ show n) app0) TValue (suffixTValue -> Just s) @@ -884,7 +901,8 @@ argTypes :: IsSymExprBuilder sym => TValue (What4 sym) -> IO [TValue (What4 sym) argTypes v = case v of VPiType v1 f -> - do v2 <- f (error "argTypes: unsupported dependent SAW-Core type") + do x <- delay (fail "argTypes: unsupported dependent SAW-Core type") + v2 <- f x vs <- argTypes v2 return (v1 : vs) _ -> return [] @@ -899,6 +917,8 @@ vAsFirstOrderType v = -> return FOTBit VIntType -> return FOTInt + VIntModType n + -> return (FOTIntMod n) VVecType n v2 -> FOTVec n <$> vAsFirstOrderType v2 VArrayType iv ev @@ -928,17 +948,20 @@ data TypedExpr sym where TypedExpr :: BaseTypeRepr ty -> SymExpr sym ty -> TypedExpr sym +-- | Create a fresh constant with the given name and type. +mkConstant :: + forall sym ty. + (IsSymExprBuilder sym) => + sym -> String -> BaseTypeRepr ty -> IO (SymExpr sym ty) +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 = - case W.userSymbol str of - Right solverSymbol -> do - c <- W.freshConstant (given :: sym) solverSymbol ty - return (TypedExpr ty c) - Left _ -> - fail $ "Cannot create solver symbol " ++ str + do c <- mkConstant (given :: sym) str ty + return (TypedExpr ty c) nextId :: StateT Int IO String nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s)) @@ -962,10 +985,11 @@ myfun ::(Map String (Labeler sym, SValue sym)) -> (Map String (Labeler sym), Map myfun = fmap fst A.&&& fmap snd data Labeler sym - = BaseLabel (TypedExpr sym) - | VecLabel (Vector (Labeler sym)) - | TupleLabel (Vector (Labeler sym)) - | RecLabel (Map FieldName (Labeler sym)) + = BaseLabel (TypedExpr sym) + | IntModLabel Natural (SymInteger sym) + | VecLabel (Vector (Labeler sym)) + | TupleLabel (Vector (Labeler sym)) + | RecLabel (Map FieldName (Labeler sym)) newVarFOT :: forall sym. (IsSymExprBuilder sym, Given sym) => @@ -987,6 +1011,12 @@ newVarFOT (FOTRec tm) args <- traverse (return . ready) (vals :: (Map String (SValue sym))) return (RecLabel labels, vRecord args) +newVarFOT (FOTIntMod n) + = do nm <- nextId + let r = BaseIntegerRepr + si <- lift $ mkConstant (given :: sym) nm r + return (IntModLabel n si, VIntMod n si) + newVarFOT fot | Some r <- fotToBaseType fot = do nm <- nextId @@ -1000,6 +1030,27 @@ typedToSValue :: (IsExpr (SymExpr sym)) => TypedExpr sym -> IO (SValue sym) typedToSValue (TypedExpr ty expr) = maybe (fail "Cannot handle") return $ symExprToValue ty expr +getLabelValues :: + forall sym t. + (SymExpr sym ~ B.Expr t) => + GroundEvalFn t -> Labeler sym -> IO FirstOrderValue +getLabelValues f = + \case + TupleLabel labels -> + FOVTuple <$> traverse (getLabelValues f) (V.toList labels) + VecLabel labels -> + FOVVec vty <$> traverse (getLabelValues f) (V.toList labels) + where vty = error "TODO: compute vector type, or just store it" + RecLabel labels -> + FOVRec <$> traverse (getLabelValues f) labels + IntModLabel n x -> + FOVIntMod n <$> groundEval f x + BaseLabel (TypedExpr ty bv) -> + do gv <- groundEval f bv + case (groundToFOV ty gv) of + Left err -> fail err + Right fov -> pure fov + ---------------------------------------------------------------------- -- Evaluation through crucible-saw backend @@ -1093,7 +1144,7 @@ parseUninterpretedSAW sym sc ref trm app ty = VPiType t1 f -> return $ strictFun $ \x -> do - app' <- applyUnintApp app x + app' <- applyUnintApp sym app x arg <- mkArgTerm sc t1 x let trm' = ArgTermApply trm arg t2 <- f (ready x) 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 1d62689a..a7273611 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs @@ -48,6 +48,8 @@ fotToBaseType FOTBit = Some BaseBoolRepr fotToBaseType FOTInt = Some BaseIntegerRepr +fotToBaseType (FOTIntMod _n) + = Some BaseIntegerRepr fotToBaseType (FOTVec nat FOTBit) | Just (Some (PosNat nr)) <- somePosNat nat = Some (BaseBVRepr nr) @@ -124,4 +126,4 @@ tupleToList (viewAssign -> AssignExtend rs r) (viewAssign -> AssignExtend gvs gv (:) <$> groundToFOV r (unGVW gv) <*> tupleToList rs gvs #if !MIN_VERSION_GLASGOW_HASKELL(8,10,0,0) tupleToList _ _ = error "GADTs should rule this out." -#endif \ No newline at end of file +#endif diff --git a/saw-core/src/Verifier/SAW/FiniteValue.hs b/saw-core/src/Verifier/SAW/FiniteValue.hs index 4f249d9c..292f9069 100644 --- a/saw-core/src/Verifier/SAW/FiniteValue.hs +++ b/saw-core/src/Verifier/SAW/FiniteValue.hs @@ -48,6 +48,7 @@ data FiniteValue data FirstOrderType = FOTBit | FOTInt + | FOTIntMod Natural | FOTVec Natural FirstOrderType | FOTArray FirstOrderType FirstOrderType | FOTTuple [FirstOrderType] @@ -58,6 +59,7 @@ data FirstOrderType data FirstOrderValue = FOVBit Bool | FOVInt Integer + | FOVIntMod Natural Integer | FOVWord Natural Integer -- ^ a more efficient special case for 'FOVVec FOTBit _'. | FOVVec FirstOrderType [FirstOrderValue] | FOVArray FirstOrderType FirstOrderType @@ -90,6 +92,7 @@ instance Show FirstOrderValue where case fv of FOVBit b -> shows b FOVInt i -> shows i + FOVIntMod _ i -> shows i FOVWord _ x -> shows x FOVVec _ vs -> showString "[" . commaSep (map shows vs) . showString "]" FOVArray{} -> shows $ firstOrderTypeOf fv @@ -110,6 +113,7 @@ ppFirstOrderValue opts = loop | b -> text "True" | otherwise -> text "False" FOVInt i -> integer i + FOVIntMod _ i -> integer i FOVWord _w i -> ppNat opts i FOVVec _ xs -> brackets (sep (punctuate comma (map loop xs))) FOVArray{} -> text $ show $ firstOrderTypeOf fv @@ -160,6 +164,7 @@ firstOrderTypeOf fv = case fv of FOVBit _ -> FOTBit FOVInt _ -> FOTInt + FOVIntMod n _ -> FOTIntMod n FOVWord n _ -> FOTVec n FOTBit FOVVec t vs -> FOTVec (fromIntegral (length vs)) t -- Note: FOVArray contains type information, but not an actual Array value, @@ -201,6 +206,8 @@ asFirstOrderType sc t = do -> return FOTBit (R.asIntegerType -> Just ()) -> return FOTInt + (R.asIntModType -> Just n) + -> return (FOTIntMod n) (R.isVecType return -> Just (n R.:*: tp)) -> FOTVec n <$> asFirstOrderType sc tp (R.asArrayType -> Just (tp1 R.:*: tp2)) -> do @@ -237,6 +244,7 @@ scFirstOrderType sc ft = case ft of FOTBit -> scBoolType sc FOTInt -> scIntegerType sc + FOTIntMod n -> scIntModType sc =<< scNat sc n FOTVec n t -> do n' <- scNat sc n t' <- scFirstOrderType sc t scVecType sc n' t' @@ -259,6 +267,13 @@ scFirstOrderValue sc fv = FOVInt i | i >= 0 -> scNatToInt sc =<< scNat sc (fromInteger i) | True -> scIntNeg sc =<< scNatToInt sc =<< scNat sc (fromInteger (- i)) + FOVIntMod 0 i -> + do n' <- scNat sc 0 + scToIntMod sc n' =<< scFirstOrderValue sc (FOVInt i) + FOVIntMod n i -> + do n' <- scNat sc n + i' <- scNatToInt sc =<< scNat sc (fromInteger (i `mod` toInteger n)) + scToIntMod sc n' i' FOVWord n x -> scBvConst sc n x FOVVec t vs -> do t' <- scFirstOrderType sc t vs' <- traverse (scFirstOrderValue sc) vs diff --git a/saw-core/src/Verifier/SAW/Recognizer.hs b/saw-core/src/Verifier/SAW/Recognizer.hs index 9543721a..8190f949 100644 --- a/saw-core/src/Verifier/SAW/Recognizer.hs +++ b/saw-core/src/Verifier/SAW/Recognizer.hs @@ -59,6 +59,7 @@ module Verifier.SAW.Recognizer , asBool , asBoolType , asIntegerType + , asIntModType , asBitvectorType , asVectorType , asVecType @@ -343,6 +344,9 @@ asBoolType = isGlobalDef "Prelude.Bool" asIntegerType :: Recognizer Term () asIntegerType = isGlobalDef "Prelude.Integer" +asIntModType :: Recognizer Term Natural +asIntModType = isGlobalDef "Prelude.IntMod" @> asNat + asVectorType :: Recognizer Term (Term, Term) asVectorType = helper ((isGlobalDef "Prelude.Vec" @> return) <@> return) where helper r t = diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index b7c4f9ce..b8b0ae12 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -170,6 +170,9 @@ module Verifier.SAW.SharedTerm , scIntEq, scIntLe, scIntLt , scIntToNat, scNatToInt , scIntToBv, scBvToInt, scSbvToInt + -- *** IntMod + , scIntModType + , scToIntMod -- *** Vectors , scAppend , scJoin @@ -1699,6 +1702,21 @@ scSbvToInt scSbvToInt sc n x = scGlobalApply sc "Prelude.sbvToInt" [n,x] +-- Primitive operations on IntMod + +-- | Create a term representing the prelude @IntMod@ type. +-- +-- > IntMod : Nat -> sort 0; +scIntModType :: SharedContext -> Term -> IO Term +scIntModType sc n = scGlobalApply sc "Prelude.IntMod" [n] + +-- | Convert an integer to an integer mod n. +-- +-- > toIntMod : (n : Nat) -> Integer -> IntMod n; +scToIntMod :: SharedContext -> Term -> Term -> IO Term +scToIntMod sc n x = scGlobalApply sc "Prelude.toIntMod" [n, x] + + -- Primitive operations on bitvectors -- | Create a term computing the type of a length-n bitvector. diff --git a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs index b8fac5a2..2f76992c 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs +++ b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs @@ -253,7 +253,6 @@ constMap = , ("Prelude.bvToInt" , bvToIntOp) , ("Prelude.sbvToInt", sbvToIntOp) -- Integers mod n - , ("Prelude.IntMod" , constFun (TValue VIntType)) , ("Prelude.toIntMod" , toIntModOp) , ("Prelude.fromIntMod", constFun (VFun force)) , ("Prelude.intModEq" , intModEqOp) @@ -319,27 +318,27 @@ toIntModOp :: CValue toIntModOp = Prims.natFun $ \n -> return $ Prims.intFun "toIntModOp" $ \x -> return $ - VInt (x `mod` toInteger n) + VIntMod n (x `mod` toInteger n) intModEqOp :: CValue intModEqOp = constFun $ - Prims.intFun "intModEqOp" $ \x -> return $ - Prims.intFun "intModEqOp" $ \y -> return $ + Prims.intModFun "intModEqOp" $ \x -> return $ + Prims.intModFun "intModEqOp" $ \y -> return $ VBool (x == y) intModBinOp :: (Integer -> Integer -> Integer) -> CValue intModBinOp f = Prims.natFun $ \n -> return $ - Prims.intFun "intModBinOp x" $ \x -> return $ - Prims.intFun "intModBinOp y" $ \y -> return $ - VInt (f x y `mod` toInteger n) + Prims.intModFun "intModBinOp x" $ \x -> return $ + Prims.intModFun "intModBinOp y" $ \y -> return $ + VIntMod n (f x y `mod` toInteger n) intModUnOp :: (Integer -> Integer) -> CValue intModUnOp f = Prims.natFun $ \n -> return $ - Prims.intFun "intModUnOp" $ \x -> return $ - VInt (f x `mod` toInteger n) + Prims.intModFun "intModUnOp" $ \x -> return $ + VIntMod n (f x `mod` toInteger n) ------------------------------------------------------------ diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs index 5131e532..7666a582 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Prims.hs +++ b/saw-core/src/Verifier/SAW/Simulator/Prims.hs @@ -226,6 +226,8 @@ constMap bp = Map.fromList -} , ("Prelude.intMin", intBinOp "intMin" (bpIntMin bp)) , ("Prelude.intMax", intBinOp "intMax" (bpIntMax bp)) + -- Modular Integers + , ("Prelude.IntMod", natFun $ \n -> pure $ TValue (VIntModType n)) -- Vectors , ("Prelude.Vec", vecTypeOp) , ("Prelude.gen", genOp) @@ -295,6 +297,11 @@ intFun msg f = strictFun g where g (VInt i) = f i g _ = panic $ "expected Integer "++ msg +intModFun :: VMonad l => String -> (VInt l -> MValue l) -> Value l +intModFun msg f = strictFun g + where g (VIntMod _ i) = f i + g _ = panic $ "expected IntMod "++ msg + toBool :: Show (Extra l) => Value l -> VBool l toBool (VBool b) = b toBool x = panic $ unwords ["Verifier.SAW.Simulator.toBool", show x] @@ -1249,6 +1256,7 @@ muxValue bp b = value value (VBool x) (VBool y) = VBool <$> bpMuxBool bp b x y value (VWord x) (VWord y) = VWord <$> bpMuxWord bp b x y value (VInt x) (VInt y) = VInt <$> bpMuxInt bp b x y + value (VIntMod n x) (VIntMod _ y) = VIntMod n <$> bpMuxInt bp b x y value (VNat m) (VNat n) | m == n = return $ VNat m value (VString x) (VString y) | x == y = return $ VString x value (VFloat x) (VFloat y) | x == y = return $ VFloat x diff --git a/saw-core/src/Verifier/SAW/Simulator/RME.hs b/saw-core/src/Verifier/SAW/Simulator/RME.hs index 0135b6ba..1991f1ee 100644 --- a/saw-core/src/Verifier/SAW/Simulator/RME.hs +++ b/saw-core/src/Verifier/SAW/Simulator/RME.hs @@ -240,9 +240,8 @@ constMap = , ("Prelude.bvToInt" , bvToIntOp) , ("Prelude.sbvToInt", sbvToIntOp) -- Integers mod n - , ("Prelude.IntMod" , constFun (TValue VIntType)) , ("Prelude.toIntMod" , toIntModOp) - , ("Prelude.fromIntMod", constFun (VFun force)) + , ("Prelude.fromIntMod", fromIntModOp) , ("Prelude.intModEq" , intModEqOp) , ("Prelude.intModAdd" , intModBinOp (+)) , ("Prelude.intModSub" , intModBinOp (-)) @@ -301,27 +300,33 @@ toIntModOp :: RValue toIntModOp = Prims.natFun $ \n -> return $ Prims.intFun "toIntModOp" $ \x -> return $ - VInt (x `mod` toInteger n) + VIntMod n (x `mod` toInteger n) + +fromIntModOp :: RValue +fromIntModOp = + constFun $ + Prims.intModFun "fromIntModOp" $ \x -> return $ + VInt x intModEqOp :: RValue intModEqOp = constFun $ - Prims.intFun "intModEqOp" $ \x -> return $ - Prims.intFun "intModEqOp" $ \y -> return $ + Prims.intModFun "intModEqOp" $ \x -> return $ + Prims.intModFun "intModEqOp" $ \y -> return $ VBool (RME.constant (x == y)) intModBinOp :: (Integer -> Integer -> Integer) -> RValue intModBinOp f = Prims.natFun $ \n -> return $ - Prims.intFun "intModBinOp x" $ \x -> return $ - Prims.intFun "intModBinOp y" $ \y -> return $ - VInt (f x y `mod` toInteger n) + Prims.intModFun "intModBinOp x" $ \x -> return $ + Prims.intModFun "intModBinOp y" $ \y -> return $ + VIntMod n (f x y `mod` toInteger n) intModUnOp :: (Integer -> Integer) -> RValue intModUnOp f = Prims.natFun $ \n -> return $ - Prims.intFun "intModUnOp" $ \x -> return $ - VInt (f x `mod` toInteger n) + Prims.intModFun "intModUnOp" $ \x -> return $ + VIntMod n (f x `mod` toInteger n) ---------------------------------------- diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs index 12c94923..34030ed5 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Value.hs +++ b/saw-core/src/Verifier/SAW/Simulator/Value.hs @@ -56,6 +56,7 @@ data Value l | VToNat (Value l) | VNat !Natural | VInt (VInt l) + | VIntMod !Natural (VInt l) | VArray (VArray l) | VString !String | VFloat !Float @@ -69,6 +70,7 @@ data TValue l = VVecType !Natural !(TValue l) | VBoolType | VIntType + | VIntModType !Natural | VArrayType !(TValue l) !(TValue l) | VPiType !(TValue l) !(Thunk l -> EvalM l (TValue l)) | VUnitType @@ -155,6 +157,7 @@ instance Show (Extra l) => Show (Value l) where VToNat x -> showString "bvToNat " . showParen True (shows x) VNat n -> shows n VInt _ -> showString "<>" + VIntMod n _ -> showString ("<>") VArray{} -> showString "<>" VFloat float -> shows float VDouble double -> shows double @@ -172,6 +175,7 @@ instance Show (Extra l) => Show (TValue l) where case v of VBoolType -> showString "Bool" VIntType -> showString "Integer" + VIntModType n -> showParen True (showString "IntMod " . shows n) VArrayType{} -> showString "Array" VPiType t _ -> showParen True (shows t . showString " -> ...") @@ -271,6 +275,7 @@ suffixTValue tv = Just ("_Vec_" ++ show n ++ a') VBoolType -> Just "_Bool" VIntType -> Just "_Int" + VIntModType n -> Just ("_IntMod_" ++ show n) VArrayType a b -> do a' <- suffixTValue a b' <- suffixTValue b